%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP083-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:07 AM UTC 2026
% Result : Unsatisfiable 29.65s 4.71s
% Output : CNFRefutation 29.65s
% 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,axiom,
( 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(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_4886,plain,
( 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_4887,plain,
( 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_4886]) ).
cnf(c_4888,plain,
( 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_4887]) ).
cnf(c_4889,plain,
( 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_4888]) ).
cnf(c_4890,plain,
( 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_4889]) ).
cnf(c_4891,plain,
( 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_4890]) ).
cnf(c_4892,plain,
( 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_4891]) ).
cnf(c_4893,plain,
( 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_4892]) ).
cnf(c_4894,plain,
( 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_4893]) ).
cnf(c_4,plain,
( 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_4894]) ).
cnf(c_4895,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_4895]) ).
cnf(c_4896,plain,
multiply(inverse(double_divide(A,double_divide(B,A))),inverse(C)) = inverse(double_divide(double_divide(D,inverse(E)),double_divide(inverse(double_divide(B,inverse(double_divide(C,E)))),inverse(double_divide(F,double_divide(D,F)))))),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_8,plain,
inverse(double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B))))) = inverse(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(paramod,[status(thm)],[c_2,c_4896]) ).
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_4897,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_4897]) ).
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_20,plain,
inverse(double_divide(double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))),D)) = inverse(double_divide(E,double_divide(double_divide(C,inverse(double_divide(A,D))),E))),
inference(paramod,[status(thm)],[c_1,c_10]) ).
cnf(c_4898,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_4898]) ).
cnf(c_4899,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_4899]) ).
cnf(c_36,plain,
double_divide(inverse(A),inverse(double_divide(double_divide(B,C),double_divide(D,double_divide(B,D))))) = double_divide(double_divide(E,inverse(F)),double_divide(inverse(double_divide(C,inverse(double_divide(A,F)))),inverse(double_divide(V6,double_divide(E,V6))))),
inference(paramod,[status(thm)],[c_30,c_5]) ).
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_4900,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_4900]) ).
cnf(c_4901,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_4901]) ).
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_4902,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_4902]) ).
cnf(c_4903,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_4903]) ).
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_4904,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_4904]) ).
cnf(c_4905,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_4905]) ).
cnf(c_4906,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_4906]) ).
cnf(c_4907,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_4907]) ).
cnf(c_4908,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_4909,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_4908]) ).
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_4909]) ).
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_4910,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_4910]) ).
cnf(c_4911,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_4911]) ).
cnf(c_4912,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_4912]) ).
cnf(c_4913,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_4914,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_4913]) ).
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_4914]) ).
cnf(c_561,plain,
double_divide(double_divide(A,inverse(double_divide(B,double_divide(C,B)))),A) = double_divide(double_divide(D,inverse(double_divide(E,double_divide(C,E)))),D),
inference(paramod,[status(thm)],[c_10,c_514]) ).
cnf(c_4915,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_4915]) ).
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_4916,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_4916]) ).
cnf(c_4917,plain,
inverse(double_divide(inverse(A),inverse(double_divide(B,double_divide(double_divide(inverse(double_divide(A,C)),inverse(double_divide(D,double_divide(E,D)))),B))))) = inverse(double_divide(double_divide(F,inverse(C)),double_divide(inverse(double_divide(double_divide(V6,inverse(double_divide(V7,double_divide(E,V7)))),V6)),inverse(double_divide(V8,double_divide(F,V8)))))),
inference(paramod,[status(thm)],[c_561,c_8]) ).
cnf(c_4918,plain,
inverse(double_divide(double_divide(inverse(D),inverse(C)),double_divide(E,D))) = inverse(double_divide(double_divide(F,inverse(C)),double_divide(inverse(double_divide(double_divide(V6,inverse(double_divide(V7,double_divide(E,V7)))),V6)),inverse(double_divide(V8,double_divide(F,V8)))))),
inference(paramod,[status(thm)],[c_153,c_4917]) ).
cnf(c_1098,plain,
inverse(double_divide(double_divide(inverse(A),inverse(B)),double_divide(C,A))) = inverse(double_divide(double_divide(inverse(D),inverse(B)),double_divide(C,D))),
inference(paramod,[status(thm)],[c_560,c_4918]) ).
cnf(c_1154,plain,
inverse(double_divide(double_divide(inverse(double_divide(A,double_divide(B,A))),B),double_divide(C,double_divide(D,double_divide(inverse(E),D))))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_300,c_1098]) ).
cnf(c_4919,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_4919]) ).
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_1291,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(D,double_divide(C,D)))) = double_divide(inverse(double_divide(A,inverse(double_divide(B,E)))),inverse(double_divide(F,double_divide(E,F)))),
inference(paramod,[status(thm)],[c_1191,c_1191]) ).
cnf(c_1298,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(double_divide(D,C),double_divide(E,double_divide(D,E))))) = double_divide(inverse(double_divide(A,inverse(double_divide(B,F)))),inverse(double_divide(V6,double_divide(F,V6)))),
inference(paramod,[status(thm)],[c_30,c_1291]) ).
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_4920,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_4920]) ).
cnf(c_4921,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_4921]) ).
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_4922,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_4922]) ).
cnf(c_4923,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_4924,plain,
D = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(D,V6)))),F)),
inference(paramod,[status(thm)],[c_418,c_4923]) ).
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_4924]) ).
cnf(c_4925,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_4926,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_4925]) ).
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_4926]) ).
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_1764,plain,
double_divide(double_divide(A,inverse(double_divide(B,inverse(double_divide(C,double_divide(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_1744,c_18]) ).
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_4927,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_4927]) ).
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_4928,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_4928]) ).
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_4929,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_4929]) ).
cnf(c_4930,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_4930]) ).
cnf(c_2844,plain,
double_divide(double_divide(inverse(double_divide(A,double_divide(B,A))),inverse(inverse(double_divide(C,double_divide(B,C))))),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_225,c_2106]) ).
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_3218,plain,
double_divide(double_divide(inverse(A),inverse(double_divide(B,double_divide(C,B)))),D) = double_divide(C,double_divide(inverse(double_divide(E,double_divide(inverse(double_divide(A,D)),E))),double_divide(F,inverse(F)))),
inference(paramod,[status(thm)],[c_2296,c_158]) ).
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_4931,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_4932,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_4931]) ).
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_4932]) ).
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_4933,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_4933]) ).
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_4934,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_4934]) ).
cnf(c_4935,plain,
multiply(inverse(A),A) = inverse(double_divide(B,inverse(B))),
inference(paramod,[status(thm)],[c_3423,c_2]) ).
cnf(c_3579,plain,
inverse(double_divide(A,inverse(A))) = inverse(double_divide(B,inverse(B))),
inference(paramod,[status(thm)],[c_2,c_4935]) ).
cnf(c_4936,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_3633,plain,
double_divide(double_divide(A,inverse(A)),inverse(double_divide(B,inverse(B)))) = double_divide(C,inverse(C)),
inference(copy,[status(thm)],[c_4936]) ).
cnf(c_3636,plain,
( 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 ),
inference(resolve,[status(thm)],[c_3579,c_4]) ).
cnf(c_3795,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_4937,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_3797,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_4937]) ).
cnf(c_3857,plain,
inverse(double_divide(double_divide(inverse(A),inverse(double_divide(double_divide(B,inverse(B)),double_divide(C,double_divide(D,C))))),E)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_3433,c_20]) ).
cnf(c_4938,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_3970,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_4938]) ).
cnf(c_4939,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_3633,c_1339]) ).
cnf(c_4305,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_4939]) ).
cnf(c_4940,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_3633]) ).
cnf(c_4372,plain,
inverse(inverse(double_divide(A,inverse(A)))) = double_divide(B,inverse(B)),
inference(paramod,[status(thm)],[c_3390,c_4940]) ).
cnf(c_4941,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(double_divide(D,E),double_divide(F,double_divide(D,F))))) = double_divide(double_divide(V6,inverse(double_divide(inverse(B),inverse(double_divide(V7,double_divide(A,V7)))))),double_divide(inverse(double_divide(E,inverse(C))),inverse(double_divide(V8,double_divide(V6,V8))))),
inference(paramod,[status(thm)],[c_1,c_36]) ).
cnf(c_4374,plain,
double_divide(inverse(double_divide(A,inverse(double_divide(B,C)))),inverse(double_divide(double_divide(D,E),double_divide(F,double_divide(D,F))))) = double_divide(double_divide(inverse(B),inverse(A)),double_divide(E,inverse(C))),
inference(paramod,[status(thm)],[c_1764,c_4941]) ).
cnf(c_4385,plain,
double_divide(inverse(A),inverse(double_divide(double_divide(B,C),double_divide(D,double_divide(B,D))))) = double_divide(double_divide(E,inverse(E)),double_divide(inverse(double_divide(C,inverse(double_divide(A,F)))),inverse(double_divide(V6,double_divide(F,V6))))),
inference(paramod,[status(thm)],[c_1291,c_36]) ).
cnf(c_4942,plain,
double_divide(double_divide(inverse(B),inverse(A)),double_divide(C,inverse(C))) = double_divide(inverse(double_divide(A,inverse(double_divide(B,F)))),inverse(double_divide(V6,double_divide(F,V6)))),
inference(paramod,[status(thm)],[c_4374,c_1298]) ).
cnf(c_4391,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(B),inverse(A)),double_divide(E,inverse(E))),
inference(copy,[status(thm)],[c_4942]) ).
cnf(c_4393,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_4372,c_1]) ).
cnf(c_4943,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_4372,c_225]) ).
cnf(c_4944,plain,
double_divide(inverse(A),C) = double_divide(inverse(double_divide(D,double_divide(A,D))),C),
inference(paramod,[status(thm)],[c_4305,c_4943]) ).
cnf(c_4450,plain,
double_divide(inverse(double_divide(A,double_divide(B,A))),C) = double_divide(inverse(B),C),
inference(copy,[status(thm)],[c_4944]) ).
cnf(c_4945,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_4372,c_19]) ).
cnf(c_4946,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_4450,c_4945]) ).
cnf(c_4947,plain,
inverse(D) = inverse(double_divide(F,double_divide(D,F))),
inference(paramod,[status(thm)],[c_4393,c_4946]) ).
cnf(c_4481,plain,
inverse(double_divide(A,double_divide(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_4947]) ).
cnf(c_4948,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_4372,c_391]) ).
cnf(c_4949,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_4481,c_4948]) ).
cnf(c_4950,plain,
inverse(B) = double_divide(B,inverse(double_divide(inverse(C),C))),
inference(paramod,[status(thm)],[c_4305,c_4949]) ).
cnf(c_4486,plain,
double_divide(A,inverse(double_divide(inverse(B),B))) = inverse(A),
inference(copy,[status(thm)],[c_4950]) ).
cnf(c_4951,plain,
inverse(double_divide(A,double_divide(B,A))) = double_divide(inverse(inverse(double_divide(C,inverse(C)))),B),
inference(paramod,[status(thm)],[c_4372,c_1744]) ).
cnf(c_4952,plain,
inverse(B) = double_divide(inverse(inverse(double_divide(C,inverse(C)))),B),
inference(paramod,[status(thm)],[c_4481,c_4951]) ).
cnf(c_4669,plain,
double_divide(inverse(inverse(double_divide(A,inverse(A)))),B) = inverse(B),
inference(copy,[status(thm)],[c_4952]) ).
cnf(c_4953,plain,
double_divide(inverse(inverse(double_divide(A,inverse(A)))),B) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_4372,c_2085]) ).
cnf(c_4954,plain,
inverse(B) = double_divide(double_divide(C,inverse(C)),B),
inference(paramod,[status(thm)],[c_4669,c_4953]) ).
cnf(c_4673,plain,
double_divide(double_divide(A,inverse(A)),B) = inverse(B),
inference(copy,[status(thm)],[c_4954]) ).
cnf(c_4955,plain,
double_divide(inverse(A),inverse(double_divide(inverse(C),C))) = double_divide(D,double_divide(A,D)),
inference(paramod,[status(thm)],[c_4481,c_3970]) ).
cnf(c_4956,plain,
inverse(inverse(A)) = double_divide(D,double_divide(A,D)),
inference(paramod,[status(thm)],[c_4486,c_4955]) ).
cnf(c_4721,plain,
double_divide(A,double_divide(B,A)) = inverse(inverse(B)),
inference(copy,[status(thm)],[c_4956]) ).
cnf(c_4957,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_4721,c_3797]) ).
cnf(c_4958,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_4721,c_4957]) ).
cnf(c_4959,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_4673,c_4958]) ).
cnf(c_4960,plain,
inverse(inverse(inverse(inverse(inverse(C))))) = double_divide(C,double_divide(D,inverse(D))),
inference(paramod,[status(thm)],[c_4673,c_4959]) ).
cnf(c_4761,plain,
double_divide(A,double_divide(B,inverse(B))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(copy,[status(thm)],[c_4960]) ).
cnf(c_4961,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_4761,c_3795]) ).
cnf(c_4962,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_4721,c_4961]) ).
cnf(c_4963,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_4721,c_4962]) ).
cnf(c_4762,plain,
inverse(inverse(inverse(inverse(inverse(inverse(A)))))) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_4721,c_4963]) ).
cnf(c_4964,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_4721,c_3561]) ).
cnf(c_4784,plain,
double_divide(A,inverse(double_divide(inverse(inverse(inverse(B))),B))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(paramod,[status(thm)],[c_4761,c_4964]) ).
cnf(c_4965,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_4761,c_3499]) ).
cnf(c_4966,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_4762,c_4965]) ).
cnf(c_4967,plain,
inverse(inverse(inverse(A))) = double_divide(A,inverse(double_divide(inverse(inverse(inverse(D))),D))),
inference(paramod,[status(thm)],[c_4721,c_4966]) ).
cnf(c_4968,plain,
inverse(inverse(inverse(A))) = inverse(inverse(inverse(inverse(inverse(A))))),
inference(paramod,[status(thm)],[c_4784,c_4967]) ).
cnf(c_4786,plain,
inverse(inverse(inverse(inverse(inverse(A))))) = inverse(inverse(inverse(A))),
inference(copy,[status(thm)],[c_4968]) ).
cnf(c_4969,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_4721,c_3459]) ).
cnf(c_4970,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_4721,c_4969]) ).
cnf(c_4971,plain,
inverse(inverse(C)) = double_divide(inverse(C),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4721,c_4970]) ).
cnf(c_4972,plain,
inverse(inverse(C)) = inverse(inverse(inverse(inverse(inverse(inverse(C)))))),
inference(paramod,[status(thm)],[c_4761,c_4971]) ).
cnf(c_4973,plain,
inverse(inverse(C)) = inverse(inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_4786,c_4972]) ).
cnf(c_4793,plain,
inverse(inverse(inverse(inverse(A)))) = inverse(inverse(A)),
inference(copy,[status(thm)],[c_4973]) ).
cnf(c_4974,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_4721,c_3422]) ).
cnf(c_4975,plain,
inverse(inverse(inverse(B))) = double_divide(inverse(inverse(inverse(inverse(double_divide(D,inverse(D)))))),B),
inference(paramod,[status(thm)],[c_4721,c_4974]) ).
cnf(c_4976,plain,
inverse(inverse(inverse(B))) = double_divide(inverse(inverse(double_divide(D,inverse(D)))),B),
inference(paramod,[status(thm)],[c_4793,c_4975]) ).
cnf(c_4794,plain,
inverse(inverse(inverse(A))) = inverse(A),
inference(paramod,[status(thm)],[c_4669,c_4976]) ).
cnf(c_4977,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_4721,c_3358]) ).
cnf(c_4978,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_4721,c_4977]) ).
cnf(c_4979,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_4794,c_4978]) ).
cnf(c_4980,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(inverse(inverse(inverse(inverse(C)))))))),
inference(paramod,[status(thm)],[c_4761,c_4979]) ).
cnf(c_4981,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(inverse(inverse(C)))))),
inference(paramod,[status(thm)],[c_4794,c_4980]) ).
cnf(c_4982,plain,
inverse(inverse(double_divide(B,inverse(C)))) = double_divide(B,inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_4794,c_4981]) ).
cnf(c_4798,plain,
inverse(inverse(double_divide(A,inverse(B)))) = double_divide(A,inverse(B)),
inference(paramod,[status(thm)],[c_4794,c_4982]) ).
cnf(c_4983,plain,
double_divide(double_divide(inverse(A),inverse(inverse(inverse(C)))),D) = double_divide(C,double_divide(inverse(double_divide(E,double_divide(inverse(double_divide(A,D)),E))),double_divide(F,inverse(F)))),
inference(paramod,[status(thm)],[c_4721,c_3218]) ).
cnf(c_4984,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,double_divide(inverse(double_divide(E,double_divide(inverse(double_divide(A,D)),E))),double_divide(F,inverse(F)))),
inference(paramod,[status(thm)],[c_4794,c_4983]) ).
cnf(c_4985,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,double_divide(inverse(inverse(inverse(inverse(double_divide(A,D))))),double_divide(F,inverse(F)))),
inference(paramod,[status(thm)],[c_4721,c_4984]) ).
cnf(c_4986,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,double_divide(inverse(inverse(double_divide(A,D))),double_divide(F,inverse(F)))),
inference(paramod,[status(thm)],[c_4794,c_4985]) ).
cnf(c_4987,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,inverse(inverse(inverse(inverse(inverse(inverse(inverse(double_divide(A,D))))))))),
inference(paramod,[status(thm)],[c_4761,c_4986]) ).
cnf(c_4988,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,inverse(inverse(inverse(inverse(inverse(double_divide(A,D))))))),
inference(paramod,[status(thm)],[c_4794,c_4987]) ).
cnf(c_4989,plain,
double_divide(double_divide(inverse(A),inverse(C)),D) = double_divide(C,inverse(inverse(inverse(double_divide(A,D))))),
inference(paramod,[status(thm)],[c_4794,c_4988]) ).
cnf(c_4808,plain,
double_divide(double_divide(inverse(A),inverse(B)),C) = double_divide(B,inverse(double_divide(A,C))),
inference(paramod,[status(thm)],[c_4794,c_4989]) ).
cnf(c_4990,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_4721,c_3211]) ).
cnf(c_4991,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_4794,c_4990]) ).
cnf(c_4992,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_4761,c_4991]) ).
cnf(c_4993,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_4798,c_4992]) ).
cnf(c_4994,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_4798,c_4993]) ).
cnf(c_4995,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_4798,c_4994]) ).
cnf(c_4996,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_4721,c_4995]) ).
cnf(c_4997,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = double_divide(A,inverse(double_divide(inverse(F),F))),
inference(paramod,[status(thm)],[c_4794,c_4996]) ).
cnf(c_4809,plain,
double_divide(A,inverse(double_divide(B,inverse(B)))) = inverse(A),
inference(paramod,[status(thm)],[c_4486,c_4997]) ).
cnf(c_4998,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_4673,c_3198]) ).
cnf(c_4999,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_4809,c_4998]) ).
cnf(c_5000,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_4721,c_4999]) ).
cnf(c_5001,plain,
double_divide(inverse(inverse(A)),D) = double_divide(E,double_divide(inverse(inverse(double_divide(A,D))),E)),
inference(paramod,[status(thm)],[c_4794,c_5000]) ).
cnf(c_5002,plain,
double_divide(inverse(inverse(A)),D) = inverse(inverse(inverse(inverse(double_divide(A,D))))),
inference(paramod,[status(thm)],[c_4721,c_5001]) ).
cnf(c_5003,plain,
double_divide(inverse(inverse(A)),D) = inverse(inverse(double_divide(A,D))),
inference(paramod,[status(thm)],[c_4794,c_5002]) ).
cnf(c_4811,plain,
inverse(inverse(double_divide(A,B))) = double_divide(inverse(inverse(A)),B),
inference(copy,[status(thm)],[c_5003]) ).
cnf(c_5004,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_4673,c_3075]) ).
cnf(c_5005,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_4809,c_5004]) ).
cnf(c_5006,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_4811,c_5005]) ).
cnf(c_5007,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_4721,c_5006]) ).
cnf(c_5008,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(double_divide(E,double_divide(inverse(B),E)))),
inference(paramod,[status(thm)],[c_4794,c_5007]) ).
cnf(c_5009,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(inverse(inverse(inverse(B))))),
inference(paramod,[status(thm)],[c_4721,c_5008]) ).
cnf(c_4823,plain,
double_divide(inverse(inverse(A)),B) = double_divide(A,inverse(inverse(B))),
inference(paramod,[status(thm)],[c_4794,c_5009]) ).
cnf(c_5010,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_4721,c_3037]) ).
cnf(c_5011,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_4794,c_5010]) ).
cnf(c_5012,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_4721,c_5011]) ).
cnf(c_5013,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_4794,c_5012]) ).
cnf(c_5014,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_4673,c_5013]) ).
cnf(c_5015,plain,
double_divide(inverse(inverse(C)),inverse(inverse(D))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4809,c_5014]) ).
cnf(c_5016,plain,
double_divide(C,inverse(inverse(inverse(inverse(D))))) = double_divide(C,D),
inference(paramod,[status(thm)],[c_4823,c_5015]) ).
cnf(c_4824,plain,
double_divide(A,inverse(inverse(B))) = double_divide(A,B),
inference(paramod,[status(thm)],[c_4794,c_5016]) ).
cnf(c_5017,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_4721,c_3021]) ).
cnf(c_5018,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_4811,c_5017]) ).
cnf(c_5019,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_4823,c_5018]) ).
cnf(c_5020,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_4824,c_5019]) ).
cnf(c_5021,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_4811,c_5020]) ).
cnf(c_5022,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_4823,c_5021]) ).
cnf(c_5023,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_4824,c_5022]) ).
cnf(c_5024,plain,
double_divide(double_divide(B,C),double_divide(inverse(B),inverse(double_divide(D,inverse(D))))) = C,
inference(paramod,[status(thm)],[c_4673,c_5023]) ).
cnf(c_5025,plain,
double_divide(double_divide(B,C),inverse(inverse(B))) = C,
inference(paramod,[status(thm)],[c_4809,c_5024]) ).
cnf(c_4825,plain,
double_divide(double_divide(A,B),A) = B,
inference(paramod,[status(thm)],[c_4824,c_5025]) ).
cnf(c_5026,plain,
double_divide(double_divide(inverse(inverse(inverse(B))),inverse(inverse(double_divide(C,double_divide(B,C))))),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_4721,c_2844]) ).
cnf(c_5027,plain,
double_divide(double_divide(inverse(B),inverse(inverse(double_divide(C,double_divide(B,C))))),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_4794,c_5026]) ).
cnf(c_5028,plain,
double_divide(double_divide(inverse(B),inverse(inverse(inverse(inverse(B))))),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_4721,c_5027]) ).
cnf(c_5029,plain,
double_divide(double_divide(inverse(B),inverse(inverse(B))),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_4794,c_5028]) ).
cnf(c_5030,plain,
double_divide(double_divide(inverse(B),B),D) = double_divide(double_divide(E,inverse(E)),D),
inference(paramod,[status(thm)],[c_4824,c_5029]) ).
cnf(c_4829,plain,
double_divide(double_divide(inverse(A),A),B) = inverse(B),
inference(paramod,[status(thm)],[c_4673,c_5030]) ).
cnf(c_5031,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_4721,c_2209]) ).
cnf(c_5032,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_4794,c_5031]) ).
cnf(c_5033,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_4721,c_5032]) ).
cnf(c_5034,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_4794,c_5033]) ).
cnf(c_5035,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(double_divide(C,double_divide(F,inverse(F))))),E),
inference(paramod,[status(thm)],[c_4721,c_5034]) ).
cnf(c_5036,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(inverse(inverse(inverse(inverse(C))))))),E),
inference(paramod,[status(thm)],[c_4761,c_5035]) ).
cnf(c_5037,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(inverse(inverse(C))))),E),
inference(paramod,[status(thm)],[c_4794,c_5036]) ).
cnf(c_5038,plain,
inverse(inverse(C)) = double_divide(double_divide(E,inverse(inverse(C))),E),
inference(paramod,[status(thm)],[c_4794,c_5037]) ).
cnf(c_5039,plain,
inverse(inverse(C)) = double_divide(double_divide(E,C),E),
inference(paramod,[status(thm)],[c_4824,c_5038]) ).
cnf(c_4831,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_4825,c_5039]) ).
cnf(c_5040,plain,
inverse(double_divide(double_divide(inverse(inverse(inverse(B))),B),double_divide(C,double_divide(D,double_divide(inverse(E),D))))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4721,c_1154]) ).
cnf(c_5041,plain,
inverse(double_divide(double_divide(inverse(B),B),double_divide(C,double_divide(D,double_divide(inverse(E),D))))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4831,c_5040]) ).
cnf(c_5042,plain,
inverse(double_divide(double_divide(inverse(B),B),double_divide(C,inverse(inverse(inverse(E)))))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4721,c_5041]) ).
cnf(c_5043,plain,
inverse(double_divide(double_divide(inverse(B),B),double_divide(C,inverse(E)))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4831,c_5042]) ).
cnf(c_5044,plain,
inverse(inverse(double_divide(C,inverse(E)))) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4829,c_5043]) ).
cnf(c_5045,plain,
double_divide(C,inverse(E)) = inverse(double_divide(double_divide(inverse(F),inverse(E)),double_divide(C,F))),
inference(paramod,[status(thm)],[c_4831,c_5044]) ).
cnf(c_5046,plain,
double_divide(C,inverse(E)) = inverse(double_divide(E,inverse(double_divide(F,double_divide(C,F))))),
inference(paramod,[status(thm)],[c_4808,c_5045]) ).
cnf(c_5047,plain,
double_divide(C,inverse(E)) = inverse(double_divide(E,inverse(inverse(inverse(C))))),
inference(paramod,[status(thm)],[c_4721,c_5046]) ).
cnf(c_5048,plain,
double_divide(C,inverse(E)) = inverse(double_divide(E,inverse(C))),
inference(paramod,[status(thm)],[c_4831,c_5047]) ).
cnf(c_4851,plain,
inverse(double_divide(A,inverse(B))) = double_divide(B,inverse(A)),
inference(copy,[status(thm)],[c_5048]) ).
cnf(c_5049,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(double_divide(D,double_divide(C,D)))) = double_divide(double_divide(inverse(B),inverse(A)),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4851,c_4391]) ).
cnf(c_5050,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(inverse(inverse(C)))) = double_divide(double_divide(inverse(B),inverse(A)),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4721,c_5049]) ).
cnf(c_5051,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(C)) = double_divide(double_divide(inverse(B),inverse(A)),double_divide(E,inverse(E))),
inference(paramod,[status(thm)],[c_4831,c_5050]) ).
cnf(c_5052,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(C)) = inverse(inverse(inverse(inverse(inverse(double_divide(inverse(B),inverse(A))))))),
inference(paramod,[status(thm)],[c_4761,c_5051]) ).
cnf(c_5053,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(C)) = inverse(inverse(inverse(inverse(double_divide(A,inverse(inverse(B))))))),
inference(paramod,[status(thm)],[c_4851,c_5052]) ).
cnf(c_5054,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(C)) = inverse(inverse(inverse(inverse(double_divide(A,B))))),
inference(paramod,[status(thm)],[c_4831,c_5053]) ).
cnf(c_5055,plain,
double_divide(double_divide(double_divide(B,C),inverse(A)),inverse(C)) = inverse(inverse(double_divide(A,B))),
inference(paramod,[status(thm)],[c_4831,c_5054]) ).
cnf(c_4873,plain,
double_divide(double_divide(double_divide(A,B),inverse(C)),inverse(B)) = double_divide(C,A),
inference(paramod,[status(thm)],[c_4831,c_5055]) ).
cnf(c_5056,plain,
double_divide(inverse(A),inverse(double_divide(double_divide(B,C),inverse(inverse(B))))) = double_divide(double_divide(E,inverse(E)),double_divide(inverse(double_divide(C,inverse(double_divide(A,F)))),inverse(double_divide(V6,double_divide(F,V6))))),
inference(paramod,[status(thm)],[c_4721,c_4385]) ).
cnf(c_5057,plain,
double_divide(inverse(A),inverse(double_divide(double_divide(B,C),B))) = double_divide(double_divide(E,inverse(E)),double_divide(inverse(double_divide(C,inverse(double_divide(A,F)))),inverse(double_divide(V6,double_divide(F,V6))))),
inference(paramod,[status(thm)],[c_4831,c_5056]) ).
cnf(c_5058,plain,
double_divide(inverse(A),inverse(C)) = double_divide(double_divide(E,inverse(E)),double_divide(inverse(double_divide(C,inverse(double_divide(A,F)))),inverse(double_divide(V6,double_divide(F,V6))))),
inference(paramod,[status(thm)],[c_4825,c_5057]) ).
cnf(c_5059,plain,
double_divide(inverse(A),inverse(C)) = double_divide(double_divide(E,inverse(E)),double_divide(double_divide(double_divide(A,F),inverse(C)),inverse(double_divide(V6,double_divide(F,V6))))),
inference(paramod,[status(thm)],[c_4851,c_5058]) ).
cnf(c_5060,plain,
double_divide(inverse(A),inverse(C)) = double_divide(double_divide(E,inverse(E)),double_divide(double_divide(double_divide(A,F),inverse(C)),inverse(inverse(inverse(F))))),
inference(paramod,[status(thm)],[c_4721,c_5059]) ).
cnf(c_5061,plain,
double_divide(inverse(A),inverse(C)) = double_divide(double_divide(E,inverse(E)),double_divide(double_divide(double_divide(A,F),inverse(C)),inverse(F))),
inference(paramod,[status(thm)],[c_4831,c_5060]) ).
cnf(c_5062,plain,
double_divide(inverse(A),inverse(C)) = double_divide(double_divide(E,inverse(E)),double_divide(C,A)),
inference(paramod,[status(thm)],[c_4873,c_5061]) ).
cnf(c_5063,plain,
double_divide(inverse(A),inverse(C)) = inverse(double_divide(C,A)),
inference(paramod,[status(thm)],[c_4673,c_5062]) ).
cnf(c_4875,plain,
inverse(double_divide(A,B)) = double_divide(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_5063]) ).
cnf(c_5064,plain,
inverse(double_divide(double_divide(inverse(A),inverse(double_divide(double_divide(B,inverse(B)),inverse(inverse(D))))),E)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4721,c_3857]) ).
cnf(c_5065,plain,
inverse(double_divide(double_divide(inverse(A),inverse(double_divide(double_divide(B,inverse(B)),D))),E)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4831,c_5064]) ).
cnf(c_5066,plain,
inverse(double_divide(double_divide(inverse(A),inverse(inverse(D))),E)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4673,c_5065]) ).
cnf(c_5067,plain,
inverse(double_divide(double_divide(inverse(A),D),E)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4831,c_5066]) ).
cnf(c_5068,plain,
double_divide(inverse(E),inverse(double_divide(inverse(A),D))) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4875,c_5067]) ).
cnf(c_5069,plain,
double_divide(inverse(E),double_divide(inverse(D),inverse(inverse(A)))) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4875,c_5068]) ).
cnf(c_5070,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),inverse(double_divide(A,E))),F))),
inference(paramod,[status(thm)],[c_4831,c_5069]) ).
cnf(c_5071,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(double_divide(F,double_divide(double_divide(inverse(D),double_divide(inverse(E),inverse(A))),F))),
inference(paramod,[status(thm)],[c_4875,c_5070]) ).
cnf(c_5072,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(inverse(double_divide(inverse(D),double_divide(inverse(E),inverse(A)))))),
inference(paramod,[status(thm)],[c_4721,c_5071]) ).
cnf(c_5073,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(double_divide(inverse(double_divide(inverse(E),inverse(A))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_4875,c_5072]) ).
cnf(c_5074,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(double_divide(double_divide(inverse(inverse(A)),inverse(inverse(E))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_4875,c_5073]) ).
cnf(c_5075,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(double_divide(double_divide(A,inverse(inverse(E))),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_4831,c_5074]) ).
cnf(c_5076,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(double_divide(double_divide(A,E),inverse(inverse(D))))),
inference(paramod,[status(thm)],[c_4831,c_5075]) ).
cnf(c_5077,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(inverse(double_divide(double_divide(A,E),D))),
inference(paramod,[status(thm)],[c_4831,c_5076]) ).
cnf(c_5078,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(double_divide(inverse(D),inverse(double_divide(A,E)))),
inference(paramod,[status(thm)],[c_4875,c_5077]) ).
cnf(c_5079,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = inverse(double_divide(inverse(D),double_divide(inverse(E),inverse(A)))),
inference(paramod,[status(thm)],[c_4875,c_5078]) ).
cnf(c_5080,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = double_divide(inverse(double_divide(inverse(E),inverse(A))),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_4875,c_5079]) ).
cnf(c_5081,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = double_divide(double_divide(inverse(inverse(A)),inverse(inverse(E))),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_4875,c_5080]) ).
cnf(c_5082,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = double_divide(double_divide(A,inverse(inverse(E))),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_4831,c_5081]) ).
cnf(c_5083,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = double_divide(double_divide(A,E),inverse(inverse(D))),
inference(paramod,[status(thm)],[c_4831,c_5082]) ).
cnf(c_5084,plain,
double_divide(inverse(E),double_divide(inverse(D),A)) = double_divide(double_divide(A,E),D),
inference(paramod,[status(thm)],[c_4831,c_5083]) ).
cnf(c_4880,plain,
double_divide(double_divide(A,B),C) = double_divide(inverse(B),double_divide(inverse(C),A)),
inference(copy,[status(thm)],[c_5084]) ).
cnf(c_5085,plain,
double_divide(A,double_divide(B,inverse(B))) = inverse(inverse(inverse(A))),
inference(paramod,[status(thm)],[c_4831,c_4761]) ).
cnf(c_4884,plain,
double_divide(A,double_divide(B,inverse(B))) = inverse(A),
inference(paramod,[status(thm)],[c_4831,c_5085]) ).
cnf(c_5086,plain,
( inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| inverse(double_divide(a2,double_divide(inverse(inverse(b2)),inverse(b2)))) != a2 ),
inference(paramod,[status(thm)],[c_4875,c_3636]) ).
cnf(c_5087,plain,
( inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| inverse(double_divide(a2,double_divide(b2,inverse(b2)))) != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5086]) ).
cnf(c_5088,plain,
( inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| inverse(inverse(a2)) != a2 ),
inference(paramod,[status(thm)],[c_4884,c_5087]) ).
cnf(c_5089,plain,
( inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5088]) ).
cnf(c_5090,plain,
( inverse(double_divide(double_divide(inverse(b3),inverse(c3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5089]) ).
cnf(c_5091,plain,
( inverse(double_divide(inverse(inverse(c3)),double_divide(inverse(a3),inverse(b3)))) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4880,c_5090]) ).
cnf(c_5092,plain,
( inverse(double_divide(c3,double_divide(inverse(a3),inverse(b3)))) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5091]) ).
cnf(c_5093,plain,
( double_divide(inverse(double_divide(inverse(a3),inverse(b3))),inverse(c3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5092]) ).
cnf(c_5094,plain,
( double_divide(double_divide(inverse(inverse(b3)),inverse(inverse(a3))),inverse(c3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5093]) ).
cnf(c_5095,plain,
( double_divide(double_divide(b3,inverse(inverse(a3))),inverse(c3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5094]) ).
cnf(c_5096,plain,
( double_divide(double_divide(b3,a3),inverse(c3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5095]) ).
cnf(c_5097,plain,
( double_divide(inverse(a3),double_divide(inverse(inverse(c3)),b3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4880,c_5096]) ).
cnf(c_5098,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5097]) ).
cnf(c_5099,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != inverse(double_divide(c3,double_divide(inverse(a3),inverse(b3))))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5098]) ).
cnf(c_5100,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(inverse(double_divide(inverse(a3),inverse(b3))),inverse(c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5099]) ).
cnf(c_5101,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(double_divide(inverse(inverse(b3)),inverse(inverse(a3))),inverse(c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4875,c_5100]) ).
cnf(c_5102,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(double_divide(b3,inverse(inverse(a3))),inverse(c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5101]) ).
cnf(c_5103,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(double_divide(b3,a3),inverse(c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5102]) ).
cnf(c_5104,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(inverse(a3),double_divide(inverse(inverse(c3)),b3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4880,c_5103]) ).
cnf(c_5105,plain,
( double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(inverse(a3),double_divide(c3,b3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_4831,c_5104]) ).
cnf(c_5106,plain,
double_divide(inverse(a3),double_divide(c3,b3)) != double_divide(inverse(a3),double_divide(c3,b3)),
inference(copy,[status(thm)],[c_5105]) ).
cnf(c_4885,plain,
$false,
inference(copy,[status(thm)],[c_5106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP083-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n026.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Fri Sep 25 14:24:09 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.42 % Process 2726523 was started by sandbox2 on n026,
% 0.16/0.42 % Fri Sep 25 14:24:09 2026
% 0.16/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.42
% 0.16/0.42 % From the command line: assign(max_seconds, 300).
% 29.65/4.71
% 29.65/4.71 % Assigning unary symbol inverse kb_weight 0 and highest precedence (11).
% 29.65/4.71
% 29.65/4.71 % SZS status Unsatisfiable for theBenchmark
% 29.65/4.71
% 29.65/4.71 % Proof 1 at 3.14 (+ 1.09) seconds.
% 29.65/4.71 % Length of proof is 125.
% 29.65/4.71 % Level of proof is 49.
% 29.65/4.71 % Maximum clause weight is 100.000.
% 29.65/4.71 % Given clauses 104.
% 29.65/4.71
% 29.65/4.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------