%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 12:35:19 PM UTC 2026
% Result : Theorem 0.17s 0.67s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 13
% Syntax : Number of formulae : 77 ( 34 unt; 0 def)
% Number of atoms : 133 ( 63 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 103 ( 47 ~; 40 |; 7 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 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 : 65 ( 63 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] :
( g(A)
=> g(inv(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
g(eh),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( g(A)
=> product(eh,A) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( g(A)
=> product(A,inv(A)) = eh ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [B,A] :
( h(A)
=> h(opp(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
h(eg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [C,B,A] :
( ( h(C)
& h(B)
& h(A) )
=> sum(sum(A,B),C) = sum(A,sum(B,C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( h(A)
=> sum(A,eg) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( h(A)
=> sum(A,opp(A)) = eg ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( h(A)
=> sum(opp(A),A) = eg ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( g(A)
=> h(f(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [B,A] : f(product(A,B)) = sum(f(A),f(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f23,plain,
! [A] :
( g(inv(A))
| ~ g(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f24,plain,
! [X0] :
( g(inv(X0))
| ~ g(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
g(eh),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
! [A] :
( product(eh,A) = A
| ~ g(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f29,plain,
! [X0] :
( product(eh,X0) = X0
| ~ g(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f32,plain,
! [A] :
( product(A,inv(A)) = eh
| ~ g(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f33,plain,
! [X0] :
( product(X0,inv(X0)) = eh
| ~ g(X0) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f38,plain,
! [B,A] :
( h(opp(B))
| ~ h(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f39,plain,
( ! [B] : h(opp(B))
| ! [A] : ~ h(A) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( h(opp(X1))
| ~ h(X0) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
h(eg),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f42,plain,
! [C,B,A] :
( sum(sum(A,B),C) = sum(A,sum(B,C))
| ~ h(C)
| ~ h(B)
| ~ h(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1,X2] :
( sum(sum(X0,X1),X2) = sum(X0,sum(X1,X2))
| ~ h(X2)
| ~ h(X1)
| ~ h(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f46,plain,
! [A] :
( sum(A,eg) = A
| ~ h(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f47,plain,
! [X0] :
( sum(X0,eg) = X0
| ~ h(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
! [A] :
( sum(A,opp(A)) = eg
| ~ h(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f49,plain,
! [X0] :
( sum(X0,opp(X0)) = eg
| ~ h(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [A] :
( sum(opp(A),A) = eg
| ~ h(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f51,plain,
! [X0] :
( sum(opp(X0),X0) = eg
| ~ h(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [A] :
( h(f(A))
| ~ g(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f53,plain,
! [X0] :
( h(f(X0))
| ~ g(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1] : f(product(X0,X1)) = sum(f(X0),f(X1)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f55,plain,
? [X0] :
( ( f(inv(X0)) != opp(f(X0))
& g(X0) )
| f(eh) != eg ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f56,plain,
( ? [X0] :
( f(inv(X0)) != opp(f(X0))
& g(X0) )
| f(eh) != eg ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
( ( f(inv(sK0_skl)) != opp(f(sK0_skl))
& g(sK0_skl) )
| f(eh) != eg ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f56]) ).
fof(f58,plain,
( g(sK0_skl)
| f(eh) != eg ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
( f(inv(sK0_skl)) != opp(f(sK0_skl))
| f(eh) != eg ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f62,plain,
! [X0] : h(opp(X0)),
inference(resolution,[status(thm)],[f40,f41]) ).
fof(f64,plain,
h(f(eh)),
inference(resolution,[status(thm)],[f53,f25]) ).
fof(f66,plain,
product(eh,eh) = eh,
inference(resolution,[status(thm)],[f29,f25]) ).
fof(f78,plain,
sum(f(eh),eg) = f(eh),
inference(resolution,[status(thm)],[f47,f64]) ).
fof(f79,plain,
! [X0] : sum(opp(X0),eg) = opp(X0),
inference(resolution,[status(thm)],[f47,f62]) ).
fof(f163,plain,
sum(f(eh),opp(f(eh))) = eg,
inference(resolution,[status(thm)],[f49,f64]) ).
fof(f192,plain,
! [X0,X1] :
( sum(sum(f(eh),X0),X1) = sum(f(eh),sum(X0,X1))
| ~ h(X1)
| ~ h(X0) ),
inference(resolution,[status(thm)],[f43,f64]) ).
fof(f193,plain,
! [X0,X1,X2] :
( sum(sum(opp(X2),X0),X1) = sum(opp(X2),sum(X0,X1))
| ~ h(X1)
| ~ h(X0) ),
inference(resolution,[status(thm)],[f43,f62]) ).
fof(f215,plain,
! [X0] :
( sum(sum(f(eh),f(eh)),X0) = sum(f(eh),sum(f(eh),X0))
| ~ h(X0) ),
inference(resolution,[status(thm)],[f192,f64]) ).
fof(f218,plain,
! [X0] :
( sum(f(product(eh,eh)),X0) = sum(f(eh),sum(f(eh),X0))
| ~ h(X0) ),
inference(forward_demodulation,[status(thm)],[f54,f215]) ).
fof(f219,plain,
! [X0] :
( sum(f(eh),X0) = sum(f(eh),sum(f(eh),X0))
| ~ h(X0) ),
inference(forward_demodulation,[status(thm)],[f66,f218]) ).
fof(f222,plain,
! [X0] : sum(f(eh),opp(X0)) = sum(f(eh),sum(f(eh),opp(X0))),
inference(resolution,[status(thm)],[f219,f62]) ).
fof(f232,plain,
sum(f(eh),opp(f(eh))) = sum(f(eh),eg),
inference(paramodulation,[status(thm)],[f163,f222]) ).
fof(f234,plain,
eg = sum(f(eh),eg),
inference(forward_demodulation,[status(thm)],[f163,f232]) ).
fof(f241,plain,
( f(inv(sK0_skl)) != opp(f(sK0_skl))
| eg != eg ),
inference(backward_demodulation,[status(thm)],[f249,f59]) ).
fof(f242,plain,
( g(sK0_skl)
| eg != eg ),
inference(backward_demodulation,[status(thm)],[f249,f58]) ).
fof(f249,plain,
eg = f(eh),
inference(forward_demodulation,[status(thm)],[f78,f234]) ).
fof(f267,plain,
f(inv(sK0_skl)) != opp(f(sK0_skl)),
inference(trivial_equality_resolution,[status(thm)],[f241]) ).
fof(f268,plain,
g(sK0_skl),
inference(trivial_equality_resolution,[status(thm)],[f242]) ).
fof(f280,plain,
product(sK0_skl,inv(sK0_skl)) = eh,
inference(resolution,[status(thm)],[f268,f33]) ).
fof(f285,plain,
h(f(sK0_skl)),
inference(resolution,[status(thm)],[f268,f53]) ).
fof(f286,plain,
g(inv(sK0_skl)),
inference(resolution,[status(thm)],[f268,f24]) ).
fof(f298,plain,
! [X0,X1] :
( sum(sum(opp(X1),f(sK0_skl)),X0) = sum(opp(X1),sum(f(sK0_skl),X0))
| ~ h(X0) ),
inference(resolution,[status(thm)],[f285,f193]) ).
fof(f300,plain,
sum(opp(f(sK0_skl)),f(sK0_skl)) = eg,
inference(resolution,[status(thm)],[f285,f51]) ).
fof(f312,plain,
product(eh,inv(sK0_skl)) = inv(sK0_skl),
inference(resolution,[status(thm)],[f286,f29]) ).
fof(f313,plain,
h(f(inv(sK0_skl))),
inference(resolution,[status(thm)],[f286,f53]) ).
fof(f318,plain,
! [X0] : f(product(eh,X0)) = sum(eg,f(X0)),
inference(paramodulation,[status(thm)],[f249,f54]) ).
fof(f1512,plain,
! [X0] : sum(sum(opp(X0),f(sK0_skl)),f(inv(sK0_skl))) = sum(opp(X0),sum(f(sK0_skl),f(inv(sK0_skl)))),
inference(resolution,[status(thm)],[f298,f313]) ).
fof(f1521,plain,
! [X0] : sum(sum(opp(X0),f(sK0_skl)),f(inv(sK0_skl))) = sum(opp(X0),f(product(sK0_skl,inv(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f54,f1512]) ).
fof(f1522,plain,
! [X0] : sum(sum(opp(X0),f(sK0_skl)),f(inv(sK0_skl))) = sum(opp(X0),f(eh)),
inference(forward_demodulation,[status(thm)],[f280,f1521]) ).
fof(f1523,plain,
! [X0] : sum(sum(opp(X0),f(sK0_skl)),f(inv(sK0_skl))) = sum(opp(X0),eg),
inference(forward_demodulation,[status(thm)],[f249,f1522]) ).
fof(f1524,plain,
! [X0] : sum(sum(opp(X0),f(sK0_skl)),f(inv(sK0_skl))) = opp(X0),
inference(forward_demodulation,[status(thm)],[f79,f1523]) ).
fof(f1575,plain,
sum(eg,f(inv(sK0_skl))) = opp(f(sK0_skl)),
inference(paramodulation,[status(thm)],[f300,f1524]) ).
fof(f1577,plain,
f(product(eh,inv(sK0_skl))) = opp(f(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f318,f1575]) ).
fof(f1578,plain,
f(inv(sK0_skl)) = opp(f(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f312,f1577]) ).
fof(f1579,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1578,f267]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n026.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 20:42:21 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.67 % Refutation found
% 0.17/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/0.72 % Elapsed time: 0.269483 seconds
% 0.17/0.72 % CPU time: 1.749367 seconds
% 0.17/0.72 % Total memory used: 86.917 MB
% 0.17/0.72 % Net memory used: 85.821 MB
%------------------------------------------------------------------------------