%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO016+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 13:08:51 EDT 2023 % Result : Theorem 183.21s 25.47s % Output : Proof 183.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : PRO016+4 : TPTP v8.1.2. Released v4.0.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Aug 28 18:44:12 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.68 ________ _____ % 0.20/0.68 ___ __ \_________(_)________________________________ % 0.20/0.68 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.68 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.68 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.68 % 0.20/0.68 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.68 (2023-06-19) % 0.20/0.68 % 0.20/0.68 (c) Philipp Rümmer, 2009-2023 % 0.20/0.68 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.68 Amanda Stjerna. % 0.20/0.68 Free software under BSD-3-Clause. % 0.20/0.68 % 0.20/0.68 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.68 % 0.20/0.68 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.70 Running up to 7 provers in parallel. % 0.20/0.71 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.71 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.71 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.71 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.71 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.71 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.71 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.97/1.24 Prover 1: Preprocessing ... % 2.97/1.24 Prover 4: Preprocessing ... % 3.52/1.31 Prover 6: Preprocessing ... % 3.52/1.31 Prover 5: Preprocessing ... % 3.52/1.31 Prover 0: Preprocessing ... % 3.52/1.31 Prover 2: Preprocessing ... % 3.52/1.31 Prover 3: Preprocessing ... % 6.94/1.72 Prover 2: Constructing countermodel ... % 6.94/1.74 Prover 5: Proving ... % 7.71/1.85 Prover 3: Constructing countermodel ... % 8.14/1.91 Prover 1: Constructing countermodel ... % 8.14/1.91 Prover 6: Proving ... % 10.11/2.17 Prover 4: Constructing countermodel ... % 10.84/2.28 Prover 0: Proving ... % 72.72/10.38 Prover 2: stopped % 73.35/10.39 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 73.91/10.49 Prover 7: Preprocessing ... % 74.74/10.58 Prover 7: Constructing countermodel ... % 101.08/14.04 Prover 5: stopped % 101.08/14.04 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 101.22/14.10 Prover 8: Preprocessing ... % 102.13/14.22 Prover 8: Warning: ignoring some quantifiers % 102.75/14.26 Prover 8: Constructing countermodel ... % 115.80/16.08 Prover 1: stopped % 115.80/16.09 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 116.43/16.16 Prover 9: Preprocessing ... % 118.32/16.38 Prover 9: Constructing countermodel ... % 129.99/17.96 Prover 6: stopped % 129.99/17.96 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 130.68/18.06 Prover 10: Preprocessing ... % 131.33/18.10 Prover 10: Constructing countermodel ... % 182.68/25.43 Prover 7: Found proof (size 227) % 182.68/25.43 Prover 7: proved (15006ms) % 182.68/25.43 Prover 9: stopped % 182.68/25.43 Prover 0: stopped % 182.68/25.43 Prover 10: stopped % 182.68/25.44 Prover 3: stopped % 183.15/25.46 Prover 4: stopped % 183.21/25.47 Prover 8: stopped % 183.21/25.47 % 183.21/25.47 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 183.21/25.47 % 183.21/25.48 % SZS output start Proof for theBenchmark % 183.21/25.49 Assumptions after simplification: % 183.21/25.49 --------------------------------- % 183.21/25.49 % 183.21/25.49 (goals) % 183.21/25.50 $i(tptp2) & $i(tptp1) & $i(tptp3) & $i(tptp0) & ? [v0: $i] : ? [v1: $i] : % 183.21/25.50 ($i(v1) & $i(v0) & arboreal(v0) & subactivity_occurrence(v0, v1) & % 183.21/25.50 occurrence_of(v1, tptp0) & ~ leaf_occ(v0, v1) & ! [v2: $i] : ! [v3: $i] : % 183.21/25.50 ( ~ $i(v3) | ~ $i(v2) | ~ next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, % 183.21/25.50 v3, tptp0) | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp2) | ~ % 183.21/25.50 occurrence_of(v2, tptp3) | occurrence_of(v3, tptp1) | ? [v4: $i] : % 183.21/25.50 ($i(v4) & min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp1))) & ! % 183.21/25.50 [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ next_subocc(v0, v2, % 183.21/25.50 tptp0) | ~ min_precedes(v2, v3, tptp0) | ~ leaf_occ(v3, v1) | ~ % 183.21/25.50 occurrence_of(v3, tptp2) | ~ occurrence_of(v2, tptp3) | ? [v4: $i] : % 183.21/25.50 ($i(v4) & ((min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp2)) | % 183.21/25.50 (min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp1))))) & ! [v2: % 183.21/25.50 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ next_subocc(v0, v2, tptp0) % 183.21/25.50 | ~ min_precedes(v2, v3, tptp0) | ~ leaf_occ(v3, v1) | ~ % 183.21/25.50 occurrence_of(v3, tptp1) | ~ occurrence_of(v2, tptp3) | occurrence_of(v3, % 183.21/25.50 tptp2) | ? [v4: $i] : ($i(v4) & min_precedes(v2, v4, tptp0) & % 183.21/25.50 occurrence_of(v4, tptp2))) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 183.21/25.50 $i(v2) | ~ next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, v3, tptp0) | % 183.21/25.50 ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp1) | ~ occurrence_of(v2, % 183.21/25.50 tptp3) | ? [v4: $i] : ($i(v4) & ((min_precedes(v2, v4, tptp0) & % 183.21/25.50 occurrence_of(v4, tptp2)) | (min_precedes(v2, v4, tptp0) & % 183.21/25.50 occurrence_of(v4, tptp1)))))) % 183.21/25.50 % 183.21/25.50 (sos) % 183.21/25.50 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 183.21/25.50 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 183.21/25.50 root(v2, v0))) % 183.21/25.50 % 183.21/25.50 (sos_02) % 183.21/25.50 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 183.21/25.50 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | % 183.21/25.50 ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | % 183.21/25.50 min_precedes(v2, v3, v0)) % 183.21/25.50 % 183.21/25.50 (sos_04) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 183.21/25.51 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ arboreal(v3) | ~ arboreal(v2) | ~ % 183.21/25.51 subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ % 183.21/25.51 occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 183.21/25.51 % 183.21/25.51 (sos_06) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 183.21/25.51 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 183.21/25.51 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 183.21/25.51 occurrence_of(v3, v0))) % 183.21/25.51 % 183.21/25.51 (sos_08) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 183.21/25.51 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 183.21/25.51 % 183.21/25.51 (sos_09) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 183.21/25.51 | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v1, v3, v2) | ~ leaf_occ(v1, v0) % 183.21/25.51 | ~ occurrence_of(v0, v2)) % 183.21/25.51 % 183.21/25.51 (sos_11) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 183.21/25.51 subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0: $i] : ! % 183.21/25.51 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v0, v1) | % 183.21/25.51 activity_occurrence(v0)) % 183.21/25.51 % 183.21/25.51 (sos_12) % 183.21/25.51 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 183.21/25.51 & activity(v1) & occurrence_of(v0, v1))) % 183.21/25.51 % 183.21/25.51 (sos_13) % 183.21/25.51 ! [v0: $i] : ( ~ $i(v0) | ~ legal(v0) | arboreal(v0)) % 183.21/25.51 % 183.21/25.51 (sos_17) % 183.21/25.51 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | % 183.21/25.51 legal(v0)) % 183.21/25.51 % 183.21/25.51 (sos_18) % 183.39/25.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 183.39/25.51 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 183.39/25.51 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 183.39/25.51 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 183.39/25.51 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 183.39/25.51 % 183.39/25.51 (sos_19) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 183.39/25.52 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 183.39/25.52 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 183.39/25.52 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 183.39/25.52 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 183.39/25.52 % 183.39/25.52 (sos_22) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 183.39/25.52 ~ min_precedes(v0, v1, v2) | ~ root(v1, v2)) % 183.39/25.52 % 183.39/25.52 (sos_25) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 183.39/25.52 ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0: $i] : ! [v1: $i] : ! % 183.39/25.52 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 183.39/25.52 arboreal(v0)) % 183.39/25.52 % 183.39/25.52 (sos_26) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 183.39/25.52 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 183.39/25.52 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 183.39/25.52 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 183.39/25.52 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 183.39/25.52 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 183.39/25.52 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 183.39/25.52 min_precedes(v0, v3, v2))) % 183.39/25.52 % 183.39/25.52 (sos_27) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 183.39/25.52 | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | ~ % 183.39/25.52 subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | % 183.39/25.52 subactivity_occurrence(v0, v3)) % 183.39/25.52 % 183.39/25.52 (sos_28) % 183.39/25.52 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 183.39/25.52 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, % 183.39/25.52 v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 183.39/25.52 % 183.39/25.52 (sos_32) % 183.39/25.52 $i(tptp2) & $i(tptp1) & $i(tptp4) & $i(tptp3) & $i(tptp0) & ! [v0: $i] : ! % 183.39/25.52 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | ~ % 183.39/25.52 subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, tptp0) | leaf_occ(v0, % 183.39/25.52 v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v4) & $i(v3) & $i(v2) % 183.39/25.52 & next_subocc(v3, v4, tptp0) & next_subocc(v2, v3, tptp0) & % 183.39/25.52 next_subocc(v0, v2, tptp0) & leaf_occ(v4, v1) & occurrence_of(v3, tptp4) & % 183.39/25.52 occurrence_of(v2, tptp3) & (occurrence_of(v4, tptp2) | occurrence_of(v4, % 183.39/25.52 tptp1)))) % 183.39/25.52 % 183.39/25.52 (sos_34) % 183.39/25.52 $i(tptp0) & ~ atomic(tptp0) % 183.39/25.52 % 183.39/25.52 Further assumptions not needed in the proof: % 183.39/25.52 -------------------------------------------- % 183.39/25.52 sos_01, sos_03, sos_05, sos_07, sos_10, sos_14, sos_15, sos_16, sos_20, sos_21, % 183.39/25.52 sos_23, sos_24, sos_29, sos_30, sos_31, sos_33, sos_35, sos_36, sos_37, sos_38, % 183.39/25.52 sos_39, sos_40, sos_41, sos_42, sos_43, sos_44 % 183.39/25.52 % 183.39/25.52 Those formulas are unsatisfiable: % 183.39/25.52 --------------------------------- % 183.39/25.52 % 183.39/25.52 Begin of proof % 183.39/25.52 | % 183.39/25.52 | ALPHA: (goals) implies: % 183.39/25.53 | (1) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & arboreal(v0) & % 183.39/25.53 | subactivity_occurrence(v0, v1) & occurrence_of(v1, tptp0) & ~ % 183.39/25.53 | leaf_occ(v0, v1) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 183.39/25.53 | | ~ next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, v3, tptp0) | % 183.39/25.53 | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp2) | ~ % 183.39/25.53 | occurrence_of(v2, tptp3) | occurrence_of(v3, tptp1) | ? [v4: $i] : % 183.39/25.53 | ($i(v4) & min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp1))) % 183.39/25.53 | & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ % 183.39/25.53 | next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, v3, tptp0) | ~ % 183.39/25.53 | leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp2) | ~ % 183.39/25.53 | occurrence_of(v2, tptp3) | ? [v4: $i] : ($i(v4) & % 183.39/25.53 | ((min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp2)) | % 183.39/25.53 | (min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp1))))) & % 183.39/25.53 | ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ % 183.39/25.53 | next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, v3, tptp0) | ~ % 183.39/25.53 | leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp1) | ~ % 183.39/25.53 | occurrence_of(v2, tptp3) | occurrence_of(v3, tptp2) | ? [v4: $i] : % 183.39/25.53 | ($i(v4) & min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp2))) % 183.39/25.53 | & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ % 183.39/25.53 | next_subocc(v0, v2, tptp0) | ~ min_precedes(v2, v3, tptp0) | ~ % 183.39/25.53 | leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp1) | ~ % 183.39/25.53 | occurrence_of(v2, tptp3) | ? [v4: $i] : ($i(v4) & % 183.39/25.53 | ((min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp2)) | % 183.39/25.53 | (min_precedes(v2, v4, tptp0) & occurrence_of(v4, tptp1)))))) % 183.39/25.53 | % 183.39/25.53 | ALPHA: (sos_34) implies: % 183.39/25.53 | (2) ~ atomic(tptp0) % 183.39/25.53 | % 183.39/25.53 | ALPHA: (sos_32) implies: % 183.39/25.53 | (3) $i(tptp0) % 183.39/25.53 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | % 183.39/25.53 | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, tptp0) | % 183.39/25.53 | leaf_occ(v0, v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v4) % 183.39/25.53 | & $i(v3) & $i(v2) & next_subocc(v3, v4, tptp0) & next_subocc(v2, % 183.39/25.53 | v3, tptp0) & next_subocc(v0, v2, tptp0) & leaf_occ(v4, v1) & % 183.39/25.53 | occurrence_of(v3, tptp4) & occurrence_of(v2, tptp3) & % 183.39/25.53 | (occurrence_of(v4, tptp2) | occurrence_of(v4, tptp1)))) % 183.39/25.53 | % 183.39/25.53 | ALPHA: (sos_26) implies: % 183.39/25.53 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 183.39/25.53 | $i(v0) | ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 183.39/25.53 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 183.39/25.53 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 183.39/25.53 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 183.39/25.53 | % 183.39/25.53 | ALPHA: (sos_25) implies: % 183.39/25.53 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 183.39/25.53 | $i(v0) | ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 183.39/25.53 | % 183.39/25.53 | ALPHA: (sos_19) implies: % 183.39/25.53 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 183.39/25.53 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 183.39/25.54 | root(v0, v2) & occurrence_of(v1, v2))) % 183.39/25.54 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 183.39/25.54 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 183.39/25.54 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 183.39/25.54 | % 183.39/25.54 | ALPHA: (sos_18) implies: % 183.39/25.54 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 183.39/25.54 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 183.39/25.54 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 183.39/25.54 | % 183.39/25.54 | ALPHA: (sos_11) implies: % 183.39/25.54 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 183.39/25.54 | subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 183.39/25.54 | % 183.39/25.54 | DELTA: instantiating (1) with fresh symbols all_36_0, all_36_1 gives: % 183.39/25.54 | (12) $i(all_36_0) & $i(all_36_1) & arboreal(all_36_1) & % 183.39/25.54 | subactivity_occurrence(all_36_1, all_36_0) & occurrence_of(all_36_0, % 183.39/25.54 | tptp0) & ~ leaf_occ(all_36_1, all_36_0) & ! [v0: $i] : ! [v1: $i] % 183.39/25.54 | : ( ~ $i(v1) | ~ $i(v0) | ~ next_subocc(all_36_1, v0, tptp0) | ~ % 183.39/25.54 | min_precedes(v0, v1, tptp0) | ~ leaf_occ(v1, all_36_0) | ~ % 183.39/25.54 | occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | % 183.39/25.54 | occurrence_of(v1, tptp1) | ? [v2: $i] : ($i(v2) & min_precedes(v0, % 183.39/25.54 | v2, tptp0) & occurrence_of(v2, tptp1))) & ! [v0: $i] : ! [v1: % 183.39/25.54 | $i] : ( ~ $i(v1) | ~ $i(v0) | ~ next_subocc(all_36_1, v0, tptp0) | % 183.39/25.54 | ~ min_precedes(v0, v1, tptp0) | ~ leaf_occ(v1, all_36_0) | ~ % 183.39/25.54 | occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ? [v2: $i] % 183.39/25.54 | : ($i(v2) & ((min_precedes(v0, v2, tptp0) & occurrence_of(v2, % 183.39/25.54 | tptp2)) | (min_precedes(v0, v2, tptp0) & occurrence_of(v2, % 183.39/25.54 | tptp1))))) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 183.39/25.54 | $i(v0) | ~ next_subocc(all_36_1, v0, tptp0) | ~ min_precedes(v0, % 183.39/25.54 | v1, tptp0) | ~ leaf_occ(v1, all_36_0) | ~ occurrence_of(v1, % 183.39/25.54 | tptp1) | ~ occurrence_of(v0, tptp3) | occurrence_of(v1, tptp2) | % 183.39/25.54 | ? [v2: $i] : ($i(v2) & min_precedes(v0, v2, tptp0) & % 183.39/25.54 | occurrence_of(v2, tptp2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 183.39/25.54 | $i(v1) | ~ $i(v0) | ~ next_subocc(all_36_1, v0, tptp0) | ~ % 183.39/25.54 | min_precedes(v0, v1, tptp0) | ~ leaf_occ(v1, all_36_0) | ~ % 183.39/25.54 | occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ? [v2: $i] % 183.39/25.54 | : ($i(v2) & ((min_precedes(v0, v2, tptp0) & occurrence_of(v2, % 183.39/25.54 | tptp2)) | (min_precedes(v0, v2, tptp0) & occurrence_of(v2, % 183.39/25.54 | tptp1))))) % 183.39/25.54 | % 183.39/25.54 | ALPHA: (12) implies: % 183.39/25.54 | (13) ~ leaf_occ(all_36_1, all_36_0) % 183.39/25.54 | (14) occurrence_of(all_36_0, tptp0) % 183.39/25.54 | (15) subactivity_occurrence(all_36_1, all_36_0) % 183.39/25.54 | (16) arboreal(all_36_1) % 183.39/25.54 | (17) $i(all_36_1) % 183.39/25.54 | (18) $i(all_36_0) % 183.39/25.54 | % 183.39/25.54 | GROUND_INST: instantiating (sos) with tptp0, all_36_0, simplifying with (2), % 183.39/25.54 | (3), (14), (18) gives: % 183.39/25.54 | (19) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_36_0) & % 183.39/25.54 | root(v0, tptp0)) % 183.39/25.54 | % 183.39/25.54 | GROUND_INST: instantiating (11) with all_36_1, all_36_0, simplifying with % 183.39/25.54 | (15), (17), (18) gives: % 183.39/25.54 | (20) activity_occurrence(all_36_0) % 183.39/25.54 | % 183.39/25.55 | GROUND_INST: instantiating (4) with all_36_1, all_36_0, simplifying with (13), % 183.39/25.55 | (14), (15), (16), (17), (18) gives: % 183.39/25.55 | (21) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 183.39/25.55 | next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) & % 183.39/25.55 | next_subocc(all_36_1, v0, tptp0) & leaf_occ(v2, all_36_0) & % 183.39/25.55 | occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & % 183.39/25.55 | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 183.39/25.55 | % 183.39/25.55 | DELTA: instantiating (19) with fresh symbol all_49_0 gives: % 183.39/25.55 | (22) $i(all_49_0) & subactivity_occurrence(all_49_0, all_36_0) & % 183.39/25.55 | root(all_49_0, tptp0) % 183.39/25.55 | % 183.39/25.55 | ALPHA: (22) implies: % 183.39/25.55 | (23) root(all_49_0, tptp0) % 183.39/25.55 | (24) subactivity_occurrence(all_49_0, all_36_0) % 183.39/25.55 | (25) $i(all_49_0) % 183.39/25.55 | % 183.39/25.55 | DELTA: instantiating (21) with fresh symbols all_51_0, all_51_1, all_51_2 % 183.39/25.55 | gives: % 183.56/25.55 | (26) $i(all_51_0) & $i(all_51_1) & $i(all_51_2) & next_subocc(all_51_1, % 183.56/25.55 | all_51_0, tptp0) & next_subocc(all_51_2, all_51_1, tptp0) & % 183.56/25.55 | next_subocc(all_36_1, all_51_2, tptp0) & leaf_occ(all_51_0, all_36_0) % 183.56/25.55 | & occurrence_of(all_51_1, tptp4) & occurrence_of(all_51_2, tptp3) & % 183.56/25.55 | (occurrence_of(all_51_0, tptp2) | occurrence_of(all_51_0, tptp1)) % 183.56/25.55 | % 183.56/25.55 | ALPHA: (26) implies: % 183.56/25.55 | (27) leaf_occ(all_51_0, all_36_0) % 183.56/25.55 | (28) next_subocc(all_36_1, all_51_2, tptp0) % 183.56/25.55 | (29) next_subocc(all_51_2, all_51_1, tptp0) % 183.56/25.55 | (30) next_subocc(all_51_1, all_51_0, tptp0) % 183.56/25.55 | (31) $i(all_51_2) % 183.56/25.55 | (32) $i(all_51_1) % 183.56/25.55 | (33) $i(all_51_0) % 183.56/25.55 | % 183.56/25.55 | PRED_UNIFY: (13), (27) imply: % 183.56/25.55 | (34) ~ (all_51_0 = all_36_1) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (9) with all_36_1, all_36_0, tptp0, simplifying % 183.56/25.55 | with (3), (14), (15), (17), (18) gives: % 183.56/25.55 | (35) ~ root(all_36_1, tptp0) | root_occ(all_36_1, all_36_0) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (sos_17) with all_49_0, tptp0, simplifying with % 183.56/25.55 | (3), (23), (25) gives: % 183.56/25.55 | (36) legal(all_49_0) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (9) with all_49_0, all_36_0, tptp0, simplifying % 183.56/25.55 | with (3), (14), (18), (23), (24), (25) gives: % 183.56/25.55 | (37) root_occ(all_49_0, all_36_0) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (sos_02) with tptp0, all_36_0, all_36_1, all_51_0, % 183.56/25.55 | simplifying with (3), (14), (15), (16), (17), (18), (27), (33) % 183.56/25.55 | gives: % 183.56/25.55 | (38) all_51_0 = all_36_1 | min_precedes(all_36_1, all_51_0, tptp0) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (10) with all_51_0, all_36_0, simplifying with % 183.56/25.55 | (18), (27), (33) gives: % 183.56/25.55 | (39) ? [v0: $i] : ($i(v0) & leaf(all_51_0, v0) & % 183.56/25.55 | subactivity_occurrence(all_51_0, all_36_0) & occurrence_of(all_36_0, % 183.56/25.55 | v0)) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (sos_12) with all_36_0, simplifying with (18), (20) % 183.56/25.55 | gives: % 183.56/25.55 | (40) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_36_0, v0)) % 183.56/25.55 | % 183.56/25.55 | GROUND_INST: instantiating (5) with all_36_1, all_51_2, tptp0, simplifying % 183.56/25.55 | with (3), (17), (28), (31) gives: % 183.56/25.55 | (41) min_precedes(all_36_1, all_51_2, tptp0) % 183.56/25.55 | % 183.56/25.56 | GROUND_INST: instantiating (7) with all_51_2, all_51_1, tptp0, simplifying % 183.56/25.56 | with (3), (29), (31), (32) gives: % 183.56/25.56 | (42) arboreal(all_51_2) % 183.56/25.56 | % 183.56/25.56 | GROUND_INST: instantiating (5) with all_51_2, all_51_1, tptp0, simplifying % 183.56/25.56 | with (3), (29), (31), (32) gives: % 183.56/25.56 | (43) min_precedes(all_51_2, all_51_1, tptp0) % 183.56/25.56 | % 183.56/25.56 | GROUND_INST: instantiating (7) with all_51_1, all_51_0, tptp0, simplifying % 183.56/25.56 | with (3), (30), (32), (33) gives: % 183.56/25.56 | (44) arboreal(all_51_1) % 183.56/25.56 | % 183.56/25.56 | GROUND_INST: instantiating (5) with all_51_1, all_51_0, tptp0, simplifying % 183.56/25.56 | with (3), (30), (32), (33) gives: % 183.56/25.56 | (45) min_precedes(all_51_1, all_51_0, tptp0) % 183.56/25.56 | % 183.56/25.56 | DELTA: instantiating (40) with fresh symbol all_63_0 gives: % 183.56/25.56 | (46) $i(all_63_0) & activity(all_63_0) & occurrence_of(all_36_0, all_63_0) % 183.56/25.56 | % 183.56/25.56 | ALPHA: (46) implies: % 183.56/25.56 | (47) occurrence_of(all_36_0, all_63_0) % 183.56/25.56 | (48) $i(all_63_0) % 183.56/25.56 | % 183.56/25.56 | DELTA: instantiating (39) with fresh symbol all_69_0 gives: % 183.56/25.56 | (49) $i(all_69_0) & leaf(all_51_0, all_69_0) & % 183.56/25.56 | subactivity_occurrence(all_51_0, all_36_0) & occurrence_of(all_36_0, % 183.56/25.56 | all_69_0) % 183.56/25.56 | % 183.56/25.56 | ALPHA: (49) implies: % 183.56/25.56 | (50) occurrence_of(all_36_0, all_69_0) % 183.56/25.56 | (51) subactivity_occurrence(all_51_0, all_36_0) % 183.56/25.56 | (52) $i(all_69_0) % 183.56/25.56 | % 183.56/25.56 | BETA: splitting (38) gives: % 183.56/25.56 | % 183.56/25.56 | Case 1: % 183.56/25.56 | | % 183.56/25.56 | | (53) min_precedes(all_36_1, all_51_0, tptp0) % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, all_69_0, % 183.56/25.56 | | simplifying with (3), (14), (18), (50), (52) gives: % 183.56/25.56 | | (54) all_69_0 = tptp0 % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_08) with all_36_0, all_63_0, all_69_0, % 183.56/25.56 | | simplifying with (18), (47), (48), (50), (52) gives: % 183.56/25.56 | | (55) all_69_0 = all_63_0 % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (8) with all_49_0, all_36_0, simplifying with % 183.56/25.56 | | (18), (25), (37) gives: % 183.56/25.56 | | (56) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_49_0, all_36_0) & % 183.56/25.56 | | root(all_49_0, v0) & occurrence_of(all_36_0, v0)) % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_22) with all_36_1, all_49_0, tptp0, % 183.56/25.56 | | simplifying with (3), (17), (23), (25) gives: % 183.56/25.56 | | (57) ~ min_precedes(all_36_1, all_49_0, tptp0) % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_06) with tptp0, all_36_1, all_51_2, % 183.56/25.56 | | simplifying with (3), (17), (31), (41) gives: % 183.56/25.56 | | (58) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_51_2, v0) & % 183.56/25.56 | | subactivity_occurrence(all_36_1, v0) & occurrence_of(v0, tptp0)) % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_09) with all_36_0, all_51_2, tptp0, % 183.56/25.56 | | all_51_1, simplifying with (3), (14), (18), (31), (32), (43) % 183.56/25.56 | | gives: % 183.56/25.56 | | (59) ~ leaf_occ(all_51_2, all_36_0) % 183.56/25.56 | | % 183.56/25.56 | | GROUND_INST: instantiating (sos_27) with all_51_2, all_51_1, tptp0, % 183.56/25.56 | | all_36_0, simplifying with (3), (14), (18), (31), (32), (43) % 183.56/25.56 | | gives: % 183.56/25.57 | | (60) ~ subactivity_occurrence(all_51_1, all_36_0) | % 183.56/25.57 | | subactivity_occurrence(all_51_2, all_36_0) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (sos_27) with all_51_1, all_51_0, tptp0, % 183.56/25.57 | | all_36_0, simplifying with (3), (14), (18), (32), (33), (45), % 183.56/25.57 | | (51) gives: % 183.56/25.57 | | (61) subactivity_occurrence(all_51_1, all_36_0) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (sos_06) with tptp0, all_51_1, all_51_0, % 183.56/25.57 | | simplifying with (3), (32), (33), (45) gives: % 183.56/25.57 | | (62) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_51_0, v0) & % 183.56/25.57 | | subactivity_occurrence(all_51_1, v0) & occurrence_of(v0, tptp0)) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (sos_02) with tptp0, all_36_0, all_49_0, % 183.56/25.57 | | all_51_0, simplifying with (3), (14), (18), (24), (25), (27), % 183.56/25.57 | | (33) gives: % 183.56/25.57 | | (63) all_51_0 = all_49_0 | ~ arboreal(all_49_0) | min_precedes(all_49_0, % 183.56/25.57 | | all_51_0, tptp0) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (4) with all_49_0, all_36_0, simplifying with % 183.56/25.57 | | (14), (18), (24), (25) gives: % 183.56/25.57 | | (64) ~ arboreal(all_49_0) | leaf_occ(all_49_0, all_36_0) | ? [v0: $i] : % 183.56/25.57 | | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 183.56/25.57 | | next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) & % 183.56/25.57 | | next_subocc(all_49_0, v0, tptp0) & leaf_occ(v2, all_36_0) & % 183.56/25.57 | | occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & % 183.56/25.57 | | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (4) with all_51_2, all_36_0, simplifying with % 183.56/25.57 | | (14), (18), (31), (42) gives: % 183.56/25.57 | | (65) ~ subactivity_occurrence(all_51_2, all_36_0) | leaf_occ(all_51_2, % 183.56/25.57 | | all_36_0) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & % 183.56/25.57 | | $i(v1) & $i(v0) & next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, % 183.56/25.57 | | tptp0) & next_subocc(all_51_2, v0, tptp0) & leaf_occ(v2, % 183.56/25.57 | | all_36_0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) % 183.56/25.57 | | & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (4) with all_51_1, all_36_0, simplifying with % 183.56/25.57 | | (14), (18), (32), (44) gives: % 183.56/25.57 | | (66) ~ subactivity_occurrence(all_51_1, all_36_0) | leaf_occ(all_51_1, % 183.56/25.57 | | all_36_0) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & % 183.56/25.57 | | $i(v1) & $i(v0) & next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, % 183.56/25.57 | | tptp0) & next_subocc(all_51_1, v0, tptp0) & leaf_occ(v2, % 183.56/25.57 | | all_36_0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) % 183.56/25.57 | | & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.57 | | % 183.56/25.57 | | GROUND_INST: instantiating (sos_13) with all_49_0, simplifying with (25), % 183.56/25.57 | | (36) gives: % 183.56/25.57 | | (67) arboreal(all_49_0) % 183.56/25.57 | | % 183.56/25.57 | | COMBINE_EQS: (54), (55) imply: % 183.56/25.57 | | (68) all_63_0 = tptp0 % 183.56/25.57 | | % 183.56/25.57 | | DELTA: instantiating (58) with fresh symbol all_113_0 gives: % 183.56/25.57 | | (69) $i(all_113_0) & subactivity_occurrence(all_51_2, all_113_0) & % 183.56/25.57 | | subactivity_occurrence(all_36_1, all_113_0) & % 183.56/25.57 | | occurrence_of(all_113_0, tptp0) % 183.56/25.57 | | % 183.56/25.57 | | ALPHA: (69) implies: % 183.56/25.57 | | (70) occurrence_of(all_113_0, tptp0) % 183.56/25.57 | | (71) subactivity_occurrence(all_36_1, all_113_0) % 183.56/25.57 | | (72) $i(all_113_0) % 183.56/25.57 | | % 183.56/25.57 | | DELTA: instantiating (62) with fresh symbol all_117_0 gives: % 183.56/25.58 | | (73) $i(all_117_0) & subactivity_occurrence(all_51_0, all_117_0) & % 183.56/25.58 | | subactivity_occurrence(all_51_1, all_117_0) & % 183.56/25.58 | | occurrence_of(all_117_0, tptp0) % 183.56/25.58 | | % 183.56/25.58 | | ALPHA: (73) implies: % 183.56/25.58 | | (74) occurrence_of(all_117_0, tptp0) % 183.56/25.58 | | (75) subactivity_occurrence(all_51_1, all_117_0) % 183.56/25.58 | | (76) $i(all_117_0) % 183.56/25.58 | | % 183.56/25.58 | | DELTA: instantiating (56) with fresh symbol all_119_0 gives: % 183.56/25.58 | | (77) $i(all_119_0) & subactivity_occurrence(all_49_0, all_36_0) & % 183.56/25.58 | | root(all_49_0, all_119_0) & occurrence_of(all_36_0, all_119_0) % 183.56/25.58 | | % 183.56/25.58 | | ALPHA: (77) implies: % 183.56/25.58 | | (78) occurrence_of(all_36_0, all_119_0) % 183.56/25.58 | | (79) $i(all_119_0) % 183.56/25.58 | | % 183.56/25.58 | | BETA: splitting (60) gives: % 183.56/25.58 | | % 183.56/25.58 | | Case 1: % 183.56/25.58 | | | % 183.56/25.58 | | | (80) ~ subactivity_occurrence(all_51_1, all_36_0) % 183.56/25.58 | | | % 183.56/25.58 | | | PRED_UNIFY: (61), (80) imply: % 183.56/25.58 | | | (81) $false % 183.56/25.58 | | | % 183.56/25.58 | | | CLOSE: (81) is inconsistent. % 183.56/25.58 | | | % 183.56/25.58 | | Case 2: % 183.56/25.58 | | | % 183.56/25.58 | | | (82) subactivity_occurrence(all_51_2, all_36_0) % 183.56/25.58 | | | % 183.56/25.58 | | | BETA: splitting (65) gives: % 183.56/25.58 | | | % 183.56/25.58 | | | Case 1: % 183.56/25.58 | | | | % 183.56/25.58 | | | | (83) ~ subactivity_occurrence(all_51_2, all_36_0) % 183.56/25.58 | | | | % 183.56/25.58 | | | | PRED_UNIFY: (82), (83) imply: % 183.56/25.58 | | | | (84) $false % 183.56/25.58 | | | | % 183.56/25.58 | | | | CLOSE: (84) is inconsistent. % 183.56/25.58 | | | | % 183.56/25.58 | | | Case 2: % 183.56/25.58 | | | | % 183.56/25.58 | | | | (85) leaf_occ(all_51_2, all_36_0) | ? [v0: $i] : ? [v1: $i] : ? % 183.56/25.58 | | | | [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & next_subocc(v1, v2, % 183.56/25.58 | | | | tptp0) & next_subocc(v0, v1, tptp0) & next_subocc(all_51_2, % 183.56/25.58 | | | | v0, tptp0) & leaf_occ(v2, all_36_0) & occurrence_of(v1, % 183.56/25.58 | | | | tptp4) & occurrence_of(v0, tptp3) & (occurrence_of(v2, % 183.56/25.58 | | | | tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.58 | | | | % 183.56/25.58 | | | | BETA: splitting (85) gives: % 183.56/25.58 | | | | % 183.56/25.58 | | | | Case 1: % 183.56/25.58 | | | | | % 183.56/25.58 | | | | | (86) leaf_occ(all_51_2, all_36_0) % 183.56/25.58 | | | | | % 183.56/25.58 | | | | | PRED_UNIFY: (59), (86) imply: % 183.56/25.58 | | | | | (87) $false % 183.56/25.58 | | | | | % 183.56/25.58 | | | | | CLOSE: (87) is inconsistent. % 183.56/25.58 | | | | | % 183.56/25.58 | | | | Case 2: % 183.56/25.58 | | | | | % 183.56/25.58 | | | | | (88) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 183.56/25.58 | | | | | $i(v0) & next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, % 183.56/25.58 | | | | | tptp0) & next_subocc(all_51_2, v0, tptp0) & leaf_occ(v2, % 183.56/25.58 | | | | | all_36_0) & occurrence_of(v1, tptp4) & occurrence_of(v0, % 183.56/25.58 | | | | | tptp3) & (occurrence_of(v2, tptp2) | occurrence_of(v2, % 183.56/25.58 | | | | | tptp1))) % 183.56/25.58 | | | | | % 183.56/25.58 | | | | | DELTA: instantiating (88) with fresh symbols all_156_0, all_156_1, % 183.56/25.58 | | | | | all_156_2 gives: % 183.56/25.59 | | | | | (89) $i(all_156_0) & $i(all_156_1) & $i(all_156_2) & % 183.56/25.59 | | | | | next_subocc(all_156_1, all_156_0, tptp0) & % 183.56/25.59 | | | | | next_subocc(all_156_2, all_156_1, tptp0) & % 183.56/25.59 | | | | | next_subocc(all_51_2, all_156_2, tptp0) & leaf_occ(all_156_0, % 183.56/25.59 | | | | | all_36_0) & occurrence_of(all_156_1, tptp4) & % 183.56/25.59 | | | | | occurrence_of(all_156_2, tptp3) & (occurrence_of(all_156_0, % 183.56/25.59 | | | | | tptp2) | occurrence_of(all_156_0, tptp1)) % 183.56/25.59 | | | | | % 183.56/25.59 | | | | | ALPHA: (89) implies: % 183.56/25.59 | | | | | (90) leaf_occ(all_156_0, all_36_0) % 183.56/25.59 | | | | | (91) next_subocc(all_51_2, all_156_2, tptp0) % 183.56/25.59 | | | | | (92) next_subocc(all_156_2, all_156_1, tptp0) % 183.56/25.59 | | | | | (93) next_subocc(all_156_1, all_156_0, tptp0) % 183.56/25.59 | | | | | (94) $i(all_156_2) % 183.56/25.59 | | | | | (95) $i(all_156_1) % 183.56/25.59 | | | | | (96) $i(all_156_0) % 183.56/25.59 | | | | | % 183.56/25.59 | | | | | PRED_UNIFY: (53), (57) imply: % 183.56/25.59 | | | | | (97) ~ (all_51_0 = all_49_0) % 183.56/25.59 | | | | | % 183.56/25.59 | | | | | BETA: splitting (63) gives: % 183.56/25.59 | | | | | % 183.56/25.59 | | | | | Case 1: % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | (98) min_precedes(all_49_0, all_51_0, tptp0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, all_119_0, % 183.56/25.59 | | | | | | simplifying with (3), (14), (18), (78), (79) gives: % 183.56/25.59 | | | | | | (99) all_119_0 = tptp0 % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (9) with all_36_1, all_113_0, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (17), (70), (71), (72) gives: % 183.56/25.59 | | | | | | (100) ~ root(all_36_1, tptp0) | root_occ(all_36_1, all_113_0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (sos_09) with all_36_0, all_51_1, tptp0, % 183.56/25.59 | | | | | | all_51_0, simplifying with (3), (14), (18), (32), (33), % 183.56/25.59 | | | | | | (45) gives: % 183.56/25.59 | | | | | | (101) ~ leaf_occ(all_51_1, all_36_0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (sos_28) with all_51_0, all_156_0, % 183.56/25.59 | | | | | | all_36_0, tptp0, simplifying with (2), (3), (14), (18), % 183.56/25.59 | | | | | | (27), (33), (90), (96) gives: % 183.56/25.59 | | | | | | (102) all_156_0 = all_51_0 % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (10) with all_156_0, all_36_0, % 183.56/25.59 | | | | | | simplifying with (18), (90), (96) gives: % 183.56/25.59 | | | | | | (103) ? [v0: $i] : ($i(v0) & leaf(all_156_0, v0) & % 183.56/25.59 | | | | | | subactivity_occurrence(all_156_0, all_36_0) & % 183.56/25.59 | | | | | | occurrence_of(all_36_0, v0)) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (sos_09) with all_36_0, all_49_0, tptp0, % 183.56/25.59 | | | | | | all_51_0, simplifying with (3), (14), (18), (25), (33), % 183.56/25.59 | | | | | | (98) gives: % 183.56/25.59 | | | | | | (104) ~ leaf_occ(all_49_0, all_36_0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (5) with all_51_2, all_156_2, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (31), (91), (94) gives: % 183.56/25.59 | | | | | | (105) min_precedes(all_51_2, all_156_2, tptp0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (7) with all_156_2, all_156_1, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (92), (94), (95) gives: % 183.56/25.59 | | | | | | (106) arboreal(all_156_2) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (5) with all_156_2, all_156_1, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (92), (94), (95) gives: % 183.56/25.59 | | | | | | (107) min_precedes(all_156_2, all_156_1, tptp0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (7) with all_156_1, all_156_0, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (93), (95), (96) gives: % 183.56/25.59 | | | | | | (108) arboreal(all_156_1) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | GROUND_INST: instantiating (5) with all_156_1, all_156_0, tptp0, % 183.56/25.59 | | | | | | simplifying with (3), (93), (95), (96) gives: % 183.56/25.59 | | | | | | (109) min_precedes(all_156_1, all_156_0, tptp0) % 183.56/25.59 | | | | | | % 183.56/25.59 | | | | | | DELTA: instantiating (103) with fresh symbol all_206_0 gives: % 183.56/25.60 | | | | | | (110) $i(all_206_0) & leaf(all_156_0, all_206_0) & % 183.56/25.60 | | | | | | subactivity_occurrence(all_156_0, all_36_0) & % 183.56/25.60 | | | | | | occurrence_of(all_36_0, all_206_0) % 183.56/25.60 | | | | | | % 183.56/25.60 | | | | | | ALPHA: (110) implies: % 183.56/25.60 | | | | | | (111) occurrence_of(all_36_0, all_206_0) % 183.56/25.60 | | | | | | (112) subactivity_occurrence(all_156_0, all_36_0) % 183.56/25.60 | | | | | | (113) $i(all_206_0) % 183.56/25.60 | | | | | | % 183.56/25.60 | | | | | | REDUCE: (93), (102) imply: % 183.56/25.60 | | | | | | (114) next_subocc(all_156_1, all_51_0, tptp0) % 183.56/25.60 | | | | | | % 183.56/25.60 | | | | | | REDUCE: (102), (109) imply: % 183.56/25.60 | | | | | | (115) min_precedes(all_156_1, all_51_0, tptp0) % 183.56/25.60 | | | | | | % 183.56/25.60 | | | | | | BETA: splitting (64) gives: % 183.56/25.60 | | | | | | % 183.56/25.60 | | | | | | Case 1: % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | (116) ~ arboreal(all_49_0) % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | PRED_UNIFY: (67), (116) imply: % 183.56/25.60 | | | | | | | (117) $false % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | CLOSE: (117) is inconsistent. % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | Case 2: % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | (118) leaf_occ(all_49_0, all_36_0) | ? [v0: $i] : ? [v1: $i] % 183.56/25.60 | | | | | | | : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 183.56/25.60 | | | | | | | next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) % 183.56/25.60 | | | | | | | & next_subocc(all_49_0, v0, tptp0) & leaf_occ(v2, % 183.56/25.60 | | | | | | | all_36_0) & occurrence_of(v1, tptp4) & % 183.56/25.60 | | | | | | | occurrence_of(v0, tptp3) & (occurrence_of(v2, tptp2) | % 183.56/25.60 | | | | | | | occurrence_of(v2, tptp1))) % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | BETA: splitting (118) gives: % 183.56/25.60 | | | | | | | % 183.56/25.60 | | | | | | | Case 1: % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | (119) leaf_occ(all_49_0, all_36_0) % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | PRED_UNIFY: (104), (119) imply: % 183.56/25.60 | | | | | | | | (120) $false % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | CLOSE: (120) is inconsistent. % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | Case 2: % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | (121) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & % 183.56/25.60 | | | | | | | | $i(v1) & $i(v0) & next_subocc(v1, v2, tptp0) & % 183.56/25.60 | | | | | | | | next_subocc(v0, v1, tptp0) & next_subocc(all_49_0, % 183.56/25.60 | | | | | | | | v0, tptp0) & leaf_occ(v2, all_36_0) & % 183.56/25.60 | | | | | | | | occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & % 183.56/25.60 | | | | | | | | (occurrence_of(v2, tptp2) | occurrence_of(v2, % 183.56/25.60 | | | | | | | | tptp1))) % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | DELTA: instantiating (121) with fresh symbols all_270_0, % 183.56/25.60 | | | | | | | | all_270_1, all_270_2 gives: % 183.56/25.60 | | | | | | | | (122) $i(all_270_0) & $i(all_270_1) & $i(all_270_2) & % 183.56/25.60 | | | | | | | | next_subocc(all_270_1, all_270_0, tptp0) & % 183.56/25.60 | | | | | | | | next_subocc(all_270_2, all_270_1, tptp0) & % 183.56/25.60 | | | | | | | | next_subocc(all_49_0, all_270_2, tptp0) & % 183.56/25.60 | | | | | | | | leaf_occ(all_270_0, all_36_0) & % 183.56/25.60 | | | | | | | | occurrence_of(all_270_1, tptp4) & % 183.56/25.60 | | | | | | | | occurrence_of(all_270_2, tptp3) & % 183.56/25.60 | | | | | | | | (occurrence_of(all_270_0, tptp2) | % 183.56/25.60 | | | | | | | | occurrence_of(all_270_0, tptp1)) % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | ALPHA: (122) implies: % 183.56/25.60 | | | | | | | | (123) leaf_occ(all_270_0, all_36_0) % 183.56/25.60 | | | | | | | | (124) $i(all_270_0) % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | BETA: splitting (66) gives: % 183.56/25.60 | | | | | | | | % 183.56/25.60 | | | | | | | | Case 1: % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | (125) ~ subactivity_occurrence(all_51_1, all_36_0) % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | PRED_UNIFY: (61), (125) imply: % 183.56/25.60 | | | | | | | | | (126) $false % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | CLOSE: (126) is inconsistent. % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | Case 2: % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | (127) leaf_occ(all_51_1, all_36_0) | ? [v0: $i] : ? [v1: % 183.56/25.60 | | | | | | | | | $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 183.56/25.60 | | | | | | | | | next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, % 183.56/25.60 | | | | | | | | | tptp0) & next_subocc(all_51_1, v0, tptp0) & % 183.56/25.60 | | | | | | | | | leaf_occ(v2, all_36_0) & occurrence_of(v1, tptp4) & % 183.56/25.60 | | | | | | | | | occurrence_of(v0, tptp3) & (occurrence_of(v2, % 183.56/25.60 | | | | | | | | | tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | BETA: splitting (127) gives: % 183.56/25.60 | | | | | | | | | % 183.56/25.60 | | | | | | | | | Case 1: % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | (128) leaf_occ(all_51_1, all_36_0) % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | PRED_UNIFY: (101), (128) imply: % 183.56/25.60 | | | | | | | | | | (129) $false % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | CLOSE: (129) is inconsistent. % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | Case 2: % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | (130) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & % 183.56/25.60 | | | | | | | | | | $i(v1) & $i(v0) & next_subocc(v1, v2, tptp0) & % 183.56/25.60 | | | | | | | | | | next_subocc(v0, v1, tptp0) & % 183.56/25.60 | | | | | | | | | | next_subocc(all_51_1, v0, tptp0) & leaf_occ(v2, % 183.56/25.60 | | | | | | | | | | all_36_0) & occurrence_of(v1, tptp4) & % 183.56/25.60 | | | | | | | | | | occurrence_of(v0, tptp3) & (occurrence_of(v2, % 183.56/25.60 | | | | | | | | | | tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | DELTA: instantiating (130) with fresh symbols all_295_0, % 183.56/25.60 | | | | | | | | | | all_295_1, all_295_2 gives: % 183.56/25.60 | | | | | | | | | | (131) $i(all_295_0) & $i(all_295_1) & $i(all_295_2) & % 183.56/25.60 | | | | | | | | | | next_subocc(all_295_1, all_295_0, tptp0) & % 183.56/25.60 | | | | | | | | | | next_subocc(all_295_2, all_295_1, tptp0) & % 183.56/25.60 | | | | | | | | | | next_subocc(all_51_1, all_295_2, tptp0) & % 183.56/25.60 | | | | | | | | | | leaf_occ(all_295_0, all_36_0) & % 183.56/25.60 | | | | | | | | | | occurrence_of(all_295_1, tptp4) & % 183.56/25.60 | | | | | | | | | | occurrence_of(all_295_2, tptp3) & % 183.56/25.60 | | | | | | | | | | (occurrence_of(all_295_0, tptp2) | % 183.56/25.60 | | | | | | | | | | occurrence_of(all_295_0, tptp1)) % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | ALPHA: (131) implies: % 183.56/25.60 | | | | | | | | | | (132) leaf_occ(all_295_0, all_36_0) % 183.56/25.60 | | | | | | | | | | (133) $i(all_295_0) % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | BETA: splitting (35) gives: % 183.56/25.60 | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | Case 1: % 183.56/25.60 | | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, % 183.56/25.60 | | | | | | | | | | | all_206_0, simplifying with (3), (14), (18), % 183.56/25.60 | | | | | | | | | | | (111), (113) gives: % 183.56/25.60 | | | | | | | | | | | (134) all_206_0 = tptp0 % 183.56/25.60 | | | | | | | | | | | % 183.56/25.60 | | | | | | | | | | | GROUND_INST: instantiating (sos_09) with all_36_0, all_156_2, % 183.56/25.60 | | | | | | | | | | | tptp0, all_156_1, simplifying with (3), (14), % 183.56/25.60 | | | | | | | | | | | (18), (94), (95), (107) gives: % 183.56/25.61 | | | | | | | | | | | (135) ~ leaf_occ(all_156_2, all_36_0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (6) with all_51_2, all_51_1, tptp0, % 183.56/25.61 | | | | | | | | | | | all_156_2, simplifying with (3), (29), (31), (32), % 183.56/25.61 | | | | | | | | | | | (94), (105) gives: % 183.56/25.61 | | | | | | | | | | | (136) ~ min_precedes(all_156_2, all_51_1, tptp0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_156_2, all_156_1, % 183.56/25.61 | | | | | | | | | | | tptp0, all_36_0, simplifying with (3), (14), (18), % 183.56/25.61 | | | | | | | | | | | (94), (95), (107) gives: % 183.56/25.61 | | | | | | | | | | | (137) ~ subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.61 | | | | | | | | | | | subactivity_occurrence(all_156_2, all_36_0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_156_1, all_51_0, % 183.56/25.61 | | | | | | | | | | | tptp0, all_36_0, simplifying with (3), (14), (18), % 183.56/25.61 | | | | | | | | | | | (33), (51), (95), (115) gives: % 183.56/25.61 | | | | | | | | | | | (138) subactivity_occurrence(all_156_1, all_36_0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (4) with all_156_2, all_36_0, % 183.56/25.61 | | | | | | | | | | | simplifying with (14), (18), (94), (106) gives: % 183.56/25.61 | | | | | | | | | | | (139) ~ subactivity_occurrence(all_156_2, all_36_0) | % 183.56/25.61 | | | | | | | | | | | leaf_occ(all_156_2, all_36_0) | ? [v0: $i] : ? % 183.56/25.61 | | | | | | | | | | | [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) % 183.56/25.61 | | | | | | | | | | | & next_subocc(v1, v2, tptp0) & next_subocc(v0, % 183.56/25.61 | | | | | | | | | | | v1, tptp0) & next_subocc(all_156_2, v0, tptp0) % 183.56/25.61 | | | | | | | | | | | & leaf_occ(v2, all_36_0) & occurrence_of(v1, % 183.56/25.61 | | | | | | | | | | | tptp4) & occurrence_of(v0, tptp3) & % 183.56/25.61 | | | | | | | | | | | (occurrence_of(v2, tptp2) | occurrence_of(v2, % 183.56/25.61 | | | | | | | | | | | tptp1))) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (sos_04) with tptp0, all_117_0, % 183.56/25.61 | | | | | | | | | | | all_156_1, all_51_1, simplifying with (3), (32), % 183.56/25.61 | | | | | | | | | | | (44), (74), (75), (76), (95), (108) gives: % 183.56/25.61 | | | | | | | | | | | (140) all_156_1 = all_51_1 | ~ % 183.56/25.61 | | | | | | | | | | | subactivity_occurrence(all_156_1, all_117_0) | % 183.56/25.61 | | | | | | | | | | | min_precedes(all_156_1, all_51_1, tptp0) | % 183.56/25.61 | | | | | | | | | | | min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (sos_04) with all_206_0, all_36_0, % 183.56/25.61 | | | | | | | | | | | all_156_1, all_51_1, simplifying with (18), (32), % 183.56/25.61 | | | | | | | | | | | (44), (61), (95), (108), (111), (113) gives: % 183.56/25.61 | | | | | | | | | | | (141) all_156_1 = all_51_1 | ~ % 183.56/25.61 | | | | | | | | | | | subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.61 | | | | | | | | | | | min_precedes(all_156_1, all_51_1, all_206_0) | % 183.56/25.61 | | | | | | | | | | | min_precedes(all_51_1, all_156_1, all_206_0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | GROUND_INST: instantiating (6) with all_156_1, all_51_0, tptp0, % 183.56/25.61 | | | | | | | | | | | all_51_1, simplifying with (3), (32), (33), (45), % 183.56/25.61 | | | | | | | | | | | (95), (114) gives: % 183.56/25.61 | | | | | | | | | | | (142) ~ min_precedes(all_156_1, all_51_1, tptp0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | REF_CLOSE: (3), (6), (30), (32), (33), (95), (107), (115), % 183.56/25.61 | | | | | | | | | | | (134), (135), (136), (137), (138), (139), (140), % 183.56/25.61 | | | | | | | | | | | (141), (142) are inconsistent by sub-proof #1. % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | Case 2: % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | (143) root(all_36_1, tptp0) % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | BETA: splitting (100) gives: % 183.56/25.61 | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | Case 1: % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | (144) ~ root(all_36_1, tptp0) % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | PRED_UNIFY: (143), (144) imply: % 183.56/25.61 | | | | | | | | | | | | (145) $false % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | CLOSE: (145) is inconsistent. % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | Case 2: % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, % 183.56/25.61 | | | | | | | | | | | | all_206_0, simplifying with (3), (14), (18), % 183.56/25.61 | | | | | | | | | | | | (111), (113) gives: % 183.56/25.61 | | | | | | | | | | | | (146) all_206_0 = tptp0 % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_28) with all_51_0, all_295_0, % 183.56/25.61 | | | | | | | | | | | | all_36_0, tptp0, simplifying with (2), (3), (14), % 183.56/25.61 | | | | | | | | | | | | (18), (27), (33), (132), (133) gives: % 183.56/25.61 | | | | | | | | | | | | (147) all_295_0 = all_51_0 % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_28) with all_270_0, all_295_0, % 183.56/25.61 | | | | | | | | | | | | all_36_0, tptp0, simplifying with (2), (3), (14), % 183.56/25.61 | | | | | | | | | | | | (18), (123), (124), (132), (133) gives: % 183.56/25.61 | | | | | | | | | | | | (148) all_295_0 = all_270_0 % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_09) with all_36_0, all_156_2, % 183.56/25.61 | | | | | | | | | | | | tptp0, all_156_1, simplifying with (3), (14), % 183.56/25.61 | | | | | | | | | | | | (18), (94), (95), (107) gives: % 183.56/25.61 | | | | | | | | | | | | (149) ~ leaf_occ(all_156_2, all_36_0) % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (6) with all_51_2, all_51_1, tptp0, % 183.56/25.61 | | | | | | | | | | | | all_156_2, simplifying with (3), (29), (31), (32), % 183.56/25.61 | | | | | | | | | | | | (94), (105) gives: % 183.56/25.61 | | | | | | | | | | | | (150) ~ min_precedes(all_156_2, all_51_1, tptp0) % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_156_2, all_156_1, % 183.56/25.61 | | | | | | | | | | | | tptp0, all_36_0, simplifying with (3), (14), (18), % 183.56/25.61 | | | | | | | | | | | | (94), (95), (107) gives: % 183.56/25.61 | | | | | | | | | | | | (151) ~ subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.61 | | | | | | | | | | | | subactivity_occurrence(all_156_2, all_36_0) % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_156_1, all_51_0, % 183.56/25.61 | | | | | | | | | | | | tptp0, all_36_0, simplifying with (3), (14), (18), % 183.56/25.61 | | | | | | | | | | | | (33), (51), (95), (115) gives: % 183.56/25.61 | | | | | | | | | | | | (152) subactivity_occurrence(all_156_1, all_36_0) % 183.56/25.61 | | | | | | | | | | | | % 183.56/25.61 | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_156_2, all_36_0, % 183.56/25.61 | | | | | | | | | | | | simplifying with (14), (18), (94), (106) gives: % 183.56/25.62 | | | | | | | | | | | | (153) ~ subactivity_occurrence(all_156_2, all_36_0) | % 183.56/25.62 | | | | | | | | | | | | leaf_occ(all_156_2, all_36_0) | ? [v0: $i] : ? % 183.56/25.62 | | | | | | | | | | | | [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) % 183.56/25.62 | | | | | | | | | | | | & next_subocc(v1, v2, tptp0) & next_subocc(v0, % 183.56/25.62 | | | | | | | | | | | | v1, tptp0) & next_subocc(all_156_2, v0, tptp0) % 183.56/25.62 | | | | | | | | | | | | & leaf_occ(v2, all_36_0) & occurrence_of(v1, % 183.56/25.62 | | | | | | | | | | | | tptp4) & occurrence_of(v0, tptp3) & % 183.56/25.62 | | | | | | | | | | | | (occurrence_of(v2, tptp2) | occurrence_of(v2, % 183.56/25.62 | | | | | | | | | | | | tptp1))) % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | GROUND_INST: instantiating (sos_04) with tptp0, all_117_0, % 183.56/25.62 | | | | | | | | | | | | all_156_1, all_51_1, simplifying with (3), (32), % 183.56/25.62 | | | | | | | | | | | | (44), (74), (75), (76), (95), (108) gives: % 183.56/25.62 | | | | | | | | | | | | (154) all_156_1 = all_51_1 | ~ % 183.56/25.62 | | | | | | | | | | | | subactivity_occurrence(all_156_1, all_117_0) | % 183.56/25.62 | | | | | | | | | | | | min_precedes(all_156_1, all_51_1, tptp0) | % 183.56/25.62 | | | | | | | | | | | | min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | GROUND_INST: instantiating (sos_04) with all_206_0, all_36_0, % 183.56/25.62 | | | | | | | | | | | | all_156_1, all_51_1, simplifying with (18), (32), % 183.56/25.62 | | | | | | | | | | | | (44), (61), (95), (108), (111), (113) gives: % 183.56/25.62 | | | | | | | | | | | | (155) all_156_1 = all_51_1 | ~ % 183.56/25.62 | | | | | | | | | | | | subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.62 | | | | | | | | | | | | min_precedes(all_156_1, all_51_1, all_206_0) | % 183.56/25.62 | | | | | | | | | | | | min_precedes(all_51_1, all_156_1, all_206_0) % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | GROUND_INST: instantiating (6) with all_156_1, all_51_0, tptp0, % 183.56/25.62 | | | | | | | | | | | | all_51_1, simplifying with (3), (32), (33), (45), % 183.56/25.62 | | | | | | | | | | | | (95), (114) gives: % 183.56/25.62 | | | | | | | | | | | | (156) ~ min_precedes(all_156_1, all_51_1, tptp0) % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | COMBINE_EQS: (147), (148) imply: % 183.56/25.62 | | | | | | | | | | | | (157) all_270_0 = all_51_0 % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | SIMP: (157) implies: % 183.56/25.62 | | | | | | | | | | | | (158) all_270_0 = all_51_0 % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | | REF_CLOSE: (3), (6), (30), (32), (33), (95), (107), (115), % 183.56/25.62 | | | | | | | | | | | | (146), (149), (150), (151), (152), (153), (154), % 183.56/25.62 | | | | | | | | | | | | (155), (156) are inconsistent by sub-proof #1. % 183.56/25.62 | | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | | End of split % 183.56/25.62 | | | | | | | | | | | % 183.56/25.62 | | | | | | | | | | End of split % 183.56/25.62 | | | | | | | | | | % 183.56/25.62 | | | | | | | | | End of split % 183.56/25.62 | | | | | | | | | % 183.56/25.62 | | | | | | | | End of split % 183.56/25.62 | | | | | | | | % 183.56/25.62 | | | | | | | End of split % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | End of split % 183.56/25.62 | | | | | | % 183.56/25.62 | | | | | Case 2: % 183.56/25.62 | | | | | | % 183.56/25.62 | | | | | | (159) all_51_0 = all_49_0 | ~ arboreal(all_49_0) % 183.56/25.62 | | | | | | % 183.56/25.62 | | | | | | BETA: splitting (159) gives: % 183.56/25.62 | | | | | | % 183.56/25.62 | | | | | | Case 1: % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | (160) ~ arboreal(all_49_0) % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | PRED_UNIFY: (67), (160) imply: % 183.56/25.62 | | | | | | | (161) $false % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | CLOSE: (161) is inconsistent. % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | Case 2: % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | (162) all_51_0 = all_49_0 % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | REDUCE: (97), (162) imply: % 183.56/25.62 | | | | | | | (163) $false % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | | CLOSE: (163) is inconsistent. % 183.56/25.62 | | | | | | | % 183.56/25.62 | | | | | | End of split % 183.56/25.62 | | | | | | % 183.56/25.62 | | | | | End of split % 183.56/25.62 | | | | | % 183.56/25.62 | | | | End of split % 183.56/25.62 | | | | % 183.56/25.62 | | | End of split % 183.56/25.62 | | | % 183.56/25.62 | | End of split % 183.56/25.62 | | % 183.56/25.62 | Case 2: % 183.56/25.62 | | % 183.56/25.62 | | (164) all_51_0 = all_36_1 % 183.56/25.62 | | % 183.56/25.62 | | REDUCE: (34), (164) imply: % 183.56/25.62 | | (165) $false % 183.56/25.62 | | % 183.56/25.62 | | CLOSE: (165) is inconsistent. % 183.56/25.62 | | % 183.56/25.62 | End of split % 183.56/25.62 | % 183.56/25.62 End of proof % 183.56/25.62 % 183.56/25.62 Sub-proof #1 shows that the following formulas are inconsistent: % 183.56/25.62 ---------------------------------------------------------------- % 183.56/25.62 (1) ~ min_precedes(all_156_2, all_51_1, tptp0) % 183.56/25.62 (2) $i(all_51_0) % 183.56/25.62 (3) all_156_1 = all_51_1 | ~ subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.62 min_precedes(all_156_1, all_51_1, all_206_0) | min_precedes(all_51_1, % 183.56/25.62 all_156_1, all_206_0) % 183.56/25.62 (4) ~ subactivity_occurrence(all_156_2, all_36_0) | leaf_occ(all_156_2, % 183.56/25.62 all_36_0) | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) % 183.56/25.62 & $i(v0) & next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) & % 183.56/25.62 next_subocc(all_156_2, v0, tptp0) & leaf_occ(v2, all_36_0) & % 183.56/25.62 occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & % 183.56/25.62 (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 183.56/25.62 (5) all_156_1 = all_51_1 | ~ subactivity_occurrence(all_156_1, all_117_0) | % 183.56/25.62 min_precedes(all_156_1, all_51_1, tptp0) | min_precedes(all_51_1, % 183.56/25.62 all_156_1, tptp0) % 183.56/25.62 (6) $i(all_156_1) % 183.56/25.62 (7) all_206_0 = tptp0 % 183.56/25.62 (8) min_precedes(all_156_1, all_51_0, tptp0) % 183.56/25.62 (9) ~ min_precedes(all_156_1, all_51_1, tptp0) % 183.56/25.62 (10) $i(all_51_1) % 183.56/25.62 (11) $i(tptp0) % 183.56/25.62 (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 183.56/25.62 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 183.56/25.62 min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 183.56/25.62 (13) ~ subactivity_occurrence(all_156_1, all_36_0) | % 183.56/25.62 subactivity_occurrence(all_156_2, all_36_0) % 183.56/25.62 (14) next_subocc(all_51_1, all_51_0, tptp0) % 183.56/25.62 (15) min_precedes(all_156_2, all_156_1, tptp0) % 183.56/25.62 (16) subactivity_occurrence(all_156_1, all_36_0) % 183.56/25.62 (17) ~ leaf_occ(all_156_2, all_36_0) % 183.56/25.62 % 183.56/25.62 Begin of proof % 183.56/25.62 | % 183.56/25.62 | BETA: splitting (13) gives: % 183.56/25.62 | % 183.56/25.62 | Case 1: % 183.56/25.62 | | % 183.56/25.62 | | (18) ~ subactivity_occurrence(all_156_1, all_36_0) % 183.56/25.62 | | % 183.56/25.62 | | PRED_UNIFY: (16), (18) imply: % 183.56/25.62 | | (19) $false % 183.56/25.62 | | % 183.56/25.62 | | CLOSE: (19) is inconsistent. % 183.56/25.62 | | % 183.56/25.62 | Case 2: % 183.56/25.62 | | % 183.56/25.62 | | (20) subactivity_occurrence(all_156_2, all_36_0) % 183.56/25.62 | | % 183.56/25.62 | | BETA: splitting (4) gives: % 183.56/25.62 | | % 183.56/25.62 | | Case 1: % 183.56/25.62 | | | % 183.56/25.62 | | | (21) ~ subactivity_occurrence(all_156_2, all_36_0) % 183.56/25.62 | | | % 183.56/25.62 | | | PRED_UNIFY: (20), (21) imply: % 183.56/25.62 | | | (22) $false % 183.56/25.62 | | | % 183.56/25.62 | | | CLOSE: (22) is inconsistent. % 183.56/25.62 | | | % 183.56/25.62 | | Case 2: % 183.56/25.62 | | | % 183.56/25.63 | | | (23) leaf_occ(all_156_2, all_36_0) | ? [v0: $i] : ? [v1: $i] : ? % 183.56/25.63 | | | [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & next_subocc(v1, v2, tptp0) % 183.56/25.63 | | | & next_subocc(v0, v1, tptp0) & next_subocc(all_156_2, v0, tptp0) % 183.56/25.63 | | | & leaf_occ(v2, all_36_0) & occurrence_of(v1, tptp4) & % 183.56/25.63 | | | occurrence_of(v0, tptp3) & (occurrence_of(v2, tptp2) | % 183.56/25.63 | | | occurrence_of(v2, tptp1))) % 183.56/25.63 | | | % 183.56/25.63 | | | BETA: splitting (23) gives: % 183.56/25.63 | | | % 183.56/25.63 | | | Case 1: % 183.56/25.63 | | | | % 183.56/25.63 | | | | (24) leaf_occ(all_156_2, all_36_0) % 183.56/25.63 | | | | % 183.56/25.63 | | | | PRED_UNIFY: (17), (24) imply: % 183.56/25.63 | | | | (25) $false % 183.56/25.63 | | | | % 183.56/25.63 | | | | CLOSE: (25) is inconsistent. % 183.56/25.63 | | | | % 183.56/25.63 | | | Case 2: % 183.56/25.63 | | | | % 183.56/25.63 | | | | % 183.56/25.63 | | | | PRED_UNIFY: (1), (15) imply: % 183.56/25.63 | | | | (26) ~ (all_156_1 = all_51_1) % 183.56/25.63 | | | | % 183.56/25.63 | | | | BETA: splitting (5) gives: % 183.56/25.63 | | | | % 183.56/25.63 | | | | Case 1: % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | (27) min_precedes(all_156_1, all_51_1, tptp0) % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | PRED_UNIFY: (9), (27) imply: % 183.56/25.63 | | | | | (28) $false % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | CLOSE: (28) is inconsistent. % 183.56/25.63 | | | | | % 183.56/25.63 | | | | Case 2: % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | (29) all_156_1 = all_51_1 | ~ subactivity_occurrence(all_156_1, % 183.56/25.63 | | | | | all_117_0) | min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | BETA: splitting (29) gives: % 183.56/25.63 | | | | | % 183.56/25.63 | | | | | Case 1: % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | (30) min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | GROUND_INST: instantiating (12) with all_51_1, all_51_0, tptp0, % 183.56/25.63 | | | | | | all_156_1, simplifying with (2), (6), (8), (10), (11), % 183.56/25.63 | | | | | | (14), (30) gives: % 183.56/25.63 | | | | | | (31) $false % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | CLOSE: (31) is inconsistent. % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | Case 2: % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | (32) ~ min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | BETA: splitting (3) gives: % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | | Case 1: % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | (33) ~ subactivity_occurrence(all_156_1, all_36_0) % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | PRED_UNIFY: (16), (33) imply: % 183.56/25.63 | | | | | | | (34) $false % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | CLOSE: (34) is inconsistent. % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | Case 2: % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | (35) all_156_1 = all_51_1 | min_precedes(all_156_1, all_51_1, % 183.56/25.63 | | | | | | | all_206_0) | min_precedes(all_51_1, all_156_1, % 183.56/25.63 | | | | | | | all_206_0) % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | BETA: splitting (35) gives: % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | | Case 1: % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | (36) min_precedes(all_156_1, all_51_1, all_206_0) % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | REDUCE: (7), (36) imply: % 183.56/25.63 | | | | | | | | (37) min_precedes(all_156_1, all_51_1, tptp0) % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | PRED_UNIFY: (9), (37) imply: % 183.56/25.63 | | | | | | | | (38) $false % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | CLOSE: (38) is inconsistent. % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | Case 2: % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | (39) all_156_1 = all_51_1 | min_precedes(all_51_1, all_156_1, % 183.56/25.63 | | | | | | | | all_206_0) % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | BETA: splitting (39) gives: % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | | Case 1: % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | (40) min_precedes(all_51_1, all_156_1, all_206_0) % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | REDUCE: (7), (40) imply: % 183.56/25.63 | | | | | | | | | (41) min_precedes(all_51_1, all_156_1, tptp0) % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | PRED_UNIFY: (32), (41) imply: % 183.56/25.63 | | | | | | | | | (42) $false % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | CLOSE: (42) is inconsistent. % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | Case 2: % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | (43) all_156_1 = all_51_1 % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | REDUCE: (26), (43) imply: % 183.56/25.63 | | | | | | | | | (44) $false % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | | CLOSE: (44) is inconsistent. % 183.56/25.63 | | | | | | | | | % 183.56/25.63 | | | | | | | | End of split % 183.56/25.63 | | | | | | | | % 183.56/25.63 | | | | | | | End of split % 183.56/25.63 | | | | | | | % 183.56/25.63 | | | | | | End of split % 183.56/25.63 | | | | | | % 183.56/25.63 | | | | | End of split % 183.56/25.63 | | | | | % 183.56/25.63 | | | | End of split % 183.56/25.63 | | | | % 183.56/25.63 | | | End of split % 183.56/25.63 | | | % 183.56/25.63 | | End of split % 183.56/25.63 | | % 183.56/25.63 | End of split % 183.56/25.63 | % 183.56/25.63 End of proof % 183.56/25.63 % SZS output end Proof for theBenchmark % 183.56/25.63 % 183.56/25.63 24947ms %------------------------------------------------------------------------------