%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : PRO010+1 : 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:36:57 EST 2010
% Result : Theorem 0.22s
% Output : CNFRefutation 0.22s
% 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(6,axiom,
! [X16,X17] :
( leaf(X16,X17)
<=> ( ( root(X16,X17)
| ? [X18] : min_precedes(X18,X16,X17) )
& ~ ? [X19] : min_precedes(X16,X19,X17) ) ),
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',sos_21) ).
fof(12,axiom,
tptp1 != tptp2,
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',sos_47) ).
fof(19,axiom,
! [X38,X39,X40] :
( ( occurrence_of(X38,X39)
& occurrence_of(X38,X40) )
=> X39 = X40 ),
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',sos_02) ).
fof(33,axiom,
! [X69] :
( occurrence_of(X69,tptp0)
=> ? [X70,X71,X72] :
( occurrence_of(X70,tptp3)
& root_occ(X70,X69)
& occurrence_of(X71,tptp4)
& next_subocc(X70,X71,tptp0)
& ( occurrence_of(X72,tptp1)
| occurrence_of(X72,tptp2) )
& next_subocc(X71,X72,tptp0)
& leaf_occ(X72,X69) ) ),
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',sos_35) ).
fof(34,axiom,
! [X73,X74] :
( leaf_occ(X73,X74)
<=> ? [X75] :
( occurrence_of(X74,X75)
& subactivity_occurrence(X73,X74)
& leaf(X73,X75) ) ),
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',sos_34) ).
fof(49,conjecture,
! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( leaf_occ(X112,X110)
& ( occurrence_of(X112,tptp1)
=> ~ ? [X113] :
( occurrence_of(X113,tptp2)
& min_precedes(X111,X113,tptp0) ) )
& ( occurrence_of(X112,tptp2)
=> ~ ? [X114] :
( occurrence_of(X114,tptp1)
& min_precedes(X111,X114,tptp0) ) ) ) ),
file('/tmp/tmpZdwf1b/sel_PRO010+1.p_1',goals) ).
fof(50,negated_conjecture,
~ ! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( leaf_occ(X112,X110)
& ( occurrence_of(X112,tptp1)
=> ~ ? [X113] :
( occurrence_of(X113,tptp2)
& min_precedes(X111,X113,tptp0) ) )
& ( occurrence_of(X112,tptp2)
=> ~ ? [X114] :
( occurrence_of(X114,tptp1)
& min_precedes(X111,X114,tptp0) ) ) ) ),
inference(assume_negation,[status(cth)],[49]) ).
fof(85,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)],[6]) ).
fof(86,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)],[85]) ).
fof(87,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)],[86]) ).
fof(88,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)],[87]) ).
fof(89,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)],[88]) ).
cnf(91,plain,
( ~ leaf(X1,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[89]) ).
cnf(119,plain,
tptp1 != tptp2,
inference(split_conjunct,[status(thm)],[12]) ).
fof(130,plain,
! [X38,X39,X40] :
( ~ occurrence_of(X38,X39)
| ~ occurrence_of(X38,X40)
| X39 = X40 ),
inference(fof_nnf,[status(thm)],[19]) ).
fof(131,plain,
! [X41,X42,X43] :
( ~ occurrence_of(X41,X42)
| ~ occurrence_of(X41,X43)
| X42 = X43 ),
inference(variable_rename,[status(thm)],[130]) ).
cnf(132,plain,
( X1 = X2
| ~ occurrence_of(X3,X2)
| ~ occurrence_of(X3,X1) ),
inference(split_conjunct,[status(thm)],[131]) ).
fof(180,plain,
! [X69] :
( ~ occurrence_of(X69,tptp0)
| ? [X70,X71,X72] :
( occurrence_of(X70,tptp3)
& root_occ(X70,X69)
& occurrence_of(X71,tptp4)
& next_subocc(X70,X71,tptp0)
& ( occurrence_of(X72,tptp1)
| occurrence_of(X72,tptp2) )
& next_subocc(X71,X72,tptp0)
& leaf_occ(X72,X69) ) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(181,plain,
! [X73] :
( ~ occurrence_of(X73,tptp0)
| ? [X74,X75,X76] :
( occurrence_of(X74,tptp3)
& root_occ(X74,X73)
& occurrence_of(X75,tptp4)
& next_subocc(X74,X75,tptp0)
& ( occurrence_of(X76,tptp1)
| occurrence_of(X76,tptp2) )
& next_subocc(X75,X76,tptp0)
& leaf_occ(X76,X73) ) ),
inference(variable_rename,[status(thm)],[180]) ).
fof(182,plain,
! [X73] :
( ~ occurrence_of(X73,tptp0)
| ( occurrence_of(esk10_1(X73),tptp3)
& root_occ(esk10_1(X73),X73)
& occurrence_of(esk11_1(X73),tptp4)
& next_subocc(esk10_1(X73),esk11_1(X73),tptp0)
& ( occurrence_of(esk12_1(X73),tptp1)
| occurrence_of(esk12_1(X73),tptp2) )
& next_subocc(esk11_1(X73),esk12_1(X73),tptp0)
& leaf_occ(esk12_1(X73),X73) ) ),
inference(skolemize,[status(esa)],[181]) ).
fof(183,plain,
! [X73] :
( ( occurrence_of(esk10_1(X73),tptp3)
| ~ occurrence_of(X73,tptp0) )
& ( root_occ(esk10_1(X73),X73)
| ~ occurrence_of(X73,tptp0) )
& ( occurrence_of(esk11_1(X73),tptp4)
| ~ occurrence_of(X73,tptp0) )
& ( next_subocc(esk10_1(X73),esk11_1(X73),tptp0)
| ~ occurrence_of(X73,tptp0) )
& ( occurrence_of(esk12_1(X73),tptp1)
| occurrence_of(esk12_1(X73),tptp2)
| ~ occurrence_of(X73,tptp0) )
& ( next_subocc(esk11_1(X73),esk12_1(X73),tptp0)
| ~ occurrence_of(X73,tptp0) )
& ( leaf_occ(esk12_1(X73),X73)
| ~ occurrence_of(X73,tptp0) ) ),
inference(distribute,[status(thm)],[182]) ).
cnf(184,plain,
( leaf_occ(esk12_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[183]) ).
fof(191,plain,
! [X73,X74] :
( ( ~ leaf_occ(X73,X74)
| ? [X75] :
( occurrence_of(X74,X75)
& subactivity_occurrence(X73,X74)
& leaf(X73,X75) ) )
& ( ! [X75] :
( ~ occurrence_of(X74,X75)
| ~ subactivity_occurrence(X73,X74)
| ~ leaf(X73,X75) )
| leaf_occ(X73,X74) ) ),
inference(fof_nnf,[status(thm)],[34]) ).
fof(192,plain,
! [X76,X77] :
( ( ~ leaf_occ(X76,X77)
| ? [X78] :
( occurrence_of(X77,X78)
& subactivity_occurrence(X76,X77)
& leaf(X76,X78) ) )
& ( ! [X79] :
( ~ occurrence_of(X77,X79)
| ~ subactivity_occurrence(X76,X77)
| ~ leaf(X76,X79) )
| leaf_occ(X76,X77) ) ),
inference(variable_rename,[status(thm)],[191]) ).
fof(193,plain,
! [X76,X77] :
( ( ~ leaf_occ(X76,X77)
| ( occurrence_of(X77,esk13_2(X76,X77))
& subactivity_occurrence(X76,X77)
& leaf(X76,esk13_2(X76,X77)) ) )
& ( ! [X79] :
( ~ occurrence_of(X77,X79)
| ~ subactivity_occurrence(X76,X77)
| ~ leaf(X76,X79) )
| leaf_occ(X76,X77) ) ),
inference(skolemize,[status(esa)],[192]) ).
fof(194,plain,
! [X76,X77,X79] :
( ( ~ occurrence_of(X77,X79)
| ~ subactivity_occurrence(X76,X77)
| ~ leaf(X76,X79)
| leaf_occ(X76,X77) )
& ( ~ leaf_occ(X76,X77)
| ( occurrence_of(X77,esk13_2(X76,X77))
& subactivity_occurrence(X76,X77)
& leaf(X76,esk13_2(X76,X77)) ) ) ),
inference(shift_quantors,[status(thm)],[193]) ).
fof(195,plain,
! [X76,X77,X79] :
( ( ~ occurrence_of(X77,X79)
| ~ subactivity_occurrence(X76,X77)
| ~ leaf(X76,X79)
| leaf_occ(X76,X77) )
& ( occurrence_of(X77,esk13_2(X76,X77))
| ~ leaf_occ(X76,X77) )
& ( subactivity_occurrence(X76,X77)
| ~ leaf_occ(X76,X77) )
& ( leaf(X76,esk13_2(X76,X77))
| ~ leaf_occ(X76,X77) ) ),
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(253,negated_conjecture,
? [X110] :
( occurrence_of(X110,tptp0)
& ! [X111,X112] :
( ~ leaf_occ(X112,X110)
| ( occurrence_of(X112,tptp1)
& ? [X113] :
( occurrence_of(X113,tptp2)
& min_precedes(X111,X113,tptp0) ) )
| ( occurrence_of(X112,tptp2)
& ? [X114] :
( occurrence_of(X114,tptp1)
& min_precedes(X111,X114,tptp0) ) ) ) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(254,negated_conjecture,
? [X115] :
( occurrence_of(X115,tptp0)
& ! [X116,X117] :
( ~ leaf_occ(X117,X115)
| ( occurrence_of(X117,tptp1)
& ? [X118] :
( occurrence_of(X118,tptp2)
& min_precedes(X116,X118,tptp0) ) )
| ( occurrence_of(X117,tptp2)
& ? [X119] :
( occurrence_of(X119,tptp1)
& min_precedes(X116,X119,tptp0) ) ) ) ),
inference(variable_rename,[status(thm)],[253]) ).
fof(255,negated_conjecture,
( occurrence_of(esk19_0,tptp0)
& ! [X116,X117] :
( ~ leaf_occ(X117,esk19_0)
| ( occurrence_of(X117,tptp1)
& occurrence_of(esk20_2(X116,X117),tptp2)
& min_precedes(X116,esk20_2(X116,X117),tptp0) )
| ( occurrence_of(X117,tptp2)
& occurrence_of(esk21_2(X116,X117),tptp1)
& min_precedes(X116,esk21_2(X116,X117),tptp0) ) ) ),
inference(skolemize,[status(esa)],[254]) ).
fof(256,negated_conjecture,
! [X116,X117] :
( ( ~ leaf_occ(X117,esk19_0)
| ( occurrence_of(X117,tptp1)
& occurrence_of(esk20_2(X116,X117),tptp2)
& min_precedes(X116,esk20_2(X116,X117),tptp0) )
| ( occurrence_of(X117,tptp2)
& occurrence_of(esk21_2(X116,X117),tptp1)
& min_precedes(X116,esk21_2(X116,X117),tptp0) ) )
& occurrence_of(esk19_0,tptp0) ),
inference(shift_quantors,[status(thm)],[255]) ).
fof(257,negated_conjecture,
! [X116,X117] :
( ( occurrence_of(X117,tptp2)
| occurrence_of(X117,tptp1)
| ~ leaf_occ(X117,esk19_0) )
& ( occurrence_of(esk21_2(X116,X117),tptp1)
| occurrence_of(X117,tptp1)
| ~ leaf_occ(X117,esk19_0) )
& ( min_precedes(X116,esk21_2(X116,X117),tptp0)
| occurrence_of(X117,tptp1)
| ~ leaf_occ(X117,esk19_0) )
& ( occurrence_of(X117,tptp2)
| occurrence_of(esk20_2(X116,X117),tptp2)
| ~ leaf_occ(X117,esk19_0) )
& ( occurrence_of(esk21_2(X116,X117),tptp1)
| occurrence_of(esk20_2(X116,X117),tptp2)
| ~ leaf_occ(X117,esk19_0) )
& ( min_precedes(X116,esk21_2(X116,X117),tptp0)
| occurrence_of(esk20_2(X116,X117),tptp2)
| ~ leaf_occ(X117,esk19_0) )
& ( occurrence_of(X117,tptp2)
| min_precedes(X116,esk20_2(X116,X117),tptp0)
| ~ leaf_occ(X117,esk19_0) )
& ( occurrence_of(esk21_2(X116,X117),tptp1)
| min_precedes(X116,esk20_2(X116,X117),tptp0)
| ~ leaf_occ(X117,esk19_0) )
& ( min_precedes(X116,esk21_2(X116,X117),tptp0)
| min_precedes(X116,esk20_2(X116,X117),tptp0)
| ~ leaf_occ(X117,esk19_0) )
& occurrence_of(esk19_0,tptp0) ),
inference(distribute,[status(thm)],[256]) ).
cnf(258,negated_conjecture,
occurrence_of(esk19_0,tptp0),
inference(split_conjunct,[status(thm)],[257]) ).
cnf(261,negated_conjecture,
( min_precedes(X2,esk20_2(X2,X1),tptp0)
| occurrence_of(X1,tptp2)
| ~ leaf_occ(X1,esk19_0) ),
inference(split_conjunct,[status(thm)],[257]) ).
cnf(265,negated_conjecture,
( occurrence_of(X1,tptp1)
| min_precedes(X2,esk21_2(X2,X1),tptp0)
| ~ leaf_occ(X1,esk19_0) ),
inference(split_conjunct,[status(thm)],[257]) ).
cnf(299,negated_conjecture,
( X1 = tptp0
| ~ occurrence_of(esk19_0,X1) ),
inference(spm,[status(thm)],[132,258,theory(equality)]) ).
cnf(347,negated_conjecture,
( occurrence_of(X2,tptp2)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk19_0) ),
inference(spm,[status(thm)],[91,261,theory(equality)]) ).
cnf(355,negated_conjecture,
( occurrence_of(X2,tptp1)
| ~ leaf(X1,tptp0)
| ~ leaf_occ(X2,esk19_0) ),
inference(spm,[status(thm)],[91,265,theory(equality)]) ).
cnf(506,negated_conjecture,
( esk13_2(X1,esk19_0) = tptp0
| ~ leaf_occ(X1,esk19_0) ),
inference(spm,[status(thm)],[299,198,theory(equality)]) ).
cnf(606,negated_conjecture,
( leaf(X1,tptp0)
| ~ leaf_occ(X1,esk19_0) ),
inference(spm,[status(thm)],[196,506,theory(equality)]) ).
cnf(628,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk19_0,tptp0) ),
inference(spm,[status(thm)],[347,184,theory(equality)]) ).
cnf(629,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[628,258,theory(equality)]) ).
cnf(630,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[629,theory(equality)]) ).
cnf(632,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| ~ leaf_occ(X1,esk19_0) ),
inference(spm,[status(thm)],[630,606,theory(equality)]) ).
cnf(633,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| ~ occurrence_of(esk19_0,tptp0) ),
inference(spm,[status(thm)],[632,184,theory(equality)]) ).
cnf(634,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp2)
| $false ),
inference(rw,[status(thm)],[633,258,theory(equality)]) ).
cnf(635,negated_conjecture,
occurrence_of(esk12_1(esk19_0),tptp2),
inference(cn,[status(thm)],[634,theory(equality)]) ).
cnf(640,negated_conjecture,
( X1 = tptp2
| ~ occurrence_of(esk12_1(esk19_0),X1) ),
inference(spm,[status(thm)],[132,635,theory(equality)]) ).
cnf(749,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| ~ leaf(X1,tptp0)
| ~ occurrence_of(esk19_0,tptp0) ),
inference(spm,[status(thm)],[355,184,theory(equality)]) ).
cnf(750,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| ~ leaf(X1,tptp0)
| $false ),
inference(rw,[status(thm)],[749,258,theory(equality)]) ).
cnf(751,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| ~ leaf(X1,tptp0) ),
inference(cn,[status(thm)],[750,theory(equality)]) ).
cnf(753,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| ~ leaf_occ(X1,esk19_0) ),
inference(spm,[status(thm)],[751,606,theory(equality)]) ).
cnf(754,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| ~ occurrence_of(esk19_0,tptp0) ),
inference(spm,[status(thm)],[753,184,theory(equality)]) ).
cnf(755,negated_conjecture,
( occurrence_of(esk12_1(esk19_0),tptp1)
| $false ),
inference(rw,[status(thm)],[754,258,theory(equality)]) ).
cnf(756,negated_conjecture,
occurrence_of(esk12_1(esk19_0),tptp1),
inference(cn,[status(thm)],[755,theory(equality)]) ).
cnf(764,negated_conjecture,
tptp1 = tptp2,
inference(spm,[status(thm)],[640,756,theory(equality)]) ).
cnf(777,negated_conjecture,
$false,
inference(sr,[status(thm)],[764,119,theory(equality)]) ).
cnf(778,negated_conjecture,
$false,
777,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/PRO/PRO010+1.p
% --creating new selector for []
% -running prover on /tmp/tmpZdwf1b/sel_PRO010+1.p_1 with time limit 29
% -prover status Theorem
% Problem PRO010+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/PRO/PRO010+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/PRO/PRO010+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
%
%------------------------------------------------------------------------------