%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : PRO010+3 : 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:23 EST 2010
% Result : Theorem 0.23s
% Output : CNFRefutation 0.23s
% 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(9,axiom,
! [X16,X17] :
( leaf(X16,X17)
<=> ( ( root(X16,X17)
| ? [X18] : min_precedes(X18,X16,X17) )
& ~ ? [X19] : min_precedes(X16,X19,X17) ) ),
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',sos_21) ).
fof(12,axiom,
! [X27] :
( occurrence_of(X27,tptp0)
=> ? [X28,X29,X30] :
( occurrence_of(X28,tptp3)
& root_occ(X28,X27)
& occurrence_of(X29,tptp4)
& next_subocc(X28,X29,tptp0)
& ( occurrence_of(X30,tptp1)
| occurrence_of(X30,tptp2) )
& next_subocc(X29,X30,tptp0)
& leaf_occ(X30,X27) ) ),
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',sos_49) ).
fof(23,axiom,
! [X66,X67,X68] :
( ( occurrence_of(X66,X67)
& occurrence_of(X66,X68) )
=> X67 = X68 ),
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',sos_02) ).
fof(41,axiom,
! [X117,X118] :
( leaf_occ(X117,X118)
<=> ? [X119] :
( occurrence_of(X118,X119)
& subactivity_occurrence(X117,X118)
& leaf(X117,X119) ) ),
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',sos_34) ).
fof(42,axiom,
tptp1 != tptp2,
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',sos_61) ).
fof(63,conjecture,
! [X166] :
( occurrence_of(X166,tptp0)
=> ? [X167,X168] :
( leaf_occ(X168,X166)
& ( occurrence_of(X168,tptp1)
=> ~ ? [X169] :
( occurrence_of(X169,tptp2)
& min_precedes(X167,X169,tptp0) ) )
& ( occurrence_of(X168,tptp2)
=> ~ ? [X170] :
( occurrence_of(X170,tptp1)
& min_precedes(X167,X170,tptp0) ) ) ) ),
file('/tmp/tmpdFSU0l/sel_PRO010+3.p_1',goals) ).
fof(64,negated_conjecture,
~ ! [X166] :
( occurrence_of(X166,tptp0)
=> ? [X167,X168] :
( leaf_occ(X168,X166)
& ( occurrence_of(X168,tptp1)
=> ~ ? [X169] :
( occurrence_of(X169,tptp2)
& min_precedes(X167,X169,tptp0) ) )
& ( occurrence_of(X168,tptp2)
=> ~ ? [X170] :
( occurrence_of(X170,tptp1)
& min_precedes(X167,X170,tptp0) ) ) ) ),
inference(assume_negation,[status(cth)],[63]) ).
fof(106,plain,
! [X16,X17] :
( ( ~ leaf(X16,X17)
| ( ( root(X16,X17)
| ? [X18] : min_precedes(X18,X16,X17) )
& ! [X19] : ~ min_precedes(X16,X19,X17) ) )
& ( ( ~ root(X16,X17)
& ! [X18] : ~ min_precedes(X18,X16,X17) )
| ? [X19] : min_precedes(X16,X19,X17)
| leaf(X16,X17) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(107,plain,
! [X20,X21] :
( ( ~ leaf(X20,X21)
| ( ( root(X20,X21)
| ? [X22] : min_precedes(X22,X20,X21) )
& ! [X23] : ~ min_precedes(X20,X23,X21) ) )
& ( ( ~ root(X20,X21)
& ! [X24] : ~ min_precedes(X24,X20,X21) )
| ? [X25] : min_precedes(X20,X25,X21)
| leaf(X20,X21) ) ),
inference(variable_rename,[status(thm)],[106]) ).
fof(108,plain,
! [X20,X21] :
( ( ~ leaf(X20,X21)
| ( ( root(X20,X21)
| min_precedes(esk3_2(X20,X21),X20,X21) )
& ! [X23] : ~ min_precedes(X20,X23,X21) ) )
& ( ( ~ root(X20,X21)
& ! [X24] : ~ min_precedes(X24,X20,X21) )
| min_precedes(X20,esk4_2(X20,X21),X21)
| leaf(X20,X21) ) ),
inference(skolemize,[status(esa)],[107]) ).
fof(109,plain,
! [X20,X21,X23,X24] :
( ( ( ~ min_precedes(X24,X20,X21)
& ~ root(X20,X21) )
| min_precedes(X20,esk4_2(X20,X21),X21)
| leaf(X20,X21) )
& ( ( ~ min_precedes(X20,X23,X21)
& ( root(X20,X21)
| min_precedes(esk3_2(X20,X21),X20,X21) ) )
| ~ leaf(X20,X21) ) ),
inference(shift_quantors,[status(thm)],[108]) ).
fof(110,plain,
! [X20,X21,X23,X24] :
( ( ~ min_precedes(X24,X20,X21)
| min_precedes(X20,esk4_2(X20,X21),X21)
| leaf(X20,X21) )
& ( ~ root(X20,X21)
| min_precedes(X20,esk4_2(X20,X21),X21)
| leaf(X20,X21) )
& ( ~ min_precedes(X20,X23,X21)
| ~ leaf(X20,X21) )
& ( root(X20,X21)
| min_precedes(esk3_2(X20,X21),X20,X21)
| ~ leaf(X20,X21) ) ),
inference(distribute,[status(thm)],[109]) ).
cnf(112,plain,
( ~ leaf(X1,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[110]) ).
fof(133,plain,
! [X27] :
( ~ occurrence_of(X27,tptp0)
| ? [X28,X29,X30] :
( occurrence_of(X28,tptp3)
& root_occ(X28,X27)
& occurrence_of(X29,tptp4)
& next_subocc(X28,X29,tptp0)
& ( occurrence_of(X30,tptp1)
| occurrence_of(X30,tptp2) )
& next_subocc(X29,X30,tptp0)
& leaf_occ(X30,X27) ) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(134,plain,
! [X31] :
( ~ occurrence_of(X31,tptp0)
| ? [X32,X33,X34] :
( occurrence_of(X32,tptp3)
& root_occ(X32,X31)
& occurrence_of(X33,tptp4)
& next_subocc(X32,X33,tptp0)
& ( occurrence_of(X34,tptp1)
| occurrence_of(X34,tptp2) )
& next_subocc(X33,X34,tptp0)
& leaf_occ(X34,X31) ) ),
inference(variable_rename,[status(thm)],[133]) ).
fof(135,plain,
! [X31] :
( ~ occurrence_of(X31,tptp0)
| ( occurrence_of(esk7_1(X31),tptp3)
& root_occ(esk7_1(X31),X31)
& occurrence_of(esk8_1(X31),tptp4)
& next_subocc(esk7_1(X31),esk8_1(X31),tptp0)
& ( occurrence_of(esk9_1(X31),tptp1)
| occurrence_of(esk9_1(X31),tptp2) )
& next_subocc(esk8_1(X31),esk9_1(X31),tptp0)
& leaf_occ(esk9_1(X31),X31) ) ),
inference(skolemize,[status(esa)],[134]) ).
fof(136,plain,
! [X31] :
( ( occurrence_of(esk7_1(X31),tptp3)
| ~ occurrence_of(X31,tptp0) )
& ( root_occ(esk7_1(X31),X31)
| ~ occurrence_of(X31,tptp0) )
& ( occurrence_of(esk8_1(X31),tptp4)
| ~ occurrence_of(X31,tptp0) )
& ( next_subocc(esk7_1(X31),esk8_1(X31),tptp0)
| ~ occurrence_of(X31,tptp0) )
& ( occurrence_of(esk9_1(X31),tptp1)
| occurrence_of(esk9_1(X31),tptp2)
| ~ occurrence_of(X31,tptp0) )
& ( next_subocc(esk8_1(X31),esk9_1(X31),tptp0)
| ~ occurrence_of(X31,tptp0) )
& ( leaf_occ(esk9_1(X31),X31)
| ~ occurrence_of(X31,tptp0) ) ),
inference(distribute,[status(thm)],[135]) ).
cnf(137,plain,
( leaf_occ(esk9_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[136]) ).
fof(174,plain,
! [X66,X67,X68] :
( ~ occurrence_of(X66,X67)
| ~ occurrence_of(X66,X68)
| X67 = X68 ),
inference(fof_nnf,[status(thm)],[23]) ).
fof(175,plain,
! [X69,X70,X71] :
( ~ occurrence_of(X69,X70)
| ~ occurrence_of(X69,X71)
| X70 = X71 ),
inference(variable_rename,[status(thm)],[174]) ).
cnf(176,plain,
( X1 = X2
| ~ occurrence_of(X3,X2)
| ~ occurrence_of(X3,X1) ),
inference(split_conjunct,[status(thm)],[175]) ).
fof(241,plain,
! [X117,X118] :
( ( ~ leaf_occ(X117,X118)
| ? [X119] :
( occurrence_of(X118,X119)
& subactivity_occurrence(X117,X118)
& leaf(X117,X119) ) )
& ( ! [X119] :
( ~ occurrence_of(X118,X119)
| ~ subactivity_occurrence(X117,X118)
| ~ leaf(X117,X119) )
| leaf_occ(X117,X118) ) ),
inference(fof_nnf,[status(thm)],[41]) ).
fof(242,plain,
! [X120,X121] :
( ( ~ leaf_occ(X120,X121)
| ? [X122] :
( occurrence_of(X121,X122)
& subactivity_occurrence(X120,X121)
& leaf(X120,X122) ) )
& ( ! [X123] :
( ~ occurrence_of(X121,X123)
| ~ subactivity_occurrence(X120,X121)
| ~ leaf(X120,X123) )
| leaf_occ(X120,X121) ) ),
inference(variable_rename,[status(thm)],[241]) ).
fof(243,plain,
! [X120,X121] :
( ( ~ leaf_occ(X120,X121)
| ( occurrence_of(X121,esk13_2(X120,X121))
& subactivity_occurrence(X120,X121)
& leaf(X120,esk13_2(X120,X121)) ) )
& ( ! [X123] :
( ~ occurrence_of(X121,X123)
| ~ subactivity_occurrence(X120,X121)
| ~ leaf(X120,X123) )
| leaf_occ(X120,X121) ) ),
inference(skolemize,[status(esa)],[242]) ).
fof(244,plain,
! [X120,X121,X123] :
( ( ~ occurrence_of(X121,X123)
| ~ subactivity_occurrence(X120,X121)
| ~ leaf(X120,X123)
| leaf_occ(X120,X121) )
& ( ~ leaf_occ(X120,X121)
| ( occurrence_of(X121,esk13_2(X120,X121))
& subactivity_occurrence(X120,X121)
& leaf(X120,esk13_2(X120,X121)) ) ) ),
inference(shift_quantors,[status(thm)],[243]) ).
fof(245,plain,
! [X120,X121,X123] :
( ( ~ occurrence_of(X121,X123)
| ~ subactivity_occurrence(X120,X121)
| ~ leaf(X120,X123)
| leaf_occ(X120,X121) )
& ( occurrence_of(X121,esk13_2(X120,X121))
| ~ leaf_occ(X120,X121) )
& ( subactivity_occurrence(X120,X121)
| ~ leaf_occ(X120,X121) )
& ( leaf(X120,esk13_2(X120,X121))
| ~ leaf_occ(X120,X121) ) ),
inference(distribute,[status(thm)],[244]) ).
cnf(246,plain,
( leaf(X1,esk13_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[245]) ).
cnf(248,plain,
( occurrence_of(X2,esk13_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[245]) ).
cnf(250,plain,
tptp1 != tptp2,
inference(split_conjunct,[status(thm)],[42]) ).
fof(320,negated_conjecture,
? [X166] :
( occurrence_of(X166,tptp0)
& ! [X167,X168] :
( ~ leaf_occ(X168,X166)
| ( occurrence_of(X168,tptp1)
& ? [X169] :
( occurrence_of(X169,tptp2)
& min_precedes(X167,X169,tptp0) ) )
| ( occurrence_of(X168,tptp2)
& ? [X170] :
( occurrence_of(X170,tptp1)
& min_precedes(X167,X170,tptp0) ) ) ) ),
inference(fof_nnf,[status(thm)],[64]) ).
fof(321,negated_conjecture,
? [X171] :
( occurrence_of(X171,tptp0)
& ! [X172,X173] :
( ~ leaf_occ(X173,X171)
| ( occurrence_of(X173,tptp1)
& ? [X174] :
( occurrence_of(X174,tptp2)
& min_precedes(X172,X174,tptp0) ) )
| ( occurrence_of(X173,tptp2)
& ? [X175] :
( occurrence_of(X175,tptp1)
& min_precedes(X172,X175,tptp0) ) ) ) ),
inference(variable_rename,[status(thm)],[320]) ).
fof(322,negated_conjecture,
( occurrence_of(esk20_0,tptp0)
& ! [X172,X173] :
( ~ leaf_occ(X173,esk20_0)
| ( occurrence_of(X173,tptp1)
& occurrence_of(esk21_2(X172,X173),tptp2)
& min_precedes(X172,esk21_2(X172,X173),tptp0) )
| ( occurrence_of(X173,tptp2)
& occurrence_of(esk22_2(X172,X173),tptp1)
& min_precedes(X172,esk22_2(X172,X173),tptp0) ) ) ),
inference(skolemize,[status(esa)],[321]) ).
fof(323,negated_conjecture,
! [X172,X173] :
( ( ~ leaf_occ(X173,esk20_0)
| ( occurrence_of(X173,tptp1)
& occurrence_of(esk21_2(X172,X173),tptp2)
& min_precedes(X172,esk21_2(X172,X173),tptp0) )
| ( occurrence_of(X173,tptp2)
& occurrence_of(esk22_2(X172,X173),tptp1)
& min_precedes(X172,esk22_2(X172,X173),tptp0) ) )
& occurrence_of(esk20_0,tptp0) ),
inference(shift_quantors,[status(thm)],[322]) ).
fof(324,negated_conjecture,
! [X172,X173] :
( ( occurrence_of(X173,tptp2)
| occurrence_of(X173,tptp1)
| ~ leaf_occ(X173,esk20_0) )
& ( occurrence_of(esk22_2(X172,X173),tptp1)
| occurrence_of(X173,tptp1)
| ~ leaf_occ(X173,esk20_0) )
& ( min_precedes(X172,esk22_2(X172,X173),tptp0)
| occurrence_of(X173,tptp1)
| ~ leaf_occ(X173,esk20_0) )
& ( occurrence_of(X173,tptp2)
| occurrence_of(esk21_2(X172,X173),tptp2)
| ~ leaf_occ(X173,esk20_0) )
& ( occurrence_of(esk22_2(X172,X173),tptp1)
| occurrence_of(esk21_2(X172,X173),tptp2)
| ~ leaf_occ(X173,esk20_0) )
& ( min_precedes(X172,esk22_2(X172,X173),tptp0)
| occurrence_of(esk21_2(X172,X173),tptp2)
| ~ leaf_occ(X173,esk20_0) )
& ( occurrence_of(X173,tptp2)
| min_precedes(X172,esk21_2(X172,X173),tptp0)
| ~ leaf_occ(X173,esk20_0) )
& ( occurrence_of(esk22_2(X172,X173),tptp1)
| min_precedes(X172,esk21_2(X172,X173),tptp0)
| ~ leaf_occ(X173,esk20_0) )
& ( min_precedes(X172,esk22_2(X172,X173),tptp0)
| min_precedes(X172,esk21_2(X172,X173),tptp0)
| ~ leaf_occ(X173,esk20_0) )
& occurrence_of(esk20_0,tptp0) ),
inference(distribute,[status(thm)],[323]) ).
cnf(325,negated_conjecture,
occurrence_of(esk20_0,tptp0),
inference(split_conjunct,[status(thm)],[324]) ).
cnf(328,negated_conjecture,
( min_precedes(X2,esk21_2(X2,X1),tptp0)
| occurrence_of(X1,tptp2)
| ~ leaf_occ(X1,esk20_0) ),
inference(split_conjunct,[status(thm)],[324]) ).
cnf(332,negated_conjecture,
( occurrence_of(X1,tptp1)
| min_precedes(X2,esk22_2(X2,X1),tptp0)
| ~ leaf_occ(X1,esk20_0) ),
inference(split_conjunct,[status(thm)],[324]) ).
cnf(366,negated_conjecture,
( X1 = tptp0
| ~ occurrence_of(esk20_0,X1) ),
inference(spm,[status(thm)],[176,325,theory(equality)]) ).
cnf(423,negated_conjecture,
( occurrence_of(X2,tptp1)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk20_0) ),
inference(spm,[status(thm)],[112,332,theory(equality)]) ).
cnf(428,negated_conjecture,
( occurrence_of(X2,tptp2)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk20_0) ),
inference(spm,[status(thm)],[112,328,theory(equality)]) ).
cnf(646,negated_conjecture,
( esk13_2(X1,esk20_0) = tptp0
| ~ leaf_occ(X1,esk20_0) ),
inference(spm,[status(thm)],[366,248,theory(equality)]) ).
cnf(750,negated_conjecture,
( leaf(X1,tptp0)
| ~ leaf_occ(X1,esk20_0) ),
inference(spm,[status(thm)],[246,646,theory(equality)]) ).
cnf(775,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk20_0,tptp0) ),
inference(spm,[status(thm)],[423,137,theory(equality)]) ).
cnf(776,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[775,325,theory(equality)]) ).
cnf(777,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[776,theory(equality)]) ).
cnf(779,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| ~ leaf_occ(X1,esk20_0) ),
inference(spm,[status(thm)],[777,750,theory(equality)]) ).
cnf(780,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| ~ occurrence_of(esk20_0,tptp0) ),
inference(spm,[status(thm)],[779,137,theory(equality)]) ).
cnf(781,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp1)
| $false ),
inference(rw,[status(thm)],[780,325,theory(equality)]) ).
cnf(782,negated_conjecture,
occurrence_of(esk9_1(esk20_0),tptp1),
inference(cn,[status(thm)],[781,theory(equality)]) ).
cnf(787,negated_conjecture,
( X1 = tptp1
| ~ occurrence_of(esk9_1(esk20_0),X1) ),
inference(spm,[status(thm)],[176,782,theory(equality)]) ).
cnf(921,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk20_0,tptp0) ),
inference(spm,[status(thm)],[428,137,theory(equality)]) ).
cnf(922,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[921,325,theory(equality)]) ).
cnf(923,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[922,theory(equality)]) ).
cnf(925,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| ~ leaf_occ(X1,esk20_0) ),
inference(spm,[status(thm)],[923,750,theory(equality)]) ).
cnf(926,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| ~ occurrence_of(esk20_0,tptp0) ),
inference(spm,[status(thm)],[925,137,theory(equality)]) ).
cnf(927,negated_conjecture,
( occurrence_of(esk9_1(esk20_0),tptp2)
| $false ),
inference(rw,[status(thm)],[926,325,theory(equality)]) ).
cnf(928,negated_conjecture,
occurrence_of(esk9_1(esk20_0),tptp2),
inference(cn,[status(thm)],[927,theory(equality)]) ).
cnf(936,negated_conjecture,
tptp2 = tptp1,
inference(spm,[status(thm)],[787,928,theory(equality)]) ).
cnf(950,negated_conjecture,
$false,
inference(sr,[status(thm)],[936,250,theory(equality)]) ).
cnf(951,negated_conjecture,
$false,
950,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/PRO/PRO010+3.p
% --creating new selector for []
% -running prover on /tmp/tmpdFSU0l/sel_PRO010+3.p_1 with time limit 29
% -prover status Theorem
% Problem PRO010+3.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/PRO/PRO010+3.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/PRO/PRO010+3.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
%
%------------------------------------------------------------------------------