%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:24:38 AM UTC 2026
% Result : Theorem 42.95s 7.59s
% Output : CNFRefutation 42.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 14
% Syntax : Number of formulae : 112 ( 72 unt; 0 def)
% Number of atoms : 163 ( 102 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 91 ( 40 ~; 37 |; 4 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 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 : 111 ( 3 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos02,axiom,
! [X0] :
( g(X0)
=> g(inv(X0)) ) ).
fof(sos03,axiom,
g(eh) ).
fof(sos05,axiom,
! [X0] :
( g(X0)
=> product(eh,X0) = X0 ) ).
fof(sos08,axiom,
! [X0] :
( g(X0)
=> product(inv(X0),X0) = eh ) ).
fof(sos10,axiom,
! [X0,X1] :
( h(X1)
=> h(opp(X0)) ) ).
fof(sos11,axiom,
h(eg) ).
fof(sos12,axiom,
! [X0,X1,X2] :
( ( h(X0)
& h(X1)
& h(X2) )
=> sum(sum(X2,X1),X0) = sum(X2,sum(X1,X0)) ) ).
fof(sos13,axiom,
! [X0] :
( h(X0)
=> sum(eg,X0) = X0 ) ).
fof(sos14,axiom,
! [X0] :
( h(X0)
=> sum(X0,eg) = X0 ) ).
fof(sos15,axiom,
! [X0] :
( h(X0)
=> sum(X0,opp(X0)) = eg ) ).
fof(sos16,axiom,
! [X0] :
( h(X0)
=> sum(opp(X0),X0) = eg ) ).
fof(sos17,axiom,
! [X0] :
( g(X0)
=> h(f(X0)) ) ).
fof(sos18,axiom,
! [X0,X1] : f(product(X1,X0)) = sum(f(X1),f(X0)) ).
fof(goals,conjecture,
! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( f(inv(X0)) = opp(f(X0))
| ~ g(X0) )
& f(eh) = eg ),
inference(negate_conjecture,[status(cth)],[goals]) ).
cnf(c1,plain,
( g(inv(X0))
| ~ g(X0) ),
inference(clausification,[status(esa)],[sos02]) ).
cnf(c2,plain,
g(eh),
inference(clausification,[status(esa)],[sos03]) ).
cnf(c4,plain,
( product(eh,X0) = X0
| ~ g(X0) ),
inference(clausification,[status(esa)],[sos05]) ).
cnf(c7,plain,
( product(inv(X0),X0) = eh
| ~ g(X0) ),
inference(clausification,[status(esa)],[sos08]) ).
cnf(c9,plain,
( h(opp(X1))
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos10]) ).
cnf(c10,plain,
h(eg),
inference(clausification,[status(esa)],[sos11]) ).
cnf(c11,plain,
( sum(sum(X0,X1),X2) = sum(X0,sum(X1,X2))
| ~ h(X2)
| ~ h(X1)
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos12]) ).
cnf(c12,plain,
( sum(eg,X0) = X0
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos13]) ).
cnf(c13,plain,
( sum(X0,eg) = X0
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos14]) ).
cnf(c14,plain,
( sum(X0,opp(X0)) = eg
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos15]) ).
cnf(c15,plain,
( sum(opp(X0),X0) = eg
| ~ h(X0) ),
inference(clausification,[status(esa)],[sos16]) ).
cnf(c16,plain,
( h(f(X0))
| ~ g(X0) ),
inference(clausification,[status(esa)],[sos17]) ).
cnf(c17,plain,
f(product(X0,X1)) = sum(f(X0),f(X1)),
inference(clausification,[status(esa)],[sos18]) ).
cnf(c18,plain,
( g(sK24)
| f(eh) != eg ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c19,plain,
( f(inv(sK24)) != opp(f(sK24))
| f(eh) != eg ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
h(opp(X0)),
inference(resolution,[status(thm)],[c9,c10]) ).
cnf(d1,plain,
sum(opp(X0),eg) = opp(X0),
inference(resolution,[status(thm)],[c13,d0]) ).
cnf(d2,plain,
( ~ g(X0)
| sum(opp(f(X0)),f(X0)) = eg ),
inference(resolution,[status(thm)],[c15,c16]) ).
cnf(d3,plain,
sum(opp(f(eh)),f(eh)) = eg,
inference(resolution,[status(thm)],[d2,c2]) ).
cnf(d4,plain,
product(eh,eh) = eh,
inference(resolution,[status(thm)],[c4,c2]) ).
cnf(d5,plain,
( ~ g(X0)
| sum(f(X0),eg) = f(X0) ),
inference(resolution,[status(thm)],[c13,c16]) ).
cnf(d6,plain,
sum(f(eh),eg) = f(eh),
inference(resolution,[status(thm)],[d5,c2]) ).
cnf(d7,plain,
sum(eg,opp(X0)) = opp(X0),
inference(resolution,[status(thm)],[c12,d0]) ).
cnf(d8,plain,
( ~ g(X0)
| ~ h(X2)
| ~ h(X1)
| sum(sum(f(X0),X1),X2) = sum(f(X0),sum(X1,X2)) ),
inference(resolution,[status(thm)],[c11,c16]) ).
cnf(d9,plain,
( ~ h(X2)
| ~ g(X0)
| sum(sum(f(X0),opp(X1)),X2) = sum(f(X0),sum(opp(X1),X2)) ),
inference(resolution,[status(thm)],[d8,d0]) ).
cnf(d10,plain,
( ~ g(X0)
| sum(sum(f(X0),opp(X1)),opp(X2)) = sum(f(X0),sum(opp(X1),opp(X2))) ),
inference(resolution,[status(thm)],[d9,d0]) ).
cnf(d11,plain,
sum(sum(f(eh),opp(X0)),opp(X1)) = sum(f(eh),sum(opp(X0),opp(X1))),
inference(resolution,[status(thm)],[d10,c2]) ).
cnf(d12,plain,
( ~ h(X1)
| ~ g(X0)
| sum(sum(f(X0),eg),X1) = sum(f(X0),sum(eg,X1)) ),
inference(resolution,[status(thm)],[d8,c10]) ).
cnf(d13,plain,
( ~ g(X0)
| sum(sum(f(X0),eg),opp(X1)) = sum(f(X0),sum(eg,opp(X1))) ),
inference(resolution,[status(thm)],[d12,d0]) ).
cnf(d14,plain,
( ~ g(X1)
| sum(sum(f(X1),eg),opp(X0)) = sum(f(X1),opp(X0)) ),
inference(demodulation,[status(thm)],[d13,d7]) ).
cnf(d15,plain,
sum(sum(f(eh),eg),opp(X0)) = sum(f(eh),opp(X0)),
inference(resolution,[status(thm)],[d14,c2]) ).
cnf(d16,plain,
sum(f(eh),opp(X0)) = sum(f(eh),opp(X0)),
inference(demodulation,[status(thm)],[d15,d6]) ).
cnf(d17,plain,
( ~ g(X0)
| sum(f(X0),opp(f(X0))) = eg ),
inference(resolution,[status(thm)],[c14,c16]) ).
cnf(d18,plain,
sum(f(eh),opp(f(eh))) = eg,
inference(resolution,[status(thm)],[d17,c2]) ).
cnf(d19,plain,
eg = sum(f(eh),opp(f(eh))),
inference(superposition,[status(thm)],[d18,d16]) ).
cnf(d20,plain,
sum(eg,opp(X0)) = sum(f(eh),sum(opp(f(eh)),opp(X0))),
inference(superposition,[status(thm)],[d19,d11]) ).
cnf(d21,plain,
opp(X0) = sum(f(eh),sum(opp(f(eh)),opp(X0))),
inference(demodulation,[status(thm)],[d20,d7]) ).
cnf(d22,plain,
( ~ h(X2)
| ~ h(X1)
| sum(sum(opp(X0),X1),X2) = sum(opp(X0),sum(X1,X2)) ),
inference(resolution,[status(thm)],[c11,d0]) ).
cnf(d23,plain,
( ~ h(X1)
| sum(sum(opp(X0),eg),X1) = sum(opp(X0),sum(eg,X1)) ),
inference(resolution,[status(thm)],[d22,c10]) ).
cnf(d24,plain,
( ~ h(X1)
| sum(opp(X0),X1) = sum(opp(X0),sum(eg,X1)) ),
inference(demodulation,[status(thm)],[d23,d1]) ).
cnf(d25,plain,
sum(opp(X0),opp(X1)) = sum(opp(X0),sum(eg,opp(X1))),
inference(resolution,[status(thm)],[d24,d0]) ).
cnf(d26,plain,
sum(opp(X1),opp(X0)) = sum(opp(X1),opp(X0)),
inference(demodulation,[status(thm)],[d25,d7]) ).
cnf(d27,plain,
sum(opp(X0),opp(opp(X0))) = eg,
inference(resolution,[status(thm)],[c14,d0]) ).
cnf(d28,plain,
eg = sum(opp(X0),opp(opp(X0))),
inference(superposition,[status(thm)],[d27,d26]) ).
cnf(d29,plain,
opp(opp(f(eh))) = sum(f(eh),eg),
inference(superposition,[status(thm)],[d28,d21]) ).
cnf(d30,plain,
opp(opp(f(eh))) = f(eh),
inference(demodulation,[status(thm)],[d29,d6]) ).
cnf(d31,plain,
( ~ h(X2)
| sum(sum(opp(X0),opp(X1)),X2) = sum(opp(X0),sum(opp(X1),X2)) ),
inference(resolution,[status(thm)],[d22,d0]) ).
cnf(d32,plain,
sum(sum(opp(X0),opp(X1)),opp(X2)) = sum(opp(X0),sum(opp(X1),opp(X2))),
inference(resolution,[status(thm)],[d31,d0]) ).
cnf(d33,plain,
sum(eg,opp(X1)) = sum(opp(X0),sum(opp(opp(X0)),opp(X1))),
inference(superposition,[status(thm)],[d28,d32]) ).
cnf(d34,plain,
opp(X0) = sum(opp(X1),sum(opp(opp(X1)),opp(X0))),
inference(demodulation,[status(thm)],[d33,d7]) ).
cnf(d35,plain,
opp(opp(f(eh))) = sum(opp(X0),sum(opp(opp(X0)),f(eh))),
inference(superposition,[status(thm)],[d30,d34]) ).
cnf(d36,plain,
f(eh) = sum(opp(X0),sum(opp(opp(X0)),f(eh))),
inference(demodulation,[status(thm)],[d35,d30]) ).
cnf(d37,plain,
f(eh) = sum(opp(f(eh)),sum(f(eh),f(eh))),
inference(superposition,[status(thm)],[d30,d36]) ).
cnf(d38,plain,
f(eh) = sum(opp(f(eh)),f(product(eh,eh))),
inference(demodulation,[status(thm)],[d37,c17]) ).
cnf(d39,plain,
f(eh) = sum(opp(f(eh)),f(eh)),
inference(demodulation,[status(thm)],[d38,d4]) ).
cnf(d40,plain,
f(eh) = eg,
inference(demodulation,[status(thm)],[d39,d3]) ).
cnf(d41,plain,
g(sK24),
inference(resolution,[status(thm)],[d40,c18]) ).
cnf(d42,plain,
product(inv(sK24),sK24) = eh,
inference(resolution,[status(thm)],[d41,c7]) ).
cnf(d43,plain,
sum(f(sK24),eg) = f(sK24),
inference(resolution,[status(thm)],[d41,d5]) ).
cnf(d44,plain,
sum(sum(f(sK24),opp(X0)),opp(X1)) = sum(f(sK24),sum(opp(X0),opp(X1))),
inference(resolution,[status(thm)],[d41,d10]) ).
cnf(d45,plain,
sum(sum(f(sK24),eg),opp(X0)) = sum(f(sK24),opp(X0)),
inference(resolution,[status(thm)],[d41,d14]) ).
cnf(d46,plain,
sum(f(sK24),opp(X0)) = sum(f(sK24),opp(X0)),
inference(demodulation,[status(thm)],[d45,d43]) ).
cnf(d47,plain,
sum(f(sK24),opp(f(sK24))) = eg,
inference(resolution,[status(thm)],[d41,d17]) ).
cnf(d48,plain,
eg = sum(f(sK24),opp(f(sK24))),
inference(superposition,[status(thm)],[d47,d46]) ).
cnf(d49,plain,
sum(eg,opp(X0)) = sum(f(sK24),sum(opp(f(sK24)),opp(X0))),
inference(superposition,[status(thm)],[d48,d44]) ).
cnf(d50,plain,
opp(X0) = sum(f(sK24),sum(opp(f(sK24)),opp(X0))),
inference(demodulation,[status(thm)],[d49,d7]) ).
cnf(d51,plain,
opp(opp(f(sK24))) = sum(f(sK24),eg),
inference(superposition,[status(thm)],[d28,d50]) ).
cnf(d52,plain,
opp(opp(f(sK24))) = f(sK24),
inference(demodulation,[status(thm)],[d51,d43]) ).
cnf(d53,plain,
opp(opp(opp(X0))) = sum(opp(X0),eg),
inference(superposition,[status(thm)],[d28,d34]) ).
cnf(d54,plain,
opp(opp(opp(X0))) = opp(X0),
inference(demodulation,[status(thm)],[d53,d1]) ).
cnf(d55,plain,
opp(X1) = sum(opp(opp(X0)),sum(opp(X0),opp(X1))),
inference(superposition,[status(thm)],[d54,d34]) ).
cnf(d56,plain,
opp(opp(f(sK24))) = sum(opp(opp(X0)),sum(opp(X0),f(sK24))),
inference(superposition,[status(thm)],[d52,d55]) ).
cnf(d57,plain,
f(sK24) = sum(opp(opp(X0)),sum(opp(X0),f(sK24))),
inference(demodulation,[status(thm)],[d56,d52]) ).
cnf(d58,plain,
sum(eg,opp(X0)) = opp(opp(opp(X0))),
inference(superposition,[status(thm)],[d54,d7]) ).
cnf(d59,plain,
opp(X0) = opp(opp(opp(X0))),
inference(demodulation,[status(thm)],[d58,d7]) ).
cnf(d60,plain,
f(sK24) = sum(opp(X0),sum(opp(opp(X0)),f(sK24))),
inference(superposition,[status(thm)],[d59,d57]) ).
cnf(d61,plain,
( ~ g(X0)
| sum(f(inv(X0)),eg) = f(inv(X0)) ),
inference(resolution,[status(thm)],[d5,c1]) ).
cnf(d62,plain,
sum(f(inv(sK24)),eg) = f(inv(sK24)),
inference(resolution,[status(thm)],[d41,d61]) ).
cnf(d63,plain,
( ~ g(X0)
| sum(sum(f(inv(X0)),opp(X1)),opp(X2)) = sum(f(inv(X0)),sum(opp(X1),opp(X2))) ),
inference(resolution,[status(thm)],[d10,c1]) ).
cnf(d64,plain,
sum(sum(f(inv(sK24)),opp(X0)),opp(X1)) = sum(f(inv(sK24)),sum(opp(X0),opp(X1))),
inference(resolution,[status(thm)],[d41,d63]) ).
cnf(d65,plain,
( ~ g(X0)
| sum(f(inv(X0)),opp(f(inv(X0)))) = eg ),
inference(resolution,[status(thm)],[d17,c1]) ).
cnf(d66,plain,
sum(f(inv(sK24)),opp(f(inv(sK24)))) = eg,
inference(resolution,[status(thm)],[d41,d65]) ).
cnf(d67,plain,
sum(eg,opp(X0)) = sum(f(inv(sK24)),sum(opp(f(inv(sK24))),opp(X0))),
inference(superposition,[status(thm)],[d66,d64]) ).
cnf(d68,plain,
opp(X0) = sum(f(inv(sK24)),sum(opp(f(inv(sK24))),opp(X0))),
inference(demodulation,[status(thm)],[d67,d7]) ).
cnf(d69,plain,
opp(opp(f(inv(sK24)))) = sum(f(inv(sK24)),eg),
inference(superposition,[status(thm)],[d28,d68]) ).
cnf(d70,plain,
opp(opp(f(inv(sK24)))) = f(inv(sK24)),
inference(demodulation,[status(thm)],[d69,d62]) ).
cnf(d71,plain,
f(sK24) = sum(opp(f(inv(sK24))),sum(f(inv(sK24)),f(sK24))),
inference(superposition,[status(thm)],[d70,d60]) ).
cnf(d72,plain,
f(sK24) = sum(opp(f(inv(sK24))),f(product(inv(sK24),sK24))),
inference(demodulation,[status(thm)],[d71,c17]) ).
cnf(d73,plain,
f(sK24) = sum(opp(f(inv(sK24))),f(eh)),
inference(demodulation,[status(thm)],[d72,d42]) ).
cnf(d74,plain,
f(sK24) = sum(opp(f(inv(sK24))),eg),
inference(demodulation,[status(thm)],[d73,d40]) ).
cnf(d75,plain,
f(sK24) = opp(f(inv(sK24))),
inference(demodulation,[status(thm)],[d74,d1]) ).
cnf(d76,plain,
opp(X1) = sum(opp(opp(opp(X0))),sum(opp(opp(X0)),opp(X1))),
inference(superposition,[status(thm)],[d54,d34]) ).
cnf(d77,plain,
opp(X1) = opp(X1),
inference(demodulation,[status(thm)],[d76,d55]) ).
cnf(d78,plain,
f(inv(sK24)) = opp(opp(f(inv(sK24)))),
inference(superposition,[status(thm)],[d70,d77]) ).
cnf(d79,plain,
f(inv(sK24)) = opp(f(sK24)),
inference(demodulation,[status(thm)],[d78,d75]) ).
cnf(d80,plain,
f(inv(sK24)) != opp(f(sK24)),
inference(resolution,[status(thm)],[d40,c19]) ).
cnf(d81,plain,
$false,
inference(resolution,[status(thm)],[d80,d79]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP776+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Fri Sep 25 15:50:59 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.95/7.59 % SZS status Theorem for theBenchmark.p
% 42.95/7.59 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------