%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO017+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art09.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 : Wed Dec 29 21:19:36 EST 2010
% Result : Theorem 174.97s
% Output : Solution 271.62s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP24309/PRO017+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~goals:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_22:
% CSA axiom sos_22 found
% Looking for CSA axiom ... sos_25:
% CSA axiom sos_25 found
% Looking for CSA axiom ... sos_29:
% CSA axiom sos_29 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_31: CSA axiom sos_31 found
% Looking for CSA axiom ... sos_34:
% CSA axiom sos_34 found
% Looking for CSA axiom ... sos_35:
% CSA axiom sos_35 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_28:
% CSA axiom sos_28 found
% Looking for CSA axiom ... sos_45:
% CSA axiom sos_45 found
% Looking for CSA axiom ... sos_46:
% CSA axiom sos_46 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_47:
% CSA axiom sos_47 found
% Looking for CSA axiom ... sos_07:
% CSA axiom sos_07 found
% Looking for CSA axiom ... sos_21:
% CSA axiom sos_21 found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_32: CSA axiom sos_32 found
% Looking for CSA axiom ... sos_37:
% CSA axiom sos_37 found
% Looking for CSA axiom ... sos_39:
% CSA axiom sos_39 found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_40:
% CSA axiom sos_40 found
% Looking for CSA axiom ... sos_41:
% CSA axiom sos_41 found
% Looking for CSA axiom ... sos_08:
% CSA axiom sos_08 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_36:
% CSA axiom sos_36 found
% Looking for CSA axiom ... sos_02:
% CSA axiom sos_02 found
% Looking for CSA axiom ... sos_42:
% CSA axiom sos_42 found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :sos_42:sos_02:sos_36:sos_08:sos_41:sos_40:sos_39:sos_37:sos_32:sos_21:sos_07:sos_47:sos_46:sos_45:sos_28:sos_35:sos_34:sos_31:sos_29:sos_25:sos_22 (21)
% Unselected axioms are ... :sos_43:sos_44:sos_19:sos_26:sos_27:sos_13:sos_14:sos_30:sos_33:sos_15:sos_18:sos_20:sos_24:sos_04:sos_05:sos_11:sos:sos_01:sos_38:sos_03:sos_16:sos_09:sos_23:sos_06:sos_12:sos_10:sos_17 (27)
% SZS status THM for /tmp/SystemOnTPTP24309/PRO017+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP24309/PRO017+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 27722
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.63 CPU 2.03 WC
% PrfWatch: 3.24 CPU 4.06 WC
% PrfWatch: 5.20 CPU 6.06 WC
% PrfWatch: 7.20 CPU 8.06 WC
% PrfWatch: 9.19 CPU 10.07 WC
% PrfWatch: 11.18 CPU 12.07 WC
% PrfWatch: 13.18 CPU 14.08 WC
% PrfWatch: 15.16 CPU 16.08 WC
% PrfWatch: 17.16 CPU 18.09 WC
% PrfWatch: 19.14 CPU 20.09 WC
% PrfWatch: 21.14 CPU 22.10 WC
% PrfWatch: 23.13 CPU 24.10 WC
% PrfWatch: 25.12 CPU 26.11 WC
% PrfWatch: 27.11 CPU 28.11 WC
% PrfWatch: 29.10 CPU 30.12 WC
% PrfWatch: 31.07 CPU 32.12 WC
% PrfWatch: 33.06 CPU 34.13 WC
% PrfWatch: 34.67 CPU 36.13 WC
% PrfWatch: 36.32 CPU 38.14 WC
% PrfWatch: 38.31 CPU 40.14 WC
% PrfWatch: 40.31 CPU 42.14 WC
% PrfWatch: 42.29 CPU 44.15 WC
% PrfWatch: 44.29 CPU 46.15 WC
% PrfWatch: 46.28 CPU 48.16 WC
% PrfWatch: 48.27 CPU 50.16 WC
% PrfWatch: 50.26 CPU 52.17 WC
% PrfWatch: 52.25 CPU 54.17 WC
% PrfWatch: 54.24 CPU 56.18 WC
% PrfWatch: 56.22 CPU 58.18 WC
% PrfWatch: 58.22 CPU 60.19 WC
% PrfWatch: 60.22 CPU 62.19 WC
% PrfWatch: 62.19 CPU 64.20 WC
% PrfWatch: 63.76 CPU 66.20 WC
% PrfWatch: 65.45 CPU 68.22 WC
% PrfWatch: 67.44 CPU 70.22 WC
% PrfWatch: 69.43 CPU 72.23 WC
% PrfWatch: 71.43 CPU 74.23 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 73.44 CPU 76.24 WC
% PrfWatch: 75.43 CPU 78.24 WC
% PrfWatch: 77.43 CPU 80.25 WC
% PrfWatch: 79.42 CPU 82.25 WC
% PrfWatch: 81.41 CPU 84.26 WC
% PrfWatch: 83.41 CPU 86.26 WC
% PrfWatch: 85.41 CPU 88.26 WC
% PrfWatch: 87.40 CPU 90.27 WC
% PrfWatch: 89.03 CPU 92.27 WC
% PrfWatch: 90.69 CPU 94.28 WC
% PrfWatch: 92.69 CPU 96.28 WC
% PrfWatch: 94.68 CPU 98.29 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(tptp4=tptp3),file('/tmp/SRASS.s.p', sos_42)).
% fof(2, axiom,![X1]:![X2]:![X3]:((occurrence_of(X1,X2)&occurrence_of(X1,X3))=>X2=X3),file('/tmp/SRASS.s.p', sos_02)).
% fof(5, axiom,atomic(tptp3),file('/tmp/SRASS.s.p', sos_41)).
% fof(10, axiom,![X10]:![X11]:(leaf(X10,X11)<=>((root(X10,X11)|?[X12]:min_precedes(X12,X10,X11))&~(?[X13]:min_precedes(X10,X13,X11)))),file('/tmp/SRASS.s.p', sos_21)).
% fof(11, axiom,![X14]:![X15]:(occurrence_of(X14,X15)=>(arboreal(X14)<=>atomic(X15))),file('/tmp/SRASS.s.p', sos_07)).
% fof(13, axiom,~(tptp3=tptp1),file('/tmp/SRASS.s.p', sos_46)).
% fof(14, axiom,~(tptp3=tptp2),file('/tmp/SRASS.s.p', sos_45)).
% fof(16, axiom,![X20]:![X21]:((((occurrence_of(X21,tptp0)&subactivity_occurrence(X20,X21))&arboreal(X20))&~(leaf_occ(X20,X21)))=>?[X22]:?[X23]:?[X24]:((((((occurrence_of(X22,tptp3)&next_subocc(X20,X22,tptp0))&occurrence_of(X23,tptp4))&min_precedes(X22,X23,tptp0))&(occurrence_of(X24,tptp2)|occurrence_of(X24,tptp1)))&min_precedes(X23,X24,tptp0))&![X25]:(min_precedes(X22,X25,tptp0)=>(X25=X23|X25=X24)))),file('/tmp/SRASS.s.p', sos_35)).
% fof(17, axiom,![X26]:![X27]:(leaf_occ(X26,X27)<=>?[X28]:((occurrence_of(X27,X28)&subactivity_occurrence(X26,X27))&leaf(X26,X28))),file('/tmp/SRASS.s.p', sos_34)).
% fof(20, axiom,![X36]:![X37]:![X38]:(min_precedes(X37,X38,X36)=>?[X39]:((occurrence_of(X39,X36)&subactivity_occurrence(X37,X39))&subactivity_occurrence(X38,X39))),file('/tmp/SRASS.s.p', sos_25)).
% fof(21, axiom,![X40]:![X41]:![X42]:(next_subocc(X40,X41,X42)<=>(min_precedes(X40,X41,X42)&~(?[X43]:(min_precedes(X40,X43,X42)&min_precedes(X43,X41,X42))))),file('/tmp/SRASS.s.p', sos_22)).
% fof(22, conjecture,![X44]:![X45]:((((occurrence_of(X45,tptp0)&subactivity_occurrence(X44,X45))&arboreal(X44))&~(leaf_occ(X44,X45)))=>?[X46]:?[X47]:((((occurrence_of(X46,tptp3)&next_subocc(X44,X46,tptp0))&(occurrence_of(X47,tptp2)|occurrence_of(X47,tptp1)))&min_precedes(X46,X47,tptp0))&leaf(X47,tptp0))),file('/tmp/SRASS.s.p', goals)).
% fof(23, negated_conjecture,~(![X44]:![X45]:((((occurrence_of(X45,tptp0)&subactivity_occurrence(X44,X45))&arboreal(X44))&~(leaf_occ(X44,X45)))=>?[X46]:?[X47]:((((occurrence_of(X46,tptp3)&next_subocc(X44,X46,tptp0))&(occurrence_of(X47,tptp2)|occurrence_of(X47,tptp1)))&min_precedes(X46,X47,tptp0))&leaf(X47,tptp0)))),inference(assume_negation,[status(cth)],[22])).
% fof(26, plain,![X20]:![X21]:((((occurrence_of(X21,tptp0)&subactivity_occurrence(X20,X21))&arboreal(X20))&~(leaf_occ(X20,X21)))=>?[X22]:?[X23]:?[X24]:((((((occurrence_of(X22,tptp3)&next_subocc(X20,X22,tptp0))&occurrence_of(X23,tptp4))&min_precedes(X22,X23,tptp0))&(occurrence_of(X24,tptp2)|occurrence_of(X24,tptp1)))&min_precedes(X23,X24,tptp0))&![X25]:(min_precedes(X22,X25,tptp0)=>(X25=X23|X25=X24)))),inference(fof_simplification,[status(thm)],[16,theory(equality)])).
% fof(27, negated_conjecture,~(![X44]:![X45]:((((occurrence_of(X45,tptp0)&subactivity_occurrence(X44,X45))&arboreal(X44))&~(leaf_occ(X44,X45)))=>?[X46]:?[X47]:((((occurrence_of(X46,tptp3)&next_subocc(X44,X46,tptp0))&(occurrence_of(X47,tptp2)|occurrence_of(X47,tptp1)))&min_precedes(X46,X47,tptp0))&leaf(X47,tptp0)))),inference(fof_simplification,[status(thm)],[23,theory(equality)])).
% cnf(28,plain,(tptp4!=tptp3),inference(split_conjunct,[status(thm)],[1])).
% fof(29, plain,![X1]:![X2]:![X3]:((~(occurrence_of(X1,X2))|~(occurrence_of(X1,X3)))|X2=X3),inference(fof_nnf,[status(thm)],[2])).
% fof(30, plain,![X4]:![X5]:![X6]:((~(occurrence_of(X4,X5))|~(occurrence_of(X4,X6)))|X5=X6),inference(variable_rename,[status(thm)],[29])).
% cnf(31,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[30])).
% cnf(36,plain,(atomic(tptp3)),inference(split_conjunct,[status(thm)],[5])).
% fof(46, plain,![X10]:![X11]:((~(leaf(X10,X11))|((root(X10,X11)|?[X12]:min_precedes(X12,X10,X11))&![X13]:~(min_precedes(X10,X13,X11))))&(((~(root(X10,X11))&![X12]:~(min_precedes(X12,X10,X11)))|?[X13]:min_precedes(X10,X13,X11))|leaf(X10,X11))),inference(fof_nnf,[status(thm)],[10])).
% fof(47, plain,![X14]:![X15]:((~(leaf(X14,X15))|((root(X14,X15)|?[X16]:min_precedes(X16,X14,X15))&![X17]:~(min_precedes(X14,X17,X15))))&(((~(root(X14,X15))&![X18]:~(min_precedes(X18,X14,X15)))|?[X19]:min_precedes(X14,X19,X15))|leaf(X14,X15))),inference(variable_rename,[status(thm)],[46])).
% fof(48, plain,![X14]:![X15]:((~(leaf(X14,X15))|((root(X14,X15)|min_precedes(esk2_2(X14,X15),X14,X15))&![X17]:~(min_precedes(X14,X17,X15))))&(((~(root(X14,X15))&![X18]:~(min_precedes(X18,X14,X15)))|min_precedes(X14,esk3_2(X14,X15),X15))|leaf(X14,X15))),inference(skolemize,[status(esa)],[47])).
% fof(49, plain,![X14]:![X15]:![X17]:![X18]:((((~(min_precedes(X18,X14,X15))&~(root(X14,X15)))|min_precedes(X14,esk3_2(X14,X15),X15))|leaf(X14,X15))&((~(min_precedes(X14,X17,X15))&(root(X14,X15)|min_precedes(esk2_2(X14,X15),X14,X15)))|~(leaf(X14,X15)))),inference(shift_quantors,[status(thm)],[48])).
% fof(50, plain,![X14]:![X15]:![X17]:![X18]:((((~(min_precedes(X18,X14,X15))|min_precedes(X14,esk3_2(X14,X15),X15))|leaf(X14,X15))&((~(root(X14,X15))|min_precedes(X14,esk3_2(X14,X15),X15))|leaf(X14,X15)))&((~(min_precedes(X14,X17,X15))|~(leaf(X14,X15)))&((root(X14,X15)|min_precedes(esk2_2(X14,X15),X14,X15))|~(leaf(X14,X15))))),inference(distribute,[status(thm)],[49])).
% cnf(52,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[50])).
% fof(55, plain,![X14]:![X15]:(~(occurrence_of(X14,X15))|((~(arboreal(X14))|atomic(X15))&(~(atomic(X15))|arboreal(X14)))),inference(fof_nnf,[status(thm)],[11])).
% fof(56, plain,![X16]:![X17]:(~(occurrence_of(X16,X17))|((~(arboreal(X16))|atomic(X17))&(~(atomic(X17))|arboreal(X16)))),inference(variable_rename,[status(thm)],[55])).
% fof(57, plain,![X16]:![X17]:(((~(arboreal(X16))|atomic(X17))|~(occurrence_of(X16,X17)))&((~(atomic(X17))|arboreal(X16))|~(occurrence_of(X16,X17)))),inference(distribute,[status(thm)],[56])).
% cnf(58,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[57])).
% cnf(61,plain,(tptp3!=tptp1),inference(split_conjunct,[status(thm)],[13])).
% cnf(62,plain,(tptp3!=tptp2),inference(split_conjunct,[status(thm)],[14])).
% fof(66, plain,![X20]:![X21]:((((~(occurrence_of(X21,tptp0))|~(subactivity_occurrence(X20,X21)))|~(arboreal(X20)))|leaf_occ(X20,X21))|?[X22]:?[X23]:?[X24]:((((((occurrence_of(X22,tptp3)&next_subocc(X20,X22,tptp0))&occurrence_of(X23,tptp4))&min_precedes(X22,X23,tptp0))&(occurrence_of(X24,tptp2)|occurrence_of(X24,tptp1)))&min_precedes(X23,X24,tptp0))&![X25]:(~(min_precedes(X22,X25,tptp0))|(X25=X23|X25=X24)))),inference(fof_nnf,[status(thm)],[26])).
% fof(67, plain,![X26]:![X27]:((((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))|?[X28]:?[X29]:?[X30]:((((((occurrence_of(X28,tptp3)&next_subocc(X26,X28,tptp0))&occurrence_of(X29,tptp4))&min_precedes(X28,X29,tptp0))&(occurrence_of(X30,tptp2)|occurrence_of(X30,tptp1)))&min_precedes(X29,X30,tptp0))&![X31]:(~(min_precedes(X28,X31,tptp0))|(X31=X29|X31=X30)))),inference(variable_rename,[status(thm)],[66])).
% fof(68, plain,![X26]:![X27]:((((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))|((((((occurrence_of(esk4_2(X26,X27),tptp3)&next_subocc(X26,esk4_2(X26,X27),tptp0))&occurrence_of(esk5_2(X26,X27),tptp4))&min_precedes(esk4_2(X26,X27),esk5_2(X26,X27),tptp0))&(occurrence_of(esk6_2(X26,X27),tptp2)|occurrence_of(esk6_2(X26,X27),tptp1)))&min_precedes(esk5_2(X26,X27),esk6_2(X26,X27),tptp0))&![X31]:(~(min_precedes(esk4_2(X26,X27),X31,tptp0))|(X31=esk5_2(X26,X27)|X31=esk6_2(X26,X27))))),inference(skolemize,[status(esa)],[67])).
% fof(69, plain,![X26]:![X27]:![X31]:(((~(min_precedes(esk4_2(X26,X27),X31,tptp0))|(X31=esk5_2(X26,X27)|X31=esk6_2(X26,X27)))&(((((occurrence_of(esk4_2(X26,X27),tptp3)&next_subocc(X26,esk4_2(X26,X27),tptp0))&occurrence_of(esk5_2(X26,X27),tptp4))&min_precedes(esk4_2(X26,X27),esk5_2(X26,X27),tptp0))&(occurrence_of(esk6_2(X26,X27),tptp2)|occurrence_of(esk6_2(X26,X27),tptp1)))&min_precedes(esk5_2(X26,X27),esk6_2(X26,X27),tptp0)))|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))),inference(shift_quantors,[status(thm)],[68])).
% fof(70, plain,![X26]:![X27]:![X31]:(((~(min_precedes(esk4_2(X26,X27),X31,tptp0))|(X31=esk5_2(X26,X27)|X31=esk6_2(X26,X27)))|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27)))&((((((occurrence_of(esk4_2(X26,X27),tptp3)|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27)))&(next_subocc(X26,esk4_2(X26,X27),tptp0)|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))))&(occurrence_of(esk5_2(X26,X27),tptp4)|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))))&(min_precedes(esk4_2(X26,X27),esk5_2(X26,X27),tptp0)|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))))&((occurrence_of(esk6_2(X26,X27),tptp2)|occurrence_of(esk6_2(X26,X27),tptp1))|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))))&(min_precedes(esk5_2(X26,X27),esk6_2(X26,X27),tptp0)|(((~(occurrence_of(X27,tptp0))|~(subactivity_occurrence(X26,X27)))|~(arboreal(X26)))|leaf_occ(X26,X27))))),inference(distribute,[status(thm)],[69])).
% cnf(72,plain,(leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp1)|occurrence_of(esk6_2(X1,X2),tptp2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(73,plain,(leaf_occ(X1,X2)|min_precedes(esk4_2(X1,X2),esk5_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(74,plain,(leaf_occ(X1,X2)|occurrence_of(esk5_2(X1,X2),tptp4)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(75,plain,(leaf_occ(X1,X2)|next_subocc(X1,esk4_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(76,plain,(leaf_occ(X1,X2)|occurrence_of(esk4_2(X1,X2),tptp3)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% cnf(77,plain,(leaf_occ(X1,X2)|X3=esk6_2(X1,X2)|X3=esk5_2(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~min_precedes(esk4_2(X1,X2),X3,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% fof(78, plain,![X26]:![X27]:((~(leaf_occ(X26,X27))|?[X28]:((occurrence_of(X27,X28)&subactivity_occurrence(X26,X27))&leaf(X26,X28)))&(![X28]:((~(occurrence_of(X27,X28))|~(subactivity_occurrence(X26,X27)))|~(leaf(X26,X28)))|leaf_occ(X26,X27))),inference(fof_nnf,[status(thm)],[17])).
% fof(79, plain,![X29]:![X30]:((~(leaf_occ(X29,X30))|?[X31]:((occurrence_of(X30,X31)&subactivity_occurrence(X29,X30))&leaf(X29,X31)))&(![X32]:((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(leaf(X29,X32)))|leaf_occ(X29,X30))),inference(variable_rename,[status(thm)],[78])).
% fof(80, plain,![X29]:![X30]:((~(leaf_occ(X29,X30))|((occurrence_of(X30,esk7_2(X29,X30))&subactivity_occurrence(X29,X30))&leaf(X29,esk7_2(X29,X30))))&(![X32]:((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(leaf(X29,X32)))|leaf_occ(X29,X30))),inference(skolemize,[status(esa)],[79])).
% fof(81, plain,![X29]:![X30]:![X32]:((((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(leaf(X29,X32)))|leaf_occ(X29,X30))&(~(leaf_occ(X29,X30))|((occurrence_of(X30,esk7_2(X29,X30))&subactivity_occurrence(X29,X30))&leaf(X29,esk7_2(X29,X30))))),inference(shift_quantors,[status(thm)],[80])).
% fof(82, plain,![X29]:![X30]:![X32]:((((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(leaf(X29,X32)))|leaf_occ(X29,X30))&(((occurrence_of(X30,esk7_2(X29,X30))|~(leaf_occ(X29,X30)))&(subactivity_occurrence(X29,X30)|~(leaf_occ(X29,X30))))&(leaf(X29,esk7_2(X29,X30))|~(leaf_occ(X29,X30))))),inference(distribute,[status(thm)],[81])).
% cnf(83,plain,(leaf(X1,esk7_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[82])).
% cnf(85,plain,(occurrence_of(X2,esk7_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[82])).
% fof(93, plain,![X36]:![X37]:![X38]:(~(min_precedes(X37,X38,X36))|?[X39]:((occurrence_of(X39,X36)&subactivity_occurrence(X37,X39))&subactivity_occurrence(X38,X39))),inference(fof_nnf,[status(thm)],[20])).
% fof(94, plain,![X40]:![X41]:![X42]:(~(min_precedes(X41,X42,X40))|?[X43]:((occurrence_of(X43,X40)&subactivity_occurrence(X41,X43))&subactivity_occurrence(X42,X43))),inference(variable_rename,[status(thm)],[93])).
% fof(95, plain,![X40]:![X41]:![X42]:(~(min_precedes(X41,X42,X40))|((occurrence_of(esk8_3(X40,X41,X42),X40)&subactivity_occurrence(X41,esk8_3(X40,X41,X42)))&subactivity_occurrence(X42,esk8_3(X40,X41,X42)))),inference(skolemize,[status(esa)],[94])).
% fof(96, plain,![X40]:![X41]:![X42]:(((occurrence_of(esk8_3(X40,X41,X42),X40)|~(min_precedes(X41,X42,X40)))&(subactivity_occurrence(X41,esk8_3(X40,X41,X42))|~(min_precedes(X41,X42,X40))))&(subactivity_occurrence(X42,esk8_3(X40,X41,X42))|~(min_precedes(X41,X42,X40)))),inference(distribute,[status(thm)],[95])).
% cnf(97,plain,(subactivity_occurrence(X2,esk8_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[96])).
% cnf(99,plain,(occurrence_of(esk8_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[96])).
% fof(100, plain,![X40]:![X41]:![X42]:((~(next_subocc(X40,X41,X42))|(min_precedes(X40,X41,X42)&![X43]:(~(min_precedes(X40,X43,X42))|~(min_precedes(X43,X41,X42)))))&((~(min_precedes(X40,X41,X42))|?[X43]:(min_precedes(X40,X43,X42)&min_precedes(X43,X41,X42)))|next_subocc(X40,X41,X42))),inference(fof_nnf,[status(thm)],[21])).
% fof(101, plain,![X44]:![X45]:![X46]:((~(next_subocc(X44,X45,X46))|(min_precedes(X44,X45,X46)&![X47]:(~(min_precedes(X44,X47,X46))|~(min_precedes(X47,X45,X46)))))&((~(min_precedes(X44,X45,X46))|?[X48]:(min_precedes(X44,X48,X46)&min_precedes(X48,X45,X46)))|next_subocc(X44,X45,X46))),inference(variable_rename,[status(thm)],[100])).
% fof(102, plain,![X44]:![X45]:![X46]:((~(next_subocc(X44,X45,X46))|(min_precedes(X44,X45,X46)&![X47]:(~(min_precedes(X44,X47,X46))|~(min_precedes(X47,X45,X46)))))&((~(min_precedes(X44,X45,X46))|(min_precedes(X44,esk9_3(X44,X45,X46),X46)&min_precedes(esk9_3(X44,X45,X46),X45,X46)))|next_subocc(X44,X45,X46))),inference(skolemize,[status(esa)],[101])).
% fof(103, plain,![X44]:![X45]:![X46]:![X47]:((((~(min_precedes(X44,X47,X46))|~(min_precedes(X47,X45,X46)))&min_precedes(X44,X45,X46))|~(next_subocc(X44,X45,X46)))&((~(min_precedes(X44,X45,X46))|(min_precedes(X44,esk9_3(X44,X45,X46),X46)&min_precedes(esk9_3(X44,X45,X46),X45,X46)))|next_subocc(X44,X45,X46))),inference(shift_quantors,[status(thm)],[102])).
% fof(104, plain,![X44]:![X45]:![X46]:![X47]:((((~(min_precedes(X44,X47,X46))|~(min_precedes(X47,X45,X46)))|~(next_subocc(X44,X45,X46)))&(min_precedes(X44,X45,X46)|~(next_subocc(X44,X45,X46))))&(((min_precedes(X44,esk9_3(X44,X45,X46),X46)|~(min_precedes(X44,X45,X46)))|next_subocc(X44,X45,X46))&((min_precedes(esk9_3(X44,X45,X46),X45,X46)|~(min_precedes(X44,X45,X46)))|next_subocc(X44,X45,X46)))),inference(distribute,[status(thm)],[103])).
% cnf(107,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[104])).
% fof(109, negated_conjecture,?[X44]:?[X45]:((((occurrence_of(X45,tptp0)&subactivity_occurrence(X44,X45))&arboreal(X44))&~(leaf_occ(X44,X45)))&![X46]:![X47]:((((~(occurrence_of(X46,tptp3))|~(next_subocc(X44,X46,tptp0)))|(~(occurrence_of(X47,tptp2))&~(occurrence_of(X47,tptp1))))|~(min_precedes(X46,X47,tptp0)))|~(leaf(X47,tptp0)))),inference(fof_nnf,[status(thm)],[27])).
% fof(110, negated_conjecture,?[X48]:?[X49]:((((occurrence_of(X49,tptp0)&subactivity_occurrence(X48,X49))&arboreal(X48))&~(leaf_occ(X48,X49)))&![X50]:![X51]:((((~(occurrence_of(X50,tptp3))|~(next_subocc(X48,X50,tptp0)))|(~(occurrence_of(X51,tptp2))&~(occurrence_of(X51,tptp1))))|~(min_precedes(X50,X51,tptp0)))|~(leaf(X51,tptp0)))),inference(variable_rename,[status(thm)],[109])).
% fof(111, negated_conjecture,((((occurrence_of(esk11_0,tptp0)&subactivity_occurrence(esk10_0,esk11_0))&arboreal(esk10_0))&~(leaf_occ(esk10_0,esk11_0)))&![X50]:![X51]:((((~(occurrence_of(X50,tptp3))|~(next_subocc(esk10_0,X50,tptp0)))|(~(occurrence_of(X51,tptp2))&~(occurrence_of(X51,tptp1))))|~(min_precedes(X50,X51,tptp0)))|~(leaf(X51,tptp0)))),inference(skolemize,[status(esa)],[110])).
% fof(112, negated_conjecture,![X50]:![X51]:(((((~(occurrence_of(X50,tptp3))|~(next_subocc(esk10_0,X50,tptp0)))|(~(occurrence_of(X51,tptp2))&~(occurrence_of(X51,tptp1))))|~(min_precedes(X50,X51,tptp0)))|~(leaf(X51,tptp0)))&(((occurrence_of(esk11_0,tptp0)&subactivity_occurrence(esk10_0,esk11_0))&arboreal(esk10_0))&~(leaf_occ(esk10_0,esk11_0)))),inference(shift_quantors,[status(thm)],[111])).
% fof(113, negated_conjecture,![X50]:![X51]:(((((~(occurrence_of(X51,tptp2))|(~(occurrence_of(X50,tptp3))|~(next_subocc(esk10_0,X50,tptp0))))|~(min_precedes(X50,X51,tptp0)))|~(leaf(X51,tptp0)))&(((~(occurrence_of(X51,tptp1))|(~(occurrence_of(X50,tptp3))|~(next_subocc(esk10_0,X50,tptp0))))|~(min_precedes(X50,X51,tptp0)))|~(leaf(X51,tptp0))))&(((occurrence_of(esk11_0,tptp0)&subactivity_occurrence(esk10_0,esk11_0))&arboreal(esk10_0))&~(leaf_occ(esk10_0,esk11_0)))),inference(distribute,[status(thm)],[112])).
% cnf(114,negated_conjecture,(~leaf_occ(esk10_0,esk11_0)),inference(split_conjunct,[status(thm)],[113])).
% cnf(115,negated_conjecture,(arboreal(esk10_0)),inference(split_conjunct,[status(thm)],[113])).
% cnf(116,negated_conjecture,(subactivity_occurrence(esk10_0,esk11_0)),inference(split_conjunct,[status(thm)],[113])).
% cnf(117,negated_conjecture,(occurrence_of(esk11_0,tptp0)),inference(split_conjunct,[status(thm)],[113])).
% cnf(131,plain,(X1=X2|~occurrence_of(esk8_3(X2,X3,X4),X1)|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[31,99,theory(equality)])).
% cnf(134,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|~atomic(tptp3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[58,76,theory(equality)])).
% cnf(135,plain,(X1=tptp3|leaf_occ(X2,X3)|~occurrence_of(esk4_2(X2,X3),X1)|~subactivity_occurrence(X2,X3)|~arboreal(X2)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[31,76,theory(equality)])).
% cnf(137,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|$false|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(rw,[status(thm)],[134,36,theory(equality)])).
% cnf(138,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(cn,[status(thm)],[137,theory(equality)])).
% cnf(157,plain,(min_precedes(X1,esk4_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[107,75,theory(equality)])).
% cnf(166,plain,(X1=tptp2|leaf_occ(X2,X3)|occurrence_of(esk6_2(X2,X3),tptp1)|~occurrence_of(esk6_2(X2,X3),X1)|~subactivity_occurrence(X2,X3)|~arboreal(X2)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[31,72,theory(equality)])).
% cnf(177,plain,(leaf_occ(X1,X2)|~leaf(esk4_2(X1,X2),tptp0)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[52,73,theory(equality)])).
% cnf(197,plain,(esk7_2(X1,esk8_3(X2,X3,X4))=X2|~min_precedes(X3,X4,X2)|~leaf_occ(X1,esk8_3(X2,X3,X4))),inference(spm,[status(thm)],[131,85,theory(equality)])).
% cnf(333,plain,(leaf(X1,X2)|~leaf_occ(X1,esk8_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[83,197,theory(equality)])).
% cnf(365,plain,(esk6_2(X1,X2)=esk4_2(esk4_2(X1,X2),X3)|esk5_2(X1,X2)=esk4_2(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|leaf_occ(esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~arboreal(esk4_2(X1,X2))|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[77,157,theory(equality)])).
% cnf(2241,plain,(esk4_2(esk4_2(X1,X2),X3)=esk6_2(X1,X2)|esk4_2(esk4_2(X1,X2),X3)=esk5_2(X1,X2)|leaf_occ(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[365,138])).
% cnf(2243,plain,(leaf_occ(esk4_2(X1,X2),X3)|occurrence_of(esk6_2(X1,X2),tptp3)|esk4_2(esk4_2(X1,X2),X3)=esk5_2(X1,X2)|leaf_occ(X1,X2)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~arboreal(esk4_2(X1,X2))|~occurrence_of(X3,tptp0)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[76,2241,theory(equality)])).
% cnf(316330,plain,(esk4_2(esk4_2(X1,X2),X3)=esk5_2(X1,X2)|leaf_occ(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[2243,138])).
% cnf(316603,plain,(X1=tptp3|leaf_occ(esk4_2(X2,X3),X4)|leaf_occ(X2,X3)|occurrence_of(esk6_2(X2,X3),tptp3)|~subactivity_occurrence(esk4_2(X2,X3),X4)|~arboreal(esk4_2(X2,X3))|~occurrence_of(esk5_2(X2,X3),X1)|~occurrence_of(X4,tptp0)|~subactivity_occurrence(X2,X3)|~arboreal(X2)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[135,316330,theory(equality)])).
% cnf(775655,plain,(X1=tptp3|leaf_occ(esk4_2(X2,X3),X4)|leaf_occ(X2,X3)|occurrence_of(esk6_2(X2,X3),tptp3)|~subactivity_occurrence(esk4_2(X2,X3),X4)|~subactivity_occurrence(X2,X3)|~arboreal(X2)|~occurrence_of(esk5_2(X2,X3),X1)|~occurrence_of(X4,tptp0)|~occurrence_of(X3,tptp0)),inference(csr,[status(thm)],[316603,138])).
% cnf(775657,plain,(tptp4=tptp3|leaf_occ(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[775655,74,theory(equality)])).
% cnf(775658,plain,(leaf_occ(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~subactivity_occurrence(esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X2,tptp0)),inference(sr,[status(thm)],[775657,28,theory(equality)])).
% cnf(775662,plain,(leaf(esk4_2(X1,X2),X3)|leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~min_precedes(X4,X5,X3)|~subactivity_occurrence(esk4_2(X1,X2),esk8_3(X3,X4,X5))|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(esk8_3(X3,X4,X5),tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[333,775658,theory(equality)])).
% cnf(775959,plain,(leaf_occ(X1,X2)|leaf(esk4_2(X1,X2),X3)|occurrence_of(esk6_2(X1,X2),tptp3)|~min_precedes(X4,esk4_2(X1,X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(esk8_3(X3,X4,esk4_2(X1,X2)),tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[775662,97,theory(equality)])).
% cnf(776637,plain,(leaf_occ(X1,X2)|leaf(esk4_2(X1,X2),tptp0)|occurrence_of(esk6_2(X1,X2),tptp3)|~min_precedes(X3,esk4_2(X1,X2),tptp0)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[775959,99,theory(equality)])).
% cnf(776638,plain,(leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~min_precedes(X3,esk4_2(X1,X2),tptp0)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[776637,177])).
% cnf(776669,plain,(leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[776638,157,theory(equality)])).
% cnf(776671,plain,(X1=tptp3|leaf_occ(X2,X3)|~occurrence_of(esk6_2(X2,X3),X1)|~subactivity_occurrence(X2,X3)|~arboreal(X2)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[31,776669,theory(equality)])).
% cnf(776694,plain,(tptp3=tptp2|leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp1)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[166,776669,theory(equality)])).
% cnf(776702,plain,(leaf_occ(X1,X2)|occurrence_of(esk6_2(X1,X2),tptp1)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(sr,[status(thm)],[776694,62,theory(equality)])).
% cnf(777140,plain,(tptp1=tptp3|leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[776671,776702,theory(equality)])).
% cnf(777148,plain,(leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)),inference(sr,[status(thm)],[777140,61,theory(equality)])).
% cnf(777154,negated_conjecture,(~subactivity_occurrence(esk10_0,esk11_0)|~arboreal(esk10_0)|~occurrence_of(esk11_0,tptp0)),inference(spm,[status(thm)],[114,777148,theory(equality)])).
% cnf(777301,negated_conjecture,($false|~arboreal(esk10_0)|~occurrence_of(esk11_0,tptp0)),inference(rw,[status(thm)],[777154,116,theory(equality)])).
% cnf(777302,negated_conjecture,($false|$false|~occurrence_of(esk11_0,tptp0)),inference(rw,[status(thm)],[777301,115,theory(equality)])).
% cnf(777303,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[777302,117,theory(equality)])).
% cnf(777304,negated_conjecture,($false),inference(cn,[status(thm)],[777303,theory(equality)])).
% cnf(777305,negated_conjecture,($false),777304,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 13664
% # ...of these trivial : 0
% # ...subsumed : 5894
% # ...remaining for further processing: 7770
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 3048
% # Backward-rewritten : 0
% # Generated clauses : 685974
% # ...of the previous two non-trivial : 676633
% # Contextual simplify-reflections : 18957
% # Paramodulations : 685963
% # Factorizations : 6
% # Equation resolutions : 0
% # Current number of processed clauses: 4720
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 7
% # Non-unit-clauses : 4706
% # Current number of unprocessed clauses: 311631
% # ...number of literals in the above : 4108390
% # Clause-clause subsumption calls (NU) : 2618024
% # Rec. Clause-clause subsumption calls : 591822
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 673 leaves, 8.42+/-29.809 terms/leaf
% # Paramod-from index: 109 leaves, 4.23+/-13.237 terms/leaf
% # Paramod-into index: 443 leaves, 6.81+/-26.897 terms/leaf
% # -------------------------------------------------
% # User time : 71.490 s
% # System time : 1.573 s
% # Total time : 73.063 s
% # Maximum resident set size: 0 pages
% PrfWatch: 96.24 CPU 99.86 WC
% FINAL PrfWatch: 96.24 CPU 99.87 WC
% SZS output end Solution for /tmp/SystemOnTPTP24309/PRO017+1.tptp
%
%------------------------------------------------------------------------------