%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : PRO002+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 : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 13:08:44 EDT 2023 % Result : Theorem 81.09s 11.28s % Output : Proof 81.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO002+4 : TPTP v8.1.2. Released v4.0.0. % 0.11/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Aug 28 19:28:26 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.62 Running up to 7 provers in parallel. % 0.20/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.12/1.14 Prover 4: Preprocessing ... % 3.12/1.14 Prover 1: Preprocessing ... % 3.12/1.18 Prover 0: Preprocessing ... % 3.12/1.18 Prover 6: Preprocessing ... % 3.12/1.18 Prover 2: Preprocessing ... % 3.12/1.18 Prover 5: Preprocessing ... % 3.12/1.18 Prover 3: Preprocessing ... % 6.17/1.63 Prover 5: Proving ... % 6.17/1.63 Prover 2: Constructing countermodel ... % 7.65/1.78 Prover 6: Proving ... % 8.05/1.81 Prover 1: Constructing countermodel ... % 8.05/1.81 Prover 3: Constructing countermodel ... % 9.77/2.09 Prover 4: Constructing countermodel ... % 10.52/2.16 Prover 0: Proving ... % 18.21/3.22 Prover 3: gave up % 18.21/3.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.21/3.30 Prover 7: Preprocessing ... % 19.87/3.39 Prover 7: Constructing countermodel ... % 67.15/9.46 Prover 2: stopped % 67.15/9.46 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 67.58/9.53 Prover 8: Preprocessing ... % 68.53/9.68 Prover 8: Warning: ignoring some quantifiers % 68.53/9.70 Prover 8: Constructing countermodel ... % 80.63/11.27 Prover 7: Found proof (size 129) % 80.63/11.27 Prover 7: proved (8025ms) % 81.09/11.27 Prover 0: stopped % 81.09/11.27 Prover 8: stopped % 81.09/11.27 Prover 5: stopped % 81.09/11.27 Prover 6: stopped % 81.09/11.27 Prover 1: stopped % 81.09/11.27 Prover 4: stopped % 81.09/11.28 % 81.09/11.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.09/11.28 % 81.09/11.29 % SZS output start Proof for theBenchmark % 81.09/11.29 Assumptions after simplification: % 81.09/11.29 --------------------------------- % 81.09/11.29 % 81.09/11.29 (goals) % 81.09/11.30 $i(tptp0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 81.09/11.30 $i(v0) & tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 81.09/11.30 % 81.09/11.30 (sos) % 81.09/11.30 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 81.09/11.30 | atomic(v0) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v2, v1) & % 81.09/11.30 root(v2, v0))) % 81.09/11.30 % 81.09/11.30 (sos_02) % 81.09/11.30 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ $i(v3) | % 81.09/11.30 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | % 81.09/11.30 ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | % 81.09/11.30 min_precedes(v2, v3, v0)) % 81.09/11.30 % 81.09/11.30 (sos_03) % 81.09/11.30 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ occurrence_of(v1, v0) % 81.09/11.30 | activity_occurrence(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 81.09/11.30 $i(v0) | ~ occurrence_of(v1, v0) | activity(v0)) % 81.09/11.30 % 81.09/11.30 (sos_05) % 81.09/11.30 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root(v1, v0) | ? [v2: % 81.09/11.30 $i] : ($i(v2) & atocc(v1, v2) & subactivity(v2, v0))) % 81.09/11.30 % 81.09/11.30 (sos_06) % 81.09/11.31 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 81.09/11.31 ~ min_precedes(v1, v2, v0) | ? [v3: $i] : ($i(v3) & % 81.09/11.31 subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & % 81.09/11.31 occurrence_of(v3, v0))) % 81.09/11.31 % 81.09/11.31 (sos_08) % 81.09/11.31 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 81.09/11.31 ~ $i(v0) | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 81.09/11.31 % 81.09/11.31 (sos_12) % 81.09/11.31 ! [v0: $i] : ( ~ $i(v0) | ~ activity_occurrence(v0) | ? [v1: $i] : ($i(v1) % 81.09/11.31 & activity(v1) & occurrence_of(v0, v1))) % 81.09/11.31 % 81.09/11.31 (sos_14) % 81.09/11.31 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 81.09/11.31 ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | % 81.09/11.31 atocc(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.31 atocc(v0, v1) | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 81.09/11.31 occurrence_of(v0, v2))) % 81.09/11.31 % 81.09/11.31 (sos_16) % 81.09/11.31 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ arboreal(v0) | ~ % 81.09/11.31 occurrence_of(v0, v1) | atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) % 81.09/11.31 | ~ $i(v0) | ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 81.09/11.31 % 81.09/11.31 (sos_19) % 81.09/11.31 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 81.09/11.31 ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, % 81.09/11.31 v2) | root_occ(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 81.09/11.31 $i(v0) | ~ root_occ(v0, v1) | ? [v2: $i] : ($i(v2) & % 81.09/11.31 subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 81.09/11.31 % 81.09/11.31 (sos_26) % 81.09/11.32 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 81.09/11.32 | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, % 81.09/11.32 v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0: $i] : ! [v1: $i] : ! % 81.09/11.32 [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | % 81.09/11.32 min_precedes(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 81.09/11.32 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ min_precedes(v0, v1, v2) | % 81.09/11.32 next_subocc(v0, v1, v2) | ? [v3: $i] : ($i(v3) & min_precedes(v3, v1, v2) & % 81.09/11.32 min_precedes(v0, v3, v2))) % 81.09/11.32 % 81.09/11.32 (sos_29) % 81.09/11.32 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ $i(v3) | % 81.09/11.32 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ root_occ(v1, v2) | ~ root_occ(v0, % 81.09/11.32 v2) | ~ occurrence_of(v2, v3)) % 81.09/11.32 % 81.09/11.32 (sos_32) % 81.09/11.32 $i(tptp2) & $i(tptp3) & $i(tptp4) & $i(tptp0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 81.09/11.32 occurrence_of(v0, tptp0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 81.09/11.32 next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & % 81.09/11.32 occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, % 81.09/11.32 tptp3)))) % 81.09/11.32 % 81.09/11.32 (sos_45) % 81.09/11.32 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 81.09/11.32 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, % 81.09/11.32 v1, v2, v3, v4) | activity(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 81.09/11.32 : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 81.09/11.32 ~ $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0: % 81.09/11.32 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | % 81.09/11.32 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(v0, v1, v2, % 81.09/11.32 v3, v4) | root(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 81.09/11.32 [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 81.09/11.32 $i(v0) | ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 81.09/11.32 % 81.09/11.32 (sos_46) % 81.09/11.32 $i(tptp2) & $i(tptp3) & $i(tptp4) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 81.09/11.32 ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.32 send_message(tptp2, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 81.09/11.32 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.32 send_message(tptp3, v0, v1, v2, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 81.09/11.32 $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.32 send_message(tptp4, v0, v1, v2, v3)) % 81.09/11.32 % 81.09/11.32 (sos_47) % 81.09/11.32 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 81.09/11.32 $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 81.09/11.32 | ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | % 81.09/11.32 min_precedes(v3, v5, v4)) % 81.09/11.32 % 81.09/11.32 (sos_48) % 81.09/11.32 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 81.09/11.32 ~ tptp1(v0, v1, v2) | ~ atomic(v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 81.09/11.32 $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ % 81.09/11.32 atomic(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ % 81.09/11.32 $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | activity(v0)) & ! [v0: $i] : ! % 81.09/11.32 [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, % 81.09/11.32 v2) | root(v2, v1)) % 81.09/11.32 % 81.09/11.32 (sos_49) % 81.09/11.33 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 81.09/11.33 | ~ $i(v1) | ~ $i(v0) | ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | % 81.09/11.33 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & % 81.09/11.33 $i(v5) & $i(v4) & send_message(v4, v5, v6, v2, v1) & root_occ(v7, v3) & % 81.09/11.33 occurrence_of(v7, v4))) % 81.09/11.33 % 81.09/11.33 Further assumptions not needed in the proof: % 81.09/11.33 -------------------------------------------- % 81.09/11.33 sos_01, sos_04, sos_07, sos_09, sos_10, sos_11, sos_13, sos_15, sos_17, sos_18, % 81.09/11.33 sos_20, sos_21, sos_22, sos_23, sos_24, sos_25, sos_27, sos_28, sos_30, sos_31, % 81.09/11.33 sos_33, sos_34, sos_35, sos_36, sos_37, sos_38, sos_39, sos_40, sos_41, sos_42, % 81.09/11.33 sos_43, sos_44, sos_50 % 81.09/11.33 % 81.09/11.33 Those formulas are unsatisfiable: % 81.09/11.33 --------------------------------- % 81.09/11.33 % 81.09/11.33 Begin of proof % 81.09/11.33 | % 81.09/11.33 | ALPHA: (goals) implies: % 81.09/11.33 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & $i(v0) & % 81.09/11.33 | tptp1(v0, tptp0, v1) & occurrence_of(v2, v0)) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_48) implies: % 81.09/11.33 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 81.09/11.33 | $i(v0) | ~ tptp1(v0, v1, v2) | root(v2, v1)) % 81.09/11.33 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 81.09/11.33 | $i(v0) | ~ tptp1(v0, v1, v2) | ~ atomic(v0)) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_46) implies: % 81.09/11.33 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 81.09/11.33 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp3, v0, v1, v2, % 81.09/11.33 | v3)) % 81.09/11.33 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 81.09/11.33 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ send_message(tptp2, v0, v1, v2, % 81.09/11.33 | v3)) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_45) implies: % 81.09/11.33 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 81.09/11.33 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.33 | send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_32) implies: % 81.09/11.33 | (7) $i(tptp0) % 81.09/11.33 | (8) $i(tptp3) % 81.09/11.33 | (9) $i(tptp2) % 81.09/11.33 | (10) ! [v0: $i] : ( ~ $i(v0) | ~ occurrence_of(v0, tptp0) | ? [v1: $i] : % 81.09/11.33 | ? [v2: $i] : ($i(v2) & $i(v1) & next_subocc(v1, v2, tptp0) & % 81.09/11.33 | leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & % 81.09/11.33 | (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_26) implies: % 81.09/11.33 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 81.09/11.33 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ next_subocc(v0, v1, v2) | ~ % 81.09/11.33 | min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 81.09/11.33 | % 81.09/11.33 | ALPHA: (sos_19) implies: % 81.09/11.34 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ root_occ(v0, % 81.09/11.34 | v1) | ? [v2: $i] : ($i(v2) & subactivity_occurrence(v0, v1) & % 81.09/11.34 | root(v0, v2) & occurrence_of(v1, v2))) % 81.09/11.34 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 81.09/11.34 | $i(v0) | ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ % 81.09/11.34 | occurrence_of(v1, v2) | root_occ(v0, v1)) % 81.09/11.34 | % 81.09/11.34 | ALPHA: (sos_16) implies: % 81.09/11.34 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atomic(v1) | % 81.09/11.34 | ~ occurrence_of(v0, v1) | arboreal(v0)) % 81.09/11.34 | % 81.09/11.34 | ALPHA: (sos_14) implies: % 81.09/11.34 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ atocc(v0, v1) % 81.09/11.34 | | ? [v2: $i] : ($i(v2) & subactivity(v1, v2) & atomic(v2) & % 81.09/11.34 | occurrence_of(v0, v2))) % 81.09/11.34 | % 81.09/11.34 | ALPHA: (sos_03) implies: % 81.09/11.34 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 81.09/11.34 | occurrence_of(v1, v0) | activity_occurrence(v1)) % 81.09/11.34 | % 81.09/11.34 | DELTA: instantiating (1) with fresh symbols all_42_0, all_42_1, all_42_2 % 81.09/11.34 | gives: % 81.09/11.34 | (17) $i(all_42_0) & $i(all_42_1) & $i(all_42_2) & tptp1(all_42_2, tptp0, % 81.09/11.34 | all_42_1) & occurrence_of(all_42_0, all_42_2) % 81.09/11.34 | % 81.09/11.34 | ALPHA: (17) implies: % 81.09/11.34 | (18) occurrence_of(all_42_0, all_42_2) % 81.09/11.34 | (19) tptp1(all_42_2, tptp0, all_42_1) % 81.09/11.34 | (20) $i(all_42_2) % 81.09/11.34 | (21) $i(all_42_1) % 81.09/11.34 | (22) $i(all_42_0) % 81.09/11.34 | % 81.09/11.34 | GROUND_INST: instantiating (16) with all_42_2, all_42_0, simplifying with % 81.09/11.34 | (18), (20), (22) gives: % 81.09/11.34 | (23) activity_occurrence(all_42_0) % 81.09/11.34 | % 81.09/11.34 | GROUND_INST: instantiating (sos) with all_42_2, all_42_0, simplifying with % 81.09/11.34 | (18), (20), (22) gives: % 81.09/11.34 | (24) atomic(all_42_2) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 81.09/11.34 | all_42_0) & root(v0, all_42_2)) % 81.09/11.34 | % 81.09/11.34 | GROUND_INST: instantiating (sos_49) with all_42_2, tptp0, all_42_1, all_42_0, % 81.09/11.34 | simplifying with (7), (18), (19), (20), (21), (22) gives: % 81.09/11.34 | (25) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ($i(v3) & % 81.09/11.34 | $i(v2) & $i(v1) & $i(v0) & send_message(v0, v1, v2, all_42_1, tptp0) % 81.09/11.34 | & root_occ(v3, all_42_0) & occurrence_of(v3, v0)) % 81.09/11.34 | % 81.09/11.34 | GROUND_INST: instantiating (2) with all_42_2, tptp0, all_42_1, simplifying % 81.09/11.34 | with (7), (19), (20), (21) gives: % 81.09/11.34 | (26) root(all_42_1, tptp0) % 81.09/11.34 | % 81.09/11.34 | DELTA: instantiating (25) with fresh symbols all_54_0, all_54_1, all_54_2, % 81.09/11.34 | all_54_3 gives: % 81.09/11.34 | (27) $i(all_54_0) & $i(all_54_1) & $i(all_54_2) & $i(all_54_3) & % 81.09/11.34 | send_message(all_54_3, all_54_2, all_54_1, all_42_1, tptp0) & % 81.09/11.34 | root_occ(all_54_0, all_42_0) & occurrence_of(all_54_0, all_54_3) % 81.09/11.34 | % 81.09/11.34 | ALPHA: (27) implies: % 81.09/11.34 | (28) occurrence_of(all_54_0, all_54_3) % 81.09/11.34 | (29) root_occ(all_54_0, all_42_0) % 81.09/11.34 | (30) send_message(all_54_3, all_54_2, all_54_1, all_42_1, tptp0) % 81.09/11.35 | (31) $i(all_54_3) % 81.09/11.35 | (32) $i(all_54_2) % 81.09/11.35 | (33) $i(all_54_1) % 81.09/11.35 | (34) $i(all_54_0) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (16) with all_54_3, all_54_0, simplifying with % 81.09/11.35 | (28), (31), (34) gives: % 81.09/11.35 | (35) activity_occurrence(all_54_0) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (12) with all_54_0, all_42_0, simplifying with % 81.09/11.35 | (22), (29), (34) gives: % 81.09/11.35 | (36) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_54_0, all_42_0) & % 81.09/11.35 | root(all_54_0, v0) & occurrence_of(all_42_0, v0)) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (sos_12) with all_42_0, simplifying with (22), (23) % 81.09/11.35 | gives: % 81.09/11.35 | (37) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_42_0, v0)) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (sos_47) with all_54_3, all_54_2, all_54_1, % 81.09/11.35 | all_42_1, tptp0, all_54_0, simplifying with (7), (21), (28), % 81.09/11.35 | (30), (31), (32), (33), (34) gives: % 81.09/11.35 | (38) min_precedes(all_42_1, all_54_0, tptp0) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (5) with all_54_2, all_54_1, all_42_1, tptp0, % 81.09/11.35 | simplifying with (7), (21), (32), (33) gives: % 81.09/11.35 | (39) ~ send_message(tptp2, all_54_2, all_54_1, all_42_1, tptp0) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (4) with all_54_2, all_54_1, all_42_1, tptp0, % 81.09/11.35 | simplifying with (7), (21), (32), (33) gives: % 81.09/11.35 | (40) ~ send_message(tptp3, all_54_2, all_54_1, all_42_1, tptp0) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (6) with all_54_3, all_54_2, all_54_1, all_42_1, % 81.09/11.35 | tptp0, simplifying with (7), (21), (30), (31), (32), (33) gives: % 81.09/11.35 | (41) atomic(all_54_3) % 81.09/11.35 | % 81.09/11.35 | DELTA: instantiating (37) with fresh symbol all_66_0 gives: % 81.09/11.35 | (42) $i(all_66_0) & activity(all_66_0) & occurrence_of(all_42_0, all_66_0) % 81.09/11.35 | % 81.09/11.35 | ALPHA: (42) implies: % 81.09/11.35 | (43) occurrence_of(all_42_0, all_66_0) % 81.09/11.35 | (44) $i(all_66_0) % 81.09/11.35 | % 81.09/11.35 | DELTA: instantiating (36) with fresh symbol all_70_0 gives: % 81.09/11.35 | (45) $i(all_70_0) & subactivity_occurrence(all_54_0, all_42_0) & % 81.09/11.35 | root(all_54_0, all_70_0) & occurrence_of(all_42_0, all_70_0) % 81.09/11.35 | % 81.09/11.35 | ALPHA: (45) implies: % 81.09/11.35 | (46) occurrence_of(all_42_0, all_70_0) % 81.09/11.35 | (47) root(all_54_0, all_70_0) % 81.09/11.35 | (48) $i(all_70_0) % 81.09/11.35 | % 81.09/11.35 | PRED_UNIFY: (30), (40) imply: % 81.09/11.35 | (49) ~ (all_54_3 = tptp3) % 81.09/11.35 | % 81.09/11.35 | PRED_UNIFY: (30), (39) imply: % 81.09/11.35 | (50) ~ (all_54_3 = tptp2) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (sos_08) with all_42_0, all_54_3, all_66_0, % 81.09/11.35 | simplifying with (22), (31), (43), (44) gives: % 81.09/11.35 | (51) all_66_0 = all_54_3 | ~ occurrence_of(all_42_0, all_54_3) % 81.09/11.35 | % 81.09/11.35 | GROUND_INST: instantiating (sos) with all_66_0, all_42_0, simplifying with % 81.09/11.35 | (22), (43), (44) gives: % 81.09/11.35 | (52) atomic(all_66_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 81.09/11.35 | all_42_0) & root(v0, all_66_0)) % 81.09/11.35 | % 81.51/11.35 | GROUND_INST: instantiating (sos_08) with all_42_0, all_42_2, all_70_0, % 81.51/11.35 | simplifying with (18), (20), (22), (46), (48) gives: % 81.51/11.35 | (53) all_70_0 = all_42_2 % 81.51/11.35 | % 81.51/11.36 | GROUND_INST: instantiating (sos_08) with all_42_0, all_66_0, all_70_0, % 81.51/11.36 | simplifying with (22), (43), (44), (46), (48) gives: % 81.51/11.36 | (54) all_70_0 = all_66_0 % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (sos) with all_70_0, all_42_0, simplifying with % 81.51/11.36 | (22), (46), (48) gives: % 81.51/11.36 | (55) atomic(all_70_0) | ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, % 81.51/11.36 | all_42_0) & root(v0, all_70_0)) % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (3) with all_42_2, tptp0, all_42_1, simplifying % 81.51/11.36 | with (7), (19), (20), (21) gives: % 81.51/11.36 | (56) ~ atomic(all_42_2) % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (14) with all_54_0, all_54_3, simplifying with % 81.51/11.36 | (28), (31), (34), (41) gives: % 81.51/11.36 | (57) arboreal(all_54_0) % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (sos_05) with all_70_0, all_54_0, simplifying with % 81.51/11.36 | (34), (47), (48) gives: % 81.51/11.36 | (58) ? [v0: $i] : ($i(v0) & atocc(all_54_0, v0) & subactivity(v0, % 81.51/11.36 | all_70_0)) % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (sos_06) with tptp0, all_42_1, all_54_0, % 81.51/11.36 | simplifying with (7), (21), (34), (38) gives: % 81.51/11.36 | (59) ? [v0: $i] : ($i(v0) & subactivity_occurrence(all_54_0, v0) & % 81.51/11.36 | subactivity_occurrence(all_42_1, v0) & occurrence_of(v0, tptp0)) % 81.51/11.36 | % 81.51/11.36 | GROUND_INST: instantiating (sos_12) with all_54_0, simplifying with (34), (35) % 81.51/11.36 | gives: % 81.51/11.36 | (60) ? [v0: $i] : ($i(v0) & activity(v0) & occurrence_of(all_54_0, v0)) % 81.51/11.36 | % 81.51/11.36 | COMBINE_EQS: (53), (54) imply: % 81.51/11.36 | (61) all_66_0 = all_42_2 % 81.51/11.36 | % 81.51/11.36 | DELTA: instantiating (60) with fresh symbol all_82_0 gives: % 81.51/11.36 | (62) $i(all_82_0) & activity(all_82_0) & occurrence_of(all_54_0, all_82_0) % 81.51/11.36 | % 81.51/11.36 | ALPHA: (62) implies: % 81.51/11.36 | (63) occurrence_of(all_54_0, all_82_0) % 81.51/11.36 | (64) $i(all_82_0) % 81.51/11.36 | % 81.51/11.36 | DELTA: instantiating (58) with fresh symbol all_86_0 gives: % 81.51/11.36 | (65) $i(all_86_0) & atocc(all_54_0, all_86_0) & subactivity(all_86_0, % 81.51/11.36 | all_70_0) % 81.51/11.36 | % 81.51/11.36 | ALPHA: (65) implies: % 81.51/11.36 | (66) atocc(all_54_0, all_86_0) % 81.51/11.36 | (67) $i(all_86_0) % 81.51/11.36 | % 81.51/11.36 | DELTA: instantiating (59) with fresh symbol all_90_0 gives: % 81.51/11.36 | (68) $i(all_90_0) & subactivity_occurrence(all_54_0, all_90_0) & % 81.51/11.36 | subactivity_occurrence(all_42_1, all_90_0) & occurrence_of(all_90_0, % 81.51/11.36 | tptp0) % 81.51/11.36 | % 81.51/11.36 | ALPHA: (68) implies: % 81.51/11.36 | (69) occurrence_of(all_90_0, tptp0) % 81.51/11.36 | (70) subactivity_occurrence(all_42_1, all_90_0) % 81.51/11.36 | (71) subactivity_occurrence(all_54_0, all_90_0) % 81.51/11.36 | (72) $i(all_90_0) % 81.51/11.36 | % 81.51/11.36 | BETA: splitting (24) gives: % 81.51/11.36 | % 81.51/11.36 | Case 1: % 81.51/11.36 | | % 81.51/11.36 | | (73) atomic(all_42_2) % 81.51/11.36 | | % 81.51/11.36 | | PRED_UNIFY: (56), (73) imply: % 81.51/11.36 | | (74) $false % 81.51/11.36 | | % 81.51/11.36 | | CLOSE: (74) is inconsistent. % 81.51/11.36 | | % 81.51/11.36 | Case 2: % 81.51/11.36 | | % 81.51/11.36 | | (75) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 81.51/11.36 | | root(v0, all_42_2)) % 81.51/11.36 | | % 81.51/11.36 | | DELTA: instantiating (75) with fresh symbol all_98_0 gives: % 81.51/11.37 | | (76) $i(all_98_0) & subactivity_occurrence(all_98_0, all_42_0) & % 81.51/11.37 | | root(all_98_0, all_42_2) % 81.51/11.37 | | % 81.51/11.37 | | ALPHA: (76) implies: % 81.51/11.37 | | (77) root(all_98_0, all_42_2) % 81.51/11.37 | | (78) subactivity_occurrence(all_98_0, all_42_0) % 81.51/11.37 | | (79) $i(all_98_0) % 81.51/11.37 | | % 81.51/11.37 | | BETA: splitting (52) gives: % 81.51/11.37 | | % 81.51/11.37 | | Case 1: % 81.51/11.37 | | | % 81.51/11.37 | | | (80) atomic(all_66_0) % 81.51/11.37 | | | % 81.51/11.37 | | | REDUCE: (61), (80) imply: % 81.51/11.37 | | | (81) atomic(all_42_2) % 81.51/11.37 | | | % 81.51/11.37 | | | PRED_UNIFY: (56), (81) imply: % 81.51/11.37 | | | (82) $false % 81.51/11.37 | | | % 81.51/11.37 | | | CLOSE: (82) is inconsistent. % 81.51/11.37 | | | % 81.51/11.37 | | Case 2: % 81.51/11.37 | | | % 81.51/11.37 | | | (83) ~ atomic(all_66_0) % 81.51/11.37 | | | (84) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 81.51/11.37 | | | root(v0, all_66_0)) % 81.51/11.37 | | | % 81.51/11.37 | | | DELTA: instantiating (84) with fresh symbol all_103_0 gives: % 81.51/11.37 | | | (85) $i(all_103_0) & subactivity_occurrence(all_103_0, all_42_0) & % 81.51/11.37 | | | root(all_103_0, all_66_0) % 81.51/11.37 | | | % 81.51/11.37 | | | ALPHA: (85) implies: % 81.51/11.37 | | | (86) root(all_103_0, all_66_0) % 81.51/11.37 | | | (87) subactivity_occurrence(all_103_0, all_42_0) % 81.51/11.37 | | | (88) $i(all_103_0) % 81.51/11.37 | | | % 81.51/11.37 | | | REDUCE: (61), (86) imply: % 81.51/11.37 | | | (89) root(all_103_0, all_42_2) % 81.51/11.37 | | | % 81.51/11.37 | | | BETA: splitting (55) gives: % 81.51/11.37 | | | % 81.51/11.37 | | | Case 1: % 81.51/11.37 | | | | % 81.51/11.37 | | | | (90) atomic(all_70_0) % 81.51/11.37 | | | | % 81.51/11.37 | | | | REDUCE: (53), (90) imply: % 81.51/11.37 | | | | (91) atomic(all_42_2) % 81.51/11.37 | | | | % 81.51/11.37 | | | | PRED_UNIFY: (56), (91) imply: % 81.51/11.37 | | | | (92) $false % 81.51/11.37 | | | | % 81.51/11.37 | | | | CLOSE: (92) is inconsistent. % 81.51/11.37 | | | | % 81.51/11.37 | | | Case 2: % 81.51/11.37 | | | | % 81.51/11.37 | | | | (93) ~ atomic(all_70_0) % 81.51/11.37 | | | | (94) ? [v0: $i] : ($i(v0) & subactivity_occurrence(v0, all_42_0) & % 81.51/11.37 | | | | root(v0, all_70_0)) % 81.51/11.37 | | | | % 81.51/11.37 | | | | DELTA: instantiating (94) with fresh symbol all_108_0 gives: % 81.51/11.37 | | | | (95) $i(all_108_0) & subactivity_occurrence(all_108_0, all_42_0) & % 81.51/11.37 | | | | root(all_108_0, all_70_0) % 81.51/11.37 | | | | % 81.51/11.37 | | | | ALPHA: (95) implies: % 81.51/11.37 | | | | (96) root(all_108_0, all_70_0) % 81.51/11.37 | | | | (97) subactivity_occurrence(all_108_0, all_42_0) % 81.51/11.37 | | | | (98) $i(all_108_0) % 81.51/11.37 | | | | % 81.51/11.37 | | | | REDUCE: (53), (96) imply: % 81.51/11.37 | | | | (99) root(all_108_0, all_42_2) % 81.51/11.37 | | | | % 81.51/11.37 | | | | PRED_UNIFY: (41), (56) imply: % 81.51/11.37 | | | | (100) ~ (all_54_3 = all_42_2) % 81.51/11.37 | | | | % 81.51/11.37 | | | | BETA: splitting (51) gives: % 81.51/11.37 | | | | % 81.51/11.37 | | | | Case 1: % 81.51/11.37 | | | | | % 81.51/11.37 | | | | | % 81.51/11.37 | | | | | GROUND_INST: instantiating (sos_08) with all_54_0, all_54_3, all_82_0, % 81.51/11.37 | | | | | simplifying with (28), (31), (34), (63), (64) gives: % 81.51/11.37 | | | | | (101) all_82_0 = all_54_3 % 81.51/11.37 | | | | | % 81.51/11.37 | | | | | GROUND_INST: instantiating (10) with all_90_0, simplifying with (69), % 81.51/11.37 | | | | | (72) gives: % 81.51/11.37 | | | | | (102) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & % 81.51/11.37 | | | | | next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_90_0) & % 81.51/11.37 | | | | | root_occ(v0, all_90_0) & occurrence_of(v0, tptp4) & % 81.51/11.37 | | | | | (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 81.51/11.37 | | | | | % 81.51/11.37 | | | | | GROUND_INST: instantiating (13) with all_42_1, all_90_0, tptp0, % 81.51/11.37 | | | | | simplifying with (7), (21), (26), (69), (70), (72) gives: % 81.51/11.37 | | | | | (103) root_occ(all_42_1, all_90_0) % 81.51/11.37 | | | | | % 81.51/11.37 | | | | | GROUND_INST: instantiating (13) with all_98_0, all_42_0, all_42_2, % 81.51/11.37 | | | | | simplifying with (18), (20), (22), (77), (78), (79) % 81.51/11.37 | | | | | gives: % 81.51/11.38 | | | | | (104) root_occ(all_98_0, all_42_0) % 81.51/11.38 | | | | | % 81.51/11.38 | | | | | GROUND_INST: instantiating (13) with all_103_0, all_42_0, all_42_2, % 81.51/11.38 | | | | | simplifying with (18), (20), (22), (87), (88), (89) % 81.51/11.38 | | | | | gives: % 81.51/11.38 | | | | | (105) root_occ(all_103_0, all_42_0) % 81.51/11.38 | | | | | % 81.51/11.38 | | | | | GROUND_INST: instantiating (13) with all_108_0, all_42_0, all_42_2, % 81.51/11.38 | | | | | simplifying with (18), (20), (22), (97), (98), (99) % 81.51/11.38 | | | | | gives: % 81.51/11.38 | | | | | (106) root_occ(all_108_0, all_42_0) % 81.51/11.38 | | | | | % 81.51/11.38 | | | | | GROUND_INST: instantiating (15) with all_54_0, all_86_0, simplifying % 81.51/11.38 | | | | | with (34), (66), (67) gives: % 81.51/11.38 | | | | | (107) ? [v0: $i] : ($i(v0) & subactivity(all_86_0, v0) & % 81.51/11.38 | | | | | atomic(v0) & occurrence_of(all_54_0, v0)) % 81.68/11.38 | | | | | % 81.68/11.38 | | | | | DELTA: instantiating (107) with fresh symbol all_140_0 gives: % 81.68/11.39 | | | | | (108) $i(all_140_0) & subactivity(all_86_0, all_140_0) & % 81.68/11.39 | | | | | atomic(all_140_0) & occurrence_of(all_54_0, all_140_0) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | ALPHA: (108) implies: % 81.68/11.39 | | | | | (109) occurrence_of(all_54_0, all_140_0) % 81.68/11.39 | | | | | (110) $i(all_140_0) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | DELTA: instantiating (102) with fresh symbols all_146_0, all_146_1 % 81.68/11.39 | | | | | gives: % 81.68/11.39 | | | | | (111) $i(all_146_0) & $i(all_146_1) & next_subocc(all_146_1, % 81.68/11.39 | | | | | all_146_0, tptp0) & leaf_occ(all_146_0, all_90_0) & % 81.68/11.39 | | | | | root_occ(all_146_1, all_90_0) & occurrence_of(all_146_1, % 81.68/11.39 | | | | | tptp4) & (occurrence_of(all_146_0, tptp2) | % 81.68/11.39 | | | | | occurrence_of(all_146_0, tptp3)) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | ALPHA: (111) implies: % 81.68/11.39 | | | | | (112) root_occ(all_146_1, all_90_0) % 81.68/11.39 | | | | | (113) leaf_occ(all_146_0, all_90_0) % 81.68/11.39 | | | | | (114) next_subocc(all_146_1, all_146_0, tptp0) % 81.68/11.39 | | | | | (115) $i(all_146_1) % 81.68/11.39 | | | | | (116) $i(all_146_0) % 81.68/11.39 | | | | | (117) occurrence_of(all_146_0, tptp2) | occurrence_of(all_146_0, % 81.68/11.39 | | | | | tptp3) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_08) with all_54_0, all_54_3, % 81.68/11.39 | | | | | all_140_0, simplifying with (28), (31), (34), (109), % 81.68/11.39 | | | | | (110) gives: % 81.68/11.39 | | | | | (118) all_140_0 = all_54_3 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_29) with all_98_0, all_103_0, % 81.68/11.39 | | | | | all_42_0, all_42_2, simplifying with (18), (20), (22), % 81.68/11.39 | | | | | (79), (88), (104), (105) gives: % 81.68/11.39 | | | | | (119) all_103_0 = all_98_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_29) with all_54_0, all_108_0, % 81.68/11.39 | | | | | all_42_0, all_42_2, simplifying with (18), (20), (22), % 81.68/11.39 | | | | | (29), (34), (98), (106) gives: % 81.68/11.39 | | | | | (120) all_108_0 = all_54_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_29) with all_103_0, all_108_0, % 81.68/11.39 | | | | | all_42_0, all_42_2, simplifying with (18), (20), (22), % 81.68/11.39 | | | | | (88), (98), (105), (106) gives: % 81.68/11.39 | | | | | (121) all_108_0 = all_103_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_29) with all_42_1, all_146_1, % 81.68/11.39 | | | | | all_90_0, tptp0, simplifying with (7), (21), (69), (72), % 81.68/11.39 | | | | | (103), (112), (115) gives: % 81.68/11.39 | | | | | (122) all_146_1 = all_42_1 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | GROUND_INST: instantiating (sos_02) with tptp0, all_90_0, all_54_0, % 81.68/11.39 | | | | | all_146_0, simplifying with (7), (34), (57), (69), (71), % 81.68/11.39 | | | | | (72), (113), (116) gives: % 81.68/11.39 | | | | | (123) all_146_0 = all_54_0 | min_precedes(all_54_0, all_146_0, % 81.68/11.39 | | | | | tptp0) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | COMBINE_EQS: (120), (121) imply: % 81.68/11.39 | | | | | (124) all_103_0 = all_54_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | SIMP: (124) implies: % 81.68/11.39 | | | | | (125) all_103_0 = all_54_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | COMBINE_EQS: (119), (125) imply: % 81.68/11.39 | | | | | (126) all_98_0 = all_54_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | SIMP: (126) implies: % 81.68/11.39 | | | | | (127) all_98_0 = all_54_0 % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | REDUCE: (114), (122) imply: % 81.68/11.39 | | | | | (128) next_subocc(all_42_1, all_146_0, tptp0) % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | BETA: splitting (117) gives: % 81.68/11.39 | | | | | % 81.68/11.39 | | | | | Case 1: % 81.68/11.39 | | | | | | % 81.68/11.39 | | | | | | (129) occurrence_of(all_146_0, tptp2) % 81.68/11.39 | | | | | | % 81.68/11.39 | | | | | | BETA: splitting (123) gives: % 81.68/11.39 | | | | | | % 81.68/11.39 | | | | | | Case 1: % 81.68/11.39 | | | | | | | % 81.68/11.39 | | | | | | | (130) min_precedes(all_54_0, all_146_0, tptp0) % 81.68/11.39 | | | | | | | % 81.68/11.39 | | | | | | | GROUND_INST: instantiating (11) with all_42_1, all_146_0, tptp0, % 81.68/11.39 | | | | | | | all_54_0, simplifying with (7), (21), (34), (38), % 81.68/11.39 | | | | | | | (116), (128), (130) gives: % 81.68/11.39 | | | | | | | (131) $false % 81.68/11.39 | | | | | | | % 81.68/11.39 | | | | | | | CLOSE: (131) is inconsistent. % 81.68/11.39 | | | | | | | % 81.68/11.39 | | | | | | Case 2: % 81.68/11.39 | | | | | | | % 81.68/11.40 | | | | | | | (132) all_146_0 = all_54_0 % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | REDUCE: (129), (132) imply: % 81.68/11.40 | | | | | | | (133) occurrence_of(all_54_0, tptp2) % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | GROUND_INST: instantiating (sos_08) with all_54_0, all_54_3, % 81.68/11.40 | | | | | | | tptp2, simplifying with (9), (28), (31), (34), (133) % 81.68/11.40 | | | | | | | gives: % 81.68/11.40 | | | | | | | (134) all_54_3 = tptp2 % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | REDUCE: (50), (134) imply: % 81.68/11.40 | | | | | | | (135) $false % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | CLOSE: (135) is inconsistent. % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | End of split % 81.68/11.40 | | | | | | % 81.68/11.40 | | | | | Case 2: % 81.68/11.40 | | | | | | % 81.68/11.40 | | | | | | (136) occurrence_of(all_146_0, tptp3) % 81.68/11.40 | | | | | | % 81.68/11.40 | | | | | | BETA: splitting (123) gives: % 81.68/11.40 | | | | | | % 81.68/11.40 | | | | | | Case 1: % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | (137) min_precedes(all_54_0, all_146_0, tptp0) % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | GROUND_INST: instantiating (11) with all_42_1, all_146_0, tptp0, % 81.68/11.40 | | | | | | | all_54_0, simplifying with (7), (21), (34), (38), % 81.68/11.40 | | | | | | | (116), (128), (137) gives: % 81.68/11.40 | | | | | | | (138) $false % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | CLOSE: (138) is inconsistent. % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | Case 2: % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | (139) all_146_0 = all_54_0 % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | REDUCE: (136), (139) imply: % 81.68/11.40 | | | | | | | (140) occurrence_of(all_54_0, tptp3) % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | GROUND_INST: instantiating (sos_08) with all_54_0, all_54_3, % 81.68/11.40 | | | | | | | tptp3, simplifying with (8), (28), (31), (34), (140) % 81.68/11.40 | | | | | | | gives: % 81.68/11.40 | | | | | | | (141) all_54_3 = tptp3 % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | REDUCE: (49), (141) imply: % 81.68/11.40 | | | | | | | (142) $false % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | | CLOSE: (142) is inconsistent. % 81.68/11.40 | | | | | | | % 81.68/11.40 | | | | | | End of split % 81.68/11.40 | | | | | | % 81.68/11.40 | | | | | End of split % 81.68/11.40 | | | | | % 81.68/11.40 | | | | Case 2: % 81.68/11.40 | | | | | % 81.68/11.40 | | | | | (143) all_66_0 = all_54_3 % 81.68/11.40 | | | | | % 81.68/11.40 | | | | | COMBINE_EQS: (61), (143) imply: % 81.68/11.40 | | | | | (144) all_54_3 = all_42_2 % 81.68/11.40 | | | | | % 81.68/11.40 | | | | | REDUCE: (100), (144) imply: % 81.68/11.40 | | | | | (145) $false % 81.68/11.40 | | | | | % 81.68/11.40 | | | | | CLOSE: (145) is inconsistent. % 81.68/11.40 | | | | | % 81.68/11.40 | | | | End of split % 81.68/11.40 | | | | % 81.68/11.40 | | | End of split % 81.68/11.40 | | | % 81.68/11.40 | | End of split % 81.68/11.40 | | % 81.68/11.40 | End of split % 81.68/11.40 | % 81.68/11.40 End of proof % 81.68/11.40 % SZS output end Proof for theBenchmark % 81.68/11.40 % 81.68/11.40 10793ms %------------------------------------------------------------------------------