%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP502-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:29:54 AM UTC 2026
% Result : Unsatisfiable 12.49s 2.30s
% Output : CNFRefutation 12.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 3
% Syntax : Number of formulae : 74 ( 74 unt; 0 def)
% Number of atoms : 74 ( 73 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 10 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 322 ( 0 sgn 6 !; 0 ?)
% 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_1,axiom,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('theBenchmark.p',prove_these_axioms_1) ).
cnf(c_3,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(clausify,[status(thm)],[prove_these_axioms_1]) ).
cnf(c_3581,plain,
inverse(double_divide(a1,inverse(a1))) != multiply(inverse(b1),b1),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_3582,plain,
inverse(double_divide(a1,inverse(a1))) != inverse(double_divide(b1,inverse(b1))),
inference(paramod,[status(thm)],[c_2,c_3581]) ).
cnf(c_4,plain,
inverse(double_divide(b1,inverse(b1))) != inverse(double_divide(a1,inverse(a1))),
inference(copy,[status(thm)],[c_3582]) ).
cnf(c_3583,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_3583]) ).
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_3584,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_3584]) ).
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_3585,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_3585]) ).
cnf(c_3586,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_3586]) ).
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_3587,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_3587]) ).
cnf(c_3588,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_3588]) ).
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_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_3589,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_3590,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_3589]) ).
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_3590]) ).
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_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_3591,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_3591]) ).
cnf(c_3592,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_3592]) ).
cnf(c_3593,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_3594,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_3593]) ).
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_3594]) ).
cnf(c_3595,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_3595]) ).
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_3596,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_3596]) ).
cnf(c_3597,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_3597]) ).
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_3598,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_3598]) ).
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_3599,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_3600,plain,
D = double_divide(F,double_divide(inverse(inverse(double_divide(V6,double_divide(D,V6)))),F)),
inference(paramod,[status(thm)],[c_418,c_3599]) ).
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_3600]) ).
cnf(c_3601,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_3602,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_3601]) ).
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_3602]) ).
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_3603,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_3603]) ).
cnf(c_3604,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_3604]) ).
cnf(c_3605,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_3605]) ).
cnf(c_3606,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_3606]) ).
cnf(c_3580,plain,
$false,
inference(resolve,[status(thm)],[c_3579,c_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP502-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.62 % Computer : n017.cluster.edu
% 0.15/0.62 % Model : x86_64 x86_64
% 0.15/0.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.62 % Memory : 8046.5625MB
% 0.15/0.62 % OS : Linux 6.8.0-71-generic
% 0.15/0.62 % CPULimit : 300
% 0.15/0.62 % WCLimit : 300
% 0.15/0.62 % DateTime : Fri Sep 25 14:52:33 UTC 2026
% 0.15/0.63 % CPUTime :
% 0.15/0.63 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.63 % Process 2570500 was started by sandbox on n017,
% 0.15/0.63 % Fri Sep 25 14:52:33 2026
% 0.15/0.63 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.64
% 0.15/0.64 % From the command line: assign(max_seconds, 300).
% 12.49/2.30
% 12.49/2.30 % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 12.49/2.30
% 12.49/2.30 % SZS status Unsatisfiable for theBenchmark
% 12.49/2.30
% 12.49/2.30 % Proof 1 at 1.21 (+ 0.43) seconds.
% 12.49/2.30 % Length of proof is 45.
% 12.49/2.30 % Level of proof is 28.
% 12.49/2.30 % Maximum clause weight is 98.000.
% 12.49/2.30 % Given clauses 98.
% 12.49/2.30
% 12.49/2.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------