%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWB106+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art07.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 : Fri Mar 4 00:55:34 EST 2011
% Result : Theorem 0.36s
% Output : CNFRefutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 71 ( 18 unt; 0 def)
% Number of atoms : 264 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 326 ( 133 ~; 131 |; 52 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-4 aty)
% Number of variables : 133 ( 9 sgn 91 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(23,axiom,
! [X1] : ir(X1),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',simple_ir) ).
fof(39,axiom,
! [X8,X9] :
( iext(uri_rdfs_subClassOf,X8,X9)
<=> ( ic(X8)
& ic(X9)
& ! [X1] :
( icext(X8,X1)
=> icext(X9,X1) ) ) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_rdfsext_subclassof) ).
fof(42,axiom,
! [X10,X6,X2] :
( ( iext(uri_owl_someValuesFrom,X10,X2)
& iext(uri_owl_onProperty,X10,X6) )
=> ! [X1] :
( icext(X10,X1)
<=> ? [X11] :
( iext(X6,X1,X11)
& icext(X2,X11) ) ) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_restrict_somevaluesfrom) ).
fof(44,axiom,
! [X1,X11] :
( iext(uri_owl_onProperty,X1,X11)
=> ( icext(uri_owl_Restriction,X1)
& ip(X11) ) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_prop_onproperty_ext) ).
fof(47,axiom,
! [X10,X6,X12] :
( ( iext(uri_owl_hasSelf,X10,X12)
& iext(uri_owl_onProperty,X10,X6) )
=> ! [X1] :
( icext(X10,X1)
<=> iext(X6,X1,X1) ) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_restrict_hasself) ).
fof(85,axiom,
! [X1] :
( icext(uri_owl_Restriction,X1)
=> ic(X1) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_class_restriction_ext) ).
fof(89,axiom,
! [X1] :
( icext(uri_owl_Thing,X1)
<=> ir(X1) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_class_thing_ext) ).
fof(91,axiom,
! [X1,X11] :
( iext(uri_owl_someValuesFrom,X1,X11)
=> ( icext(uri_owl_Restriction,X1)
& ic(X11) ) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',owl_prop_somevaluesfrom_ext) ).
fof(99,conjecture,
iext(uri_rdfs_subClassOf,uri_ex_z1,uri_ex_z2),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',conclusion_rdfbased_sem_restrict_term_selfsome) ).
fof(100,axiom,
( iext(uri_owl_someValuesFrom,uri_ex_z2,uri_owl_Thing)
& iext(uri_owl_onProperty,uri_ex_z2,uri_ex_p)
& iext(uri_owl_hasSelf,uri_ex_z1,literal_typed(dat_str_true,uri_xsd_boolean))
& iext(uri_owl_onProperty,uri_ex_z1,uri_ex_p) ),
file('/tmp/tmp2aDb5e/sel_SWB106+1.p_1',premise_rdfbased_sem_restrict_term_selfsome) ).
fof(101,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_z1,uri_ex_z2),
inference(assume_negation,[status(cth)],[99]) ).
fof(102,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_z1,uri_ex_z2),
inference(fof_simplification,[status(thm)],[101,theory(equality)]) ).
fof(159,plain,
! [X2] : ir(X2),
inference(variable_rename,[status(thm)],[23]) ).
cnf(160,plain,
ir(X1),
inference(split_conjunct,[status(thm)],[159]) ).
fof(207,plain,
! [X8,X9] :
( ( ~ iext(uri_rdfs_subClassOf,X8,X9)
| ( ic(X8)
& ic(X9)
& ! [X1] :
( ~ icext(X8,X1)
| icext(X9,X1) ) ) )
& ( ~ ic(X8)
| ~ ic(X9)
| ? [X1] :
( icext(X8,X1)
& ~ icext(X9,X1) )
| iext(uri_rdfs_subClassOf,X8,X9) ) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(208,plain,
! [X10,X11] :
( ( ~ iext(uri_rdfs_subClassOf,X10,X11)
| ( ic(X10)
& ic(X11)
& ! [X12] :
( ~ icext(X10,X12)
| icext(X11,X12) ) ) )
& ( ~ ic(X10)
| ~ ic(X11)
| ? [X13] :
( icext(X10,X13)
& ~ icext(X11,X13) )
| iext(uri_rdfs_subClassOf,X10,X11) ) ),
inference(variable_rename,[status(thm)],[207]) ).
fof(209,plain,
! [X10,X11] :
( ( ~ iext(uri_rdfs_subClassOf,X10,X11)
| ( ic(X10)
& ic(X11)
& ! [X12] :
( ~ icext(X10,X12)
| icext(X11,X12) ) ) )
& ( ~ ic(X10)
| ~ ic(X11)
| ( icext(X10,esk1_2(X10,X11))
& ~ icext(X11,esk1_2(X10,X11)) )
| iext(uri_rdfs_subClassOf,X10,X11) ) ),
inference(skolemize,[status(esa)],[208]) ).
fof(210,plain,
! [X10,X11,X12] :
( ( ( ( ~ icext(X10,X12)
| icext(X11,X12) )
& ic(X10)
& ic(X11) )
| ~ iext(uri_rdfs_subClassOf,X10,X11) )
& ( ~ ic(X10)
| ~ ic(X11)
| ( icext(X10,esk1_2(X10,X11))
& ~ icext(X11,esk1_2(X10,X11)) )
| iext(uri_rdfs_subClassOf,X10,X11) ) ),
inference(shift_quantors,[status(thm)],[209]) ).
fof(211,plain,
! [X10,X11,X12] :
( ( ~ icext(X10,X12)
| icext(X11,X12)
| ~ iext(uri_rdfs_subClassOf,X10,X11) )
& ( ic(X10)
| ~ iext(uri_rdfs_subClassOf,X10,X11) )
& ( ic(X11)
| ~ iext(uri_rdfs_subClassOf,X10,X11) )
& ( icext(X10,esk1_2(X10,X11))
| ~ ic(X10)
| ~ ic(X11)
| iext(uri_rdfs_subClassOf,X10,X11) )
& ( ~ icext(X11,esk1_2(X10,X11))
| ~ ic(X10)
| ~ ic(X11)
| iext(uri_rdfs_subClassOf,X10,X11) ) ),
inference(distribute,[status(thm)],[210]) ).
cnf(212,plain,
( iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X2)
| ~ ic(X1)
| ~ icext(X2,esk1_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[211]) ).
cnf(213,plain,
( iext(uri_rdfs_subClassOf,X1,X2)
| icext(X1,esk1_2(X1,X2))
| ~ ic(X2)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[211]) ).
fof(223,plain,
! [X10,X6,X2] :
( ~ iext(uri_owl_someValuesFrom,X10,X2)
| ~ iext(uri_owl_onProperty,X10,X6)
| ! [X1] :
( ( ~ icext(X10,X1)
| ? [X11] :
( iext(X6,X1,X11)
& icext(X2,X11) ) )
& ( ! [X11] :
( ~ iext(X6,X1,X11)
| ~ icext(X2,X11) )
| icext(X10,X1) ) ) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(224,plain,
! [X12,X13,X14] :
( ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13)
| ! [X15] :
( ( ~ icext(X12,X15)
| ? [X16] :
( iext(X13,X15,X16)
& icext(X14,X16) ) )
& ( ! [X17] :
( ~ iext(X13,X15,X17)
| ~ icext(X14,X17) )
| icext(X12,X15) ) ) ),
inference(variable_rename,[status(thm)],[223]) ).
fof(225,plain,
! [X12,X13,X14] :
( ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13)
| ! [X15] :
( ( ~ icext(X12,X15)
| ( iext(X13,X15,esk2_4(X12,X13,X14,X15))
& icext(X14,esk2_4(X12,X13,X14,X15)) ) )
& ( ! [X17] :
( ~ iext(X13,X15,X17)
| ~ icext(X14,X17) )
| icext(X12,X15) ) ) ),
inference(skolemize,[status(esa)],[224]) ).
fof(226,plain,
! [X12,X13,X14,X15,X17] :
( ( ( ~ iext(X13,X15,X17)
| ~ icext(X14,X17)
| icext(X12,X15) )
& ( ~ icext(X12,X15)
| ( iext(X13,X15,esk2_4(X12,X13,X14,X15))
& icext(X14,esk2_4(X12,X13,X14,X15)) ) ) )
| ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13) ),
inference(shift_quantors,[status(thm)],[225]) ).
fof(227,plain,
! [X12,X13,X14,X15,X17] :
( ( ~ iext(X13,X15,X17)
| ~ icext(X14,X17)
| icext(X12,X15)
| ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13) )
& ( iext(X13,X15,esk2_4(X12,X13,X14,X15))
| ~ icext(X12,X15)
| ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13) )
& ( icext(X14,esk2_4(X12,X13,X14,X15))
| ~ icext(X12,X15)
| ~ iext(uri_owl_someValuesFrom,X12,X14)
| ~ iext(uri_owl_onProperty,X12,X13) ) ),
inference(distribute,[status(thm)],[226]) ).
cnf(230,plain,
( icext(X1,X4)
| ~ iext(uri_owl_onProperty,X1,X2)
| ~ iext(uri_owl_someValuesFrom,X1,X3)
| ~ icext(X3,X5)
| ~ iext(X2,X4,X5) ),
inference(split_conjunct,[status(thm)],[227]) ).
fof(234,plain,
! [X1,X11] :
( ~ iext(uri_owl_onProperty,X1,X11)
| ( icext(uri_owl_Restriction,X1)
& ip(X11) ) ),
inference(fof_nnf,[status(thm)],[44]) ).
fof(235,plain,
! [X12,X13] :
( ~ iext(uri_owl_onProperty,X12,X13)
| ( icext(uri_owl_Restriction,X12)
& ip(X13) ) ),
inference(variable_rename,[status(thm)],[234]) ).
fof(236,plain,
! [X12,X13] :
( ( icext(uri_owl_Restriction,X12)
| ~ iext(uri_owl_onProperty,X12,X13) )
& ( ip(X13)
| ~ iext(uri_owl_onProperty,X12,X13) ) ),
inference(distribute,[status(thm)],[235]) ).
cnf(238,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_onProperty,X1,X2) ),
inference(split_conjunct,[status(thm)],[236]) ).
fof(245,plain,
! [X10,X6,X12] :
( ~ iext(uri_owl_hasSelf,X10,X12)
| ~ iext(uri_owl_onProperty,X10,X6)
| ! [X1] :
( ( ~ icext(X10,X1)
| iext(X6,X1,X1) )
& ( ~ iext(X6,X1,X1)
| icext(X10,X1) ) ) ),
inference(fof_nnf,[status(thm)],[47]) ).
fof(246,plain,
! [X13,X14,X15] :
( ~ iext(uri_owl_hasSelf,X13,X15)
| ~ iext(uri_owl_onProperty,X13,X14)
| ! [X16] :
( ( ~ icext(X13,X16)
| iext(X14,X16,X16) )
& ( ~ iext(X14,X16,X16)
| icext(X13,X16) ) ) ),
inference(variable_rename,[status(thm)],[245]) ).
fof(247,plain,
! [X13,X14,X15,X16] :
( ( ( ~ icext(X13,X16)
| iext(X14,X16,X16) )
& ( ~ iext(X14,X16,X16)
| icext(X13,X16) ) )
| ~ iext(uri_owl_hasSelf,X13,X15)
| ~ iext(uri_owl_onProperty,X13,X14) ),
inference(shift_quantors,[status(thm)],[246]) ).
fof(248,plain,
! [X13,X14,X15,X16] :
( ( ~ icext(X13,X16)
| iext(X14,X16,X16)
| ~ iext(uri_owl_hasSelf,X13,X15)
| ~ iext(uri_owl_onProperty,X13,X14) )
& ( ~ iext(X14,X16,X16)
| icext(X13,X16)
| ~ iext(uri_owl_hasSelf,X13,X15)
| ~ iext(uri_owl_onProperty,X13,X14) ) ),
inference(distribute,[status(thm)],[247]) ).
cnf(250,plain,
( iext(X2,X4,X4)
| ~ iext(uri_owl_onProperty,X1,X2)
| ~ iext(uri_owl_hasSelf,X1,X3)
| ~ icext(X1,X4) ),
inference(split_conjunct,[status(thm)],[248]) ).
fof(355,plain,
! [X1] :
( ~ icext(uri_owl_Restriction,X1)
| ic(X1) ),
inference(fof_nnf,[status(thm)],[85]) ).
fof(356,plain,
! [X2] :
( ~ icext(uri_owl_Restriction,X2)
| ic(X2) ),
inference(variable_rename,[status(thm)],[355]) ).
cnf(357,plain,
( ic(X1)
| ~ icext(uri_owl_Restriction,X1) ),
inference(split_conjunct,[status(thm)],[356]) ).
fof(365,plain,
! [X1] :
( ( ~ icext(uri_owl_Thing,X1)
| ir(X1) )
& ( ~ ir(X1)
| icext(uri_owl_Thing,X1) ) ),
inference(fof_nnf,[status(thm)],[89]) ).
fof(366,plain,
! [X2] :
( ( ~ icext(uri_owl_Thing,X2)
| ir(X2) )
& ( ~ ir(X2)
| icext(uri_owl_Thing,X2) ) ),
inference(variable_rename,[status(thm)],[365]) ).
cnf(367,plain,
( icext(uri_owl_Thing,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[366]) ).
fof(372,plain,
! [X1,X11] :
( ~ iext(uri_owl_someValuesFrom,X1,X11)
| ( icext(uri_owl_Restriction,X1)
& ic(X11) ) ),
inference(fof_nnf,[status(thm)],[91]) ).
fof(373,plain,
! [X12,X13] :
( ~ iext(uri_owl_someValuesFrom,X12,X13)
| ( icext(uri_owl_Restriction,X12)
& ic(X13) ) ),
inference(variable_rename,[status(thm)],[372]) ).
fof(374,plain,
! [X12,X13] :
( ( icext(uri_owl_Restriction,X12)
| ~ iext(uri_owl_someValuesFrom,X12,X13) )
& ( ic(X13)
| ~ iext(uri_owl_someValuesFrom,X12,X13) ) ),
inference(distribute,[status(thm)],[373]) ).
cnf(376,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_someValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[374]) ).
cnf(399,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_ex_z1,uri_ex_z2),
inference(split_conjunct,[status(thm)],[102]) ).
cnf(400,plain,
iext(uri_owl_onProperty,uri_ex_z1,uri_ex_p),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(401,plain,
iext(uri_owl_hasSelf,uri_ex_z1,literal_typed(dat_str_true,uri_xsd_boolean)),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(402,plain,
iext(uri_owl_onProperty,uri_ex_z2,uri_ex_p),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(403,plain,
iext(uri_owl_someValuesFrom,uri_ex_z2,uri_owl_Thing),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(414,plain,
( icext(uri_owl_Thing,X1)
| $false ),
inference(rw,[status(thm)],[367,160,theory(equality)]),
[unfolding] ).
cnf(456,plain,
icext(uri_owl_Restriction,uri_ex_z2),
inference(spm,[status(thm)],[376,403,theory(equality)]) ).
cnf(457,plain,
icext(uri_owl_Restriction,uri_ex_z1),
inference(spm,[status(thm)],[238,400,theory(equality)]) ).
cnf(467,plain,
( iext(uri_ex_p,X1,X1)
| ~ iext(uri_owl_hasSelf,uri_ex_z1,X2)
| ~ icext(uri_ex_z1,X1) ),
inference(spm,[status(thm)],[250,400,theory(equality)]) ).
cnf(496,plain,
( icext(uri_ex_z2,X1)
| ~ iext(uri_owl_onProperty,uri_ex_z2,X2)
| ~ iext(X2,X1,X3)
| ~ icext(uri_owl_Thing,X3) ),
inference(spm,[status(thm)],[230,403,theory(equality)]) ).
cnf(497,plain,
( icext(uri_ex_z2,X1)
| ~ iext(uri_owl_onProperty,uri_ex_z2,X2)
| ~ iext(X2,X1,X3)
| $false ),
inference(rw,[status(thm)],[496,414,theory(equality)]) ).
cnf(498,plain,
( icext(uri_ex_z2,X1)
| ~ iext(uri_owl_onProperty,uri_ex_z2,X2)
| ~ iext(X2,X1,X3) ),
inference(cn,[status(thm)],[497,theory(equality)]) ).
cnf(670,plain,
( iext(uri_ex_p,X1,X1)
| ~ icext(uri_ex_z1,X1) ),
inference(spm,[status(thm)],[467,401,theory(equality)]) ).
cnf(708,plain,
( icext(uri_ex_z2,X1)
| ~ iext(uri_ex_p,X1,X2) ),
inference(spm,[status(thm)],[498,402,theory(equality)]) ).
cnf(711,plain,
( icext(uri_ex_z2,X1)
| ~ icext(uri_ex_z1,X1) ),
inference(spm,[status(thm)],[708,670,theory(equality)]) ).
cnf(712,plain,
( icext(uri_ex_z2,esk1_2(uri_ex_z1,X1))
| iext(uri_rdfs_subClassOf,uri_ex_z1,X1)
| ~ ic(X1)
| ~ ic(uri_ex_z1) ),
inference(spm,[status(thm)],[711,213,theory(equality)]) ).
cnf(724,plain,
( iext(uri_rdfs_subClassOf,uri_ex_z1,uri_ex_z2)
| ~ ic(uri_ex_z2)
| ~ ic(uri_ex_z1) ),
inference(spm,[status(thm)],[212,712,theory(equality)]) ).
cnf(725,plain,
( ~ ic(uri_ex_z2)
| ~ ic(uri_ex_z1) ),
inference(sr,[status(thm)],[724,399,theory(equality)]) ).
cnf(728,plain,
( ~ ic(uri_ex_z2)
| ~ icext(uri_owl_Restriction,uri_ex_z1) ),
inference(spm,[status(thm)],[725,357,theory(equality)]) ).
cnf(729,plain,
( ~ ic(uri_ex_z2)
| $false ),
inference(rw,[status(thm)],[728,457,theory(equality)]) ).
cnf(730,plain,
~ ic(uri_ex_z2),
inference(cn,[status(thm)],[729,theory(equality)]) ).
cnf(731,plain,
~ icext(uri_owl_Restriction,uri_ex_z2),
inference(spm,[status(thm)],[730,357,theory(equality)]) ).
cnf(732,plain,
$false,
inference(rw,[status(thm)],[731,456,theory(equality)]) ).
cnf(733,plain,
$false,
inference(cn,[status(thm)],[732,theory(equality)]) ).
cnf(734,plain,
$false,
733,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWB/SWB106+1.p
% --creating new selector for [SWB001+0.ax]
% -running prover on /tmp/tmp2aDb5e/sel_SWB106+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWB106+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWB/SWB106+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWB/SWB106+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
%
%------------------------------------------------------------------------------