%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP503-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:29:54 AM UTC 2026
% Result : Unsatisfiable 13.43s 7.14s
% Output : CNFRefutation 13.43s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : double_divide(double_divide(VAR_0,inverse(double_divide(VAR_1,VAR_2))),double_divide(inverse(VAR_1),inverse(double_divide(VAR_3,double_divide(VAR_0,VAR_3))))) = VAR_2,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(A,D))))) = 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_2,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('theBenchmark.p',prove_these_axioms_2) ).
cnf(c_3,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(clausify,[status(thm)],[prove_these_axioms_2]) ).
cnf(c_4938,plain,
multiply(inverse(double_divide(b2,inverse(b2))),a2) != a2,
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_4,plain,
inverse(double_divide(a2,inverse(double_divide(b2,inverse(b2))))) != a2,
inference(paramod,[status(thm)],[c_2,c_4938]) ).
cnf(c_4939,plain,
double_divide(double_divide(A,inverse(B)),double_divide(inverse(double_divide(C,inverse(double_divide(D,B)))),inverse(double_divide(E,double_divide(A,E))))) = double_divide(inverse(D),inverse(double_divide(F,double_divide(C,F)))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))) = double_divide(double_divide(D,inverse(E)),double_divide(inverse(double_divide(C,inverse(double_divide(A,E)))),inverse(double_divide(F,double_divide(D,F))))),
inference(copy,[status(thm)],[c_4939]) ).
cnf(c_9,plain,
double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))) = double_divide(inverse(A),inverse(double_divide(D,double_divide(C,D)))),
inference(paramod,[status(thm)],[c_5,c_5]) ).
cnf(c_4940,plain,
double_divide(double_divide(A,inverse(double_divide(inverse(B),inverse(double_divide(C,double_divide(D,C)))))),double_divide(inverse(inverse(B)),inverse(double_divide(E,double_divide(A,E))))) = inverse(double_divide(F,double_divide(D,F))),
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_10,plain,
inverse(double_divide(A,double_divide(B,A))) = inverse(double_divide(C,double_divide(B,C))),
inference(paramod,[status(thm)],[c_1,c_4940]) ).
cnf(c_18,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_19,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(B,double_divide(C,B)),D))),double_divide(inverse(double_divide(E,double_divide(C,E))),inverse(double_divide(F,double_divide(A,F))))) = D,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_4941,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(double_divide(D,double_divide(E,D))),inverse(double_divide(F,double_divide(A,F))))) = double_divide(C,double_divide(V6,double_divide(E,V6))),
inference(paramod,[status(thm)],[c_10,c_18]) ).
cnf(c_30,plain,
double_divide(A,double_divide(B,double_divide(C,B))) = double_divide(A,double_divide(D,double_divide(C,D))),
inference(paramod,[status(thm)],[c_18,c_4941]) ).
cnf(c_4942,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,double_divide(D,C))))),double_divide(inverse(B),inverse(double_divide(E,double_divide(A,E))))) = double_divide(F,double_divide(D,F)),
inference(paramod,[status(thm)],[c_30,c_1]) ).
cnf(c_32,plain,
double_divide(A,double_divide(B,A)) = double_divide(C,double_divide(B,C)),
inference(paramod,[status(thm)],[c_1,c_4942]) ).
cnf(c_45,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(B,C),double_divide(D,double_divide(B,D))))),double_divide(inverse(E),inverse(double_divide(F,double_divide(A,F))))) = double_divide(C,E),
inference(paramod,[status(thm)],[c_30,c_18]) ).
cnf(c_49,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))),D) = double_divide(E,double_divide(double_divide(C,inverse(double_divide(A,D))),E)),
inference(paramod,[status(thm)],[c_1,c_32]) ).
cnf(c_4943,plain,
double_divide(A,double_divide(B,A)) = double_divide(double_divide(C,B),double_divide(D,double_divide(C,D))),
inference(paramod,[status(thm)],[c_32,c_30]) ).
cnf(c_53,plain,
double_divide(double_divide(A,B),double_divide(C,double_divide(A,C))) = double_divide(D,double_divide(B,D)),
inference(copy,[status(thm)],[c_4943]) ).
cnf(c_4944,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(C,double_divide(D,C)))) = double_divide(double_divide(E,inverse(double_divide(F,double_divide(A,F)))),double_divide(inverse(double_divide(D,inverse(double_divide(V6,double_divide(B,V6))))),inverse(double_divide(V7,double_divide(E,V7))))),
inference(paramod,[status(thm)],[c_53,c_5]) ).
cnf(c_59,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(C,double_divide(D,C)))) = double_divide(A,double_divide(D,inverse(double_divide(E,double_divide(B,E))))),
inference(paramod,[status(thm)],[c_18,c_4944]) ).
cnf(c_115,plain,
double_divide(inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),A)),inverse(double_divide(D,double_divide(inverse(B),D)))) = C,
inference(paramod,[status(thm)],[c_59,c_1]) ).
cnf(c_127,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(D,double_divide(A,inverse(double_divide(E,double_divide(F,E)))))) = double_divide(C,double_divide(D,F)),
inference(paramod,[status(thm)],[c_59,c_18]) ).
cnf(c_134,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)),inverse(double_divide(C,double_divide(D,C)))) = double_divide(E,double_divide(D,E)),
inference(paramod,[status(thm)],[c_59,c_32]) ).
cnf(c_147,plain,
double_divide(A,double_divide(B,inverse(double_divide(C,double_divide(D,C))))) = double_divide(A,double_divide(B,inverse(double_divide(E,double_divide(D,E))))),
inference(paramod,[status(thm)],[c_59,c_59]) ).
cnf(c_153,plain,
double_divide(inverse(A),inverse(double_divide(B,double_divide(double_divide(inverse(double_divide(A,C)),inverse(double_divide(D,E))),B)))) = double_divide(double_divide(inverse(D),inverse(C)),E),
inference(paramod,[status(thm)],[c_115,c_5]) ).
cnf(c_158,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))),D) = double_divide(C,double_divide(double_divide(E,inverse(double_divide(A,D))),E)),
inference(paramod,[status(thm)],[c_115,c_18]) ).
cnf(c_195,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(E,double_divide(C,E)),
inference(paramod,[status(thm)],[c_147,c_32]) ).
cnf(c_4945,plain,
double_divide(double_divide(A,inverse(double_divide(double_divide(B,inverse(double_divide(C,double_divide(D,C)))),double_divide(E,double_divide(B,E))))),double_divide(inverse(F),inverse(double_divide(V6,double_divide(A,V6))))) = double_divide(inverse(double_divide(V7,double_divide(D,V7))),F),
inference(paramod,[status(thm)],[c_195,c_18]) ).
cnf(c_225,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),C) = double_divide(inverse(double_divide(D,double_divide(B,D))),C),
inference(paramod,[status(thm)],[c_45,c_4945]) ).
cnf(c_4946,plain,
multiply(A,inverse(double_divide(B,double_divide(C,B)))) = inverse(double_divide(inverse(double_divide(D,double_divide(C,D))),A)),
inference(paramod,[status(thm)],[c_225,c_2]) ).
cnf(c_236,plain,
inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),C)) = inverse(double_divide(inverse(double_divide(D,double_divide(B,D))),C)),
inference(paramod,[status(thm)],[c_2,c_4946]) ).
cnf(c_242,plain,
double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),A)) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(C,E))),D)),
inference(paramod,[status(thm)],[c_225,c_32]) ).
cnf(c_4947,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),F)),inverse(double_divide(V6,double_divide(A,V6))))) = double_divide(C,double_divide(inverse(double_divide(V7,double_divide(E,V7))),F)),
inference(paramod,[status(thm)],[c_236,c_18]) ).
cnf(c_265,plain,
double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),D)) = double_divide(A,double_divide(inverse(double_divide(E,double_divide(C,E))),D)),
inference(paramod,[status(thm)],[c_18,c_4947]) ).
cnf(c_4948,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(double_divide(D,double_divide(E,D))),double_divide(A,inverse(double_divide(F,double_divide(E,F)))))) = double_divide(V6,double_divide(inverse(double_divide(V7,double_divide(C,V7))),V6)),
inference(paramod,[status(thm)],[c_195,c_242]) ).
cnf(c_291,plain,
double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),C)) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(A,E))),D)),
inference(paramod,[status(thm)],[c_127,c_4948]) ).
cnf(c_4949,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(inverse(double_divide(C,double_divide(D,C))),B)))),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = double_divide(inverse(double_divide(F,double_divide(V6,F))),V6),
inference(paramod,[status(thm)],[c_291,c_1]) ).
cnf(c_300,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),B) = double_divide(inverse(double_divide(C,double_divide(D,C))),D),
inference(paramod,[status(thm)],[c_18,c_4949]) ).
cnf(c_4950,plain,
multiply(A,inverse(double_divide(B,double_divide(A,B)))) = inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D)),
inference(paramod,[status(thm)],[c_300,c_2]) ).
cnf(c_339,plain,
inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)) = inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D)),
inference(paramod,[status(thm)],[c_2,c_4950]) ).
cnf(c_4951,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E))),inverse(double_divide(F,double_divide(A,F))))) = inverse(double_divide(V6,double_divide(C,V6))),
inference(paramod,[status(thm)],[c_134,c_1]) ).
cnf(c_4952,plain,
double_divide(C,inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E))) = inverse(double_divide(V6,double_divide(C,V6))),
inference(paramod,[status(thm)],[c_18,c_4951]) ).
cnf(c_391,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(B,inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D))),
inference(copy,[status(thm)],[c_4952]) ).
cnf(c_418,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),double_divide(inverse(inverse(double_divide(C,double_divide(D,C)))),inverse(double_divide(E,double_divide(B,E))))) = D,
inference(paramod,[status(thm)],[c_391,c_1]) ).
cnf(c_479,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C))) = double_divide(A,inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E))),
inference(paramod,[status(thm)],[c_391,c_391]) ).
cnf(c_507,plain,
double_divide(A,double_divide(double_divide(B,inverse(double_divide(C,D))),B)) = double_divide(E,double_divide(double_divide(A,inverse(double_divide(C,D))),E)),
inference(paramod,[status(thm)],[c_158,c_49]) ).
cnf(c_4953,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(double_divide(D,E))),B)))),double_divide(inverse(C),inverse(double_divide(F,double_divide(A,F))))) = double_divide(double_divide(V6,inverse(double_divide(D,E))),V6),
inference(paramod,[status(thm)],[c_507,c_1]) ).
cnf(c_514,plain,
double_divide(double_divide(A,inverse(double_divide(B,C))),A) = double_divide(double_divide(D,inverse(double_divide(B,C))),D),
inference(paramod,[status(thm)],[c_18,c_4953]) ).
cnf(c_4954,plain,
double_divide(A,double_divide(double_divide(B,inverse(C)),B)) = double_divide(D,double_divide(double_divide(A,inverse(double_divide(double_divide(E,inverse(double_divide(F,C))),double_divide(inverse(F),inverse(double_divide(V6,double_divide(E,V6))))))),D)),
inference(paramod,[status(thm)],[c_1,c_507]) ).
cnf(c_515,plain,
double_divide(A,double_divide(double_divide(B,inverse(C)),B)) = double_divide(D,double_divide(double_divide(A,inverse(C)),D)),
inference(paramod,[status(thm)],[c_1,c_4954]) ).
cnf(c_4955,plain,
double_divide(double_divide(A,inverse(B)),A) = double_divide(double_divide(C,inverse(double_divide(double_divide(D,inverse(double_divide(E,B))),double_divide(inverse(E),inverse(double_divide(F,double_divide(D,F))))))),C),
inference(paramod,[status(thm)],[c_1,c_514]) ).
cnf(c_558,plain,
double_divide(double_divide(A,inverse(B)),A) = double_divide(double_divide(C,inverse(B)),C),
inference(paramod,[status(thm)],[c_1,c_4955]) ).
cnf(c_4956,plain,
double_divide(inverse(A),inverse(double_divide(B,double_divide(double_divide(inverse(double_divide(A,C)),inverse(double_divide(D,E))),B)))) = double_divide(double_divide(F,inverse(C)),double_divide(inverse(double_divide(double_divide(V6,inverse(double_divide(D,E))),V6)),inverse(double_divide(V7,double_divide(F,V7))))),
inference(paramod,[status(thm)],[c_514,c_5]) ).
cnf(c_4957,plain,
double_divide(double_divide(inverse(D),inverse(C)),E) = double_divide(double_divide(F,inverse(C)),double_divide(inverse(double_divide(double_divide(V6,inverse(double_divide(D,E))),V6)),inverse(double_divide(V7,double_divide(F,V7))))),
inference(paramod,[status(thm)],[c_153,c_4956]) ).
cnf(c_560,plain,
double_divide(double_divide(A,inverse(B)),double_divide(inverse(double_divide(double_divide(C,inverse(double_divide(D,E))),C)),inverse(double_divide(F,double_divide(A,F))))) = double_divide(double_divide(inverse(D),inverse(B)),E),
inference(copy,[status(thm)],[c_4957]) ).
cnf(c_4958,plain,
double_divide(A,inverse(double_divide(double_divide(B,inverse(double_divide(C,A))),B))) = double_divide(double_divide(D,inverse(double_divide(E,double_divide(inverse(C),E)))),D),
inference(paramod,[status(thm)],[c_115,c_514]) ).
cnf(c_571,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(inverse(C),B)))),A) = double_divide(D,inverse(double_divide(double_divide(E,inverse(double_divide(C,D))),E))),
inference(copy,[status(thm)],[c_4958]) ).
cnf(c_614,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(D)),C)))),double_divide(inverse(E),inverse(double_divide(F,double_divide(A,F))))) = double_divide(double_divide(B,inverse(D)),E),
inference(paramod,[status(thm)],[c_558,c_18]) ).
cnf(c_687,plain,
inverse(double_divide(A,double_divide(double_divide(inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C)),inverse(D)),A))) = double_divide(double_divide(E,inverse(D)),E),
inference(paramod,[status(thm)],[c_558,c_391]) ).
cnf(c_696,plain,
double_divide(double_divide(double_divide(A,inverse(B)),A),double_divide(inverse(C),inverse(B))) = double_divide(double_divide(D,inverse(C)),D),
inference(paramod,[status(thm)],[c_558,c_558]) ).
cnf(c_4959,plain,
double_divide(double_divide(A,double_divide(double_divide(B,inverse(double_divide(C,inverse(C)))),B)),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = double_divide(double_divide(F,inverse(D)),F),
inference(paramod,[status(thm)],[c_158,c_696]) ).
cnf(c_816,plain,
double_divide(double_divide(A,inverse(B)),A) = double_divide(double_divide(C,double_divide(double_divide(D,inverse(double_divide(E,inverse(E)))),D)),double_divide(inverse(B),inverse(double_divide(F,double_divide(C,F))))),
inference(copy,[status(thm)],[c_4959]) ).
cnf(c_4960,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(D,double_divide(C,D)))) = double_divide(double_divide(E,inverse(A)),double_divide(inverse(double_divide(double_divide(F,inverse(double_divide(V6,double_divide(inverse(B),V6)))),F)),inverse(double_divide(V7,double_divide(E,V7))))),
inference(paramod,[status(thm)],[c_571,c_5]) ).
cnf(c_1191,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(D,double_divide(C,D)))) = double_divide(double_divide(inverse(E),inverse(A)),double_divide(inverse(B),E)),
inference(paramod,[status(thm)],[c_560,c_4960]) ).
cnf(c_1253,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(inverse(double_divide(B,inverse(C))),inverse(double_divide(C,D))))),double_divide(inverse(B),A)) = D,
inference(paramod,[status(thm)],[c_1191,c_115]) ).
cnf(c_1339,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(D,B)))),A)) = double_divide(inverse(D),C),
inference(paramod,[status(thm)],[c_115,c_1253]) ).
cnf(c_1381,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,C))),double_divide(inverse(double_divide(inverse(D),inverse(double_divide(E,double_divide(B,E))))),A)) = double_divide(inverse(C),D),
inference(paramod,[status(thm)],[c_10,c_1339]) ).
cnf(c_4961,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,inverse(double_divide(C,double_divide(D,C)))))),double_divide(inverse(double_divide(inverse(E),inverse(double_divide(F,double_divide(B,F))))),A)) = double_divide(inverse(inverse(double_divide(V6,double_divide(D,V6)))),E),
inference(paramod,[status(thm)],[c_195,c_1339]) ).
cnf(c_1404,plain,
double_divide(inverse(inverse(double_divide(A,double_divide(B,A)))),C) = double_divide(inverse(inverse(double_divide(D,double_divide(B,D)))),C),
inference(paramod,[status(thm)],[c_1381,c_4961]) ).
cnf(c_4962,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(double_divide(inverse(double_divide(D,double_divide(E,D))),E),B)))),A)) = double_divide(inverse(double_divide(inverse(double_divide(F,double_divide(V6,F))),V6)),C),
inference(paramod,[status(thm)],[c_339,c_1339]) ).
cnf(c_1416,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)),C) = double_divide(inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E)),C),
inference(paramod,[status(thm)],[c_1339,c_4962]) ).
cnf(c_1429,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(double_divide(D,inverse(E)),D)))),A)) = double_divide(inverse(double_divide(B,inverse(E))),C),
inference(paramod,[status(thm)],[c_558,c_1339]) ).
cnf(c_4963,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(double_divide(double_divide(C,inverse(D)),inverse(E))),inverse(double_divide(E,B)))),A)) = double_divide(C,double_divide(double_divide(F,inverse(D)),F)),
inference(paramod,[status(thm)],[c_515,c_1339]) ).
cnf(c_1433,plain,
double_divide(inverse(A),double_divide(double_divide(B,inverse(C)),inverse(A))) = double_divide(B,double_divide(double_divide(D,inverse(C)),D)),
inference(paramod,[status(thm)],[c_1339,c_4963]) ).
cnf(c_4964,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),double_divide(inverse(inverse(double_divide(C,double_divide(D,C)))),inverse(double_divide(E,double_divide(B,E))))) = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(D,V6)))),F)),
inference(paramod,[status(thm)],[c_1404,c_195]) ).
cnf(c_4965,plain,
D = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(D,V6)))),F)),
inference(paramod,[status(thm)],[c_418,c_4964]) ).
cnf(c_1697,plain,
double_divide(A,double_divide(inverse(inverse(double_divide(B,double_divide(C,B)))),A)) = C,
inference(copy,[status(thm)],[c_4965]) ).
cnf(c_4966,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)),inverse(double_divide(C,double_divide(inverse(inverse(double_divide(D,double_divide(E,D)))),C)))) = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(E,V6)))),F)),
inference(paramod,[status(thm)],[c_1404,c_134]) ).
cnf(c_4967,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)),inverse(E)) = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(E,V6)))),F)),
inference(paramod,[status(thm)],[c_1697,c_4966]) ).
cnf(c_1715,plain,
double_divide(inverse(double_divide(inverse(double_divide(A,double_divide(B,A))),B)),inverse(C)) = C,
inference(paramod,[status(thm)],[c_1697,c_4967]) ).
cnf(c_1744,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(double_divide(C,inverse(B)),C),
inference(paramod,[status(thm)],[c_1715,c_687]) ).
cnf(c_1746,plain,
double_divide(double_divide(A,double_divide(double_divide(B,inverse(C)),B)),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_1744,c_1]) ).
cnf(c_2085,plain,
double_divide(double_divide(A,inverse(B)),A) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_1746,c_816]) ).
cnf(c_4968,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(double_divide(C,inverse(B)),C)))),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = double_divide(double_divide(F,inverse(F)),D),
inference(paramod,[status(thm)],[c_2085,c_18]) ).
cnf(c_2106,plain,
double_divide(double_divide(A,inverse(A)),B) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_614,c_4968]) ).
cnf(c_2209,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_2085,c_195]) ).
cnf(c_4969,plain,
inverse(double_divide(A,double_divide(double_divide(inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C)),inverse(D)),A))) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_2085,c_391]) ).
cnf(c_2296,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_1715,c_4969]) ).
cnf(c_2449,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(double_divide(D,inverse(D)),E)))),A)) = double_divide(inverse(double_divide(B,inverse(E))),C),
inference(paramod,[status(thm)],[c_2085,c_1339]) ).
cnf(c_4970,plain,
double_divide(double_divide(inverse(A),inverse(B)),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(double_divide(D,inverse(B)),D)))),A)) = double_divide(inverse(double_divide(E,inverse(E))),C),
inference(paramod,[status(thm)],[c_2085,c_1339]) ).
cnf(c_2450,plain,
double_divide(inverse(double_divide(A,inverse(A))),B) = double_divide(inverse(double_divide(C,inverse(C))),B),
inference(paramod,[status(thm)],[c_1429,c_4970]) ).
cnf(c_4971,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),double_divide(inverse(double_divide(D,inverse(D))),inverse(double_divide(E,double_divide(A,E))))) = double_divide(C,double_divide(F,inverse(F))),
inference(paramod,[status(thm)],[c_2450,c_18]) ).
cnf(c_2535,plain,
double_divide(A,double_divide(B,inverse(B))) = double_divide(A,double_divide(C,inverse(C))),
inference(paramod,[status(thm)],[c_18,c_4971]) ).
cnf(c_3021,plain,
double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(B,C)),A))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_2296,c_1]) ).
cnf(c_3037,plain,
double_divide(inverse(double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),A))),double_divide(inverse(D),inverse(double_divide(E,double_divide(double_divide(F,inverse(F)),E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_2296,c_18]) ).
cnf(c_3075,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(C,double_divide(double_divide(D,inverse(D)),C)))) = double_divide(A,inverse(double_divide(E,double_divide(inverse(double_divide(F,double_divide(B,F))),E)))),
inference(paramod,[status(thm)],[c_2296,c_59]) ).
cnf(c_3198,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,double_divide(double_divide(C,inverse(C)),B)))),D) = double_divide(E,double_divide(inverse(double_divide(F,double_divide(inverse(double_divide(A,D)),F))),E)),
inference(paramod,[status(thm)],[c_2296,c_49]) ).
cnf(c_3211,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,inverse(double_divide(C,double_divide(B,C))))),double_divide(D,inverse(D))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_2296,c_479]) ).
cnf(c_3358,plain,
double_divide(inverse(A),double_divide(double_divide(B,inverse(C)),inverse(A))) = double_divide(B,double_divide(inverse(double_divide(D,double_divide(inverse(C),D))),double_divide(E,inverse(E)))),
inference(paramod,[status(thm)],[c_2296,c_1433]) ).
cnf(c_4972,plain,
inverse(double_divide(A,double_divide(inverse(inverse(double_divide(B,double_divide(C,B)))),A))) = double_divide(double_divide(D,inverse(D)),inverse(inverse(double_divide(E,double_divide(C,E))))),
inference(paramod,[status(thm)],[c_1404,c_2296]) ).
cnf(c_4973,plain,
inverse(C) = double_divide(double_divide(D,inverse(D)),inverse(inverse(double_divide(E,double_divide(C,E))))),
inference(paramod,[status(thm)],[c_1697,c_4972]) ).
cnf(c_3390,plain,
double_divide(double_divide(A,inverse(A)),inverse(inverse(double_divide(B,double_divide(C,B))))) = inverse(C),
inference(copy,[status(thm)],[c_4973]) ).
cnf(c_3422,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(inverse(double_divide(C,double_divide(inverse(double_divide(D,inverse(D))),C))),B),
inference(paramod,[status(thm)],[c_2296,c_2296]) ).
cnf(c_4974,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,inverse(C))))),double_divide(inverse(B),inverse(double_divide(D,double_divide(A,D))))) = double_divide(E,inverse(E)),
inference(paramod,[status(thm)],[c_2535,c_1]) ).
cnf(c_3423,plain,
double_divide(A,inverse(A)) = double_divide(B,inverse(B)),
inference(paramod,[status(thm)],[c_1,c_4974]) ).
cnf(c_3433,plain,
double_divide(inverse(A),double_divide(B,inverse(B))) = double_divide(C,double_divide(A,C)),
inference(paramod,[status(thm)],[c_2535,c_32]) ).
cnf(c_3459,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(inverse(C),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_2535,c_195]) ).
cnf(c_3499,plain,
inverse(double_divide(inverse(A),double_divide(B,inverse(B)))) = double_divide(A,inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D))),
inference(paramod,[status(thm)],[c_2535,c_391]) ).
cnf(c_4975,plain,
double_divide(A,double_divide(inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C)),inverse(inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E))))) = double_divide(A,double_divide(F,inverse(F))),
inference(paramod,[status(thm)],[c_1416,c_2535]) ).
cnf(c_3561,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C))) = double_divide(A,double_divide(D,inverse(D))),
inference(paramod,[status(thm)],[c_1715,c_4975]) ).
cnf(c_3580,plain,
inverse(double_divide(a2,inverse(double_divide(A,inverse(A))))) != a2,
inference(paramod,[status(thm)],[c_3423,c_4]) ).
cnf(c_4976,plain,
double_divide(A,inverse(A)) = double_divide(double_divide(B,inverse(B)),inverse(double_divide(C,inverse(C)))),
inference(paramod,[status(thm)],[c_3423,c_2106]) ).
cnf(c_3634,plain,
double_divide(double_divide(A,inverse(A)),inverse(double_divide(B,inverse(B)))) = double_divide(C,inverse(C)),
inference(copy,[status(thm)],[c_4976]) ).
cnf(c_3700,plain,
inverse(double_divide(a2,inverse(inverse(double_divide(A,double_divide(double_divide(inverse(double_divide(B,double_divide(C,B))),C),A)))))) != a2,
inference(paramod,[status(thm)],[c_391,c_3580]) ).
cnf(c_3763,plain,
double_divide(inverse(inverse(double_divide(double_divide(A,inverse(double_divide(B,C))),A))),double_divide(D,inverse(D))) = double_divide(inverse(double_divide(E,double_divide(inverse(B),E))),C),
inference(paramod,[status(thm)],[c_115,c_3433]) ).
cnf(c_3828,plain,
double_divide(inverse(A),double_divide(B,inverse(B))) = double_divide(double_divide(inverse(double_divide(C,double_divide(D,C))),E),double_divide(A,double_divide(inverse(double_divide(F,double_divide(D,F))),E))),
inference(paramod,[status(thm)],[c_265,c_3433]) ).
cnf(c_4977,plain,
double_divide(A,double_divide(B,double_divide(double_divide(C,double_divide(double_divide(D,inverse(D)),C)),B))) = double_divide(E,double_divide(inverse(double_divide(F,double_divide(A,F))),E)),
inference(paramod,[status(thm)],[c_3433,c_291]) ).
cnf(c_3830,plain,
double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),A)) = double_divide(C,double_divide(D,double_divide(double_divide(E,double_divide(double_divide(F,inverse(F)),E)),D))),
inference(copy,[status(thm)],[c_4977]) ).
cnf(c_4978,plain,
double_divide(A,double_divide(inverse(double_divide(B,double_divide(C,B))),C)) = double_divide(double_divide(D,inverse(D)),double_divide(E,double_divide(double_divide(F,double_divide(A,F)),E))),
inference(paramod,[status(thm)],[c_3433,c_291]) ).
cnf(c_3832,plain,
double_divide(double_divide(A,inverse(A)),double_divide(B,double_divide(double_divide(C,double_divide(D,C)),B))) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(F,E))),F)),
inference(copy,[status(thm)],[c_4978]) ).
cnf(c_4979,plain,
double_divide(inverse(A),double_divide(inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C)),inverse(inverse(double_divide(inverse(double_divide(D,double_divide(E,D))),E))))) = double_divide(F,double_divide(A,F)),
inference(paramod,[status(thm)],[c_1416,c_3433]) ).
cnf(c_4003,plain,
double_divide(inverse(A),inverse(double_divide(inverse(double_divide(B,double_divide(C,B))),C))) = double_divide(D,double_divide(A,D)),
inference(paramod,[status(thm)],[c_1715,c_4979]) ).
cnf(c_4980,plain,
double_divide(double_divide(inverse(A),inverse(inverse(B))),double_divide(inverse(double_divide(inverse(C),inverse(double_divide(double_divide(D,inverse(D)),inverse(double_divide(E,inverse(E))))))),A)) = double_divide(inverse(B),C),
inference(paramod,[status(thm)],[c_3634,c_1339]) ).
cnf(c_4411,plain,
double_divide(inverse(double_divide(inverse(A),inverse(inverse(double_divide(B,inverse(B)))))),C) = double_divide(inverse(A),C),
inference(paramod,[status(thm)],[c_2449,c_4980]) ).
cnf(c_4981,plain,
double_divide(double_divide(A,inverse(A)),inverse(inverse(double_divide(B,double_divide(inverse(double_divide(C,inverse(C))),B))))) = double_divide(D,inverse(D)),
inference(paramod,[status(thm)],[c_2296,c_3634]) ).
cnf(c_4478,plain,
inverse(inverse(double_divide(A,inverse(A)))) = double_divide(B,inverse(B)),
inference(paramod,[status(thm)],[c_3390,c_4981]) ).
cnf(c_4483,plain,
double_divide(double_divide(A,inverse(inverse(inverse(double_divide(B,inverse(B)))))),double_divide(inverse(C),inverse(double_divide(D,double_divide(A,D))))) = inverse(C),
inference(paramod,[status(thm)],[c_4478,c_1]) ).
cnf(c_4982,plain,
double_divide(inverse(double_divide(inverse(A),inverse(inverse(double_divide(B,inverse(B)))))),C) = double_divide(inverse(double_divide(D,double_divide(A,D))),C),
inference(paramod,[status(thm)],[c_4478,c_225]) ).
cnf(c_4983,plain,
double_divide(inverse(A),C) = double_divide(inverse(double_divide(D,double_divide(A,D))),C),
inference(paramod,[status(thm)],[c_4411,c_4982]) ).
cnf(c_4540,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),C) = double_divide(inverse(B),C),
inference(copy,[status(thm)],[c_4983]) ).
cnf(c_4984,plain,
double_divide(double_divide(A,inverse(inverse(inverse(double_divide(B,inverse(B)))))),double_divide(inverse(double_divide(C,double_divide(D,C))),inverse(double_divide(E,double_divide(A,E))))) = inverse(double_divide(F,double_divide(D,F))),
inference(paramod,[status(thm)],[c_4478,c_19]) ).
cnf(c_4985,plain,
double_divide(double_divide(A,inverse(inverse(inverse(double_divide(B,inverse(B)))))),double_divide(inverse(D),inverse(double_divide(E,double_divide(A,E))))) = inverse(double_divide(F,double_divide(D,F))),
inference(paramod,[status(thm)],[c_4540,c_4984]) ).
cnf(c_4986,plain,
inverse(D) = inverse(double_divide(F,double_divide(D,F))),
inference(paramod,[status(thm)],[c_4483,c_4985]) ).
cnf(c_4571,plain,
inverse(double_divide(A,double_divide(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_4986]) ).
cnf(c_4987,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(B,inverse(double_divide(inverse(double_divide(inverse(C),inverse(inverse(double_divide(D,inverse(D)))))),C))),
inference(paramod,[status(thm)],[c_4478,c_391]) ).
cnf(c_4988,plain,
inverse(B) = double_divide(B,inverse(double_divide(inverse(double_divide(inverse(C),inverse(inverse(double_divide(D,inverse(D)))))),C))),
inference(paramod,[status(thm)],[c_4571,c_4987]) ).
cnf(c_4989,plain,
inverse(B) = double_divide(B,inverse(double_divide(inverse(C),C))),
inference(paramod,[status(thm)],[c_4411,c_4988]) ).
cnf(c_4576,plain,
double_divide(A,inverse(double_divide(inverse(B),B))) = inverse(A),
inference(copy,[status(thm)],[c_4989]) ).
cnf(c_4990,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(inverse(inverse(double_divide(C,inverse(C)))),B),
inference(paramod,[status(thm)],[c_4478,c_1744]) ).
cnf(c_4991,plain,
inverse(B) = double_divide(inverse(inverse(double_divide(C,inverse(C)))),B),
inference(paramod,[status(thm)],[c_4571,c_4990]) ).
cnf(c_4759,plain,
double_divide(inverse(inverse(double_divide(A,inverse(A)))),B) = inverse(B),
inference(copy,[status(thm)],[c_4991]) ).
cnf(c_4992,plain,
double_divide(inverse(inverse(double_divide(A,inverse(A)))),B) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_4478,c_2085]) ).
cnf(c_4993,plain,
inverse(B) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_4759,c_4992]) ).
cnf(c_4763,plain,
double_divide(double_divide(A,inverse(A)),B) = inverse(B),
inference(copy,[status(thm)],[c_4993]) ).
cnf(c_4994,plain,
double_divide(double_divide(A,inverse(B)),A) = double_divide(inverse(inverse(double_divide(C,inverse(C)))),B),
inference(paramod,[status(thm)],[c_4478,c_2085]) ).
cnf(c_4764,plain,
double_divide(double_divide(A,inverse(B)),A) = inverse(B),
inference(paramod,[status(thm)],[c_4759,c_4994]) ).
cnf(c_4995,plain,
double_divide(inverse(A),inverse(double_divide(inverse(C),C))) = double_divide(D,double_divide(A,D)),
inference(paramod,[status(thm)],[c_4571,c_4003]) ).
cnf(c_4996,plain,
inverse(inverse(A)) = double_divide(D,double_divide(A,D)),
inference(paramod,[status(thm)],[c_4576,c_4995]) ).
cnf(c_4822,plain,
double_divide(A,double_divide(B,A)) = inverse(inverse(B)),
inference(copy,[status(thm)],[c_4996]) ).
cnf(c_4997,plain,
double_divide(double_divide(A,inverse(A)),double_divide(B,double_divide(inverse(inverse(D)),B))) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(F,E))),F)),
inference(paramod,[status(thm)],[c_4822,c_3832]) ).
cnf(c_4998,plain,
double_divide(double_divide(A,inverse(A)),inverse(inverse(inverse(inverse(D))))) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(F,E))),F)),
inference(paramod,[status(thm)],[c_4822,c_4997]) ).
cnf(c_4999,plain,
inverse(inverse(inverse(inverse(inverse(D))))) = double_divide(D,double_divide(inverse(double_divide(E,double_divide(F,E))),F)),
inference(paramod,[status(thm)],[c_4763,c_4998]) ).
cnf(c_5000,plain,
inverse(inverse(inverse(inverse(inverse(D))))) = double_divide(D,double_divide(inverse(inverse(inverse(F))),F)),
inference(paramod,[status(thm)],[c_4822,c_4999]) ).
cnf(c_4861,plain,
double_divide(A,double_divide(inverse(inverse(inverse(B))),B)) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(copy,[status(thm)],[c_5000]) ).
cnf(c_5001,plain,
double_divide(A,double_divide(inverse(inverse(inverse(C))),A)) = double_divide(C,double_divide(D,double_divide(double_divide(E,double_divide(double_divide(F,inverse(F)),E)),D))),
inference(paramod,[status(thm)],[c_4822,c_3830]) ).
cnf(c_5002,plain,
inverse(inverse(inverse(inverse(inverse(C))))) = double_divide(C,double_divide(D,double_divide(double_divide(E,double_divide(double_divide(F,inverse(F)),E)),D))),
inference(paramod,[status(thm)],[c_4822,c_5001]) ).
cnf(c_5003,plain,
inverse(inverse(inverse(inverse(inverse(C))))) = double_divide(C,double_divide(D,double_divide(double_divide(E,inverse(E)),D))),
inference(paramod,[status(thm)],[c_4763,c_5002]) ).
cnf(c_5004,plain,
inverse(inverse(inverse(inverse(inverse(C))))) = double_divide(C,double_divide(D,inverse(D))),
inference(paramod,[status(thm)],[c_4763,c_5003]) ).
cnf(c_4862,plain,
double_divide(A,double_divide(B,inverse(B))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(copy,[status(thm)],[c_5004]) ).
cnf(c_5005,plain,
inverse(inverse(inverse(inverse(inverse(inverse(A)))))) = double_divide(double_divide(inverse(double_divide(C,double_divide(D,C))),E),double_divide(A,double_divide(inverse(double_divide(F,double_divide(D,F))),E))),
inference(paramod,[status(thm)],[c_4862,c_3828]) ).
cnf(c_5006,plain,
inverse(inverse(inverse(inverse(inverse(inverse(A)))))) = double_divide(double_divide(inverse(inverse(inverse(D))),E),double_divide(A,double_divide(inverse(double_divide(F,double_divide(D,F))),E))),
inference(paramod,[status(thm)],[c_4822,c_5005]) ).
cnf(c_5007,plain,
inverse(inverse(inverse(inverse(inverse(inverse(A)))))) = double_divide(double_divide(inverse(inverse(inverse(D))),E),double_divide(A,double_divide(inverse(inverse(inverse(D))),E))),
inference(paramod,[status(thm)],[c_4822,c_5006]) ).
cnf(c_4863,plain,
inverse(inverse(inverse(inverse(inverse(inverse(A)))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_4822,c_5007]) ).
cnf(c_5008,plain,
double_divide(inverse(inverse(inverse(double_divide(B,C)))),double_divide(D,inverse(D))) = double_divide(inverse(double_divide(E,double_divide(inverse(B),E))),C),
inference(paramod,[status(thm)],[c_4764,c_3763]) ).
cnf(c_5009,plain,
inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(double_divide(B,C))))))))) = double_divide(inverse(double_divide(E,double_divide(inverse(B),E))),C),
inference(paramod,[status(thm)],[c_4862,c_5008]) ).
cnf(c_5010,plain,
inverse(inverse(inverse(inverse(double_divide(B,C))))) = double_divide(inverse(double_divide(E,double_divide(inverse(B),E))),C),
inference(paramod,[status(thm)],[c_4863,c_5009]) ).
cnf(c_4875,plain,
inverse(inverse(inverse(inverse(double_divide(A,B))))) = double_divide(inverse(inverse(inverse(inverse(A)))),B),
inference(paramod,[status(thm)],[c_4822,c_5010]) ).
cnf(c_5011,plain,
inverse(double_divide(a2,inverse(inverse(double_divide(A,double_divide(double_divide(inverse(inverse(inverse(C))),C),A)))))) != a2,
inference(paramod,[status(thm)],[c_4822,c_3700]) ).
cnf(c_5012,plain,
inverse(double_divide(a2,inverse(inverse(inverse(inverse(double_divide(inverse(inverse(inverse(C))),C))))))) != a2,
inference(paramod,[status(thm)],[c_4822,c_5011]) ).
cnf(c_5013,plain,
inverse(double_divide(a2,double_divide(inverse(inverse(inverse(inverse(inverse(inverse(inverse(C))))))),C))) != a2,
inference(paramod,[status(thm)],[c_4875,c_5012]) ).
cnf(c_5014,plain,
inverse(double_divide(a2,double_divide(inverse(inverse(inverse(C))),C))) != a2,
inference(paramod,[status(thm)],[c_4863,c_5013]) ).
cnf(c_5015,plain,
inverse(inverse(inverse(inverse(inverse(inverse(a2)))))) != a2,
inference(paramod,[status(thm)],[c_4861,c_5014]) ).
cnf(c_4878,plain,
inverse(inverse(a2)) != a2,
inference(paramod,[status(thm)],[c_4863,c_5015]) ).
cnf(c_5016,plain,
double_divide(A,inverse(double_divide(inverse(inverse(inverse(C))),C))) = double_divide(A,double_divide(D,inverse(D))),
inference(paramod,[status(thm)],[c_4822,c_3561]) ).
cnf(c_4889,plain,
double_divide(A,inverse(double_divide(inverse(inverse(inverse(B))),B))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(paramod,[status(thm)],[c_4862,c_5016]) ).
cnf(c_5017,plain,
inverse(inverse(inverse(inverse(inverse(inverse(inverse(A))))))) = double_divide(A,inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D))),
inference(paramod,[status(thm)],[c_4862,c_3499]) ).
cnf(c_5018,plain,
inverse(inverse(inverse(A))) = double_divide(A,inverse(double_divide(inverse(double_divide(C,double_divide(D,C))),D))),
inference(paramod,[status(thm)],[c_4863,c_5017]) ).
cnf(c_5019,plain,
inverse(inverse(inverse(A))) = double_divide(A,inverse(double_divide(inverse(inverse(inverse(D))),D))),
inference(paramod,[status(thm)],[c_4822,c_5018]) ).
cnf(c_5020,plain,
inverse(inverse(inverse(A))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(paramod,[status(thm)],[c_4889,c_5019]) ).
cnf(c_4891,plain,
inverse(inverse(inverse(inverse(inverse(A))))) = inverse(inverse(inverse(A))),
inference(copy,[status(thm)],[c_5020]) ).
cnf(c_5021,plain,
double_divide(inverse(inverse(inverse(B))),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(inverse(C),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4822,c_3459]) ).
cnf(c_5022,plain,
double_divide(inverse(inverse(inverse(B))),double_divide(C,inverse(inverse(inverse(B))))) = double_divide(inverse(C),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4822,c_5021]) ).
cnf(c_5023,plain,
inverse(inverse(C)) = double_divide(inverse(C),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4822,c_5022]) ).
cnf(c_5024,plain,
inverse(inverse(C)) = inverse(inverse(inverse(inverse(inverse(inverse(C)))))),
inference(paramod,[status(thm)],[c_4862,c_5023]) ).
cnf(c_5025,plain,
inverse(inverse(C)) = inverse(inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_4891,c_5024]) ).
cnf(c_4898,plain,
inverse(inverse(inverse(inverse(A)))) = inverse(inverse(A)),
inference(copy,[status(thm)],[c_5025]) ).
cnf(c_5026,plain,
inverse(inverse(inverse(B))) = double_divide(inverse(double_divide(C,double_divide(inverse(double_divide(D,inverse(D))),C))),B),
inference(paramod,[status(thm)],[c_4822,c_3422]) ).
cnf(c_5027,plain,
inverse(inverse(inverse(B))) = double_divide(inverse(inverse(inverse(inverse(double_divide(D,inverse(D)))))),B),
inference(paramod,[status(thm)],[c_4822,c_5026]) ).
cnf(c_5028,plain,
inverse(inverse(inverse(B))) = double_divide(inverse(inverse(double_divide(D,inverse(D)))),B),
inference(paramod,[status(thm)],[c_4898,c_5027]) ).
cnf(c_4899,plain,
inverse(inverse(inverse(A))) = inverse(A),
inference(paramod,[status(thm)],[c_4759,c_5028]) ).
cnf(c_5029,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,double_divide(inverse(double_divide(D,double_divide(inverse(C),D))),double_divide(E,inverse(E)))),
inference(paramod,[status(thm)],[c_4822,c_3358]) ).
cnf(c_5030,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,double_divide(inverse(inverse(inverse(inverse(C)))),double_divide(E,inverse(E)))),
inference(paramod,[status(thm)],[c_4822,c_5029]) ).
cnf(c_5031,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,double_divide(inverse(inverse(C)),double_divide(E,inverse(E)))),
inference(paramod,[status(thm)],[c_4899,c_5030]) ).
cnf(c_5032,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(inverse(inverse(inverse(inverse(C)))))))),
inference(paramod,[status(thm)],[c_4862,c_5031]) ).
cnf(c_5033,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(inverse(inverse(C)))))),
inference(paramod,[status(thm)],[c_4899,c_5032]) ).
cnf(c_5034,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_4899,c_5033]) ).
cnf(c_4903,plain,
inverse(inverse(double_divide(A,inverse(B)))) = double_divide(A,inverse(B)),
inference(paramod,[status(thm)],[c_4899,c_5034]) ).
cnf(c_5035,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,inverse(inverse(inverse(B))))),double_divide(D,inverse(D))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4822,c_3211]) ).
cnf(c_5036,plain,
double_divide(A,inverse(double_divide(inverse(double_divide(B,inverse(B))),double_divide(D,inverse(D))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4899,c_5035]) ).
cnf(c_5037,plain,
double_divide(A,inverse(inverse(inverse(inverse(inverse(inverse(inverse(double_divide(B,inverse(B)))))))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4862,c_5036]) ).
cnf(c_5038,plain,
double_divide(A,inverse(inverse(inverse(inverse(inverse(double_divide(B,inverse(B)))))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4903,c_5037]) ).
cnf(c_5039,plain,
double_divide(A,inverse(inverse(inverse(double_divide(B,inverse(B)))))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4903,c_5038]) ).
cnf(c_5040,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,inverse(double_divide(inverse(double_divide(E,double_divide(F,E))),F))),
inference(paramod,[status(thm)],[c_4903,c_5039]) ).
cnf(c_5041,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,inverse(double_divide(inverse(inverse(inverse(F))),F))),
inference(paramod,[status(thm)],[c_4822,c_5040]) ).
cnf(c_5042,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,inverse(double_divide(inverse(F),F))),
inference(paramod,[status(thm)],[c_4899,c_5041]) ).
cnf(c_4914,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_4576,c_5042]) ).
cnf(c_5043,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,inverse(B)))),D) = double_divide(E,double_divide(inverse(double_divide(F,double_divide(inverse(double_divide(A,D)),F))),E)),
inference(paramod,[status(thm)],[c_4763,c_3198]) ).
cnf(c_5044,plain,
double_divide(inverse(inverse(A)),D) = double_divide(E,double_divide(inverse(double_divide(F,double_divide(inverse(double_divide(A,D)),F))),E)),
inference(paramod,[status(thm)],[c_4914,c_5043]) ).
cnf(c_5045,plain,
double_divide(inverse(inverse(A)),D) = double_divide(E,double_divide(inverse(inverse(inverse(inverse(double_divide(A,D))))),E)),
inference(paramod,[status(thm)],[c_4822,c_5044]) ).
cnf(c_5046,plain,
double_divide(inverse(inverse(A)),D) = double_divide(E,double_divide(inverse(inverse(double_divide(A,D))),E)),
inference(paramod,[status(thm)],[c_4899,c_5045]) ).
cnf(c_5047,plain,
double_divide(inverse(inverse(A)),D) = inverse(inverse(inverse(inverse(double_divide(A,D))))),
inference(paramod,[status(thm)],[c_4822,c_5046]) ).
cnf(c_5048,plain,
double_divide(inverse(inverse(A)),D) = inverse(inverse(double_divide(A,D))),
inference(paramod,[status(thm)],[c_4899,c_5047]) ).
cnf(c_4916,plain,
inverse(inverse(double_divide(A,B))) = double_divide(inverse(inverse(A)),B),
inference(copy,[status(thm)],[c_5048]) ).
cnf(c_5049,plain,
double_divide(inverse(double_divide(A,B)),inverse(double_divide(C,inverse(C)))) = double_divide(A,inverse(double_divide(E,double_divide(inverse(double_divide(F,double_divide(B,F))),E)))),
inference(paramod,[status(thm)],[c_4763,c_3075]) ).
cnf(c_5050,plain,
inverse(inverse(double_divide(A,B))) = double_divide(A,inverse(double_divide(E,double_divide(inverse(double_divide(F,double_divide(B,F))),E)))),
inference(paramod,[status(thm)],[c_4914,c_5049]) ).
cnf(c_5051,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(double_divide(E,double_divide(inverse(double_divide(F,double_divide(B,F))),E)))),
inference(paramod,[status(thm)],[c_4916,c_5050]) ).
cnf(c_5052,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(double_divide(E,double_divide(inverse(inverse(inverse(B))),E)))),
inference(paramod,[status(thm)],[c_4822,c_5051]) ).
cnf(c_5053,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(double_divide(E,double_divide(inverse(B),E)))),
inference(paramod,[status(thm)],[c_4899,c_5052]) ).
cnf(c_5054,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(inverse(inverse(inverse(B))))),
inference(paramod,[status(thm)],[c_4822,c_5053]) ).
cnf(c_4928,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(inverse(B))),
inference(paramod,[status(thm)],[c_4899,c_5054]) ).
cnf(c_5055,plain,
double_divide(inverse(double_divide(A,double_divide(inverse(inverse(inverse(C))),A))),double_divide(inverse(D),inverse(double_divide(E,double_divide(double_divide(F,inverse(F)),E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4822,c_3037]) ).
cnf(c_5056,plain,
double_divide(inverse(double_divide(A,double_divide(inverse(C),A))),double_divide(inverse(D),inverse(double_divide(E,double_divide(double_divide(F,inverse(F)),E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4899,c_5055]) ).
cnf(c_5057,plain,
double_divide(inverse(inverse(inverse(inverse(C)))),double_divide(inverse(D),inverse(double_divide(E,double_divide(double_divide(F,inverse(F)),E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4822,c_5056]) ).
cnf(c_5058,plain,
double_divide(inverse(inverse(C)),double_divide(inverse(D),inverse(double_divide(E,double_divide(double_divide(F,inverse(F)),E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4899,c_5057]) ).
cnf(c_5059,plain,
double_divide(inverse(inverse(C)),double_divide(inverse(D),inverse(double_divide(E,inverse(E))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4763,c_5058]) ).
cnf(c_5060,plain,
double_divide(inverse(inverse(C)),inverse(inverse(D))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4914,c_5059]) ).
cnf(c_5061,plain,
double_divide(C,inverse(inverse(inverse(inverse(D))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4928,c_5060]) ).
cnf(c_4929,plain,
double_divide(A,inverse(inverse(B))) = double_divide(A,B),
inference(paramod,[status(thm)],[c_4899,c_5061]) ).
cnf(c_5062,plain,
double_divide(inverse(inverse(inverse(inverse(double_divide(B,C))))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4822,c_3021]) ).
cnf(c_5063,plain,
double_divide(inverse(inverse(double_divide(inverse(inverse(B)),C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4916,c_5062]) ).
cnf(c_5064,plain,
double_divide(inverse(inverse(double_divide(B,inverse(inverse(C))))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4928,c_5063]) ).
cnf(c_5065,plain,
double_divide(inverse(inverse(double_divide(B,C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4929,c_5064]) ).
cnf(c_5066,plain,
double_divide(double_divide(inverse(inverse(B)),C),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4916,c_5065]) ).
cnf(c_5067,plain,
double_divide(double_divide(B,inverse(inverse(C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4928,c_5066]) ).
cnf(c_5068,plain,
double_divide(double_divide(B,C),double_divide(inverse(B),inverse(double_divide(D,double_divide(double_divide(E,inverse(E)),D))))) = C,
inference(paramod,[status(thm)],[c_4929,c_5067]) ).
cnf(c_5069,plain,
double_divide(double_divide(B,C),double_divide(inverse(B),inverse(double_divide(D,inverse(D))))) = C,
inference(paramod,[status(thm)],[c_4763,c_5068]) ).
cnf(c_5070,plain,
double_divide(double_divide(B,C),inverse(inverse(B))) = C,
inference(paramod,[status(thm)],[c_4914,c_5069]) ).
cnf(c_4930,plain,
double_divide(double_divide(A,B),A) = B,
inference(paramod,[status(thm)],[c_4929,c_5070]) ).
cnf(c_5071,plain,
double_divide(inverse(inverse(inverse(B))),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4822,c_2209]) ).
cnf(c_5072,plain,
double_divide(inverse(B),double_divide(C,inverse(double_divide(D,double_divide(B,D))))) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4899,c_5071]) ).
cnf(c_5073,plain,
double_divide(inverse(B),double_divide(C,inverse(inverse(inverse(B))))) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4822,c_5072]) ).
cnf(c_5074,plain,
double_divide(inverse(B),double_divide(C,inverse(B))) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4899,c_5073]) ).
cnf(c_5075,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4822,c_5074]) ).
cnf(c_5076,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(inverse(inverse(inverse(inverse(C))))))),E),
inference(paramod,[status(thm)],[c_4862,c_5075]) ).
cnf(c_5077,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(inverse(inverse(C))))),E),
inference(paramod,[status(thm)],[c_4899,c_5076]) ).
cnf(c_5078,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(C))),E),
inference(paramod,[status(thm)],[c_4899,c_5077]) ).
cnf(c_5079,plain,
inverse(inverse(C)) = double_divide(double_divide(E,C),E),
inference(paramod,[status(thm)],[c_4929,c_5078]) ).
cnf(c_4936,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_4930,c_5079]) ).
cnf(c_4937,plain,
$false,
inference(resolve,[status(thm)],[c_4936,c_4878]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP503-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n019.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Fri Sep 25 14:57:26 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.37 % Process 3039218 was started by sandbox2 on n019,
% 0.09/5.37 % Fri Sep 25 14:57:26 2026
% 0.09/5.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/5.38
% 0.09/5.38 % From the command line: assign(max_seconds, 300).
% 13.43/7.14
% 13.43/7.14 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 13.43/7.14
% 13.43/7.14 % SZS status Unsatisfiable for theBenchmark
% 13.43/7.14
% 13.43/7.14 % Proof 1 at 1.25 (+ 0.44) seconds.
% 13.43/7.14 % Length of proof is 109.
% 13.43/7.14 % Level of proof is 45.
% 13.43/7.14 % Maximum clause weight is 100.000.
% 13.43/7.14 % Given clauses 108.
% 13.43/7.14
% 13.43/7.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------