%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO001+2 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n019.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:43 EDT 2023 % Result : Theorem 134.95s 18.76s % Output : Proof 136.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PRO001+2 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Aug 28 19:20:13 EDT 2023 % 0.12/0.35 % CPUTime : % 0.19/0.59 ________ _____ % 0.19/0.59 ___ __ \_________(_)________________________________ % 0.19/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.59 % 0.19/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.59 (2023-06-19) % 0.19/0.59 % 0.19/0.59 (c) Philipp Rümmer, 2009-2023 % 0.19/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.59 Amanda Stjerna. % 0.19/0.59 Free software under BSD-3-Clause. % 0.19/0.59 % 0.19/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.59 % 0.19/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.06/1.14 Prover 4: Preprocessing ... % 3.06/1.14 Prover 1: Preprocessing ... % 3.70/1.17 Prover 0: Preprocessing ... % 3.70/1.17 Prover 6: Preprocessing ... % 3.70/1.17 Prover 5: Preprocessing ... % 3.70/1.17 Prover 2: Preprocessing ... % 3.70/1.17 Prover 3: Preprocessing ... % 6.87/1.65 Prover 2: Constructing countermodel ... % 6.87/1.68 Prover 5: Proving ... % 8.24/1.87 Prover 3: Constructing countermodel ... % 8.86/1.89 Prover 1: Constructing countermodel ... % 8.86/1.89 Prover 6: Proving ... % 9.22/2.08 Prover 4: Constructing countermodel ... % 10.60/2.14 Prover 0: Proving ... % 73.23/10.33 Prover 2: stopped % 73.23/10.33 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 73.23/10.45 Prover 7: Preprocessing ... % 73.23/10.54 Prover 7: Constructing countermodel ... % 100.87/13.95 Prover 5: stopped % 100.87/13.96 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 101.47/14.01 Prover 8: Preprocessing ... % 102.50/14.12 Prover 8: Warning: ignoring some quantifiers % 102.50/14.12 Prover 8: Constructing countermodel ... % 115.23/15.97 Prover 1: stopped % 115.23/15.97 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 116.89/16.05 Prover 9: Preprocessing ... % 118.00/16.23 Prover 9: Constructing countermodel ... % 130.29/17.87 Prover 6: stopped % 130.29/17.89 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 130.75/17.98 Prover 10: Preprocessing ... % 130.75/18.04 Prover 10: Constructing countermodel ... % 134.31/18.35 Prover 7: Found proof (size 463) % 134.31/18.35 Prover 7: proved (7977ms) % 134.31/18.35 Prover 3: stopped % 134.31/18.35 Prover 10: stopped % 134.31/18.36 Prover 8: stopped % 134.31/18.36 Prover 4: stopped % 134.46/18.37 Prover 0: stopped % 134.95/18.75 Prover 9: stopped % 134.95/18.75 % 134.95/18.76 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 134.95/18.76 % 135.32/18.82 % SZS output start Proof for theBenchmark % 135.32/18.83 Assumptions after simplification: % 135.32/18.83 --------------------------------- % 135.32/18.83 % 135.32/18.83 (goals) % 135.35/18.84 $i(tptp0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 135.35/18.84 $i(v0) & tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 135.35/18.84 % 135.35/18.84 (sos_02) % 135.35/18.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 135.35/18.84 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 135.35/18.84 v2) | ~ occurrence_of(v2, v3)) % 135.35/18.84 % 135.35/18.84 (sos_03) % 135.35/18.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 135.35/18.84 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, % 135.35/18.84 v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 135.35/18.84 % 135.35/18.84 (sos_04) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 135.35/18.85 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 135.35/18.85 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 135.35/18.85 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 135.35/18.85 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 135.35/18.85 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 135.35/18.85 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 135.35/18.85 min_precedes(v0, v3, v2))) % 135.35/18.85 % 135.35/18.85 (sos_05) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.85 ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0: $i] : ! [v1: $i] : ! % 135.35/18.85 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 135.35/18.85 arboreal(v0)) % 135.35/18.85 % 135.35/18.85 (sos_07) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.85 ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 135.35/18.85 % 135.35/18.85 (sos_10) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.85 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 135.35/18.85 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 135.35/18.85 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 135.35/18.85 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 135.35/18.85 % 135.35/18.85 (sos_11) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.85 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 135.35/18.85 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 135.35/18.85 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 135.35/18.85 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 135.35/18.85 % 135.35/18.85 (sos_12) % 135.35/18.85 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | % 135.35/18.85 legal(v0)) % 135.35/18.85 % 135.35/18.85 (sos_13) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | ~ % 135.35/18.86 occurrence_of(v0, v1) | atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) % 135.35/18.86 | ~ $i(v0) | ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 135.35/18.86 % 135.35/18.86 (sos_14) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.86 ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0: $i] : ! [v1: $i] : % 135.35/18.86 ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v2, v0, v1) % 135.35/18.86 | leaf(v0, v1) | ? [v3: $i] : ($i(v3) & min_precedes(v0, v3, v1))) & ! % 135.35/18.86 [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | root(v0, % 135.35/18.86 v1) | ? [v2: $i] : ($i(v2) & min_precedes(v2, v0, v1))) & ! [v0: $i] : % 135.35/18.86 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | leaf(v0, v1) | ? [v2: % 135.35/18.86 $i] : ($i(v2) & min_precedes(v0, v2, v1))) % 135.35/18.86 % 135.35/18.86 (sos_15) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.86 ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | % 135.35/18.86 atocc(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.86 atocc(v0, v1) | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 135.35/18.86 occurrence_of(v0, v2))) % 135.35/18.86 % 135.35/18.86 (sos_16) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) | ~ % 135.35/18.86 legal(v0) | root(v0, v1)) % 135.35/18.86 % 135.35/18.86 (sos_17) % 135.35/18.86 ! [v0: $i] : ( ~ $i(v0) | ~ legal(v0) | arboreal(v0)) % 135.35/18.86 % 135.35/18.86 (sos_18) % 135.35/18.86 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 135.35/18.86 & activity(v1) & occurrence_of(v0, v1))) % 135.35/18.86 % 135.35/18.86 (sos_19) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.86 subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0: $i] : ! % 135.35/18.86 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v0, v1) | % 135.35/18.86 activity_occurrence(v0)) % 135.35/18.86 % 135.35/18.86 (sos_21) % 135.35/18.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 135.35/18.86 | ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | % 135.35/18.86 ~ min_precedes(v1, v3, v2)) % 135.35/18.86 % 135.35/18.86 (sos_22) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 135.35/18.87 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 135.35/18.87 % 135.35/18.87 (sos_24) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.87 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 135.35/18.87 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 135.35/18.87 occurrence_of(v3, v0))) % 135.35/18.87 % 135.35/18.87 (sos_26) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.87 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ? [v4: $i] : ($i(v4) & $i(v3) & % 135.35/18.87 subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, % 135.35/18.87 v3))) % 135.35/18.87 % 135.35/18.87 (sos_27) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v1, v0) | ? [v2: % 135.35/18.87 $i] : ($i(v2) & subactivity(v2, v0) & atocc(v1, v2))) % 135.35/18.87 % 135.35/18.87 (sos_28) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 135.35/18.87 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v3, v1) | ~ % 135.35/18.87 subactivity_occurrence(v2, v1) | ~ arboreal(v3) | ~ arboreal(v2) | ~ % 135.35/18.87 occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 135.35/18.87 % 135.35/18.87 (sos_29) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 135.35/18.87 | activity(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.87 occurrence_of(v1, v0) | activity_occurrence(v1)) % 135.35/18.87 % 135.35/18.87 (sos_30) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 135.35/18.87 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 135.35/18.87 root(v2, v0))) % 135.35/18.87 % 135.35/18.87 (sos_31) % 135.35/18.87 ! [v0: $i] : ( ~ $i(v0) | ~ activity(v0) | subactivity(v0, v0)) % 135.35/18.87 % 135.35/18.87 (sos_32) % 135.35/18.87 $i(tptp2) & $i(tptp3) & $i(tptp4) & $i(tptp0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 135.35/18.87 occurrence_of(v0, tptp0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 135.35/18.87 next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & % 135.35/18.87 occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, % 135.35/18.87 tptp3)))) % 135.35/18.87 % 135.35/18.87 (sos_34) % 135.35/18.87 $i(tptp0) & ~ atomic(tptp0) % 135.35/18.87 % 135.35/18.87 (sos_37) % 135.35/18.87 $i(tptp2) & atomic(tptp2) % 135.35/18.87 % 135.35/18.87 (sos_45) % 135.35/18.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 135.35/18.87 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, % 135.35/18.87 v1, v2, v3, v4) | activity(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 135.35/18.87 : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 135.35/18.87 ~ $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0: % 135.35/18.87 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | % 135.35/18.87 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, v1, v2, % 135.35/18.87 v3, v4) | root(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 135.35/18.87 [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.87 $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 135.35/18.87 % 135.35/18.87 (sos_46) % 135.35/18.88 $i(tptp2) & $i(tptp3) & $i(tptp4) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 135.35/18.88 ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.88 send_message(tptp2, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 135.35/18.88 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.88 send_message(tptp3, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 135.35/18.88 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.88 send_message(tptp4, v0, v1, v2, v3)) % 135.35/18.88 % 135.35/18.88 (sos_47) % 135.35/18.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 135.35/18.88 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 135.35/18.88 | ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | % 135.35/18.88 min_precedes(v3, v5, v4)) % 135.35/18.88 % 135.35/18.88 (sos_48) % 135.35/18.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 135.35/18.88 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.88 transmit_message(v0, v1, v2, v3, v4) | ~ atomic(v0)) & ! [v0: $i] : ! % 135.35/18.88 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | % 135.35/18.88 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ transmit_message(v0, v1, v2, v3, v4) | % 135.35/18.88 activity(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 135.35/18.88 [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.88 transmit_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0: $i] : ! [v1: % 135.35/18.88 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ % 135.35/18.88 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ transmit_message(v0, v1, v2, v3, v4) | % 135.35/18.88 root(v1, v2)) % 135.35/18.88 % 135.35/18.88 (sos_51) % 135.35/18.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 135.35/18.88 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 135.35/18.88 | ~ transmit_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | ? % 135.35/18.88 [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & send_message(v6, v1, v2, v3, v4) % 135.35/18.88 & root_occ(v7, v5) & occurrence_of(v7, v6))) % 135.35/18.88 % 135.35/18.88 (sos_52) % 135.35/18.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 135.35/18.88 ~ tptp1(v0, v1, v2) | ~ atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 135.35/18.88 $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ % 135.35/18.88 atomic(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ % 135.35/18.88 $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | activity(v0)) & ! [v0: $i] : ! % 135.35/18.88 [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, % 135.35/18.88 v2) | root(v2, v1)) % 135.35/18.88 % 135.35/18.88 (sos_53) % 135.35/18.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 135.35/18.88 | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | % 135.35/18.88 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & % 135.35/18.88 $i(v5) & $i(v4) & transmit_message(v4, v5, v6, v2, v1) & % 135.35/18.88 subactivity_occurrence(v7, v3) & occurrence_of(v7, v4))) % 135.35/18.88 % 135.35/18.88 Further assumptions not needed in the proof: % 135.35/18.88 -------------------------------------------- % 135.35/18.88 sos, sos_01, sos_06, sos_08, sos_09, sos_20, sos_23, sos_25, sos_33, sos_35, % 135.35/18.88 sos_36, sos_38, sos_39, sos_40, sos_41, sos_42, sos_43, sos_44, sos_49, sos_50, % 135.35/18.88 sos_54 % 135.35/18.88 % 135.35/18.88 Those formulas are unsatisfiable: % 135.35/18.88 --------------------------------- % 135.35/18.88 % 135.35/18.88 Begin of proof % 135.35/18.88 | % 135.35/18.88 | ALPHA: (goals) implies: % 135.35/18.88 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 135.35/18.88 | tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 135.35/18.88 | % 135.35/18.88 | ALPHA: (sos_52) implies: % 135.35/18.89 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.89 | $i(v0) | ~ tptp1(v0, v1, v2) | root(v2, v1)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_48) implies: % 135.35/18.89 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 135.35/18.89 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | transmit_message(v0, v1, v2, v3, v4) | root(v1, v2)) % 135.35/18.89 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 135.35/18.89 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | transmit_message(v0, v1, v2, v3, v4) | ~ atomic(v0)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_46) implies: % 135.35/18.89 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 135.35/18.89 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp3, v0, v1, v2, % 135.35/18.89 | v3)) % 135.35/18.89 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 135.35/18.89 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp2, v0, v1, v2, % 135.35/18.89 | v3)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_45) implies: % 135.35/18.89 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 135.35/18.89 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 135.35/18.89 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 135.35/18.89 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | send_message(v0, v1, v2, v3, v4) | activity(v0)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_37) implies: % 135.35/18.89 | (9) atomic(tptp2) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_34) implies: % 135.35/18.89 | (10) ~ atomic(tptp0) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_32) implies: % 135.35/18.89 | (11) $i(tptp0) % 135.35/18.89 | (12) $i(tptp3) % 135.35/18.89 | (13) $i(tptp2) % 135.35/18.89 | (14) ! [v0: $i] : ( ~ $i(v0) | ~ occurrence_of(v0, tptp0) | ? [v1: $i] : % 135.35/18.89 | ? [v2: $i] : ($i(v2) & $i(v1) & next_subocc(v1, v2, tptp0) & % 135.35/18.89 | leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & % 135.35/18.89 | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_29) implies: % 135.35/18.89 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_19) implies: % 135.35/18.89 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 135.35/18.89 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 135.35/18.89 | subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_15) implies: % 135.35/18.89 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) % 135.35/18.89 | | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 135.35/18.89 | occurrence_of(v0, v2))) % 135.35/18.89 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.89 | $i(v0) | ~ subactivity(v1, v2) | ~ atomic(v2) | ~ % 135.35/18.89 | occurrence_of(v0, v2) | atocc(v0, v1)) % 135.35/18.89 | % 135.35/18.89 | ALPHA: (sos_14) implies: % 135.35/18.90 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.90 | $i(v0) | ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3: $i] : % 135.35/18.90 | ($i(v3) & min_precedes(v0, v3, v1))) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (sos_13) implies: % 135.35/18.90 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atomic(v1) | % 135.35/18.90 | ~ occurrence_of(v0, v1) | arboreal(v0)) % 135.35/18.90 | (22) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | % 135.35/18.90 | ~ occurrence_of(v0, v1) | atomic(v1)) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (sos_11) implies: % 135.35/18.90 | (23) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 135.35/18.90 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 135.35/18.90 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 135.35/18.90 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.90 | $i(v0) | ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ % 135.35/18.90 | occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (sos_10) implies: % 135.35/18.90 | (25) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 135.35/18.90 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 135.35/18.90 | root(v0, v2) & occurrence_of(v1, v2))) % 135.35/18.90 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.90 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 135.35/18.90 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (sos_05) implies: % 135.35/18.90 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 135.35/18.90 | $i(v0) | ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (sos_04) implies: % 135.35/18.90 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 135.35/18.90 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 135.35/18.90 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 135.35/18.90 | % 135.35/18.90 | DELTA: instantiating (1) with fresh symbols all_46_0, all_46_1, all_46_2 % 135.35/18.90 | gives: % 135.35/18.90 | (29) $i(all_46_0) & $i(all_46_1) & $i(all_46_2) & tptp1(all_46_2, tptp0, % 135.35/18.90 | all_46_1) & occurrence_of(all_46_0, all_46_2) % 135.35/18.90 | % 135.35/18.90 | ALPHA: (29) implies: % 135.35/18.90 | (30) occurrence_of(all_46_0, all_46_2) % 135.35/18.90 | (31) tptp1(all_46_2, tptp0, all_46_1) % 135.35/18.90 | (32) $i(all_46_2) % 135.35/18.90 | (33) $i(all_46_1) % 135.35/18.90 | (34) $i(all_46_0) % 135.35/18.90 | % 135.35/18.90 | GROUND_INST: instantiating (sos_53) with all_46_2, tptp0, all_46_1, all_46_0, % 135.35/18.90 | simplifying with (11), (30), (31), (32), (33), (34) gives: % 135.35/18.90 | (35) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ($i(v3) & % 135.35/18.90 | $i(v2) & $i(v1) & $i(v0) & transmit_message(v0, v1, v2, all_46_1, % 135.35/18.90 | tptp0) & subactivity_occurrence(v3, all_46_0) & occurrence_of(v3, % 135.35/18.90 | v0)) % 135.35/18.90 | % 135.35/18.90 | GROUND_INST: instantiating (2) with all_46_2, tptp0, all_46_1, simplifying % 135.35/18.90 | with (11), (31), (32), (33) gives: % 135.35/18.90 | (36) root(all_46_1, tptp0) % 135.35/18.90 | % 135.35/18.90 | DELTA: instantiating (35) with fresh symbols all_58_0, all_58_1, all_58_2, % 135.35/18.90 | all_58_3 gives: % 135.35/18.91 | (37) $i(all_58_0) & $i(all_58_1) & $i(all_58_2) & $i(all_58_3) & % 135.35/18.91 | transmit_message(all_58_3, all_58_2, all_58_1, all_46_1, tptp0) & % 135.35/18.91 | subactivity_occurrence(all_58_0, all_46_0) & occurrence_of(all_58_0, % 135.35/18.91 | all_58_3) % 135.35/18.91 | % 135.35/18.91 | ALPHA: (37) implies: % 135.35/18.91 | (38) occurrence_of(all_58_0, all_58_3) % 135.35/18.91 | (39) subactivity_occurrence(all_58_0, all_46_0) % 135.35/18.91 | (40) transmit_message(all_58_3, all_58_2, all_58_1, all_46_1, tptp0) % 135.35/18.91 | (41) $i(all_58_3) % 135.35/18.91 | (42) $i(all_58_2) % 135.35/18.91 | (43) $i(all_58_1) % 135.35/18.91 | (44) $i(all_58_0) % 135.35/18.91 | % 135.35/18.91 | GROUND_INST: instantiating (21) with all_58_0, tptp2, simplifying with (9), % 135.35/18.91 | (13), (44) gives: % 135.35/18.91 | (45) ~ occurrence_of(all_58_0, tptp2) | arboreal(all_58_0) % 135.35/18.91 | % 135.35/18.91 | GROUND_INST: instantiating (sos_30) with all_58_3, all_58_0, simplifying with % 135.35/18.91 | (38), (41), (44) gives: % 135.35/18.91 | (46) atomic(all_58_3) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 135.35/18.91 | all_58_0) & root(v0, all_58_3)) % 135.35/18.91 | % 135.35/18.91 | GROUND_INST: instantiating (sos_27) with tptp0, all_46_1, simplifying with % 135.35/18.91 | (11), (33), (36) gives: % 135.35/18.91 | (47) ? [v0: $i] : ($i(v0) & subactivity(v0, tptp0) & atocc(all_46_1, v0)) % 135.35/18.91 | % 135.35/18.91 | GROUND_INST: instantiating (sos_12) with all_46_1, tptp0, simplifying with % 135.35/18.91 | (11), (33), (36) gives: % 135.35/18.91 | (48) legal(all_46_1) % 135.35/18.91 | % 135.35/18.91 | GROUND_INST: instantiating (16) with all_58_0, all_46_0, simplifying with % 135.35/18.91 | (34), (39), (44) gives: % 135.35/18.91 | (49) activity_occurrence(all_58_0) % 135.35/18.91 | % 135.73/18.91 | GROUND_INST: instantiating (sos_51) with all_58_3, all_58_2, all_58_1, % 135.73/18.91 | all_46_1, tptp0, all_58_0, simplifying with (11), (33), (38), % 135.73/18.91 | (40), (41), (42), (43), (44) gives: % 135.73/18.91 | (50) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & send_message(v0, % 135.73/18.91 | all_58_2, all_58_1, all_46_1, tptp0) & root_occ(v1, all_58_0) & % 135.73/18.91 | occurrence_of(v1, v0)) % 135.73/18.91 | % 135.73/18.91 | GROUND_INST: instantiating (3) with all_58_3, all_58_2, all_58_1, all_46_1, % 135.73/18.91 | tptp0, simplifying with (11), (33), (40), (41), (42), (43) gives: % 135.73/18.91 | (51) root(all_58_2, all_58_1) % 135.73/18.91 | % 135.73/18.91 | DELTA: instantiating (47) with fresh symbol all_70_0 gives: % 135.73/18.91 | (52) $i(all_70_0) & subactivity(all_70_0, tptp0) & atocc(all_46_1, % 135.73/18.91 | all_70_0) % 135.73/18.91 | % 135.73/18.91 | ALPHA: (52) implies: % 135.73/18.91 | (53) atocc(all_46_1, all_70_0) % 135.73/18.91 | (54) $i(all_70_0) % 135.73/18.91 | % 135.73/18.91 | DELTA: instantiating (50) with fresh symbols all_74_0, all_74_1 gives: % 135.73/18.91 | (55) $i(all_74_0) & $i(all_74_1) & send_message(all_74_1, all_58_2, % 135.73/18.91 | all_58_1, all_46_1, tptp0) & root_occ(all_74_0, all_58_0) & % 135.73/18.91 | occurrence_of(all_74_0, all_74_1) % 135.73/18.91 | % 135.73/18.91 | ALPHA: (55) implies: % 135.73/18.91 | (56) occurrence_of(all_74_0, all_74_1) % 135.73/18.91 | (57) root_occ(all_74_0, all_58_0) % 135.73/18.91 | (58) send_message(all_74_1, all_58_2, all_58_1, all_46_1, tptp0) % 135.73/18.91 | (59) $i(all_74_1) % 135.73/18.91 | (60) $i(all_74_0) % 135.73/18.91 | % 135.73/18.91 | GROUND_INST: instantiating (15) with all_74_1, all_74_0, simplifying with % 135.73/18.91 | (56), (59), (60) gives: % 135.73/18.91 | (61) activity_occurrence(all_74_0) % 135.73/18.91 | % 135.73/18.91 | GROUND_INST: instantiating (25) with all_74_0, all_58_0, simplifying with % 135.73/18.91 | (44), (57), (60) gives: % 135.73/18.91 | (62) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_74_0, all_58_0) & % 135.73/18.91 | root(all_74_0, v0) & occurrence_of(all_58_0, v0)) % 135.73/18.91 | % 135.73/18.91 | GROUND_INST: instantiating (sos_27) with all_58_1, all_58_2, simplifying with % 135.73/18.91 | (42), (43), (51) gives: % 135.73/18.91 | (63) ? [v0: $i] : ($i(v0) & subactivity(v0, all_58_1) & atocc(all_58_2, % 135.73/18.91 | v0)) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (sos_12) with all_58_2, all_58_1, simplifying with % 135.73/18.92 | (42), (43), (51) gives: % 135.73/18.92 | (64) legal(all_58_2) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (sos_17) with all_46_1, simplifying with (33), (48) % 135.73/18.92 | gives: % 135.73/18.92 | (65) arboreal(all_46_1) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (18) with all_46_1, all_70_0, simplifying with % 135.73/18.92 | (33), (53), (54) gives: % 135.73/18.92 | (66) ? [v0: $i] : ($i(v0) & subactivity(all_70_0, v0) & atomic(v0) & % 135.73/18.92 | occurrence_of(all_46_1, v0)) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (sos_18) with all_58_0, simplifying with (44), (49) % 135.73/18.92 | gives: % 135.73/18.92 | (67) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_58_0, v0)) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (sos_47) with all_74_1, all_58_2, all_58_1, % 135.73/18.92 | all_46_1, tptp0, all_74_0, simplifying with (11), (33), (42), % 135.73/18.92 | (43), (56), (58), (59), (60) gives: % 135.73/18.92 | (68) min_precedes(all_46_1, all_74_0, tptp0) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (6) with all_58_2, all_58_1, all_46_1, tptp0, % 135.73/18.92 | simplifying with (11), (33), (42), (43) gives: % 135.73/18.92 | (69) ~ send_message(tptp2, all_58_2, all_58_1, all_46_1, tptp0) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (5) with all_58_2, all_58_1, all_46_1, tptp0, % 135.73/18.92 | simplifying with (11), (33), (42), (43) gives: % 135.73/18.92 | (70) ~ send_message(tptp3, all_58_2, all_58_1, all_46_1, tptp0) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (8) with all_74_1, all_58_2, all_58_1, all_46_1, % 135.73/18.92 | tptp0, simplifying with (11), (33), (42), (43), (58), (59) gives: % 135.73/18.92 | (71) activity(all_74_1) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (7) with all_74_1, all_58_2, all_58_1, all_46_1, % 135.73/18.92 | tptp0, simplifying with (11), (33), (42), (43), (58), (59) gives: % 135.73/18.92 | (72) atomic(all_74_1) % 135.73/18.92 | % 135.73/18.92 | DELTA: instantiating (63) with fresh symbol all_94_0 gives: % 135.73/18.92 | (73) $i(all_94_0) & subactivity(all_94_0, all_58_1) & atocc(all_58_2, % 135.73/18.92 | all_94_0) % 135.73/18.92 | % 135.73/18.92 | ALPHA: (73) implies: % 135.73/18.92 | (74) atocc(all_58_2, all_94_0) % 135.73/18.92 | (75) $i(all_94_0) % 135.73/18.92 | % 135.73/18.92 | DELTA: instantiating (67) with fresh symbol all_96_0 gives: % 135.73/18.92 | (76) $i(all_96_0) & activity(all_96_0) & occurrence_of(all_58_0, all_96_0) % 135.73/18.92 | % 135.73/18.92 | ALPHA: (76) implies: % 135.73/18.92 | (77) occurrence_of(all_58_0, all_96_0) % 135.73/18.92 | (78) $i(all_96_0) % 135.73/18.92 | % 135.73/18.92 | DELTA: instantiating (62) with fresh symbol all_98_0 gives: % 135.73/18.92 | (79) $i(all_98_0) & subactivity_occurrence(all_74_0, all_58_0) & % 135.73/18.92 | root(all_74_0, all_98_0) & occurrence_of(all_58_0, all_98_0) % 135.73/18.92 | % 135.73/18.92 | ALPHA: (79) implies: % 135.73/18.92 | (80) occurrence_of(all_58_0, all_98_0) % 135.73/18.92 | (81) root(all_74_0, all_98_0) % 135.73/18.92 | (82) $i(all_98_0) % 135.73/18.92 | % 135.73/18.92 | DELTA: instantiating (66) with fresh symbol all_100_0 gives: % 135.73/18.92 | (83) $i(all_100_0) & subactivity(all_70_0, all_100_0) & atomic(all_100_0) & % 135.73/18.92 | occurrence_of(all_46_1, all_100_0) % 135.73/18.92 | % 135.73/18.92 | ALPHA: (83) implies: % 135.73/18.92 | (84) occurrence_of(all_46_1, all_100_0) % 135.73/18.92 | (85) $i(all_100_0) % 135.73/18.92 | % 135.73/18.92 | PRED_UNIFY: (58), (70) imply: % 135.73/18.92 | (86) ~ (all_74_1 = tptp3) % 135.73/18.92 | % 135.73/18.92 | PRED_UNIFY: (58), (69) imply: % 135.73/18.92 | (87) ~ (all_74_1 = tptp2) % 135.73/18.92 | % 135.73/18.92 | GROUND_INST: instantiating (20) with all_74_0, tptp0, all_46_1, simplifying % 135.73/18.92 | with (11), (33), (60), (68) gives: % 135.73/18.92 | (88) leaf(all_74_0, tptp0) | ? [v0: $i] : ($i(v0) & min_precedes(all_74_0, % 135.73/18.92 | v0, tptp0)) % 135.73/18.92 | % 135.73/18.93 | GROUND_INST: instantiating (sos_26) with tptp0, all_46_1, all_74_0, % 135.73/18.93 | simplifying with (11), (33), (60), (68) gives: % 135.73/18.93 | (89) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & subactivity(v1, tptp0) % 135.73/18.93 | & subactivity(v0, tptp0) & atocc(all_74_0, v1) & atocc(all_46_1, % 135.73/18.93 | v0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_24) with tptp0, all_46_1, all_74_0, % 135.73/18.93 | simplifying with (11), (33), (60), (68) gives: % 135.73/18.93 | (90) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_74_0, v0) & % 135.73/18.93 | subactivity_occurrence(all_46_1, v0) & occurrence_of(v0, tptp0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_30) with all_96_0, all_58_0, simplifying with % 135.73/18.93 | (44), (77), (78) gives: % 135.73/18.93 | (91) atomic(all_96_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 135.73/18.93 | all_58_0) & root(v0, all_96_0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_22) with all_58_0, all_58_3, all_98_0, % 135.73/18.93 | simplifying with (38), (41), (44), (80), (82) gives: % 135.73/18.93 | (92) all_98_0 = all_58_3 % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_22) with all_58_0, all_96_0, all_98_0, % 135.73/18.93 | simplifying with (44), (77), (78), (80), (82) gives: % 135.73/18.93 | (93) all_98_0 = all_96_0 % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_30) with all_98_0, all_58_0, simplifying with % 135.73/18.93 | (44), (80), (82) gives: % 135.73/18.93 | (94) atomic(all_98_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 135.73/18.93 | all_58_0) & root(v0, all_98_0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (4) with all_58_3, all_58_2, all_58_1, all_46_1, % 135.73/18.93 | tptp0, simplifying with (11), (33), (40), (41), (42), (43) gives: % 135.73/18.93 | (95) ~ atomic(all_58_3) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_27) with all_98_0, all_74_0, simplifying with % 135.73/18.93 | (60), (81), (82) gives: % 135.73/18.93 | (96) ? [v0: $i] : ($i(v0) & subactivity(v0, all_98_0) & atocc(all_74_0, % 135.73/18.93 | v0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_12) with all_74_0, all_98_0, simplifying with % 135.73/18.93 | (60), (81), (82) gives: % 135.73/18.93 | (97) legal(all_74_0) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_17) with all_58_2, simplifying with (42), (64) % 135.73/18.93 | gives: % 135.73/18.93 | (98) arboreal(all_58_2) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (18) with all_58_2, all_94_0, simplifying with % 135.73/18.93 | (42), (74), (75) gives: % 135.73/18.93 | (99) ? [v0: $i] : ($i(v0) & subactivity(all_94_0, v0) & atomic(v0) & % 135.73/18.93 | occurrence_of(all_58_2, v0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_18) with all_74_0, simplifying with (60), (61) % 135.73/18.93 | gives: % 135.73/18.93 | (100) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_74_0, v0)) % 135.73/18.93 | % 135.73/18.93 | GROUND_INST: instantiating (sos_31) with all_74_1, simplifying with (59), (71) % 135.73/18.93 | gives: % 135.73/18.93 | (101) subactivity(all_74_1, all_74_1) % 135.73/18.93 | % 135.73/18.93 | COMBINE_EQS: (92), (93) imply: % 135.73/18.93 | (102) all_96_0 = all_58_3 % 135.73/18.93 | % 135.73/18.93 | DELTA: instantiating (100) with fresh symbol all_112_0 gives: % 135.73/18.93 | (103) $i(all_112_0) & activity(all_112_0) & occurrence_of(all_74_0, % 135.73/18.93 | all_112_0) % 135.73/18.93 | % 135.73/18.93 | ALPHA: (103) implies: % 135.73/18.93 | (104) occurrence_of(all_74_0, all_112_0) % 135.73/18.93 | (105) $i(all_112_0) % 135.73/18.93 | % 135.73/18.93 | DELTA: instantiating (96) with fresh symbol all_116_0 gives: % 135.73/18.93 | (106) $i(all_116_0) & subactivity(all_116_0, all_98_0) & atocc(all_74_0, % 135.73/18.93 | all_116_0) % 135.73/18.93 | % 135.73/18.93 | ALPHA: (106) implies: % 135.73/18.93 | (107) atocc(all_74_0, all_116_0) % 135.73/18.93 | (108) $i(all_116_0) % 135.73/18.93 | % 135.73/18.93 | DELTA: instantiating (99) with fresh symbol all_118_0 gives: % 135.73/18.93 | (109) $i(all_118_0) & subactivity(all_94_0, all_118_0) & atomic(all_118_0) % 135.73/18.93 | & occurrence_of(all_58_2, all_118_0) % 135.73/18.93 | % 135.73/18.93 | ALPHA: (109) implies: % 135.73/18.93 | (110) occurrence_of(all_58_2, all_118_0) % 135.73/18.93 | (111) $i(all_118_0) % 135.73/18.93 | % 135.73/18.93 | DELTA: instantiating (90) with fresh symbol all_120_0 gives: % 135.73/18.94 | (112) $i(all_120_0) & subactivity_occurrence(all_74_0, all_120_0) & % 135.73/18.94 | subactivity_occurrence(all_46_1, all_120_0) & % 135.73/18.94 | occurrence_of(all_120_0, tptp0) % 135.73/18.94 | % 135.73/18.94 | ALPHA: (112) implies: % 135.73/18.94 | (113) occurrence_of(all_120_0, tptp0) % 135.73/18.94 | (114) subactivity_occurrence(all_46_1, all_120_0) % 135.73/18.94 | (115) subactivity_occurrence(all_74_0, all_120_0) % 135.73/18.94 | (116) $i(all_120_0) % 135.73/18.94 | % 135.73/18.94 | DELTA: instantiating (89) with fresh symbols all_122_0, all_122_1 gives: % 135.73/18.94 | (117) $i(all_122_0) & $i(all_122_1) & subactivity(all_122_0, tptp0) & % 135.73/18.94 | subactivity(all_122_1, tptp0) & atocc(all_74_0, all_122_0) & % 135.73/18.94 | atocc(all_46_1, all_122_1) % 135.73/18.94 | % 135.73/18.94 | ALPHA: (117) implies: % 135.73/18.94 | (118) atocc(all_74_0, all_122_0) % 135.73/18.94 | (119) $i(all_122_0) % 135.73/18.94 | % 135.73/18.94 | BETA: splitting (46) gives: % 135.73/18.94 | % 135.73/18.94 | Case 1: % 135.73/18.94 | | % 135.73/18.94 | | (120) atomic(all_58_3) % 135.73/18.94 | | % 135.73/18.94 | | PRED_UNIFY: (95), (120) imply: % 135.73/18.94 | | (121) $false % 135.73/18.94 | | % 135.73/18.94 | | CLOSE: (121) is inconsistent. % 135.73/18.94 | | % 135.73/18.94 | Case 2: % 135.73/18.94 | | % 135.73/18.94 | | (122) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_58_0) & % 135.73/18.94 | | root(v0, all_58_3)) % 135.73/18.94 | | % 135.73/18.94 | | DELTA: instantiating (122) with fresh symbol all_136_0 gives: % 135.73/18.94 | | (123) $i(all_136_0) & subactivity_occurrence(all_136_0, all_58_0) & % 135.73/18.94 | | root(all_136_0, all_58_3) % 135.73/18.94 | | % 135.73/18.94 | | ALPHA: (123) implies: % 135.73/18.94 | | (124) root(all_136_0, all_58_3) % 135.73/18.94 | | (125) subactivity_occurrence(all_136_0, all_58_0) % 135.73/18.94 | | (126) $i(all_136_0) % 135.73/18.94 | | % 135.73/18.94 | | BETA: splitting (94) gives: % 135.73/18.94 | | % 135.73/18.94 | | Case 1: % 135.73/18.94 | | | % 135.73/18.94 | | | (127) atomic(all_98_0) % 135.73/18.94 | | | % 135.73/18.94 | | | REDUCE: (92), (127) imply: % 135.73/18.94 | | | (128) atomic(all_58_3) % 135.73/18.94 | | | % 135.73/18.94 | | | PRED_UNIFY: (95), (128) imply: % 135.73/18.94 | | | (129) $false % 135.73/18.94 | | | % 135.73/18.94 | | | CLOSE: (129) is inconsistent. % 135.73/18.94 | | | % 135.73/18.94 | | Case 2: % 135.73/18.94 | | | % 135.73/18.94 | | | (130) ~ atomic(all_98_0) % 135.73/18.94 | | | (131) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_58_0) & % 135.73/18.94 | | | root(v0, all_98_0)) % 135.73/18.94 | | | % 135.73/18.94 | | | DELTA: instantiating (131) with fresh symbol all_145_0 gives: % 135.73/18.94 | | | (132) $i(all_145_0) & subactivity_occurrence(all_145_0, all_58_0) & % 135.73/18.94 | | | root(all_145_0, all_98_0) % 135.73/18.94 | | | % 135.73/18.94 | | | ALPHA: (132) implies: % 135.73/18.94 | | | (133) root(all_145_0, all_98_0) % 135.73/18.94 | | | (134) subactivity_occurrence(all_145_0, all_58_0) % 135.73/18.94 | | | (135) $i(all_145_0) % 135.73/18.94 | | | % 135.73/18.94 | | | REDUCE: (92), (133) imply: % 135.73/18.94 | | | (136) root(all_145_0, all_58_3) % 135.73/18.94 | | | % 135.73/18.94 | | | BETA: splitting (91) gives: % 135.73/18.94 | | | % 135.73/18.94 | | | Case 1: % 135.73/18.94 | | | | % 135.73/18.94 | | | | (137) atomic(all_96_0) % 135.73/18.94 | | | | % 135.73/18.94 | | | | REDUCE: (102), (137) imply: % 135.73/18.94 | | | | (138) atomic(all_58_3) % 135.73/18.94 | | | | % 135.73/18.94 | | | | PRED_UNIFY: (95), (138) imply: % 135.73/18.94 | | | | (139) $false % 135.73/18.94 | | | | % 135.73/18.94 | | | | CLOSE: (139) is inconsistent. % 135.73/18.94 | | | | % 135.73/18.94 | | | Case 2: % 135.73/18.94 | | | | % 135.73/18.94 | | | | (140) ~ atomic(all_96_0) % 135.73/18.94 | | | | (141) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_58_0) & % 135.73/18.94 | | | | root(v0, all_96_0)) % 135.73/18.94 | | | | % 135.73/18.94 | | | | DELTA: instantiating (141) with fresh symbol all_159_0 gives: % 135.73/18.94 | | | | (142) $i(all_159_0) & subactivity_occurrence(all_159_0, all_58_0) & % 135.73/18.94 | | | | root(all_159_0, all_96_0) % 135.73/18.94 | | | | % 135.73/18.94 | | | | ALPHA: (142) implies: % 135.73/18.94 | | | | (143) root(all_159_0, all_96_0) % 135.73/18.94 | | | | (144) subactivity_occurrence(all_159_0, all_58_0) % 135.73/18.94 | | | | (145) $i(all_159_0) % 135.73/18.94 | | | | % 135.73/18.94 | | | | REDUCE: (102), (143) imply: % 135.73/18.94 | | | | (146) root(all_159_0, all_58_3) % 135.73/18.94 | | | | % 135.73/18.94 | | | | GROUND_INST: instantiating (sos_47) with all_74_1, all_58_2, all_58_1, % 135.73/18.94 | | | | all_46_1, tptp0, all_58_2, simplifying with (11), (33), % 135.73/18.94 | | | | (42), (43), (58), (59) gives: % 135.73/18.95 | | | | (147) ~ occurrence_of(all_58_2, all_74_1) | min_precedes(all_46_1, % 135.73/18.95 | | | | all_58_2, tptp0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_22) with all_46_1, all_100_0, all_118_0, % 135.73/18.95 | | | | simplifying with (33), (84), (85), (111) gives: % 135.73/18.95 | | | | (148) all_118_0 = all_100_0 | ~ occurrence_of(all_46_1, all_118_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_74_1, all_112_0, % 135.73/18.95 | | | | simplifying with (56), (59), (60), (104), (105) gives: % 135.73/18.95 | | | | (149) all_112_0 = all_74_1 % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (14) with all_120_0, simplifying with (113), % 135.73/18.95 | | | | (116) gives: % 135.73/18.95 | | | | (150) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & next_subocc(v0, % 135.73/18.95 | | | | v1, tptp0) & leaf_occ(v1, all_120_0) & root_occ(v0, % 135.73/18.95 | | | | all_120_0) & occurrence_of(v0, tptp4) & (occurrence_of(v1, % 135.73/18.95 | | | | tptp2) | occurrence_of(v1, tptp3))) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_30) with tptp0, all_120_0, simplifying % 135.73/18.95 | | | | with (10), (11), (113), (116) gives: % 135.73/18.95 | | | | (151) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_120_0) & % 135.73/18.95 | | | | root(v0, tptp0)) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_27) with all_58_3, all_136_0, % 135.73/18.95 | | | | simplifying with (41), (124), (126) gives: % 135.73/18.95 | | | | (152) ? [v0: $i] : ($i(v0) & subactivity(v0, all_58_3) & % 135.73/18.95 | | | | atocc(all_136_0, v0)) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_12) with all_136_0, all_58_3, % 135.73/18.95 | | | | simplifying with (41), (124), (126) gives: % 135.73/18.95 | | | | (153) legal(all_136_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_27) with all_58_3, all_145_0, % 135.73/18.95 | | | | simplifying with (41), (135), (136) gives: % 135.73/18.95 | | | | (154) ? [v0: $i] : ($i(v0) & subactivity(v0, all_58_3) & % 135.73/18.95 | | | | atocc(all_145_0, v0)) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_27) with all_58_3, all_159_0, % 135.73/18.95 | | | | simplifying with (41), (145), (146) gives: % 135.73/18.95 | | | | (155) ? [v0: $i] : ($i(v0) & subactivity(v0, all_58_3) & % 135.73/18.95 | | | | atocc(all_159_0, v0)) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (26) with all_46_1, all_120_0, tptp0, % 135.73/18.95 | | | | simplifying with (11), (33), (36), (113), (114), (116) % 135.73/18.95 | | | | gives: % 135.73/18.95 | | | | (156) root_occ(all_46_1, all_120_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (sos_28) with tptp0, all_120_0, all_58_2, % 135.73/18.95 | | | | all_46_1, simplifying with (11), (33), (42), (65), (98), % 135.73/18.95 | | | | (113), (114), (116) gives: % 135.73/18.95 | | | | (157) all_58_2 = all_46_1 | ~ subactivity_occurrence(all_58_2, % 135.73/18.95 | | | | all_120_0) | min_precedes(all_58_2, all_46_1, tptp0) | % 135.73/18.95 | | | | min_precedes(all_46_1, all_58_2, tptp0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (17) with all_74_0, all_120_0, simplifying % 135.73/18.95 | | | | with (60), (115), (116) gives: % 135.73/18.95 | | | | (158) activity_occurrence(all_120_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (26) with all_136_0, all_58_0, all_58_3, % 135.73/18.95 | | | | simplifying with (38), (41), (44), (124), (125), (126) % 135.73/18.95 | | | | gives: % 135.73/18.95 | | | | (159) root_occ(all_136_0, all_58_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (16) with all_136_0, all_58_0, simplifying % 135.73/18.95 | | | | with (44), (125), (126) gives: % 135.73/18.95 | | | | (160) activity_occurrence(all_136_0) % 135.73/18.95 | | | | % 135.73/18.95 | | | | GROUND_INST: instantiating (26) with all_145_0, all_58_0, all_58_3, % 135.73/18.95 | | | | simplifying with (38), (41), (44), (134), (135), (136) % 135.73/18.95 | | | | gives: % 135.73/18.95 | | | | (161) root_occ(all_145_0, all_58_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (16) with all_145_0, all_58_0, simplifying % 135.73/18.96 | | | | with (44), (134), (135) gives: % 135.73/18.96 | | | | (162) activity_occurrence(all_145_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (26) with all_159_0, all_58_0, all_58_3, % 135.73/18.96 | | | | simplifying with (38), (41), (44), (144), (145), (146) % 135.73/18.96 | | | | gives: % 135.73/18.96 | | | | (163) root_occ(all_159_0, all_58_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (16) with all_159_0, all_58_0, simplifying % 135.73/18.96 | | | | with (44), (144), (145) gives: % 135.73/18.96 | | | | (164) activity_occurrence(all_159_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (sos_16) with all_74_0, all_116_0, % 135.73/18.96 | | | | simplifying with (60), (97), (107), (108) gives: % 135.73/18.96 | | | | (165) root(all_74_0, all_116_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (18) with all_74_0, all_116_0, simplifying % 135.73/18.96 | | | | with (60), (107), (108) gives: % 135.73/18.96 | | | | (166) ? [v0: $i] : ($i(v0) & subactivity(all_116_0, v0) & atomic(v0) % 135.73/18.96 | | | | & occurrence_of(all_74_0, v0)) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (sos_16) with all_74_0, all_122_0, % 135.73/18.96 | | | | simplifying with (60), (97), (118), (119) gives: % 135.73/18.96 | | | | (167) root(all_74_0, all_122_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (18) with all_74_0, all_122_0, simplifying % 135.73/18.96 | | | | with (60), (118), (119) gives: % 135.73/18.96 | | | | (168) ? [v0: $i] : ($i(v0) & subactivity(all_122_0, v0) & atomic(v0) % 135.73/18.96 | | | | & occurrence_of(all_74_0, v0)) % 135.73/18.96 | | | | % 135.73/18.96 | | | | GROUND_INST: instantiating (19) with all_74_0, all_74_1, all_74_1, % 135.73/18.96 | | | | simplifying with (56), (59), (60), (72), (101) gives: % 135.73/18.96 | | | | (169) atocc(all_74_0, all_74_1) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (155) with fresh symbol all_183_0 gives: % 135.73/18.96 | | | | (170) $i(all_183_0) & subactivity(all_183_0, all_58_3) & % 135.73/18.96 | | | | atocc(all_159_0, all_183_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (170) implies: % 135.73/18.96 | | | | (171) atocc(all_159_0, all_183_0) % 135.73/18.96 | | | | (172) $i(all_183_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (154) with fresh symbol all_189_0 gives: % 135.73/18.96 | | | | (173) $i(all_189_0) & subactivity(all_189_0, all_58_3) & % 135.73/18.96 | | | | atocc(all_145_0, all_189_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (173) implies: % 135.73/18.96 | | | | (174) atocc(all_145_0, all_189_0) % 135.73/18.96 | | | | (175) $i(all_189_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (151) with fresh symbol all_193_0 gives: % 135.73/18.96 | | | | (176) $i(all_193_0) & subactivity_occurrence(all_193_0, all_120_0) & % 135.73/18.96 | | | | root(all_193_0, tptp0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (176) implies: % 135.73/18.96 | | | | (177) root(all_193_0, tptp0) % 135.73/18.96 | | | | (178) subactivity_occurrence(all_193_0, all_120_0) % 135.73/18.96 | | | | (179) $i(all_193_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (152) with fresh symbol all_195_0 gives: % 135.73/18.96 | | | | (180) $i(all_195_0) & subactivity(all_195_0, all_58_3) & % 135.73/18.96 | | | | atocc(all_136_0, all_195_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (180) implies: % 135.73/18.96 | | | | (181) atocc(all_136_0, all_195_0) % 135.73/18.96 | | | | (182) $i(all_195_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (166) with fresh symbol all_199_0 gives: % 135.73/18.96 | | | | (183) $i(all_199_0) & subactivity(all_116_0, all_199_0) & % 135.73/18.96 | | | | atomic(all_199_0) & occurrence_of(all_74_0, all_199_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (183) implies: % 135.73/18.96 | | | | (184) occurrence_of(all_74_0, all_199_0) % 135.73/18.96 | | | | (185) $i(all_199_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (168) with fresh symbol all_205_0 gives: % 135.73/18.96 | | | | (186) $i(all_205_0) & subactivity(all_122_0, all_205_0) & % 135.73/18.96 | | | | atomic(all_205_0) & occurrence_of(all_74_0, all_205_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (186) implies: % 135.73/18.96 | | | | (187) occurrence_of(all_74_0, all_205_0) % 135.73/18.96 | | | | (188) $i(all_205_0) % 135.73/18.96 | | | | % 135.73/18.96 | | | | DELTA: instantiating (150) with fresh symbols all_207_0, all_207_1 % 135.73/18.96 | | | | gives: % 135.73/18.96 | | | | (189) $i(all_207_0) & $i(all_207_1) & next_subocc(all_207_1, % 135.73/18.96 | | | | all_207_0, tptp0) & leaf_occ(all_207_0, all_120_0) & % 135.73/18.96 | | | | root_occ(all_207_1, all_120_0) & occurrence_of(all_207_1, % 135.73/18.96 | | | | tptp4) & (occurrence_of(all_207_0, tptp2) | % 135.73/18.96 | | | | occurrence_of(all_207_0, tptp3)) % 135.73/18.96 | | | | % 135.73/18.96 | | | | ALPHA: (189) implies: % 135.73/18.96 | | | | (190) root_occ(all_207_1, all_120_0) % 135.73/18.96 | | | | (191) leaf_occ(all_207_0, all_120_0) % 135.73/18.96 | | | | (192) next_subocc(all_207_1, all_207_0, tptp0) % 135.73/18.96 | | | | (193) $i(all_207_1) % 135.73/18.96 | | | | (194) $i(all_207_0) % 135.73/18.96 | | | | (195) occurrence_of(all_207_0, tptp2) | occurrence_of(all_207_0, % 135.73/18.96 | | | | tptp3) % 135.73/18.96 | | | | % 135.73/18.96 | | | | BETA: splitting (45) gives: % 135.73/18.96 | | | | % 135.73/18.96 | | | | Case 1: % 135.73/18.96 | | | | | % 135.73/18.96 | | | | | % 135.73/18.96 | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_74_1, % 135.73/18.96 | | | | | all_205_0, simplifying with (56), (59), (60), (187), % 135.73/18.96 | | | | | (188) gives: % 135.73/18.96 | | | | | (196) all_205_0 = all_74_1 % 135.73/18.96 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_199_0, % 135.73/18.97 | | | | | all_205_0, simplifying with (60), (184), (185), (187), % 135.73/18.97 | | | | | (188) gives: % 135.73/18.97 | | | | | (197) all_205_0 = all_199_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (25) with all_46_1, all_120_0, simplifying % 135.73/18.97 | | | | | with (33), (116), (156) gives: % 135.73/18.97 | | | | | (198) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_46_1, % 135.73/18.97 | | | | | all_120_0) & root(all_46_1, v0) & % 135.73/18.97 | | | | | occurrence_of(all_120_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_02) with all_136_0, all_145_0, % 135.73/18.97 | | | | | all_58_0, all_58_3, simplifying with (38), (41), (44), % 135.73/18.97 | | | | | (126), (135), (159), (161) gives: % 135.73/18.97 | | | | | (199) all_145_0 = all_136_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_02) with all_74_0, all_159_0, % 135.73/18.97 | | | | | all_58_0, all_58_3, simplifying with (38), (41), (44), % 135.73/18.97 | | | | | (57), (60), (145), (163) gives: % 135.73/18.97 | | | | | (200) all_159_0 = all_74_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_02) with all_145_0, all_159_0, % 135.73/18.97 | | | | | all_58_0, all_58_3, simplifying with (38), (41), (44), % 135.73/18.97 | | | | | (135), (145), (161), (163) gives: % 135.73/18.97 | | | | | (201) all_159_0 = all_145_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_02) with all_46_1, all_207_1, % 135.73/18.97 | | | | | all_120_0, tptp0, simplifying with (11), (33), (113), % 135.73/18.97 | | | | | (116), (156), (190), (193) gives: % 135.73/18.97 | | | | | (202) all_207_1 = all_46_1 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (25) with all_207_1, all_120_0, simplifying % 135.73/18.97 | | | | | with (116), (190), (193) gives: % 135.73/18.97 | | | | | (203) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_207_1, % 135.73/18.97 | | | | | all_120_0) & root(all_207_1, v0) & % 135.73/18.97 | | | | | occurrence_of(all_120_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (23) with all_207_0, all_120_0, simplifying % 135.73/18.97 | | | | | with (116), (191), (194) gives: % 135.73/18.97 | | | | | (204) ? [v0: $i] : ($i(v0) & leaf(all_207_0, v0) & % 135.73/18.97 | | | | | subactivity_occurrence(all_207_0, all_120_0) & % 135.73/18.97 | | | | | occurrence_of(all_120_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (27) with all_207_1, all_207_0, tptp0, % 135.73/18.97 | | | | | simplifying with (11), (192), (193), (194) gives: % 135.73/18.97 | | | | | (205) arboreal(all_207_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_27) with all_116_0, all_74_0, % 135.73/18.97 | | | | | simplifying with (60), (108), (165) gives: % 135.73/18.97 | | | | | (206) ? [v0: $i] : ($i(v0) & subactivity(v0, all_116_0) & % 135.73/18.97 | | | | | atocc(all_74_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_27) with all_122_0, all_74_0, % 135.73/18.97 | | | | | simplifying with (60), (119), (167) gives: % 135.73/18.97 | | | | | (207) ? [v0: $i] : ($i(v0) & subactivity(v0, all_122_0) & % 135.73/18.97 | | | | | atocc(all_74_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_17) with all_136_0, simplifying with % 135.73/18.97 | | | | | (126), (153) gives: % 135.73/18.97 | | | | | (208) arboreal(all_136_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (26) with all_193_0, all_120_0, tptp0, % 135.73/18.97 | | | | | simplifying with (11), (113), (116), (177), (178), (179) % 135.73/18.97 | | | | | gives: % 135.73/18.97 | | | | | (209) root_occ(all_193_0, all_120_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (18) with all_74_0, all_74_1, simplifying % 135.73/18.97 | | | | | with (59), (60), (169) gives: % 135.73/18.97 | | | | | (210) ? [v0: $i] : ($i(v0) & subactivity(all_74_1, v0) & % 135.73/18.97 | | | | | atomic(v0) & occurrence_of(all_74_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (18) with all_136_0, all_195_0, simplifying % 135.73/18.97 | | | | | with (126), (181), (182) gives: % 135.73/18.97 | | | | | (211) ? [v0: $i] : ($i(v0) & subactivity(all_195_0, v0) & % 135.73/18.97 | | | | | atomic(v0) & occurrence_of(all_136_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (18) with all_145_0, all_189_0, simplifying % 135.73/18.97 | | | | | with (135), (174), (175) gives: % 135.73/18.97 | | | | | (212) ? [v0: $i] : ($i(v0) & subactivity(all_189_0, v0) & % 135.73/18.97 | | | | | atomic(v0) & occurrence_of(all_145_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (18) with all_159_0, all_183_0, simplifying % 135.73/18.97 | | | | | with (145), (171), (172) gives: % 135.73/18.97 | | | | | (213) ? [v0: $i] : ($i(v0) & subactivity(all_183_0, v0) & % 135.73/18.97 | | | | | atomic(v0) & occurrence_of(all_159_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_18) with all_120_0, simplifying with % 135.73/18.97 | | | | | (116), (158) gives: % 135.73/18.97 | | | | | (214) ? [v0: $i] : ($i(v0) & activity(v0) & % 135.73/18.97 | | | | | occurrence_of(all_120_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_18) with all_136_0, simplifying with % 135.73/18.97 | | | | | (126), (160) gives: % 135.73/18.97 | | | | | (215) ? [v0: $i] : ($i(v0) & activity(v0) & % 135.73/18.97 | | | | | occurrence_of(all_136_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_18) with all_145_0, simplifying with % 135.73/18.97 | | | | | (135), (162) gives: % 135.73/18.97 | | | | | (216) ? [v0: $i] : ($i(v0) & activity(v0) & % 135.73/18.97 | | | | | occurrence_of(all_145_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | GROUND_INST: instantiating (sos_18) with all_159_0, simplifying with % 135.73/18.97 | | | | | (145), (164) gives: % 135.73/18.97 | | | | | (217) ? [v0: $i] : ($i(v0) & activity(v0) & % 135.73/18.97 | | | | | occurrence_of(all_159_0, v0)) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | COMBINE_EQS: (196), (197) imply: % 135.73/18.97 | | | | | (218) all_199_0 = all_74_1 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | SIMP: (218) implies: % 135.73/18.97 | | | | | (219) all_199_0 = all_74_1 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | COMBINE_EQS: (200), (201) imply: % 135.73/18.97 | | | | | (220) all_145_0 = all_74_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | SIMP: (220) implies: % 135.73/18.97 | | | | | (221) all_145_0 = all_74_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | COMBINE_EQS: (199), (221) imply: % 135.73/18.97 | | | | | (222) all_136_0 = all_74_0 % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | DELTA: instantiating (214) with fresh symbol all_291_0 gives: % 135.73/18.97 | | | | | (223) $i(all_291_0) & activity(all_291_0) & % 135.73/18.97 | | | | | occurrence_of(all_120_0, all_291_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | ALPHA: (223) implies: % 135.73/18.97 | | | | | (224) occurrence_of(all_120_0, all_291_0) % 135.73/18.97 | | | | | (225) $i(all_291_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | DELTA: instantiating (206) with fresh symbol all_295_0 gives: % 135.73/18.97 | | | | | (226) $i(all_295_0) & subactivity(all_295_0, all_116_0) & % 135.73/18.97 | | | | | atocc(all_74_0, all_295_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | ALPHA: (226) implies: % 135.73/18.97 | | | | | (227) atocc(all_74_0, all_295_0) % 135.73/18.97 | | | | | (228) $i(all_295_0) % 135.73/18.97 | | | | | % 135.73/18.97 | | | | | DELTA: instantiating (207) with fresh symbol all_301_0 gives: % 135.73/18.98 | | | | | (229) $i(all_301_0) & subactivity(all_301_0, all_122_0) & % 135.73/18.98 | | | | | atocc(all_74_0, all_301_0) % 135.73/18.98 | | | | | % 135.73/18.98 | | | | | ALPHA: (229) implies: % 135.73/18.98 | | | | | (230) atocc(all_74_0, all_301_0) % 135.73/18.98 | | | | | (231) $i(all_301_0) % 135.73/18.98 | | | | | % 135.73/18.98 | | | | | DELTA: instantiating (217) with fresh symbol all_303_0 gives: % 136.03/18.98 | | | | | (232) $i(all_303_0) & activity(all_303_0) & % 136.03/18.98 | | | | | occurrence_of(all_159_0, all_303_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (232) implies: % 136.03/18.98 | | | | | (233) occurrence_of(all_159_0, all_303_0) % 136.03/18.98 | | | | | (234) $i(all_303_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (216) with fresh symbol all_305_0 gives: % 136.03/18.98 | | | | | (235) $i(all_305_0) & activity(all_305_0) & % 136.03/18.98 | | | | | occurrence_of(all_145_0, all_305_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (235) implies: % 136.03/18.98 | | | | | (236) occurrence_of(all_145_0, all_305_0) % 136.03/18.98 | | | | | (237) $i(all_305_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (215) with fresh symbol all_307_0 gives: % 136.03/18.98 | | | | | (238) $i(all_307_0) & activity(all_307_0) & % 136.03/18.98 | | | | | occurrence_of(all_136_0, all_307_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (238) implies: % 136.03/18.98 | | | | | (239) occurrence_of(all_136_0, all_307_0) % 136.03/18.98 | | | | | (240) $i(all_307_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (210) with fresh symbol all_315_0 gives: % 136.03/18.98 | | | | | (241) $i(all_315_0) & subactivity(all_74_1, all_315_0) & % 136.03/18.98 | | | | | atomic(all_315_0) & occurrence_of(all_74_0, all_315_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (241) implies: % 136.03/18.98 | | | | | (242) occurrence_of(all_74_0, all_315_0) % 136.03/18.98 | | | | | (243) $i(all_315_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (211) with fresh symbol all_319_0 gives: % 136.03/18.98 | | | | | (244) $i(all_319_0) & subactivity(all_195_0, all_319_0) & % 136.03/18.98 | | | | | atomic(all_319_0) & occurrence_of(all_136_0, all_319_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (244) implies: % 136.03/18.98 | | | | | (245) occurrence_of(all_136_0, all_319_0) % 136.03/18.98 | | | | | (246) $i(all_319_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (212) with fresh symbol all_323_0 gives: % 136.03/18.98 | | | | | (247) $i(all_323_0) & subactivity(all_189_0, all_323_0) & % 136.03/18.98 | | | | | atomic(all_323_0) & occurrence_of(all_145_0, all_323_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (247) implies: % 136.03/18.98 | | | | | (248) occurrence_of(all_145_0, all_323_0) % 136.03/18.98 | | | | | (249) $i(all_323_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (213) with fresh symbol all_325_0 gives: % 136.03/18.98 | | | | | (250) $i(all_325_0) & subactivity(all_183_0, all_325_0) & % 136.03/18.98 | | | | | atomic(all_325_0) & occurrence_of(all_159_0, all_325_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (250) implies: % 136.03/18.98 | | | | | (251) occurrence_of(all_159_0, all_325_0) % 136.03/18.98 | | | | | (252) $i(all_325_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (204) with fresh symbol all_329_0 gives: % 136.03/18.98 | | | | | (253) $i(all_329_0) & leaf(all_207_0, all_329_0) & % 136.03/18.98 | | | | | subactivity_occurrence(all_207_0, all_120_0) & % 136.03/18.98 | | | | | occurrence_of(all_120_0, all_329_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (253) implies: % 136.03/18.98 | | | | | (254) occurrence_of(all_120_0, all_329_0) % 136.03/18.98 | | | | | (255) subactivity_occurrence(all_207_0, all_120_0) % 136.03/18.98 | | | | | (256) leaf(all_207_0, all_329_0) % 136.03/18.98 | | | | | (257) $i(all_329_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (203) with fresh symbol all_335_0 gives: % 136.03/18.98 | | | | | (258) $i(all_335_0) & subactivity_occurrence(all_207_1, all_120_0) % 136.03/18.98 | | | | | & root(all_207_1, all_335_0) & occurrence_of(all_120_0, % 136.03/18.98 | | | | | all_335_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (258) implies: % 136.03/18.98 | | | | | (259) occurrence_of(all_120_0, all_335_0) % 136.03/18.98 | | | | | (260) $i(all_335_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | DELTA: instantiating (198) with fresh symbol all_343_0 gives: % 136.03/18.98 | | | | | (261) $i(all_343_0) & subactivity_occurrence(all_46_1, all_120_0) & % 136.03/18.98 | | | | | root(all_46_1, all_343_0) & occurrence_of(all_120_0, % 136.03/18.98 | | | | | all_343_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | ALPHA: (261) implies: % 136.03/18.98 | | | | | (262) occurrence_of(all_120_0, all_343_0) % 136.03/18.98 | | | | | (263) $i(all_343_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (171), (200) imply: % 136.03/18.98 | | | | | (264) atocc(all_74_0, all_183_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (208), (222) imply: % 136.03/18.98 | | | | | (265) arboreal(all_74_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (192), (202) imply: % 136.03/18.98 | | | | | (266) next_subocc(all_46_1, all_207_0, tptp0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (200), (251) imply: % 136.03/18.98 | | | | | (267) occurrence_of(all_74_0, all_325_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (200), (233) imply: % 136.03/18.98 | | | | | (268) occurrence_of(all_74_0, all_303_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (221), (248) imply: % 136.03/18.98 | | | | | (269) occurrence_of(all_74_0, all_323_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (221), (236) imply: % 136.03/18.98 | | | | | (270) occurrence_of(all_74_0, all_305_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (222), (245) imply: % 136.03/18.98 | | | | | (271) occurrence_of(all_74_0, all_319_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | REDUCE: (222), (239) imply: % 136.03/18.98 | | | | | (272) occurrence_of(all_74_0, all_307_0) % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | BETA: splitting (88) gives: % 136.03/18.98 | | | | | % 136.03/18.98 | | | | | Case 1: % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | (273) leaf(all_74_0, tptp0) % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_74_1, % 136.03/18.98 | | | | | | all_315_0, simplifying with (56), (59), (60), (242), % 136.03/18.98 | | | | | | (243) gives: % 136.03/18.98 | | | | | | (274) all_315_0 = all_74_1 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_307_0, % 136.03/18.98 | | | | | | all_315_0, simplifying with (60), (240), (242), (243), % 136.03/18.98 | | | | | | (272) gives: % 136.03/18.98 | | | | | | (275) all_315_0 = all_307_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_319_0, % 136.03/18.98 | | | | | | all_323_0, simplifying with (60), (246), (249), (269), % 136.03/18.98 | | | | | | (271) gives: % 136.03/18.98 | | | | | | (276) all_323_0 = all_319_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_303_0, % 136.03/18.98 | | | | | | all_323_0, simplifying with (60), (234), (249), (268), % 136.03/18.98 | | | | | | (269) gives: % 136.03/18.98 | | | | | | (277) all_323_0 = all_303_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_319_0, % 136.03/18.98 | | | | | | all_325_0, simplifying with (60), (246), (252), (267), % 136.03/18.98 | | | | | | (271) gives: % 136.03/18.98 | | | | | | (278) all_325_0 = all_319_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_307_0, % 136.03/18.98 | | | | | | all_325_0, simplifying with (60), (240), (252), (267), % 136.03/18.98 | | | | | | (272) gives: % 136.03/18.98 | | | | | | (279) all_325_0 = all_307_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_305_0, % 136.03/18.98 | | | | | | all_325_0, simplifying with (60), (237), (252), (267), % 136.03/18.98 | | | | | | (270) gives: % 136.03/18.98 | | | | | | (280) all_325_0 = all_305_0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, tptp0, % 136.03/18.98 | | | | | | all_329_0, simplifying with (11), (113), (116), (254), % 136.03/18.98 | | | | | | (257) gives: % 136.03/18.98 | | | | | | (281) all_329_0 = tptp0 % 136.03/18.98 | | | | | | % 136.03/18.98 | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_329_0, % 136.03/18.98 | | | | | | all_335_0, simplifying with (116), (254), (257), (259), % 136.03/18.98 | | | | | | (260) gives: % 136.03/18.98 | | | | | | (282) all_335_0 = all_329_0 % 136.03/18.98 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_335_0, % 136.03/18.99 | | | | | | all_343_0, simplifying with (116), (259), (260), (262), % 136.03/18.99 | | | | | | (263) gives: % 136.03/18.99 | | | | | | (283) all_343_0 = all_335_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_291_0, % 136.03/18.99 | | | | | | all_343_0, simplifying with (116), (224), (225), (262), % 136.03/18.99 | | | | | | (263) gives: % 136.03/18.99 | | | | | | (284) all_343_0 = all_291_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (24) with all_74_0, all_120_0, tptp0, % 136.03/18.99 | | | | | | simplifying with (11), (60), (113), (115), (116), (273) % 136.03/18.99 | | | | | | gives: % 136.03/18.99 | | | | | | (285) leaf_occ(all_74_0, all_120_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (18) with all_74_0, all_183_0, % 136.03/18.99 | | | | | | simplifying with (60), (172), (264) gives: % 136.03/18.99 | | | | | | (286) ? [v0: $i] : ($i(v0) & subactivity(all_183_0, v0) & % 136.03/18.99 | | | | | | atomic(v0) & occurrence_of(all_74_0, v0)) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (18) with all_74_0, all_295_0, % 136.03/18.99 | | | | | | simplifying with (60), (227), (228) gives: % 136.03/18.99 | | | | | | (287) ? [v0: $i] : ($i(v0) & subactivity(all_295_0, v0) & % 136.03/18.99 | | | | | | atomic(v0) & occurrence_of(all_74_0, v0)) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | GROUND_INST: instantiating (18) with all_74_0, all_301_0, % 136.03/18.99 | | | | | | simplifying with (60), (230), (231) gives: % 136.03/18.99 | | | | | | (288) ? [v0: $i] : ($i(v0) & subactivity(all_301_0, v0) & % 136.03/18.99 | | | | | | atomic(v0) & occurrence_of(all_74_0, v0)) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (283), (284) imply: % 136.03/18.99 | | | | | | (289) all_335_0 = all_291_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (289) implies: % 136.03/18.99 | | | | | | (290) all_335_0 = all_291_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (282), (290) imply: % 136.03/18.99 | | | | | | (291) all_329_0 = all_291_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (291) implies: % 136.03/18.99 | | | | | | (292) all_329_0 = all_291_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (281), (292) imply: % 136.03/18.99 | | | | | | (293) all_291_0 = tptp0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (278), (280) imply: % 136.03/18.99 | | | | | | (294) all_319_0 = all_305_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (294) implies: % 136.03/18.99 | | | | | | (295) all_319_0 = all_305_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (279), (280) imply: % 136.03/18.99 | | | | | | (296) all_307_0 = all_305_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (296) implies: % 136.03/18.99 | | | | | | (297) all_307_0 = all_305_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (276), (277) imply: % 136.03/18.99 | | | | | | (298) all_319_0 = all_303_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (298) implies: % 136.03/18.99 | | | | | | (299) all_319_0 = all_303_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (295), (299) imply: % 136.03/18.99 | | | | | | (300) all_305_0 = all_303_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (300) implies: % 136.03/18.99 | | | | | | (301) all_305_0 = all_303_0 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (274), (275) imply: % 136.03/18.99 | | | | | | (302) all_307_0 = all_74_1 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (302) implies: % 136.03/18.99 | | | | | | (303) all_307_0 = all_74_1 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (297), (303) imply: % 136.03/18.99 | | | | | | (304) all_305_0 = all_74_1 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | SIMP: (304) implies: % 136.03/18.99 | | | | | | (305) all_305_0 = all_74_1 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | COMBINE_EQS: (301), (305) imply: % 136.03/18.99 | | | | | | (306) all_303_0 = all_74_1 % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | DELTA: instantiating (288) with fresh symbol all_611_0 gives: % 136.03/18.99 | | | | | | (307) $i(all_611_0) & subactivity(all_301_0, all_611_0) & % 136.03/18.99 | | | | | | atomic(all_611_0) & occurrence_of(all_74_0, all_611_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | ALPHA: (307) implies: % 136.03/18.99 | | | | | | (308) occurrence_of(all_74_0, all_611_0) % 136.03/18.99 | | | | | | (309) $i(all_611_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | DELTA: instantiating (287) with fresh symbol all_613_0 gives: % 136.03/18.99 | | | | | | (310) $i(all_613_0) & subactivity(all_295_0, all_613_0) & % 136.03/18.99 | | | | | | atomic(all_613_0) & occurrence_of(all_74_0, all_613_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | ALPHA: (310) implies: % 136.03/18.99 | | | | | | (311) occurrence_of(all_74_0, all_613_0) % 136.03/18.99 | | | | | | (312) $i(all_613_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | DELTA: instantiating (286) with fresh symbol all_615_0 gives: % 136.03/18.99 | | | | | | (313) $i(all_615_0) & subactivity(all_183_0, all_615_0) & % 136.03/18.99 | | | | | | atomic(all_615_0) & occurrence_of(all_74_0, all_615_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | ALPHA: (313) implies: % 136.03/18.99 | | | | | | (314) occurrence_of(all_74_0, all_615_0) % 136.03/18.99 | | | | | | (315) $i(all_615_0) % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | BETA: splitting (195) gives: % 136.03/18.99 | | | | | | % 136.03/18.99 | | | | | | Case 1: % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | (316) occurrence_of(all_207_0, tptp2) % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_611_0, % 136.03/18.99 | | | | | | | all_613_0, simplifying with (60), (308), (309), % 136.03/18.99 | | | | | | | (311), (312) gives: % 136.03/18.99 | | | | | | | (317) all_613_0 = all_611_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_74_1, % 136.03/18.99 | | | | | | | all_615_0, simplifying with (56), (59), (60), (314), % 136.03/18.99 | | | | | | | (315) gives: % 136.03/18.99 | | | | | | | (318) all_615_0 = all_74_1 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_613_0, % 136.03/18.99 | | | | | | | all_615_0, simplifying with (60), (311), (312), % 136.03/18.99 | | | | | | | (314), (315) gives: % 136.03/18.99 | | | | | | | (319) all_615_0 = all_613_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_611_0, % 136.03/18.99 | | | | | | | tptp2, simplifying with (13), (60), (308), (309) % 136.03/18.99 | | | | | | | gives: % 136.03/18.99 | | | | | | | (320) all_611_0 = tptp2 | ~ occurrence_of(all_74_0, tptp2) % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_03) with all_207_0, all_74_0, % 136.03/18.99 | | | | | | | all_120_0, tptp0, simplifying with (10), (11), (60), % 136.03/18.99 | | | | | | | (113), (116), (191), (194), (285) gives: % 136.03/18.99 | | | | | | | (321) all_207_0 = all_74_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | COMBINE_EQS: (318), (319) imply: % 136.03/18.99 | | | | | | | (322) all_613_0 = all_74_1 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | SIMP: (322) implies: % 136.03/18.99 | | | | | | | (323) all_613_0 = all_74_1 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | COMBINE_EQS: (317), (323) imply: % 136.03/18.99 | | | | | | | (324) all_611_0 = all_74_1 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | REDUCE: (316), (321) imply: % 136.03/18.99 | | | | | | | (325) occurrence_of(all_74_0, tptp2) % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | BETA: splitting (320) gives: % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | Case 1: % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | (326) ~ occurrence_of(all_74_0, tptp2) % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | PRED_UNIFY: (325), (326) imply: % 136.03/18.99 | | | | | | | | (327) $false % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | CLOSE: (327) is inconsistent. % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | Case 2: % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | (328) all_611_0 = tptp2 % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | COMBINE_EQS: (324), (328) imply: % 136.03/18.99 | | | | | | | | (329) all_74_1 = tptp2 % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | REDUCE: (87), (329) imply: % 136.03/18.99 | | | | | | | | (330) $false % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | | CLOSE: (330) is inconsistent. % 136.03/18.99 | | | | | | | | % 136.03/18.99 | | | | | | | End of split % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | Case 2: % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | (331) occurrence_of(all_207_0, tptp3) % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_74_1, % 136.03/18.99 | | | | | | | all_613_0, simplifying with (56), (59), (60), (311), % 136.03/18.99 | | | | | | | (312) gives: % 136.03/18.99 | | | | | | | (332) all_613_0 = all_74_1 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_613_0, % 136.03/18.99 | | | | | | | all_615_0, simplifying with (60), (311), (312), % 136.03/18.99 | | | | | | | (314), (315) gives: % 136.03/18.99 | | | | | | | (333) all_615_0 = all_613_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_611_0, % 136.03/18.99 | | | | | | | all_615_0, simplifying with (60), (308), (309), % 136.03/18.99 | | | | | | | (314), (315) gives: % 136.03/18.99 | | | | | | | (334) all_615_0 = all_611_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_22) with all_74_0, all_611_0, % 136.03/18.99 | | | | | | | tptp3, simplifying with (12), (60), (308), (309) % 136.03/18.99 | | | | | | | gives: % 136.03/18.99 | | | | | | | (335) all_611_0 = tptp3 | ~ occurrence_of(all_74_0, tptp3) % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | GROUND_INST: instantiating (sos_03) with all_207_0, all_74_0, % 136.03/18.99 | | | | | | | all_120_0, tptp0, simplifying with (10), (11), (60), % 136.03/18.99 | | | | | | | (113), (116), (191), (194), (285) gives: % 136.03/18.99 | | | | | | | (336) all_207_0 = all_74_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | COMBINE_EQS: (333), (334) imply: % 136.03/18.99 | | | | | | | (337) all_613_0 = all_611_0 % 136.03/18.99 | | | | | | | % 136.03/18.99 | | | | | | | SIMP: (337) implies: % 136.03/18.99 | | | | | | | (338) all_613_0 = all_611_0 % 136.03/18.99 | | | | | | | % 136.03/19.00 | | | | | | | COMBINE_EQS: (332), (338) imply: % 136.03/19.00 | | | | | | | (339) all_611_0 = all_74_1 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | SIMP: (339) implies: % 136.03/19.00 | | | | | | | (340) all_611_0 = all_74_1 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | REDUCE: (331), (336) imply: % 136.03/19.00 | | | | | | | (341) occurrence_of(all_74_0, tptp3) % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | BETA: splitting (335) gives: % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | Case 1: % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | (342) ~ occurrence_of(all_74_0, tptp3) % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | PRED_UNIFY: (341), (342) imply: % 136.03/19.00 | | | | | | | | (343) $false % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | CLOSE: (343) is inconsistent. % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | Case 2: % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | (344) all_611_0 = tptp3 % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | COMBINE_EQS: (340), (344) imply: % 136.03/19.00 | | | | | | | | (345) all_74_1 = tptp3 % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | REDUCE: (86), (345) imply: % 136.03/19.00 | | | | | | | | (346) $false % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | CLOSE: (346) is inconsistent. % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | End of split % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | End of split % 136.03/19.00 | | | | | | % 136.03/19.00 | | | | | Case 2: % 136.03/19.00 | | | | | | % 136.03/19.00 | | | | | | (347) ~ leaf(all_74_0, tptp0) % 136.03/19.00 | | | | | | % 136.03/19.00 | | | | | | BETA: splitting (147) gives: % 136.03/19.00 | | | | | | % 136.03/19.00 | | | | | | Case 1: % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_30) with all_291_0, all_120_0, % 136.03/19.00 | | | | | | | simplifying with (116), (224), (225) gives: % 136.03/19.00 | | | | | | | (348) atomic(all_291_0) | ? [v0: $i] : ($i(v0) & % 136.03/19.00 | | | | | | | subactivity_occurrence(v0, all_120_0) & root(v0, % 136.03/19.00 | | | | | | | all_291_0)) % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, tptp0, % 136.03/19.00 | | | | | | | all_329_0, simplifying with (11), (113), (116), % 136.03/19.00 | | | | | | | (254), (257) gives: % 136.03/19.00 | | | | | | | (349) all_329_0 = tptp0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_329_0, % 136.03/19.00 | | | | | | | all_335_0, simplifying with (116), (254), (257), % 136.03/19.00 | | | | | | | (259), (260) gives: % 136.03/19.00 | | | | | | | (350) all_335_0 = all_329_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_335_0, % 136.03/19.00 | | | | | | | all_343_0, simplifying with (116), (259), (260), % 136.03/19.00 | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | (351) all_343_0 = all_335_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_291_0, % 136.03/19.00 | | | | | | | all_343_0, simplifying with (116), (224), (225), % 136.03/19.00 | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | (352) all_343_0 = all_291_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | GROUND_INST: instantiating (sos_02) with all_46_1, all_193_0, % 136.03/19.00 | | | | | | | all_120_0, all_291_0, simplifying with (33), (116), % 136.03/19.00 | | | | | | | (156), (179), (209), (224), (225) gives: % 136.03/19.00 | | | | | | | (353) all_193_0 = all_46_1 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | COMBINE_EQS: (351), (352) imply: % 136.03/19.00 | | | | | | | (354) all_335_0 = all_291_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | SIMP: (354) implies: % 136.03/19.00 | | | | | | | (355) all_335_0 = all_291_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | COMBINE_EQS: (350), (355) imply: % 136.03/19.00 | | | | | | | (356) all_329_0 = all_291_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | SIMP: (356) implies: % 136.03/19.00 | | | | | | | (357) all_329_0 = all_291_0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | COMBINE_EQS: (349), (357) imply: % 136.03/19.00 | | | | | | | (358) all_291_0 = tptp0 % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | REDUCE: (256), (349) imply: % 136.03/19.00 | | | | | | | (359) leaf(all_207_0, tptp0) % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | REF_CLOSE: (10), (11), (28), (33), (60), (68), (113), (115), % 136.03/19.00 | | | | | | | (116), (191), (194), (205), (224), (225), (254), (255), % 136.03/19.00 | | | | | | | (257), (259), (260), (262), (263), (265), (266), (347), % 136.03/19.00 | | | | | | | (348), (358), (359), (sos_21), (sos_22), (sos_28) are % 136.03/19.00 | | | | | | | inconsistent by sub-proof #1. % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | Case 2: % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | (360) ~ min_precedes(all_46_1, all_58_2, tptp0) % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | BETA: splitting (157) gives: % 136.03/19.00 | | | | | | | % 136.03/19.00 | | | | | | | Case 1: % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | (361) min_precedes(all_58_2, all_46_1, tptp0) % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | GROUND_INST: instantiating (sos_07) with all_58_2, all_46_1, % 136.03/19.00 | | | | | | | | tptp0, simplifying with (11), (33), (36), (42), % 136.03/19.00 | | | | | | | | (361) gives: % 136.03/19.00 | | | | | | | | (362) $false % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | CLOSE: (362) is inconsistent. % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | Case 2: % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | (363) all_58_2 = all_46_1 | ~ % 136.03/19.00 | | | | | | | | subactivity_occurrence(all_58_2, all_120_0) | % 136.03/19.00 | | | | | | | | min_precedes(all_46_1, all_58_2, tptp0) % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | BETA: splitting (148) gives: % 136.03/19.00 | | | | | | | | % 136.03/19.00 | | | | | | | | Case 1: % 136.03/19.00 | | | | | | | | | % 136.03/19.00 | | | | | | | | | (364) ~ occurrence_of(all_46_1, all_118_0) % 136.03/19.00 | | | | | | | | | % 136.03/19.00 | | | | | | | | | PRED_UNIFY: (110), (364) imply: % 136.03/19.00 | | | | | | | | | (365) ~ (all_58_2 = all_46_1) % 136.03/19.00 | | | | | | | | | % 136.03/19.00 | | | | | | | | | BETA: splitting (363) gives: % 136.03/19.00 | | | | | | | | | % 136.03/19.00 | | | | | | | | | Case 1: % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | (366) min_precedes(all_46_1, all_58_2, tptp0) % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | PRED_UNIFY: (360), (366) imply: % 136.03/19.00 | | | | | | | | | | (367) $false % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | CLOSE: (367) is inconsistent. % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | Case 2: % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | (368) all_58_2 = all_46_1 | ~ % 136.03/19.00 | | | | | | | | | | subactivity_occurrence(all_58_2, all_120_0) % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | BETA: splitting (368) gives: % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | Case 1: % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_30) with all_291_0, all_120_0, % 136.03/19.00 | | | | | | | | | | | simplifying with (116), (224), (225) gives: % 136.03/19.00 | | | | | | | | | | | (369) atomic(all_291_0) | ? [v0: $i] : ($i(v0) & % 136.03/19.00 | | | | | | | | | | | subactivity_occurrence(v0, all_120_0) & root(v0, % 136.03/19.00 | | | | | | | | | | | all_291_0)) % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, tptp0, % 136.03/19.00 | | | | | | | | | | | all_343_0, simplifying with (11), (113), (116), % 136.03/19.00 | | | | | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | | | | | (370) all_343_0 = tptp0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_335_0, % 136.03/19.00 | | | | | | | | | | | all_343_0, simplifying with (116), (259), (260), % 136.03/19.00 | | | | | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | | | | | (371) all_343_0 = all_335_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_329_0, % 136.03/19.00 | | | | | | | | | | | all_343_0, simplifying with (116), (254), (257), % 136.03/19.00 | | | | | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | | | | | (372) all_343_0 = all_329_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_291_0, % 136.03/19.00 | | | | | | | | | | | all_343_0, simplifying with (116), (224), (225), % 136.03/19.00 | | | | | | | | | | | (262), (263) gives: % 136.03/19.00 | | | | | | | | | | | (373) all_343_0 = all_291_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | GROUND_INST: instantiating (sos_02) with all_46_1, all_193_0, % 136.03/19.00 | | | | | | | | | | | all_120_0, all_291_0, simplifying with (33), % 136.03/19.00 | | | | | | | | | | | (116), (156), (179), (209), (224), (225) gives: % 136.03/19.00 | | | | | | | | | | | (374) all_193_0 = all_46_1 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (371), (373) imply: % 136.03/19.00 | | | | | | | | | | | (375) all_335_0 = all_291_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (370), (371) imply: % 136.03/19.00 | | | | | | | | | | | (376) all_335_0 = tptp0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (371), (372) imply: % 136.03/19.00 | | | | | | | | | | | (377) all_335_0 = all_329_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (376), (377) imply: % 136.03/19.00 | | | | | | | | | | | (378) all_329_0 = tptp0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (375), (377) imply: % 136.03/19.00 | | | | | | | | | | | (379) all_329_0 = all_291_0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | COMBINE_EQS: (378), (379) imply: % 136.03/19.00 | | | | | | | | | | | (380) all_291_0 = tptp0 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | REDUCE: (256), (378) imply: % 136.03/19.00 | | | | | | | | | | | (381) leaf(all_207_0, tptp0) % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | REF_CLOSE: (10), (11), (28), (33), (60), (68), (113), (115), % 136.03/19.00 | | | | | | | | | | | (116), (191), (194), (205), (224), (225), (254), % 136.03/19.00 | | | | | | | | | | | (255), (257), (259), (260), (262), (263), (265), % 136.03/19.00 | | | | | | | | | | | (266), (347), (369), (380), (381), (sos_21), % 136.03/19.00 | | | | | | | | | | | (sos_22), (sos_28) are inconsistent by sub-proof % 136.03/19.00 | | | | | | | | | | | #1. % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | Case 2: % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | (382) all_58_2 = all_46_1 % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | REDUCE: (365), (382) imply: % 136.03/19.00 | | | | | | | | | | | (383) $false % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | | CLOSE: (383) is inconsistent. % 136.03/19.00 | | | | | | | | | | | % 136.03/19.00 | | | | | | | | | | End of split % 136.03/19.00 | | | | | | | | | | % 136.03/19.00 | | | | | | | | | End of split % 136.03/19.00 | | | | | | | | | % 136.03/19.00 | | | | | | | | Case 2: % 136.03/19.00 | | | | | | | | | % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_30) with all_291_0, all_120_0, % 136.03/19.01 | | | | | | | | | simplifying with (116), (224), (225) gives: % 136.03/19.01 | | | | | | | | | (384) atomic(all_291_0) | ? [v0: $i] : ($i(v0) & % 136.03/19.01 | | | | | | | | | subactivity_occurrence(v0, all_120_0) & root(v0, % 136.03/19.01 | | | | | | | | | all_291_0)) % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, tptp0, % 136.03/19.01 | | | | | | | | | all_335_0, simplifying with (11), (113), (116), % 136.03/19.01 | | | | | | | | | (259), (260) gives: % 136.03/19.01 | | | | | | | | | (385) all_335_0 = tptp0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_335_0, % 136.03/19.01 | | | | | | | | | all_343_0, simplifying with (116), (259), (260), % 136.03/19.01 | | | | | | | | | (262), (263) gives: % 136.03/19.01 | | | | | | | | | (386) all_343_0 = all_335_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_329_0, % 136.03/19.01 | | | | | | | | | all_343_0, simplifying with (116), (254), (257), % 136.03/19.01 | | | | | | | | | (262), (263) gives: % 136.03/19.01 | | | | | | | | | (387) all_343_0 = all_329_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_120_0, all_291_0, % 136.03/19.01 | | | | | | | | | all_343_0, simplifying with (116), (224), (225), % 136.03/19.01 | | | | | | | | | (262), (263) gives: % 136.03/19.01 | | | | | | | | | (388) all_343_0 = all_291_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | GROUND_INST: instantiating (sos_02) with all_46_1, all_193_0, % 136.03/19.01 | | | | | | | | | all_120_0, all_291_0, simplifying with (33), % 136.03/19.01 | | | | | | | | | (116), (156), (179), (209), (224), (225) gives: % 136.03/19.01 | | | | | | | | | (389) all_193_0 = all_46_1 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | COMBINE_EQS: (386), (387) imply: % 136.03/19.01 | | | | | | | | | (390) all_335_0 = all_329_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | SIMP: (390) implies: % 136.03/19.01 | | | | | | | | | (391) all_335_0 = all_329_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | COMBINE_EQS: (387), (388) imply: % 136.03/19.01 | | | | | | | | | (392) all_329_0 = all_291_0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | COMBINE_EQS: (385), (391) imply: % 136.03/19.01 | | | | | | | | | (393) all_329_0 = tptp0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | SIMP: (393) implies: % 136.03/19.01 | | | | | | | | | (394) all_329_0 = tptp0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | COMBINE_EQS: (392), (394) imply: % 136.03/19.01 | | | | | | | | | (395) all_291_0 = tptp0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | SIMP: (395) implies: % 136.03/19.01 | | | | | | | | | (396) all_291_0 = tptp0 % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | REDUCE: (256), (394) imply: % 136.03/19.01 | | | | | | | | | (397) leaf(all_207_0, tptp0) % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | | REF_CLOSE: (10), (11), (28), (33), (60), (68), (113), (115), % 136.03/19.01 | | | | | | | | | (116), (191), (194), (205), (224), (225), (254), % 136.03/19.01 | | | | | | | | | (255), (257), (259), (260), (262), (263), (265), % 136.03/19.01 | | | | | | | | | (266), (347), (384), (396), (397), (sos_21), % 136.03/19.01 | | | | | | | | | (sos_22), (sos_28) are inconsistent by sub-proof % 136.03/19.01 | | | | | | | | | #1. % 136.03/19.01 | | | | | | | | | % 136.03/19.01 | | | | | | | | End of split % 136.03/19.01 | | | | | | | | % 136.03/19.01 | | | | | | | End of split % 136.03/19.01 | | | | | | | % 136.03/19.01 | | | | | | End of split % 136.03/19.01 | | | | | | % 136.03/19.01 | | | | | End of split % 136.03/19.01 | | | | | % 136.03/19.01 | | | | Case 2: % 136.03/19.01 | | | | | % 136.03/19.01 | | | | | (398) arboreal(all_58_0) % 136.03/19.01 | | | | | % 136.03/19.01 | | | | | GROUND_INST: instantiating (22) with all_58_0, all_58_3, simplifying % 136.03/19.01 | | | | | with (38), (41), (44), (95), (398) gives: % 136.03/19.01 | | | | | (399) $false % 136.03/19.01 | | | | | % 136.03/19.01 | | | | | CLOSE: (399) is inconsistent. % 136.03/19.01 | | | | | % 136.03/19.01 | | | | End of split % 136.03/19.01 | | | | % 136.03/19.01 | | | End of split % 136.03/19.01 | | | % 136.03/19.01 | | End of split % 136.03/19.01 | | % 136.03/19.01 | End of split % 136.03/19.01 | % 136.03/19.01 End of proof % 136.03/19.01 % 136.03/19.01 Sub-proof #1 shows that the following formulas are inconsistent: % 136.03/19.01 ---------------------------------------------------------------- % 136.03/19.01 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 136.03/19.01 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v1, v0) | ~ % 136.03/19.01 occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) % 136.03/19.01 (2) occurrence_of(all_120_0, all_343_0) % 136.03/19.01 (3) subactivity_occurrence(all_207_0, all_120_0) % 136.03/19.01 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ % 136.03/19.01 $i(v1) | ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, % 136.03/19.01 v1)) % 136.03/19.01 (5) arboreal(all_74_0) % 136.03/19.01 (6) $i(all_46_1) % 136.03/19.01 (7) occurrence_of(all_120_0, all_329_0) % 136.03/19.01 (8) arboreal(all_207_0) % 136.03/19.01 (9) atomic(all_291_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 136.03/19.01 all_120_0) & root(v0, all_291_0)) % 136.03/19.01 (10) occurrence_of(all_120_0, tptp0) % 136.03/19.01 (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 136.03/19.01 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 136.03/19.01 min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 136.03/19.01 (12) ~ leaf(all_74_0, tptp0) % 136.03/19.01 (13) leaf_occ(all_207_0, all_120_0) % 136.03/19.01 (14) $i(all_329_0) % 136.03/19.01 (15) ~ atomic(tptp0) % 136.03/19.01 (16) $i(all_207_0) % 136.03/19.01 (17) $i(all_74_0) % 136.03/19.01 (18) $i(all_291_0) % 136.03/19.01 (19) all_291_0 = tptp0 % 136.03/19.01 (20) $i(tptp0) % 136.03/19.01 (21) $i(all_343_0) % 136.03/19.01 (22) $i(all_335_0) % 136.03/19.01 (23) subactivity_occurrence(all_74_0, all_120_0) % 136.03/19.01 (24) occurrence_of(all_120_0, all_291_0) % 136.03/19.01 (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ % 136.03/19.01 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 136.03/19.01 subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | % 136.03/19.01 ~ arboreal(v3) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | % 136.03/19.01 min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 136.03/19.01 (26) $i(all_120_0) % 136.03/19.01 (27) occurrence_of(all_120_0, all_335_0) % 136.03/19.01 (28) next_subocc(all_46_1, all_207_0, tptp0) % 136.03/19.01 (29) min_precedes(all_46_1, all_74_0, tptp0) % 136.03/19.01 (30) leaf(all_207_0, tptp0) % 136.03/19.01 % 136.03/19.01 Begin of proof % 136.03/19.01 | % 136.03/19.01 | BETA: splitting (9) gives: % 136.03/19.01 | % 136.03/19.01 | Case 1: % 136.03/19.01 | | % 136.03/19.01 | | (31) atomic(all_291_0) % 136.03/19.01 | | % 136.03/19.01 | | REDUCE: (19), (31) imply: % 136.03/19.01 | | (32) atomic(tptp0) % 136.03/19.01 | | % 136.03/19.01 | | PRED_UNIFY: (15), (32) imply: % 136.03/19.01 | | (33) $false % 136.03/19.01 | | % 136.03/19.01 | | CLOSE: (33) is inconsistent. % 136.03/19.01 | | % 136.03/19.01 | Case 2: % 136.03/19.01 | | % 136.03/19.01 | | % 136.03/19.01 | | PRED_UNIFY: (12), (30) imply: % 136.03/19.01 | | (34) ~ (all_207_0 = all_74_0) % 136.03/19.01 | | % 136.03/19.01 | | GROUND_INST: instantiating (1) with all_120_0, all_207_0, tptp0, all_74_0, % 136.03/19.01 | | simplifying with (10), (13), (16), (17), (20), (26) gives: % 136.03/19.01 | | (35) ~ min_precedes(all_207_0, all_74_0, tptp0) % 136.03/19.01 | | % 136.03/19.01 | | GROUND_INST: instantiating (4) with all_120_0, all_291_0, all_335_0, % 136.03/19.01 | | simplifying with (18), (22), (24), (26), (27) gives: % 136.03/19.01 | | (36) all_335_0 = all_291_0 % 136.03/19.01 | | % 136.03/19.01 | | GROUND_INST: instantiating (4) with all_120_0, tptp0, all_343_0, simplifying % 136.03/19.01 | | with (2), (10), (20), (21), (26) gives: % 136.03/19.01 | | (37) all_343_0 = tptp0 % 136.03/19.01 | | % 136.03/19.01 | | GROUND_INST: instantiating (4) with all_120_0, all_335_0, all_343_0, % 136.03/19.01 | | simplifying with (2), (21), (22), (26), (27) gives: % 136.03/19.01 | | (38) all_343_0 = all_335_0 % 136.03/19.01 | | % 136.03/19.02 | | GROUND_INST: instantiating (4) with all_120_0, all_329_0, all_343_0, % 136.03/19.02 | | simplifying with (2), (7), (14), (21), (26) gives: % 136.03/19.02 | | (39) all_343_0 = all_329_0 % 136.03/19.02 | | % 136.03/19.02 | | GROUND_INST: instantiating (11) with all_46_1, all_207_0, tptp0, all_74_0, % 136.03/19.02 | | simplifying with (6), (16), (17), (20), (28), (29) gives: % 136.03/19.02 | | (40) ~ min_precedes(all_74_0, all_207_0, tptp0) % 136.03/19.02 | | % 136.03/19.02 | | GROUND_INST: instantiating (25) with all_291_0, all_120_0, all_207_0, % 136.03/19.02 | | all_74_0, simplifying with (3), (5), (8), (16), (17), (18), % 136.03/19.02 | | (23), (24), (26) gives: % 136.03/19.02 | | (41) all_207_0 = all_74_0 | min_precedes(all_207_0, all_74_0, all_291_0) % 136.03/19.02 | | | min_precedes(all_74_0, all_207_0, all_291_0) % 136.03/19.02 | | % 136.03/19.02 | | COMBINE_EQS: (38), (39) imply: % 136.03/19.02 | | (42) all_335_0 = all_329_0 % 136.03/19.02 | | % 136.03/19.02 | | SIMP: (42) implies: % 136.03/19.02 | | (43) all_335_0 = all_329_0 % 136.03/19.02 | | % 136.03/19.02 | | COMBINE_EQS: (37), (39) imply: % 136.03/19.02 | | (44) all_329_0 = tptp0 % 136.03/19.02 | | % 136.03/19.02 | | COMBINE_EQS: (36), (43) imply: % 136.03/19.02 | | (45) all_329_0 = all_291_0 % 136.03/19.02 | | % 136.03/19.02 | | SIMP: (45) implies: % 136.03/19.02 | | (46) all_329_0 = all_291_0 % 136.03/19.02 | | % 136.03/19.02 | | COMBINE_EQS: (44), (46) imply: % 136.03/19.02 | | (47) all_291_0 = tptp0 % 136.03/19.02 | | % 136.03/19.02 | | BETA: splitting (41) gives: % 136.03/19.02 | | % 136.03/19.02 | | Case 1: % 136.03/19.02 | | | % 136.03/19.02 | | | (48) min_precedes(all_207_0, all_74_0, all_291_0) % 136.03/19.02 | | | % 136.03/19.02 | | | REDUCE: (19), (48) imply: % 136.03/19.02 | | | (49) min_precedes(all_207_0, all_74_0, tptp0) % 136.03/19.02 | | | % 136.03/19.02 | | | PRED_UNIFY: (35), (49) imply: % 136.03/19.02 | | | (50) $false % 136.03/19.02 | | | % 136.03/19.02 | | | CLOSE: (50) is inconsistent. % 136.03/19.02 | | | % 136.03/19.02 | | Case 2: % 136.03/19.02 | | | % 136.03/19.02 | | | (51) all_207_0 = all_74_0 | min_precedes(all_74_0, all_207_0, % 136.03/19.02 | | | all_291_0) % 136.03/19.02 | | | % 136.03/19.02 | | | BETA: splitting (51) gives: % 136.03/19.02 | | | % 136.03/19.02 | | | Case 1: % 136.03/19.02 | | | | % 136.03/19.02 | | | | (52) min_precedes(all_74_0, all_207_0, all_291_0) % 136.03/19.02 | | | | % 136.03/19.02 | | | | REDUCE: (19), (52) imply: % 136.03/19.02 | | | | (53) min_precedes(all_74_0, all_207_0, tptp0) % 136.03/19.02 | | | | % 136.03/19.02 | | | | PRED_UNIFY: (40), (53) imply: % 136.03/19.02 | | | | (54) $false % 136.03/19.02 | | | | % 136.03/19.02 | | | | CLOSE: (54) is inconsistent. % 136.03/19.02 | | | | % 136.03/19.02 | | | Case 2: % 136.03/19.02 | | | | % 136.03/19.02 | | | | (55) all_207_0 = all_74_0 % 136.03/19.02 | | | | % 136.03/19.02 | | | | REDUCE: (34), (55) imply: % 136.03/19.02 | | | | (56) $false % 136.03/19.02 | | | | % 136.03/19.02 | | | | CLOSE: (56) is inconsistent. % 136.03/19.02 | | | | % 136.03/19.02 | | | End of split % 136.03/19.02 | | | % 136.03/19.02 | | End of split % 136.03/19.02 | | % 136.03/19.02 | End of split % 136.03/19.02 | % 136.03/19.02 End of proof % 136.03/19.02 % SZS output end Proof for theBenchmark % 136.03/19.02 % 136.03/19.02 18422ms %------------------------------------------------------------------------------