%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO002+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n013.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:52 EDT 2022 % Result : Theorem 9.61s 2.95s % Output : Proof 12.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO002+4 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n013.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 02:56:43 EDT 2022 % 0.12/0.34 % CPUTime : % 0.55/0.59 ____ _ % 0.55/0.59 ___ / __ \_____(_)___ ________ __________ % 0.55/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.59 % 0.55/0.59 A Theorem Prover for First-Order Logic % 0.55/0.59 (ePrincess v.1.0) % 0.55/0.59 % 0.55/0.59 (c) Philipp Rümmer, 2009-2015 % 0.55/0.59 (c) Peter Backeman, 2014-2015 % 0.55/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.59 Bug reports to peter@backeman.se % 0.55/0.59 % 0.55/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.59 % 0.55/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.81/1.01 Prover 0: Preprocessing ... % 2.59/1.27 Prover 0: Constructing countermodel ... % 9.61/2.95 Prover 0: proved (2308ms) % 9.61/2.95 % 9.61/2.95 No countermodel exists, formula is valid % 9.61/2.95 % SZS status Theorem for theBenchmark % 9.61/2.95 % 9.61/2.95 Generating proof ... found it (size 169) % 12.34/3.59 % 12.34/3.59 % SZS output start Proof for theBenchmark % 12.34/3.59 Assumed formulas after preprocessing and simplification: % 12.34/3.59 | (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] : ( ~ send_message(v3, v4, v5, v6, v7) | ~ occurrence_of(v8, v3) | min_precedes(v6, v8, v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = v5 | ~ min_precedes(v6, v5, v3) | ~ leaf_occ(v7, v4) | ~ root_occ(v6, v4) | ~ subactivity_occurrence(v5, v4) | ~ occurrence_of(v4, v3) | min_precedes(v5, v7, v3)) & ! [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 | ~ arboreal(v6) | ~ arboreal(v5) | ~ subactivity_occurrence(v6, v4) | ~ subactivity_occurrence(v5, v4) | ~ occurrence_of(v4, v3) | min_precedes(v6, v5, v3) | min_precedes(v5, v6, v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v5 | ~ arboreal(v5) | ~ leaf_occ(v6, v4) | ~ subactivity_occurrence(v5, v4) | ~ occurrence_of(v4, 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] : (send_message(v7, v8, v9, v5, v4) & root_occ(v10, v6) & occurrence_of(v10, v7))) & ! [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] : ( ~ precedes(v4, v5) | ~ min_precedes(v3, v5, v6) | ~ min_precedes(v3, v4, v6) | min_precedes(v4, v5, v6)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ min_precedes(v6, v4, v5) | ~ root_occ(v4, v3) | ~ occurrence_of(v3, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ min_precedes(v4, v6, v5) | ~ leaf_occ(v4, v3) | ~ occurrence_of(v3, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ min_precedes(v3, v4, v5) | ~ subactivity_occurrence(v4, v6) | ~ occurrence_of(v6, v5) | subactivity_occurrence(v3, 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] : ( ~ 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] : ( ~ 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(v4, v5) | ~ atomic(v5) | ~ occurrence_of(v3, v5) | atocc(v3, v4)) & ! [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] : (subactivity_occurrence(v5, v6) & subactivity_occurrence(v4, v6) & occurrence_of(v6, v3))) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | ~ root(v4, v5)) & ! [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] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | precedes(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | ? [v6] : (min_precedes(v6, v4, v5) & root(v6, v5))) & ! [v3] : ! [v4] : ! [v5] : ( ~ subactivity_occurrence(v3, v4) | ~ root(v3, v5) | ~ occurrence_of(v4, v5) | root_occ(v3, v4)) & ! [v3] : ! [v4] : ~ tptp1(tptp0, v3, v4) & ! [v3] : ! [v4] : ( ~ precedes(v3, v4) | earlier(v3, v4)) & ! [v3] : ! [v4] : ( ~ precedes(v3, v4) | legal(v4)) & ! [v3] : ! [v4] : ( ~ earlier(v4, v3) | ~ earlier(v3, v4)) & ! [v3] : ! [v4] : ( ~ earlier(v3, v4) | ~ legal(v4) | precedes(v3, v4)) & ! [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] : ( ~ atocc(v3, v4) | ? [v5] : (subactivity(v4, v5) & atomic(v5) & occurrence_of(v3, v5))) & ! [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] : ( ~ root_occ(v3, v4) | ? [v5] : (subactivity_occurrence(v3, v4) & root(v3, v5) & occurrence_of(v4, v5))) & ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v3, v4) | activity_occurrence(v4)) & ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v3, v4) | activity_occurrence(v3)) & ! [v3] : ! [v4] : ( ~ root(v4, v3) | ? [v5] : (atocc(v4, v5) & subactivity(v5, v3))) & ! [v3] : ! [v4] : ( ~ root(v3, v4) | legal(v3)) & ! [v3] : ! [v4] : ( ~ root(v3, v4) | leaf(v3, v4) | ? [v5] : min_precedes(v3, v5, v4)) & ! [v3] : ! [v4] : ( ~ atomic(v4) | ~ occurrence_of(v3, v4) | arboreal(v3)) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | activity_occurrence(v4)) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | activity(v3)) & ! [v3] : ! [v4] : ( ~ occurrence_of(v4, v3) | atomic(v3) | ? [v5] : (subactivity_occurrence(v5, v4) & root(v5, v3))) & ! [v3] : ( ~ legal(v3) | arboreal(v3)) & ! [v3] : ( ~ activity_occurrence(v3) | ? [v4] : (activity(v4) & occurrence_of(v3, v4))) & ! [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))))) % 12.34/3.62 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2 yields: % 12.34/3.62 | (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] : ( ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | min_precedes(v3, v5, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ min_precedes(v3, v2, v0) | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v2, v4, v0)) & ! [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 | ~ arboreal(v3) | ~ arboreal(v2) | ~ subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, 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] : (send_message(v4, v5, v6, v2, v1) & root_occ(v7, v3) & occurrence_of(v7, v4))) & ! [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] : ( ~ precedes(v1, v2) | ~ min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v1, v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v3, v1, v2) | ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v3, v2) | ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v0, v1, v2) | ~ subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | subactivity_occurrence(v0, 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] : ( ~ 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] : ( ~ 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(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) & ! [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] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ~ root(v1, v2)) & ! [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] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & root(v3, v2))) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) & ! [v0] : ! [v1] : ~ tptp1(tptp0, v0, v1) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) & ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ earlier(v0, v1) | ~ legal(v1) | precedes(v0, v1)) & ! [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] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) & ! [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] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) & ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (atocc(v1, v2) & subactivity(v2, v0))) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) & ! [v0] : ( ~ legal(v0) | arboreal(v0)) & ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) & ! [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)))) % 12.34/3.63 | % 12.34/3.63 | Applying alpha-rule on (1) yields: % 12.34/3.63 | (2) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 12.34/3.63 | (3) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 12.34/3.63 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 12.34/3.63 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ send_message(v0, v1, v2, v3, v4) | ~ occurrence_of(v5, v0) | min_precedes(v3, v5, v4)) % 12.34/3.63 | (6) ! [v0] : ! [v1] : ( ~ earlier(v0, v1) | ~ legal(v1) | precedes(v0, v1)) % 12.34/3.63 | (7) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 12.34/3.63 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v3, v1, v2) | ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2)) % 12.34/3.63 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v0)) % 12.34/3.63 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ tptp1(v0, v1, v2) | ~ occurrence_of(v3, v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (send_message(v4, v5, v6, v2, v1) & root_occ(v7, v3) & occurrence_of(v7, v4))) % 12.34/3.63 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | ~ atomic(v1)) % 12.34/3.63 | (12) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 12.34/3.63 | (13) ~ (tptp5 = tptp4) % 12.34/3.63 | (14) ~ (tptp5 = tptp2) % 12.34/3.63 | (15) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (atocc(v1, v2) & subactivity(v2, v0))) % 12.34/3.63 | (16) ~ (tptp3 = tptp4) % 12.34/3.63 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 12.34/3.63 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 12.34/3.63 | (19) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 12.34/3.63 | (20) ~ (tptp2 = tptp3) % 12.34/3.63 | (21) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 12.34/3.63 | (22) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 12.34/3.63 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp4, v0, v1, v2, v3) % 12.34/3.63 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 12.34/3.63 | (25) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 12.34/3.63 | (26) atomic(tptp3) % 12.34/3.63 | (27) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 12.34/3.63 | (28) ~ (tptp2 = tptp4) % 12.34/3.63 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | activity(v0)) % 12.34/3.63 | (30) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 12.34/3.63 | (31) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 12.34/3.63 | (32) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 12.34/3.63 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ arboreal(v3) | ~ arboreal(v2) | ~ subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) % 12.34/3.63 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ~ root(v1, v2)) % 12.34/3.63 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ arboreal(v2) | ~ leaf_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v2, v3, v0)) % 12.34/3.63 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 12.34/3.63 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 12.34/3.63 | (38) atomic(tptp5) % 12.34/3.63 | (39) ~ atomic(tptp0) % 12.34/3.63 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ min_precedes(v3, v2, v0) | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ occurrence_of(v1, v0) | min_precedes(v2, v4, v0)) % 12.34/3.63 | (41) ! [v0] : ! [v1] : ~ tptp1(tptp0, v0, v1) % 12.34/3.63 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp3, v0, v1, v2, v3) % 12.34/3.63 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 12.34/3.63 | (44) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 12.34/3.63 | (45) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 12.34/3.63 | (46) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & root(v3, v2))) % 12.34/3.64 | (47) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 12.34/3.64 | (48) activity(tptp0) % 12.34/3.64 | (49) ~ (tptp5 = tptp3) % 12.34/3.64 | (50) atomic(tptp4) % 12.34/3.64 | (51) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 12.34/3.64 | (52) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 12.34/3.64 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v0, v1, v2) | ~ subactivity_occurrence(v1, v3) | ~ occurrence_of(v3, v2) | subactivity_occurrence(v0, v3)) % 12.34/3.64 | (54) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 12.34/3.64 | (55) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 12.34/3.64 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 12.34/3.64 | (57) tptp1(all_0_2_2, tptp0, all_0_1_1) % 12.34/3.64 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v3, v2) | ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2)) % 12.34/3.64 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | activity(v0)) % 12.34/3.64 | (60) occurrence_of(all_0_0_0, all_0_2_2) % 12.34/3.64 | (61) ! [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)))) % 12.34/3.64 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 12.34/3.64 | (63) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 12.34/3.64 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 12.34/3.64 | (65) ! [v0] : ! [v1] : ! [v2] : ( ~ tptp1(v0, v1, v2) | root(v2, v1)) % 12.34/3.64 | (66) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) % 12.34/3.64 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | atomic(v0)) % 12.34/3.64 | (68) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 12.34/3.64 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v3, v4)) % 12.34/3.64 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ send_message(v0, v1, v2, v3, v4) | root(v1, v2)) % 12.34/3.64 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ~ send_message(tptp2, v0, v1, v2, v3) % 12.34/3.64 | (72) atomic(tptp2) % 12.34/3.64 | (73) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 12.34/3.64 | (74) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 12.34/3.64 | (75) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 12.34/3.64 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ precedes(v1, v2) | ~ min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v1, v2, v3)) % 12.34/3.64 | % 12.34/3.64 | Instantiating formula (65) with all_0_1_1, tptp0, all_0_2_2 and discharging atoms tptp1(all_0_2_2, tptp0, all_0_1_1), yields: % 12.34/3.64 | (77) root(all_0_1_1, tptp0) % 12.34/3.64 | % 12.34/3.64 | Instantiating formula (10) 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: % 12.34/3.64 | (78) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (send_message(v0, v1, v2, all_0_1_1, tptp0) & root_occ(v3, all_0_0_0) & occurrence_of(v3, v0)) % 12.34/3.64 | % 12.34/3.64 | Instantiating formula (75) with all_0_0_0, all_0_2_2 and discharging atoms occurrence_of(all_0_0_0, all_0_2_2), yields: % 12.34/3.64 | (79) activity_occurrence(all_0_0_0) % 12.34/3.64 | % 12.34/3.64 | Instantiating (78) with all_9_0_3, all_9_1_4, all_9_2_5, all_9_3_6 yields: % 12.34/3.64 | (80) send_message(all_9_3_6, all_9_2_5, all_9_1_4, all_0_1_1, tptp0) & root_occ(all_9_0_3, all_0_0_0) & occurrence_of(all_9_0_3, all_9_3_6) % 12.34/3.64 | % 12.34/3.64 | Applying alpha-rule on (80) yields: % 12.34/3.64 | (81) send_message(all_9_3_6, all_9_2_5, all_9_1_4, all_0_1_1, tptp0) % 12.73/3.64 | (82) root_occ(all_9_0_3, all_0_0_0) % 12.73/3.64 | (83) occurrence_of(all_9_0_3, all_9_3_6) % 12.73/3.64 | % 12.73/3.64 | Instantiating formula (52) with all_0_0_0 and discharging atoms activity_occurrence(all_0_0_0), yields: % 12.73/3.64 | (84) ? [v0] : (activity(v0) & occurrence_of(all_0_0_0, v0)) % 12.73/3.64 | % 12.73/3.64 | Instantiating formula (7) with all_0_0_0, all_9_0_3 and discharging atoms root_occ(all_9_0_3, all_0_0_0), yields: % 12.73/3.64 | (85) ? [v0] : (subactivity_occurrence(all_9_0_3, all_0_0_0) & root(all_9_0_3, v0) & occurrence_of(all_0_0_0, v0)) % 12.73/3.64 | % 12.73/3.64 | Instantiating formula (5) with all_9_0_3, tptp0, all_0_1_1, all_9_1_4, all_9_2_5, all_9_3_6 and discharging atoms send_message(all_9_3_6, all_9_2_5, all_9_1_4, all_0_1_1, tptp0), occurrence_of(all_9_0_3, all_9_3_6), yields: % 12.73/3.64 | (86) min_precedes(all_0_1_1, all_9_0_3, tptp0) % 12.73/3.64 | % 12.73/3.64 | Instantiating formula (75) with all_9_0_3, all_9_3_6 and discharging atoms occurrence_of(all_9_0_3, all_9_3_6), yields: % 12.73/3.64 | (87) activity_occurrence(all_9_0_3) % 12.73/3.64 | % 12.73/3.64 | Instantiating (85) with all_19_0_8 yields: % 12.73/3.64 | (88) subactivity_occurrence(all_9_0_3, all_0_0_0) & root(all_9_0_3, all_19_0_8) & occurrence_of(all_0_0_0, all_19_0_8) % 12.73/3.64 | % 12.73/3.64 | Applying alpha-rule on (88) yields: % 12.73/3.64 | (89) subactivity_occurrence(all_9_0_3, all_0_0_0) % 12.73/3.64 | (90) root(all_9_0_3, all_19_0_8) % 12.73/3.64 | (91) occurrence_of(all_0_0_0, all_19_0_8) % 12.73/3.64 | % 12.73/3.64 | Instantiating (84) with all_21_0_9 yields: % 12.73/3.64 | (92) activity(all_21_0_9) & occurrence_of(all_0_0_0, all_21_0_9) % 12.73/3.64 | % 12.73/3.64 | Applying alpha-rule on (92) yields: % 12.73/3.64 | (93) activity(all_21_0_9) % 12.73/3.64 | (94) occurrence_of(all_0_0_0, all_21_0_9) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (12) with all_21_0_9, all_0_2_2, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_21_0_9), occurrence_of(all_0_0_0, all_0_2_2), yields: % 12.73/3.65 | (95) all_21_0_9 = all_0_2_2 % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (12) with all_19_0_8, all_21_0_9, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_21_0_9), occurrence_of(all_0_0_0, all_19_0_8), yields: % 12.73/3.65 | (96) all_21_0_9 = all_19_0_8 % 12.73/3.65 | % 12.73/3.65 | Combining equations (95,96) yields a new equation: % 12.73/3.65 | (97) all_19_0_8 = all_0_2_2 % 12.73/3.65 | % 12.73/3.65 | From (97) and (90) follows: % 12.73/3.65 | (98) root(all_9_0_3, all_0_2_2) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (52) with all_9_0_3 and discharging atoms activity_occurrence(all_9_0_3), yields: % 12.73/3.65 | (99) ? [v0] : (activity(v0) & occurrence_of(all_9_0_3, v0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (4) with all_9_0_3, all_0_1_1, tptp0 and discharging atoms min_precedes(all_0_1_1, all_9_0_3, tptp0), yields: % 12.73/3.65 | (100) ? [v0] : (subactivity_occurrence(all_9_0_3, v0) & subactivity_occurrence(all_0_1_1, v0) & occurrence_of(v0, tptp0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (46) with tptp0, all_9_0_3, all_0_1_1 and discharging atoms min_precedes(all_0_1_1, all_9_0_3, tptp0), yields: % 12.73/3.65 | (101) ? [v0] : (min_precedes(v0, all_9_0_3, tptp0) & root(v0, tptp0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (15) with all_9_0_3, all_0_2_2 and discharging atoms root(all_9_0_3, all_0_2_2), yields: % 12.73/3.65 | (102) ? [v0] : (atocc(all_9_0_3, v0) & subactivity(v0, all_0_2_2)) % 12.73/3.65 | % 12.73/3.65 | Instantiating (102) with all_33_0_10 yields: % 12.73/3.65 | (103) atocc(all_9_0_3, all_33_0_10) & subactivity(all_33_0_10, all_0_2_2) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (103) yields: % 12.73/3.65 | (104) atocc(all_9_0_3, all_33_0_10) % 12.73/3.65 | (105) subactivity(all_33_0_10, all_0_2_2) % 12.73/3.65 | % 12.73/3.65 | Instantiating (101) with all_37_0_12 yields: % 12.73/3.65 | (106) min_precedes(all_37_0_12, all_9_0_3, tptp0) & root(all_37_0_12, tptp0) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (106) yields: % 12.73/3.65 | (107) min_precedes(all_37_0_12, all_9_0_3, tptp0) % 12.73/3.65 | (108) root(all_37_0_12, tptp0) % 12.73/3.65 | % 12.73/3.65 | Instantiating (100) with all_39_0_13 yields: % 12.73/3.65 | (109) subactivity_occurrence(all_9_0_3, all_39_0_13) & subactivity_occurrence(all_0_1_1, all_39_0_13) & occurrence_of(all_39_0_13, tptp0) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (109) yields: % 12.73/3.65 | (110) subactivity_occurrence(all_9_0_3, all_39_0_13) % 12.73/3.65 | (111) subactivity_occurrence(all_0_1_1, all_39_0_13) % 12.73/3.65 | (112) occurrence_of(all_39_0_13, tptp0) % 12.73/3.65 | % 12.73/3.65 | Instantiating (99) with all_43_0_15 yields: % 12.73/3.65 | (113) activity(all_43_0_15) & occurrence_of(all_9_0_3, all_43_0_15) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (113) yields: % 12.73/3.65 | (114) activity(all_43_0_15) % 12.73/3.65 | (115) occurrence_of(all_9_0_3, all_43_0_15) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (12) with all_43_0_15, all_9_3_6, all_9_0_3 and discharging atoms occurrence_of(all_9_0_3, all_43_0_15), occurrence_of(all_9_0_3, all_9_3_6), yields: % 12.73/3.65 | (116) all_43_0_15 = all_9_3_6 % 12.73/3.65 | % 12.73/3.65 | From (116) and (115) follows: % 12.73/3.65 | (83) occurrence_of(all_9_0_3, all_9_3_6) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (66) with all_33_0_10, all_9_0_3 and discharging atoms atocc(all_9_0_3, all_33_0_10), yields: % 12.73/3.65 | (118) ? [v0] : (subactivity(all_33_0_10, v0) & atomic(v0) & occurrence_of(all_9_0_3, v0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (4) with all_9_0_3, all_37_0_12, tptp0 and discharging atoms min_precedes(all_37_0_12, all_9_0_3, tptp0), yields: % 12.73/3.65 | (119) ? [v0] : (subactivity_occurrence(all_37_0_12, v0) & subactivity_occurrence(all_9_0_3, v0) & occurrence_of(v0, tptp0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (46) with tptp0, all_9_0_3, all_37_0_12 and discharging atoms min_precedes(all_37_0_12, all_9_0_3, tptp0), yields: % 12.73/3.65 | (101) ? [v0] : (min_precedes(v0, all_9_0_3, tptp0) & root(v0, tptp0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (53) with all_39_0_13, tptp0, all_9_0_3, all_37_0_12 and discharging atoms min_precedes(all_37_0_12, all_9_0_3, tptp0), subactivity_occurrence(all_9_0_3, all_39_0_13), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.65 | (121) subactivity_occurrence(all_37_0_12, all_39_0_13) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (68) with tptp0, all_39_0_13, all_0_1_1 and discharging atoms subactivity_occurrence(all_0_1_1, all_39_0_13), root(all_0_1_1, tptp0), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.65 | (122) root_occ(all_0_1_1, all_39_0_13) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (61) with all_39_0_13 and discharging atoms occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.65 | (123) ? [v0] : ? [v1] : (next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_39_0_13) & root_occ(v0, all_39_0_13) & occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 12.73/3.65 | % 12.73/3.65 | Instantiating formula (63) with all_39_0_13, tptp0 and discharging atoms occurrence_of(all_39_0_13, tptp0), ~ atomic(tptp0), yields: % 12.73/3.65 | (124) ? [v0] : (subactivity_occurrence(v0, all_39_0_13) & root(v0, tptp0)) % 12.73/3.65 | % 12.73/3.65 | Instantiating (124) with all_55_0_16 yields: % 12.73/3.65 | (125) subactivity_occurrence(all_55_0_16, all_39_0_13) & root(all_55_0_16, tptp0) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (125) yields: % 12.73/3.65 | (126) subactivity_occurrence(all_55_0_16, all_39_0_13) % 12.73/3.65 | (127) root(all_55_0_16, tptp0) % 12.73/3.65 | % 12.73/3.65 | Instantiating (123) with all_59_0_18, all_59_1_19 yields: % 12.73/3.65 | (128) next_subocc(all_59_1_19, all_59_0_18, tptp0) & leaf_occ(all_59_0_18, all_39_0_13) & root_occ(all_59_1_19, all_39_0_13) & occurrence_of(all_59_1_19, tptp4) & (occurrence_of(all_59_0_18, tptp2) | occurrence_of(all_59_0_18, tptp3)) % 12.73/3.65 | % 12.73/3.65 | Applying alpha-rule on (128) yields: % 12.73/3.65 | (129) leaf_occ(all_59_0_18, all_39_0_13) % 12.73/3.65 | (130) occurrence_of(all_59_0_18, tptp2) | occurrence_of(all_59_0_18, tptp3) % 12.73/3.65 | (131) next_subocc(all_59_1_19, all_59_0_18, tptp0) % 12.73/3.66 | (132) occurrence_of(all_59_1_19, tptp4) % 12.73/3.66 | (133) root_occ(all_59_1_19, all_39_0_13) % 12.73/3.66 | % 12.73/3.66 | Instantiating (119) with all_61_0_20 yields: % 12.73/3.66 | (134) subactivity_occurrence(all_37_0_12, all_61_0_20) & subactivity_occurrence(all_9_0_3, all_61_0_20) & occurrence_of(all_61_0_20, tptp0) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (134) yields: % 12.73/3.66 | (135) subactivity_occurrence(all_37_0_12, all_61_0_20) % 12.73/3.66 | (136) subactivity_occurrence(all_9_0_3, all_61_0_20) % 12.73/3.66 | (137) occurrence_of(all_61_0_20, tptp0) % 12.73/3.66 | % 12.73/3.66 | Instantiating (118) with all_63_0_21 yields: % 12.73/3.66 | (138) subactivity(all_33_0_10, all_63_0_21) & atomic(all_63_0_21) & occurrence_of(all_9_0_3, all_63_0_21) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (138) yields: % 12.73/3.66 | (139) subactivity(all_33_0_10, all_63_0_21) % 12.73/3.66 | (140) atomic(all_63_0_21) % 12.73/3.66 | (141) occurrence_of(all_9_0_3, all_63_0_21) % 12.73/3.66 | % 12.73/3.66 | Instantiating (101) with all_65_0_22 yields: % 12.73/3.66 | (142) min_precedes(all_65_0_22, all_9_0_3, tptp0) & root(all_65_0_22, tptp0) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (142) yields: % 12.73/3.66 | (143) min_precedes(all_65_0_22, all_9_0_3, tptp0) % 12.73/3.66 | (144) root(all_65_0_22, tptp0) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (64) with tptp0, all_39_0_13, all_0_1_1, all_59_1_19 and discharging atoms root_occ(all_59_1_19, all_39_0_13), root_occ(all_0_1_1, all_39_0_13), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.66 | (145) all_59_1_19 = all_0_1_1 % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (12) with all_63_0_21, all_9_3_6, all_9_0_3 and discharging atoms occurrence_of(all_9_0_3, all_63_0_21), occurrence_of(all_9_0_3, all_9_3_6), yields: % 12.73/3.66 | (146) all_63_0_21 = all_9_3_6 % 12.73/3.66 | % 12.73/3.66 | From (145) and (131) follows: % 12.73/3.66 | (147) next_subocc(all_0_1_1, all_59_0_18, tptp0) % 12.73/3.66 | % 12.73/3.66 | From (145) and (133) follows: % 12.73/3.66 | (122) root_occ(all_0_1_1, all_39_0_13) % 12.73/3.66 | % 12.73/3.66 | From (146) and (141) follows: % 12.73/3.66 | (83) occurrence_of(all_9_0_3, all_9_3_6) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (4) with all_9_0_3, all_65_0_22, tptp0 and discharging atoms min_precedes(all_65_0_22, all_9_0_3, tptp0), yields: % 12.73/3.66 | (150) ? [v0] : (subactivity_occurrence(all_65_0_22, v0) & subactivity_occurrence(all_9_0_3, v0) & occurrence_of(v0, tptp0)) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (46) with tptp0, all_9_0_3, all_65_0_22 and discharging atoms min_precedes(all_65_0_22, all_9_0_3, tptp0), yields: % 12.73/3.66 | (101) ? [v0] : (min_precedes(v0, all_9_0_3, tptp0) & root(v0, tptp0)) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (3) with all_39_0_13, all_59_0_18 and discharging atoms leaf_occ(all_59_0_18, all_39_0_13), yields: % 12.73/3.66 | (152) ? [v0] : (leaf(all_59_0_18, v0) & subactivity_occurrence(all_59_0_18, all_39_0_13) & occurrence_of(all_39_0_13, v0)) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (40) with all_59_0_18, all_0_1_1, all_9_0_3, all_39_0_13, tptp0 and discharging atoms min_precedes(all_0_1_1, all_9_0_3, tptp0), leaf_occ(all_59_0_18, all_39_0_13), root_occ(all_0_1_1, all_39_0_13), subactivity_occurrence(all_9_0_3, all_39_0_13), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.66 | (153) all_59_0_18 = all_9_0_3 | min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (7) with all_39_0_13, all_0_1_1 and discharging atoms root_occ(all_0_1_1, all_39_0_13), yields: % 12.73/3.66 | (154) ? [v0] : (subactivity_occurrence(all_0_1_1, all_39_0_13) & root(all_0_1_1, v0) & occurrence_of(all_39_0_13, v0)) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (68) with tptp0, all_39_0_13, all_37_0_12 and discharging atoms subactivity_occurrence(all_37_0_12, all_39_0_13), root(all_37_0_12, tptp0), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.66 | (155) root_occ(all_37_0_12, all_39_0_13) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (68) with tptp0, all_39_0_13, all_55_0_16 and discharging atoms subactivity_occurrence(all_55_0_16, all_39_0_13), root(all_55_0_16, tptp0), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.66 | (156) root_occ(all_55_0_16, all_39_0_13) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (53) with all_61_0_20, tptp0, all_9_0_3, all_65_0_22 and discharging atoms min_precedes(all_65_0_22, all_9_0_3, tptp0), subactivity_occurrence(all_9_0_3, all_61_0_20), occurrence_of(all_61_0_20, tptp0), yields: % 12.73/3.66 | (157) subactivity_occurrence(all_65_0_22, all_61_0_20) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (68) with tptp0, all_61_0_20, all_37_0_12 and discharging atoms subactivity_occurrence(all_37_0_12, all_61_0_20), root(all_37_0_12, tptp0), occurrence_of(all_61_0_20, tptp0), yields: % 12.73/3.66 | (158) root_occ(all_37_0_12, all_61_0_20) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (61) with all_61_0_20 and discharging atoms occurrence_of(all_61_0_20, tptp0), yields: % 12.73/3.66 | (159) ? [v0] : ? [v1] : (next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_61_0_20) & root_occ(v0, all_61_0_20) & occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 12.73/3.66 | % 12.73/3.66 | Instantiating formula (63) with all_61_0_20, tptp0 and discharging atoms occurrence_of(all_61_0_20, tptp0), ~ atomic(tptp0), yields: % 12.73/3.66 | (160) ? [v0] : (subactivity_occurrence(v0, all_61_0_20) & root(v0, tptp0)) % 12.73/3.66 | % 12.73/3.66 | Instantiating (160) with all_83_0_24 yields: % 12.73/3.66 | (161) subactivity_occurrence(all_83_0_24, all_61_0_20) & root(all_83_0_24, tptp0) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (161) yields: % 12.73/3.66 | (162) subactivity_occurrence(all_83_0_24, all_61_0_20) % 12.73/3.66 | (163) root(all_83_0_24, tptp0) % 12.73/3.66 | % 12.73/3.66 | Instantiating (159) with all_85_0_25, all_85_1_26 yields: % 12.73/3.66 | (164) next_subocc(all_85_1_26, all_85_0_25, tptp0) & leaf_occ(all_85_0_25, all_61_0_20) & root_occ(all_85_1_26, all_61_0_20) & occurrence_of(all_85_1_26, tptp4) & (occurrence_of(all_85_0_25, tptp2) | occurrence_of(all_85_0_25, tptp3)) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (164) yields: % 12.73/3.66 | (165) root_occ(all_85_1_26, all_61_0_20) % 12.73/3.66 | (166) occurrence_of(all_85_0_25, tptp2) | occurrence_of(all_85_0_25, tptp3) % 12.73/3.66 | (167) occurrence_of(all_85_1_26, tptp4) % 12.73/3.66 | (168) next_subocc(all_85_1_26, all_85_0_25, tptp0) % 12.73/3.66 | (169) leaf_occ(all_85_0_25, all_61_0_20) % 12.73/3.66 | % 12.73/3.66 | Instantiating (154) with all_89_0_28 yields: % 12.73/3.66 | (170) subactivity_occurrence(all_0_1_1, all_39_0_13) & root(all_0_1_1, all_89_0_28) & occurrence_of(all_39_0_13, all_89_0_28) % 12.73/3.66 | % 12.73/3.66 | Applying alpha-rule on (170) yields: % 12.73/3.66 | (111) subactivity_occurrence(all_0_1_1, all_39_0_13) % 12.73/3.67 | (172) root(all_0_1_1, all_89_0_28) % 12.73/3.67 | (173) occurrence_of(all_39_0_13, all_89_0_28) % 12.73/3.67 | % 12.73/3.67 | Instantiating (152) with all_91_0_29 yields: % 12.73/3.67 | (174) leaf(all_59_0_18, all_91_0_29) & subactivity_occurrence(all_59_0_18, all_39_0_13) & occurrence_of(all_39_0_13, all_91_0_29) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (174) yields: % 12.73/3.67 | (175) leaf(all_59_0_18, all_91_0_29) % 12.73/3.67 | (176) subactivity_occurrence(all_59_0_18, all_39_0_13) % 12.73/3.67 | (177) occurrence_of(all_39_0_13, all_91_0_29) % 12.73/3.67 | % 12.73/3.67 | Instantiating (101) with all_93_0_30 yields: % 12.73/3.67 | (178) min_precedes(all_93_0_30, all_9_0_3, tptp0) & root(all_93_0_30, tptp0) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (178) yields: % 12.73/3.67 | (179) min_precedes(all_93_0_30, all_9_0_3, tptp0) % 12.73/3.67 | (180) root(all_93_0_30, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating (150) with all_99_0_33 yields: % 12.73/3.67 | (181) subactivity_occurrence(all_65_0_22, all_99_0_33) & subactivity_occurrence(all_9_0_3, all_99_0_33) & occurrence_of(all_99_0_33, tptp0) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (181) yields: % 12.73/3.67 | (182) subactivity_occurrence(all_65_0_22, all_99_0_33) % 12.73/3.67 | (183) subactivity_occurrence(all_9_0_3, all_99_0_33) % 12.73/3.67 | (184) occurrence_of(all_99_0_33, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (12) with all_91_0_29, tptp0, all_39_0_13 and discharging atoms occurrence_of(all_39_0_13, all_91_0_29), occurrence_of(all_39_0_13, tptp0), yields: % 12.73/3.67 | (185) all_91_0_29 = tptp0 % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (64) with all_89_0_28, all_39_0_13, all_0_1_1, all_55_0_16 and discharging atoms root_occ(all_55_0_16, all_39_0_13), root_occ(all_0_1_1, all_39_0_13), occurrence_of(all_39_0_13, all_89_0_28), yields: % 12.73/3.67 | (186) all_55_0_16 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (64) with all_89_0_28, all_39_0_13, all_55_0_16, all_37_0_12 and discharging atoms root_occ(all_55_0_16, all_39_0_13), root_occ(all_37_0_12, all_39_0_13), occurrence_of(all_39_0_13, all_89_0_28), yields: % 12.73/3.67 | (187) all_55_0_16 = all_37_0_12 % 12.73/3.67 | % 12.73/3.67 | Combining equations (187,186) yields a new equation: % 12.73/3.67 | (188) all_37_0_12 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | Simplifying 188 yields: % 12.73/3.67 | (189) all_37_0_12 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | From (185) and (175) follows: % 12.73/3.67 | (190) leaf(all_59_0_18, tptp0) % 12.73/3.67 | % 12.73/3.67 | From (189) and (158) follows: % 12.73/3.67 | (191) root_occ(all_0_1_1, all_61_0_20) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (74) with tptp0, all_59_0_18 and discharging atoms leaf(all_59_0_18, tptp0), ~ atomic(tptp0), yields: % 12.73/3.67 | (192) ? [v0] : (leaf_occ(all_59_0_18, v0) & occurrence_of(v0, tptp0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (46) with tptp0, all_9_0_3, all_93_0_30 and discharging atoms min_precedes(all_93_0_30, all_9_0_3, tptp0), yields: % 12.73/3.67 | (101) ? [v0] : (min_precedes(v0, all_9_0_3, tptp0) & root(v0, tptp0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (3) with all_61_0_20, all_85_0_25 and discharging atoms leaf_occ(all_85_0_25, all_61_0_20), yields: % 12.73/3.67 | (194) ? [v0] : (leaf(all_85_0_25, v0) & subactivity_occurrence(all_85_0_25, all_61_0_20) & occurrence_of(all_61_0_20, v0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (68) with tptp0, all_61_0_20, all_65_0_22 and discharging atoms subactivity_occurrence(all_65_0_22, all_61_0_20), root(all_65_0_22, tptp0), occurrence_of(all_61_0_20, tptp0), yields: % 12.73/3.67 | (195) root_occ(all_65_0_22, all_61_0_20) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (55) with all_39_0_13, all_59_0_18 and discharging atoms subactivity_occurrence(all_59_0_18, all_39_0_13), yields: % 12.73/3.67 | (196) activity_occurrence(all_59_0_18) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (68) with tptp0, all_61_0_20, all_83_0_24 and discharging atoms subactivity_occurrence(all_83_0_24, all_61_0_20), root(all_83_0_24, tptp0), occurrence_of(all_61_0_20, tptp0), yields: % 12.73/3.67 | (197) root_occ(all_83_0_24, all_61_0_20) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (53) with all_99_0_33, tptp0, all_9_0_3, all_93_0_30 and discharging atoms min_precedes(all_93_0_30, all_9_0_3, tptp0), subactivity_occurrence(all_9_0_3, all_99_0_33), occurrence_of(all_99_0_33, tptp0), yields: % 12.73/3.67 | (198) subactivity_occurrence(all_93_0_30, all_99_0_33) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (68) with tptp0, all_99_0_33, all_65_0_22 and discharging atoms subactivity_occurrence(all_65_0_22, all_99_0_33), root(all_65_0_22, tptp0), occurrence_of(all_99_0_33, tptp0), yields: % 12.73/3.67 | (199) root_occ(all_65_0_22, all_99_0_33) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (61) with all_99_0_33 and discharging atoms occurrence_of(all_99_0_33, tptp0), yields: % 12.73/3.67 | (200) ? [v0] : ? [v1] : (next_subocc(v0, v1, tptp0) & leaf_occ(v1, all_99_0_33) & root_occ(v0, all_99_0_33) & occurrence_of(v0, tptp4) & (occurrence_of(v1, tptp2) | occurrence_of(v1, tptp3))) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (63) with all_99_0_33, tptp0 and discharging atoms occurrence_of(all_99_0_33, tptp0), ~ atomic(tptp0), yields: % 12.73/3.67 | (201) ? [v0] : (subactivity_occurrence(v0, all_99_0_33) & root(v0, tptp0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating (194) with all_125_0_39 yields: % 12.73/3.67 | (202) leaf(all_85_0_25, all_125_0_39) & subactivity_occurrence(all_85_0_25, all_61_0_20) & occurrence_of(all_61_0_20, all_125_0_39) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (202) yields: % 12.73/3.67 | (203) leaf(all_85_0_25, all_125_0_39) % 12.73/3.67 | (204) subactivity_occurrence(all_85_0_25, all_61_0_20) % 12.73/3.67 | (205) occurrence_of(all_61_0_20, all_125_0_39) % 12.73/3.67 | % 12.73/3.67 | Instantiating (192) with all_127_0_40 yields: % 12.73/3.67 | (206) leaf_occ(all_59_0_18, all_127_0_40) & occurrence_of(all_127_0_40, tptp0) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (206) yields: % 12.73/3.67 | (207) leaf_occ(all_59_0_18, all_127_0_40) % 12.73/3.67 | (208) occurrence_of(all_127_0_40, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating (101) with all_139_0_46 yields: % 12.73/3.67 | (209) min_precedes(all_139_0_46, all_9_0_3, tptp0) & root(all_139_0_46, tptp0) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (209) yields: % 12.73/3.67 | (210) min_precedes(all_139_0_46, all_9_0_3, tptp0) % 12.73/3.67 | (211) root(all_139_0_46, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating (200) with all_145_0_49, all_145_1_50 yields: % 12.73/3.67 | (212) next_subocc(all_145_1_50, all_145_0_49, tptp0) & leaf_occ(all_145_0_49, all_99_0_33) & root_occ(all_145_1_50, all_99_0_33) & occurrence_of(all_145_1_50, tptp4) & (occurrence_of(all_145_0_49, tptp2) | occurrence_of(all_145_0_49, tptp3)) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (212) yields: % 12.73/3.67 | (213) root_occ(all_145_1_50, all_99_0_33) % 12.73/3.67 | (214) next_subocc(all_145_1_50, all_145_0_49, tptp0) % 12.73/3.67 | (215) leaf_occ(all_145_0_49, all_99_0_33) % 12.73/3.67 | (216) occurrence_of(all_145_0_49, tptp2) | occurrence_of(all_145_0_49, tptp3) % 12.73/3.67 | (217) occurrence_of(all_145_1_50, tptp4) % 12.73/3.67 | % 12.73/3.67 | Instantiating (201) with all_147_0_51 yields: % 12.73/3.67 | (218) subactivity_occurrence(all_147_0_51, all_99_0_33) & root(all_147_0_51, tptp0) % 12.73/3.67 | % 12.73/3.67 | Applying alpha-rule on (218) yields: % 12.73/3.67 | (219) subactivity_occurrence(all_147_0_51, all_99_0_33) % 12.73/3.67 | (220) root(all_147_0_51, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (64) with all_125_0_39, all_61_0_20, all_0_1_1, all_83_0_24 and discharging atoms root_occ(all_83_0_24, all_61_0_20), root_occ(all_0_1_1, all_61_0_20), occurrence_of(all_61_0_20, all_125_0_39), yields: % 12.73/3.67 | (221) all_83_0_24 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (64) with all_125_0_39, all_61_0_20, all_83_0_24, all_65_0_22 and discharging atoms root_occ(all_83_0_24, all_61_0_20), root_occ(all_65_0_22, all_61_0_20), occurrence_of(all_61_0_20, all_125_0_39), yields: % 12.73/3.67 | (222) all_83_0_24 = all_65_0_22 % 12.73/3.67 | % 12.73/3.67 | Combining equations (222,221) yields a new equation: % 12.73/3.67 | (223) all_65_0_22 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | Simplifying 223 yields: % 12.73/3.67 | (224) all_65_0_22 = all_0_1_1 % 12.73/3.67 | % 12.73/3.67 | From (224) and (199) follows: % 12.73/3.67 | (225) root_occ(all_0_1_1, all_99_0_33) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (52) with all_59_0_18 and discharging atoms activity_occurrence(all_59_0_18), yields: % 12.73/3.67 | (226) ? [v0] : (activity(v0) & occurrence_of(all_59_0_18, v0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (43) with all_139_0_46, tptp0, all_9_0_3 and discharging atoms min_precedes(all_139_0_46, all_9_0_3, tptp0), yields: % 12.73/3.67 | (227) leaf(all_9_0_3, tptp0) | ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (3) with all_99_0_33, all_145_0_49 and discharging atoms leaf_occ(all_145_0_49, all_99_0_33), yields: % 12.73/3.67 | (228) ? [v0] : (leaf(all_145_0_49, v0) & subactivity_occurrence(all_145_0_49, all_99_0_33) & occurrence_of(all_99_0_33, v0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (3) with all_127_0_40, all_59_0_18 and discharging atoms leaf_occ(all_59_0_18, all_127_0_40), yields: % 12.73/3.67 | (229) ? [v0] : (leaf(all_59_0_18, v0) & subactivity_occurrence(all_59_0_18, all_127_0_40) & occurrence_of(all_127_0_40, v0)) % 12.73/3.67 | % 12.73/3.67 | Instantiating formula (68) with tptp0, all_99_0_33, all_93_0_30 and discharging atoms subactivity_occurrence(all_93_0_30, all_99_0_33), root(all_93_0_30, tptp0), occurrence_of(all_99_0_33, tptp0), yields: % 12.73/3.68 | (230) root_occ(all_93_0_30, all_99_0_33) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (68) with tptp0, all_99_0_33, all_147_0_51 and discharging atoms subactivity_occurrence(all_147_0_51, all_99_0_33), root(all_147_0_51, tptp0), occurrence_of(all_99_0_33, tptp0), yields: % 12.73/3.68 | (231) root_occ(all_147_0_51, all_99_0_33) % 12.73/3.68 | % 12.73/3.68 | Instantiating (229) with all_204_0_60 yields: % 12.73/3.68 | (232) leaf(all_59_0_18, all_204_0_60) & subactivity_occurrence(all_59_0_18, all_127_0_40) & occurrence_of(all_127_0_40, all_204_0_60) % 12.73/3.68 | % 12.73/3.68 | Applying alpha-rule on (232) yields: % 12.73/3.68 | (233) leaf(all_59_0_18, all_204_0_60) % 12.73/3.68 | (234) subactivity_occurrence(all_59_0_18, all_127_0_40) % 12.73/3.68 | (235) occurrence_of(all_127_0_40, all_204_0_60) % 12.73/3.68 | % 12.73/3.68 | Instantiating (228) with all_206_0_61 yields: % 12.73/3.68 | (236) leaf(all_145_0_49, all_206_0_61) & subactivity_occurrence(all_145_0_49, all_99_0_33) & occurrence_of(all_99_0_33, all_206_0_61) % 12.73/3.68 | % 12.73/3.68 | Applying alpha-rule on (236) yields: % 12.73/3.68 | (237) leaf(all_145_0_49, all_206_0_61) % 12.73/3.68 | (238) subactivity_occurrence(all_145_0_49, all_99_0_33) % 12.73/3.68 | (239) occurrence_of(all_99_0_33, all_206_0_61) % 12.73/3.68 | % 12.73/3.68 | Instantiating (226) with all_258_0_90 yields: % 12.73/3.68 | (240) activity(all_258_0_90) & occurrence_of(all_59_0_18, all_258_0_90) % 12.73/3.68 | % 12.73/3.68 | Applying alpha-rule on (240) yields: % 12.73/3.68 | (241) activity(all_258_0_90) % 12.73/3.68 | (242) occurrence_of(all_59_0_18, all_258_0_90) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (12) with all_204_0_60, tptp0, all_127_0_40 and discharging atoms occurrence_of(all_127_0_40, all_204_0_60), occurrence_of(all_127_0_40, tptp0), yields: % 12.73/3.68 | (243) all_204_0_60 = tptp0 % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (64) with all_206_0_61, all_99_0_33, all_0_1_1, all_147_0_51 and discharging atoms root_occ(all_147_0_51, all_99_0_33), root_occ(all_0_1_1, all_99_0_33), occurrence_of(all_99_0_33, all_206_0_61), yields: % 12.73/3.68 | (244) all_147_0_51 = all_0_1_1 % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (64) with all_206_0_61, all_99_0_33, all_147_0_51, all_93_0_30 and discharging atoms root_occ(all_147_0_51, all_99_0_33), root_occ(all_93_0_30, all_99_0_33), occurrence_of(all_99_0_33, all_206_0_61), yields: % 12.73/3.68 | (245) all_147_0_51 = all_93_0_30 % 12.73/3.68 | % 12.73/3.68 | Combining equations (245,244) yields a new equation: % 12.73/3.68 | (246) all_93_0_30 = all_0_1_1 % 12.73/3.68 | % 12.73/3.68 | Simplifying 246 yields: % 12.73/3.68 | (247) all_93_0_30 = all_0_1_1 % 12.73/3.68 | % 12.73/3.68 | From (243) and (233) follows: % 12.73/3.68 | (190) leaf(all_59_0_18, tptp0) % 12.73/3.68 | % 12.73/3.68 | From (247) and (179) follows: % 12.73/3.68 | (86) min_precedes(all_0_1_1, all_9_0_3, tptp0) % 12.73/3.68 | % 12.73/3.68 +-Applying beta-rule and splitting (227), into two cases. % 12.73/3.68 |-Branch one: % 12.73/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.73/3.68 | % 12.73/3.68 +-Applying beta-rule and splitting (130), into two cases. % 12.73/3.68 |-Branch one: % 12.73/3.68 | (251) occurrence_of(all_59_0_18, tptp2) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (12) with tptp2, all_258_0_90, all_59_0_18 and discharging atoms occurrence_of(all_59_0_18, all_258_0_90), occurrence_of(all_59_0_18, tptp2), yields: % 12.73/3.68 | (252) all_258_0_90 = tptp2 % 12.73/3.68 | % 12.73/3.68 | From (252) and (242) follows: % 12.73/3.68 | (251) occurrence_of(all_59_0_18, tptp2) % 12.73/3.68 | % 12.73/3.68 +-Applying beta-rule and splitting (153), into two cases. % 12.73/3.68 |-Branch one: % 12.73/3.68 | (254) min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (51) with all_59_0_18, tptp0, all_9_0_3 and discharging atoms leaf(all_9_0_3, tptp0), min_precedes(all_9_0_3, all_59_0_18, tptp0), yields: % 12.73/3.68 | (255) $false % 12.73/3.68 | % 12.73/3.68 |-The branch is then unsatisfiable % 12.73/3.68 |-Branch two: % 12.73/3.68 | (256) ~ min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.73/3.68 | (257) all_59_0_18 = all_9_0_3 % 12.73/3.68 | % 12.73/3.68 | From (257) and (251) follows: % 12.73/3.68 | (258) occurrence_of(all_9_0_3, tptp2) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (12) with tptp2, all_9_3_6, all_9_0_3 and discharging atoms occurrence_of(all_9_0_3, all_9_3_6), occurrence_of(all_9_0_3, tptp2), yields: % 12.73/3.68 | (259) all_9_3_6 = tptp2 % 12.73/3.68 | % 12.73/3.68 | From (259) and (81) follows: % 12.73/3.68 | (260) send_message(tptp2, all_9_2_5, all_9_1_4, all_0_1_1, tptp0) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (71) with tptp0, all_0_1_1, all_9_1_4, all_9_2_5 and discharging atoms send_message(tptp2, all_9_2_5, all_9_1_4, all_0_1_1, tptp0), yields: % 12.73/3.68 | (255) $false % 12.73/3.68 | % 12.73/3.68 |-The branch is then unsatisfiable % 12.73/3.68 |-Branch two: % 12.73/3.68 | (262) ~ occurrence_of(all_59_0_18, tptp2) % 12.73/3.68 | (263) occurrence_of(all_59_0_18, tptp3) % 12.73/3.68 | % 12.73/3.68 | Instantiating formula (12) with tptp3, all_258_0_90, all_59_0_18 and discharging atoms occurrence_of(all_59_0_18, all_258_0_90), occurrence_of(all_59_0_18, tptp3), yields: % 12.73/3.68 | (264) all_258_0_90 = tptp3 % 12.73/3.68 | % 12.73/3.68 | From (264) and (242) follows: % 12.92/3.68 | (263) occurrence_of(all_59_0_18, tptp3) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (153), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (254) min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.92/3.68 | % 12.92/3.68 | Instantiating formula (51) with all_59_0_18, tptp0, all_9_0_3 and discharging atoms leaf(all_9_0_3, tptp0), min_precedes(all_9_0_3, all_59_0_18, tptp0), yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (256) ~ min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.92/3.68 | (257) all_59_0_18 = all_9_0_3 % 12.92/3.68 | % 12.92/3.68 | From (257) and (263) follows: % 12.92/3.68 | (270) occurrence_of(all_9_0_3, tptp3) % 12.92/3.68 | % 12.92/3.68 | Instantiating formula (12) with tptp3, all_9_3_6, all_9_0_3 and discharging atoms occurrence_of(all_9_0_3, all_9_3_6), occurrence_of(all_9_0_3, tptp3), yields: % 12.92/3.68 | (271) all_9_3_6 = tptp3 % 12.92/3.68 | % 12.92/3.68 | From (271) and (81) follows: % 12.92/3.68 | (272) send_message(tptp3, all_9_2_5, all_9_1_4, all_0_1_1, tptp0) % 12.92/3.68 | % 12.92/3.68 | Instantiating formula (42) with tptp0, all_0_1_1, all_9_1_4, all_9_2_5 and discharging atoms send_message(tptp3, all_9_2_5, all_9_1_4, all_0_1_1, tptp0), yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (274) ~ leaf(all_9_0_3, tptp0) % 12.92/3.68 | (275) ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (227), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.92/3.68 | % 12.92/3.68 | Using (250) and (274) yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (274) ~ leaf(all_9_0_3, tptp0) % 12.92/3.68 | (275) ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (227), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.92/3.68 | % 12.92/3.68 | Using (250) and (274) yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (274) ~ leaf(all_9_0_3, tptp0) % 12.92/3.68 | (275) ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (227), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.92/3.68 | % 12.92/3.68 | Using (250) and (274) yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (274) ~ leaf(all_9_0_3, tptp0) % 12.92/3.68 | (275) ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (227), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.92/3.68 | % 12.92/3.68 | Using (250) and (274) yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (274) ~ leaf(all_9_0_3, tptp0) % 12.92/3.68 | (275) ? [v0] : min_precedes(all_9_0_3, v0, tptp0) % 12.92/3.68 | % 12.92/3.68 +-Applying beta-rule and splitting (153), into two cases. % 12.92/3.68 |-Branch one: % 12.92/3.68 | (254) min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.92/3.68 | % 12.92/3.68 | Instantiating formula (37) with all_9_0_3, tptp0, all_59_0_18, all_0_1_1 and discharging atoms next_subocc(all_0_1_1, all_59_0_18, tptp0), min_precedes(all_9_0_3, all_59_0_18, tptp0), min_precedes(all_0_1_1, all_9_0_3, tptp0), yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 |-Branch two: % 12.92/3.68 | (256) ~ min_precedes(all_9_0_3, all_59_0_18, tptp0) % 12.92/3.68 | (257) all_59_0_18 = all_9_0_3 % 12.92/3.68 | % 12.92/3.68 | From (257) and (190) follows: % 12.92/3.68 | (250) leaf(all_9_0_3, tptp0) % 12.92/3.68 | % 12.92/3.68 | Using (250) and (274) yields: % 12.92/3.68 | (255) $false % 12.92/3.68 | % 12.92/3.68 |-The branch is then unsatisfiable % 12.92/3.68 % SZS output end Proof for theBenchmark % 12.92/3.68 % 12.92/3.68 3083ms %------------------------------------------------------------------------------