%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP106-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 : n003.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:27:20 AM UTC 2026
% Result : Unsatisfiable 0.02s 0.47s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 3
% Syntax : Number of formulae : 198 ( 170 unt; 0 def)
% Number of atoms : 259 ( 258 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 151 ( 90 ~; 61 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 631 ( 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,axiom,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('theBenchmark.p',prove_these_axioms) ).
cnf(c_3,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(clausify,[status(thm)],[prove_these_axioms]) ).
cnf(c_471,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| inverse(double_divide(a1,inverse(a1))) != multiply(inverse(b1),b1) ),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_472,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_471]) ).
cnf(c_473,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(double_divide(b2,inverse(b2))),a2) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_472]) ).
cnf(c_474,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_473]) ).
cnf(c_475,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(inverse(double_divide(b3,a3)),c3) != multiply(a3,multiply(b3,c3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_474]) ).
cnf(c_476,plain,
( multiply(a4,b4) != multiply(b4,a4)
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != multiply(a3,multiply(b3,c3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_475]) ).
cnf(c_477,plain,
( multiply(a4,b4) != multiply(b4,a4)
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != multiply(a3,inverse(double_divide(c3,b3)))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_476]) ).
cnf(c_478,plain,
( multiply(a4,b4) != multiply(b4,a4)
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_477]) ).
cnf(c_479,plain,
( inverse(double_divide(b4,a4)) != multiply(b4,a4)
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_478]) ).
cnf(c_480,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))) ),
inference(paramod,[status(thm)],[c_2,c_479]) ).
cnf(c_481,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(copy,[status(thm)],[c_480]) ).
cnf(c_4,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(copy,[status(thm)],[c_481]) ).
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_482,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_482]) ).
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_483,plain,
multiply(inverse(double_divide(A,B)),double_divide(C,B)) = inverse(inverse(double_divide(double_divide(D,A),inverse(double_divide(D,C))))),
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_484,plain,
inverse(double_divide(double_divide(C,B),inverse(double_divide(A,B)))) = inverse(inverse(double_divide(double_divide(D,A),inverse(double_divide(D,C))))),
inference(paramod,[status(thm)],[c_2,c_483]) ).
cnf(c_24,plain,
inverse(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C))))) = inverse(double_divide(double_divide(C,D),inverse(double_divide(B,D)))),
inference(copy,[status(thm)],[c_484]) ).
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_39,plain,
inverse(double_divide(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,B))),D),A)) = double_divide(double_divide(C,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_40,plain,
inverse(double_divide(double_divide(double_divide(A,B),C),double_divide(double_divide(D,E),inverse(double_divide(B,E))))) = double_divide(double_divide(inverse(double_divide(A,D)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_9,c_9]) ).
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_43,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))),inverse(double_divide(double_divide(C,D),E)))) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(B,D)),F))),
inference(paramod,[status(thm)],[c_9,c_9]) ).
cnf(c_54,plain,
inverse(double_divide(double_divide(A,inverse(B)),inverse(double_divide(A,C)))) = double_divide(double_divide(inverse(double_divide(B,C)),D),D),
inference(paramod,[status(thm)],[c_19,c_5]) ).
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_69,plain,
double_divide(double_divide(inverse(A),B),inverse(double_divide(inverse(double_divide(C,D)),B))) = double_divide(inverse(double_divide(A,C)),D),
inference(paramod,[status(thm)],[c_19,c_19]) ).
cnf(c_485,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_485]) ).
cnf(c_84,plain,
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_41,c_9]) ).
cnf(c_486,plain,
multiply(A,double_divide(B,A)) = inverse(double_divide(double_divide(B,C),C)),
inference(paramod,[status(thm)],[c_76,c_2]) ).
cnf(c_97,plain,
inverse(double_divide(double_divide(A,B),B)) = inverse(double_divide(double_divide(A,C),C)),
inference(paramod,[status(thm)],[c_2,c_486]) ).
cnf(c_106,plain,
inverse(double_divide(double_divide(A,B),B)) = double_divide(double_divide(C,D),inverse(double_divide(inverse(double_divide(A,C)),D))),
inference(paramod,[status(thm)],[c_76,c_9]) ).
cnf(c_117,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,C)))),inverse(double_divide(B,D)))) = inverse(double_divide(double_divide(double_divide(C,D),E),E)),
inference(paramod,[status(thm)],[c_9,c_97]) ).
cnf(c_149,plain,
inverse(double_divide(double_divide(A,B),B)) = double_divide(A,inverse(double_divide(C,inverse(double_divide(double_divide(C,D),D))))),
inference(paramod,[status(thm)],[c_76,c_7]) ).
cnf(c_487,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(C))))) = inverse(double_divide(double_divide(C,inverse(double_divide(D,B))),D)),
inference(paramod,[status(thm)],[c_16,c_1]) ).
cnf(c_153,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)) = inverse(double_divide(double_divide(D,C),inverse(double_divide(D,inverse(A))))),
inference(copy,[status(thm)],[c_487]) ).
cnf(c_161,plain,
inverse(double_divide(double_divide(inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)),D),inverse(A))) = double_divide(double_divide(C,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_16,c_9]) ).
cnf(c_488,plain,
double_divide(double_divide(inverse(A),B),inverse(double_divide(C,B))) = inverse(double_divide(double_divide(A,inverse(double_divide(D,C))),D)),
inference(paramod,[status(thm)],[c_16,c_19]) ).
cnf(c_167,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)) = double_divide(double_divide(inverse(A),D),inverse(double_divide(C,D))),
inference(copy,[status(thm)],[c_488]) ).
cnf(c_489,plain,
double_divide(double_divide(A,B),inverse(C)) = double_divide(double_divide(A,D),inverse(double_divide(inverse(double_divide(double_divide(C,inverse(double_divide(E,B))),E)),D))),
inference(paramod,[status(thm)],[c_16,c_41]) ).
cnf(c_171,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(double_divide(C,inverse(double_divide(D,E))),D)),B))) = double_divide(double_divide(A,E),inverse(C)),
inference(copy,[status(thm)],[c_489]) ).
cnf(c_176,plain,
inverse(double_divide(double_divide(A,inverse(B)),inverse(double_divide(A,double_divide(C,D))))) = double_divide(inverse(double_divide(double_divide(B,inverse(double_divide(E,F))),E)),inverse(double_divide(C,inverse(double_divide(F,D))))),
inference(paramod,[status(thm)],[c_16,c_7]) ).
cnf(c_177,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,D)))) = double_divide(B,inverse(double_divide(inverse(double_divide(double_divide(D,inverse(double_divide(E,F))),E)),inverse(double_divide(C,F))))),
inference(paramod,[status(thm)],[c_16,c_7]) ).
cnf(c_490,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,double_divide(double_divide(D,E),inverse(double_divide(D,E))))))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_84,c_1]) ).
cnf(c_181,plain,
double_divide(A,inverse(double_divide(double_divide(B,C),inverse(double_divide(D,inverse(double_divide(B,C))))))) = double_divide(A,D),
inference(paramod,[status(thm)],[c_7,c_490]) ).
cnf(c_491,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(double_divide(C,D),inverse(double_divide(E,inverse(double_divide(C,D)))))))) = E,
inference(paramod,[status(thm)],[c_84,c_1]) ).
cnf(c_183,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),C)) = C,
inference(paramod,[status(thm)],[c_181,c_491]) ).
cnf(c_492,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(double_divide(C,inverse(double_divide(D,E))),D)))) = double_divide(C,E),
inference(paramod,[status(thm)],[c_84,c_5]) ).
cnf(c_191,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),B)) = double_divide(A,C),
inference(paramod,[status(thm)],[c_183,c_492]) ).
cnf(c_493,plain,
inverse(double_divide(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(C,inverse(double_divide(D,E))))),C)) = double_divide(D,E),
inference(paramod,[status(thm)],[c_84,c_6]) ).
cnf(c_196,plain,
double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(C,D))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_191,c_493]) ).
cnf(c_198,plain,
inverse(double_divide(double_divide(double_divide(double_divide(A,B),inverse(double_divide(C,B))),C),A)) = double_divide(double_divide(D,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_6,c_84]) ).
cnf(c_200,plain,
inverse(double_divide(double_divide(double_divide(A,B),C),double_divide(double_divide(D,E),inverse(double_divide(D,E))))) = double_divide(double_divide(inverse(double_divide(A,B)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_84,c_9]) ).
cnf(c_494,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(double_divide(C,D),E)))) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(C,D)),F))),
inference(paramod,[status(thm)],[c_84,c_9]) ).
cnf(c_495,plain,
inverse(double_divide(double_divide(C,D),E)) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(C,D)),F))),
inference(paramod,[status(thm)],[c_196,c_494]) ).
cnf(c_203,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(C,D)),B))) = inverse(double_divide(double_divide(C,D),A)),
inference(copy,[status(thm)],[c_495]) ).
cnf(c_496,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,double_divide(C,D))))) = double_divide(inverse(double_divide(double_divide(E,F),inverse(double_divide(E,F)))),inverse(double_divide(B,inverse(double_divide(C,D))))),
inference(paramod,[status(thm)],[c_84,c_9]) ).
cnf(c_205,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,double_divide(C,D))))) = double_divide(B,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_196,c_496]) ).
cnf(c_221,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(inverse(double_divide(double_divide(D,E),inverse(double_divide(D,E)))))) = double_divide(double_divide(A,F),inverse(double_divide(double_divide(B,C),F))),
inference(paramod,[status(thm)],[c_84,c_41]) ).
cnf(c_497,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),inverse(double_divide(A,B)))),inverse(double_divide(double_divide(C,D),double_divide(E,F))))) = double_divide(C,inverse(double_divide(E,inverse(double_divide(D,F))))),
inference(paramod,[status(thm)],[c_84,c_7]) ).
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_196,c_497]) ).
cnf(c_498,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,double_divide(double_divide(C,D),D))))) = double_divide(B,inverse(inverse(double_divide(double_divide(E,F),inverse(double_divide(E,F)))))),
inference(paramod,[status(thm)],[c_84,c_7]) ).
cnf(c_234,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(double_divide(B,C),C))) = double_divide(A,inverse(inverse(double_divide(double_divide(D,E),inverse(double_divide(D,E)))))),
inference(paramod,[status(thm)],[c_205,c_498]) ).
cnf(c_246,plain,
inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(A,D)))) = double_divide(B,inverse(double_divide(double_divide(D,E),inverse(double_divide(C,E))))),
inference(paramod,[status(thm)],[c_191,c_177]) ).
cnf(c_499,plain,
double_divide(inverse(B),inverse(double_divide(C,D))) = double_divide(inverse(double_divide(double_divide(B,inverse(double_divide(E,F))),E)),inverse(double_divide(C,inverse(double_divide(F,D))))),
inference(paramod,[status(thm)],[c_205,c_176]) ).
cnf(c_500,plain,
double_divide(inverse(B),inverse(double_divide(C,D))) = double_divide(double_divide(B,F),inverse(double_divide(C,inverse(double_divide(F,D))))),
inference(paramod,[status(thm)],[c_191,c_499]) ).
cnf(c_247,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,inverse(double_divide(B,D))))) = double_divide(inverse(A),inverse(double_divide(C,D))),
inference(copy,[status(thm)],[c_500]) ).
cnf(c_248,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(C,D),B))) = double_divide(double_divide(A,D),inverse(C)),
inference(paramod,[status(thm)],[c_191,c_171]) ).
cnf(c_501,plain,
double_divide(A,C) = double_divide(double_divide(inverse(A),D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_191,c_167]) ).
cnf(c_251,plain,
double_divide(double_divide(inverse(A),B),inverse(double_divide(C,B))) = double_divide(A,C),
inference(copy,[status(thm)],[c_501]) ).
cnf(c_253,plain,
inverse(double_divide(double_divide(double_divide(A,B),C),inverse(A))) = double_divide(double_divide(B,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_191,c_161]) ).
cnf(c_502,plain,
double_divide(A,C) = inverse(double_divide(double_divide(D,C),inverse(double_divide(D,inverse(A))))),
inference(paramod,[status(thm)],[c_191,c_153]) ).
cnf(c_257,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(C))))) = double_divide(C,B),
inference(copy,[status(thm)],[c_502]) ).
cnf(c_503,plain,
double_divide(A,inverse(double_divide(C,D))) = double_divide(inverse(double_divide(A,C)),D),
inference(paramod,[status(thm)],[c_191,c_59]) ).
cnf(c_261,plain,
double_divide(inverse(double_divide(A,B)),C) = double_divide(A,inverse(double_divide(B,C))),
inference(copy,[status(thm)],[c_503]) ).
cnf(c_264,plain,
double_divide(double_divide(A,B),B) = A,
inference(paramod,[status(thm)],[c_191,c_16]) ).
cnf(c_504,plain,
inverse(A) = double_divide(double_divide(C,D),inverse(double_divide(inverse(double_divide(A,C)),D))),
inference(paramod,[status(thm)],[c_264,c_106]) ).
cnf(c_505,plain,
inverse(A) = double_divide(double_divide(C,D),inverse(double_divide(A,inverse(double_divide(C,D))))),
inference(paramod,[status(thm)],[c_261,c_504]) ).
cnf(c_266,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,inverse(double_divide(A,B))))) = inverse(C),
inference(copy,[status(thm)],[c_505]) ).
cnf(c_506,plain,
double_divide(double_divide(inverse(A),B),inverse(double_divide(C,inverse(double_divide(D,B))))) = double_divide(inverse(double_divide(A,C)),D),
inference(paramod,[status(thm)],[c_261,c_69]) ).
cnf(c_268,plain,
double_divide(double_divide(inverse(A),B),inverse(double_divide(C,inverse(double_divide(D,B))))) = double_divide(A,inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_261,c_506]) ).
cnf(c_507,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(A,C)),inverse(double_divide(double_divide(C,D),E)))))) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(B,D)),F))),
inference(paramod,[status(thm)],[c_261,c_43]) ).
cnf(c_508,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(double_divide(C,D),E)))))))) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(B,D)),F))),
inference(paramod,[status(thm)],[c_261,c_507]) ).
cnf(c_509,plain,
double_divide(double_divide(C,inverse(double_divide(double_divide(C,D),E))),B) = double_divide(double_divide(E,F),inverse(double_divide(inverse(double_divide(B,D)),F))),
inference(paramod,[status(thm)],[c_257,c_508]) ).
cnf(c_271,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(A,B),C))),D) = double_divide(double_divide(C,E),inverse(double_divide(D,inverse(double_divide(B,E))))),
inference(paramod,[status(thm)],[c_261,c_509]) ).
cnf(c_510,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_261,c_35]) ).
cnf(c_511,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(C,D),inverse(double_divide(inverse(double_divide(A,D)),B))))) = C,
inference(paramod,[status(thm)],[c_261,c_510]) ).
cnf(c_512,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(C,D),inverse(double_divide(A,inverse(double_divide(D,B))))))) = C,
inference(paramod,[status(thm)],[c_261,c_511]) ).
cnf(c_513,plain,
double_divide(double_divide(A,B),inverse(double_divide(inverse(C),inverse(double_divide(A,B))))) = C,
inference(paramod,[status(thm)],[c_247,c_512]) ).
cnf(c_272,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_266,c_513]) ).
cnf(c_514,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(D,E),inverse(double_divide(C,inverse(double_divide(D,E))))))) = double_divide(double_divide(inverse(double_divide(A,B)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_231,c_200]) ).
cnf(c_515,plain,
double_divide(double_divide(A,B),inverse(inverse(C))) = double_divide(double_divide(inverse(double_divide(A,B)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_266,c_514]) ).
cnf(c_516,plain,
double_divide(double_divide(A,B),C) = double_divide(double_divide(inverse(double_divide(A,B)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_272,c_515]) ).
cnf(c_517,plain,
double_divide(double_divide(A,B),C) = double_divide(double_divide(A,inverse(double_divide(B,F))),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_261,c_516]) ).
cnf(c_280,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),inverse(double_divide(D,C))) = double_divide(double_divide(A,B),D),
inference(copy,[status(thm)],[c_517]) ).
cnf(c_518,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(A,C)),inverse(double_divide(B,D)))))) = inverse(double_divide(double_divide(double_divide(C,D),E),E)),
inference(paramod,[status(thm)],[c_261,c_117]) ).
cnf(c_519,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(C,inverse(double_divide(B,D)))))))) = inverse(double_divide(double_divide(double_divide(C,D),E),E)),
inference(paramod,[status(thm)],[c_261,c_518]) ).
cnf(c_520,plain,
double_divide(double_divide(C,inverse(double_divide(B,D))),B) = inverse(double_divide(double_divide(double_divide(C,D),E),E)),
inference(paramod,[status(thm)],[c_257,c_519]) ).
cnf(c_283,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),B) = inverse(double_divide(A,C)),
inference(paramod,[status(thm)],[c_264,c_520]) ).
cnf(c_521,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(D,E),inverse(double_divide(C,inverse(double_divide(B,E))))))) = double_divide(double_divide(inverse(double_divide(A,D)),F),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_231,c_40]) ).
cnf(c_522,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(D,E),inverse(double_divide(C,inverse(double_divide(B,E))))))) = double_divide(double_divide(A,inverse(double_divide(D,F))),inverse(double_divide(C,F))),
inference(paramod,[status(thm)],[c_261,c_521]) ).
cnf(c_290,plain,
double_divide(double_divide(A,B),inverse(double_divide(double_divide(C,D),inverse(double_divide(E,inverse(double_divide(B,D))))))) = double_divide(double_divide(A,C),E),
inference(paramod,[status(thm)],[c_280,c_522]) ).
cnf(c_523,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(double_divide(D,E),inverse(double_divide(D,E)))) = double_divide(double_divide(A,F),inverse(double_divide(double_divide(B,C),F))),
inference(paramod,[status(thm)],[c_272,c_221]) ).
cnf(c_293,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(double_divide(D,E),inverse(double_divide(D,E)))) = double_divide(double_divide(A,C),inverse(B)),
inference(paramod,[status(thm)],[c_248,c_523]) ).
cnf(c_524,plain,
double_divide(inverse(double_divide(A,B)),inverse(B)) = double_divide(A,inverse(inverse(double_divide(double_divide(D,E),inverse(double_divide(D,E)))))),
inference(paramod,[status(thm)],[c_264,c_234]) ).
cnf(c_525,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,inverse(inverse(double_divide(double_divide(D,E),inverse(double_divide(D,E)))))),
inference(paramod,[status(thm)],[c_261,c_524]) ).
cnf(c_307,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,double_divide(double_divide(C,D),inverse(double_divide(C,D)))),
inference(paramod,[status(thm)],[c_272,c_525]) ).
cnf(c_308,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,inverse(double_divide(D,B))))) = inverse(double_divide(double_divide(C,D),A)),
inference(paramod,[status(thm)],[c_261,c_203]) ).
cnf(c_320,plain,
inverse(double_divide(double_divide(A,inverse(B)),inverse(double_divide(A,C)))) = double_divide(double_divide(B,inverse(double_divide(C,D))),D),
inference(paramod,[status(thm)],[c_261,c_54]) ).
cnf(c_526,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(inverse(double_divide(A,C)),B)))) = C,
inference(paramod,[status(thm)],[c_261,c_38]) ).
cnf(c_527,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(A,inverse(double_divide(C,B)))))) = C,
inference(paramod,[status(thm)],[c_261,c_526]) ).
cnf(c_528,plain,
inverse(inverse(double_divide(double_divide(A,C),A))) = C,
inference(paramod,[status(thm)],[c_308,c_527]) ).
cnf(c_323,plain,
double_divide(double_divide(A,B),A) = B,
inference(paramod,[status(thm)],[c_272,c_528]) ).
cnf(c_529,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_261,c_4]) ).
cnf(c_326,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(copy,[status(thm)],[c_529]) ).
cnf(c_530,plain,
inverse(A) = double_divide(A,inverse(double_divide(C,inverse(double_divide(double_divide(C,D),D))))),
inference(paramod,[status(thm)],[c_264,c_149]) ).
cnf(c_531,plain,
inverse(A) = double_divide(A,inverse(double_divide(C,inverse(C)))),
inference(paramod,[status(thm)],[c_264,c_530]) ).
cnf(c_327,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = inverse(A),
inference(copy,[status(thm)],[c_531]) ).
cnf(c_532,plain,
double_divide(double_divide(A,B),inverse(double_divide(A,C))) = inverse(double_divide(double_divide(C,D),inverse(double_divide(B,D)))),
inference(paramod,[status(thm)],[c_272,c_24]) ).
cnf(c_332,plain,
inverse(double_divide(double_divide(A,B),inverse(double_divide(C,B)))) = double_divide(double_divide(D,C),inverse(double_divide(D,A))),
inference(copy,[status(thm)],[c_532]) ).
cnf(c_533,plain,
inverse(double_divide(inverse(double_divide(double_divide(A,B),B)),A)) = double_divide(double_divide(D,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_283,c_198]) ).
cnf(c_334,plain,
inverse(double_divide(inverse(A),A)) = double_divide(double_divide(B,C),inverse(double_divide(B,C))),
inference(paramod,[status(thm)],[c_264,c_533]) ).
cnf(c_534,plain,
double_divide(double_divide(A,B),inverse(inverse(double_divide(double_divide(E,B),C)))) = double_divide(double_divide(A,C),E),
inference(paramod,[status(thm)],[c_308,c_290]) ).
cnf(c_335,plain,
double_divide(double_divide(A,B),double_divide(double_divide(C,B),D)) = double_divide(double_divide(A,D),C),
inference(paramod,[status(thm)],[c_272,c_534]) ).
cnf(c_336,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(A,B),C))),D) = inverse(double_divide(double_divide(D,B),C)),
inference(paramod,[status(thm)],[c_308,c_271]) ).
cnf(c_338,plain,
inverse(double_divide(double_divide(A,B),inverse(C))) = double_divide(C,inverse(double_divide(A,B))),
inference(paramod,[status(thm)],[c_308,c_268]) ).
cnf(c_535,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(inverse(a2)) != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_327,c_326]) ).
cnf(c_536,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| a2 != a2
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_272,c_535]) ).
cnf(c_342,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(copy,[status(thm)],[c_536]) ).
cnf(c_537,plain,
inverse(A) = double_divide(A,double_divide(double_divide(C,D),inverse(double_divide(C,D)))),
inference(paramod,[status(thm)],[c_327,c_307]) ).
cnf(c_343,plain,
double_divide(A,double_divide(double_divide(B,C),inverse(double_divide(B,C)))) = inverse(A),
inference(copy,[status(thm)],[c_537]) ).
cnf(c_344,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,B))) = double_divide(double_divide(D,A),inverse(double_divide(D,C))),
inference(paramod,[status(thm)],[c_338,c_332]) ).
cnf(c_538,plain,
double_divide(double_divide(A,C),inverse(double_divide(A,inverse(B)))) = double_divide(double_divide(B,inverse(double_divide(C,D))),D),
inference(paramod,[status(thm)],[c_338,c_320]) ).
cnf(c_347,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),C) = double_divide(double_divide(D,B),inverse(double_divide(D,inverse(A)))),
inference(copy,[status(thm)],[c_538]) ).
cnf(c_355,plain,
double_divide(double_divide(A,inverse(B)),inverse(double_divide(A,C))) = double_divide(B,C),
inference(paramod,[status(thm)],[c_338,c_257]) ).
cnf(c_539,plain,
double_divide(A,inverse(double_divide(double_divide(A,B),C))) = double_divide(double_divide(B,D),inverse(double_divide(C,D))),
inference(paramod,[status(thm)],[c_338,c_253]) ).
cnf(c_356,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,B))) = double_divide(D,inverse(double_divide(double_divide(D,A),C))),
inference(copy,[status(thm)],[c_539]) ).
cnf(c_540,plain,
inverse(double_divide(double_divide(B,C),D)) = double_divide(B,inverse(double_divide(double_divide(D,E),inverse(double_divide(C,E))))),
inference(paramod,[status(thm)],[c_355,c_246]) ).
cnf(c_541,plain,
inverse(double_divide(double_divide(B,C),D)) = double_divide(B,double_divide(double_divide(C,E),inverse(double_divide(D,E)))),
inference(paramod,[status(thm)],[c_338,c_540]) ).
cnf(c_358,plain,
double_divide(A,double_divide(double_divide(B,C),inverse(double_divide(D,C)))) = inverse(double_divide(double_divide(A,B),D)),
inference(copy,[status(thm)],[c_541]) ).
cnf(c_364,plain,
inverse(double_divide(A,inverse(double_divide(B,C)))) = double_divide(double_divide(A,C),inverse(B)),
inference(paramod,[status(thm)],[c_343,c_293]) ).
cnf(c_542,plain,
double_divide(double_divide(A,B),double_divide(double_divide(C,B),inverse(D))) = inverse(double_divide(double_divide(C,D),A)),
inference(paramod,[status(thm)],[c_364,c_308]) ).
cnf(c_543,plain,
double_divide(double_divide(A,inverse(D)),C) = inverse(double_divide(double_divide(C,D),A)),
inference(paramod,[status(thm)],[c_335,c_542]) ).
cnf(c_378,plain,
inverse(double_divide(double_divide(A,B),C)) = double_divide(double_divide(C,inverse(B)),A),
inference(copy,[status(thm)],[c_543]) ).
cnf(c_544,plain,
double_divide(double_divide(A,inverse(D)),double_divide(double_divide(A,B),inverse(double_divide(C,B)))) = double_divide(double_divide(C,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_378,c_39]) ).
cnf(c_545,plain,
inverse(double_divide(double_divide(double_divide(A,inverse(D)),A),C)) = double_divide(double_divide(C,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_358,c_544]) ).
cnf(c_546,plain,
inverse(double_divide(inverse(D),C)) = double_divide(double_divide(C,E),inverse(double_divide(D,E))),
inference(paramod,[status(thm)],[c_323,c_545]) ).
cnf(c_395,plain,
double_divide(double_divide(A,B),inverse(double_divide(C,B))) = inverse(double_divide(inverse(C),A)),
inference(copy,[status(thm)],[c_546]) ).
cnf(c_547,plain,
inverse(double_divide(inverse(C),A)) = double_divide(D,inverse(double_divide(double_divide(D,A),C))),
inference(paramod,[status(thm)],[c_395,c_356]) ).
cnf(c_548,plain,
inverse(double_divide(inverse(C),A)) = double_divide(D,double_divide(double_divide(C,inverse(A)),D)),
inference(paramod,[status(thm)],[c_378,c_547]) ).
cnf(c_400,plain,
double_divide(A,double_divide(double_divide(B,inverse(C)),A)) = inverse(double_divide(inverse(B),C)),
inference(copy,[status(thm)],[c_548]) ).
cnf(c_549,plain,
double_divide(double_divide(A,double_divide(double_divide(C,inverse(B)),A)),D) = inverse(double_divide(double_divide(D,B),C)),
inference(paramod,[status(thm)],[c_378,c_336]) ).
cnf(c_550,plain,
double_divide(inverse(double_divide(inverse(C),B)),D) = inverse(double_divide(double_divide(D,B),C)),
inference(paramod,[status(thm)],[c_400,c_549]) ).
cnf(c_551,plain,
double_divide(inverse(C),inverse(double_divide(B,D))) = inverse(double_divide(double_divide(D,B),C)),
inference(paramod,[status(thm)],[c_261,c_550]) ).
cnf(c_552,plain,
double_divide(inverse(C),inverse(double_divide(B,D))) = double_divide(double_divide(C,inverse(B)),D),
inference(paramod,[status(thm)],[c_378,c_551]) ).
cnf(c_403,plain,
double_divide(double_divide(A,inverse(B)),C) = double_divide(inverse(A),inverse(double_divide(B,C))),
inference(copy,[status(thm)],[c_552]) ).
cnf(c_553,plain,
inverse(double_divide(inverse(C),A)) = double_divide(double_divide(D,A),inverse(double_divide(D,C))),
inference(paramod,[status(thm)],[c_395,c_344]) ).
cnf(c_410,plain,
double_divide(double_divide(A,B),inverse(double_divide(A,C))) = inverse(double_divide(inverse(C),B)),
inference(copy,[status(thm)],[c_553]) ).
cnf(c_412,plain,
inverse(double_divide(inverse(A),A)) = inverse(double_divide(inverse(B),B)),
inference(paramod,[status(thm)],[c_410,c_334]) ).
cnf(c_414,plain,
inverse(double_divide(inverse(A),inverse(B))) = double_divide(B,A),
inference(paramod,[status(thm)],[c_395,c_251]) ).
cnf(c_554,plain,
double_divide(inverse(A),inverse(double_divide(double_divide(B,C),C))) = double_divide(double_divide(D,B),inverse(double_divide(D,inverse(A)))),
inference(paramod,[status(thm)],[c_403,c_347]) ).
cnf(c_555,plain,
double_divide(inverse(A),inverse(B)) = double_divide(double_divide(D,B),inverse(double_divide(D,inverse(A)))),
inference(paramod,[status(thm)],[c_264,c_554]) ).
cnf(c_556,plain,
double_divide(inverse(A),inverse(B)) = inverse(double_divide(inverse(inverse(A)),B)),
inference(paramod,[status(thm)],[c_410,c_555]) ).
cnf(c_557,plain,
double_divide(inverse(A),inverse(B)) = inverse(double_divide(A,B)),
inference(paramod,[status(thm)],[c_272,c_556]) ).
cnf(c_429,plain,
inverse(double_divide(A,B)) = double_divide(inverse(A),inverse(B)),
inference(copy,[status(thm)],[c_557]) ).
cnf(c_558,plain,
double_divide(inverse(inverse(A)),inverse(inverse(B))) = double_divide(B,A),
inference(paramod,[status(thm)],[c_429,c_414]) ).
cnf(c_559,plain,
double_divide(A,inverse(inverse(B))) = double_divide(B,A),
inference(paramod,[status(thm)],[c_272,c_558]) ).
cnf(c_455,plain,
double_divide(A,B) = double_divide(B,A),
inference(paramod,[status(thm)],[c_272,c_559]) ).
cnf(c_560,plain,
inverse(double_divide(A,inverse(A))) = inverse(double_divide(inverse(B),B)),
inference(paramod,[status(thm)],[c_455,c_412]) ).
cnf(c_561,plain,
double_divide(inverse(A),inverse(inverse(A))) = inverse(double_divide(inverse(B),B)),
inference(paramod,[status(thm)],[c_429,c_560]) ).
cnf(c_562,plain,
double_divide(inverse(A),A) = inverse(double_divide(inverse(B),B)),
inference(paramod,[status(thm)],[c_272,c_561]) ).
cnf(c_563,plain,
double_divide(A,inverse(A)) = inverse(double_divide(inverse(B),B)),
inference(paramod,[status(thm)],[c_455,c_562]) ).
cnf(c_564,plain,
double_divide(A,inverse(A)) = inverse(double_divide(B,inverse(B))),
inference(paramod,[status(thm)],[c_455,c_563]) ).
cnf(c_565,plain,
double_divide(A,inverse(A)) = double_divide(inverse(B),inverse(inverse(B))),
inference(paramod,[status(thm)],[c_429,c_564]) ).
cnf(c_566,plain,
double_divide(A,inverse(A)) = double_divide(inverse(B),B),
inference(paramod,[status(thm)],[c_272,c_565]) ).
cnf(c_456,plain,
double_divide(A,inverse(A)) = double_divide(B,inverse(B)),
inference(paramod,[status(thm)],[c_455,c_566]) ).
cnf(c_567,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(inverse(b1),inverse(inverse(b1))) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_429,c_342]) ).
cnf(c_568,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(inverse(b1),b1) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_272,c_567]) ).
cnf(c_569,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != inverse(double_divide(a1,inverse(a1))) ),
inference(paramod,[status(thm)],[c_455,c_568]) ).
cnf(c_570,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != double_divide(inverse(a1),inverse(inverse(a1))) ),
inference(paramod,[status(thm)],[c_429,c_569]) ).
cnf(c_571,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != double_divide(inverse(a1),a1) ),
inference(paramod,[status(thm)],[c_272,c_570]) ).
cnf(c_572,plain,
( inverse(double_divide(b4,a4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)) ),
inference(paramod,[status(thm)],[c_455,c_571]) ).
cnf(c_573,plain,
( inverse(double_divide(a4,b4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)) ),
inference(paramod,[status(thm)],[c_455,c_572]) ).
cnf(c_574,plain,
( double_divide(inverse(a4),inverse(b4)) != inverse(double_divide(a4,b4))
| double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)) ),
inference(paramod,[status(thm)],[c_429,c_573]) ).
cnf(c_575,plain,
( double_divide(inverse(a4),inverse(b4)) != double_divide(inverse(a4),inverse(b4))
| double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)) ),
inference(paramod,[status(thm)],[c_429,c_574]) ).
cnf(c_576,plain,
double_divide(b1,inverse(b1)) != double_divide(a1,inverse(a1)),
inference(copy,[status(thm)],[c_575]) ).
cnf(c_470,plain,
$false,
inference(resolve,[status(thm)],[c_456,c_576]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP106-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 14:24:23 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.37 % Process 369681 was started by sandbox2 on n003,
% 0.02/0.37 % Fri Sep 25 14:24:23 2026
% 0.02/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.37
% 0.02/0.37 % From the command line: assign(max_seconds, 300).
% 0.02/0.47
% 0.02/0.47 % Assigning unary symbol inverse kb_weight 0 and highest precedence (13).
% 0.02/0.47
% 0.02/0.47 % SZS status Unsatisfiable for theBenchmark
% 0.02/0.47
% 0.02/0.47 % Proof 1 at 0.06 (+ 0.02) seconds.
% 0.02/0.47 % Length of proof is 89.
% 0.02/0.47 % Level of proof is 22.
% 0.02/0.47 % Maximum clause weight is 88.000.
% 0.02/0.47 % Given clauses 13.
% 0.02/0.47
% 0.02/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------