%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO018+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n008.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:44:03 EDT 2022 % Result : Theorem 50.87s 18.27s % Output : Proof 146.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO018+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n008.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 03:31:07 EDT 2022 % 0.13/0.34 % CPUTime : % 0.49/0.60 ____ _ % 0.49/0.60 ___ / __ \_____(_)___ ________ __________ % 0.49/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.49/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.49/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.49/0.60 % 0.49/0.60 A Theorem Prover for First-Order Logic % 0.49/0.60 (ePrincess v.1.0) % 0.49/0.60 % 0.49/0.60 (c) Philipp Rümmer, 2009-2015 % 0.49/0.60 (c) Peter Backeman, 2014-2015 % 0.49/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.49/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.49/0.60 Bug reports to peter@backeman.se % 0.49/0.60 % 0.49/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.49/0.60 % 0.49/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.69/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.81/1.00 Prover 0: Preprocessing ... % 2.50/1.23 Prover 0: Constructing countermodel ... % 19.36/5.94 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 19.67/6.02 Prover 1: Preprocessing ... % 20.65/6.20 Prover 1: Constructing countermodel ... % 30.31/8.54 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 30.62/8.59 Prover 2: Preprocessing ... % 31.35/8.76 Prover 2: Warning: ignoring some quantifiers % 31.35/8.77 Prover 2: Constructing countermodel ... % 40.36/11.55 Prover 0: stopped % 40.61/11.75 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 40.61/11.80 Prover 3: Preprocessing ... % 40.61/11.83 Prover 3: Constructing countermodel ... % 50.87/18.27 Prover 3: proved (6513ms) % 50.87/18.27 Prover 2: stopped % 50.87/18.27 Prover 1: stopped % 50.87/18.27 % 50.87/18.27 No countermodel exists, formula is valid % 50.87/18.27 % SZS status Theorem for theBenchmark % 50.87/18.27 % 50.87/18.27 Generating proof ... found it (size 286) % 146.07/96.13 % 146.07/96.13 % SZS output start Proof for theBenchmark % 146.07/96.13 Assumed formulas after preprocessing and simplification: % 146.07/96.13 | (0) ? [v0] : ? [v1] : ( ~ (tptp2 = tptp1) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) & subactivity_occurrence(v0, v1) & arboreal(v0) & atomic(tptp2) & atomic(tptp1) & atomic(tptp4) & atomic(tptp3) & occurrence_of(v1, tptp0) & ~ leaf_occ(v0, v1) & ~ atomic(tptp0) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ subactivity_occurrence(v5, v3) | ~ subactivity_occurrence(v4, v3) | ~ arboreal(v5) | ~ arboreal(v4) | ~ occurrence_of(v3, v2) | min_precedes(v5, v4, v2) | min_precedes(v4, v5, v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ leaf_occ(v3, v4) | ~ leaf_occ(v2, v4) | ~ occurrence_of(v4, v5) | atomic(v5)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ root_occ(v3, v4) | ~ root_occ(v2, v4) | ~ occurrence_of(v4, v5)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ next_subocc(v2, v3, v4) | ~ min_precedes(v5, v3, v4) | ~ min_precedes(v2, v5, v4)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ leaf_occ(v3, v2) | ~ occurrence_of(v2, v4) | ~ min_precedes(v3, v5, v4)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ root_occ(v3, v2) | ~ occurrence_of(v2, v4) | ~ min_precedes(v5, v3, v4)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ min_precedes(v3, v4, v5) | ~ min_precedes(v2, v3, v5) | min_precedes(v2, v4, v5)) & ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ occurrence_of(v2, v4) | ~ occurrence_of(v2, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ subactivity(v3, v4) | ~ atomic(v4) | ~ occurrence_of(v2, v4) | atocc(v2, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ leaf(v2, v4) | ~ subactivity_occurrence(v2, v3) | ~ occurrence_of(v3, v4) | leaf_occ(v2, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ leaf(v2, v3) | ~ min_precedes(v2, v4, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v2, v3) | ~ root(v2, v4) | ~ occurrence_of(v3, v4) | root_occ(v2, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ root(v3, v4) | ~ min_precedes(v2, v3, v4)) & ! [v2] : ! [v3] : ! [v4] : ( ~ next_subocc(v2, v3, v4) | arboreal(v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ next_subocc(v2, v3, v4) | arboreal(v2)) & ! [v2] : ! [v3] : ! [v4] : ( ~ next_subocc(v2, v3, v4) | min_precedes(v2, v3, v4)) & ! [v2] : ! [v3] : ! [v4] : ( ~ earlier(v3, v4) | ~ earlier(v2, v3) | earlier(v2, v4)) & ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v4, v2, v3) | leaf(v2, v3) | ? [v5] : min_precedes(v2, v5, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v3, v4, v2) | ? [v5] : ? [v6] : (subactivity(v6, v2) & subactivity(v5, v2) & atocc(v4, v6) & atocc(v3, v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v3, v4, v2) | ? [v5] : (subactivity_occurrence(v4, v5) & subactivity_occurrence(v3, v5) & occurrence_of(v5, v2))) & ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v2, v3, v4) | precedes(v2, v3)) & ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v2, v3, v4) | next_subocc(v2, v3, v4) | ? [v5] : (min_precedes(v5, v3, v4) & min_precedes(v2, v5, v4))) & ! [v2] : ! [v3] : ( ~ atocc(v2, v3) | ~ legal(v2) | root(v2, v3)) & ! [v2] : ! [v3] : ( ~ atocc(v2, v3) | ? [v4] : (subactivity(v3, v4) & atomic(v4) & occurrence_of(v2, v4))) & ! [v2] : ! [v3] : ( ~ leaf(v2, v3) | root(v2, v3) | ? [v4] : min_precedes(v4, v2, v3)) & ! [v2] : ! [v3] : ( ~ leaf(v2, v3) | atomic(v3) | ? [v4] : (leaf_occ(v2, v4) & occurrence_of(v4, v3))) & ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | ~ arboreal(v2) | ~ occurrence_of(v3, tptp0) | leaf_occ(v2, v3) | ? [v4] : ? [v5] : ? [v6] : (next_subocc(v2, v4, tptp0) & occurrence_of(v5, tptp4) & occurrence_of(v4, tptp3) & min_precedes(v5, v6, tptp0) & min_precedes(v4, v5, tptp0) & ! [v7] : (v7 = v6 | v7 = v5 | ~ min_precedes(v4, v7, tptp0)) & (occurrence_of(v6, tptp2) | occurrence_of(v6, tptp1)))) & ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | activity_occurrence(v3)) & ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | activity_occurrence(v2)) & ! [v2] : ! [v3] : ( ~ legal(v3) | ~ earlier(v2, v3) | precedes(v2, v3)) & ! [v2] : ! [v3] : ( ~ root(v3, v2) | ? [v4] : (subactivity(v4, v2) & atocc(v3, v4))) & ! [v2] : ! [v3] : ( ~ root(v2, v3) | leaf(v2, v3) | ? [v4] : min_precedes(v2, v4, v3)) & ! [v2] : ! [v3] : ( ~ root(v2, v3) | legal(v2)) & ! [v2] : ! [v3] : ( ~ precedes(v2, v3) | legal(v3)) & ! [v2] : ! [v3] : ( ~ precedes(v2, v3) | earlier(v2, v3)) & ! [v2] : ! [v3] : ( ~ arboreal(v2) | ~ occurrence_of(v2, v3) | atomic(v3)) & ! [v2] : ! [v3] : ( ~ next_subocc(v0, v2, tptp0) | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp2) | ~ occurrence_of(v2, tptp3) | ~ min_precedes(v2, v3, tptp0) | occurrence_of(v3, tptp1) | ? [v4] : (occurrence_of(v4, tptp1) & min_precedes(v2, v4, tptp0))) & ! [v2] : ! [v3] : ( ~ next_subocc(v0, v2, tptp0) | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp2) | ~ occurrence_of(v2, tptp3) | ~ min_precedes(v2, v3, tptp0) | ? [v4] : ((occurrence_of(v4, tptp2) & min_precedes(v2, v4, tptp0)) | (occurrence_of(v4, tptp1) & min_precedes(v2, v4, tptp0)))) & ! [v2] : ! [v3] : ( ~ next_subocc(v0, v2, tptp0) | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp1) | ~ occurrence_of(v2, tptp3) | ~ min_precedes(v2, v3, tptp0) | occurrence_of(v3, tptp2) | ? [v4] : (occurrence_of(v4, tptp2) & min_precedes(v2, v4, tptp0))) & ! [v2] : ! [v3] : ( ~ next_subocc(v0, v2, tptp0) | ~ leaf_occ(v3, v1) | ~ occurrence_of(v3, tptp1) | ~ occurrence_of(v2, tptp3) | ~ min_precedes(v2, v3, tptp0) | ? [v4] : ((occurrence_of(v4, tptp2) & min_precedes(v2, v4, tptp0)) | (occurrence_of(v4, tptp1) & min_precedes(v2, v4, tptp0)))) & ! [v2] : ! [v3] : ( ~ leaf_occ(v2, v3) | ? [v4] : (leaf(v2, v4) & subactivity_occurrence(v2, v3) & occurrence_of(v3, v4))) & ! [v2] : ! [v3] : ( ~ atomic(v3) | ~ occurrence_of(v2, v3) | arboreal(v2)) & ! [v2] : ! [v3] : ( ~ root_occ(v2, v3) | ? [v4] : (subactivity_occurrence(v2, v3) & root(v2, v4) & occurrence_of(v3, v4))) & ! [v2] : ! [v3] : ( ~ occurrence_of(v3, v2) | activity(v2)) & ! [v2] : ! [v3] : ( ~ occurrence_of(v3, v2) | activity_occurrence(v3)) & ! [v2] : ! [v3] : ( ~ occurrence_of(v3, v2) | atomic(v2) | ? [v4] : (subactivity_occurrence(v4, v3) & root(v4, v2))) & ! [v2] : ! [v3] : ( ~ earlier(v3, v2) | ~ earlier(v2, v3)) & ! [v2] : ( ~ activity(v2) | subactivity(v2, v2)) & ! [v2] : ( ~ activity_occurrence(v2) | ? [v3] : (activity(v3) & occurrence_of(v2, v3))) & ! [v2] : ( ~ legal(v2) | arboreal(v2))) % 146.24/96.16 | Instantiating (0) with all_0_0_0, all_0_1_1 yields: % 146.24/96.16 | (1) ~ (tptp2 = tptp1) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) & subactivity_occurrence(all_0_1_1, all_0_0_0) & arboreal(all_0_1_1) & atomic(tptp2) & atomic(tptp1) & atomic(tptp4) & atomic(tptp3) & occurrence_of(all_0_0_0, tptp0) & ~ leaf_occ(all_0_1_1, all_0_0_0) & ~ atomic(tptp0) & ! [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] : ( ~ 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] : ( ~ 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] : ( ~ 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) | ~ arboreal(v0) | ~ occurrence_of(v1, tptp0) | leaf_occ(v0, v1) | ? [v2] : ? [v3] : ? [v4] : (next_subocc(v0, v2, tptp0) & occurrence_of(v3, tptp4) & occurrence_of(v2, tptp3) & min_precedes(v3, v4, tptp0) & min_precedes(v2, v3, tptp0) & ! [v5] : (v5 = v4 | v5 = v3 | ~ min_precedes(v2, v5, tptp0)) & (occurrence_of(v4, tptp2) | occurrence_of(v4, tptp1)))) & ! [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] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | occurrence_of(v1, tptp1) | ? [v2] : (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0))) & ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | ? [v2] : ((occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0)) | (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0)))) & ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | occurrence_of(v1, tptp2) | ? [v2] : (occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0))) & ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | ? [v2] : ((occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0)) | (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0)))) & ! [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)) % 146.24/96.17 | % 146.24/96.17 | Applying alpha-rule on (1) yields: % 146.24/96.17 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, v3))) % 146.24/96.17 | (3) atomic(tptp1) % 146.24/96.17 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 146.24/96.18 | (5) atomic(tptp4) % 146.24/96.18 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) % 146.24/96.18 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 146.24/96.18 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 146.24/96.18 | (9) ~ (tptp2 = tptp1) % 146.24/96.18 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 146.24/96.18 | (11) ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | ? [v2] : ((occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0)) | (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0)))) % 146.24/96.18 | (12) occurrence_of(all_0_0_0, tptp0) % 146.24/96.18 | (13) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 146.24/96.18 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 146.24/96.18 | (15) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 146.24/96.18 | (16) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 146.24/96.18 | (17) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 146.24/96.18 | (18) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) % 146.24/96.18 | (19) ~ leaf_occ(all_0_1_1, all_0_0_0) % 146.24/96.18 | (20) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 146.24/96.18 | (21) ~ (tptp2 = tptp4) % 146.24/96.18 | (22) ~ (tptp2 = tptp3) % 146.24/96.18 | (23) ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) % 146.24/96.18 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 146.24/96.18 | (25) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 146.24/96.18 | (26) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 146.24/96.18 | (27) ~ (tptp4 = tptp3) % 146.24/96.18 | (28) arboreal(all_0_1_1) % 146.24/96.18 | (29) activity(tptp0) % 146.24/96.18 | (30) ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) % 146.24/96.18 | (31) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) % 146.24/96.18 | (32) subactivity_occurrence(all_0_1_1, all_0_0_0) % 146.24/96.18 | (33) ! [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)) % 146.24/96.18 | (34) ~ (tptp1 = tptp3) % 146.24/96.18 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 146.24/96.18 | (36) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 146.24/96.18 | (37) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 146.24/96.18 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 146.24/96.18 | (39) atomic(tptp3) % 146.24/96.18 | (40) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 146.24/96.18 | (41) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 146.24/96.18 | (42) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 146.24/96.18 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v0, v2, v3)) % 146.24/96.18 | (44) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 146.24/96.18 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 146.24/96.18 | (46) atomic(tptp2) % 146.24/96.18 | (47) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 146.24/96.18 | (48) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 146.24/96.18 | (49) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 146.24/96.18 | (50) ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | occurrence_of(v1, tptp1) | ? [v2] : (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0))) % 146.24/96.18 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v3, v1, v2)) % 146.24/96.18 | (52) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) % 146.24/96.18 | (53) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | ~ arboreal(v0) | ~ occurrence_of(v1, tptp0) | leaf_occ(v0, v1) | ? [v2] : ? [v3] : ? [v4] : (next_subocc(v0, v2, tptp0) & occurrence_of(v3, tptp4) & occurrence_of(v2, tptp3) & min_precedes(v3, v4, tptp0) & min_precedes(v2, v3, tptp0) & ! [v5] : (v5 = v4 | v5 = v3 | ~ min_precedes(v2, v5, tptp0)) & (occurrence_of(v4, tptp2) | occurrence_of(v4, tptp1)))) % 146.24/96.19 | (54) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 146.24/96.19 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 146.24/96.19 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 146.24/96.19 | (57) ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | ? [v2] : ((occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0)) | (occurrence_of(v2, tptp1) & min_precedes(v0, v2, tptp0)))) % 146.24/96.19 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 146.24/96.19 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 146.42/96.19 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 146.42/96.19 | (61) ~ atomic(tptp0) % 146.42/96.19 | (62) ~ (tptp1 = tptp4) % 146.42/96.19 | (63) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 146.42/96.19 | (64) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 146.42/96.19 | (65) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 146.42/96.19 | (66) ! [v0] : ! [v1] : ( ~ next_subocc(all_0_1_1, v0, tptp0) | ~ leaf_occ(v1, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0) | occurrence_of(v1, tptp2) | ? [v2] : (occurrence_of(v2, tptp2) & min_precedes(v0, v2, tptp0))) % 146.42/96.19 | (67) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (53) with all_0_0_0, all_0_1_1 and discharging atoms subactivity_occurrence(all_0_1_1, all_0_0_0), arboreal(all_0_1_1), occurrence_of(all_0_0_0, tptp0), ~ leaf_occ(all_0_1_1, all_0_0_0), yields: % 146.42/96.19 | (68) ? [v0] : ? [v1] : ? [v2] : (next_subocc(all_0_1_1, v0, tptp0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & min_precedes(v1, v2, tptp0) & min_precedes(v0, v1, tptp0) & ! [v3] : (v3 = v2 | v3 = v1 | ~ min_precedes(v0, v3, tptp0)) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 146.42/96.19 | % 146.42/96.19 | Instantiating (68) with all_15_0_3, all_15_1_4, all_15_2_5 yields: % 146.42/96.19 | (69) next_subocc(all_0_1_1, all_15_2_5, tptp0) & occurrence_of(all_15_1_4, tptp4) & occurrence_of(all_15_2_5, tptp3) & min_precedes(all_15_1_4, all_15_0_3, tptp0) & min_precedes(all_15_2_5, all_15_1_4, tptp0) & ! [v0] : (v0 = all_15_0_3 | v0 = all_15_1_4 | ~ min_precedes(all_15_2_5, v0, tptp0)) & (occurrence_of(all_15_0_3, tptp2) | occurrence_of(all_15_0_3, tptp1)) % 146.42/96.19 | % 146.42/96.19 | Applying alpha-rule on (69) yields: % 146.42/96.19 | (70) min_precedes(all_15_1_4, all_15_0_3, tptp0) % 146.42/96.19 | (71) occurrence_of(all_15_2_5, tptp3) % 146.42/96.19 | (72) occurrence_of(all_15_0_3, tptp2) | occurrence_of(all_15_0_3, tptp1) % 146.42/96.19 | (73) min_precedes(all_15_2_5, all_15_1_4, tptp0) % 146.42/96.19 | (74) occurrence_of(all_15_1_4, tptp4) % 146.42/96.19 | (75) ! [v0] : (v0 = all_15_0_3 | v0 = all_15_1_4 | ~ min_precedes(all_15_2_5, v0, tptp0)) % 146.42/96.19 | (76) next_subocc(all_0_1_1, all_15_2_5, tptp0) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (54) with tptp3, tptp4, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.19 | (77) tptp4 = tptp3 | ~ occurrence_of(all_15_2_5, tptp4) % 146.42/96.19 | % 146.42/96.19 +-Applying beta-rule and splitting (77), into two cases. % 146.42/96.19 |-Branch one: % 146.42/96.19 | (78) ~ occurrence_of(all_15_2_5, tptp4) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (35) with tptp0, all_15_2_5, all_0_1_1 and discharging atoms next_subocc(all_0_1_1, all_15_2_5, tptp0), yields: % 146.42/96.19 | (79) min_precedes(all_0_1_1, all_15_2_5, tptp0) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (20) with tptp4, all_15_1_4 and discharging atoms atomic(tptp4), occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.19 | (80) arboreal(all_15_1_4) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (48) with all_15_1_4, tptp4 and discharging atoms occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.19 | (81) activity(tptp4) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (37) with all_15_1_4, tptp4 and discharging atoms occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.19 | (82) activity_occurrence(all_15_1_4) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (20) with tptp3, all_15_2_5 and discharging atoms atomic(tptp3), occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.19 | (83) arboreal(all_15_2_5) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (48) with all_15_2_5, tptp3 and discharging atoms occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.19 | (84) activity(tptp3) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (37) with all_15_2_5, tptp3 and discharging atoms occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.19 | (85) activity_occurrence(all_15_2_5) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (2) with all_15_0_3, all_15_1_4, tptp0 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.42/96.19 | (86) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_15_0_3, v1) & atocc(all_15_1_4, v0)) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (4) with all_15_0_3, all_15_1_4, tptp0 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.42/96.19 | (87) ? [v0] : (subactivity_occurrence(all_15_0_3, v0) & subactivity_occurrence(all_15_1_4, v0) & occurrence_of(v0, tptp0)) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (38) with tptp0, all_15_0_3, all_15_1_4 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.42/96.19 | (88) precedes(all_15_1_4, all_15_0_3) % 146.42/96.19 | % 146.42/96.19 | Instantiating formula (41) with tptp0, all_15_0_3, all_15_1_4 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.42/96.19 | (89) next_subocc(all_15_1_4, all_15_0_3, tptp0) | ? [v0] : (min_precedes(v0, all_15_0_3, tptp0) & min_precedes(all_15_1_4, v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (43) with tptp0, all_15_0_3, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.20 | (90) min_precedes(all_15_2_5, all_15_0_3, tptp0) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (2) with all_15_1_4, all_15_2_5, tptp0 and discharging atoms min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.20 | (91) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_15_1_4, v1) & atocc(all_15_2_5, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (4) with all_15_1_4, all_15_2_5, tptp0 and discharging atoms min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.20 | (92) ? [v0] : (subactivity_occurrence(all_15_1_4, v0) & subactivity_occurrence(all_15_2_5, v0) & occurrence_of(v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (38) with tptp0, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.20 | (93) precedes(all_15_2_5, all_15_1_4) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (41) with tptp0, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.20 | (94) next_subocc(all_15_2_5, all_15_1_4, tptp0) | ? [v0] : (min_precedes(v0, all_15_1_4, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating (86) with all_46_0_7, all_46_1_8 yields: % 146.42/96.20 | (95) subactivity(all_46_0_7, tptp0) & subactivity(all_46_1_8, tptp0) & atocc(all_15_0_3, all_46_0_7) & atocc(all_15_1_4, all_46_1_8) % 146.42/96.20 | % 146.42/96.20 | Applying alpha-rule on (95) yields: % 146.42/96.20 | (96) subactivity(all_46_0_7, tptp0) % 146.42/96.20 | (97) subactivity(all_46_1_8, tptp0) % 146.42/96.20 | (98) atocc(all_15_0_3, all_46_0_7) % 146.42/96.20 | (99) atocc(all_15_1_4, all_46_1_8) % 146.42/96.20 | % 146.42/96.20 | Instantiating (92) with all_48_0_9 yields: % 146.42/96.20 | (100) subactivity_occurrence(all_15_1_4, all_48_0_9) & subactivity_occurrence(all_15_2_5, all_48_0_9) & occurrence_of(all_48_0_9, tptp0) % 146.42/96.20 | % 146.42/96.20 | Applying alpha-rule on (100) yields: % 146.42/96.20 | (101) subactivity_occurrence(all_15_1_4, all_48_0_9) % 146.42/96.20 | (102) subactivity_occurrence(all_15_2_5, all_48_0_9) % 146.42/96.20 | (103) occurrence_of(all_48_0_9, tptp0) % 146.42/96.20 | % 146.42/96.20 | Instantiating (91) with all_50_0_10, all_50_1_11 yields: % 146.42/96.20 | (104) subactivity(all_50_0_10, tptp0) & subactivity(all_50_1_11, tptp0) & atocc(all_15_1_4, all_50_0_10) & atocc(all_15_2_5, all_50_1_11) % 146.42/96.20 | % 146.42/96.20 | Applying alpha-rule on (104) yields: % 146.42/96.20 | (105) subactivity(all_50_0_10, tptp0) % 146.42/96.20 | (106) subactivity(all_50_1_11, tptp0) % 146.42/96.20 | (107) atocc(all_15_1_4, all_50_0_10) % 146.42/96.20 | (108) atocc(all_15_2_5, all_50_1_11) % 146.42/96.20 | % 146.42/96.20 | Instantiating (87) with all_52_0_12 yields: % 146.42/96.20 | (109) subactivity_occurrence(all_15_0_3, all_52_0_12) & subactivity_occurrence(all_15_1_4, all_52_0_12) & occurrence_of(all_52_0_12, tptp0) % 146.42/96.20 | % 146.42/96.20 | Applying alpha-rule on (109) yields: % 146.42/96.20 | (110) subactivity_occurrence(all_15_0_3, all_52_0_12) % 146.42/96.20 | (111) subactivity_occurrence(all_15_1_4, all_52_0_12) % 146.42/96.20 | (112) occurrence_of(all_52_0_12, tptp0) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (23) with tptp4 and discharging atoms activity(tptp4), yields: % 146.42/96.20 | (113) subactivity(tptp4, tptp4) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (23) with tptp3 and discharging atoms activity(tptp3), yields: % 146.42/96.20 | (114) subactivity(tptp3, tptp3) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (67) with all_15_1_4 and discharging atoms activity_occurrence(all_15_1_4), yields: % 146.42/96.20 | (115) ? [v0] : (activity(v0) & occurrence_of(all_15_1_4, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (67) with all_15_2_5 and discharging atoms activity_occurrence(all_15_2_5), yields: % 146.42/96.20 | (116) ? [v0] : (activity(v0) & occurrence_of(all_15_2_5, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (52) with all_50_0_10, all_15_1_4 and discharging atoms atocc(all_15_1_4, all_50_0_10), yields: % 146.42/96.20 | (117) ? [v0] : (subactivity(all_50_0_10, v0) & atomic(v0) & occurrence_of(all_15_1_4, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (52) with all_46_1_8, all_15_1_4 and discharging atoms atocc(all_15_1_4, all_46_1_8), yields: % 146.42/96.20 | (118) ? [v0] : (subactivity(all_46_1_8, v0) & atomic(v0) & occurrence_of(all_15_1_4, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (52) with all_50_1_11, all_15_2_5 and discharging atoms atocc(all_15_2_5, all_50_1_11), yields: % 146.42/96.20 | (119) ? [v0] : (subactivity(all_50_1_11, v0) & atomic(v0) & occurrence_of(all_15_2_5, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (17) with all_15_0_3, all_15_1_4 and discharging atoms precedes(all_15_1_4, all_15_0_3), yields: % 146.42/96.20 | (120) earlier(all_15_1_4, all_15_0_3) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (64) with all_15_1_4, all_15_2_5 and discharging atoms precedes(all_15_2_5, all_15_1_4), yields: % 146.42/96.20 | (121) legal(all_15_1_4) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (53) with all_52_0_12, all_15_1_4 and discharging atoms subactivity_occurrence(all_15_1_4, all_52_0_12), arboreal(all_15_1_4), occurrence_of(all_52_0_12, tptp0), yields: % 146.42/96.20 | (122) leaf_occ(all_15_1_4, all_52_0_12) | ? [v0] : ? [v1] : ? [v2] : (next_subocc(all_15_1_4, v0, tptp0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & min_precedes(v1, v2, tptp0) & min_precedes(v0, v1, tptp0) & ! [v3] : (v3 = v2 | v3 = v1 | ~ min_precedes(v0, v3, tptp0)) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (53) with all_48_0_9, all_15_2_5 and discharging atoms subactivity_occurrence(all_15_2_5, all_48_0_9), arboreal(all_15_2_5), occurrence_of(all_48_0_9, tptp0), yields: % 146.42/96.20 | (123) leaf_occ(all_15_2_5, all_48_0_9) | ? [v0] : ? [v1] : ? [v2] : (next_subocc(all_15_2_5, v0, tptp0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & min_precedes(v1, v2, tptp0) & min_precedes(v0, v1, tptp0) & ! [v3] : (v3 = v2 | v3 = v1 | ~ min_precedes(v0, v3, tptp0)) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (37) with all_52_0_12, tptp0 and discharging atoms occurrence_of(all_52_0_12, tptp0), yields: % 146.42/96.20 | (124) activity_occurrence(all_52_0_12) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (42) with all_52_0_12, tptp0 and discharging atoms occurrence_of(all_52_0_12, tptp0), ~ atomic(tptp0), yields: % 146.42/96.20 | (125) ? [v0] : (subactivity_occurrence(v0, all_52_0_12) & root(v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (37) with all_48_0_9, tptp0 and discharging atoms occurrence_of(all_48_0_9, tptp0), yields: % 146.42/96.20 | (126) activity_occurrence(all_48_0_9) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (42) with all_48_0_9, tptp0 and discharging atoms occurrence_of(all_48_0_9, tptp0), ~ atomic(tptp0), yields: % 146.42/96.20 | (127) ? [v0] : (subactivity_occurrence(v0, all_48_0_9) & root(v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (2) with all_15_0_3, all_15_2_5, tptp0 and discharging atoms min_precedes(all_15_2_5, all_15_0_3, tptp0), yields: % 146.42/96.20 | (128) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_15_0_3, v1) & atocc(all_15_2_5, v0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (41) with tptp0, all_15_0_3, all_15_2_5 and discharging atoms min_precedes(all_15_2_5, all_15_0_3, tptp0), yields: % 146.42/96.20 | (129) next_subocc(all_15_2_5, all_15_0_3, tptp0) | ? [v0] : (min_precedes(v0, all_15_0_3, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (43) with tptp0, all_15_1_4, all_15_2_5, all_0_1_1 and discharging atoms min_precedes(all_15_2_5, all_15_1_4, tptp0), min_precedes(all_0_1_1, all_15_2_5, tptp0), yields: % 146.42/96.20 | (130) min_precedes(all_0_1_1, all_15_1_4, tptp0) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (43) with tptp0, all_15_0_3, all_15_2_5, all_0_1_1 and discharging atoms min_precedes(all_15_2_5, all_15_0_3, tptp0), min_precedes(all_0_1_1, all_15_2_5, tptp0), yields: % 146.42/96.20 | (131) min_precedes(all_0_1_1, all_15_0_3, tptp0) % 146.42/96.20 | % 146.42/96.20 | Instantiating formula (2) with all_15_2_5, all_0_1_1, tptp0 and discharging atoms min_precedes(all_0_1_1, all_15_2_5, tptp0), yields: % 146.42/96.20 | (132) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_15_2_5, v1) & atocc(all_0_1_1, v0)) % 146.42/96.21 | % 146.42/96.21 | Instantiating (128) with all_84_0_17, all_84_1_18 yields: % 146.42/96.21 | (133) subactivity(all_84_0_17, tptp0) & subactivity(all_84_1_18, tptp0) & atocc(all_15_0_3, all_84_0_17) & atocc(all_15_2_5, all_84_1_18) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (133) yields: % 146.42/96.21 | (134) subactivity(all_84_0_17, tptp0) % 146.42/96.21 | (135) subactivity(all_84_1_18, tptp0) % 146.42/96.21 | (136) atocc(all_15_0_3, all_84_0_17) % 146.42/96.21 | (137) atocc(all_15_2_5, all_84_1_18) % 146.42/96.21 | % 146.42/96.21 | Instantiating (125) with all_86_0_19 yields: % 146.42/96.21 | (138) subactivity_occurrence(all_86_0_19, all_52_0_12) & root(all_86_0_19, tptp0) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (138) yields: % 146.42/96.21 | (139) subactivity_occurrence(all_86_0_19, all_52_0_12) % 146.42/96.21 | (140) root(all_86_0_19, tptp0) % 146.42/96.21 | % 146.42/96.21 | Instantiating (117) with all_88_0_20 yields: % 146.42/96.21 | (141) subactivity(all_50_0_10, all_88_0_20) & atomic(all_88_0_20) & occurrence_of(all_15_1_4, all_88_0_20) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (141) yields: % 146.42/96.21 | (142) subactivity(all_50_0_10, all_88_0_20) % 146.42/96.21 | (143) atomic(all_88_0_20) % 146.42/96.21 | (144) occurrence_of(all_15_1_4, all_88_0_20) % 146.42/96.21 | % 146.42/96.21 | Instantiating (116) with all_96_0_24 yields: % 146.42/96.21 | (145) activity(all_96_0_24) & occurrence_of(all_15_2_5, all_96_0_24) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (145) yields: % 146.42/96.21 | (146) activity(all_96_0_24) % 146.42/96.21 | (147) occurrence_of(all_15_2_5, all_96_0_24) % 146.42/96.21 | % 146.42/96.21 | Instantiating (115) with all_98_0_25 yields: % 146.42/96.21 | (148) activity(all_98_0_25) & occurrence_of(all_15_1_4, all_98_0_25) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (148) yields: % 146.42/96.21 | (149) activity(all_98_0_25) % 146.42/96.21 | (150) occurrence_of(all_15_1_4, all_98_0_25) % 146.42/96.21 | % 146.42/96.21 | Instantiating (119) with all_100_0_26 yields: % 146.42/96.21 | (151) subactivity(all_50_1_11, all_100_0_26) & atomic(all_100_0_26) & occurrence_of(all_15_2_5, all_100_0_26) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (151) yields: % 146.42/96.21 | (152) subactivity(all_50_1_11, all_100_0_26) % 146.42/96.21 | (153) atomic(all_100_0_26) % 146.42/96.21 | (154) occurrence_of(all_15_2_5, all_100_0_26) % 146.42/96.21 | % 146.42/96.21 | Instantiating (118) with all_102_0_27 yields: % 146.42/96.21 | (155) subactivity(all_46_1_8, all_102_0_27) & atomic(all_102_0_27) & occurrence_of(all_15_1_4, all_102_0_27) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (155) yields: % 146.42/96.21 | (156) subactivity(all_46_1_8, all_102_0_27) % 146.42/96.21 | (157) atomic(all_102_0_27) % 146.42/96.21 | (158) occurrence_of(all_15_1_4, all_102_0_27) % 146.42/96.21 | % 146.42/96.21 | Instantiating (132) with all_106_0_29, all_106_1_30 yields: % 146.42/96.21 | (159) subactivity(all_106_0_29, tptp0) & subactivity(all_106_1_30, tptp0) & atocc(all_15_2_5, all_106_0_29) & atocc(all_0_1_1, all_106_1_30) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (159) yields: % 146.42/96.21 | (160) subactivity(all_106_0_29, tptp0) % 146.42/96.21 | (161) subactivity(all_106_1_30, tptp0) % 146.42/96.21 | (162) atocc(all_15_2_5, all_106_0_29) % 146.42/96.21 | (163) atocc(all_0_1_1, all_106_1_30) % 146.42/96.21 | % 146.42/96.21 | Instantiating (127) with all_108_0_31 yields: % 146.42/96.21 | (164) subactivity_occurrence(all_108_0_31, all_48_0_9) & root(all_108_0_31, tptp0) % 146.42/96.21 | % 146.42/96.21 | Applying alpha-rule on (164) yields: % 146.42/96.21 | (165) subactivity_occurrence(all_108_0_31, all_48_0_9) % 146.42/96.21 | (166) root(all_108_0_31, tptp0) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (54) with all_102_0_27, tptp4, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, all_102_0_27), occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.21 | (167) all_102_0_27 = tptp4 % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (54) with all_98_0_25, all_102_0_27, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, all_102_0_27), occurrence_of(all_15_1_4, all_98_0_25), yields: % 146.42/96.21 | (168) all_102_0_27 = all_98_0_25 % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (54) with all_88_0_20, all_102_0_27, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, all_102_0_27), occurrence_of(all_15_1_4, all_88_0_20), yields: % 146.42/96.21 | (169) all_102_0_27 = all_88_0_20 % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (54) with all_100_0_26, tptp3, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, all_100_0_26), occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.21 | (170) all_100_0_26 = tptp3 % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (54) with all_96_0_24, all_100_0_26, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, all_100_0_26), occurrence_of(all_15_2_5, all_96_0_24), yields: % 146.42/96.21 | (171) all_100_0_26 = all_96_0_24 % 146.42/96.21 | % 146.42/96.21 | Combining equations (169,168) yields a new equation: % 146.42/96.21 | (172) all_98_0_25 = all_88_0_20 % 146.42/96.21 | % 146.42/96.21 | Combining equations (167,168) yields a new equation: % 146.42/96.21 | (173) all_98_0_25 = tptp4 % 146.42/96.21 | % 146.42/96.21 | Combining equations (170,171) yields a new equation: % 146.42/96.21 | (174) all_96_0_24 = tptp3 % 146.42/96.21 | % 146.42/96.21 | Combining equations (173,172) yields a new equation: % 146.42/96.21 | (175) all_88_0_20 = tptp4 % 146.42/96.21 | % 146.42/96.21 | Combining equations (174,171) yields a new equation: % 146.42/96.21 | (170) all_100_0_26 = tptp3 % 146.42/96.21 | % 146.42/96.21 | From (170) and (153) follows: % 146.42/96.21 | (39) atomic(tptp3) % 146.42/96.21 | % 146.42/96.21 | From (175) and (143) follows: % 146.42/96.21 | (5) atomic(tptp4) % 146.42/96.21 | % 146.42/96.21 | From (175) and (144) follows: % 146.42/96.21 | (74) occurrence_of(all_15_1_4, tptp4) % 146.42/96.21 | % 146.42/96.21 | From (174) and (147) follows: % 146.42/96.21 | (71) occurrence_of(all_15_2_5, tptp3) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (67) with all_52_0_12 and discharging atoms activity_occurrence(all_52_0_12), yields: % 146.42/96.21 | (181) ? [v0] : (activity(v0) & occurrence_of(all_52_0_12, v0)) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (67) with all_48_0_9 and discharging atoms activity_occurrence(all_48_0_9), yields: % 146.42/96.21 | (182) ? [v0] : (activity(v0) & occurrence_of(all_48_0_9, v0)) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (56) with tptp4, tptp4, all_15_1_4 and discharging atoms subactivity(tptp4, tptp4), atomic(tptp4), occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.21 | (183) atocc(all_15_1_4, tptp4) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (56) with tptp3, tptp3, all_15_2_5 and discharging atoms subactivity(tptp3, tptp3), atomic(tptp3), occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.21 | (184) atocc(all_15_2_5, tptp3) % 146.42/96.21 | % 146.42/96.21 | Instantiating formula (52) with all_106_0_29, all_15_2_5 and discharging atoms atocc(all_15_2_5, all_106_0_29), yields: % 146.42/96.21 | (185) ? [v0] : (subactivity(all_106_0_29, v0) & atomic(v0) & occurrence_of(all_15_2_5, v0)) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (52) with all_84_1_18, all_15_2_5 and discharging atoms atocc(all_15_2_5, all_84_1_18), yields: % 146.42/96.22 | (186) ? [v0] : (subactivity(all_84_1_18, v0) & atomic(v0) & occurrence_of(all_15_2_5, v0)) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (55) with tptp0, all_48_0_9, all_108_0_31 and discharging atoms subactivity_occurrence(all_108_0_31, all_48_0_9), root(all_108_0_31, tptp0), occurrence_of(all_48_0_9, tptp0), yields: % 146.42/96.22 | (187) root_occ(all_108_0_31, all_48_0_9) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (55) with tptp0, all_52_0_12, all_86_0_19 and discharging atoms subactivity_occurrence(all_86_0_19, all_52_0_12), root(all_86_0_19, tptp0), occurrence_of(all_52_0_12, tptp0), yields: % 146.42/96.22 | (188) root_occ(all_86_0_19, all_52_0_12) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (30) with all_15_1_4, all_15_1_4 and discharging atoms legal(all_15_1_4), yields: % 146.42/96.22 | (189) ~ earlier(all_15_1_4, all_15_1_4) | precedes(all_15_1_4, all_15_1_4) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (60) with all_0_1_1, tptp0, all_15_0_3 and discharging atoms min_precedes(all_0_1_1, all_15_0_3, tptp0), yields: % 146.42/96.22 | (190) leaf(all_15_0_3, tptp0) | ? [v0] : min_precedes(all_15_0_3, v0, tptp0) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (60) with all_0_1_1, tptp0, all_15_1_4 and discharging atoms min_precedes(all_0_1_1, all_15_1_4, tptp0), yields: % 146.42/96.22 | (191) leaf(all_15_1_4, tptp0) | ? [v0] : min_precedes(all_15_1_4, v0, tptp0) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (2) with all_15_1_4, all_0_1_1, tptp0 and discharging atoms min_precedes(all_0_1_1, all_15_1_4, tptp0), yields: % 146.42/96.22 | (192) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_15_1_4, v1) & atocc(all_0_1_1, v0)) % 146.42/96.22 | % 146.42/96.22 | Instantiating (192) with all_146_0_35, all_146_1_36 yields: % 146.42/96.22 | (193) subactivity(all_146_0_35, tptp0) & subactivity(all_146_1_36, tptp0) & atocc(all_15_1_4, all_146_0_35) & atocc(all_0_1_1, all_146_1_36) % 146.42/96.22 | % 146.42/96.22 | Applying alpha-rule on (193) yields: % 146.42/96.22 | (194) subactivity(all_146_0_35, tptp0) % 146.42/96.22 | (195) subactivity(all_146_1_36, tptp0) % 146.42/96.22 | (196) atocc(all_15_1_4, all_146_0_35) % 146.42/96.22 | (197) atocc(all_0_1_1, all_146_1_36) % 146.42/96.22 | % 146.42/96.22 | Instantiating (182) with all_148_0_37 yields: % 146.42/96.22 | (198) activity(all_148_0_37) & occurrence_of(all_48_0_9, all_148_0_37) % 146.42/96.22 | % 146.42/96.22 | Applying alpha-rule on (198) yields: % 146.42/96.22 | (199) activity(all_148_0_37) % 146.42/96.22 | (200) occurrence_of(all_48_0_9, all_148_0_37) % 146.42/96.22 | % 146.42/96.22 | Instantiating (186) with all_158_0_42 yields: % 146.42/96.22 | (201) subactivity(all_84_1_18, all_158_0_42) & atomic(all_158_0_42) & occurrence_of(all_15_2_5, all_158_0_42) % 146.42/96.22 | % 146.42/96.22 | Applying alpha-rule on (201) yields: % 146.42/96.22 | (202) subactivity(all_84_1_18, all_158_0_42) % 146.42/96.22 | (203) atomic(all_158_0_42) % 146.42/96.22 | (204) occurrence_of(all_15_2_5, all_158_0_42) % 146.42/96.22 | % 146.42/96.22 | Instantiating (181) with all_160_0_43 yields: % 146.42/96.22 | (205) activity(all_160_0_43) & occurrence_of(all_52_0_12, all_160_0_43) % 146.42/96.22 | % 146.42/96.22 | Applying alpha-rule on (205) yields: % 146.42/96.22 | (206) activity(all_160_0_43) % 146.42/96.22 | (207) occurrence_of(all_52_0_12, all_160_0_43) % 146.42/96.22 | % 146.42/96.22 | Instantiating (185) with all_162_0_44 yields: % 146.42/96.22 | (208) subactivity(all_106_0_29, all_162_0_44) & atomic(all_162_0_44) & occurrence_of(all_15_2_5, all_162_0_44) % 146.42/96.22 | % 146.42/96.22 | Applying alpha-rule on (208) yields: % 146.42/96.22 | (209) subactivity(all_106_0_29, all_162_0_44) % 146.42/96.22 | (210) atomic(all_162_0_44) % 146.42/96.22 | (211) occurrence_of(all_15_2_5, all_162_0_44) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (54) with all_160_0_43, tptp0, all_52_0_12 and discharging atoms occurrence_of(all_52_0_12, all_160_0_43), occurrence_of(all_52_0_12, tptp0), yields: % 146.42/96.22 | (212) all_160_0_43 = tptp0 % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (54) with all_148_0_37, tptp0, all_48_0_9 and discharging atoms occurrence_of(all_48_0_9, all_148_0_37), occurrence_of(all_48_0_9, tptp0), yields: % 146.42/96.22 | (213) all_148_0_37 = tptp0 % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (54) with all_162_0_44, tptp3, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, all_162_0_44), occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.22 | (214) all_162_0_44 = tptp3 % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (54) with all_158_0_42, all_162_0_44, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, all_162_0_44), occurrence_of(all_15_2_5, all_158_0_42), yields: % 146.42/96.22 | (215) all_162_0_44 = all_158_0_42 % 146.42/96.22 | % 146.42/96.22 | Combining equations (214,215) yields a new equation: % 146.42/96.22 | (216) all_158_0_42 = tptp3 % 146.42/96.22 | % 146.42/96.22 | From (212) and (207) follows: % 146.42/96.22 | (112) occurrence_of(all_52_0_12, tptp0) % 146.42/96.22 | % 146.42/96.22 | From (213) and (200) follows: % 146.42/96.22 | (103) occurrence_of(all_48_0_9, tptp0) % 146.42/96.22 | % 146.42/96.22 | From (216) and (204) follows: % 146.42/96.22 | (71) occurrence_of(all_15_2_5, tptp3) % 146.42/96.22 | % 146.42/96.22 +-Applying beta-rule and splitting (190), into two cases. % 146.42/96.22 |-Branch one: % 146.42/96.22 | (220) leaf(all_15_0_3, tptp0) % 146.42/96.22 | % 146.42/96.22 +-Applying beta-rule and splitting (89), into two cases. % 146.42/96.22 |-Branch one: % 146.42/96.22 | (221) next_subocc(all_15_1_4, all_15_0_3, tptp0) % 146.42/96.22 | % 146.42/96.22 +-Applying beta-rule and splitting (94), into two cases. % 146.42/96.22 |-Branch one: % 146.42/96.22 | (222) next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.42/96.22 | % 146.42/96.22 +-Applying beta-rule and splitting (191), into two cases. % 146.42/96.22 |-Branch one: % 146.42/96.22 | (223) leaf(all_15_1_4, tptp0) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (59) with all_15_0_3, tptp0, all_15_1_4 and discharging atoms leaf(all_15_1_4, tptp0), min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.42/96.22 | (224) $false % 146.42/96.22 | % 146.42/96.22 |-The branch is then unsatisfiable % 146.42/96.22 |-Branch two: % 146.42/96.22 | (225) ~ leaf(all_15_1_4, tptp0) % 146.42/96.22 | (226) ? [v0] : min_precedes(all_15_1_4, v0, tptp0) % 146.42/96.22 | % 146.42/96.22 +-Applying beta-rule and splitting (191), into two cases. % 146.42/96.22 |-Branch one: % 146.42/96.22 | (223) leaf(all_15_1_4, tptp0) % 146.42/96.22 | % 146.42/96.22 | Using (223) and (225) yields: % 146.42/96.22 | (224) $false % 146.42/96.22 | % 146.42/96.22 |-The branch is then unsatisfiable % 146.42/96.22 |-Branch two: % 146.42/96.22 | (225) ~ leaf(all_15_1_4, tptp0) % 146.42/96.22 | (226) ? [v0] : min_precedes(all_15_1_4, v0, tptp0) % 146.42/96.22 | % 146.42/96.22 | Instantiating (226) with all_248_0_5487 yields: % 146.42/96.22 | (231) min_precedes(all_15_1_4, all_248_0_5487, tptp0) % 146.42/96.22 | % 146.42/96.22 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_1_4, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_15_1_4, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.22 | (232) ~ min_precedes(all_15_1_4, all_15_1_4, tptp0) % 146.42/96.22 | % 146.42/96.22 | Using (231) and (232) yields: % 146.42/96.22 | (233) ~ (all_248_0_5487 = all_15_1_4) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (52) with all_146_0_35, all_15_1_4 and discharging atoms atocc(all_15_1_4, all_146_0_35), yields: % 146.42/96.23 | (234) ? [v0] : (subactivity(all_146_0_35, v0) & atomic(v0) & occurrence_of(all_15_1_4, v0)) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (52) with tptp4, all_15_1_4 and discharging atoms atocc(all_15_1_4, tptp4), yields: % 146.42/96.23 | (235) ? [v0] : (subactivity(tptp4, v0) & atomic(v0) & occurrence_of(all_15_1_4, v0)) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (52) with tptp3, all_15_2_5 and discharging atoms atocc(all_15_2_5, tptp3), yields: % 146.42/96.23 | (236) ? [v0] : (subactivity(tptp3, v0) & atomic(v0) & occurrence_of(all_15_2_5, v0)) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (16) with all_48_0_9, all_108_0_31 and discharging atoms root_occ(all_108_0_31, all_48_0_9), yields: % 146.42/96.23 | (237) ? [v0] : (subactivity_occurrence(all_108_0_31, all_48_0_9) & root(all_108_0_31, v0) & occurrence_of(all_48_0_9, v0)) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (43) with tptp0, all_248_0_5487, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_248_0_5487, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.23 | (238) min_precedes(all_15_2_5, all_248_0_5487, tptp0) % 146.42/96.23 | % 146.42/96.23 | Instantiating (236) with all_288_0_5493 yields: % 146.42/96.23 | (239) subactivity(tptp3, all_288_0_5493) & atomic(all_288_0_5493) & occurrence_of(all_15_2_5, all_288_0_5493) % 146.42/96.23 | % 146.42/96.23 | Applying alpha-rule on (239) yields: % 146.42/96.23 | (240) subactivity(tptp3, all_288_0_5493) % 146.42/96.23 | (241) atomic(all_288_0_5493) % 146.42/96.23 | (242) occurrence_of(all_15_2_5, all_288_0_5493) % 146.42/96.23 | % 146.42/96.23 | Instantiating (234) with all_314_0_5506 yields: % 146.42/96.23 | (243) subactivity(all_146_0_35, all_314_0_5506) & atomic(all_314_0_5506) & occurrence_of(all_15_1_4, all_314_0_5506) % 146.42/96.23 | % 146.42/96.23 | Applying alpha-rule on (243) yields: % 146.42/96.23 | (244) subactivity(all_146_0_35, all_314_0_5506) % 146.42/96.23 | (245) atomic(all_314_0_5506) % 146.42/96.23 | (246) occurrence_of(all_15_1_4, all_314_0_5506) % 146.42/96.23 | % 146.42/96.23 | Instantiating (235) with all_316_0_5507 yields: % 146.42/96.23 | (247) subactivity(tptp4, all_316_0_5507) & atomic(all_316_0_5507) & occurrence_of(all_15_1_4, all_316_0_5507) % 146.42/96.23 | % 146.42/96.23 | Applying alpha-rule on (247) yields: % 146.42/96.23 | (248) subactivity(tptp4, all_316_0_5507) % 146.42/96.23 | (249) atomic(all_316_0_5507) % 146.42/96.23 | (250) occurrence_of(all_15_1_4, all_316_0_5507) % 146.42/96.23 | % 146.42/96.23 | Instantiating (237) with all_342_0_5523 yields: % 146.42/96.23 | (251) subactivity_occurrence(all_108_0_31, all_48_0_9) & root(all_108_0_31, all_342_0_5523) & occurrence_of(all_48_0_9, all_342_0_5523) % 146.42/96.23 | % 146.42/96.23 | Applying alpha-rule on (251) yields: % 146.42/96.23 | (165) subactivity_occurrence(all_108_0_31, all_48_0_9) % 146.42/96.23 | (253) root(all_108_0_31, all_342_0_5523) % 146.42/96.23 | (254) occurrence_of(all_48_0_9, all_342_0_5523) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (54) with all_342_0_5523, tptp0, all_48_0_9 and discharging atoms occurrence_of(all_48_0_9, all_342_0_5523), occurrence_of(all_48_0_9, tptp0), yields: % 146.42/96.23 | (255) all_342_0_5523 = tptp0 % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (54) with all_316_0_5507, tptp4, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, all_316_0_5507), occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.23 | (256) all_316_0_5507 = tptp4 % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (54) with all_314_0_5506, all_316_0_5507, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, all_316_0_5507), occurrence_of(all_15_1_4, all_314_0_5506), yields: % 146.42/96.23 | (257) all_316_0_5507 = all_314_0_5506 % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (54) with all_288_0_5493, tptp3, all_15_2_5 and discharging atoms occurrence_of(all_15_2_5, all_288_0_5493), occurrence_of(all_15_2_5, tptp3), yields: % 146.42/96.23 | (258) all_288_0_5493 = tptp3 % 146.42/96.23 | % 146.42/96.23 | Using (242) and (78) yields: % 146.42/96.23 | (259) ~ (all_288_0_5493 = tptp4) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (45) with all_248_0_5487, tptp0, all_15_0_3, all_15_1_4 and discharging atoms next_subocc(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_1_4, all_248_0_5487, tptp0), yields: % 146.42/96.23 | (260) ~ min_precedes(all_248_0_5487, all_15_0_3, tptp0) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (75) with all_248_0_5487 and discharging atoms min_precedes(all_15_2_5, all_248_0_5487, tptp0), yields: % 146.42/96.23 | (261) all_248_0_5487 = all_15_0_3 | all_248_0_5487 = all_15_1_4 % 146.42/96.23 | % 146.42/96.23 | Combining equations (256,257) yields a new equation: % 146.42/96.23 | (262) all_314_0_5506 = tptp4 % 146.42/96.23 | % 146.42/96.23 | Equations (258) can reduce 259 to: % 146.42/96.23 | (263) ~ (tptp4 = tptp3) % 146.42/96.23 | % 146.42/96.23 | Simplifying 263 yields: % 146.42/96.23 | (27) ~ (tptp4 = tptp3) % 146.42/96.23 | % 146.42/96.23 | From (255) and (254) follows: % 146.42/96.23 | (103) occurrence_of(all_48_0_9, tptp0) % 146.42/96.23 | % 146.42/96.23 | From (262) and (246) follows: % 146.42/96.23 | (74) occurrence_of(all_15_1_4, tptp4) % 146.42/96.23 | % 146.42/96.23 +-Applying beta-rule and splitting (261), into two cases. % 146.42/96.23 |-Branch one: % 146.42/96.23 | (267) all_248_0_5487 = all_15_0_3 % 146.42/96.23 | % 146.42/96.23 | From (267) and (231) follows: % 146.42/96.23 | (70) min_precedes(all_15_1_4, all_15_0_3, tptp0) % 146.42/96.23 | % 146.42/96.23 | From (267) and (260) follows: % 146.42/96.23 | (269) ~ min_precedes(all_15_0_3, all_15_0_3, tptp0) % 146.42/96.23 | % 146.42/96.23 +-Applying beta-rule and splitting (129), into two cases. % 146.42/96.23 |-Branch one: % 146.42/96.23 | (270) next_subocc(all_15_2_5, all_15_0_3, tptp0) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_0_3, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_15_0_3, tptp0), min_precedes(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.23 | (224) $false % 146.42/96.23 | % 146.42/96.23 |-The branch is then unsatisfiable % 146.42/96.23 |-Branch two: % 146.42/96.23 | (272) ~ next_subocc(all_15_2_5, all_15_0_3, tptp0) % 146.42/96.23 | (273) ? [v0] : (min_precedes(v0, all_15_0_3, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.42/96.23 | % 146.42/96.23 | Instantiating (273) with all_442_0_5527 yields: % 146.42/96.23 | (274) min_precedes(all_442_0_5527, all_15_0_3, tptp0) & min_precedes(all_15_2_5, all_442_0_5527, tptp0) % 146.42/96.23 | % 146.42/96.23 | Applying alpha-rule on (274) yields: % 146.42/96.23 | (275) min_precedes(all_442_0_5527, all_15_0_3, tptp0) % 146.42/96.23 | (276) min_precedes(all_15_2_5, all_442_0_5527, tptp0) % 146.42/96.23 | % 146.42/96.23 | Using (275) and (269) yields: % 146.42/96.23 | (277) ~ (all_442_0_5527 = all_15_0_3) % 146.42/96.23 | % 146.42/96.23 | Instantiating formula (75) with all_442_0_5527 and discharging atoms min_precedes(all_15_2_5, all_442_0_5527, tptp0), yields: % 146.42/96.23 | (278) all_442_0_5527 = all_15_0_3 | all_442_0_5527 = all_15_1_4 % 146.42/96.24 | % 146.42/96.24 +-Applying beta-rule and splitting (278), into two cases. % 146.42/96.24 |-Branch one: % 146.42/96.24 | (279) all_442_0_5527 = all_15_0_3 % 146.42/96.24 | % 146.42/96.24 | Equations (279) can reduce 277 to: % 146.42/96.24 | (280) $false % 146.42/96.24 | % 146.42/96.24 |-The branch is then unsatisfiable % 146.42/96.24 |-Branch two: % 146.42/96.24 | (277) ~ (all_442_0_5527 = all_15_0_3) % 146.42/96.24 | (282) all_442_0_5527 = all_15_1_4 % 146.42/96.24 | % 146.42/96.24 | From (282) and (275) follows: % 146.42/96.24 | (70) min_precedes(all_15_1_4, all_15_0_3, tptp0) % 146.42/96.24 | % 146.42/96.24 | From (282) and (276) follows: % 146.42/96.24 | (73) min_precedes(all_15_2_5, all_15_1_4, tptp0) % 146.42/96.24 | % 146.42/96.24 | Instantiating formula (54) with tptp3, tptp4, all_15_1_4 and discharging atoms occurrence_of(all_15_1_4, tptp4), yields: % 146.42/96.24 | (285) tptp4 = tptp3 | ~ occurrence_of(all_15_1_4, tptp3) % 146.42/96.24 | % 146.42/96.24 +-Applying beta-rule and splitting (285), into two cases. % 146.42/96.24 |-Branch one: % 146.42/96.24 | (286) ~ occurrence_of(all_15_1_4, tptp3) % 146.42/96.24 | % 146.42/96.24 +-Applying beta-rule and splitting (123), into two cases. % 146.42/96.24 |-Branch one: % 146.42/96.24 | (287) leaf_occ(all_15_2_5, all_48_0_9) % 146.42/96.24 | % 146.42/96.24 | Instantiating formula (6) with all_15_1_4, tptp0, all_15_2_5, all_48_0_9 and discharging atoms leaf_occ(all_15_2_5, all_48_0_9), occurrence_of(all_48_0_9, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.24 | (224) $false % 146.42/96.24 | % 146.42/96.24 |-The branch is then unsatisfiable % 146.42/96.24 |-Branch two: % 146.42/96.24 | (289) ~ leaf_occ(all_15_2_5, all_48_0_9) % 146.42/96.24 | (290) ? [v0] : ? [v1] : ? [v2] : (next_subocc(all_15_2_5, v0, tptp0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & min_precedes(v1, v2, tptp0) & min_precedes(v0, v1, tptp0) & ! [v3] : (v3 = v2 | v3 = v1 | ~ min_precedes(v0, v3, tptp0)) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 146.42/96.24 | % 146.42/96.24 | Instantiating (290) with all_591_0_5532, all_591_1_5533, all_591_2_5534 yields: % 146.42/96.24 | (291) next_subocc(all_15_2_5, all_591_2_5534, tptp0) & occurrence_of(all_591_1_5533, tptp4) & occurrence_of(all_591_2_5534, tptp3) & min_precedes(all_591_1_5533, all_591_0_5532, tptp0) & min_precedes(all_591_2_5534, all_591_1_5533, tptp0) & ! [v0] : (v0 = all_591_0_5532 | v0 = all_591_1_5533 | ~ min_precedes(all_591_2_5534, v0, tptp0)) & (occurrence_of(all_591_0_5532, tptp2) | occurrence_of(all_591_0_5532, tptp1)) % 146.42/96.24 | % 146.42/96.24 | Applying alpha-rule on (291) yields: % 146.42/96.24 | (292) occurrence_of(all_591_0_5532, tptp2) | occurrence_of(all_591_0_5532, tptp1) % 146.42/96.24 | (293) next_subocc(all_15_2_5, all_591_2_5534, tptp0) % 146.42/96.24 | (294) occurrence_of(all_591_1_5533, tptp4) % 146.42/96.24 | (295) min_precedes(all_591_1_5533, all_591_0_5532, tptp0) % 146.42/96.24 | (296) ! [v0] : (v0 = all_591_0_5532 | v0 = all_591_1_5533 | ~ min_precedes(all_591_2_5534, v0, tptp0)) % 146.42/96.24 | (297) min_precedes(all_591_2_5534, all_591_1_5533, tptp0) % 146.42/96.24 | (298) occurrence_of(all_591_2_5534, tptp3) % 146.42/96.24 | % 146.42/96.24 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_0_3, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.42/96.24 | (272) ~ next_subocc(all_15_2_5, all_15_0_3, tptp0) % 146.42/96.24 | % 146.42/96.24 | Using (293) and (272) yields: % 146.42/96.24 | (300) ~ (all_591_2_5534 = all_15_0_3) % 146.42/96.24 | % 146.42/96.24 | Using (298) and (286) yields: % 146.42/96.24 | (301) ~ (all_591_2_5534 = all_15_1_4) % 146.42/96.24 | % 146.42/96.24 | Instantiating formula (35) with tptp0, all_591_2_5534, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_591_2_5534, tptp0), yields: % 146.68/96.24 | (302) min_precedes(all_15_2_5, all_591_2_5534, tptp0) % 146.68/96.24 | % 146.68/96.24 | Instantiating formula (75) with all_591_2_5534 and discharging atoms min_precedes(all_15_2_5, all_591_2_5534, tptp0), yields: % 146.68/96.24 | (303) all_591_2_5534 = all_15_0_3 | all_591_2_5534 = all_15_1_4 % 146.68/96.24 | % 146.68/96.24 +-Applying beta-rule and splitting (303), into two cases. % 146.68/96.24 |-Branch one: % 146.68/96.24 | (304) all_591_2_5534 = all_15_0_3 % 146.68/96.24 | % 146.68/96.24 | Equations (304) can reduce 300 to: % 146.68/96.24 | (280) $false % 146.68/96.24 | % 146.68/96.24 |-The branch is then unsatisfiable % 146.68/96.24 |-Branch two: % 146.68/96.24 | (300) ~ (all_591_2_5534 = all_15_0_3) % 146.68/96.24 | (307) all_591_2_5534 = all_15_1_4 % 146.68/96.24 | % 146.68/96.24 | Equations (307) can reduce 301 to: % 146.68/96.24 | (280) $false % 146.68/96.24 | % 146.68/96.24 |-The branch is then unsatisfiable % 146.68/96.24 |-Branch two: % 146.68/96.24 | (309) occurrence_of(all_15_1_4, tptp3) % 146.68/96.24 | (310) tptp4 = tptp3 % 146.68/96.24 | % 146.68/96.24 | Equations (310) can reduce 27 to: % 146.68/96.24 | (280) $false % 146.68/96.24 | % 146.68/96.24 |-The branch is then unsatisfiable % 146.68/96.24 |-Branch two: % 146.68/96.24 | (312) ~ (all_248_0_5487 = all_15_0_3) % 146.68/96.24 | (313) all_248_0_5487 = all_15_1_4 % 146.68/96.24 | % 146.68/96.24 | Equations (313) can reduce 233 to: % 146.68/96.24 | (280) $false % 146.68/96.24 | % 146.68/96.24 |-The branch is then unsatisfiable % 146.68/96.24 |-Branch two: % 146.68/96.24 | (315) ~ next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.68/96.24 | (316) ? [v0] : (min_precedes(v0, all_15_1_4, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.68/96.24 | % 146.68/96.24 | Instantiating (316) with all_236_0_5927 yields: % 146.68/96.24 | (317) min_precedes(all_236_0_5927, all_15_1_4, tptp0) & min_precedes(all_15_2_5, all_236_0_5927, tptp0) % 146.68/96.24 | % 146.68/96.24 | Applying alpha-rule on (317) yields: % 146.68/96.25 | (318) min_precedes(all_236_0_5927, all_15_1_4, tptp0) % 146.68/96.25 | (319) min_precedes(all_15_2_5, all_236_0_5927, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_0_3, all_15_1_4 and discharging atoms next_subocc(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.68/96.25 | (232) ~ min_precedes(all_15_1_4, all_15_1_4, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (59) with all_15_1_4, tptp0, all_15_0_3 and discharging atoms leaf(all_15_0_3, tptp0), yields: % 146.68/96.25 | (321) ~ min_precedes(all_15_0_3, all_15_1_4, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (75) with all_236_0_5927 and discharging atoms min_precedes(all_15_2_5, all_236_0_5927, tptp0), yields: % 146.68/96.25 | (322) all_236_0_5927 = all_15_0_3 | all_236_0_5927 = all_15_1_4 % 146.68/96.25 | % 146.68/96.25 | Using (318) and (321) yields: % 146.68/96.25 | (323) ~ (all_236_0_5927 = all_15_0_3) % 146.68/96.25 | % 146.68/96.25 | Using (318) and (232) yields: % 146.68/96.25 | (324) ~ (all_236_0_5927 = all_15_1_4) % 146.68/96.25 | % 146.68/96.25 +-Applying beta-rule and splitting (322), into two cases. % 146.68/96.25 |-Branch one: % 146.68/96.25 | (325) all_236_0_5927 = all_15_0_3 % 146.68/96.25 | % 146.68/96.25 | Equations (325) can reduce 323 to: % 146.68/96.25 | (280) $false % 146.68/96.25 | % 146.68/96.25 |-The branch is then unsatisfiable % 146.68/96.25 |-Branch two: % 146.68/96.25 | (323) ~ (all_236_0_5927 = all_15_0_3) % 146.68/96.25 | (328) all_236_0_5927 = all_15_1_4 % 146.68/96.25 | % 146.68/96.25 | Equations (328) can reduce 324 to: % 146.68/96.25 | (280) $false % 146.68/96.25 | % 146.68/96.25 |-The branch is then unsatisfiable % 146.68/96.25 |-Branch two: % 146.68/96.25 | (330) ~ next_subocc(all_15_1_4, all_15_0_3, tptp0) % 146.68/96.25 | (331) ? [v0] : (min_precedes(v0, all_15_0_3, tptp0) & min_precedes(all_15_1_4, v0, tptp0)) % 146.68/96.25 | % 146.68/96.25 | Instantiating (331) with all_230_0_5928 yields: % 146.68/96.25 | (332) min_precedes(all_230_0_5928, all_15_0_3, tptp0) & min_precedes(all_15_1_4, all_230_0_5928, tptp0) % 146.68/96.25 | % 146.68/96.25 | Applying alpha-rule on (332) yields: % 146.68/96.25 | (333) min_precedes(all_230_0_5928, all_15_0_3, tptp0) % 146.68/96.25 | (334) min_precedes(all_15_1_4, all_230_0_5928, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (59) with all_15_0_3, tptp0, all_15_0_3 and discharging atoms leaf(all_15_0_3, tptp0), yields: % 146.68/96.25 | (269) ~ min_precedes(all_15_0_3, all_15_0_3, tptp0) % 146.68/96.25 | % 146.68/96.25 | Using (333) and (269) yields: % 146.68/96.25 | (336) ~ (all_230_0_5928 = all_15_0_3) % 146.68/96.25 | % 146.68/96.25 +-Applying beta-rule and splitting (94), into two cases. % 146.68/96.25 |-Branch one: % 146.68/96.25 | (222) next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_1_4, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_15_1_4, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.68/96.25 | (232) ~ min_precedes(all_15_1_4, all_15_1_4, tptp0) % 146.68/96.25 | % 146.68/96.25 | Using (334) and (232) yields: % 146.68/96.25 | (339) ~ (all_230_0_5928 = all_15_1_4) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (43) with tptp0, all_230_0_5928, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_230_0_5928, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.68/96.25 | (340) min_precedes(all_15_2_5, all_230_0_5928, tptp0) % 146.68/96.25 | % 146.68/96.25 | Instantiating formula (75) with all_230_0_5928 and discharging atoms min_precedes(all_15_2_5, all_230_0_5928, tptp0), yields: % 146.68/96.25 | (341) all_230_0_5928 = all_15_0_3 | all_230_0_5928 = all_15_1_4 % 146.68/96.25 | % 146.68/96.25 +-Applying beta-rule and splitting (341), into two cases. % 146.68/96.25 |-Branch one: % 146.68/96.25 | (342) all_230_0_5928 = all_15_0_3 % 146.68/96.25 | % 146.73/96.25 | Equations (342) can reduce 336 to: % 146.73/96.25 | (280) $false % 146.73/96.25 | % 146.73/96.25 |-The branch is then unsatisfiable % 146.73/96.25 |-Branch two: % 146.73/96.25 | (336) ~ (all_230_0_5928 = all_15_0_3) % 146.73/96.25 | (345) all_230_0_5928 = all_15_1_4 % 146.73/96.25 | % 146.73/96.25 | Equations (345) can reduce 339 to: % 146.73/96.25 | (280) $false % 146.73/96.25 | % 146.73/96.25 |-The branch is then unsatisfiable % 146.73/96.25 |-Branch two: % 146.73/96.25 | (315) ~ next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.73/96.25 | (316) ? [v0] : (min_precedes(v0, all_15_1_4, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.73/96.25 | % 146.73/96.25 | Instantiating (316) with all_246_0_5977 yields: % 146.73/96.25 | (349) min_precedes(all_246_0_5977, all_15_1_4, tptp0) & min_precedes(all_15_2_5, all_246_0_5977, tptp0) % 146.73/96.25 | % 146.73/96.25 | Applying alpha-rule on (349) yields: % 146.73/96.25 | (350) min_precedes(all_246_0_5977, all_15_1_4, tptp0) % 146.73/96.25 | (351) min_precedes(all_15_2_5, all_246_0_5977, tptp0) % 146.73/96.25 | % 146.73/96.25 | Instantiating formula (59) with all_15_1_4, tptp0, all_15_0_3 and discharging atoms leaf(all_15_0_3, tptp0), yields: % 146.73/96.25 | (321) ~ min_precedes(all_15_0_3, all_15_1_4, tptp0) % 146.73/96.25 | % 146.73/96.25 | Instantiating formula (75) with all_246_0_5977 and discharging atoms min_precedes(all_15_2_5, all_246_0_5977, tptp0), yields: % 146.73/96.25 | (353) all_246_0_5977 = all_15_0_3 | all_246_0_5977 = all_15_1_4 % 146.73/96.25 | % 146.73/96.25 | Using (350) and (321) yields: % 146.73/96.25 | (354) ~ (all_246_0_5977 = all_15_0_3) % 146.73/96.25 | % 146.73/96.25 +-Applying beta-rule and splitting (353), into two cases. % 146.73/96.25 |-Branch one: % 146.73/96.25 | (355) all_246_0_5977 = all_15_0_3 % 146.73/96.25 | % 146.73/96.25 | Equations (355) can reduce 354 to: % 146.73/96.25 | (280) $false % 146.73/96.25 | % 146.73/96.25 |-The branch is then unsatisfiable % 146.73/96.25 |-Branch two: % 146.73/96.25 | (354) ~ (all_246_0_5977 = all_15_0_3) % 146.73/96.25 | (358) all_246_0_5977 = all_15_1_4 % 146.73/96.25 | % 146.73/96.25 | From (358) and (351) follows: % 146.73/96.25 | (73) min_precedes(all_15_2_5, all_15_1_4, tptp0) % 146.73/96.25 | % 146.73/96.25 | Instantiating formula (16) with all_52_0_12, all_86_0_19 and discharging atoms root_occ(all_86_0_19, all_52_0_12), yields: % 146.73/96.26 | (360) ? [v0] : (subactivity_occurrence(all_86_0_19, all_52_0_12) & root(all_86_0_19, v0) & occurrence_of(all_52_0_12, v0)) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (43) with tptp0, all_230_0_5928, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_230_0_5928, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.73/96.26 | (340) min_precedes(all_15_2_5, all_230_0_5928, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating (360) with all_376_0_6025 yields: % 146.73/96.26 | (362) subactivity_occurrence(all_86_0_19, all_52_0_12) & root(all_86_0_19, all_376_0_6025) & occurrence_of(all_52_0_12, all_376_0_6025) % 146.73/96.26 | % 146.73/96.26 | Applying alpha-rule on (362) yields: % 146.73/96.26 | (139) subactivity_occurrence(all_86_0_19, all_52_0_12) % 146.73/96.26 | (364) root(all_86_0_19, all_376_0_6025) % 146.73/96.26 | (365) occurrence_of(all_52_0_12, all_376_0_6025) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (54) with all_376_0_6025, tptp0, all_52_0_12 and discharging atoms occurrence_of(all_52_0_12, all_376_0_6025), occurrence_of(all_52_0_12, tptp0), yields: % 146.73/96.26 | (366) all_376_0_6025 = tptp0 % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (75) with all_230_0_5928 and discharging atoms min_precedes(all_15_2_5, all_230_0_5928, tptp0), yields: % 146.73/96.26 | (341) all_230_0_5928 = all_15_0_3 | all_230_0_5928 = all_15_1_4 % 146.73/96.26 | % 146.73/96.26 | From (366) and (365) follows: % 146.73/96.26 | (112) occurrence_of(all_52_0_12, tptp0) % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (341), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (342) all_230_0_5928 = all_15_0_3 % 146.73/96.26 | % 146.73/96.26 | Equations (342) can reduce 336 to: % 146.73/96.26 | (280) $false % 146.73/96.26 | % 146.73/96.26 |-The branch is then unsatisfiable % 146.73/96.26 |-Branch two: % 146.73/96.26 | (336) ~ (all_230_0_5928 = all_15_0_3) % 146.73/96.26 | (345) all_230_0_5928 = all_15_1_4 % 146.73/96.26 | % 146.73/96.26 | From (345) and (334) follows: % 146.73/96.26 | (373) min_precedes(all_15_1_4, all_15_1_4, tptp0) % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (122), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (374) leaf_occ(all_15_1_4, all_52_0_12) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (6) with all_15_1_4, tptp0, all_15_1_4, all_52_0_12 and discharging atoms leaf_occ(all_15_1_4, all_52_0_12), occurrence_of(all_52_0_12, tptp0), min_precedes(all_15_1_4, all_15_1_4, tptp0), yields: % 146.73/96.26 | (224) $false % 146.73/96.26 | % 146.73/96.26 |-The branch is then unsatisfiable % 146.73/96.26 |-Branch two: % 146.73/96.26 | (376) ~ leaf_occ(all_15_1_4, all_52_0_12) % 146.73/96.26 | (377) ? [v0] : ? [v1] : ? [v2] : (next_subocc(all_15_1_4, v0, tptp0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & min_precedes(v1, v2, tptp0) & min_precedes(v0, v1, tptp0) & ! [v3] : (v3 = v2 | v3 = v1 | ~ min_precedes(v0, v3, tptp0)) & (occurrence_of(v2, tptp2) | occurrence_of(v2, tptp1))) % 146.73/96.26 | % 146.73/96.26 | Instantiating (377) with all_518_0_6033, all_518_1_6034, all_518_2_6035 yields: % 146.73/96.26 | (378) next_subocc(all_15_1_4, all_518_2_6035, tptp0) & occurrence_of(all_518_1_6034, tptp4) & occurrence_of(all_518_2_6035, tptp3) & min_precedes(all_518_1_6034, all_518_0_6033, tptp0) & min_precedes(all_518_2_6035, all_518_1_6034, tptp0) & ! [v0] : (v0 = all_518_0_6033 | v0 = all_518_1_6034 | ~ min_precedes(all_518_2_6035, v0, tptp0)) & (occurrence_of(all_518_0_6033, tptp2) | occurrence_of(all_518_0_6033, tptp1)) % 146.73/96.26 | % 146.73/96.26 | Applying alpha-rule on (378) yields: % 146.73/96.26 | (379) min_precedes(all_518_1_6034, all_518_0_6033, tptp0) % 146.73/96.26 | (380) ! [v0] : (v0 = all_518_0_6033 | v0 = all_518_1_6034 | ~ min_precedes(all_518_2_6035, v0, tptp0)) % 146.73/96.26 | (381) next_subocc(all_15_1_4, all_518_2_6035, tptp0) % 146.73/96.26 | (382) min_precedes(all_518_2_6035, all_518_1_6034, tptp0) % 146.73/96.26 | (383) occurrence_of(all_518_1_6034, tptp4) % 146.73/96.26 | (384) occurrence_of(all_518_0_6033, tptp2) | occurrence_of(all_518_0_6033, tptp1) % 146.73/96.26 | (385) occurrence_of(all_518_2_6035, tptp3) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (45) with all_15_1_4, tptp0, all_518_2_6035, all_15_1_4 and discharging atoms next_subocc(all_15_1_4, all_518_2_6035, tptp0), min_precedes(all_15_1_4, all_15_1_4, tptp0), yields: % 146.73/96.26 | (386) ~ min_precedes(all_15_1_4, all_518_2_6035, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (35) with tptp0, all_518_2_6035, all_15_1_4 and discharging atoms next_subocc(all_15_1_4, all_518_2_6035, tptp0), ~ min_precedes(all_15_1_4, all_518_2_6035, tptp0), yields: % 146.73/96.26 | (224) $false % 146.73/96.26 | % 146.73/96.26 |-The branch is then unsatisfiable % 146.73/96.26 |-Branch two: % 146.73/96.26 | (388) ~ leaf(all_15_0_3, tptp0) % 146.73/96.26 | (389) ? [v0] : min_precedes(all_15_0_3, v0, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating (389) with all_224_0_6060 yields: % 146.73/96.26 | (390) min_precedes(all_15_0_3, all_224_0_6060, tptp0) % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (94), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (222) next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (45) with all_15_0_3, tptp0, all_15_1_4, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_15_1_4, tptp0), min_precedes(all_15_2_5, all_15_0_3, tptp0), yields: % 146.73/96.26 | (321) ~ min_precedes(all_15_0_3, all_15_1_4, tptp0) % 146.73/96.26 | % 146.73/96.26 | Using (390) and (321) yields: % 146.73/96.26 | (393) ~ (all_224_0_6060 = all_15_1_4) % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (89), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (221) next_subocc(all_15_1_4, all_15_0_3, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (45) with all_15_0_3, tptp0, all_15_0_3, all_15_1_4 and discharging atoms next_subocc(all_15_1_4, all_15_0_3, tptp0), min_precedes(all_15_1_4, all_15_0_3, tptp0), yields: % 146.73/96.26 | (269) ~ min_precedes(all_15_0_3, all_15_0_3, tptp0) % 146.73/96.26 | % 146.73/96.26 | Using (390) and (269) yields: % 146.73/96.26 | (396) ~ (all_224_0_6060 = all_15_0_3) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (43) with tptp0, all_224_0_6060, all_15_0_3, all_15_2_5 and discharging atoms min_precedes(all_15_0_3, all_224_0_6060, tptp0), min_precedes(all_15_2_5, all_15_0_3, tptp0), yields: % 146.73/96.26 | (397) min_precedes(all_15_2_5, all_224_0_6060, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (75) with all_224_0_6060 and discharging atoms min_precedes(all_15_2_5, all_224_0_6060, tptp0), yields: % 146.73/96.26 | (398) all_224_0_6060 = all_15_0_3 | all_224_0_6060 = all_15_1_4 % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (398), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (399) all_224_0_6060 = all_15_0_3 % 146.73/96.26 | % 146.73/96.26 | Equations (399) can reduce 396 to: % 146.73/96.26 | (280) $false % 146.73/96.26 | % 146.73/96.26 |-The branch is then unsatisfiable % 146.73/96.26 |-Branch two: % 146.73/96.26 | (396) ~ (all_224_0_6060 = all_15_0_3) % 146.73/96.26 | (402) all_224_0_6060 = all_15_1_4 % 146.73/96.26 | % 146.73/96.26 | Equations (402) can reduce 393 to: % 146.73/96.26 | (280) $false % 146.73/96.26 | % 146.73/96.26 |-The branch is then unsatisfiable % 146.73/96.26 |-Branch two: % 146.73/96.26 | (330) ~ next_subocc(all_15_1_4, all_15_0_3, tptp0) % 146.73/96.26 | (331) ? [v0] : (min_precedes(v0, all_15_0_3, tptp0) & min_precedes(all_15_1_4, v0, tptp0)) % 146.73/96.26 | % 146.73/96.26 | Instantiating (331) with all_265_0_6111 yields: % 146.73/96.26 | (406) min_precedes(all_265_0_6111, all_15_0_3, tptp0) & min_precedes(all_15_1_4, all_265_0_6111, tptp0) % 146.73/96.26 | % 146.73/96.26 | Applying alpha-rule on (406) yields: % 146.73/96.26 | (407) min_precedes(all_265_0_6111, all_15_0_3, tptp0) % 146.73/96.26 | (408) min_precedes(all_15_1_4, all_265_0_6111, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (45) with all_15_1_4, tptp0, all_15_1_4, all_15_2_5 and discharging atoms next_subocc(all_15_2_5, all_15_1_4, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.73/96.26 | (232) ~ min_precedes(all_15_1_4, all_15_1_4, tptp0) % 146.73/96.26 | % 146.73/96.26 | Using (408) and (232) yields: % 146.73/96.26 | (410) ~ (all_265_0_6111 = all_15_1_4) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (38) with tptp0, all_15_0_3, all_265_0_6111 and discharging atoms min_precedes(all_265_0_6111, all_15_0_3, tptp0), yields: % 146.73/96.26 | (411) precedes(all_265_0_6111, all_15_0_3) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (43) with tptp0, all_265_0_6111, all_15_1_4, all_15_2_5 and discharging atoms min_precedes(all_15_1_4, all_265_0_6111, tptp0), min_precedes(all_15_2_5, all_15_1_4, tptp0), yields: % 146.73/96.26 | (412) min_precedes(all_15_2_5, all_265_0_6111, tptp0) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (75) with all_265_0_6111 and discharging atoms min_precedes(all_15_2_5, all_265_0_6111, tptp0), yields: % 146.73/96.26 | (413) all_265_0_6111 = all_15_0_3 | all_265_0_6111 = all_15_1_4 % 146.73/96.26 | % 146.73/96.26 +-Applying beta-rule and splitting (413), into two cases. % 146.73/96.26 |-Branch one: % 146.73/96.26 | (414) all_265_0_6111 = all_15_0_3 % 146.73/96.26 | % 146.73/96.26 | From (414) and (411) follows: % 146.73/96.26 | (415) precedes(all_15_0_3, all_15_0_3) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (17) with all_15_0_3, all_15_0_3 and discharging atoms precedes(all_15_0_3, all_15_0_3), yields: % 146.73/96.26 | (416) earlier(all_15_0_3, all_15_0_3) % 146.73/96.26 | % 146.73/96.26 | Instantiating formula (47) with all_15_0_3, all_15_0_3 and discharging atoms earlier(all_15_0_3, all_15_0_3), yields: % 146.73/96.26 | (224) $false % 146.73/96.26 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 |-Branch two: % 146.73/96.27 | (418) ~ (all_265_0_6111 = all_15_0_3) % 146.73/96.27 | (419) all_265_0_6111 = all_15_1_4 % 146.73/96.27 | % 146.73/96.27 | Equations (419) can reduce 410 to: % 146.73/96.27 | (280) $false % 146.73/96.27 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 |-Branch two: % 146.73/96.27 | (315) ~ next_subocc(all_15_2_5, all_15_1_4, tptp0) % 146.73/96.27 | (316) ? [v0] : (min_precedes(v0, all_15_1_4, tptp0) & min_precedes(all_15_2_5, v0, tptp0)) % 146.73/96.27 | % 146.73/96.27 | Instantiating (316) with all_251_0_6909 yields: % 146.73/96.27 | (423) min_precedes(all_251_0_6909, all_15_1_4, tptp0) & min_precedes(all_15_2_5, all_251_0_6909, tptp0) % 146.73/96.27 | % 146.73/96.27 | Applying alpha-rule on (423) yields: % 146.73/96.27 | (424) min_precedes(all_251_0_6909, all_15_1_4, tptp0) % 146.73/96.27 | (425) min_precedes(all_15_2_5, all_251_0_6909, tptp0) % 146.73/96.27 | % 146.73/96.27 | Instantiating formula (75) with all_251_0_6909 and discharging atoms min_precedes(all_15_2_5, all_251_0_6909, tptp0), yields: % 146.73/96.27 | (426) all_251_0_6909 = all_15_0_3 | all_251_0_6909 = all_15_1_4 % 146.73/96.27 | % 146.73/96.27 | Instantiating formula (38) with tptp0, all_15_1_4, all_251_0_6909 and discharging atoms min_precedes(all_251_0_6909, all_15_1_4, tptp0), yields: % 146.73/96.27 | (427) precedes(all_251_0_6909, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 +-Applying beta-rule and splitting (189), into two cases. % 146.73/96.27 |-Branch one: % 146.73/96.27 | (428) ~ earlier(all_15_1_4, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 | Instantiating formula (17) with all_15_1_4, all_251_0_6909 and discharging atoms precedes(all_251_0_6909, all_15_1_4), yields: % 146.73/96.27 | (429) earlier(all_251_0_6909, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 | Instantiating formula (47) with all_15_0_3, all_15_1_4 and discharging atoms earlier(all_15_1_4, all_15_0_3), yields: % 146.73/96.27 | (430) ~ earlier(all_15_0_3, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 | Using (429) and (428) yields: % 146.73/96.27 | (431) ~ (all_251_0_6909 = all_15_1_4) % 146.73/96.27 | % 146.73/96.27 +-Applying beta-rule and splitting (426), into two cases. % 146.73/96.27 |-Branch one: % 146.73/96.27 | (432) all_251_0_6909 = all_15_0_3 % 146.73/96.27 | % 146.73/96.27 | From (432) and (429) follows: % 146.73/96.27 | (433) earlier(all_15_0_3, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 | Using (433) and (430) yields: % 146.73/96.27 | (224) $false % 146.73/96.27 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 |-Branch two: % 146.73/96.27 | (435) ~ (all_251_0_6909 = all_15_0_3) % 146.73/96.27 | (436) all_251_0_6909 = all_15_1_4 % 146.73/96.27 | % 146.73/96.27 | Equations (436) can reduce 431 to: % 146.73/96.27 | (280) $false % 146.73/96.27 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 |-Branch two: % 146.73/96.27 | (438) earlier(all_15_1_4, all_15_1_4) % 146.73/96.27 | (439) precedes(all_15_1_4, all_15_1_4) % 146.73/96.27 | % 146.73/96.27 | Instantiating formula (47) with all_15_1_4, all_15_1_4 and discharging atoms earlier(all_15_1_4, all_15_1_4), yields: % 146.73/96.27 | (224) $false % 146.73/96.27 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 |-Branch two: % 146.73/96.27 | (441) occurrence_of(all_15_2_5, tptp4) % 146.73/96.27 | (310) tptp4 = tptp3 % 146.73/96.27 | % 146.73/96.27 | Equations (310) can reduce 27 to: % 146.73/96.27 | (280) $false % 146.73/96.27 | % 146.73/96.27 |-The branch is then unsatisfiable % 146.73/96.27 % SZS output end Proof for theBenchmark % 146.73/96.27 % 146.73/96.27 95659ms %------------------------------------------------------------------------------