%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : PRO012+4 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art02.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:38:40 EST 2010
% Result : Theorem 65.27s
% Output : CNFRefutation 65.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 21
% Syntax : Number of formulae : 214 ( 41 unt; 0 def)
% Number of atoms : 749 ( 56 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 851 ( 316 ~; 364 |; 146 &)
% ( 5 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 376 ( 8 sgn 233 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1,X2,X3] :
( min_precedes(X1,X2,X3)
=> precedes(X1,X2) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_24) ).
fof(3,axiom,
! [X7,X8] :
( ( occurrence_of(X8,X7)
& ~ atomic(X7) )
=> ? [X9] :
( root(X9,X7)
& subactivity_occurrence(X9,X8) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos) ).
fof(4,axiom,
! [X10,X11,X12,X13] :
( ( min_precedes(X10,X11,X12)
& occurrence_of(X13,X12)
& subactivity_occurrence(X11,X13) )
=> subactivity_occurrence(X10,X13) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_27) ).
fof(5,axiom,
! [X14,X15] :
( earlier(X14,X15)
=> ~ earlier(X15,X14) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_20) ).
fof(6,axiom,
! [X16,X17] :
( precedes(X16,X17)
<=> ( earlier(X16,X17)
& legal(X17) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_21) ).
fof(7,axiom,
! [X18,X19,X20] :
( min_precedes(X18,X19,X20)
=> ~ root(X19,X20) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_22) ).
fof(8,axiom,
! [X21,X22,X23] :
( min_precedes(X21,X22,X23)
=> ? [X24] :
( root(X24,X23)
& min_precedes(X24,X22,X23) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_23) ).
fof(10,axiom,
! [X29,X30,X31,X32] :
( ( occurrence_of(X31,X32)
& root_occ(X29,X31)
& root_occ(X30,X31) )
=> X29 = X30 ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_29) ).
fof(20,axiom,
! [X51,X52,X53] :
( min_precedes(X52,X53,X51)
=> ? [X54] :
( occurrence_of(X54,X51)
& subactivity_occurrence(X52,X54)
& subactivity_occurrence(X53,X54) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_06) ).
fof(22,axiom,
! [X58,X59,X60,X61] :
( ( occurrence_of(X59,X58)
& arboreal(X60)
& arboreal(X61)
& subactivity_occurrence(X60,X59)
& subactivity_occurrence(X61,X59) )
=> ( min_precedes(X60,X61,X58)
| min_precedes(X61,X60,X58)
| X60 = X61 ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_04) ).
fof(26,axiom,
! [X65] :
( occurrence_of(X65,tptp0)
=> ? [X66,X67,X68] :
( occurrence_of(X66,tptp3)
& root_occ(X66,X65)
& occurrence_of(X67,tptp4)
& min_precedes(X66,X67,tptp0)
& ( occurrence_of(X68,tptp2)
| occurrence_of(X68,tptp1) )
& min_precedes(X67,X68,tptp0)
& ! [X69] :
( min_precedes(X66,X69,tptp0)
=> ( X69 = X67
| X69 = X68 ) ) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_32) ).
fof(27,axiom,
! [X70,X71,X72,X73] :
( ( min_precedes(X70,X71,X73)
& min_precedes(X70,X72,X73)
& precedes(X71,X72) )
=> min_precedes(X71,X72,X73) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_31) ).
fof(28,axiom,
! [X74,X75,X76] :
( ( earlier(X74,X75)
& earlier(X75,X76) )
=> earlier(X74,X76) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_30) ).
fof(32,axiom,
~ atomic(tptp0),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_34) ).
fof(34,axiom,
atomic(tptp3),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_38) ).
fof(35,axiom,
! [X77,X78,X79] :
( next_subocc(X77,X78,X79)
<=> ( min_precedes(X77,X78,X79)
& ~ ? [X80] :
( min_precedes(X77,X80,X79)
& min_precedes(X80,X78,X79) ) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_26) ).
fof(36,axiom,
! [X81,X82] :
( root_occ(X81,X82)
<=> ? [X83] :
( occurrence_of(X82,X83)
& subactivity_occurrence(X81,X82)
& root(X81,X83) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_19) ).
fof(40,axiom,
! [X93] :
( legal(X93)
=> arboreal(X93) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_13) ).
fof(42,axiom,
! [X96,X97] :
( leaf(X96,X97)
<=> ( ( root(X96,X97)
| ? [X98] : min_precedes(X98,X96,X97) )
& ~ ? [X99] : min_precedes(X96,X99,X97) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_15) ).
fof(45,axiom,
! [X105,X106] :
( occurrence_of(X105,X106)
=> ( arboreal(X105)
<=> atomic(X106) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',sos_16) ).
fof(46,conjecture,
! [X107] :
( occurrence_of(X107,tptp0)
=> ? [X108,X109] :
( occurrence_of(X108,tptp3)
& root_occ(X108,X107)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& min_precedes(X108,X109,tptp0) ) ),
file('/tmp/tmpPz7R2e/sel_PRO012+4.p_2',goals) ).
fof(47,negated_conjecture,
~ ! [X107] :
( occurrence_of(X107,tptp0)
=> ? [X108,X109] :
( occurrence_of(X108,tptp3)
& root_occ(X108,X107)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& min_precedes(X108,X109,tptp0) ) ),
inference(assume_negation,[status(cth)],[46]) ).
fof(48,plain,
! [X7,X8] :
( ( occurrence_of(X8,X7)
& ~ atomic(X7) )
=> ? [X9] :
( root(X9,X7)
& subactivity_occurrence(X9,X8) ) ),
inference(fof_simplification,[status(thm)],[3,theory(equality)]) ).
fof(49,plain,
! [X14,X15] :
( earlier(X14,X15)
=> ~ earlier(X15,X14) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(50,plain,
! [X18,X19,X20] :
( min_precedes(X18,X19,X20)
=> ~ root(X19,X20) ),
inference(fof_simplification,[status(thm)],[7,theory(equality)]) ).
fof(54,plain,
~ atomic(tptp0),
inference(fof_simplification,[status(thm)],[32,theory(equality)]) ).
fof(55,plain,
! [X1,X2,X3] :
( ~ min_precedes(X1,X2,X3)
| precedes(X1,X2) ),
inference(fof_nnf,[status(thm)],[1]) ).
fof(56,plain,
! [X4,X5,X6] :
( ~ min_precedes(X4,X5,X6)
| precedes(X4,X5) ),
inference(variable_rename,[status(thm)],[55]) ).
cnf(57,plain,
( precedes(X1,X2)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[56]) ).
fof(63,plain,
! [X7,X8] :
( ~ occurrence_of(X8,X7)
| atomic(X7)
| ? [X9] :
( root(X9,X7)
& subactivity_occurrence(X9,X8) ) ),
inference(fof_nnf,[status(thm)],[48]) ).
fof(64,plain,
! [X10,X11] :
( ~ occurrence_of(X11,X10)
| atomic(X10)
| ? [X12] :
( root(X12,X10)
& subactivity_occurrence(X12,X11) ) ),
inference(variable_rename,[status(thm)],[63]) ).
fof(65,plain,
! [X10,X11] :
( ~ occurrence_of(X11,X10)
| atomic(X10)
| ( root(esk1_2(X10,X11),X10)
& subactivity_occurrence(esk1_2(X10,X11),X11) ) ),
inference(skolemize,[status(esa)],[64]) ).
fof(66,plain,
! [X10,X11] :
( ( root(esk1_2(X10,X11),X10)
| ~ occurrence_of(X11,X10)
| atomic(X10) )
& ( subactivity_occurrence(esk1_2(X10,X11),X11)
| ~ occurrence_of(X11,X10)
| atomic(X10) ) ),
inference(distribute,[status(thm)],[65]) ).
cnf(67,plain,
( atomic(X1)
| subactivity_occurrence(esk1_2(X1,X2),X2)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[66]) ).
cnf(68,plain,
( atomic(X1)
| root(esk1_2(X1,X2),X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[66]) ).
fof(69,plain,
! [X10,X11,X12,X13] :
( ~ min_precedes(X10,X11,X12)
| ~ occurrence_of(X13,X12)
| ~ subactivity_occurrence(X11,X13)
| subactivity_occurrence(X10,X13) ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(70,plain,
! [X14,X15,X16,X17] :
( ~ min_precedes(X14,X15,X16)
| ~ occurrence_of(X17,X16)
| ~ subactivity_occurrence(X15,X17)
| subactivity_occurrence(X14,X17) ),
inference(variable_rename,[status(thm)],[69]) ).
cnf(71,plain,
( subactivity_occurrence(X1,X2)
| ~ subactivity_occurrence(X3,X2)
| ~ occurrence_of(X2,X4)
| ~ min_precedes(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[70]) ).
fof(72,plain,
! [X14,X15] :
( ~ earlier(X14,X15)
| ~ earlier(X15,X14) ),
inference(fof_nnf,[status(thm)],[49]) ).
fof(73,plain,
! [X16,X17] :
( ~ earlier(X16,X17)
| ~ earlier(X17,X16) ),
inference(variable_rename,[status(thm)],[72]) ).
cnf(74,plain,
( ~ earlier(X1,X2)
| ~ earlier(X2,X1) ),
inference(split_conjunct,[status(thm)],[73]) ).
fof(75,plain,
! [X16,X17] :
( ( ~ precedes(X16,X17)
| ( earlier(X16,X17)
& legal(X17) ) )
& ( ~ earlier(X16,X17)
| ~ legal(X17)
| precedes(X16,X17) ) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(76,plain,
! [X18,X19] :
( ( ~ precedes(X18,X19)
| ( earlier(X18,X19)
& legal(X19) ) )
& ( ~ earlier(X18,X19)
| ~ legal(X19)
| precedes(X18,X19) ) ),
inference(variable_rename,[status(thm)],[75]) ).
fof(77,plain,
! [X18,X19] :
( ( earlier(X18,X19)
| ~ precedes(X18,X19) )
& ( legal(X19)
| ~ precedes(X18,X19) )
& ( ~ earlier(X18,X19)
| ~ legal(X19)
| precedes(X18,X19) ) ),
inference(distribute,[status(thm)],[76]) ).
cnf(78,plain,
( precedes(X1,X2)
| ~ legal(X2)
| ~ earlier(X1,X2) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(79,plain,
( legal(X2)
| ~ precedes(X1,X2) ),
inference(split_conjunct,[status(thm)],[77]) ).
cnf(80,plain,
( earlier(X1,X2)
| ~ precedes(X1,X2) ),
inference(split_conjunct,[status(thm)],[77]) ).
fof(81,plain,
! [X18,X19,X20] :
( ~ min_precedes(X18,X19,X20)
| ~ root(X19,X20) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(82,plain,
! [X21,X22,X23] :
( ~ min_precedes(X21,X22,X23)
| ~ root(X22,X23) ),
inference(variable_rename,[status(thm)],[81]) ).
cnf(83,plain,
( ~ root(X1,X2)
| ~ min_precedes(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[82]) ).
fof(84,plain,
! [X21,X22,X23] :
( ~ min_precedes(X21,X22,X23)
| ? [X24] :
( root(X24,X23)
& min_precedes(X24,X22,X23) ) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(85,plain,
! [X25,X26,X27] :
( ~ min_precedes(X25,X26,X27)
| ? [X28] :
( root(X28,X27)
& min_precedes(X28,X26,X27) ) ),
inference(variable_rename,[status(thm)],[84]) ).
fof(86,plain,
! [X25,X26,X27] :
( ~ min_precedes(X25,X26,X27)
| ( root(esk2_3(X25,X26,X27),X27)
& min_precedes(esk2_3(X25,X26,X27),X26,X27) ) ),
inference(skolemize,[status(esa)],[85]) ).
fof(87,plain,
! [X25,X26,X27] :
( ( root(esk2_3(X25,X26,X27),X27)
| ~ min_precedes(X25,X26,X27) )
& ( min_precedes(esk2_3(X25,X26,X27),X26,X27)
| ~ min_precedes(X25,X26,X27) ) ),
inference(distribute,[status(thm)],[86]) ).
cnf(88,plain,
( min_precedes(esk2_3(X1,X2,X3),X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[87]) ).
fof(93,plain,
! [X29,X30,X31,X32] :
( ~ occurrence_of(X31,X32)
| ~ root_occ(X29,X31)
| ~ root_occ(X30,X31)
| X29 = X30 ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(94,plain,
! [X33,X34,X35,X36] :
( ~ occurrence_of(X35,X36)
| ~ root_occ(X33,X35)
| ~ root_occ(X34,X35)
| X33 = X34 ),
inference(variable_rename,[status(thm)],[93]) ).
cnf(95,plain,
( X1 = X2
| ~ root_occ(X2,X3)
| ~ root_occ(X1,X3)
| ~ occurrence_of(X3,X4) ),
inference(split_conjunct,[status(thm)],[94]) ).
fof(118,plain,
! [X51,X52,X53] :
( ~ min_precedes(X52,X53,X51)
| ? [X54] :
( occurrence_of(X54,X51)
& subactivity_occurrence(X52,X54)
& subactivity_occurrence(X53,X54) ) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(119,plain,
! [X55,X56,X57] :
( ~ min_precedes(X56,X57,X55)
| ? [X58] :
( occurrence_of(X58,X55)
& subactivity_occurrence(X56,X58)
& subactivity_occurrence(X57,X58) ) ),
inference(variable_rename,[status(thm)],[118]) ).
fof(120,plain,
! [X55,X56,X57] :
( ~ min_precedes(X56,X57,X55)
| ( occurrence_of(esk3_3(X55,X56,X57),X55)
& subactivity_occurrence(X56,esk3_3(X55,X56,X57))
& subactivity_occurrence(X57,esk3_3(X55,X56,X57)) ) ),
inference(skolemize,[status(esa)],[119]) ).
fof(121,plain,
! [X55,X56,X57] :
( ( occurrence_of(esk3_3(X55,X56,X57),X55)
| ~ min_precedes(X56,X57,X55) )
& ( subactivity_occurrence(X56,esk3_3(X55,X56,X57))
| ~ min_precedes(X56,X57,X55) )
& ( subactivity_occurrence(X57,esk3_3(X55,X56,X57))
| ~ min_precedes(X56,X57,X55) ) ),
inference(distribute,[status(thm)],[120]) ).
cnf(122,plain,
( subactivity_occurrence(X2,esk3_3(X3,X1,X2))
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[121]) ).
cnf(123,plain,
( subactivity_occurrence(X1,esk3_3(X3,X1,X2))
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[121]) ).
cnf(124,plain,
( occurrence_of(esk3_3(X3,X1,X2),X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[121]) ).
fof(131,plain,
! [X58,X59,X60,X61] :
( ~ occurrence_of(X59,X58)
| ~ arboreal(X60)
| ~ arboreal(X61)
| ~ subactivity_occurrence(X60,X59)
| ~ subactivity_occurrence(X61,X59)
| min_precedes(X60,X61,X58)
| min_precedes(X61,X60,X58)
| X60 = X61 ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(132,plain,
! [X62,X63,X64,X65] :
( ~ occurrence_of(X63,X62)
| ~ arboreal(X64)
| ~ arboreal(X65)
| ~ subactivity_occurrence(X64,X63)
| ~ subactivity_occurrence(X65,X63)
| min_precedes(X64,X65,X62)
| min_precedes(X65,X64,X62)
| X64 = X65 ),
inference(variable_rename,[status(thm)],[131]) ).
cnf(133,plain,
( X1 = X2
| min_precedes(X2,X1,X3)
| min_precedes(X1,X2,X3)
| ~ subactivity_occurrence(X2,X4)
| ~ subactivity_occurrence(X1,X4)
| ~ arboreal(X2)
| ~ arboreal(X1)
| ~ occurrence_of(X4,X3) ),
inference(split_conjunct,[status(thm)],[132]) ).
fof(142,plain,
! [X65] :
( ~ occurrence_of(X65,tptp0)
| ? [X66,X67,X68] :
( occurrence_of(X66,tptp3)
& root_occ(X66,X65)
& occurrence_of(X67,tptp4)
& min_precedes(X66,X67,tptp0)
& ( occurrence_of(X68,tptp2)
| occurrence_of(X68,tptp1) )
& min_precedes(X67,X68,tptp0)
& ! [X69] :
( ~ min_precedes(X66,X69,tptp0)
| X69 = X67
| X69 = X68 ) ) ),
inference(fof_nnf,[status(thm)],[26]) ).
fof(143,plain,
! [X70] :
( ~ occurrence_of(X70,tptp0)
| ? [X71,X72,X73] :
( occurrence_of(X71,tptp3)
& root_occ(X71,X70)
& occurrence_of(X72,tptp4)
& min_precedes(X71,X72,tptp0)
& ( occurrence_of(X73,tptp2)
| occurrence_of(X73,tptp1) )
& min_precedes(X72,X73,tptp0)
& ! [X74] :
( ~ min_precedes(X71,X74,tptp0)
| X74 = X72
| X74 = X73 ) ) ),
inference(variable_rename,[status(thm)],[142]) ).
fof(144,plain,
! [X70] :
( ~ occurrence_of(X70,tptp0)
| ( occurrence_of(esk6_1(X70),tptp3)
& root_occ(esk6_1(X70),X70)
& occurrence_of(esk7_1(X70),tptp4)
& min_precedes(esk6_1(X70),esk7_1(X70),tptp0)
& ( occurrence_of(esk8_1(X70),tptp2)
| occurrence_of(esk8_1(X70),tptp1) )
& min_precedes(esk7_1(X70),esk8_1(X70),tptp0)
& ! [X74] :
( ~ min_precedes(esk6_1(X70),X74,tptp0)
| X74 = esk7_1(X70)
| X74 = esk8_1(X70) ) ) ),
inference(skolemize,[status(esa)],[143]) ).
fof(145,plain,
! [X70,X74] :
( ( ( ~ min_precedes(esk6_1(X70),X74,tptp0)
| X74 = esk7_1(X70)
| X74 = esk8_1(X70) )
& occurrence_of(esk6_1(X70),tptp3)
& root_occ(esk6_1(X70),X70)
& occurrence_of(esk7_1(X70),tptp4)
& min_precedes(esk6_1(X70),esk7_1(X70),tptp0)
& ( occurrence_of(esk8_1(X70),tptp2)
| occurrence_of(esk8_1(X70),tptp1) )
& min_precedes(esk7_1(X70),esk8_1(X70),tptp0) )
| ~ occurrence_of(X70,tptp0) ),
inference(shift_quantors,[status(thm)],[144]) ).
fof(146,plain,
! [X70,X74] :
( ( ~ min_precedes(esk6_1(X70),X74,tptp0)
| X74 = esk7_1(X70)
| X74 = esk8_1(X70)
| ~ occurrence_of(X70,tptp0) )
& ( occurrence_of(esk6_1(X70),tptp3)
| ~ occurrence_of(X70,tptp0) )
& ( root_occ(esk6_1(X70),X70)
| ~ occurrence_of(X70,tptp0) )
& ( occurrence_of(esk7_1(X70),tptp4)
| ~ occurrence_of(X70,tptp0) )
& ( min_precedes(esk6_1(X70),esk7_1(X70),tptp0)
| ~ occurrence_of(X70,tptp0) )
& ( occurrence_of(esk8_1(X70),tptp2)
| occurrence_of(esk8_1(X70),tptp1)
| ~ occurrence_of(X70,tptp0) )
& ( min_precedes(esk7_1(X70),esk8_1(X70),tptp0)
| ~ occurrence_of(X70,tptp0) ) ),
inference(distribute,[status(thm)],[145]) ).
cnf(147,plain,
( min_precedes(esk7_1(X1),esk8_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(148,plain,
( occurrence_of(esk8_1(X1),tptp1)
| occurrence_of(esk8_1(X1),tptp2)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(149,plain,
( min_precedes(esk6_1(X1),esk7_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(151,plain,
( root_occ(esk6_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(152,plain,
( occurrence_of(esk6_1(X1),tptp3)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(153,plain,
( X2 = esk8_1(X1)
| X2 = esk7_1(X1)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(esk6_1(X1),X2,tptp0) ),
inference(split_conjunct,[status(thm)],[146]) ).
fof(154,plain,
! [X70,X71,X72,X73] :
( ~ min_precedes(X70,X71,X73)
| ~ min_precedes(X70,X72,X73)
| ~ precedes(X71,X72)
| min_precedes(X71,X72,X73) ),
inference(fof_nnf,[status(thm)],[27]) ).
fof(155,plain,
! [X74,X75,X76,X77] :
( ~ min_precedes(X74,X75,X77)
| ~ min_precedes(X74,X76,X77)
| ~ precedes(X75,X76)
| min_precedes(X75,X76,X77) ),
inference(variable_rename,[status(thm)],[154]) ).
cnf(156,plain,
( min_precedes(X1,X2,X3)
| ~ precedes(X1,X2)
| ~ min_precedes(X4,X2,X3)
| ~ min_precedes(X4,X1,X3) ),
inference(split_conjunct,[status(thm)],[155]) ).
fof(157,plain,
! [X74,X75,X76] :
( ~ earlier(X74,X75)
| ~ earlier(X75,X76)
| earlier(X74,X76) ),
inference(fof_nnf,[status(thm)],[28]) ).
fof(158,plain,
! [X77,X78,X79] :
( ~ earlier(X77,X78)
| ~ earlier(X78,X79)
| earlier(X77,X79) ),
inference(variable_rename,[status(thm)],[157]) ).
cnf(159,plain,
( earlier(X1,X2)
| ~ earlier(X3,X2)
| ~ earlier(X1,X3) ),
inference(split_conjunct,[status(thm)],[158]) ).
cnf(163,plain,
~ atomic(tptp0),
inference(split_conjunct,[status(thm)],[54]) ).
cnf(165,plain,
atomic(tptp3),
inference(split_conjunct,[status(thm)],[34]) ).
fof(166,plain,
! [X77,X78,X79] :
( ( ~ next_subocc(X77,X78,X79)
| ( min_precedes(X77,X78,X79)
& ! [X80] :
( ~ min_precedes(X77,X80,X79)
| ~ min_precedes(X80,X78,X79) ) ) )
& ( ~ min_precedes(X77,X78,X79)
| ? [X80] :
( min_precedes(X77,X80,X79)
& min_precedes(X80,X78,X79) )
| next_subocc(X77,X78,X79) ) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(167,plain,
! [X81,X82,X83] :
( ( ~ next_subocc(X81,X82,X83)
| ( min_precedes(X81,X82,X83)
& ! [X84] :
( ~ min_precedes(X81,X84,X83)
| ~ min_precedes(X84,X82,X83) ) ) )
& ( ~ min_precedes(X81,X82,X83)
| ? [X85] :
( min_precedes(X81,X85,X83)
& min_precedes(X85,X82,X83) )
| next_subocc(X81,X82,X83) ) ),
inference(variable_rename,[status(thm)],[166]) ).
fof(168,plain,
! [X81,X82,X83] :
( ( ~ next_subocc(X81,X82,X83)
| ( min_precedes(X81,X82,X83)
& ! [X84] :
( ~ min_precedes(X81,X84,X83)
| ~ min_precedes(X84,X82,X83) ) ) )
& ( ~ min_precedes(X81,X82,X83)
| ( min_precedes(X81,esk9_3(X81,X82,X83),X83)
& min_precedes(esk9_3(X81,X82,X83),X82,X83) )
| next_subocc(X81,X82,X83) ) ),
inference(skolemize,[status(esa)],[167]) ).
fof(169,plain,
! [X81,X82,X83,X84] :
( ( ( ( ~ min_precedes(X81,X84,X83)
| ~ min_precedes(X84,X82,X83) )
& min_precedes(X81,X82,X83) )
| ~ next_subocc(X81,X82,X83) )
& ( ~ min_precedes(X81,X82,X83)
| ( min_precedes(X81,esk9_3(X81,X82,X83),X83)
& min_precedes(esk9_3(X81,X82,X83),X82,X83) )
| next_subocc(X81,X82,X83) ) ),
inference(shift_quantors,[status(thm)],[168]) ).
fof(170,plain,
! [X81,X82,X83,X84] :
( ( ~ min_precedes(X81,X84,X83)
| ~ min_precedes(X84,X82,X83)
| ~ next_subocc(X81,X82,X83) )
& ( min_precedes(X81,X82,X83)
| ~ next_subocc(X81,X82,X83) )
& ( min_precedes(X81,esk9_3(X81,X82,X83),X83)
| ~ min_precedes(X81,X82,X83)
| next_subocc(X81,X82,X83) )
& ( min_precedes(esk9_3(X81,X82,X83),X82,X83)
| ~ min_precedes(X81,X82,X83)
| next_subocc(X81,X82,X83) ) ),
inference(distribute,[status(thm)],[169]) ).
cnf(171,plain,
( next_subocc(X1,X2,X3)
| min_precedes(esk9_3(X1,X2,X3),X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[170]) ).
cnf(172,plain,
( next_subocc(X1,X2,X3)
| min_precedes(X1,esk9_3(X1,X2,X3),X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[170]) ).
cnf(174,plain,
( ~ next_subocc(X1,X2,X3)
| ~ min_precedes(X4,X2,X3)
| ~ min_precedes(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[170]) ).
fof(175,plain,
! [X81,X82] :
( ( ~ root_occ(X81,X82)
| ? [X83] :
( occurrence_of(X82,X83)
& subactivity_occurrence(X81,X82)
& root(X81,X83) ) )
& ( ! [X83] :
( ~ occurrence_of(X82,X83)
| ~ subactivity_occurrence(X81,X82)
| ~ root(X81,X83) )
| root_occ(X81,X82) ) ),
inference(fof_nnf,[status(thm)],[36]) ).
fof(176,plain,
! [X84,X85] :
( ( ~ root_occ(X84,X85)
| ? [X86] :
( occurrence_of(X85,X86)
& subactivity_occurrence(X84,X85)
& root(X84,X86) ) )
& ( ! [X87] :
( ~ occurrence_of(X85,X87)
| ~ subactivity_occurrence(X84,X85)
| ~ root(X84,X87) )
| root_occ(X84,X85) ) ),
inference(variable_rename,[status(thm)],[175]) ).
fof(177,plain,
! [X84,X85] :
( ( ~ root_occ(X84,X85)
| ( occurrence_of(X85,esk10_2(X84,X85))
& subactivity_occurrence(X84,X85)
& root(X84,esk10_2(X84,X85)) ) )
& ( ! [X87] :
( ~ occurrence_of(X85,X87)
| ~ subactivity_occurrence(X84,X85)
| ~ root(X84,X87) )
| root_occ(X84,X85) ) ),
inference(skolemize,[status(esa)],[176]) ).
fof(178,plain,
! [X84,X85,X87] :
( ( ~ occurrence_of(X85,X87)
| ~ subactivity_occurrence(X84,X85)
| ~ root(X84,X87)
| root_occ(X84,X85) )
& ( ~ root_occ(X84,X85)
| ( occurrence_of(X85,esk10_2(X84,X85))
& subactivity_occurrence(X84,X85)
& root(X84,esk10_2(X84,X85)) ) ) ),
inference(shift_quantors,[status(thm)],[177]) ).
fof(179,plain,
! [X84,X85,X87] :
( ( ~ occurrence_of(X85,X87)
| ~ subactivity_occurrence(X84,X85)
| ~ root(X84,X87)
| root_occ(X84,X85) )
& ( occurrence_of(X85,esk10_2(X84,X85))
| ~ root_occ(X84,X85) )
& ( subactivity_occurrence(X84,X85)
| ~ root_occ(X84,X85) )
& ( root(X84,esk10_2(X84,X85))
| ~ root_occ(X84,X85) ) ),
inference(distribute,[status(thm)],[178]) ).
cnf(183,plain,
( root_occ(X1,X2)
| ~ root(X1,X3)
| ~ subactivity_occurrence(X1,X2)
| ~ occurrence_of(X2,X3) ),
inference(split_conjunct,[status(thm)],[179]) ).
fof(202,plain,
! [X93] :
( ~ legal(X93)
| arboreal(X93) ),
inference(fof_nnf,[status(thm)],[40]) ).
fof(203,plain,
! [X94] :
( ~ legal(X94)
| arboreal(X94) ),
inference(variable_rename,[status(thm)],[202]) ).
cnf(204,plain,
( arboreal(X1)
| ~ legal(X1) ),
inference(split_conjunct,[status(thm)],[203]) ).
fof(211,plain,
! [X96,X97] :
( ( ~ leaf(X96,X97)
| ( ( root(X96,X97)
| ? [X98] : min_precedes(X98,X96,X97) )
& ! [X99] : ~ min_precedes(X96,X99,X97) ) )
& ( ( ~ root(X96,X97)
& ! [X98] : ~ min_precedes(X98,X96,X97) )
| ? [X99] : min_precedes(X96,X99,X97)
| leaf(X96,X97) ) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(212,plain,
! [X100,X101] :
( ( ~ leaf(X100,X101)
| ( ( root(X100,X101)
| ? [X102] : min_precedes(X102,X100,X101) )
& ! [X103] : ~ min_precedes(X100,X103,X101) ) )
& ( ( ~ root(X100,X101)
& ! [X104] : ~ min_precedes(X104,X100,X101) )
| ? [X105] : min_precedes(X100,X105,X101)
| leaf(X100,X101) ) ),
inference(variable_rename,[status(thm)],[211]) ).
fof(213,plain,
! [X100,X101] :
( ( ~ leaf(X100,X101)
| ( ( root(X100,X101)
| min_precedes(esk13_2(X100,X101),X100,X101) )
& ! [X103] : ~ min_precedes(X100,X103,X101) ) )
& ( ( ~ root(X100,X101)
& ! [X104] : ~ min_precedes(X104,X100,X101) )
| min_precedes(X100,esk14_2(X100,X101),X101)
| leaf(X100,X101) ) ),
inference(skolemize,[status(esa)],[212]) ).
fof(214,plain,
! [X100,X101,X103,X104] :
( ( ( ~ min_precedes(X104,X100,X101)
& ~ root(X100,X101) )
| min_precedes(X100,esk14_2(X100,X101),X101)
| leaf(X100,X101) )
& ( ( ~ min_precedes(X100,X103,X101)
& ( root(X100,X101)
| min_precedes(esk13_2(X100,X101),X100,X101) ) )
| ~ leaf(X100,X101) ) ),
inference(shift_quantors,[status(thm)],[213]) ).
fof(215,plain,
! [X100,X101,X103,X104] :
( ( ~ min_precedes(X104,X100,X101)
| min_precedes(X100,esk14_2(X100,X101),X101)
| leaf(X100,X101) )
& ( ~ root(X100,X101)
| min_precedes(X100,esk14_2(X100,X101),X101)
| leaf(X100,X101) )
& ( ~ min_precedes(X100,X103,X101)
| ~ leaf(X100,X101) )
& ( root(X100,X101)
| min_precedes(esk13_2(X100,X101),X100,X101)
| ~ leaf(X100,X101) ) ),
inference(distribute,[status(thm)],[214]) ).
cnf(217,plain,
( ~ leaf(X1,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[215]) ).
cnf(219,plain,
( leaf(X1,X2)
| min_precedes(X1,esk14_2(X1,X2),X2)
| ~ min_precedes(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[215]) ).
fof(232,plain,
! [X105,X106] :
( ~ occurrence_of(X105,X106)
| ( ( ~ arboreal(X105)
| atomic(X106) )
& ( ~ atomic(X106)
| arboreal(X105) ) ) ),
inference(fof_nnf,[status(thm)],[45]) ).
fof(233,plain,
! [X107,X108] :
( ~ occurrence_of(X107,X108)
| ( ( ~ arboreal(X107)
| atomic(X108) )
& ( ~ atomic(X108)
| arboreal(X107) ) ) ),
inference(variable_rename,[status(thm)],[232]) ).
fof(234,plain,
! [X107,X108] :
( ( ~ arboreal(X107)
| atomic(X108)
| ~ occurrence_of(X107,X108) )
& ( ~ atomic(X108)
| arboreal(X107)
| ~ occurrence_of(X107,X108) ) ),
inference(distribute,[status(thm)],[233]) ).
cnf(235,plain,
( arboreal(X1)
| ~ occurrence_of(X1,X2)
| ~ atomic(X2) ),
inference(split_conjunct,[status(thm)],[234]) ).
fof(237,negated_conjecture,
? [X107] :
( occurrence_of(X107,tptp0)
& ! [X108,X109] :
( ~ occurrence_of(X108,tptp3)
| ~ root_occ(X108,X107)
| ( ~ occurrence_of(X109,tptp2)
& ~ occurrence_of(X109,tptp1) )
| ~ min_precedes(X108,X109,tptp0) ) ),
inference(fof_nnf,[status(thm)],[47]) ).
fof(238,negated_conjecture,
? [X110] :
( occurrence_of(X110,tptp0)
& ! [X111,X112] :
( ~ occurrence_of(X111,tptp3)
| ~ root_occ(X111,X110)
| ( ~ occurrence_of(X112,tptp2)
& ~ occurrence_of(X112,tptp1) )
| ~ min_precedes(X111,X112,tptp0) ) ),
inference(variable_rename,[status(thm)],[237]) ).
fof(239,negated_conjecture,
( occurrence_of(esk16_0,tptp0)
& ! [X111,X112] :
( ~ occurrence_of(X111,tptp3)
| ~ root_occ(X111,esk16_0)
| ( ~ occurrence_of(X112,tptp2)
& ~ occurrence_of(X112,tptp1) )
| ~ min_precedes(X111,X112,tptp0) ) ),
inference(skolemize,[status(esa)],[238]) ).
fof(240,negated_conjecture,
! [X111,X112] :
( ( ~ occurrence_of(X111,tptp3)
| ~ root_occ(X111,esk16_0)
| ( ~ occurrence_of(X112,tptp2)
& ~ occurrence_of(X112,tptp1) )
| ~ min_precedes(X111,X112,tptp0) )
& occurrence_of(esk16_0,tptp0) ),
inference(shift_quantors,[status(thm)],[239]) ).
fof(241,negated_conjecture,
! [X111,X112] :
( ( ~ occurrence_of(X112,tptp2)
| ~ occurrence_of(X111,tptp3)
| ~ root_occ(X111,esk16_0)
| ~ min_precedes(X111,X112,tptp0) )
& ( ~ occurrence_of(X112,tptp1)
| ~ occurrence_of(X111,tptp3)
| ~ root_occ(X111,esk16_0)
| ~ min_precedes(X111,X112,tptp0) )
& occurrence_of(esk16_0,tptp0) ),
inference(distribute,[status(thm)],[240]) ).
cnf(242,negated_conjecture,
occurrence_of(esk16_0,tptp0),
inference(split_conjunct,[status(thm)],[241]) ).
cnf(243,negated_conjecture,
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,esk16_0)
| ~ occurrence_of(X1,tptp3)
| ~ occurrence_of(X2,tptp1) ),
inference(split_conjunct,[status(thm)],[241]) ).
cnf(244,negated_conjecture,
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,esk16_0)
| ~ occurrence_of(X1,tptp3)
| ~ occurrence_of(X2,tptp2) ),
inference(split_conjunct,[status(thm)],[241]) ).
cnf(252,negated_conjecture,
occurrence_of(esk6_1(esk16_0),tptp3),
inference(spm,[status(thm)],[152,242,theory(equality)]) ).
cnf(253,negated_conjecture,
root_occ(esk6_1(esk16_0),esk16_0),
inference(spm,[status(thm)],[151,242,theory(equality)]) ).
cnf(260,negated_conjecture,
( occurrence_of(esk8_1(esk16_0),tptp1)
| occurrence_of(esk8_1(esk16_0),tptp2) ),
inference(spm,[status(thm)],[148,242,theory(equality)]) ).
cnf(261,negated_conjecture,
min_precedes(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),
inference(spm,[status(thm)],[149,242,theory(equality)]) ).
cnf(262,negated_conjecture,
min_precedes(esk7_1(esk16_0),esk8_1(esk16_0),tptp0),
inference(spm,[status(thm)],[147,242,theory(equality)]) ).
cnf(263,negated_conjecture,
( root(esk1_2(tptp0,esk16_0),tptp0)
| atomic(tptp0) ),
inference(spm,[status(thm)],[68,242,theory(equality)]) ).
cnf(265,negated_conjecture,
root(esk1_2(tptp0,esk16_0),tptp0),
inference(sr,[status(thm)],[263,163,theory(equality)]) ).
cnf(266,negated_conjecture,
( subactivity_occurrence(esk1_2(tptp0,esk16_0),esk16_0)
| atomic(tptp0) ),
inference(spm,[status(thm)],[67,242,theory(equality)]) ).
cnf(268,negated_conjecture,
subactivity_occurrence(esk1_2(tptp0,esk16_0),esk16_0),
inference(sr,[status(thm)],[266,163,theory(equality)]) ).
cnf(269,negated_conjecture,
( esk8_1(esk16_0) = X1
| esk7_1(esk16_0) = X1
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[153,242,theory(equality)]) ).
cnf(277,negated_conjecture,
( root_occ(esk1_2(tptp0,esk16_0),esk16_0)
| ~ root(esk1_2(tptp0,esk16_0),X1)
| ~ occurrence_of(esk16_0,X1) ),
inference(spm,[status(thm)],[183,268,theory(equality)]) ).
cnf(292,negated_conjecture,
( arboreal(esk6_1(esk16_0))
| ~ atomic(tptp3) ),
inference(spm,[status(thm)],[235,252,theory(equality)]) ).
cnf(297,negated_conjecture,
( arboreal(esk6_1(esk16_0))
| $false ),
inference(rw,[status(thm)],[292,165,theory(equality)]) ).
cnf(298,negated_conjecture,
arboreal(esk6_1(esk16_0)),
inference(cn,[status(thm)],[297,theory(equality)]) ).
cnf(340,negated_conjecture,
( ~ occurrence_of(X1,tptp2)
| ~ occurrence_of(esk6_1(esk16_0),tptp3)
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[244,253,theory(equality)]) ).
cnf(341,negated_conjecture,
( ~ occurrence_of(X1,tptp1)
| ~ occurrence_of(esk6_1(esk16_0),tptp3)
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[243,253,theory(equality)]) ).
cnf(342,negated_conjecture,
( ~ occurrence_of(X1,tptp2)
| $false
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(rw,[status(thm)],[340,252,theory(equality)]) ).
cnf(343,negated_conjecture,
( ~ occurrence_of(X1,tptp2)
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(cn,[status(thm)],[342,theory(equality)]) ).
cnf(344,negated_conjecture,
( ~ occurrence_of(X1,tptp1)
| $false
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(rw,[status(thm)],[341,252,theory(equality)]) ).
cnf(345,negated_conjecture,
( ~ occurrence_of(X1,tptp1)
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(cn,[status(thm)],[344,theory(equality)]) ).
cnf(459,negated_conjecture,
( root_occ(esk1_2(tptp0,esk16_0),esk16_0)
| ~ root(esk1_2(tptp0,esk16_0),tptp0) ),
inference(spm,[status(thm)],[277,242,theory(equality)]) ).
cnf(461,negated_conjecture,
( root_occ(esk1_2(tptp0,esk16_0),esk16_0)
| $false ),
inference(rw,[status(thm)],[459,265,theory(equality)]) ).
cnf(462,negated_conjecture,
root_occ(esk1_2(tptp0,esk16_0),esk16_0),
inference(cn,[status(thm)],[461,theory(equality)]) ).
cnf(500,negated_conjecture,
( occurrence_of(esk8_1(esk16_0),tptp2)
| ~ min_precedes(esk6_1(esk16_0),esk8_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[345,260,theory(equality)]) ).
cnf(510,negated_conjecture,
( X1 = esk1_2(tptp0,esk16_0)
| ~ root_occ(X1,esk16_0)
| ~ occurrence_of(esk16_0,X2) ),
inference(spm,[status(thm)],[95,462,theory(equality)]) ).
cnf(534,negated_conjecture,
precedes(esk6_1(esk16_0),esk7_1(esk16_0)),
inference(spm,[status(thm)],[57,261,theory(equality)]) ).
cnf(543,negated_conjecture,
min_precedes(esk2_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),esk7_1(esk16_0),tptp0),
inference(spm,[status(thm)],[88,261,theory(equality)]) ).
cnf(545,negated_conjecture,
( subactivity_occurrence(esk6_1(esk16_0),X1)
| ~ subactivity_occurrence(esk7_1(esk16_0),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[71,261,theory(equality)]) ).
cnf(546,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| min_precedes(esk6_1(esk16_0),esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),tptp0) ),
inference(spm,[status(thm)],[172,261,theory(equality)]) ).
cnf(547,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| min_precedes(esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[171,261,theory(equality)]) ).
cnf(550,negated_conjecture,
precedes(esk7_1(esk16_0),esk8_1(esk16_0)),
inference(spm,[status(thm)],[57,262,theory(equality)]) ).
cnf(552,negated_conjecture,
~ leaf(esk7_1(esk16_0),tptp0),
inference(spm,[status(thm)],[217,262,theory(equality)]) ).
cnf(564,negated_conjecture,
( min_precedes(X1,esk8_1(esk16_0),tptp0)
| ~ precedes(X1,esk8_1(esk16_0))
| ~ min_precedes(esk7_1(esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[156,262,theory(equality)]) ).
cnf(567,negated_conjecture,
earlier(esk6_1(esk16_0),esk7_1(esk16_0)),
inference(spm,[status(thm)],[80,534,theory(equality)]) ).
cnf(570,negated_conjecture,
legal(esk8_1(esk16_0)),
inference(spm,[status(thm)],[79,550,theory(equality)]) ).
cnf(571,negated_conjecture,
earlier(esk7_1(esk16_0),esk8_1(esk16_0)),
inference(spm,[status(thm)],[80,550,theory(equality)]) ).
cnf(599,negated_conjecture,
( earlier(X1,esk8_1(esk16_0))
| ~ earlier(X1,esk7_1(esk16_0)) ),
inference(spm,[status(thm)],[159,571,theory(equality)]) ).
cnf(626,negated_conjecture,
( esk6_1(esk16_0) = esk1_2(tptp0,esk16_0)
| ~ occurrence_of(esk16_0,X1) ),
inference(spm,[status(thm)],[510,253,theory(equality)]) ).
cnf(627,negated_conjecture,
esk1_2(tptp0,esk16_0) = esk6_1(esk16_0),
inference(spm,[status(thm)],[626,242,theory(equality)]) ).
cnf(651,negated_conjecture,
root(esk6_1(esk16_0),tptp0),
inference(rw,[status(thm)],[265,627,theory(equality)]) ).
cnf(1352,negated_conjecture,
~ min_precedes(esk6_1(esk16_0),esk8_1(esk16_0),tptp0),
inference(csr,[status(thm)],[500,343]) ).
cnf(1685,negated_conjecture,
( leaf(esk7_1(esk16_0),tptp0)
| min_precedes(esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0) ),
inference(spm,[status(thm)],[219,543,theory(equality)]) ).
cnf(1691,negated_conjecture,
min_precedes(esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0),
inference(sr,[status(thm)],[1685,552,theory(equality)]) ).
cnf(1692,negated_conjecture,
precedes(esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),
inference(spm,[status(thm)],[57,1691,theory(equality)]) ).
cnf(1695,negated_conjecture,
subactivity_occurrence(esk14_2(esk7_1(esk16_0),tptp0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0))),
inference(spm,[status(thm)],[122,1691,theory(equality)]) ).
cnf(1696,negated_conjecture,
subactivity_occurrence(esk7_1(esk16_0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0))),
inference(spm,[status(thm)],[123,1691,theory(equality)]) ).
cnf(1698,negated_conjecture,
occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),tptp0),
inference(spm,[status(thm)],[124,1691,theory(equality)]) ).
cnf(1708,negated_conjecture,
legal(esk14_2(esk7_1(esk16_0),tptp0)),
inference(spm,[status(thm)],[79,1692,theory(equality)]) ).
cnf(1710,negated_conjecture,
arboreal(esk14_2(esk7_1(esk16_0),tptp0)),
inference(spm,[status(thm)],[204,1708,theory(equality)]) ).
cnf(1857,negated_conjecture,
( subactivity_occurrence(esk6_1(esk16_0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)))
| ~ subactivity_occurrence(esk7_1(esk16_0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0))) ),
inference(spm,[status(thm)],[545,1698,theory(equality)]) ).
cnf(1959,negated_conjecture,
( esk7_1(esk16_0) = esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| esk8_1(esk16_0) = esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[269,546,theory(equality)]) ).
cnf(2067,negated_conjecture,
( precedes(esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),esk7_1(esk16_0))
| next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[57,547,theory(equality)]) ).
cnf(3093,negated_conjecture,
( X1 = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(X1,esk14_2(esk7_1(esk16_0),tptp0),X2)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),X1,X2)
| ~ subactivity_occurrence(X1,esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)))
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X2)
| ~ arboreal(esk14_2(esk7_1(esk16_0),tptp0))
| ~ arboreal(X1) ),
inference(spm,[status(thm)],[133,1695,theory(equality)]) ).
cnf(3095,negated_conjecture,
( X1 = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(X1,esk14_2(esk7_1(esk16_0),tptp0),X2)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),X1,X2)
| ~ subactivity_occurrence(X1,esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)))
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X2)
| $false
| ~ arboreal(X1) ),
inference(rw,[status(thm)],[3093,1710,theory(equality)]) ).
cnf(3096,negated_conjecture,
( X1 = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(X1,esk14_2(esk7_1(esk16_0),tptp0),X2)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),X1,X2)
| ~ subactivity_occurrence(X1,esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)))
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X2)
| ~ arboreal(X1) ),
inference(cn,[status(thm)],[3095,theory(equality)]) ).
cnf(4055,negated_conjecture,
earlier(esk6_1(esk16_0),esk8_1(esk16_0)),
inference(spm,[status(thm)],[599,567,theory(equality)]) ).
cnf(4102,negated_conjecture,
( precedes(esk6_1(esk16_0),esk8_1(esk16_0))
| ~ legal(esk8_1(esk16_0)) ),
inference(spm,[status(thm)],[78,4055,theory(equality)]) ).
cnf(4104,negated_conjecture,
( precedes(esk6_1(esk16_0),esk8_1(esk16_0))
| $false ),
inference(rw,[status(thm)],[4102,570,theory(equality)]) ).
cnf(4105,negated_conjecture,
precedes(esk6_1(esk16_0),esk8_1(esk16_0)),
inference(cn,[status(thm)],[4104,theory(equality)]) ).
cnf(4108,negated_conjecture,
( min_precedes(esk6_1(esk16_0),esk8_1(esk16_0),tptp0)
| ~ min_precedes(esk7_1(esk16_0),esk6_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[564,4105,theory(equality)]) ).
cnf(4111,negated_conjecture,
~ min_precedes(esk7_1(esk16_0),esk6_1(esk16_0),tptp0),
inference(sr,[status(thm)],[4108,1352,theory(equality)]) ).
cnf(5686,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| min_precedes(esk6_1(esk16_0),esk8_1(esk16_0),tptp0)
| esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) = esk7_1(esk16_0) ),
inference(spm,[status(thm)],[546,1959,theory(equality)]) ).
cnf(5690,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) = esk7_1(esk16_0) ),
inference(sr,[status(thm)],[5686,1352,theory(equality)]) ).
cnf(5976,negated_conjecture,
( subactivity_occurrence(esk6_1(esk16_0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)))
| $false ),
inference(rw,[status(thm)],[1857,1696,theory(equality)]) ).
cnf(5977,negated_conjecture,
subactivity_occurrence(esk6_1(esk16_0),esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0))),
inference(cn,[status(thm)],[5976,theory(equality)]) ).
cnf(6542,negated_conjecture,
( earlier(esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),esk7_1(esk16_0))
| next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[80,2067,theory(equality)]) ).
cnf(6545,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| precedes(esk7_1(esk16_0),esk7_1(esk16_0)) ),
inference(spm,[status(thm)],[2067,5690,theory(equality)]) ).
cnf(6571,negated_conjecture,
( earlier(esk7_1(esk16_0),esk7_1(esk16_0))
| next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[80,6545,theory(equality)]) ).
cnf(6706,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| ~ earlier(esk7_1(esk16_0),esk9_3(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)) ),
inference(spm,[status(thm)],[74,6542,theory(equality)]) ).
cnf(6828,negated_conjecture,
( next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0)
| ~ earlier(esk7_1(esk16_0),esk7_1(esk16_0)) ),
inference(spm,[status(thm)],[6706,5690,theory(equality)]) ).
cnf(6829,negated_conjecture,
next_subocc(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),
inference(csr,[status(thm)],[6828,6571]) ).
cnf(6833,negated_conjecture,
( ~ min_precedes(X1,esk7_1(esk16_0),tptp0)
| ~ min_precedes(esk6_1(esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[174,6829,theory(equality)]) ).
cnf(10257,negated_conjecture,
( esk6_1(esk16_0) = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),esk6_1(esk16_0),X1)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),X1)
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X1)
| ~ arboreal(esk6_1(esk16_0)) ),
inference(spm,[status(thm)],[3096,5977,theory(equality)]) ).
cnf(10267,negated_conjecture,
( esk6_1(esk16_0) = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),esk6_1(esk16_0),X1)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),X1)
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X1)
| $false ),
inference(rw,[status(thm)],[10257,298,theory(equality)]) ).
cnf(10268,negated_conjecture,
( esk6_1(esk16_0) = esk14_2(esk7_1(esk16_0),tptp0)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),esk6_1(esk16_0),X1)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),X1)
| ~ occurrence_of(esk3_3(tptp0,esk7_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0)),X1) ),
inference(cn,[status(thm)],[10267,theory(equality)]) ).
cnf(104104,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0)
| min_precedes(esk14_2(esk7_1(esk16_0),tptp0),esk6_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[10268,1698,theory(equality)]) ).
cnf(104118,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0)
| ~ root(esk6_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[83,104104,theory(equality)]) ).
cnf(104134,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0)
| $false ),
inference(rw,[status(thm)],[104118,651,theory(equality)]) ).
cnf(104135,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| min_precedes(esk6_1(esk16_0),esk14_2(esk7_1(esk16_0),tptp0),tptp0) ),
inference(cn,[status(thm)],[104134,theory(equality)]) ).
cnf(104153,negated_conjecture,
( esk7_1(esk16_0) = esk14_2(esk7_1(esk16_0),tptp0)
| esk8_1(esk16_0) = esk14_2(esk7_1(esk16_0),tptp0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0) ),
inference(spm,[status(thm)],[269,104135,theory(equality)]) ).
cnf(104158,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk7_1(esk16_0)
| esk8_1(esk16_0) != esk6_1(esk16_0) ),
inference(ef,[status(thm)],[104153,theory(equality)]) ).
cnf(105663,negated_conjecture,
( esk8_1(esk16_0) = esk6_1(esk16_0)
| min_precedes(esk6_1(esk16_0),esk8_1(esk16_0),tptp0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk7_1(esk16_0) ),
inference(spm,[status(thm)],[104135,104153,theory(equality)]) ).
cnf(106033,negated_conjecture,
( esk8_1(esk16_0) = esk6_1(esk16_0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk7_1(esk16_0) ),
inference(sr,[status(thm)],[105663,1352,theory(equality)]) ).
cnf(108146,negated_conjecture,
( esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk7_1(esk16_0) ),
inference(csr,[status(thm)],[104158,106033]) ).
cnf(108148,negated_conjecture,
( min_precedes(esk7_1(esk16_0),esk7_1(esk16_0),tptp0)
| esk14_2(esk7_1(esk16_0),tptp0) = esk6_1(esk16_0) ),
inference(spm,[status(thm)],[1691,108146,theory(equality)]) ).
cnf(120310,negated_conjecture,
( min_precedes(esk7_1(esk16_0),esk6_1(esk16_0),tptp0)
| min_precedes(esk7_1(esk16_0),esk7_1(esk16_0),tptp0) ),
inference(spm,[status(thm)],[1691,108148,theory(equality)]) ).
cnf(121812,negated_conjecture,
min_precedes(esk7_1(esk16_0),esk7_1(esk16_0),tptp0),
inference(sr,[status(thm)],[120310,4111,theory(equality)]) ).
cnf(122368,negated_conjecture,
~ min_precedes(esk6_1(esk16_0),esk7_1(esk16_0),tptp0),
inference(spm,[status(thm)],[6833,121812,theory(equality)]) ).
cnf(122380,negated_conjecture,
$false,
inference(rw,[status(thm)],[122368,261,theory(equality)]) ).
cnf(122381,negated_conjecture,
$false,
inference(cn,[status(thm)],[122380,theory(equality)]) ).
cnf(122382,negated_conjecture,
$false,
122381,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/PRO/PRO012+4.p
% --creating new selector for []
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpPz7R2e/sel_PRO012+4.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpPz7R2e/sel_PRO012+4.p_2 with time limit 81
% -prover status Theorem
% Problem PRO012+4.p solved in phase 1.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/PRO/PRO012+4.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/PRO/PRO012+4.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
%
%------------------------------------------------------------------------------