%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO003+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n005.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:44 EDT 2023 % Result : Theorem 56.87s 8.25s % Output : Proof 158.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO003+4 : TPTP v8.1.2. Released v4.0.0. % 0.11/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n005.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Mon Aug 28 19:12:53 EDT 2023 % 0.13/0.34 % CPUTime : % 0.18/0.59 ________ _____ % 0.18/0.59 ___ __ \_________(_)________________________________ % 0.18/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.18/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.18/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.18/0.59 % 0.18/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.18/0.59 (2023-06-19) % 0.18/0.59 % 0.18/0.59 (c) Philipp Rümmer, 2009-2023 % 0.18/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.18/0.59 Amanda Stjerna. % 0.18/0.59 Free software under BSD-3-Clause. % 0.18/0.59 % 0.18/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.18/0.59 % 0.18/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.18/0.60 Running up to 7 provers in parallel. % 0.18/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.18/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.18/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.18/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.18/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.18/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.18/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.22/1.13 Prover 4: Preprocessing ... % 3.22/1.13 Prover 1: Preprocessing ... % 3.22/1.17 Prover 6: Preprocessing ... % 3.22/1.17 Prover 0: Preprocessing ... % 3.22/1.17 Prover 3: Preprocessing ... % 3.22/1.17 Prover 5: Preprocessing ... % 3.22/1.17 Prover 2: Preprocessing ... % 6.24/1.59 Prover 2: Constructing countermodel ... % 6.24/1.61 Prover 5: Proving ... % 7.69/1.76 Prover 1: Constructing countermodel ... % 7.89/1.79 Prover 3: Constructing countermodel ... % 7.89/1.80 Prover 6: Proving ... % 9.33/2.00 Prover 4: Constructing countermodel ... % 9.75/2.05 Prover 0: Proving ... % 56.87/8.25 Prover 2: proved (7604ms) % 56.87/8.25 % 56.87/8.25 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.87/8.25 % 56.87/8.25 Prover 3: stopped % 56.87/8.25 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 56.87/8.26 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 56.87/8.26 Prover 6: stopped % 56.87/8.26 Prover 5: stopped % 57.39/8.28 Prover 0: stopped % 57.39/8.28 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 57.39/8.28 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 57.39/8.28 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 57.39/8.33 Prover 8: Preprocessing ... % 58.03/8.36 Prover 10: Preprocessing ... % 58.03/8.37 Prover 7: Preprocessing ... % 58.23/8.40 Prover 11: Preprocessing ... % 58.23/8.41 Prover 10: Constructing countermodel ... % 58.23/8.42 Prover 13: Preprocessing ... % 58.58/8.44 Prover 7: Constructing countermodel ... % 58.70/8.48 Prover 13: Constructing countermodel ... % 58.70/8.50 Prover 8: Warning: ignoring some quantifiers % 58.70/8.50 Prover 8: Constructing countermodel ... % 59.69/8.61 Prover 11: Constructing countermodel ... % 91.76/12.73 Prover 13: stopped % 91.76/12.74 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 92.33/12.81 Prover 16: Preprocessing ... % 92.33/12.84 Prover 16: Constructing countermodel ... % 116.48/15.97 Prover 1: stopped % 116.48/15.97 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 116.74/16.02 Prover 19: Preprocessing ... % 116.95/16.13 Prover 19: Warning: ignoring some quantifiers % 116.95/16.13 Prover 19: Constructing countermodel ... % 131.07/17.98 Prover 16: stopped % 142.94/19.74 Prover 19: stopped % 157.08/22.40 Prover 7: Found proof (size 266) % 157.08/22.40 Prover 7: proved (14107ms) % 157.08/22.41 Prover 10: stopped % 157.08/22.41 Prover 8: stopped % 157.08/22.41 Prover 11: stopped % 157.08/22.41 Prover 4: stopped % 157.08/22.41 % 157.08/22.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 157.08/22.41 % 157.38/22.43 % SZS output start Proof for theBenchmark % 157.38/22.44 Assumptions after simplification: % 157.38/22.44 --------------------------------- % 157.38/22.44 % 157.38/22.44 (goals) % 157.38/22.44 $i(tptp0) & ? [v0: $i] : ($i(v0) & occurrence_of(v0, tptp0)) % 157.38/22.44 % 157.38/22.44 (sos) % 157.38/22.44 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 157.38/22.44 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 157.38/22.44 root(v2, v0))) % 157.38/22.44 % 157.38/22.44 (sos_01) % 157.38/22.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v4 = v2 % 157.38/22.45 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 157.38/22.45 min_precedes(v3, v2, v0) | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ % 157.38/22.45 subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v2, % 157.38/22.45 v4, v0)) % 157.38/22.45 % 157.38/22.45 (sos_02) % 157.38/22.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 157.38/22.45 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | % 157.38/22.45 ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | % 157.38/22.45 min_precedes(v2, v3, v0)) % 157.38/22.45 % 157.38/22.45 (sos_03) % 157.50/22.45 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 157.50/22.45 | activity_occurrence(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 157.50/22.45 $i(v0) | ~ occurrence_of(v1, v0) | activity(v0)) % 157.50/22.45 % 157.50/22.45 (sos_06) % 157.50/22.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 157.50/22.45 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 157.50/22.45 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 157.50/22.45 occurrence_of(v3, v0))) % 157.50/22.45 % 157.50/22.45 (sos_07) % 157.50/22.45 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | % 157.50/22.45 atomic(v1) | ? [v2: $i] : ($i(v2) & leaf_occ(v0, v2) & occurrence_of(v2, % 157.50/22.45 v1))) % 157.50/22.45 % 157.50/22.45 (sos_08) % 157.50/22.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 157.50/22.45 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 157.50/22.45 % 157.50/22.45 (sos_12) % 157.50/22.45 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 157.50/22.45 & activity(v1) & occurrence_of(v0, v1))) % 157.50/22.45 % 157.50/22.45 (sos_16) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | ~ % 157.50/22.46 occurrence_of(v0, v1) | atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) % 157.50/22.46 | ~ $i(v0) | ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 157.50/22.46 % 157.50/22.46 (sos_18) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 157.50/22.46 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 157.50/22.46 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 157.50/22.46 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 157.50/22.46 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 157.50/22.46 % 157.50/22.46 (sos_19) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 157.50/22.46 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 157.50/22.46 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 157.50/22.46 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 157.50/22.46 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 157.50/22.46 % 157.50/22.46 (sos_23) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 157.50/22.46 ~ min_precedes(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, % 157.50/22.46 v2) & root(v3, v2))) % 157.50/22.46 % 157.50/22.46 (sos_25) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 157.50/22.46 ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0: $i] : ! [v1: $i] : ! % 157.50/22.46 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 157.50/22.46 arboreal(v0)) % 157.50/22.46 % 157.50/22.46 (sos_26) % 157.50/22.46 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 157.50/22.46 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 157.50/22.46 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 157.50/22.47 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 157.50/22.47 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 157.50/22.47 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 157.50/22.47 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 157.50/22.47 min_precedes(v0, v3, v2))) % 157.50/22.47 % 157.50/22.47 (sos_27) % 157.50/22.47 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 157.50/22.47 | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | ~ % 157.50/22.47 subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | % 157.50/22.47 subactivity_occurrence(v0, v3)) % 157.50/22.47 % 157.50/22.47 (sos_29) % 157.50/22.47 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 157.50/22.47 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 157.50/22.47 v2) | ~ occurrence_of(v2, v3)) % 157.50/22.47 % 157.50/22.47 (sos_32) % 157.50/22.47 $i(tptp3) & $i(tptp4) & $i(tptp0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 157.50/22.47 occurrence_of(v0, tptp0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 157.50/22.47 next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & % 157.50/22.47 occurrence_of(v2, tptp3) & occurrence_of(v1, tptp4))) % 157.50/22.47 % 157.50/22.47 (sos_34) % 157.50/22.47 $i(tptp0) & ~ atomic(tptp0) % 157.50/22.47 % 157.50/22.47 (sos_37) % 157.50/22.47 $i(tptp2) & atomic(tptp2) % 157.50/22.47 % 157.50/22.47 (sos_38) % 157.50/22.47 $i(tptp1) & atomic(tptp1) % 157.50/22.47 % 157.50/22.47 (sos_40) % 157.50/22.47 ~ (tptp3 = tptp4) & $i(tptp3) & $i(tptp4) % 157.50/22.47 % 157.50/22.47 (sos_42) % 157.50/22.47 ~ (tptp1 = tptp3) & $i(tptp1) & $i(tptp3) % 157.50/22.47 % 157.50/22.47 (sos_45) % 157.50/22.47 $i(tptp1) & $i(tptp0) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | % 157.50/22.47 ~ root_occ(v0, v1) | ~ occurrence_of(v1, tptp0) | ? [v2: $i] : ($i(v2) & % 157.50/22.47 next_subocc(v0, v2, tptp0) & occurrence_of(v2, tptp1))) % 157.50/22.47 % 157.50/22.47 Further assumptions not needed in the proof: % 157.50/22.47 -------------------------------------------- % 157.50/22.47 sos_04, sos_05, sos_09, sos_10, sos_11, sos_13, sos_14, sos_15, sos_17, sos_20, % 157.50/22.47 sos_21, sos_22, sos_24, sos_28, sos_30, sos_31, sos_33, sos_35, sos_36, sos_39, % 157.50/22.47 sos_41, sos_43, sos_44 % 157.50/22.47 % 157.50/22.47 Those formulas are unsatisfiable: % 157.50/22.47 --------------------------------- % 157.50/22.47 % 157.50/22.47 Begin of proof % 157.50/22.47 | % 157.50/22.47 | ALPHA: (goals) implies: % 157.50/22.47 | (1) ? [v0: $i] : ($i(v0) & occurrence_of(v0, tptp0)) % 157.50/22.47 | % 157.50/22.47 | ALPHA: (sos_45) implies: % 157.50/22.47 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 157.50/22.47 | v1) | ~ occurrence_of(v1, tptp0) | ? [v2: $i] : ($i(v2) & % 157.50/22.47 | next_subocc(v0, v2, tptp0) & occurrence_of(v2, tptp1))) % 157.50/22.47 | % 157.50/22.47 | ALPHA: (sos_42) implies: % 157.50/22.48 | (3) ~ (tptp1 = tptp3) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_40) implies: % 157.50/22.48 | (4) ~ (tptp3 = tptp4) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_38) implies: % 157.50/22.48 | (5) $i(tptp1) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_37) implies: % 157.50/22.48 | (6) atomic(tptp2) % 157.50/22.48 | (7) $i(tptp2) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_34) implies: % 157.50/22.48 | (8) ~ atomic(tptp0) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_32) implies: % 157.50/22.48 | (9) $i(tptp0) % 157.50/22.48 | (10) $i(tptp4) % 157.50/22.48 | (11) $i(tptp3) % 157.50/22.48 | (12) ! [v0: $i] : ( ~ $i(v0) | ~ occurrence_of(v0, tptp0) | ? [v1: $i] : % 157.50/22.48 | ? [v2: $i] : ($i(v2) & $i(v1) & next_subocc(v1, v2, tptp0) & % 157.50/22.48 | leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v2, tptp3) & % 157.50/22.48 | occurrence_of(v1, tptp4))) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_26) implies: % 157.50/22.48 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 157.50/22.48 | $i(v0) | ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 157.50/22.48 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 157.50/22.48 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 157.50/22.48 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_25) implies: % 157.50/22.48 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 157.50/22.48 | $i(v0) | ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_19) implies: % 157.50/22.48 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 157.50/22.48 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 157.50/22.48 | root(v0, v2) & occurrence_of(v1, v2))) % 157.50/22.48 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 157.50/22.48 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 157.50/22.48 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_18) implies: % 157.50/22.48 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 157.50/22.48 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 157.50/22.48 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_16) implies: % 157.50/22.48 | (19) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atomic(v1) | % 157.50/22.48 | ~ occurrence_of(v0, v1) | arboreal(v0)) % 157.50/22.48 | (20) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | % 157.50/22.48 | ~ occurrence_of(v0, v1) | atomic(v1)) % 157.50/22.48 | % 157.50/22.48 | ALPHA: (sos_03) implies: % 157.50/22.49 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 157.50/22.49 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 157.50/22.49 | % 157.50/22.49 | DELTA: instantiating (1) with fresh symbol all_37_0 gives: % 157.50/22.49 | (22) $i(all_37_0) & occurrence_of(all_37_0, tptp0) % 157.50/22.49 | % 157.50/22.49 | ALPHA: (22) implies: % 157.50/22.49 | (23) occurrence_of(all_37_0, tptp0) % 157.50/22.49 | (24) $i(all_37_0) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (12) with all_37_0, simplifying with (23), (24) % 157.50/22.49 | gives: % 157.50/22.49 | (25) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & next_subocc(v0, v1, % 157.50/22.49 | tptp0) & leaf_occ(v1, all_37_0) & root_occ(v0, all_37_0) & % 157.50/22.49 | occurrence_of(v1, tptp3) & occurrence_of(v0, tptp4)) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (21) with tptp0, all_37_0, simplifying with (9), % 157.50/22.49 | (23), (24) gives: % 157.50/22.49 | (26) activity_occurrence(all_37_0) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (sos) with tptp0, all_37_0, simplifying with (8), % 157.50/22.49 | (9), (23), (24) gives: % 157.50/22.49 | (27) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_37_0) & % 157.50/22.49 | root(v0, tptp0)) % 157.50/22.49 | % 157.50/22.49 | DELTA: instantiating (27) with fresh symbol all_49_0 gives: % 157.50/22.49 | (28) $i(all_49_0) & subactivity_occurrence(all_49_0, all_37_0) & % 157.50/22.49 | root(all_49_0, tptp0) % 157.50/22.49 | % 157.50/22.49 | ALPHA: (28) implies: % 157.50/22.49 | (29) root(all_49_0, tptp0) % 157.50/22.49 | (30) subactivity_occurrence(all_49_0, all_37_0) % 157.50/22.49 | (31) $i(all_49_0) % 157.50/22.49 | % 157.50/22.49 | DELTA: instantiating (25) with fresh symbols all_51_0, all_51_1 gives: % 157.50/22.49 | (32) $i(all_51_0) & $i(all_51_1) & next_subocc(all_51_1, all_51_0, tptp0) & % 157.50/22.49 | leaf_occ(all_51_0, all_37_0) & root_occ(all_51_1, all_37_0) & % 157.50/22.49 | occurrence_of(all_51_0, tptp3) & occurrence_of(all_51_1, tptp4) % 157.50/22.49 | % 157.50/22.49 | ALPHA: (32) implies: % 157.50/22.49 | (33) occurrence_of(all_51_1, tptp4) % 157.50/22.49 | (34) occurrence_of(all_51_0, tptp3) % 157.50/22.49 | (35) root_occ(all_51_1, all_37_0) % 157.50/22.49 | (36) leaf_occ(all_51_0, all_37_0) % 157.50/22.49 | (37) next_subocc(all_51_1, all_51_0, tptp0) % 157.50/22.49 | (38) $i(all_51_1) % 157.50/22.49 | (39) $i(all_51_0) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (sos_08) with all_51_1, tptp4, tptp3, simplifying % 157.50/22.49 | with (10), (11), (33), (38) gives: % 157.50/22.49 | (40) tptp3 = tptp4 | ~ occurrence_of(all_51_1, tptp3) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (21) with tptp3, all_51_0, simplifying with (11), % 157.50/22.49 | (34), (39) gives: % 157.50/22.49 | (41) activity_occurrence(all_51_0) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (17) with all_49_0, all_37_0, tptp0, simplifying % 157.50/22.49 | with (9), (23), (24), (29), (30), (31) gives: % 157.50/22.49 | (42) root_occ(all_49_0, all_37_0) % 157.50/22.49 | % 157.50/22.49 | GROUND_INST: instantiating (2) with all_51_1, all_37_0, simplifying with (23), % 157.50/22.49 | (24), (35), (38) gives: % 157.50/22.49 | (43) ? [v0: $i] : ($i(v0) & next_subocc(all_51_1, v0, tptp0) & % 157.50/22.49 | occurrence_of(v0, tptp1)) % 157.50/22.49 | % 157.50/22.50 | GROUND_INST: instantiating (16) with all_51_1, all_37_0, simplifying with % 157.50/22.50 | (24), (35), (38) gives: % 157.50/22.50 | (44) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_51_1, all_37_0) & % 157.50/22.50 | root(all_51_1, v0) & occurrence_of(all_37_0, v0)) % 157.50/22.50 | % 157.50/22.50 | GROUND_INST: instantiating (18) with all_51_0, all_37_0, simplifying with % 157.50/22.50 | (24), (36), (39) gives: % 157.50/22.50 | (45) ? [v0: $i] : ($i(v0) & leaf(all_51_0, v0) & % 157.50/22.50 | subactivity_occurrence(all_51_0, all_37_0) & occurrence_of(all_37_0, % 157.50/22.50 | v0)) % 157.50/22.50 | % 157.50/22.50 | GROUND_INST: instantiating (sos_12) with all_37_0, simplifying with (24), (26) % 157.50/22.50 | gives: % 157.50/22.50 | (46) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_37_0, v0)) % 157.50/22.50 | % 157.50/22.50 | GROUND_INST: instantiating (13) with all_51_1, all_51_0, tptp0, simplifying % 157.50/22.50 | with (9), (37), (38), (39) gives: % 157.50/22.50 | (47) min_precedes(all_51_1, all_51_0, tptp0) % 157.50/22.50 | % 157.50/22.50 | DELTA: instantiating (46) with fresh symbol all_59_0 gives: % 157.50/22.50 | (48) $i(all_59_0) & activity(all_59_0) & occurrence_of(all_37_0, all_59_0) % 157.50/22.50 | % 157.50/22.50 | ALPHA: (48) implies: % 157.50/22.50 | (49) occurrence_of(all_37_0, all_59_0) % 157.50/22.50 | (50) $i(all_59_0) % 157.50/22.50 | % 157.50/22.50 | DELTA: instantiating (43) with fresh symbol all_63_0 gives: % 157.50/22.50 | (51) $i(all_63_0) & next_subocc(all_51_1, all_63_0, tptp0) & % 157.50/22.50 | occurrence_of(all_63_0, tptp1) % 157.50/22.50 | % 157.50/22.50 | ALPHA: (51) implies: % 157.50/22.50 | (52) occurrence_of(all_63_0, tptp1) % 157.50/22.50 | (53) next_subocc(all_51_1, all_63_0, tptp0) % 157.50/22.50 | (54) $i(all_63_0) % 157.50/22.50 | % 157.50/22.50 | DELTA: instantiating (45) with fresh symbol all_65_0 gives: % 157.50/22.50 | (55) $i(all_65_0) & leaf(all_51_0, all_65_0) & % 157.50/22.50 | subactivity_occurrence(all_51_0, all_37_0) & occurrence_of(all_37_0, % 157.50/22.50 | all_65_0) % 157.50/22.50 | % 157.50/22.50 | ALPHA: (55) implies: % 157.50/22.50 | (56) occurrence_of(all_37_0, all_65_0) % 157.50/22.50 | (57) subactivity_occurrence(all_51_0, all_37_0) % 157.50/22.50 | (58) leaf(all_51_0, all_65_0) % 157.50/22.50 | (59) $i(all_65_0) % 157.50/22.50 | % 157.50/22.50 | DELTA: instantiating (44) with fresh symbol all_67_0 gives: % 157.50/22.50 | (60) $i(all_67_0) & subactivity_occurrence(all_51_1, all_37_0) & % 157.50/22.50 | root(all_51_1, all_67_0) & occurrence_of(all_37_0, all_67_0) % 157.50/22.50 | % 157.50/22.50 | ALPHA: (60) implies: % 157.50/22.50 | (61) occurrence_of(all_37_0, all_67_0) % 157.50/22.50 | (62) $i(all_67_0) % 157.50/22.50 | % 157.50/22.50 | BETA: splitting (40) gives: % 157.50/22.50 | % 157.50/22.50 | Case 1: % 157.50/22.50 | | % 157.50/22.50 | | % 157.50/22.50 | | GROUND_INST: instantiating (19) with all_37_0, tptp2, simplifying with (6), % 157.50/22.50 | | (7), (24) gives: % 157.50/22.50 | | (63) ~ occurrence_of(all_37_0, tptp2) | arboreal(all_37_0) % 157.50/22.50 | | % 157.50/22.50 | | GROUND_INST: instantiating (sos) with all_59_0, all_37_0, simplifying with % 157.50/22.50 | | (24), (49), (50) gives: % 157.50/22.50 | | (64) atomic(all_59_0) | ? [v0: $i] : ($i(v0) & % 157.50/22.50 | | subactivity_occurrence(v0, all_37_0) & root(v0, all_59_0)) % 157.50/22.50 | | % 157.50/22.50 | | GROUND_INST: instantiating (sos_08) with all_37_0, tptp0, all_65_0, % 157.50/22.50 | | simplifying with (9), (23), (24), (56), (59) gives: % 157.50/22.50 | | (65) all_65_0 = tptp0 % 157.50/22.50 | | % 157.50/22.50 | | GROUND_INST: instantiating (sos) with all_65_0, all_37_0, simplifying with % 157.50/22.50 | | (24), (56), (59) gives: % 157.50/22.50 | | (66) atomic(all_65_0) | ? [v0: $i] : ($i(v0) & % 157.50/22.50 | | subactivity_occurrence(v0, all_37_0) & root(v0, all_65_0)) % 157.50/22.50 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_08) with all_37_0, all_65_0, all_67_0, % 157.50/22.51 | | simplifying with (24), (56), (59), (61), (62) gives: % 157.50/22.51 | | (67) all_67_0 = all_65_0 % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_08) with all_37_0, all_59_0, all_67_0, % 157.50/22.51 | | simplifying with (24), (49), (50), (61), (62) gives: % 157.50/22.51 | | (68) all_67_0 = all_59_0 % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos) with all_67_0, all_37_0, simplifying with % 157.50/22.51 | | (24), (61), (62) gives: % 157.50/22.51 | | (69) atomic(all_67_0) | ? [v0: $i] : ($i(v0) & % 157.50/22.51 | | subactivity_occurrence(v0, all_37_0) & root(v0, all_67_0)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_08) with all_51_0, tptp3, tptp1, simplifying % 157.50/22.51 | | with (5), (11), (34), (39) gives: % 157.50/22.51 | | (70) tptp1 = tptp3 | ~ occurrence_of(all_51_0, tptp1) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (21) with tptp1, all_63_0, simplifying with (5), % 157.50/22.51 | | (52), (54) gives: % 157.50/22.51 | | (71) activity_occurrence(all_63_0) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_29) with all_51_1, all_49_0, all_37_0, % 157.50/22.51 | | all_59_0, simplifying with (24), (31), (35), (38), (42), (49), % 157.50/22.51 | | (50) gives: % 157.50/22.51 | | (72) all_51_1 = all_49_0 % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (2) with all_49_0, all_37_0, simplifying with % 157.50/22.51 | | (23), (24), (31), (42) gives: % 157.50/22.51 | | (73) ? [v0: $i] : ($i(v0) & next_subocc(all_49_0, v0, tptp0) & % 157.50/22.51 | | occurrence_of(v0, tptp1)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (16) with all_49_0, all_37_0, simplifying with % 157.50/22.51 | | (24), (31), (42) gives: % 157.50/22.51 | | (74) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_49_0, all_37_0) & % 157.50/22.51 | | root(all_49_0, v0) & occurrence_of(all_37_0, v0)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_23) with all_51_1, all_51_0, tptp0, % 157.50/22.51 | | simplifying with (9), (38), (39), (47) gives: % 157.50/22.51 | | (75) ? [v0: $i] : ($i(v0) & min_precedes(v0, all_51_0, tptp0) & root(v0, % 157.50/22.51 | | tptp0)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_12) with all_51_0, simplifying with (39), % 157.50/22.51 | | (41) gives: % 157.50/22.51 | | (76) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_51_0, v0)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (sos_07) with all_51_0, all_65_0, simplifying % 157.50/22.51 | | with (39), (58), (59) gives: % 157.50/22.51 | | (77) atomic(all_65_0) | ? [v0: $i] : ($i(v0) & leaf_occ(all_51_0, v0) & % 157.50/22.51 | | occurrence_of(v0, all_65_0)) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (15) with all_51_1, all_63_0, tptp0, simplifying % 157.50/22.51 | | with (9), (38), (53), (54) gives: % 157.50/22.51 | | (78) arboreal(all_63_0) % 157.50/22.51 | | % 157.50/22.51 | | GROUND_INST: instantiating (13) with all_51_1, all_63_0, tptp0, simplifying % 157.50/22.51 | | with (9), (38), (53), (54) gives: % 157.50/22.51 | | (79) min_precedes(all_51_1, all_63_0, tptp0) % 157.50/22.51 | | % 157.50/22.51 | | COMBINE_EQS: (67), (68) imply: % 157.50/22.52 | | (80) all_65_0 = all_59_0 % 157.50/22.52 | | % 157.50/22.52 | | SIMP: (80) implies: % 157.50/22.52 | | (81) all_65_0 = all_59_0 % 157.50/22.52 | | % 157.50/22.52 | | COMBINE_EQS: (65), (81) imply: % 157.50/22.52 | | (82) all_59_0 = tptp0 % 157.50/22.52 | | % 157.50/22.52 | | SIMP: (82) implies: % 157.50/22.52 | | (83) all_59_0 = tptp0 % 157.50/22.52 | | % 157.50/22.52 | | COMBINE_EQS: (68), (83) imply: % 157.50/22.52 | | (84) all_67_0 = tptp0 % 157.50/22.52 | | % 157.50/22.52 | | DELTA: instantiating (76) with fresh symbol all_91_0 gives: % 157.50/22.52 | | (85) $i(all_91_0) & activity(all_91_0) & occurrence_of(all_51_0, % 157.50/22.52 | | all_91_0) % 157.50/22.52 | | % 157.50/22.52 | | ALPHA: (85) implies: % 157.50/22.52 | | (86) occurrence_of(all_51_0, all_91_0) % 157.50/22.52 | | (87) $i(all_91_0) % 157.50/22.52 | | % 157.50/22.52 | | DELTA: instantiating (73) with fresh symbol all_93_0 gives: % 157.50/22.52 | | (88) $i(all_93_0) & next_subocc(all_49_0, all_93_0, tptp0) & % 157.50/22.52 | | occurrence_of(all_93_0, tptp1) % 157.50/22.52 | | % 157.50/22.52 | | ALPHA: (88) implies: % 157.50/22.52 | | (89) occurrence_of(all_93_0, tptp1) % 157.50/22.52 | | (90) $i(all_93_0) % 157.50/22.52 | | % 157.50/22.52 | | DELTA: instantiating (75) with fresh symbol all_101_0 gives: % 157.50/22.52 | | (91) $i(all_101_0) & min_precedes(all_101_0, all_51_0, tptp0) & % 157.50/22.52 | | root(all_101_0, tptp0) % 157.50/22.52 | | % 157.50/22.52 | | ALPHA: (91) implies: % 157.50/22.52 | | (92) root(all_101_0, tptp0) % 157.50/22.52 | | (93) min_precedes(all_101_0, all_51_0, tptp0) % 157.50/22.52 | | (94) $i(all_101_0) % 157.50/22.52 | | % 157.50/22.52 | | DELTA: instantiating (74) with fresh symbol all_107_0 gives: % 157.50/22.52 | | (95) $i(all_107_0) & subactivity_occurrence(all_49_0, all_37_0) & % 157.50/22.52 | | root(all_49_0, all_107_0) & occurrence_of(all_37_0, all_107_0) % 157.50/22.52 | | % 157.50/22.52 | | ALPHA: (95) implies: % 157.50/22.52 | | (96) occurrence_of(all_37_0, all_107_0) % 157.50/22.52 | | (97) root(all_49_0, all_107_0) % 157.50/22.52 | | (98) $i(all_107_0) % 157.50/22.52 | | % 157.50/22.52 | | REDUCE: (37), (72) imply: % 157.50/22.52 | | (99) next_subocc(all_49_0, all_51_0, tptp0) % 157.50/22.52 | | % 157.50/22.52 | | REDUCE: (72), (79) imply: % 157.50/22.52 | | (100) min_precedes(all_49_0, all_63_0, tptp0) % 157.50/22.52 | | % 157.50/22.52 | | BETA: splitting (77) gives: % 157.50/22.52 | | % 157.50/22.52 | | Case 1: % 157.50/22.52 | | | % 157.50/22.52 | | | (101) atomic(all_65_0) % 157.50/22.52 | | | % 157.50/22.52 | | | REDUCE: (65), (101) imply: % 157.50/22.52 | | | (102) atomic(tptp0) % 157.50/22.52 | | | % 157.50/22.52 | | | PRED_UNIFY: (8), (102) imply: % 157.50/22.52 | | | (103) $false % 157.50/22.52 | | | % 157.50/22.52 | | | CLOSE: (103) is inconsistent. % 157.50/22.52 | | | % 157.50/22.52 | | Case 2: % 157.50/22.52 | | | % 157.50/22.52 | | | (104) ~ atomic(all_65_0) % 157.50/22.52 | | | (105) ? [v0: $i] : ($i(v0) & leaf_occ(all_51_0, v0) & % 157.50/22.52 | | | occurrence_of(v0, all_65_0)) % 157.50/22.52 | | | % 157.50/22.52 | | | DELTA: instantiating (105) with fresh symbol all_116_0 gives: % 157.50/22.52 | | | (106) $i(all_116_0) & leaf_occ(all_51_0, all_116_0) & % 157.50/22.52 | | | occurrence_of(all_116_0, all_65_0) % 157.50/22.52 | | | % 157.50/22.52 | | | ALPHA: (106) implies: % 157.50/22.52 | | | (107) occurrence_of(all_116_0, all_65_0) % 157.50/22.52 | | | (108) leaf_occ(all_51_0, all_116_0) % 157.50/22.52 | | | (109) $i(all_116_0) % 157.50/22.52 | | | % 157.50/22.52 | | | REDUCE: (65), (107) imply: % 157.50/22.52 | | | (110) occurrence_of(all_116_0, tptp0) % 157.50/22.52 | | | % 157.50/22.52 | | | BETA: splitting (64) gives: % 157.50/22.52 | | | % 157.50/22.52 | | | Case 1: % 157.50/22.52 | | | | % 157.50/22.52 | | | | (111) atomic(all_59_0) % 157.50/22.52 | | | | % 157.50/22.52 | | | | REDUCE: (83), (111) imply: % 157.50/22.52 | | | | (112) atomic(tptp0) % 157.50/22.52 | | | | % 157.50/22.52 | | | | PRED_UNIFY: (8), (112) imply: % 157.50/22.52 | | | | (113) $false % 157.50/22.52 | | | | % 157.50/22.52 | | | | CLOSE: (113) is inconsistent. % 157.50/22.52 | | | | % 157.50/22.52 | | | Case 2: % 157.50/22.52 | | | | % 157.50/22.52 | | | | (114) ~ atomic(all_59_0) % 157.50/22.52 | | | | (115) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_37_0) & % 157.50/22.52 | | | | root(v0, all_59_0)) % 157.50/22.52 | | | | % 157.50/22.52 | | | | DELTA: instantiating (115) with fresh symbol all_121_0 gives: % 157.87/22.52 | | | | (116) $i(all_121_0) & subactivity_occurrence(all_121_0, all_37_0) & % 157.87/22.52 | | | | root(all_121_0, all_59_0) % 157.87/22.52 | | | | % 157.87/22.52 | | | | ALPHA: (116) implies: % 157.87/22.53 | | | | (117) root(all_121_0, all_59_0) % 157.87/22.53 | | | | (118) subactivity_occurrence(all_121_0, all_37_0) % 157.87/22.53 | | | | (119) $i(all_121_0) % 157.87/22.53 | | | | % 157.87/22.53 | | | | REDUCE: (83), (117) imply: % 157.87/22.53 | | | | (120) root(all_121_0, tptp0) % 157.87/22.53 | | | | % 157.87/22.53 | | | | BETA: splitting (69) gives: % 157.87/22.53 | | | | % 157.87/22.53 | | | | Case 1: % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | (121) atomic(all_67_0) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | REDUCE: (84), (121) imply: % 157.87/22.53 | | | | | (122) atomic(tptp0) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | PRED_UNIFY: (8), (122) imply: % 157.87/22.53 | | | | | (123) $false % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | CLOSE: (123) is inconsistent. % 157.87/22.53 | | | | | % 157.87/22.53 | | | | Case 2: % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | (124) ~ atomic(all_67_0) % 157.87/22.53 | | | | | (125) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_37_0) % 157.87/22.53 | | | | | & root(v0, all_67_0)) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | DELTA: instantiating (125) with fresh symbol all_130_0 gives: % 157.87/22.53 | | | | | (126) $i(all_130_0) & subactivity_occurrence(all_130_0, all_37_0) & % 157.87/22.53 | | | | | root(all_130_0, all_67_0) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | ALPHA: (126) implies: % 157.87/22.53 | | | | | (127) root(all_130_0, all_67_0) % 157.87/22.53 | | | | | (128) subactivity_occurrence(all_130_0, all_37_0) % 157.87/22.53 | | | | | (129) $i(all_130_0) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | REDUCE: (84), (127) imply: % 157.87/22.53 | | | | | (130) root(all_130_0, tptp0) % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | BETA: splitting (66) gives: % 157.87/22.53 | | | | | % 157.87/22.53 | | | | | Case 1: % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | (131) atomic(all_65_0) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | REDUCE: (65), (131) imply: % 157.87/22.53 | | | | | | (132) atomic(tptp0) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | PRED_UNIFY: (8), (132) imply: % 157.87/22.53 | | | | | | (133) $false % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | CLOSE: (133) is inconsistent. % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | Case 2: % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | (134) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 157.87/22.53 | | | | | | all_37_0) & root(v0, all_65_0)) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | DELTA: instantiating (134) with fresh symbol all_135_0 gives: % 157.87/22.53 | | | | | | (135) $i(all_135_0) & subactivity_occurrence(all_135_0, all_37_0) % 157.87/22.53 | | | | | | & root(all_135_0, all_65_0) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | ALPHA: (135) implies: % 157.87/22.53 | | | | | | (136) root(all_135_0, all_65_0) % 157.87/22.53 | | | | | | (137) subactivity_occurrence(all_135_0, all_37_0) % 157.87/22.53 | | | | | | (138) $i(all_135_0) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | REDUCE: (65), (136) imply: % 157.87/22.53 | | | | | | (139) root(all_135_0, tptp0) % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | BETA: splitting (70) gives: % 157.87/22.53 | | | | | | % 157.87/22.53 | | | | | | Case 1: % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | (140) ~ occurrence_of(all_51_0, tptp1) % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | PRED_UNIFY: (52), (140) imply: % 157.87/22.53 | | | | | | | (141) ~ (all_63_0 = all_51_0) % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | PRED_UNIFY: (86), (140) imply: % 157.87/22.53 | | | | | | | (142) ~ (all_91_0 = tptp1) % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | GROUND_INST: instantiating (sos_08) with all_37_0, tptp0, % 157.87/22.53 | | | | | | | all_107_0, simplifying with (9), (23), (24), (96), % 157.87/22.53 | | | | | | | (98) gives: % 157.87/22.53 | | | | | | | (143) all_107_0 = tptp0 % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | GROUND_INST: instantiating (sos_08) with all_51_0, tptp3, % 157.87/22.53 | | | | | | | all_91_0, simplifying with (11), (34), (39), (86), % 157.87/22.53 | | | | | | | (87) gives: % 157.87/22.53 | | | | | | | (144) all_91_0 = tptp3 % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | GROUND_INST: instantiating (12) with all_116_0, simplifying with % 157.87/22.53 | | | | | | | (109), (110) gives: % 157.87/22.53 | | | | | | | (145) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & % 157.87/22.53 | | | | | | | next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_116_0) & % 157.87/22.53 | | | | | | | root_occ(v0, all_116_0) & occurrence_of(v1, tptp3) & % 157.87/22.53 | | | | | | | occurrence_of(v0, tptp4)) % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | GROUND_INST: instantiating (21) with tptp0, all_116_0, simplifying % 157.87/22.53 | | | | | | | with (9), (109), (110) gives: % 157.87/22.53 | | | | | | | (146) activity_occurrence(all_116_0) % 157.87/22.53 | | | | | | | % 157.87/22.53 | | | | | | | GROUND_INST: instantiating (sos) with tptp0, all_116_0, % 157.87/22.53 | | | | | | | simplifying with (8), (9), (109), (110) gives: % 157.87/22.54 | | | | | | | (147) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 157.87/22.54 | | | | | | | all_116_0) & root(v0, tptp0)) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (17) with all_121_0, all_37_0, tptp0, % 157.87/22.54 | | | | | | | simplifying with (9), (23), (24), (118), (119), (120) % 157.87/22.54 | | | | | | | gives: % 157.87/22.54 | | | | | | | (148) root_occ(all_121_0, all_37_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (17) with all_101_0, all_37_0, tptp0, % 157.87/22.54 | | | | | | | simplifying with (9), (23), (24), (92), (94) gives: % 157.87/22.54 | | | | | | | (149) ~ subactivity_occurrence(all_101_0, all_37_0) | % 157.87/22.54 | | | | | | | root_occ(all_101_0, all_37_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (17) with all_130_0, all_37_0, tptp0, % 157.87/22.54 | | | | | | | simplifying with (9), (23), (24), (128), (129), (130) % 157.87/22.54 | | | | | | | gives: % 157.87/22.54 | | | | | | | (150) root_occ(all_130_0, all_37_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (17) with all_135_0, all_37_0, tptp0, % 157.87/22.54 | | | | | | | simplifying with (9), (23), (24), (137), (138), (139) % 157.87/22.54 | | | | | | | gives: % 157.87/22.54 | | | | | | | (151) root_occ(all_135_0, all_37_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (18) with all_51_0, all_116_0, % 157.87/22.54 | | | | | | | simplifying with (39), (108), (109) gives: % 157.87/22.54 | | | | | | | (152) ? [v0: $i] : ($i(v0) & leaf(all_51_0, v0) & % 157.87/22.54 | | | | | | | subactivity_occurrence(all_51_0, all_116_0) & % 157.87/22.54 | | | | | | | occurrence_of(all_116_0, v0)) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_06) with tptp0, all_49_0, % 157.87/22.54 | | | | | | | all_63_0, simplifying with (9), (31), (54), (100) % 157.87/22.54 | | | | | | | gives: % 157.87/22.54 | | | | | | | (153) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_63_0, % 157.87/22.54 | | | | | | | v0) & subactivity_occurrence(all_49_0, v0) & % 157.87/22.54 | | | | | | | occurrence_of(v0, tptp0)) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_23) with all_49_0, all_63_0, % 157.87/22.54 | | | | | | | tptp0, simplifying with (9), (31), (54), (100) gives: % 157.87/22.54 | | | | | | | (154) ? [v0: $i] : ($i(v0) & min_precedes(v0, all_63_0, tptp0) % 157.87/22.54 | | | | | | | & root(v0, tptp0)) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_27) with all_101_0, all_51_0, % 157.87/22.54 | | | | | | | tptp0, all_37_0, simplifying with (9), (23), (24), % 157.87/22.54 | | | | | | | (39), (57), (93), (94) gives: % 157.87/22.54 | | | | | | | (155) subactivity_occurrence(all_101_0, all_37_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_37_0, % 157.87/22.54 | | | | | | | all_63_0, all_51_0, simplifying with (9), (23), (24), % 157.87/22.54 | | | | | | | (36), (39), (54), (78) gives: % 157.87/22.54 | | | | | | | (156) all_63_0 = all_51_0 | ~ subactivity_occurrence(all_63_0, % 157.87/22.54 | | | | | | | all_37_0) | min_precedes(all_63_0, all_51_0, tptp0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_02) with all_107_0, all_37_0, % 157.87/22.54 | | | | | | | all_63_0, all_51_0, simplifying with (24), (36), % 157.87/22.54 | | | | | | | (39), (54), (78), (96), (98) gives: % 157.87/22.54 | | | | | | | (157) all_63_0 = all_51_0 | ~ subactivity_occurrence(all_63_0, % 157.87/22.54 | | | | | | | all_37_0) | min_precedes(all_63_0, all_51_0, all_107_0) % 157.87/22.54 | | | | | | | % 157.87/22.54 | | | | | | | GROUND_INST: instantiating (sos_12) with all_63_0, simplifying % 157.87/22.54 | | | | | | | with (54), (71) gives: % 157.87/22.55 | | | | | | | (158) ? [v0: $i] : ($i(v0) & activity(v0) & % 157.87/22.55 | | | | | | | occurrence_of(all_63_0, v0)) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | GROUND_INST: instantiating (14) with all_49_0, all_51_0, tptp0, % 157.87/22.55 | | | | | | | all_63_0, simplifying with (9), (31), (39), (54), % 157.87/22.55 | | | | | | | (99), (100) gives: % 157.87/22.55 | | | | | | | (159) ~ min_precedes(all_63_0, all_51_0, tptp0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (158) with fresh symbol all_151_0 gives: % 157.87/22.55 | | | | | | | (160) $i(all_151_0) & activity(all_151_0) & % 157.87/22.55 | | | | | | | occurrence_of(all_63_0, all_151_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (160) implies: % 157.87/22.55 | | | | | | | (161) occurrence_of(all_63_0, all_151_0) % 157.87/22.55 | | | | | | | (162) $i(all_151_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (75) with fresh symbol all_161_0 gives: % 157.87/22.55 | | | | | | | (163) $i(all_161_0) & min_precedes(all_161_0, all_51_0, tptp0) % 157.87/22.55 | | | | | | | & root(all_161_0, tptp0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (163) implies: % 157.87/22.55 | | | | | | | (164) root(all_161_0, tptp0) % 157.87/22.55 | | | | | | | (165) min_precedes(all_161_0, all_51_0, tptp0) % 157.87/22.55 | | | | | | | (166) $i(all_161_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (147) with fresh symbol all_163_0 gives: % 157.87/22.55 | | | | | | | (167) $i(all_163_0) & subactivity_occurrence(all_163_0, % 157.87/22.55 | | | | | | | all_116_0) & root(all_163_0, tptp0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (167) implies: % 157.87/22.55 | | | | | | | (168) root(all_163_0, tptp0) % 157.87/22.55 | | | | | | | (169) subactivity_occurrence(all_163_0, all_116_0) % 157.87/22.55 | | | | | | | (170) $i(all_163_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (154) with fresh symbol all_169_0 gives: % 157.87/22.55 | | | | | | | (171) $i(all_169_0) & min_precedes(all_169_0, all_63_0, tptp0) % 157.87/22.55 | | | | | | | & root(all_169_0, tptp0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (171) implies: % 157.87/22.55 | | | | | | | (172) min_precedes(all_169_0, all_63_0, tptp0) % 157.87/22.55 | | | | | | | (173) $i(all_169_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (152) with fresh symbol all_173_0 gives: % 157.87/22.55 | | | | | | | (174) $i(all_173_0) & leaf(all_51_0, all_173_0) & % 157.87/22.55 | | | | | | | subactivity_occurrence(all_51_0, all_116_0) & % 157.87/22.55 | | | | | | | occurrence_of(all_116_0, all_173_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (174) implies: % 157.87/22.55 | | | | | | | (175) occurrence_of(all_116_0, all_173_0) % 157.87/22.55 | | | | | | | (176) subactivity_occurrence(all_51_0, all_116_0) % 157.87/22.55 | | | | | | | (177) $i(all_173_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (153) with fresh symbol all_177_0 gives: % 157.87/22.55 | | | | | | | (178) $i(all_177_0) & subactivity_occurrence(all_63_0, % 157.87/22.55 | | | | | | | all_177_0) & subactivity_occurrence(all_49_0, % 157.87/22.55 | | | | | | | all_177_0) & occurrence_of(all_177_0, tptp0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (178) implies: % 157.87/22.55 | | | | | | | (179) occurrence_of(all_177_0, tptp0) % 157.87/22.55 | | | | | | | (180) subactivity_occurrence(all_49_0, all_177_0) % 157.87/22.55 | | | | | | | (181) subactivity_occurrence(all_63_0, all_177_0) % 157.87/22.55 | | | | | | | (182) $i(all_177_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | DELTA: instantiating (145) with fresh symbols all_179_0, all_179_1 % 157.87/22.55 | | | | | | | gives: % 157.87/22.55 | | | | | | | (183) $i(all_179_0) & $i(all_179_1) & next_subocc(all_179_1, % 157.87/22.55 | | | | | | | all_179_0, tptp0) & leaf_occ(all_179_0, all_116_0) & % 157.87/22.55 | | | | | | | root_occ(all_179_1, all_116_0) & occurrence_of(all_179_0, % 157.87/22.55 | | | | | | | tptp3) & occurrence_of(all_179_1, tptp4) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | ALPHA: (183) implies: % 157.87/22.55 | | | | | | | (184) root_occ(all_179_1, all_116_0) % 157.87/22.55 | | | | | | | (185) leaf_occ(all_179_0, all_116_0) % 157.87/22.55 | | | | | | | (186) $i(all_179_1) % 157.87/22.55 | | | | | | | (187) $i(all_179_0) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | REDUCE: (142), (144) imply: % 157.87/22.55 | | | | | | | (188) ~ (tptp1 = tptp3) % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | BETA: splitting (149) gives: % 157.87/22.55 | | | | | | | % 157.87/22.55 | | | | | | | Case 1: % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | (189) ~ subactivity_occurrence(all_101_0, all_37_0) % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | PRED_UNIFY: (155), (189) imply: % 157.87/22.55 | | | | | | | | (190) $false % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | CLOSE: (190) is inconsistent. % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | Case 2: % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | (191) root_occ(all_101_0, all_37_0) % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | BETA: splitting (157) gives: % 157.87/22.55 | | | | | | | | % 157.87/22.55 | | | | | | | | Case 1: % 157.87/22.55 | | | | | | | | | % 157.87/22.55 | | | | | | | | | % 157.87/22.55 | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_63_0, tptp1, % 157.87/22.55 | | | | | | | | | all_151_0, simplifying with (5), (52), (54), % 157.87/22.55 | | | | | | | | | (161), (162) gives: % 157.87/22.55 | | | | | | | | | (192) all_151_0 = tptp1 % 157.87/22.55 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_116_0, tptp0, % 157.87/22.56 | | | | | | | | | all_173_0, simplifying with (9), (109), (110), % 157.87/22.56 | | | | | | | | | (175), (177) gives: % 157.87/22.56 | | | | | | | | | (193) all_173_0 = tptp0 % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (12) with all_177_0, simplifying % 157.87/22.56 | | | | | | | | | with (179), (182) gives: % 157.87/22.56 | | | | | | | | | (194) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & % 157.87/22.56 | | | | | | | | | next_subocc(v0, v1, tptp0) & leaf_occ(v1, % 157.87/22.56 | | | | | | | | | all_177_0) & root_occ(v0, all_177_0) & % 157.87/22.56 | | | | | | | | | occurrence_of(v1, tptp3) & occurrence_of(v0, % 157.87/22.56 | | | | | | | | | tptp4)) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_93_0, tptp1, % 157.87/22.56 | | | | | | | | | tptp3, simplifying with (5), (11), (89), (90) % 157.87/22.56 | | | | | | | | | gives: % 157.87/22.56 | | | | | | | | | (195) tptp1 = tptp3 | ~ occurrence_of(all_93_0, tptp3) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_63_0, all_151_0, % 157.87/22.56 | | | | | | | | | tptp3, simplifying with (11), (54), (161), (162) % 157.87/22.56 | | | | | | | | | gives: % 157.87/22.56 | | | | | | | | | (196) all_151_0 = tptp3 | ~ occurrence_of(all_63_0, tptp3) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (17) with all_49_0, all_177_0, % 157.87/22.56 | | | | | | | | | tptp0, simplifying with (9), (29), (31), (179), % 157.87/22.56 | | | | | | | | | (180), (182) gives: % 157.87/22.56 | | | | | | | | | (197) root_occ(all_49_0, all_177_0) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_101_0, all_51_0, % 157.87/22.56 | | | | | | | | | tptp0, all_116_0, simplifying with (9), (39), % 157.87/22.56 | | | | | | | | | (93), (94), (109), (110), (176) gives: % 157.87/22.56 | | | | | | | | | (198) subactivity_occurrence(all_101_0, all_116_0) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (17) with all_101_0, all_116_0, % 157.87/22.56 | | | | | | | | | tptp0, simplifying with (9), (92), (94), (109), % 157.87/22.56 | | | | | | | | | (110) gives: % 157.87/22.56 | | | | | | | | | (199) ~ subactivity_occurrence(all_101_0, all_116_0) | % 157.87/22.56 | | | | | | | | | root_occ(all_101_0, all_116_0) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (17) with all_163_0, all_116_0, % 157.87/22.56 | | | | | | | | | tptp0, simplifying with (9), (109), (110), (168), % 157.87/22.56 | | | | | | | | | (169), (170) gives: % 157.87/22.56 | | | | | | | | | (200) root_occ(all_163_0, all_116_0) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (17) with all_161_0, all_116_0, % 157.87/22.56 | | | | | | | | | tptp0, simplifying with (9), (109), (110), (164), % 157.87/22.56 | | | | | | | | | (166) gives: % 157.87/22.56 | | | | | | | | | (201) ~ subactivity_occurrence(all_161_0, all_116_0) | % 157.87/22.56 | | | | | | | | | root_occ(all_161_0, all_116_0) % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_49_0, all_130_0, % 157.87/22.56 | | | | | | | | | all_37_0, tptp0, simplifying with (9), (23), (24), % 157.87/22.56 | | | | | | | | | (31), (42), (129), (150) gives: % 157.87/22.56 | | | | | | | | | (202) all_130_0 = all_49_0 % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_101_0, all_130_0, % 157.87/22.56 | | | | | | | | | all_37_0, tptp0, simplifying with (9), (23), (24), % 157.87/22.56 | | | | | | | | | (94), (129), (150), (191) gives: % 157.87/22.56 | | | | | | | | | (203) all_130_0 = all_101_0 % 157.87/22.56 | | | | | | | | | % 157.87/22.56 | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_130_0, all_135_0, % 157.87/22.56 | | | | | | | | | all_37_0, tptp0, simplifying with (9), (23), (24), % 157.87/22.56 | | | | | | | | | (129), (138), (150), (151) gives: % 157.87/22.56 | | | | | | | | | (204) all_135_0 = all_130_0 % 157.87/22.56 | | | | | | | | | % 157.87/22.57 | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_121_0, all_135_0, % 157.87/22.57 | | | | | | | | | all_37_0, tptp0, simplifying with (9), (23), (24), % 157.87/22.57 | | | | | | | | | (119), (138), (148), (151) gives: % 157.87/22.57 | | | | | | | | | (205) all_135_0 = all_121_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | GROUND_INST: instantiating (16) with all_179_1, all_116_0, % 157.87/22.57 | | | | | | | | | simplifying with (109), (184), (186) gives: % 157.87/22.57 | | | | | | | | | (206) ? [v0: $i] : ($i(v0) & % 157.87/22.57 | | | | | | | | | subactivity_occurrence(all_179_1, all_116_0) & % 157.87/22.57 | | | | | | | | | root(all_179_1, v0) & occurrence_of(all_116_0, v0)) % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | GROUND_INST: instantiating (18) with all_179_0, all_116_0, % 157.87/22.57 | | | | | | | | | simplifying with (109), (185), (187) gives: % 157.87/22.57 | | | | | | | | | (207) ? [v0: $i] : ($i(v0) & leaf(all_179_0, v0) & % 157.87/22.57 | | | | | | | | | subactivity_occurrence(all_179_0, all_116_0) & % 157.87/22.57 | | | | | | | | | occurrence_of(all_116_0, v0)) % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | GROUND_INST: instantiating (sos_27) with all_161_0, all_51_0, % 157.87/22.57 | | | | | | | | | tptp0, all_116_0, simplifying with (9), (39), % 157.87/22.57 | | | | | | | | | (109), (110), (165), (166), (176) gives: % 157.87/22.57 | | | | | | | | | (208) subactivity_occurrence(all_161_0, all_116_0) % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | GROUND_INST: instantiating (sos_12) with all_116_0, simplifying % 157.87/22.57 | | | | | | | | | with (109), (146) gives: % 157.87/22.57 | | | | | | | | | (209) ? [v0: $i] : ($i(v0) & activity(v0) & % 157.87/22.57 | | | | | | | | | occurrence_of(all_116_0, v0)) % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | COMBINE_EQS: (204), (205) imply: % 157.87/22.57 | | | | | | | | | (210) all_130_0 = all_121_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | SIMP: (210) implies: % 157.87/22.57 | | | | | | | | | (211) all_130_0 = all_121_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | COMBINE_EQS: (202), (211) imply: % 157.87/22.57 | | | | | | | | | (212) all_121_0 = all_49_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | COMBINE_EQS: (203), (211) imply: % 157.87/22.57 | | | | | | | | | (213) all_121_0 = all_101_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | COMBINE_EQS: (212), (213) imply: % 157.87/22.57 | | | | | | | | | (214) all_101_0 = all_49_0 % 157.87/22.57 | | | | | | | | | % 157.87/22.57 | | | | | | | | | DELTA: instantiating (209) with fresh symbol all_217_0 gives: % 157.87/22.57 | | | | | | | | | (215) $i(all_217_0) & activity(all_217_0) & % 157.87/22.57 | | | | | | | | | occurrence_of(all_116_0, all_217_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | ALPHA: (215) implies: % 158.10/22.57 | | | | | | | | | (216) occurrence_of(all_116_0, all_217_0) % 158.10/22.57 | | | | | | | | | (217) $i(all_217_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | DELTA: instantiating (154) with fresh symbol all_227_0 gives: % 158.10/22.57 | | | | | | | | | (218) $i(all_227_0) & min_precedes(all_227_0, all_63_0, % 158.10/22.57 | | | | | | | | | tptp0) & root(all_227_0, tptp0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | ALPHA: (218) implies: % 158.10/22.57 | | | | | | | | | (219) min_precedes(all_227_0, all_63_0, tptp0) % 158.10/22.57 | | | | | | | | | (220) $i(all_227_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | DELTA: instantiating (206) with fresh symbol all_287_0 gives: % 158.10/22.57 | | | | | | | | | (221) $i(all_287_0) & subactivity_occurrence(all_179_1, % 158.10/22.57 | | | | | | | | | all_116_0) & root(all_179_1, all_287_0) & % 158.10/22.57 | | | | | | | | | occurrence_of(all_116_0, all_287_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | ALPHA: (221) implies: % 158.10/22.57 | | | | | | | | | (222) occurrence_of(all_116_0, all_287_0) % 158.10/22.57 | | | | | | | | | (223) $i(all_287_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | DELTA: instantiating (207) with fresh symbol all_289_0 gives: % 158.10/22.57 | | | | | | | | | (224) $i(all_289_0) & leaf(all_179_0, all_289_0) & % 158.10/22.57 | | | | | | | | | subactivity_occurrence(all_179_0, all_116_0) & % 158.10/22.57 | | | | | | | | | occurrence_of(all_116_0, all_289_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | ALPHA: (224) implies: % 158.10/22.57 | | | | | | | | | (225) occurrence_of(all_116_0, all_289_0) % 158.10/22.57 | | | | | | | | | (226) $i(all_289_0) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | DELTA: instantiating (194) with fresh symbols all_301_0, % 158.10/22.57 | | | | | | | | | all_301_1 gives: % 158.10/22.57 | | | | | | | | | (227) $i(all_301_0) & $i(all_301_1) & % 158.10/22.57 | | | | | | | | | next_subocc(all_301_1, all_301_0, tptp0) & % 158.10/22.57 | | | | | | | | | leaf_occ(all_301_0, all_177_0) & root_occ(all_301_1, % 158.10/22.57 | | | | | | | | | all_177_0) & occurrence_of(all_301_0, tptp3) & % 158.10/22.57 | | | | | | | | | occurrence_of(all_301_1, tptp4) % 158.10/22.57 | | | | | | | | | % 158.10/22.57 | | | | | | | | | ALPHA: (227) implies: % 158.10/22.57 | | | | | | | | | (228) occurrence_of(all_301_0, tptp3) % 158.10/22.57 | | | | | | | | | (229) root_occ(all_301_1, all_177_0) % 158.10/22.57 | | | | | | | | | (230) leaf_occ(all_301_0, all_177_0) % 158.10/22.57 | | | | | | | | | (231) next_subocc(all_301_1, all_301_0, tptp0) % 158.10/22.57 | | | | | | | | | (232) $i(all_301_1) % 158.10/22.58 | | | | | | | | | (233) $i(all_301_0) % 158.10/22.58 | | | | | | | | | % 158.10/22.58 | | | | | | | | | REDUCE: (198), (214) imply: % 158.10/22.58 | | | | | | | | | (234) subactivity_occurrence(all_49_0, all_116_0) % 158.10/22.58 | | | | | | | | | % 158.10/22.58 | | | | | | | | | BETA: splitting (199) gives: % 158.10/22.58 | | | | | | | | | % 158.10/22.58 | | | | | | | | | Case 1: % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | (235) ~ subactivity_occurrence(all_101_0, all_116_0) % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | REDUCE: (214), (235) imply: % 158.10/22.58 | | | | | | | | | | (236) ~ subactivity_occurrence(all_49_0, all_116_0) % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | PRED_UNIFY: (234), (236) imply: % 158.10/22.58 | | | | | | | | | | (237) $false % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | CLOSE: (237) is inconsistent. % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | Case 2: % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | (238) root_occ(all_101_0, all_116_0) % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | REDUCE: (214), (238) imply: % 158.10/22.58 | | | | | | | | | | (239) root_occ(all_49_0, all_116_0) % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | BETA: splitting (196) gives: % 158.10/22.58 | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | Case 1: % 158.10/22.58 | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | (240) ~ occurrence_of(all_63_0, tptp3) % 158.10/22.58 | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | BETA: splitting (201) gives: % 158.10/22.58 | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | Case 1: % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | (241) ~ subactivity_occurrence(all_161_0, all_116_0) % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | PRED_UNIFY: (208), (241) imply: % 158.10/22.58 | | | | | | | | | | | | (242) $false % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | CLOSE: (242) is inconsistent. % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | Case 2: % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | (243) root_occ(all_161_0, all_116_0) % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | BETA: splitting (195) gives: % 158.10/22.58 | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | Case 1: % 158.10/22.58 | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | PRED_UNIFY: (228), (240) imply: % 158.10/22.58 | | | | | | | | | | | | | (244) ~ (all_301_0 = all_63_0) % 158.10/22.58 | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | BETA: splitting (63) gives: % 158.10/22.58 | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | Case 1: % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_116_0, all_217_0, % 158.10/22.58 | | | | | | | | | | | | | | all_287_0, simplifying with (109), (216), (217), % 158.10/22.58 | | | | | | | | | | | | | | (222), (223) gives: % 158.10/22.58 | | | | | | | | | | | | | | (245) all_287_0 = all_217_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_116_0, tptp0, % 158.10/22.58 | | | | | | | | | | | | | | all_289_0, simplifying with (9), (109), (110), % 158.10/22.58 | | | | | | | | | | | | | | (225), (226) gives: % 158.10/22.58 | | | | | | | | | | | | | | (246) all_289_0 = tptp0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_08) with all_116_0, all_287_0, % 158.10/22.58 | | | | | | | | | | | | | | all_289_0, simplifying with (109), (222), (223), % 158.10/22.58 | | | | | | | | | | | | | | (225), (226) gives: % 158.10/22.58 | | | | | | | | | | | | | | (247) all_289_0 = all_287_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_179_1, all_49_0, % 158.10/22.58 | | | | | | | | | | | | | | all_116_0, all_217_0, simplifying with (31), % 158.10/22.58 | | | | | | | | | | | | | | (109), (184), (186), (216), (217), (239) gives: % 158.10/22.58 | | | | | | | | | | | | | | (248) all_179_1 = all_49_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_179_1, all_163_0, % 158.10/22.58 | | | | | | | | | | | | | | all_116_0, all_217_0, simplifying with (109), % 158.10/22.58 | | | | | | | | | | | | | | (170), (184), (186), (200), (216), (217) gives: % 158.10/22.58 | | | | | | | | | | | | | | (249) all_179_1 = all_163_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_161_0, all_163_0, % 158.10/22.58 | | | | | | | | | | | | | | all_116_0, all_217_0, simplifying with (109), % 158.10/22.58 | | | | | | | | | | | | | | (166), (170), (200), (216), (217), (243) gives: % 158.10/22.58 | | | | | | | | | | | | | | (250) all_163_0 = all_161_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_29) with all_49_0, all_301_1, % 158.10/22.58 | | | | | | | | | | | | | | all_177_0, tptp0, simplifying with (9), (31), % 158.10/22.58 | | | | | | | | | | | | | | (179), (182), (197), (229), (232) gives: % 158.10/22.58 | | | | | | | | | | | | | | (251) all_301_1 = all_49_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_177_0, % 158.10/22.58 | | | | | | | | | | | | | | all_63_0, all_301_0, simplifying with (9), (54), % 158.10/22.58 | | | | | | | | | | | | | | (78), (179), (181), (182), (230), (233) gives: % 158.10/22.58 | | | | | | | | | | | | | | (252) all_301_0 = all_63_0 | min_precedes(all_63_0, % 158.10/22.58 | | | | | | | | | | | | | | all_301_0, tptp0) % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (sos_01) with tptp0, all_177_0, % 158.10/22.58 | | | | | | | | | | | | | | all_63_0, all_227_0, all_301_0, simplifying with % 158.10/22.58 | | | | | | | | | | | | | | (9), (54), (179), (181), (182), (219), (220), % 158.10/22.58 | | | | | | | | | | | | | | (230), (233) gives: % 158.10/22.58 | | | | | | | | | | | | | | (253) all_301_0 = all_63_0 | ~ root_occ(all_227_0, % 158.10/22.58 | | | | | | | | | | | | | | all_177_0) | min_precedes(all_63_0, all_301_0, % 158.10/22.58 | | | | | | | | | | | | | | tptp0) % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | COMBINE_EQS: (246), (247) imply: % 158.10/22.58 | | | | | | | | | | | | | | (254) all_287_0 = tptp0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | SIMP: (254) implies: % 158.10/22.58 | | | | | | | | | | | | | | (255) all_287_0 = tptp0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | COMBINE_EQS: (245), (255) imply: % 158.10/22.58 | | | | | | | | | | | | | | (256) all_217_0 = tptp0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | SIMP: (256) implies: % 158.10/22.58 | | | | | | | | | | | | | | (257) all_217_0 = tptp0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | COMBINE_EQS: (248), (249) imply: % 158.10/22.58 | | | | | | | | | | | | | | (258) all_163_0 = all_49_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | SIMP: (258) implies: % 158.10/22.58 | | | | | | | | | | | | | | (259) all_163_0 = all_49_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | COMBINE_EQS: (250), (259) imply: % 158.10/22.58 | | | | | | | | | | | | | | (260) all_161_0 = all_49_0 % 158.10/22.58 | | | | | | | | | | | | | | % 158.10/22.58 | | | | | | | | | | | | | | SIMP: (260) implies: % 158.10/22.59 | | | | | | | | | | | | | | (261) all_161_0 = all_49_0 % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | REDUCE: (231), (251) imply: % 158.10/22.59 | | | | | | | | | | | | | | (262) next_subocc(all_49_0, all_301_0, tptp0) % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | BETA: splitting (253) gives: % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | Case 1: % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | (263) min_precedes(all_63_0, all_301_0, tptp0) % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | GROUND_INST: instantiating (14) with all_49_0, all_301_0, % 158.10/22.59 | | | | | | | | | | | | | | | tptp0, all_63_0, simplifying with (9), (31), (54), % 158.10/22.59 | | | | | | | | | | | | | | | (100), (233), (262), (263) gives: % 158.10/22.59 | | | | | | | | | | | | | | | (264) $false % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | CLOSE: (264) is inconsistent. % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | (265) ~ min_precedes(all_63_0, all_301_0, tptp0) % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | BETA: splitting (252) gives: % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | Case 1: % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | (266) min_precedes(all_63_0, all_301_0, tptp0) % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | PRED_UNIFY: (265), (266) imply: % 158.10/22.59 | | | | | | | | | | | | | | | | (267) $false % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | CLOSE: (267) is inconsistent. % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | (268) all_301_0 = all_63_0 % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | REDUCE: (244), (268) imply: % 158.10/22.59 | | | | | | | | | | | | | | | | (269) $false % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | | CLOSE: (269) is inconsistent. % 158.10/22.59 | | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | (270) arboreal(all_37_0) % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (20) with all_37_0, tptp0, % 158.10/22.59 | | | | | | | | | | | | | | simplifying with (8), (9), (23), (24), (270) % 158.10/22.59 | | | | | | | | | | | | | | gives: % 158.10/22.59 | | | | | | | | | | | | | | (271) $false % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | | CLOSE: (271) is inconsistent. % 158.10/22.59 | | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | (272) tptp1 = tptp3 % 158.10/22.59 | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | REDUCE: (3), (272) imply: % 158.10/22.59 | | | | | | | | | | | | | (273) $false % 158.10/22.59 | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | | CLOSE: (273) is inconsistent. % 158.10/22.59 | | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | (274) all_151_0 = tptp3 % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | COMBINE_EQS: (192), (274) imply: % 158.10/22.59 | | | | | | | | | | | (275) tptp1 = tptp3 % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | REDUCE: (3), (275) imply: % 158.10/22.59 | | | | | | | | | | | (276) $false % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | CLOSE: (276) is inconsistent. % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | % 158.10/22.59 | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | % 158.10/22.59 | | | | | | | | | (277) subactivity_occurrence(all_63_0, all_37_0) % 158.10/22.59 | | | | | | | | | % 158.10/22.59 | | | | | | | | | BETA: splitting (156) gives: % 158.10/22.59 | | | | | | | | | % 158.10/22.59 | | | | | | | | | Case 1: % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | (278) min_precedes(all_63_0, all_51_0, tptp0) % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | PRED_UNIFY: (159), (278) imply: % 158.10/22.59 | | | | | | | | | | (279) $false % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | CLOSE: (279) is inconsistent. % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | (280) all_63_0 = all_51_0 | ~ % 158.10/22.59 | | | | | | | | | | subactivity_occurrence(all_63_0, all_37_0) % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | BETA: splitting (280) gives: % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | Case 1: % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | (281) ~ subactivity_occurrence(all_63_0, all_37_0) % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | PRED_UNIFY: (277), (281) imply: % 158.10/22.59 | | | | | | | | | | | (282) $false % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | CLOSE: (282) is inconsistent. % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | Case 2: % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | (283) all_63_0 = all_51_0 % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | REDUCE: (141), (283) imply: % 158.10/22.59 | | | | | | | | | | | (284) $false % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | | CLOSE: (284) is inconsistent. % 158.10/22.59 | | | | | | | | | | | % 158.10/22.59 | | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | | % 158.10/22.59 | | | | | | | | | End of split % 158.10/22.59 | | | | | | | | | % 158.10/22.59 | | | | | | | | End of split % 158.10/22.59 | | | | | | | | % 158.10/22.59 | | | | | | | End of split % 158.10/22.59 | | | | | | | % 158.10/22.59 | | | | | | Case 2: % 158.10/22.59 | | | | | | | % 158.10/22.59 | | | | | | | (285) tptp1 = tptp3 % 158.10/22.59 | | | | | | | % 158.10/22.59 | | | | | | | REDUCE: (3), (285) imply: % 158.10/22.59 | | | | | | | (286) $false % 158.10/22.59 | | | | | | | % 158.10/22.59 | | | | | | | CLOSE: (286) is inconsistent. % 158.10/22.59 | | | | | | | % 158.10/22.59 | | | | | | End of split % 158.10/22.59 | | | | | | % 158.10/22.59 | | | | | End of split % 158.10/22.59 | | | | | % 158.10/22.59 | | | | End of split % 158.10/22.59 | | | | % 158.10/22.59 | | | End of split % 158.10/22.59 | | | % 158.10/22.59 | | End of split % 158.10/22.59 | | % 158.10/22.59 | Case 2: % 158.10/22.59 | | % 158.10/22.59 | | (287) tptp3 = tptp4 % 158.10/22.59 | | % 158.10/22.59 | | REDUCE: (4), (287) imply: % 158.10/22.59 | | (288) $false % 158.10/22.59 | | % 158.10/22.59 | | CLOSE: (288) is inconsistent. % 158.10/22.59 | | % 158.10/22.59 | End of split % 158.10/22.59 | % 158.10/22.59 End of proof % 158.10/22.59 % SZS output end Proof for theBenchmark % 158.10/22.59 % 158.10/22.59 22002ms %------------------------------------------------------------------------------