%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP593-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 : n017.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:30:26 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.41s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 3
% Syntax : Number of formulae : 208 ( 208 unt; 0 def)
% Number of atoms : 208 ( 207 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 9 ( 9 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 758 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : inverse(double_divide(double_divide(VAR_0,VAR_1),inverse(double_divide(VAR_0,inverse(double_divide(VAR_2,VAR_1)))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(C,B)))))) = C,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(multiply,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_1) = inverse(double_divide(VAR_1,VAR_0)),
file('theBenchmark.p',multiply) ).
cnf(c_2,plain,
multiply(A,B) = inverse(double_divide(B,A)),
inference(clausify,[status(thm)],[multiply]) ).
fof(prove_these_axioms_1,axiom,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('theBenchmark.p',prove_these_axioms_1) ).
cnf(c_3,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(clausify,[status(thm)],[prove_these_axioms_1]) ).
cnf(c_412,plain,
inverse(double_divide(a1,inverse(a1))) != multiply(inverse(b1),b1),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_413,plain,
inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))),
inference(paramod,[status(thm)],[c_2,c_412]) ).
cnf(c_4,plain,
inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))),
inference(copy,[status(thm)],[c_413]) ).
cnf(c_5,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,D))))),inverse(double_divide(A,C)))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_6,plain,
inverse(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,B))),C)) = A,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_7,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,double_divide(D,E))))) = double_divide(B,inverse(double_divide(D,inverse(double_divide(C,E))))),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_9,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))) = double_divide(double_divide(C,D),inverse(double_divide(B,D))),
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_13,plain,
inverse(double_divide(double_divide(double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(C,D)),B))),D),A)) = C,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_14,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))) = double_divide(double_divide(double_divide(B,D),inverse(double_divide(inverse(double_divide(C,E)),D))),E),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_414,plain,
A = double_divide(inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)),C),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_16,plain,
double_divide(inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)),C) = A,
inference(copy,[status(thm)],[c_414]) ).
cnf(c_19,plain,
double_divide(double_divide(inverse(double_divide(A,B)),C),inverse(double_divide(B,C))) = A,
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_25,plain,
inverse(double_divide(double_divide(A,double_divide(double_divide(B,C),inverse(double_divide(D,C)))),inverse(double_divide(A,E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_9,c_5]) ).
cnf(c_35,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(inverse(double_divide(double_divide(C,D),A)),D)),B))) = C,
inference(paramod,[status(thm)],[c_9,c_6]) ).
cnf(c_38,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))),B)) = C,
inference(paramod,[status(thm)],[c_9,c_6]) ).
cnf(c_41,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,B))) = double_divide(double_divide(A,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_9,c_9]) ).
cnf(c_45,plain,
inverse(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B))))) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_9,c_9]) ).
cnf(c_51,plain,
inverse(double_divide(double_divide(double_divide(inverse(double_divide(A,B)),C),C),inverse(A))) = B,
inference(paramod,[status(thm)],[c_19,c_1]) ).
cnf(c_59,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,D))))),B)) = double_divide(inverse(double_divide(A,C)),D),
inference(paramod,[status(thm)],[c_19,c_6]) ).
cnf(c_63,plain,
inverse(double_divide(double_divide(double_divide(inverse(double_divide(A,B)),C),D),inverse(A))) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_19,c_9]) ).
cnf(c_65,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(double_divide(B,C)),D)),inverse(double_divide(A,E)))) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_19,c_9]) ).
cnf(c_415,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(double_divide(B,C),inverse(double_divide(D,C))))),inverse(double_divide(A,D)))) = double_divide(double_divide(B,E),E),
inference(paramod,[status(thm)],[c_41,c_5]) ).
cnf(c_76,plain,
double_divide(double_divide(A,B),B) = double_divide(double_divide(A,C),C),
inference(paramod,[status(thm)],[c_5,c_415]) ).
cnf(c_77,plain,
inverse(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,B))),inverse(double_divide(double_divide(A,inverse(double_divide(D,E))),D)))) = double_divide(C,E),
inference(paramod,[status(thm)],[c_41,c_5]) ).
cnf(c_416,plain,
double_divide(double_divide(A,B),C) = double_divide(double_divide(A,D),inverse(double_divide(double_divide(double_divide(C,E),inverse(double_divide(B,E))),D))),
inference(paramod,[status(thm)],[c_6,c_41]) ).
cnf(c_81,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(double_divide(C,D),inverse(double_divide(E,D))),B))) = double_divide(double_divide(A,E),C),
inference(copy,[status(thm)],[c_416]) ).
cnf(c_86,plain,
inverse(double_divide(double_divide(A,double_divide(B,C)),inverse(double_divide(A,D)))) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(double_divide(B,F),inverse(double_divide(E,F))))),
inference(paramod,[status(thm)],[c_41,c_9]) ).
cnf(c_94,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(double_divide(D,E),inverse(double_divide(B,E))))) = double_divide(double_divide(A,F),inverse(double_divide(double_divide(D,C),F))),
inference(paramod,[status(thm)],[c_41,c_41]) ).
cnf(c_104,plain,
inverse(double_divide(double_divide(double_divide(A,B),B),inverse(double_divide(double_divide(A,C),D)))) = double_divide(double_divide(D,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_76,c_9]) ).
cnf(c_105,plain,
inverse(double_divide(double_divide(double_divide(A,B),C),inverse(double_divide(double_divide(A,D),D)))) = double_divide(double_divide(B,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_76,c_9]) ).
cnf(c_417,plain,
double_divide(double_divide(double_divide(A,B),B),C) = double_divide(double_divide(double_divide(A,C),D),D),
inference(paramod,[status(thm)],[c_76,c_76]) ).
cnf(c_116,plain,
double_divide(double_divide(double_divide(A,B),C),C) = double_divide(double_divide(double_divide(A,D),D),B),
inference(copy,[status(thm)],[c_417]) ).
cnf(c_177,plain,
inverse(double_divide(double_divide(A,double_divide(double_divide(B,C),D)),inverse(double_divide(A,E)))) = double_divide(double_divide(E,D),inverse(double_divide(double_divide(double_divide(B,F),F),C))),
inference(paramod,[status(thm)],[c_116,c_9]) ).
cnf(c_184,plain,
double_divide(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))),D),D) = double_divide(double_divide(double_divide(double_divide(C,E),F),F),inverse(double_divide(B,E))),
inference(paramod,[status(thm)],[c_9,c_116]) ).
cnf(c_189,plain,
double_divide(double_divide(inverse(double_divide(A,double_divide(double_divide(B,C),C))),D),inverse(double_divide(double_divide(double_divide(B,D),E),E))) = A,
inference(paramod,[status(thm)],[c_116,c_19]) ).
cnf(c_418,plain,
double_divide(A,inverse(double_divide(B,C))) = double_divide(double_divide(double_divide(inverse(double_divide(A,B)),D),D),C),
inference(paramod,[status(thm)],[c_19,c_116]) ).
cnf(c_190,plain,
double_divide(double_divide(double_divide(inverse(double_divide(A,B)),C),C),D) = double_divide(A,inverse(double_divide(B,D))),
inference(copy,[status(thm)],[c_418]) ).
cnf(c_222,plain,
inverse(double_divide(A,inverse(double_divide(B,inverse(A))))) = B,
inference(paramod,[status(thm)],[c_190,c_51]) ).
cnf(c_226,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)) = double_divide(A,C),
inference(paramod,[status(thm)],[c_1,c_222]) ).
cnf(c_229,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(inverse(double_divide(C,inverse(A))),D))))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_222,c_5]) ).
cnf(c_231,plain,
inverse(double_divide(double_divide(A,B),double_divide(C,D))) = double_divide(A,inverse(double_divide(C,inverse(double_divide(B,D))))),
inference(paramod,[status(thm)],[c_5,c_222]) ).
cnf(c_419,plain,
inverse(double_divide(A,B)) = double_divide(double_divide(B,C),inverse(double_divide(inverse(A),C))),
inference(paramod,[status(thm)],[c_6,c_222]) ).
cnf(c_234,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(C),B))) = inverse(double_divide(C,A)),
inference(copy,[status(thm)],[c_419]) ).
cnf(c_241,plain,
inverse(double_divide(double_divide(A,B),inverse(C))) = double_divide(inverse(double_divide(C,A)),B),
inference(paramod,[status(thm)],[c_19,c_222]) ).
cnf(c_420,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(double_divide(C,D),inverse(double_divide(A,D)))))) = double_divide(C,B),
inference(paramod,[status(thm)],[c_41,c_222]) ).
cnf(c_421,plain,
inverse(double_divide(double_divide(A,B),double_divide(inverse(double_divide(double_divide(A,D),C)),D))) = double_divide(C,B),
inference(paramod,[status(thm)],[c_241,c_420]) ).
cnf(c_243,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),inverse(double_divide(D,B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_231,c_421]) ).
cnf(c_422,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,double_divide(C,D))))) = double_divide(E,inverse(double_divide(C,inverse(double_divide(inverse(double_divide(B,inverse(E))),D))))),
inference(paramod,[status(thm)],[c_222,c_7]) ).
cnf(c_246,plain,
double_divide(inverse(double_divide(double_divide(A,double_divide(B,C)),A)),D) = double_divide(E,inverse(double_divide(B,inverse(double_divide(inverse(double_divide(D,inverse(E))),C))))),
inference(paramod,[status(thm)],[c_241,c_422]) ).
cnf(c_423,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,double_divide(D,inverse(D)))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_222,c_7]) ).
cnf(c_248,plain,
double_divide(inverse(double_divide(double_divide(A,double_divide(B,inverse(B))),A)),inverse(double_divide(C,D))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_241,c_423]) ).
cnf(c_424,plain,
inverse(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,B))),double_divide(A,E))) = double_divide(C,E),
inference(paramod,[status(thm)],[c_226,c_77]) ).
cnf(c_255,plain,
double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(inverse(double_divide(C,B)),D))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_231,c_424]) ).
cnf(c_425,plain,
double_divide(A,inverse(double_divide(C,D))) = double_divide(inverse(double_divide(A,C)),D),
inference(paramod,[status(thm)],[c_226,c_59]) ).
cnf(c_256,plain,
double_divide(inverse(double_divide(A,B)),C) = double_divide(A,inverse(double_divide(B,C))),
inference(copy,[status(thm)],[c_425]) ).
cnf(c_259,plain,
double_divide(double_divide(A,B),B) = A,
inference(paramod,[status(thm)],[c_226,c_16]) ).
cnf(c_426,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(double_divide(C,D),inverse(double_divide(A,D)))),B))) = C,
inference(paramod,[status(thm)],[c_256,c_35]) ).
cnf(c_427,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(inverse(double_divide(double_divide(A,D),C)),D),B))) = C,
inference(paramod,[status(thm)],[c_241,c_426]) ).
cnf(c_428,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(double_divide(A,D),inverse(double_divide(C,D))),B))) = C,
inference(paramod,[status(thm)],[c_256,c_427]) ).
cnf(c_280,plain,
double_divide(double_divide(A,B),A) = B,
inference(paramod,[status(thm)],[c_81,c_428]) ).
cnf(c_429,plain,
double_divide(inverse(double_divide(double_divide(A,C),A)),B) = double_divide(double_divide(double_divide(B,D),inverse(double_divide(inverse(double_divide(C,E)),D))),E),
inference(paramod,[status(thm)],[c_241,c_14]) ).
cnf(c_430,plain,
double_divide(inverse(C),B) = double_divide(double_divide(double_divide(B,D),inverse(double_divide(inverse(double_divide(C,E)),D))),E),
inference(paramod,[status(thm)],[c_280,c_429]) ).
cnf(c_431,plain,
double_divide(inverse(C),B) = double_divide(double_divide(double_divide(B,D),inverse(double_divide(C,inverse(double_divide(E,D))))),E),
inference(paramod,[status(thm)],[c_256,c_430]) ).
cnf(c_282,plain,
double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,inverse(double_divide(D,B))))),D) = double_divide(inverse(C),A),
inference(copy,[status(thm)],[c_431]) ).
cnf(c_432,plain,
inverse(double_divide(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,inverse(double_divide(D,B))))),D),A)) = C,
inference(paramod,[status(thm)],[c_256,c_13]) ).
cnf(c_433,plain,
inverse(double_divide(double_divide(inverse(C),A),A)) = C,
inference(paramod,[status(thm)],[c_282,c_432]) ).
cnf(c_283,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_259,c_433]) ).
cnf(c_434,plain,
double_divide(double_divide(double_divide(inverse(double_divide(double_divide(A,C),A)),B),D),D) = double_divide(double_divide(double_divide(double_divide(C,E),F),F),inverse(double_divide(B,E))),
inference(paramod,[status(thm)],[c_241,c_184]) ).
cnf(c_435,plain,
double_divide(double_divide(double_divide(inverse(C),B),D),D) = double_divide(double_divide(double_divide(double_divide(C,E),F),F),inverse(double_divide(B,E))),
inference(paramod,[status(thm)],[c_280,c_434]) ).
cnf(c_436,plain,
double_divide(inverse(C),B) = double_divide(double_divide(double_divide(double_divide(C,E),F),F),inverse(double_divide(B,E))),
inference(paramod,[status(thm)],[c_259,c_435]) ).
cnf(c_437,plain,
double_divide(inverse(C),B) = double_divide(double_divide(C,E),inverse(double_divide(B,E))),
inference(paramod,[status(thm)],[c_259,c_436]) ).
cnf(c_293,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,B))) = double_divide(inverse(A),C),
inference(copy,[status(thm)],[c_437]) ).
cnf(c_438,plain,
double_divide(inverse(double_divide(double_divide(A,E),A)),double_divide(double_divide(B,C),D)) = double_divide(double_divide(E,D),inverse(double_divide(double_divide(double_divide(B,F),F),C))),
inference(paramod,[status(thm)],[c_241,c_177]) ).
cnf(c_439,plain,
double_divide(inverse(E),double_divide(double_divide(B,C),D)) = double_divide(double_divide(E,D),inverse(double_divide(double_divide(double_divide(B,F),F),C))),
inference(paramod,[status(thm)],[c_280,c_438]) ).
cnf(c_440,plain,
double_divide(inverse(E),double_divide(double_divide(B,C),D)) = double_divide(double_divide(E,D),inverse(double_divide(B,C))),
inference(paramod,[status(thm)],[c_259,c_439]) ).
cnf(c_295,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,D))) = double_divide(inverse(A),double_divide(double_divide(C,D),B)),
inference(copy,[status(thm)],[c_440]) ).
cnf(c_441,plain,
inverse(double_divide(double_divide(double_divide(A,B),C),inverse(A))) = double_divide(double_divide(B,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_259,c_105]) ).
cnf(c_442,plain,
double_divide(inverse(double_divide(A,double_divide(A,B))),C) = double_divide(double_divide(B,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_241,c_441]) ).
cnf(c_443,plain,
double_divide(A,inverse(double_divide(double_divide(A,B),C))) = double_divide(double_divide(B,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_256,c_442]) ).
cnf(c_318,plain,
double_divide(A,inverse(double_divide(double_divide(A,B),C))) = double_divide(inverse(B),C),
inference(paramod,[status(thm)],[c_293,c_443]) ).
cnf(c_444,plain,
inverse(double_divide(A,inverse(double_divide(double_divide(A,C),D)))) = double_divide(double_divide(D,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_259,c_104]) ).
cnf(c_445,plain,
inverse(double_divide(inverse(C),D)) = double_divide(double_divide(D,E),inverse(double_divide(C,E))),
inference(paramod,[status(thm)],[c_318,c_444]) ).
cnf(c_319,plain,
inverse(double_divide(inverse(A),B)) = double_divide(inverse(B),A),
inference(paramod,[status(thm)],[c_293,c_445]) ).
cnf(c_446,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(inverse(D),B))) = double_divide(double_divide(A,F),inverse(double_divide(double_divide(D,C),F))),
inference(paramod,[status(thm)],[c_293,c_94]) ).
cnf(c_447,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(inverse(B),D)) = double_divide(double_divide(A,F),inverse(double_divide(double_divide(D,C),F))),
inference(paramod,[status(thm)],[c_319,c_446]) ).
cnf(c_321,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(inverse(B),D)) = double_divide(inverse(A),double_divide(D,C)),
inference(paramod,[status(thm)],[c_293,c_447]) ).
cnf(c_448,plain,
inverse(double_divide(inverse(A),double_divide(double_divide(A,D),double_divide(B,C)))) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(double_divide(B,F),inverse(double_divide(E,F))))),
inference(paramod,[status(thm)],[c_295,c_86]) ).
cnf(c_449,plain,
double_divide(inverse(double_divide(double_divide(A,D),double_divide(B,C))),A) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(double_divide(B,F),inverse(double_divide(E,F))))),
inference(paramod,[status(thm)],[c_319,c_448]) ).
cnf(c_450,plain,
double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(D,C))))),A) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(double_divide(B,F),inverse(double_divide(E,F))))),
inference(paramod,[status(thm)],[c_231,c_449]) ).
cnf(c_451,plain,
inverse(double_divide(B,inverse(double_divide(D,C)))) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(double_divide(B,F),inverse(double_divide(E,F))))),
inference(paramod,[status(thm)],[c_280,c_450]) ).
cnf(c_452,plain,
inverse(double_divide(B,inverse(double_divide(D,C)))) = double_divide(double_divide(D,inverse(double_divide(E,C))),inverse(double_divide(inverse(B),E))),
inference(paramod,[status(thm)],[c_293,c_451]) ).
cnf(c_453,plain,
inverse(double_divide(B,inverse(double_divide(D,C)))) = double_divide(double_divide(D,inverse(double_divide(E,C))),double_divide(inverse(E),B)),
inference(paramod,[status(thm)],[c_319,c_452]) ).
cnf(c_323,plain,
inverse(double_divide(A,inverse(double_divide(B,C)))) = double_divide(inverse(B),double_divide(A,C)),
inference(paramod,[status(thm)],[c_321,c_453]) ).
cnf(c_454,plain,
inverse(double_divide(double_divide(A,double_divide(B,inverse(double_divide(C,D)))),inverse(double_divide(A,E)))) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_256,c_65]) ).
cnf(c_455,plain,
inverse(double_divide(inverse(A),double_divide(double_divide(A,E),double_divide(B,inverse(double_divide(C,D)))))) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_295,c_454]) ).
cnf(c_456,plain,
double_divide(inverse(double_divide(double_divide(A,E),double_divide(B,inverse(double_divide(C,D))))),A) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_319,c_455]) ).
cnf(c_457,plain,
double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(E,inverse(double_divide(C,D))))))),A) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_231,c_456]) ).
cnf(c_458,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(inverse(C),double_divide(E,D))))),A) = double_divide(double_divide(E,inverse(double_divide(C,D))),inverse(B)),
inference(paramod,[status(thm)],[c_323,c_457]) ).
cnf(c_330,plain,
inverse(double_divide(A,double_divide(inverse(B),double_divide(C,D)))) = double_divide(double_divide(C,inverse(double_divide(B,D))),inverse(A)),
inference(paramod,[status(thm)],[c_280,c_458]) ).
cnf(c_459,plain,
inverse(double_divide(double_divide(double_divide(A,inverse(double_divide(B,C))),D),inverse(A))) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_256,c_63]) ).
cnf(c_460,plain,
double_divide(inverse(double_divide(A,double_divide(A,inverse(double_divide(B,C))))),D) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_241,c_459]) ).
cnf(c_461,plain,
double_divide(A,inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),D))) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_256,c_460]) ).
cnf(c_462,plain,
double_divide(inverse(inverse(double_divide(B,C))),D) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_318,c_461]) ).
cnf(c_463,plain,
double_divide(double_divide(B,C),D) = double_divide(double_divide(inverse(double_divide(B,C)),E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_283,c_462]) ).
cnf(c_464,plain,
double_divide(double_divide(B,C),D) = double_divide(double_divide(B,inverse(double_divide(C,E))),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_256,c_463]) ).
cnf(c_465,plain,
double_divide(double_divide(B,C),D) = double_divide(inverse(B),double_divide(double_divide(D,E),inverse(double_divide(C,E)))),
inference(paramod,[status(thm)],[c_295,c_464]) ).
cnf(c_332,plain,
double_divide(double_divide(A,B),C) = double_divide(inverse(A),double_divide(inverse(C),B)),
inference(paramod,[status(thm)],[c_293,c_465]) ).
cnf(c_466,plain,
inverse(inverse(double_divide(inverse(A),double_divide(inverse(inverse(double_divide(A,B))),B)))) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_332,c_45]) ).
cnf(c_467,plain,
inverse(inverse(double_divide(inverse(A),double_divide(double_divide(A,B),B)))) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_283,c_466]) ).
cnf(c_468,plain,
inverse(inverse(double_divide(inverse(A),A))) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_259,c_467]) ).
cnf(c_469,plain,
inverse(double_divide(inverse(A),A)) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_319,c_468]) ).
cnf(c_470,plain,
double_divide(inverse(A),A) = double_divide(double_divide(C,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_319,c_469]) ).
cnf(c_471,plain,
double_divide(inverse(A),A) = double_divide(inverse(C),double_divide(inverse(inverse(double_divide(C,D))),D)),
inference(paramod,[status(thm)],[c_332,c_470]) ).
cnf(c_472,plain,
double_divide(inverse(A),A) = double_divide(inverse(C),double_divide(double_divide(C,D),D)),
inference(paramod,[status(thm)],[c_283,c_471]) ).
cnf(c_339,plain,
double_divide(inverse(A),A) = double_divide(inverse(B),B),
inference(paramod,[status(thm)],[c_259,c_472]) ).
cnf(c_473,plain,
inverse(double_divide(inverse(double_divide(inverse(A),double_divide(inverse(inverse(double_divide(A,C))),B))),B)) = C,
inference(paramod,[status(thm)],[c_332,c_38]) ).
cnf(c_474,plain,
inverse(double_divide(inverse(double_divide(inverse(A),double_divide(double_divide(A,C),B))),B)) = C,
inference(paramod,[status(thm)],[c_283,c_473]) ).
cnf(c_475,plain,
inverse(double_divide(inverse(double_divide(inverse(A),double_divide(inverse(A),double_divide(inverse(B),C)))),B)) = C,
inference(paramod,[status(thm)],[c_332,c_474]) ).
cnf(c_476,plain,
inverse(double_divide(double_divide(double_divide(inverse(B),inverse(double_divide(A,C))),inverse(inverse(A))),B)) = C,
inference(paramod,[status(thm)],[c_330,c_475]) ).
cnf(c_477,plain,
inverse(double_divide(double_divide(double_divide(inverse(B),inverse(double_divide(A,C))),A),B)) = C,
inference(paramod,[status(thm)],[c_283,c_476]) ).
cnf(c_478,plain,
inverse(double_divide(double_divide(inverse(inverse(B)),double_divide(inverse(A),inverse(double_divide(A,C)))),B)) = C,
inference(paramod,[status(thm)],[c_332,c_477]) ).
cnf(c_479,plain,
inverse(double_divide(double_divide(B,double_divide(inverse(A),inverse(double_divide(A,C)))),B)) = C,
inference(paramod,[status(thm)],[c_283,c_478]) ).
cnf(c_480,plain,
inverse(double_divide(inverse(A),inverse(double_divide(A,C)))) = C,
inference(paramod,[status(thm)],[c_280,c_479]) ).
cnf(c_342,plain,
double_divide(inverse(A),double_divide(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_323,c_480]) ).
cnf(c_481,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(B),double_divide(inverse(inverse(double_divide(D,C))),C))),inverse(double_divide(A,E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_332,c_25]) ).
cnf(c_482,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(B),double_divide(double_divide(D,C),C))),inverse(double_divide(A,E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_283,c_481]) ).
cnf(c_483,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(B),D)),inverse(double_divide(A,E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_259,c_482]) ).
cnf(c_484,plain,
inverse(double_divide(inverse(A),double_divide(inverse(inverse(double_divide(A,E))),double_divide(inverse(B),D)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_332,c_483]) ).
cnf(c_485,plain,
inverse(double_divide(inverse(A),double_divide(double_divide(A,E),double_divide(inverse(B),D)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_283,c_484]) ).
cnf(c_486,plain,
inverse(double_divide(inverse(A),double_divide(inverse(A),double_divide(inverse(double_divide(inverse(B),D)),E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_332,c_485]) ).
cnf(c_487,plain,
inverse(double_divide(inverse(A),double_divide(inverse(A),double_divide(double_divide(inverse(D),B),E)))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_319,c_486]) ).
cnf(c_488,plain,
inverse(double_divide(inverse(A),double_divide(inverse(A),double_divide(inverse(inverse(D)),double_divide(inverse(E),B))))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_332,c_487]) ).
cnf(c_489,plain,
inverse(double_divide(inverse(A),double_divide(inverse(A),double_divide(D,double_divide(inverse(E),B))))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_283,c_488]) ).
cnf(c_490,plain,
inverse(double_divide(D,double_divide(inverse(E),B))) = double_divide(double_divide(E,D),B),
inference(paramod,[status(thm)],[c_342,c_489]) ).
cnf(c_346,plain,
inverse(double_divide(A,double_divide(inverse(B),C))) = double_divide(inverse(B),double_divide(inverse(C),A)),
inference(paramod,[status(thm)],[c_332,c_490]) ).
cnf(c_491,plain,
double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(B,D))))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_256,c_255]) ).
cnf(c_492,plain,
double_divide(double_divide(A,B),inverse(double_divide(A,double_divide(inverse(B),double_divide(C,D))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_323,c_491]) ).
cnf(c_493,plain,
double_divide(double_divide(A,B),double_divide(inverse(B),double_divide(inverse(double_divide(C,D)),A))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_346,c_492]) ).
cnf(c_494,plain,
double_divide(double_divide(A,B),double_divide(inverse(B),double_divide(C,inverse(double_divide(D,A))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_256,c_493]) ).
cnf(c_495,plain,
double_divide(inverse(A),double_divide(inverse(double_divide(inverse(B),double_divide(C,inverse(double_divide(D,A))))),B)) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_494]) ).
cnf(c_496,plain,
double_divide(inverse(A),double_divide(double_divide(inverse(double_divide(C,inverse(double_divide(D,A)))),B),B)) = double_divide(C,D),
inference(paramod,[status(thm)],[c_319,c_495]) ).
cnf(c_497,plain,
double_divide(inverse(A),double_divide(double_divide(double_divide(inverse(D),double_divide(C,A)),B),B)) = double_divide(C,D),
inference(paramod,[status(thm)],[c_323,c_496]) ).
cnf(c_498,plain,
double_divide(inverse(A),double_divide(double_divide(inverse(inverse(D)),double_divide(inverse(B),double_divide(C,A))),B)) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_497]) ).
cnf(c_499,plain,
double_divide(inverse(A),double_divide(double_divide(D,double_divide(inverse(B),double_divide(C,A))),B)) = double_divide(C,D),
inference(paramod,[status(thm)],[c_283,c_498]) ).
cnf(c_500,plain,
double_divide(inverse(A),double_divide(inverse(D),double_divide(inverse(B),double_divide(inverse(B),double_divide(C,A))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_499]) ).
cnf(c_351,plain,
double_divide(inverse(A),double_divide(inverse(B),double_divide(C,A))) = double_divide(C,B),
inference(paramod,[status(thm)],[c_342,c_500]) ).
cnf(c_501,plain,
double_divide(inverse(double_divide(B,inverse(B))),inverse(double_divide(C,D))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_280,c_248]) ).
cnf(c_502,plain,
double_divide(B,inverse(double_divide(inverse(B),inverse(double_divide(C,D))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_256,c_501]) ).
cnf(c_353,plain,
double_divide(A,double_divide(inverse(B),double_divide(inverse(A),C))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_323,c_502]) ).
cnf(c_503,plain,
double_divide(inverse(double_divide(B,C)),D) = double_divide(E,inverse(double_divide(B,inverse(double_divide(inverse(double_divide(D,inverse(E))),C))))),
inference(paramod,[status(thm)],[c_280,c_246]) ).
cnf(c_504,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,inverse(double_divide(B,inverse(double_divide(inverse(double_divide(D,inverse(E))),C))))),
inference(paramod,[status(thm)],[c_256,c_503]) ).
cnf(c_505,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,inverse(double_divide(B,inverse(double_divide(D,inverse(double_divide(inverse(E),C))))))),
inference(paramod,[status(thm)],[c_256,c_504]) ).
cnf(c_506,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,inverse(double_divide(B,inverse(double_divide(D,double_divide(inverse(C),E)))))),
inference(paramod,[status(thm)],[c_319,c_505]) ).
cnf(c_507,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,inverse(double_divide(B,double_divide(inverse(C),double_divide(inverse(E),D))))),
inference(paramod,[status(thm)],[c_346,c_506]) ).
cnf(c_508,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,double_divide(inverse(C),double_divide(inverse(double_divide(inverse(E),D)),B))),
inference(paramod,[status(thm)],[c_346,c_507]) ).
cnf(c_509,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,double_divide(inverse(C),double_divide(double_divide(inverse(D),E),B))),
inference(paramod,[status(thm)],[c_319,c_508]) ).
cnf(c_510,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,double_divide(inverse(C),double_divide(inverse(inverse(D)),double_divide(inverse(B),E)))),
inference(paramod,[status(thm)],[c_332,c_509]) ).
cnf(c_511,plain,
double_divide(B,inverse(double_divide(C,D))) = double_divide(E,double_divide(inverse(C),double_divide(D,double_divide(inverse(B),E)))),
inference(paramod,[status(thm)],[c_283,c_510]) ).
cnf(c_355,plain,
double_divide(A,double_divide(inverse(B),double_divide(C,double_divide(inverse(D),A)))) = double_divide(D,inverse(double_divide(B,C))),
inference(copy,[status(thm)],[c_511]) ).
cnf(c_512,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(inverse(A),double_divide(inverse(C),B))),inverse(double_divide(D,B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_243]) ).
cnf(c_513,plain,
double_divide(A,inverse(double_divide(double_divide(inverse(C),double_divide(inverse(B),inverse(A))),inverse(double_divide(D,B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_346,c_512]) ).
cnf(c_514,plain,
double_divide(A,inverse(double_divide(inverse(inverse(C)),double_divide(inverse(inverse(double_divide(D,B))),double_divide(inverse(B),inverse(A)))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_513]) ).
cnf(c_515,plain,
double_divide(A,inverse(double_divide(C,double_divide(inverse(inverse(double_divide(D,B))),double_divide(inverse(B),inverse(A)))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_283,c_514]) ).
cnf(c_516,plain,
double_divide(A,inverse(double_divide(C,double_divide(double_divide(D,B),double_divide(inverse(B),inverse(A)))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_283,c_515]) ).
cnf(c_517,plain,
double_divide(A,inverse(double_divide(C,double_divide(inverse(D),double_divide(inverse(double_divide(inverse(B),inverse(A))),B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_332,c_516]) ).
cnf(c_518,plain,
double_divide(A,inverse(double_divide(C,double_divide(inverse(D),double_divide(double_divide(inverse(inverse(A)),B),B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_319,c_517]) ).
cnf(c_519,plain,
double_divide(A,inverse(double_divide(C,double_divide(inverse(D),double_divide(double_divide(A,B),B))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_283,c_518]) ).
cnf(c_520,plain,
double_divide(A,inverse(double_divide(C,double_divide(inverse(D),A)))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_259,c_519]) ).
cnf(c_521,plain,
double_divide(A,double_divide(inverse(D),double_divide(inverse(A),C))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_346,c_520]) ).
cnf(c_356,plain,
double_divide(A,B) = double_divide(B,A),
inference(paramod,[status(thm)],[c_353,c_521]) ).
cnf(c_522,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,inverse(double_divide(inverse(A),D))))))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_256,c_229]) ).
cnf(c_523,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(inverse(D),A)))))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_319,c_522]) ).
cnf(c_524,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,double_divide(inverse(D),double_divide(inverse(A),C))))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_346,c_523]) ).
cnf(c_525,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(D),double_divide(inverse(double_divide(inverse(A),C)),B))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_346,c_524]) ).
cnf(c_526,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(D),double_divide(double_divide(inverse(C),A),B))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_319,c_525]) ).
cnf(c_527,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(D),double_divide(inverse(inverse(C)),double_divide(inverse(B),A)))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_332,c_526]) ).
cnf(c_528,plain,
inverse(double_divide(double_divide(A,double_divide(inverse(D),double_divide(C,double_divide(inverse(B),A)))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_283,c_527]) ).
cnf(c_529,plain,
inverse(double_divide(double_divide(B,inverse(double_divide(D,C))),C)) = double_divide(B,D),
inference(paramod,[status(thm)],[c_355,c_528]) ).
cnf(c_359,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(C,A))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_356,c_529]) ).
cnf(c_530,plain,
double_divide(double_divide(inverse(double_divide(A,double_divide(C,double_divide(B,C)))),D),inverse(double_divide(double_divide(double_divide(B,D),E),E))) = A,
inference(paramod,[status(thm)],[c_356,c_189]) ).
cnf(c_531,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(C,double_divide(B,C)),D))),inverse(double_divide(double_divide(double_divide(B,D),E),E))) = A,
inference(paramod,[status(thm)],[c_256,c_530]) ).
cnf(c_532,plain,
double_divide(double_divide(A,inverse(double_divide(inverse(C),double_divide(inverse(D),double_divide(B,C))))),inverse(double_divide(double_divide(double_divide(B,D),E),E))) = A,
inference(paramod,[status(thm)],[c_332,c_531]) ).
cnf(c_533,plain,
double_divide(double_divide(A,inverse(double_divide(B,D))),inverse(double_divide(double_divide(double_divide(B,D),E),E))) = A,
inference(paramod,[status(thm)],[c_351,c_532]) ).
cnf(c_534,plain,
double_divide(double_divide(A,inverse(double_divide(B,D))),inverse(double_divide(double_divide(inverse(B),double_divide(inverse(E),D)),E))) = A,
inference(paramod,[status(thm)],[c_332,c_533]) ).
cnf(c_535,plain,
double_divide(double_divide(A,inverse(double_divide(B,D))),inverse(double_divide(E,double_divide(inverse(B),double_divide(inverse(E),D))))) = A,
inference(paramod,[status(thm)],[c_356,c_534]) ).
cnf(c_536,plain,
double_divide(double_divide(A,inverse(double_divide(B,D))),inverse(double_divide(B,D))) = A,
inference(paramod,[status(thm)],[c_353,c_535]) ).
cnf(c_537,plain,
double_divide(inverse(double_divide(B,D)),double_divide(A,inverse(double_divide(B,D)))) = A,
inference(paramod,[status(thm)],[c_356,c_536]) ).
cnf(c_538,plain,
double_divide(B,inverse(double_divide(D,double_divide(A,inverse(double_divide(B,D)))))) = A,
inference(paramod,[status(thm)],[c_256,c_537]) ).
cnf(c_362,plain,
double_divide(A,double_divide(B,A)) = B,
inference(paramod,[status(thm)],[c_359,c_538]) ).
cnf(c_539,plain,
double_divide(double_divide(A,B),double_divide(inverse(B),C)) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_319,c_234]) ).
cnf(c_540,plain,
double_divide(inverse(A),double_divide(inverse(double_divide(inverse(B),C)),B)) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_332,c_539]) ).
cnf(c_541,plain,
double_divide(inverse(A),double_divide(double_divide(inverse(C),B),B)) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_319,c_540]) ).
cnf(c_542,plain,
double_divide(inverse(A),double_divide(B,double_divide(inverse(C),B))) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_356,c_541]) ).
cnf(c_543,plain,
double_divide(inverse(A),inverse(C)) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_362,c_542]) ).
cnf(c_381,plain,
inverse(double_divide(A,B)) = double_divide(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_543]) ).
cnf(c_544,plain,
double_divide(A,inverse(A)) = double_divide(inverse(B),B),
inference(paramod,[status(thm)],[c_356,c_339]) ).
cnf(c_407,plain,
double_divide(A,inverse(A)) = double_divide(B,inverse(B)),
inference(paramod,[status(thm)],[c_356,c_544]) ).
cnf(c_545,plain,
double_divide(inverse(inverse(b1)),inverse(b1)) != inverse(double_divide(a1,inverse(a1))),
inference(paramod,[status(thm)],[c_381,c_4]) ).
cnf(c_546,plain,
double_divide(b1,inverse(b1)) != inverse(double_divide(a1,inverse(a1))),
inference(paramod,[status(thm)],[c_283,c_545]) ).
cnf(c_547,plain,
double_divide(b1,inverse(b1)) != double_divide(inverse(inverse(a1)),inverse(a1)),
inference(paramod,[status(thm)],[c_381,c_546]) ).
cnf(c_548,plain,
double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)),
inference(paramod,[status(thm)],[c_283,c_547]) ).
cnf(c_411,plain,
$false,
inference(resolve,[status(thm)],[c_407,c_548]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP593-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.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:57:03 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 2581409 was started by sandbox on n017,
% 0.08/0.35 % Fri Sep 25 14:57:03 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).
% 0.12/0.41
% 0.12/0.41 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 0.12/0.41
% 0.12/0.41 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.41
% 0.12/0.41 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.12/0.41 % Length of proof is 68.
% 0.12/0.41 % Level of proof is 23.
% 0.12/0.41 % Maximum clause weight is 77.000.
% 0.12/0.41 % Given clauses 13.
% 0.12/0.41
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------