%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP612-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:29 AM UTC 2026
% Result : Unsatisfiable 0.16s 0.53s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 3
% Syntax : Number of formulae : 218 ( 218 unt; 0 def)
% Number of atoms : 218 ( 217 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 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; 2 con; 0-2 aty)
% Number of variables : 898 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : inverse(double_divide(inverse(double_divide(inverse(double_divide(VAR_0,VAR_1)),VAR_2)),double_divide(VAR_0,VAR_2))) = VAR_1,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),C)),double_divide(A,C))) = B,
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_4,axiom,
multiply(a,b) != multiply(b,a),
file('theBenchmark.p',prove_these_axioms_4) ).
cnf(c_3,plain,
multiply(a,b) != multiply(b,a),
inference(clausify,[status(thm)],[prove_these_axioms_4]) ).
cnf(c_484,plain,
inverse(double_divide(b,a)) != multiply(b,a),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_4,plain,
inverse(double_divide(b,a)) != inverse(double_divide(a,b)),
inference(paramod,[status(thm)],[c_2,c_484]) ).
cnf(c_5,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(inverse(double_divide(C,A)),D)),B))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_6,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,A)),double_divide(B,C)))) = C,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_7,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(double_divide(D,E)),C))) = double_divide(inverse(double_divide(inverse(double_divide(A,D)),B)),E),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_10,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(C,B))) = double_divide(inverse(double_divide(D,C)),double_divide(D,A)),
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_14,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,C)),D)),double_divide(inverse(double_divide(E,C)),double_divide(E,A))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_485,plain,
A = double_divide(B,inverse(double_divide(C,double_divide(inverse(double_divide(B,C)),A)))),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_16,plain,
double_divide(A,inverse(double_divide(B,double_divide(inverse(double_divide(A,B)),C)))) = C,
inference(copy,[status(thm)],[c_485]) ).
cnf(c_19,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(double_divide(B,C)))) = C,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_21,plain,
inverse(double_divide(inverse(inverse(double_divide(inverse(double_divide(A,B)),double_divide(C,B)))),double_divide(D,double_divide(D,A)))) = C,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_486,plain,
inverse(double_divide(A,double_divide(B,double_divide(C,D)))) = double_divide(inverse(double_divide(E,B)),double_divide(E,inverse(double_divide(inverse(double_divide(C,A)),D)))),
inference(paramod,[status(thm)],[c_1,c_10]) ).
cnf(c_23,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(double_divide(inverse(double_divide(C,D)),E)))) = inverse(double_divide(D,double_divide(B,double_divide(C,E)))),
inference(copy,[status(thm)],[c_486]) ).
cnf(c_30,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(inverse(double_divide(inverse(double_divide(C,D)),double_divide(A,D)))),B))) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_10,c_5]) ).
cnf(c_39,plain,
inverse(double_divide(A,double_divide(B,double_divide(inverse(double_divide(C,D)),double_divide(C,A))))) = double_divide(inverse(double_divide(E,B)),double_divide(E,D)),
inference(paramod,[status(thm)],[c_6,c_10]) ).
cnf(c_41,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,C)) = double_divide(inverse(double_divide(D,B)),double_divide(D,C)),
inference(paramod,[status(thm)],[c_10,c_10]) ).
cnf(c_49,plain,
inverse(double_divide(inverse(double_divide(inverse(A),B)),double_divide(inverse(double_divide(C,D)),B))) = double_divide(C,inverse(double_divide(D,A))),
inference(paramod,[status(thm)],[c_19,c_1]) ).
cnf(c_60,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,C)),A)),D))) = double_divide(B,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_19,c_6]) ).
cnf(c_70,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,inverse(D))) = double_divide(B,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_19,c_19]) ).
cnf(c_487,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(inverse(double_divide(C,A)),double_divide(C,D))),B))) = double_divide(E,double_divide(E,D)),
inference(paramod,[status(thm)],[c_41,c_5]) ).
cnf(c_77,plain,
double_divide(A,double_divide(A,B)) = double_divide(C,double_divide(C,B)),
inference(paramod,[status(thm)],[c_5,c_487]) ).
cnf(c_488,plain,
double_divide(A,double_divide(B,C)) = double_divide(inverse(double_divide(D,double_divide(inverse(double_divide(E,B)),double_divide(E,A)))),double_divide(D,C)),
inference(paramod,[status(thm)],[c_6,c_41]) ).
cnf(c_81,plain,
double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(B,C)),double_divide(B,D)))),double_divide(A,E)) = double_divide(D,double_divide(C,E)),
inference(copy,[status(thm)],[c_488]) ).
cnf(c_82,plain,
inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),double_divide(A,C))),double_divide(D,double_divide(E,C)))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_41,c_10]) ).
cnf(c_84,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(A,B))) = double_divide(inverse(double_divide(C,D)),double_divide(C,D)),
inference(paramod,[status(thm)],[c_41,c_10]) ).
cnf(c_489,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,inverse(double_divide(inverse(double_divide(D,C)),double_divide(D,E))))) = double_divide(B,E),
inference(paramod,[status(thm)],[c_41,c_19]) ).
cnf(c_91,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,A)),double_divide(C,double_divide(C,D))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_23,c_489]) ).
cnf(c_490,plain,
double_divide(inverse(A),double_divide(inverse(double_divide(B,C)),D)) = double_divide(inverse(double_divide(E,double_divide(B,inverse(double_divide(C,A))))),double_divide(E,D)),
inference(paramod,[status(thm)],[c_19,c_41]) ).
cnf(c_92,plain,
double_divide(inverse(double_divide(A,double_divide(B,inverse(double_divide(C,D))))),double_divide(A,E)) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(copy,[status(thm)],[c_490]) ).
cnf(c_491,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(double_divide(inverse(double_divide(D,double_divide(D,B))),E)),C))) = double_divide(A,E),
inference(paramod,[status(thm)],[c_77,c_5]) ).
cnf(c_100,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,inverse(double_divide(B,double_divide(B,C))))),C)),D) = double_divide(A,D),
inference(paramod,[status(thm)],[c_7,c_491]) ).
cnf(c_492,plain,
inverse(double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),double_divide(C,B))),D)),double_divide(inverse(double_divide(E,F)),D))) = double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(V6,C)),E)),double_divide(V6,A))),F),
inference(paramod,[status(thm)],[c_10,c_7]) ).
cnf(c_493,plain,
double_divide(E,inverse(double_divide(F,double_divide(inverse(double_divide(A,B)),double_divide(C,B))))) = double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(V6,C)),E)),double_divide(V6,A))),F),
inference(paramod,[status(thm)],[c_49,c_492]) ).
cnf(c_132,plain,
double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),C)),double_divide(A,D))),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(copy,[status(thm)],[c_493]) ).
cnf(c_137,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(C,D)),B))) = double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),double_divide(E,inverse(double_divide(F,A))))),D),
inference(paramod,[status(thm)],[c_19,c_7]) ).
cnf(c_138,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(D),C))) = double_divide(inverse(double_divide(inverse(double_divide(A,inverse(double_divide(E,F)))),B)),double_divide(E,inverse(double_divide(F,D)))),
inference(paramod,[status(thm)],[c_19,c_7]) ).
cnf(c_149,plain,
inverse(double_divide(A,double_divide(A,B))) = double_divide(inverse(double_divide(inverse(double_divide(C,double_divide(C,D))),D)),B),
inference(paramod,[status(thm)],[c_77,c_7]) ).
cnf(c_162,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(C,double_divide(inverse(double_divide(D,C)),E))),B))) = double_divide(inverse(E),double_divide(D,A)),
inference(paramod,[status(thm)],[c_16,c_10]) ).
cnf(c_494,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(C))) = inverse(double_divide(D,double_divide(inverse(double_divide(B,D)),C))),
inference(paramod,[status(thm)],[c_16,c_19]) ).
cnf(c_168,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,A)),C))) = double_divide(inverse(double_divide(D,B)),double_divide(D,inverse(C))),
inference(copy,[status(thm)],[c_494]) ).
cnf(c_495,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(double_divide(D,inverse(double_divide(E,double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(A,D)),B)),E)),F))))),C))) = F,
inference(paramod,[status(thm)],[c_16,c_7]) ).
cnf(c_496,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(double_divide(D,double_divide(inverse(double_divide(A,D)),inverse(double_divide(B,F))))),C))) = F,
inference(paramod,[status(thm)],[c_60,c_495]) ).
cnf(c_179,plain,
double_divide(inverse(inverse(double_divide(A,B))),double_divide(C,double_divide(C,A))) = B,
inference(paramod,[status(thm)],[c_162,c_496]) ).
cnf(c_497,plain,
inverse(double_divide(inverse(double_divide(double_divide(inverse(double_divide(A,B)),double_divide(A,B)),C)),double_divide(inverse(double_divide(D,E)),C))) = double_divide(D,E),
inference(paramod,[status(thm)],[c_84,c_1]) ).
cnf(c_182,plain,
double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),C)),double_divide(A,B))),D) = double_divide(C,D),
inference(paramod,[status(thm)],[c_7,c_497]) ).
cnf(c_185,plain,
inverse(double_divide(inverse(inverse(double_divide(inverse(double_divide(A,B)),double_divide(A,B)))),double_divide(C,double_divide(C,D)))) = D,
inference(paramod,[status(thm)],[c_84,c_1]) ).
cnf(c_498,plain,
inverse(double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(A,B)),C)),double_divide(A,B))),inverse(double_divide(inverse(double_divide(D,E)),double_divide(D,E))))) = C,
inference(paramod,[status(thm)],[c_84,c_1]) ).
cnf(c_186,plain,
inverse(double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(B,C))))) = A,
inference(paramod,[status(thm)],[c_182,c_498]) ).
cnf(c_499,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(inverse(double_divide(double_divide(inverse(double_divide(D,E)),double_divide(D,E)),F)),C))) = double_divide(inverse(double_divide(A,B)),F),
inference(paramod,[status(thm)],[c_84,c_5]) ).
cnf(c_190,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(B,C)),double_divide(B,C)))),D)),E) = double_divide(inverse(double_divide(A,D)),E),
inference(paramod,[status(thm)],[c_7,c_499]) ).
cnf(c_500,plain,
inverse(double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(B,A)),C))),inverse(double_divide(inverse(double_divide(D,E)),double_divide(D,E))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_84,c_5]) ).
cnf(c_193,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,A)),C))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_186,c_500]) ).
cnf(c_501,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,C)),A)),inverse(double_divide(inverse(double_divide(D,E)),double_divide(D,E)))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_84,c_6]) ).
cnf(c_199,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(inverse(double_divide(C,D)),double_divide(C,D)))) = double_divide(A,B),
inference(paramod,[status(thm)],[c_193,c_501]) ).
cnf(c_502,plain,
inverse(double_divide(inverse(double_divide(A,double_divide(B,C))),inverse(double_divide(inverse(double_divide(D,E)),double_divide(D,E))))) = double_divide(inverse(double_divide(F,inverse(double_divide(B,C)))),double_divide(F,A)),
inference(paramod,[status(thm)],[c_84,c_10]) ).
cnf(c_503,plain,
inverse(double_divide(A,double_divide(B,C))) = double_divide(inverse(double_divide(F,inverse(double_divide(B,C)))),double_divide(F,A)),
inference(paramod,[status(thm)],[c_199,c_502]) ).
cnf(c_206,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,D)) = inverse(double_divide(D,double_divide(B,C))),
inference(copy,[status(thm)],[c_503]) ).
cnf(c_504,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(D,C))) = double_divide(inverse(double_divide(inverse(double_divide(A,B)),D)),inverse(double_divide(inverse(double_divide(E,F)),double_divide(E,F)))),
inference(paramod,[status(thm)],[c_84,c_10]) ).
cnf(c_208,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),C)),double_divide(D,C))) = double_divide(inverse(double_divide(A,B)),D),
inference(paramod,[status(thm)],[c_199,c_504]) ).
cnf(c_505,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),double_divide(C,D))),inverse(double_divide(inverse(double_divide(E,F)),double_divide(E,F))))) = double_divide(inverse(double_divide(inverse(double_divide(A,C)),B)),D),
inference(paramod,[status(thm)],[c_84,c_7]) ).
cnf(c_233,plain,
inverse(double_divide(double_divide(A,B),double_divide(C,D))) = double_divide(inverse(double_divide(inverse(double_divide(A,C)),B)),D),
inference(paramod,[status(thm)],[c_199,c_505]) ).
cnf(c_506,plain,
inverse(double_divide(inverse(double_divide(double_divide(inverse(double_divide(A,B)),C),D)),double_divide(inverse(double_divide(double_divide(A,B),E)),D))) = double_divide(inverse(double_divide(inverse(inverse(double_divide(inverse(double_divide(F,V6)),double_divide(F,V6)))),C)),E),
inference(paramod,[status(thm)],[c_84,c_7]) ).
cnf(c_507,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,B)),C)),inverse(double_divide(double_divide(A,B),E))) = double_divide(inverse(double_divide(inverse(inverse(double_divide(inverse(double_divide(F,V6)),double_divide(F,V6)))),C)),E),
inference(paramod,[status(thm)],[c_208,c_506]) ).
cnf(c_234,plain,
double_divide(inverse(double_divide(inverse(inverse(double_divide(inverse(double_divide(A,B)),double_divide(A,B)))),C)),D) = double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),inverse(double_divide(double_divide(E,F),D))),
inference(copy,[status(thm)],[c_507]) ).
cnf(c_508,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(double_divide(A,B),double_divide(double_divide(inverse(double_divide(C,D)),double_divide(C,D)),E)))) = E,
inference(paramod,[status(thm)],[c_84,c_16]) ).
cnf(c_509,plain,
double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(C,D)),double_divide(C,D)))),B)),E)) = E,
inference(paramod,[status(thm)],[c_233,c_508]) ).
cnf(c_238,plain,
double_divide(inverse(double_divide(A,B)),double_divide(inverse(double_divide(A,B)),C)) = C,
inference(paramod,[status(thm)],[c_190,c_509]) ).
cnf(c_510,plain,
double_divide(B,C) = double_divide(inverse(double_divide(D,B)),double_divide(D,inverse(C))),
inference(paramod,[status(thm)],[c_193,c_168]) ).
cnf(c_251,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(C))) = double_divide(B,C),
inference(copy,[status(thm)],[c_510]) ).
cnf(c_253,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(double_divide(C,D),B))) = double_divide(inverse(D),double_divide(C,A)),
inference(paramod,[status(thm)],[c_193,c_162]) ).
cnf(c_260,plain,
double_divide(A,double_divide(B,double_divide(B,C))) = double_divide(A,C),
inference(paramod,[status(thm)],[c_193,c_91]) ).
cnf(c_262,plain,
double_divide(inverse(double_divide(A,B)),C) = double_divide(A,inverse(double_divide(B,C))),
inference(paramod,[status(thm)],[c_193,c_60]) ).
cnf(c_511,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(A,inverse(D))))) = double_divide(B,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_262,c_70]) ).
cnf(c_270,plain,
double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,inverse(D))))))) = double_divide(B,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_262,c_511]) ).
cnf(c_512,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(inverse(double_divide(inverse(double_divide(A,inverse(double_divide(E,F)))),B)),double_divide(E,inverse(double_divide(F,D)))),
inference(paramod,[status(thm)],[c_262,c_138]) ).
cnf(c_513,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(inverse(double_divide(A,inverse(double_divide(inverse(double_divide(E,F)),B)))),double_divide(E,inverse(double_divide(F,D)))),
inference(paramod,[status(thm)],[c_262,c_512]) ).
cnf(c_514,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(inverse(double_divide(A,inverse(double_divide(E,inverse(double_divide(F,B)))))),double_divide(E,inverse(double_divide(F,D)))),
inference(paramod,[status(thm)],[c_262,c_513]) ).
cnf(c_515,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,inverse(double_divide(F,B)))),double_divide(E,inverse(double_divide(F,D)))))),
inference(paramod,[status(thm)],[c_262,c_514]) ).
cnf(c_516,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(A,inverse(double_divide(E,inverse(double_divide(inverse(double_divide(F,B)),double_divide(E,inverse(double_divide(F,D)))))))),
inference(paramod,[status(thm)],[c_262,c_515]) ).
cnf(c_517,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(A,inverse(double_divide(E,inverse(double_divide(F,inverse(double_divide(B,double_divide(E,inverse(double_divide(F,D)))))))))),
inference(paramod,[status(thm)],[c_262,c_516]) ).
cnf(c_278,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,double_divide(inverse(D),C))))) = double_divide(A,inverse(double_divide(E,inverse(double_divide(B,double_divide(E,D)))))),
inference(paramod,[status(thm)],[c_270,c_517]) ).
cnf(c_518,plain,
inverse(double_divide(inverse(inverse(double_divide(A,inverse(double_divide(B,double_divide(A,B)))))),double_divide(C,double_divide(C,D)))) = D,
inference(paramod,[status(thm)],[c_262,c_185]) ).
cnf(c_288,plain,
inverse(double_divide(inverse(inverse(double_divide(A,inverse(double_divide(B,double_divide(A,B)))))),C)) = C,
inference(paramod,[status(thm)],[c_260,c_518]) ).
cnf(c_519,plain,
double_divide(A,inverse(double_divide(double_divide(B,inverse(double_divide(C,D))),double_divide(A,E)))) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_262,c_92]) ).
cnf(c_520,plain,
double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,A)),inverse(double_divide(C,D)))),E)) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_233,c_519]) ).
cnf(c_521,plain,
double_divide(A,double_divide(inverse(double_divide(B,inverse(double_divide(A,inverse(double_divide(C,D)))))),E)) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_262,c_520]) ).
cnf(c_522,plain,
double_divide(A,double_divide(B,inverse(double_divide(inverse(double_divide(A,inverse(double_divide(C,D)))),E)))) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_262,c_521]) ).
cnf(c_523,plain,
double_divide(A,double_divide(B,inverse(double_divide(A,inverse(double_divide(inverse(double_divide(C,D)),E)))))) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_262,c_522]) ).
cnf(c_524,plain,
double_divide(A,double_divide(B,inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(D,E)))))))) = double_divide(inverse(D),double_divide(inverse(double_divide(B,C)),E)),
inference(paramod,[status(thm)],[c_262,c_523]) ).
cnf(c_317,plain,
double_divide(A,double_divide(B,inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(D,E)))))))) = double_divide(inverse(D),double_divide(B,inverse(double_divide(C,E)))),
inference(paramod,[status(thm)],[c_262,c_524]) ).
cnf(c_525,plain,
double_divide(inverse(double_divide(A,double_divide(B,inverse(double_divide(C,double_divide(B,D)))))),double_divide(A,E)) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_81]) ).
cnf(c_526,plain,
double_divide(A,inverse(double_divide(double_divide(B,inverse(double_divide(C,double_divide(B,D)))),double_divide(A,E)))) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_525]) ).
cnf(c_527,plain,
double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,A)),inverse(double_divide(C,double_divide(B,D))))),E)) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_233,c_526]) ).
cnf(c_528,plain,
double_divide(A,double_divide(inverse(double_divide(B,inverse(double_divide(A,inverse(double_divide(C,double_divide(B,D))))))),E)) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_527]) ).
cnf(c_529,plain,
double_divide(A,double_divide(B,inverse(double_divide(inverse(double_divide(A,inverse(double_divide(C,double_divide(B,D))))),E)))) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_528]) ).
cnf(c_530,plain,
double_divide(A,double_divide(B,inverse(double_divide(A,inverse(double_divide(inverse(double_divide(C,double_divide(B,D))),E)))))) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_529]) ).
cnf(c_531,plain,
double_divide(A,double_divide(B,inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(double_divide(B,D),E)))))))) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_262,c_530]) ).
cnf(c_532,plain,
double_divide(inverse(double_divide(B,D)),double_divide(B,inverse(double_divide(C,E)))) = double_divide(D,double_divide(C,E)),
inference(paramod,[status(thm)],[c_317,c_531]) ).
cnf(c_320,plain,
double_divide(A,inverse(double_divide(B,double_divide(A,inverse(double_divide(C,D)))))) = double_divide(B,double_divide(C,D)),
inference(paramod,[status(thm)],[c_262,c_532]) ).
cnf(c_533,plain,
inverse(double_divide(inverse(double_divide(A,inverse(double_divide(B,double_divide(A,C))))),double_divide(D,double_divide(E,C)))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_82]) ).
cnf(c_534,plain,
inverse(double_divide(A,inverse(double_divide(inverse(double_divide(B,double_divide(A,C))),double_divide(D,double_divide(E,C)))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_533]) ).
cnf(c_535,plain,
inverse(double_divide(A,inverse(double_divide(B,inverse(double_divide(double_divide(A,C),double_divide(D,double_divide(E,C)))))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_534]) ).
cnf(c_536,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(inverse(double_divide(inverse(double_divide(A,D)),C)),double_divide(E,C)))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_233,c_535]) ).
cnf(c_537,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(inverse(double_divide(A,inverse(double_divide(D,C)))),double_divide(E,C)))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_536]) ).
cnf(c_538,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(A,inverse(double_divide(inverse(double_divide(D,C)),double_divide(E,C)))))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_537]) ).
cnf(c_539,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(A,inverse(double_divide(D,inverse(double_divide(C,double_divide(E,C)))))))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_262,c_538]) ).
cnf(c_540,plain,
inverse(double_divide(B,double_divide(D,inverse(double_divide(C,double_divide(E,C)))))) = double_divide(inverse(double_divide(F,D)),double_divide(F,inverse(double_divide(E,B)))),
inference(paramod,[status(thm)],[c_320,c_539]) ).
cnf(c_541,plain,
inverse(double_divide(B,double_divide(D,inverse(double_divide(C,double_divide(E,C)))))) = double_divide(F,inverse(double_divide(D,double_divide(F,inverse(double_divide(E,B)))))),
inference(paramod,[status(thm)],[c_262,c_540]) ).
cnf(c_323,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(C,double_divide(D,C)))))) = double_divide(B,double_divide(D,A)),
inference(paramod,[status(thm)],[c_320,c_541]) ).
cnf(c_542,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(double_divide(C,inverse(double_divide(D,E)))))) = inverse(double_divide(D,double_divide(B,double_divide(C,E)))),
inference(paramod,[status(thm)],[c_262,c_23]) ).
cnf(c_543,plain,
double_divide(A,inverse(double_divide(B,double_divide(A,inverse(double_divide(C,inverse(double_divide(D,E)))))))) = inverse(double_divide(D,double_divide(B,double_divide(C,E)))),
inference(paramod,[status(thm)],[c_262,c_542]) ).
cnf(c_544,plain,
double_divide(B,double_divide(C,inverse(double_divide(D,E)))) = inverse(double_divide(D,double_divide(B,double_divide(C,E)))),
inference(paramod,[status(thm)],[c_320,c_543]) ).
cnf(c_326,plain,
inverse(double_divide(A,double_divide(B,double_divide(C,D)))) = double_divide(B,double_divide(C,inverse(double_divide(A,D)))),
inference(copy,[status(thm)],[c_544]) ).
cnf(c_545,plain,
inverse(double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,C))) = B,
inference(paramod,[status(thm)],[c_262,c_1]) ).
cnf(c_546,plain,
inverse(double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(A,C))))) = B,
inference(paramod,[status(thm)],[c_262,c_545]) ).
cnf(c_339,plain,
inverse(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,C))))))) = B,
inference(paramod,[status(thm)],[c_262,c_546]) ).
cnf(c_342,plain,
double_divide(inverse(inverse(double_divide(A,B))),A) = B,
inference(paramod,[status(thm)],[c_260,c_179]) ).
cnf(c_547,plain,
inverse(double_divide(inverse(inverse(double_divide(A,inverse(double_divide(B,double_divide(C,B)))))),double_divide(D,double_divide(D,A)))) = C,
inference(paramod,[status(thm)],[c_262,c_21]) ).
cnf(c_548,plain,
inverse(double_divide(inverse(inverse(double_divide(A,inverse(double_divide(B,double_divide(C,B)))))),A)) = C,
inference(paramod,[status(thm)],[c_260,c_547]) ).
cnf(c_346,plain,
inverse(inverse(double_divide(A,double_divide(B,A)))) = B,
inference(paramod,[status(thm)],[c_342,c_548]) ).
cnf(c_350,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,D),B))))) = double_divide(inverse(D),double_divide(C,A)),
inference(paramod,[status(thm)],[c_262,c_253]) ).
cnf(c_351,plain,
double_divide(A,inverse(double_divide(B,double_divide(A,inverse(C))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_262,c_251]) ).
cnf(c_549,plain,
double_divide(inverse(double_divide(A,B)),double_divide(A,inverse(double_divide(B,C)))) = C,
inference(paramod,[status(thm)],[c_262,c_238]) ).
cnf(c_550,plain,
double_divide(A,inverse(double_divide(B,double_divide(A,inverse(double_divide(B,C)))))) = C,
inference(paramod,[status(thm)],[c_262,c_549]) ).
cnf(c_359,plain,
double_divide(A,double_divide(A,B)) = B,
inference(paramod,[status(thm)],[c_351,c_550]) ).
cnf(c_551,plain,
double_divide(inverse(double_divide(inverse(inverse(double_divide(A,inverse(double_divide(B,double_divide(A,B)))))),C)),D) = double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),inverse(double_divide(double_divide(E,F),D))),
inference(paramod,[status(thm)],[c_262,c_234]) ).
cnf(c_552,plain,
double_divide(C,D) = double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),inverse(double_divide(double_divide(E,F),D))),
inference(paramod,[status(thm)],[c_288,c_551]) ).
cnf(c_553,plain,
double_divide(C,D) = double_divide(inverse(double_divide(E,inverse(double_divide(F,C)))),inverse(double_divide(double_divide(E,F),D))),
inference(paramod,[status(thm)],[c_262,c_552]) ).
cnf(c_554,plain,
double_divide(C,D) = double_divide(E,inverse(double_divide(inverse(double_divide(F,C)),inverse(double_divide(double_divide(E,F),D))))),
inference(paramod,[status(thm)],[c_262,c_553]) ).
cnf(c_555,plain,
double_divide(C,D) = double_divide(E,inverse(double_divide(F,inverse(double_divide(C,inverse(double_divide(double_divide(E,F),D))))))),
inference(paramod,[status(thm)],[c_262,c_554]) ).
cnf(c_362,plain,
double_divide(A,inverse(double_divide(B,inverse(double_divide(C,inverse(double_divide(double_divide(A,B),D))))))) = double_divide(C,D),
inference(copy,[status(thm)],[c_555]) ).
cnf(c_556,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(A,D)))) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_262,c_206]) ).
cnf(c_370,plain,
double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,D)))))) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_262,c_556]) ).
cnf(c_557,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,B))),D) = double_divide(C,D),
inference(paramod,[status(thm)],[c_262,c_182]) ).
cnf(c_558,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(A,B))))),D) = double_divide(C,D),
inference(paramod,[status(thm)],[c_262,c_557]) ).
cnf(c_559,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,B))))))),D) = double_divide(C,D),
inference(paramod,[status(thm)],[c_262,c_558]) ).
cnf(c_560,plain,
double_divide(inverse(inverse(double_divide(B,double_divide(B,C)))),D) = double_divide(C,D),
inference(paramod,[status(thm)],[c_370,c_559]) ).
cnf(c_380,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,B),
inference(paramod,[status(thm)],[c_359,c_560]) ).
cnf(c_561,plain,
inverse(B) = double_divide(inverse(double_divide(inverse(double_divide(C,double_divide(C,D))),D)),B),
inference(paramod,[status(thm)],[c_359,c_149]) ).
cnf(c_562,plain,
inverse(B) = double_divide(inverse(double_divide(inverse(D),D)),B),
inference(paramod,[status(thm)],[c_359,c_561]) ).
cnf(c_563,plain,
inverse(B) = double_divide(inverse(D),inverse(double_divide(D,B))),
inference(paramod,[status(thm)],[c_262,c_562]) ).
cnf(c_382,plain,
double_divide(inverse(A),inverse(double_divide(A,B))) = inverse(B),
inference(copy,[status(thm)],[c_563]) ).
cnf(c_564,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(C,inverse(double_divide(D,B))))) = double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),double_divide(E,inverse(double_divide(F,A))))),D),
inference(paramod,[status(thm)],[c_262,c_137]) ).
cnf(c_565,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(E,F)),C)),double_divide(E,inverse(double_divide(F,A))))),D),
inference(paramod,[status(thm)],[c_262,c_564]) ).
cnf(c_566,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(double_divide(inverse(double_divide(E,inverse(double_divide(F,C)))),double_divide(E,inverse(double_divide(F,A))))),D),
inference(paramod,[status(thm)],[c_262,c_565]) ).
cnf(c_567,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(double_divide(E,inverse(double_divide(inverse(double_divide(F,C)),double_divide(E,inverse(double_divide(F,A))))))),D),
inference(paramod,[status(thm)],[c_262,c_566]) ).
cnf(c_568,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(double_divide(E,inverse(double_divide(F,inverse(double_divide(C,double_divide(E,inverse(double_divide(F,A))))))))),D),
inference(paramod,[status(thm)],[c_262,c_567]) ).
cnf(c_569,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(inverse(double_divide(inverse(double_divide(F,A)),double_divide(F,C)))),D),
inference(paramod,[status(thm)],[c_370,c_568]) ).
cnf(c_570,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(inverse(inverse(double_divide(F,inverse(double_divide(A,double_divide(F,C)))))),D),
inference(paramod,[status(thm)],[c_262,c_569]) ).
cnf(c_384,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(double_divide(D,B))))))) = double_divide(double_divide(E,inverse(double_divide(A,double_divide(E,C)))),D),
inference(paramod,[status(thm)],[c_380,c_570]) ).
cnf(c_571,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),double_divide(A,D))),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(paramod,[status(thm)],[c_262,c_132]) ).
cnf(c_572,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(inverse(double_divide(B,C)),double_divide(A,D))))),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(paramod,[status(thm)],[c_262,c_571]) ).
cnf(c_573,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,D))))))),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(paramod,[status(thm)],[c_262,c_572]) ).
cnf(c_574,plain,
double_divide(inverse(inverse(double_divide(D,double_divide(B,C)))),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(paramod,[status(thm)],[c_370,c_573]) ).
cnf(c_575,plain,
double_divide(double_divide(D,double_divide(B,C)),E) = double_divide(C,inverse(double_divide(E,double_divide(inverse(double_divide(D,F)),double_divide(B,F))))),
inference(paramod,[status(thm)],[c_380,c_574]) ).
cnf(c_576,plain,
double_divide(double_divide(D,double_divide(B,C)),E) = double_divide(C,inverse(double_divide(E,double_divide(D,inverse(double_divide(F,double_divide(B,F))))))),
inference(paramod,[status(thm)],[c_262,c_575]) ).
cnf(c_386,plain,
double_divide(double_divide(A,double_divide(B,C)),D) = double_divide(C,double_divide(A,double_divide(B,D))),
inference(paramod,[status(thm)],[c_323,c_576]) ).
cnf(c_577,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,inverse(C))),C)),D) = double_divide(A,D),
inference(paramod,[status(thm)],[c_359,c_100]) ).
cnf(c_578,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(inverse(C),C)))),D) = double_divide(A,D),
inference(paramod,[status(thm)],[c_262,c_577]) ).
cnf(c_579,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(inverse(C),C)),D))) = double_divide(A,D),
inference(paramod,[status(thm)],[c_262,c_578]) ).
cnf(c_580,plain,
double_divide(A,inverse(double_divide(inverse(C),inverse(double_divide(C,D))))) = double_divide(A,D),
inference(paramod,[status(thm)],[c_262,c_579]) ).
cnf(c_390,plain,
double_divide(A,inverse(inverse(B))) = double_divide(A,B),
inference(paramod,[status(thm)],[c_382,c_580]) ).
cnf(c_581,plain,
inverse(double_divide(A,double_divide(B,double_divide(C,inverse(double_divide(D,double_divide(C,A))))))) = double_divide(inverse(double_divide(E,B)),double_divide(E,D)),
inference(paramod,[status(thm)],[c_262,c_39]) ).
cnf(c_582,plain,
double_divide(B,double_divide(C,inverse(double_divide(A,inverse(double_divide(D,double_divide(C,A))))))) = double_divide(inverse(double_divide(E,B)),double_divide(E,D)),
inference(paramod,[status(thm)],[c_326,c_581]) ).
cnf(c_583,plain,
double_divide(B,inverse(double_divide(A,double_divide(A,D)))) = double_divide(inverse(double_divide(E,B)),double_divide(E,D)),
inference(paramod,[status(thm)],[c_370,c_582]) ).
cnf(c_584,plain,
double_divide(B,inverse(D)) = double_divide(inverse(double_divide(E,B)),double_divide(E,D)),
inference(paramod,[status(thm)],[c_359,c_583]) ).
cnf(c_585,plain,
double_divide(B,inverse(D)) = double_divide(E,inverse(double_divide(B,double_divide(E,D)))),
inference(paramod,[status(thm)],[c_262,c_584]) ).
cnf(c_402,plain,
double_divide(A,inverse(double_divide(B,double_divide(A,C)))) = double_divide(B,inverse(C)),
inference(copy,[status(thm)],[c_585]) ).
cnf(c_586,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(inverse(inverse(double_divide(C,inverse(double_divide(D,double_divide(A,D)))))),B))) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_262,c_30]) ).
cnf(c_587,plain,
inverse(double_divide(inverse(double_divide(A,B)),double_divide(double_divide(C,inverse(double_divide(D,double_divide(A,D)))),B))) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_380,c_586]) ).
cnf(c_588,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(double_divide(D,double_divide(A,D)))),B))))) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_262,c_587]) ).
cnf(c_589,plain,
double_divide(inverse(inverse(double_divide(D,double_divide(A,D)))),double_divide(C,A)) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_350,c_588]) ).
cnf(c_590,plain,
double_divide(A,double_divide(C,A)) = double_divide(E,double_divide(E,C)),
inference(paramod,[status(thm)],[c_346,c_589]) ).
cnf(c_403,plain,
double_divide(A,double_divide(B,A)) = B,
inference(paramod,[status(thm)],[c_359,c_590]) ).
cnf(c_591,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,inverse(double_divide(C,D)))),double_divide(inverse(double_divide(E,C)),double_divide(E,A))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_262,c_14]) ).
cnf(c_592,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,inverse(double_divide(C,D)))),double_divide(E,inverse(double_divide(C,double_divide(E,A))))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_262,c_591]) ).
cnf(c_593,plain,
inverse(double_divide(A,double_divide(inverse(double_divide(B,inverse(double_divide(C,D)))),double_divide(C,inverse(A))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_402,c_592]) ).
cnf(c_594,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(inverse(double_divide(C,D)),double_divide(C,inverse(A))))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_262,c_593]) ).
cnf(c_595,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(C,inverse(double_divide(D,double_divide(C,inverse(A))))))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_262,c_594]) ).
cnf(c_596,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(D,inverse(inverse(A))))))) = double_divide(B,D),
inference(paramod,[status(thm)],[c_402,c_595]) ).
cnf(c_408,plain,
inverse(double_divide(A,double_divide(B,inverse(double_divide(C,A))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_390,c_596]) ).
cnf(c_597,plain,
inverse(double_divide(A,inverse(double_divide(B,double_divide(C,B))))) = double_divide(inverse(double_divide(D,C)),double_divide(D,A)),
inference(paramod,[status(thm)],[c_262,c_10]) ).
cnf(c_598,plain,
inverse(double_divide(A,inverse(C))) = double_divide(inverse(double_divide(D,C)),double_divide(D,A)),
inference(paramod,[status(thm)],[c_403,c_597]) ).
cnf(c_599,plain,
inverse(double_divide(A,inverse(C))) = double_divide(D,inverse(double_divide(C,double_divide(D,A)))),
inference(paramod,[status(thm)],[c_262,c_598]) ).
cnf(c_409,plain,
inverse(double_divide(A,inverse(B))) = double_divide(B,inverse(A)),
inference(paramod,[status(thm)],[c_402,c_599]) ).
cnf(c_600,plain,
inverse(double_divide(double_divide(A,B),inverse(inverse(D)))) = double_divide(A,inverse(double_divide(E,inverse(double_divide(B,double_divide(E,D)))))),
inference(paramod,[status(thm)],[c_403,c_278]) ).
cnf(c_601,plain,
inverse(double_divide(double_divide(A,B),D)) = double_divide(A,inverse(double_divide(E,inverse(double_divide(B,double_divide(E,D)))))),
inference(paramod,[status(thm)],[c_390,c_600]) ).
cnf(c_602,plain,
inverse(double_divide(double_divide(A,B),D)) = double_divide(A,inverse(double_divide(B,inverse(D)))),
inference(paramod,[status(thm)],[c_402,c_601]) ).
cnf(c_412,plain,
inverse(double_divide(double_divide(A,B),C)) = double_divide(A,double_divide(C,inverse(B))),
inference(paramod,[status(thm)],[c_409,c_602]) ).
cnf(c_603,plain,
inverse(double_divide(A,inverse(double_divide(B,inverse(A))))) = B,
inference(paramod,[status(thm)],[c_403,c_339]) ).
cnf(c_604,plain,
inverse(double_divide(A,double_divide(A,inverse(B)))) = B,
inference(paramod,[status(thm)],[c_409,c_603]) ).
cnf(c_432,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_359,c_604]) ).
cnf(c_605,plain,
inverse(double_divide(A,double_divide(C,D))) = double_divide(double_divide(E,inverse(double_divide(A,double_divide(E,C)))),D),
inference(paramod,[status(thm)],[c_408,c_384]) ).
cnf(c_443,plain,
inverse(double_divide(A,double_divide(B,C))) = double_divide(double_divide(A,inverse(B)),C),
inference(paramod,[status(thm)],[c_402,c_605]) ).
cnf(c_606,plain,
inverse(double_divide(A,inverse(double_divide(C,D)))) = double_divide(inverse(D),double_divide(C,A)),
inference(paramod,[status(thm)],[c_403,c_350]) ).
cnf(c_453,plain,
double_divide(double_divide(A,B),inverse(C)) = double_divide(inverse(B),double_divide(A,C)),
inference(paramod,[status(thm)],[c_409,c_606]) ).
cnf(c_607,plain,
double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(A)),D)))) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_443,c_370]) ).
cnf(c_608,plain,
double_divide(A,double_divide(double_divide(B,inverse(double_divide(C,inverse(A)))),D)) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_443,c_607]) ).
cnf(c_609,plain,
double_divide(A,double_divide(double_divide(B,double_divide(A,inverse(C))),D)) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_409,c_608]) ).
cnf(c_610,plain,
double_divide(A,double_divide(inverse(C),double_divide(B,double_divide(A,D)))) = inverse(double_divide(D,double_divide(B,C))),
inference(paramod,[status(thm)],[c_386,c_609]) ).
cnf(c_461,plain,
double_divide(A,double_divide(inverse(B),double_divide(C,double_divide(A,D)))) = double_divide(double_divide(D,inverse(C)),B),
inference(paramod,[status(thm)],[c_443,c_610]) ).
cnf(c_611,plain,
double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(A,double_divide(D,inverse(B)))))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_412,c_362]) ).
cnf(c_612,plain,
double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(A)),double_divide(D,inverse(B)))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_443,c_611]) ).
cnf(c_613,plain,
double_divide(A,double_divide(double_divide(B,inverse(double_divide(C,inverse(A)))),double_divide(D,inverse(B)))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_443,c_612]) ).
cnf(c_614,plain,
double_divide(A,double_divide(double_divide(B,double_divide(A,inverse(C))),double_divide(D,inverse(B)))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_409,c_613]) ).
cnf(c_615,plain,
double_divide(A,double_divide(inverse(C),double_divide(B,double_divide(A,double_divide(D,inverse(B)))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_386,c_614]) ).
cnf(c_616,plain,
double_divide(double_divide(double_divide(D,inverse(B)),inverse(B)),C) = double_divide(C,D),
inference(paramod,[status(thm)],[c_461,c_615]) ).
cnf(c_617,plain,
double_divide(double_divide(inverse(inverse(B)),double_divide(D,B)),C) = double_divide(C,D),
inference(paramod,[status(thm)],[c_453,c_616]) ).
cnf(c_618,plain,
double_divide(double_divide(B,double_divide(D,B)),C) = double_divide(C,D),
inference(paramod,[status(thm)],[c_432,c_617]) ).
cnf(c_463,plain,
double_divide(A,B) = double_divide(B,A),
inference(paramod,[status(thm)],[c_403,c_618]) ).
cnf(c_619,plain,
inverse(double_divide(a,b)) != inverse(double_divide(a,b)),
inference(paramod,[status(thm)],[c_463,c_4]) ).
cnf(c_483,plain,
$false,
inference(copy,[status(thm)],[c_619]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP612-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n011.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 15:02:14 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.43 % Process 2309731 was started by sandbox2 on n011,
% 0.16/0.43 % Fri Sep 25 15:02:14 2026
% 0.16/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.44
% 0.16/0.44 % From the command line: assign(max_seconds, 300).
% 0.16/0.53
% 0.16/0.53 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 0.16/0.53
% 0.16/0.53 % SZS status Unsatisfiable for theBenchmark
% 0.16/0.53
% 0.16/0.53 % Proof 1 at 0.06 (+ 0.02) seconds.
% 0.16/0.53 % Length of proof is 79.
% 0.16/0.53 % Level of proof is 18.
% 0.16/0.53 % Maximum clause weight is 90.000.
% 0.16/0.53 % Given clauses 13.
% 0.16/0.53
% 0.16/0.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------