%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:31:25 AM UTC 2026
% Result : Theorem 11.43s 1.96s
% Output : CNFRefutation 11.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 14
% Syntax : Number of formulae : 72 ( 38 unt; 0 def)
% Number of atoms : 118 ( 64 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 83 ( 37 ~; 29 |; 7 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 49 ( 3 sgn 17 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos02,axiom,
! [A] :
( g(A)
=> g(inv(A)) ),
file('theBenchmark.p',sos02) ).
fof(sos05,axiom,
! [A] :
( g(A)
=> product(eh,A) = A ),
file('theBenchmark.p',sos05) ).
fof(sos08,axiom,
! [A] :
( g(A)
=> product(inv(A),A) = eh ),
file('theBenchmark.p',sos08) ).
fof(sos10,axiom,
! [B,A] :
( h(A)
=> h(opp(B)) ),
file('theBenchmark.p',sos10) ).
fof(sos12,axiom,
! [C,B,A] :
( ( h(C)
& h(B)
& h(A) )
=> sum(sum(A,B),C) = sum(A,sum(B,C)) ),
file('theBenchmark.p',sos12) ).
fof(sos13,axiom,
! [A] :
( h(A)
=> sum(eg,A) = A ),
file('theBenchmark.p',sos13) ).
fof(sos14,axiom,
! [A] :
( h(A)
=> sum(A,eg) = A ),
file('theBenchmark.p',sos14) ).
fof(sos15,axiom,
! [A] :
( h(A)
=> sum(A,opp(A)) = eg ),
file('theBenchmark.p',sos15) ).
fof(sos16,axiom,
! [A] :
( h(A)
=> sum(opp(A),A) = eg ),
file('theBenchmark.p',sos16) ).
fof(sos17,axiom,
! [A] :
( g(A)
=> h(f(A)) ),
file('theBenchmark.p',sos17) ).
fof(sos18,axiom,
! [B,A] : f(product(A,B)) = sum(f(A),f(B)),
file('theBenchmark.p',sos18) ).
fof(goals,conjecture,
! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_19,plain,
( g(inv(A))
| ~ g(A) ),
inference(clausify,[status(thm)],[sos02]) ).
fof(sos03,axiom,
g(eh),
file('theBenchmark.p',sos03) ).
cnf(c_20,plain,
g(eh),
inference(clausify,[status(thm)],[sos03]) ).
cnf(c_22,plain,
( product(eh,A) = A
| ~ g(A) ),
inference(clausify,[status(thm)],[sos05]) ).
cnf(c_25,plain,
( product(inv(A),A) = eh
| ~ g(A) ),
inference(clausify,[status(thm)],[sos08]) ).
cnf(c_27,plain,
( h(opp(B))
| ~ h(A) ),
inference(clausify,[status(thm)],[sos10]) ).
fof(sos11,axiom,
h(eg),
file('theBenchmark.p',sos11) ).
cnf(c_28,plain,
h(eg),
inference(clausify,[status(thm)],[sos11]) ).
cnf(c_29,plain,
( sum(sum(A,B),C) = sum(A,sum(B,C))
| ~ h(C)
| ~ h(B)
| ~ h(A) ),
inference(clausify,[status(thm)],[sos12]) ).
cnf(c_30,plain,
( sum(eg,A) = A
| ~ h(A) ),
inference(clausify,[status(thm)],[sos13]) ).
cnf(c_31,plain,
( sum(A,eg) = A
| ~ h(A) ),
inference(clausify,[status(thm)],[sos14]) ).
cnf(c_32,plain,
( sum(A,opp(A)) = eg
| ~ h(A) ),
inference(clausify,[status(thm)],[sos15]) ).
cnf(c_33,plain,
( sum(opp(A),A) = eg
| ~ h(A) ),
inference(clausify,[status(thm)],[sos16]) ).
cnf(c_34,plain,
( h(f(A))
| ~ g(A) ),
inference(clausify,[status(thm)],[sos17]) ).
cnf(c_35,plain,
f(product(A,B)) = sum(f(A),f(B)),
inference(clausify,[status(thm)],[sos18]) ).
fof(nnf_17,plain,
? [X0] :
( ( f(inv(X0)) != opp(f(X0))
& g(X0) )
| f(eh) != eg ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ( f(inv(sK0)) != opp(f(sK0))
& g(sK0) )
| f(eh) != eg ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[nnf_17]) ).
fof(sk_goals_neg,plain,
( ( f(inv(sK0)) != opp(f(sK0))
| f(eh) != eg )
& ( g(sK0)
| f(eh) != eg ) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_36,negated_conjecture,
( g(sK0)
| f(eh) != eg ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_37,negated_conjecture,
( f(inv(sK0)) != opp(f(sK0))
| f(eh) != eg ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_38,negated_conjecture,
( opp(f(sK0)) != f(inv(sK0))
| f(eh) != eg ),
inference(copy,[status(thm)],[c_37]) ).
cnf(c_42,plain,
product(eh,eh) = eh,
inference(resolve,[status(thm)],[c_22,c_20]) ).
cnf(c_45,plain,
h(opp(A)),
inference(resolve,[status(thm)],[c_27,c_28]) ).
cnf(c_51,plain,
h(f(eh)),
inference(resolve,[status(thm)],[c_34,c_20]) ).
cnf(c_2020,plain,
f(eh) = sum(f(eh),f(eh)),
inference(paramod,[status(thm)],[c_42,c_35]) ).
cnf(c_56,plain,
sum(f(eh),f(eh)) = f(eh),
inference(copy,[status(thm)],[c_2020]) ).
cnf(c_60,plain,
sum(eg,opp(A)) = opp(A),
inference(resolve,[status(thm)],[c_30,c_45]) ).
cnf(c_66,plain,
sum(opp(f(eh)),f(eh)) = eg,
inference(resolve,[status(thm)],[c_33,c_51]) ).
cnf(c_69,plain,
sum(eg,f(eh)) = f(eh),
inference(resolve,[status(thm)],[c_30,c_51]) ).
cnf(c_2021,plain,
( sum(sum(opp(C),A),B) = sum(opp(C),sum(A,B))
| ~ h(B)
| ~ h(A) ),
inference(resolve,[status(thm)],[c_29,c_45]) ).
cnf(c_2022,plain,
( sum(sum(opp(B),f(eh)),A) = sum(opp(B),sum(f(eh),A))
| ~ h(A) ),
inference(resolve,[status(thm)],[c_2021,c_51]) ).
cnf(c_2023,plain,
sum(sum(opp(A),f(eh)),f(eh)) = sum(opp(A),sum(f(eh),f(eh))),
inference(resolve,[status(thm)],[c_2022,c_51]) ).
cnf(c_71,plain,
sum(sum(opp(A),f(eh)),f(eh)) = sum(opp(A),f(eh)),
inference(paramod,[status(thm)],[c_56,c_2023]) ).
cnf(c_2024,plain,
sum(eg,f(eh)) = sum(opp(f(eh)),f(eh)),
inference(paramod,[status(thm)],[c_66,c_71]) ).
cnf(c_2025,plain,
f(eh) = sum(opp(f(eh)),f(eh)),
inference(paramod,[status(thm)],[c_69,c_2024]) ).
cnf(c_289,plain,
f(eh) = eg,
inference(paramod,[status(thm)],[c_66,c_2025]) ).
cnf(c_2026,negated_conjecture,
( opp(f(sK0)) != f(inv(sK0))
| eg != eg ),
inference(paramod,[status(thm)],[c_289,c_38]) ).
cnf(c_290,negated_conjecture,
opp(f(sK0)) != f(inv(sK0)),
inference(copy,[status(thm)],[c_2026]) ).
cnf(c_2027,negated_conjecture,
( g(sK0)
| eg != eg ),
inference(paramod,[status(thm)],[c_289,c_36]) ).
cnf(c_291,negated_conjecture,
g(sK0),
inference(copy,[status(thm)],[c_2027]) ).
cnf(c_292,negated_conjecture,
h(f(sK0)),
inference(resolve,[status(thm)],[c_34,c_291]) ).
cnf(c_293,negated_conjecture,
product(inv(sK0),sK0) = eh,
inference(resolve,[status(thm)],[c_25,c_291]) ).
cnf(c_300,negated_conjecture,
g(inv(sK0)),
inference(resolve,[status(thm)],[c_19,c_291]) ).
cnf(c_303,plain,
sum(f(sK0),opp(f(sK0))) = eg,
inference(resolve,[status(thm)],[c_32,c_292]) ).
cnf(c_373,plain,
h(f(inv(sK0))),
inference(resolve,[status(thm)],[c_34,c_300]) ).
cnf(c_416,plain,
sum(f(inv(sK0)),eg) = f(inv(sK0)),
inference(resolve,[status(thm)],[c_31,c_373]) ).
cnf(c_2028,plain,
( sum(sum(f(inv(sK0)),A),B) = sum(f(inv(sK0)),sum(A,B))
| ~ h(B)
| ~ h(A) ),
inference(resolve,[status(thm)],[c_29,c_373]) ).
cnf(c_2029,plain,
( sum(sum(f(inv(sK0)),f(sK0)),A) = sum(f(inv(sK0)),sum(f(sK0),A))
| ~ h(A) ),
inference(resolve,[status(thm)],[c_2028,c_292]) ).
cnf(c_476,plain,
sum(sum(f(inv(sK0)),f(sK0)),opp(A)) = sum(f(inv(sK0)),sum(f(sK0),opp(A))),
inference(resolve,[status(thm)],[c_2029,c_45]) ).
cnf(c_2030,plain,
f(eh) = sum(f(inv(sK0)),f(sK0)),
inference(paramod,[status(thm)],[c_293,c_35]) ).
cnf(c_2031,plain,
eg = sum(f(inv(sK0)),f(sK0)),
inference(paramod,[status(thm)],[c_289,c_2030]) ).
cnf(c_570,plain,
sum(f(inv(sK0)),f(sK0)) = eg,
inference(copy,[status(thm)],[c_2031]) ).
cnf(c_2032,plain,
sum(eg,opp(A)) = sum(f(inv(sK0)),sum(f(sK0),opp(A))),
inference(paramod,[status(thm)],[c_570,c_476]) ).
cnf(c_2033,plain,
opp(A) = sum(f(inv(sK0)),sum(f(sK0),opp(A))),
inference(paramod,[status(thm)],[c_60,c_2032]) ).
cnf(c_572,plain,
sum(f(inv(sK0)),sum(f(sK0),opp(A))) = opp(A),
inference(copy,[status(thm)],[c_2033]) ).
cnf(c_2034,plain,
sum(f(inv(sK0)),eg) = opp(f(sK0)),
inference(paramod,[status(thm)],[c_303,c_572]) ).
cnf(c_2035,plain,
f(inv(sK0)) = opp(f(sK0)),
inference(paramod,[status(thm)],[c_416,c_2034]) ).
cnf(c_2036,plain,
opp(f(sK0)) = f(inv(sK0)),
inference(copy,[status(thm)],[c_2035]) ).
cnf(c_2019,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_290,c_2036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n007.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Fri Sep 25 15:44:23 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.47 % Process 1399597 was started by sandbox2 on n007,
% 0.20/0.47 % Fri Sep 25 15:44:23 2026
% 0.20/0.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/0.47
% 0.20/0.47 % From the command line: assign(max_seconds, 300).
% 11.43/1.96
% 11.43/1.96 % SZS status Theorem for theBenchmark
% 11.43/1.96
% 11.43/1.96 % Proof 1 at 1.09 (+ 0.37) seconds.
% 11.43/1.96 % Length of proof is 49.
% 11.43/1.96 % Level of proof is 11.
% 11.43/1.96 % Maximum clause weight is 54.000.
% 11.43/1.96 % Given clauses 129.
% 11.43/1.96
% 11.43/1.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------