%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n012.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:58 EDT 2022 % Result : Theorem 13.76s 4.03s % Output : Proof 16.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO012+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 03:18:11 EDT 2022 % 0.12/0.34 % CPUTime : % 0.65/0.63 ____ _ % 0.65/0.63 ___ / __ \_____(_)___ ________ __________ % 0.65/0.63 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.65/0.63 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.65/0.63 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.65/0.63 % 0.65/0.63 A Theorem Prover for First-Order Logic % 0.65/0.63 (ePrincess v.1.0) % 0.65/0.63 % 0.65/0.63 (c) Philipp Rümmer, 2009-2015 % 0.65/0.63 (c) Peter Backeman, 2014-2015 % 0.65/0.63 (contributions by Angelo Brillout, Peter Baumgartner) % 0.65/0.63 Free software under GNU Lesser General Public License (LGPL). % 0.65/0.63 Bug reports to peter@backeman.se % 0.65/0.63 % 0.65/0.63 For more information, visit http://user.uu.se/~petba168/breu/ % 0.65/0.63 % 0.65/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.72/0.70 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.86/1.04 Prover 0: Preprocessing ... % 2.41/1.32 Prover 0: Constructing countermodel ... % 13.76/4.02 Prover 0: proved (3326ms) % 13.76/4.03 % 13.76/4.03 No countermodel exists, formula is valid % 13.76/4.03 % SZS status Theorem for theBenchmark % 13.76/4.03 % 13.76/4.03 Generating proof ... found it (size 133) % 15.83/4.51 % 15.83/4.51 % SZS output start Proof for theBenchmark % 15.83/4.51 Assumed formulas after preprocessing and simplification: % 15.83/4.51 | (0) ? [v0] : ( ~ (tptp1 = tptp2) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) & atomic(tptp1) & atomic(tptp2) & atomic(tptp4) & atomic(tptp3) & occurrence_of(v0, tptp0) & ~ atomic(tptp0) & ! [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] : (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] : ( ~ next_subocc(v1, v2, v3) | ~ min_precedes(v4, v2, v3) | ~ min_precedes(v1, v4, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ leaf_occ(v2, v1) | ~ occurrence_of(v1, v3) | ~ min_precedes(v2, v4, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ root_occ(v2, v1) | ~ occurrence_of(v1, v3) | ~ min_precedes(v4, v2, v3)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ min_precedes(v2, v3, v4) | ~ min_precedes(v1, v2, v4) | min_precedes(v1, v3, v4)) & ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ occurrence_of(v1, v3) | ~ occurrence_of(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity(v2, v3) | ~ atomic(v3) | ~ occurrence_of(v1, v3) | atocc(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ leaf(v1, v3) | ~ subactivity_occurrence(v1, v2) | ~ occurrence_of(v2, v3) | leaf_occ(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ leaf(v1, v2) | ~ min_precedes(v1, v3, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ subactivity_occurrence(v1, v2) | ~ root(v1, v3) | ~ occurrence_of(v2, v3) | root_occ(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ root(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] : ( ~ next_subocc(v1, v2, v3) | min_precedes(v1, v2, v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ earlier(v2, v3) | ~ earlier(v1, v2) | earlier(v1, 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] : (subactivity(v5, v1) & subactivity(v4, v1) & atocc(v3, v5) & atocc(v2, v4))) & ! [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) | precedes(v1, v2)) & ! [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] : ( ~ atocc(v1, v2) | ~ legal(v1) | root(v1, v2)) & ! [v1] : ! [v2] : ( ~ atocc(v1, v2) | ? [v3] : (subactivity(v2, v3) & atomic(v3) & occurrence_of(v1, v3))) & ! [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] : ( ~ subactivity_occurrence(v1, v2) | activity_occurrence(v2)) & ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v1, v2) | activity_occurrence(v1)) & ! [v1] : ! [v2] : ( ~ legal(v2) | ~ earlier(v1, v2) | precedes(v1, v2)) & ! [v1] : ! [v2] : ( ~ root(v2, v1) | ? [v3] : (subactivity(v3, v1) & atocc(v2, v3))) & ! [v1] : ! [v2] : ( ~ root(v1, v2) | leaf(v1, v2) | ? [v3] : min_precedes(v1, v3, v2)) & ! [v1] : ! [v2] : ( ~ root(v1, v2) | legal(v1)) & ! [v1] : ! [v2] : ( ~ precedes(v1, v2) | legal(v2)) & ! [v1] : ! [v2] : ( ~ precedes(v1, v2) | earlier(v1, v2)) & ! [v1] : ! [v2] : ( ~ arboreal(v1) | ~ occurrence_of(v1, v2) | atomic(v2)) & ! [v1] : ! [v2] : ( ~ leaf_occ(v1, v2) | ? [v3] : (leaf(v1, v3) & subactivity_occurrence(v1, v2) & occurrence_of(v2, v3))) & ! [v1] : ! [v2] : ( ~ atomic(v2) | ~ occurrence_of(v1, v2) | arboreal(v1)) & ! [v1] : ! [v2] : ( ~ root_occ(v1, v2) | ? [v3] : (subactivity_occurrence(v1, v2) & root(v1, v3) & occurrence_of(v2, v3))) & ! [v1] : ! [v2] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v2, tptp1) | ~ occurrence_of(v1, tptp3) | ~ min_precedes(v1, v2, tptp0)) & ! [v1] : ! [v2] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v2, tptp2) | ~ occurrence_of(v1, tptp3) | ~ min_precedes(v1, v2, tptp0)) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | activity(v1)) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | activity_occurrence(v2)) & ! [v1] : ! [v2] : ( ~ occurrence_of(v2, v1) | atomic(v1) | ? [v3] : (subactivity_occurrence(v3, v2) & root(v3, v1))) & ! [v1] : ! [v2] : ( ~ earlier(v2, v1) | ~ earlier(v1, v2)) & ! [v1] : ( ~ activity(v1) | subactivity(v1, v1)) & ! [v1] : ( ~ activity_occurrence(v1) | ? [v2] : (activity(v2) & occurrence_of(v1, v2))) & ! [v1] : ( ~ legal(v1) | arboreal(v1)) & ! [v1] : ( ~ occurrence_of(v1, tptp0) | ? [v2] : ? [v3] : ? [v4] : (root_occ(v2, v1) & 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, tptp1) | occurrence_of(v4, tptp2))))) % 15.83/4.53 | Instantiating (0) with all_0_0_0 yields: % 15.83/4.53 | (1) ~ (tptp1 = tptp2) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) & atomic(tptp1) & atomic(tptp2) & atomic(tptp4) & atomic(tptp3) & occurrence_of(all_0_0_0, tptp0) & ~ 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) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) & ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) & ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) & ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) & ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) & ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) & ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) & ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) & ! [v0] : ! [v1] : ( ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) & ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) & ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) & ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) & ! [v0] : ( ~ legal(v0) | arboreal(v0)) & ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : ? [v3] : (root_occ(v1, v0) & occurrence_of(v2, tptp4) & occurrence_of(v1, tptp3) & min_precedes(v2, v3, tptp0) & min_precedes(v1, v2, tptp0) & ! [v4] : (v4 = v3 | v4 = v2 | ~ min_precedes(v1, v4, tptp0)) & (occurrence_of(v3, tptp1) | occurrence_of(v3, tptp2)))) % 15.83/4.54 | % 15.83/4.54 | Applying alpha-rule on (1) yields: % 15.83/4.54 | (2) activity(tptp0) % 15.83/4.54 | (3) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 15.83/4.54 | (4) atomic(tptp1) % 15.83/4.54 | (5) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 15.83/4.54 | (6) ! [v0] : ! [v1] : ( ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) % 15.83/4.54 | (7) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 16.09/4.54 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 16.09/4.54 | (9) occurrence_of(all_0_0_0, tptp0) % 16.09/4.54 | (10) atomic(tptp3) % 16.09/4.54 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 16.09/4.54 | (12) atomic(tptp2) % 16.09/4.54 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 16.09/4.54 | (14) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 16.09/4.54 | (15) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 16.09/4.54 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 16.09/4.54 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 16.09/4.54 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 16.09/4.54 | (19) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 16.09/4.54 | (20) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) % 16.09/4.54 | (21) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 16.09/4.54 | (22) atomic(tptp4) % 16.09/4.54 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 16.09/4.54 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 16.09/4.54 | (25) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 16.09/4.54 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) % 16.09/4.54 | (27) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 16.09/4.54 | (28) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 16.09/4.54 | (29) ! [v0] : ! [v1] : ( ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) % 16.09/4.54 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 16.09/4.54 | (31) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 16.09/4.54 | (32) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 16.09/4.54 | (33) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 16.09/4.55 | (34) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 16.09/4.55 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 16.09/4.55 | (36) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) % 16.09/4.55 | (37) ~ (tptp1 = tptp2) % 16.09/4.55 | (38) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 16.09/4.55 | (39) ! [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)) % 16.09/4.55 | (40) ~ (tptp1 = tptp4) % 16.09/4.55 | (41) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 16.09/4.55 | (42) ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) % 16.09/4.55 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v0, v2, v3)) % 16.09/4.55 | (44) ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : ? [v3] : (root_occ(v1, v0) & occurrence_of(v2, tptp4) & occurrence_of(v1, tptp3) & min_precedes(v2, v3, tptp0) & min_precedes(v1, v2, tptp0) & ! [v4] : (v4 = v3 | v4 = v2 | ~ min_precedes(v1, v4, tptp0)) & (occurrence_of(v3, tptp1) | occurrence_of(v3, tptp2)))) % 16.09/4.55 | (45) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) % 16.09/4.55 | (46) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, v3))) % 16.09/4.55 | (47) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 16.09/4.55 | (48) ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) % 16.09/4.55 | (49) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 16.09/4.55 | (50) ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 16.09/4.55 | (51) ~ (tptp1 = tptp3) % 16.09/4.55 | (52) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 16.09/4.55 | (53) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 16.09/4.55 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v3, v1, v2)) % 16.09/4.55 | (55) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 16.09/4.55 | (56) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 16.09/4.55 | (57) ~ (tptp2 = tptp3) % 16.09/4.55 | (58) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 16.09/4.55 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 16.09/4.55 | (60) ~ (tptp2 = tptp4) % 16.09/4.55 | (61) ~ (tptp4 = tptp3) % 16.09/4.55 | (62) ~ atomic(tptp0) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (44) with all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, tptp0), yields: % 16.09/4.55 | (63) ? [v0] : ? [v1] : ? [v2] : (root_occ(v0, all_0_0_0) & 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, tptp1) | occurrence_of(v2, tptp2))) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (34) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0), yields: % 16.09/4.55 | (64) activity_occurrence(all_0_0_0) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (5) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0), ~ atomic(tptp0), yields: % 16.09/4.55 | (65) ? [v0] : (subactivity_occurrence(v0, all_0_0_0) & root(v0, tptp0)) % 16.09/4.55 | % 16.09/4.55 | Instantiating (65) with all_9_0_1 yields: % 16.09/4.55 | (66) subactivity_occurrence(all_9_0_1, all_0_0_0) & root(all_9_0_1, tptp0) % 16.09/4.55 | % 16.09/4.55 | Applying alpha-rule on (66) yields: % 16.09/4.55 | (67) subactivity_occurrence(all_9_0_1, all_0_0_0) % 16.09/4.55 | (68) root(all_9_0_1, tptp0) % 16.09/4.55 | % 16.09/4.55 | Instantiating (63) with all_11_0_2, all_11_1_3, all_11_2_4 yields: % 16.09/4.55 | (69) root_occ(all_11_2_4, all_0_0_0) & occurrence_of(all_11_1_3, tptp4) & occurrence_of(all_11_2_4, tptp3) & min_precedes(all_11_1_3, all_11_0_2, tptp0) & min_precedes(all_11_2_4, all_11_1_3, tptp0) & ! [v0] : (v0 = all_11_0_2 | v0 = all_11_1_3 | ~ min_precedes(all_11_2_4, v0, tptp0)) & (occurrence_of(all_11_0_2, tptp1) | occurrence_of(all_11_0_2, tptp2)) % 16.09/4.55 | % 16.09/4.55 | Applying alpha-rule on (69) yields: % 16.09/4.55 | (70) occurrence_of(all_11_2_4, tptp3) % 16.09/4.55 | (71) occurrence_of(all_11_0_2, tptp1) | occurrence_of(all_11_0_2, tptp2) % 16.09/4.55 | (72) root_occ(all_11_2_4, all_0_0_0) % 16.09/4.55 | (73) ! [v0] : (v0 = all_11_0_2 | v0 = all_11_1_3 | ~ min_precedes(all_11_2_4, v0, tptp0)) % 16.09/4.55 | (74) occurrence_of(all_11_1_3, tptp4) % 16.09/4.55 | (75) min_precedes(all_11_2_4, all_11_1_3, tptp0) % 16.09/4.55 | (76) min_precedes(all_11_1_3, all_11_0_2, tptp0) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (49) with all_0_0_0 and discharging atoms activity_occurrence(all_0_0_0), yields: % 16.09/4.55 | (77) ? [v0] : (activity(v0) & occurrence_of(all_0_0_0, v0)) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (52) 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: % 16.09/4.55 | (78) root_occ(all_9_0_1, all_0_0_0) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (45) with all_9_0_1, tptp0 and discharging atoms root(all_9_0_1, tptp0), yields: % 16.09/4.55 | (79) ? [v0] : (subactivity(v0, tptp0) & atocc(all_9_0_1, v0)) % 16.09/4.55 | % 16.09/4.55 | Instantiating formula (47) with tptp0, all_9_0_1 and discharging atoms root(all_9_0_1, tptp0), yields: % 16.09/4.56 | (80) legal(all_9_0_1) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (41) with all_0_0_0, all_11_2_4 and discharging atoms root_occ(all_11_2_4, all_0_0_0), yields: % 16.09/4.56 | (81) ? [v0] : (subactivity_occurrence(all_11_2_4, all_0_0_0) & root(all_11_2_4, v0) & occurrence_of(all_0_0_0, v0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (3) with all_11_2_4, tptp3 and discharging atoms occurrence_of(all_11_2_4, tptp3), yields: % 16.09/4.56 | (82) activity(tptp3) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (34) with all_11_2_4, tptp3 and discharging atoms occurrence_of(all_11_2_4, tptp3), yields: % 16.09/4.56 | (83) activity_occurrence(all_11_2_4) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (43) with tptp0, all_11_0_2, all_11_1_3, all_11_2_4 and discharging atoms min_precedes(all_11_1_3, all_11_0_2, tptp0), min_precedes(all_11_2_4, all_11_1_3, tptp0), yields: % 16.09/4.56 | (84) min_precedes(all_11_2_4, all_11_0_2, tptp0) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (46) with all_11_1_3, all_11_2_4, tptp0 and discharging atoms min_precedes(all_11_2_4, all_11_1_3, tptp0), yields: % 16.09/4.56 | (85) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_11_1_3, v1) & atocc(all_11_2_4, v0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (35) with all_11_1_3, all_11_2_4, tptp0 and discharging atoms min_precedes(all_11_2_4, all_11_1_3, tptp0), yields: % 16.09/4.56 | (86) ? [v0] : (subactivity_occurrence(all_11_1_3, v0) & subactivity_occurrence(all_11_2_4, v0) & occurrence_of(v0, tptp0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating (79) with all_22_0_7 yields: % 16.09/4.56 | (87) subactivity(all_22_0_7, tptp0) & atocc(all_9_0_1, all_22_0_7) % 16.09/4.56 | % 16.09/4.56 | Applying alpha-rule on (87) yields: % 16.09/4.56 | (88) subactivity(all_22_0_7, tptp0) % 16.09/4.56 | (89) atocc(all_9_0_1, all_22_0_7) % 16.09/4.56 | % 16.09/4.56 | Instantiating (81) with all_24_0_8 yields: % 16.09/4.56 | (90) subactivity_occurrence(all_11_2_4, all_0_0_0) & root(all_11_2_4, all_24_0_8) & occurrence_of(all_0_0_0, all_24_0_8) % 16.09/4.56 | % 16.09/4.56 | Applying alpha-rule on (90) yields: % 16.09/4.56 | (91) subactivity_occurrence(all_11_2_4, all_0_0_0) % 16.09/4.56 | (92) root(all_11_2_4, all_24_0_8) % 16.09/4.56 | (93) occurrence_of(all_0_0_0, all_24_0_8) % 16.09/4.56 | % 16.09/4.56 | Instantiating (77) with all_26_0_9 yields: % 16.09/4.56 | (94) activity(all_26_0_9) & occurrence_of(all_0_0_0, all_26_0_9) % 16.09/4.56 | % 16.09/4.56 | Applying alpha-rule on (94) yields: % 16.09/4.56 | (95) activity(all_26_0_9) % 16.09/4.56 | (96) occurrence_of(all_0_0_0, all_26_0_9) % 16.09/4.56 | % 16.09/4.56 | Instantiating (86) with all_28_0_10 yields: % 16.09/4.56 | (97) subactivity_occurrence(all_11_1_3, all_28_0_10) & subactivity_occurrence(all_11_2_4, all_28_0_10) & occurrence_of(all_28_0_10, tptp0) % 16.09/4.56 | % 16.09/4.56 | Applying alpha-rule on (97) yields: % 16.09/4.56 | (98) subactivity_occurrence(all_11_1_3, all_28_0_10) % 16.09/4.56 | (99) subactivity_occurrence(all_11_2_4, all_28_0_10) % 16.09/4.56 | (100) occurrence_of(all_28_0_10, tptp0) % 16.09/4.56 | % 16.09/4.56 | Instantiating (85) with all_32_0_12, all_32_1_13 yields: % 16.09/4.56 | (101) subactivity(all_32_0_12, tptp0) & subactivity(all_32_1_13, tptp0) & atocc(all_11_1_3, all_32_0_12) & atocc(all_11_2_4, all_32_1_13) % 16.09/4.56 | % 16.09/4.56 | Applying alpha-rule on (101) yields: % 16.09/4.56 | (102) subactivity(all_32_0_12, tptp0) % 16.09/4.56 | (103) subactivity(all_32_1_13, tptp0) % 16.09/4.56 | (104) atocc(all_11_1_3, all_32_0_12) % 16.09/4.56 | (105) atocc(all_11_2_4, all_32_1_13) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (58) with all_26_0_9, tptp0, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_26_0_9), occurrence_of(all_0_0_0, tptp0), yields: % 16.09/4.56 | (106) all_26_0_9 = tptp0 % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (13) with all_24_0_8, all_0_0_0, all_11_2_4, all_9_0_1 and discharging atoms root_occ(all_11_2_4, all_0_0_0), root_occ(all_9_0_1, all_0_0_0), occurrence_of(all_0_0_0, all_24_0_8), yields: % 16.09/4.56 | (107) all_11_2_4 = all_9_0_1 % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (58) with all_24_0_8, all_26_0_9, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_26_0_9), occurrence_of(all_0_0_0, all_24_0_8), yields: % 16.09/4.56 | (108) all_26_0_9 = all_24_0_8 % 16.09/4.56 | % 16.09/4.56 | Combining equations (106,108) yields a new equation: % 16.09/4.56 | (109) all_24_0_8 = tptp0 % 16.09/4.56 | % 16.09/4.56 | From (107) and (83) follows: % 16.09/4.56 | (110) activity_occurrence(all_9_0_1) % 16.09/4.56 | % 16.09/4.56 | From (107) and (105) follows: % 16.09/4.56 | (111) atocc(all_9_0_1, all_32_1_13) % 16.09/4.56 | % 16.09/4.56 | From (107) and (99) follows: % 16.09/4.56 | (112) subactivity_occurrence(all_9_0_1, all_28_0_10) % 16.09/4.56 | % 16.09/4.56 | From (107)(109) and (92) follows: % 16.09/4.56 | (68) root(all_9_0_1, tptp0) % 16.09/4.56 | % 16.09/4.56 | From (107) and (72) follows: % 16.09/4.56 | (78) root_occ(all_9_0_1, all_0_0_0) % 16.09/4.56 | % 16.09/4.56 | From (107) and (70) follows: % 16.09/4.56 | (115) occurrence_of(all_9_0_1, tptp3) % 16.09/4.56 | % 16.09/4.56 | From (107) and (84) follows: % 16.09/4.56 | (116) min_precedes(all_9_0_1, all_11_0_2, tptp0) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (42) with tptp3 and discharging atoms activity(tptp3), yields: % 16.09/4.56 | (117) subactivity(tptp3, tptp3) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (49) with all_9_0_1 and discharging atoms activity_occurrence(all_9_0_1), yields: % 16.09/4.56 | (118) ? [v0] : (activity(v0) & occurrence_of(all_9_0_1, v0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (36) with all_32_1_13, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_32_1_13), yields: % 16.09/4.56 | (119) ? [v0] : (subactivity(all_32_1_13, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (36) with all_22_0_7, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_22_0_7), yields: % 16.09/4.56 | (120) ? [v0] : (subactivity(all_22_0_7, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (20) with all_32_1_13, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_32_1_13), legal(all_9_0_1), yields: % 16.09/4.56 | (121) root(all_9_0_1, all_32_1_13) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (20) with all_22_0_7, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_22_0_7), legal(all_9_0_1), yields: % 16.09/4.56 | (122) root(all_9_0_1, all_22_0_7) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (52) with tptp0, all_28_0_10, all_9_0_1 and discharging atoms subactivity_occurrence(all_9_0_1, all_28_0_10), root(all_9_0_1, tptp0), occurrence_of(all_28_0_10, tptp0), yields: % 16.09/4.56 | (123) root_occ(all_9_0_1, all_28_0_10) % 16.09/4.56 | % 16.09/4.56 | Instantiating formula (44) with all_28_0_10 and discharging atoms occurrence_of(all_28_0_10, tptp0), yields: % 16.09/4.56 | (124) ? [v0] : ? [v1] : ? [v2] : (root_occ(v0, all_28_0_10) & 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, tptp1) | occurrence_of(v2, tptp2))) % 16.09/4.57 | % 16.09/4.57 | Instantiating formula (34) with all_28_0_10, tptp0 and discharging atoms occurrence_of(all_28_0_10, tptp0), yields: % 16.09/4.57 | (125) activity_occurrence(all_28_0_10) % 16.09/4.57 | % 16.09/4.57 | Instantiating formula (5) with all_28_0_10, tptp0 and discharging atoms occurrence_of(all_28_0_10, tptp0), ~ atomic(tptp0), yields: % 16.09/4.57 | (126) ? [v0] : (subactivity_occurrence(v0, all_28_0_10) & root(v0, tptp0)) % 16.09/4.57 | % 16.09/4.57 | Instantiating formula (46) with all_11_0_2, all_9_0_1, tptp0 and discharging atoms min_precedes(all_9_0_1, all_11_0_2, tptp0), yields: % 16.09/4.57 | (127) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_11_0_2, v1) & atocc(all_9_0_1, v0)) % 16.09/4.57 | % 16.09/4.57 | Instantiating (124) with all_44_0_14, all_44_1_15, all_44_2_16 yields: % 16.09/4.57 | (128) root_occ(all_44_2_16, all_28_0_10) & occurrence_of(all_44_1_15, tptp4) & occurrence_of(all_44_2_16, tptp3) & min_precedes(all_44_1_15, all_44_0_14, tptp0) & min_precedes(all_44_2_16, all_44_1_15, tptp0) & ! [v0] : (v0 = all_44_0_14 | v0 = all_44_1_15 | ~ min_precedes(all_44_2_16, v0, tptp0)) & (occurrence_of(all_44_0_14, tptp1) | occurrence_of(all_44_0_14, tptp2)) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (128) yields: % 16.22/4.57 | (129) min_precedes(all_44_1_15, all_44_0_14, tptp0) % 16.22/4.57 | (130) occurrence_of(all_44_0_14, tptp1) | occurrence_of(all_44_0_14, tptp2) % 16.22/4.57 | (131) root_occ(all_44_2_16, all_28_0_10) % 16.22/4.57 | (132) occurrence_of(all_44_1_15, tptp4) % 16.22/4.57 | (133) ! [v0] : (v0 = all_44_0_14 | v0 = all_44_1_15 | ~ min_precedes(all_44_2_16, v0, tptp0)) % 16.22/4.57 | (134) occurrence_of(all_44_2_16, tptp3) % 16.22/4.57 | (135) min_precedes(all_44_2_16, all_44_1_15, tptp0) % 16.22/4.57 | % 16.22/4.57 | Instantiating (120) with all_47_0_17 yields: % 16.22/4.57 | (136) subactivity(all_22_0_7, all_47_0_17) & atomic(all_47_0_17) & occurrence_of(all_9_0_1, all_47_0_17) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (136) yields: % 16.22/4.57 | (137) subactivity(all_22_0_7, all_47_0_17) % 16.22/4.57 | (138) atomic(all_47_0_17) % 16.22/4.57 | (139) occurrence_of(all_9_0_1, all_47_0_17) % 16.22/4.57 | % 16.22/4.57 | Instantiating (119) with all_49_0_18 yields: % 16.22/4.57 | (140) subactivity(all_32_1_13, all_49_0_18) & atomic(all_49_0_18) & occurrence_of(all_9_0_1, all_49_0_18) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (140) yields: % 16.22/4.57 | (141) subactivity(all_32_1_13, all_49_0_18) % 16.22/4.57 | (142) atomic(all_49_0_18) % 16.22/4.57 | (143) occurrence_of(all_9_0_1, all_49_0_18) % 16.22/4.57 | % 16.22/4.57 | Instantiating (126) with all_55_0_21 yields: % 16.22/4.57 | (144) subactivity_occurrence(all_55_0_21, all_28_0_10) & root(all_55_0_21, tptp0) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (144) yields: % 16.22/4.57 | (145) subactivity_occurrence(all_55_0_21, all_28_0_10) % 16.22/4.57 | (146) root(all_55_0_21, tptp0) % 16.22/4.57 | % 16.22/4.57 | Instantiating (118) with all_57_0_22 yields: % 16.22/4.57 | (147) activity(all_57_0_22) & occurrence_of(all_9_0_1, all_57_0_22) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (147) yields: % 16.22/4.57 | (148) activity(all_57_0_22) % 16.22/4.57 | (149) occurrence_of(all_9_0_1, all_57_0_22) % 16.22/4.57 | % 16.22/4.57 | Instantiating (127) with all_70_0_30, all_70_1_31 yields: % 16.22/4.57 | (150) subactivity(all_70_0_30, tptp0) & subactivity(all_70_1_31, tptp0) & atocc(all_11_0_2, all_70_0_30) & atocc(all_9_0_1, all_70_1_31) % 16.22/4.57 | % 16.22/4.57 | Applying alpha-rule on (150) yields: % 16.22/4.57 | (151) subactivity(all_70_0_30, tptp0) % 16.22/4.57 | (152) subactivity(all_70_1_31, tptp0) % 16.22/4.57 | (153) atocc(all_11_0_2, all_70_0_30) % 16.22/4.57 | (154) atocc(all_9_0_1, all_70_1_31) % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (13) with tptp0, all_28_0_10, all_9_0_1, all_44_2_16 and discharging atoms root_occ(all_44_2_16, all_28_0_10), root_occ(all_9_0_1, all_28_0_10), occurrence_of(all_28_0_10, tptp0), yields: % 16.22/4.57 | (155) all_44_2_16 = all_9_0_1 % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (58) with all_57_0_22, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_57_0_22), occurrence_of(all_9_0_1, tptp3), yields: % 16.22/4.57 | (156) all_57_0_22 = tptp3 % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (58) with all_49_0_18, all_57_0_22, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_57_0_22), occurrence_of(all_9_0_1, all_49_0_18), yields: % 16.22/4.57 | (157) all_57_0_22 = all_49_0_18 % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (58) with all_47_0_17, all_57_0_22, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_57_0_22), occurrence_of(all_9_0_1, all_47_0_17), yields: % 16.22/4.57 | (158) all_57_0_22 = all_47_0_17 % 16.22/4.57 | % 16.22/4.57 | Combining equations (156,157) yields a new equation: % 16.22/4.57 | (159) all_49_0_18 = tptp3 % 16.22/4.57 | % 16.22/4.57 | Combining equations (158,157) yields a new equation: % 16.22/4.57 | (160) all_49_0_18 = all_47_0_17 % 16.22/4.57 | % 16.22/4.57 | Combining equations (160,159) yields a new equation: % 16.22/4.57 | (161) all_47_0_17 = tptp3 % 16.22/4.57 | % 16.22/4.57 | Simplifying 161 yields: % 16.22/4.57 | (162) all_47_0_17 = tptp3 % 16.22/4.57 | % 16.22/4.57 | From (162) and (138) follows: % 16.22/4.57 | (10) atomic(tptp3) % 16.22/4.57 | % 16.22/4.57 | From (155) and (131) follows: % 16.22/4.57 | (123) root_occ(all_9_0_1, all_28_0_10) % 16.22/4.57 | % 16.22/4.57 | From (162) and (139) follows: % 16.22/4.57 | (115) occurrence_of(all_9_0_1, tptp3) % 16.22/4.57 | % 16.22/4.57 | From (155) and (135) follows: % 16.22/4.57 | (166) min_precedes(all_9_0_1, all_44_1_15, tptp0) % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (49) with all_28_0_10 and discharging atoms activity_occurrence(all_28_0_10), yields: % 16.22/4.57 | (167) ? [v0] : (activity(v0) & occurrence_of(all_28_0_10, v0)) % 16.22/4.57 | % 16.22/4.57 | Instantiating formula (24) with tptp3, tptp3, all_9_0_1 and discharging atoms subactivity(tptp3, tptp3), atomic(tptp3), occurrence_of(all_9_0_1, tptp3), yields: % 16.22/4.58 | (168) atocc(all_9_0_1, tptp3) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with all_70_1_31, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_70_1_31), yields: % 16.22/4.58 | (169) ? [v0] : (subactivity(all_70_1_31, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (52) with tptp0, all_28_0_10, all_55_0_21 and discharging atoms subactivity_occurrence(all_55_0_21, all_28_0_10), root(all_55_0_21, tptp0), occurrence_of(all_28_0_10, tptp0), yields: % 16.22/4.58 | (170) root_occ(all_55_0_21, all_28_0_10) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (45) with all_55_0_21, tptp0 and discharging atoms root(all_55_0_21, tptp0), yields: % 16.22/4.58 | (171) ? [v0] : (subactivity(v0, tptp0) & atocc(all_55_0_21, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (45) with all_9_0_1, all_32_1_13 and discharging atoms root(all_9_0_1, all_32_1_13), yields: % 16.22/4.58 | (172) ? [v0] : (subactivity(v0, all_32_1_13) & atocc(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (45) with all_9_0_1, all_22_0_7 and discharging atoms root(all_9_0_1, all_22_0_7), yields: % 16.22/4.58 | (173) ? [v0] : (subactivity(v0, all_22_0_7) & atocc(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (46) with all_44_1_15, all_9_0_1, tptp0 and discharging atoms min_precedes(all_9_0_1, all_44_1_15, tptp0), yields: % 16.22/4.58 | (174) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_44_1_15, v1) & atocc(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating (167) with all_82_0_32 yields: % 16.22/4.58 | (175) activity(all_82_0_32) & occurrence_of(all_28_0_10, all_82_0_32) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (175) yields: % 16.22/4.58 | (176) activity(all_82_0_32) % 16.22/4.58 | (177) occurrence_of(all_28_0_10, all_82_0_32) % 16.22/4.58 | % 16.22/4.58 | Instantiating (174) with all_86_0_34, all_86_1_35 yields: % 16.22/4.58 | (178) subactivity(all_86_0_34, tptp0) & subactivity(all_86_1_35, tptp0) & atocc(all_44_1_15, all_86_0_34) & atocc(all_9_0_1, all_86_1_35) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (178) yields: % 16.22/4.58 | (179) subactivity(all_86_0_34, tptp0) % 16.22/4.58 | (180) subactivity(all_86_1_35, tptp0) % 16.22/4.58 | (181) atocc(all_44_1_15, all_86_0_34) % 16.22/4.58 | (182) atocc(all_9_0_1, all_86_1_35) % 16.22/4.58 | % 16.22/4.58 | Instantiating (171) with all_90_0_37 yields: % 16.22/4.58 | (183) subactivity(all_90_0_37, tptp0) & atocc(all_55_0_21, all_90_0_37) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (183) yields: % 16.22/4.58 | (184) subactivity(all_90_0_37, tptp0) % 16.22/4.58 | (185) atocc(all_55_0_21, all_90_0_37) % 16.22/4.58 | % 16.22/4.58 | Instantiating (173) with all_107_0_49 yields: % 16.22/4.58 | (186) subactivity(all_107_0_49, all_22_0_7) & atocc(all_9_0_1, all_107_0_49) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (186) yields: % 16.22/4.58 | (187) subactivity(all_107_0_49, all_22_0_7) % 16.22/4.58 | (188) atocc(all_9_0_1, all_107_0_49) % 16.22/4.58 | % 16.22/4.58 | Instantiating (172) with all_115_0_54 yields: % 16.22/4.58 | (189) subactivity(all_115_0_54, all_32_1_13) & atocc(all_9_0_1, all_115_0_54) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (189) yields: % 16.22/4.58 | (190) subactivity(all_115_0_54, all_32_1_13) % 16.22/4.58 | (191) atocc(all_9_0_1, all_115_0_54) % 16.22/4.58 | % 16.22/4.58 | Instantiating (169) with all_119_0_56 yields: % 16.22/4.58 | (192) subactivity(all_70_1_31, all_119_0_56) & atomic(all_119_0_56) & occurrence_of(all_9_0_1, all_119_0_56) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (192) yields: % 16.22/4.58 | (193) subactivity(all_70_1_31, all_119_0_56) % 16.22/4.58 | (194) atomic(all_119_0_56) % 16.22/4.58 | (195) occurrence_of(all_9_0_1, all_119_0_56) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (13) with all_82_0_32, all_28_0_10, all_9_0_1, all_55_0_21 and discharging atoms root_occ(all_55_0_21, all_28_0_10), root_occ(all_9_0_1, all_28_0_10), occurrence_of(all_28_0_10, all_82_0_32), yields: % 16.22/4.58 | (196) all_55_0_21 = all_9_0_1 % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (58) with all_119_0_56, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_119_0_56), occurrence_of(all_9_0_1, tptp3), yields: % 16.22/4.58 | (197) all_119_0_56 = tptp3 % 16.22/4.58 | % 16.22/4.58 | From (196) and (185) follows: % 16.22/4.58 | (198) atocc(all_9_0_1, all_90_0_37) % 16.22/4.58 | % 16.22/4.58 | From (197) and (195) follows: % 16.22/4.58 | (115) occurrence_of(all_9_0_1, tptp3) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with all_115_0_54, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_115_0_54), yields: % 16.22/4.58 | (200) ? [v0] : (subactivity(all_115_0_54, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with all_107_0_49, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_107_0_49), yields: % 16.22/4.58 | (201) ? [v0] : (subactivity(all_107_0_49, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with all_90_0_37, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_90_0_37), yields: % 16.22/4.58 | (202) ? [v0] : (subactivity(all_90_0_37, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with all_86_1_35, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_86_1_35), yields: % 16.22/4.58 | (203) ? [v0] : (subactivity(all_86_1_35, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating formula (36) with tptp3, all_9_0_1 and discharging atoms atocc(all_9_0_1, tptp3), yields: % 16.22/4.58 | (204) ? [v0] : (subactivity(tptp3, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 16.22/4.58 | % 16.22/4.58 | Instantiating (203) with all_139_0_61 yields: % 16.22/4.58 | (205) subactivity(all_86_1_35, all_139_0_61) & atomic(all_139_0_61) & occurrence_of(all_9_0_1, all_139_0_61) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (205) yields: % 16.22/4.58 | (206) subactivity(all_86_1_35, all_139_0_61) % 16.22/4.58 | (207) atomic(all_139_0_61) % 16.22/4.58 | (208) occurrence_of(all_9_0_1, all_139_0_61) % 16.22/4.58 | % 16.22/4.58 | Instantiating (201) with all_141_0_62 yields: % 16.22/4.58 | (209) subactivity(all_107_0_49, all_141_0_62) & atomic(all_141_0_62) & occurrence_of(all_9_0_1, all_141_0_62) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (209) yields: % 16.22/4.58 | (210) subactivity(all_107_0_49, all_141_0_62) % 16.22/4.58 | (211) atomic(all_141_0_62) % 16.22/4.58 | (212) occurrence_of(all_9_0_1, all_141_0_62) % 16.22/4.58 | % 16.22/4.58 | Instantiating (200) with all_159_0_72 yields: % 16.22/4.58 | (213) subactivity(all_115_0_54, all_159_0_72) & atomic(all_159_0_72) & occurrence_of(all_9_0_1, all_159_0_72) % 16.22/4.58 | % 16.22/4.58 | Applying alpha-rule on (213) yields: % 16.22/4.59 | (214) subactivity(all_115_0_54, all_159_0_72) % 16.22/4.59 | (215) atomic(all_159_0_72) % 16.22/4.59 | (216) occurrence_of(all_9_0_1, all_159_0_72) % 16.22/4.59 | % 16.22/4.59 | Instantiating (202) with all_176_0_84 yields: % 16.22/4.59 | (217) subactivity(all_90_0_37, all_176_0_84) & atomic(all_176_0_84) & occurrence_of(all_9_0_1, all_176_0_84) % 16.22/4.59 | % 16.22/4.59 | Applying alpha-rule on (217) yields: % 16.22/4.59 | (218) subactivity(all_90_0_37, all_176_0_84) % 16.22/4.59 | (219) atomic(all_176_0_84) % 16.22/4.59 | (220) occurrence_of(all_9_0_1, all_176_0_84) % 16.22/4.59 | % 16.22/4.59 | Instantiating (204) with all_199_0_97 yields: % 16.22/4.59 | (221) subactivity(tptp3, all_199_0_97) & atomic(all_199_0_97) & occurrence_of(all_9_0_1, all_199_0_97) % 16.22/4.59 | % 16.22/4.59 | Applying alpha-rule on (221) yields: % 16.22/4.59 | (222) subactivity(tptp3, all_199_0_97) % 16.22/4.59 | (223) atomic(all_199_0_97) % 16.22/4.59 | (224) occurrence_of(all_9_0_1, all_199_0_97) % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (58) with all_176_0_84, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_176_0_84), occurrence_of(all_9_0_1, tptp3), yields: % 16.22/4.59 | (225) all_176_0_84 = tptp3 % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (58) with all_176_0_84, all_199_0_97, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_199_0_97), occurrence_of(all_9_0_1, all_176_0_84), yields: % 16.22/4.59 | (226) all_199_0_97 = all_176_0_84 % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (58) with all_159_0_72, all_176_0_84, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_176_0_84), occurrence_of(all_9_0_1, all_159_0_72), yields: % 16.22/4.59 | (227) all_176_0_84 = all_159_0_72 % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (58) with all_141_0_62, all_176_0_84, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_176_0_84), occurrence_of(all_9_0_1, all_141_0_62), yields: % 16.22/4.59 | (228) all_176_0_84 = all_141_0_62 % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (58) with all_139_0_61, all_199_0_97, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_199_0_97), occurrence_of(all_9_0_1, all_139_0_61), yields: % 16.22/4.59 | (229) all_199_0_97 = all_139_0_61 % 16.22/4.59 | % 16.22/4.59 | Combining equations (226,229) yields a new equation: % 16.22/4.59 | (230) all_176_0_84 = all_139_0_61 % 16.22/4.59 | % 16.22/4.59 | Simplifying 230 yields: % 16.22/4.59 | (231) all_176_0_84 = all_139_0_61 % 16.22/4.59 | % 16.22/4.59 | Combining equations (228,227) yields a new equation: % 16.22/4.59 | (232) all_159_0_72 = all_141_0_62 % 16.22/4.59 | % 16.22/4.59 | Combining equations (225,227) yields a new equation: % 16.22/4.59 | (233) all_159_0_72 = tptp3 % 16.22/4.59 | % 16.22/4.59 | Combining equations (231,227) yields a new equation: % 16.22/4.59 | (234) all_159_0_72 = all_139_0_61 % 16.22/4.59 | % 16.22/4.59 | Combining equations (233,232) yields a new equation: % 16.22/4.59 | (235) all_141_0_62 = tptp3 % 16.22/4.59 | % 16.22/4.59 | Combining equations (234,232) yields a new equation: % 16.22/4.59 | (236) all_141_0_62 = all_139_0_61 % 16.22/4.59 | % 16.22/4.59 | Combining equations (235,236) yields a new equation: % 16.22/4.59 | (237) all_139_0_61 = tptp3 % 16.22/4.59 | % 16.22/4.59 | From (237) and (208) follows: % 16.22/4.59 | (115) occurrence_of(all_9_0_1, tptp3) % 16.22/4.59 | % 16.22/4.59 +-Applying beta-rule and splitting (71), into two cases. % 16.22/4.59 |-Branch one: % 16.22/4.59 | (239) occurrence_of(all_11_0_2, tptp1) % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (6) with all_11_0_2, all_9_0_1 and discharging atoms root_occ(all_9_0_1, all_0_0_0), occurrence_of(all_11_0_2, tptp1), occurrence_of(all_9_0_1, tptp3), min_precedes(all_9_0_1, all_11_0_2, tptp0), yields: % 16.22/4.59 | (240) $false % 16.22/4.59 | % 16.22/4.59 |-The branch is then unsatisfiable % 16.22/4.59 |-Branch two: % 16.22/4.59 | (241) ~ occurrence_of(all_11_0_2, tptp1) % 16.22/4.59 | (242) occurrence_of(all_11_0_2, tptp2) % 16.22/4.59 | % 16.22/4.59 | Instantiating formula (29) with all_11_0_2, all_9_0_1 and discharging atoms root_occ(all_9_0_1, all_0_0_0), occurrence_of(all_11_0_2, tptp2), occurrence_of(all_9_0_1, tptp3), min_precedes(all_9_0_1, all_11_0_2, tptp0), yields: % 16.22/4.59 | (240) $false % 16.22/4.59 | % 16.22/4.59 |-The branch is then unsatisfiable % 16.22/4.59 % SZS output end Proof for theBenchmark % 16.22/4.59 % 16.22/4.59 3942ms %------------------------------------------------------------------------------