%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GRP776+1 : TPTP v5.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 11:33:33 EST 2010
% Result : Theorem 15.21s
% Output : CNFRefutation 15.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 18
% Syntax : Number of formulae : 166 ( 19 unt; 0 def)
% Number of atoms : 389 ( 131 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 419 ( 196 ~; 195 |; 13 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 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 : 171 ( 2 sgn 73 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1,X2] : f(product(X2,X1)) = sum(f(X2),f(X1)),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos18) ).
fof(2,conjecture,
! [X3] :
( f(eh) = eg
& ( ~ g(X3)
| f(inv(X3)) = opp(f(X3)) ) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',goals) ).
fof(3,axiom,
! [X2] :
( g(X2)
=> h(f(X2)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos17) ).
fof(4,axiom,
! [X2] :
( h(X2)
=> sum(opp(X2),X2) = eg ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos16) ).
fof(5,axiom,
! [X2] :
( h(X2)
=> sum(eg,X2) = X2 ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos13) ).
fof(6,axiom,
! [X4,X1,X2] :
( ( h(X2)
& h(X1)
& h(X4) )
=> sum(sum(X2,X1),X4) = sum(X2,sum(X1,X4)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos12) ).
fof(8,axiom,
! [X1,X2] :
( h(X2)
=> h(opp(X1)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos10) ).
fof(9,axiom,
! [X2] :
( g(X2)
=> product(inv(X2),X2) = eh ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos08) ).
fof(10,axiom,
! [X1,X2] :
( ( h(X2)
& h(X1) )
=> h(sum(X2,X1)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos09) ).
fof(11,axiom,
! [X2] :
( h(X2)
=> sum(X2,opp(X2)) = eg ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos15) ).
fof(12,axiom,
! [X2] :
( h(X2)
=> sum(X2,eg) = X2 ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos14) ).
fof(13,axiom,
! [X4,X1,X2] :
( ( g(X2)
& g(X1)
& g(X4) )
=> product(product(X2,X1),X4) = product(X2,product(X1,X4)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos04) ).
fof(14,axiom,
! [X2] :
( g(X2)
=> product(eh,X2) = X2 ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos05) ).
fof(15,axiom,
! [X2] :
( g(X2)
=> product(X2,eh) = X2 ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos06) ).
fof(16,axiom,
! [X2] :
( g(X2)
=> product(X2,inv(X2)) = eh ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos07) ).
fof(17,axiom,
! [X1,X2] :
( ( g(X2)
& g(X1) )
=> g(product(X2,X1)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos01) ).
fof(18,axiom,
! [X2] :
( g(X2)
=> g(inv(X2)) ),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos02) ).
fof(19,axiom,
g(eh),
file('/tmp/tmpgOPK5H/sel_GRP776+1.p_1',sos03) ).
fof(20,negated_conjecture,
~ ! [X3] :
( f(eh) = eg
& ( ~ g(X3)
| f(inv(X3)) = opp(f(X3)) ) ),
inference(assume_negation,[status(cth)],[2]) ).
fof(21,negated_conjecture,
~ ! [X3] :
( f(eh) = eg
& ( ~ g(X3)
| f(inv(X3)) = opp(f(X3)) ) ),
inference(fof_simplification,[status(thm)],[20,theory(equality)]) ).
fof(22,plain,
! [X3,X4] : f(product(X4,X3)) = sum(f(X4),f(X3)),
inference(variable_rename,[status(thm)],[1]) ).
cnf(23,plain,
f(product(X1,X2)) = sum(f(X1),f(X2)),
inference(split_conjunct,[status(thm)],[22]) ).
fof(24,negated_conjecture,
? [X3] :
( f(eh) != eg
| ( g(X3)
& f(inv(X3)) != opp(f(X3)) ) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(25,negated_conjecture,
? [X4] :
( f(eh) != eg
| ( g(X4)
& f(inv(X4)) != opp(f(X4)) ) ),
inference(variable_rename,[status(thm)],[24]) ).
fof(26,negated_conjecture,
( f(eh) != eg
| ( g(esk1_0)
& f(inv(esk1_0)) != opp(f(esk1_0)) ) ),
inference(skolemize,[status(esa)],[25]) ).
fof(27,negated_conjecture,
( ( g(esk1_0)
| f(eh) != eg )
& ( f(inv(esk1_0)) != opp(f(esk1_0))
| f(eh) != eg ) ),
inference(distribute,[status(thm)],[26]) ).
cnf(28,negated_conjecture,
( f(eh) != eg
| f(inv(esk1_0)) != opp(f(esk1_0)) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(29,negated_conjecture,
( g(esk1_0)
| f(eh) != eg ),
inference(split_conjunct,[status(thm)],[27]) ).
fof(30,plain,
! [X2] :
( ~ g(X2)
| h(f(X2)) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(31,plain,
! [X3] :
( ~ g(X3)
| h(f(X3)) ),
inference(variable_rename,[status(thm)],[30]) ).
cnf(32,plain,
( h(f(X1))
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[31]) ).
fof(33,plain,
! [X2] :
( ~ h(X2)
| sum(opp(X2),X2) = eg ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(34,plain,
! [X3] :
( ~ h(X3)
| sum(opp(X3),X3) = eg ),
inference(variable_rename,[status(thm)],[33]) ).
cnf(35,plain,
( sum(opp(X1),X1) = eg
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[34]) ).
fof(36,plain,
! [X2] :
( ~ h(X2)
| sum(eg,X2) = X2 ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(37,plain,
! [X3] :
( ~ h(X3)
| sum(eg,X3) = X3 ),
inference(variable_rename,[status(thm)],[36]) ).
cnf(38,plain,
( sum(eg,X1) = X1
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[37]) ).
fof(39,plain,
! [X4,X1,X2] :
( ~ h(X2)
| ~ h(X1)
| ~ h(X4)
| sum(sum(X2,X1),X4) = sum(X2,sum(X1,X4)) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(40,plain,
! [X5,X6,X7] :
( ~ h(X7)
| ~ h(X6)
| ~ h(X5)
| sum(sum(X7,X6),X5) = sum(X7,sum(X6,X5)) ),
inference(variable_rename,[status(thm)],[39]) ).
cnf(41,plain,
( sum(sum(X1,X2),X3) = sum(X1,sum(X2,X3))
| ~ h(X3)
| ~ h(X2)
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[40]) ).
fof(43,plain,
! [X1,X2] :
( ~ h(X2)
| h(opp(X1)) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(44,plain,
! [X3,X4] :
( ~ h(X4)
| h(opp(X3)) ),
inference(variable_rename,[status(thm)],[43]) ).
cnf(45,plain,
( h(opp(X1))
| ~ h(X2) ),
inference(split_conjunct,[status(thm)],[44]) ).
fof(46,plain,
! [X2] :
( ~ g(X2)
| product(inv(X2),X2) = eh ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(47,plain,
! [X3] :
( ~ g(X3)
| product(inv(X3),X3) = eh ),
inference(variable_rename,[status(thm)],[46]) ).
cnf(48,plain,
( product(inv(X1),X1) = eh
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[47]) ).
fof(49,plain,
! [X1,X2] :
( ~ h(X2)
| ~ h(X1)
| h(sum(X2,X1)) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(50,plain,
! [X3,X4] :
( ~ h(X4)
| ~ h(X3)
| h(sum(X4,X3)) ),
inference(variable_rename,[status(thm)],[49]) ).
cnf(51,plain,
( h(sum(X1,X2))
| ~ h(X2)
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[50]) ).
fof(52,plain,
! [X2] :
( ~ h(X2)
| sum(X2,opp(X2)) = eg ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(53,plain,
! [X3] :
( ~ h(X3)
| sum(X3,opp(X3)) = eg ),
inference(variable_rename,[status(thm)],[52]) ).
cnf(54,plain,
( sum(X1,opp(X1)) = eg
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[53]) ).
fof(55,plain,
! [X2] :
( ~ h(X2)
| sum(X2,eg) = X2 ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(56,plain,
! [X3] :
( ~ h(X3)
| sum(X3,eg) = X3 ),
inference(variable_rename,[status(thm)],[55]) ).
cnf(57,plain,
( sum(X1,eg) = X1
| ~ h(X1) ),
inference(split_conjunct,[status(thm)],[56]) ).
fof(58,plain,
! [X4,X1,X2] :
( ~ g(X2)
| ~ g(X1)
| ~ g(X4)
| product(product(X2,X1),X4) = product(X2,product(X1,X4)) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(59,plain,
! [X5,X6,X7] :
( ~ g(X7)
| ~ g(X6)
| ~ g(X5)
| product(product(X7,X6),X5) = product(X7,product(X6,X5)) ),
inference(variable_rename,[status(thm)],[58]) ).
cnf(60,plain,
( product(product(X1,X2),X3) = product(X1,product(X2,X3))
| ~ g(X3)
| ~ g(X2)
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[59]) ).
fof(61,plain,
! [X2] :
( ~ g(X2)
| product(eh,X2) = X2 ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(62,plain,
! [X3] :
( ~ g(X3)
| product(eh,X3) = X3 ),
inference(variable_rename,[status(thm)],[61]) ).
cnf(63,plain,
( product(eh,X1) = X1
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[62]) ).
fof(64,plain,
! [X2] :
( ~ g(X2)
| product(X2,eh) = X2 ),
inference(fof_nnf,[status(thm)],[15]) ).
fof(65,plain,
! [X3] :
( ~ g(X3)
| product(X3,eh) = X3 ),
inference(variable_rename,[status(thm)],[64]) ).
cnf(66,plain,
( product(X1,eh) = X1
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[65]) ).
fof(67,plain,
! [X2] :
( ~ g(X2)
| product(X2,inv(X2)) = eh ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(68,plain,
! [X3] :
( ~ g(X3)
| product(X3,inv(X3)) = eh ),
inference(variable_rename,[status(thm)],[67]) ).
cnf(69,plain,
( product(X1,inv(X1)) = eh
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[68]) ).
fof(70,plain,
! [X1,X2] :
( ~ g(X2)
| ~ g(X1)
| g(product(X2,X1)) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(71,plain,
! [X3,X4] :
( ~ g(X4)
| ~ g(X3)
| g(product(X4,X3)) ),
inference(variable_rename,[status(thm)],[70]) ).
cnf(72,plain,
( g(product(X1,X2))
| ~ g(X2)
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[71]) ).
fof(73,plain,
! [X2] :
( ~ g(X2)
| g(inv(X2)) ),
inference(fof_nnf,[status(thm)],[18]) ).
fof(74,plain,
! [X3] :
( ~ g(X3)
| g(inv(X3)) ),
inference(variable_rename,[status(thm)],[73]) ).
cnf(75,plain,
( g(inv(X1))
| ~ g(X1) ),
inference(split_conjunct,[status(thm)],[74]) ).
cnf(76,plain,
g(eh),
inference(split_conjunct,[status(thm)],[19]) ).
cnf(93,plain,
( eh = inv(eh)
| ~ g(inv(eh))
| ~ g(eh) ),
inference(spm,[status(thm)],[63,69,theory(equality)]) ).
cnf(95,plain,
( eh = inv(eh)
| ~ g(inv(eh))
| $false ),
inference(rw,[status(thm)],[93,76,theory(equality)]) ).
cnf(96,plain,
( eh = inv(eh)
| ~ g(inv(eh)) ),
inference(cn,[status(thm)],[95,theory(equality)]) ).
cnf(113,plain,
( h(sum(f(X1),f(X2)))
| ~ g(product(X1,X2)) ),
inference(spm,[status(thm)],[32,23,theory(equality)]) ).
cnf(115,plain,
( f(X1) = sum(f(eh),f(X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[23,63,theory(equality)]) ).
cnf(116,plain,
( f(eh) = sum(f(X1),f(inv(X1)))
| ~ g(X1) ),
inference(spm,[status(thm)],[23,69,theory(equality)]) ).
cnf(122,plain,
( g(product(X1,product(X2,X3)))
| ~ g(X3)
| ~ g(product(X1,X2))
| ~ g(X2)
| ~ g(X1) ),
inference(spm,[status(thm)],[72,60,theory(equality)]) ).
cnf(125,plain,
( product(eh,X2) = product(inv(X1),product(X1,X2))
| ~ g(X2)
| ~ g(X1)
| ~ g(inv(X1)) ),
inference(spm,[status(thm)],[60,48,theory(equality)]) ).
cnf(140,plain,
( sum(X1,sum(X2,opp(sum(X1,X2)))) = eg
| ~ h(sum(X1,X2))
| ~ h(opp(sum(X1,X2)))
| ~ h(X2)
| ~ h(X1) ),
inference(spm,[status(thm)],[54,41,theory(equality)]) ).
cnf(141,plain,
( sum(eg,X2) = sum(X1,sum(opp(X1),X2))
| ~ h(X2)
| ~ h(opp(X1))
| ~ h(X1) ),
inference(spm,[status(thm)],[41,54,theory(equality)]) ).
cnf(142,plain,
( sum(eg,X2) = sum(opp(X1),sum(X1,X2))
| ~ h(X2)
| ~ h(X1)
| ~ h(opp(X1)) ),
inference(spm,[status(thm)],[41,35,theory(equality)]) ).
cnf(151,plain,
( inv(eh) = eh
| ~ g(eh) ),
inference(spm,[status(thm)],[96,75,theory(equality)]) ).
cnf(152,plain,
( inv(eh) = eh
| $false ),
inference(rw,[status(thm)],[151,76,theory(equality)]) ).
cnf(153,plain,
inv(eh) = eh,
inference(cn,[status(thm)],[152,theory(equality)]) ).
cnf(155,plain,
( product(eh,eh) = eh
| ~ g(eh) ),
inference(spm,[status(thm)],[69,153,theory(equality)]) ).
cnf(163,plain,
( product(eh,eh) = eh
| $false ),
inference(rw,[status(thm)],[155,76,theory(equality)]) ).
cnf(164,plain,
product(eh,eh) = eh,
inference(cn,[status(thm)],[163,theory(equality)]) ).
cnf(167,plain,
f(eh) = sum(f(eh),f(eh)),
inference(spm,[status(thm)],[23,164,theory(equality)]) ).
cnf(169,plain,
( product(eh,X1) = product(eh,product(eh,X1))
| ~ g(X1)
| ~ g(eh) ),
inference(spm,[status(thm)],[60,164,theory(equality)]) ).
cnf(173,plain,
( product(eh,X1) = product(eh,product(eh,X1))
| ~ g(X1)
| $false ),
inference(rw,[status(thm)],[169,76,theory(equality)]) ).
cnf(174,plain,
( product(eh,X1) = product(eh,product(eh,X1))
| ~ g(X1) ),
inference(cn,[status(thm)],[173,theory(equality)]) ).
cnf(213,plain,
( h(sum(f(eh),f(eh)))
| ~ g(eh) ),
inference(spm,[status(thm)],[113,164,theory(equality)]) ).
cnf(220,plain,
( h(f(eh))
| ~ g(eh) ),
inference(rw,[status(thm)],[213,167,theory(equality)]) ).
cnf(221,plain,
( h(f(eh))
| $false ),
inference(rw,[status(thm)],[220,76,theory(equality)]) ).
cnf(222,plain,
h(f(eh)),
inference(cn,[status(thm)],[221,theory(equality)]) ).
cnf(229,plain,
( g(product(X1,product(X2,X3)))
| ~ g(X2)
| ~ g(X1)
| ~ g(X3) ),
inference(csr,[status(thm)],[122,72]) ).
cnf(494,plain,
( g(product(eh,X1))
| ~ g(X1)
| ~ g(eh) ),
inference(spm,[status(thm)],[229,174,theory(equality)]) ).
cnf(516,plain,
( g(product(eh,X1))
| ~ g(X1)
| $false ),
inference(rw,[status(thm)],[494,76,theory(equality)]) ).
cnf(517,plain,
( g(product(eh,X1))
| ~ g(X1) ),
inference(cn,[status(thm)],[516,theory(equality)]) ).
cnf(1475,plain,
( product(inv(X1),product(X1,X2)) = product(eh,X2)
| ~ g(X2)
| ~ g(X1) ),
inference(csr,[status(thm)],[125,75]) ).
cnf(1483,plain,
( product(inv(inv(X1)),eh) = product(eh,X1)
| ~ g(X1)
| ~ g(inv(X1)) ),
inference(spm,[status(thm)],[1475,48,theory(equality)]) ).
cnf(2730,plain,
( sum(X1,sum(X2,opp(sum(X1,X2)))) = eg
| ~ h(sum(X1,X2))
| ~ h(X2)
| ~ h(X1) ),
inference(csr,[status(thm)],[140,45]) ).
cnf(2731,plain,
( sum(X1,sum(X2,opp(sum(X1,X2)))) = eg
| ~ h(X2)
| ~ h(X1) ),
inference(csr,[status(thm)],[2730,51]) ).
cnf(2732,plain,
( sum(f(eh),sum(f(eh),opp(f(eh)))) = eg
| ~ h(f(eh)) ),
inference(spm,[status(thm)],[2731,167,theory(equality)]) ).
cnf(2776,plain,
( sum(f(eh),sum(f(eh),opp(f(eh)))) = eg
| $false ),
inference(rw,[status(thm)],[2732,222,theory(equality)]) ).
cnf(2777,plain,
sum(f(eh),sum(f(eh),opp(f(eh)))) = eg,
inference(cn,[status(thm)],[2776,theory(equality)]) ).
cnf(3022,plain,
( sum(X1,sum(opp(X1),X2)) = sum(eg,X2)
| ~ h(X1)
| ~ h(X2) ),
inference(csr,[status(thm)],[141,45]) ).
cnf(3026,plain,
( sum(X1,eg) = sum(eg,opp(opp(X1)))
| ~ h(opp(opp(X1)))
| ~ h(X1)
| ~ h(opp(X1)) ),
inference(spm,[status(thm)],[3022,54,theory(equality)]) ).
cnf(3091,plain,
( sum(f(eh),eg) = eg
| ~ h(f(eh)) ),
inference(spm,[status(thm)],[2777,54,theory(equality)]) ).
cnf(3100,plain,
( sum(f(eh),eg) = eg
| $false ),
inference(rw,[status(thm)],[3091,222,theory(equality)]) ).
cnf(3101,plain,
sum(f(eh),eg) = eg,
inference(cn,[status(thm)],[3100,theory(equality)]) ).
cnf(3114,plain,
( eg = f(eh)
| ~ h(f(eh)) ),
inference(spm,[status(thm)],[57,3101,theory(equality)]) ).
cnf(3125,plain,
( eg = f(eh)
| $false ),
inference(rw,[status(thm)],[3114,222,theory(equality)]) ).
cnf(3126,plain,
eg = f(eh),
inference(cn,[status(thm)],[3125,theory(equality)]) ).
cnf(3183,plain,
( sum(f(X1),f(inv(X1))) = eg
| ~ g(X1) ),
inference(rw,[status(thm)],[116,3126,theory(equality)]) ).
cnf(3184,plain,
( sum(eg,f(X1)) = f(X1)
| ~ g(X1) ),
inference(rw,[status(thm)],[115,3126,theory(equality)]) ).
cnf(3188,negated_conjecture,
( g(esk1_0)
| $false ),
inference(rw,[status(thm)],[29,3126,theory(equality)]) ).
cnf(3189,negated_conjecture,
g(esk1_0),
inference(cn,[status(thm)],[3188,theory(equality)]) ).
cnf(3190,negated_conjecture,
( opp(f(esk1_0)) != f(inv(esk1_0))
| $false ),
inference(rw,[status(thm)],[28,3126,theory(equality)]) ).
cnf(3191,negated_conjecture,
opp(f(esk1_0)) != f(inv(esk1_0)),
inference(cn,[status(thm)],[3190,theory(equality)]) ).
cnf(3278,plain,
( sum(opp(X1),sum(X1,X2)) = sum(eg,X2)
| ~ h(X2)
| ~ h(X1) ),
inference(csr,[status(thm)],[142,45]) ).
cnf(3285,plain,
( sum(opp(opp(X1)),eg) = sum(eg,X1)
| ~ h(X1)
| ~ h(opp(X1)) ),
inference(spm,[status(thm)],[3278,35,theory(equality)]) ).
cnf(3869,plain,
( sum(opp(f(X1)),eg) = sum(eg,f(inv(X1)))
| ~ h(f(inv(X1)))
| ~ h(f(X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[3278,3183,theory(equality)]) ).
cnf(17912,plain,
( product(inv(inv(X1)),eh) = product(eh,X1)
| ~ g(X1) ),
inference(csr,[status(thm)],[1483,75]) ).
cnf(17915,plain,
( product(eh,X1) = inv(inv(X1))
| ~ g(inv(inv(X1)))
| ~ g(X1) ),
inference(spm,[status(thm)],[66,17912,theory(equality)]) ).
cnf(18605,plain,
( inv(inv(X1)) = product(eh,X1)
| ~ g(X1)
| ~ g(inv(X1)) ),
inference(spm,[status(thm)],[17915,75,theory(equality)]) ).
cnf(18611,plain,
( inv(inv(X1)) = product(eh,X1)
| ~ g(X1) ),
inference(csr,[status(thm)],[18605,75]) ).
cnf(18638,plain,
( inv(product(eh,X1)) = product(eh,inv(X1))
| ~ g(inv(X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[18611,18611,theory(equality)]) ).
cnf(18715,plain,
( inv(product(eh,X1)) = product(eh,inv(X1))
| ~ g(X1) ),
inference(csr,[status(thm)],[18638,75]) ).
cnf(18717,plain,
( g(product(eh,inv(X1)))
| ~ g(product(eh,X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[75,18715,theory(equality)]) ).
cnf(18719,plain,
( inv(X1) = product(eh,inv(X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[18715,63,theory(equality)]) ).
cnf(18888,plain,
( g(product(eh,inv(X1)))
| ~ g(X1) ),
inference(csr,[status(thm)],[18717,517]) ).
cnf(18894,plain,
( h(sum(f(eh),f(inv(X1))))
| ~ g(X1) ),
inference(spm,[status(thm)],[113,18888,theory(equality)]) ).
cnf(18920,plain,
( h(sum(eg,f(inv(X1))))
| ~ g(X1) ),
inference(rw,[status(thm)],[18894,3126,theory(equality)]) ).
cnf(18931,plain,
( f(inv(X1)) = sum(f(eh),f(inv(X1)))
| ~ g(X1) ),
inference(spm,[status(thm)],[23,18719,theory(equality)]) ).
cnf(18990,plain,
( f(inv(X1)) = sum(eg,f(inv(X1)))
| ~ g(X1) ),
inference(rw,[status(thm)],[18931,3126,theory(equality)]) ).
cnf(19057,plain,
( h(f(inv(X1)))
| ~ g(X1)
| ~ g(inv(X1)) ),
inference(spm,[status(thm)],[18920,3184,theory(equality)]) ).
cnf(19073,plain,
( h(f(inv(X1)))
| ~ g(X1) ),
inference(csr,[status(thm)],[19057,75]) ).
cnf(22777,plain,
( sum(opp(opp(X1)),eg) = sum(eg,X1)
| ~ h(X1) ),
inference(csr,[status(thm)],[3285,45]) ).
cnf(22778,plain,
( sum(eg,X1) = opp(opp(X1))
| ~ h(opp(opp(X1)))
| ~ h(X1) ),
inference(spm,[status(thm)],[57,22777,theory(equality)]) ).
cnf(23386,plain,
( opp(opp(X1)) = sum(eg,X1)
| ~ h(X1) ),
inference(csr,[status(thm)],[22778,45]) ).
cnf(23420,plain,
( opp(sum(eg,X1)) = sum(eg,opp(X1))
| ~ h(opp(X1))
| ~ h(X1) ),
inference(spm,[status(thm)],[23386,23386,theory(equality)]) ).
cnf(24390,plain,
( opp(sum(eg,X1)) = sum(eg,opp(X1))
| ~ h(X1) ),
inference(csr,[status(thm)],[23420,45]) ).
cnf(24394,plain,
( opp(X1) = sum(eg,opp(X1))
| ~ h(X1) ),
inference(spm,[status(thm)],[24390,38,theory(equality)]) ).
cnf(255037,plain,
( sum(eg,opp(opp(X1))) = sum(X1,eg)
| ~ h(opp(opp(X1)))
| ~ h(X1) ),
inference(csr,[status(thm)],[3026,45]) ).
cnf(255038,plain,
( sum(eg,opp(opp(X1))) = sum(X1,eg)
| ~ h(X1) ),
inference(csr,[status(thm)],[255037,45]) ).
cnf(255064,plain,
( sum(X1,eg) = opp(opp(X1))
| ~ h(opp(X1))
| ~ h(X1) ),
inference(spm,[status(thm)],[24394,255038,theory(equality)]) ).
cnf(255185,plain,
( opp(opp(X1)) = sum(X1,eg)
| ~ h(X1) ),
inference(csr,[status(thm)],[255064,45]) ).
cnf(255201,plain,
( opp(sum(eg,X1)) = sum(opp(X1),eg)
| ~ h(opp(X1))
| ~ h(X1) ),
inference(spm,[status(thm)],[255185,23386,theory(equality)]) ).
cnf(257616,plain,
( opp(sum(eg,X1)) = sum(opp(X1),eg)
| ~ h(X1) ),
inference(csr,[status(thm)],[255201,45]) ).
cnf(257619,plain,
( opp(X1) = sum(opp(X1),eg)
| ~ h(X1) ),
inference(spm,[status(thm)],[257616,38,theory(equality)]) ).
cnf(448116,plain,
( sum(opp(f(X1)),eg) = sum(eg,f(inv(X1)))
| ~ h(f(inv(X1)))
| ~ g(X1) ),
inference(csr,[status(thm)],[3869,32]) ).
cnf(448117,plain,
( sum(opp(f(X1)),eg) = sum(eg,f(inv(X1)))
| ~ g(X1) ),
inference(csr,[status(thm)],[448116,19073]) ).
cnf(448210,plain,
( sum(eg,f(inv(X1))) = opp(f(X1))
| ~ h(f(X1))
| ~ g(X1) ),
inference(spm,[status(thm)],[257619,448117,theory(equality)]) ).
cnf(449767,plain,
( opp(f(X1)) = sum(eg,f(inv(X1)))
| ~ g(X1) ),
inference(csr,[status(thm)],[448210,32]) ).
cnf(449770,negated_conjecture,
( sum(eg,f(inv(esk1_0))) != f(inv(esk1_0))
| ~ g(esk1_0) ),
inference(spm,[status(thm)],[3191,449767,theory(equality)]) ).
cnf(449885,negated_conjecture,
( sum(eg,f(inv(esk1_0))) != f(inv(esk1_0))
| $false ),
inference(rw,[status(thm)],[449770,3189,theory(equality)]) ).
cnf(449886,negated_conjecture,
sum(eg,f(inv(esk1_0))) != f(inv(esk1_0)),
inference(cn,[status(thm)],[449885,theory(equality)]) ).
cnf(450044,negated_conjecture,
~ g(esk1_0),
inference(spm,[status(thm)],[449886,18990,theory(equality)]) ).
cnf(450045,negated_conjecture,
$false,
inference(rw,[status(thm)],[450044,3189,theory(equality)]) ).
cnf(450046,negated_conjecture,
$false,
inference(cn,[status(thm)],[450045,theory(equality)]) ).
cnf(450047,negated_conjecture,
$false,
450046,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GRP/GRP776+1.p
% --creating new selector for []
% -running prover on /tmp/tmpgOPK5H/sel_GRP776+1.p_1 with time limit 29
% -prover status Theorem
% Problem GRP776+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GRP/GRP776+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GRP/GRP776+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------