%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO003+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.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 6.88s 2.29s % Output : Proof 13.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO003+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n025.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 02:18:38 EDT 2022 % 0.13/0.34 % CPUTime : % 0.53/0.58 ____ _ % 0.53/0.58 ___ / __ \_____(_)___ ________ __________ % 0.53/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.53/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.53/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.53/0.58 % 0.53/0.58 A Theorem Prover for First-Order Logic % 0.53/0.58 (ePrincess v.1.0) % 0.53/0.58 % 0.53/0.58 (c) Philipp Rümmer, 2009-2015 % 0.53/0.58 (c) Peter Backeman, 2014-2015 % 0.53/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.53/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.53/0.58 Bug reports to peter@backeman.se % 0.53/0.58 % 0.53/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.53/0.58 % 0.53/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.76/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.87/1.01 Prover 0: Preprocessing ... % 3.14/1.35 Prover 0: Constructing countermodel ... % 6.88/2.28 Prover 0: proved (1649ms) % 6.88/2.29 % 6.88/2.29 No countermodel exists, formula is valid % 6.88/2.29 % SZS status Theorem for theBenchmark % 6.88/2.29 % 6.88/2.29 Generating proof ... found it (size 100) % 13.19/3.75 % 13.19/3.75 % SZS output start Proof for theBenchmark % 13.19/3.75 Assumed formulas after preprocessing and simplification: % 13.19/3.75 | (0) ? [v0] : ( ~ (tptp1 = tptp2) & ~ (tptp1 = tptp3) & ~ (tptp1 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp3 = tptp4) & atomic(tptp1) & atomic(tptp2) & atomic(tptp3) & atomic(tptp4) & activity(tptp0) & occurrence_of(v0, tptp0) & ~ atomic(tptp0) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v3 | ~ leaf_occ(v5, v2) | ~ root_occ(v4, v2) | ~ subactivity_occurrence(v3, v2) | ~ min_precedes(v4, v3, v1) | ~ occurrence_of(v2, v1) | min_precedes(v3, v5, v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ leaf_occ(v5, v2) | ~ root_occ(v4, v2) | ~ subactivity_occurrence(v3, v2) | ~ min_precedes(v3, v5, v1) | ~ occurrence_of(v2, v1) | min_precedes(v4, v3, v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ subactivity_occurrence(v3, v5) | ~ subactivity_occurrence(v2, v5) | ~ next_subocc(v1, v3, v4) | ~ next_subocc(v1, v2, v4) | ~ occurrence_of(v5, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ leaf_occ(v4, v2) | ~ subactivity_occurrence(v3, v2) | ~ arboreal(v3) | ~ occurrence_of(v2, v1) | min_precedes(v3, v4, v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ root_occ(v4, v2) | ~ subactivity_occurrence(v3, v2) | ~ arboreal(v3) | ~ occurrence_of(v2, v1) | min_precedes(v4, v3, v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ subactivity_occurrence(v4, v2) | ~ subactivity_occurrence(v3, v2) | ~ arboreal(v4) | ~ arboreal(v3) | ~ occurrence_of(v2, v1) | min_precedes(v4, v3, v1) | min_precedes(v3, v4, v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ leaf_occ(v2, v1) | ~ root_occ(v3, v1) | ~ occurrence_of(v1, v4) | min_precedes(v3, v2, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ next_subocc(v3, v1, v4) | ~ next_subocc(v2, v1, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ leaf_occ(v2, v3) | ~ leaf_occ(v1, v3) | ~ occurrence_of(v3, v4) | atomic(v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ root_occ(v2, v3) | ~ root_occ(v1, v3) | ~ occurrence_of(v3, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ leaf_occ(v2, v1) | ~ min_precedes(v2, v4, v3) | ~ occurrence_of(v1, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ root_occ(v2, v1) | ~ min_precedes(v4, v2, v3) | ~ occurrence_of(v1, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v3, v4) | ~ occurrence_of(v4, v2) | ~ occurrence_of(v3, v1) | atomic(v1) | subactivity(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ subactivity_occurrence(v2, v4) | ~ min_precedes(v1, v2, v3) | ~ occurrence_of(v4, v3) | subactivity_occurrence(v1, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ next_subocc(v1, v2, v3) | ~ min_precedes(v4, v2, v3) | ~ min_precedes(v1, v4, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v3, v1, v4) | ~ min_precedes(v2, v1, v4) | ~ precedes(v2, v3) | min_precedes(v2, v3, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v1, v3, v4) | ~ min_precedes(v1, v2, v4) | ~ precedes(v2, v3) | min_precedes(v2, v3, v4)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ subactivity(v1, v2) | ~ occurrence_of(v4, v2) | ~ occurrence_of(v3, v1) | subactivity_occurrence(v3, v4) | ? [v5] : (subactivity_occurrence(v5, v4) & ~ subactivity_occurrence(v5, v3))) & ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ occurrence_of(v1, v3) | ~ occurrence_of(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ earlier(v3, v2) | ~ earlier(v1, v2) | earlier(v3, v1) | earlier(v1, v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | ~ subactivity_occurrence(v1, v2) | subactivity_occurrence(v1, v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v1, v2) | ~ leaf(v1, v3) | ~ occurrence_of(v2, v3) | leaf_occ(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v1, v2) | ~ root(v1, v3) | ~ occurrence_of(v2, v3) | root_occ(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v1, v2, v3) | min_precedes(v1, v2, v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v1, v2, v3) | arboreal(v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v1, v2, v3) | arboreal(v1)) & ! [v1] : ! [v2] : ! [v3] : ( ~ leaf(v1, v2) | ~ min_precedes(v1, v3, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ root(v2, v3) | ~ min_precedes(v1, v2, v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v3, v1, v2) | leaf(v1, v2) | ? [v4] : min_precedes(v1, v4, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v2, v3, v1) | ? [v4] : ? [v5] : (atocc(v3, v5) & atocc(v2, v4) & subactivity(v5, v1) & subactivity(v4, v1))) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v2, v3, v1) | ? [v4] : (subactivity_occurrence(v3, v4) & subactivity_occurrence(v2, v4) & occurrence_of(v4, v1))) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ atomic(v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | next_subocc(v1, v2, v3) | ? [v4] : (min_precedes(v4, v2, v3) & min_precedes(v1, v4, v3))) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | precedes(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | arboreal(v1)) & ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ? [v4] : (root(v4, v3) & min_precedes(v4, v2, v3))) & ! [v1] : ! [v2] : ! [v3] : ( ~ atomic(v3) | ~ subactivity(v2, v3) | ~ occurrence_of(v1, v3) | atocc(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ earlier(v2, v3) | ~ earlier(v1, v2) | earlier(v1, v3)) & ! [v1] : ! [v2] : ( ~ leaf_occ(v1, v2) | ? [v3] : (subactivity_occurrence(v1, v2) & leaf(v1, v3) & occurrence_of(v2, v3))) & ! [v1] : ! [v2] : ( ~ root_occ(v1, v2) | ~ occurrence_of(v2, tptp0) | ? [v3] : (next_subocc(v1, v3, tptp0) & occurrence_of(v3, tptp1))) & ! [v1] : ! [v2] : ( ~ root_occ(v1, v2) | ? [v3] : (subactivity_occurrence(v1, v2) & root(v1, v3) & occurrence_of(v2, v3))) & ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v1, v2) | activity_occurrence(v2)) & ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v1, v2) | activity_occurrence(v1)) & ! [v1] : ! [v2] : ( ~ leaf(v1, v2) | root(v1, v2) | ? [v3] : min_precedes(v3, v1, v2)) & ! [v1] : ! [v2] : ( ~ leaf(v1, v2) | atomic(v2) | ? [v3] : (leaf_occ(v1, v3) & occurrence_of(v3, v2))) & ! [v1] : ! [v2] : ( ~ root(v2, v1) | atomic(v1) | ? [v3] : (subactivity_occurrence(v2, v3) & occurrence_of(v3, v1))) & ! [v1] : ! [v2] : ( ~ root(v2, v1) | ? [v3] : (atocc(v2, v3) & subactivity(v3, v1))) & ! [v1] : ! [v2] : ( ~ root(v1, v2) | leaf(v1, v2) | ? [v3] : min_precedes(v1, v3, v2)) & ! [v1] : ! [v2] : ( ~ root(v1, v2) | legal(v1)) & ! [v1] : ! [v2] : ( ~ atocc(v1, v2) | ~ legal(v1) | root(v1, v2)) & ! [v1] : ! [v2] : ( ~ atocc(v1, v2) | ? [v3] : (atomic(v3) & subactivity(v2, v3) & occurrence_of(v1, v3))) & ! [v1] : ! [v2] : ( ~ precedes(v1, v2) | legal(v2)) & ! [v1] : ! [v2] : ( ~ precedes(v1, v2) | earlier(v1, v2)) & ! [v1] : ! [v2] : ( ~ legal(v2) | ~ earlier(v1, v2) | precedes(v1, v2)) & ! [v1] : ! [v2] : ( ~ legal(v1) | ~ earlier(v2, v1) | legal(v2)) & ! [v1] : ! [v2] : ( ~ atomic(v2) | ~ occurrence_of(v1, v2) | arboreal(v1)) & ! [v1] : ! [v2] : ( ~ arboreal(v1) | ~ occurrence_of(v1, v2) | atomic(v2)) & ! [v1] : ! [v2] : ( ~ earlier(v2, v1) | ~ earlier(v1, v2)) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | atomic(v1) | ? [v3] : (subactivity_occurrence(v3, v2) & root(v3, v1))) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | activity_occurrence(v2)) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | activity(v1)) & ! [v1] : ( ~ legal(v1) | arboreal(v1)) & ! [v1] : ( ~ activity_occurrence(v1) | ? [v2] : (activity(v2) & occurrence_of(v1, v2))) & ! [v1] : ( ~ activity(v1) | subactivity(v1, v1)) & ! [v1] : ( ~ occurrence_of(v1, tptp0) | ? [v2] : ? [v3] : (leaf_occ(v3, v1) & root_occ(v2, v1) & next_subocc(v2, v3, tptp0) & occurrence_of(v3, tptp3) & occurrence_of(v2, tptp4)))) % 13.43/3.78 | Instantiating (0) with all_0_0_0 yields: % 13.43/3.78 | (1) ~ (tptp1 = tptp2) & ~ (tptp1 = tptp3) & ~ (tptp1 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp3 = tptp4) & atomic(tptp1) & atomic(tptp2) & atomic(tptp3) & atomic(tptp4) & activity(tptp0) & occurrence_of(all_0_0_0, tptp0) & ~ atomic(tptp0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ min_precedes(v3, v2, v0) | ~ occurrence_of(v1, v0) | min_precedes(v2, v4, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ min_precedes(v2, v4, v0) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ subactivity_occurrence(v2, v4) | ~ subactivity_occurrence(v1, v4) | ~ next_subocc(v0, v2, v3) | ~ next_subocc(v0, v1, v3) | ~ occurrence_of(v4, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ leaf_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ subactivity_occurrence(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v3) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0) | min_precedes(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ leaf_occ(v1, v0) | ~ root_occ(v2, v0) | ~ occurrence_of(v0, v3) | min_precedes(v2, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ next_subocc(v2, v0, v3) | ~ next_subocc(v1, v0, v3)) & ! [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] : ( ~ leaf_occ(v1, v0) | ~ min_precedes(v1, v3, v2) | ~ occurrence_of(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ min_precedes(v3, v1, v2) | ~ occurrence_of(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | ~ occurrence_of(v3, v1) | ~ occurrence_of(v2, v0) | atomic(v0) | subactivity(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v1, v3) | ~ min_precedes(v0, v1, v2) | ~ occurrence_of(v3, v2) | subactivity_occurrence(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v2, v0, v3) | ~ min_precedes(v1, v0, v3) | ~ precedes(v1, v2) | min_precedes(v1, v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | ~ precedes(v1, v2) | min_precedes(v1, v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity(v0, v1) | ~ occurrence_of(v3, v1) | ~ occurrence_of(v2, v0) | subactivity_occurrence(v2, v3) | ? [v4] : (subactivity_occurrence(v4, v3) & ~ subactivity_occurrence(v4, v2))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ earlier(v2, v1) | ~ earlier(v0, v1) | earlier(v2, v0) | earlier(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v1, v2) | ~ subactivity_occurrence(v0, v1) | subactivity_occurrence(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ leaf(v0, v2) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, 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] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, 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] : (atocc(v2, v4) & atocc(v1, v3) & subactivity(v4, v0) & subactivity(v3, v0))) & ! [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) | ~ atomic(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) | arboreal(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ? [v3] : (root(v3, v2) & min_precedes(v3, v1, v2))) & ! [v0] : ! [v1] : ! [v2] : ( ~ atomic(v2) | ~ subactivity(v1, v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) & ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & leaf(v0, v2) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ~ occurrence_of(v1, tptp0) | ? [v2] : (next_subocc(v0, v2, tptp0) & occurrence_of(v2, tptp1))) & ! [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] : ( ~ 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] : ( ~ root(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v1, v2) & occurrence_of(v2, v0))) & ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (atocc(v1, v2) & subactivity(v2, v0))) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) & ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) & ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (atomic(v2) & subactivity(v1, v2) & occurrence_of(v0, v2))) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) & ! [v0] : ! [v1] : ( ~ legal(v0) | ~ earlier(v1, v0) | legal(v1)) & ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) & ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) & ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) & ! [v0] : ( ~ legal(v0) | arboreal(v0)) & ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) & ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) & ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : (leaf_occ(v2, v0) & root_occ(v1, v0) & next_subocc(v1, v2, tptp0) & occurrence_of(v2, tptp3) & occurrence_of(v1, tptp4))) % 13.43/3.80 | % 13.43/3.80 | Applying alpha-rule on (1) yields: % 13.43/3.80 | (2) atomic(tptp2) % 13.43/3.80 | (3) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v1, v2) | ~ subactivity_occurrence(v0, v1) | subactivity_occurrence(v0, v2)) % 13.43/3.80 | (4) ~ (tptp1 = tptp3) % 13.43/3.80 | (5) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 13.43/3.80 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 13.43/3.80 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ min_precedes(v1, v3, v2) | ~ occurrence_of(v0, v2)) % 13.43/3.80 | (8) occurrence_of(all_0_0_0, tptp0) % 13.43/3.80 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 13.43/3.80 | (10) atomic(tptp4) % 13.43/3.80 | (11) ! [v0] : ! [v1] : ( ~ root(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v1, v2) & occurrence_of(v2, v0))) % 13.43/3.80 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0)) % 13.43/3.80 | (13) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ earlier(v2, v1) | ~ earlier(v0, v1) | earlier(v2, v0) | earlier(v0, v2)) % 13.43/3.80 | (14) ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : (leaf_occ(v2, v0) & root_occ(v1, v0) & next_subocc(v1, v2, tptp0) & occurrence_of(v2, tptp3) & occurrence_of(v1, tptp4))) % 13.43/3.80 | (15) ~ atomic(tptp0) % 13.43/3.80 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 13.43/3.80 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v1, v3) | ~ min_precedes(v0, v1, v2) | ~ occurrence_of(v3, v2) | subactivity_occurrence(v0, v3)) % 13.43/3.80 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 13.43/3.80 | (19) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 13.43/3.80 | (20) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 13.43/3.80 | (21) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (atomic(v2) & subactivity(v1, v2) & occurrence_of(v0, v2))) % 13.43/3.80 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ min_precedes(v3, v1, v2) | ~ occurrence_of(v0, v2)) % 13.43/3.80 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ min_precedes(v3, v2, v0) | ~ occurrence_of(v1, v0) | min_precedes(v2, v4, v0)) % 13.43/3.80 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (atocc(v2, v4) & atocc(v1, v3) & subactivity(v4, v0) & subactivity(v3, v0))) % 13.43/3.80 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 13.43/3.80 | (26) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 13.43/3.80 | (27) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 13.43/3.80 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ? [v3] : (root(v3, v2) & min_precedes(v3, v1, v2))) % 13.43/3.80 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v0, v2, v3) | ~ min_precedes(v0, v1, v3) | ~ precedes(v1, v2) | min_precedes(v1, v2, v3)) % 13.43/3.80 | (30) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 13.43/3.80 | (31) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 13.43/3.80 | (32) ! [v0] : ! [v1] : ! [v2] : ( ~ atomic(v2) | ~ subactivity(v1, v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 13.43/3.80 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ leaf_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ arboreal(v2) | ~ occurrence_of(v1, v0) | min_precedes(v2, v3, v0)) % 13.43/3.80 | (34) atomic(tptp1) % 13.43/3.80 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity(v0, v1) | ~ occurrence_of(v3, v1) | ~ occurrence_of(v2, v0) | subactivity_occurrence(v2, v3) | ? [v4] : (subactivity_occurrence(v4, v3) & ~ subactivity_occurrence(v4, v2))) % 13.43/3.81 | (36) atomic(tptp3) % 13.43/3.81 | (37) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 13.43/3.81 | (38) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 13.43/3.81 | (39) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 13.43/3.81 | (40) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ leaf(v0, v2) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 13.43/3.81 | (41) ~ (tptp1 = tptp4) % 13.43/3.81 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ leaf_occ(v4, v1) | ~ root_occ(v3, v1) | ~ subactivity_occurrence(v2, v1) | ~ min_precedes(v2, v4, v0) | ~ occurrence_of(v1, v0) | min_precedes(v3, v2, v0)) % 13.43/3.81 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ leaf_occ(v1, v0) | ~ root_occ(v2, v0) | ~ occurrence_of(v0, v3) | min_precedes(v2, v1, v3)) % 13.43/3.81 | (44) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | ~ atomic(v2)) % 13.43/3.81 | (45) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 13.43/3.81 | (46) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 13.43/3.81 | (47) ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) % 13.43/3.81 | (48) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 13.43/3.81 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | arboreal(v0)) % 13.43/3.81 | (50) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (atocc(v1, v2) & subactivity(v2, v0))) % 13.43/3.81 | (51) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 13.43/3.81 | (52) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 13.43/3.81 | (53) activity(tptp0) % 13.43/3.81 | (54) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 13.43/3.81 | (55) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 13.43/3.81 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 13.43/3.81 | (57) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 13.43/3.81 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ next_subocc(v2, v0, v3) | ~ next_subocc(v1, v0, v3)) % 13.43/3.81 | (59) ~ (tptp1 = tptp2) % 13.43/3.81 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 13.43/3.81 | (61) ~ (tptp2 = tptp4) % 13.43/3.81 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 13.43/3.81 | (63) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 13.43/3.81 | (64) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) % 13.43/3.81 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ subactivity_occurrence(v2, v4) | ~ subactivity_occurrence(v1, v4) | ~ next_subocc(v0, v2, v3) | ~ next_subocc(v0, v1, v3) | ~ occurrence_of(v4, v3)) % 13.43/3.81 | (66) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 13.43/3.81 | (67) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ~ occurrence_of(v1, tptp0) | ? [v2] : (next_subocc(v0, v2, tptp0) & occurrence_of(v2, tptp1))) % 13.43/3.81 | (68) ~ (tptp2 = tptp3) % 13.43/3.81 | (69) ! [v0] : ! [v1] : ( ~ legal(v0) | ~ earlier(v1, v0) | legal(v1)) % 13.43/3.81 | (70) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & leaf(v0, v2) & occurrence_of(v1, v2))) % 13.43/3.81 | (71) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 13.43/3.81 | (72) ! [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)) % 13.43/3.81 | (73) ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) % 13.43/3.81 | (74) ~ (tptp3 = tptp4) % 13.43/3.81 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v2, v0, v3) | ~ min_precedes(v1, v0, v3) | ~ precedes(v1, v2) | min_precedes(v1, v2, v3)) % 13.43/3.82 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v2, v3) | ~ occurrence_of(v3, v1) | ~ occurrence_of(v2, v0) | atomic(v0) | subactivity(v0, v1)) % 13.43/3.82 | (77) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 13.43/3.82 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 13.43/3.82 | (79) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (14) with all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, tptp0), yields: % 13.43/3.82 | (80) ? [v0] : ? [v1] : (leaf_occ(v1, all_0_0_0) & root_occ(v0, all_0_0_0) & next_subocc(v0, v1, tptp0) & occurrence_of(v1, tptp3) & occurrence_of(v0, tptp4)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (55) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0), ~ atomic(tptp0), yields: % 13.43/3.82 | (81) ? [v0] : (subactivity_occurrence(v0, all_0_0_0) & root(v0, tptp0)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (66) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0), yields: % 13.43/3.82 | (82) activity_occurrence(all_0_0_0) % 13.43/3.82 | % 13.43/3.82 | Instantiating (81) with all_9_0_1 yields: % 13.43/3.82 | (83) subactivity_occurrence(all_9_0_1, all_0_0_0) & root(all_9_0_1, tptp0) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (83) yields: % 13.43/3.82 | (84) subactivity_occurrence(all_9_0_1, all_0_0_0) % 13.43/3.82 | (85) root(all_9_0_1, tptp0) % 13.43/3.82 | % 13.43/3.82 | Instantiating (80) with all_11_0_2, all_11_1_3 yields: % 13.43/3.82 | (86) leaf_occ(all_11_0_2, all_0_0_0) & root_occ(all_11_1_3, all_0_0_0) & next_subocc(all_11_1_3, all_11_0_2, tptp0) & occurrence_of(all_11_0_2, tptp3) & occurrence_of(all_11_1_3, tptp4) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (86) yields: % 13.43/3.82 | (87) root_occ(all_11_1_3, all_0_0_0) % 13.43/3.82 | (88) next_subocc(all_11_1_3, all_11_0_2, tptp0) % 13.43/3.82 | (89) occurrence_of(all_11_0_2, tptp3) % 13.43/3.82 | (90) leaf_occ(all_11_0_2, all_0_0_0) % 13.43/3.82 | (91) occurrence_of(all_11_1_3, tptp4) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (67) with all_0_0_0, all_11_1_3 and discharging atoms root_occ(all_11_1_3, all_0_0_0), occurrence_of(all_0_0_0, tptp0), yields: % 13.43/3.82 | (92) ? [v0] : (next_subocc(all_11_1_3, v0, tptp0) & occurrence_of(v0, tptp1)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (26) with all_0_0_0, all_11_1_3 and discharging atoms root_occ(all_11_1_3, all_0_0_0), yields: % 13.43/3.82 | (93) ? [v0] : (subactivity_occurrence(all_11_1_3, all_0_0_0) & root(all_11_1_3, v0) & occurrence_of(all_0_0_0, v0)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (20) with tptp0, all_0_0_0, all_9_0_1 and discharging atoms subactivity_occurrence(all_9_0_1, all_0_0_0), root(all_9_0_1, tptp0), occurrence_of(all_0_0_0, tptp0), yields: % 13.43/3.82 | (94) root_occ(all_9_0_1, all_0_0_0) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (11) with all_9_0_1, tptp0 and discharging atoms root(all_9_0_1, tptp0), ~ atomic(tptp0), yields: % 13.43/3.82 | (95) ? [v0] : (subactivity_occurrence(all_9_0_1, v0) & occurrence_of(v0, tptp0)) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (38) with all_0_0_0 and discharging atoms activity_occurrence(all_0_0_0), yields: % 13.43/3.82 | (96) ? [v0] : (activity(v0) & occurrence_of(all_0_0_0, v0)) % 13.43/3.82 | % 13.43/3.82 | Instantiating (96) with all_19_0_4 yields: % 13.43/3.82 | (97) activity(all_19_0_4) & occurrence_of(all_0_0_0, all_19_0_4) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (97) yields: % 13.43/3.82 | (98) activity(all_19_0_4) % 13.43/3.82 | (99) occurrence_of(all_0_0_0, all_19_0_4) % 13.43/3.82 | % 13.43/3.82 | Instantiating (95) with all_21_0_5 yields: % 13.43/3.82 | (100) subactivity_occurrence(all_9_0_1, all_21_0_5) & occurrence_of(all_21_0_5, tptp0) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (100) yields: % 13.43/3.82 | (101) subactivity_occurrence(all_9_0_1, all_21_0_5) % 13.43/3.82 | (102) occurrence_of(all_21_0_5, tptp0) % 13.43/3.82 | % 13.43/3.82 | Instantiating (93) with all_25_0_7 yields: % 13.43/3.82 | (103) subactivity_occurrence(all_11_1_3, all_0_0_0) & root(all_11_1_3, all_25_0_7) & occurrence_of(all_0_0_0, all_25_0_7) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (103) yields: % 13.43/3.82 | (104) subactivity_occurrence(all_11_1_3, all_0_0_0) % 13.43/3.82 | (105) root(all_11_1_3, all_25_0_7) % 13.43/3.82 | (106) occurrence_of(all_0_0_0, all_25_0_7) % 13.43/3.82 | % 13.43/3.82 | Instantiating (92) with all_27_0_8 yields: % 13.43/3.82 | (107) next_subocc(all_11_1_3, all_27_0_8, tptp0) & occurrence_of(all_27_0_8, tptp1) % 13.43/3.82 | % 13.43/3.82 | Applying alpha-rule on (107) yields: % 13.43/3.82 | (108) next_subocc(all_11_1_3, all_27_0_8, tptp0) % 13.43/3.82 | (109) occurrence_of(all_27_0_8, tptp1) % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (63) with all_25_0_7, tptp0, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_25_0_7), occurrence_of(all_0_0_0, tptp0), yields: % 13.43/3.82 | (110) all_25_0_7 = tptp0 % 13.43/3.82 | % 13.43/3.82 | Instantiating formula (56) with all_19_0_4, all_0_0_0, all_11_1_3, all_9_0_1 and discharging atoms root_occ(all_11_1_3, all_0_0_0), root_occ(all_9_0_1, all_0_0_0), occurrence_of(all_0_0_0, all_19_0_4), yields: % 13.43/3.82 | (111) all_11_1_3 = all_9_0_1 % 13.43/3.82 | % 13.43/3.82 | From (111) and (108) follows: % 13.43/3.83 | (112) next_subocc(all_9_0_1, all_27_0_8, tptp0) % 13.43/3.83 | % 13.43/3.83 | From (111)(110) and (105) follows: % 13.43/3.83 | (85) root(all_9_0_1, tptp0) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (16) with tptp0, all_27_0_8, all_9_0_1 and discharging atoms next_subocc(all_9_0_1, all_27_0_8, tptp0), yields: % 13.43/3.83 | (114) min_precedes(all_9_0_1, all_27_0_8, tptp0) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (66) with all_27_0_8, tptp1 and discharging atoms occurrence_of(all_27_0_8, tptp1), yields: % 13.43/3.83 | (115) activity_occurrence(all_27_0_8) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (79) with all_27_0_8, tptp1 and discharging atoms occurrence_of(all_27_0_8, tptp1), yields: % 13.43/3.83 | (116) activity(tptp1) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (20) with tptp0, all_21_0_5, all_9_0_1 and discharging atoms subactivity_occurrence(all_9_0_1, all_21_0_5), root(all_9_0_1, tptp0), occurrence_of(all_21_0_5, tptp0), yields: % 13.43/3.83 | (117) root_occ(all_9_0_1, all_21_0_5) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (14) with all_21_0_5 and discharging atoms occurrence_of(all_21_0_5, tptp0), yields: % 13.43/3.83 | (118) ? [v0] : ? [v1] : (leaf_occ(v1, all_21_0_5) & root_occ(v0, all_21_0_5) & next_subocc(v0, v1, tptp0) & occurrence_of(v1, tptp3) & occurrence_of(v0, tptp4)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (66) with all_21_0_5, tptp0 and discharging atoms occurrence_of(all_21_0_5, tptp0), yields: % 13.43/3.83 | (119) activity_occurrence(all_21_0_5) % 13.43/3.83 | % 13.43/3.83 | Instantiating (118) with all_59_0_20, all_59_1_21 yields: % 13.43/3.83 | (120) leaf_occ(all_59_0_20, all_21_0_5) & root_occ(all_59_1_21, all_21_0_5) & next_subocc(all_59_1_21, all_59_0_20, tptp0) & occurrence_of(all_59_0_20, tptp3) & occurrence_of(all_59_1_21, tptp4) % 13.43/3.83 | % 13.43/3.83 | Applying alpha-rule on (120) yields: % 13.43/3.83 | (121) occurrence_of(all_59_1_21, tptp4) % 13.43/3.83 | (122) occurrence_of(all_59_0_20, tptp3) % 13.43/3.83 | (123) next_subocc(all_59_1_21, all_59_0_20, tptp0) % 13.43/3.83 | (124) leaf_occ(all_59_0_20, all_21_0_5) % 13.43/3.83 | (125) root_occ(all_59_1_21, all_21_0_5) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (56) with tptp0, all_21_0_5, all_9_0_1, all_59_1_21 and discharging atoms root_occ(all_59_1_21, all_21_0_5), root_occ(all_9_0_1, all_21_0_5), occurrence_of(all_21_0_5, tptp0), yields: % 13.43/3.83 | (126) all_59_1_21 = all_9_0_1 % 13.43/3.83 | % 13.43/3.83 | From (126) and (125) follows: % 13.43/3.83 | (117) root_occ(all_9_0_1, all_21_0_5) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (70) with all_21_0_5, all_59_0_20 and discharging atoms leaf_occ(all_59_0_20, all_21_0_5), yields: % 13.43/3.83 | (128) ? [v0] : (subactivity_occurrence(all_59_0_20, all_21_0_5) & leaf(all_59_0_20, v0) & occurrence_of(all_21_0_5, v0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (26) with all_21_0_5, all_9_0_1 and discharging atoms root_occ(all_9_0_1, all_21_0_5), yields: % 13.43/3.83 | (129) ? [v0] : (subactivity_occurrence(all_9_0_1, all_21_0_5) & root(all_9_0_1, v0) & occurrence_of(all_21_0_5, v0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (24) with all_27_0_8, all_9_0_1, tptp0 and discharging atoms min_precedes(all_9_0_1, all_27_0_8, tptp0), yields: % 13.43/3.83 | (130) ? [v0] : ? [v1] : (atocc(all_27_0_8, v1) & atocc(all_9_0_1, v0) & subactivity(v1, tptp0) & subactivity(v0, tptp0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (60) with all_27_0_8, all_9_0_1, tptp0 and discharging atoms min_precedes(all_9_0_1, all_27_0_8, tptp0), yields: % 13.43/3.83 | (131) ? [v0] : (subactivity_occurrence(all_27_0_8, v0) & subactivity_occurrence(all_9_0_1, v0) & occurrence_of(v0, tptp0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (28) with tptp0, all_27_0_8, all_9_0_1 and discharging atoms min_precedes(all_9_0_1, all_27_0_8, tptp0), yields: % 13.43/3.83 | (132) ? [v0] : (root(v0, tptp0) & min_precedes(v0, all_27_0_8, tptp0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (38) with all_27_0_8 and discharging atoms activity_occurrence(all_27_0_8), yields: % 13.43/3.83 | (133) ? [v0] : (activity(v0) & occurrence_of(all_27_0_8, v0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (38) with all_21_0_5 and discharging atoms activity_occurrence(all_21_0_5), yields: % 13.43/3.83 | (134) ? [v0] : (activity(v0) & occurrence_of(all_21_0_5, v0)) % 13.43/3.83 | % 13.43/3.83 | Instantiating formula (73) with tptp1 and discharging atoms activity(tptp1), yields: % 13.43/3.83 | (135) subactivity(tptp1, tptp1) % 13.43/3.83 | % 13.43/3.83 | Instantiating (131) with all_73_0_23 yields: % 13.43/3.83 | (136) subactivity_occurrence(all_27_0_8, all_73_0_23) & subactivity_occurrence(all_9_0_1, all_73_0_23) & occurrence_of(all_73_0_23, tptp0) % 13.43/3.83 | % 13.43/3.83 | Applying alpha-rule on (136) yields: % 13.43/3.83 | (137) subactivity_occurrence(all_27_0_8, all_73_0_23) % 13.43/3.83 | (138) subactivity_occurrence(all_9_0_1, all_73_0_23) % 13.43/3.83 | (139) occurrence_of(all_73_0_23, tptp0) % 13.43/3.83 | % 13.43/3.83 | Instantiating (130) with all_75_0_24, all_75_1_25 yields: % 13.43/3.83 | (140) atocc(all_27_0_8, all_75_0_24) & atocc(all_9_0_1, all_75_1_25) & subactivity(all_75_0_24, tptp0) & subactivity(all_75_1_25, tptp0) % 13.43/3.83 | % 13.43/3.83 | Applying alpha-rule on (140) yields: % 13.43/3.83 | (141) atocc(all_27_0_8, all_75_0_24) % 13.43/3.83 | (142) atocc(all_9_0_1, all_75_1_25) % 13.43/3.83 | (143) subactivity(all_75_0_24, tptp0) % 13.43/3.83 | (144) subactivity(all_75_1_25, tptp0) % 13.43/3.83 | % 13.43/3.83 | Instantiating (132) with all_79_0_27 yields: % 13.43/3.83 | (145) root(all_79_0_27, tptp0) & min_precedes(all_79_0_27, all_27_0_8, tptp0) % 13.43/3.83 | % 13.43/3.83 | Applying alpha-rule on (145) yields: % 13.43/3.83 | (146) root(all_79_0_27, tptp0) % 13.43/3.83 | (147) min_precedes(all_79_0_27, all_27_0_8, tptp0) % 13.43/3.83 | % 13.43/3.83 | Instantiating (129) with all_91_0_34 yields: % 13.43/3.83 | (148) subactivity_occurrence(all_9_0_1, all_21_0_5) & root(all_9_0_1, all_91_0_34) & occurrence_of(all_21_0_5, all_91_0_34) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (148) yields: % 13.43/3.84 | (101) subactivity_occurrence(all_9_0_1, all_21_0_5) % 13.43/3.84 | (150) root(all_9_0_1, all_91_0_34) % 13.43/3.84 | (151) occurrence_of(all_21_0_5, all_91_0_34) % 13.43/3.84 | % 13.43/3.84 | Instantiating (128) with all_95_0_36 yields: % 13.43/3.84 | (152) subactivity_occurrence(all_59_0_20, all_21_0_5) & leaf(all_59_0_20, all_95_0_36) & occurrence_of(all_21_0_5, all_95_0_36) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (152) yields: % 13.43/3.84 | (153) subactivity_occurrence(all_59_0_20, all_21_0_5) % 13.43/3.84 | (154) leaf(all_59_0_20, all_95_0_36) % 13.43/3.84 | (155) occurrence_of(all_21_0_5, all_95_0_36) % 13.43/3.84 | % 13.43/3.84 | Instantiating (134) with all_99_0_38 yields: % 13.43/3.84 | (156) activity(all_99_0_38) & occurrence_of(all_21_0_5, all_99_0_38) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (156) yields: % 13.43/3.84 | (157) activity(all_99_0_38) % 13.43/3.84 | (158) occurrence_of(all_21_0_5, all_99_0_38) % 13.43/3.84 | % 13.43/3.84 | Instantiating (133) with all_103_0_41 yields: % 13.43/3.84 | (159) activity(all_103_0_41) & occurrence_of(all_27_0_8, all_103_0_41) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (159) yields: % 13.43/3.84 | (160) activity(all_103_0_41) % 13.43/3.84 | (161) occurrence_of(all_27_0_8, all_103_0_41) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (63) with all_103_0_41, tptp1, all_27_0_8 and discharging atoms occurrence_of(all_27_0_8, all_103_0_41), occurrence_of(all_27_0_8, tptp1), yields: % 13.43/3.84 | (162) all_103_0_41 = tptp1 % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (63) with all_99_0_38, tptp0, all_21_0_5 and discharging atoms occurrence_of(all_21_0_5, all_99_0_38), occurrence_of(all_21_0_5, tptp0), yields: % 13.43/3.84 | (163) all_99_0_38 = tptp0 % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (63) with all_95_0_36, all_99_0_38, all_21_0_5 and discharging atoms occurrence_of(all_21_0_5, all_99_0_38), occurrence_of(all_21_0_5, all_95_0_36), yields: % 13.43/3.84 | (164) all_99_0_38 = all_95_0_36 % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (63) with all_91_0_34, all_99_0_38, all_21_0_5 and discharging atoms occurrence_of(all_21_0_5, all_99_0_38), occurrence_of(all_21_0_5, all_91_0_34), yields: % 13.43/3.84 | (165) all_99_0_38 = all_91_0_34 % 13.43/3.84 | % 13.43/3.84 | Combining equations (165,164) yields a new equation: % 13.43/3.84 | (166) all_95_0_36 = all_91_0_34 % 13.43/3.84 | % 13.43/3.84 | Combining equations (163,164) yields a new equation: % 13.43/3.84 | (167) all_95_0_36 = tptp0 % 13.43/3.84 | % 13.43/3.84 | Combining equations (167,166) yields a new equation: % 13.43/3.84 | (168) all_91_0_34 = tptp0 % 13.43/3.84 | % 13.43/3.84 | From (168) and (150) follows: % 13.43/3.84 | (85) root(all_9_0_1, tptp0) % 13.43/3.84 | % 13.43/3.84 | From (162) and (161) follows: % 13.43/3.84 | (109) occurrence_of(all_27_0_8, tptp1) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (21) with all_75_0_24, all_27_0_8 and discharging atoms atocc(all_27_0_8, all_75_0_24), yields: % 13.43/3.84 | (171) ? [v0] : (atomic(v0) & subactivity(all_75_0_24, v0) & occurrence_of(all_27_0_8, v0)) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (24) with all_27_0_8, all_79_0_27, tptp0 and discharging atoms min_precedes(all_79_0_27, all_27_0_8, tptp0), yields: % 13.43/3.84 | (172) ? [v0] : ? [v1] : (atocc(all_79_0_27, v0) & atocc(all_27_0_8, v1) & subactivity(v1, tptp0) & subactivity(v0, tptp0)) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (32) with tptp1, tptp1, all_27_0_8 and discharging atoms atomic(tptp1), subactivity(tptp1, tptp1), occurrence_of(all_27_0_8, tptp1), yields: % 13.43/3.84 | (173) atocc(all_27_0_8, tptp1) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (20) with tptp0, all_73_0_23, all_9_0_1 and discharging atoms subactivity_occurrence(all_9_0_1, all_73_0_23), root(all_9_0_1, tptp0), occurrence_of(all_73_0_23, tptp0), yields: % 13.43/3.84 | (174) root_occ(all_9_0_1, all_73_0_23) % 13.43/3.84 | % 13.43/3.84 | Instantiating formula (14) with all_73_0_23 and discharging atoms occurrence_of(all_73_0_23, tptp0), yields: % 13.43/3.84 | (175) ? [v0] : ? [v1] : (leaf_occ(v1, all_73_0_23) & root_occ(v0, all_73_0_23) & next_subocc(v0, v1, tptp0) & occurrence_of(v1, tptp3) & occurrence_of(v0, tptp4)) % 13.43/3.84 | % 13.43/3.84 | Instantiating (172) with all_163_0_68, all_163_1_69 yields: % 13.43/3.84 | (176) atocc(all_79_0_27, all_163_1_69) & atocc(all_27_0_8, all_163_0_68) & subactivity(all_163_0_68, tptp0) & subactivity(all_163_1_69, tptp0) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (176) yields: % 13.43/3.84 | (177) atocc(all_79_0_27, all_163_1_69) % 13.43/3.84 | (178) atocc(all_27_0_8, all_163_0_68) % 13.43/3.84 | (179) subactivity(all_163_0_68, tptp0) % 13.43/3.84 | (180) subactivity(all_163_1_69, tptp0) % 13.43/3.84 | % 13.43/3.84 | Instantiating (171) with all_165_0_70 yields: % 13.43/3.84 | (181) atomic(all_165_0_70) & subactivity(all_75_0_24, all_165_0_70) & occurrence_of(all_27_0_8, all_165_0_70) % 13.43/3.84 | % 13.43/3.84 | Applying alpha-rule on (181) yields: % 13.43/3.84 | (182) atomic(all_165_0_70) % 13.43/3.85 | (183) subactivity(all_75_0_24, all_165_0_70) % 13.43/3.85 | (184) occurrence_of(all_27_0_8, all_165_0_70) % 13.43/3.85 | % 13.43/3.85 | Instantiating (175) with all_189_0_85, all_189_1_86 yields: % 13.43/3.85 | (185) leaf_occ(all_189_0_85, all_73_0_23) & root_occ(all_189_1_86, all_73_0_23) & next_subocc(all_189_1_86, all_189_0_85, tptp0) & occurrence_of(all_189_0_85, tptp3) & occurrence_of(all_189_1_86, tptp4) % 13.43/3.85 | % 13.43/3.85 | Applying alpha-rule on (185) yields: % 13.43/3.85 | (186) occurrence_of(all_189_0_85, tptp3) % 13.43/3.85 | (187) leaf_occ(all_189_0_85, all_73_0_23) % 13.43/3.85 | (188) next_subocc(all_189_1_86, all_189_0_85, tptp0) % 13.43/3.85 | (189) occurrence_of(all_189_1_86, tptp4) % 13.43/3.85 | (190) root_occ(all_189_1_86, all_73_0_23) % 13.43/3.85 | % 13.43/3.85 | Instantiating formula (56) with tptp0, all_73_0_23, all_9_0_1, all_189_1_86 and discharging atoms root_occ(all_189_1_86, all_73_0_23), root_occ(all_9_0_1, all_73_0_23), occurrence_of(all_73_0_23, tptp0), yields: % 13.43/3.85 | (191) all_189_1_86 = all_9_0_1 % 13.43/3.85 | % 13.43/3.85 | Instantiating formula (63) with all_165_0_70, tptp1, all_27_0_8 and discharging atoms occurrence_of(all_27_0_8, all_165_0_70), occurrence_of(all_27_0_8, tptp1), yields: % 13.43/3.85 | (192) all_165_0_70 = tptp1 % 13.43/3.85 | % 13.43/3.85 | From (191) and (188) follows: % 13.43/3.85 | (193) next_subocc(all_9_0_1, all_189_0_85, tptp0) % 13.43/3.85 | % 13.43/3.85 | From (192) and (184) follows: % 13.43/3.85 | (109) occurrence_of(all_27_0_8, tptp1) % 13.43/3.85 | % 13.43/3.85 | Instantiating formula (70) with all_73_0_23, all_189_0_85 and discharging atoms leaf_occ(all_189_0_85, all_73_0_23), yields: % 13.43/3.85 | (195) ? [v0] : (subactivity_occurrence(all_189_0_85, all_73_0_23) & leaf(all_189_0_85, v0) & occurrence_of(all_73_0_23, v0)) % 13.43/3.85 | % 13.43/3.85 | Instantiating formula (21) with all_163_0_68, all_27_0_8 and discharging atoms atocc(all_27_0_8, all_163_0_68), yields: % 13.43/3.85 | (196) ? [v0] : (atomic(v0) & subactivity(all_163_0_68, v0) & occurrence_of(all_27_0_8, v0)) % 13.43/3.85 | % 13.43/3.85 | Instantiating formula (21) with tptp1, all_27_0_8 and discharging atoms atocc(all_27_0_8, tptp1), yields: % 13.43/3.85 | (197) ? [v0] : (atomic(v0) & subactivity(tptp1, v0) & occurrence_of(all_27_0_8, v0)) % 13.43/3.85 | % 13.43/3.85 | Instantiating (196) with all_356_0_166 yields: % 13.43/3.85 | (198) atomic(all_356_0_166) & subactivity(all_163_0_68, all_356_0_166) & occurrence_of(all_27_0_8, all_356_0_166) % 13.43/3.85 | % 13.43/3.85 | Applying alpha-rule on (198) yields: % 13.43/3.85 | (199) atomic(all_356_0_166) % 13.43/3.85 | (200) subactivity(all_163_0_68, all_356_0_166) % 13.43/3.85 | (201) occurrence_of(all_27_0_8, all_356_0_166) % 13.43/3.85 | % 13.43/3.85 | Instantiating (195) with all_472_0_232 yields: % 13.43/3.85 | (202) subactivity_occurrence(all_189_0_85, all_73_0_23) & leaf(all_189_0_85, all_472_0_232) & occurrence_of(all_73_0_23, all_472_0_232) % 13.43/3.85 | % 13.85/3.85 | Applying alpha-rule on (202) yields: % 13.85/3.85 | (203) subactivity_occurrence(all_189_0_85, all_73_0_23) % 13.85/3.85 | (204) leaf(all_189_0_85, all_472_0_232) % 13.85/3.85 | (205) occurrence_of(all_73_0_23, all_472_0_232) % 13.85/3.85 | % 13.85/3.85 | Instantiating (197) with all_480_0_236 yields: % 13.85/3.85 | (206) atomic(all_480_0_236) & subactivity(tptp1, all_480_0_236) & occurrence_of(all_27_0_8, all_480_0_236) % 13.85/3.85 | % 13.85/3.85 | Applying alpha-rule on (206) yields: % 13.85/3.85 | (207) atomic(all_480_0_236) % 13.85/3.85 | (208) subactivity(tptp1, all_480_0_236) % 13.85/3.85 | (209) occurrence_of(all_27_0_8, all_480_0_236) % 13.85/3.85 | % 13.85/3.85 | Instantiating formula (65) with all_73_0_23, tptp0, all_189_0_85, all_27_0_8, all_9_0_1 and discharging atoms subactivity_occurrence(all_189_0_85, all_73_0_23), subactivity_occurrence(all_27_0_8, all_73_0_23), next_subocc(all_9_0_1, all_189_0_85, tptp0), next_subocc(all_9_0_1, all_27_0_8, tptp0), occurrence_of(all_73_0_23, tptp0), yields: % 13.85/3.85 | (210) all_189_0_85 = all_27_0_8 % 13.85/3.85 | % 13.85/3.85 | Instantiating formula (63) with all_480_0_236, tptp1, all_27_0_8 and discharging atoms occurrence_of(all_27_0_8, all_480_0_236), occurrence_of(all_27_0_8, tptp1), yields: % 13.85/3.85 | (211) all_480_0_236 = tptp1 % 13.85/3.85 | % 13.85/3.85 | Instantiating formula (63) with all_356_0_166, all_480_0_236, all_27_0_8 and discharging atoms occurrence_of(all_27_0_8, all_480_0_236), occurrence_of(all_27_0_8, all_356_0_166), yields: % 13.85/3.85 | (212) all_480_0_236 = all_356_0_166 % 13.85/3.85 | % 13.85/3.85 | Combining equations (211,212) yields a new equation: % 13.85/3.85 | (213) all_356_0_166 = tptp1 % 13.85/3.85 | % 13.85/3.85 | From (210) and (186) follows: % 13.85/3.85 | (214) occurrence_of(all_27_0_8, tptp3) % 13.85/3.86 | % 13.85/3.86 | From (213) and (201) follows: % 13.85/3.86 | (109) occurrence_of(all_27_0_8, tptp1) % 13.85/3.86 | % 13.85/3.86 | Instantiating formula (63) with tptp3, tptp1, all_27_0_8 and discharging atoms occurrence_of(all_27_0_8, tptp1), occurrence_of(all_27_0_8, tptp3), yields: % 13.85/3.86 | (216) tptp1 = tptp3 % 13.85/3.86 | % 13.85/3.86 | Equations (216) can reduce 4 to: % 13.85/3.86 | (217) $false % 13.85/3.86 | % 13.85/3.86 |-The branch is then unsatisfiable % 13.85/3.86 % SZS output end Proof for theBenchmark % 13.85/3.86 % 13.85/3.86 3262ms %------------------------------------------------------------------------------