%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO001+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 : n010.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 154.96s 21.29s % Output : Proof 155.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PRO001+4 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Aug 28 19:08:19 EDT 2023 % 0.12/0.35 % CPUTime : % 0.19/0.66 ________ _____ % 0.19/0.66 ___ __ \_________(_)________________________________ % 0.19/0.66 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.66 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.66 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.66 % 0.19/0.66 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.66 (2023-06-19) % 0.19/0.66 % 0.19/0.66 (c) Philipp Rümmer, 2009-2023 % 0.19/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.66 Amanda Stjerna. % 0.19/0.66 Free software under BSD-3-Clause. % 0.19/0.66 % 0.19/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.66 % 0.19/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.67 Running up to 7 provers in parallel. % 0.19/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.42/1.27 Prover 1: Preprocessing ... % 3.42/1.27 Prover 4: Preprocessing ... % 3.64/1.31 Prover 2: Preprocessing ... % 3.64/1.31 Prover 5: Preprocessing ... % 3.64/1.31 Prover 6: Preprocessing ... % 3.64/1.31 Prover 0: Preprocessing ... % 3.64/1.31 Prover 3: Preprocessing ... % 7.09/1.78 Prover 2: Constructing countermodel ... % 7.09/1.79 Prover 5: Proving ... % 8.41/1.97 Prover 1: Constructing countermodel ... % 8.41/1.99 Prover 3: Constructing countermodel ... % 8.41/1.99 Prover 6: Proving ... % 10.73/2.28 Prover 4: Constructing countermodel ... % 10.73/2.31 Prover 0: Proving ... % 56.00/8.21 Prover 3: gave up % 56.00/8.21 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 56.62/8.33 Prover 7: Preprocessing ... % 56.62/8.44 Prover 7: Constructing countermodel ... % 71.46/10.18 Prover 2: stopped % 71.46/10.19 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 72.04/10.25 Prover 8: Preprocessing ... % 73.43/10.49 Prover 8: Warning: ignoring some quantifiers % 73.43/10.49 Prover 8: Constructing countermodel ... % 100.62/14.02 Prover 5: stopped % 100.62/14.02 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 100.62/14.05 Prover 9: Preprocessing ... % 102.43/14.27 Prover 9: Constructing countermodel ... % 114.74/16.05 Prover 1: stopped % 114.74/16.07 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 116.78/16.15 Prover 10: Preprocessing ... % 117.20/16.18 Prover 10: Constructing countermodel ... % 130.27/17.93 Prover 6: stopped % 130.27/17.93 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 130.97/18.02 Prover 11: Preprocessing ... % 132.64/18.20 Prover 11: Constructing countermodel ... % 154.65/21.23 Prover 10: Found proof (size 263) % 154.65/21.23 Prover 10: proved (5166ms) % 154.65/21.24 Prover 11: stopped % 154.65/21.24 Prover 7: stopped % 154.65/21.24 Prover 8: stopped % 154.65/21.24 Prover 4: stopped % 154.96/21.25 Prover 9: stopped % 154.96/21.29 Prover 0: stopped % 154.96/21.29 % 154.96/21.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 154.96/21.29 % 154.96/21.33 % SZS output start Proof for theBenchmark % 154.96/21.33 Assumptions after simplification: % 154.96/21.33 --------------------------------- % 154.96/21.33 % 154.96/21.33 (goals) % 154.96/21.34 $i(tptp0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 154.96/21.34 $i(v0) & tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 154.96/21.34 % 154.96/21.34 (sos) % 154.96/21.34 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 154.96/21.34 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 154.96/21.34 root(v2, v0))) % 154.96/21.34 % 154.96/21.34 (sos_01) % 154.96/21.34 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v4 = v2 % 154.96/21.34 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 154.96/21.34 min_precedes(v3, v2, v0) | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ % 154.96/21.34 subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v2, % 154.96/21.34 v4, v0)) % 154.96/21.34 % 154.96/21.34 (sos_03) % 155.17/21.34 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 155.17/21.34 | activity_occurrence(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 155.17/21.34 $i(v0) | ~ occurrence_of(v1, v0) | activity(v0)) % 155.17/21.34 % 155.17/21.34 (sos_05) % 155.17/21.35 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v1, v0) | ? [v2: % 155.17/21.35 $i] : ($i(v2) & atocc(v1, v2) & subactivity(v2, v0))) % 155.17/21.35 % 155.17/21.35 (sos_06) % 155.17/21.35 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.35 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 155.17/21.35 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 155.17/21.35 occurrence_of(v3, v0))) % 155.17/21.35 % 155.17/21.35 (sos_08) % 155.17/21.35 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 155.17/21.35 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 155.17/21.35 % 155.17/21.35 (sos_11) % 155.17/21.35 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.35 subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0: $i] : ! % 155.17/21.35 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v0, v1) | % 155.17/21.35 activity_occurrence(v0)) % 155.17/21.35 % 155.17/21.35 (sos_12) % 155.17/21.35 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 155.17/21.35 & activity(v1) & occurrence_of(v0, v1))) % 155.17/21.35 % 155.17/21.35 (sos_14) % 155.17/21.35 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.35 ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | % 155.17/21.35 atocc(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.35 atocc(v0, v1) | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 155.17/21.35 occurrence_of(v0, v2))) % 155.17/21.35 % 155.17/21.35 (sos_15) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.36 ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0: $i] : ! [v1: $i] : % 155.17/21.36 ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v2, v0, v1) % 155.17/21.36 | leaf(v0, v1) | ? [v3: $i] : ($i(v3) & min_precedes(v0, v3, v1))) & ! % 155.17/21.36 [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | root(v0, % 155.17/21.36 v1) | ? [v2: $i] : ($i(v2) & min_precedes(v2, v0, v1))) & ! [v0: $i] : % 155.17/21.36 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | leaf(v0, v1) | ? [v2: % 155.17/21.36 $i] : ($i(v2) & min_precedes(v0, v2, v1))) % 155.17/21.36 % 155.17/21.36 (sos_18) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.36 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 155.17/21.36 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 155.17/21.36 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 155.17/21.36 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 155.17/21.36 % 155.17/21.36 (sos_19) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.36 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 155.17/21.36 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 155.17/21.36 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 155.17/21.36 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 155.17/21.36 % 155.17/21.36 (sos_23) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.36 ~ min_precedes(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, % 155.17/21.36 v2) & root(v3, v2))) % 155.17/21.36 % 155.17/21.36 (sos_26) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 155.17/21.36 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 155.17/21.36 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 155.17/21.36 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 155.17/21.36 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 155.17/21.36 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 155.17/21.36 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 155.17/21.36 min_precedes(v0, v3, v2))) % 155.17/21.36 % 155.17/21.36 (sos_27) % 155.17/21.36 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 155.17/21.36 | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | ~ % 155.17/21.36 subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | % 155.17/21.36 subactivity_occurrence(v0, v3)) % 155.17/21.36 % 155.17/21.36 (sos_29) % 155.17/21.37 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 155.17/21.37 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 155.17/21.37 v2) | ~ occurrence_of(v2, v3)) % 155.17/21.37 % 155.17/21.37 (sos_32) % 155.17/21.37 $i(tptp2) & $i(tptp3) & $i(tptp4) & $i(tptp0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 155.17/21.37 occurrence_of(v0, tptp0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 155.17/21.37 next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & % 155.17/21.37 occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, % 155.17/21.37 tptp3)))) % 155.17/21.37 % 155.17/21.37 (sos_34) % 155.17/21.37 $i(tptp0) & ~ atomic(tptp0) % 155.17/21.37 % 155.17/21.37 (sos_46) % 155.17/21.37 $i(tptp2) & $i(tptp3) & $i(tptp4) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 155.17/21.37 ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.37 send_message(tptp2, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 155.17/21.37 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.37 send_message(tptp3, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 155.17/21.37 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.37 send_message(tptp4, v0, v1, v2, v3)) % 155.17/21.37 % 155.17/21.37 (sos_47) % 155.17/21.37 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 155.17/21.37 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 155.17/21.37 | ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | % 155.17/21.37 min_precedes(v3, v5, v4)) % 155.17/21.37 % 155.17/21.37 (sos_51) % 155.17/21.37 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 155.17/21.37 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 155.17/21.37 | ~ transmit_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | ? % 155.17/21.37 [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & send_message(v6, v1, v2, v3, v4) % 155.17/21.37 & root_occ(v7, v5) & occurrence_of(v7, v6))) % 155.17/21.37 % 155.17/21.37 (sos_52) % 155.17/21.37 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 155.17/21.37 ~ tptp1(v0, v1, v2) | ~ atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 155.17/21.37 $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ % 155.17/21.37 atomic(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ % 155.17/21.37 $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | activity(v0)) & ! [v0: $i] : ! % 155.17/21.37 [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, % 155.17/21.37 v2) | root(v2, v1)) % 155.17/21.37 % 155.17/21.37 (sos_53) % 155.17/21.37 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 155.17/21.37 | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | % 155.17/21.37 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & % 155.17/21.37 $i(v5) & $i(v4) & transmit_message(v4, v5, v6, v2, v1) & % 155.17/21.37 subactivity_occurrence(v7, v3) & occurrence_of(v7, v4))) % 155.17/21.37 % 155.17/21.37 Further assumptions not needed in the proof: % 155.17/21.37 -------------------------------------------- % 155.17/21.38 sos_02, sos_04, sos_07, sos_09, sos_10, sos_13, sos_16, sos_17, sos_20, sos_21, % 155.17/21.38 sos_22, sos_24, sos_25, sos_28, sos_30, sos_31, sos_33, sos_35, sos_36, sos_37, % 155.17/21.38 sos_38, sos_39, sos_40, sos_41, sos_42, sos_43, sos_44, sos_45, sos_48, sos_49, % 155.17/21.38 sos_50, sos_54 % 155.17/21.38 % 155.17/21.38 Those formulas are unsatisfiable: % 155.17/21.38 --------------------------------- % 155.17/21.38 % 155.17/21.38 Begin of proof % 155.17/21.38 | % 155.17/21.38 | ALPHA: (goals) implies: % 155.17/21.38 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 155.17/21.38 | tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_52) implies: % 155.17/21.38 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 155.17/21.38 | $i(v0) | ~ tptp1(v0, v1, v2) | root(v2, v1)) % 155.17/21.38 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 155.17/21.38 | $i(v0) | ~ tptp1(v0, v1, v2) | ~ atomic(v0)) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_46) implies: % 155.17/21.38 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 155.17/21.38 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp3, v0, v1, v2, % 155.17/21.38 | v3)) % 155.17/21.38 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 155.17/21.38 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp2, v0, v1, v2, % 155.17/21.38 | v3)) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_34) implies: % 155.17/21.38 | (6) ~ atomic(tptp0) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_32) implies: % 155.17/21.38 | (7) $i(tptp0) % 155.17/21.38 | (8) $i(tptp3) % 155.17/21.38 | (9) $i(tptp2) % 155.17/21.38 | (10) ! [v0: $i] : ( ~ $i(v0) | ~ occurrence_of(v0, tptp0) | ? [v1: $i] : % 155.17/21.38 | ? [v2: $i] : ($i(v2) & $i(v1) & next_subocc(v1, v2, tptp0) & % 155.17/21.38 | leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & % 155.17/21.38 | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_26) implies: % 155.17/21.38 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 155.17/21.38 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 155.17/21.38 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 155.17/21.38 | % 155.17/21.38 | ALPHA: (sos_19) implies: % 155.17/21.38 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 155.17/21.38 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 155.17/21.38 | root(v0, v2) & occurrence_of(v1, v2))) % 155.17/21.39 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 155.17/21.39 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 155.17/21.39 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (sos_18) implies: % 155.17/21.39 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 155.17/21.39 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 155.17/21.39 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (sos_15) implies: % 155.17/21.39 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 155.17/21.39 | $i(v0) | ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3: $i] : % 155.17/21.39 | ($i(v3) & min_precedes(v0, v3, v1))) % 155.17/21.39 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 155.17/21.39 | $i(v0) | ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (sos_14) implies: % 155.17/21.39 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) % 155.17/21.39 | | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 155.17/21.39 | occurrence_of(v0, v2))) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (sos_11) implies: % 155.17/21.39 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.39 | subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 155.17/21.39 | (19) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.39 | subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (sos_03) implies: % 155.17/21.39 | (20) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 155.17/21.39 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 155.17/21.39 | % 155.17/21.39 | DELTA: instantiating (1) with fresh symbols all_46_0, all_46_1, all_46_2 % 155.17/21.39 | gives: % 155.17/21.39 | (21) $i(all_46_0) & $i(all_46_1) & $i(all_46_2) & tptp1(all_46_2, tptp0, % 155.17/21.39 | all_46_1) & occurrence_of(all_46_0, all_46_2) % 155.17/21.39 | % 155.17/21.39 | ALPHA: (21) implies: % 155.17/21.39 | (22) occurrence_of(all_46_0, all_46_2) % 155.17/21.39 | (23) tptp1(all_46_2, tptp0, all_46_1) % 155.17/21.39 | (24) $i(all_46_2) % 155.17/21.39 | (25) $i(all_46_1) % 155.17/21.39 | (26) $i(all_46_0) % 155.17/21.39 | % 155.17/21.39 | GROUND_INST: instantiating (20) with all_46_2, all_46_0, simplifying with % 155.17/21.39 | (22), (24), (26) gives: % 155.17/21.39 | (27) activity_occurrence(all_46_0) % 155.17/21.39 | % 155.17/21.39 | GROUND_INST: instantiating (sos) with all_46_2, all_46_0, simplifying with % 155.17/21.39 | (22), (24), (26) gives: % 155.17/21.39 | (28) atomic(all_46_2) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 155.17/21.39 | all_46_0) & root(v0, all_46_2)) % 155.17/21.39 | % 155.17/21.39 | GROUND_INST: instantiating (sos_53) with all_46_2, tptp0, all_46_1, all_46_0, % 155.17/21.39 | simplifying with (7), (22), (23), (24), (25), (26) gives: % 155.17/21.39 | (29) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ($i(v3) & % 155.17/21.40 | $i(v2) & $i(v1) & $i(v0) & transmit_message(v0, v1, v2, all_46_1, % 155.17/21.40 | tptp0) & subactivity_occurrence(v3, all_46_0) & occurrence_of(v3, % 155.17/21.40 | v0)) % 155.17/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (2) with all_46_2, tptp0, all_46_1, simplifying % 155.40/21.40 | with (7), (23), (24), (25) gives: % 155.40/21.40 | (30) root(all_46_1, tptp0) % 155.40/21.40 | % 155.40/21.40 | DELTA: instantiating (29) with fresh symbols all_54_0, all_54_1, all_54_2, % 155.40/21.40 | all_54_3 gives: % 155.40/21.40 | (31) $i(all_54_0) & $i(all_54_1) & $i(all_54_2) & $i(all_54_3) & % 155.40/21.40 | transmit_message(all_54_3, all_54_2, all_54_1, all_46_1, tptp0) & % 155.40/21.40 | subactivity_occurrence(all_54_0, all_46_0) & occurrence_of(all_54_0, % 155.40/21.40 | all_54_3) % 155.40/21.40 | % 155.40/21.40 | ALPHA: (31) implies: % 155.40/21.40 | (32) occurrence_of(all_54_0, all_54_3) % 155.40/21.40 | (33) transmit_message(all_54_3, all_54_2, all_54_1, all_46_1, tptp0) % 155.40/21.40 | (34) $i(all_54_3) % 155.40/21.40 | (35) $i(all_54_2) % 155.40/21.40 | (36) $i(all_54_1) % 155.40/21.40 | (37) $i(all_54_0) % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (sos_12) with all_46_0, simplifying with (26), (27) % 155.40/21.40 | gives: % 155.40/21.40 | (38) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_46_0, v0)) % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (sos_51) with all_54_3, all_54_2, all_54_1, % 155.40/21.40 | all_46_1, tptp0, all_54_0, simplifying with (7), (25), (32), % 155.40/21.40 | (33), (34), (35), (36), (37) gives: % 155.40/21.40 | (39) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & send_message(v0, % 155.40/21.40 | all_54_2, all_54_1, all_46_1, tptp0) & root_occ(v1, all_54_0) & % 155.40/21.40 | occurrence_of(v1, v0)) % 155.40/21.40 | % 155.40/21.40 | DELTA: instantiating (38) with fresh symbol all_64_0 gives: % 155.40/21.40 | (40) $i(all_64_0) & activity(all_64_0) & occurrence_of(all_46_0, all_64_0) % 155.40/21.40 | % 155.40/21.40 | ALPHA: (40) implies: % 155.40/21.40 | (41) occurrence_of(all_46_0, all_64_0) % 155.40/21.40 | (42) $i(all_64_0) % 155.40/21.40 | % 155.40/21.40 | DELTA: instantiating (39) with fresh symbols all_66_0, all_66_1 gives: % 155.40/21.40 | (43) $i(all_66_0) & $i(all_66_1) & send_message(all_66_1, all_54_2, % 155.40/21.40 | all_54_1, all_46_1, tptp0) & root_occ(all_66_0, all_54_0) & % 155.40/21.40 | occurrence_of(all_66_0, all_66_1) % 155.40/21.40 | % 155.40/21.40 | ALPHA: (43) implies: % 155.40/21.40 | (44) occurrence_of(all_66_0, all_66_1) % 155.40/21.40 | (45) root_occ(all_66_0, all_54_0) % 155.40/21.40 | (46) send_message(all_66_1, all_54_2, all_54_1, all_46_1, tptp0) % 155.40/21.40 | (47) $i(all_66_1) % 155.40/21.40 | (48) $i(all_66_0) % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (sos_08) with all_46_0, all_46_2, all_64_0, % 155.40/21.40 | simplifying with (22), (24), (26), (41), (42) gives: % 155.40/21.40 | (49) all_64_0 = all_46_2 % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (20) with all_66_1, all_66_0, simplifying with % 155.40/21.40 | (44), (47), (48) gives: % 155.40/21.40 | (50) activity_occurrence(all_66_0) % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (12) with all_66_0, all_54_0, simplifying with % 155.40/21.40 | (37), (45), (48) gives: % 155.40/21.40 | (51) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_66_0, all_54_0) & % 155.40/21.40 | root(all_66_0, v0) & occurrence_of(all_54_0, v0)) % 155.40/21.40 | % 155.40/21.40 | GROUND_INST: instantiating (sos_47) with all_66_1, all_54_2, all_54_1, % 155.40/21.40 | all_46_1, tptp0, all_66_0, simplifying with (7), (25), (35), % 155.40/21.40 | (36), (44), (46), (47), (48) gives: % 155.40/21.40 | (52) min_precedes(all_46_1, all_66_0, tptp0) % 155.40/21.40 | % 155.40/21.40 | DELTA: instantiating (51) with fresh symbol all_78_0 gives: % 155.40/21.40 | (53) $i(all_78_0) & subactivity_occurrence(all_66_0, all_54_0) & % 155.40/21.40 | root(all_66_0, all_78_0) & occurrence_of(all_54_0, all_78_0) % 155.40/21.40 | % 155.40/21.40 | ALPHA: (53) implies: % 155.40/21.40 | (54) root(all_66_0, all_78_0) % 155.40/21.41 | (55) $i(all_78_0) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos_05) with all_78_0, all_66_0, simplifying with % 155.40/21.41 | (48), (54), (55) gives: % 155.40/21.41 | (56) ? [v0: $i] : ($i(v0) & atocc(all_66_0, v0) & subactivity(v0, % 155.40/21.41 | all_78_0)) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos_06) with tptp0, all_46_1, all_66_0, % 155.40/21.41 | simplifying with (7), (25), (48), (52) gives: % 155.40/21.41 | (57) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_66_0, v0) & % 155.40/21.41 | subactivity_occurrence(all_46_1, v0) & occurrence_of(v0, tptp0)) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos_23) with all_46_1, all_66_0, tptp0, % 155.40/21.41 | simplifying with (7), (25), (48), (52) gives: % 155.40/21.41 | (58) ? [v0: $i] : ($i(v0) & min_precedes(v0, all_66_0, tptp0) & root(v0, % 155.40/21.41 | tptp0)) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos_12) with all_66_0, simplifying with (48), (50) % 155.40/21.41 | gives: % 155.40/21.41 | (59) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_66_0, v0)) % 155.40/21.41 | % 155.40/21.41 | DELTA: instantiating (56) with fresh symbol all_88_0 gives: % 155.40/21.41 | (60) $i(all_88_0) & atocc(all_66_0, all_88_0) & subactivity(all_88_0, % 155.40/21.41 | all_78_0) % 155.40/21.41 | % 155.40/21.41 | ALPHA: (60) implies: % 155.40/21.41 | (61) atocc(all_66_0, all_88_0) % 155.40/21.41 | (62) $i(all_88_0) % 155.40/21.41 | % 155.40/21.41 | DELTA: instantiating (59) with fresh symbol all_90_0 gives: % 155.40/21.41 | (63) $i(all_90_0) & activity(all_90_0) & occurrence_of(all_66_0, all_90_0) % 155.40/21.41 | % 155.40/21.41 | ALPHA: (63) implies: % 155.40/21.41 | (64) occurrence_of(all_66_0, all_90_0) % 155.40/21.41 | (65) $i(all_90_0) % 155.40/21.41 | % 155.40/21.41 | DELTA: instantiating (58) with fresh symbol all_92_0 gives: % 155.40/21.41 | (66) $i(all_92_0) & min_precedes(all_92_0, all_66_0, tptp0) & % 155.40/21.41 | root(all_92_0, tptp0) % 155.40/21.41 | % 155.40/21.41 | ALPHA: (66) implies: % 155.40/21.41 | (67) root(all_92_0, tptp0) % 155.40/21.41 | (68) min_precedes(all_92_0, all_66_0, tptp0) % 155.40/21.41 | (69) $i(all_92_0) % 155.40/21.41 | % 155.40/21.41 | DELTA: instantiating (57) with fresh symbol all_96_0 gives: % 155.40/21.41 | (70) $i(all_96_0) & subactivity_occurrence(all_66_0, all_96_0) & % 155.40/21.41 | subactivity_occurrence(all_46_1, all_96_0) & occurrence_of(all_96_0, % 155.40/21.41 | tptp0) % 155.40/21.41 | % 155.40/21.41 | ALPHA: (70) implies: % 155.40/21.41 | (71) occurrence_of(all_96_0, tptp0) % 155.40/21.41 | (72) subactivity_occurrence(all_46_1, all_96_0) % 155.40/21.41 | (73) subactivity_occurrence(all_66_0, all_96_0) % 155.40/21.41 | (74) $i(all_96_0) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos_08) with all_66_0, all_66_1, all_90_0, % 155.40/21.41 | simplifying with (44), (47), (48), (64), (65) gives: % 155.40/21.41 | (75) all_90_0 = all_66_1 % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (10) with all_96_0, simplifying with (71), (74) % 155.40/21.41 | gives: % 155.40/21.41 | (76) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & next_subocc(v0, v1, % 155.40/21.41 | tptp0) & leaf_occ(v1, all_96_0) & root_occ(v0, all_96_0) & % 155.40/21.41 | occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | % 155.40/21.41 | occurrence_of(v1, tptp3))) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (sos) with tptp0, all_96_0, simplifying with (6), % 155.40/21.41 | (7), (71), (74) gives: % 155.40/21.41 | (77) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_96_0) & % 155.40/21.41 | root(v0, tptp0)) % 155.40/21.41 | % 155.40/21.41 | GROUND_INST: instantiating (13) with all_46_1, all_96_0, tptp0, simplifying % 155.40/21.41 | with (7), (25), (30), (71), (72), (74) gives: % 155.40/21.41 | (78) root_occ(all_46_1, all_96_0) % 155.40/21.41 | % 155.40/21.42 | GROUND_INST: instantiating (19) with all_66_0, all_96_0, simplifying with % 155.40/21.42 | (48), (73), (74) gives: % 155.40/21.42 | (79) activity_occurrence(all_96_0) % 155.40/21.42 | % 155.40/21.42 | GROUND_INST: instantiating (sos_27) with all_92_0, all_66_0, tptp0, all_96_0, % 155.40/21.42 | simplifying with (7), (48), (68), (69), (71), (73), (74) gives: % 155.40/21.42 | (80) subactivity_occurrence(all_92_0, all_96_0) % 155.40/21.42 | % 155.40/21.42 | GROUND_INST: instantiating (sos_06) with tptp0, all_92_0, all_66_0, % 155.40/21.42 | simplifying with (7), (48), (68), (69) gives: % 155.40/21.42 | (81) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_92_0, v0) & % 155.40/21.42 | subactivity_occurrence(all_66_0, v0) & occurrence_of(v0, tptp0)) % 155.40/21.42 | % 155.40/21.42 | GROUND_INST: instantiating (17) with all_66_0, all_88_0, simplifying with % 155.40/21.42 | (48), (61), (62) gives: % 155.40/21.42 | (82) ? [v0: $i] : ($i(v0) & subactivity(all_88_0, v0) & atomic(v0) & % 155.40/21.42 | occurrence_of(all_66_0, v0)) % 155.40/21.42 | % 155.40/21.42 | DELTA: instantiating (58) with fresh symbol all_106_0 gives: % 155.40/21.42 | (83) $i(all_106_0) & min_precedes(all_106_0, all_66_0, tptp0) & % 155.40/21.42 | root(all_106_0, tptp0) % 155.40/21.42 | % 155.40/21.42 | ALPHA: (83) implies: % 155.40/21.42 | (84) root(all_106_0, tptp0) % 155.40/21.42 | (85) min_precedes(all_106_0, all_66_0, tptp0) % 155.40/21.42 | (86) $i(all_106_0) % 155.40/21.42 | % 155.40/21.42 | DELTA: instantiating (77) with fresh symbol all_110_0 gives: % 155.40/21.42 | (87) $i(all_110_0) & subactivity_occurrence(all_110_0, all_96_0) & % 155.40/21.42 | root(all_110_0, tptp0) % 155.40/21.42 | % 155.40/21.42 | ALPHA: (87) implies: % 155.40/21.42 | (88) root(all_110_0, tptp0) % 155.40/21.42 | (89) subactivity_occurrence(all_110_0, all_96_0) % 155.40/21.42 | (90) $i(all_110_0) % 155.40/21.42 | % 155.40/21.42 | DELTA: instantiating (82) with fresh symbol all_112_0 gives: % 155.40/21.42 | (91) $i(all_112_0) & subactivity(all_88_0, all_112_0) & atomic(all_112_0) & % 155.40/21.42 | occurrence_of(all_66_0, all_112_0) % 155.40/21.42 | % 155.40/21.42 | ALPHA: (91) implies: % 155.40/21.42 | (92) occurrence_of(all_66_0, all_112_0) % 155.40/21.42 | (93) $i(all_112_0) % 155.40/21.42 | % 155.40/21.42 | DELTA: instantiating (81) with fresh symbol all_114_0 gives: % 155.40/21.42 | (94) $i(all_114_0) & subactivity_occurrence(all_92_0, all_114_0) & % 155.40/21.42 | subactivity_occurrence(all_66_0, all_114_0) & occurrence_of(all_114_0, % 155.40/21.42 | tptp0) % 155.40/21.42 | % 155.40/21.42 | ALPHA: (94) implies: % 155.40/21.42 | (95) occurrence_of(all_114_0, tptp0) % 155.40/21.42 | (96) subactivity_occurrence(all_66_0, all_114_0) % 155.40/21.42 | (97) subactivity_occurrence(all_92_0, all_114_0) % 155.40/21.42 | (98) $i(all_114_0) % 155.40/21.42 | % 155.40/21.42 | DELTA: instantiating (76) with fresh symbols all_116_0, all_116_1 gives: % 155.40/21.42 | (99) $i(all_116_0) & $i(all_116_1) & next_subocc(all_116_1, all_116_0, % 155.40/21.42 | tptp0) & leaf_occ(all_116_0, all_96_0) & root_occ(all_116_1, % 155.40/21.42 | all_96_0) & occurrence_of(all_116_1, tptp4) & % 155.40/21.42 | (occurrence_of(all_116_0, tptp2) | occurrence_of(all_116_0, tptp3)) % 155.40/21.42 | % 155.40/21.42 | ALPHA: (99) implies: % 155.40/21.42 | (100) root_occ(all_116_1, all_96_0) % 155.40/21.42 | (101) leaf_occ(all_116_0, all_96_0) % 155.40/21.42 | (102) next_subocc(all_116_1, all_116_0, tptp0) % 155.40/21.42 | (103) $i(all_116_1) % 155.40/21.42 | (104) $i(all_116_0) % 155.40/21.42 | (105) occurrence_of(all_116_0, tptp2) | occurrence_of(all_116_0, tptp3) % 155.40/21.42 | % 155.40/21.42 | GROUND_INST: instantiating (sos_08) with all_66_0, all_66_1, all_112_0, % 155.40/21.42 | simplifying with (44), (47), (48), (92), (93) gives: % 155.40/21.42 | (106) all_112_0 = all_66_1 % 155.40/21.42 | % 155.40/21.42 | GROUND_INST: instantiating (10) with all_114_0, simplifying with (95), (98) % 155.40/21.42 | gives: % 155.40/21.42 | (107) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & next_subocc(v0, v1, % 155.40/21.42 | tptp0) & leaf_occ(v1, all_114_0) & root_occ(v0, all_114_0) & % 155.40/21.42 | occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | % 155.40/21.42 | occurrence_of(v1, tptp3))) % 155.40/21.42 | % 155.40/21.43 | GROUND_INST: instantiating (sos) with tptp0, all_114_0, simplifying with (6), % 155.40/21.43 | (7), (95), (98) gives: % 155.40/21.43 | (108) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_114_0) & % 155.40/21.43 | root(v0, tptp0)) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (13) with all_92_0, all_96_0, tptp0, simplifying % 155.40/21.43 | with (7), (67), (69), (71), (74), (80) gives: % 155.40/21.43 | (109) root_occ(all_92_0, all_96_0) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (13) with all_92_0, all_114_0, tptp0, simplifying % 155.40/21.43 | with (7), (67), (69), (95), (97), (98) gives: % 155.40/21.43 | (110) root_occ(all_92_0, all_114_0) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (19) with all_92_0, all_114_0, simplifying with % 155.40/21.43 | (69), (97), (98) gives: % 155.40/21.43 | (111) activity_occurrence(all_114_0) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (13) with all_110_0, all_96_0, tptp0, simplifying % 155.40/21.43 | with (7), (71), (74), (88), (89), (90) gives: % 155.40/21.43 | (112) root_occ(all_110_0, all_96_0) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (12) with all_46_1, all_96_0, simplifying with % 155.40/21.43 | (25), (74), (78) gives: % 155.40/21.43 | (113) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_46_1, all_96_0) & % 155.40/21.43 | root(all_46_1, v0) & occurrence_of(all_96_0, v0)) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (sos_29) with all_46_1, all_116_1, all_96_0, tptp0, % 155.40/21.43 | simplifying with (7), (25), (71), (74), (78), (100), (103) gives: % 155.40/21.43 | (114) all_116_1 = all_46_1 % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (12) with all_116_1, all_96_0, simplifying with % 155.40/21.43 | (74), (100), (103) gives: % 155.40/21.43 | (115) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_116_1, all_96_0) & % 155.40/21.43 | root(all_116_1, v0) & occurrence_of(all_96_0, v0)) % 155.40/21.43 | % 155.40/21.43 | GROUND_INST: instantiating (14) with all_116_0, all_96_0, simplifying with % 155.40/21.43 | (74), (101), (104) gives: % 155.40/21.43 | (116) ? [v0: $i] : ($i(v0) & leaf(all_116_0, v0) & % 155.40/21.43 | subactivity_occurrence(all_116_0, all_96_0) & % 155.40/21.43 | occurrence_of(all_96_0, v0)) % 155.40/21.43 | % 155.40/21.44 | GROUND_INST: instantiating (sos_27) with all_106_0, all_66_0, tptp0, all_96_0, % 155.40/21.44 | simplifying with (7), (48), (71), (73), (74), (85), (86) gives: % 155.40/21.44 | (117) subactivity_occurrence(all_106_0, all_96_0) % 155.40/21.44 | % 155.40/21.44 | GROUND_INST: instantiating (sos_27) with all_106_0, all_66_0, tptp0, % 155.40/21.44 | all_114_0, simplifying with (7), (48), (85), (86), (95), (96), % 155.40/21.44 | (98) gives: % 155.40/21.44 | (118) subactivity_occurrence(all_106_0, all_114_0) % 155.40/21.44 | % 155.40/21.44 | GROUND_INST: instantiating (sos_06) with tptp0, all_106_0, all_66_0, % 155.40/21.44 | simplifying with (7), (48), (85), (86) gives: % 155.40/21.44 | (119) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_106_0, v0) & % 155.40/21.44 | subactivity_occurrence(all_66_0, v0) & occurrence_of(v0, tptp0)) % 155.40/21.44 | % 155.40/21.44 | GROUND_INST: instantiating (sos_12) with all_96_0, simplifying with (74), (79) % 155.40/21.44 | gives: % 155.40/21.44 | (120) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_96_0, v0)) % 155.40/21.44 | % 155.40/21.44 | DELTA: instantiating (58) with fresh symbol all_128_0 gives: % 155.40/21.44 | (121) $i(all_128_0) & min_precedes(all_128_0, all_66_0, tptp0) & % 155.40/21.44 | root(all_128_0, tptp0) % 155.40/21.44 | % 155.40/21.44 | ALPHA: (121) implies: % 155.40/21.44 | (122) root(all_128_0, tptp0) % 155.40/21.44 | (123) min_precedes(all_128_0, all_66_0, tptp0) % 155.40/21.44 | (124) $i(all_128_0) % 155.40/21.44 | % 155.40/21.44 | DELTA: instantiating (108) with fresh symbol all_130_0 gives: % 155.40/21.44 | (125) $i(all_130_0) & subactivity_occurrence(all_130_0, all_114_0) & % 155.40/21.44 | root(all_130_0, tptp0) % 155.40/21.44 | % 155.40/21.44 | ALPHA: (125) implies: % 155.40/21.44 | (126) root(all_130_0, tptp0) % 155.40/21.44 | (127) subactivity_occurrence(all_130_0, all_114_0) % 155.40/21.44 | (128) $i(all_130_0) % 155.40/21.44 | % 155.40/21.44 | DELTA: instantiating (120) with fresh symbol all_132_0 gives: % 155.40/21.44 | (129) $i(all_132_0) & activity(all_132_0) & occurrence_of(all_96_0, % 155.40/21.44 | all_132_0) % 155.40/21.44 | % 155.40/21.44 | ALPHA: (129) implies: % 155.40/21.44 | (130) occurrence_of(all_96_0, all_132_0) % 155.40/21.44 | (131) $i(all_132_0) % 155.40/21.44 | % 155.40/21.44 | DELTA: instantiating (113) with fresh symbol all_136_0 gives: % 155.40/21.44 | (132) $i(all_136_0) & subactivity_occurrence(all_46_1, all_96_0) & % 155.40/21.44 | root(all_46_1, all_136_0) & occurrence_of(all_96_0, all_136_0) % 155.40/21.44 | % 155.40/21.44 | ALPHA: (132) implies: % 155.69/21.45 | (133) occurrence_of(all_96_0, all_136_0) % 155.69/21.45 | (134) $i(all_136_0) % 155.69/21.45 | % 155.69/21.45 | DELTA: instantiating (119) with fresh symbol all_138_0 gives: % 155.69/21.45 | (135) $i(all_138_0) & subactivity_occurrence(all_106_0, all_138_0) & % 155.69/21.45 | subactivity_occurrence(all_66_0, all_138_0) & % 155.69/21.45 | occurrence_of(all_138_0, tptp0) % 155.69/21.45 | % 155.69/21.45 | ALPHA: (135) implies: % 155.69/21.45 | (136) occurrence_of(all_138_0, tptp0) % 155.69/21.45 | (137) subactivity_occurrence(all_66_0, all_138_0) % 155.69/21.45 | (138) subactivity_occurrence(all_106_0, all_138_0) % 155.69/21.45 | (139) $i(all_138_0) % 155.69/21.45 | % 155.69/21.45 | DELTA: instantiating (115) with fresh symbol all_142_0 gives: % 155.69/21.45 | (140) $i(all_142_0) & subactivity_occurrence(all_116_1, all_96_0) & % 155.69/21.45 | root(all_116_1, all_142_0) & occurrence_of(all_96_0, all_142_0) % 155.69/21.45 | % 155.69/21.45 | ALPHA: (140) implies: % 155.69/21.45 | (141) occurrence_of(all_96_0, all_142_0) % 155.69/21.45 | (142) $i(all_142_0) % 155.69/21.45 | % 155.69/21.45 | DELTA: instantiating (116) with fresh symbol all_144_0 gives: % 155.69/21.45 | (143) $i(all_144_0) & leaf(all_116_0, all_144_0) & % 155.69/21.45 | subactivity_occurrence(all_116_0, all_96_0) & occurrence_of(all_96_0, % 155.69/21.46 | all_144_0) % 155.69/21.46 | % 155.69/21.46 | ALPHA: (143) implies: % 155.69/21.46 | (144) occurrence_of(all_96_0, all_144_0) % 155.69/21.46 | (145) subactivity_occurrence(all_116_0, all_96_0) % 155.69/21.46 | (146) leaf(all_116_0, all_144_0) % 155.69/21.46 | (147) $i(all_144_0) % 155.69/21.46 | % 155.69/21.46 | DELTA: instantiating (107) with fresh symbols all_146_0, all_146_1 gives: % 155.69/21.46 | (148) $i(all_146_0) & $i(all_146_1) & next_subocc(all_146_1, all_146_0, % 155.69/21.46 | tptp0) & leaf_occ(all_146_0, all_114_0) & root_occ(all_146_1, % 155.69/21.46 | all_114_0) & occurrence_of(all_146_1, tptp4) & % 155.69/21.46 | (occurrence_of(all_146_0, tptp2) | occurrence_of(all_146_0, tptp3)) % 155.69/21.46 | % 155.69/21.46 | ALPHA: (148) implies: % 155.69/21.46 | (149) root_occ(all_146_1, all_114_0) % 155.69/21.46 | (150) leaf_occ(all_146_0, all_114_0) % 155.69/21.46 | (151) $i(all_146_1) % 155.69/21.46 | (152) $i(all_146_0) % 155.69/21.46 | % 155.69/21.46 | REDUCE: (102), (114) imply: % 155.69/21.46 | (153) next_subocc(all_46_1, all_116_0, tptp0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (sos_08) with all_96_0, tptp0, all_136_0, % 155.69/21.46 | simplifying with (7), (71), (74), (133), (134) gives: % 155.69/21.46 | (154) all_136_0 = tptp0 % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (sos_08) with all_96_0, all_136_0, all_142_0, % 155.69/21.46 | simplifying with (74), (133), (134), (141), (142) gives: % 155.69/21.46 | (155) all_142_0 = all_136_0 % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (sos_08) with all_96_0, all_142_0, all_144_0, % 155.69/21.46 | simplifying with (74), (141), (142), (144), (147) gives: % 155.69/21.46 | (156) all_144_0 = all_142_0 % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (sos_08) with all_96_0, all_132_0, all_144_0, % 155.69/21.46 | simplifying with (74), (130), (131), (144), (147) gives: % 155.69/21.46 | (157) all_144_0 = all_132_0 % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (10) with all_138_0, simplifying with (136), (139) % 155.69/21.46 | gives: % 155.69/21.46 | (158) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & next_subocc(v0, v1, % 155.69/21.46 | tptp0) & leaf_occ(v1, all_138_0) & root_occ(v0, all_138_0) & % 155.69/21.46 | occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | % 155.69/21.46 | occurrence_of(v1, tptp3))) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (sos) with tptp0, all_138_0, simplifying with (6), % 155.69/21.46 | (7), (136), (139) gives: % 155.69/21.46 | (159) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_138_0) & % 155.69/21.46 | root(v0, tptp0)) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (13) with all_106_0, all_96_0, tptp0, simplifying % 155.69/21.46 | with (7), (71), (74), (84), (86), (117) gives: % 155.69/21.46 | (160) root_occ(all_106_0, all_96_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (13) with all_106_0, all_114_0, tptp0, simplifying % 155.69/21.46 | with (7), (84), (86), (95), (98), (118) gives: % 155.69/21.46 | (161) root_occ(all_106_0, all_114_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (13) with all_106_0, all_138_0, tptp0, simplifying % 155.69/21.46 | with (7), (84), (86), (136), (138), (139) gives: % 155.69/21.46 | (162) root_occ(all_106_0, all_138_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (19) with all_106_0, all_138_0, simplifying with % 155.69/21.46 | (86), (138), (139) gives: % 155.69/21.46 | (163) activity_occurrence(all_138_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (18) with all_116_0, all_96_0, simplifying with % 155.69/21.46 | (74), (104), (145) gives: % 155.69/21.46 | (164) activity_occurrence(all_116_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (13) with all_130_0, all_114_0, tptp0, simplifying % 155.69/21.46 | with (7), (95), (98), (126), (127), (128) gives: % 155.69/21.46 | (165) root_occ(all_130_0, all_114_0) % 155.69/21.46 | % 155.69/21.46 | GROUND_INST: instantiating (12) with all_92_0, all_114_0, simplifying with % 155.69/21.46 | (69), (98), (110) gives: % 155.69/21.47 | (166) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_92_0, all_114_0) & % 155.69/21.47 | root(all_92_0, v0) & occurrence_of(all_114_0, v0)) % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (sos_29) with all_46_1, all_110_0, all_96_0, % 155.69/21.47 | all_132_0, simplifying with (25), (74), (78), (90), (112), (130), % 155.69/21.47 | (131) gives: % 155.69/21.47 | (167) all_110_0 = all_46_1 % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (sos_29) with all_92_0, all_110_0, all_96_0, % 155.69/21.47 | all_132_0, simplifying with (69), (74), (90), (109), (112), % 155.69/21.47 | (130), (131) gives: % 155.69/21.47 | (168) all_110_0 = all_92_0 % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (12) with all_146_1, all_114_0, simplifying with % 155.69/21.47 | (98), (149), (151) gives: % 155.69/21.47 | (169) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_146_1, all_114_0) % 155.69/21.47 | & root(all_146_1, v0) & occurrence_of(all_114_0, v0)) % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (14) with all_146_0, all_114_0, simplifying with % 155.69/21.47 | (98), (150), (152) gives: % 155.69/21.47 | (170) ? [v0: $i] : ($i(v0) & leaf(all_146_0, v0) & % 155.69/21.47 | subactivity_occurrence(all_146_0, all_114_0) & % 155.69/21.47 | occurrence_of(all_114_0, v0)) % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (sos_27) with all_128_0, all_66_0, tptp0, % 155.69/21.47 | all_138_0, simplifying with (7), (48), (123), (124), (136), % 155.69/21.47 | (137), (139) gives: % 155.69/21.47 | (171) subactivity_occurrence(all_128_0, all_138_0) % 155.69/21.47 | % 155.69/21.47 | GROUND_INST: instantiating (sos_12) with all_114_0, simplifying with (98), % 155.69/21.47 | (111) gives: % 155.69/21.47 | (172) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_114_0, v0)) % 155.69/21.47 | % 155.69/21.47 | COMBINE_EQS: (156), (157) imply: % 155.69/21.47 | (173) all_142_0 = all_132_0 % 155.69/21.47 | % 155.69/21.47 | SIMP: (173) implies: % 155.69/21.47 | (174) all_142_0 = all_132_0 % 155.69/21.47 | % 155.69/21.47 | COMBINE_EQS: (155), (174) imply: % 155.69/21.47 | (175) all_136_0 = all_132_0 % 155.69/21.47 | % 155.69/21.47 | SIMP: (175) implies: % 155.69/21.47 | (176) all_136_0 = all_132_0 % 155.69/21.47 | % 155.69/21.47 | COMBINE_EQS: (154), (176) imply: % 155.69/21.47 | (177) all_132_0 = tptp0 % 155.69/21.47 | % 155.69/21.47 | COMBINE_EQS: (167), (168) imply: % 155.69/21.47 | (178) all_92_0 = all_46_1 % 155.69/21.47 | % 155.69/21.47 | SIMP: (178) implies: % 155.69/21.47 | (179) all_92_0 = all_46_1 % 155.69/21.47 | % 155.69/21.47 | COMBINE_EQS: (157), (177) imply: % 155.69/21.47 | (180) all_144_0 = tptp0 % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (58) with fresh symbol all_154_0 gives: % 155.69/21.47 | (181) $i(all_154_0) & min_precedes(all_154_0, all_66_0, tptp0) & % 155.69/21.47 | root(all_154_0, tptp0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (181) implies: % 155.69/21.47 | (182) min_precedes(all_154_0, all_66_0, tptp0) % 155.69/21.47 | (183) $i(all_154_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (159) with fresh symbol all_164_0 gives: % 155.69/21.47 | (184) $i(all_164_0) & subactivity_occurrence(all_164_0, all_138_0) & % 155.69/21.47 | root(all_164_0, tptp0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (184) implies: % 155.69/21.47 | (185) root(all_164_0, tptp0) % 155.69/21.47 | (186) subactivity_occurrence(all_164_0, all_138_0) % 155.69/21.47 | (187) $i(all_164_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (172) with fresh symbol all_168_0 gives: % 155.69/21.47 | (188) $i(all_168_0) & activity(all_168_0) & occurrence_of(all_114_0, % 155.69/21.47 | all_168_0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (188) implies: % 155.69/21.47 | (189) occurrence_of(all_114_0, all_168_0) % 155.69/21.47 | (190) $i(all_168_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (170) with fresh symbol all_180_0 gives: % 155.69/21.47 | (191) $i(all_180_0) & leaf(all_146_0, all_180_0) & % 155.69/21.47 | subactivity_occurrence(all_146_0, all_114_0) & % 155.69/21.47 | occurrence_of(all_114_0, all_180_0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (191) implies: % 155.69/21.47 | (192) occurrence_of(all_114_0, all_180_0) % 155.69/21.47 | (193) $i(all_180_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (166) with fresh symbol all_184_0 gives: % 155.69/21.47 | (194) $i(all_184_0) & subactivity_occurrence(all_92_0, all_114_0) & % 155.69/21.47 | root(all_92_0, all_184_0) & occurrence_of(all_114_0, all_184_0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (194) implies: % 155.69/21.47 | (195) occurrence_of(all_114_0, all_184_0) % 155.69/21.47 | (196) $i(all_184_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (169) with fresh symbol all_186_0 gives: % 155.69/21.47 | (197) $i(all_186_0) & subactivity_occurrence(all_146_1, all_114_0) & % 155.69/21.47 | root(all_146_1, all_186_0) & occurrence_of(all_114_0, all_186_0) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (197) implies: % 155.69/21.47 | (198) occurrence_of(all_114_0, all_186_0) % 155.69/21.47 | (199) $i(all_186_0) % 155.69/21.47 | % 155.69/21.47 | DELTA: instantiating (158) with fresh symbols all_192_0, all_192_1 gives: % 155.69/21.47 | (200) $i(all_192_0) & $i(all_192_1) & next_subocc(all_192_1, all_192_0, % 155.69/21.47 | tptp0) & leaf_occ(all_192_0, all_138_0) & root_occ(all_192_1, % 155.69/21.47 | all_138_0) & occurrence_of(all_192_1, tptp4) & % 155.69/21.47 | (occurrence_of(all_192_0, tptp2) | occurrence_of(all_192_0, tptp3)) % 155.69/21.47 | % 155.69/21.47 | ALPHA: (200) implies: % 155.69/21.47 | (201) root_occ(all_192_1, all_138_0) % 155.69/21.47 | (202) leaf_occ(all_192_0, all_138_0) % 155.69/21.47 | (203) $i(all_192_1) % 155.69/21.47 | (204) $i(all_192_0) % 155.69/21.47 | % 155.69/21.47 | REDUCE: (146), (180) imply: % 155.69/21.47 | (205) leaf(all_116_0, tptp0) % 155.69/21.47 | % 155.69/21.47 | REDUCE: (110), (179) imply: % 155.69/21.47 | (206) root_occ(all_46_1, all_114_0) % 155.69/21.47 | % 155.69/21.47 | BETA: splitting (28) gives: % 155.69/21.47 | % 155.69/21.47 | Case 1: % 155.69/21.47 | | % 155.69/21.47 | | (207) atomic(all_46_2) % 155.69/21.47 | | % 155.69/21.47 | | GROUND_INST: instantiating (3) with all_46_2, tptp0, all_46_1, simplifying % 155.69/21.47 | | with (7), (23), (24), (25), (207) gives: % 155.69/21.47 | | (208) $false % 155.69/21.48 | | % 155.69/21.48 | | CLOSE: (208) is inconsistent. % 155.69/21.48 | | % 155.69/21.48 | Case 2: % 155.69/21.48 | | % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_08) with all_114_0, all_180_0, all_184_0, % 155.69/21.48 | | simplifying with (98), (192), (193), (195), (196) gives: % 155.69/21.48 | | (209) all_184_0 = all_180_0 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_08) with all_114_0, all_168_0, all_184_0, % 155.69/21.48 | | simplifying with (98), (189), (190), (195), (196) gives: % 155.69/21.48 | | (210) all_184_0 = all_168_0 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_08) with all_114_0, tptp0, all_186_0, % 155.69/21.48 | | simplifying with (7), (95), (98), (198), (199) gives: % 155.69/21.48 | | (211) all_186_0 = tptp0 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_08) with all_114_0, all_184_0, all_186_0, % 155.69/21.48 | | simplifying with (98), (195), (196), (198), (199) gives: % 155.69/21.48 | | (212) all_186_0 = all_184_0 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (13) with all_128_0, all_138_0, tptp0, % 155.69/21.48 | | simplifying with (7), (122), (124), (136), (139), (171) gives: % 155.69/21.48 | | (213) root_occ(all_128_0, all_138_0) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (13) with all_164_0, all_138_0, tptp0, % 155.69/21.48 | | simplifying with (7), (136), (139), (185), (186), (187) gives: % 155.69/21.48 | | (214) root_occ(all_164_0, all_138_0) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_01) with tptp0, all_96_0, all_66_0, % 155.69/21.48 | | all_106_0, all_116_0, simplifying with (7), (48), (71), (73), % 155.69/21.48 | | (74), (85), (86), (101), (104), (160) gives: % 155.69/21.48 | | (215) all_116_0 = all_66_0 | min_precedes(all_66_0, all_116_0, tptp0) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (12) with all_106_0, all_138_0, simplifying with % 155.69/21.48 | | (86), (139), (162) gives: % 155.69/21.48 | | (216) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_106_0, % 155.69/21.48 | | all_138_0) & root(all_106_0, v0) & occurrence_of(all_138_0, % 155.69/21.48 | | v0)) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_29) with all_106_0, all_130_0, all_114_0, % 155.69/21.48 | | all_168_0, simplifying with (86), (98), (128), (161), (165), % 155.69/21.48 | | (189), (190) gives: % 155.69/21.48 | | (217) all_130_0 = all_106_0 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_29) with all_46_1, all_130_0, all_114_0, % 155.69/21.48 | | all_168_0, simplifying with (25), (98), (128), (165), (189), % 155.69/21.48 | | (190), (206) gives: % 155.69/21.48 | | (218) all_130_0 = all_46_1 % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (12) with all_192_1, all_138_0, simplifying with % 155.69/21.48 | | (139), (201), (203) gives: % 155.69/21.48 | | (219) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_192_1, % 155.69/21.48 | | all_138_0) & root(all_192_1, v0) & occurrence_of(all_138_0, % 155.69/21.48 | | v0)) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (14) with all_192_0, all_138_0, simplifying with % 155.69/21.48 | | (139), (202), (204) gives: % 155.69/21.48 | | (220) ? [v0: $i] : ($i(v0) & leaf(all_192_0, v0) & % 155.69/21.48 | | subactivity_occurrence(all_192_0, all_138_0) & % 155.69/21.48 | | occurrence_of(all_138_0, v0)) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (15) with all_66_0, tptp0, all_154_0, simplifying % 155.69/21.48 | | with (7), (48), (182), (183) gives: % 155.69/21.48 | | (221) leaf(all_66_0, tptp0) | ? [v0: $i] : ($i(v0) & % 155.69/21.48 | | min_precedes(all_66_0, v0, tptp0)) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_12) with all_116_0, simplifying with (104), % 155.69/21.48 | | (164) gives: % 155.69/21.48 | | (222) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_116_0, % 155.69/21.48 | | v0)) % 155.69/21.48 | | % 155.69/21.48 | | GROUND_INST: instantiating (sos_12) with all_138_0, simplifying with (139), % 155.69/21.48 | | (163) gives: % 155.69/21.48 | | (223) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_138_0, % 155.69/21.48 | | v0)) % 155.69/21.48 | | % 155.69/21.48 | | COMBINE_EQS: (211), (212) imply: % 155.69/21.48 | | (224) all_184_0 = tptp0 % 155.69/21.48 | | % 155.69/21.48 | | SIMP: (224) implies: % 155.69/21.48 | | (225) all_184_0 = tptp0 % 155.69/21.48 | | % 155.69/21.48 | | COMBINE_EQS: (209), (210) imply: % 155.69/21.48 | | (226) all_180_0 = all_168_0 % 155.69/21.48 | | % 155.69/21.48 | | COMBINE_EQS: (209), (225) imply: % 155.69/21.48 | | (227) all_180_0 = tptp0 % 155.69/21.48 | | % 155.69/21.48 | | COMBINE_EQS: (226), (227) imply: % 155.69/21.48 | | (228) all_168_0 = tptp0 % 155.69/21.48 | | % 155.69/21.48 | | COMBINE_EQS: (217), (218) imply: % 155.69/21.48 | | (229) all_106_0 = all_46_1 % 155.69/21.48 | | % 155.69/21.48 | | SIMP: (229) implies: % 155.69/21.48 | | (230) all_106_0 = all_46_1 % 155.69/21.48 | | % 155.69/21.48 | | DELTA: instantiating (222) with fresh symbol all_244_0 gives: % 155.69/21.48 | | (231) $i(all_244_0) & activity(all_244_0) & occurrence_of(all_116_0, % 155.69/21.48 | | all_244_0) % 155.69/21.48 | | % 155.69/21.48 | | ALPHA: (231) implies: % 155.69/21.48 | | (232) occurrence_of(all_116_0, all_244_0) % 155.69/21.48 | | (233) $i(all_244_0) % 155.69/21.48 | | % 155.69/21.48 | | DELTA: instantiating (223) with fresh symbol all_258_0 gives: % 155.69/21.48 | | (234) $i(all_258_0) & activity(all_258_0) & occurrence_of(all_138_0, % 155.69/21.48 | | all_258_0) % 155.69/21.48 | | % 155.69/21.48 | | ALPHA: (234) implies: % 155.69/21.48 | | (235) occurrence_of(all_138_0, all_258_0) % 155.69/21.48 | | (236) $i(all_258_0) % 155.69/21.48 | | % 155.69/21.48 | | DELTA: instantiating (219) with fresh symbol all_288_0 gives: % 155.69/21.48 | | (237) $i(all_288_0) & subactivity_occurrence(all_192_1, all_138_0) & % 155.69/21.48 | | root(all_192_1, all_288_0) & occurrence_of(all_138_0, all_288_0) % 155.69/21.48 | | % 155.69/21.48 | | ALPHA: (237) implies: % 155.69/21.48 | | (238) occurrence_of(all_138_0, all_288_0) % 155.69/21.48 | | (239) $i(all_288_0) % 155.69/21.48 | | % 155.69/21.48 | | DELTA: instantiating (216) with fresh symbol all_292_0 gives: % 155.69/21.48 | | (240) $i(all_292_0) & subactivity_occurrence(all_106_0, all_138_0) & % 155.69/21.48 | | root(all_106_0, all_292_0) & occurrence_of(all_138_0, all_292_0) % 155.69/21.48 | | % 155.69/21.48 | | ALPHA: (240) implies: % 155.69/21.48 | | (241) occurrence_of(all_138_0, all_292_0) % 155.69/21.48 | | (242) $i(all_292_0) % 155.69/21.48 | | % 155.69/21.48 | | DELTA: instantiating (220) with fresh symbol all_312_0 gives: % 155.69/21.49 | | (243) $i(all_312_0) & leaf(all_192_0, all_312_0) & % 155.69/21.49 | | subactivity_occurrence(all_192_0, all_138_0) & % 155.69/21.49 | | occurrence_of(all_138_0, all_312_0) % 155.69/21.49 | | % 155.69/21.49 | | ALPHA: (243) implies: % 155.69/21.49 | | (244) occurrence_of(all_138_0, all_312_0) % 155.69/21.49 | | (245) $i(all_312_0) % 155.69/21.49 | | % 155.69/21.49 | | REDUCE: (162), (230) imply: % 155.69/21.49 | | (246) root_occ(all_46_1, all_138_0) % 155.69/21.49 | | % 155.69/21.49 | | BETA: splitting (221) gives: % 155.69/21.49 | | % 155.69/21.49 | | Case 1: % 155.69/21.49 | | | % 155.69/21.49 | | | (247) leaf(all_66_0, tptp0) % 155.69/21.49 | | | % 155.69/21.49 | | | BETA: splitting (105) gives: % 155.69/21.49 | | | % 155.69/21.49 | | | Case 1: % 155.69/21.49 | | | | % 155.69/21.49 | | | | (248) occurrence_of(all_116_0, tptp2) % 155.69/21.49 | | | | % 155.69/21.49 | | | | BETA: splitting (215) gives: % 155.69/21.49 | | | | % 155.69/21.49 | | | | Case 1: % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | (249) min_precedes(all_66_0, all_116_0, tptp0) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (16) with all_66_0, tptp0, all_116_0, % 155.69/21.49 | | | | | simplifying with (7), (48), (104), (247), (249) gives: % 155.69/21.49 | | | | | (250) $false % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | CLOSE: (250) is inconsistent. % 155.69/21.49 | | | | | % 155.69/21.49 | | | | Case 2: % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | (251) all_116_0 = all_66_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | REDUCE: (232), (251) imply: % 155.69/21.49 | | | | | (252) occurrence_of(all_66_0, all_244_0) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | REDUCE: (248), (251) imply: % 155.69/21.49 | | | | | (253) occurrence_of(all_66_0, tptp2) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_66_0, all_66_1, % 155.69/21.49 | | | | | all_244_0, simplifying with (44), (47), (48), (233), % 155.69/21.49 | | | | | (252) gives: % 155.69/21.49 | | | | | (254) all_244_0 = all_66_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_66_0, tptp2, all_244_0, % 155.69/21.49 | | | | | simplifying with (9), (48), (233), (252), (253) gives: % 155.69/21.49 | | | | | (255) all_244_0 = tptp2 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_288_0, % 155.69/21.49 | | | | | all_292_0, simplifying with (139), (238), (239), (241), % 155.69/21.49 | | | | | (242) gives: % 155.69/21.49 | | | | | (256) all_292_0 = all_288_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_258_0, % 155.69/21.49 | | | | | all_292_0, simplifying with (139), (235), (236), (241), % 155.69/21.49 | | | | | (242) gives: % 155.69/21.49 | | | | | (257) all_292_0 = all_258_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, tptp0, all_312_0, % 155.69/21.49 | | | | | simplifying with (7), (136), (139), (244), (245) gives: % 155.69/21.49 | | | | | (258) all_312_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_288_0, % 155.69/21.49 | | | | | all_312_0, simplifying with (139), (238), (239), (244), % 155.69/21.49 | | | | | (245) gives: % 155.69/21.49 | | | | | (259) all_312_0 = all_288_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_29) with all_128_0, all_164_0, % 155.69/21.49 | | | | | all_138_0, all_258_0, simplifying with (124), (139), % 155.69/21.49 | | | | | (187), (213), (214), (235), (236) gives: % 155.69/21.49 | | | | | (260) all_164_0 = all_128_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_29) with all_46_1, all_164_0, % 155.69/21.49 | | | | | all_138_0, all_258_0, simplifying with (25), (139), % 155.69/21.49 | | | | | (187), (214), (235), (236), (246) gives: % 155.69/21.49 | | | | | (261) all_164_0 = all_46_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (258), (259) imply: % 155.69/21.49 | | | | | (262) all_288_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (262) implies: % 155.69/21.49 | | | | | (263) all_288_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (256), (257) imply: % 155.69/21.49 | | | | | (264) all_288_0 = all_258_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (264) implies: % 155.69/21.49 | | | | | (265) all_288_0 = all_258_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (263), (265) imply: % 155.69/21.49 | | | | | (266) all_258_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (266) implies: % 155.69/21.49 | | | | | (267) all_258_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (254), (255) imply: % 155.69/21.49 | | | | | (268) all_66_1 = tptp2 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (268) implies: % 155.69/21.49 | | | | | (269) all_66_1 = tptp2 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (260), (261) imply: % 155.69/21.49 | | | | | (270) all_128_0 = all_46_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (270) implies: % 155.69/21.49 | | | | | (271) all_128_0 = all_46_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | REDUCE: (46), (269) imply: % 155.69/21.49 | | | | | (272) send_message(tptp2, all_54_2, all_54_1, all_46_1, tptp0) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (5) with all_54_2, all_54_1, all_46_1, % 155.69/21.49 | | | | | tptp0, simplifying with (7), (25), (35), (36), (272) % 155.69/21.49 | | | | | gives: % 155.69/21.49 | | | | | (273) $false % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | CLOSE: (273) is inconsistent. % 155.69/21.49 | | | | | % 155.69/21.49 | | | | End of split % 155.69/21.49 | | | | % 155.69/21.49 | | | Case 2: % 155.69/21.49 | | | | % 155.69/21.49 | | | | (274) occurrence_of(all_116_0, tptp3) % 155.69/21.49 | | | | % 155.69/21.49 | | | | BETA: splitting (215) gives: % 155.69/21.49 | | | | % 155.69/21.49 | | | | Case 1: % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | (275) min_precedes(all_66_0, all_116_0, tptp0) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (16) with all_66_0, tptp0, all_116_0, % 155.69/21.49 | | | | | simplifying with (7), (48), (104), (247), (275) gives: % 155.69/21.49 | | | | | (276) $false % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | CLOSE: (276) is inconsistent. % 155.69/21.49 | | | | | % 155.69/21.49 | | | | Case 2: % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | (277) all_116_0 = all_66_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | REDUCE: (232), (277) imply: % 155.69/21.49 | | | | | (278) occurrence_of(all_66_0, all_244_0) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | REDUCE: (274), (277) imply: % 155.69/21.49 | | | | | (279) occurrence_of(all_66_0, tptp3) % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_66_0, all_66_1, % 155.69/21.49 | | | | | all_244_0, simplifying with (44), (47), (48), (233), % 155.69/21.49 | | | | | (278) gives: % 155.69/21.49 | | | | | (280) all_244_0 = all_66_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_66_0, tptp3, all_244_0, % 155.69/21.49 | | | | | simplifying with (8), (48), (233), (278), (279) gives: % 155.69/21.49 | | | | | (281) all_244_0 = tptp3 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_258_0, % 155.69/21.49 | | | | | all_288_0, simplifying with (139), (235), (236), (238), % 155.69/21.49 | | | | | (239) gives: % 155.69/21.49 | | | | | (282) all_288_0 = all_258_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_288_0, % 155.69/21.49 | | | | | all_292_0, simplifying with (139), (238), (239), (241), % 155.69/21.49 | | | | | (242) gives: % 155.69/21.49 | | | | | (283) all_292_0 = all_288_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, tptp0, all_312_0, % 155.69/21.49 | | | | | simplifying with (7), (136), (139), (244), (245) gives: % 155.69/21.49 | | | | | (284) all_312_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_08) with all_138_0, all_292_0, % 155.69/21.49 | | | | | all_312_0, simplifying with (139), (241), (242), (244), % 155.69/21.49 | | | | | (245) gives: % 155.69/21.49 | | | | | (285) all_312_0 = all_292_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_29) with all_128_0, all_164_0, % 155.69/21.49 | | | | | all_138_0, all_258_0, simplifying with (124), (139), % 155.69/21.49 | | | | | (187), (213), (214), (235), (236) gives: % 155.69/21.49 | | | | | (286) all_164_0 = all_128_0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | GROUND_INST: instantiating (sos_29) with all_46_1, all_164_0, % 155.69/21.49 | | | | | all_138_0, all_258_0, simplifying with (25), (139), % 155.69/21.49 | | | | | (187), (214), (235), (236), (246) gives: % 155.69/21.49 | | | | | (287) all_164_0 = all_46_1 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (284), (285) imply: % 155.69/21.49 | | | | | (288) all_292_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (288) implies: % 155.69/21.49 | | | | | (289) all_292_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (283), (289) imply: % 155.69/21.49 | | | | | (290) all_288_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (290) implies: % 155.69/21.49 | | | | | (291) all_288_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (282), (291) imply: % 155.69/21.49 | | | | | (292) all_258_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (292) implies: % 155.69/21.49 | | | | | (293) all_258_0 = tptp0 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | COMBINE_EQS: (280), (281) imply: % 155.69/21.49 | | | | | (294) all_66_1 = tptp3 % 155.69/21.49 | | | | | % 155.69/21.49 | | | | | SIMP: (294) implies: % 155.69/21.50 | | | | | (295) all_66_1 = tptp3 % 155.69/21.50 | | | | | % 155.69/21.50 | | | | | COMBINE_EQS: (286), (287) imply: % 155.69/21.50 | | | | | (296) all_128_0 = all_46_1 % 155.69/21.50 | | | | | % 155.69/21.50 | | | | | REDUCE: (46), (295) imply: % 155.69/21.50 | | | | | (297) send_message(tptp3, all_54_2, all_54_1, all_46_1, tptp0) % 155.69/21.50 | | | | | % 155.69/21.50 | | | | | GROUND_INST: instantiating (4) with all_54_2, all_54_1, all_46_1, % 155.69/21.50 | | | | | tptp0, simplifying with (7), (25), (35), (36), (297) % 155.69/21.50 | | | | | gives: % 155.69/21.50 | | | | | (298) $false % 155.69/21.50 | | | | | % 155.69/21.50 | | | | | CLOSE: (298) is inconsistent. % 155.69/21.50 | | | | | % 155.69/21.50 | | | | End of split % 155.69/21.50 | | | | % 155.69/21.50 | | | End of split % 155.69/21.50 | | | % 155.69/21.50 | | Case 2: % 155.69/21.50 | | | % 155.69/21.50 | | | (299) ~ leaf(all_66_0, tptp0) % 155.69/21.50 | | | % 155.69/21.50 | | | BETA: splitting (215) gives: % 155.69/21.50 | | | % 155.69/21.50 | | | Case 1: % 155.69/21.50 | | | | % 155.69/21.50 | | | | (300) min_precedes(all_66_0, all_116_0, tptp0) % 155.69/21.50 | | | | % 155.69/21.50 | | | | GROUND_INST: instantiating (11) with all_46_1, all_116_0, tptp0, % 155.69/21.50 | | | | all_66_0, simplifying with (7), (25), (48), (52), (104), % 155.69/21.50 | | | | (153), (300) gives: % 155.69/21.50 | | | | (301) $false % 155.69/21.50 | | | | % 155.69/21.50 | | | | CLOSE: (301) is inconsistent. % 155.69/21.50 | | | | % 155.69/21.50 | | | Case 2: % 155.69/21.50 | | | | % 155.69/21.50 | | | | (302) all_116_0 = all_66_0 % 155.69/21.50 | | | | % 155.69/21.50 | | | | REDUCE: (205), (302) imply: % 155.69/21.50 | | | | (303) leaf(all_66_0, tptp0) % 155.69/21.50 | | | | % 155.69/21.50 | | | | PRED_UNIFY: (299), (303) imply: % 155.69/21.50 | | | | (304) $false % 155.69/21.50 | | | | % 155.69/21.50 | | | | CLOSE: (304) is inconsistent. % 155.69/21.50 | | | | % 155.69/21.50 | | | End of split % 155.69/21.50 | | | % 155.69/21.50 | | End of split % 155.69/21.50 | | % 155.69/21.50 | End of split % 155.69/21.50 | % 155.69/21.50 End of proof % 155.69/21.50 % SZS output end Proof for theBenchmark % 155.69/21.50 % 155.69/21.50 20835ms %------------------------------------------------------------------------------