%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : PRO012+4 : 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:59 EDT 2022 % Result : Theorem 31.21s 9.25s % Output : Proof 59.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PRO012+4 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.35 % Computer : n012.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jun 13 03:52:55 EDT 2022 % 0.13/0.35 % CPUTime : % 0.60/0.59 ____ _ % 0.60/0.60 ___ / __ \_____(_)___ ________ __________ % 0.60/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.60/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.60/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.60/0.60 % 0.60/0.60 A Theorem Prover for First-Order Logic % 0.60/0.60 (ePrincess v.1.0) % 0.60/0.60 % 0.60/0.60 (c) Philipp Rümmer, 2009-2015 % 0.60/0.60 (c) Peter Backeman, 2014-2015 % 0.60/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.60/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.60/0.60 Bug reports to peter@backeman.se % 0.60/0.60 % 0.60/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.60/0.60 % 0.60/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.73/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.80/0.98 Prover 0: Preprocessing ... % 2.52/1.22 Prover 0: Constructing countermodel ... % 17.26/5.94 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 17.57/6.01 Prover 1: Preprocessing ... % 18.58/6.22 Prover 1: Constructing countermodel ... % 28.27/8.54 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 28.27/8.59 Prover 2: Preprocessing ... % 29.07/8.77 Prover 2: Warning: ignoring some quantifiers % 29.07/8.78 Prover 2: Constructing countermodel ... % 31.21/9.24 Prover 2: proved (704ms) % 31.21/9.24 Prover 1: stopped % 31.21/9.24 Prover 0: stopped % 31.21/9.25 % 31.21/9.25 No countermodel exists, formula is valid % 31.21/9.25 % SZS status Theorem for theBenchmark % 31.21/9.25 % 31.21/9.25 Generating proof ... Warning: ignoring some quantifiers % 58.25/20.02 found it (size 290) % 58.25/20.02 % 58.25/20.02 % SZS output start Proof for theBenchmark % 58.25/20.02 Assumed formulas after preprocessing and simplification: % 58.25/20.02 | (0) ? [v0] : ? [v1] : ( ~ (v0 = 0) & ~ (tptp1 = tptp2) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) = 0 & occurrence_of(v1, tptp0) = 0 & atomic(tptp1) = 0 & atomic(tptp2) = 0 & atomic(tptp4) = 0 & atomic(tptp3) = 0 & atomic(tptp0) = v0 & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = v4 | ~ (min_precedes(v5, v4, v2) = 0) | ~ (min_precedes(v4, v6, v2) = v7) | ~ (occurrence_of(v3, v2) = 0) | ? [v8] : (( ~ (v8 = 0) & root_occ(v5, v3) = v8) | ( ~ (v8 = 0) & leaf_occ(v6, v3) = v8) | ( ~ (v8 = 0) & subactivity_occurrence(v4, v3) = v8))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = v4 | ~ (min_precedes(v5, v4, v2) = 0) | ~ (min_precedes(v4, v6, v2) = v7) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v8] : (( ~ (v8 = 0) & root_occ(v5, v3) = v8) | ( ~ (v8 = 0) & leaf_occ(v6, v3) = v8) | ( ~ (v8 = 0) & occurrence_of(v3, v2) = v8))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = v4 | ~ (min_precedes(v4, v6, v2) = v7) | ~ (root_occ(v5, v3) = 0) | ? [v8] : (( ~ (v8 = 0) & min_precedes(v5, v4, v2) = v8) | ( ~ (v8 = 0) & leaf_occ(v6, v3) = v8) | ( ~ (v8 = 0) & occurrence_of(v3, v2) = v8) | ( ~ (v8 = 0) & subactivity_occurrence(v4, v3) = v8))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v4 | ~ (min_precedes(v5, v4, v2) = 0) | ~ (leaf_occ(v6, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v4, v6, v2) = 0) | ( ~ (v7 = 0) & root_occ(v5, v3) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v4 | ~ (root_occ(v5, v3) = 0) | ~ (leaf_occ(v6, v3) = 0) | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v4, v6, v2) = 0) | ( ~ (v7 = 0) & min_precedes(v5, v4, v2) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v5, v4, v2) = v6) | ~ (occurrence_of(v3, v2) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v5, v3) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v5, v4, v2) = v6) | ~ (subactivity_occurrence(v5, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v5, v4, v2) = v6) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v5, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (leaf_occ(v5, v3) = 0) | ? [v7] : (( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (occurrence_of(v3, v2) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v5, v4, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v5, v3) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (occurrence_of(v3, v2) = 0) | ? [v7] : (( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & leaf_occ(v5, v3) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (subactivity_occurrence(v5, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v5, v4, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v4, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v7] : ((v7 = 0 & min_precedes(v5, v4, v2) = 0) | ( ~ (v7 = 0) & arboreal(v5) = v7) | ( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v5, v3) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v5 = v4 | ~ (min_precedes(v4, v5, v2) = v6) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v7] : (( ~ (v7 = 0) & arboreal(v4) = v7) | ( ~ (v7 = 0) & leaf_occ(v5, v3) = v7) | ( ~ (v7 = 0) & occurrence_of(v3, v2) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | v3 = v2 | ~ (leaf_occ(v3, v4) = 0) | ~ (leaf_occ(v2, v4) = 0) | ~ (atomic(v5) = v6) | ? [v7] : ( ~ (v7 = 0) & occurrence_of(v4, v5) = v7)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (min_precedes(v3, v4, v5) = v6) | ~ (min_precedes(v2, v4, v5) = 0) | ? [v7] : (( ~ (v7 = 0) & precedes(v3, v4) = v7) | ( ~ (v7 = 0) & min_precedes(v2, v3, v5) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (min_precedes(v3, v4, v5) = v6) | ~ (min_precedes(v2, v3, v5) = 0) | ? [v7] : (( ~ (v7 = 0) & precedes(v3, v4) = v7) | ( ~ (v7 = 0) & min_precedes(v2, v4, v5) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (min_precedes(v2, v3, v4) = 0) | ~ (subactivity_occurrence(v2, v5) = v6) | ? [v7] : (( ~ (v7 = 0) & occurrence_of(v5, v4) = v7) | ( ~ (v7 = 0) & subactivity_occurrence(v3, v5) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (occurrence_of(v5, v4) = 0) | ~ (subactivity_occurrence(v3, v5) = 0) | ~ (subactivity_occurrence(v2, v5) = v6) | ? [v7] : ( ~ (v7 = 0) & min_precedes(v2, v3, v4) = v7)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v3 = v2 | ~ (next_subocc(v6, v5, v4) = v3) | ~ (next_subocc(v6, v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v3 = v2 | ~ (min_precedes(v6, v5, v4) = v3) | ~ (min_precedes(v6, v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (min_precedes(v6, v3, v4) = 0) | ~ (min_precedes(v2, v3, v4) = v5) | ? [v7] : (( ~ (v7 = 0) & next_subocc(v2, v3, v4) = v7) | ( ~ (v7 = 0) & min_precedes(v2, v6, v4) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (min_precedes(v2, v6, v4) = 0) | ~ (min_precedes(v2, v3, v4) = v5) | ? [v7] : (( ~ (v7 = 0) & next_subocc(v2, v3, v4) = v7) | ( ~ (v7 = 0) & min_precedes(v6, v3, v4) = v7))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (arboreal(v5) = 0) | ~ (arboreal(v4) = 0) | ~ (occurrence_of(v3, v2) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v5, v4, v2) = 0) | (v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & subactivity_occurrence(v5, v3) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v4, v3) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (arboreal(v5) = 0) | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v5, v4, v2) = 0) | (v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & arboreal(v4) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v5, v3) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (arboreal(v4) = 0) | ~ (leaf_occ(v5, v3) = 0) | ~ (occurrence_of(v3, v2) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & subactivity_occurrence(v4, v3) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (arboreal(v4) = 0) | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v5, v3) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v5, v4, v2) = 0) | (v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & arboreal(v5) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v4, v3) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (leaf_occ(v5, v3) = 0) | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & arboreal(v4) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v5, v3) = 0) | ~ (subactivity_occurrence(v4, v3) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v5, v4, v2) = 0) | (v6 = 0 & min_precedes(v4, v5, v2) = 0) | ( ~ (v6 = 0) & arboreal(v5) = v6) | ( ~ (v6 = 0) & arboreal(v4) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (next_subocc(v2, v3, v4) = v5) | ? [v6] : ? [v7] : ? [v8] : ((v8 = 0 & v7 = 0 & min_precedes(v6, v3, v4) = 0 & min_precedes(v2, v6, v4) = 0) | ( ~ (v6 = 0) & min_precedes(v2, v3, v4) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (earlier(v3, v4) = 0) | ~ (earlier(v2, v4) = v5) | ? [v6] : ( ~ (v6 = 0) & earlier(v2, v3) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (earlier(v2, v4) = v5) | ~ (earlier(v2, v3) = 0) | ? [v6] : ( ~ (v6 = 0) & earlier(v3, v4) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (min_precedes(v2, v3, v4) = v5) | ? [v6] : ( ~ (v6 = 0) & next_subocc(v2, v3, v4) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (leaf(v2, v3) = v4) | ~ (min_precedes(v5, v2, v3) = 0) | ? [v6] : min_precedes(v2, v6, v3) = 0) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (subactivity(v3, v5) = 0) | ~ (atocc(v2, v3) = v4) | ? [v6] : (( ~ (v6 = 0) & occurrence_of(v2, v5) = v6) | ( ~ (v6 = 0) & atomic(v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (atocc(v2, v3) = v4) | ~ (occurrence_of(v2, v5) = 0) | ? [v6] : (( ~ (v6 = 0) & subactivity(v3, v5) = v6) | ( ~ (v6 = 0) & atomic(v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v4 = 0 | ~ (atocc(v2, v3) = v4) | ~ (atomic(v5) = 0) | ? [v6] : (( ~ (v6 = 0) & subactivity(v3, v5) = v6) | ( ~ (v6 = 0) & occurrence_of(v2, v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (precedes(v5, v4) = v3) | ~ (precedes(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (earlier(v5, v4) = v3) | ~ (earlier(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (leaf(v5, v4) = v3) | ~ (leaf(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (subactivity(v5, v4) = v3) | ~ (subactivity(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (atocc(v5, v4) = v3) | ~ (atocc(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (root_occ(v5, v4) = v3) | ~ (root_occ(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (root_occ(v3, v4) = 0) | ~ (root_occ(v2, v4) = 0) | ~ (occurrence_of(v4, v5) = 0)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (leaf_occ(v5, v4) = v3) | ~ (leaf_occ(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (leaf_occ(v3, v4) = 0) | ~ (leaf_occ(v2, v4) = 0) | ~ (occurrence_of(v4, v5) = 0) | atomic(v5) = 0) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (occurrence_of(v5, v4) = v3) | ~ (occurrence_of(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (root(v5, v4) = v3) | ~ (root(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (subactivity_occurrence(v5, v4) = v3) | ~ (subactivity_occurrence(v5, v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (next_subocc(v2, v3, v4) = 0) | ~ (min_precedes(v5, v3, v4) = 0) | ? [v6] : ( ~ (v6 = 0) & min_precedes(v2, v5, v4) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (next_subocc(v2, v3, v4) = 0) | ~ (min_precedes(v2, v5, v4) = 0) | ? [v6] : ( ~ (v6 = 0) & min_precedes(v5, v3, v4) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (precedes(v3, v4) = 0) | ~ (min_precedes(v2, v4, v5) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v3, v4, v5) = 0) | ( ~ (v6 = 0) & min_precedes(v2, v3, v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (precedes(v3, v4) = 0) | ~ (min_precedes(v2, v3, v5) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v3, v4, v5) = 0) | ( ~ (v6 = 0) & min_precedes(v2, v4, v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v5, v3, v4) = 0) | ~ (root_occ(v3, v2) = 0) | ~ (occurrence_of(v2, v4) = 0)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v5, v2, v3) = 0) | ~ (root(v2, v3) = v4) | ? [v6] : ? [v7] : ((v7 = 0 & min_precedes(v2, v6, v3) = 0) | (v6 = 0 & leaf(v2, v3) = 0))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v3, v5, v4) = 0) | ~ (leaf_occ(v3, v2) = 0) | ~ (occurrence_of(v2, v4) = 0)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v2, v5, v3) = 0) | ~ (root(v2, v3) = v4) | ? [v6] : ( ~ (v6 = 0) & leaf(v2, v3) = v6)) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v2, v4, v5) = 0) | ~ (min_precedes(v2, v3, v5) = 0) | ? [v6] : ((v6 = 0 & min_precedes(v3, v4, v5) = 0) | ( ~ (v6 = 0) & precedes(v3, v4) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v2, v3, v4) = 0) | ~ (occurrence_of(v5, v4) = 0) | ? [v6] : ((v6 = 0 & subactivity_occurrence(v2, v5) = 0) | ( ~ (v6 = 0) & subactivity_occurrence(v3, v5) = v6))) & ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (min_precedes(v2, v3, v4) = 0) | ~ (subactivity_occurrence(v3, v5) = 0) | ? [v6] : ((v6 = 0 & subactivity_occurrence(v2, v5) = 0) | ( ~ (v6 = 0) & occurrence_of(v5, v4) = v6))) & ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (occurrence_of(v2, v4) = 0) | ~ (occurrence_of(v2, v3) = 0)) & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (precedes(v2, v3) = v4) | ? [v5] : (( ~ (v5 = 0) & earlier(v2, v3) = v5) | ( ~ (v5 = 0) & legal(v3) = v5))) & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (leaf(v2, v3) = v4) | ? [v5] : ? [v6] : ((v6 = 0 & min_precedes(v2, v5, v3) = 0) | ( ~ (v5 = 0) & root(v2, v3) = v5))) & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (root_occ(v2, v3) = v4) | ? [v5] : (subactivity_occurrence(v2, v3) = v5 & ! [v6] : ( ~ (v5 = 0) | ~ (occurrence_of(v3, v6) = 0) | ? [v7] : ( ~ (v7 = 0) & root(v2, v6) = v7)) & ! [v6] : ( ~ (v5 = 0) | ~ (root(v2, v6) = 0) | ? [v7] : ( ~ (v7 = 0) & occurrence_of(v3, v6) = v7)))) & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (leaf_occ(v2, v3) = v4) | ? [v5] : (subactivity_occurrence(v2, v3) = v5 & ! [v6] : ( ~ (v5 = 0) | ~ (leaf(v2, v6) = 0) | ? [v7] : ( ~ (v7 = 0) & occurrence_of(v3, v6) = v7)) & ! [v6] : ( ~ (v5 = 0) | ~ (occurrence_of(v3, v6) = 0) | ? [v7] : ( ~ (v7 = 0) & leaf(v2, v6) = v7)))) & ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (root(v2, v3) = v4) | ? [v5] : ? [v6] : ((v6 = 0 & min_precedes(v5, v2, v3) = 0) | ( ~ (v5 = 0) & leaf(v2, v3) = v5))) & ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (legal(v4) = v3) | ~ (legal(v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (activity(v4) = v3) | ~ (activity(v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (activity_occurrence(v4) = v3) | ~ (activity_occurrence(v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (arboreal(v4) = v3) | ~ (arboreal(v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (atomic(v4) = v3) | ~ (atomic(v4) = v2)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (next_subocc(v2, v3, v4) = 0) | min_precedes(v2, v3, v4) = 0) & ! [v2] : ! [v3] : ! [v4] : ( ~ (next_subocc(v2, v3, v4) = 0) | (arboreal(v3) = 0 & arboreal(v2) = 0)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (earlier(v3, v4) = 0) | ~ (earlier(v2, v3) = 0) | earlier(v2, v4) = 0) & ! [v2] : ! [v3] : ! [v4] : ( ~ (earlier(v2, v3) = v4) | ? [v5] : ((v5 = 0 & v4 = 0 & legal(v3) = 0) | ( ~ (v5 = 0) & precedes(v2, v3) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (leaf(v2, v4) = 0) | ~ (subactivity_occurrence(v2, v3) = 0) | ? [v5] : ((v5 = 0 & leaf_occ(v2, v3) = 0) | ( ~ (v5 = 0) & occurrence_of(v3, v4) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (leaf(v2, v3) = 0) | ~ (min_precedes(v2, v4, v3) = 0)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v3, v4, v2) = 0) | ? [v5] : (occurrence_of(v5, v2) = 0 & subactivity_occurrence(v4, v5) = 0 & subactivity_occurrence(v3, v5) = 0)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v2, v3, v4) = 0) | precedes(v2, v3) = 0) & ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v2, v3, v4) = 0) | ? [v5] : ? [v6] : ? [v7] : ((v7 = 0 & v6 = 0 & min_precedes(v5, v3, v4) = 0 & min_precedes(v2, v5, v4) = 0) | (v5 = 0 & next_subocc(v2, v3, v4) = 0))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v2, v3, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & root(v3, v4) = v5)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v2, v3, v4) = 0) | ? [v5] : (min_precedes(v5, v3, v4) = 0 & root(v5, v4) = 0)) & ! [v2] : ! [v3] : ! [v4] : ( ~ (occurrence_of(v3, v4) = 0) | ~ (subactivity_occurrence(v2, v3) = 0) | ? [v5] : ((v5 = 0 & root_occ(v2, v3) = 0) | ( ~ (v5 = 0) & root(v2, v4) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (occurrence_of(v3, v4) = 0) | ~ (subactivity_occurrence(v2, v3) = 0) | ? [v5] : ((v5 = 0 & leaf_occ(v2, v3) = 0) | ( ~ (v5 = 0) & leaf(v2, v4) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (root(v2, v4) = 0) | ~ (subactivity_occurrence(v2, v3) = 0) | ? [v5] : ((v5 = 0 & root_occ(v2, v3) = 0) | ( ~ (v5 = 0) & occurrence_of(v3, v4) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (subactivity_occurrence(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : ((v7 = 0 & v6 = 0 & v4 = 0 & leaf(v2, v5) = 0 & occurrence_of(v3, v5) = 0) | ( ~ (v5 = 0) & leaf_occ(v2, v3) = v5))) & ! [v2] : ! [v3] : ! [v4] : ( ~ (subactivity_occurrence(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : ((v7 = 0 & v6 = 0 & v4 = 0 & occurrence_of(v3, v5) = 0 & root(v2, v5) = 0) | ( ~ (v5 = 0) & root_occ(v2, v3) = v5))) & ! [v2] : ! [v3] : (v3 = 0 | ~ (arboreal(v2) = v3) | ? [v4] : ( ~ (v4 = 0) & legal(v2) = v4)) & ! [v2] : ! [v3] : ( ~ (precedes(v2, v3) = 0) | (earlier(v2, v3) = 0 & legal(v3) = 0)) & ! [v2] : ! [v3] : ( ~ (earlier(v3, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & earlier(v2, v3) = v4)) & ! [v2] : ! [v3] : ( ~ (earlier(v2, v3) = 0) | ? [v4] : ( ~ (v4 = 0) & earlier(v3, v2) = v4)) & ! [v2] : ! [v3] : ( ~ (earlier(v2, v3) = 0) | ? [v4] : ((v4 = 0 & precedes(v2, v3) = 0) | ( ~ (v4 = 0) & legal(v3) = v4))) & ! [v2] : ! [v3] : ( ~ (leaf(v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & leaf_occ(v2, v4) = 0 & occurrence_of(v4, v3) = 0) | (v4 = 0 & atomic(v3) = 0))) & ! [v2] : ! [v3] : ( ~ (leaf(v2, v3) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & min_precedes(v4, v2, v3) = 0) | (v4 = 0 & root(v2, v3) = 0))) & ! [v2] : ! [v3] : ( ~ (atocc(v2, v3) = 0) | ? [v4] : (subactivity(v3, v4) = 0 & occurrence_of(v2, v4) = 0 & atomic(v4) = 0)) & ! [v2] : ! [v3] : ( ~ (min_precedes(v2, v3, tptp0) = 0) | ? [v4] : ? [v5] : (( ~ (v5 = 0) & ~ (v4 = 0) & occurrence_of(v3, tptp1) = v5 & occurrence_of(v3, tptp2) = v4) | ( ~ (v4 = 0) & root_occ(v2, v1) = v4) | ( ~ (v4 = 0) & occurrence_of(v2, tptp3) = v4))) & ! [v2] : ! [v3] : ( ~ (root_occ(v2, v3) = 0) | ? [v4] : (occurrence_of(v3, v4) = 0 & root(v2, v4) = 0 & subactivity_occurrence(v2, v3) = 0)) & ! [v2] : ! [v3] : ( ~ (leaf_occ(v2, v3) = 0) | ? [v4] : (leaf(v2, v4) = 0 & occurrence_of(v3, v4) = 0 & subactivity_occurrence(v2, v3) = 0)) & ! [v2] : ! [v3] : ( ~ (occurrence_of(v3, v2) = 0) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & root(v4, v2) = 0 & subactivity_occurrence(v4, v3) = 0) | (v4 = 0 & atomic(v2) = 0))) & ! [v2] : ! [v3] : ( ~ (occurrence_of(v3, v2) = 0) | (activity(v2) = 0 & activity_occurrence(v3) = 0)) & ! [v2] : ! [v3] : ( ~ (occurrence_of(v2, v3) = 0) | ? [v4] : ? [v5] : (((v5 = 0 & atomic(v3) = 0) | ( ~ (v4 = 0) & arboreal(v2) = v4)) & ((v4 = 0 & arboreal(v2) = 0) | ( ~ (v5 = 0) & atomic(v3) = v5)))) & ! [v2] : ! [v3] : ( ~ (root(v3, v2) = 0) | ? [v4] : (subactivity(v4, v2) = 0 & atocc(v3, v4) = 0)) & ! [v2] : ! [v3] : ( ~ (root(v2, v3) = 0) | legal(v2) = 0) & ! [v2] : ! [v3] : ( ~ (root(v2, v3) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & min_precedes(v2, v4, v3) = 0) | (v4 = 0 & leaf(v2, v3) = 0))) & ! [v2] : ! [v3] : ( ~ (subactivity_occurrence(v2, v3) = 0) | (activity_occurrence(v3) = 0 & activity_occurrence(v2) = 0)) & ! [v2] : ( ~ (legal(v2) = 0) | arboreal(v2) = 0) & ! [v2] : ( ~ (activity_occurrence(v2) = 0) | ? [v3] : (activity(v3) = 0 & occurrence_of(v2, v3) = 0)) & ! [v2] : ( ~ (occurrence_of(v2, tptp0) = 0) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (min_precedes(v4, v5, tptp0) = 0 & min_precedes(v3, v4, tptp0) = 0 & root_occ(v3, v2) = 0 & occurrence_of(v4, tptp4) = 0 & occurrence_of(v3, tptp3) = 0 & ! [v8] : (v8 = v5 | v8 = v4 | ~ (min_precedes(v3, v8, tptp0) = 0)) & ((v7 = 0 & occurrence_of(v5, tptp1) = 0) | (v6 = 0 & occurrence_of(v5, tptp2) = 0)))) & ? [v2] : ? [v3] : ? [v4] : ? [v5] : next_subocc(v4, v3, v2) = v5 & ? [v2] : ? [v3] : ? [v4] : ? [v5] : min_precedes(v4, v3, v2) = v5 & ? [v2] : ? [v3] : ? [v4] : precedes(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : earlier(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : leaf(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : subactivity(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : atocc(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : root_occ(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : leaf_occ(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : occurrence_of(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : root(v3, v2) = v4 & ? [v2] : ? [v3] : ? [v4] : subactivity_occurrence(v3, v2) = v4 & ? [v2] : ? [v3] : legal(v2) = v3 & ? [v2] : ? [v3] : activity(v2) = v3 & ? [v2] : ? [v3] : activity_occurrence(v2) = v3 & ? [v2] : ? [v3] : arboreal(v2) = v3 & ? [v2] : ? [v3] : atomic(v2) = v3) % 58.63/20.13 | Instantiating (0) with all_0_0_0, all_0_1_1 yields: % 58.63/20.13 | (1) ~ (all_0_1_1 = 0) & ~ (tptp1 = tptp2) & ~ (tptp1 = tptp4) & ~ (tptp1 = tptp3) & ~ (tptp2 = tptp4) & ~ (tptp2 = tptp3) & ~ (tptp4 = tptp3) & activity(tptp0) = 0 & occurrence_of(all_0_0_0, tptp0) = 0 & atomic(tptp1) = 0 & atomic(tptp2) = 0 & atomic(tptp4) = 0 & atomic(tptp3) = 0 & atomic(tptp0) = all_0_1_1 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (min_precedes(v2, v4, v0) = v5) | ~ (occurrence_of(v1, v0) = 0) | ? [v6] : (( ~ (v6 = 0) & root_occ(v3, v1) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v2, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (min_precedes(v2, v4, v0) = v5) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v6] : (( ~ (v6 = 0) & root_occ(v3, v1) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & occurrence_of(v1, v0) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v2, v4, v0) = v5) | ~ (root_occ(v3, v1) = 0) | ? [v6] : (( ~ (v6 = 0) & min_precedes(v3, v2, v0) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & occurrence_of(v1, v0) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v2, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (leaf_occ(v4, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v4, v0) = 0) | ( ~ (v5 = 0) & root_occ(v3, v1) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (root_occ(v3, v1) = 0) | ~ (leaf_occ(v4, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v4, v0) = 0) | ( ~ (v5 = 0) & min_precedes(v3, v2, v0) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (leaf_occ(v3, v1) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & leaf_occ(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & leaf_occ(v3, v1) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v1 = v0 | ~ (leaf_occ(v1, v2) = 0) | ~ (leaf_occ(v0, v2) = 0) | ~ (atomic(v3) = v4) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v2, v3) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v1, v2, v3) = v4) | ~ (min_precedes(v0, v2, v3) = 0) | ? [v5] : (( ~ (v5 = 0) & precedes(v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v1, v3) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v1, v2, v3) = v4) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v5] : (( ~ (v5 = 0) & precedes(v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v2, v3) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v0, v1, v2) = 0) | ~ (subactivity_occurrence(v0, v3) = v4) | ? [v5] : (( ~ (v5 = 0) & occurrence_of(v3, v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v1, v3) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v1, v3) = 0) | ~ (subactivity_occurrence(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & min_precedes(v0, v1, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (next_subocc(v4, v3, v2) = v1) | ~ (next_subocc(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (min_precedes(v4, v3, v2) = v1) | ~ (min_precedes(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v4, v1, v2) = 0) | ~ (min_precedes(v0, v1, v2) = v3) | ? [v5] : (( ~ (v5 = 0) & next_subocc(v0, v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v4, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v0, v4, v2) = 0) | ~ (min_precedes(v0, v1, v2) = v3) | ? [v5] : (( ~ (v5 = 0) & next_subocc(v0, v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v4, v1, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v3) = 0) | ~ (arboreal(v2) = 0) | ~ (occurrence_of(v1, v0) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v3, v1) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v3) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v2) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v3, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v2) = 0) | ~ (leaf_occ(v3, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v2) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v3) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (leaf_occ(v3, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v2) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v3, v1) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v3) = v4) | ( ~ (v4 = 0) & arboreal(v2) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (next_subocc(v0, v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & min_precedes(v4, v1, v2) = 0 & min_precedes(v0, v4, v2) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v1, v2) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (earlier(v1, v2) = 0) | ~ (earlier(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & earlier(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (earlier(v0, v2) = v3) | ~ (earlier(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & earlier(v1, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (min_precedes(v0, v1, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & next_subocc(v0, v1, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (leaf(v0, v1) = v2) | ~ (min_precedes(v3, v0, v1) = 0) | ? [v4] : min_precedes(v0, v4, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (subactivity(v1, v3) = 0) | ~ (atocc(v0, v1) = v2) | ? [v4] : (( ~ (v4 = 0) & occurrence_of(v0, v3) = v4) | ( ~ (v4 = 0) & atomic(v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (atocc(v0, v1) = v2) | ~ (occurrence_of(v0, v3) = 0) | ? [v4] : (( ~ (v4 = 0) & subactivity(v1, v3) = v4) | ( ~ (v4 = 0) & atomic(v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (atocc(v0, v1) = v2) | ~ (atomic(v3) = 0) | ? [v4] : (( ~ (v4 = 0) & subactivity(v1, v3) = v4) | ( ~ (v4 = 0) & occurrence_of(v0, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (precedes(v3, v2) = v1) | ~ (precedes(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (earlier(v3, v2) = v1) | ~ (earlier(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf(v3, v2) = v1) | ~ (leaf(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subactivity(v3, v2) = v1) | ~ (subactivity(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (atocc(v3, v2) = v1) | ~ (atocc(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root_occ(v3, v2) = v1) | ~ (root_occ(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root_occ(v1, v2) = 0) | ~ (root_occ(v0, v2) = 0) | ~ (occurrence_of(v2, v3) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf_occ(v3, v2) = v1) | ~ (leaf_occ(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf_occ(v1, v2) = 0) | ~ (leaf_occ(v0, v2) = 0) | ~ (occurrence_of(v2, v3) = 0) | atomic(v3) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (occurrence_of(v3, v2) = v1) | ~ (occurrence_of(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root(v3, v2) = v1) | ~ (root(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subactivity_occurrence(v3, v2) = v1) | ~ (subactivity_occurrence(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (next_subocc(v0, v1, v2) = 0) | ~ (min_precedes(v3, v1, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & min_precedes(v0, v3, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (next_subocc(v0, v1, v2) = 0) | ~ (min_precedes(v0, v3, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & min_precedes(v3, v1, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (precedes(v1, v2) = 0) | ~ (min_precedes(v0, v2, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v1, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (precedes(v1, v2) = 0) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v2, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v3, v1, v2) = 0) | ~ (root_occ(v1, v0) = 0) | ~ (occurrence_of(v0, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v3, v0, v1) = 0) | ~ (root(v0, v1) = v2) | ? [v4] : ? [v5] : ((v5 = 0 & min_precedes(v0, v4, v1) = 0) | (v4 = 0 & leaf(v0, v1) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v1, v3, v2) = 0) | ~ (leaf_occ(v1, v0) = 0) | ~ (occurrence_of(v0, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v3, v1) = 0) | ~ (root(v0, v1) = v2) | ? [v4] : ( ~ (v4 = 0) & leaf(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v2, v3) = 0) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & precedes(v1, v2) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v1, v2) = 0) | ~ (occurrence_of(v3, v2) = 0) | ? [v4] : ((v4 = 0 & subactivity_occurrence(v0, v3) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v1, v3) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v1, v2) = 0) | ~ (subactivity_occurrence(v1, v3) = 0) | ? [v4] : ((v4 = 0 & subactivity_occurrence(v0, v3) = 0) | ( ~ (v4 = 0) & occurrence_of(v3, v2) = v4))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (occurrence_of(v0, v2) = 0) | ~ (occurrence_of(v0, v1) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (precedes(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & earlier(v0, v1) = v3) | ( ~ (v3 = 0) & legal(v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leaf(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & min_precedes(v0, v3, v1) = 0) | ( ~ (v3 = 0) & root(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (root_occ(v0, v1) = v2) | ? [v3] : (subactivity_occurrence(v0, v1) = v3 & ! [v4] : ( ~ (v3 = 0) | ~ (occurrence_of(v1, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & root(v0, v4) = v5)) & ! [v4] : ( ~ (v3 = 0) | ~ (root(v0, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v1, v4) = v5)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leaf_occ(v0, v1) = v2) | ? [v3] : (subactivity_occurrence(v0, v1) = v3 & ! [v4] : ( ~ (v3 = 0) | ~ (leaf(v0, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v1, v4) = v5)) & ! [v4] : ( ~ (v3 = 0) | ~ (occurrence_of(v1, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & leaf(v0, v4) = v5)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (root(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & min_precedes(v3, v0, v1) = 0) | ( ~ (v3 = 0) & leaf(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (legal(v2) = v1) | ~ (legal(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (activity(v2) = v1) | ~ (activity(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (activity_occurrence(v2) = v1) | ~ (activity_occurrence(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (arboreal(v2) = v1) | ~ (arboreal(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atomic(v2) = v1) | ~ (atomic(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (next_subocc(v0, v1, v2) = 0) | min_precedes(v0, v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (next_subocc(v0, v1, v2) = 0) | (arboreal(v1) = 0 & arboreal(v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (earlier(v1, v2) = 0) | ~ (earlier(v0, v1) = 0) | earlier(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (earlier(v0, v1) = v2) | ? [v3] : ((v3 = 0 & v2 = 0 & legal(v1) = 0) | ( ~ (v3 = 0) & precedes(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (leaf(v0, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & leaf_occ(v0, v1) = 0) | ( ~ (v3 = 0) & occurrence_of(v1, v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (leaf(v0, v1) = 0) | ~ (min_precedes(v0, v2, v1) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v1, v2, v0) = 0) | ? [v3] : (occurrence_of(v3, v0) = 0 & subactivity_occurrence(v2, v3) = 0 & subactivity_occurrence(v1, v3) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | precedes(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & min_precedes(v3, v1, v2) = 0 & min_precedes(v0, v3, v2) = 0) | (v3 = 0 & next_subocc(v0, v1, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : ( ~ (v3 = 0) & root(v1, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : (min_precedes(v3, v1, v2) = 0 & root(v3, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (occurrence_of(v1, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & root_occ(v0, v1) = 0) | ( ~ (v3 = 0) & root(v0, v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (occurrence_of(v1, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & leaf_occ(v0, v1) = 0) | ( ~ (v3 = 0) & leaf(v0, v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (root(v0, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & root_occ(v0, v1) = 0) | ( ~ (v3 = 0) & occurrence_of(v1, v2) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subactivity_occurrence(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & v2 = 0 & leaf(v0, v3) = 0 & occurrence_of(v1, v3) = 0) | ( ~ (v3 = 0) & leaf_occ(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (subactivity_occurrence(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & v2 = 0 & occurrence_of(v1, v3) = 0 & root(v0, v3) = 0) | ( ~ (v3 = 0) & root_occ(v0, v1) = v3))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (arboreal(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & legal(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (precedes(v0, v1) = 0) | (earlier(v0, v1) = 0 & legal(v1) = 0)) & ! [v0] : ! [v1] : ( ~ (earlier(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & earlier(v0, v1) = v2)) & ! [v0] : ! [v1] : ( ~ (earlier(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & earlier(v1, v0) = v2)) & ! [v0] : ! [v1] : ( ~ (earlier(v0, v1) = 0) | ? [v2] : ((v2 = 0 & precedes(v0, v1) = 0) | ( ~ (v2 = 0) & legal(v1) = v2))) & ! [v0] : ! [v1] : ( ~ (leaf(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & leaf_occ(v0, v2) = 0 & occurrence_of(v2, v1) = 0) | (v2 = 0 & atomic(v1) = 0))) & ! [v0] : ! [v1] : ( ~ (leaf(v0, v1) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & min_precedes(v2, v0, v1) = 0) | (v2 = 0 & root(v0, v1) = 0))) & ! [v0] : ! [v1] : ( ~ (atocc(v0, v1) = 0) | ? [v2] : (subactivity(v1, v2) = 0 & occurrence_of(v0, v2) = 0 & atomic(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (min_precedes(v0, v1, tptp0) = 0) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & ~ (v2 = 0) & occurrence_of(v1, tptp1) = v3 & occurrence_of(v1, tptp2) = v2) | ( ~ (v2 = 0) & root_occ(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & occurrence_of(v0, tptp3) = v2))) & ! [v0] : ! [v1] : ( ~ (root_occ(v0, v1) = 0) | ? [v2] : (occurrence_of(v1, v2) = 0 & root(v0, v2) = 0 & subactivity_occurrence(v0, v1) = 0)) & ! [v0] : ! [v1] : ( ~ (leaf_occ(v0, v1) = 0) | ? [v2] : (leaf(v0, v2) = 0 & occurrence_of(v1, v2) = 0 & subactivity_occurrence(v0, v1) = 0)) & ! [v0] : ! [v1] : ( ~ (occurrence_of(v1, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & root(v2, v0) = 0 & subactivity_occurrence(v2, v1) = 0) | (v2 = 0 & atomic(v0) = 0))) & ! [v0] : ! [v1] : ( ~ (occurrence_of(v1, v0) = 0) | (activity(v0) = 0 & activity_occurrence(v1) = 0)) & ! [v0] : ! [v1] : ( ~ (occurrence_of(v0, v1) = 0) | ? [v2] : ? [v3] : (((v3 = 0 & atomic(v1) = 0) | ( ~ (v2 = 0) & arboreal(v0) = v2)) & ((v2 = 0 & arboreal(v0) = 0) | ( ~ (v3 = 0) & atomic(v1) = v3)))) & ! [v0] : ! [v1] : ( ~ (root(v1, v0) = 0) | ? [v2] : (subactivity(v2, v0) = 0 & atocc(v1, v2) = 0)) & ! [v0] : ! [v1] : ( ~ (root(v0, v1) = 0) | legal(v0) = 0) & ! [v0] : ! [v1] : ( ~ (root(v0, v1) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & min_precedes(v0, v2, v1) = 0) | (v2 = 0 & leaf(v0, v1) = 0))) & ! [v0] : ! [v1] : ( ~ (subactivity_occurrence(v0, v1) = 0) | (activity_occurrence(v1) = 0 & activity_occurrence(v0) = 0)) & ! [v0] : ( ~ (legal(v0) = 0) | arboreal(v0) = 0) & ! [v0] : ( ~ (activity_occurrence(v0) = 0) | ? [v1] : (activity(v1) = 0 & occurrence_of(v0, v1) = 0)) & ! [v0] : ( ~ (occurrence_of(v0, tptp0) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (min_precedes(v2, v3, tptp0) = 0 & min_precedes(v1, v2, tptp0) = 0 & root_occ(v1, v0) = 0 & occurrence_of(v2, tptp4) = 0 & occurrence_of(v1, tptp3) = 0 & ! [v6] : (v6 = v3 | v6 = v2 | ~ (min_precedes(v1, v6, tptp0) = 0)) & ((v5 = 0 & occurrence_of(v3, tptp1) = 0) | (v4 = 0 & occurrence_of(v3, tptp2) = 0)))) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : next_subocc(v2, v1, v0) = v3 & ? [v0] : ? [v1] : ? [v2] : ? [v3] : min_precedes(v2, v1, v0) = v3 & ? [v0] : ? [v1] : ? [v2] : precedes(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : earlier(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : leaf(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subactivity(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : atocc(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : root_occ(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : leaf_occ(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : occurrence_of(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : root(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : subactivity_occurrence(v1, v0) = v2 & ? [v0] : ? [v1] : legal(v0) = v1 & ? [v0] : ? [v1] : activity(v0) = v1 & ? [v0] : ? [v1] : activity_occurrence(v0) = v1 & ? [v0] : ? [v1] : arboreal(v0) = v1 & ? [v0] : ? [v1] : atomic(v0) = v1 % 58.63/20.17 | % 58.63/20.17 | Applying alpha-rule on (1) yields: % 58.63/20.17 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (root_occ(v3, v1) = 0) | ~ (leaf_occ(v4, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v4, v0) = 0) | ( ~ (v5 = 0) & min_precedes(v3, v2, v0) = v5))) % 58.63/20.17 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v0, v1, v2) = 0) | ~ (subactivity_occurrence(v0, v3) = v4) | ? [v5] : (( ~ (v5 = 0) & occurrence_of(v3, v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v1, v3) = v5))) % 58.63/20.17 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ (next_subocc(v0, v1, v2) = 0) | (arboreal(v1) = 0 & arboreal(v0) = 0)) % 58.63/20.17 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (leaf_occ(v3, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v2) = v4))) % 58.63/20.18 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (next_subocc(v0, v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & min_precedes(v4, v1, v2) = 0 & min_precedes(v0, v4, v2) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v1, v2) = v4))) % 58.63/20.18 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (atocc(v0, v1) = v2) | ~ (occurrence_of(v0, v3) = 0) | ? [v4] : (( ~ (v4 = 0) & subactivity(v1, v3) = v4) | ( ~ (v4 = 0) & atomic(v3) = v4))) % 58.63/20.18 | (8) ? [v0] : ? [v1] : ? [v2] : leaf(v1, v0) = v2 % 58.63/20.18 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v2) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v3) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) % 58.63/20.18 | (10) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (precedes(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & earlier(v0, v1) = v3) | ( ~ (v3 = 0) & legal(v1) = v3))) % 58.63/20.18 | (11) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (activity_occurrence(v2) = v1) | ~ (activity_occurrence(v2) = v0)) % 58.63/20.18 | (12) ~ (tptp4 = tptp3) % 58.63/20.18 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & leaf_occ(v3, v1) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5))) % 58.63/20.18 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5))) % 58.63/20.18 | (15) ! [v0] : ( ~ (activity_occurrence(v0) = 0) | ? [v1] : (activity(v1) = 0 & occurrence_of(v0, v1) = 0)) % 58.63/20.18 | (16) ~ (tptp1 = tptp3) % 58.63/20.18 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (atocc(v3, v2) = v1) | ~ (atocc(v3, v2) = v0)) % 58.63/20.18 | (18) ! [v0] : ! [v1] : ( ~ (precedes(v0, v1) = 0) | (earlier(v0, v1) = 0 & legal(v1) = 0)) % 58.63/20.18 | (19) ~ (tptp2 = tptp4) % 58.63/20.18 | (20) atomic(tptp3) = 0 % 58.63/20.18 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root_occ(v1, v2) = 0) | ~ (root_occ(v0, v2) = 0) | ~ (occurrence_of(v2, v3) = 0)) % 58.63/20.18 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (min_precedes(v2, v4, v0) = v5) | ~ (occurrence_of(v1, v0) = 0) | ? [v6] : (( ~ (v6 = 0) & root_occ(v3, v1) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v2, v1) = v6))) % 58.63/20.18 | (23) ! [v0] : ( ~ (legal(v0) = 0) | arboreal(v0) = 0) % 58.63/20.18 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ (occurrence_of(v1, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & root_occ(v0, v1) = 0) | ( ~ (v3 = 0) & root(v0, v2) = v3))) % 58.63/20.18 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root(v3, v2) = v1) | ~ (root(v3, v2) = v0)) % 58.63/20.18 | (26) ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : (min_precedes(v3, v1, v2) = 0 & root(v3, v2) = 0)) % 58.63/20.18 | (27) ! [v0] : ! [v1] : ( ~ (atocc(v0, v1) = 0) | ? [v2] : (subactivity(v1, v2) = 0 & occurrence_of(v0, v2) = 0 & atomic(v2) = 0)) % 58.63/20.18 | (28) ? [v0] : ? [v1] : activity_occurrence(v0) = v1 % 58.63/20.18 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (next_subocc(v0, v1, v2) = 0) | ~ (min_precedes(v0, v3, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & min_precedes(v3, v1, v2) = v4)) % 58.63/20.18 | (30) ! [v0] : ! [v1] : ( ~ (root_occ(v0, v1) = 0) | ? [v2] : (occurrence_of(v1, v2) = 0 & root(v0, v2) = 0 & subactivity_occurrence(v0, v1) = 0)) % 58.63/20.18 | (31) ? [v0] : ? [v1] : ? [v2] : subactivity(v1, v0) = v2 % 58.63/20.19 | (32) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (occurrence_of(v0, v2) = 0) | ~ (occurrence_of(v0, v1) = 0)) % 58.63/20.19 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (earlier(v0, v2) = v3) | ~ (earlier(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & earlier(v1, v2) = v4)) % 58.63/20.19 | (34) ! [v0] : ! [v1] : ( ~ (earlier(v0, v1) = 0) | ? [v2] : ((v2 = 0 & precedes(v0, v1) = 0) | ( ~ (v2 = 0) & legal(v1) = v2))) % 58.63/20.19 | (35) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (arboreal(v2) = v1) | ~ (arboreal(v2) = v0)) % 58.63/20.19 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (precedes(v1, v2) = 0) | ~ (min_precedes(v0, v2, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v1, v3) = v4))) % 58.63/20.19 | (37) ! [v0] : ! [v1] : ( ~ (root(v0, v1) = 0) | legal(v0) = 0) % 58.63/20.19 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (subactivity_occurrence(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & v2 = 0 & leaf(v0, v3) = 0 & occurrence_of(v1, v3) = 0) | ( ~ (v3 = 0) & leaf_occ(v0, v1) = v3))) % 58.63/20.19 | (39) ? [v0] : ? [v1] : ? [v2] : root_occ(v1, v0) = v2 % 58.63/20.19 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5))) % 58.63/20.19 | (41) ? [v0] : ? [v1] : ? [v2] : leaf_occ(v1, v0) = v2 % 58.63/20.19 | (42) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (activity(v2) = v1) | ~ (activity(v2) = v0)) % 58.63/20.19 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (leaf(v0, v1) = v2) | ~ (min_precedes(v3, v0, v1) = 0) | ? [v4] : min_precedes(v0, v4, v1) = 0) % 58.63/20.19 | (44) ! [v0] : ! [v1] : ( ~ (root(v1, v0) = 0) | ? [v2] : (subactivity(v2, v0) = 0 & atocc(v1, v2) = 0)) % 58.63/20.19 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (earlier(v3, v2) = v1) | ~ (earlier(v3, v2) = v0)) % 58.63/20.19 | (46) ! [v0] : ! [v1] : ( ~ (subactivity_occurrence(v0, v1) = 0) | (activity_occurrence(v1) = 0 & activity_occurrence(v0) = 0)) % 58.63/20.19 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v3, v1) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v3) = v4) | ( ~ (v4 = 0) & arboreal(v2) = v4))) % 58.63/20.19 | (48) atomic(tptp1) = 0 % 58.63/20.19 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ (next_subocc(v0, v1, v2) = 0) | min_precedes(v0, v1, v2) = 0) % 58.63/20.19 | (50) ! [v0] : ! [v1] : ( ~ (occurrence_of(v1, v0) = 0) | (activity(v0) = 0 & activity_occurrence(v1) = 0)) % 58.63/20.19 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v3, v1) = 0) | ~ (root(v0, v1) = v2) | ? [v4] : ( ~ (v4 = 0) & leaf(v0, v1) = v4)) % 58.63/20.19 | (52) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leaf(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & min_precedes(v0, v3, v1) = 0) | ( ~ (v3 = 0) & root(v0, v1) = v3))) % 58.63/20.19 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ (earlier(v1, v2) = 0) | ~ (earlier(v0, v1) = 0) | earlier(v0, v2) = 0) % 58.63/20.19 | (54) ? [v0] : ? [v1] : activity(v0) = v1 % 58.63/20.19 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (min_precedes(v0, v1, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & next_subocc(v0, v1, v2) = v4)) % 58.63/20.20 | (56) ~ (tptp2 = tptp3) % 58.63/20.20 | (57) ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : ( ~ (v3 = 0) & root(v1, v2) = v3)) % 58.63/20.20 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & leaf_occ(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 58.63/20.20 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ (root(v0, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & root_occ(v0, v1) = 0) | ( ~ (v3 = 0) & occurrence_of(v1, v2) = v3))) % 58.63/20.20 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 58.63/20.20 | (61) ? [v0] : ? [v1] : arboreal(v0) = v1 % 58.63/20.20 | (62) ~ (tptp1 = tptp2) % 58.63/20.20 | (63) ! [v0] : ! [v1] : ! [v2] : ( ~ (occurrence_of(v1, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & leaf_occ(v0, v1) = 0) | ( ~ (v3 = 0) & leaf(v0, v2) = v3))) % 58.63/20.20 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (root_occ(v3, v2) = v1) | ~ (root_occ(v3, v2) = v0)) % 58.63/20.20 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (occurrence_of(v3, v2) = 0) | ~ (subactivity_occurrence(v1, v3) = 0) | ~ (subactivity_occurrence(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & min_precedes(v0, v1, v2) = v5)) % 58.63/20.20 | (66) atomic(tptp0) = all_0_1_1 % 58.63/20.20 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subactivity(v3, v2) = v1) | ~ (subactivity(v3, v2) = v0)) % 58.63/20.20 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (occurrence_of(v3, v2) = v1) | ~ (occurrence_of(v3, v2) = v0)) % 58.63/20.20 | (69) ? [v0] : ? [v1] : ? [v2] : ? [v3] : min_precedes(v2, v1, v0) = v3 % 58.63/20.20 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (leaf_occ(v4, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v4, v0) = 0) | ( ~ (v5 = 0) & root_occ(v3, v1) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 58.63/20.20 | (71) ! [v0] : ! [v1] : (v1 = 0 | ~ (arboreal(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & legal(v0) = v2)) % 58.63/20.20 | (72) ! [v0] : ! [v1] : ( ~ (earlier(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & earlier(v1, v0) = v2)) % 58.63/20.20 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v2) = 0) | ~ (leaf_occ(v3, v1) = 0) | ~ (occurrence_of(v1, v0) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) % 58.63/20.20 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v3) = 0) | ~ (arboreal(v2) = 0) | ~ (occurrence_of(v1, v0) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v3, v1) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v2, v1) = v4))) % 58.63/20.20 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (subactivity(v1, v3) = 0) | ~ (atocc(v0, v1) = v2) | ? [v4] : (( ~ (v4 = 0) & occurrence_of(v0, v3) = v4) | ( ~ (v4 = 0) & atomic(v3) = v4))) % 58.63/20.20 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v1, v2) = 0) | ~ (subactivity_occurrence(v1, v3) = 0) | ? [v4] : ((v4 = 0 & subactivity_occurrence(v0, v3) = 0) | ( ~ (v4 = 0) & occurrence_of(v3, v2) = v4))) % 58.63/20.20 | (77) ! [v0] : ! [v1] : ( ~ (earlier(v1, v0) = 0) | ? [v2] : ( ~ (v2 = 0) & earlier(v0, v1) = v2)) % 58.63/20.20 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf_occ(v1, v2) = 0) | ~ (leaf_occ(v0, v2) = 0) | ~ (occurrence_of(v2, v3) = 0) | atomic(v3) = 0) % 58.63/20.20 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v3, v1, v2) = 0) | ~ (root_occ(v1, v0) = 0) | ~ (occurrence_of(v0, v2) = 0)) % 58.63/20.20 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (min_precedes(v4, v3, v2) = v1) | ~ (min_precedes(v4, v3, v2) = v0)) % 58.63/20.20 | (81) ? [v0] : ? [v1] : ? [v2] : earlier(v1, v0) = v2 % 58.63/20.20 | (82) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf_occ(v3, v2) = v1) | ~ (leaf_occ(v3, v2) = v0)) % 58.63/20.20 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v1 = v0 | ~ (leaf_occ(v1, v2) = 0) | ~ (leaf_occ(v0, v2) = 0) | ~ (atomic(v3) = v4) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v2, v3) = v5)) % 58.63/20.20 | (84) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (precedes(v3, v2) = v1) | ~ (precedes(v3, v2) = v0)) % 58.63/20.20 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v1, v2, v3) = v4) | ~ (min_precedes(v0, v2, v3) = 0) | ? [v5] : (( ~ (v5 = 0) & precedes(v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v1, v3) = v5))) % 58.63/20.20 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (next_subocc(v0, v1, v2) = 0) | ~ (min_precedes(v3, v1, v2) = 0) | ? [v4] : ( ~ (v4 = 0) & min_precedes(v0, v3, v2) = v4)) % 58.63/20.20 | (87) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v4, v1, v2) = 0) | ~ (min_precedes(v0, v1, v2) = v3) | ? [v5] : (( ~ (v5 = 0) & next_subocc(v0, v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v4, v2) = v5))) % 58.63/20.20 | (88) ? [v0] : ? [v1] : legal(v0) = v1 % 58.63/20.20 | (89) activity(tptp0) = 0 % 58.63/20.20 | (90) ! [v0] : ! [v1] : ( ~ (occurrence_of(v1, v0) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & root(v2, v0) = 0 & subactivity_occurrence(v2, v1) = 0) | (v2 = 0 & atomic(v0) = 0))) % 58.63/20.20 | (91) atomic(tptp4) = 0 % 58.63/20.20 | (92) ? [v0] : ? [v1] : ? [v2] : root(v1, v0) = v2 % 58.63/20.20 | (93) ! [v0] : ! [v1] : ( ~ (leaf(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & leaf_occ(v0, v2) = 0 & occurrence_of(v2, v1) = 0) | (v2 = 0 & atomic(v1) = 0))) % 58.63/20.20 | (94) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v1, v2) = 0) | ~ (occurrence_of(v3, v2) = 0) | ? [v4] : ((v4 = 0 & subactivity_occurrence(v0, v3) = 0) | ( ~ (v4 = 0) & subactivity_occurrence(v1, v3) = v4))) % 58.63/20.20 | (95) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leaf(v3, v2) = v1) | ~ (leaf(v3, v2) = v0)) % 58.63/20.20 | (96) ! [v0] : ! [v1] : ! [v2] : ( ~ (subactivity_occurrence(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & v2 = 0 & occurrence_of(v1, v3) = 0 & root(v0, v3) = 0) | ( ~ (v3 = 0) & root_occ(v0, v1) = v3))) % 58.63/20.21 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v3, v0, v1) = 0) | ~ (root(v0, v1) = v2) | ? [v4] : ? [v5] : ((v5 = 0 & min_precedes(v0, v4, v1) = 0) | (v4 = 0 & leaf(v0, v1) = 0))) % 58.63/20.21 | (98) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v0, v2, v3) = 0) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & precedes(v1, v2) = v4))) % 58.63/20.21 | (99) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (min_precedes(v1, v3, v2) = 0) | ~ (leaf_occ(v1, v0) = 0) | ~ (occurrence_of(v0, v2) = 0)) % 58.63/20.21 | (100) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (precedes(v1, v2) = 0) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v1, v2, v3) = 0) | ( ~ (v4 = 0) & min_precedes(v0, v2, v3) = v4))) % 58.63/20.21 | (101) occurrence_of(all_0_0_0, tptp0) = 0 % 58.63/20.21 | (102) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (atomic(v2) = v1) | ~ (atomic(v2) = v0)) % 58.63/20.21 | (103) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (legal(v2) = v1) | ~ (legal(v2) = v0)) % 58.63/20.21 | (104) ? [v0] : ? [v1] : ? [v2] : subactivity_occurrence(v1, v0) = v2 % 58.63/20.21 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (min_precedes(v0, v4, v2) = 0) | ~ (min_precedes(v0, v1, v2) = v3) | ? [v5] : (( ~ (v5 = 0) & next_subocc(v0, v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v4, v1, v2) = v5))) % 58.63/20.21 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (leaf_occ(v3, v1) = 0) | ? [v5] : (( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 58.63/20.21 | (107) ~ (tptp1 = tptp4) % 58.63/20.21 | (108) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 58.63/20.21 | (109) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leaf_occ(v0, v1) = v2) | ? [v3] : (subactivity_occurrence(v0, v1) = v3 & ! [v4] : ( ~ (v3 = 0) | ~ (leaf(v0, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v1, v4) = v5)) & ! [v4] : ( ~ (v3 = 0) | ~ (occurrence_of(v1, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & leaf(v0, v4) = v5)))) % 58.63/20.21 | (110) ? [v0] : ? [v1] : atomic(v0) = v1 % 58.63/20.21 | (111) ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & min_precedes(v3, v1, v2) = 0 & min_precedes(v0, v3, v2) = 0) | (v3 = 0 & next_subocc(v0, v1, v2) = 0))) % 58.63/20.21 | (112) ! [v0] : ! [v1] : ( ~ (leaf_occ(v0, v1) = 0) | ? [v2] : (leaf(v0, v2) = 0 & occurrence_of(v1, v2) = 0 & subactivity_occurrence(v0, v1) = 0)) % 58.63/20.21 | (113) ? [v0] : ? [v1] : ? [v2] : precedes(v1, v0) = v2 % 58.63/20.21 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (min_precedes(v1, v2, v3) = v4) | ~ (min_precedes(v0, v1, v3) = 0) | ? [v5] : (( ~ (v5 = 0) & precedes(v1, v2) = v5) | ( ~ (v5 = 0) & min_precedes(v0, v2, v3) = v5))) % 59.12/20.21 | (115) ! [v0] : ! [v1] : ! [v2] : ( ~ (earlier(v0, v1) = v2) | ? [v3] : ((v3 = 0 & v2 = 0 & legal(v1) = 0) | ( ~ (v3 = 0) & precedes(v0, v1) = v3))) % 59.12/20.21 | (116) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (earlier(v1, v2) = 0) | ~ (earlier(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & earlier(v0, v1) = v4)) % 59.12/20.21 | (117) ? [v0] : ? [v1] : ? [v2] : atocc(v1, v0) = v2 % 59.12/20.21 | (118) ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v0, v1, v2) = 0) | precedes(v0, v1) = 0) % 59.12/20.21 | (119) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v3, v2, v0) = 0) | ~ (min_precedes(v2, v4, v0) = v5) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v6] : (( ~ (v6 = 0) & root_occ(v3, v1) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & occurrence_of(v1, v0) = v6))) % 59.12/20.21 | (120) ! [v0] : ! [v1] : ! [v2] : ( ~ (leaf(v0, v1) = 0) | ~ (min_precedes(v0, v2, v1) = 0)) % 59.12/20.21 | (121) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (root_occ(v0, v1) = v2) | ? [v3] : (subactivity_occurrence(v0, v1) = v3 & ! [v4] : ( ~ (v3 = 0) | ~ (occurrence_of(v1, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & root(v0, v4) = v5)) & ! [v4] : ( ~ (v3 = 0) | ~ (root(v0, v4) = 0) | ? [v5] : ( ~ (v5 = 0) & occurrence_of(v1, v4) = v5)))) % 59.12/20.21 | (122) ! [v0] : ! [v1] : ( ~ (root(v0, v1) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & min_precedes(v0, v2, v1) = 0) | (v2 = 0 & leaf(v0, v1) = 0))) % 59.12/20.21 | (123) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (root(v0, v1) = v2) | ? [v3] : ? [v4] : ((v4 = 0 & min_precedes(v3, v0, v1) = 0) | ( ~ (v3 = 0) & leaf(v0, v1) = v3))) % 59.12/20.21 | (124) ! [v0] : ( ~ (occurrence_of(v0, tptp0) = 0) | ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (min_precedes(v2, v3, tptp0) = 0 & min_precedes(v1, v2, tptp0) = 0 & root_occ(v1, v0) = 0 & occurrence_of(v2, tptp4) = 0 & occurrence_of(v1, tptp3) = 0 & ! [v6] : (v6 = v3 | v6 = v2 | ~ (min_precedes(v1, v6, tptp0) = 0)) & ((v5 = 0 & occurrence_of(v3, tptp1) = 0) | (v4 = 0 & occurrence_of(v3, tptp2) = 0)))) % 59.12/20.21 | (125) ? [v0] : ? [v1] : ? [v2] : ? [v3] : next_subocc(v2, v1, v0) = v3 % 59.12/20.21 | (126) ! [v0] : ! [v1] : ! [v2] : ( ~ (min_precedes(v1, v2, v0) = 0) | ? [v3] : (occurrence_of(v3, v0) = 0 & subactivity_occurrence(v2, v3) = 0 & subactivity_occurrence(v1, v3) = 0)) % 59.12/20.21 | (127) atomic(tptp2) = 0 % 59.12/20.21 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (arboreal(v3) = 0) | ~ (occurrence_of(v1, v0) = 0) | ~ (subactivity_occurrence(v2, v1) = 0) | ? [v4] : ((v4 = 0 & min_precedes(v3, v2, v0) = 0) | (v4 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v4 = 0) & arboreal(v2) = v4) | ( ~ (v4 = 0) & subactivity_occurrence(v3, v1) = v4))) % 59.12/20.21 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (subactivity_occurrence(v3, v2) = v1) | ~ (subactivity_occurrence(v3, v2) = v0)) % 59.12/20.21 | (130) ! [v0] : ! [v1] : ( ~ (min_precedes(v0, v1, tptp0) = 0) | ? [v2] : ? [v3] : (( ~ (v3 = 0) & ~ (v2 = 0) & occurrence_of(v1, tptp1) = v3 & occurrence_of(v1, tptp2) = v2) | ( ~ (v2 = 0) & root_occ(v0, all_0_0_0) = v2) | ( ~ (v2 = 0) & occurrence_of(v0, tptp3) = v2))) % 59.12/20.21 | (131) ? [v0] : ? [v1] : ? [v2] : occurrence_of(v1, v0) = v2 % 59.12/20.21 | (132) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v2, v3, v0) = v4) | ~ (occurrence_of(v1, v0) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v3, v2, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v3, v1) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 59.12/20.21 | (133) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (next_subocc(v4, v3, v2) = v1) | ~ (next_subocc(v4, v3, v2) = v0)) % 59.12/20.21 | (134) ! [v0] : ! [v1] : ( ~ (leaf(v0, v1) = 0) | ? [v2] : ? [v3] : ((v3 = 0 & min_precedes(v2, v0, v1) = 0) | (v2 = 0 & root(v0, v1) = 0))) % 59.12/20.22 | (135) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = v2 | ~ (min_precedes(v3, v2, v0) = v4) | ~ (subactivity_occurrence(v3, v1) = 0) | ? [v5] : ((v5 = 0 & min_precedes(v2, v3, v0) = 0) | ( ~ (v5 = 0) & arboreal(v3) = v5) | ( ~ (v5 = 0) & arboreal(v2) = v5) | ( ~ (v5 = 0) & occurrence_of(v1, v0) = v5) | ( ~ (v5 = 0) & subactivity_occurrence(v2, v1) = v5))) % 59.12/20.22 | (136) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (atocc(v0, v1) = v2) | ~ (atomic(v3) = 0) | ? [v4] : (( ~ (v4 = 0) & subactivity(v1, v3) = v4) | ( ~ (v4 = 0) & occurrence_of(v0, v3) = v4))) % 59.12/20.22 | (137) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = v2 | ~ (min_precedes(v2, v4, v0) = v5) | ~ (root_occ(v3, v1) = 0) | ? [v6] : (( ~ (v6 = 0) & min_precedes(v3, v2, v0) = v6) | ( ~ (v6 = 0) & leaf_occ(v4, v1) = v6) | ( ~ (v6 = 0) & occurrence_of(v1, v0) = v6) | ( ~ (v6 = 0) & subactivity_occurrence(v2, v1) = v6))) % 59.12/20.22 | (138) ! [v0] : ! [v1] : ! [v2] : ( ~ (leaf(v0, v2) = 0) | ~ (subactivity_occurrence(v0, v1) = 0) | ? [v3] : ((v3 = 0 & leaf_occ(v0, v1) = 0) | ( ~ (v3 = 0) & occurrence_of(v1, v2) = v3))) % 59.12/20.22 | (139) ~ (all_0_1_1 = 0) % 59.12/20.22 | (140) ! [v0] : ! [v1] : ( ~ (occurrence_of(v0, v1) = 0) | ? [v2] : ? [v3] : (((v3 = 0 & atomic(v1) = 0) | ( ~ (v2 = 0) & arboreal(v0) = v2)) & ((v2 = 0 & arboreal(v0) = 0) | ( ~ (v3 = 0) & atomic(v1) = v3)))) % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (124) with all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, tptp0) = 0, yields: % 59.12/20.22 | (141) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (min_precedes(v1, v2, tptp0) = 0 & min_precedes(v0, v1, tptp0) = 0 & root_occ(v0, all_0_0_0) = 0 & occurrence_of(v1, tptp4) = 0 & occurrence_of(v0, tptp3) = 0 & ! [v5] : (v5 = v2 | v5 = v1 | ~ (min_precedes(v0, v5, tptp0) = 0)) & ((v4 = 0 & occurrence_of(v2, tptp1) = 0) | (v3 = 0 & occurrence_of(v2, tptp2) = 0))) % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (90) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0) = 0, yields: % 59.12/20.22 | (142) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & root(v0, tptp0) = 0 & subactivity_occurrence(v0, all_0_0_0) = 0) | (v0 = 0 & atomic(tptp0) = 0)) % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (50) with all_0_0_0, tptp0 and discharging atoms occurrence_of(all_0_0_0, tptp0) = 0, yields: % 59.12/20.22 | (143) activity(tptp0) = 0 & activity_occurrence(all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (143) yields: % 59.12/20.22 | (89) activity(tptp0) = 0 % 59.12/20.22 | (145) activity_occurrence(all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (140) with tptp0, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, tptp0) = 0, yields: % 59.12/20.22 | (146) ? [v0] : ? [v1] : (((v1 = 0 & atomic(tptp0) = 0) | ( ~ (v0 = 0) & arboreal(all_0_0_0) = v0)) & ((v0 = 0 & arboreal(all_0_0_0) = 0) | ( ~ (v1 = 0) & atomic(tptp0) = v1))) % 59.12/20.22 | % 59.12/20.22 | Instantiating (142) with all_43_0_50, all_43_1_51, all_43_2_52 yields: % 59.12/20.22 | (147) (all_43_0_50 = 0 & all_43_1_51 = 0 & root(all_43_2_52, tptp0) = 0 & subactivity_occurrence(all_43_2_52, all_0_0_0) = 0) | (all_43_2_52 = 0 & atomic(tptp0) = 0) % 59.12/20.22 | % 59.12/20.22 | Instantiating (141) with all_44_0_53, all_44_1_54, all_44_2_55, all_44_3_56, all_44_4_57 yields: % 59.12/20.22 | (148) min_precedes(all_44_3_56, all_44_2_55, tptp0) = 0 & min_precedes(all_44_4_57, all_44_3_56, tptp0) = 0 & root_occ(all_44_4_57, all_0_0_0) = 0 & occurrence_of(all_44_3_56, tptp4) = 0 & occurrence_of(all_44_4_57, tptp3) = 0 & ! [v0] : (v0 = all_44_2_55 | v0 = all_44_3_56 | ~ (min_precedes(all_44_4_57, v0, tptp0) = 0)) & ((all_44_0_53 = 0 & occurrence_of(all_44_2_55, tptp1) = 0) | (all_44_1_54 = 0 & occurrence_of(all_44_2_55, tptp2) = 0)) % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (148) yields: % 59.12/20.22 | (149) (all_44_0_53 = 0 & occurrence_of(all_44_2_55, tptp1) = 0) | (all_44_1_54 = 0 & occurrence_of(all_44_2_55, tptp2) = 0) % 59.12/20.22 | (150) occurrence_of(all_44_4_57, tptp3) = 0 % 59.12/20.22 | (151) min_precedes(all_44_4_57, all_44_3_56, tptp0) = 0 % 59.12/20.22 | (152) occurrence_of(all_44_3_56, tptp4) = 0 % 59.12/20.22 | (153) ! [v0] : (v0 = all_44_2_55 | v0 = all_44_3_56 | ~ (min_precedes(all_44_4_57, v0, tptp0) = 0)) % 59.12/20.22 | (154) root_occ(all_44_4_57, all_0_0_0) = 0 % 59.12/20.22 | (155) min_precedes(all_44_3_56, all_44_2_55, tptp0) = 0 % 59.12/20.22 | % 59.12/20.22 | Instantiating (146) with all_47_0_58, all_47_1_59 yields: % 59.12/20.22 | (156) ((all_47_0_58 = 0 & atomic(tptp0) = 0) | ( ~ (all_47_1_59 = 0) & arboreal(all_0_0_0) = all_47_1_59)) & ((all_47_1_59 = 0 & arboreal(all_0_0_0) = 0) | ( ~ (all_47_0_58 = 0) & atomic(tptp0) = all_47_0_58)) % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (156) yields: % 59.12/20.22 | (157) (all_47_0_58 = 0 & atomic(tptp0) = 0) | ( ~ (all_47_1_59 = 0) & arboreal(all_0_0_0) = all_47_1_59) % 59.12/20.22 | (158) (all_47_1_59 = 0 & arboreal(all_0_0_0) = 0) | ( ~ (all_47_0_58 = 0) & atomic(tptp0) = all_47_0_58) % 59.12/20.22 | % 59.12/20.22 +-Applying beta-rule and splitting (147), into two cases. % 59.12/20.22 |-Branch one: % 59.12/20.22 | (159) all_43_0_50 = 0 & all_43_1_51 = 0 & root(all_43_2_52, tptp0) = 0 & subactivity_occurrence(all_43_2_52, all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (159) yields: % 59.12/20.22 | (160) all_43_0_50 = 0 % 59.12/20.22 | (161) all_43_1_51 = 0 % 59.12/20.22 | (162) root(all_43_2_52, tptp0) = 0 % 59.12/20.22 | (163) subactivity_occurrence(all_43_2_52, all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 +-Applying beta-rule and splitting (157), into two cases. % 59.12/20.22 |-Branch one: % 59.12/20.22 | (164) all_47_0_58 = 0 & atomic(tptp0) = 0 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (164) yields: % 59.12/20.22 | (165) all_47_0_58 = 0 % 59.12/20.22 | (166) atomic(tptp0) = 0 % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (102) with tptp0, 0, all_0_1_1 and discharging atoms atomic(tptp0) = all_0_1_1, atomic(tptp0) = 0, yields: % 59.12/20.22 | (167) all_0_1_1 = 0 % 59.12/20.22 | % 59.12/20.22 | Equations (167) can reduce 139 to: % 59.12/20.22 | (168) $false % 59.12/20.22 | % 59.12/20.22 |-The branch is then unsatisfiable % 59.12/20.22 |-Branch two: % 59.12/20.22 | (169) ~ (all_47_1_59 = 0) & arboreal(all_0_0_0) = all_47_1_59 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (169) yields: % 59.12/20.22 | (170) ~ (all_47_1_59 = 0) % 59.12/20.22 | (171) arboreal(all_0_0_0) = all_47_1_59 % 59.12/20.22 | % 59.12/20.22 +-Applying beta-rule and splitting (158), into two cases. % 59.12/20.22 |-Branch one: % 59.12/20.22 | (172) all_47_1_59 = 0 & arboreal(all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (172) yields: % 59.12/20.22 | (173) all_47_1_59 = 0 % 59.12/20.22 | (174) arboreal(all_0_0_0) = 0 % 59.12/20.22 | % 59.12/20.22 | Equations (173) can reduce 170 to: % 59.12/20.22 | (168) $false % 59.12/20.22 | % 59.12/20.22 |-The branch is then unsatisfiable % 59.12/20.22 |-Branch two: % 59.12/20.22 | (176) ~ (all_47_0_58 = 0) & atomic(tptp0) = all_47_0_58 % 59.12/20.22 | % 59.12/20.22 | Applying alpha-rule on (176) yields: % 59.12/20.22 | (177) ~ (all_47_0_58 = 0) % 59.12/20.22 | (178) atomic(tptp0) = all_47_0_58 % 59.12/20.22 | % 59.12/20.22 | Instantiating formula (102) with tptp0, all_47_0_58, all_0_1_1 and discharging atoms atomic(tptp0) = all_47_0_58, atomic(tptp0) = all_0_1_1, yields: % 59.12/20.22 | (179) all_47_0_58 = all_0_1_1 % 59.12/20.22 | % 59.12/20.22 | Equations (179) can reduce 177 to: % 59.12/20.22 | (139) ~ (all_0_1_1 = 0) % 59.12/20.22 | % 59.12/20.22 | From (179) and (178) follows: % 59.12/20.23 | (66) atomic(tptp0) = all_0_1_1 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (15) with all_0_0_0 and discharging atoms activity_occurrence(all_0_0_0) = 0, yields: % 59.12/20.23 | (182) ? [v0] : (activity(v0) = 0 & occurrence_of(all_0_0_0, v0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (126) with all_44_2_55, all_44_3_56, tptp0 and discharging atoms min_precedes(all_44_3_56, all_44_2_55, tptp0) = 0, yields: % 59.12/20.23 | (183) ? [v0] : (occurrence_of(v0, tptp0) = 0 & subactivity_occurrence(all_44_2_55, v0) = 0 & subactivity_occurrence(all_44_3_56, v0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (26) with tptp0, all_44_2_55, all_44_3_56 and discharging atoms min_precedes(all_44_3_56, all_44_2_55, tptp0) = 0, yields: % 59.12/20.23 | (184) ? [v0] : (min_precedes(v0, all_44_2_55, tptp0) = 0 & root(v0, tptp0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (126) with all_44_3_56, all_44_4_57, tptp0 and discharging atoms min_precedes(all_44_4_57, all_44_3_56, tptp0) = 0, yields: % 59.12/20.23 | (185) ? [v0] : (occurrence_of(v0, tptp0) = 0 & subactivity_occurrence(all_44_3_56, v0) = 0 & subactivity_occurrence(all_44_4_57, v0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (26) with tptp0, all_44_3_56, all_44_4_57 and discharging atoms min_precedes(all_44_4_57, all_44_3_56, tptp0) = 0, yields: % 59.12/20.23 | (186) ? [v0] : (min_precedes(v0, all_44_3_56, tptp0) = 0 & root(v0, tptp0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (30) with all_0_0_0, all_44_4_57 and discharging atoms root_occ(all_44_4_57, all_0_0_0) = 0, yields: % 59.12/20.23 | (187) ? [v0] : (occurrence_of(all_0_0_0, v0) = 0 & root(all_44_4_57, v0) = 0 & subactivity_occurrence(all_44_4_57, all_0_0_0) = 0) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (24) with tptp0, all_0_0_0, all_43_2_52 and discharging atoms occurrence_of(all_0_0_0, tptp0) = 0, subactivity_occurrence(all_43_2_52, all_0_0_0) = 0, yields: % 59.12/20.23 | (188) ? [v0] : ((v0 = 0 & root_occ(all_43_2_52, all_0_0_0) = 0) | ( ~ (v0 = 0) & root(all_43_2_52, tptp0) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (96) with 0, all_0_0_0, all_43_2_52 and discharging atoms subactivity_occurrence(all_43_2_52, all_0_0_0) = 0, yields: % 59.12/20.23 | (189) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & occurrence_of(all_0_0_0, v0) = 0 & root(all_43_2_52, v0) = 0) | ( ~ (v0 = 0) & root_occ(all_43_2_52, all_0_0_0) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating (187) with all_72_0_65 yields: % 59.12/20.23 | (190) occurrence_of(all_0_0_0, all_72_0_65) = 0 & root(all_44_4_57, all_72_0_65) = 0 & subactivity_occurrence(all_44_4_57, all_0_0_0) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (190) yields: % 59.12/20.23 | (191) occurrence_of(all_0_0_0, all_72_0_65) = 0 % 59.12/20.23 | (192) root(all_44_4_57, all_72_0_65) = 0 % 59.12/20.23 | (193) subactivity_occurrence(all_44_4_57, all_0_0_0) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating (186) with all_74_0_66 yields: % 59.12/20.23 | (194) min_precedes(all_74_0_66, all_44_3_56, tptp0) = 0 & root(all_74_0_66, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (194) yields: % 59.12/20.23 | (195) min_precedes(all_74_0_66, all_44_3_56, tptp0) = 0 % 59.12/20.23 | (196) root(all_74_0_66, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating (185) with all_76_0_67 yields: % 59.12/20.23 | (197) occurrence_of(all_76_0_67, tptp0) = 0 & subactivity_occurrence(all_44_3_56, all_76_0_67) = 0 & subactivity_occurrence(all_44_4_57, all_76_0_67) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (197) yields: % 59.12/20.23 | (198) occurrence_of(all_76_0_67, tptp0) = 0 % 59.12/20.23 | (199) subactivity_occurrence(all_44_3_56, all_76_0_67) = 0 % 59.12/20.23 | (200) subactivity_occurrence(all_44_4_57, all_76_0_67) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating (184) with all_80_0_70 yields: % 59.12/20.23 | (201) min_precedes(all_80_0_70, all_44_2_55, tptp0) = 0 & root(all_80_0_70, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (201) yields: % 59.12/20.23 | (202) min_precedes(all_80_0_70, all_44_2_55, tptp0) = 0 % 59.12/20.23 | (203) root(all_80_0_70, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating (188) with all_91_0_84 yields: % 59.12/20.23 | (204) (all_91_0_84 = 0 & root_occ(all_43_2_52, all_0_0_0) = 0) | ( ~ (all_91_0_84 = 0) & root(all_43_2_52, tptp0) = all_91_0_84) % 59.12/20.23 | % 59.12/20.23 | Instantiating (183) with all_94_0_88 yields: % 59.12/20.23 | (205) occurrence_of(all_94_0_88, tptp0) = 0 & subactivity_occurrence(all_44_2_55, all_94_0_88) = 0 & subactivity_occurrence(all_44_3_56, all_94_0_88) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (205) yields: % 59.12/20.23 | (206) occurrence_of(all_94_0_88, tptp0) = 0 % 59.12/20.23 | (207) subactivity_occurrence(all_44_2_55, all_94_0_88) = 0 % 59.12/20.23 | (208) subactivity_occurrence(all_44_3_56, all_94_0_88) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating (189) with all_105_0_101, all_105_1_102, all_105_2_103 yields: % 59.12/20.23 | (209) (all_105_0_101 = 0 & all_105_1_102 = 0 & occurrence_of(all_0_0_0, all_105_2_103) = 0 & root(all_43_2_52, all_105_2_103) = 0) | ( ~ (all_105_2_103 = 0) & root_occ(all_43_2_52, all_0_0_0) = all_105_2_103) % 59.12/20.23 | % 59.12/20.23 | Instantiating (182) with all_108_0_107 yields: % 59.12/20.23 | (210) activity(all_108_0_107) = 0 & occurrence_of(all_0_0_0, all_108_0_107) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (210) yields: % 59.12/20.23 | (211) activity(all_108_0_107) = 0 % 59.12/20.23 | (212) occurrence_of(all_0_0_0, all_108_0_107) = 0 % 59.12/20.23 | % 59.12/20.23 +-Applying beta-rule and splitting (209), into two cases. % 59.12/20.23 |-Branch one: % 59.12/20.23 | (213) all_105_0_101 = 0 & all_105_1_102 = 0 & occurrence_of(all_0_0_0, all_105_2_103) = 0 & root(all_43_2_52, all_105_2_103) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (213) yields: % 59.12/20.23 | (214) all_105_0_101 = 0 % 59.12/20.23 | (215) all_105_1_102 = 0 % 59.12/20.23 | (216) occurrence_of(all_0_0_0, all_105_2_103) = 0 % 59.12/20.23 | (217) root(all_43_2_52, all_105_2_103) = 0 % 59.12/20.23 | % 59.12/20.23 +-Applying beta-rule and splitting (204), into two cases. % 59.12/20.23 |-Branch one: % 59.12/20.23 | (218) all_91_0_84 = 0 & root_occ(all_43_2_52, all_0_0_0) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (218) yields: % 59.12/20.23 | (219) all_91_0_84 = 0 % 59.12/20.23 | (220) root_occ(all_43_2_52, all_0_0_0) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (32) with all_105_2_103, tptp0, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_105_2_103) = 0, occurrence_of(all_0_0_0, tptp0) = 0, yields: % 59.12/20.23 | (221) all_105_2_103 = tptp0 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (32) with all_105_2_103, all_108_0_107, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_108_0_107) = 0, occurrence_of(all_0_0_0, all_105_2_103) = 0, yields: % 59.12/20.23 | (222) all_108_0_107 = all_105_2_103 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (21) with all_72_0_65, all_0_0_0, all_44_4_57, all_43_2_52 and discharging atoms root_occ(all_44_4_57, all_0_0_0) = 0, root_occ(all_43_2_52, all_0_0_0) = 0, occurrence_of(all_0_0_0, all_72_0_65) = 0, yields: % 59.12/20.23 | (223) all_44_4_57 = all_43_2_52 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (32) with all_72_0_65, all_108_0_107, all_0_0_0 and discharging atoms occurrence_of(all_0_0_0, all_108_0_107) = 0, occurrence_of(all_0_0_0, all_72_0_65) = 0, yields: % 59.12/20.23 | (224) all_108_0_107 = all_72_0_65 % 59.12/20.23 | % 59.12/20.23 | Combining equations (222,224) yields a new equation: % 59.12/20.23 | (225) all_105_2_103 = all_72_0_65 % 59.12/20.23 | % 59.12/20.23 | Simplifying 225 yields: % 59.12/20.23 | (226) all_105_2_103 = all_72_0_65 % 59.12/20.23 | % 59.12/20.23 | Combining equations (221,226) yields a new equation: % 59.12/20.23 | (227) all_72_0_65 = tptp0 % 59.12/20.23 | % 59.12/20.23 | Combining equations (227,226) yields a new equation: % 59.12/20.23 | (221) all_105_2_103 = tptp0 % 59.12/20.23 | % 59.12/20.23 | From (223) and (151) follows: % 59.12/20.23 | (229) min_precedes(all_43_2_52, all_44_3_56, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | From (223) and (154) follows: % 59.12/20.23 | (220) root_occ(all_43_2_52, all_0_0_0) = 0 % 59.12/20.23 | % 59.12/20.23 | From (221) and (217) follows: % 59.12/20.23 | (162) root(all_43_2_52, tptp0) = 0 % 59.12/20.23 | % 59.12/20.23 | From (223) and (200) follows: % 59.12/20.23 | (232) subactivity_occurrence(all_43_2_52, all_76_0_67) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (130) with all_44_2_55, all_80_0_70 and discharging atoms min_precedes(all_80_0_70, all_44_2_55, tptp0) = 0, yields: % 59.12/20.23 | (233) ? [v0] : ? [v1] : (( ~ (v1 = 0) & ~ (v0 = 0) & occurrence_of(all_44_2_55, tptp1) = v1 & occurrence_of(all_44_2_55, tptp2) = v0) | ( ~ (v0 = 0) & root_occ(all_80_0_70, all_0_0_0) = v0) | ( ~ (v0 = 0) & occurrence_of(all_80_0_70, tptp3) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (94) with all_94_0_88, tptp0, all_44_3_56, all_74_0_66 and discharging atoms min_precedes(all_74_0_66, all_44_3_56, tptp0) = 0, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.23 | (234) ? [v0] : ((v0 = 0 & subactivity_occurrence(all_74_0_66, all_94_0_88) = 0) | ( ~ (v0 = 0) & subactivity_occurrence(all_44_3_56, all_94_0_88) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (124) with all_94_0_88 and discharging atoms occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.23 | (235) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (min_precedes(v1, v2, tptp0) = 0 & min_precedes(v0, v1, tptp0) = 0 & root_occ(v0, all_94_0_88) = 0 & occurrence_of(v1, tptp4) = 0 & occurrence_of(v0, tptp3) = 0 & ! [v5] : (v5 = v2 | v5 = v1 | ~ (min_precedes(v0, v5, tptp0) = 0)) & ((v4 = 0 & occurrence_of(v2, tptp1) = 0) | (v3 = 0 & occurrence_of(v2, tptp2) = 0))) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (90) with all_94_0_88, tptp0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.23 | (236) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & root(v0, tptp0) = 0 & subactivity_occurrence(v0, all_94_0_88) = 0) | (v0 = 0 & atomic(tptp0) = 0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (76) with all_94_0_88, tptp0, all_44_2_55, all_80_0_70 and discharging atoms min_precedes(all_80_0_70, all_44_2_55, tptp0) = 0, subactivity_occurrence(all_44_2_55, all_94_0_88) = 0, yields: % 59.12/20.23 | (237) ? [v0] : ((v0 = 0 & subactivity_occurrence(all_80_0_70, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (46) with all_94_0_88, all_44_2_55 and discharging atoms subactivity_occurrence(all_44_2_55, all_94_0_88) = 0, yields: % 59.12/20.23 | (238) activity_occurrence(all_94_0_88) = 0 & activity_occurrence(all_44_2_55) = 0 % 59.12/20.23 | % 59.12/20.23 | Applying alpha-rule on (238) yields: % 59.12/20.23 | (239) activity_occurrence(all_94_0_88) = 0 % 59.12/20.23 | (240) activity_occurrence(all_44_2_55) = 0 % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (76) with all_94_0_88, tptp0, all_44_3_56, all_43_2_52 and discharging atoms min_precedes(all_43_2_52, all_44_3_56, tptp0) = 0, subactivity_occurrence(all_44_3_56, all_94_0_88) = 0, yields: % 59.12/20.23 | (241) ? [v0] : ((v0 = 0 & subactivity_occurrence(all_43_2_52, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.23 | % 59.12/20.23 | Instantiating formula (59) with tptp0, all_76_0_67, all_43_2_52 and discharging atoms root(all_43_2_52, tptp0) = 0, subactivity_occurrence(all_43_2_52, all_76_0_67) = 0, yields: % 59.12/20.24 | (242) ? [v0] : ((v0 = 0 & root_occ(all_43_2_52, all_76_0_67) = 0) | ( ~ (v0 = 0) & occurrence_of(all_76_0_67, tptp0) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (96) with 0, all_76_0_67, all_43_2_52 and discharging atoms subactivity_occurrence(all_43_2_52, all_76_0_67) = 0, yields: % 59.12/20.24 | (243) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & occurrence_of(all_76_0_67, v0) = 0 & root(all_43_2_52, v0) = 0) | ( ~ (v0 = 0) & root_occ(all_43_2_52, all_76_0_67) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating (235) with all_157_0_109, all_157_1_110, all_157_2_111, all_157_3_112, all_157_4_113 yields: % 59.12/20.24 | (244) min_precedes(all_157_3_112, all_157_2_111, tptp0) = 0 & min_precedes(all_157_4_113, all_157_3_112, tptp0) = 0 & root_occ(all_157_4_113, all_94_0_88) = 0 & occurrence_of(all_157_3_112, tptp4) = 0 & occurrence_of(all_157_4_113, tptp3) = 0 & ! [v0] : (v0 = all_157_2_111 | v0 = all_157_3_112 | ~ (min_precedes(all_157_4_113, v0, tptp0) = 0)) & ((all_157_0_109 = 0 & occurrence_of(all_157_2_111, tptp1) = 0) | (all_157_1_110 = 0 & occurrence_of(all_157_2_111, tptp2) = 0)) % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (244) yields: % 59.12/20.24 | (245) root_occ(all_157_4_113, all_94_0_88) = 0 % 59.12/20.24 | (246) occurrence_of(all_157_3_112, tptp4) = 0 % 59.12/20.24 | (247) (all_157_0_109 = 0 & occurrence_of(all_157_2_111, tptp1) = 0) | (all_157_1_110 = 0 & occurrence_of(all_157_2_111, tptp2) = 0) % 59.12/20.24 | (248) min_precedes(all_157_4_113, all_157_3_112, tptp0) = 0 % 59.12/20.24 | (249) ! [v0] : (v0 = all_157_2_111 | v0 = all_157_3_112 | ~ (min_precedes(all_157_4_113, v0, tptp0) = 0)) % 59.12/20.24 | (250) min_precedes(all_157_3_112, all_157_2_111, tptp0) = 0 % 59.12/20.24 | (251) occurrence_of(all_157_4_113, tptp3) = 0 % 59.12/20.24 | % 59.12/20.24 | Instantiating (242) with all_161_0_117 yields: % 59.12/20.24 | (252) (all_161_0_117 = 0 & root_occ(all_43_2_52, all_76_0_67) = 0) | ( ~ (all_161_0_117 = 0) & occurrence_of(all_76_0_67, tptp0) = all_161_0_117) % 59.12/20.24 | % 59.12/20.24 | Instantiating (237) with all_169_0_130 yields: % 59.12/20.24 | (253) (all_169_0_130 = 0 & subactivity_occurrence(all_80_0_70, all_94_0_88) = 0) | ( ~ (all_169_0_130 = 0) & occurrence_of(all_94_0_88, tptp0) = all_169_0_130) % 59.12/20.24 | % 59.12/20.24 | Instantiating (234) with all_174_0_134 yields: % 59.12/20.24 | (254) (all_174_0_134 = 0 & subactivity_occurrence(all_74_0_66, all_94_0_88) = 0) | ( ~ (all_174_0_134 = 0) & subactivity_occurrence(all_44_3_56, all_94_0_88) = all_174_0_134) % 59.12/20.24 | % 59.12/20.24 | Instantiating (233) with all_188_0_148, all_188_1_149 yields: % 59.12/20.24 | (255) ( ~ (all_188_0_148 = 0) & ~ (all_188_1_149 = 0) & occurrence_of(all_44_2_55, tptp1) = all_188_0_148 & occurrence_of(all_44_2_55, tptp2) = all_188_1_149) | ( ~ (all_188_1_149 = 0) & root_occ(all_80_0_70, all_0_0_0) = all_188_1_149) | ( ~ (all_188_1_149 = 0) & occurrence_of(all_80_0_70, tptp3) = all_188_1_149) % 59.12/20.24 | % 59.12/20.24 | Instantiating (243) with all_210_0_169, all_210_1_170, all_210_2_171 yields: % 59.12/20.24 | (256) (all_210_0_169 = 0 & all_210_1_170 = 0 & occurrence_of(all_76_0_67, all_210_2_171) = 0 & root(all_43_2_52, all_210_2_171) = 0) | ( ~ (all_210_2_171 = 0) & root_occ(all_43_2_52, all_76_0_67) = all_210_2_171) % 59.12/20.24 | % 59.12/20.24 | Instantiating (241) with all_216_0_177 yields: % 59.12/20.24 | (257) (all_216_0_177 = 0 & subactivity_occurrence(all_43_2_52, all_94_0_88) = 0) | ( ~ (all_216_0_177 = 0) & occurrence_of(all_94_0_88, tptp0) = all_216_0_177) % 59.12/20.24 | % 59.12/20.24 | Instantiating (236) with all_243_0_215, all_243_1_216, all_243_2_217 yields: % 59.12/20.24 | (258) (all_243_0_215 = 0 & all_243_1_216 = 0 & root(all_243_2_217, tptp0) = 0 & subactivity_occurrence(all_243_2_217, all_94_0_88) = 0) | (all_243_2_217 = 0 & atomic(tptp0) = 0) % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (258), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (259) all_243_0_215 = 0 & all_243_1_216 = 0 & root(all_243_2_217, tptp0) = 0 & subactivity_occurrence(all_243_2_217, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (259) yields: % 59.12/20.24 | (260) all_243_0_215 = 0 % 59.12/20.24 | (261) all_243_1_216 = 0 % 59.12/20.24 | (262) root(all_243_2_217, tptp0) = 0 % 59.12/20.24 | (263) subactivity_occurrence(all_243_2_217, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (252), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (264) all_161_0_117 = 0 & root_occ(all_43_2_52, all_76_0_67) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (264) yields: % 59.12/20.24 | (265) all_161_0_117 = 0 % 59.12/20.24 | (266) root_occ(all_43_2_52, all_76_0_67) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (253), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (267) all_169_0_130 = 0 & subactivity_occurrence(all_80_0_70, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (267) yields: % 59.12/20.24 | (268) all_169_0_130 = 0 % 59.12/20.24 | (269) subactivity_occurrence(all_80_0_70, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (257), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (270) all_216_0_177 = 0 & subactivity_occurrence(all_43_2_52, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (270) yields: % 59.12/20.24 | (271) all_216_0_177 = 0 % 59.12/20.24 | (272) subactivity_occurrence(all_43_2_52, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (256), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (273) all_210_0_169 = 0 & all_210_1_170 = 0 & occurrence_of(all_76_0_67, all_210_2_171) = 0 & root(all_43_2_52, all_210_2_171) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (273) yields: % 59.12/20.24 | (274) all_210_0_169 = 0 % 59.12/20.24 | (275) all_210_1_170 = 0 % 59.12/20.24 | (276) occurrence_of(all_76_0_67, all_210_2_171) = 0 % 59.12/20.24 | (277) root(all_43_2_52, all_210_2_171) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (254), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (278) all_174_0_134 = 0 & subactivity_occurrence(all_74_0_66, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (278) yields: % 59.12/20.24 | (279) all_174_0_134 = 0 % 59.12/20.24 | (280) subactivity_occurrence(all_74_0_66, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (32) with all_210_2_171, tptp0, all_76_0_67 and discharging atoms occurrence_of(all_76_0_67, all_210_2_171) = 0, occurrence_of(all_76_0_67, tptp0) = 0, yields: % 59.12/20.24 | (281) all_210_2_171 = tptp0 % 59.12/20.24 | % 59.12/20.24 | From (281) and (277) follows: % 59.12/20.24 | (162) root(all_43_2_52, tptp0) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (149), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (283) all_44_0_53 = 0 & occurrence_of(all_44_2_55, tptp1) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (283) yields: % 59.12/20.24 | (284) all_44_0_53 = 0 % 59.12/20.24 | (285) occurrence_of(all_44_2_55, tptp1) = 0 % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (15) with all_44_2_55 and discharging atoms activity_occurrence(all_44_2_55) = 0, yields: % 59.12/20.24 | (286) ? [v0] : (activity(v0) = 0 & occurrence_of(all_44_2_55, v0) = 0) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (59) with tptp0, all_94_0_88, all_243_2_217 and discharging atoms root(all_243_2_217, tptp0) = 0, subactivity_occurrence(all_243_2_217, all_94_0_88) = 0, yields: % 59.12/20.24 | (287) ? [v0] : ((v0 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (59) with tptp0, all_94_0_88, all_80_0_70 and discharging atoms root(all_80_0_70, tptp0) = 0, subactivity_occurrence(all_80_0_70, all_94_0_88) = 0, yields: % 59.12/20.24 | (288) ? [v0] : ((v0 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (59) with tptp0, all_94_0_88, all_74_0_66 and discharging atoms root(all_74_0_66, tptp0) = 0, subactivity_occurrence(all_74_0_66, all_94_0_88) = 0, yields: % 59.12/20.24 | (289) ? [v0] : ((v0 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (59) with tptp0, all_94_0_88, all_43_2_52 and discharging atoms root(all_43_2_52, tptp0) = 0, subactivity_occurrence(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.24 | (290) ? [v0] : ((v0 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating formula (96) with 0, all_94_0_88, all_43_2_52 and discharging atoms subactivity_occurrence(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.24 | (291) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & occurrence_of(all_94_0_88, v0) = 0 & root(all_43_2_52, v0) = 0) | ( ~ (v0 = 0) & root_occ(all_43_2_52, all_94_0_88) = v0)) % 59.12/20.24 | % 59.12/20.24 | Instantiating (291) with all_368_0_251, all_368_1_252, all_368_2_253 yields: % 59.12/20.24 | (292) (all_368_0_251 = 0 & all_368_1_252 = 0 & occurrence_of(all_94_0_88, all_368_2_253) = 0 & root(all_43_2_52, all_368_2_253) = 0) | ( ~ (all_368_2_253 = 0) & root_occ(all_43_2_52, all_94_0_88) = all_368_2_253) % 59.12/20.24 | % 59.12/20.24 | Instantiating (290) with all_373_0_262 yields: % 59.12/20.24 | (293) (all_373_0_262 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0) | ( ~ (all_373_0_262 = 0) & occurrence_of(all_94_0_88, tptp0) = all_373_0_262) % 59.12/20.24 | % 59.12/20.24 | Instantiating (289) with all_440_0_345 yields: % 59.12/20.24 | (294) (all_440_0_345 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0) | ( ~ (all_440_0_345 = 0) & occurrence_of(all_94_0_88, tptp0) = all_440_0_345) % 59.12/20.24 | % 59.12/20.24 | Instantiating (288) with all_452_0_361 yields: % 59.12/20.24 | (295) (all_452_0_361 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0) | ( ~ (all_452_0_361 = 0) & occurrence_of(all_94_0_88, tptp0) = all_452_0_361) % 59.12/20.24 | % 59.12/20.24 | Instantiating (287) with all_558_0_489 yields: % 59.12/20.24 | (296) (all_558_0_489 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0) | ( ~ (all_558_0_489 = 0) & occurrence_of(all_94_0_88, tptp0) = all_558_0_489) % 59.12/20.24 | % 59.12/20.24 | Instantiating (286) with all_583_0_512 yields: % 59.12/20.24 | (297) activity(all_583_0_512) = 0 & occurrence_of(all_44_2_55, all_583_0_512) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (297) yields: % 59.12/20.24 | (298) activity(all_583_0_512) = 0 % 59.12/20.24 | (299) occurrence_of(all_44_2_55, all_583_0_512) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (296), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (300) all_558_0_489 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (300) yields: % 59.12/20.24 | (301) all_558_0_489 = 0 % 59.12/20.24 | (302) root_occ(all_243_2_217, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (295), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (303) all_452_0_361 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (303) yields: % 59.12/20.24 | (304) all_452_0_361 = 0 % 59.12/20.24 | (305) root_occ(all_80_0_70, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (294), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (306) all_440_0_345 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 | Applying alpha-rule on (306) yields: % 59.12/20.24 | (307) all_440_0_345 = 0 % 59.12/20.24 | (308) root_occ(all_74_0_66, all_94_0_88) = 0 % 59.12/20.24 | % 59.12/20.24 +-Applying beta-rule and splitting (293), into two cases. % 59.12/20.24 |-Branch one: % 59.12/20.24 | (309) all_373_0_262 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (309) yields: % 59.12/20.25 | (310) all_373_0_262 = 0 % 59.12/20.25 | (311) root_occ(all_43_2_52, all_94_0_88) = 0 % 59.12/20.25 | % 59.12/20.25 +-Applying beta-rule and splitting (292), into two cases. % 59.12/20.25 |-Branch one: % 59.12/20.25 | (312) all_368_0_251 = 0 & all_368_1_252 = 0 & occurrence_of(all_94_0_88, all_368_2_253) = 0 & root(all_43_2_52, all_368_2_253) = 0 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (312) yields: % 59.12/20.25 | (313) all_368_0_251 = 0 % 59.12/20.25 | (314) all_368_1_252 = 0 % 59.12/20.25 | (315) occurrence_of(all_94_0_88, all_368_2_253) = 0 % 59.12/20.25 | (316) root(all_43_2_52, all_368_2_253) = 0 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (21) with all_368_2_253, all_94_0_88, all_157_4_113, all_80_0_70 and discharging atoms root_occ(all_157_4_113, all_94_0_88) = 0, root_occ(all_80_0_70, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_253) = 0, yields: % 59.12/20.25 | (317) all_157_4_113 = all_80_0_70 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (21) with all_368_2_253, all_94_0_88, all_157_4_113, all_74_0_66 and discharging atoms root_occ(all_157_4_113, all_94_0_88) = 0, root_occ(all_74_0_66, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_253) = 0, yields: % 59.12/20.25 | (318) all_157_4_113 = all_74_0_66 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (21) with all_368_2_253, all_94_0_88, all_243_2_217, all_80_0_70 and discharging atoms root_occ(all_243_2_217, all_94_0_88) = 0, root_occ(all_80_0_70, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_253) = 0, yields: % 59.12/20.25 | (319) all_243_2_217 = all_80_0_70 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (21) with all_368_2_253, all_94_0_88, all_243_2_217, all_43_2_52 and discharging atoms root_occ(all_243_2_217, all_94_0_88) = 0, root_occ(all_43_2_52, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_253) = 0, yields: % 59.12/20.25 | (320) all_243_2_217 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (32) with all_583_0_512, tptp1, all_44_2_55 and discharging atoms occurrence_of(all_44_2_55, all_583_0_512) = 0, occurrence_of(all_44_2_55, tptp1) = 0, yields: % 59.12/20.25 | (321) all_583_0_512 = tptp1 % 59.12/20.25 | % 59.12/20.25 | Combining equations (319,320) yields a new equation: % 59.12/20.25 | (322) all_80_0_70 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | Simplifying 322 yields: % 59.12/20.25 | (323) all_80_0_70 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | Combining equations (317,318) yields a new equation: % 59.12/20.25 | (324) all_80_0_70 = all_74_0_66 % 59.12/20.25 | % 59.12/20.25 | Simplifying 324 yields: % 59.12/20.25 | (325) all_80_0_70 = all_74_0_66 % 59.12/20.25 | % 59.12/20.25 | Combining equations (323,325) yields a new equation: % 59.12/20.25 | (326) all_74_0_66 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | Combining equations (326,325) yields a new equation: % 59.12/20.25 | (323) all_80_0_70 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | Combining equations (326,318) yields a new equation: % 59.12/20.25 | (328) all_157_4_113 = all_43_2_52 % 59.12/20.25 | % 59.12/20.25 | From (328) and (251) follows: % 59.12/20.25 | (329) occurrence_of(all_43_2_52, tptp3) = 0 % 59.12/20.25 | % 59.12/20.25 | From (321) and (299) follows: % 59.12/20.25 | (285) occurrence_of(all_44_2_55, tptp1) = 0 % 59.12/20.25 | % 59.12/20.25 +-Applying beta-rule and splitting (255), into two cases. % 59.12/20.25 |-Branch one: % 59.12/20.25 | (331) ( ~ (all_188_0_148 = 0) & ~ (all_188_1_149 = 0) & occurrence_of(all_44_2_55, tptp1) = all_188_0_148 & occurrence_of(all_44_2_55, tptp2) = all_188_1_149) | ( ~ (all_188_1_149 = 0) & root_occ(all_80_0_70, all_0_0_0) = all_188_1_149) % 59.12/20.25 | % 59.12/20.25 +-Applying beta-rule and splitting (331), into two cases. % 59.12/20.25 |-Branch one: % 59.12/20.25 | (332) ~ (all_188_0_148 = 0) & ~ (all_188_1_149 = 0) & occurrence_of(all_44_2_55, tptp1) = all_188_0_148 & occurrence_of(all_44_2_55, tptp2) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (332) yields: % 59.12/20.25 | (333) ~ (all_188_0_148 = 0) % 59.12/20.25 | (334) ~ (all_188_1_149 = 0) % 59.12/20.25 | (335) occurrence_of(all_44_2_55, tptp1) = all_188_0_148 % 59.12/20.25 | (336) occurrence_of(all_44_2_55, tptp2) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_44_2_55, tptp1, all_188_0_148, 0 and discharging atoms occurrence_of(all_44_2_55, tptp1) = all_188_0_148, occurrence_of(all_44_2_55, tptp1) = 0, yields: % 59.12/20.25 | (337) all_188_0_148 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (337) can reduce 333 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (339) ~ (all_188_1_149 = 0) & root_occ(all_80_0_70, all_0_0_0) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (339) yields: % 59.12/20.25 | (334) ~ (all_188_1_149 = 0) % 59.12/20.25 | (341) root_occ(all_80_0_70, all_0_0_0) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | From (323) and (341) follows: % 59.12/20.25 | (342) root_occ(all_43_2_52, all_0_0_0) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (64) with all_43_2_52, all_0_0_0, all_188_1_149, 0 and discharging atoms root_occ(all_43_2_52, all_0_0_0) = all_188_1_149, root_occ(all_43_2_52, all_0_0_0) = 0, yields: % 59.12/20.25 | (343) all_188_1_149 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (343) can reduce 334 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (345) ~ (all_188_1_149 = 0) & occurrence_of(all_80_0_70, tptp3) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (345) yields: % 59.12/20.25 | (334) ~ (all_188_1_149 = 0) % 59.12/20.25 | (347) occurrence_of(all_80_0_70, tptp3) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | From (323) and (347) follows: % 59.12/20.25 | (348) occurrence_of(all_43_2_52, tptp3) = all_188_1_149 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_43_2_52, tptp3, all_188_1_149, 0 and discharging atoms occurrence_of(all_43_2_52, tptp3) = all_188_1_149, occurrence_of(all_43_2_52, tptp3) = 0, yields: % 59.12/20.25 | (343) all_188_1_149 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (343) can reduce 334 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (351) ~ (all_368_2_253 = 0) & root_occ(all_43_2_52, all_94_0_88) = all_368_2_253 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (351) yields: % 59.12/20.25 | (352) ~ (all_368_2_253 = 0) % 59.12/20.25 | (353) root_occ(all_43_2_52, all_94_0_88) = all_368_2_253 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (64) with all_43_2_52, all_94_0_88, 0, all_368_2_253 and discharging atoms root_occ(all_43_2_52, all_94_0_88) = all_368_2_253, root_occ(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.25 | (354) all_368_2_253 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (354) can reduce 352 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (356) ~ (all_373_0_262 = 0) & occurrence_of(all_94_0_88, tptp0) = all_373_0_262 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (356) yields: % 59.12/20.25 | (357) ~ (all_373_0_262 = 0) % 59.12/20.25 | (358) occurrence_of(all_94_0_88, tptp0) = all_373_0_262 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_94_0_88, tptp0, all_373_0_262, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_373_0_262, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.25 | (310) all_373_0_262 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (310) can reduce 357 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (361) ~ (all_440_0_345 = 0) & occurrence_of(all_94_0_88, tptp0) = all_440_0_345 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (361) yields: % 59.12/20.25 | (362) ~ (all_440_0_345 = 0) % 59.12/20.25 | (363) occurrence_of(all_94_0_88, tptp0) = all_440_0_345 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_94_0_88, tptp0, all_440_0_345, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_440_0_345, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.25 | (307) all_440_0_345 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (307) can reduce 362 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (366) ~ (all_452_0_361 = 0) & occurrence_of(all_94_0_88, tptp0) = all_452_0_361 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (366) yields: % 59.12/20.25 | (367) ~ (all_452_0_361 = 0) % 59.12/20.25 | (368) occurrence_of(all_94_0_88, tptp0) = all_452_0_361 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_94_0_88, tptp0, all_452_0_361, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_452_0_361, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.25 | (304) all_452_0_361 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (304) can reduce 367 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (371) ~ (all_558_0_489 = 0) & occurrence_of(all_94_0_88, tptp0) = all_558_0_489 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (371) yields: % 59.12/20.25 | (372) ~ (all_558_0_489 = 0) % 59.12/20.25 | (373) occurrence_of(all_94_0_88, tptp0) = all_558_0_489 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (68) with all_94_0_88, tptp0, all_558_0_489, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_558_0_489, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.25 | (301) all_558_0_489 = 0 % 59.12/20.25 | % 59.12/20.25 | Equations (301) can reduce 372 to: % 59.12/20.25 | (168) $false % 59.12/20.25 | % 59.12/20.25 |-The branch is then unsatisfiable % 59.12/20.25 |-Branch two: % 59.12/20.25 | (376) all_44_1_54 = 0 & occurrence_of(all_44_2_55, tptp2) = 0 % 59.12/20.25 | % 59.12/20.25 | Applying alpha-rule on (376) yields: % 59.12/20.25 | (377) all_44_1_54 = 0 % 59.12/20.25 | (378) occurrence_of(all_44_2_55, tptp2) = 0 % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (15) with all_44_2_55 and discharging atoms activity_occurrence(all_44_2_55) = 0, yields: % 59.12/20.25 | (286) ? [v0] : (activity(v0) = 0 & occurrence_of(all_44_2_55, v0) = 0) % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (59) with tptp0, all_94_0_88, all_243_2_217 and discharging atoms root(all_243_2_217, tptp0) = 0, subactivity_occurrence(all_243_2_217, all_94_0_88) = 0, yields: % 59.12/20.25 | (287) ? [v0] : ((v0 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.25 | % 59.12/20.25 | Instantiating formula (59) with tptp0, all_94_0_88, all_80_0_70 and discharging atoms root(all_80_0_70, tptp0) = 0, subactivity_occurrence(all_80_0_70, all_94_0_88) = 0, yields: % 59.12/20.26 | (288) ? [v0] : ((v0 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (59) with tptp0, all_94_0_88, all_74_0_66 and discharging atoms root(all_74_0_66, tptp0) = 0, subactivity_occurrence(all_74_0_66, all_94_0_88) = 0, yields: % 59.12/20.26 | (289) ? [v0] : ((v0 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (59) with tptp0, all_94_0_88, all_43_2_52 and discharging atoms root(all_43_2_52, tptp0) = 0, subactivity_occurrence(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.26 | (290) ? [v0] : ((v0 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0) | ( ~ (v0 = 0) & occurrence_of(all_94_0_88, tptp0) = v0)) % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (96) with 0, all_94_0_88, all_43_2_52 and discharging atoms subactivity_occurrence(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.26 | (291) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & occurrence_of(all_94_0_88, v0) = 0 & root(all_43_2_52, v0) = 0) | ( ~ (v0 = 0) & root_occ(all_43_2_52, all_94_0_88) = v0)) % 59.12/20.26 | % 59.12/20.26 | Instantiating (291) with all_368_0_631, all_368_1_632, all_368_2_633 yields: % 59.12/20.26 | (385) (all_368_0_631 = 0 & all_368_1_632 = 0 & occurrence_of(all_94_0_88, all_368_2_633) = 0 & root(all_43_2_52, all_368_2_633) = 0) | ( ~ (all_368_2_633 = 0) & root_occ(all_43_2_52, all_94_0_88) = all_368_2_633) % 59.12/20.26 | % 59.12/20.26 | Instantiating (290) with all_373_0_642 yields: % 59.12/20.26 | (386) (all_373_0_642 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0) | ( ~ (all_373_0_642 = 0) & occurrence_of(all_94_0_88, tptp0) = all_373_0_642) % 59.12/20.26 | % 59.12/20.26 | Instantiating (289) with all_440_0_725 yields: % 59.12/20.26 | (387) (all_440_0_725 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0) | ( ~ (all_440_0_725 = 0) & occurrence_of(all_94_0_88, tptp0) = all_440_0_725) % 59.12/20.26 | % 59.12/20.26 | Instantiating (288) with all_452_0_741 yields: % 59.12/20.26 | (388) (all_452_0_741 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0) | ( ~ (all_452_0_741 = 0) & occurrence_of(all_94_0_88, tptp0) = all_452_0_741) % 59.12/20.26 | % 59.12/20.26 | Instantiating (287) with all_558_0_869 yields: % 59.12/20.26 | (389) (all_558_0_869 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0) | ( ~ (all_558_0_869 = 0) & occurrence_of(all_94_0_88, tptp0) = all_558_0_869) % 59.12/20.26 | % 59.12/20.26 | Instantiating (286) with all_583_0_892 yields: % 59.12/20.26 | (390) activity(all_583_0_892) = 0 & occurrence_of(all_44_2_55, all_583_0_892) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (390) yields: % 59.12/20.26 | (391) activity(all_583_0_892) = 0 % 59.12/20.26 | (392) occurrence_of(all_44_2_55, all_583_0_892) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (389), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (393) all_558_0_869 = 0 & root_occ(all_243_2_217, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (393) yields: % 59.12/20.26 | (394) all_558_0_869 = 0 % 59.12/20.26 | (302) root_occ(all_243_2_217, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (388), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (396) all_452_0_741 = 0 & root_occ(all_80_0_70, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (396) yields: % 59.12/20.26 | (397) all_452_0_741 = 0 % 59.12/20.26 | (305) root_occ(all_80_0_70, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (387), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (399) all_440_0_725 = 0 & root_occ(all_74_0_66, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (399) yields: % 59.12/20.26 | (400) all_440_0_725 = 0 % 59.12/20.26 | (308) root_occ(all_74_0_66, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (386), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (402) all_373_0_642 = 0 & root_occ(all_43_2_52, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (402) yields: % 59.12/20.26 | (403) all_373_0_642 = 0 % 59.12/20.26 | (311) root_occ(all_43_2_52, all_94_0_88) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (385), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (405) all_368_0_631 = 0 & all_368_1_632 = 0 & occurrence_of(all_94_0_88, all_368_2_633) = 0 & root(all_43_2_52, all_368_2_633) = 0 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (405) yields: % 59.12/20.26 | (406) all_368_0_631 = 0 % 59.12/20.26 | (407) all_368_1_632 = 0 % 59.12/20.26 | (408) occurrence_of(all_94_0_88, all_368_2_633) = 0 % 59.12/20.26 | (409) root(all_43_2_52, all_368_2_633) = 0 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (21) with all_368_2_633, all_94_0_88, all_157_4_113, all_80_0_70 and discharging atoms root_occ(all_157_4_113, all_94_0_88) = 0, root_occ(all_80_0_70, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_633) = 0, yields: % 59.12/20.26 | (317) all_157_4_113 = all_80_0_70 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (21) with all_368_2_633, all_94_0_88, all_157_4_113, all_74_0_66 and discharging atoms root_occ(all_157_4_113, all_94_0_88) = 0, root_occ(all_74_0_66, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_633) = 0, yields: % 59.12/20.26 | (318) all_157_4_113 = all_74_0_66 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (21) with all_368_2_633, all_94_0_88, all_243_2_217, all_80_0_70 and discharging atoms root_occ(all_243_2_217, all_94_0_88) = 0, root_occ(all_80_0_70, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_633) = 0, yields: % 59.12/20.26 | (319) all_243_2_217 = all_80_0_70 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (21) with all_368_2_633, all_94_0_88, all_243_2_217, all_43_2_52 and discharging atoms root_occ(all_243_2_217, all_94_0_88) = 0, root_occ(all_43_2_52, all_94_0_88) = 0, occurrence_of(all_94_0_88, all_368_2_633) = 0, yields: % 59.12/20.26 | (320) all_243_2_217 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (32) with all_583_0_892, tptp2, all_44_2_55 and discharging atoms occurrence_of(all_44_2_55, all_583_0_892) = 0, occurrence_of(all_44_2_55, tptp2) = 0, yields: % 59.12/20.26 | (414) all_583_0_892 = tptp2 % 59.12/20.26 | % 59.12/20.26 | Combining equations (319,320) yields a new equation: % 59.12/20.26 | (322) all_80_0_70 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | Simplifying 322 yields: % 59.12/20.26 | (323) all_80_0_70 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | Combining equations (317,318) yields a new equation: % 59.12/20.26 | (324) all_80_0_70 = all_74_0_66 % 59.12/20.26 | % 59.12/20.26 | Simplifying 324 yields: % 59.12/20.26 | (325) all_80_0_70 = all_74_0_66 % 59.12/20.26 | % 59.12/20.26 | Combining equations (323,325) yields a new equation: % 59.12/20.26 | (326) all_74_0_66 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | Combining equations (326,325) yields a new equation: % 59.12/20.26 | (323) all_80_0_70 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | Combining equations (326,318) yields a new equation: % 59.12/20.26 | (328) all_157_4_113 = all_43_2_52 % 59.12/20.26 | % 59.12/20.26 | From (328) and (251) follows: % 59.12/20.26 | (329) occurrence_of(all_43_2_52, tptp3) = 0 % 59.12/20.26 | % 59.12/20.26 | From (414) and (392) follows: % 59.12/20.26 | (378) occurrence_of(all_44_2_55, tptp2) = 0 % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (255), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (331) ( ~ (all_188_0_148 = 0) & ~ (all_188_1_149 = 0) & occurrence_of(all_44_2_55, tptp1) = all_188_0_148 & occurrence_of(all_44_2_55, tptp2) = all_188_1_149) | ( ~ (all_188_1_149 = 0) & root_occ(all_80_0_70, all_0_0_0) = all_188_1_149) % 59.12/20.26 | % 59.12/20.26 +-Applying beta-rule and splitting (331), into two cases. % 59.12/20.26 |-Branch one: % 59.12/20.26 | (332) ~ (all_188_0_148 = 0) & ~ (all_188_1_149 = 0) & occurrence_of(all_44_2_55, tptp1) = all_188_0_148 & occurrence_of(all_44_2_55, tptp2) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (332) yields: % 59.12/20.26 | (333) ~ (all_188_0_148 = 0) % 59.12/20.26 | (334) ~ (all_188_1_149 = 0) % 59.12/20.26 | (335) occurrence_of(all_44_2_55, tptp1) = all_188_0_148 % 59.12/20.26 | (336) occurrence_of(all_44_2_55, tptp2) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (68) with all_44_2_55, tptp2, all_188_1_149, 0 and discharging atoms occurrence_of(all_44_2_55, tptp2) = all_188_1_149, occurrence_of(all_44_2_55, tptp2) = 0, yields: % 59.12/20.26 | (343) all_188_1_149 = 0 % 59.12/20.26 | % 59.12/20.26 | Equations (343) can reduce 334 to: % 59.12/20.26 | (168) $false % 59.12/20.26 | % 59.12/20.26 |-The branch is then unsatisfiable % 59.12/20.26 |-Branch two: % 59.12/20.26 | (339) ~ (all_188_1_149 = 0) & root_occ(all_80_0_70, all_0_0_0) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (339) yields: % 59.12/20.26 | (334) ~ (all_188_1_149 = 0) % 59.12/20.26 | (341) root_occ(all_80_0_70, all_0_0_0) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | From (323) and (341) follows: % 59.12/20.26 | (342) root_occ(all_43_2_52, all_0_0_0) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (64) with all_43_2_52, all_0_0_0, all_188_1_149, 0 and discharging atoms root_occ(all_43_2_52, all_0_0_0) = all_188_1_149, root_occ(all_43_2_52, all_0_0_0) = 0, yields: % 59.12/20.26 | (343) all_188_1_149 = 0 % 59.12/20.26 | % 59.12/20.26 | Equations (343) can reduce 334 to: % 59.12/20.26 | (168) $false % 59.12/20.26 | % 59.12/20.26 |-The branch is then unsatisfiable % 59.12/20.26 |-Branch two: % 59.12/20.26 | (345) ~ (all_188_1_149 = 0) & occurrence_of(all_80_0_70, tptp3) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (345) yields: % 59.12/20.26 | (334) ~ (all_188_1_149 = 0) % 59.12/20.26 | (347) occurrence_of(all_80_0_70, tptp3) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | From (323) and (347) follows: % 59.12/20.26 | (348) occurrence_of(all_43_2_52, tptp3) = all_188_1_149 % 59.12/20.26 | % 59.12/20.26 | Instantiating formula (68) with all_43_2_52, tptp3, all_188_1_149, 0 and discharging atoms occurrence_of(all_43_2_52, tptp3) = all_188_1_149, occurrence_of(all_43_2_52, tptp3) = 0, yields: % 59.12/20.26 | (343) all_188_1_149 = 0 % 59.12/20.26 | % 59.12/20.26 | Equations (343) can reduce 334 to: % 59.12/20.26 | (168) $false % 59.12/20.26 | % 59.12/20.26 |-The branch is then unsatisfiable % 59.12/20.26 |-Branch two: % 59.12/20.26 | (444) ~ (all_368_2_633 = 0) & root_occ(all_43_2_52, all_94_0_88) = all_368_2_633 % 59.12/20.26 | % 59.12/20.26 | Applying alpha-rule on (444) yields: % 59.12/20.26 | (445) ~ (all_368_2_633 = 0) % 59.12/20.27 | (446) root_occ(all_43_2_52, all_94_0_88) = all_368_2_633 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (64) with all_43_2_52, all_94_0_88, 0, all_368_2_633 and discharging atoms root_occ(all_43_2_52, all_94_0_88) = all_368_2_633, root_occ(all_43_2_52, all_94_0_88) = 0, yields: % 59.12/20.27 | (447) all_368_2_633 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (447) can reduce 445 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (449) ~ (all_373_0_642 = 0) & occurrence_of(all_94_0_88, tptp0) = all_373_0_642 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (449) yields: % 59.12/20.27 | (450) ~ (all_373_0_642 = 0) % 59.12/20.27 | (451) occurrence_of(all_94_0_88, tptp0) = all_373_0_642 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_373_0_642, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_373_0_642, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (403) all_373_0_642 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (403) can reduce 450 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (454) ~ (all_440_0_725 = 0) & occurrence_of(all_94_0_88, tptp0) = all_440_0_725 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (454) yields: % 59.12/20.27 | (455) ~ (all_440_0_725 = 0) % 59.12/20.27 | (456) occurrence_of(all_94_0_88, tptp0) = all_440_0_725 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_440_0_725, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_440_0_725, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (400) all_440_0_725 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (400) can reduce 455 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (459) ~ (all_452_0_741 = 0) & occurrence_of(all_94_0_88, tptp0) = all_452_0_741 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (459) yields: % 59.12/20.27 | (460) ~ (all_452_0_741 = 0) % 59.12/20.27 | (461) occurrence_of(all_94_0_88, tptp0) = all_452_0_741 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_452_0_741, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_452_0_741, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (397) all_452_0_741 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (397) can reduce 460 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (464) ~ (all_558_0_869 = 0) & occurrence_of(all_94_0_88, tptp0) = all_558_0_869 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (464) yields: % 59.12/20.27 | (465) ~ (all_558_0_869 = 0) % 59.12/20.27 | (466) occurrence_of(all_94_0_88, tptp0) = all_558_0_869 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_558_0_869, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_558_0_869, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (394) all_558_0_869 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (394) can reduce 465 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (469) ~ (all_174_0_134 = 0) & subactivity_occurrence(all_44_3_56, all_94_0_88) = all_174_0_134 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (469) yields: % 59.12/20.27 | (470) ~ (all_174_0_134 = 0) % 59.12/20.27 | (471) subactivity_occurrence(all_44_3_56, all_94_0_88) = all_174_0_134 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (129) with all_44_3_56, all_94_0_88, all_174_0_134, 0 and discharging atoms subactivity_occurrence(all_44_3_56, all_94_0_88) = all_174_0_134, subactivity_occurrence(all_44_3_56, all_94_0_88) = 0, yields: % 59.12/20.27 | (279) all_174_0_134 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (279) can reduce 470 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (474) ~ (all_210_2_171 = 0) & root_occ(all_43_2_52, all_76_0_67) = all_210_2_171 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (474) yields: % 59.12/20.27 | (475) ~ (all_210_2_171 = 0) % 59.12/20.27 | (476) root_occ(all_43_2_52, all_76_0_67) = all_210_2_171 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (64) with all_43_2_52, all_76_0_67, 0, all_210_2_171 and discharging atoms root_occ(all_43_2_52, all_76_0_67) = all_210_2_171, root_occ(all_43_2_52, all_76_0_67) = 0, yields: % 59.12/20.27 | (477) all_210_2_171 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (477) can reduce 475 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (479) ~ (all_216_0_177 = 0) & occurrence_of(all_94_0_88, tptp0) = all_216_0_177 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (479) yields: % 59.12/20.27 | (480) ~ (all_216_0_177 = 0) % 59.12/20.27 | (481) occurrence_of(all_94_0_88, tptp0) = all_216_0_177 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_216_0_177, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_216_0_177, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (271) all_216_0_177 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (271) can reduce 480 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (484) ~ (all_169_0_130 = 0) & occurrence_of(all_94_0_88, tptp0) = all_169_0_130 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (484) yields: % 59.12/20.27 | (485) ~ (all_169_0_130 = 0) % 59.12/20.27 | (486) occurrence_of(all_94_0_88, tptp0) = all_169_0_130 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_94_0_88, tptp0, all_169_0_130, 0 and discharging atoms occurrence_of(all_94_0_88, tptp0) = all_169_0_130, occurrence_of(all_94_0_88, tptp0) = 0, yields: % 59.12/20.27 | (268) all_169_0_130 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (268) can reduce 485 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (489) ~ (all_161_0_117 = 0) & occurrence_of(all_76_0_67, tptp0) = all_161_0_117 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (489) yields: % 59.12/20.27 | (490) ~ (all_161_0_117 = 0) % 59.12/20.27 | (491) occurrence_of(all_76_0_67, tptp0) = all_161_0_117 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (68) with all_76_0_67, tptp0, all_161_0_117, 0 and discharging atoms occurrence_of(all_76_0_67, tptp0) = all_161_0_117, occurrence_of(all_76_0_67, tptp0) = 0, yields: % 59.12/20.27 | (265) all_161_0_117 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (265) can reduce 490 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (494) all_243_2_217 = 0 & atomic(tptp0) = 0 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (494) yields: % 59.12/20.27 | (495) all_243_2_217 = 0 % 59.12/20.27 | (166) atomic(tptp0) = 0 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (102) with tptp0, 0, all_0_1_1 and discharging atoms atomic(tptp0) = all_0_1_1, atomic(tptp0) = 0, yields: % 59.12/20.27 | (167) all_0_1_1 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (167) can reduce 139 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (499) ~ (all_91_0_84 = 0) & root(all_43_2_52, tptp0) = all_91_0_84 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (499) yields: % 59.12/20.27 | (500) ~ (all_91_0_84 = 0) % 59.12/20.27 | (501) root(all_43_2_52, tptp0) = all_91_0_84 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (25) with all_43_2_52, tptp0, all_91_0_84, 0 and discharging atoms root(all_43_2_52, tptp0) = all_91_0_84, root(all_43_2_52, tptp0) = 0, yields: % 59.12/20.27 | (219) all_91_0_84 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (219) can reduce 500 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (504) ~ (all_105_2_103 = 0) & root_occ(all_43_2_52, all_0_0_0) = all_105_2_103 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (504) yields: % 59.12/20.27 | (505) ~ (all_105_2_103 = 0) % 59.12/20.27 | (506) root_occ(all_43_2_52, all_0_0_0) = all_105_2_103 % 59.12/20.27 | % 59.12/20.27 +-Applying beta-rule and splitting (204), into two cases. % 59.12/20.27 |-Branch one: % 59.12/20.27 | (218) all_91_0_84 = 0 & root_occ(all_43_2_52, all_0_0_0) = 0 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (218) yields: % 59.12/20.27 | (219) all_91_0_84 = 0 % 59.12/20.27 | (220) root_occ(all_43_2_52, all_0_0_0) = 0 % 59.12/20.27 | % 59.12/20.27 | Instantiating formula (64) with all_43_2_52, all_0_0_0, 0, all_105_2_103 and discharging atoms root_occ(all_43_2_52, all_0_0_0) = all_105_2_103, root_occ(all_43_2_52, all_0_0_0) = 0, yields: % 59.12/20.27 | (510) all_105_2_103 = 0 % 59.12/20.27 | % 59.12/20.27 | Equations (510) can reduce 505 to: % 59.12/20.27 | (168) $false % 59.12/20.27 | % 59.12/20.27 |-The branch is then unsatisfiable % 59.12/20.27 |-Branch two: % 59.12/20.27 | (499) ~ (all_91_0_84 = 0) & root(all_43_2_52, tptp0) = all_91_0_84 % 59.12/20.27 | % 59.12/20.27 | Applying alpha-rule on (499) yields: % 59.12/20.27 | (500) ~ (all_91_0_84 = 0) % 59.12/20.28 | (501) root(all_43_2_52, tptp0) = all_91_0_84 % 59.12/20.28 | % 59.12/20.28 | Instantiating formula (25) with all_43_2_52, tptp0, all_91_0_84, 0 and discharging atoms root(all_43_2_52, tptp0) = all_91_0_84, root(all_43_2_52, tptp0) = 0, yields: % 59.12/20.28 | (219) all_91_0_84 = 0 % 59.12/20.28 | % 59.12/20.28 | Equations (219) can reduce 500 to: % 59.12/20.28 | (168) $false % 59.12/20.28 | % 59.12/20.28 |-The branch is then unsatisfiable % 59.12/20.28 |-Branch two: % 59.12/20.28 | (517) all_43_2_52 = 0 & atomic(tptp0) = 0 % 59.12/20.28 | % 59.12/20.28 | Applying alpha-rule on (517) yields: % 59.12/20.28 | (518) all_43_2_52 = 0 % 59.12/20.28 | (166) atomic(tptp0) = 0 % 59.12/20.28 | % 59.12/20.28 | Instantiating formula (102) with tptp0, 0, all_0_1_1 and discharging atoms atomic(tptp0) = all_0_1_1, atomic(tptp0) = 0, yields: % 59.12/20.28 | (167) all_0_1_1 = 0 % 59.12/20.28 | % 59.12/20.28 | Equations (167) can reduce 139 to: % 59.12/20.28 | (168) $false % 59.12/20.28 | % 59.12/20.28 |-The branch is then unsatisfiable % 59.12/20.28 % SZS output end Proof for theBenchmark % 59.12/20.28 % 59.12/20.28 19668ms %------------------------------------------------------------------------------