%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR116+7 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art09.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 08:02:36 EST 2010
% Result : Theorem 1.44s
% Output : CNFRefutation 1.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 6
% Syntax : Number of formulae : 58 ( 21 unt; 0 def)
% Number of atoms : 485 ( 0 equ)
% Maximal formula atoms : 165 ( 8 avg)
% Number of connectives : 668 ( 241 ~; 229 |; 194 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 165 ( 10 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 5 prp; 0-3 aty)
% Number of functors : 46 ( 46 usr; 46 con; 0-0 aty)
% Number of variables : 114 ( 4 sgn 30 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(75,axiom,
( attr(c12,c13)
& attr(c12,c14)
& sub(c12,mensch_1_1)
& sub(c13,eigenname_1_1)
& val(c13,nelson_0)
& sub(c14,familiename_1_1)
& val(c14,mandela_0)
& prop(c18,neugew__344hlt_1_1)
& sub(c18,abgeordneten_haus_1_2)
& prop(c25,schwarz_1_1)
& sub(c25,c27)
& pmod(c27,erst_1_1,pr__344sident_1_1)
& attch(c33,c25)
& sub(c33,land_1_1)
& agt(c38,c18)
& obj(c38,c12)
& rslt(c38,c47)
& subs(c38,w__344hlen_1_2)
& temp(c38,c5)
& arg1(c47,c12)
& arg2(c47,c25)
& subr(c47,rprs_0)
& sub(c5,montag__1_1)
& sort(c12,d)
& card(c12,int1)
& etype(c12,int0)
& fact(c12,real)
& gener(c12,sp)
& quant(c12,one)
& refer(c12,det)
& varia(c12,con)
& sort(c13,na)
& card(c13,int1)
& etype(c13,int0)
& fact(c13,real)
& gener(c13,sp)
& quant(c13,one)
& refer(c13,indet)
& varia(c13,varia_c)
& sort(c14,na)
& card(c14,int1)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& quant(c14,one)
& refer(c14,indet)
& varia(c14,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c18,d)
& sort(c18,io)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& sort(neugew__344hlt_1_1,gq)
& sort(abgeordneten_haus_1_2,d)
& sort(abgeordneten_haus_1_2,io)
& card(abgeordneten_haus_1_2,int1)
& etype(abgeordneten_haus_1_2,int0)
& fact(abgeordneten_haus_1_2,real)
& gener(abgeordneten_haus_1_2,ge)
& quant(abgeordneten_haus_1_2,one)
& refer(abgeordneten_haus_1_2,refer_c)
& varia(abgeordneten_haus_1_2,varia_c)
& sort(c25,d)
& card(c25,int1)
& etype(c25,int0)
& fact(c25,real)
& gener(c25,sp)
& quant(c25,one)
& refer(c25,det)
& varia(c25,con)
& sort(schwarz_1_1,tq)
& sort(c27,d)
& card(c27,int1)
& etype(c27,int0)
& fact(c27,real)
& gener(c27,ge)
& quant(c27,one)
& refer(c27,refer_c)
& varia(c27,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(c33,d)
& sort(c33,io)
& card(c33,int1)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& quant(c33,one)
& refer(c33,det)
& varia(c33,con)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(c38,da)
& fact(c38,real)
& gener(c38,sp)
& sort(c47,st)
& fact(c47,real)
& gener(c47,sp)
& sort(w__344hlen_1_2,da)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& sort(c5,ta)
& card(c5,int1)
& etype(c5,int0)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& sort(rprs_0,st)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& sort(montag__1_1,ta)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c) ),
file('/tmp/tmpmUv40f/sel_CSR116+7.p_1',ave07_era5_synth_qa07_010_mira_news_1614) ).
fof(76,conjecture,
? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( pmod(X9,erst_1_1,pr__344sident_1_1)
& arg1(X4,X1)
& arg2(X4,X5)
& attr(X1,X2)
& attr(X1,X3)
& attr(X6,X7)
& obj(X8,X1)
& prop(X5,schwarz_1_1)
& rslt(X8,X4)
& sub(X2,familiename_1_1)
& sub(X3,eigenname_1_1)
& sub(X5,X9)
& subr(X4,rprs_0)
& subs(X8,w__344hlen_1_2)
& val(X2,mandela_0)
& val(X3,nelson_0) ),
file('/tmp/tmpmUv40f/sel_CSR116+7.p_1',synth_qa07_010_mira_news_1614) ).
fof(77,negated_conjecture,
~ ? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( pmod(X9,erst_1_1,pr__344sident_1_1)
& arg1(X4,X1)
& arg2(X4,X5)
& attr(X1,X2)
& attr(X1,X3)
& attr(X6,X7)
& obj(X8,X1)
& prop(X5,schwarz_1_1)
& rslt(X8,X4)
& sub(X2,familiename_1_1)
& sub(X3,eigenname_1_1)
& sub(X5,X9)
& subr(X4,rprs_0)
& subs(X8,w__344hlen_1_2)
& val(X2,mandela_0)
& val(X3,nelson_0) ),
inference(assume_negation,[status(cth)],[76]) ).
cnf(431,plain,
subr(c47,rprs_0),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(432,plain,
arg2(c47,c25),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(433,plain,
arg1(c47,c12),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(435,plain,
subs(c38,w__344hlen_1_2),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(436,plain,
rslt(c38,c47),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(437,plain,
obj(c38,c12),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(441,plain,
pmod(c27,erst_1_1,pr__344sident_1_1),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(442,plain,
sub(c25,c27),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(443,plain,
prop(c25,schwarz_1_1),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(446,plain,
val(c14,mandela_0),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(447,plain,
sub(c14,familiename_1_1),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(448,plain,
val(c13,nelson_0),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(449,plain,
sub(c13,eigenname_1_1),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(451,plain,
attr(c12,c14),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(452,plain,
attr(c12,c13),
inference(split_conjunct,[status(thm)],[75]) ).
fof(453,negated_conjecture,
! [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ pmod(X9,erst_1_1,pr__344sident_1_1)
| ~ arg1(X4,X1)
| ~ arg2(X4,X5)
| ~ attr(X1,X2)
| ~ attr(X1,X3)
| ~ attr(X6,X7)
| ~ obj(X8,X1)
| ~ prop(X5,schwarz_1_1)
| ~ rslt(X8,X4)
| ~ sub(X2,familiename_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X5,X9)
| ~ subr(X4,rprs_0)
| ~ subs(X8,w__344hlen_1_2)
| ~ val(X2,mandela_0)
| ~ val(X3,nelson_0) ),
inference(fof_nnf,[status(thm)],[77]) ).
fof(454,negated_conjecture,
! [X10,X11,X12,X13,X14,X15,X16,X17,X18] :
( ~ pmod(X18,erst_1_1,pr__344sident_1_1)
| ~ arg1(X13,X10)
| ~ arg2(X13,X14)
| ~ attr(X10,X11)
| ~ attr(X10,X12)
| ~ attr(X15,X16)
| ~ obj(X17,X10)
| ~ prop(X14,schwarz_1_1)
| ~ rslt(X17,X13)
| ~ sub(X11,familiename_1_1)
| ~ sub(X12,eigenname_1_1)
| ~ sub(X14,X18)
| ~ subr(X13,rprs_0)
| ~ subs(X17,w__344hlen_1_2)
| ~ val(X11,mandela_0)
| ~ val(X12,nelson_0) ),
inference(variable_rename,[status(thm)],[453]) ).
cnf(455,negated_conjecture,
( ~ val(X1,nelson_0)
| ~ val(X2,mandela_0)
| ~ subs(X3,w__344hlen_1_2)
| ~ subr(X4,rprs_0)
| ~ sub(X5,X6)
| ~ sub(X1,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ rslt(X3,X4)
| ~ prop(X5,schwarz_1_1)
| ~ obj(X3,X7)
| ~ attr(X8,X9)
| ~ attr(X7,X1)
| ~ attr(X7,X2)
| ~ arg2(X4,X5)
| ~ arg1(X4,X7)
| ~ pmod(X6,erst_1_1,pr__344sident_1_1) ),
inference(split_conjunct,[status(thm)],[454]) ).
fof(588,plain,
( ~ epred1_0
<=> ! [X4,X3,X2,X7,X1,X5,X6] :
( ~ subs(X3,w__344hlen_1_2)
| ~ arg1(X4,X7)
| ~ arg2(X4,X5)
| ~ obj(X3,X7)
| ~ subr(X4,rprs_0)
| ~ rslt(X3,X4)
| ~ sub(X5,X6)
| ~ sub(X1,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ attr(X7,X1)
| ~ attr(X7,X2)
| ~ val(X1,nelson_0)
| ~ val(X2,mandela_0)
| ~ prop(X5,schwarz_1_1)
| ~ pmod(X6,erst_1_1,pr__344sident_1_1) ) ),
introduced(definition),
[split] ).
cnf(589,plain,
( epred1_0
| ~ subs(X3,w__344hlen_1_2)
| ~ arg1(X4,X7)
| ~ arg2(X4,X5)
| ~ obj(X3,X7)
| ~ subr(X4,rprs_0)
| ~ rslt(X3,X4)
| ~ sub(X5,X6)
| ~ sub(X1,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ attr(X7,X1)
| ~ attr(X7,X2)
| ~ val(X1,nelson_0)
| ~ val(X2,mandela_0)
| ~ prop(X5,schwarz_1_1)
| ~ pmod(X6,erst_1_1,pr__344sident_1_1) ),
inference(split_equiv,[status(thm)],[588]) ).
fof(590,plain,
( ~ epred2_0
<=> ! [X9,X8] : ~ attr(X8,X9) ),
introduced(definition),
[split] ).
cnf(591,plain,
( epred2_0
| ~ attr(X8,X9) ),
inference(split_equiv,[status(thm)],[590]) ).
cnf(592,negated_conjecture,
( ~ epred2_0
| ~ epred1_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[455,588,theory(equality)]),590,theory(equality)]),
[split] ).
cnf(594,plain,
epred2_0,
inference(spm,[status(thm)],[591,452,theory(equality)]) ).
cnf(598,negated_conjecture,
( $false
| ~ epred1_0 ),
inference(rw,[status(thm)],[592,594,theory(equality)]) ).
cnf(599,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[598,theory(equality)]) ).
cnf(600,negated_conjecture,
( ~ subs(X3,w__344hlen_1_2)
| ~ arg1(X4,X7)
| ~ arg2(X4,X5)
| ~ obj(X3,X7)
| ~ subr(X4,rprs_0)
| ~ rslt(X3,X4)
| ~ sub(X5,X6)
| ~ sub(X1,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ attr(X7,X1)
| ~ attr(X7,X2)
| ~ val(X1,nelson_0)
| ~ val(X2,mandela_0)
| ~ prop(X5,schwarz_1_1)
| ~ pmod(X6,erst_1_1,pr__344sident_1_1) ),
inference(sr,[status(thm)],[589,599,theory(equality)]) ).
cnf(601,plain,
( ~ prop(X1,schwarz_1_1)
| ~ val(X2,nelson_0)
| ~ val(X3,mandela_0)
| ~ attr(X4,X2)
| ~ attr(X4,X3)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ sub(X1,c27)
| ~ rslt(X5,X6)
| ~ subr(X6,rprs_0)
| ~ obj(X5,X4)
| ~ arg2(X6,X1)
| ~ arg1(X6,X4)
| ~ subs(X5,w__344hlen_1_2) ),
inference(spm,[status(thm)],[600,441,theory(equality)]) ).
cnf(602,plain,
( ~ prop(X1,schwarz_1_1)
| ~ val(X2,mandela_0)
| ~ attr(X3,c13)
| ~ attr(X3,X2)
| ~ sub(c13,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ sub(X1,c27)
| ~ rslt(X4,X5)
| ~ subr(X5,rprs_0)
| ~ obj(X4,X3)
| ~ arg2(X5,X1)
| ~ arg1(X5,X3)
| ~ subs(X4,w__344hlen_1_2) ),
inference(spm,[status(thm)],[601,448,theory(equality)]) ).
cnf(604,plain,
( ~ prop(X1,schwarz_1_1)
| ~ val(X2,mandela_0)
| ~ attr(X3,c13)
| ~ attr(X3,X2)
| $false
| ~ sub(X2,familiename_1_1)
| ~ sub(X1,c27)
| ~ rslt(X4,X5)
| ~ subr(X5,rprs_0)
| ~ obj(X4,X3)
| ~ arg2(X5,X1)
| ~ arg1(X5,X3)
| ~ subs(X4,w__344hlen_1_2) ),
inference(rw,[status(thm)],[602,449,theory(equality)]) ).
cnf(605,plain,
( ~ prop(X1,schwarz_1_1)
| ~ val(X2,mandela_0)
| ~ attr(X3,c13)
| ~ attr(X3,X2)
| ~ sub(X2,familiename_1_1)
| ~ sub(X1,c27)
| ~ rslt(X4,X5)
| ~ subr(X5,rprs_0)
| ~ obj(X4,X3)
| ~ arg2(X5,X1)
| ~ arg1(X5,X3)
| ~ subs(X4,w__344hlen_1_2) ),
inference(cn,[status(thm)],[604,theory(equality)]) ).
cnf(614,plain,
( ~ prop(X1,schwarz_1_1)
| ~ attr(X2,c13)
| ~ attr(X2,c14)
| ~ sub(c14,familiename_1_1)
| ~ sub(X1,c27)
| ~ rslt(X3,X4)
| ~ subr(X4,rprs_0)
| ~ obj(X3,X2)
| ~ arg2(X4,X1)
| ~ arg1(X4,X2)
| ~ subs(X3,w__344hlen_1_2) ),
inference(spm,[status(thm)],[605,446,theory(equality)]) ).
cnf(616,plain,
( ~ prop(X1,schwarz_1_1)
| ~ attr(X2,c13)
| ~ attr(X2,c14)
| $false
| ~ sub(X1,c27)
| ~ rslt(X3,X4)
| ~ subr(X4,rprs_0)
| ~ obj(X3,X2)
| ~ arg2(X4,X1)
| ~ arg1(X4,X2)
| ~ subs(X3,w__344hlen_1_2) ),
inference(rw,[status(thm)],[614,447,theory(equality)]) ).
cnf(617,plain,
( ~ prop(X1,schwarz_1_1)
| ~ attr(X2,c13)
| ~ attr(X2,c14)
| ~ sub(X1,c27)
| ~ rslt(X3,X4)
| ~ subr(X4,rprs_0)
| ~ obj(X3,X2)
| ~ arg2(X4,X1)
| ~ arg1(X4,X2)
| ~ subs(X3,w__344hlen_1_2) ),
inference(cn,[status(thm)],[616,theory(equality)]) ).
cnf(618,plain,
( ~ prop(X1,schwarz_1_1)
| ~ attr(X2,c13)
| ~ attr(X2,c14)
| ~ sub(X1,c27)
| ~ rslt(X3,c47)
| ~ obj(X3,X2)
| ~ arg2(c47,X1)
| ~ arg1(c47,X2)
| ~ subs(X3,w__344hlen_1_2) ),
inference(spm,[status(thm)],[617,431,theory(equality)]) ).
fof(620,plain,
( ~ epred3_0
<=> ! [X1] :
( ~ arg2(c47,X1)
| ~ sub(X1,c27)
| ~ prop(X1,schwarz_1_1) ) ),
introduced(definition),
[split] ).
cnf(621,plain,
( epred3_0
| ~ arg2(c47,X1)
| ~ sub(X1,c27)
| ~ prop(X1,schwarz_1_1) ),
inference(split_equiv,[status(thm)],[620]) ).
fof(622,plain,
( ~ epred4_0
<=> ! [X3,X2] :
( ~ subs(X3,w__344hlen_1_2)
| ~ arg1(c47,X2)
| ~ obj(X3,X2)
| ~ rslt(X3,c47)
| ~ attr(X2,c14)
| ~ attr(X2,c13) ) ),
introduced(definition),
[split] ).
cnf(623,plain,
( epred4_0
| ~ subs(X3,w__344hlen_1_2)
| ~ arg1(c47,X2)
| ~ obj(X3,X2)
| ~ rslt(X3,c47)
| ~ attr(X2,c14)
| ~ attr(X2,c13) ),
inference(split_equiv,[status(thm)],[622]) ).
cnf(624,plain,
( ~ epred4_0
| ~ epred3_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[618,620,theory(equality)]),622,theory(equality)]),
[split] ).
cnf(628,plain,
( epred3_0
| ~ prop(c25,schwarz_1_1)
| ~ sub(c25,c27) ),
inference(spm,[status(thm)],[621,432,theory(equality)]) ).
cnf(629,plain,
( epred3_0
| $false
| ~ sub(c25,c27) ),
inference(rw,[status(thm)],[628,443,theory(equality)]) ).
cnf(630,plain,
( epred3_0
| $false
| $false ),
inference(rw,[status(thm)],[629,442,theory(equality)]) ).
cnf(631,plain,
epred3_0,
inference(cn,[status(thm)],[630,theory(equality)]) ).
cnf(633,plain,
( ~ epred4_0
| $false ),
inference(rw,[status(thm)],[624,631,theory(equality)]) ).
cnf(634,plain,
~ epred4_0,
inference(cn,[status(thm)],[633,theory(equality)]) ).
cnf(635,plain,
( ~ subs(X3,w__344hlen_1_2)
| ~ arg1(c47,X2)
| ~ obj(X3,X2)
| ~ rslt(X3,c47)
| ~ attr(X2,c14)
| ~ attr(X2,c13) ),
inference(sr,[status(thm)],[623,634,theory(equality)]) ).
cnf(636,plain,
( ~ attr(c12,c14)
| ~ attr(c12,c13)
| ~ rslt(c38,c47)
| ~ arg1(c47,c12)
| ~ subs(c38,w__344hlen_1_2) ),
inference(spm,[status(thm)],[635,437,theory(equality)]) ).
cnf(638,plain,
( $false
| ~ attr(c12,c13)
| ~ rslt(c38,c47)
| ~ arg1(c47,c12)
| ~ subs(c38,w__344hlen_1_2) ),
inference(rw,[status(thm)],[636,451,theory(equality)]) ).
cnf(639,plain,
( $false
| $false
| ~ rslt(c38,c47)
| ~ arg1(c47,c12)
| ~ subs(c38,w__344hlen_1_2) ),
inference(rw,[status(thm)],[638,452,theory(equality)]) ).
cnf(640,plain,
( $false
| $false
| $false
| ~ arg1(c47,c12)
| ~ subs(c38,w__344hlen_1_2) ),
inference(rw,[status(thm)],[639,436,theory(equality)]) ).
cnf(641,plain,
( $false
| $false
| $false
| $false
| ~ subs(c38,w__344hlen_1_2) ),
inference(rw,[status(thm)],[640,433,theory(equality)]) ).
cnf(642,plain,
( $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[641,435,theory(equality)]) ).
cnf(643,plain,
$false,
inference(cn,[status(thm)],[642,theory(equality)]) ).
cnf(644,plain,
$false,
643,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR116+7.p
% --creating new selector for [CSR004+0.ax]
% -running prover on /tmp/tmpmUv40f/sel_CSR116+7.p_1 with time limit 29
% -prover status Theorem
% Problem CSR116+7.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR116+7.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR116+7.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
%
%------------------------------------------------------------------------------