%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO002+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 : n028.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 94.04s 13.04s % Output : Proof 94.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PRO002+2 : TPTP v8.1.2. Released v4.0.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Aug 28 19:47:40 EDT 2023 % 0.12/0.33 % CPUTime : % 0.49/0.61 ________ _____ % 0.49/0.61 ___ __ \_________(_)________________________________ % 0.49/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.49/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.49/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.49/0.61 % 0.49/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.49/0.61 (2023-06-19) % 0.49/0.61 % 0.49/0.61 (c) Philipp Rümmer, 2009-2023 % 0.49/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.49/0.61 Amanda Stjerna. % 0.49/0.61 Free software under BSD-3-Clause. % 0.49/0.61 % 0.49/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.49/0.61 % 0.49/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.49/0.63 Running up to 7 provers in parallel. % 0.49/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.49/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.49/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.49/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.49/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.49/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.49/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.91/1.20 Prover 4: Preprocessing ... % 2.91/1.20 Prover 1: Preprocessing ... % 3.14/1.24 Prover 2: Preprocessing ... % 3.14/1.24 Prover 6: Preprocessing ... % 3.14/1.24 Prover 5: Preprocessing ... % 3.14/1.24 Prover 3: Preprocessing ... % 3.14/1.24 Prover 0: Preprocessing ... % 7.12/1.72 Prover 5: Proving ... % 7.12/1.74 Prover 2: Constructing countermodel ... % 7.49/1.88 Prover 1: Constructing countermodel ... % 8.49/1.94 Prover 6: Proving ... % 8.92/1.96 Prover 3: Constructing countermodel ... % 9.55/2.10 Prover 4: Constructing countermodel ... % 9.55/2.13 Prover 0: Proving ... % 73.05/10.33 Prover 2: stopped % 73.05/10.35 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 73.52/10.40 Prover 7: Preprocessing ... % 73.52/10.46 Prover 7: Constructing countermodel ... % 93.46/13.02 Prover 7: Found proof (size 298) % 93.46/13.02 Prover 7: proved (2674ms) % 93.46/13.02 Prover 5: stopped % 93.46/13.02 Prover 1: stopped % 93.46/13.02 Prover 3: stopped % 93.46/13.03 Prover 4: stopped % 93.46/13.03 Prover 6: stopped % 94.04/13.04 Prover 0: stopped % 94.04/13.04 % 94.04/13.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 94.04/13.04 % 94.04/13.06 % SZS output start Proof for theBenchmark % 94.04/13.07 Assumptions after simplification: % 94.04/13.07 --------------------------------- % 94.04/13.07 % 94.04/13.07 (goals) % 94.04/13.07 $i(tptp0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 94.04/13.07 $i(v0) & tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 94.04/13.07 % 94.04/13.07 (sos_02) % 94.04/13.07 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 94.04/13.07 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 94.04/13.07 v2) | ~ occurrence_of(v2, v3)) % 94.04/13.07 % 94.04/13.07 (sos_03) % 94.04/13.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 94.04/13.08 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, % 94.04/13.08 v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 94.04/13.08 % 94.04/13.08 (sos_04) % 94.04/13.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 94.04/13.08 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 94.04/13.08 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 94.04/13.08 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 94.04/13.08 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 94.04/13.08 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 94.04/13.08 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 94.04/13.08 min_precedes(v0, v3, v2))) % 94.04/13.08 % 94.04/13.08 (sos_05) % 94.04/13.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.08 ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0: $i] : ! [v1: $i] : ! % 94.04/13.08 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 94.04/13.08 arboreal(v0)) % 94.04/13.08 % 94.04/13.08 (sos_10) % 94.04/13.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.08 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 94.04/13.08 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 94.04/13.08 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 94.04/13.08 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 94.04/13.08 % 94.04/13.08 (sos_11) % 94.04/13.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.09 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 94.04/13.09 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 94.04/13.09 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 94.04/13.09 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 94.04/13.09 % 94.04/13.09 (sos_12) % 94.04/13.09 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | % 94.04/13.09 legal(v0)) % 94.04/13.09 % 94.04/13.09 (sos_14) % 94.04/13.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.09 ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0: $i] : ! [v1: $i] : % 94.04/13.09 ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v2, v0, v1) % 94.04/13.09 | leaf(v0, v1) | ? [v3: $i] : ($i(v3) & min_precedes(v0, v3, v1))) & ! % 94.04/13.09 [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | root(v0, % 94.04/13.09 v1) | ? [v2: $i] : ($i(v2) & min_precedes(v2, v0, v1))) & ! [v0: $i] : % 94.04/13.09 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | leaf(v0, v1) | ? [v2: % 94.04/13.09 $i] : ($i(v2) & min_precedes(v0, v2, v1))) % 94.04/13.09 % 94.04/13.09 (sos_15) % 94.04/13.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.09 ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | % 94.04/13.09 atocc(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.04/13.09 atocc(v0, v1) | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 94.04/13.09 occurrence_of(v0, v2))) % 94.04/13.09 % 94.04/13.09 (sos_16) % 94.04/13.10 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) | ~ % 94.04/13.10 legal(v0) | root(v0, v1)) % 94.04/13.10 % 94.04/13.10 (sos_17) % 94.04/13.10 ! [v0: $i] : ( ~ $i(v0) | ~ legal(v0) | arboreal(v0)) % 94.04/13.10 % 94.04/13.10 (sos_18) % 94.04/13.10 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 94.04/13.10 & activity(v1) & occurrence_of(v0, v1))) % 94.04/13.10 % 94.04/13.10 (sos_19) % 94.04/13.10 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.04/13.10 subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0: $i] : ! % 94.04/13.10 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v0, v1) | % 94.04/13.10 activity_occurrence(v0)) % 94.04/13.10 % 94.04/13.10 (sos_22) % 94.04/13.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 94.04/13.10 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 94.04/13.10 % 94.04/13.10 (sos_24) % 94.04/13.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.04/13.10 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 94.04/13.10 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 94.04/13.10 occurrence_of(v3, v0))) % 94.04/13.10 % 94.04/13.10 (sos_26) % 94.21/13.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.21/13.10 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ? [v4: $i] : ($i(v4) & $i(v3) & % 94.21/13.10 subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, % 94.21/13.10 v3))) % 94.21/13.10 % 94.21/13.10 (sos_27) % 94.21/13.10 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v1, v0) | ? [v2: % 94.21/13.10 $i] : ($i(v2) & subactivity(v2, v0) & atocc(v1, v2))) % 94.21/13.10 % 94.21/13.10 (sos_28) % 94.21/13.11 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 94.21/13.11 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v3, v1) | ~ % 94.21/13.11 subactivity_occurrence(v2, v1) | ~ arboreal(v3) | ~ arboreal(v2) | ~ % 94.21/13.11 occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 94.21/13.11 % 94.21/13.11 (sos_29) % 94.21/13.11 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 94.21/13.11 | activity(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.11 occurrence_of(v1, v0) | activity_occurrence(v1)) % 94.21/13.11 % 94.21/13.11 (sos_30) % 94.21/13.11 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 94.21/13.11 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 94.21/13.11 root(v2, v0))) % 94.21/13.11 % 94.21/13.11 (sos_31) % 94.21/13.11 ! [v0: $i] : ( ~ $i(v0) | ~ activity(v0) | subactivity(v0, v0)) % 94.21/13.11 % 94.21/13.11 (sos_32) % 94.21/13.11 $i(tptp2) & $i(tptp3) & $i(tptp4) & $i(tptp0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 94.21/13.11 occurrence_of(v0, tptp0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 94.21/13.11 next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & % 94.21/13.11 occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, % 94.21/13.11 tptp3)))) % 94.21/13.11 % 94.21/13.11 (sos_34) % 94.21/13.11 $i(tptp0) & ~ atomic(tptp0) % 94.21/13.11 % 94.21/13.11 (sos_45) % 94.21/13.11 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 94.21/13.11 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, % 94.21/13.11 v1, v2, v3, v4) | activity(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 94.21/13.11 : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 94.21/13.11 ~ $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0: % 94.21/13.11 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | % 94.21/13.11 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, v1, v2, % 94.21/13.11 v3, v4) | root(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 94.21/13.11 [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.11 $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 94.21/13.11 % 94.21/13.11 (sos_46) % 94.21/13.12 $i(tptp2) & $i(tptp3) & $i(tptp4) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 94.21/13.12 ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.12 send_message(tptp2, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 94.21/13.12 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.12 send_message(tptp3, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 94.21/13.12 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.12 send_message(tptp4, v0, v1, v2, v3)) % 94.21/13.12 % 94.21/13.12 (sos_47) % 94.21/13.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 94.21/13.12 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 94.21/13.12 | ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | % 94.21/13.12 min_precedes(v3, v5, v4)) % 94.21/13.12 % 94.21/13.12 (sos_48) % 94.21/13.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 94.21/13.12 ~ tptp1(v0, v1, v2) | ~ atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 94.21/13.12 $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ % 94.21/13.12 atomic(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ % 94.21/13.12 $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | activity(v0)) & ! [v0: $i] : ! % 94.21/13.12 [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, % 94.21/13.12 v2) | root(v2, v1)) % 94.21/13.12 % 94.21/13.12 (sos_49) % 94.21/13.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 94.21/13.12 | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | % 94.21/13.12 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & % 94.21/13.12 $i(v5) & $i(v4) & send_message(v4, v5, v6, v2, v1) & root_occ(v7, v3) & % 94.21/13.12 occurrence_of(v7, v4))) % 94.21/13.12 % 94.21/13.12 Further assumptions not needed in the proof: % 94.21/13.12 -------------------------------------------- % 94.21/13.12 sos, sos_01, sos_06, sos_07, sos_08, sos_09, sos_13, sos_20, sos_21, sos_23, % 94.21/13.12 sos_25, sos_33, sos_35, sos_36, sos_37, sos_38, sos_39, sos_40, sos_41, sos_42, % 94.21/13.12 sos_43, sos_44, sos_50 % 94.21/13.12 % 94.21/13.12 Those formulas are unsatisfiable: % 94.21/13.12 --------------------------------- % 94.21/13.12 % 94.21/13.12 Begin of proof % 94.21/13.12 | % 94.21/13.12 | ALPHA: (goals) implies: % 94.21/13.12 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 94.21/13.12 | tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 94.21/13.12 | % 94.21/13.12 | ALPHA: (sos_48) implies: % 94.21/13.12 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.12 | $i(v0) | ~ tptp1(v0, v1, v2) | root(v2, v1)) % 94.21/13.12 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.12 | $i(v0) | ~ tptp1(v0, v1, v2) | ~ atomic(v0)) % 94.21/13.12 | % 94.21/13.12 | ALPHA: (sos_46) implies: % 94.21/13.13 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 94.21/13.13 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp3, v0, v1, v2, % 94.21/13.13 | v3)) % 94.21/13.13 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 94.21/13.13 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp2, v0, v1, v2, % 94.21/13.13 | v3)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_45) implies: % 94.21/13.13 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 94.21/13.13 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 94.21/13.13 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 94.21/13.13 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | send_message(v0, v1, v2, v3, v4) | root(v1, v2)) % 94.21/13.13 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 94.21/13.13 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | send_message(v0, v1, v2, v3, v4) | activity(v0)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_34) implies: % 94.21/13.13 | (9) ~ atomic(tptp0) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_32) implies: % 94.21/13.13 | (10) $i(tptp0) % 94.21/13.13 | (11) $i(tptp3) % 94.21/13.13 | (12) $i(tptp2) % 94.21/13.13 | (13) ! [v0: $i] : ( ~ $i(v0) | ~ occurrence_of(v0, tptp0) | ? [v1: $i] : % 94.21/13.13 | ? [v2: $i] : ($i(v2) & $i(v1) & next_subocc(v1, v2, tptp0) & % 94.21/13.13 | leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & % 94.21/13.13 | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_29) implies: % 94.21/13.13 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_19) implies: % 94.21/13.13 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 94.21/13.13 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 94.21/13.13 | subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_15) implies: % 94.21/13.13 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) % 94.21/13.13 | | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 94.21/13.13 | occurrence_of(v0, v2))) % 94.21/13.13 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.13 | $i(v0) | ~ subactivity(v1, v2) | ~ atomic(v2) | ~ % 94.21/13.13 | occurrence_of(v0, v2) | atocc(v0, v1)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_14) implies: % 94.21/13.13 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.13 | $i(v0) | ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3: $i] : % 94.21/13.13 | ($i(v3) & min_precedes(v0, v3, v1))) % 94.21/13.13 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.13 | $i(v0) | ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 94.21/13.13 | % 94.21/13.13 | ALPHA: (sos_11) implies: % 94.21/13.14 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 94.21/13.14 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 94.21/13.14 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 94.21/13.14 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.14 | $i(v0) | ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ % 94.21/13.14 | occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 94.21/13.14 | % 94.21/13.14 | ALPHA: (sos_10) implies: % 94.21/13.14 | (23) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 94.21/13.14 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 94.21/13.14 | root(v0, v2) & occurrence_of(v1, v2))) % 94.21/13.14 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.14 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 94.21/13.14 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 94.21/13.14 | % 94.21/13.14 | ALPHA: (sos_05) implies: % 94.21/13.14 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 94.21/13.14 | $i(v0) | ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 94.21/13.14 | % 94.21/13.14 | ALPHA: (sos_04) implies: % 94.21/13.14 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 94.21/13.14 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 94.21/13.14 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 94.21/13.14 | % 94.21/13.14 | DELTA: instantiating (1) with fresh symbols all_42_0, all_42_1, all_42_2 % 94.21/13.14 | gives: % 94.21/13.14 | (27) $i(all_42_0) & $i(all_42_1) & $i(all_42_2) & tptp1(all_42_2, tptp0, % 94.21/13.14 | all_42_1) & occurrence_of(all_42_0, all_42_2) % 94.21/13.14 | % 94.21/13.14 | ALPHA: (27) implies: % 94.21/13.14 | (28) occurrence_of(all_42_0, all_42_2) % 94.21/13.14 | (29) tptp1(all_42_2, tptp0, all_42_1) % 94.21/13.14 | (30) $i(all_42_2) % 94.21/13.14 | (31) $i(all_42_1) % 94.21/13.14 | (32) $i(all_42_0) % 94.21/13.14 | % 94.21/13.14 | GROUND_INST: instantiating (14) with all_42_2, all_42_0, simplifying with % 94.21/13.14 | (28), (30), (32) gives: % 94.21/13.14 | (33) activity_occurrence(all_42_0) % 94.21/13.14 | % 94.21/13.14 | GROUND_INST: instantiating (sos_30) with all_42_2, all_42_0, simplifying with % 94.21/13.14 | (28), (30), (32) gives: % 94.21/13.14 | (34) atomic(all_42_2) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 94.21/13.14 | all_42_0) & root(v0, all_42_2)) % 94.21/13.14 | % 94.21/13.14 | GROUND_INST: instantiating (sos_49) with all_42_2, tptp0, all_42_1, all_42_0, % 94.21/13.14 | simplifying with (10), (28), (29), (30), (31), (32) gives: % 94.21/13.14 | (35) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ($i(v3) & % 94.21/13.14 | $i(v2) & $i(v1) & $i(v0) & send_message(v0, v1, v2, all_42_1, tptp0) % 94.21/13.14 | & root_occ(v3, all_42_0) & occurrence_of(v3, v0)) % 94.21/13.14 | % 94.21/13.14 | GROUND_INST: instantiating (2) with all_42_2, tptp0, all_42_1, simplifying % 94.21/13.14 | with (10), (29), (30), (31) gives: % 94.21/13.14 | (36) root(all_42_1, tptp0) % 94.21/13.14 | % 94.21/13.14 | DELTA: instantiating (35) with fresh symbols all_54_0, all_54_1, all_54_2, % 94.21/13.14 | all_54_3 gives: % 94.21/13.14 | (37) $i(all_54_0) & $i(all_54_1) & $i(all_54_2) & $i(all_54_3) & % 94.21/13.14 | send_message(all_54_3, all_54_2, all_54_1, all_42_1, tptp0) & % 94.21/13.14 | root_occ(all_54_0, all_42_0) & occurrence_of(all_54_0, all_54_3) % 94.21/13.14 | % 94.21/13.14 | ALPHA: (37) implies: % 94.21/13.15 | (38) occurrence_of(all_54_0, all_54_3) % 94.21/13.15 | (39) root_occ(all_54_0, all_42_0) % 94.21/13.15 | (40) send_message(all_54_3, all_54_2, all_54_1, all_42_1, tptp0) % 94.21/13.15 | (41) $i(all_54_3) % 94.21/13.15 | (42) $i(all_54_2) % 94.21/13.15 | (43) $i(all_54_1) % 94.21/13.15 | (44) $i(all_54_0) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (14) with all_54_3, all_54_0, simplifying with % 94.21/13.15 | (38), (41), (44) gives: % 94.21/13.15 | (45) activity_occurrence(all_54_0) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (23) with all_54_0, all_42_0, simplifying with % 94.21/13.15 | (32), (39), (44) gives: % 94.21/13.15 | (46) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_54_0, all_42_0) & % 94.21/13.15 | root(all_54_0, v0) & occurrence_of(all_42_0, v0)) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (sos_18) with all_42_0, simplifying with (32), (33) % 94.21/13.15 | gives: % 94.21/13.15 | (47) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_42_0, v0)) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (sos_47) with all_54_3, all_54_2, all_54_1, % 94.21/13.15 | all_42_1, tptp0, all_54_0, simplifying with (10), (31), (38), % 94.21/13.15 | (40), (41), (42), (43), (44) gives: % 94.21/13.15 | (48) min_precedes(all_42_1, all_54_0, tptp0) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (5) with all_54_2, all_54_1, all_42_1, tptp0, % 94.21/13.15 | simplifying with (10), (31), (42), (43) gives: % 94.21/13.15 | (49) ~ send_message(tptp2, all_54_2, all_54_1, all_42_1, tptp0) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (4) with all_54_2, all_54_1, all_42_1, tptp0, % 94.21/13.15 | simplifying with (10), (31), (42), (43) gives: % 94.21/13.15 | (50) ~ send_message(tptp3, all_54_2, all_54_1, all_42_1, tptp0) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (8) with all_54_3, all_54_2, all_54_1, all_42_1, % 94.21/13.15 | tptp0, simplifying with (10), (31), (40), (41), (42), (43) gives: % 94.21/13.15 | (51) activity(all_54_3) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (7) with all_54_3, all_54_2, all_54_1, all_42_1, % 94.21/13.15 | tptp0, simplifying with (10), (31), (40), (41), (42), (43) gives: % 94.21/13.15 | (52) root(all_54_2, all_54_1) % 94.21/13.15 | % 94.21/13.15 | GROUND_INST: instantiating (6) with all_54_3, all_54_2, all_54_1, all_42_1, % 94.21/13.15 | tptp0, simplifying with (10), (31), (40), (41), (42), (43) gives: % 94.21/13.15 | (53) atomic(all_54_3) % 94.21/13.15 | % 94.21/13.15 | DELTA: instantiating (47) with fresh symbol all_68_0 gives: % 94.21/13.15 | (54) $i(all_68_0) & activity(all_68_0) & occurrence_of(all_42_0, all_68_0) % 94.21/13.15 | % 94.21/13.15 | ALPHA: (54) implies: % 94.21/13.15 | (55) occurrence_of(all_42_0, all_68_0) % 94.21/13.15 | (56) $i(all_68_0) % 94.21/13.15 | % 94.21/13.15 | DELTA: instantiating (46) with fresh symbol all_70_0 gives: % 94.21/13.15 | (57) $i(all_70_0) & subactivity_occurrence(all_54_0, all_42_0) & % 94.21/13.15 | root(all_54_0, all_70_0) & occurrence_of(all_42_0, all_70_0) % 94.21/13.15 | % 94.21/13.15 | ALPHA: (57) implies: % 94.21/13.15 | (58) occurrence_of(all_42_0, all_70_0) % 94.21/13.15 | (59) root(all_54_0, all_70_0) % 94.21/13.15 | (60) $i(all_70_0) % 94.21/13.15 | % 94.21/13.15 | PRED_UNIFY: (40), (50) imply: % 94.21/13.15 | (61) ~ (all_54_3 = tptp3) % 94.21/13.15 | % 94.21/13.15 | PRED_UNIFY: (40), (49) imply: % 94.21/13.15 | (62) ~ (all_54_3 = tptp2) % 94.21/13.15 | % 94.21/13.16 | GROUND_INST: instantiating (19) with all_54_0, tptp0, all_42_1, simplifying % 94.21/13.16 | with (10), (31), (44), (48) gives: % 94.21/13.16 | (63) leaf(all_54_0, tptp0) | ? [v0: $i] : ($i(v0) & min_precedes(all_54_0, % 94.21/13.16 | v0, tptp0)) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_26) with tptp0, all_42_1, all_54_0, % 94.21/13.16 | simplifying with (10), (31), (44), (48) gives: % 94.21/13.16 | (64) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & subactivity(v1, tptp0) % 94.21/13.16 | & subactivity(v0, tptp0) & atocc(all_54_0, v1) & atocc(all_42_1, % 94.21/13.16 | v0)) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_24) with tptp0, all_42_1, all_54_0, % 94.21/13.16 | simplifying with (10), (31), (44), (48) gives: % 94.21/13.16 | (65) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_54_0, v0) & % 94.21/13.16 | subactivity_occurrence(all_42_1, v0) & occurrence_of(v0, tptp0)) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_30) with all_68_0, all_42_0, simplifying with % 94.21/13.16 | (32), (55), (56) gives: % 94.21/13.16 | (66) atomic(all_68_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 94.21/13.16 | all_42_0) & root(v0, all_68_0)) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_22) with all_42_0, all_42_2, all_70_0, % 94.21/13.16 | simplifying with (28), (30), (32), (58), (60) gives: % 94.21/13.16 | (67) all_70_0 = all_42_2 % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_22) with all_42_0, all_54_3, all_70_0, % 94.21/13.16 | simplifying with (32), (41), (58), (60) gives: % 94.21/13.16 | (68) all_70_0 = all_54_3 | ~ occurrence_of(all_42_0, all_54_3) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_22) with all_42_0, all_68_0, all_70_0, % 94.21/13.16 | simplifying with (32), (55), (56), (58), (60) gives: % 94.21/13.16 | (69) all_70_0 = all_68_0 % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (sos_30) with all_70_0, all_42_0, simplifying with % 94.21/13.16 | (32), (58), (60) gives: % 94.21/13.16 | (70) atomic(all_70_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 94.21/13.16 | all_42_0) & root(v0, all_70_0)) % 94.21/13.16 | % 94.21/13.16 | GROUND_INST: instantiating (3) with all_42_2, tptp0, all_42_1, simplifying % 94.21/13.16 | with (10), (29), (30), (31) gives: % 94.21/13.16 | (71) ~ atomic(all_42_2) % 94.21/13.16 | % 94.48/13.16 | GROUND_INST: instantiating (sos_27) with all_54_1, all_54_2, simplifying with % 94.48/13.16 | (42), (43), (52) gives: % 94.48/13.16 | (72) ? [v0: $i] : ($i(v0) & subactivity(v0, all_54_1) & atocc(all_54_2, % 94.48/13.16 | v0)) % 94.48/13.16 | % 94.48/13.16 | GROUND_INST: instantiating (sos_27) with all_70_0, all_54_0, simplifying with % 94.48/13.16 | (44), (59), (60) gives: % 94.48/13.16 | (73) ? [v0: $i] : ($i(v0) & subactivity(v0, all_70_0) & atocc(all_54_0, % 94.48/13.16 | v0)) % 94.48/13.16 | % 94.48/13.16 | GROUND_INST: instantiating (sos_12) with all_54_0, all_70_0, simplifying with % 94.48/13.16 | (44), (59), (60) gives: % 94.48/13.16 | (74) legal(all_54_0) % 94.48/13.16 | % 94.48/13.16 | GROUND_INST: instantiating (sos_18) with all_54_0, simplifying with (44), (45) % 94.48/13.16 | gives: % 94.48/13.16 | (75) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.16 | % 94.48/13.17 | GROUND_INST: instantiating (sos_31) with all_54_3, simplifying with (41), (51) % 94.48/13.17 | gives: % 94.48/13.17 | (76) subactivity(all_54_3, all_54_3) % 94.48/13.17 | % 94.48/13.17 | COMBINE_EQS: (67), (69) imply: % 94.48/13.17 | (77) all_68_0 = all_42_2 % 94.48/13.17 | % 94.48/13.17 | DELTA: instantiating (73) with fresh symbol all_82_0 gives: % 94.48/13.17 | (78) $i(all_82_0) & subactivity(all_82_0, all_70_0) & atocc(all_54_0, % 94.48/13.17 | all_82_0) % 94.48/13.17 | % 94.48/13.17 | ALPHA: (78) implies: % 94.48/13.17 | (79) atocc(all_54_0, all_82_0) % 94.48/13.17 | (80) $i(all_82_0) % 94.48/13.17 | % 94.48/13.17 | DELTA: instantiating (75) with fresh symbol all_84_0 gives: % 94.48/13.17 | (81) $i(all_84_0) & activity(all_84_0) & occurrence_of(all_54_0, all_84_0) % 94.48/13.17 | % 94.48/13.17 | ALPHA: (81) implies: % 94.48/13.17 | (82) occurrence_of(all_54_0, all_84_0) % 94.48/13.17 | (83) $i(all_84_0) % 94.48/13.17 | % 94.48/13.17 | DELTA: instantiating (72) with fresh symbol all_86_0 gives: % 94.48/13.17 | (84) $i(all_86_0) & subactivity(all_86_0, all_54_1) & atocc(all_54_2, % 94.48/13.17 | all_86_0) % 94.48/13.17 | % 94.48/13.17 | ALPHA: (84) implies: % 94.48/13.17 | (85) atocc(all_54_2, all_86_0) % 94.48/13.17 | (86) $i(all_86_0) % 94.48/13.17 | % 94.48/13.17 | DELTA: instantiating (65) with fresh symbol all_88_0 gives: % 94.48/13.17 | (87) $i(all_88_0) & subactivity_occurrence(all_54_0, all_88_0) & % 94.48/13.17 | subactivity_occurrence(all_42_1, all_88_0) & occurrence_of(all_88_0, % 94.48/13.17 | tptp0) % 94.48/13.17 | % 94.48/13.17 | ALPHA: (87) implies: % 94.48/13.17 | (88) occurrence_of(all_88_0, tptp0) % 94.48/13.17 | (89) subactivity_occurrence(all_42_1, all_88_0) % 94.48/13.17 | (90) subactivity_occurrence(all_54_0, all_88_0) % 94.48/13.17 | (91) $i(all_88_0) % 94.48/13.17 | % 94.48/13.17 | DELTA: instantiating (64) with fresh symbols all_92_0, all_92_1 gives: % 94.48/13.17 | (92) $i(all_92_0) & $i(all_92_1) & subactivity(all_92_0, tptp0) & % 94.48/13.17 | subactivity(all_92_1, tptp0) & atocc(all_54_0, all_92_0) & % 94.48/13.17 | atocc(all_42_1, all_92_1) % 94.48/13.17 | % 94.48/13.17 | ALPHA: (92) implies: % 94.48/13.17 | (93) atocc(all_54_0, all_92_0) % 94.48/13.17 | (94) $i(all_92_0) % 94.48/13.17 | % 94.48/13.17 | BETA: splitting (34) gives: % 94.48/13.17 | % 94.48/13.17 | Case 1: % 94.48/13.17 | | % 94.48/13.17 | | (95) atomic(all_42_2) % 94.48/13.17 | | % 94.48/13.17 | | PRED_UNIFY: (71), (95) imply: % 94.48/13.17 | | (96) $false % 94.48/13.17 | | % 94.48/13.17 | | CLOSE: (96) is inconsistent. % 94.48/13.17 | | % 94.48/13.17 | Case 2: % 94.48/13.17 | | % 94.48/13.17 | | (97) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 94.48/13.17 | | root(v0, all_42_2)) % 94.48/13.17 | | % 94.48/13.17 | | DELTA: instantiating (97) with fresh symbol all_98_0 gives: % 94.48/13.17 | | (98) $i(all_98_0) & subactivity_occurrence(all_98_0, all_42_0) & % 94.48/13.17 | | root(all_98_0, all_42_2) % 94.48/13.17 | | % 94.48/13.17 | | ALPHA: (98) implies: % 94.48/13.17 | | (99) root(all_98_0, all_42_2) % 94.48/13.17 | | (100) subactivity_occurrence(all_98_0, all_42_0) % 94.48/13.17 | | (101) $i(all_98_0) % 94.48/13.17 | | % 94.48/13.17 | | BETA: splitting (70) gives: % 94.48/13.17 | | % 94.48/13.17 | | Case 1: % 94.48/13.17 | | | % 94.48/13.17 | | | (102) atomic(all_70_0) % 94.48/13.17 | | | % 94.48/13.17 | | | REDUCE: (67), (102) imply: % 94.48/13.17 | | | (103) atomic(all_42_2) % 94.48/13.17 | | | % 94.48/13.17 | | | PRED_UNIFY: (71), (103) imply: % 94.48/13.17 | | | (104) $false % 94.48/13.17 | | | % 94.48/13.17 | | | CLOSE: (104) is inconsistent. % 94.48/13.17 | | | % 94.48/13.17 | | Case 2: % 94.48/13.17 | | | % 94.48/13.17 | | | (105) ~ atomic(all_70_0) % 94.48/13.17 | | | (106) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 94.48/13.17 | | | root(v0, all_70_0)) % 94.48/13.17 | | | % 94.48/13.17 | | | DELTA: instantiating (106) with fresh symbol all_103_0 gives: % 94.48/13.17 | | | (107) $i(all_103_0) & subactivity_occurrence(all_103_0, all_42_0) & % 94.48/13.17 | | | root(all_103_0, all_70_0) % 94.48/13.17 | | | % 94.48/13.17 | | | ALPHA: (107) implies: % 94.48/13.17 | | | (108) root(all_103_0, all_70_0) % 94.48/13.17 | | | (109) subactivity_occurrence(all_103_0, all_42_0) % 94.48/13.17 | | | (110) $i(all_103_0) % 94.48/13.17 | | | % 94.48/13.17 | | | REDUCE: (67), (108) imply: % 94.48/13.17 | | | (111) root(all_103_0, all_42_2) % 94.48/13.17 | | | % 94.48/13.17 | | | BETA: splitting (66) gives: % 94.48/13.17 | | | % 94.48/13.17 | | | Case 1: % 94.48/13.17 | | | | % 94.48/13.17 | | | | (112) atomic(all_68_0) % 94.48/13.17 | | | | % 94.48/13.17 | | | | REDUCE: (77), (112) imply: % 94.48/13.17 | | | | (113) atomic(all_42_2) % 94.48/13.17 | | | | % 94.48/13.18 | | | | PRED_UNIFY: (71), (113) imply: % 94.48/13.18 | | | | (114) $false % 94.48/13.18 | | | | % 94.48/13.18 | | | | CLOSE: (114) is inconsistent. % 94.48/13.18 | | | | % 94.48/13.18 | | | Case 2: % 94.48/13.18 | | | | % 94.48/13.18 | | | | (115) ~ atomic(all_68_0) % 94.48/13.18 | | | | (116) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 94.48/13.18 | | | | root(v0, all_68_0)) % 94.48/13.18 | | | | % 94.48/13.18 | | | | DELTA: instantiating (116) with fresh symbol all_108_0 gives: % 94.48/13.18 | | | | (117) $i(all_108_0) & subactivity_occurrence(all_108_0, all_42_0) & % 94.48/13.18 | | | | root(all_108_0, all_68_0) % 94.48/13.18 | | | | % 94.48/13.18 | | | | ALPHA: (117) implies: % 94.48/13.18 | | | | (118) root(all_108_0, all_68_0) % 94.48/13.18 | | | | (119) subactivity_occurrence(all_108_0, all_42_0) % 94.48/13.18 | | | | (120) $i(all_108_0) % 94.48/13.18 | | | | % 94.48/13.18 | | | | REDUCE: (77), (118) imply: % 94.48/13.18 | | | | (121) root(all_108_0, all_42_2) % 94.48/13.18 | | | | % 94.48/13.18 | | | | PRED_UNIFY: (53), (71) imply: % 94.48/13.18 | | | | (122) ~ (all_54_3 = all_42_2) % 94.48/13.18 | | | | % 94.48/13.18 | | | | BETA: splitting (68) gives: % 94.48/13.18 | | | | % 94.48/13.18 | | | | Case 1: % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_54_3, all_84_0, % 94.48/13.18 | | | | | simplifying with (38), (41), (44), (82), (83) gives: % 94.48/13.18 | | | | | (123) all_84_0 = all_54_3 % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (13) with all_88_0, simplifying with (88), % 94.48/13.18 | | | | | (91) gives: % 94.48/13.18 | | | | | (124) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & % 94.48/13.18 | | | | | next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_88_0) & % 94.48/13.18 | | | | | root_occ(v0, all_88_0) & occurrence_of(v0, tptp4) & % 94.48/13.18 | | | | | (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_30) with tptp0, all_88_0, simplifying % 94.48/13.18 | | | | | with (9), (10), (88), (91) gives: % 94.48/13.18 | | | | | (125) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_88_0) % 94.48/13.18 | | | | | & root(v0, tptp0)) % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_27) with all_42_2, all_98_0, % 94.48/13.18 | | | | | simplifying with (30), (99), (101) gives: % 94.48/13.18 | | | | | (126) ? [v0: $i] : ($i(v0) & subactivity(v0, all_42_2) & % 94.48/13.18 | | | | | atocc(all_98_0, v0)) % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_12) with all_98_0, all_42_2, % 94.48/13.18 | | | | | simplifying with (30), (99), (101) gives: % 94.48/13.18 | | | | | (127) legal(all_98_0) % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_27) with all_42_2, all_103_0, % 94.48/13.18 | | | | | simplifying with (30), (110), (111) gives: % 94.48/13.18 | | | | | (128) ? [v0: $i] : ($i(v0) & subactivity(v0, all_42_2) & % 94.48/13.18 | | | | | atocc(all_103_0, v0)) % 94.48/13.18 | | | | | % 94.48/13.18 | | | | | GROUND_INST: instantiating (sos_27) with all_42_2, all_108_0, % 94.48/13.18 | | | | | simplifying with (30), (120), (121) gives: % 94.48/13.18 | | | | | (129) ? [v0: $i] : ($i(v0) & subactivity(v0, all_42_2) & % 94.48/13.18 | | | | | atocc(all_108_0, v0)) % 94.48/13.18 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (24) with all_42_1, all_88_0, tptp0, % 94.48/13.19 | | | | | simplifying with (10), (31), (36), (88), (89), (91) % 94.48/13.19 | | | | | gives: % 94.48/13.19 | | | | | (130) root_occ(all_42_1, all_88_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (16) with all_54_0, all_88_0, simplifying % 94.48/13.19 | | | | | with (44), (90), (91) gives: % 94.48/13.19 | | | | | (131) activity_occurrence(all_88_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (24) with all_98_0, all_42_0, all_42_2, % 94.48/13.19 | | | | | simplifying with (28), (30), (32), (99), (100), (101) % 94.48/13.19 | | | | | gives: % 94.48/13.19 | | | | | (132) root_occ(all_98_0, all_42_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (15) with all_98_0, all_42_0, simplifying % 94.48/13.19 | | | | | with (32), (100), (101) gives: % 94.48/13.19 | | | | | (133) activity_occurrence(all_98_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (24) with all_103_0, all_42_0, all_42_2, % 94.48/13.19 | | | | | simplifying with (28), (30), (32), (109), (110), (111) % 94.48/13.19 | | | | | gives: % 94.48/13.19 | | | | | (134) root_occ(all_103_0, all_42_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (15) with all_103_0, all_42_0, simplifying % 94.48/13.19 | | | | | with (32), (109), (110) gives: % 94.48/13.19 | | | | | (135) activity_occurrence(all_103_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (24) with all_108_0, all_42_0, all_42_2, % 94.48/13.19 | | | | | simplifying with (28), (30), (32), (119), (120), (121) % 94.48/13.19 | | | | | gives: % 94.48/13.19 | | | | | (136) root_occ(all_108_0, all_42_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (15) with all_108_0, all_42_0, simplifying % 94.48/13.19 | | | | | with (32), (119), (120) gives: % 94.48/13.19 | | | | | (137) activity_occurrence(all_108_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (17) with all_54_2, all_86_0, simplifying % 94.48/13.19 | | | | | with (42), (85), (86) gives: % 94.48/13.19 | | | | | (138) ? [v0: $i] : ($i(v0) & subactivity(all_86_0, v0) & % 94.48/13.19 | | | | | atomic(v0) & occurrence_of(all_54_2, v0)) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (sos_16) with all_54_0, all_82_0, % 94.48/13.19 | | | | | simplifying with (44), (74), (79), (80) gives: % 94.48/13.19 | | | | | (139) root(all_54_0, all_82_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (17) with all_54_0, all_82_0, simplifying % 94.48/13.19 | | | | | with (44), (79), (80) gives: % 94.48/13.19 | | | | | (140) ? [v0: $i] : ($i(v0) & subactivity(all_82_0, v0) & % 94.48/13.19 | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (sos_16) with all_54_0, all_92_0, % 94.48/13.19 | | | | | simplifying with (44), (74), (93), (94) gives: % 94.48/13.19 | | | | | (141) root(all_54_0, all_92_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (17) with all_54_0, all_92_0, simplifying % 94.48/13.19 | | | | | with (44), (93), (94) gives: % 94.48/13.19 | | | | | (142) ? [v0: $i] : ($i(v0) & subactivity(all_92_0, v0) & % 94.48/13.19 | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | GROUND_INST: instantiating (18) with all_54_0, all_54_3, all_54_3, % 94.48/13.19 | | | | | simplifying with (38), (41), (44), (53), (76) gives: % 94.48/13.19 | | | | | (143) atocc(all_54_0, all_54_3) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | DELTA: instantiating (128) with fresh symbol all_128_0 gives: % 94.48/13.19 | | | | | (144) $i(all_128_0) & subactivity(all_128_0, all_42_2) & % 94.48/13.19 | | | | | atocc(all_103_0, all_128_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | ALPHA: (144) implies: % 94.48/13.19 | | | | | (145) atocc(all_103_0, all_128_0) % 94.48/13.19 | | | | | (146) $i(all_128_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | DELTA: instantiating (129) with fresh symbol all_132_0 gives: % 94.48/13.19 | | | | | (147) $i(all_132_0) & subactivity(all_132_0, all_42_2) & % 94.48/13.19 | | | | | atocc(all_108_0, all_132_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | ALPHA: (147) implies: % 94.48/13.19 | | | | | (148) atocc(all_108_0, all_132_0) % 94.48/13.19 | | | | | (149) $i(all_132_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | DELTA: instantiating (125) with fresh symbol all_134_0 gives: % 94.48/13.19 | | | | | (150) $i(all_134_0) & subactivity_occurrence(all_134_0, all_88_0) & % 94.48/13.19 | | | | | root(all_134_0, tptp0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | ALPHA: (150) implies: % 94.48/13.19 | | | | | (151) root(all_134_0, tptp0) % 94.48/13.19 | | | | | (152) subactivity_occurrence(all_134_0, all_88_0) % 94.48/13.19 | | | | | (153) $i(all_134_0) % 94.48/13.19 | | | | | % 94.48/13.19 | | | | | DELTA: instantiating (126) with fresh symbol all_136_0 gives: % 94.48/13.19 | | | | | (154) $i(all_136_0) & subactivity(all_136_0, all_42_2) & % 94.48/13.20 | | | | | atocc(all_98_0, all_136_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | ALPHA: (154) implies: % 94.48/13.20 | | | | | (155) atocc(all_98_0, all_136_0) % 94.48/13.20 | | | | | (156) $i(all_136_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | DELTA: instantiating (138) with fresh symbol all_138_0 gives: % 94.48/13.20 | | | | | (157) $i(all_138_0) & subactivity(all_86_0, all_138_0) & % 94.48/13.20 | | | | | atomic(all_138_0) & occurrence_of(all_54_2, all_138_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | ALPHA: (157) implies: % 94.48/13.20 | | | | | (158) atomic(all_138_0) % 94.48/13.20 | | | | | (159) $i(all_138_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | DELTA: instantiating (142) with fresh symbol all_140_0 gives: % 94.48/13.20 | | | | | (160) $i(all_140_0) & subactivity(all_92_0, all_140_0) & % 94.48/13.20 | | | | | atomic(all_140_0) & occurrence_of(all_54_0, all_140_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | ALPHA: (160) implies: % 94.48/13.20 | | | | | (161) occurrence_of(all_54_0, all_140_0) % 94.48/13.20 | | | | | (162) $i(all_140_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | DELTA: instantiating (140) with fresh symbol all_142_0 gives: % 94.48/13.20 | | | | | (163) $i(all_142_0) & subactivity(all_82_0, all_142_0) & % 94.48/13.20 | | | | | atomic(all_142_0) & occurrence_of(all_54_0, all_142_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | ALPHA: (163) implies: % 94.48/13.20 | | | | | (164) occurrence_of(all_54_0, all_142_0) % 94.48/13.20 | | | | | (165) $i(all_142_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | DELTA: instantiating (124) with fresh symbols all_146_0, all_146_1 % 94.48/13.20 | | | | | gives: % 94.48/13.20 | | | | | (166) $i(all_146_0) & $i(all_146_1) & next_subocc(all_146_1, % 94.48/13.20 | | | | | all_146_0, tptp0) & leaf_occ(all_146_0, all_88_0) & % 94.48/13.20 | | | | | root_occ(all_146_1, all_88_0) & occurrence_of(all_146_1, % 94.48/13.20 | | | | | tptp4) & (occurrence_of(all_146_0, tptp2) | % 94.48/13.20 | | | | | occurrence_of(all_146_0, tptp3)) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | ALPHA: (166) implies: % 94.48/13.20 | | | | | (167) root_occ(all_146_1, all_88_0) % 94.48/13.20 | | | | | (168) leaf_occ(all_146_0, all_88_0) % 94.48/13.20 | | | | | (169) next_subocc(all_146_1, all_146_0, tptp0) % 94.48/13.20 | | | | | (170) $i(all_146_1) % 94.48/13.20 | | | | | (171) $i(all_146_0) % 94.48/13.20 | | | | | (172) occurrence_of(all_146_0, tptp2) | occurrence_of(all_146_0, % 94.48/13.20 | | | | | tptp3) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | PRED_UNIFY: (71), (158) imply: % 94.48/13.20 | | | | | (173) ~ (all_138_0 = all_42_2) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_22) with all_42_0, all_42_2, % 94.48/13.20 | | | | | all_138_0, simplifying with (28), (30), (32), (159) % 94.48/13.20 | | | | | gives: % 94.48/13.20 | | | | | (174) all_138_0 = all_42_2 | ~ occurrence_of(all_42_0, all_138_0) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_54_3, % 94.48/13.20 | | | | | all_142_0, simplifying with (38), (41), (44), (164), % 94.48/13.20 | | | | | (165) gives: % 94.48/13.20 | | | | | (175) all_142_0 = all_54_3 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_140_0, % 94.48/13.20 | | | | | all_142_0, simplifying with (44), (161), (162), (164), % 94.48/13.20 | | | | | (165) gives: % 94.48/13.20 | | | | | (176) all_142_0 = all_140_0 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (23) with all_42_1, all_88_0, simplifying % 94.48/13.20 | | | | | with (31), (91), (130) gives: % 94.48/13.20 | | | | | (177) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_42_1, % 94.48/13.20 | | | | | all_88_0) & root(all_42_1, v0) & occurrence_of(all_88_0, % 94.48/13.20 | | | | | v0)) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_02) with all_98_0, all_103_0, % 94.48/13.20 | | | | | all_42_0, all_42_2, simplifying with (28), (30), (32), % 94.48/13.20 | | | | | (101), (110), (132), (134) gives: % 94.48/13.20 | | | | | (178) all_103_0 = all_98_0 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_02) with all_54_0, all_108_0, % 94.48/13.20 | | | | | all_42_0, all_42_2, simplifying with (28), (30), (32), % 94.48/13.20 | | | | | (39), (44), (120), (136) gives: % 94.48/13.20 | | | | | (179) all_108_0 = all_54_0 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_02) with all_103_0, all_108_0, % 94.48/13.20 | | | | | all_42_0, all_42_2, simplifying with (28), (30), (32), % 94.48/13.20 | | | | | (110), (120), (134), (136) gives: % 94.48/13.20 | | | | | (180) all_108_0 = all_103_0 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (sos_02) with all_42_1, all_146_1, % 94.48/13.20 | | | | | all_88_0, tptp0, simplifying with (10), (31), (88), (91), % 94.48/13.20 | | | | | (130), (167), (170) gives: % 94.48/13.20 | | | | | (181) all_146_1 = all_42_1 % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (23) with all_146_1, all_88_0, simplifying % 94.48/13.20 | | | | | with (91), (167), (170) gives: % 94.48/13.20 | | | | | (182) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_146_1, % 94.48/13.20 | | | | | all_88_0) & root(all_146_1, v0) & occurrence_of(all_88_0, % 94.48/13.20 | | | | | v0)) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (21) with all_146_0, all_88_0, simplifying % 94.48/13.20 | | | | | with (91), (168), (171) gives: % 94.48/13.20 | | | | | (183) ? [v0: $i] : ($i(v0) & leaf(all_146_0, v0) & % 94.48/13.20 | | | | | subactivity_occurrence(all_146_0, all_88_0) & % 94.48/13.20 | | | | | occurrence_of(all_88_0, v0)) % 94.48/13.20 | | | | | % 94.48/13.20 | | | | | GROUND_INST: instantiating (25) with all_146_1, all_146_0, tptp0, % 94.48/13.20 | | | | | simplifying with (10), (169), (170), (171) gives: % 94.48/13.21 | | | | | (184) arboreal(all_146_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_27) with all_82_0, all_54_0, % 94.48/13.21 | | | | | simplifying with (44), (80), (139) gives: % 94.48/13.21 | | | | | (185) ? [v0: $i] : ($i(v0) & subactivity(v0, all_82_0) & % 94.48/13.21 | | | | | atocc(all_54_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_27) with all_92_0, all_54_0, % 94.48/13.21 | | | | | simplifying with (44), (94), (141) gives: % 94.48/13.21 | | | | | (186) ? [v0: $i] : ($i(v0) & subactivity(v0, all_92_0) & % 94.48/13.21 | | | | | atocc(all_54_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_17) with all_98_0, simplifying with % 94.48/13.21 | | | | | (101), (127) gives: % 94.48/13.21 | | | | | (187) arboreal(all_98_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (24) with all_134_0, all_88_0, tptp0, % 94.48/13.21 | | | | | simplifying with (10), (88), (91), (151), (152), (153) % 94.48/13.21 | | | | | gives: % 94.48/13.21 | | | | | (188) root_occ(all_134_0, all_88_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (17) with all_54_0, all_54_3, simplifying % 94.48/13.21 | | | | | with (41), (44), (143) gives: % 94.48/13.21 | | | | | (189) ? [v0: $i] : ($i(v0) & subactivity(all_54_3, v0) & % 94.48/13.21 | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (17) with all_98_0, all_136_0, simplifying % 94.48/13.21 | | | | | with (101), (155), (156) gives: % 94.48/13.21 | | | | | (190) ? [v0: $i] : ($i(v0) & subactivity(all_136_0, v0) & % 94.48/13.21 | | | | | atomic(v0) & occurrence_of(all_98_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (17) with all_103_0, all_128_0, simplifying % 94.48/13.21 | | | | | with (110), (145), (146) gives: % 94.48/13.21 | | | | | (191) ? [v0: $i] : ($i(v0) & subactivity(all_128_0, v0) & % 94.48/13.21 | | | | | atomic(v0) & occurrence_of(all_103_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (17) with all_108_0, all_132_0, simplifying % 94.48/13.21 | | | | | with (120), (148), (149) gives: % 94.48/13.21 | | | | | (192) ? [v0: $i] : ($i(v0) & subactivity(all_132_0, v0) & % 94.48/13.21 | | | | | atomic(v0) & occurrence_of(all_108_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_18) with all_88_0, simplifying with % 94.48/13.21 | | | | | (91), (131) gives: % 94.48/13.21 | | | | | (193) ? [v0: $i] : ($i(v0) & activity(v0) & % 94.48/13.21 | | | | | occurrence_of(all_88_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_18) with all_98_0, simplifying with % 94.48/13.21 | | | | | (101), (133) gives: % 94.48/13.21 | | | | | (194) ? [v0: $i] : ($i(v0) & activity(v0) & % 94.48/13.21 | | | | | occurrence_of(all_98_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_18) with all_103_0, simplifying with % 94.48/13.21 | | | | | (110), (135) gives: % 94.48/13.21 | | | | | (195) ? [v0: $i] : ($i(v0) & activity(v0) & % 94.48/13.21 | | | | | occurrence_of(all_103_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | GROUND_INST: instantiating (sos_18) with all_108_0, simplifying with % 94.48/13.21 | | | | | (120), (137) gives: % 94.48/13.21 | | | | | (196) ? [v0: $i] : ($i(v0) & activity(v0) & % 94.48/13.21 | | | | | occurrence_of(all_108_0, v0)) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | COMBINE_EQS: (175), (176) imply: % 94.48/13.21 | | | | | (197) all_140_0 = all_54_3 % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | COMBINE_EQS: (179), (180) imply: % 94.48/13.21 | | | | | (198) all_103_0 = all_54_0 % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | SIMP: (198) implies: % 94.48/13.21 | | | | | (199) all_103_0 = all_54_0 % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | COMBINE_EQS: (178), (199) imply: % 94.48/13.21 | | | | | (200) all_98_0 = all_54_0 % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (185) with fresh symbol all_160_0 gives: % 94.48/13.21 | | | | | (201) $i(all_160_0) & subactivity(all_160_0, all_82_0) & % 94.48/13.21 | | | | | atocc(all_54_0, all_160_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (201) implies: % 94.48/13.21 | | | | | (202) atocc(all_54_0, all_160_0) % 94.48/13.21 | | | | | (203) $i(all_160_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (195) with fresh symbol all_162_0 gives: % 94.48/13.21 | | | | | (204) $i(all_162_0) & activity(all_162_0) & % 94.48/13.21 | | | | | occurrence_of(all_103_0, all_162_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (204) implies: % 94.48/13.21 | | | | | (205) occurrence_of(all_103_0, all_162_0) % 94.48/13.21 | | | | | (206) $i(all_162_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (194) with fresh symbol all_164_0 gives: % 94.48/13.21 | | | | | (207) $i(all_164_0) & activity(all_164_0) & occurrence_of(all_98_0, % 94.48/13.21 | | | | | all_164_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (207) implies: % 94.48/13.21 | | | | | (208) occurrence_of(all_98_0, all_164_0) % 94.48/13.21 | | | | | (209) $i(all_164_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (186) with fresh symbol all_170_0 gives: % 94.48/13.21 | | | | | (210) $i(all_170_0) & subactivity(all_170_0, all_92_0) & % 94.48/13.21 | | | | | atocc(all_54_0, all_170_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (210) implies: % 94.48/13.21 | | | | | (211) atocc(all_54_0, all_170_0) % 94.48/13.21 | | | | | (212) $i(all_170_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (196) with fresh symbol all_172_0 gives: % 94.48/13.21 | | | | | (213) $i(all_172_0) & activity(all_172_0) & % 94.48/13.21 | | | | | occurrence_of(all_108_0, all_172_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (213) implies: % 94.48/13.21 | | | | | (214) occurrence_of(all_108_0, all_172_0) % 94.48/13.21 | | | | | (215) $i(all_172_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (193) with fresh symbol all_174_0 gives: % 94.48/13.21 | | | | | (216) $i(all_174_0) & activity(all_174_0) & occurrence_of(all_88_0, % 94.48/13.21 | | | | | all_174_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (216) implies: % 94.48/13.21 | | | | | (217) occurrence_of(all_88_0, all_174_0) % 94.48/13.21 | | | | | (218) $i(all_174_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (177) with fresh symbol all_178_0 gives: % 94.48/13.21 | | | | | (219) $i(all_178_0) & subactivity_occurrence(all_42_1, all_88_0) & % 94.48/13.21 | | | | | root(all_42_1, all_178_0) & occurrence_of(all_88_0, % 94.48/13.21 | | | | | all_178_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (219) implies: % 94.48/13.21 | | | | | (220) occurrence_of(all_88_0, all_178_0) % 94.48/13.21 | | | | | (221) $i(all_178_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (191) with fresh symbol all_180_0 gives: % 94.48/13.21 | | | | | (222) $i(all_180_0) & subactivity(all_128_0, all_180_0) & % 94.48/13.21 | | | | | atomic(all_180_0) & occurrence_of(all_103_0, all_180_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (222) implies: % 94.48/13.21 | | | | | (223) occurrence_of(all_103_0, all_180_0) % 94.48/13.21 | | | | | (224) $i(all_180_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (190) with fresh symbol all_182_0 gives: % 94.48/13.21 | | | | | (225) $i(all_182_0) & subactivity(all_136_0, all_182_0) & % 94.48/13.21 | | | | | atomic(all_182_0) & occurrence_of(all_98_0, all_182_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | ALPHA: (225) implies: % 94.48/13.21 | | | | | (226) occurrence_of(all_98_0, all_182_0) % 94.48/13.21 | | | | | (227) $i(all_182_0) % 94.48/13.21 | | | | | % 94.48/13.21 | | | | | DELTA: instantiating (182) with fresh symbol all_186_0 gives: % 94.48/13.22 | | | | | (228) $i(all_186_0) & subactivity_occurrence(all_146_1, all_88_0) & % 94.48/13.22 | | | | | root(all_146_1, all_186_0) & occurrence_of(all_88_0, % 94.48/13.22 | | | | | all_186_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | ALPHA: (228) implies: % 94.48/13.22 | | | | | (229) occurrence_of(all_88_0, all_186_0) % 94.48/13.22 | | | | | (230) $i(all_186_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | DELTA: instantiating (189) with fresh symbol all_194_0 gives: % 94.48/13.22 | | | | | (231) $i(all_194_0) & subactivity(all_54_3, all_194_0) & % 94.48/13.22 | | | | | atomic(all_194_0) & occurrence_of(all_54_0, all_194_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | ALPHA: (231) implies: % 94.48/13.22 | | | | | (232) occurrence_of(all_54_0, all_194_0) % 94.48/13.22 | | | | | (233) $i(all_194_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | DELTA: instantiating (183) with fresh symbol all_196_0 gives: % 94.48/13.22 | | | | | (234) $i(all_196_0) & leaf(all_146_0, all_196_0) & % 94.48/13.22 | | | | | subactivity_occurrence(all_146_0, all_88_0) & % 94.48/13.22 | | | | | occurrence_of(all_88_0, all_196_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | ALPHA: (234) implies: % 94.48/13.22 | | | | | (235) occurrence_of(all_88_0, all_196_0) % 94.48/13.22 | | | | | (236) subactivity_occurrence(all_146_0, all_88_0) % 94.48/13.22 | | | | | (237) leaf(all_146_0, all_196_0) % 94.48/13.22 | | | | | (238) $i(all_196_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | DELTA: instantiating (192) with fresh symbol all_198_0 gives: % 94.48/13.22 | | | | | (239) $i(all_198_0) & subactivity(all_132_0, all_198_0) & % 94.48/13.22 | | | | | atomic(all_198_0) & occurrence_of(all_108_0, all_198_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | ALPHA: (239) implies: % 94.48/13.22 | | | | | (240) occurrence_of(all_108_0, all_198_0) % 94.48/13.22 | | | | | (241) $i(all_198_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (187), (200) imply: % 94.48/13.22 | | | | | (242) arboreal(all_54_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (169), (181) imply: % 94.48/13.22 | | | | | (243) next_subocc(all_42_1, all_146_0, tptp0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (179), (240) imply: % 94.48/13.22 | | | | | (244) occurrence_of(all_54_0, all_198_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (179), (214) imply: % 94.48/13.22 | | | | | (245) occurrence_of(all_54_0, all_172_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (199), (223) imply: % 94.48/13.22 | | | | | (246) occurrence_of(all_54_0, all_180_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (199), (205) imply: % 94.48/13.22 | | | | | (247) occurrence_of(all_54_0, all_162_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (200), (226) imply: % 94.48/13.22 | | | | | (248) occurrence_of(all_54_0, all_182_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | REDUCE: (200), (208) imply: % 94.48/13.22 | | | | | (249) occurrence_of(all_54_0, all_164_0) % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | BETA: splitting (174) gives: % 94.48/13.22 | | | | | % 94.48/13.22 | | | | | Case 1: % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_54_3, % 94.48/13.22 | | | | | | all_180_0, simplifying with (38), (41), (44), (224), % 94.48/13.22 | | | | | | (246) gives: % 94.48/13.22 | | | | | | (250) all_180_0 = all_54_3 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_164_0, % 94.48/13.22 | | | | | | all_180_0, simplifying with (44), (209), (224), (246), % 94.48/13.22 | | | | | | (249) gives: % 94.48/13.22 | | | | | | (251) all_180_0 = all_164_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_164_0, % 94.48/13.22 | | | | | | all_182_0, simplifying with (44), (209), (227), (248), % 94.48/13.22 | | | | | | (249) gives: % 94.48/13.22 | | | | | | (252) all_182_0 = all_164_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_180_0, % 94.48/13.22 | | | | | | all_194_0, simplifying with (44), (224), (232), (233), % 94.48/13.22 | | | | | | (246) gives: % 94.48/13.22 | | | | | | (253) all_194_0 = all_180_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_172_0, % 94.48/13.22 | | | | | | all_194_0, simplifying with (44), (215), (232), (233), % 94.48/13.22 | | | | | | (245) gives: % 94.48/13.22 | | | | | | (254) all_194_0 = all_172_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_182_0, % 94.48/13.22 | | | | | | all_198_0, simplifying with (44), (227), (241), (244), % 94.48/13.22 | | | | | | (248) gives: % 94.48/13.22 | | | | | | (255) all_198_0 = all_182_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_162_0, % 94.48/13.22 | | | | | | all_198_0, simplifying with (44), (206), (241), (244), % 94.48/13.22 | | | | | | (247) gives: % 94.48/13.22 | | | | | | (256) all_198_0 = all_162_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_88_0, tptp0, all_186_0, % 94.48/13.22 | | | | | | simplifying with (10), (88), (91), (229), (230) gives: % 94.48/13.22 | | | | | | (257) all_186_0 = tptp0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_88_0, all_174_0, % 94.48/13.22 | | | | | | all_186_0, simplifying with (91), (217), (218), (229), % 94.48/13.22 | | | | | | (230) gives: % 94.48/13.22 | | | | | | (258) all_186_0 = all_174_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_88_0, all_186_0, % 94.48/13.22 | | | | | | all_196_0, simplifying with (91), (229), (230), (235), % 94.48/13.22 | | | | | | (238) gives: % 94.48/13.22 | | | | | | (259) all_196_0 = all_186_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_22) with all_88_0, all_178_0, % 94.48/13.22 | | | | | | all_196_0, simplifying with (91), (220), (221), (235), % 94.48/13.22 | | | | | | (238) gives: % 94.48/13.22 | | | | | | (260) all_196_0 = all_178_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (sos_02) with all_42_1, all_134_0, % 94.48/13.22 | | | | | | all_88_0, all_174_0, simplifying with (31), (91), % 94.48/13.22 | | | | | | (130), (153), (188), (217), (218) gives: % 94.48/13.22 | | | | | | (261) all_134_0 = all_42_1 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (23) with all_134_0, all_88_0, % 94.48/13.22 | | | | | | simplifying with (91), (153), (188) gives: % 94.48/13.22 | | | | | | (262) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_134_0, % 94.48/13.22 | | | | | | all_88_0) & root(all_134_0, v0) & % 94.48/13.22 | | | | | | occurrence_of(all_88_0, v0)) % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (22) with all_54_0, all_88_0, all_196_0, % 94.48/13.22 | | | | | | simplifying with (44), (90), (91), (235), (238) gives: % 94.48/13.22 | | | | | | (263) ~ leaf(all_54_0, all_196_0) | leaf_occ(all_54_0, all_88_0) % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (17) with all_54_0, all_160_0, % 94.48/13.22 | | | | | | simplifying with (44), (202), (203) gives: % 94.48/13.22 | | | | | | (264) ? [v0: $i] : ($i(v0) & subactivity(all_160_0, v0) & % 94.48/13.22 | | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | GROUND_INST: instantiating (17) with all_54_0, all_170_0, % 94.48/13.22 | | | | | | simplifying with (44), (211), (212) gives: % 94.48/13.22 | | | | | | (265) ? [v0: $i] : ($i(v0) & subactivity(all_170_0, v0) & % 94.48/13.22 | | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | COMBINE_EQS: (255), (256) imply: % 94.48/13.22 | | | | | | (266) all_182_0 = all_162_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | SIMP: (266) implies: % 94.48/13.22 | | | | | | (267) all_182_0 = all_162_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | COMBINE_EQS: (259), (260) imply: % 94.48/13.22 | | | | | | (268) all_186_0 = all_178_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | SIMP: (268) implies: % 94.48/13.22 | | | | | | (269) all_186_0 = all_178_0 % 94.48/13.22 | | | | | | % 94.48/13.22 | | | | | | COMBINE_EQS: (253), (254) imply: % 94.48/13.23 | | | | | | (270) all_180_0 = all_172_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | SIMP: (270) implies: % 94.48/13.23 | | | | | | (271) all_180_0 = all_172_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (258), (269) imply: % 94.48/13.23 | | | | | | (272) all_178_0 = all_174_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (257), (269) imply: % 94.48/13.23 | | | | | | (273) all_178_0 = tptp0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (252), (267) imply: % 94.48/13.23 | | | | | | (274) all_164_0 = all_162_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | SIMP: (274) implies: % 94.48/13.23 | | | | | | (275) all_164_0 = all_162_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (251), (271) imply: % 94.48/13.23 | | | | | | (276) all_172_0 = all_164_0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (250), (271) imply: % 94.48/13.23 | | | | | | (277) all_172_0 = all_54_3 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (272), (273) imply: % 94.48/13.23 | | | | | | (278) all_174_0 = tptp0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | SIMP: (278) implies: % 94.48/13.23 | | | | | | (279) all_174_0 = tptp0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (276), (277) imply: % 94.48/13.23 | | | | | | (280) all_164_0 = all_54_3 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | SIMP: (280) implies: % 94.48/13.23 | | | | | | (281) all_164_0 = all_54_3 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (275), (281) imply: % 94.48/13.23 | | | | | | (282) all_162_0 = all_54_3 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | COMBINE_EQS: (260), (273) imply: % 94.48/13.23 | | | | | | (283) all_196_0 = tptp0 % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | DELTA: instantiating (262) with fresh symbol all_270_0 gives: % 94.48/13.23 | | | | | | (284) $i(all_270_0) & subactivity_occurrence(all_134_0, all_88_0) % 94.48/13.23 | | | | | | & root(all_134_0, all_270_0) & occurrence_of(all_88_0, % 94.48/13.23 | | | | | | all_270_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | ALPHA: (284) implies: % 94.48/13.23 | | | | | | (285) occurrence_of(all_88_0, all_270_0) % 94.48/13.23 | | | | | | (286) $i(all_270_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | DELTA: instantiating (264) with fresh symbol all_272_0 gives: % 94.48/13.23 | | | | | | (287) $i(all_272_0) & subactivity(all_160_0, all_272_0) & % 94.48/13.23 | | | | | | atomic(all_272_0) & occurrence_of(all_54_0, all_272_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | ALPHA: (287) implies: % 94.48/13.23 | | | | | | (288) occurrence_of(all_54_0, all_272_0) % 94.48/13.23 | | | | | | (289) $i(all_272_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | DELTA: instantiating (265) with fresh symbol all_274_0 gives: % 94.48/13.23 | | | | | | (290) $i(all_274_0) & subactivity(all_170_0, all_274_0) & % 94.48/13.23 | | | | | | atomic(all_274_0) & occurrence_of(all_54_0, all_274_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | ALPHA: (290) implies: % 94.48/13.23 | | | | | | (291) occurrence_of(all_54_0, all_274_0) % 94.48/13.23 | | | | | | (292) $i(all_274_0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | REDUCE: (237), (283) imply: % 94.48/13.23 | | | | | | (293) leaf(all_146_0, tptp0) % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | BETA: splitting (63) gives: % 94.48/13.23 | | | | | | % 94.48/13.23 | | | | | | Case 1: % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | (294) leaf(all_54_0, tptp0) % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | BETA: splitting (263) gives: % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | Case 1: % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | (295) ~ leaf(all_54_0, all_196_0) % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | REDUCE: (283), (295) imply: % 94.48/13.23 | | | | | | | | (296) ~ leaf(all_54_0, tptp0) % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | PRED_UNIFY: (294), (296) imply: % 94.48/13.23 | | | | | | | | (297) $false % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | CLOSE: (297) is inconsistent. % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | Case 2: % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | (298) leaf_occ(all_54_0, all_88_0) % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | BETA: splitting (172) gives: % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | | Case 1: % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | (299) occurrence_of(all_146_0, tptp2) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_54_3, % 94.48/13.23 | | | | | | | | | all_274_0, simplifying with (38), (41), (44), % 94.48/13.23 | | | | | | | | | (291), (292) gives: % 94.48/13.23 | | | | | | | | | (300) all_274_0 = all_54_3 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_272_0, % 94.48/13.23 | | | | | | | | | all_274_0, simplifying with (44), (288), (289), % 94.48/13.23 | | | | | | | | | (291), (292) gives: % 94.48/13.23 | | | | | | | | | (301) all_274_0 = all_272_0 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_272_0, % 94.48/13.23 | | | | | | | | | tptp2, simplifying with (12), (44), (288), (289) % 94.48/13.23 | | | | | | | | | gives: % 94.48/13.23 | | | | | | | | | (302) all_272_0 = tptp2 | ~ occurrence_of(all_54_0, tptp2) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_03) with all_146_0, all_54_0, % 94.48/13.23 | | | | | | | | | all_88_0, tptp0, simplifying with (9), (10), (44), % 94.48/13.23 | | | | | | | | | (88), (91), (168), (171), (298) gives: % 94.48/13.23 | | | | | | | | | (303) all_146_0 = all_54_0 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | COMBINE_EQS: (300), (301) imply: % 94.48/13.23 | | | | | | | | | (304) all_272_0 = all_54_3 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | REDUCE: (299), (303) imply: % 94.48/13.23 | | | | | | | | | (305) occurrence_of(all_54_0, tptp2) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | BETA: splitting (302) gives: % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | Case 1: % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | (306) ~ occurrence_of(all_54_0, tptp2) % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | PRED_UNIFY: (305), (306) imply: % 94.48/13.23 | | | | | | | | | | (307) $false % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | CLOSE: (307) is inconsistent. % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | Case 2: % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | (308) all_272_0 = tptp2 % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | COMBINE_EQS: (304), (308) imply: % 94.48/13.23 | | | | | | | | | | (309) all_54_3 = tptp2 % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | REDUCE: (62), (309) imply: % 94.48/13.23 | | | | | | | | | | (310) $false % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | CLOSE: (310) is inconsistent. % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | End of split % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | Case 2: % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | (311) occurrence_of(all_146_0, tptp3) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_54_3, % 94.48/13.23 | | | | | | | | | all_274_0, simplifying with (38), (41), (44), % 94.48/13.23 | | | | | | | | | (291), (292) gives: % 94.48/13.23 | | | | | | | | | (312) all_274_0 = all_54_3 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_272_0, % 94.48/13.23 | | | | | | | | | all_274_0, simplifying with (44), (288), (289), % 94.48/13.23 | | | | | | | | | (291), (292) gives: % 94.48/13.23 | | | | | | | | | (313) all_274_0 = all_272_0 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_22) with all_54_0, all_272_0, % 94.48/13.23 | | | | | | | | | tptp3, simplifying with (11), (44), (288), (289) % 94.48/13.23 | | | | | | | | | gives: % 94.48/13.23 | | | | | | | | | (314) all_272_0 = tptp3 | ~ occurrence_of(all_54_0, tptp3) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | GROUND_INST: instantiating (sos_03) with all_146_0, all_54_0, % 94.48/13.23 | | | | | | | | | all_88_0, tptp0, simplifying with (9), (10), (44), % 94.48/13.23 | | | | | | | | | (88), (91), (168), (171), (298) gives: % 94.48/13.23 | | | | | | | | | (315) all_146_0 = all_54_0 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | COMBINE_EQS: (312), (313) imply: % 94.48/13.23 | | | | | | | | | (316) all_272_0 = all_54_3 % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | REDUCE: (311), (315) imply: % 94.48/13.23 | | | | | | | | | (317) occurrence_of(all_54_0, tptp3) % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | BETA: splitting (314) gives: % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | | Case 1: % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | (318) ~ occurrence_of(all_54_0, tptp3) % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | PRED_UNIFY: (317), (318) imply: % 94.48/13.23 | | | | | | | | | | (319) $false % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | CLOSE: (319) is inconsistent. % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | Case 2: % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | (320) all_272_0 = tptp3 % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | COMBINE_EQS: (316), (320) imply: % 94.48/13.23 | | | | | | | | | | (321) all_54_3 = tptp3 % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | REDUCE: (61), (321) imply: % 94.48/13.23 | | | | | | | | | | (322) $false % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | | CLOSE: (322) is inconsistent. % 94.48/13.23 | | | | | | | | | | % 94.48/13.23 | | | | | | | | | End of split % 94.48/13.23 | | | | | | | | | % 94.48/13.23 | | | | | | | | End of split % 94.48/13.23 | | | | | | | | % 94.48/13.23 | | | | | | | End of split % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | Case 2: % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | (323) ~ leaf(all_54_0, tptp0) % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | PRED_UNIFY: (293), (323) imply: % 94.48/13.23 | | | | | | | (324) ~ (all_146_0 = all_54_0) % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | GROUND_INST: instantiating (26) with all_42_1, all_146_0, tptp0, % 94.48/13.23 | | | | | | | all_54_0, simplifying with (10), (31), (44), (48), % 94.48/13.23 | | | | | | | (171), (243) gives: % 94.48/13.23 | | | | | | | (325) ~ min_precedes(all_54_0, all_146_0, tptp0) % 94.48/13.23 | | | | | | | % 94.48/13.23 | | | | | | | GROUND_INST: instantiating (sos_28) with all_270_0, all_88_0, % 94.48/13.23 | | | | | | | all_54_0, all_146_0, simplifying with (44), (90), % 94.48/13.23 | | | | | | | (91), (171), (184), (236), (242), (285), (286) gives: % 94.48/13.24 | | | | | | | (326) all_146_0 = all_54_0 | min_precedes(all_146_0, all_54_0, % 94.48/13.24 | | | | | | | all_270_0) | min_precedes(all_54_0, all_146_0, % 94.48/13.24 | | | | | | | all_270_0) % 94.48/13.24 | | | | | | | % 94.48/13.24 | | | | | | | GROUND_INST: instantiating (sos_22) with all_88_0, tptp0, % 94.48/13.24 | | | | | | | all_270_0, simplifying with (10), (88), (91), (285), % 94.48/13.24 | | | | | | | (286) gives: % 94.48/13.24 | | | | | | | (327) all_270_0 = tptp0 % 94.48/13.24 | | | | | | | % 94.48/13.24 | | | | | | | GROUND_INST: instantiating (20) with all_146_0, tptp0, all_54_0, % 94.48/13.24 | | | | | | | simplifying with (10), (44), (171), (293) gives: % 94.48/13.24 | | | | | | | (328) ~ min_precedes(all_146_0, all_54_0, tptp0) % 94.48/13.24 | | | | | | | % 94.48/13.24 | | | | | | | BETA: splitting (326) gives: % 94.48/13.24 | | | | | | | % 94.48/13.24 | | | | | | | Case 1: % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | (329) min_precedes(all_146_0, all_54_0, all_270_0) % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | REDUCE: (327), (329) imply: % 94.48/13.24 | | | | | | | | (330) min_precedes(all_146_0, all_54_0, tptp0) % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | PRED_UNIFY: (328), (330) imply: % 94.48/13.24 | | | | | | | | (331) $false % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | CLOSE: (331) is inconsistent. % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | Case 2: % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | (332) all_146_0 = all_54_0 | min_precedes(all_54_0, % 94.48/13.24 | | | | | | | | all_146_0, all_270_0) % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | BETA: splitting (332) gives: % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | | Case 1: % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | (333) min_precedes(all_54_0, all_146_0, all_270_0) % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | REDUCE: (327), (333) imply: % 94.48/13.24 | | | | | | | | | (334) min_precedes(all_54_0, all_146_0, tptp0) % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | PRED_UNIFY: (325), (334) imply: % 94.48/13.24 | | | | | | | | | (335) $false % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | CLOSE: (335) is inconsistent. % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | Case 2: % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | (336) all_146_0 = all_54_0 % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | REDUCE: (324), (336) imply: % 94.48/13.24 | | | | | | | | | (337) $false % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | | CLOSE: (337) is inconsistent. % 94.48/13.24 | | | | | | | | | % 94.48/13.24 | | | | | | | | End of split % 94.48/13.24 | | | | | | | | % 94.48/13.24 | | | | | | | End of split % 94.48/13.24 | | | | | | | % 94.48/13.24 | | | | | | End of split % 94.48/13.24 | | | | | | % 94.48/13.24 | | | | | Case 2: % 94.48/13.24 | | | | | | % 94.48/13.24 | | | | | | (338) all_138_0 = all_42_2 % 94.48/13.24 | | | | | | % 94.48/13.24 | | | | | | REDUCE: (173), (338) imply: % 94.48/13.24 | | | | | | (339) $false % 94.48/13.24 | | | | | | % 94.48/13.24 | | | | | | CLOSE: (339) is inconsistent. % 94.48/13.24 | | | | | | % 94.48/13.24 | | | | | End of split % 94.48/13.24 | | | | | % 94.48/13.24 | | | | Case 2: % 94.48/13.24 | | | | | % 94.48/13.24 | | | | | (340) all_70_0 = all_54_3 % 94.48/13.24 | | | | | % 94.48/13.24 | | | | | COMBINE_EQS: (67), (340) imply: % 94.48/13.24 | | | | | (341) all_54_3 = all_42_2 % 94.48/13.24 | | | | | % 94.48/13.24 | | | | | SIMP: (341) implies: % 94.48/13.24 | | | | | (342) all_54_3 = all_42_2 % 94.48/13.24 | | | | | % 94.48/13.24 | | | | | REDUCE: (122), (342) imply: % 94.48/13.24 | | | | | (343) $false % 94.48/13.24 | | | | | % 94.48/13.24 | | | | | CLOSE: (343) is inconsistent. % 94.48/13.24 | | | | | % 94.48/13.24 | | | | End of split % 94.48/13.24 | | | | % 94.48/13.24 | | | End of split % 94.48/13.24 | | | % 94.48/13.24 | | End of split % 94.48/13.24 | | % 94.48/13.24 | End of split % 94.48/13.24 | % 94.48/13.24 End of proof % 94.48/13.24 % SZS output end Proof for theBenchmark % 94.48/13.24 % 94.48/13.24 12625ms %------------------------------------------------------------------------------