%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR115+82 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art04.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 07:52:43 EST 2010
% Result : Theorem 1.40s
% Output : CNFRefutation 1.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 35 ( 8 unt; 0 def)
% Number of atoms : 196 ( 0 equ)
% Maximal formula atoms : 101 ( 5 avg)
% Number of connectives : 215 ( 54 ~; 39 |; 118 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 4 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 33 con; 0-2 aty)
% Number of variables : 69 ( 12 sgn 28 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(42,axiom,
! [X1,X2] :
( name(X2,X1)
=> ? [X3] :
( attr(X2,X3)
& sub(X3,name_1_1)
& val(X3,X1) ) ),
file('/tmp/tmpF_oMRz/sel_CSR115+82.p_1',name_rel__attr_val_name_1_1) ).
fof(57,axiom,
( attr(c341,c342)
& sub(c341,mensch_1_1)
& sub(c342,familiename_1_1)
& val(c342,marzocchi_0)
& name(c358,freeride_____344ra_0)
& sub(c362,mountain_bike_1_1)
& sub(c364,bereich_1_1)
& benf(c368,c364)
& exp(c368,c341)
& loc(c368,c373)
& mcont(c368,c358)
& subs(c368,einl__344uten_1_1)
& in(c373,c362)
& sort(c341,d)
& card(c341,int1)
& etype(c341,int0)
& fact(c341,real)
& gener(c341,sp)
& quant(c341,one)
& refer(c341,det)
& varia(c341,con)
& sort(c342,na)
& card(c342,int1)
& etype(c342,int0)
& fact(c342,real)
& gener(c342,sp)
& quant(c342,one)
& refer(c342,indet)
& varia(c342,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(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(marzocchi_0,fe)
& sort(c358,o)
& card(c358,int1)
& etype(c358,int0)
& fact(c358,hypo)
& gener(c358,sp)
& quant(c358,one)
& refer(c358,refer_c)
& varia(c358,varia_c)
& sort(freeride_____344ra_0,fe)
& sort(c362,d)
& card(c362,int1)
& etype(c362,int0)
& fact(c362,real)
& gener(c362,sp)
& quant(c362,one)
& refer(c362,det)
& varia(c362,con)
& sort(mountain_bike_1_1,d)
& card(mountain_bike_1_1,int1)
& etype(mountain_bike_1_1,int0)
& fact(mountain_bike_1_1,real)
& gener(mountain_bike_1_1,ge)
& quant(mountain_bike_1_1,one)
& refer(mountain_bike_1_1,refer_c)
& varia(mountain_bike_1_1,varia_c)
& sort(c364,d)
& card(c364,int1)
& etype(c364,int0)
& fact(c364,real)
& gener(c364,sp)
& quant(c364,one)
& refer(c364,refer_c)
& varia(c364,varia_c)
& sort(bereich_1_1,d)
& card(bereich_1_1,int1)
& etype(bereich_1_1,int0)
& fact(bereich_1_1,real)
& gener(bereich_1_1,ge)
& quant(bereich_1_1,one)
& refer(bereich_1_1,refer_c)
& varia(bereich_1_1,varia_c)
& sort(c368,dn)
& fact(c368,real)
& gener(c368,sp)
& sort(c373,l)
& card(c373,int1)
& etype(c373,int0)
& fact(c373,real)
& gener(c373,sp)
& quant(c373,one)
& refer(c373,det)
& varia(c373,con)
& sort(einl__344uten_1_1,dn)
& fact(einl__344uten_1_1,real)
& gener(einl__344uten_1_1,ge) ),
file('/tmp/tmpF_oMRz/sel_CSR115+82.p_1',ave07_era5_synth_qa07_007_mira_wp_495) ).
fof(58,conjecture,
? [X1,X2,X3,X4,X5,X6] :
( attr(X1,X2)
& attr(X4,X3)
& attr(X5,X6)
& sub(X2,name_1_1)
& sub(X3,name_1_1) ),
file('/tmp/tmpF_oMRz/sel_CSR115+82.p_1',synth_qa07_007_mira_wp_495) ).
fof(59,negated_conjecture,
~ ? [X1,X2,X3,X4,X5,X6] :
( attr(X1,X2)
& attr(X4,X3)
& attr(X5,X6)
& sub(X2,name_1_1)
& sub(X3,name_1_1) ),
inference(assume_negation,[status(cth)],[58]) ).
fof(170,plain,
! [X1,X2] :
( ~ name(X2,X1)
| ? [X3] :
( attr(X2,X3)
& sub(X3,name_1_1)
& val(X3,X1) ) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(171,plain,
! [X4,X5] :
( ~ name(X5,X4)
| ? [X6] :
( attr(X5,X6)
& sub(X6,name_1_1)
& val(X6,X4) ) ),
inference(variable_rename,[status(thm)],[170]) ).
fof(172,plain,
! [X4,X5] :
( ~ name(X5,X4)
| ( attr(X5,esk7_2(X4,X5))
& sub(esk7_2(X4,X5),name_1_1)
& val(esk7_2(X4,X5),X4) ) ),
inference(skolemize,[status(esa)],[171]) ).
fof(173,plain,
! [X4,X5] :
( ( attr(X5,esk7_2(X4,X5))
| ~ name(X5,X4) )
& ( sub(esk7_2(X4,X5),name_1_1)
| ~ name(X5,X4) )
& ( val(esk7_2(X4,X5),X4)
| ~ name(X5,X4) ) ),
inference(distribute,[status(thm)],[172]) ).
cnf(175,plain,
( sub(esk7_2(X2,X1),name_1_1)
| ~ name(X1,X2) ),
inference(split_conjunct,[status(thm)],[173]) ).
cnf(176,plain,
( attr(X1,esk7_2(X2,X1))
| ~ name(X1,X2) ),
inference(split_conjunct,[status(thm)],[173]) ).
cnf(307,plain,
name(c358,freeride_____344ra_0),
inference(split_conjunct,[status(thm)],[57]) ).
cnf(311,plain,
attr(c341,c342),
inference(split_conjunct,[status(thm)],[57]) ).
fof(312,negated_conjecture,
! [X1,X2,X3,X4,X5,X6] :
( ~ attr(X1,X2)
| ~ attr(X4,X3)
| ~ attr(X5,X6)
| ~ sub(X2,name_1_1)
| ~ sub(X3,name_1_1) ),
inference(fof_nnf,[status(thm)],[59]) ).
fof(313,negated_conjecture,
! [X7,X8,X9,X10,X11,X12] :
( ~ attr(X7,X8)
| ~ attr(X10,X9)
| ~ attr(X11,X12)
| ~ sub(X8,name_1_1)
| ~ sub(X9,name_1_1) ),
inference(variable_rename,[status(thm)],[312]) ).
cnf(314,negated_conjecture,
( ~ sub(X1,name_1_1)
| ~ sub(X2,name_1_1)
| ~ attr(X3,X4)
| ~ attr(X5,X1)
| ~ attr(X6,X2) ),
inference(split_conjunct,[status(thm)],[313]) ).
fof(322,plain,
( ~ epred1_0
<=> ! [X2,X6] :
( ~ sub(X2,name_1_1)
| ~ attr(X6,X2) ) ),
introduced(definition),
[split] ).
cnf(323,plain,
( epred1_0
| ~ sub(X2,name_1_1)
| ~ attr(X6,X2) ),
inference(split_equiv,[status(thm)],[322]) ).
fof(324,plain,
( ~ epred2_0
<=> ! [X1,X5] :
( ~ sub(X1,name_1_1)
| ~ attr(X5,X1) ) ),
introduced(definition),
[split] ).
cnf(325,plain,
( epred2_0
| ~ sub(X1,name_1_1)
| ~ attr(X5,X1) ),
inference(split_equiv,[status(thm)],[324]) ).
fof(326,plain,
( ~ epred3_0
<=> ! [X4,X3] : ~ attr(X3,X4) ),
introduced(definition),
[split] ).
cnf(327,plain,
( epred3_0
| ~ attr(X3,X4) ),
inference(split_equiv,[status(thm)],[326]) ).
cnf(328,negated_conjecture,
( ~ epred3_0
| ~ epred2_0
| ~ epred1_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[314,322,theory(equality)]),324,theory(equality)]),326,theory(equality)]),
[split] ).
cnf(402,plain,
epred3_0,
inference(spm,[status(thm)],[327,311,theory(equality)]) ).
cnf(405,negated_conjecture,
( $false
| ~ epred2_0
| ~ epred1_0 ),
inference(rw,[status(thm)],[328,402,theory(equality)]) ).
cnf(406,negated_conjecture,
( ~ epred2_0
| ~ epred1_0 ),
inference(cn,[status(thm)],[405,theory(equality)]) ).
cnf(408,negated_conjecture,
( epred1_0
| ~ sub(esk7_2(X2,X1),name_1_1)
| ~ name(X1,X2) ),
inference(spm,[status(thm)],[323,176,theory(equality)]) ).
cnf(412,negated_conjecture,
( epred2_0
| ~ sub(esk7_2(X2,X1),name_1_1)
| ~ name(X1,X2) ),
inference(spm,[status(thm)],[325,176,theory(equality)]) ).
cnf(413,negated_conjecture,
( epred1_0
| ~ name(X1,X2) ),
inference(csr,[status(thm)],[408,175]) ).
cnf(414,plain,
epred1_0,
inference(spm,[status(thm)],[413,307,theory(equality)]) ).
cnf(418,negated_conjecture,
( ~ epred2_0
| $false ),
inference(rw,[status(thm)],[406,414,theory(equality)]) ).
cnf(419,negated_conjecture,
~ epred2_0,
inference(cn,[status(thm)],[418,theory(equality)]) ).
cnf(421,negated_conjecture,
( ~ sub(esk7_2(X2,X1),name_1_1)
| ~ name(X1,X2) ),
inference(sr,[status(thm)],[412,419,theory(equality)]) ).
cnf(422,negated_conjecture,
~ name(X1,X2),
inference(csr,[status(thm)],[421,175]) ).
cnf(423,plain,
$false,
inference(sr,[status(thm)],[307,422,theory(equality)]) ).
cnf(424,plain,
$false,
423,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR115+82.p
% --creating new selector for [CSR004+0.ax]
% -running prover on /tmp/tmpF_oMRz/sel_CSR115+82.p_1 with time limit 29
% -prover status Theorem
% Problem CSR115+82.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR115+82.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR115+82.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
%
%------------------------------------------------------------------------------