%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO014+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 13:08:50 EDT 2023 % Result : Theorem 68.02s 9.87s % Output : Proof 232.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.10 % Problem : PRO014+4 : TPTP v8.1.2. Released v4.0.0. % 0.10/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n005.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Mon Aug 28 19:19:53 EDT 2023 % 0.10/0.31 % CPUTime : % 0.15/0.60 ________ _____ % 0.15/0.60 ___ __ \_________(_)________________________________ % 0.15/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.15/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.15/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.15/0.60 % 0.15/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.15/0.60 (2023-06-19) % 0.15/0.60 % 0.15/0.60 (c) Philipp Rümmer, 2009-2023 % 0.15/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.15/0.60 Amanda Stjerna. % 0.15/0.60 Free software under BSD-3-Clause. % 0.15/0.60 % 0.15/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.15/0.60 % 0.15/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.15/0.62 Running up to 7 provers in parallel. % 0.15/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.15/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.15/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.15/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.15/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.15/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.15/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 3.06/1.27 Prover 4: Preprocessing ... % 3.06/1.27 Prover 1: Preprocessing ... % 3.63/1.32 Prover 5: Preprocessing ... % 3.63/1.32 Prover 6: Preprocessing ... % 3.63/1.32 Prover 0: Preprocessing ... % 3.63/1.32 Prover 3: Preprocessing ... % 3.63/1.33 Prover 2: Preprocessing ... % 7.93/1.98 Prover 2: Constructing countermodel ... % 7.93/1.99 Prover 5: Proving ... % 9.52/2.16 Prover 1: Constructing countermodel ... % 9.52/2.16 Prover 3: Constructing countermodel ... % 10.13/2.23 Prover 6: Proving ... % 12.71/2.68 Prover 4: Constructing countermodel ... % 14.42/2.83 Prover 0: Proving ... % 68.02/9.86 Prover 5: proved (9219ms) % 68.02/9.87 % 68.02/9.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.02/9.87 % 68.02/9.87 Prover 2: stopped % 68.02/9.87 Prover 3: stopped % 68.02/9.87 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 68.02/9.87 Prover 0: stopped % 68.02/9.87 Prover 6: stopped % 68.02/9.87 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 68.02/9.87 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 68.02/9.87 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 68.02/9.87 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 68.73/9.96 Prover 7: Preprocessing ... % 68.73/9.98 Prover 10: Preprocessing ... % 68.73/9.98 Prover 13: Preprocessing ... % 68.73/9.99 Prover 8: Preprocessing ... % 68.73/9.99 Prover 11: Preprocessing ... % 68.73/10.03 Prover 10: Constructing countermodel ... % 68.73/10.04 Prover 7: Constructing countermodel ... % 68.73/10.07 Prover 13: Constructing countermodel ... % 69.46/10.13 Prover 8: Warning: ignoring some quantifiers % 69.46/10.14 Prover 8: Constructing countermodel ... % 71.09/10.25 Prover 11: Constructing countermodel ... % 101.32/14.14 Prover 13: stopped % 101.32/14.16 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 101.93/14.23 Prover 16: Preprocessing ... % 102.43/14.29 Prover 16: Constructing countermodel ... % 115.26/16.00 Prover 1: stopped % 115.26/16.02 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 116.45/16.14 Prover 19: Preprocessing ... % 118.27/16.37 Prover 19: Warning: ignoring some quantifiers % 118.27/16.38 Prover 19: Constructing countermodel ... % 140.20/19.28 Prover 16: stopped % 143.32/19.78 Prover 19: stopped % 189.34/27.97 Prover 4: stopped % 197.79/29.99 Prover 7: stopped % 231.79/39.44 Prover 10: Found proof (size 236) % 231.79/39.44 Prover 10: proved (29570ms) % 231.79/39.46 Prover 8: stopped % 231.79/39.47 Prover 11: stopped % 231.79/39.47 % 231.79/39.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 231.79/39.47 % 232.13/39.51 % SZS output start Proof for theBenchmark % 232.13/39.52 Assumptions after simplification: % 232.13/39.52 --------------------------------- % 232.13/39.52 % 232.13/39.52 (goals) % 232.13/39.53 $i(tptp1) & $i(tptp2) & $i(tptp3) & $i(tptp0) & ? [v0: $i] : ? [v1: $i] : % 232.13/39.53 ($i(v1) & $i(v0) & arboreal(v0) & subactivity_occurrence(v0, v1) & % 232.13/39.53 occurrence_of(v1, tptp0) & ~ leaf_occ(v0, v1) & ! [v2: $i] : ! [v3: $i] : % 232.13/39.53 ( ~ $i(v3) | ~ $i(v2) | ~ next_subocc(v0, v2, tptp0) | ~ leaf(v3, tptp0) % 232.13/39.53 | ~ min_precedes(v2, v3, tptp0) | ~ occurrence_of(v3, tptp1) | ~ % 232.13/39.53 occurrence_of(v2, tptp3)) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 232.13/39.53 $i(v2) | ~ next_subocc(v0, v2, tptp0) | ~ leaf(v3, tptp0) | ~ % 232.13/39.53 min_precedes(v2, v3, tptp0) | ~ occurrence_of(v3, tptp2) | ~ % 232.13/39.53 occurrence_of(v2, tptp3))) % 232.13/39.53 % 232.13/39.53 (sos) % 232.13/39.53 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 232.13/39.53 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 232.13/39.53 root(v2, v0))) % 232.13/39.53 % 232.13/39.53 (sos_02) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 232.13/39.54 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | % 232.13/39.54 ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | % 232.13/39.54 min_precedes(v2, v3, v0)) % 232.13/39.54 % 232.13/39.54 (sos_03) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 232.13/39.54 | activity_occurrence(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 232.13/39.54 $i(v0) | ~ occurrence_of(v1, v0) | activity(v0)) % 232.13/39.54 % 232.13/39.54 (sos_06) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.54 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 232.13/39.54 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 232.13/39.54 occurrence_of(v3, v0))) % 232.13/39.54 % 232.13/39.54 (sos_07) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | % 232.13/39.54 atomic(v1) | ? [v2: $i] : ($i(v2) & leaf_occ(v0, v2) & occurrence_of(v2, % 232.13/39.54 v1))) % 232.13/39.54 % 232.13/39.54 (sos_08) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 232.13/39.54 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 232.13/39.54 % 232.13/39.54 (sos_11) % 232.13/39.54 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.13/39.54 subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0: $i] : ! % 232.13/39.54 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subactivity_occurrence(v0, v1) | % 232.13/39.55 activity_occurrence(v0)) % 232.13/39.55 % 232.13/39.55 (sos_12) % 232.13/39.55 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 232.13/39.55 & activity(v1) & occurrence_of(v0, v1))) % 232.13/39.55 % 232.13/39.55 (sos_15) % 232.13/39.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.55 ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0: $i] : ! [v1: $i] : % 232.13/39.55 ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v2, v0, v1) % 232.13/39.55 | leaf(v0, v1) | ? [v3: $i] : ($i(v3) & min_precedes(v0, v3, v1))) & ! % 232.13/39.55 [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | root(v0, % 232.13/39.55 v1) | ? [v2: $i] : ($i(v2) & min_precedes(v2, v0, v1))) & ! [v0: $i] : % 232.13/39.55 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | leaf(v0, v1) | ? [v2: % 232.13/39.55 $i] : ($i(v2) & min_precedes(v0, v2, v1))) % 232.13/39.55 % 232.13/39.55 (sos_18) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.56 ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, % 232.13/39.56 v2) | leaf_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 232.13/39.56 $i(v0) | ~ leaf_occ(v0, v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 232.13/39.56 subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 232.13/39.56 % 232.13/39.56 (sos_19) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.56 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 232.13/39.56 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 232.13/39.56 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 232.13/39.56 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 232.13/39.56 % 232.13/39.56 (sos_21) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ precedes(v0, v1) | % 232.13/39.56 earlier(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.13/39.56 precedes(v0, v1) | legal(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 232.13/39.56 $i(v0) | ~ earlier(v0, v1) | ~ legal(v1) | precedes(v0, v1)) % 232.13/39.56 % 232.13/39.56 (sos_22) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.56 ~ min_precedes(v0, v1, v2) | ~ root(v1, v2)) % 232.13/39.56 % 232.13/39.56 (sos_23) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.56 ~ min_precedes(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, % 232.13/39.56 v2) & root(v3, v2))) % 232.13/39.56 % 232.13/39.56 (sos_24) % 232.13/39.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.56 ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 232.13/39.56 % 232.13/39.56 (sos_25) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.57 ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0: $i] : ! [v1: $i] : ! % 232.13/39.57 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 232.13/39.57 arboreal(v0)) % 232.13/39.57 % 232.13/39.57 (sos_26) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 232.13/39.57 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 232.13/39.57 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 232.13/39.57 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 232.13/39.57 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 232.13/39.57 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 232.13/39.57 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 232.13/39.57 min_precedes(v0, v3, v2))) % 232.13/39.57 % 232.13/39.57 (sos_27) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 232.13/39.57 | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | ~ % 232.13/39.57 subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | % 232.13/39.57 subactivity_occurrence(v0, v3)) % 232.13/39.57 % 232.13/39.57 (sos_29) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 232.13/39.57 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 232.13/39.57 v2) | ~ occurrence_of(v2, v3)) % 232.13/39.57 % 232.13/39.57 (sos_30) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 232.13/39.57 ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 232.13/39.57 % 232.13/39.57 (sos_31) % 232.13/39.57 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 232.13/39.57 | ~ $i(v1) | ~ $i(v0) | ~ precedes(v1, v2) | ~ min_precedes(v0, v2, v3) % 232.13/39.57 | ~ min_precedes(v0, v1, v3) | min_precedes(v1, v2, v3)) % 232.13/39.57 % 232.13/39.57 (sos_32) % 232.13/39.57 $i(tptp1) & $i(tptp2) & $i(tptp4) & $i(tptp3) & $i(tptp0) & ! [v0: $i] : ! % 232.13/39.57 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | ~ % 232.13/39.57 subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, tptp0) | leaf_occ(v0, % 232.13/39.57 v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v4) & $i(v3) & $i(v2) % 232.13/39.57 & next_subocc(v3, v4, tptp0) & next_subocc(v2, v3, tptp0) & % 232.13/39.57 next_subocc(v0, v2, tptp0) & leaf(v4, tptp0) & occurrence_of(v3, tptp4) & % 232.13/39.57 occurrence_of(v2, tptp3) & (occurrence_of(v4, tptp1) | occurrence_of(v4, % 232.13/39.57 tptp2)))) % 232.13/39.57 % 232.13/39.58 (sos_34) % 232.13/39.58 $i(tptp0) & ~ atomic(tptp0) % 232.13/39.58 % 232.13/39.58 Further assumptions not needed in the proof: % 232.13/39.58 -------------------------------------------- % 232.13/39.58 sos_01, sos_04, sos_05, sos_09, sos_10, sos_13, sos_14, sos_16, sos_17, sos_20, % 232.13/39.58 sos_28, sos_33, sos_35, sos_36, sos_37, sos_38, sos_39, sos_40, sos_41, sos_42, % 232.13/39.58 sos_43, sos_44 % 232.13/39.58 % 232.13/39.58 Those formulas are unsatisfiable: % 232.13/39.58 --------------------------------- % 232.13/39.58 % 232.13/39.58 Begin of proof % 232.13/39.58 | % 232.13/39.58 | ALPHA: (goals) implies: % 232.13/39.58 | (1) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & arboreal(v0) & % 232.13/39.58 | subactivity_occurrence(v0, v1) & occurrence_of(v1, tptp0) & ~ % 232.13/39.58 | leaf_occ(v0, v1) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 232.13/39.58 | | ~ next_subocc(v0, v2, tptp0) | ~ leaf(v3, tptp0) | ~ % 232.13/39.58 | min_precedes(v2, v3, tptp0) | ~ occurrence_of(v3, tptp1) | ~ % 232.13/39.58 | occurrence_of(v2, tptp3)) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) % 232.13/39.58 | | ~ $i(v2) | ~ next_subocc(v0, v2, tptp0) | ~ leaf(v3, tptp0) | % 232.13/39.58 | ~ min_precedes(v2, v3, tptp0) | ~ occurrence_of(v3, tptp2) | ~ % 232.13/39.58 | occurrence_of(v2, tptp3))) % 232.13/39.58 | % 232.13/39.58 | ALPHA: (sos_34) implies: % 232.13/39.58 | (2) ~ atomic(tptp0) % 232.13/39.58 | % 232.13/39.58 | ALPHA: (sos_32) implies: % 232.13/39.58 | (3) $i(tptp0) % 232.13/39.58 | (4) $i(tptp3) % 232.13/39.59 | (5) $i(tptp2) % 232.13/39.59 | (6) $i(tptp1) % 232.13/39.59 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | % 232.13/39.59 | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, tptp0) | % 232.13/39.59 | leaf_occ(v0, v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v4) % 232.13/39.59 | & $i(v3) & $i(v2) & next_subocc(v3, v4, tptp0) & next_subocc(v2, % 232.13/39.59 | v3, tptp0) & next_subocc(v0, v2, tptp0) & leaf(v4, tptp0) & % 232.13/39.59 | occurrence_of(v3, tptp4) & occurrence_of(v2, tptp3) & % 232.13/39.59 | (occurrence_of(v4, tptp1) | occurrence_of(v4, tptp2)))) % 232.13/39.59 | % 232.13/39.59 | ALPHA: (sos_26) implies: % 232.13/39.59 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.13/39.59 | $i(v0) | ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 232.13/39.59 | % 232.13/39.59 | ALPHA: (sos_25) implies: % 232.13/39.59 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.13/39.59 | $i(v0) | ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 232.13/39.59 | % 232.13/39.59 | ALPHA: (sos_21) implies: % 232.13/39.59 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ earlier(v0, % 232.13/39.59 | v1) | ~ legal(v1) | precedes(v0, v1)) % 232.28/39.59 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ precedes(v0, % 232.28/39.59 | v1) | legal(v1)) % 232.28/39.59 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ precedes(v0, % 232.28/39.59 | v1) | earlier(v0, v1)) % 232.28/39.59 | % 232.28/39.59 | ALPHA: (sos_19) implies: % 232.28/39.59 | (13) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 232.28/39.59 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 232.28/39.59 | root(v0, v2) & occurrence_of(v1, v2))) % 232.28/39.59 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.28/39.59 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 232.28/39.59 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 232.28/39.59 | % 232.28/39.59 | ALPHA: (sos_18) implies: % 232.28/39.59 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf_occ(v0, % 232.28/39.59 | v1) | ? [v2: $i] : ($i(v2) & leaf(v0, v2) & % 232.28/39.59 | subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 232.28/39.59 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.28/39.60 | $i(v0) | ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ % 232.28/39.60 | occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 232.28/39.60 | % 232.28/39.60 | ALPHA: (sos_15) implies: % 232.28/39.60 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v0, v1) | % 232.28/39.60 | leaf(v0, v1) | ? [v2: $i] : ($i(v2) & min_precedes(v0, v2, v1))) % 232.28/39.60 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ leaf(v0, v1) | % 232.28/39.60 | root(v0, v1) | ? [v2: $i] : ($i(v2) & min_precedes(v2, v0, v1))) % 232.28/39.60 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.28/39.60 | $i(v0) | ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3: $i] : % 232.28/39.60 | ($i(v3) & min_precedes(v0, v3, v1))) % 232.28/39.60 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.28/39.60 | $i(v0) | ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 232.28/39.60 | % 232.28/39.60 | ALPHA: (sos_11) implies: % 232.28/39.60 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 232.28/39.60 | (22) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 232.28/39.60 | % 232.28/39.60 | ALPHA: (sos_03) implies: % 232.28/39.60 | (23) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 232.28/39.60 | % 232.28/39.60 | DELTA: instantiating (1) with fresh symbols all_36_0, all_36_1 gives: % 232.28/39.60 | (24) $i(all_36_0) & $i(all_36_1) & arboreal(all_36_1) & % 232.28/39.60 | subactivity_occurrence(all_36_1, all_36_0) & occurrence_of(all_36_0, % 232.28/39.60 | tptp0) & ~ leaf_occ(all_36_1, all_36_0) & ! [v0: $i] : ! [v1: $i] % 232.28/39.60 | : ( ~ $i(v1) | ~ $i(v0) | ~ next_subocc(all_36_1, v0, tptp0) | ~ % 232.28/39.60 | leaf(v1, tptp0) | ~ min_precedes(v0, v1, tptp0) | ~ % 232.28/39.60 | occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3)) & ! [v0: % 232.28/39.60 | $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | next_subocc(all_36_1, v0, tptp0) | ~ leaf(v1, tptp0) | ~ % 232.28/39.60 | min_precedes(v0, v1, tptp0) | ~ occurrence_of(v1, tptp2) | ~ % 232.28/39.60 | occurrence_of(v0, tptp3)) % 232.28/39.60 | % 232.28/39.60 | ALPHA: (24) implies: % 232.28/39.60 | (25) ~ leaf_occ(all_36_1, all_36_0) % 232.28/39.60 | (26) occurrence_of(all_36_0, tptp0) % 232.28/39.60 | (27) subactivity_occurrence(all_36_1, all_36_0) % 232.28/39.60 | (28) arboreal(all_36_1) % 232.28/39.60 | (29) $i(all_36_1) % 232.28/39.60 | (30) $i(all_36_0) % 232.28/39.60 | (31) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | next_subocc(all_36_1, v0, tptp0) | ~ leaf(v1, tptp0) | ~ % 232.28/39.60 | min_precedes(v0, v1, tptp0) | ~ occurrence_of(v1, tptp2) | ~ % 232.28/39.60 | occurrence_of(v0, tptp3)) % 232.28/39.60 | (32) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.28/39.60 | next_subocc(all_36_1, v0, tptp0) | ~ leaf(v1, tptp0) | ~ % 232.28/39.60 | min_precedes(v0, v1, tptp0) | ~ occurrence_of(v1, tptp1) | ~ % 232.28/39.60 | occurrence_of(v0, tptp3)) % 232.28/39.60 | % 232.28/39.60 | GROUND_INST: instantiating (sos) with tptp0, all_36_0, simplifying with (2), % 232.28/39.60 | (3), (26), (30) gives: % 232.28/39.61 | (33) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_36_0) & % 232.28/39.61 | root(v0, tptp0)) % 232.28/39.61 | % 232.28/39.61 | GROUND_INST: instantiating (22) with all_36_1, all_36_0, simplifying with % 232.28/39.61 | (27), (29), (30) gives: % 232.28/39.61 | (34) activity_occurrence(all_36_0) % 232.28/39.61 | % 232.28/39.61 | GROUND_INST: instantiating (7) with all_36_1, all_36_0, simplifying with (25), % 232.28/39.61 | (26), (27), (28), (29), (30) gives: % 232.28/39.61 | (35) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 232.28/39.61 | next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) & % 232.28/39.61 | next_subocc(all_36_1, v0, tptp0) & leaf(v2, tptp0) & % 232.28/39.61 | occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & % 232.28/39.61 | (occurrence_of(v2, tptp1) | occurrence_of(v2, tptp2))) % 232.28/39.61 | % 232.28/39.61 | DELTA: instantiating (33) with fresh symbol all_45_0 gives: % 232.28/39.61 | (36) $i(all_45_0) & subactivity_occurrence(all_45_0, all_36_0) & % 232.28/39.61 | root(all_45_0, tptp0) % 232.28/39.61 | % 232.28/39.61 | ALPHA: (36) implies: % 232.28/39.61 | (37) root(all_45_0, tptp0) % 232.28/39.61 | (38) subactivity_occurrence(all_45_0, all_36_0) % 232.28/39.61 | (39) $i(all_45_0) % 232.28/39.61 | % 232.28/39.61 | DELTA: instantiating (35) with fresh symbols all_47_0, all_47_1, all_47_2 % 232.28/39.61 | gives: % 232.28/39.61 | (40) $i(all_47_0) & $i(all_47_1) & $i(all_47_2) & next_subocc(all_47_1, % 232.28/39.61 | all_47_0, tptp0) & next_subocc(all_47_2, all_47_1, tptp0) & % 232.28/39.61 | next_subocc(all_36_1, all_47_2, tptp0) & leaf(all_47_0, tptp0) & % 232.28/39.61 | occurrence_of(all_47_1, tptp4) & occurrence_of(all_47_2, tptp3) & % 232.28/39.61 | (occurrence_of(all_47_0, tptp1) | occurrence_of(all_47_0, tptp2)) % 232.28/39.61 | % 232.28/39.61 | ALPHA: (40) implies: % 232.28/39.61 | (41) occurrence_of(all_47_2, tptp3) % 232.28/39.61 | (42) leaf(all_47_0, tptp0) % 232.28/39.61 | (43) next_subocc(all_36_1, all_47_2, tptp0) % 232.28/39.61 | (44) next_subocc(all_47_2, all_47_1, tptp0) % 232.28/39.61 | (45) next_subocc(all_47_1, all_47_0, tptp0) % 232.28/39.61 | (46) $i(all_47_2) % 232.28/39.61 | (47) $i(all_47_1) % 232.28/39.61 | (48) $i(all_47_0) % 232.28/39.61 | (49) occurrence_of(all_47_0, tptp1) | occurrence_of(all_47_0, tptp2) % 232.28/39.61 | % 232.28/39.61 | GROUND_INST: instantiating (23) with tptp3, all_47_2, simplifying with (4), % 232.28/39.61 | (41), (46) gives: % 232.28/39.61 | (50) activity_occurrence(all_47_2) % 232.28/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (17) with all_45_0, tptp0, simplifying with (3), % 232.75/39.61 | (37), (39) gives: % 232.75/39.61 | (51) leaf(all_45_0, tptp0) | ? [v0: $i] : ($i(v0) & min_precedes(all_45_0, % 232.75/39.61 | v0, tptp0)) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (14) with all_45_0, all_36_0, tptp0, simplifying % 232.75/39.61 | with (3), (26), (30), (37), (38), (39) gives: % 232.75/39.61 | (52) root_occ(all_45_0, all_36_0) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (sos_12) with all_36_0, simplifying with (30), (34) % 232.75/39.61 | gives: % 232.75/39.61 | (53) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_36_0, v0)) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (18) with all_47_0, tptp0, simplifying with (3), % 232.75/39.61 | (42), (48) gives: % 232.75/39.61 | (54) root(all_47_0, tptp0) | ? [v0: $i] : ($i(v0) & min_precedes(v0, % 232.75/39.61 | all_47_0, tptp0)) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (sos_07) with all_47_0, tptp0, simplifying with % 232.75/39.61 | (2), (3), (42), (48) gives: % 232.75/39.61 | (55) ? [v0: $i] : ($i(v0) & leaf_occ(all_47_0, v0) & occurrence_of(v0, % 232.75/39.61 | tptp0)) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (8) with all_36_1, all_47_2, tptp0, simplifying % 232.75/39.61 | with (3), (29), (43), (46) gives: % 232.75/39.61 | (56) min_precedes(all_36_1, all_47_2, tptp0) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (9) with all_47_2, all_47_1, tptp0, simplifying % 232.75/39.61 | with (3), (44), (46), (47) gives: % 232.75/39.61 | (57) arboreal(all_47_2) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (8) with all_47_2, all_47_1, tptp0, simplifying % 232.75/39.61 | with (3), (44), (46), (47) gives: % 232.75/39.61 | (58) min_precedes(all_47_2, all_47_1, tptp0) % 232.75/39.61 | % 232.75/39.61 | GROUND_INST: instantiating (8) with all_47_1, all_47_0, tptp0, simplifying % 232.75/39.61 | with (3), (45), (47), (48) gives: % 232.75/39.61 | (59) min_precedes(all_47_1, all_47_0, tptp0) % 232.75/39.61 | % 232.75/39.61 | DELTA: instantiating (55) with fresh symbol all_55_0 gives: % 232.75/39.62 | (60) $i(all_55_0) & leaf_occ(all_47_0, all_55_0) & occurrence_of(all_55_0, % 232.75/39.62 | tptp0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (60) implies: % 232.75/39.62 | (61) occurrence_of(all_55_0, tptp0) % 232.75/39.62 | (62) leaf_occ(all_47_0, all_55_0) % 232.75/39.62 | (63) $i(all_55_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (53) with fresh symbol all_57_0 gives: % 232.75/39.62 | (64) $i(all_57_0) & activity(all_57_0) & occurrence_of(all_36_0, all_57_0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (64) implies: % 232.75/39.62 | (65) occurrence_of(all_36_0, all_57_0) % 232.75/39.62 | (66) $i(all_57_0) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, all_57_0, % 232.75/39.62 | simplifying with (3), (26), (30), (65), (66) gives: % 232.75/39.62 | (67) all_57_0 = tptp0 % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos) with all_57_0, all_36_0, simplifying with % 232.75/39.62 | (30), (65), (66) gives: % 232.75/39.62 | (68) atomic(all_57_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 232.75/39.62 | all_36_0) & root(v0, all_57_0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (23) with tptp0, all_55_0, simplifying with (3), % 232.75/39.62 | (61), (63) gives: % 232.75/39.62 | (69) activity_occurrence(all_55_0) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (13) with all_45_0, all_36_0, simplifying with % 232.75/39.62 | (30), (39), (52) gives: % 232.75/39.62 | (70) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_45_0, all_36_0) & % 232.75/39.62 | root(all_45_0, v0) & occurrence_of(all_36_0, v0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (15) with all_47_0, all_55_0, simplifying with % 232.75/39.62 | (48), (62), (63) gives: % 232.75/39.62 | (71) ? [v0: $i] : ($i(v0) & leaf(all_47_0, v0) & % 232.75/39.62 | subactivity_occurrence(all_47_0, all_55_0) & occurrence_of(all_55_0, % 232.75/39.62 | v0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_23) with all_36_1, all_47_2, tptp0, % 232.75/39.62 | simplifying with (3), (29), (46), (56) gives: % 232.75/39.62 | (72) ? [v0: $i] : ($i(v0) & min_precedes(v0, all_47_2, tptp0) & root(v0, % 232.75/39.62 | tptp0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_24) with all_47_2, all_47_1, tptp0, % 232.75/39.62 | simplifying with (3), (46), (47), (58) gives: % 232.75/39.62 | (73) precedes(all_47_2, all_47_1) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_06) with tptp0, all_47_1, all_47_0, % 232.75/39.62 | simplifying with (3), (47), (48), (59) gives: % 232.75/39.62 | (74) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_47_0, v0) & % 232.75/39.62 | subactivity_occurrence(all_47_1, v0) & occurrence_of(v0, tptp0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_24) with all_47_1, all_47_0, tptp0, % 232.75/39.62 | simplifying with (3), (47), (48), (59) gives: % 232.75/39.62 | (75) precedes(all_47_1, all_47_0) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_23) with all_47_1, all_47_0, tptp0, % 232.75/39.62 | simplifying with (3), (47), (48), (59) gives: % 232.75/39.62 | (76) ? [v0: $i] : ($i(v0) & min_precedes(v0, all_47_0, tptp0) & root(v0, % 232.75/39.62 | tptp0)) % 232.75/39.62 | % 232.75/39.62 | GROUND_INST: instantiating (sos_12) with all_47_2, simplifying with (46), (50) % 232.75/39.62 | gives: % 232.75/39.62 | (77) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_47_2, v0)) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (72) with fresh symbol all_69_0 gives: % 232.75/39.62 | (78) $i(all_69_0) & min_precedes(all_69_0, all_47_2, tptp0) & % 232.75/39.62 | root(all_69_0, tptp0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (78) implies: % 232.75/39.62 | (79) min_precedes(all_69_0, all_47_2, tptp0) % 232.75/39.62 | (80) $i(all_69_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (77) with fresh symbol all_75_0 gives: % 232.75/39.62 | (81) $i(all_75_0) & activity(all_75_0) & occurrence_of(all_47_2, all_75_0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (81) implies: % 232.75/39.62 | (82) occurrence_of(all_47_2, all_75_0) % 232.75/39.62 | (83) $i(all_75_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (76) with fresh symbol all_81_0 gives: % 232.75/39.62 | (84) $i(all_81_0) & min_precedes(all_81_0, all_47_0, tptp0) & % 232.75/39.62 | root(all_81_0, tptp0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (84) implies: % 232.75/39.62 | (85) min_precedes(all_81_0, all_47_0, tptp0) % 232.75/39.62 | (86) $i(all_81_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (74) with fresh symbol all_87_0 gives: % 232.75/39.62 | (87) $i(all_87_0) & subactivity_occurrence(all_47_0, all_87_0) & % 232.75/39.62 | subactivity_occurrence(all_47_1, all_87_0) & occurrence_of(all_87_0, % 232.75/39.62 | tptp0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (87) implies: % 232.75/39.62 | (88) occurrence_of(all_87_0, tptp0) % 232.75/39.62 | (89) subactivity_occurrence(all_47_0, all_87_0) % 232.75/39.62 | (90) $i(all_87_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (71) with fresh symbol all_89_0 gives: % 232.75/39.62 | (91) $i(all_89_0) & leaf(all_47_0, all_89_0) & % 232.75/39.62 | subactivity_occurrence(all_47_0, all_55_0) & occurrence_of(all_55_0, % 232.75/39.62 | all_89_0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (91) implies: % 232.75/39.62 | (92) occurrence_of(all_55_0, all_89_0) % 232.75/39.62 | (93) subactivity_occurrence(all_47_0, all_55_0) % 232.75/39.62 | (94) leaf(all_47_0, all_89_0) % 232.75/39.62 | (95) $i(all_89_0) % 232.75/39.62 | % 232.75/39.62 | DELTA: instantiating (70) with fresh symbol all_91_0 gives: % 232.75/39.62 | (96) $i(all_91_0) & subactivity_occurrence(all_45_0, all_36_0) & % 232.75/39.62 | root(all_45_0, all_91_0) & occurrence_of(all_36_0, all_91_0) % 232.75/39.62 | % 232.75/39.62 | ALPHA: (96) implies: % 232.75/39.62 | (97) occurrence_of(all_36_0, all_91_0) % 232.75/39.62 | (98) $i(all_91_0) % 232.75/39.62 | % 232.75/39.62 | BETA: splitting (68) gives: % 232.75/39.62 | % 232.75/39.62 | Case 1: % 232.75/39.62 | | % 232.75/39.62 | | (99) atomic(all_57_0) % 232.75/39.62 | | % 232.75/39.62 | | REDUCE: (67), (99) imply: % 232.75/39.62 | | (100) atomic(tptp0) % 232.75/39.62 | | % 232.75/39.62 | | PRED_UNIFY: (2), (100) imply: % 232.75/39.62 | | (101) $false % 232.75/39.63 | | % 232.75/39.63 | | CLOSE: (101) is inconsistent. % 232.75/39.63 | | % 232.75/39.63 | Case 2: % 232.75/39.63 | | % 232.75/39.63 | | (102) ~ atomic(all_57_0) % 232.75/39.63 | | (103) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_36_0) & % 232.75/39.63 | | root(v0, all_57_0)) % 232.75/39.63 | | % 232.75/39.63 | | DELTA: instantiating (103) with fresh symbol all_99_0 gives: % 232.75/39.63 | | (104) $i(all_99_0) & subactivity_occurrence(all_99_0, all_36_0) & % 232.75/39.63 | | root(all_99_0, all_57_0) % 232.75/39.63 | | % 232.75/39.63 | | ALPHA: (104) implies: % 232.75/39.63 | | (105) root(all_99_0, all_57_0) % 232.75/39.63 | | (106) subactivity_occurrence(all_99_0, all_36_0) % 232.75/39.63 | | (107) $i(all_99_0) % 232.75/39.63 | | % 232.75/39.63 | | REDUCE: (67), (105) imply: % 232.75/39.63 | | (108) root(all_99_0, tptp0) % 232.75/39.63 | | % 232.75/39.63 | | GROUND_INST: instantiating (sos_08) with all_36_0, tptp0, all_91_0, % 232.75/39.63 | | simplifying with (3), (26), (30), (97), (98) gives: % 232.75/39.63 | | (109) all_91_0 = tptp0 % 232.75/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos_08) with all_47_2, tptp3, all_75_0, % 232.84/39.63 | | simplifying with (4), (41), (46), (82), (83) gives: % 232.84/39.63 | | (110) all_75_0 = tptp3 % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos_08) with all_55_0, tptp0, all_89_0, % 232.84/39.63 | | simplifying with (3), (61), (63), (92), (95) gives: % 232.84/39.63 | | (111) all_89_0 = tptp0 % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos) with all_89_0, all_55_0, simplifying with % 232.84/39.63 | | (63), (92), (95) gives: % 232.84/39.63 | | (112) atomic(all_89_0) | ? [v0: $i] : ($i(v0) & % 232.84/39.63 | | subactivity_occurrence(v0, all_55_0) & root(v0, all_89_0)) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (17) with all_99_0, tptp0, simplifying with (3), % 232.84/39.63 | | (107), (108) gives: % 232.84/39.63 | | (113) leaf(all_99_0, tptp0) | ? [v0: $i] : ($i(v0) & % 232.84/39.63 | | min_precedes(all_99_0, v0, tptp0)) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos_27) with all_47_1, all_47_0, tptp0, % 232.84/39.63 | | all_55_0, simplifying with (3), (47), (48), (59), (61), (63), % 232.84/39.63 | | (93) gives: % 232.84/39.63 | | (114) subactivity_occurrence(all_47_1, all_55_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (16) with all_47_0, all_87_0, tptp0, simplifying % 232.84/39.63 | | with (3), (42), (48), (88), (89), (90) gives: % 232.84/39.63 | | (115) leaf_occ(all_47_0, all_87_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (22) with all_47_0, all_87_0, simplifying with % 232.84/39.63 | | (48), (89), (90) gives: % 232.84/39.63 | | (116) activity_occurrence(all_87_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (21) with all_47_0, all_87_0, simplifying with % 232.84/39.63 | | (48), (89), (90) gives: % 232.84/39.63 | | (117) activity_occurrence(all_47_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (14) with all_99_0, all_36_0, tptp0, simplifying % 232.84/39.63 | | with (3), (26), (30), (106), (107), (108) gives: % 232.84/39.63 | | (118) root_occ(all_99_0, all_36_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos_12) with all_55_0, simplifying with (63), % 232.84/39.63 | | (69) gives: % 232.84/39.63 | | (119) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_55_0, v0)) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (sos_07) with all_47_0, all_89_0, simplifying % 232.84/39.63 | | with (48), (94), (95) gives: % 232.84/39.63 | | (120) atomic(all_89_0) | ? [v0: $i] : ($i(v0) & leaf_occ(all_47_0, v0) & % 232.84/39.63 | | occurrence_of(v0, all_89_0)) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (12) with all_47_2, all_47_1, simplifying with % 232.84/39.63 | | (46), (47), (73) gives: % 232.84/39.63 | | (121) earlier(all_47_2, all_47_1) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (12) with all_47_1, all_47_0, simplifying with % 232.84/39.63 | | (47), (48), (75) gives: % 232.84/39.63 | | (122) earlier(all_47_1, all_47_0) % 232.84/39.63 | | % 232.84/39.63 | | GROUND_INST: instantiating (11) with all_47_1, all_47_0, simplifying with % 232.84/39.63 | | (47), (48), (75) gives: % 232.84/39.63 | | (123) legal(all_47_0) % 232.84/39.63 | | % 232.84/39.63 | | DELTA: instantiating (72) with fresh symbol all_113_0 gives: % 232.84/39.63 | | (124) $i(all_113_0) & min_precedes(all_113_0, all_47_2, tptp0) & % 232.84/39.63 | | root(all_113_0, tptp0) % 232.84/39.63 | | % 232.84/39.63 | | ALPHA: (124) implies: % 232.84/39.63 | | (125) min_precedes(all_113_0, all_47_2, tptp0) % 232.84/39.63 | | (126) $i(all_113_0) % 232.84/39.63 | | % 232.84/39.63 | | DELTA: instantiating (119) with fresh symbol all_115_0 gives: % 232.84/39.63 | | (127) $i(all_115_0) & activity(all_115_0) & occurrence_of(all_55_0, % 232.84/39.63 | | all_115_0) % 232.84/39.63 | | % 232.84/39.63 | | ALPHA: (127) implies: % 232.84/39.63 | | (128) occurrence_of(all_55_0, all_115_0) % 232.84/39.63 | | (129) $i(all_115_0) % 232.84/39.63 | | % 232.84/39.63 | | DELTA: instantiating (76) with fresh symbol all_121_0 gives: % 232.84/39.63 | | (130) $i(all_121_0) & min_precedes(all_121_0, all_47_0, tptp0) & % 232.84/39.63 | | root(all_121_0, tptp0) % 232.84/39.63 | | % 232.84/39.63 | | ALPHA: (130) implies: % 232.84/39.63 | | (131) min_precedes(all_121_0, all_47_0, tptp0) % 232.84/39.63 | | (132) $i(all_121_0) % 232.84/39.63 | | % 232.84/39.63 | | BETA: splitting (120) gives: % 232.84/39.63 | | % 232.84/39.63 | | Case 1: % 232.84/39.63 | | | % 232.84/39.63 | | | (133) atomic(all_89_0) % 232.84/39.63 | | | % 232.84/39.63 | | | REDUCE: (111), (133) imply: % 232.84/39.63 | | | (134) atomic(tptp0) % 232.84/39.63 | | | % 232.84/39.63 | | | PRED_UNIFY: (2), (134) imply: % 232.84/39.63 | | | (135) $false % 232.84/39.63 | | | % 232.84/39.63 | | | CLOSE: (135) is inconsistent. % 232.84/39.63 | | | % 232.84/39.63 | | Case 2: % 232.84/39.63 | | | % 232.84/39.63 | | | (136) ~ atomic(all_89_0) % 232.84/39.63 | | | (137) ? [v0: $i] : ($i(v0) & leaf_occ(all_47_0, v0) & % 232.84/39.63 | | | occurrence_of(v0, all_89_0)) % 232.84/39.63 | | | % 232.84/39.64 | | | DELTA: instantiating (137) with fresh symbol all_148_0 gives: % 232.84/39.64 | | | (138) $i(all_148_0) & leaf_occ(all_47_0, all_148_0) & % 232.84/39.64 | | | occurrence_of(all_148_0, all_89_0) % 232.84/39.64 | | | % 232.84/39.64 | | | ALPHA: (138) implies: % 232.84/39.64 | | | (139) occurrence_of(all_148_0, all_89_0) % 232.84/39.64 | | | (140) leaf_occ(all_47_0, all_148_0) % 232.84/39.64 | | | (141) $i(all_148_0) % 232.84/39.64 | | | % 232.84/39.64 | | | REDUCE: (111), (139) imply: % 232.84/39.64 | | | (142) occurrence_of(all_148_0, tptp0) % 232.84/39.64 | | | % 232.84/39.64 | | | BETA: splitting (112) gives: % 232.84/39.64 | | | % 232.84/39.64 | | | Case 1: % 232.84/39.64 | | | | % 232.84/39.64 | | | | (143) atomic(all_89_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | REDUCE: (111), (143) imply: % 232.84/39.64 | | | | (144) atomic(tptp0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | PRED_UNIFY: (2), (144) imply: % 232.84/39.64 | | | | (145) $false % 232.84/39.64 | | | | % 232.84/39.64 | | | | CLOSE: (145) is inconsistent. % 232.84/39.64 | | | | % 232.84/39.64 | | | Case 2: % 232.84/39.64 | | | | % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_08) with all_55_0, tptp0, all_115_0, % 232.84/39.64 | | | | simplifying with (3), (61), (63), (128), (129) gives: % 232.84/39.64 | | | | (146) all_115_0 = tptp0 % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_27) with all_47_2, all_47_1, tptp0, % 232.84/39.64 | | | | all_55_0, simplifying with (3), (46), (47), (58), (61), % 232.84/39.64 | | | | (63), (114) gives: % 232.84/39.64 | | | | (147) subactivity_occurrence(all_47_2, all_55_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_29) with all_45_0, all_99_0, all_36_0, % 232.84/39.64 | | | | tptp0, simplifying with (3), (26), (30), (39), (52), (107), % 232.84/39.64 | | | | (118) gives: % 232.84/39.64 | | | | (148) all_99_0 = all_45_0 % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (15) with all_47_0, all_87_0, simplifying % 232.84/39.64 | | | | with (48), (90), (115) gives: % 232.84/39.64 | | | | (149) ? [v0: $i] : ($i(v0) & leaf(all_47_0, v0) & % 232.84/39.64 | | | | subactivity_occurrence(all_47_0, all_87_0) & % 232.84/39.64 | | | | occurrence_of(all_87_0, v0)) % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (15) with all_47_0, all_148_0, simplifying % 232.84/39.64 | | | | with (48), (140), (141) gives: % 232.84/39.64 | | | | (150) ? [v0: $i] : ($i(v0) & leaf(all_47_0, v0) & % 232.84/39.64 | | | | subactivity_occurrence(all_47_0, all_148_0) & % 232.84/39.64 | | | | occurrence_of(all_148_0, v0)) % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_12) with all_47_0, simplifying with % 232.84/39.64 | | | | (48), (117) gives: % 232.84/39.64 | | | | (151) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_47_0, % 232.84/39.64 | | | | v0)) % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_12) with all_87_0, simplifying with % 232.84/39.64 | | | | (90), (116) gives: % 232.84/39.64 | | | | (152) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_87_0, % 232.84/39.64 | | | | v0)) % 232.84/39.64 | | | | % 232.84/39.64 | | | | GROUND_INST: instantiating (sos_30) with all_47_2, all_47_1, all_47_0, % 232.84/39.64 | | | | simplifying with (46), (47), (48), (121), (122) gives: % 232.84/39.64 | | | | (153) earlier(all_47_2, all_47_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (152) with fresh symbol all_165_0 gives: % 232.84/39.64 | | | | (154) $i(all_165_0) & activity(all_165_0) & occurrence_of(all_87_0, % 232.84/39.64 | | | | all_165_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (154) implies: % 232.84/39.64 | | | | (155) occurrence_of(all_87_0, all_165_0) % 232.84/39.64 | | | | (156) $i(all_165_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (151) with fresh symbol all_185_0 gives: % 232.84/39.64 | | | | (157) $i(all_185_0) & activity(all_185_0) & occurrence_of(all_47_0, % 232.84/39.64 | | | | all_185_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (157) implies: % 232.84/39.64 | | | | (158) occurrence_of(all_47_0, all_185_0) % 232.84/39.64 | | | | (159) $i(all_185_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (76) with fresh symbol all_189_0 gives: % 232.84/39.64 | | | | (160) $i(all_189_0) & min_precedes(all_189_0, all_47_0, tptp0) & % 232.84/39.64 | | | | root(all_189_0, tptp0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (160) implies: % 232.84/39.64 | | | | (161) min_precedes(all_189_0, all_47_0, tptp0) % 232.84/39.64 | | | | (162) $i(all_189_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (72) with fresh symbol all_193_0 gives: % 232.84/39.64 | | | | (163) $i(all_193_0) & min_precedes(all_193_0, all_47_2, tptp0) & % 232.84/39.64 | | | | root(all_193_0, tptp0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (163) implies: % 232.84/39.64 | | | | (164) min_precedes(all_193_0, all_47_2, tptp0) % 232.84/39.64 | | | | (165) $i(all_193_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (150) with fresh symbol all_203_0 gives: % 232.84/39.64 | | | | (166) $i(all_203_0) & leaf(all_47_0, all_203_0) & % 232.84/39.64 | | | | subactivity_occurrence(all_47_0, all_148_0) & % 232.84/39.64 | | | | occurrence_of(all_148_0, all_203_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (166) implies: % 232.84/39.64 | | | | (167) occurrence_of(all_148_0, all_203_0) % 232.84/39.64 | | | | (168) leaf(all_47_0, all_203_0) % 232.84/39.64 | | | | (169) $i(all_203_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | DELTA: instantiating (149) with fresh symbol all_205_0 gives: % 232.84/39.64 | | | | (170) $i(all_205_0) & leaf(all_47_0, all_205_0) & % 232.84/39.64 | | | | subactivity_occurrence(all_47_0, all_87_0) & % 232.84/39.64 | | | | occurrence_of(all_87_0, all_205_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | ALPHA: (170) implies: % 232.84/39.64 | | | | (171) occurrence_of(all_87_0, all_205_0) % 232.84/39.64 | | | | (172) $i(all_205_0) % 232.84/39.64 | | | | % 232.84/39.64 | | | | BETA: splitting (49) gives: % 232.84/39.64 | | | | % 232.84/39.64 | | | | Case 1: % 232.84/39.64 | | | | | % 232.84/39.64 | | | | | (173) occurrence_of(all_47_0, tptp1) % 232.84/39.64 | | | | | % 232.84/39.64 | | | | | BETA: splitting (51) gives: % 232.84/39.64 | | | | | % 232.84/39.64 | | | | | Case 1: % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_55_0, all_47_2, % 232.84/39.64 | | | | | | all_47_0, simplifying with (3), (46), (48), (57), (61), % 232.84/39.64 | | | | | | (62), (63), (147) gives: % 232.84/39.64 | | | | | | (174) all_47_0 = all_47_2 | min_precedes(all_47_2, all_47_0, % 232.84/39.64 | | | | | | tptp0) % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | GROUND_INST: instantiating (19) with all_47_2, tptp0, all_193_0, % 232.84/39.64 | | | | | | simplifying with (3), (46), (164), (165) gives: % 232.84/39.64 | | | | | | (175) leaf(all_47_2, tptp0) | ? [v0: $i] : ($i(v0) & % 232.84/39.64 | | | | | | min_precedes(all_47_2, v0, tptp0)) % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | GROUND_INST: instantiating (10) with all_47_2, all_47_0, simplifying % 232.84/39.64 | | | | | | with (46), (48), (123), (153) gives: % 232.84/39.64 | | | | | | (176) precedes(all_47_2, all_47_0) % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | REF_CLOSE: (3), (20), (32), (41), (42), (43), (46), (47), (48), % 232.84/39.64 | | | | | | (59), (173), (174), (175), (176), (sos_31) are % 232.84/39.64 | | | | | | inconsistent by sub-proof #1. % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | Case 2: % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | (177) ~ leaf(all_45_0, tptp0) % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | BETA: splitting (113) gives: % 232.84/39.64 | | | | | | % 232.84/39.64 | | | | | | Case 1: % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | (178) leaf(all_99_0, tptp0) % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | REDUCE: (148), (178) imply: % 232.84/39.64 | | | | | | | (179) leaf(all_45_0, tptp0) % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | PRED_UNIFY: (177), (179) imply: % 232.84/39.64 | | | | | | | (180) $false % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | CLOSE: (180) is inconsistent. % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | Case 2: % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | % 232.84/39.64 | | | | | | | GROUND_INST: instantiating (sos_08) with all_47_0, tptp1, % 232.84/39.64 | | | | | | | all_185_0, simplifying with (6), (48), (158), (159), % 232.84/39.64 | | | | | | | (173) gives: % 232.84/39.65 | | | | | | | (181) all_185_0 = tptp1 % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (sos_08) with all_87_0, tptp0, % 232.84/39.65 | | | | | | | all_205_0, simplifying with (3), (88), (90), (171), % 232.84/39.65 | | | | | | | (172) gives: % 232.84/39.65 | | | | | | | (182) all_205_0 = tptp0 % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (sos_08) with all_87_0, all_165_0, % 232.84/39.65 | | | | | | | all_205_0, simplifying with (90), (155), (156), % 232.84/39.65 | | | | | | | (171), (172) gives: % 232.84/39.65 | | | | | | | (183) all_205_0 = all_165_0 % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (sos_08) with all_148_0, tptp0, % 232.84/39.65 | | | | | | | all_203_0, simplifying with (3), (141), (142), (167), % 232.84/39.65 | | | | | | | (169) gives: % 232.84/39.65 | | | | | | | (184) all_203_0 = tptp0 % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_55_0, % 232.84/39.65 | | | | | | | all_47_2, all_47_0, simplifying with (3), (46), (48), % 232.84/39.65 | | | | | | | (57), (61), (62), (63), (147) gives: % 232.84/39.65 | | | | | | | (185) all_47_0 = all_47_2 | min_precedes(all_47_2, all_47_0, % 232.84/39.65 | | | | | | | tptp0) % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (19) with all_47_2, tptp0, all_193_0, % 232.84/39.65 | | | | | | | simplifying with (3), (46), (164), (165) gives: % 232.84/39.65 | | | | | | | (186) leaf(all_47_2, tptp0) | ? [v0: $i] : ($i(v0) & % 232.84/39.65 | | | | | | | min_precedes(all_47_2, v0, tptp0)) % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | GROUND_INST: instantiating (10) with all_47_2, all_47_0, % 232.84/39.65 | | | | | | | simplifying with (46), (48), (123), (153) gives: % 232.84/39.65 | | | | | | | (187) precedes(all_47_2, all_47_0) % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | COMBINE_EQS: (182), (183) imply: % 232.84/39.65 | | | | | | | (188) all_165_0 = tptp0 % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | REF_CLOSE: (3), (20), (32), (41), (42), (43), (46), (47), (48), % 232.84/39.65 | | | | | | | (59), (173), (185), (186), (187), (sos_31) are % 232.84/39.65 | | | | | | | inconsistent by sub-proof #1. % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | End of split % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | End of split % 232.84/39.65 | | | | | % 232.84/39.65 | | | | Case 2: % 232.84/39.65 | | | | | % 232.84/39.65 | | | | | (189) occurrence_of(all_47_0, tptp2) % 232.84/39.65 | | | | | % 232.84/39.65 | | | | | BETA: splitting (54) gives: % 232.84/39.65 | | | | | % 232.84/39.65 | | | | | Case 1: % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | (190) root(all_47_0, tptp0) % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_22) with all_189_0, all_47_0, tptp0, % 232.84/39.65 | | | | | | simplifying with (3), (48), (161), (162), (190) gives: % 232.84/39.65 | | | | | | (191) $false % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | CLOSE: (191) is inconsistent. % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | Case 2: % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_08) with all_47_0, tptp2, all_185_0, % 232.84/39.65 | | | | | | simplifying with (5), (48), (158), (159), (189) gives: % 232.84/39.65 | | | | | | (192) all_185_0 = tptp2 % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_08) with all_87_0, tptp0, all_205_0, % 232.84/39.65 | | | | | | simplifying with (3), (88), (90), (171), (172) gives: % 232.84/39.65 | | | | | | (193) all_205_0 = tptp0 % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_08) with all_87_0, all_165_0, % 232.84/39.65 | | | | | | all_205_0, simplifying with (90), (155), (156), (171), % 232.84/39.65 | | | | | | (172) gives: % 232.84/39.65 | | | | | | (194) all_205_0 = all_165_0 % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_08) with all_148_0, tptp0, % 232.84/39.65 | | | | | | all_203_0, simplifying with (3), (141), (142), (167), % 232.84/39.65 | | | | | | (169) gives: % 232.84/39.65 | | | | | | (195) all_203_0 = tptp0 % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_55_0, all_47_2, % 232.84/39.65 | | | | | | all_47_0, simplifying with (3), (46), (48), (57), (61), % 232.84/39.65 | | | | | | (62), (63), (147) gives: % 232.84/39.65 | | | | | | (196) all_47_0 = all_47_2 | min_precedes(all_47_2, all_47_0, % 232.84/39.65 | | | | | | tptp0) % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (19) with all_47_2, tptp0, all_193_0, % 232.84/39.65 | | | | | | simplifying with (3), (46), (164), (165) gives: % 232.84/39.65 | | | | | | (197) leaf(all_47_2, tptp0) | ? [v0: $i] : ($i(v0) & % 232.84/39.65 | | | | | | min_precedes(all_47_2, v0, tptp0)) % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | GROUND_INST: instantiating (10) with all_47_2, all_47_0, simplifying % 232.84/39.65 | | | | | | with (46), (48), (123), (153) gives: % 232.84/39.65 | | | | | | (198) precedes(all_47_2, all_47_0) % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | COMBINE_EQS: (193), (194) imply: % 232.84/39.65 | | | | | | (199) all_165_0 = tptp0 % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | BETA: splitting (197) gives: % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | | Case 1: % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | (200) leaf(all_47_2, tptp0) % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | REF_CLOSE: (3), (20), (46), (47), (48), (59), (196), (198), (200), % 232.84/39.65 | | | | | | | (sos_31) are inconsistent by sub-proof #2. % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | Case 2: % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | (201) ~ leaf(all_47_2, tptp0) % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | BETA: splitting (196) gives: % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | | Case 1: % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | (202) min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | GROUND_INST: instantiating (31) with all_47_2, all_47_0, % 232.84/39.65 | | | | | | | | simplifying with (41), (42), (43), (46), (48), % 232.84/39.65 | | | | | | | | (189), (202) gives: % 232.84/39.65 | | | | | | | | (203) $false % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | CLOSE: (203) is inconsistent. % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | Case 2: % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | (204) all_47_0 = all_47_2 % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | REDUCE: (42), (204) imply: % 232.84/39.65 | | | | | | | | (205) leaf(all_47_2, tptp0) % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | PRED_UNIFY: (201), (205) imply: % 232.84/39.65 | | | | | | | | (206) $false % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | | CLOSE: (206) is inconsistent. % 232.84/39.65 | | | | | | | | % 232.84/39.65 | | | | | | | End of split % 232.84/39.65 | | | | | | | % 232.84/39.65 | | | | | | End of split % 232.84/39.65 | | | | | | % 232.84/39.65 | | | | | End of split % 232.84/39.65 | | | | | % 232.84/39.65 | | | | End of split % 232.84/39.65 | | | | % 232.84/39.65 | | | End of split % 232.84/39.65 | | | % 232.84/39.65 | | End of split % 232.84/39.65 | | % 232.84/39.65 | End of split % 232.84/39.65 | % 232.84/39.65 End of proof % 232.84/39.65 % 232.84/39.65 Sub-proof #1 shows that the following formulas are inconsistent: % 232.84/39.65 ---------------------------------------------------------------- % 232.84/39.65 (1) occurrence_of(all_47_2, tptp3) % 232.84/39.65 (2) all_47_0 = all_47_2 | min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.65 (3) precedes(all_47_2, all_47_0) % 232.84/39.65 (4) min_precedes(all_47_1, all_47_0, tptp0) % 232.84/39.65 (5) leaf(all_47_0, tptp0) % 232.84/39.65 (6) $i(all_47_1) % 232.84/39.65 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 232.84/39.65 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ precedes(v1, v2) | ~ % 232.84/39.65 min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | % 232.84/39.65 min_precedes(v1, v2, v3)) % 232.84/39.65 (8) $i(tptp0) % 232.84/39.65 (9) occurrence_of(all_47_0, tptp1) % 232.84/39.65 (10) leaf(all_47_2, tptp0) | ? [v0: $i] : ($i(v0) & min_precedes(all_47_2, % 232.84/39.65 v0, tptp0)) % 232.84/39.65 (11) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 232.84/39.65 next_subocc(all_36_1, v0, tptp0) | ~ leaf(v1, tptp0) | ~ % 232.84/39.65 min_precedes(v0, v1, tptp0) | ~ occurrence_of(v1, tptp1) | ~ % 232.84/39.65 occurrence_of(v0, tptp3)) % 232.84/39.65 (12) $i(all_47_0) % 232.84/39.65 (13) $i(all_47_2) % 232.84/39.65 (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.84/39.65 $i(v0) | ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 232.84/39.65 (15) next_subocc(all_36_1, all_47_2, tptp0) % 232.84/39.65 % 232.84/39.65 Begin of proof % 232.84/39.65 | % 232.84/39.65 | BETA: splitting (10) gives: % 232.84/39.65 | % 232.84/39.65 | Case 1: % 232.84/39.65 | | % 232.84/39.65 | | (16) leaf(all_47_2, tptp0) % 232.84/39.65 | | % 232.84/39.65 | | REF_CLOSE: (2), (3), (4), (6), (7), (8), (12), (13), (14), (16) are % 232.84/39.65 | | inconsistent by sub-proof #2. % 232.84/39.65 | | % 232.84/39.65 | Case 2: % 232.84/39.65 | | % 232.84/39.65 | | (17) ~ leaf(all_47_2, tptp0) % 232.84/39.65 | | % 232.84/39.65 | | BETA: splitting (2) gives: % 232.84/39.65 | | % 232.84/39.65 | | Case 1: % 232.84/39.65 | | | % 232.84/39.65 | | | (18) min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.65 | | | % 232.84/39.65 | | | GROUND_INST: instantiating (11) with all_47_2, all_47_0, simplifying with % 232.84/39.65 | | | (1), (5), (9), (12), (13), (15), (18) gives: % 232.84/39.65 | | | (19) $false % 232.84/39.65 | | | % 232.84/39.65 | | | CLOSE: (19) is inconsistent. % 232.84/39.65 | | | % 232.84/39.65 | | Case 2: % 232.84/39.65 | | | % 232.84/39.65 | | | (20) all_47_0 = all_47_2 % 232.84/39.65 | | | % 232.84/39.65 | | | REDUCE: (5), (20) imply: % 232.84/39.65 | | | (21) leaf(all_47_2, tptp0) % 232.84/39.66 | | | % 232.84/39.66 | | | PRED_UNIFY: (17), (21) imply: % 232.84/39.66 | | | (22) $false % 232.84/39.66 | | | % 232.84/39.66 | | | CLOSE: (22) is inconsistent. % 232.84/39.66 | | | % 232.84/39.66 | | End of split % 232.84/39.66 | | % 232.84/39.66 | End of split % 232.84/39.66 | % 232.84/39.66 End of proof % 232.84/39.66 % 232.84/39.66 Sub-proof #2 shows that the following formulas are inconsistent: % 232.84/39.66 ---------------------------------------------------------------- % 232.84/39.66 (1) all_47_0 = all_47_2 | min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.66 (2) precedes(all_47_2, all_47_0) % 232.84/39.66 (3) min_precedes(all_47_1, all_47_0, tptp0) % 232.84/39.66 (4) $i(all_47_1) % 232.84/39.66 (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 232.84/39.66 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ precedes(v1, v2) | ~ % 232.84/39.66 min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | % 232.84/39.66 min_precedes(v1, v2, v3)) % 232.84/39.66 (6) $i(tptp0) % 232.84/39.66 (7) $i(all_47_0) % 232.84/39.66 (8) $i(all_47_2) % 232.84/39.66 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 232.84/39.66 $i(v0) | ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 232.84/39.66 (10) leaf(all_47_2, tptp0) % 232.84/39.66 % 232.84/39.66 Begin of proof % 232.84/39.66 | % 232.84/39.66 | BETA: splitting (1) gives: % 232.84/39.66 | % 232.84/39.66 | Case 1: % 232.84/39.66 | | % 232.84/39.66 | | (11) min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.66 | | % 232.84/39.66 | | GROUND_INST: instantiating (9) with all_47_2, tptp0, all_47_0, simplifying % 232.84/39.66 | | with (6), (7), (8), (10), (11) gives: % 232.84/39.66 | | (12) $false % 232.84/39.66 | | % 232.84/39.66 | | CLOSE: (12) is inconsistent. % 232.84/39.66 | | % 232.84/39.66 | Case 2: % 232.84/39.66 | | % 232.84/39.66 | | (13) all_47_0 = all_47_2 % 232.84/39.66 | | (14) ~ min_precedes(all_47_2, all_47_0, tptp0) % 232.84/39.66 | | % 232.84/39.66 | | REDUCE: (2), (13) imply: % 232.84/39.66 | | (15) precedes(all_47_2, all_47_2) % 232.84/39.66 | | % 232.84/39.66 | | REDUCE: (3), (13) imply: % 232.84/39.66 | | (16) min_precedes(all_47_1, all_47_2, tptp0) % 232.84/39.66 | | % 232.84/39.66 | | REDUCE: (13), (14) imply: % 232.84/39.66 | | (17) ~ min_precedes(all_47_2, all_47_2, tptp0) % 232.84/39.66 | | % 232.84/39.66 | | GROUND_INST: instantiating (5) with all_47_1, all_47_2, all_47_2, tptp0, % 232.84/39.66 | | simplifying with (4), (6), (8), (15), (16), (17) gives: % 232.84/39.66 | | (18) $false % 232.84/39.66 | | % 232.84/39.66 | | CLOSE: (18) is inconsistent. % 232.84/39.66 | | % 232.84/39.66 | End of split % 232.84/39.66 | % 232.84/39.66 End of proof % 232.84/39.66 % SZS output end Proof for theBenchmark % 232.84/39.66 % 232.84/39.66 39051ms %------------------------------------------------------------------------------