%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n006.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 : 600s % DateTime : Mon Jul 18 17:43:50 EDT 2022 % Result : Theorem 72.36s 36.96s % Output : Proof 78.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n006.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 : 600 % 0.13/0.34 % DateTime : Mon Jun 13 01:59:42 EDT 2022 % 0.13/0.34 % CPUTime : % 0.62/0.60 ____ _ % 0.62/0.60 ___ / __ \_____(_)___ ________ __________ % 0.62/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.62/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.62/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.62/0.60 % 0.62/0.60 A Theorem Prover for First-Order Logic % 0.62/0.60 (ePrincess v.1.0) % 0.62/0.60 % 0.62/0.60 (c) Philipp Rümmer, 2009-2015 % 0.62/0.60 (c) Peter Backeman, 2014-2015 % 0.62/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.62/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.62/0.60 Bug reports to peter@backeman.se % 0.62/0.60 % 0.62/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.62/0.60 % 0.62/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.68/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.77/1.00 Prover 0: Preprocessing ... % 2.60/1.26 Prover 0: Constructing countermodel ... % 21.04/5.94 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 21.34/6.03 Prover 1: Preprocessing ... % 22.31/6.23 Prover 1: Constructing countermodel ... % 31.75/8.54 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 32.12/8.60 Prover 2: Preprocessing ... % 32.71/8.77 Prover 2: Warning: ignoring some quantifiers % 32.71/8.78 Prover 2: Constructing countermodel ... % 40.97/11.56 Prover 0: stopped % 41.32/11.76 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 41.45/11.81 Prover 3: Preprocessing ... % 41.45/11.83 Prover 3: Constructing countermodel ... % 72.36/36.96 Prover 3: proved (25203ms) % 72.36/36.96 Prover 1: stopped % 72.36/36.96 Prover 2: stopped % 72.36/36.96 % 72.36/36.96 No countermodel exists, formula is valid % 72.36/36.96 % SZS status Theorem for theBenchmark % 72.36/36.96 % 72.36/36.96 Generating proof ... found it (size 152) % 77.99/38.32 % 77.99/38.32 % SZS output start Proof for theBenchmark % 77.99/38.32 Assumed formulas after preprocessing and simplification: % 77.99/38.32 | (0) ? [v0] : ? [v1] : ? [v2] : ( ~ (tptp5 = tptp2) & ~ (tptp5 = tptp3) & ~ (tptp5 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp3 = tptp4) & tptp1(v0, tptp0, v1) & activity(tptp0) & atomic(tptp5) & atomic(tptp2) & atomic(tptp3) & atomic(tptp4) & occurrence_of(v2, v0) & ~ atomic(tptp0) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ tptp1(v3, v4, v5) | ~ transmit_message(v3, v6, v7, v8, v9)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ transmit_message(v3, v4, v5, v6, v7) | ~ occurrence_of(v8, v3) | ? [v9] : ? [v10] : (send_message(v9, v4, v5, v6, v7) & root_occ(v10, v8) & occurrence_of(v10, v9))) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ send_message(v3, v4, v5, v6, v7) | ~ occurrence_of(v8, v3) | min_precedes(v6, v8, v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ transmit_message(v3, v4, v5, v6, v7) | ~ atomic(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ transmit_message(v3, v4, v5, v6, v7) | activity(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ transmit_message(v3, v4, v5, v6, v7) | root(v6, v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ transmit_message(v3, v4, v5, v6, v7) | root(v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ send_message(v3, v4, v5, v6, v7) | activity(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ send_message(v3, v4, v5, v6, v7) | root(v6, v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ send_message(v3, v4, v5, v6, v7) | root(v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ send_message(v3, v4, v5, v6, v7) | atomic(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v5 | ~ subactivity_occurrence(v6, v4) | ~ subactivity_occurrence(v5, v4) | ~ arboreal(v6) | ~ arboreal(v5) | ~ occurrence_of(v4, v3) | min_precedes(v6, v5, v3) | min_precedes(v5, v6, v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ leaf_occ(v4, v5) | ~ leaf_occ(v3, v5) | ~ occurrence_of(v5, v6) | atomic(v6)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ root_occ(v4, v5) | ~ root_occ(v3, v5) | ~ occurrence_of(v5, v6)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ tptp1(v3, v4, v5) | ~ occurrence_of(v6, v3) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : (transmit_message(v7, v8, v9, v5, v4) & subactivity_occurrence(v10, v6) & occurrence_of(v10, v7))) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ~ transmit_message(tptp0, v3, v4, v5, v6) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ~ send_message(tptp2, v3, v4, v5, v6) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ~ send_message(tptp3, v3, v4, v5, v6) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ~ send_message(tptp4, v3, v4, v5, v6) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ next_subocc(v3, v4, v5) | ~ min_precedes(v6, v4, v5) | ~ min_precedes(v3, v6, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ leaf_occ(v4, v3) | ~ occurrence_of(v3, v5) | ~ min_precedes(v4, v6, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ root_occ(v4, v3) | ~ occurrence_of(v3, v5) | ~ min_precedes(v6, v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ min_precedes(v4, v5, v6) | ~ min_precedes(v3, v4, v6) | min_precedes(v3, v5, v6)) & ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ occurrence_of(v3, v5) | ~ occurrence_of(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ tptp1(v3, v4, v5) | ~ atomic(v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ tptp1(v3, v4, v5) | ~ atomic(v3)) & ! [v3] : ! [v4] : ! [v5] : ( ~ tptp1(v3, v4, v5) | activity(v3)) & ! [v3] : ! [v4] : ! [v5] : ( ~ tptp1(v3, v4, v5) | root(v5, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ subactivity(v4, v5) | ~ atomic(v5) | ~ occurrence_of(v3, v5) | atocc(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ leaf(v3, v5) | ~ subactivity_occurrence(v3, v4) | ~ occurrence_of(v4, v5) | leaf_occ(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ leaf(v3, v4) | ~ min_precedes(v3, v5, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ subactivity_occurrence(v3, v4) | ~ root(v3, v5) | ~ occurrence_of(v4, v5) | root_occ(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ root(v4, v5) | ~ min_precedes(v3, v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ next_subocc(v3, v4, v5) | arboreal(v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ next_subocc(v3, v4, v5) | arboreal(v3)) & ! [v3] : ! [v4] : ! [v5] : ( ~ next_subocc(v3, v4, v5) | min_precedes(v3, v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ earlier(v4, v5) | ~ earlier(v3, v4) | earlier(v3, v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v5, v3, v4) | leaf(v3, v4) | ? [v6] : min_precedes(v3, v6, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v4, v5, v3) | ? [v6] : ? [v7] : (subactivity(v7, v3) & subactivity(v6, v3) & atocc(v5, v7) & atocc(v4, v6))) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v4, v5, v3) | ? [v6] : (subactivity_occurrence(v5, v6) & subactivity_occurrence(v4, v6) & occurrence_of(v6, v3))) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | precedes(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | next_subocc(v3, v4, v5) | ? [v6] : (min_precedes(v6, v4, v5) & min_precedes(v3, v6, v5))) & ! [v3] : ! [v4] : ~ tptp1(tptp0, v3, v4) & ! [v3] : ! [v4] : ( ~ atocc(v3, v4) | ~ legal(v3) | root(v3, v4)) & ! [v3] : ! [v4] : ( ~ atocc(v3, v4) | ? [v5] : (subactivity(v4, v5) & atomic(v5) & occurrence_of(v3, v5))) & ! [v3] : ! [v4] : ( ~ leaf(v3, v4) | root(v3, v4) | ? [v5] : min_precedes(v5, v3, v4)) & ! [v3] : ! [v4] : ( ~ leaf(v3, v4) | atomic(v4) | ? [v5] : (leaf_occ(v3, v5) & occurrence_of(v5, v4))) & ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v3, v4) | activity_occurrence(v4)) & ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v3, v4) | activity_occurrence(v3)) & ! [v3] : ! [v4] : ( ~ legal(v4) | ~ earlier(v3, v4) | precedes(v3, v4)) & ! [v3] : ! [v4] : ( ~ root(v4, v3) | ? [v5] : (subactivity(v5, v3) & atocc(v4, v5))) & ! [v3] : ! [v4] : ( ~ root(v3, v4) | leaf(v3, v4) | ? [v5] : min_precedes(v3, v5, v4)) & ! [v3] : ! [v4] : ( ~ root(v3, v4) | legal(v3)) & ! [v3] : ! [v4] : ( ~ precedes(v3, v4) | legal(v4)) & ! [v3] : ! [v4] : ( ~ precedes(v3, v4) | earlier(v3, v4)) & ! [v3] : ! [v4] : ( ~ arboreal(v3) | ~ occurrence_of(v3, v4) | atomic(v4)) & ! [v3] : ! [v4] : ( ~ leaf_occ(v3, v4) | ? [v5] : (leaf(v3, v5) & subactivity_occurrence(v3, v4) & occurrence_of(v4, v5))) & ! [v3] : ! [v4] : ( ~ atomic(v4) | ~ occurrence_of(v3, v4) | arboreal(v3)) & ! [v3] : ! [v4] : ( ~ root_occ(v3, v4) | ? [v5] : (subactivity_occurrence(v3, v4) & root(v3, v5) & occurrence_of(v4, v5))) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | activity(v3)) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | activity_occurrence(v4)) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | atomic(v3) | ? [v5] : (subactivity_occurrence(v5, v4) & root(v5, v3))) & ! [v3] : ! [v4] : ( ~ earlier(v4, v3) | ~ earlier(v3, v4)) & ! [v3] : ( ~ activity(v3) | subactivity(v3, v3)) & ! [v3] : ( ~ activity_occurrence(v3) | ? [v4] : (activity(v4) & occurrence_of(v3, v4))) & ! [v3] : ( ~ legal(v3) | arboreal(v3)) & ! [v3] : ( ~ occurrence_of(v3, tptp0) | ? [v4] : ? [v5] : (next_subocc(v4, v5, tptp0) & leaf_occ(v5, v3) & root_occ(v4, v3) & occurrence_of(v4, tptp4) & (occurrence_of(v5, tptp2) | occurrence_of(v5, tptp3))))) % 77.99/38.35 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2 yields: % 77.99/38.35 | (1) ~ (tptp5 = tptp2) & ~ (tptp5 = tptp3) & ~ (tptp5 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp3 = tptp4) & tptp1(all_0_2_2, tptp0, all_0_1_1) & activity(tptp0) & atomic(tptp5) & atomic(tptp2) & atomic(tptp3) & atomic(tptp4) & occurrence_of(all_0_0_0, all_0_2_2) & ~ atomic(tptp0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ tptp1(v0, v1, v2) | ~ transmit_message(v0, v3, v4, v5, v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ transmit_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | ? [v6] : ? [v7] : (send_message(v6, v1, v2, v3, v4) & root_occ(v7, v5) & occurrence_of(v7, v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | min_precedes(v3, v5, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | ~ atomic(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | activity(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | root(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | activity(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v3) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (transmit_message(v4, v5, v6, v2, v1) & subactivity_occurrence(v7, v3) & occurrence_of(v7, v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ transmit_message(tptp0, v0, v1, v2, v3) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp2, v0, v1, v2, v3) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp3, v0, v1, v2, v3) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp4, v0, v1, v2, v3) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v3, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v0, v2, v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | activity(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | root(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) & ! [v0] : ! [v1] : ~ tptp1(tptp0, v0, v1) & ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) & ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) & ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) & ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) & ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) & ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) & ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) & ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) & ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) & ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) & ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) & ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) & ! [v0] : ( ~ legal(v0) | arboreal(v0)) & ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : (next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 77.99/38.36 | % 77.99/38.36 | Applying alpha-rule on (1) yields: % 77.99/38.36 | (2) ~ (tptp3 = tptp4) % 77.99/38.36 | (3) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 77.99/38.36 | (4) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 77.99/38.36 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 77.99/38.36 | (6) ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : (next_subocc(v1, v2, tptp0) & leaf_occ(v2, v0) & root_occ(v1, v0) & occurrence_of(v1, tptp4) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp3)))) % 77.99/38.36 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 77.99/38.36 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | activity(v0)) % 77.99/38.36 | (9) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 77.99/38.36 | (10) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 77.99/38.36 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v3) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 77.99/38.36 | (12) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 77.99/38.36 | (13) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 77.99/38.36 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) % 77.99/38.36 | (15) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 77.99/38.36 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 77.99/38.36 | (17) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 77.99/38.36 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | min_precedes(v3, v5, v4)) % 77.99/38.36 | (19) ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 77.99/38.36 | (20) ~ (tptp5 = tptp4) % 77.99/38.36 | (21) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 77.99/38.36 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, v3))) % 77.99/38.37 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp3, v0, v1, v2, v3) % 77.99/38.37 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 77.99/38.37 | (25) atomic(tptp3) % 77.99/38.37 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) % 77.99/38.37 | (27) ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) % 77.99/38.37 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v0)) % 77.99/38.37 | (29) ~ (tptp2 = tptp4) % 77.99/38.37 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp2, v0, v1, v2, v3) % 77.99/38.37 | (31) ~ (tptp2 = tptp3) % 77.99/38.37 | (32) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 77.99/38.37 | (33) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 77.99/38.37 | (34) ~ atomic(tptp0) % 77.99/38.37 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (transmit_message(v4, v5, v6, v2, v1) & subactivity_occurrence(v7, v3) & occurrence_of(v7, v4))) % 77.99/38.37 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 77.99/38.37 | (37) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 77.99/38.37 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v1)) % 77.99/38.37 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp4, v0, v1, v2, v3) % 77.99/38.37 | (40) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 77.99/38.37 | (41) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 77.99/38.37 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | root(v1, v2)) % 77.99/38.37 | (43) atomic(tptp2) % 77.99/38.37 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 77.99/38.37 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v3, v1, v2)) % 77.99/38.37 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | root(v3, v4)) % 77.99/38.37 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ tptp1(v0, v1, v2) | ~ transmit_message(v0, v3, v4, v5, v6)) % 77.99/38.37 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ transmit_message(v0, v1, v2, v3, v4) | ~ atomic(v0)) % 77.99/38.37 | (49) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 77.99/38.37 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ transmit_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | ? [v6] : ? [v7] : (send_message(v6, v1, v2, v3, v4) & root_occ(v7, v5) & occurrence_of(v7, v6))) % 77.99/38.37 | (51) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 77.99/38.37 | (52) ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) % 77.99/38.37 | (53) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 77.99/38.37 | (54) ! [v0] : ! [v1] : ~ tptp1(tptp0, v0, v1) % 77.99/38.37 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 77.99/38.37 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | activity(v0)) % 77.99/38.37 | (57) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 77.99/38.37 | (58) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 77.99/38.37 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 77.99/38.37 | (60) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) % 77.99/38.37 | (61) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 77.99/38.37 | (62) tptp1(all_0_2_2, tptp0, all_0_1_1) % 77.99/38.37 | (63) atomic(tptp4) % 77.99/38.37 | (64) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 77.99/38.37 | (65) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 77.99/38.37 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | root(v2, v1)) % 77.99/38.37 | (67) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) % 77.99/38.37 | (68) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 77.99/38.37 | (69) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 77.99/38.37 | (70) ~ (tptp5 = tptp3) % 77.99/38.37 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 77.99/38.37 | (72) ~ (tptp5 = tptp2) % 77.99/38.37 | (73) occurrence_of(all_0_0_0, all_0_2_2) % 77.99/38.37 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v1, v2)) % 77.99/38.37 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | activity(v0)) % 77.99/38.38 | (76) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 77.99/38.38 | (77) activity(tptp0) % 77.99/38.38 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v0, v2, v3)) % 77.99/38.38 | (79) atomic(tptp5) % 77.99/38.38 | (80) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) % 77.99/38.38 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ transmit_message(tptp0, v0, v1, v2, v3) % 77.99/38.38 | (82) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (66) with all_0_1_1, tptp0, all_0_2_2 and discharging atoms tptp1(all_0_2_2, tptp0, all_0_1_1), yields: % 77.99/38.38 | (83) root(all_0_1_1, tptp0) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (35) with all_0_0_0, all_0_1_1, tptp0, all_0_2_2 and discharging atoms tptp1(all_0_2_2, tptp0, all_0_1_1), occurrence_of(all_0_0_0, all_0_2_2), yields: % 77.99/38.38 | (84) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (transmit_message(v0, v1, v2, all_0_1_1, tptp0) & subactivity_occurrence(v3, all_0_0_0) & occurrence_of(v3, v0)) % 77.99/38.38 | % 77.99/38.38 | Instantiating (84) with all_17_0_3, all_17_1_4, all_17_2_5, all_17_3_6 yields: % 77.99/38.38 | (85) transmit_message(all_17_3_6, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) & subactivity_occurrence(all_17_0_3, all_0_0_0) & occurrence_of(all_17_0_3, all_17_3_6) % 77.99/38.38 | % 77.99/38.38 | Applying alpha-rule on (85) yields: % 77.99/38.38 | (86) transmit_message(all_17_3_6, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) % 77.99/38.38 | (87) subactivity_occurrence(all_17_0_3, all_0_0_0) % 77.99/38.38 | (88) occurrence_of(all_17_0_3, all_17_3_6) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (50) with all_17_0_3, tptp0, all_0_1_1, all_17_1_4, all_17_2_5, all_17_3_6 and discharging atoms transmit_message(all_17_3_6, all_17_2_5, all_17_1_4, all_0_1_1, tptp0), occurrence_of(all_17_0_3, all_17_3_6), yields: % 77.99/38.38 | (89) ? [v0] : ? [v1] : (send_message(v0, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) & root_occ(v1, all_17_0_3) & occurrence_of(v1, v0)) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (21) with all_17_0_3, all_17_3_6 and discharging atoms occurrence_of(all_17_0_3, all_17_3_6), yields: % 77.99/38.38 | (90) activity_occurrence(all_17_0_3) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (49) with all_17_0_3, all_17_3_6 and discharging atoms occurrence_of(all_17_0_3, all_17_3_6), yields: % 77.99/38.38 | (91) atomic(all_17_3_6) | ? [v0] : (subactivity_occurrence(v0, all_17_0_3) & root(v0, all_17_3_6)) % 77.99/38.38 | % 77.99/38.38 | Instantiating (89) with all_43_0_8, all_43_1_9 yields: % 77.99/38.38 | (92) send_message(all_43_1_9, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) & root_occ(all_43_0_8, all_17_0_3) & occurrence_of(all_43_0_8, all_43_1_9) % 77.99/38.38 | % 77.99/38.38 | Applying alpha-rule on (92) yields: % 77.99/38.38 | (93) send_message(all_43_1_9, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) % 77.99/38.38 | (94) root_occ(all_43_0_8, all_17_0_3) % 77.99/38.38 | (95) occurrence_of(all_43_0_8, all_43_1_9) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (30) with tptp0, all_0_1_1, all_17_1_4, all_17_2_5 yields: % 77.99/38.38 | (96) ~ send_message(tptp2, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (23) with tptp0, all_0_1_1, all_17_1_4, all_17_2_5 yields: % 77.99/38.38 | (97) ~ send_message(tptp3, all_17_2_5, all_17_1_4, all_0_1_1, tptp0) % 77.99/38.38 | % 77.99/38.38 | Using (93) and (96) yields: % 77.99/38.38 | (98) ~ (all_43_1_9 = tptp2) % 77.99/38.38 | % 77.99/38.38 | Using (93) and (97) yields: % 77.99/38.38 | (99) ~ (all_43_1_9 = tptp3) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (5) with tptp0, all_0_1_1, all_17_1_4, all_17_2_5, all_43_1_9 and discharging atoms send_message(all_43_1_9, all_17_2_5, all_17_1_4, all_0_1_1, tptp0), yields: % 77.99/38.38 | (100) atomic(all_43_1_9) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (32) with all_17_0_3 and discharging atoms activity_occurrence(all_17_0_3), yields: % 77.99/38.38 | (101) ? [v0] : (activity(v0) & occurrence_of(all_17_0_3, v0)) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (53) with all_17_0_3, all_43_0_8 and discharging atoms root_occ(all_43_0_8, all_17_0_3), yields: % 77.99/38.38 | (102) ? [v0] : (subactivity_occurrence(all_43_0_8, all_17_0_3) & root(all_43_0_8, v0) & occurrence_of(all_17_0_3, v0)) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (18) with all_43_0_8, tptp0, all_0_1_1, all_17_1_4, all_17_2_5, all_43_1_9 and discharging atoms send_message(all_43_1_9, all_17_2_5, all_17_1_4, all_0_1_1, tptp0), occurrence_of(all_43_0_8, all_43_1_9), yields: % 77.99/38.38 | (103) min_precedes(all_0_1_1, all_43_0_8, tptp0) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (65) with all_43_0_8, all_43_1_9 and discharging atoms occurrence_of(all_43_0_8, all_43_1_9), yields: % 77.99/38.38 | (104) activity(all_43_1_9) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (21) with all_43_0_8, all_43_1_9 and discharging atoms occurrence_of(all_43_0_8, all_43_1_9), yields: % 77.99/38.38 | (105) activity_occurrence(all_43_0_8) % 77.99/38.38 | % 77.99/38.38 | Instantiating (101) with all_61_0_11 yields: % 77.99/38.38 | (106) activity(all_61_0_11) & occurrence_of(all_17_0_3, all_61_0_11) % 77.99/38.38 | % 77.99/38.38 | Applying alpha-rule on (106) yields: % 77.99/38.38 | (107) activity(all_61_0_11) % 77.99/38.38 | (108) occurrence_of(all_17_0_3, all_61_0_11) % 77.99/38.38 | % 77.99/38.38 | Instantiating (102) with all_67_0_14 yields: % 77.99/38.38 | (109) subactivity_occurrence(all_43_0_8, all_17_0_3) & root(all_43_0_8, all_67_0_14) & occurrence_of(all_17_0_3, all_67_0_14) % 77.99/38.38 | % 77.99/38.38 | Applying alpha-rule on (109) yields: % 77.99/38.38 | (110) subactivity_occurrence(all_43_0_8, all_17_0_3) % 77.99/38.38 | (111) root(all_43_0_8, all_67_0_14) % 77.99/38.38 | (112) occurrence_of(all_17_0_3, all_67_0_14) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (48) with tptp0, all_0_1_1, all_17_1_4, all_17_2_5, all_17_3_6 and discharging atoms transmit_message(all_17_3_6, all_17_2_5, all_17_1_4, all_0_1_1, tptp0), yields: % 77.99/38.38 | (113) ~ atomic(all_17_3_6) % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (64) with all_67_0_14, all_17_3_6, all_17_0_3 and discharging atoms occurrence_of(all_17_0_3, all_67_0_14), occurrence_of(all_17_0_3, all_17_3_6), yields: % 77.99/38.38 | (114) all_67_0_14 = all_17_3_6 % 77.99/38.38 | % 77.99/38.38 | Instantiating formula (64) with all_61_0_11, all_67_0_14, all_17_0_3 and discharging atoms occurrence_of(all_17_0_3, all_67_0_14), occurrence_of(all_17_0_3, all_61_0_11), yields: % 77.99/38.38 | (115) all_67_0_14 = all_61_0_11 % 77.99/38.38 | % 77.99/38.38 | Combining equations (114,115) yields a new equation: % 77.99/38.38 | (116) all_61_0_11 = all_17_3_6 % 77.99/38.38 | % 77.99/38.38 | Combining equations (116,115) yields a new equation: % 77.99/38.38 | (114) all_67_0_14 = all_17_3_6 % 77.99/38.38 | % 77.99/38.38 | From (114) and (111) follows: % 78.40/38.39 | (118) root(all_43_0_8, all_17_3_6) % 78.40/38.39 | % 78.40/38.39 | From (116) and (108) follows: % 78.40/38.39 | (88) occurrence_of(all_17_0_3, all_17_3_6) % 78.40/38.39 | % 78.40/38.39 +-Applying beta-rule and splitting (91), into two cases. % 78.40/38.39 |-Branch one: % 78.40/38.39 | (120) atomic(all_17_3_6) % 78.40/38.39 | % 78.40/38.39 | Using (120) and (113) yields: % 78.40/38.39 | (121) $false % 78.40/38.39 | % 78.40/38.39 |-The branch is then unsatisfiable % 78.40/38.39 |-Branch two: % 78.40/38.39 | (113) ~ atomic(all_17_3_6) % 78.40/38.39 | (123) ? [v0] : (subactivity_occurrence(v0, all_17_0_3) & root(v0, all_17_3_6)) % 78.40/38.39 | % 78.40/38.39 | Instantiating (123) with all_82_0_16 yields: % 78.40/38.39 | (124) subactivity_occurrence(all_82_0_16, all_17_0_3) & root(all_82_0_16, all_17_3_6) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (124) yields: % 78.40/38.39 | (125) subactivity_occurrence(all_82_0_16, all_17_0_3) % 78.40/38.39 | (126) root(all_82_0_16, all_17_3_6) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (52) with all_43_1_9 and discharging atoms activity(all_43_1_9), yields: % 78.40/38.39 | (127) subactivity(all_43_1_9, all_43_1_9) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (32) with all_43_0_8 and discharging atoms activity_occurrence(all_43_0_8), yields: % 78.40/38.39 | (128) ? [v0] : (activity(v0) & occurrence_of(all_43_0_8, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (82) with all_17_3_6, all_17_0_3, all_82_0_16 and discharging atoms subactivity_occurrence(all_82_0_16, all_17_0_3), root(all_82_0_16, all_17_3_6), occurrence_of(all_17_0_3, all_17_3_6), yields: % 78.40/38.39 | (129) root_occ(all_82_0_16, all_17_0_3) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (67) with all_82_0_16, all_17_3_6 and discharging atoms root(all_82_0_16, all_17_3_6), yields: % 78.40/38.39 | (130) ? [v0] : (subactivity(v0, all_17_3_6) & atocc(all_82_0_16, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (67) with all_43_0_8, all_17_3_6 and discharging atoms root(all_43_0_8, all_17_3_6), yields: % 78.40/38.39 | (131) ? [v0] : (subactivity(v0, all_17_3_6) & atocc(all_43_0_8, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (17) with all_43_1_9, all_43_0_8 and discharging atoms atomic(all_43_1_9), occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.39 | (132) arboreal(all_43_0_8) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (7) with all_0_1_1, tptp0, all_43_0_8 and discharging atoms min_precedes(all_0_1_1, all_43_0_8, tptp0), yields: % 78.40/38.39 | (133) leaf(all_43_0_8, tptp0) | ? [v0] : min_precedes(all_43_0_8, v0, tptp0) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (22) with all_43_0_8, all_0_1_1, tptp0 and discharging atoms min_precedes(all_0_1_1, all_43_0_8, tptp0), yields: % 78.40/38.39 | (134) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_43_0_8, v1) & atocc(all_0_1_1, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (13) with all_43_0_8, all_0_1_1, tptp0 and discharging atoms min_precedes(all_0_1_1, all_43_0_8, tptp0), yields: % 78.40/38.39 | (135) ? [v0] : (subactivity_occurrence(all_43_0_8, v0) & subactivity_occurrence(all_0_1_1, v0) & occurrence_of(v0, tptp0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating (130) with all_118_0_19 yields: % 78.40/38.39 | (136) subactivity(all_118_0_19, all_17_3_6) & atocc(all_82_0_16, all_118_0_19) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (136) yields: % 78.40/38.39 | (137) subactivity(all_118_0_19, all_17_3_6) % 78.40/38.39 | (138) atocc(all_82_0_16, all_118_0_19) % 78.40/38.39 | % 78.40/38.39 | Instantiating (135) with all_120_0_20 yields: % 78.40/38.39 | (139) subactivity_occurrence(all_43_0_8, all_120_0_20) & subactivity_occurrence(all_0_1_1, all_120_0_20) & occurrence_of(all_120_0_20, tptp0) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (139) yields: % 78.40/38.39 | (140) subactivity_occurrence(all_43_0_8, all_120_0_20) % 78.40/38.39 | (141) subactivity_occurrence(all_0_1_1, all_120_0_20) % 78.40/38.39 | (142) occurrence_of(all_120_0_20, tptp0) % 78.40/38.39 | % 78.40/38.39 | Instantiating (134) with all_122_0_21, all_122_1_22 yields: % 78.40/38.39 | (143) subactivity(all_122_0_21, tptp0) & subactivity(all_122_1_22, tptp0) & atocc(all_43_0_8, all_122_0_21) & atocc(all_0_1_1, all_122_1_22) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (143) yields: % 78.40/38.39 | (144) subactivity(all_122_0_21, tptp0) % 78.40/38.39 | (145) subactivity(all_122_1_22, tptp0) % 78.40/38.39 | (146) atocc(all_43_0_8, all_122_0_21) % 78.40/38.39 | (147) atocc(all_0_1_1, all_122_1_22) % 78.40/38.39 | % 78.40/38.39 | Instantiating (131) with all_124_0_23 yields: % 78.40/38.39 | (148) subactivity(all_124_0_23, all_17_3_6) & atocc(all_43_0_8, all_124_0_23) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (148) yields: % 78.40/38.39 | (149) subactivity(all_124_0_23, all_17_3_6) % 78.40/38.39 | (150) atocc(all_43_0_8, all_124_0_23) % 78.40/38.39 | % 78.40/38.39 | Instantiating (128) with all_126_0_24 yields: % 78.40/38.39 | (151) activity(all_126_0_24) & occurrence_of(all_43_0_8, all_126_0_24) % 78.40/38.39 | % 78.40/38.39 | Applying alpha-rule on (151) yields: % 78.40/38.39 | (152) activity(all_126_0_24) % 78.40/38.39 | (153) occurrence_of(all_43_0_8, all_126_0_24) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (36) with all_17_3_6, all_17_0_3, all_82_0_16, all_43_0_8 and discharging atoms root_occ(all_82_0_16, all_17_0_3), root_occ(all_43_0_8, all_17_0_3), occurrence_of(all_17_0_3, all_17_3_6), yields: % 78.40/38.39 | (154) all_82_0_16 = all_43_0_8 % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (64) with all_126_0_24, all_43_1_9, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_126_0_24), occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.39 | (155) all_126_0_24 = all_43_1_9 % 78.40/38.39 | % 78.40/38.39 | From (154) and (138) follows: % 78.40/38.39 | (156) atocc(all_43_0_8, all_118_0_19) % 78.40/38.39 | % 78.40/38.39 | From (155) and (153) follows: % 78.40/38.39 | (95) occurrence_of(all_43_0_8, all_43_1_9) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (55) with all_43_1_9, all_43_1_9, all_43_0_8 and discharging atoms subactivity(all_43_1_9, all_43_1_9), atomic(all_43_1_9), occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.39 | (158) atocc(all_43_0_8, all_43_1_9) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (80) with all_124_0_23, all_43_0_8 and discharging atoms atocc(all_43_0_8, all_124_0_23), yields: % 78.40/38.39 | (159) ? [v0] : (subactivity(all_124_0_23, v0) & atomic(v0) & occurrence_of(all_43_0_8, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (80) with all_122_0_21, all_43_0_8 and discharging atoms atocc(all_43_0_8, all_122_0_21), yields: % 78.40/38.39 | (160) ? [v0] : (subactivity(all_122_0_21, v0) & atomic(v0) & occurrence_of(all_43_0_8, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (80) with all_118_0_19, all_43_0_8 and discharging atoms atocc(all_43_0_8, all_118_0_19), yields: % 78.40/38.39 | (161) ? [v0] : (subactivity(all_118_0_19, v0) & atomic(v0) & occurrence_of(all_43_0_8, v0)) % 78.40/38.39 | % 78.40/38.39 | Instantiating formula (82) with tptp0, all_120_0_20, all_0_1_1 and discharging atoms subactivity_occurrence(all_0_1_1, all_120_0_20), root(all_0_1_1, tptp0), occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.39 | (162) root_occ(all_0_1_1, all_120_0_20) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (6) with all_120_0_20 and discharging atoms occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.40 | (163) ? [v0] : ? [v1] : (next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_120_0_20) & root_occ(v0, all_120_0_20) & occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (21) with all_120_0_20, tptp0 and discharging atoms occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.40 | (164) activity_occurrence(all_120_0_20) % 78.40/38.40 | % 78.40/38.40 | Instantiating (161) with all_174_0_29 yields: % 78.40/38.40 | (165) subactivity(all_118_0_19, all_174_0_29) & atomic(all_174_0_29) & occurrence_of(all_43_0_8, all_174_0_29) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (165) yields: % 78.40/38.40 | (166) subactivity(all_118_0_19, all_174_0_29) % 78.40/38.40 | (167) atomic(all_174_0_29) % 78.40/38.40 | (168) occurrence_of(all_43_0_8, all_174_0_29) % 78.40/38.40 | % 78.40/38.40 | Instantiating (160) with all_182_0_33 yields: % 78.40/38.40 | (169) subactivity(all_122_0_21, all_182_0_33) & atomic(all_182_0_33) & occurrence_of(all_43_0_8, all_182_0_33) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (169) yields: % 78.40/38.40 | (170) subactivity(all_122_0_21, all_182_0_33) % 78.40/38.40 | (171) atomic(all_182_0_33) % 78.40/38.40 | (172) occurrence_of(all_43_0_8, all_182_0_33) % 78.40/38.40 | % 78.40/38.40 | Instantiating (159) with all_184_0_34 yields: % 78.40/38.40 | (173) subactivity(all_124_0_23, all_184_0_34) & atomic(all_184_0_34) & occurrence_of(all_43_0_8, all_184_0_34) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (173) yields: % 78.40/38.40 | (174) subactivity(all_124_0_23, all_184_0_34) % 78.40/38.40 | (175) atomic(all_184_0_34) % 78.40/38.40 | (176) occurrence_of(all_43_0_8, all_184_0_34) % 78.40/38.40 | % 78.40/38.40 | Instantiating (163) with all_190_0_37, all_190_1_38 yields: % 78.40/38.40 | (177) next_subocc(all_190_1_38, all_190_0_37, tptp0) & leaf_occ(all_190_0_37, all_120_0_20) & root_occ(all_190_1_38, all_120_0_20) & occurrence_of(all_190_1_38, tptp4) & (occurrence_of(all_190_0_37, tptp2) | occurrence_of(all_190_0_37, tptp3)) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (177) yields: % 78.40/38.40 | (178) occurrence_of(all_190_0_37, tptp2) | occurrence_of(all_190_0_37, tptp3) % 78.40/38.40 | (179) occurrence_of(all_190_1_38, tptp4) % 78.40/38.40 | (180) leaf_occ(all_190_0_37, all_120_0_20) % 78.40/38.40 | (181) root_occ(all_190_1_38, all_120_0_20) % 78.40/38.40 | (182) next_subocc(all_190_1_38, all_190_0_37, tptp0) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (36) with tptp0, all_120_0_20, all_0_1_1, all_190_1_38 and discharging atoms root_occ(all_190_1_38, all_120_0_20), root_occ(all_0_1_1, all_120_0_20), occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.40 | (183) all_190_1_38 = all_0_1_1 % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (64) with all_182_0_33, all_43_1_9, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_182_0_33), occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.40 | (184) all_182_0_33 = all_43_1_9 % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (64) with all_182_0_33, all_184_0_34, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_184_0_34), occurrence_of(all_43_0_8, all_182_0_33), yields: % 78.40/38.40 | (185) all_184_0_34 = all_182_0_33 % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (64) with all_174_0_29, all_184_0_34, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_184_0_34), occurrence_of(all_43_0_8, all_174_0_29), yields: % 78.40/38.40 | (186) all_184_0_34 = all_174_0_29 % 78.40/38.40 | % 78.40/38.40 | Combining equations (185,186) yields a new equation: % 78.40/38.40 | (187) all_182_0_33 = all_174_0_29 % 78.40/38.40 | % 78.40/38.40 | Simplifying 187 yields: % 78.40/38.40 | (188) all_182_0_33 = all_174_0_29 % 78.40/38.40 | % 78.40/38.40 | Combining equations (188,184) yields a new equation: % 78.40/38.40 | (189) all_174_0_29 = all_43_1_9 % 78.40/38.40 | % 78.40/38.40 | Simplifying 189 yields: % 78.40/38.40 | (190) all_174_0_29 = all_43_1_9 % 78.40/38.40 | % 78.40/38.40 | From (183) and (182) follows: % 78.40/38.40 | (191) next_subocc(all_0_1_1, all_190_0_37, tptp0) % 78.40/38.40 | % 78.40/38.40 | From (183) and (181) follows: % 78.40/38.40 | (162) root_occ(all_0_1_1, all_120_0_20) % 78.40/38.40 | % 78.40/38.40 | From (190) and (168) follows: % 78.40/38.40 | (95) occurrence_of(all_43_0_8, all_43_1_9) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (32) with all_120_0_20 and discharging atoms activity_occurrence(all_120_0_20), yields: % 78.40/38.40 | (194) ? [v0] : (activity(v0) & occurrence_of(all_120_0_20, v0)) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (80) with all_43_1_9, all_43_0_8 and discharging atoms atocc(all_43_0_8, all_43_1_9), yields: % 78.40/38.40 | (195) ? [v0] : (subactivity(all_43_1_9, v0) & atomic(v0) & occurrence_of(all_43_0_8, v0)) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (16) with tptp0, all_190_0_37, all_0_1_1 and discharging atoms next_subocc(all_0_1_1, all_190_0_37, tptp0), yields: % 78.40/38.40 | (196) arboreal(all_190_0_37) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (51) with all_120_0_20, all_190_0_37 and discharging atoms leaf_occ(all_190_0_37, all_120_0_20), yields: % 78.40/38.40 | (197) ? [v0] : (leaf(all_190_0_37, v0) & subactivity_occurrence(all_190_0_37, all_120_0_20) & occurrence_of(all_120_0_20, v0)) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (53) with all_120_0_20, all_0_1_1 and discharging atoms root_occ(all_0_1_1, all_120_0_20), yields: % 78.40/38.40 | (198) ? [v0] : (subactivity_occurrence(all_0_1_1, all_120_0_20) & root(all_0_1_1, v0) & occurrence_of(all_120_0_20, v0)) % 78.40/38.40 | % 78.40/38.40 | Instantiating (195) with all_286_0_41 yields: % 78.40/38.40 | (199) subactivity(all_43_1_9, all_286_0_41) & atomic(all_286_0_41) & occurrence_of(all_43_0_8, all_286_0_41) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (199) yields: % 78.40/38.40 | (200) subactivity(all_43_1_9, all_286_0_41) % 78.40/38.40 | (201) atomic(all_286_0_41) % 78.40/38.40 | (202) occurrence_of(all_43_0_8, all_286_0_41) % 78.40/38.40 | % 78.40/38.40 | Instantiating (198) with all_292_0_45 yields: % 78.40/38.40 | (203) subactivity_occurrence(all_0_1_1, all_120_0_20) & root(all_0_1_1, all_292_0_45) & occurrence_of(all_120_0_20, all_292_0_45) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (203) yields: % 78.40/38.40 | (141) subactivity_occurrence(all_0_1_1, all_120_0_20) % 78.40/38.40 | (205) root(all_0_1_1, all_292_0_45) % 78.40/38.40 | (206) occurrence_of(all_120_0_20, all_292_0_45) % 78.40/38.40 | % 78.40/38.40 | Instantiating (197) with all_294_0_46 yields: % 78.40/38.40 | (207) leaf(all_190_0_37, all_294_0_46) & subactivity_occurrence(all_190_0_37, all_120_0_20) & occurrence_of(all_120_0_20, all_294_0_46) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (207) yields: % 78.40/38.40 | (208) leaf(all_190_0_37, all_294_0_46) % 78.40/38.40 | (209) subactivity_occurrence(all_190_0_37, all_120_0_20) % 78.40/38.40 | (210) occurrence_of(all_120_0_20, all_294_0_46) % 78.40/38.40 | % 78.40/38.40 | Instantiating (194) with all_304_0_51 yields: % 78.40/38.40 | (211) activity(all_304_0_51) & occurrence_of(all_120_0_20, all_304_0_51) % 78.40/38.40 | % 78.40/38.40 | Applying alpha-rule on (211) yields: % 78.40/38.40 | (212) activity(all_304_0_51) % 78.40/38.40 | (213) occurrence_of(all_120_0_20, all_304_0_51) % 78.40/38.40 | % 78.40/38.40 | Instantiating formula (64) with all_294_0_46, tptp0, all_120_0_20 and discharging atoms occurrence_of(all_120_0_20, all_294_0_46), occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.40 | (214) all_294_0_46 = tptp0 % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (64) with all_294_0_46, all_304_0_51, all_120_0_20 and discharging atoms occurrence_of(all_120_0_20, all_304_0_51), occurrence_of(all_120_0_20, all_294_0_46), yields: % 78.40/38.41 | (215) all_304_0_51 = all_294_0_46 % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (64) with all_292_0_45, all_304_0_51, all_120_0_20 and discharging atoms occurrence_of(all_120_0_20, all_304_0_51), occurrence_of(all_120_0_20, all_292_0_45), yields: % 78.40/38.41 | (216) all_304_0_51 = all_292_0_45 % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (64) with all_286_0_41, all_43_1_9, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_286_0_41), occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.41 | (217) all_286_0_41 = all_43_1_9 % 78.40/38.41 | % 78.40/38.41 | Combining equations (215,216) yields a new equation: % 78.40/38.41 | (218) all_294_0_46 = all_292_0_45 % 78.40/38.41 | % 78.40/38.41 | Simplifying 218 yields: % 78.40/38.41 | (219) all_294_0_46 = all_292_0_45 % 78.40/38.41 | % 78.40/38.41 | Combining equations (214,219) yields a new equation: % 78.40/38.41 | (220) all_292_0_45 = tptp0 % 78.40/38.41 | % 78.40/38.41 | Combining equations (220,219) yields a new equation: % 78.40/38.41 | (214) all_294_0_46 = tptp0 % 78.40/38.41 | % 78.40/38.41 | From (214) and (208) follows: % 78.40/38.41 | (222) leaf(all_190_0_37, tptp0) % 78.40/38.41 | % 78.40/38.41 | From (220) and (206) follows: % 78.40/38.41 | (142) occurrence_of(all_120_0_20, tptp0) % 78.40/38.41 | % 78.40/38.41 | From (217) and (202) follows: % 78.40/38.41 | (95) occurrence_of(all_43_0_8, all_43_1_9) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (133), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (225) leaf(all_43_0_8, tptp0) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (178), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (226) occurrence_of(all_190_0_37, tptp2) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (64) with tptp2, all_43_1_9, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.41 | (227) all_43_1_9 = tptp2 | ~ occurrence_of(all_43_0_8, tptp2) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (11) with all_43_0_8, all_190_0_37, all_120_0_20, tptp0 and discharging atoms subactivity_occurrence(all_190_0_37, all_120_0_20), subactivity_occurrence(all_43_0_8, all_120_0_20), arboreal(all_190_0_37), arboreal(all_43_0_8), occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.41 | (228) all_190_0_37 = all_43_0_8 | min_precedes(all_190_0_37, all_43_0_8, tptp0) | min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (227), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (229) ~ occurrence_of(all_43_0_8, tptp2) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (40) with all_43_0_8, tptp0, all_190_0_37 and discharging atoms leaf(all_190_0_37, tptp0), yields: % 78.40/38.41 | (230) ~ min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.41 | % 78.40/38.41 | Using (226) and (229) yields: % 78.40/38.41 | (231) ~ (all_190_0_37 = all_43_0_8) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (228), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (232) min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.41 | % 78.40/38.41 | Using (232) and (230) yields: % 78.40/38.41 | (121) $false % 78.40/38.41 | % 78.40/38.41 |-The branch is then unsatisfiable % 78.40/38.41 |-Branch two: % 78.40/38.41 | (230) ~ min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.41 | (235) all_190_0_37 = all_43_0_8 | min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (235), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (236) min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (40) with all_190_0_37, tptp0, all_43_0_8 and discharging atoms leaf(all_43_0_8, tptp0), min_precedes(all_43_0_8, all_190_0_37, tptp0), yields: % 78.40/38.41 | (121) $false % 78.40/38.41 | % 78.40/38.41 |-The branch is then unsatisfiable % 78.40/38.41 |-Branch two: % 78.40/38.41 | (238) ~ min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.41 | (239) all_190_0_37 = all_43_0_8 % 78.40/38.41 | % 78.40/38.41 | Equations (239) can reduce 231 to: % 78.40/38.41 | (240) $false % 78.40/38.41 | % 78.40/38.41 |-The branch is then unsatisfiable % 78.40/38.41 |-Branch two: % 78.40/38.41 | (241) occurrence_of(all_43_0_8, tptp2) % 78.40/38.41 | (242) all_43_1_9 = tptp2 % 78.40/38.41 | % 78.40/38.41 | Equations (242) can reduce 98 to: % 78.40/38.41 | (240) $false % 78.40/38.41 | % 78.40/38.41 |-The branch is then unsatisfiable % 78.40/38.41 |-Branch two: % 78.40/38.41 | (244) ~ occurrence_of(all_190_0_37, tptp2) % 78.40/38.41 | (245) occurrence_of(all_190_0_37, tptp3) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (64) with tptp3, all_43_1_9, all_43_0_8 and discharging atoms occurrence_of(all_43_0_8, all_43_1_9), yields: % 78.40/38.41 | (246) all_43_1_9 = tptp3 | ~ occurrence_of(all_43_0_8, tptp3) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (11) with all_43_0_8, all_190_0_37, all_120_0_20, tptp0 and discharging atoms subactivity_occurrence(all_190_0_37, all_120_0_20), subactivity_occurrence(all_43_0_8, all_120_0_20), arboreal(all_190_0_37), arboreal(all_43_0_8), occurrence_of(all_120_0_20, tptp0), yields: % 78.40/38.41 | (228) all_190_0_37 = all_43_0_8 | min_precedes(all_190_0_37, all_43_0_8, tptp0) | min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (246), into two cases. % 78.40/38.41 |-Branch one: % 78.40/38.41 | (248) ~ occurrence_of(all_43_0_8, tptp3) % 78.40/38.41 | % 78.40/38.41 | Instantiating formula (40) with all_43_0_8, tptp0, all_190_0_37 and discharging atoms leaf(all_190_0_37, tptp0), yields: % 78.40/38.41 | (230) ~ min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.41 | % 78.40/38.41 | Using (245) and (248) yields: % 78.40/38.41 | (231) ~ (all_190_0_37 = all_43_0_8) % 78.40/38.41 | % 78.40/38.41 +-Applying beta-rule and splitting (228), into two cases. % 78.40/38.42 |-Branch one: % 78.40/38.42 | (232) min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.42 | % 78.40/38.42 | Using (232) and (230) yields: % 78.40/38.42 | (121) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 |-Branch two: % 78.40/38.42 | (230) ~ min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.42 | (235) all_190_0_37 = all_43_0_8 | min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.42 | % 78.40/38.42 +-Applying beta-rule and splitting (235), into two cases. % 78.40/38.42 |-Branch one: % 78.40/38.42 | (236) min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.42 | % 78.40/38.42 | Instantiating formula (40) with all_190_0_37, tptp0, all_43_0_8 and discharging atoms leaf(all_43_0_8, tptp0), min_precedes(all_43_0_8, all_190_0_37, tptp0), yields: % 78.40/38.42 | (121) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 |-Branch two: % 78.40/38.42 | (238) ~ min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.42 | (239) all_190_0_37 = all_43_0_8 % 78.40/38.42 | % 78.40/38.42 | Equations (239) can reduce 231 to: % 78.40/38.42 | (240) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 |-Branch two: % 78.40/38.42 | (260) occurrence_of(all_43_0_8, tptp3) % 78.40/38.42 | (261) all_43_1_9 = tptp3 % 78.40/38.42 | % 78.40/38.42 | Equations (261) can reduce 99 to: % 78.40/38.42 | (240) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 |-Branch two: % 78.40/38.42 | (263) ~ leaf(all_43_0_8, tptp0) % 78.40/38.42 | (264) ? [v0] : min_precedes(all_43_0_8, v0, tptp0) % 78.40/38.42 | % 78.40/38.42 | Instantiating (264) with all_334_0_111 yields: % 78.40/38.42 | (265) min_precedes(all_43_0_8, all_334_0_111, tptp0) % 78.40/38.42 | % 78.40/38.42 | Instantiating formula (71) with all_43_0_8, tptp0, all_190_0_37, all_0_1_1 and discharging atoms next_subocc(all_0_1_1, all_190_0_37, tptp0), min_precedes(all_0_1_1, all_43_0_8, tptp0), yields: % 78.40/38.42 | (238) ~ min_precedes(all_43_0_8, all_190_0_37, tptp0) % 78.40/38.42 | % 78.40/38.42 | Instantiating formula (40) with all_334_0_111, tptp0, all_43_0_8 and discharging atoms min_precedes(all_43_0_8, all_334_0_111, tptp0), yields: % 78.40/38.42 | (263) ~ leaf(all_43_0_8, tptp0) % 78.40/38.42 | % 78.40/38.42 | Using (222) and (263) yields: % 78.40/38.42 | (231) ~ (all_190_0_37 = all_43_0_8) % 78.40/38.42 | % 78.40/38.42 | Instantiating formula (11) with all_43_0_8, all_190_0_37, all_120_0_20, tptp0 and discharging atoms subactivity_occurrence(all_190_0_37, all_120_0_20), subactivity_occurrence(all_43_0_8, all_120_0_20), arboreal(all_190_0_37), arboreal(all_43_0_8), occurrence_of(all_120_0_20, tptp0), ~ min_precedes(all_43_0_8, all_190_0_37, tptp0), yields: % 78.40/38.42 | (269) all_190_0_37 = all_43_0_8 | min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.42 | % 78.40/38.42 +-Applying beta-rule and splitting (269), into two cases. % 78.40/38.42 |-Branch one: % 78.40/38.42 | (232) min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.42 | % 78.40/38.42 | Instantiating formula (40) with all_43_0_8, tptp0, all_190_0_37 and discharging atoms leaf(all_190_0_37, tptp0), min_precedes(all_190_0_37, all_43_0_8, tptp0), yields: % 78.40/38.42 | (121) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 |-Branch two: % 78.40/38.42 | (230) ~ min_precedes(all_190_0_37, all_43_0_8, tptp0) % 78.40/38.42 | (239) all_190_0_37 = all_43_0_8 % 78.40/38.42 | % 78.40/38.42 | Equations (239) can reduce 231 to: % 78.40/38.42 | (240) $false % 78.40/38.42 | % 78.40/38.42 |-The branch is then unsatisfiable % 78.40/38.42 % SZS output end Proof for theBenchmark % 78.40/38.42 % 78.40/38.42 37808ms %------------------------------------------------------------------------------