%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n027.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:56 EDT 2022 % Result : Theorem 12.86s 3.75s % Output : Proof 14.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 03:33:16 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.58 ____ _ % 0.18/0.58 ___ / __ \_____(_)___ ________ __________ % 0.18/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.18/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.18/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.18/0.58 % 0.18/0.58 A Theorem Prover for First-Order Logic % 0.18/0.58 (ePrincess v.1.0) % 0.18/0.58 % 0.18/0.58 (c) Philipp Rümmer, 2009-2015 % 0.18/0.58 (c) Peter Backeman, 2014-2015 % 0.18/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.18/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.18/0.58 Bug reports to peter@backeman.se % 0.18/0.58 % 0.18/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.18/0.58 % 0.18/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.64/0.96 Prover 0: Preprocessing ... % 1.99/1.18 Prover 0: Constructing countermodel ... % 12.86/3.75 Prover 0: proved (3121ms) % 12.86/3.75 % 12.86/3.75 No countermodel exists, formula is valid % 12.86/3.75 % SZS status Theorem for theBenchmark % 12.86/3.75 % 12.86/3.75 Generating proof ... found it (size 76) % 14.48/4.09 % 14.48/4.09 % SZS output start Proof for theBenchmark % 14.52/4.09 Assumed formulas after preprocessing and simplification: % 14.52/4.09 | (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(v2, v0) | ~ root_occ(v1, v0) | ~ occurrence_of(v2, tptp1) | ~ occurrence_of(v1, tptp3) | ~ min_precedes(v1, v2, tptp0)) & ! [v1] : ! [v2] : ( ~ leaf_occ(v2, v0) | ~ root_occ(v1, v0) | ~ occurrence_of(v2, tptp2) | ~ occurrence_of(v1, tptp3) | ~ min_precedes(v1, v2, tptp0)) & ! [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] : ( ~ 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] : (next_subocc(v3, v4, tptp0) & next_subocc(v2, v3, tptp0) & leaf_occ(v4, v1) & root_occ(v2, v1) & occurrence_of(v3, tptp4) & occurrence_of(v2, tptp3) & (occurrence_of(v4, tptp1) | occurrence_of(v4, tptp2))))) % 14.63/4.11 | Instantiating (0) with all_0_0_0 yields: % 14.63/4.11 | (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(v1, all_0_0_0) | ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) & ! [v0] : ! [v1] : ( ~ leaf_occ(v1, all_0_0_0) | ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) & ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) & ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) & ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) & ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) & ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) & ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) & ! [v0] : ( ~ legal(v0) | arboreal(v0)) & ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : ? [v3] : (next_subocc(v2, v3, tptp0) & next_subocc(v1, v2, tptp0) & leaf_occ(v3, v0) & root_occ(v1, v0) & occurrence_of(v2, tptp4) & occurrence_of(v1, tptp3) & (occurrence_of(v3, tptp1) | occurrence_of(v3, tptp2)))) % 14.63/4.12 | % 14.63/4.12 | Applying alpha-rule on (1) yields: % 14.63/4.12 | (2) activity(tptp0) % 14.63/4.12 | (3) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity(v0)) % 14.63/4.12 | (4) atomic(tptp1) % 14.63/4.12 | (5) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | atomic(v0) | ? [v2] : (subactivity_occurrence(v2, v1) & root(v2, v0))) % 14.63/4.12 | (6) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | earlier(v0, v1)) % 14.63/4.12 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ earlier(v1, v2) | ~ earlier(v0, v1) | earlier(v0, v2)) % 14.63/4.12 | (8) ! [v0] : ! [v1] : ( ~ leaf_occ(v1, all_0_0_0) | ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp2) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) % 14.63/4.12 | (9) atomic(tptp3) % 14.63/4.12 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ next_subocc(v0, v1, v2) | ~ min_precedes(v3, v1, v2) | ~ min_precedes(v0, v3, v2)) % 14.63/4.12 | (11) atomic(tptp2) % 14.63/4.12 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ root_occ(v1, v2) | ~ root_occ(v0, v2) | ~ occurrence_of(v2, v3)) % 14.63/4.12 | (13) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | atomic(v1) | ? [v2] : (leaf_occ(v0, v2) & occurrence_of(v2, v1))) % 14.63/4.12 | (14) ! [v0] : ! [v1] : ( ~ root(v0, v1) | leaf(v0, v1) | ? [v2] : min_precedes(v0, v2, v1)) % 14.63/4.12 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | precedes(v0, v1)) % 14.63/4.13 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v0)) % 14.63/4.13 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v2, v0, v1) | leaf(v0, v1) | ? [v3] : min_precedes(v0, v3, v1)) % 14.63/4.13 | (18) ! [v0] : ! [v1] : ( ~ leaf_occ(v0, v1) | ? [v2] : (leaf(v0, v2) & subactivity_occurrence(v0, v1) & occurrence_of(v1, v2))) % 14.63/4.13 | (19) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ~ legal(v0) | root(v0, v1)) % 14.63/4.13 | (20) ! [v0] : ! [v1] : ( ~ earlier(v1, v0) | ~ earlier(v0, v1)) % 14.63/4.13 | (21) atomic(tptp4) % 14.63/4.13 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ leaf_occ(v1, v2) | ~ leaf_occ(v0, v2) | ~ occurrence_of(v2, v3) | atomic(v3)) % 14.63/4.13 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity(v1, v2) | ~ atomic(v2) | ~ occurrence_of(v0, v2) | atocc(v0, v1)) % 14.63/4.13 | (24) ! [v0] : ! [v1] : ( ~ precedes(v0, v1) | legal(v1)) % 14.63/4.13 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ leaf_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v1, v3, v2)) % 14.63/4.13 | (26) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v1) | ~ min_precedes(v0, v2, v1)) % 14.63/4.13 | (27) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v0)) % 14.63/4.13 | (28) occurrence_of(all_0_0_0, tptp0) % 14.63/4.13 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | arboreal(v1)) % 14.63/4.13 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v0, v1, v2) | next_subocc(v0, v1, v2) | ? [v3] : (min_precedes(v3, v1, v2) & min_precedes(v0, v3, v2))) % 14.63/4.13 | (31) ! [v0] : ! [v1] : ( ~ subactivity_occurrence(v0, v1) | activity_occurrence(v1)) % 14.63/4.13 | (32) ! [v0] : ! [v1] : ( ~ leaf_occ(v1, all_0_0_0) | ~ root_occ(v0, all_0_0_0) | ~ occurrence_of(v1, tptp1) | ~ occurrence_of(v0, tptp3) | ~ min_precedes(v0, v1, tptp0)) % 14.63/4.13 | (33) ! [v0] : ! [v1] : ! [v2] : ( ~ leaf(v0, v2) | ~ subactivity_occurrence(v0, v1) | ~ occurrence_of(v1, v2) | leaf_occ(v0, v1)) % 14.63/4.13 | (34) ! [v0] : ! [v1] : ( ~ occurrence_of(v1, v0) | activity_occurrence(v1)) % 14.63/4.13 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : (subactivity_occurrence(v2, v3) & subactivity_occurrence(v1, v3) & occurrence_of(v3, v0))) % 14.63/4.13 | (36) ! [v0] : ! [v1] : ( ~ atocc(v0, v1) | ? [v2] : (subactivity(v1, v2) & atomic(v2) & occurrence_of(v0, v2))) % 14.63/4.13 | (37) ~ (tptp1 = tptp2) % 14.63/4.13 | (38) ! [v0] : ! [v1] : ( ~ atomic(v1) | ~ occurrence_of(v0, v1) | arboreal(v0)) % 14.63/4.13 | (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)) % 14.63/4.13 | (40) ~ (tptp1 = tptp4) % 14.63/4.13 | (41) ! [v0] : ! [v1] : ( ~ root_occ(v0, v1) | ? [v2] : (subactivity_occurrence(v0, v1) & root(v0, v2) & occurrence_of(v1, v2))) % 14.63/4.13 | (42) ! [v0] : ( ~ activity(v0) | subactivity(v0, v0)) % 14.63/4.13 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ min_precedes(v1, v2, v3) | ~ min_precedes(v0, v1, v3) | min_precedes(v0, v2, v3)) % 14.63/4.13 | (44) ! [v0] : ! [v1] : ( ~ root(v1, v0) | ? [v2] : (subactivity(v2, v0) & atocc(v1, v2))) % 14.63/4.13 | (45) ! [v0] : ! [v1] : ! [v2] : ( ~ min_precedes(v1, v2, v0) | ? [v3] : ? [v4] : (subactivity(v4, v0) & subactivity(v3, v0) & atocc(v2, v4) & atocc(v1, v3))) % 14.63/4.13 | (46) ! [v0] : ! [v1] : ( ~ root(v0, v1) | legal(v0)) % 14.63/4.13 | (47) ! [v0] : ! [v1] : ( ~ legal(v1) | ~ earlier(v0, v1) | precedes(v0, v1)) % 14.63/4.13 | (48) ! [v0] : ( ~ activity_occurrence(v0) | ? [v1] : (activity(v1) & occurrence_of(v0, v1))) % 14.63/4.13 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ root(v1, v2) | ~ min_precedes(v0, v1, v2)) % 14.63/4.13 | (50) ~ (tptp1 = tptp3) % 14.63/4.13 | (51) ! [v0] : ! [v1] : ! [v2] : ( ~ subactivity_occurrence(v0, v1) | ~ root(v0, v2) | ~ occurrence_of(v1, v2) | root_occ(v0, v1)) % 14.63/4.13 | (52) ! [v0] : ( ~ legal(v0) | arboreal(v0)) % 14.63/4.13 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ root_occ(v1, v0) | ~ occurrence_of(v0, v2) | ~ min_precedes(v3, v1, v2)) % 14.63/4.13 | (54) ! [v0] : ! [v1] : ( ~ leaf(v0, v1) | root(v0, v1) | ? [v2] : min_precedes(v2, v0, v1)) % 14.63/4.13 | (55) ! [v0] : ! [v1] : ( ~ arboreal(v0) | ~ occurrence_of(v0, v1) | atomic(v1)) % 14.63/4.13 | (56) ~ (tptp2 = tptp3) % 14.63/4.13 | (57) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ occurrence_of(v0, v2) | ~ occurrence_of(v0, v1)) % 14.63/4.13 | (58) ! [v0] : ! [v1] : ! [v2] : ( ~ next_subocc(v0, v1, v2) | min_precedes(v0, v1, v2)) % 14.63/4.14 | (59) ! [v0] : ( ~ occurrence_of(v0, tptp0) | ? [v1] : ? [v2] : ? [v3] : (next_subocc(v2, v3, tptp0) & next_subocc(v1, v2, tptp0) & leaf_occ(v3, v0) & root_occ(v1, v0) & occurrence_of(v2, tptp4) & occurrence_of(v1, tptp3) & (occurrence_of(v3, tptp1) | occurrence_of(v3, tptp2)))) % 14.63/4.14 | (60) ~ (tptp2 = tptp4) % 14.63/4.14 | (61) ~ (tptp4 = tptp3) % 14.63/4.14 | (62) ~ atomic(tptp0) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (59) with all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, tptp0), yields: % 14.63/4.14 | (63) ? [v0] : ? [v1] : ? [v2] : (next_subocc(v1, v2, tptp0) & next_subocc(v0, v1, tptp0) & leaf_occ(v2, all_0_0_0) & root_occ(v0, all_0_0_0) & occurrence_of(v1, tptp4) & occurrence_of(v0, tptp3) & (occurrence_of(v2, tptp1) | occurrence_of(v2, tptp2))) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (5) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0), ~ atomic(tptp0), yields: % 14.63/4.14 | (64) ? [v0] : (subactivity_occurrence(v0, all_0_0_0) & root(v0, tptp0)) % 14.63/4.14 | % 14.63/4.14 | Instantiating (64) with all_9_0_1 yields: % 14.63/4.14 | (65) subactivity_occurrence(all_9_0_1, all_0_0_0) & root(all_9_0_1, tptp0) % 14.63/4.14 | % 14.63/4.14 | Applying alpha-rule on (65) yields: % 14.63/4.14 | (66) subactivity_occurrence(all_9_0_1, all_0_0_0) % 14.63/4.14 | (67) root(all_9_0_1, tptp0) % 14.63/4.14 | % 14.63/4.14 | Instantiating (63) with all_11_0_2, all_11_1_3, all_11_2_4 yields: % 14.63/4.14 | (68) next_subocc(all_11_1_3, all_11_0_2, tptp0) & next_subocc(all_11_2_4, all_11_1_3, tptp0) & leaf_occ(all_11_0_2, all_0_0_0) & root_occ(all_11_2_4, all_0_0_0) & occurrence_of(all_11_1_3, tptp4) & occurrence_of(all_11_2_4, tptp3) & (occurrence_of(all_11_0_2, tptp1) | occurrence_of(all_11_0_2, tptp2)) % 14.63/4.14 | % 14.63/4.14 | Applying alpha-rule on (68) yields: % 14.63/4.14 | (69) next_subocc(all_11_2_4, all_11_1_3, tptp0) % 14.63/4.14 | (70) leaf_occ(all_11_0_2, all_0_0_0) % 14.63/4.14 | (71) occurrence_of(all_11_1_3, tptp4) % 14.63/4.14 | (72) occurrence_of(all_11_2_4, tptp3) % 14.63/4.14 | (73) root_occ(all_11_2_4, all_0_0_0) % 14.63/4.14 | (74) next_subocc(all_11_1_3, all_11_0_2, tptp0) % 14.63/4.14 | (75) occurrence_of(all_11_0_2, tptp1) | occurrence_of(all_11_0_2, tptp2) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (51) 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: % 14.63/4.14 | (76) root_occ(all_9_0_1, all_0_0_0) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (44) with all_9_0_1, tptp0 and discharging atoms root(all_9_0_1, tptp0), yields: % 14.63/4.14 | (77) ? [v0] : (subactivity(v0, tptp0) & atocc(all_9_0_1, v0)) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (46) with tptp0, all_9_0_1 and discharging atoms root(all_9_0_1, tptp0), yields: % 14.63/4.14 | (78) legal(all_9_0_1) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (58) with tptp0, all_11_0_2, all_11_1_3 and discharging atoms next_subocc(all_11_1_3, all_11_0_2, tptp0), yields: % 14.63/4.14 | (79) min_precedes(all_11_1_3, all_11_0_2, tptp0) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (58) with tptp0, all_11_1_3, all_11_2_4 and discharging atoms next_subocc(all_11_2_4, all_11_1_3, tptp0), yields: % 14.63/4.14 | (80) min_precedes(all_11_2_4, all_11_1_3, tptp0) % 14.63/4.14 | % 14.63/4.14 | 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: % 14.63/4.14 | (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)) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (3) with all_11_2_4, tptp3 and discharging atoms occurrence_of(all_11_2_4, tptp3), yields: % 14.63/4.14 | (82) activity(tptp3) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (34) with all_11_2_4, tptp3 and discharging atoms occurrence_of(all_11_2_4, tptp3), yields: % 14.63/4.14 | (83) activity_occurrence(all_11_2_4) % 14.63/4.14 | % 14.63/4.14 | Instantiating (81) with all_19_0_5 yields: % 14.63/4.14 | (84) subactivity_occurrence(all_11_2_4, all_0_0_0) & root(all_11_2_4, all_19_0_5) & occurrence_of(all_0_0_0, all_19_0_5) % 14.63/4.14 | % 14.63/4.14 | Applying alpha-rule on (84) yields: % 14.63/4.14 | (85) subactivity_occurrence(all_11_2_4, all_0_0_0) % 14.63/4.14 | (86) root(all_11_2_4, all_19_0_5) % 14.63/4.14 | (87) occurrence_of(all_0_0_0, all_19_0_5) % 14.63/4.14 | % 14.63/4.14 | Instantiating (77) with all_21_0_6 yields: % 14.63/4.14 | (88) subactivity(all_21_0_6, tptp0) & atocc(all_9_0_1, all_21_0_6) % 14.63/4.14 | % 14.63/4.14 | Applying alpha-rule on (88) yields: % 14.63/4.14 | (89) subactivity(all_21_0_6, tptp0) % 14.63/4.14 | (90) atocc(all_9_0_1, all_21_0_6) % 14.63/4.14 | % 14.63/4.14 | Instantiating formula (12) with all_19_0_5, 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_19_0_5), yields: % 14.63/4.14 | (91) all_11_2_4 = all_9_0_1 % 14.63/4.14 | % 14.63/4.14 | From (91) and (83) follows: % 14.63/4.14 | (92) activity_occurrence(all_9_0_1) % 14.63/4.14 | % 14.63/4.14 | From (91) and (73) follows: % 14.63/4.14 | (76) root_occ(all_9_0_1, all_0_0_0) % 14.63/4.14 | % 14.63/4.14 | From (91) and (72) follows: % 14.63/4.15 | (94) occurrence_of(all_9_0_1, tptp3) % 14.63/4.15 | % 14.63/4.15 | From (91) and (80) follows: % 14.63/4.15 | (95) min_precedes(all_9_0_1, all_11_1_3, tptp0) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (42) with tptp3 and discharging atoms activity(tptp3), yields: % 14.63/4.15 | (96) subactivity(tptp3, tptp3) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (48) with all_9_0_1 and discharging atoms activity_occurrence(all_9_0_1), yields: % 14.63/4.15 | (97) ? [v0] : (activity(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (36) with all_21_0_6, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_21_0_6), yields: % 14.63/4.15 | (98) ? [v0] : (subactivity(all_21_0_6, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (19) with all_21_0_6, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_21_0_6), legal(all_9_0_1), yields: % 14.63/4.15 | (99) root(all_9_0_1, all_21_0_6) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (43) with tptp0, all_11_0_2, all_11_1_3, all_9_0_1 and discharging atoms min_precedes(all_11_1_3, all_11_0_2, tptp0), min_precedes(all_9_0_1, all_11_1_3, tptp0), yields: % 14.63/4.15 | (100) min_precedes(all_9_0_1, all_11_0_2, tptp0) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (45) with all_11_1_3, all_9_0_1, tptp0 and discharging atoms min_precedes(all_9_0_1, all_11_1_3, tptp0), yields: % 14.63/4.15 | (101) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_11_1_3, v1) & atocc(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating (98) with all_37_0_9 yields: % 14.63/4.15 | (102) subactivity(all_21_0_6, all_37_0_9) & atomic(all_37_0_9) & occurrence_of(all_9_0_1, all_37_0_9) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (102) yields: % 14.63/4.15 | (103) subactivity(all_21_0_6, all_37_0_9) % 14.63/4.15 | (104) atomic(all_37_0_9) % 14.63/4.15 | (105) occurrence_of(all_9_0_1, all_37_0_9) % 14.63/4.15 | % 14.63/4.15 | Instantiating (101) with all_45_0_14, all_45_1_15 yields: % 14.63/4.15 | (106) subactivity(all_45_0_14, tptp0) & subactivity(all_45_1_15, tptp0) & atocc(all_11_1_3, all_45_0_14) & atocc(all_9_0_1, all_45_1_15) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (106) yields: % 14.63/4.15 | (107) subactivity(all_45_0_14, tptp0) % 14.63/4.15 | (108) subactivity(all_45_1_15, tptp0) % 14.63/4.15 | (109) atocc(all_11_1_3, all_45_0_14) % 14.63/4.15 | (110) atocc(all_9_0_1, all_45_1_15) % 14.63/4.15 | % 14.63/4.15 | Instantiating (97) with all_49_0_17 yields: % 14.63/4.15 | (111) activity(all_49_0_17) & occurrence_of(all_9_0_1, all_49_0_17) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (111) yields: % 14.63/4.15 | (112) activity(all_49_0_17) % 14.63/4.15 | (113) occurrence_of(all_9_0_1, all_49_0_17) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (57) with all_49_0_17, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_49_0_17), occurrence_of(all_9_0_1, tptp3), yields: % 14.63/4.15 | (114) all_49_0_17 = tptp3 % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (57) with all_37_0_9, all_49_0_17, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_49_0_17), occurrence_of(all_9_0_1, all_37_0_9), yields: % 14.63/4.15 | (115) all_49_0_17 = all_37_0_9 % 14.63/4.15 | % 14.63/4.15 | Combining equations (115,114) yields a new equation: % 14.63/4.15 | (116) all_37_0_9 = tptp3 % 14.63/4.15 | % 14.63/4.15 | Simplifying 116 yields: % 14.63/4.15 | (117) all_37_0_9 = tptp3 % 14.63/4.15 | % 14.63/4.15 | From (117) and (104) follows: % 14.63/4.15 | (9) atomic(tptp3) % 14.63/4.15 | % 14.63/4.15 | From (117) and (105) follows: % 14.63/4.15 | (94) occurrence_of(all_9_0_1, tptp3) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (23) with tptp3, tptp3, all_9_0_1 and discharging atoms subactivity(tptp3, tptp3), atomic(tptp3), occurrence_of(all_9_0_1, tptp3), yields: % 14.63/4.15 | (120) atocc(all_9_0_1, tptp3) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (36) with all_45_1_15, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_45_1_15), yields: % 14.63/4.15 | (121) ? [v0] : (subactivity(all_45_1_15, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (44) with all_9_0_1, all_21_0_6 and discharging atoms root(all_9_0_1, all_21_0_6), yields: % 14.63/4.15 | (122) ? [v0] : (subactivity(v0, all_21_0_6) & atocc(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (45) 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: % 14.63/4.15 | (123) ? [v0] : ? [v1] : (subactivity(v1, tptp0) & subactivity(v0, tptp0) & atocc(all_11_0_2, v1) & atocc(all_9_0_1, v0)) % 14.63/4.15 | % 14.63/4.15 | Instantiating (121) with all_67_0_21 yields: % 14.63/4.15 | (124) subactivity(all_45_1_15, all_67_0_21) & atomic(all_67_0_21) & occurrence_of(all_9_0_1, all_67_0_21) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (124) yields: % 14.63/4.15 | (125) subactivity(all_45_1_15, all_67_0_21) % 14.63/4.15 | (126) atomic(all_67_0_21) % 14.63/4.15 | (127) occurrence_of(all_9_0_1, all_67_0_21) % 14.63/4.15 | % 14.63/4.15 | Instantiating (123) with all_77_0_26, all_77_1_27 yields: % 14.63/4.15 | (128) subactivity(all_77_0_26, tptp0) & subactivity(all_77_1_27, tptp0) & atocc(all_11_0_2, all_77_0_26) & atocc(all_9_0_1, all_77_1_27) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (128) yields: % 14.63/4.15 | (129) subactivity(all_77_0_26, tptp0) % 14.63/4.15 | (130) subactivity(all_77_1_27, tptp0) % 14.63/4.15 | (131) atocc(all_11_0_2, all_77_0_26) % 14.63/4.15 | (132) atocc(all_9_0_1, all_77_1_27) % 14.63/4.15 | % 14.63/4.15 | Instantiating (122) with all_85_0_35 yields: % 14.63/4.15 | (133) subactivity(all_85_0_35, all_21_0_6) & atocc(all_9_0_1, all_85_0_35) % 14.63/4.15 | % 14.63/4.15 | Applying alpha-rule on (133) yields: % 14.63/4.15 | (134) subactivity(all_85_0_35, all_21_0_6) % 14.63/4.15 | (135) atocc(all_9_0_1, all_85_0_35) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (57) with all_67_0_21, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_67_0_21), occurrence_of(all_9_0_1, tptp3), yields: % 14.63/4.15 | (136) all_67_0_21 = tptp3 % 14.63/4.15 | % 14.63/4.15 | From (136) and (127) follows: % 14.63/4.15 | (94) occurrence_of(all_9_0_1, tptp3) % 14.63/4.15 | % 14.63/4.15 | Instantiating formula (36) with all_85_0_35, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_85_0_35), yields: % 14.63/4.16 | (138) ? [v0] : (subactivity(all_85_0_35, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (36) with all_77_1_27, all_9_0_1 and discharging atoms atocc(all_9_0_1, all_77_1_27), yields: % 14.63/4.16 | (139) ? [v0] : (subactivity(all_77_1_27, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (36) with tptp3, all_9_0_1 and discharging atoms atocc(all_9_0_1, tptp3), yields: % 14.63/4.16 | (140) ? [v0] : (subactivity(tptp3, v0) & atomic(v0) & occurrence_of(all_9_0_1, v0)) % 14.63/4.16 | % 14.63/4.16 | Instantiating (138) with all_127_0_53 yields: % 14.63/4.16 | (141) subactivity(all_85_0_35, all_127_0_53) & atomic(all_127_0_53) & occurrence_of(all_9_0_1, all_127_0_53) % 14.63/4.16 | % 14.63/4.16 | Applying alpha-rule on (141) yields: % 14.63/4.16 | (142) subactivity(all_85_0_35, all_127_0_53) % 14.63/4.16 | (143) atomic(all_127_0_53) % 14.63/4.16 | (144) occurrence_of(all_9_0_1, all_127_0_53) % 14.63/4.16 | % 14.63/4.16 | Instantiating (140) with all_135_0_57 yields: % 14.63/4.16 | (145) subactivity(tptp3, all_135_0_57) & atomic(all_135_0_57) & occurrence_of(all_9_0_1, all_135_0_57) % 14.63/4.16 | % 14.63/4.16 | Applying alpha-rule on (145) yields: % 14.63/4.16 | (146) subactivity(tptp3, all_135_0_57) % 14.63/4.16 | (147) atomic(all_135_0_57) % 14.63/4.16 | (148) occurrence_of(all_9_0_1, all_135_0_57) % 14.63/4.16 | % 14.63/4.16 | Instantiating (139) with all_137_0_58 yields: % 14.63/4.16 | (149) subactivity(all_77_1_27, all_137_0_58) & atomic(all_137_0_58) & occurrence_of(all_9_0_1, all_137_0_58) % 14.63/4.16 | % 14.63/4.16 | Applying alpha-rule on (149) yields: % 14.63/4.16 | (150) subactivity(all_77_1_27, all_137_0_58) % 14.63/4.16 | (151) atomic(all_137_0_58) % 14.63/4.16 | (152) occurrence_of(all_9_0_1, all_137_0_58) % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (57) with all_137_0_58, tptp3, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_137_0_58), occurrence_of(all_9_0_1, tptp3), yields: % 14.63/4.16 | (153) all_137_0_58 = tptp3 % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (57) with all_135_0_57, all_137_0_58, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_137_0_58), occurrence_of(all_9_0_1, all_135_0_57), yields: % 14.63/4.16 | (154) all_137_0_58 = all_135_0_57 % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (57) with all_127_0_53, all_137_0_58, all_9_0_1 and discharging atoms occurrence_of(all_9_0_1, all_137_0_58), occurrence_of(all_9_0_1, all_127_0_53), yields: % 14.63/4.16 | (155) all_137_0_58 = all_127_0_53 % 14.63/4.16 | % 14.63/4.16 | Combining equations (153,154) yields a new equation: % 14.63/4.16 | (156) all_135_0_57 = tptp3 % 14.63/4.16 | % 14.63/4.16 | Combining equations (155,154) yields a new equation: % 14.63/4.16 | (157) all_135_0_57 = all_127_0_53 % 14.63/4.16 | % 14.63/4.16 | Combining equations (156,157) yields a new equation: % 14.63/4.16 | (158) all_127_0_53 = tptp3 % 14.63/4.16 | % 14.63/4.16 | From (158) and (144) follows: % 14.63/4.16 | (94) occurrence_of(all_9_0_1, tptp3) % 14.63/4.16 | % 14.63/4.16 +-Applying beta-rule and splitting (75), into two cases. % 14.63/4.16 |-Branch one: % 14.63/4.16 | (160) occurrence_of(all_11_0_2, tptp1) % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (32) with all_11_0_2, all_9_0_1 and discharging atoms leaf_occ(all_11_0_2, all_0_0_0), 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: % 14.63/4.16 | (161) $false % 14.63/4.16 | % 14.63/4.16 |-The branch is then unsatisfiable % 14.63/4.16 |-Branch two: % 14.63/4.16 | (162) ~ occurrence_of(all_11_0_2, tptp1) % 14.63/4.16 | (163) occurrence_of(all_11_0_2, tptp2) % 14.63/4.16 | % 14.63/4.16 | Instantiating formula (8) with all_11_0_2, all_9_0_1 and discharging atoms leaf_occ(all_11_0_2, all_0_0_0), 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: % 14.63/4.16 | (161) $false % 14.63/4.16 | % 14.63/4.16 |-The branch is then unsatisfiable % 14.63/4.16 % SZS output end Proof for theBenchmark % 14.63/4.16 % 14.63/4.16 3573ms %------------------------------------------------------------------------------