%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 01:28:23 PM UTC 2026
% Result : Theorem 41.14s 5.58s
% Output : Proof 41.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 16
% Syntax : Number of formulae : 231 ( 181 unt; 0 def)
% Number of atoms : 297 ( 213 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 120 ( 54 ~; 48 |; 7 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-4 aty)
% Number of variables : 181 ( 14 sgn 53 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,conjecture,
! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18_neg,negated_conjecture,
~ ! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f18_nnf,plain,
? [X0] :
( ( f(inv(X0)) != opp(f(X0))
& g(X0) )
| f(eh) != eg ),
inference(nnf_transformation,[status(thm)],[f18_neg]) ).
fof(f18_sk,plain,
( ( f(inv(sk0)) != opp(f(sk0))
& g(sk0) )
| f(eh) != eg ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f18_nnf]) ).
cnf(c19,plain,
( f(inv(sk0)) != opp(f(sk0))
| f(eh) != eg ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t251,plain,
ifeq(f(eh),eg,ifeq(f(inv(sk0)),opp(f(sk0)),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t590,plain,
ifeq(f(eh),eg,ifeq(f(inv(sk0)),opp(f(sk0)),false,true),true) = true,
inference(orient,[status(thm)],[t251]) ).
fof(f11,axiom,
! [C,B,A] :
( ( h(C)
& h(B)
& h(A) )
=> sum(sum(A,B),C) = sum(A,sum(B,C)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos12) ).
fof(f11_nnf,plain,
! [C,B,A] :
( sum(sum(A,B),C) = sum(A,sum(B,C))
| ~ h(C)
| ~ h(B)
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B,C] :
( sum(sum(A,B),C) = sum(A,sum(B,C))
| ~ h(C)
| ~ h(B)
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( sum(sum(X2,X1),X0) = sum(X2,sum(X1,X0))
| ~ h(X0)
| ~ h(X1)
| ~ h(X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t255,plain,
ifeq(h(X1),true,ifeq(h(X2),true,ifeq(h(X3),true,sum(sum(X1,X2),X3),sum(X1,sum(X2,X3))),sum(X1,sum(X2,X3))),sum(X1,sum(X2,X3))) = sum(X1,sum(X2,X3)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t300,plain,
ifeq(h(X1),true,ifeq(h(X2),true,ifeq(h(X3),true,sum(sum(X1,X2),X3),sum(X1,sum(X2,X3))),sum(X1,sum(X2,X3))),sum(X1,sum(X2,X3))) = sum(X1,sum(X2,X3)),
inference(orient,[status(thm)],[t255]) ).
fof(f17,axiom,
! [B,A] : f(product(A,B)) = sum(f(A),f(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos18) ).
fof(f17_nnf,plain,
! [B,A] : f(product(A,B)) = sum(f(A),f(B)),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B] : f(product(A,B)) = sum(f(A),f(B)),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
f(product(X1,X0)) = sum(f(X1),f(X0)),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t157,plain,
sum(f(X1),f(X2)) = f(product(X1,X2)),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t537,plain,
sum(f(X1),f(X2)) = f(product(X1,X2)),
inference(orient,[status(thm)],[t157]) ).
cnf(t539,plain,
sum(X1,sum(f(X2),f(X3))) = ifeq(h(X1),true,ifeq(h(f(X2)),true,ifeq(h(f(X3)),true,sum(sum(X1,f(X2)),f(X3)),sum(X1,f(product(X2,X3)))),sum(X1,sum(f(X2),f(X3)))),sum(X1,sum(f(X2),f(X3)))),
inference(cp,[status(thm)],[t300,t537]) ).
cnf(t68413,plain,
sum(X1,f(product(X2,X3))) = ifeq(h(X1),true,ifeq(h(f(X2)),true,ifeq(h(f(X3)),true,sum(sum(X1,f(X2)),f(X3)),sum(X1,f(product(X2,X3)))),sum(X1,sum(f(X2),f(X3)))),sum(X1,sum(f(X2),f(X3)))),
inference(step,[status(thm)],[t539,t537]) ).
cnf(t68414,plain,
sum(X1,f(product(X2,X3))) = ifeq(h(X1),true,ifeq(h(f(X2)),true,ifeq(h(f(X3)),true,sum(sum(X1,f(X2)),f(X3)),sum(X1,f(product(X2,X3)))),sum(X1,f(product(X2,X3)))),sum(X1,sum(f(X2),f(X3)))),
inference(step,[status(thm)],[t68413,t537]) ).
cnf(t68415,plain,
sum(X1,f(product(X2,X3))) = ifeq(h(X1),true,ifeq(h(f(X2)),true,ifeq(h(f(X3)),true,sum(sum(X1,f(X2)),f(X3)),sum(X1,f(product(X2,X3)))),sum(X1,f(product(X2,X3)))),sum(X1,f(product(X2,X3)))),
inference(step,[status(thm)],[t68414,t537]) ).
cnf(t56418,plain,
ifeq(h(X1),true,ifeq(h(f(X2)),true,ifeq(h(f(X3)),true,sum(sum(X1,f(X2)),f(X3)),sum(X1,f(product(X2,X3)))),sum(X1,f(product(X2,X3)))),sum(X1,f(product(X2,X3)))) = sum(X1,f(product(X2,X3))),
inference(orient,[status(thm)],[t68415]) ).
fof(f5,axiom,
! [A] :
( g(A)
=> product(A,eh) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos06) ).
fof(f5_nnf,plain,
! [A] :
( product(A,eh) = A
| ~ g(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] :
( product(A,eh) = A
| ~ g(A) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( product(X0,eh) = X0
| ~ g(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(g(X0),true,product(X0,eh),X0) = X0,
inference(equality_encoding,[status(esa)],[c5]) ).
fof(f2,axiom,
g(eh),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos03) ).
fof(f2_nnf,plain,
g(eh),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
g(eh),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(hi2,axiom,
g(eh) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t4,plain,
product(eh,eh) = eh,
inference(hyper_resolution,[status(thm)],[hi5,hi2]) ).
cnf(t261,plain,
product(eh,eh) = eh,
inference(orient,[status(thm)],[t4]) ).
cnf(t57305,plain,
sum(X1,f(product(eh,eh))) = ifeq(h(X1),true,ifeq(h(f(eh)),true,ifeq(h(f(eh)),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),sum(X1,f(product(eh,eh)))),sum(X1,f(product(eh,eh)))),
inference(cp,[status(thm)],[t56418,t261]) ).
cnf(t68416,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,ifeq(h(f(eh)),true,ifeq(h(f(eh)),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),sum(X1,f(product(eh,eh)))),sum(X1,f(product(eh,eh)))),
inference(step,[status(thm)],[t57305,t261]) ).
fof(f16,axiom,
! [A] :
( g(A)
=> h(f(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos17) ).
fof(f16_nnf,plain,
! [A] :
( h(f(A))
| ~ g(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A] :
( h(f(A))
| ~ g(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( h(f(X0))
| ~ g(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi16,axiom,
ifeq(g(X0),true,h(f(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(h0,plain,
h(f(eh)) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi2]) ).
fof(f8,axiom,
! [B,A] :
( ( h(B)
& h(A) )
=> h(sum(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos09) ).
fof(f8_nnf,plain,
! [B,A] :
( h(sum(A,B))
| ~ h(B)
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] :
( h(sum(A,B))
| ~ h(B)
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( h(sum(X1,X0))
| ~ h(X0)
| ~ h(X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(h(X0),true,ifeq(h(X1),true,h(sum(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
fof(f10,axiom,
h(eg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos11) ).
fof(f10_nnf,plain,
h(eg),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
h(eg),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(hi10,axiom,
h(eg) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(h12,plain,
h(sum(eg,eg)) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi10,hi10]) ).
cnf(t90,plain,
h(sum(sum(eg,eg),f(eh))) = true,
inference(hyper_resolution,[status(thm)],[hi8,h12,h0]) ).
cnf(hi11,axiom,
ifeq(h(X0),true,ifeq(h(X1),true,ifeq(h(X2),true,sum(sum(X0,X1),X2),sum(X0,sum(X1,X2))),sum(X0,sum(X1,X2))),sum(X0,sum(X1,X2))) = sum(X0,sum(X1,X2)),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t236,plain,
sum(sum(eg,eg),f(eh)) = sum(eg,sum(eg,f(eh))),
inference(hyper_resolution,[status(thm)],[hi11,hi10,hi10,h0]) ).
cnf(t342,plain,
sum(sum(eg,eg),f(eh)) = sum(eg,sum(eg,f(eh))),
inference(orient,[status(thm)],[t236]) ).
cnf(h25,plain,
h(sum(eg,f(eh))) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi10,h0]) ).
fof(f12,axiom,
! [A] :
( h(A)
=> sum(eg,A) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos13) ).
fof(f12_nnf,plain,
! [A] :
( sum(eg,A) = A
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] :
( sum(eg,A) = A
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( sum(eg,X0) = X0
| ~ h(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(h(X0),true,sum(eg,X0),X0) = X0,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t179,plain,
sum(eg,sum(eg,f(eh))) = sum(eg,f(eh)),
inference(hyper_resolution,[status(thm)],[hi12,h25]) ).
cnf(t448,plain,
sum(eg,sum(eg,f(eh))) = sum(eg,f(eh)),
inference(orient,[status(thm)],[t179]) ).
cnf(t67292,plain,
sum(sum(eg,eg),f(eh)) = sum(eg,f(eh)),
inference(step,[status(thm)],[t342,t448]) ).
cnf(t449,plain,
sum(sum(eg,eg),f(eh)) = sum(eg,f(eh)),
inference(orient,[status(thm)],[t67292]) ).
cnf(t67317,plain,
h(sum(eg,f(eh))) = true,
inference(step,[status(thm)],[t90,t449]) ).
cnf(t25,plain,
sum(eg,f(eh)) = f(eh),
inference(hyper_resolution,[status(thm)],[hi12,h0]) ).
cnf(t519,plain,
sum(eg,f(eh)) = f(eh),
inference(orient,[status(thm)],[t25]) ).
cnf(t67318,plain,
h(f(eh)) = true,
inference(step,[status(thm)],[t67317,t519]) ).
cnf(t585,plain,
h(f(eh)) = true,
inference(orient,[status(thm)],[t67318]) ).
cnf(t68417,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,ifeq(true,true,ifeq(h(f(eh)),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),sum(X1,f(product(eh,eh)))),sum(X1,f(product(eh,eh)))),
inference(step,[status(thm)],[t68416,t585]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t68418,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,ifeq(h(f(eh)),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),sum(X1,f(product(eh,eh)))),
inference(step,[status(thm)],[t68417,t256]) ).
cnf(t68419,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,ifeq(true,true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),sum(X1,f(product(eh,eh)))),
inference(step,[status(thm)],[t68418,t585]) ).
cnf(t68420,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(product(eh,eh)))),
inference(step,[status(thm)],[t68419,t256]) ).
cnf(t68421,plain,
sum(X1,f(eh)) = ifeq(h(X1),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))),
inference(step,[status(thm)],[t68420,t261]) ).
cnf(t57310,plain,
ifeq(h(X1),true,sum(sum(X1,f(eh)),f(eh)),sum(X1,f(eh))) = sum(X1,f(eh)),
inference(orient,[status(thm)],[t68421]) ).
fof(f15,axiom,
! [A] :
( h(A)
=> sum(opp(A),A) = eg ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos16) ).
fof(f15_nnf,plain,
! [A] :
( sum(opp(A),A) = eg
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A] :
( sum(opp(A),A) = eg
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( sum(opp(X0),X0) = eg
| ~ h(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi15,axiom,
ifeq(h(X0),true,sum(opp(X0),X0),eg) = eg,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t200,plain,
sum(opp(sum(eg,f(eh))),sum(eg,f(eh))) = eg,
inference(hyper_resolution,[status(thm)],[hi15,h25]) ).
cnf(t67310,plain,
sum(opp(f(eh)),sum(eg,f(eh))) = eg,
inference(step,[status(thm)],[t200,t519]) ).
cnf(t67311,plain,
sum(opp(f(eh)),f(eh)) = eg,
inference(step,[status(thm)],[t67310,t519]) ).
cnf(t559,plain,
sum(opp(f(eh)),f(eh)) = eg,
inference(orient,[status(thm)],[t67311]) ).
cnf(t58189,plain,
sum(opp(f(eh)),f(eh)) = ifeq(h(opp(f(eh))),true,sum(eg,f(eh)),sum(opp(f(eh)),f(eh))),
inference(cp,[status(thm)],[t57310,t559]) ).
cnf(t68422,plain,
eg = ifeq(h(opp(f(eh))),true,sum(eg,f(eh)),sum(opp(f(eh)),f(eh))),
inference(step,[status(thm)],[t58189,t559]) ).
fof(f9,axiom,
! [B,A] :
( h(A)
=> h(opp(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos10) ).
fof(f9_nnf,plain,
! [B,A] :
( h(opp(B))
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] :
( h(opp(B))
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( h(opp(X0))
| ~ h(X1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t150,plain,
ifeq(h(X1),true,h(opp(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t596,plain,
ifeq(h(X1),true,h(opp(X2)),true) = true,
inference(orient,[status(thm)],[t150]) ).
cnf(h148,plain,
h(sum(sum(eg,eg),eg)) = true,
inference(hyper_resolution,[status(thm)],[hi8,h12,hi10]) ).
cnf(t145,plain,
h(sum(sum(sum(eg,eg),eg),eg)) = true,
inference(hyper_resolution,[status(thm)],[hi8,h148,hi10]) ).
fof(f13,axiom,
! [A] :
( h(A)
=> sum(A,eg) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos14) ).
fof(f13_nnf,plain,
! [A] :
( sum(A,eg) = A
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( sum(A,eg) = A
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( sum(X0,eg) = X0
| ~ h(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
ifeq(h(X0),true,sum(X0,eg),X0) = X0,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t245,plain,
sum(sum(sum(eg,eg),eg),eg) = sum(sum(eg,eg),eg),
inference(hyper_resolution,[status(thm)],[hi13,h148]) ).
cnf(t301,plain,
sum(sum(sum(eg,eg),eg),eg) = sum(sum(eg,eg),eg),
inference(orient,[status(thm)],[t245]) ).
cnf(t67314,plain,
h(sum(sum(eg,eg),eg)) = true,
inference(step,[status(thm)],[t145,t301]) ).
cnf(t185,plain,
sum(sum(eg,eg),eg) = sum(eg,sum(eg,eg)),
inference(hyper_resolution,[status(thm)],[hi11,hi10,hi10,hi10]) ).
cnf(t324,plain,
sum(sum(eg,eg),eg) = sum(eg,sum(eg,eg)),
inference(orient,[status(thm)],[t185]) ).
cnf(t101,plain,
sum(sum(eg,eg),eg) = sum(eg,eg),
inference(hyper_resolution,[status(thm)],[hi13,h12]) ).
cnf(t67283,plain,
sum(eg,sum(eg,eg)) = sum(eg,eg),
inference(step,[status(thm)],[t101,t324]) ).
cnf(t331,plain,
sum(eg,sum(eg,eg)) = sum(eg,eg),
inference(orient,[status(thm)],[t67283]) ).
cnf(t67284,plain,
sum(sum(eg,eg),eg) = sum(eg,eg),
inference(step,[status(thm)],[t324,t331]) ).
cnf(t332,plain,
sum(sum(eg,eg),eg) = sum(eg,eg),
inference(orient,[status(thm)],[t67284]) ).
cnf(t67315,plain,
h(sum(eg,eg)) = true,
inference(step,[status(thm)],[t67314,t332]) ).
cnf(t5,plain,
sum(eg,eg) = eg,
inference(hyper_resolution,[status(thm)],[hi13,hi10]) ).
cnf(t511,plain,
sum(eg,eg) = eg,
inference(orient,[status(thm)],[t5]) ).
cnf(t67316,plain,
h(eg) = true,
inference(step,[status(thm)],[t67315,t511]) ).
cnf(t581,plain,
h(eg) = true,
inference(orient,[status(thm)],[t67316]) ).
cnf(t597,plain,
true = ifeq(true,true,h(opp(X1)),true),
inference(cp,[status(thm)],[t596,t581]) ).
cnf(t67319,plain,
true = h(opp(X1)),
inference(step,[status(thm)],[t597,t256]) ).
cnf(t615,plain,
h(opp(X1)) = true,
inference(orient,[status(thm)],[t67319]) ).
cnf(t68423,plain,
eg = ifeq(true,true,sum(eg,f(eh)),sum(opp(f(eh)),f(eh))),
inference(step,[status(thm)],[t68422,t615]) ).
cnf(t68424,plain,
eg = sum(eg,f(eh)),
inference(step,[status(thm)],[t68423,t256]) ).
cnf(t68425,plain,
eg = f(eh),
inference(step,[status(thm)],[t68424,t519]) ).
cnf(t58193,plain,
f(eh) = eg,
inference(orient,[status(thm)],[t68425]) ).
cnf(t68428,plain,
ifeq(eg,eg,ifeq(f(inv(sk0)),opp(f(sk0)),false,true),true) = true,
inference(step,[status(thm)],[t590,t58193]) ).
cnf(t68429,plain,
ifeq(f(inv(sk0)),opp(f(sk0)),false,true) = true,
inference(step,[status(thm)],[t68428,t256]) ).
cnf(t58209,plain,
ifeq(f(inv(sk0)),opp(f(sk0)),false,true) = true,
inference(rw,[status(thm)],[t68429]) ).
cnf(t59330,plain,
ifeq(f(inv(sk0)),opp(f(sk0)),false,true) = true,
inference(orient,[status(thm)],[t58209]) ).
cnf(hi9,axiom,
ifeq(h(X0),true,h(opp(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h11,plain,
h(opp(V0)) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi10]) ).
fof(f14,axiom,
! [A] :
( h(A)
=> sum(A,opp(A)) = eg ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos15) ).
fof(f14_nnf,plain,
! [A] :
( sum(A,opp(A)) = eg
| ~ h(A) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A] :
( sum(A,opp(A)) = eg
| ~ h(A) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( sum(X0,opp(X0)) = eg
| ~ h(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi14,axiom,
ifeq(h(X0),true,sum(X0,opp(X0)),eg) = eg,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t50,plain,
sum(opp(X1),opp(opp(X1))) = eg,
inference(hyper_resolution,[status(thm)],[hi14,h11]) ).
cnf(t554,plain,
sum(opp(X1),opp(opp(X1))) = eg,
inference(orient,[status(thm)],[t50]) ).
cnf(t556,plain,
sum(X1,sum(opp(X2),opp(opp(X2)))) = ifeq(h(X1),true,ifeq(h(opp(X2)),true,ifeq(h(opp(opp(X2))),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),sum(X1,sum(opp(X2),opp(opp(X2))))),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(cp,[status(thm)],[t300,t554]) ).
cnf(t68677,plain,
sum(X1,eg) = ifeq(h(X1),true,ifeq(h(opp(X2)),true,ifeq(h(opp(opp(X2))),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),sum(X1,sum(opp(X2),opp(opp(X2))))),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(step,[status(thm)],[t556,t554]) ).
cnf(t68678,plain,
sum(X1,eg) = ifeq(h(X1),true,ifeq(true,true,ifeq(h(opp(opp(X2))),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),sum(X1,sum(opp(X2),opp(opp(X2))))),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(step,[status(thm)],[t68677,t615]) ).
cnf(t68679,plain,
sum(X1,eg) = ifeq(h(X1),true,ifeq(h(opp(opp(X2))),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(step,[status(thm)],[t68678,t256]) ).
cnf(t68680,plain,
sum(X1,eg) = ifeq(h(X1),true,ifeq(true,true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(step,[status(thm)],[t68679,t615]) ).
cnf(t68681,plain,
sum(X1,eg) = ifeq(h(X1),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,sum(opp(X2),opp(opp(X2))))),
inference(step,[status(thm)],[t68680,t256]) ).
cnf(t68682,plain,
sum(X1,eg) = ifeq(h(X1),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)),
inference(step,[status(thm)],[t68681,t554]) ).
cnf(t62192,plain,
ifeq(h(X1),true,sum(sum(X1,opp(X2)),opp(opp(X2))),sum(X1,eg)) = sum(X1,eg),
inference(orient,[status(thm)],[t68682]) ).
cnf(t166,plain,
ifeq(h(X1),true,sum(X1,opp(X1)),eg) = eg,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t569,plain,
ifeq(h(X1),true,sum(X1,opp(X1)),eg) = eg,
inference(orient,[status(thm)],[t166]) ).
cnf(t147,plain,
ifeq(g(X1),true,h(f(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t592,plain,
ifeq(g(X1),true,h(f(X1)),true) = true,
inference(orient,[status(thm)],[t147]) ).
fof(f1,axiom,
! [A] :
( g(A)
=> g(inv(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos02) ).
fof(f1_nnf,plain,
! [A] :
( g(inv(A))
| ~ g(A) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] :
( g(inv(A))
| ~ g(A) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( g(inv(X0))
| ~ g(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t146,plain,
ifeq(g(X1),true,g(inv(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t591,plain,
ifeq(g(X1),true,g(inv(X1)),true) = true,
inference(orient,[status(thm)],[t146]) ).
cnf(c18,plain,
( g(sk0)
| f(eh) != eg ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t93,plain,
ifeq(f(eh),eg,g(sk0),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t589,plain,
ifeq(f(eh),eg,g(sk0),true) = true,
inference(orient,[status(thm)],[t93]) ).
cnf(t68426,plain,
ifeq(eg,eg,g(sk0),true) = true,
inference(step,[status(thm)],[t589,t58193]) ).
cnf(t68427,plain,
g(sk0) = true,
inference(step,[status(thm)],[t68426,t256]) ).
cnf(t58208,plain,
g(sk0) = true,
inference(rw,[status(thm)],[t68427]) ).
cnf(t58214,plain,
g(sk0) = true,
inference(orient,[status(thm)],[t58208]) ).
cnf(t58223,plain,
true = ifeq(true,true,g(inv(sk0)),true),
inference(cp,[status(thm)],[t591,t58214]) ).
cnf(t68457,plain,
true = g(inv(sk0)),
inference(step,[status(thm)],[t58223,t256]) ).
cnf(t58285,plain,
g(inv(sk0)) = true,
inference(orient,[status(thm)],[t68457]) ).
cnf(t58293,plain,
true = ifeq(true,true,h(f(inv(sk0))),true),
inference(cp,[status(thm)],[t592,t58285]) ).
cnf(t68460,plain,
true = h(f(inv(sk0))),
inference(step,[status(thm)],[t58293,t256]) ).
cnf(t58319,plain,
h(f(inv(sk0))) = true,
inference(orient,[status(thm)],[t68460]) ).
cnf(t58328,plain,
eg = ifeq(true,true,sum(f(inv(sk0)),opp(f(inv(sk0)))),eg),
inference(cp,[status(thm)],[t569,t58319]) ).
cnf(t68493,plain,
eg = sum(f(inv(sk0)),opp(f(inv(sk0)))),
inference(step,[status(thm)],[t58328,t256]) ).
cnf(t58893,plain,
sum(f(inv(sk0)),opp(f(inv(sk0)))) = eg,
inference(orient,[status(thm)],[t68493]) ).
cnf(t62301,plain,
sum(f(inv(sk0)),eg) = ifeq(h(f(inv(sk0))),true,sum(eg,opp(opp(f(inv(sk0))))),sum(f(inv(sk0)),eg)),
inference(cp,[status(thm)],[t62192,t58893]) ).
cnf(t151,plain,
ifeq(h(X1),true,sum(X1,eg),X1) = X1,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t259,plain,
ifeq(h(X1),true,sum(X1,eg),X1) = X1,
inference(orient,[status(thm)],[t151]) ).
cnf(t58321,plain,
f(inv(sk0)) = ifeq(true,true,sum(f(inv(sk0)),eg),f(inv(sk0))),
inference(cp,[status(thm)],[t259,t58319]) ).
cnf(t68469,plain,
f(inv(sk0)) = sum(f(inv(sk0)),eg),
inference(step,[status(thm)],[t58321,t256]) ).
cnf(t58509,plain,
sum(f(inv(sk0)),eg) = f(inv(sk0)),
inference(orient,[status(thm)],[t68469]) ).
cnf(t68687,plain,
f(inv(sk0)) = ifeq(h(f(inv(sk0))),true,sum(eg,opp(opp(f(inv(sk0))))),sum(f(inv(sk0)),eg)),
inference(step,[status(thm)],[t62301,t58509]) ).
cnf(t68688,plain,
f(inv(sk0)) = ifeq(true,true,sum(eg,opp(opp(f(inv(sk0))))),sum(f(inv(sk0)),eg)),
inference(step,[status(thm)],[t68687,t58319]) ).
cnf(t68689,plain,
f(inv(sk0)) = sum(eg,opp(opp(f(inv(sk0))))),
inference(step,[status(thm)],[t68688,t256]) ).
cnf(t26,plain,
sum(eg,opp(X1)) = opp(X1),
inference(hyper_resolution,[status(thm)],[hi12,h11]) ).
cnf(t528,plain,
sum(eg,opp(X1)) = opp(X1),
inference(orient,[status(thm)],[t26]) ).
cnf(t68690,plain,
f(inv(sk0)) = opp(opp(f(inv(sk0)))),
inference(step,[status(thm)],[t68689,t528]) ).
cnf(t62608,plain,
opp(opp(f(inv(sk0)))) = f(inv(sk0)),
inference(orient,[status(thm)],[t68690]) ).
cnf(t555,plain,
sum(opp(X1),sum(opp(opp(X1)),X2)) = ifeq(h(opp(X1)),true,ifeq(h(opp(opp(X1))),true,ifeq(h(X2),true,sum(eg,X2),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),
inference(cp,[status(thm)],[t300,t554]) ).
cnf(t68619,plain,
sum(opp(X1),sum(opp(opp(X1)),X2)) = ifeq(true,true,ifeq(h(opp(opp(X1))),true,ifeq(h(X2),true,sum(eg,X2),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),
inference(step,[status(thm)],[t555,t615]) ).
cnf(t68620,plain,
sum(opp(X1),sum(opp(opp(X1)),X2)) = ifeq(h(opp(opp(X1))),true,ifeq(h(X2),true,sum(eg,X2),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),
inference(step,[status(thm)],[t68619,t256]) ).
cnf(t68621,plain,
sum(opp(X1),sum(opp(opp(X1)),X2)) = ifeq(true,true,ifeq(h(X2),true,sum(eg,X2),sum(opp(X1),sum(opp(opp(X1)),X2))),sum(opp(X1),sum(opp(opp(X1)),X2))),
inference(step,[status(thm)],[t68620,t615]) ).
cnf(t68622,plain,
sum(opp(X1),sum(opp(opp(X1)),X2)) = ifeq(h(X2),true,sum(eg,X2),sum(opp(X1),sum(opp(opp(X1)),X2))),
inference(step,[status(thm)],[t68621,t256]) ).
cnf(t60938,plain,
ifeq(h(X1),true,sum(eg,X1),sum(opp(X2),sum(opp(opp(X2)),X1))) = sum(opp(X2),sum(opp(opp(X2)),X1)),
inference(orient,[status(thm)],[t68622]) ).
cnf(t58222,plain,
true = ifeq(true,true,h(f(sk0)),true),
inference(cp,[status(thm)],[t592,t58214]) ).
cnf(t68456,plain,
true = h(f(sk0)),
inference(step,[status(thm)],[t58222,t256]) ).
cnf(t58252,plain,
h(f(sk0)) = true,
inference(orient,[status(thm)],[t68456]) ).
cnf(t60959,plain,
sum(opp(X1),sum(opp(opp(X1)),f(sk0))) = ifeq(true,true,sum(eg,f(sk0)),sum(opp(X1),sum(opp(opp(X1)),f(sk0)))),
inference(cp,[status(thm)],[t60938,t58252]) ).
cnf(t68788,plain,
sum(opp(X1),sum(opp(opp(X1)),f(sk0))) = sum(eg,f(sk0)),
inference(step,[status(thm)],[t60959,t256]) ).
cnf(t152,plain,
ifeq(h(X1),true,sum(eg,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t260,plain,
ifeq(h(X1),true,sum(eg,X1),X1) = X1,
inference(orient,[status(thm)],[t152]) ).
cnf(t58253,plain,
f(sk0) = ifeq(true,true,sum(eg,f(sk0)),f(sk0)),
inference(cp,[status(thm)],[t260,t58252]) ).
cnf(t68462,plain,
f(sk0) = sum(eg,f(sk0)),
inference(step,[status(thm)],[t58253,t256]) ).
cnf(t58370,plain,
sum(eg,f(sk0)) = f(sk0),
inference(orient,[status(thm)],[t68462]) ).
cnf(t68789,plain,
sum(opp(X1),sum(opp(opp(X1)),f(sk0))) = f(sk0),
inference(step,[status(thm)],[t68788,t58370]) ).
cnf(t66768,plain,
sum(opp(X1),sum(opp(opp(X1)),f(sk0))) = f(sk0),
inference(orient,[status(thm)],[t68789]) ).
cnf(t66780,plain,
f(sk0) = sum(opp(f(inv(sk0))),sum(f(inv(sk0)),f(sk0))),
inference(cp,[status(thm)],[t66768,t62608]) ).
cnf(t68790,plain,
f(sk0) = sum(opp(f(inv(sk0))),f(product(inv(sk0),sk0))),
inference(step,[status(thm)],[t66780,t537]) ).
fof(f7,axiom,
! [A] :
( g(A)
=> product(inv(A),A) = eh ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos08) ).
fof(f7_nnf,plain,
! [A] :
( product(inv(A),A) = eh
| ~ g(A) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] :
( product(inv(A),A) = eh
| ~ g(A) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( product(inv(X0),X0) = eh
| ~ g(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t165,plain,
ifeq(g(X1),true,product(inv(X1),X1),eh) = eh,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t286,plain,
ifeq(g(X1),true,product(inv(X1),X1),eh) = eh,
inference(orient,[status(thm)],[t165]) ).
cnf(t58217,plain,
eh = ifeq(true,true,product(inv(sk0),sk0),eh),
inference(cp,[status(thm)],[t286,t58214]) ).
cnf(t68458,plain,
eh = product(inv(sk0),sk0),
inference(step,[status(thm)],[t58217,t256]) ).
cnf(t58301,plain,
product(inv(sk0),sk0) = eh,
inference(orient,[status(thm)],[t68458]) ).
cnf(t68791,plain,
f(sk0) = sum(opp(f(inv(sk0))),f(eh)),
inference(step,[status(thm)],[t68790,t58301]) ).
cnf(t68792,plain,
f(sk0) = sum(opp(f(inv(sk0))),eg),
inference(step,[status(thm)],[t68791,t58193]) ).
cnf(t28,plain,
sum(opp(X1),eg) = opp(X1),
inference(hyper_resolution,[status(thm)],[hi13,h11]) ).
cnf(t547,plain,
sum(opp(X1),eg) = opp(X1),
inference(orient,[status(thm)],[t28]) ).
cnf(t68793,plain,
f(sk0) = opp(f(inv(sk0))),
inference(step,[status(thm)],[t68792,t547]) ).
cnf(t66793,plain,
opp(f(inv(sk0))) = f(sk0),
inference(orient,[status(thm)],[t68793]) ).
cnf(t68794,plain,
opp(f(sk0)) = f(inv(sk0)),
inference(step,[status(thm)],[t62608,t66793]) ).
cnf(t67076,plain,
opp(f(sk0)) = f(inv(sk0)),
inference(rw,[status(thm)],[t68794]) ).
cnf(t67253,plain,
f(inv(sk0)) = opp(f(sk0)),
inference(orient,[status(thm)],[t67076]) ).
cnf(t68801,plain,
ifeq(opp(f(sk0)),opp(f(sk0)),false,true) = true,
inference(step,[status(thm)],[t59330,t67253]) ).
cnf(t68802,plain,
false = true,
inference(step,[status(thm)],[t68801,t256]) ).
cnf(t67278,plain,
false = true,
inference(rw,[status(thm)],[t68802]) ).
cnf(t67279,plain,
false = true,
inference(orient,[status(thm)],[t67278]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t67279]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Wed Sep 23 16:00:54 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 41.14/5.58 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.14/5.58 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------