%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : PRO010+2 : TPTP v5.0.0. Released v4.0.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 : Sun Dec 26 00:37:19 EST 2010
% Result : Theorem 0.20s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 6
% Syntax : Number of formulae : 60 ( 8 unt; 0 def)
% Number of atoms : 296 ( 10 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 343 ( 107 ~; 125 |; 101 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 128 ( 11 sgn 65 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(7,axiom,
! [X23,X24,X25] :
( ( occurrence_of(X23,X24)
& occurrence_of(X23,X25) )
=> X24 = X25 ),
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',sos_22) ).
fof(24,axiom,
tptp1 != tptp2,
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',sos_44) ).
fof(26,axiom,
! [X63] :
( occurrence_of(X63,tptp0)
=> ? [X64,X65,X66] :
( occurrence_of(X64,tptp3)
& root_occ(X64,X63)
& occurrence_of(X65,tptp4)
& next_subocc(X64,X65,tptp0)
& ( occurrence_of(X66,tptp1)
| occurrence_of(X66,tptp2) )
& next_subocc(X65,X66,tptp0)
& leaf_occ(X66,X63) ) ),
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',sos_32) ).
fof(38,axiom,
! [X80,X81] :
( leaf_occ(X80,X81)
<=> ? [X82] :
( occurrence_of(X81,X82)
& subactivity_occurrence(X80,X81)
& leaf(X80,X82) ) ),
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',sos_11) ).
fof(43,axiom,
! [X93,X94] :
( leaf(X93,X94)
<=> ( ( root(X93,X94)
| ? [X95] : min_precedes(X95,X93,X94) )
& ~ ? [X96] : min_precedes(X93,X96,X94) ) ),
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',sos_14) ).
fof(46,conjecture,
! [X100] :
( occurrence_of(X100,tptp0)
=> ? [X101,X102] :
( leaf_occ(X102,X100)
& ( occurrence_of(X102,tptp1)
=> ~ ? [X103] :
( occurrence_of(X103,tptp2)
& min_precedes(X101,X103,tptp0) ) )
& ( occurrence_of(X102,tptp2)
=> ~ ? [X104] :
( occurrence_of(X104,tptp1)
& min_precedes(X101,X104,tptp0) ) ) ) ),
file('/tmp/tmpPM02Tw/sel_PRO010+2.p_1',goals) ).
fof(47,negated_conjecture,
~ ! [X100] :
( occurrence_of(X100,tptp0)
=> ? [X101,X102] :
( leaf_occ(X102,X100)
& ( occurrence_of(X102,tptp1)
=> ~ ? [X103] :
( occurrence_of(X103,tptp2)
& min_precedes(X101,X103,tptp0) ) )
& ( occurrence_of(X102,tptp2)
=> ~ ? [X104] :
( occurrence_of(X104,tptp1)
& min_precedes(X101,X104,tptp0) ) ) ) ),
inference(assume_negation,[status(cth)],[46]) ).
fof(85,plain,
! [X23,X24,X25] :
( ~ occurrence_of(X23,X24)
| ~ occurrence_of(X23,X25)
| X24 = X25 ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(86,plain,
! [X26,X27,X28] :
( ~ occurrence_of(X26,X27)
| ~ occurrence_of(X26,X28)
| X27 = X28 ),
inference(variable_rename,[status(thm)],[85]) ).
cnf(87,plain,
( X1 = X2
| ~ occurrence_of(X3,X2)
| ~ occurrence_of(X3,X1) ),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(144,plain,
tptp1 != tptp2,
inference(split_conjunct,[status(thm)],[24]) ).
fof(146,plain,
! [X63] :
( ~ occurrence_of(X63,tptp0)
| ? [X64,X65,X66] :
( occurrence_of(X64,tptp3)
& root_occ(X64,X63)
& occurrence_of(X65,tptp4)
& next_subocc(X64,X65,tptp0)
& ( occurrence_of(X66,tptp1)
| occurrence_of(X66,tptp2) )
& next_subocc(X65,X66,tptp0)
& leaf_occ(X66,X63) ) ),
inference(fof_nnf,[status(thm)],[26]) ).
fof(147,plain,
! [X67] :
( ~ occurrence_of(X67,tptp0)
| ? [X68,X69,X70] :
( occurrence_of(X68,tptp3)
& root_occ(X68,X67)
& occurrence_of(X69,tptp4)
& next_subocc(X68,X69,tptp0)
& ( occurrence_of(X70,tptp1)
| occurrence_of(X70,tptp2) )
& next_subocc(X69,X70,tptp0)
& leaf_occ(X70,X67) ) ),
inference(variable_rename,[status(thm)],[146]) ).
fof(148,plain,
! [X67] :
( ~ occurrence_of(X67,tptp0)
| ( occurrence_of(esk6_1(X67),tptp3)
& root_occ(esk6_1(X67),X67)
& occurrence_of(esk7_1(X67),tptp4)
& next_subocc(esk6_1(X67),esk7_1(X67),tptp0)
& ( occurrence_of(esk8_1(X67),tptp1)
| occurrence_of(esk8_1(X67),tptp2) )
& next_subocc(esk7_1(X67),esk8_1(X67),tptp0)
& leaf_occ(esk8_1(X67),X67) ) ),
inference(skolemize,[status(esa)],[147]) ).
fof(149,plain,
! [X67] :
( ( occurrence_of(esk6_1(X67),tptp3)
| ~ occurrence_of(X67,tptp0) )
& ( root_occ(esk6_1(X67),X67)
| ~ occurrence_of(X67,tptp0) )
& ( occurrence_of(esk7_1(X67),tptp4)
| ~ occurrence_of(X67,tptp0) )
& ( next_subocc(esk6_1(X67),esk7_1(X67),tptp0)
| ~ occurrence_of(X67,tptp0) )
& ( occurrence_of(esk8_1(X67),tptp1)
| occurrence_of(esk8_1(X67),tptp2)
| ~ occurrence_of(X67,tptp0) )
& ( next_subocc(esk7_1(X67),esk8_1(X67),tptp0)
| ~ occurrence_of(X67,tptp0) )
& ( leaf_occ(esk8_1(X67),X67)
| ~ occurrence_of(X67,tptp0) ) ),
inference(distribute,[status(thm)],[148]) ).
cnf(150,plain,
( leaf_occ(esk8_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[149]) ).
fof(191,plain,
! [X80,X81] :
( ( ~ leaf_occ(X80,X81)
| ? [X82] :
( occurrence_of(X81,X82)
& subactivity_occurrence(X80,X81)
& leaf(X80,X82) ) )
& ( ! [X82] :
( ~ occurrence_of(X81,X82)
| ~ subactivity_occurrence(X80,X81)
| ~ leaf(X80,X82) )
| leaf_occ(X80,X81) ) ),
inference(fof_nnf,[status(thm)],[38]) ).
fof(192,plain,
! [X83,X84] :
( ( ~ leaf_occ(X83,X84)
| ? [X85] :
( occurrence_of(X84,X85)
& subactivity_occurrence(X83,X84)
& leaf(X83,X85) ) )
& ( ! [X86] :
( ~ occurrence_of(X84,X86)
| ~ subactivity_occurrence(X83,X84)
| ~ leaf(X83,X86) )
| leaf_occ(X83,X84) ) ),
inference(variable_rename,[status(thm)],[191]) ).
fof(193,plain,
! [X83,X84] :
( ( ~ leaf_occ(X83,X84)
| ( occurrence_of(X84,esk13_2(X83,X84))
& subactivity_occurrence(X83,X84)
& leaf(X83,esk13_2(X83,X84)) ) )
& ( ! [X86] :
( ~ occurrence_of(X84,X86)
| ~ subactivity_occurrence(X83,X84)
| ~ leaf(X83,X86) )
| leaf_occ(X83,X84) ) ),
inference(skolemize,[status(esa)],[192]) ).
fof(194,plain,
! [X83,X84,X86] :
( ( ~ occurrence_of(X84,X86)
| ~ subactivity_occurrence(X83,X84)
| ~ leaf(X83,X86)
| leaf_occ(X83,X84) )
& ( ~ leaf_occ(X83,X84)
| ( occurrence_of(X84,esk13_2(X83,X84))
& subactivity_occurrence(X83,X84)
& leaf(X83,esk13_2(X83,X84)) ) ) ),
inference(shift_quantors,[status(thm)],[193]) ).
fof(195,plain,
! [X83,X84,X86] :
( ( ~ occurrence_of(X84,X86)
| ~ subactivity_occurrence(X83,X84)
| ~ leaf(X83,X86)
| leaf_occ(X83,X84) )
& ( occurrence_of(X84,esk13_2(X83,X84))
| ~ leaf_occ(X83,X84) )
& ( subactivity_occurrence(X83,X84)
| ~ leaf_occ(X83,X84) )
& ( leaf(X83,esk13_2(X83,X84))
| ~ leaf_occ(X83,X84) ) ),
inference(distribute,[status(thm)],[194]) ).
cnf(196,plain,
( leaf(X1,esk13_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(198,plain,
( occurrence_of(X2,esk13_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[195]) ).
fof(226,plain,
! [X93,X94] :
( ( ~ leaf(X93,X94)
| ( ( root(X93,X94)
| ? [X95] : min_precedes(X95,X93,X94) )
& ! [X96] : ~ min_precedes(X93,X96,X94) ) )
& ( ( ~ root(X93,X94)
& ! [X95] : ~ min_precedes(X95,X93,X94) )
| ? [X96] : min_precedes(X93,X96,X94)
| leaf(X93,X94) ) ),
inference(fof_nnf,[status(thm)],[43]) ).
fof(227,plain,
! [X97,X98] :
( ( ~ leaf(X97,X98)
| ( ( root(X97,X98)
| ? [X99] : min_precedes(X99,X97,X98) )
& ! [X100] : ~ min_precedes(X97,X100,X98) ) )
& ( ( ~ root(X97,X98)
& ! [X101] : ~ min_precedes(X101,X97,X98) )
| ? [X102] : min_precedes(X97,X102,X98)
| leaf(X97,X98) ) ),
inference(variable_rename,[status(thm)],[226]) ).
fof(228,plain,
! [X97,X98] :
( ( ~ leaf(X97,X98)
| ( ( root(X97,X98)
| min_precedes(esk16_2(X97,X98),X97,X98) )
& ! [X100] : ~ min_precedes(X97,X100,X98) ) )
& ( ( ~ root(X97,X98)
& ! [X101] : ~ min_precedes(X101,X97,X98) )
| min_precedes(X97,esk17_2(X97,X98),X98)
| leaf(X97,X98) ) ),
inference(skolemize,[status(esa)],[227]) ).
fof(229,plain,
! [X97,X98,X100,X101] :
( ( ( ~ min_precedes(X101,X97,X98)
& ~ root(X97,X98) )
| min_precedes(X97,esk17_2(X97,X98),X98)
| leaf(X97,X98) )
& ( ( ~ min_precedes(X97,X100,X98)
& ( root(X97,X98)
| min_precedes(esk16_2(X97,X98),X97,X98) ) )
| ~ leaf(X97,X98) ) ),
inference(shift_quantors,[status(thm)],[228]) ).
fof(230,plain,
! [X97,X98,X100,X101] :
( ( ~ min_precedes(X101,X97,X98)
| min_precedes(X97,esk17_2(X97,X98),X98)
| leaf(X97,X98) )
& ( ~ root(X97,X98)
| min_precedes(X97,esk17_2(X97,X98),X98)
| leaf(X97,X98) )
& ( ~ min_precedes(X97,X100,X98)
| ~ leaf(X97,X98) )
& ( root(X97,X98)
| min_precedes(esk16_2(X97,X98),X97,X98)
| ~ leaf(X97,X98) ) ),
inference(distribute,[status(thm)],[229]) ).
cnf(232,plain,
( ~ leaf(X1,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[230]) ).
fof(241,negated_conjecture,
? [X100] :
( occurrence_of(X100,tptp0)
& ! [X101,X102] :
( ~ leaf_occ(X102,X100)
| ( occurrence_of(X102,tptp1)
& ? [X103] :
( occurrence_of(X103,tptp2)
& min_precedes(X101,X103,tptp0) ) )
| ( occurrence_of(X102,tptp2)
& ? [X104] :
( occurrence_of(X104,tptp1)
& min_precedes(X101,X104,tptp0) ) ) ) ),
inference(fof_nnf,[status(thm)],[47]) ).
fof(242,negated_conjecture,
? [X105] :
( occurrence_of(X105,tptp0)
& ! [X106,X107] :
( ~ leaf_occ(X107,X105)
| ( occurrence_of(X107,tptp1)
& ? [X108] :
( occurrence_of(X108,tptp2)
& min_precedes(X106,X108,tptp0) ) )
| ( occurrence_of(X107,tptp2)
& ? [X109] :
( occurrence_of(X109,tptp1)
& min_precedes(X106,X109,tptp0) ) ) ) ),
inference(variable_rename,[status(thm)],[241]) ).
fof(243,negated_conjecture,
( occurrence_of(esk18_0,tptp0)
& ! [X106,X107] :
( ~ leaf_occ(X107,esk18_0)
| ( occurrence_of(X107,tptp1)
& occurrence_of(esk19_2(X106,X107),tptp2)
& min_precedes(X106,esk19_2(X106,X107),tptp0) )
| ( occurrence_of(X107,tptp2)
& occurrence_of(esk20_2(X106,X107),tptp1)
& min_precedes(X106,esk20_2(X106,X107),tptp0) ) ) ),
inference(skolemize,[status(esa)],[242]) ).
fof(244,negated_conjecture,
! [X106,X107] :
( ( ~ leaf_occ(X107,esk18_0)
| ( occurrence_of(X107,tptp1)
& occurrence_of(esk19_2(X106,X107),tptp2)
& min_precedes(X106,esk19_2(X106,X107),tptp0) )
| ( occurrence_of(X107,tptp2)
& occurrence_of(esk20_2(X106,X107),tptp1)
& min_precedes(X106,esk20_2(X106,X107),tptp0) ) )
& occurrence_of(esk18_0,tptp0) ),
inference(shift_quantors,[status(thm)],[243]) ).
fof(245,negated_conjecture,
! [X106,X107] :
( ( occurrence_of(X107,tptp2)
| occurrence_of(X107,tptp1)
| ~ leaf_occ(X107,esk18_0) )
& ( occurrence_of(esk20_2(X106,X107),tptp1)
| occurrence_of(X107,tptp1)
| ~ leaf_occ(X107,esk18_0) )
& ( min_precedes(X106,esk20_2(X106,X107),tptp0)
| occurrence_of(X107,tptp1)
| ~ leaf_occ(X107,esk18_0) )
& ( occurrence_of(X107,tptp2)
| occurrence_of(esk19_2(X106,X107),tptp2)
| ~ leaf_occ(X107,esk18_0) )
& ( occurrence_of(esk20_2(X106,X107),tptp1)
| occurrence_of(esk19_2(X106,X107),tptp2)
| ~ leaf_occ(X107,esk18_0) )
& ( min_precedes(X106,esk20_2(X106,X107),tptp0)
| occurrence_of(esk19_2(X106,X107),tptp2)
| ~ leaf_occ(X107,esk18_0) )
& ( occurrence_of(X107,tptp2)
| min_precedes(X106,esk19_2(X106,X107),tptp0)
| ~ leaf_occ(X107,esk18_0) )
& ( occurrence_of(esk20_2(X106,X107),tptp1)
| min_precedes(X106,esk19_2(X106,X107),tptp0)
| ~ leaf_occ(X107,esk18_0) )
& ( min_precedes(X106,esk20_2(X106,X107),tptp0)
| min_precedes(X106,esk19_2(X106,X107),tptp0)
| ~ leaf_occ(X107,esk18_0) )
& occurrence_of(esk18_0,tptp0) ),
inference(distribute,[status(thm)],[244]) ).
cnf(246,negated_conjecture,
occurrence_of(esk18_0,tptp0),
inference(split_conjunct,[status(thm)],[245]) ).
cnf(249,negated_conjecture,
( min_precedes(X2,esk19_2(X2,X1),tptp0)
| occurrence_of(X1,tptp2)
| ~ leaf_occ(X1,esk18_0) ),
inference(split_conjunct,[status(thm)],[245]) ).
cnf(253,negated_conjecture,
( occurrence_of(X1,tptp1)
| min_precedes(X2,esk20_2(X2,X1),tptp0)
| ~ leaf_occ(X1,esk18_0) ),
inference(split_conjunct,[status(thm)],[245]) ).
cnf(288,negated_conjecture,
( X1 = tptp0
| ~ occurrence_of(esk18_0,X1) ),
inference(spm,[status(thm)],[87,246,theory(equality)]) ).
cnf(338,negated_conjecture,
( occurrence_of(X2,tptp1)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk18_0) ),
inference(spm,[status(thm)],[232,253,theory(equality)]) ).
cnf(345,negated_conjecture,
( occurrence_of(X2,tptp2)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk18_0) ),
inference(spm,[status(thm)],[232,249,theory(equality)]) ).
cnf(455,negated_conjecture,
( esk13_2(X1,esk18_0) = tptp0
| ~ leaf_occ(X1,esk18_0) ),
inference(spm,[status(thm)],[288,198,theory(equality)]) ).
cnf(505,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk18_0,tptp0) ),
inference(spm,[status(thm)],[338,150,theory(equality)]) ).
cnf(506,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[505,246,theory(equality)]) ).
cnf(507,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[506,theory(equality)]) ).
cnf(518,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk18_0,tptp0) ),
inference(spm,[status(thm)],[345,150,theory(equality)]) ).
cnf(519,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[518,246,theory(equality)]) ).
cnf(520,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[519,theory(equality)]) ).
cnf(527,negated_conjecture,
( leaf(X1,tptp0)
| ~ leaf_occ(X1,esk18_0) ),
inference(spm,[status(thm)],[196,455,theory(equality)]) ).
cnf(549,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| ~ leaf_occ(X1,esk18_0) ),
inference(spm,[status(thm)],[507,527,theory(equality)]) ).
cnf(550,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| ~ leaf_occ(X1,esk18_0) ),
inference(spm,[status(thm)],[520,527,theory(equality)]) ).
cnf(552,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| ~ occurrence_of(esk18_0,tptp0) ),
inference(spm,[status(thm)],[549,150,theory(equality)]) ).
cnf(553,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp1)
| $false ),
inference(rw,[status(thm)],[552,246,theory(equality)]) ).
cnf(554,negated_conjecture,
occurrence_of(esk8_1(esk18_0),tptp1),
inference(cn,[status(thm)],[553,theory(equality)]) ).
cnf(559,negated_conjecture,
( X1 = tptp1
| ~ occurrence_of(esk8_1(esk18_0),X1) ),
inference(spm,[status(thm)],[87,554,theory(equality)]) ).
cnf(611,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| ~ occurrence_of(esk18_0,tptp0) ),
inference(spm,[status(thm)],[550,150,theory(equality)]) ).
cnf(612,negated_conjecture,
( occurrence_of(esk8_1(esk18_0),tptp2)
| $false ),
inference(rw,[status(thm)],[611,246,theory(equality)]) ).
cnf(613,negated_conjecture,
occurrence_of(esk8_1(esk18_0),tptp2),
inference(cn,[status(thm)],[612,theory(equality)]) ).
cnf(619,negated_conjecture,
tptp2 = tptp1,
inference(spm,[status(thm)],[559,613,theory(equality)]) ).
cnf(630,negated_conjecture,
$false,
inference(sr,[status(thm)],[619,144,theory(equality)]) ).
cnf(631,negated_conjecture,
$false,
630,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/PRO/PRO010+2.p
% --creating new selector for []
% -running prover on /tmp/tmpPM02Tw/sel_PRO010+2.p_1 with time limit 29
% -prover status Theorem
% Problem PRO010+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/PRO/PRO010+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/PRO/PRO010+2.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
%
%------------------------------------------------------------------------------