%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM465+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n004.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 08:44:46 EDT 2022 % Result : Theorem 7.66s 2.52s % Output : Proof 14.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : NUM465+1 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.14 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.36 % Computer : n004.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Tue Jul 5 17:36:22 EDT 2022 % 0.14/0.36 % CPUTime : % 0.62/0.66 ____ _ % 0.62/0.66 ___ / __ \_____(_)___ ________ __________ % 0.62/0.66 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.62/0.66 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.62/0.66 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.62/0.66 % 0.62/0.66 A Theorem Prover for First-Order Logic % 0.62/0.66 (ePrincess v.1.0) % 0.62/0.66 % 0.62/0.66 (c) Philipp Rümmer, 2009-2015 % 0.62/0.66 (c) Peter Backeman, 2014-2015 % 0.62/0.66 (contributions by Angelo Brillout, Peter Baumgartner) % 0.62/0.66 Free software under GNU Lesser General Public License (LGPL). % 0.62/0.66 Bug reports to peter@backeman.se % 0.62/0.66 % 0.62/0.66 For more information, visit http://user.uu.se/~petba168/breu/ % 0.62/0.66 % 0.62/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.74/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.84/1.06 Prover 0: Preprocessing ... % 3.53/1.55 Prover 0: Constructing countermodel ... % 7.66/2.52 Prover 0: proved (1812ms) % 7.66/2.52 % 7.66/2.52 No countermodel exists, formula is valid % 7.66/2.52 % SZS status Theorem for theBenchmark % 7.66/2.52 % 7.66/2.52 Generating proof ... found it (size 75) % 13.50/3.86 % 13.50/3.86 % SZS output start Proof for theBenchmark % 13.50/3.86 Assumed formulas after preprocessing and simplification: % 13.50/3.86 | (0) ? [v0] : ( ~ (xm = sz00) & ~ (sz10 = sz00) & sdtasdt0(xn, xm) = v0 & sdtlseqdt0(sz10, xm) & aNaturalNumber0(xn) & aNaturalNumber0(xm) & aNaturalNumber0(sz10) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(xn, v0) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v2, v1) = v4) | ~ (sdtpldt0(v4, v5) = v6) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : (sdtasdt0(v7, v1) = v6 & sdtasdt0(v1, v7) = v8 & sdtasdt0(v1, v3) = v10 & sdtasdt0(v1, v2) = v9 & sdtpldt0(v9, v10) = v8 & sdtpldt0(v2, v3) = v7)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ (sdtpldt0(v4, v5) = v6) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : (sdtasdt0(v7, v1) = v8 & sdtasdt0(v3, v1) = v10 & sdtasdt0(v2, v1) = v9 & sdtasdt0(v1, v7) = v6 & sdtpldt0(v9, v10) = v8 & sdtpldt0(v2, v3) = v7)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v2, v1) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtlseqdt0(v4, v5)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v2, v1) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtasdt0(v1, v3) = v7 & sdtasdt0(v1, v2) = v6 & sdtlseqdt0(v6, v7))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v2, v1) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtasdt0(v1, v3) = v7 & sdtasdt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtasdt0(v2, v1) = v7 & sdtasdt0(v1, v3) = v6 & sdtlseqdt0(v7, v5) & sdtlseqdt0(v4, v6))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtasdt0(v2, v1) = v7 & sdtasdt0(v1, v3) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v2, v1) = v5) | ~ (sdtasdt0(v1, v3) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtasdt0(v3, v1) = v7 & sdtasdt0(v1, v2) = v6 & sdtlseqdt0(v6, v4) & sdtlseqdt0(v5, v7))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v2, v1) = v5) | ~ (sdtasdt0(v1, v3) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtasdt0(v3, v1) = v7 & sdtasdt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtlseqdt0(v4, v5)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtasdt0(v3, v1) = v7 & sdtasdt0(v2, v1) = v6 & sdtlseqdt0(v6, v7))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v1, v3) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtasdt0(v3, v1) = v7 & sdtasdt0(v2, v1) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (sdtpldt0(v3, v1) = v5) | ~ (sdtpldt0(v2, v1) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtpldt0(v1, v3) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (sdtpldt0(v3, v1) = v5) | ~ (sdtpldt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtpldt0(v2, v1) = v7 & sdtpldt0(v1, v3) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (sdtpldt0(v2, v1) = v5) | ~ (sdtpldt0(v1, v3) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v5) & ~ (v6 = v4) & sdtpldt0(v3, v1) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = v2 | ~ (sdtpldt0(v1, v3) = v5) | ~ (sdtpldt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ( ~ (v7 = v6) & sdtpldt0(v3, v1) = v7 & sdtpldt0(v2, v1) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v4, v3) = v5) | ~ (sdtasdt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : (sdtasdt0(v2, v3) = v6 & sdtasdt0(v1, v6) = v5)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v4, v1) = v5) | ~ (sdtpldt0(v2, v3) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : (sdtasdt0(v3, v1) = v10 & sdtasdt0(v2, v1) = v9 & sdtasdt0(v1, v4) = v6 & sdtasdt0(v1, v3) = v8 & sdtasdt0(v1, v2) = v7 & sdtpldt0(v9, v10) = v5 & sdtpldt0(v7, v8) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v2, v3) = v4) | ~ (sdtasdt0(v1, v4) = v5) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : (sdtasdt0(v6, v3) = v5 & sdtasdt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v4) = v5) | ~ (sdtpldt0(v2, v3) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : (sdtasdt0(v4, v1) = v8 & sdtasdt0(v3, v1) = v10 & sdtasdt0(v2, v1) = v9 & sdtasdt0(v1, v3) = v7 & sdtasdt0(v1, v2) = v6 & sdtpldt0(v9, v10) = v8 & sdtpldt0(v6, v7) = v5)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v3) = v5) | ~ (sdtpldt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : (sdtpldt0(v2, v3) = v6 & sdtpldt0(v1, v6) = v5)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v2, v3) = v4) | ~ (sdtpldt0(v1, v4) = v5) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v6] : (sdtpldt0(v6, v3) = v5 & sdtpldt0(v1, v2) = v6)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtmndt0(v2, v1) = v3) | ~ (sdtpldt0(v1, v4) = v2) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v2 | ~ (sdtmndt0(v2, v1) = v3) | ~ (sdtpldt0(v1, v3) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v4) | ~ (sdtasdt0(v2, v1) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v3, v1) = v4) | ~ (sdtasdt0(v2, v1) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v1, v3) = v4) | ~ (sdtasdt0(v1, v2) = v4) | ~ sdtlseqdt0(v2, v3) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | v1 = sz00 | ~ (sdtasdt0(v1, v3) = v4) | ~ (sdtasdt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (sdtpldt0(v3, v1) = v4) | ~ (sdtpldt0(v2, v1) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = v2 | ~ (sdtpldt0(v1, v3) = v4) | ~ (sdtpldt0(v1, v2) = v4) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtmndt0(v4, v3) = v2) | ~ (sdtmndt0(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtasdt0(v4, v3) = v2) | ~ (sdtasdt0(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v4, v3) = v2) | ~ (sdtpldt0(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v3, v2) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & ~ (v5 = v4) & sdtpldt0(v3, v1) = v5 & sdtpldt0(v2, v3) = v7 & sdtpldt0(v1, v3) = v6 & sdtlseqdt0(v6, v7) & sdtlseqdt0(v5, v4))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v3, v1) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v6) & ~ (v5 = v4) & sdtpldt0(v3, v2) = v5 & sdtpldt0(v2, v3) = v7 & sdtpldt0(v1, v3) = v6 & sdtlseqdt0(v6, v7) & sdtlseqdt0(v4, v5))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v2, v3) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v4) & ~ (v6 = v5) & sdtpldt0(v3, v2) = v6 & sdtpldt0(v3, v1) = v5 & sdtpldt0(v1, v3) = v7 & sdtlseqdt0(v7, v4) & sdtlseqdt0(v5, v6))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v1, v3) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v5] : ? [v6] : ? [v7] : ( ~ (v7 = v4) & ~ (v6 = v5) & sdtpldt0(v3, v2) = v6 & sdtpldt0(v3, v1) = v5 & sdtpldt0(v2, v3) = v7 & sdtlseqdt0(v5, v6) & sdtlseqdt0(v4, v7))) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtmndt0(v2, v1) = v3) | ~ (sdtpldt0(v1, v3) = v4) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | aNaturalNumber0(v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasdt0(v2, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtasdt0(v1, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtasdt0(v2, v1) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | aNaturalNumber0(v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtpldt0(v1, v2) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v3) = v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtlseqdt0(v1, v2)) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtpldt0(v2, v1) = v3) & ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | aNaturalNumber0(v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ sdtlseqdt0(v2, v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtlseqdt0(v1, v3)) & ! [v1] : ! [v2] : (v2 = v1 | ~ (sdtasdt0(v1, sz10) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = v1 | ~ (sdtasdt0(sz10, v1) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = v1 | ~ (sdtpldt0(v1, sz00) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = v1 | ~ (sdtpldt0(sz00, v1) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = v1 | ~ sdtlseqdt0(v2, v1) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = sz00 | v1 = sz00 | ~ (sdtasdt0(v1, v2) = sz00) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtasdt0(v1, sz00) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtasdt0(sz00, v1) = v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v1, v2) = sz00) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : (v1 = sz00 | ~ (sdtpldt0(v1, v2) = sz00) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1)) & ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, sz10) = v2) | ~ aNaturalNumber0(v1) | sdtasdt0(sz10, v1) = v1) & ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, sz00) = v2) | ~ aNaturalNumber0(v1) | sdtasdt0(sz00, v1) = sz00) & ! [v1] : ! [v2] : ( ~ (sdtasdt0(sz10, v1) = v2) | ~ aNaturalNumber0(v1) | sdtasdt0(v1, sz10) = v1) & ! [v1] : ! [v2] : ( ~ (sdtasdt0(sz00, v1) = v2) | ~ aNaturalNumber0(v1) | sdtasdt0(v1, sz00) = sz00) & ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, sz00) = v2) | ~ aNaturalNumber0(v1) | sdtpldt0(sz00, v1) = v1) & ! [v1] : ! [v2] : ( ~ (sdtpldt0(sz00, v1) = v2) | ~ aNaturalNumber0(v1) | sdtpldt0(v1, sz00) = v1) & ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ? [v3] : (sdtpldt0(v1, v3) = v2 & aNaturalNumber0(v3))) & ! [v1] : ! [v2] : ( ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | sdtlseqdt0(v2, v1) | sdtlseqdt0(v1, v2)) & ! [v1] : (v1 = sz10 | v1 = sz00 | ~ aNaturalNumber0(v1) | sdtlseqdt0(sz10, v1)) & ! [v1] : ( ~ aNaturalNumber0(v1) | sdtlseqdt0(v1, v1))) % 13.63/3.92 | Instantiating (0) with all_0_0_0 yields: % 13.63/3.92 | (1) ~ (xm = sz00) & ~ (sz10 = sz00) & sdtasdt0(xn, xm) = all_0_0_0 & sdtlseqdt0(sz10, xm) & aNaturalNumber0(xn) & aNaturalNumber0(xm) & aNaturalNumber0(sz10) & aNaturalNumber0(sz00) & ~ sdtlseqdt0(xn, all_0_0_0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtlseqdt0(v5, v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v2) = v5 & sdtlseqdt0(v6, v4) & sdtlseqdt0(v3, v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, v0) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v0, v1) = v5 & sdtlseqdt0(v5, v3) & sdtlseqdt0(v4, v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, v0) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5 & sdtlseqdt0(v5, v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtpldt0(v0, v2) = v6 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtpldt0(v1, v0) = v6 & sdtpldt0(v0, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v1, v0) = v4) | ~ (sdtpldt0(v0, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v3) = v5 & sdtasdt0(v0, v2) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v6, v7) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v3, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v3) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v3) | ~ (sdtasdt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v3) | ~ (sdtpldt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v3) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v2, v1) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v0) = v4 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v2) = v5 & sdtlseqdt0(v5, v6) & sdtlseqdt0(v4, v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v2, v0) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v1) = v4 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v2) = v5 & sdtlseqdt0(v5, v6) & sdtlseqdt0(v3, v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v1, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v3) & ~ (v5 = v4) & sdtpldt0(v2, v1) = v5 & sdtpldt0(v2, v0) = v4 & sdtpldt0(v0, v2) = v6 & sdtlseqdt0(v6, v3) & sdtlseqdt0(v4, v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v3) & ~ (v5 = v4) & sdtpldt0(v2, v1) = v5 & sdtpldt0(v2, v0) = v4 & sdtpldt0(v1, v2) = v6 & sdtlseqdt0(v4, v5) & sdtlseqdt0(v3, v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v2) = v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(sz10, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(sz00, v0) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz10) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz00) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(sz00, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, sz00) = v0) & ! [v0] : ! [v1] : ( ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2] : (sdtpldt0(v0, v2) = v1 & aNaturalNumber0(v2))) & ! [v0] : ! [v1] : ( ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) & ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | sdtlseqdt0(sz10, v0)) & ! [v0] : ( ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v0)) % 13.91/3.95 | % 13.91/3.95 | Applying alpha-rule on (1) yields: % 13.91/3.95 | (2) aNaturalNumber0(sz10) % 13.91/3.95 | (3) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 13.91/3.95 | (4) sdtlseqdt0(sz10, xm) % 13.91/3.95 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) % 13.91/3.95 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v2, v1) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v0) = v4 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v2) = v5 & sdtlseqdt0(v5, v6) & sdtlseqdt0(v4, v3))) % 13.91/3.95 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, v1) = v2) % 13.91/3.95 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 13.91/3.95 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 13.91/3.95 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v2) = v5 & sdtlseqdt0(v6, v4) & sdtlseqdt0(v3, v5))) % 13.91/3.95 | (11) ! [v0] : ! [v1] : ( ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2] : (sdtpldt0(v0, v2) = v1 & aNaturalNumber0(v2))) % 13.91/3.95 | (12) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 13.91/3.95 | (13) ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | sdtlseqdt0(sz10, v0)) % 13.91/3.95 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) % 13.91/3.95 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 13.91/3.95 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 13.91/3.95 | (17) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) % 13.91/3.95 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v2)) % 13.91/3.95 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) % 13.91/3.95 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v3) & ~ (v5 = v4) & sdtpldt0(v2, v1) = v5 & sdtpldt0(v2, v0) = v4 & sdtpldt0(v1, v2) = v6 & sdtlseqdt0(v4, v5) & sdtlseqdt0(v3, v6))) % 13.91/3.95 | (21) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, sz00) = v0) % 13.91/3.96 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5)) % 13.91/3.96 | (23) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(sz00, v0) = v0) % 13.91/3.96 | (24) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 13.91/3.96 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtpldt0(v1, v0) = v6 & sdtpldt0(v0, v2) = v5)) % 14.00/3.96 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v0) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v3) = v5 & sdtasdt0(v0, v2) = v7 & sdtasdt0(v0, v1) = v6 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v6, v7) = v5)) % 14.00/3.96 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v1, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v3) & ~ (v5 = v4) & sdtpldt0(v2, v1) = v5 & sdtpldt0(v2, v0) = v4 & sdtpldt0(v0, v2) = v6 & sdtlseqdt0(v6, v3) & sdtlseqdt0(v4, v5))) % 14.00/3.96 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v4) | ~ (sdtpldt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtpldt0(v0, v2) = v6 & sdtpldt0(v0, v1) = v5)) % 14.00/3.96 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.96 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (sdtpldt0(v2, v0) = v3) | ~ (sdtpldt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.96 | (31) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 14.00/3.96 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 14.00/3.96 | (33) aNaturalNumber0(xn) % 14.00/3.96 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v3, v0) = v7 & sdtasdt0(v2, v0) = v9 & sdtasdt0(v1, v0) = v8 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v5, v6) = v4)) % 14.00/3.96 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) % 14.00/3.96 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, v0) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v0, v1) = v5 & sdtlseqdt0(v5, v3) & sdtlseqdt0(v4, v6))) % 14.00/3.96 | (37) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz00) = sz00) % 14.00/3.96 | (38) ~ sdtlseqdt0(xn, all_0_0_0) % 14.00/3.96 | (39) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz10) = v0) % 14.00/3.96 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v3) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.96 | (41) ! [v0] : ! [v1] : ( ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) % 14.00/3.96 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v1, v0) = v5 & sdtlseqdt0(v5, v6))) % 14.00/3.97 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (44) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v1, v0) = v5)) % 14.00/3.97 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v3, v4)) % 14.00/3.97 | (47) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(sz00, v0) = sz00) % 14.00/3.97 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v3) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (49) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) % 14.00/3.97 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v1, v0) = v4) | ~ (sdtpldt0(v0, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtpldt0(v2, v0) = v6 & sdtpldt0(v0, v1) = v5)) % 14.00/3.97 | (52) ~ (xm = sz00) % 14.00/3.97 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v2) = v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) % 14.00/3.97 | (54) sdtasdt0(xn, xm) = all_0_0_0 % 14.00/3.97 | (55) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v2, v0) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v4] : ? [v5] : ? [v6] : ( ~ (v6 = v5) & ~ (v4 = v3) & sdtpldt0(v2, v1) = v4 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v2) = v5 & sdtlseqdt0(v5, v6) & sdtlseqdt0(v3, v4))) % 14.00/3.97 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v1, v0) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v2, v0) = v6 & sdtasdt0(v0, v1) = v5)) % 14.00/3.97 | (58) ! [v0] : ( ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v0)) % 14.00/3.97 | (59) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (60) aNaturalNumber0(xm) % 14.00/3.97 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v6, v0) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v2) = v9 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v9) = v7 & sdtpldt0(v1, v2) = v6)) % 14.00/3.97 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v1, v0) = v2) % 14.00/3.97 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.97 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v4) & ~ (v5 = v3) & sdtasdt0(v1, v0) = v6 & sdtasdt0(v0, v2) = v5)) % 14.00/3.97 | (65) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v1, v0) = v2) % 14.00/3.98 | (66) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) % 14.00/3.98 | (67) ~ (sz10 = sz00) % 14.00/3.98 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v3) | ~ (sdtasdt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.98 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v3, v4)) % 14.00/3.98 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5)) % 14.00/3.98 | (71) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 14.00/3.98 | (72) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, v1) = v2) % 14.00/3.98 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v2, v0) = v4) | ~ (sdtasdt0(v1, v0) = v3) | ~ sdtlseqdt0(v1, v2) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v5] : ? [v6] : ( ~ (v6 = v5) & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtlseqdt0(v5, v6))) % 14.00/3.98 | (74) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(sz10, v0) = v0) % 14.00/3.98 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 14.00/3.98 | (76) aNaturalNumber0(sz00) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (41) with xn, xn and discharging atoms aNaturalNumber0(xn), yields: % 14.00/3.98 | (77) sdtlseqdt0(xn, xn) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (7) with all_0_0_0, xn, xm and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(xn), aNaturalNumber0(xm), yields: % 14.00/3.98 | (78) sdtasdt0(xm, xn) = all_0_0_0 % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (31) with all_0_0_0, xm, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(xn), aNaturalNumber0(xm), yields: % 14.00/3.98 | (79) aNaturalNumber0(all_0_0_0) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (11) with xm, sz10 and discharging atoms sdtlseqdt0(sz10, xm), aNaturalNumber0(xm), aNaturalNumber0(sz10), yields: % 14.00/3.98 | (80) ? [v0] : (sdtpldt0(sz10, v0) = xm & aNaturalNumber0(v0)) % 14.00/3.98 | % 14.00/3.98 | Instantiating (80) with all_9_0_1 yields: % 14.00/3.98 | (81) sdtpldt0(sz10, all_9_0_1) = xm & aNaturalNumber0(all_9_0_1) % 14.00/3.98 | % 14.00/3.98 | Applying alpha-rule on (81) yields: % 14.00/3.98 | (82) sdtpldt0(sz10, all_9_0_1) = xm % 14.00/3.98 | (83) aNaturalNumber0(all_9_0_1) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (11) with xn, xn and discharging atoms sdtlseqdt0(xn, xn), aNaturalNumber0(xn), yields: % 14.00/3.98 | (84) ? [v0] : (sdtpldt0(xn, v0) = xn & aNaturalNumber0(v0)) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (34) with all_0_0_0, xm, all_9_0_1, sz10, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, sdtpldt0(sz10, all_9_0_1) = xm, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 14.00/3.98 | (85) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_9_0_1, xn) = v4 & sdtasdt0(xn, all_9_0_1) = v1 & sdtasdt0(xn, sz10) = v0 & sdtasdt0(xm, xn) = v2 & sdtasdt0(sz10, xn) = v3 & sdtpldt0(v3, v4) = v2 & sdtpldt0(v0, v1) = all_0_0_0) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (26) with all_0_0_0, xm, all_9_0_1, sz10, xn and discharging atoms sdtasdt0(xm, xn) = all_0_0_0, sdtpldt0(sz10, all_9_0_1) = xm, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 14.00/3.98 | (86) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_9_0_1, xn) = v4 & sdtasdt0(xn, all_9_0_1) = v2 & sdtasdt0(xn, xm) = v0 & sdtasdt0(xn, sz10) = v1 & sdtasdt0(sz10, xn) = v3 & sdtpldt0(v3, v4) = all_0_0_0 & sdtpldt0(v1, v2) = v0) % 14.00/3.98 | % 14.00/3.98 | Instantiating formula (72) with xm, sz10, all_9_0_1 and discharging atoms sdtpldt0(sz10, all_9_0_1) = xm, aNaturalNumber0(all_9_0_1), aNaturalNumber0(sz10), yields: % 14.00/3.98 | (87) sdtpldt0(all_9_0_1, sz10) = xm % 14.00/3.98 | % 14.00/3.98 | Instantiating (86) with all_17_0_2, all_17_1_3, all_17_2_4, all_17_3_5, all_17_4_6 yields: % 14.00/3.98 | (88) sdtasdt0(all_9_0_1, xn) = all_17_0_2 & sdtasdt0(xn, all_9_0_1) = all_17_2_4 & sdtasdt0(xn, xm) = all_17_4_6 & sdtasdt0(xn, sz10) = all_17_3_5 & sdtasdt0(sz10, xn) = all_17_1_3 & sdtpldt0(all_17_1_3, all_17_0_2) = all_0_0_0 & sdtpldt0(all_17_3_5, all_17_2_4) = all_17_4_6 % 14.00/3.98 | % 14.00/3.98 | Applying alpha-rule on (88) yields: % 14.00/3.98 | (89) sdtasdt0(xn, sz10) = all_17_3_5 % 14.00/3.98 | (90) sdtasdt0(sz10, xn) = all_17_1_3 % 14.00/3.98 | (91) sdtasdt0(xn, all_9_0_1) = all_17_2_4 % 14.00/3.98 | (92) sdtasdt0(xn, xm) = all_17_4_6 % 14.00/3.99 | (93) sdtpldt0(all_17_1_3, all_17_0_2) = all_0_0_0 % 14.00/3.99 | (94) sdtasdt0(all_9_0_1, xn) = all_17_0_2 % 14.00/3.99 | (95) sdtpldt0(all_17_3_5, all_17_2_4) = all_17_4_6 % 14.00/3.99 | % 14.00/3.99 | Instantiating (85) with all_23_0_9, all_23_1_10, all_23_2_11, all_23_3_12, all_23_4_13 yields: % 14.00/3.99 | (96) sdtasdt0(all_9_0_1, xn) = all_23_0_9 & sdtasdt0(xn, all_9_0_1) = all_23_3_12 & sdtasdt0(xn, sz10) = all_23_4_13 & sdtasdt0(xm, xn) = all_23_2_11 & sdtasdt0(sz10, xn) = all_23_1_10 & sdtpldt0(all_23_1_10, all_23_0_9) = all_23_2_11 & sdtpldt0(all_23_4_13, all_23_3_12) = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | Applying alpha-rule on (96) yields: % 14.00/3.99 | (97) sdtasdt0(xn, sz10) = all_23_4_13 % 14.00/3.99 | (98) sdtpldt0(all_23_4_13, all_23_3_12) = all_0_0_0 % 14.00/3.99 | (99) sdtasdt0(all_9_0_1, xn) = all_23_0_9 % 14.00/3.99 | (100) sdtpldt0(all_23_1_10, all_23_0_9) = all_23_2_11 % 14.00/3.99 | (101) sdtasdt0(sz10, xn) = all_23_1_10 % 14.00/3.99 | (102) sdtasdt0(xm, xn) = all_23_2_11 % 14.00/3.99 | (103) sdtasdt0(xn, all_9_0_1) = all_23_3_12 % 14.00/3.99 | % 14.00/3.99 | Instantiating (84) with all_27_0_15 yields: % 14.00/3.99 | (104) sdtpldt0(xn, all_27_0_15) = xn & aNaturalNumber0(all_27_0_15) % 14.00/3.99 | % 14.00/3.99 | Applying alpha-rule on (104) yields: % 14.00/3.99 | (105) sdtpldt0(xn, all_27_0_15) = xn % 14.00/3.99 | (106) aNaturalNumber0(all_27_0_15) % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with all_9_0_1, xn, all_17_0_2, all_23_0_9 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_23_0_9, sdtasdt0(all_9_0_1, xn) = all_17_0_2, yields: % 14.00/3.99 | (107) all_23_0_9 = all_17_0_2 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with xn, all_9_0_1, all_17_2_4, all_23_3_12 and discharging atoms sdtasdt0(xn, all_9_0_1) = all_23_3_12, sdtasdt0(xn, all_9_0_1) = all_17_2_4, yields: % 14.00/3.99 | (108) all_23_3_12 = all_17_2_4 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with xn, xm, all_17_4_6, all_0_0_0 and discharging atoms sdtasdt0(xn, xm) = all_17_4_6, sdtasdt0(xn, xm) = all_0_0_0, yields: % 14.00/3.99 | (109) all_17_4_6 = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (49) with all_23_4_13, xn and discharging atoms sdtasdt0(xn, sz10) = all_23_4_13, aNaturalNumber0(xn), yields: % 14.00/3.99 | (110) all_23_4_13 = xn % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with xn, sz10, all_17_3_5, all_23_4_13 and discharging atoms sdtasdt0(xn, sz10) = all_23_4_13, sdtasdt0(xn, sz10) = all_17_3_5, yields: % 14.00/3.99 | (111) all_23_4_13 = all_17_3_5 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with xm, xn, all_23_2_11, all_0_0_0 and discharging atoms sdtasdt0(xm, xn) = all_23_2_11, sdtasdt0(xm, xn) = all_0_0_0, yields: % 14.00/3.99 | (112) all_23_2_11 = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (59) with all_23_1_10, xn and discharging atoms sdtasdt0(sz10, xn) = all_23_1_10, aNaturalNumber0(xn), yields: % 14.00/3.99 | (113) all_23_1_10 = xn % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (15) with sz10, xn, all_17_1_3, all_23_1_10 and discharging atoms sdtasdt0(sz10, xn) = all_23_1_10, sdtasdt0(sz10, xn) = all_17_1_3, yields: % 14.00/3.99 | (114) all_23_1_10 = all_17_1_3 % 14.00/3.99 | % 14.00/3.99 | Combining equations (113,114) yields a new equation: % 14.00/3.99 | (115) all_17_1_3 = xn % 14.00/3.99 | % 14.00/3.99 | Combining equations (111,110) yields a new equation: % 14.00/3.99 | (116) all_17_3_5 = xn % 14.00/3.99 | % 14.00/3.99 | Simplifying 116 yields: % 14.00/3.99 | (117) all_17_3_5 = xn % 14.00/3.99 | % 14.00/3.99 | From (107) and (99) follows: % 14.00/3.99 | (94) sdtasdt0(all_9_0_1, xn) = all_17_0_2 % 14.00/3.99 | % 14.00/3.99 | From (108) and (103) follows: % 14.00/3.99 | (91) sdtasdt0(xn, all_9_0_1) = all_17_2_4 % 14.00/3.99 | % 14.00/3.99 | From (109) and (92) follows: % 14.00/3.99 | (54) sdtasdt0(xn, xm) = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | From (117) and (89) follows: % 14.00/3.99 | (121) sdtasdt0(xn, sz10) = xn % 14.00/3.99 | % 14.00/3.99 | From (112) and (102) follows: % 14.00/3.99 | (78) sdtasdt0(xm, xn) = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | From (115) and (93) follows: % 14.00/3.99 | (123) sdtpldt0(xn, all_17_0_2) = all_0_0_0 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (31) with all_17_0_2, xn, all_9_0_1 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_17_0_2, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), yields: % 14.00/3.99 | (124) aNaturalNumber0(all_17_0_2) % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (62) with all_17_2_4, all_9_0_1, xn and discharging atoms sdtasdt0(xn, all_9_0_1) = all_17_2_4, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), yields: % 14.00/3.99 | (125) sdtasdt0(all_9_0_1, xn) = all_17_2_4 % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (14) with all_17_0_2, xn, sz10, xn, all_9_0_1 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_17_0_2, sdtasdt0(xn, sz10) = xn, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 14.00/3.99 | (126) ? [v0] : (sdtasdt0(v0, sz10) = all_17_0_2 & sdtasdt0(all_9_0_1, xn) = v0) % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (34) with all_0_0_0, xm, sz10, all_9_0_1, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, sdtpldt0(all_9_0_1, sz10) = xm, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 14.00/3.99 | (127) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_9_0_1, xn) = v3 & sdtasdt0(xn, all_9_0_1) = v0 & sdtasdt0(xn, sz10) = v1 & sdtasdt0(xm, xn) = v2 & sdtasdt0(sz10, xn) = v4 & sdtpldt0(v3, v4) = v2 & sdtpldt0(v0, v1) = all_0_0_0) % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (26) with all_0_0_0, xm, sz10, all_9_0_1, xn and discharging atoms sdtasdt0(xm, xn) = all_0_0_0, sdtpldt0(all_9_0_1, sz10) = xm, aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 14.00/3.99 | (128) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_9_0_1, xn) = v3 & sdtasdt0(xn, all_9_0_1) = v1 & sdtasdt0(xn, xm) = v0 & sdtasdt0(xn, sz10) = v2 & sdtasdt0(sz10, xn) = v4 & sdtpldt0(v3, v4) = all_0_0_0 & sdtpldt0(v1, v2) = v0) % 14.00/3.99 | % 14.00/3.99 | Instantiating formula (34) with all_17_0_2, xn, all_27_0_15, xn, all_9_0_1 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_17_0_2, sdtpldt0(xn, all_27_0_15) = xn, aNaturalNumber0(all_27_0_15), aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), yields: % 14.00/3.99 | (129) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_27_0_15, all_9_0_1) = v4 & sdtasdt0(all_9_0_1, all_27_0_15) = v1 & sdtasdt0(all_9_0_1, xn) = v0 & sdtasdt0(xn, all_9_0_1) = v3 & sdtasdt0(xn, all_9_0_1) = v2 & sdtpldt0(v3, v4) = v2 & sdtpldt0(v0, v1) = all_17_0_2) % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (26) with all_17_2_4, xn, all_27_0_15, xn, all_9_0_1 and discharging atoms sdtasdt0(xn, all_9_0_1) = all_17_2_4, sdtpldt0(xn, all_27_0_15) = xn, aNaturalNumber0(all_27_0_15), aNaturalNumber0(all_9_0_1), aNaturalNumber0(xn), yields: % 14.00/4.00 | (130) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(all_27_0_15, all_9_0_1) = v4 & sdtasdt0(all_9_0_1, all_27_0_15) = v2 & sdtasdt0(all_9_0_1, xn) = v1 & sdtasdt0(all_9_0_1, xn) = v0 & sdtasdt0(xn, all_9_0_1) = v3 & sdtpldt0(v3, v4) = all_17_2_4 & sdtpldt0(v1, v2) = v0) % 14.00/4.00 | % 14.00/4.00 | Instantiating (126) with all_61_0_39 yields: % 14.00/4.00 | (131) sdtasdt0(all_61_0_39, sz10) = all_17_0_2 & sdtasdt0(all_9_0_1, xn) = all_61_0_39 % 14.00/4.00 | % 14.00/4.00 | Applying alpha-rule on (131) yields: % 14.00/4.00 | (132) sdtasdt0(all_61_0_39, sz10) = all_17_0_2 % 14.00/4.00 | (133) sdtasdt0(all_9_0_1, xn) = all_61_0_39 % 14.00/4.00 | % 14.00/4.00 | Instantiating (130) with all_65_0_41, all_65_1_42, all_65_2_43, all_65_3_44, all_65_4_45 yields: % 14.00/4.00 | (134) sdtasdt0(all_27_0_15, all_9_0_1) = all_65_0_41 & sdtasdt0(all_9_0_1, all_27_0_15) = all_65_2_43 & sdtasdt0(all_9_0_1, xn) = all_65_3_44 & sdtasdt0(all_9_0_1, xn) = all_65_4_45 & sdtasdt0(xn, all_9_0_1) = all_65_1_42 & sdtpldt0(all_65_1_42, all_65_0_41) = all_17_2_4 & sdtpldt0(all_65_3_44, all_65_2_43) = all_65_4_45 % 14.00/4.00 | % 14.00/4.00 | Applying alpha-rule on (134) yields: % 14.00/4.00 | (135) sdtpldt0(all_65_3_44, all_65_2_43) = all_65_4_45 % 14.00/4.00 | (136) sdtasdt0(all_9_0_1, all_27_0_15) = all_65_2_43 % 14.00/4.00 | (137) sdtasdt0(xn, all_9_0_1) = all_65_1_42 % 14.00/4.00 | (138) sdtasdt0(all_9_0_1, xn) = all_65_3_44 % 14.00/4.00 | (139) sdtasdt0(all_9_0_1, xn) = all_65_4_45 % 14.00/4.00 | (140) sdtpldt0(all_65_1_42, all_65_0_41) = all_17_2_4 % 14.00/4.00 | (141) sdtasdt0(all_27_0_15, all_9_0_1) = all_65_0_41 % 14.00/4.00 | % 14.00/4.00 | Instantiating (129) with all_67_0_46, all_67_1_47, all_67_2_48, all_67_3_49, all_67_4_50 yields: % 14.00/4.00 | (142) sdtasdt0(all_27_0_15, all_9_0_1) = all_67_0_46 & sdtasdt0(all_9_0_1, all_27_0_15) = all_67_3_49 & sdtasdt0(all_9_0_1, xn) = all_67_4_50 & sdtasdt0(xn, all_9_0_1) = all_67_1_47 & sdtasdt0(xn, all_9_0_1) = all_67_2_48 & sdtpldt0(all_67_1_47, all_67_0_46) = all_67_2_48 & sdtpldt0(all_67_4_50, all_67_3_49) = all_17_0_2 % 14.00/4.00 | % 14.00/4.00 | Applying alpha-rule on (142) yields: % 14.00/4.00 | (143) sdtasdt0(all_9_0_1, all_27_0_15) = all_67_3_49 % 14.00/4.00 | (144) sdtasdt0(all_27_0_15, all_9_0_1) = all_67_0_46 % 14.00/4.00 | (145) sdtpldt0(all_67_1_47, all_67_0_46) = all_67_2_48 % 14.00/4.00 | (146) sdtasdt0(xn, all_9_0_1) = all_67_2_48 % 14.00/4.00 | (147) sdtasdt0(xn, all_9_0_1) = all_67_1_47 % 14.00/4.00 | (148) sdtpldt0(all_67_4_50, all_67_3_49) = all_17_0_2 % 14.00/4.00 | (149) sdtasdt0(all_9_0_1, xn) = all_67_4_50 % 14.00/4.00 | % 14.00/4.00 | Instantiating (128) with all_89_0_73, all_89_1_74, all_89_2_75, all_89_3_76, all_89_4_77 yields: % 14.00/4.00 | (150) sdtasdt0(all_9_0_1, xn) = all_89_1_74 & sdtasdt0(xn, all_9_0_1) = all_89_3_76 & sdtasdt0(xn, xm) = all_89_4_77 & sdtasdt0(xn, sz10) = all_89_2_75 & sdtasdt0(sz10, xn) = all_89_0_73 & sdtpldt0(all_89_1_74, all_89_0_73) = all_0_0_0 & sdtpldt0(all_89_3_76, all_89_2_75) = all_89_4_77 % 14.00/4.00 | % 14.00/4.00 | Applying alpha-rule on (150) yields: % 14.00/4.00 | (151) sdtasdt0(all_9_0_1, xn) = all_89_1_74 % 14.00/4.00 | (152) sdtpldt0(all_89_1_74, all_89_0_73) = all_0_0_0 % 14.00/4.00 | (153) sdtasdt0(xn, sz10) = all_89_2_75 % 14.00/4.00 | (154) sdtasdt0(sz10, xn) = all_89_0_73 % 14.00/4.00 | (155) sdtpldt0(all_89_3_76, all_89_2_75) = all_89_4_77 % 14.00/4.00 | (156) sdtasdt0(xn, all_9_0_1) = all_89_3_76 % 14.00/4.00 | (157) sdtasdt0(xn, xm) = all_89_4_77 % 14.00/4.00 | % 14.00/4.00 | Instantiating (127) with all_97_0_85, all_97_1_86, all_97_2_87, all_97_3_88, all_97_4_89 yields: % 14.00/4.00 | (158) sdtasdt0(all_9_0_1, xn) = all_97_1_86 & sdtasdt0(xn, all_9_0_1) = all_97_4_89 & sdtasdt0(xn, sz10) = all_97_3_88 & sdtasdt0(xm, xn) = all_97_2_87 & sdtasdt0(sz10, xn) = all_97_0_85 & sdtpldt0(all_97_1_86, all_97_0_85) = all_97_2_87 & sdtpldt0(all_97_4_89, all_97_3_88) = all_0_0_0 % 14.00/4.00 | % 14.00/4.00 | Applying alpha-rule on (158) yields: % 14.00/4.00 | (159) sdtpldt0(all_97_1_86, all_97_0_85) = all_97_2_87 % 14.00/4.00 | (160) sdtasdt0(xn, sz10) = all_97_3_88 % 14.00/4.00 | (161) sdtasdt0(sz10, xn) = all_97_0_85 % 14.00/4.00 | (162) sdtasdt0(xm, xn) = all_97_2_87 % 14.00/4.00 | (163) sdtasdt0(xn, all_9_0_1) = all_97_4_89 % 14.00/4.00 | (164) sdtpldt0(all_97_4_89, all_97_3_88) = all_0_0_0 % 14.00/4.00 | (165) sdtasdt0(all_9_0_1, xn) = all_97_1_86 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_67_4_50, all_97_1_86 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_97_1_86, sdtasdt0(all_9_0_1, xn) = all_67_4_50, yields: % 14.00/4.00 | (166) all_97_1_86 = all_67_4_50 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_65_3_44, all_89_1_74 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_89_1_74, sdtasdt0(all_9_0_1, xn) = all_65_3_44, yields: % 14.00/4.00 | (167) all_89_1_74 = all_65_3_44 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_65_3_44, all_67_4_50 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_67_4_50, sdtasdt0(all_9_0_1, xn) = all_65_3_44, yields: % 14.00/4.00 | (168) all_67_4_50 = all_65_3_44 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_65_4_45, all_97_1_86 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_97_1_86, sdtasdt0(all_9_0_1, xn) = all_65_4_45, yields: % 14.00/4.00 | (169) all_97_1_86 = all_65_4_45 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_61_0_39, all_17_0_2 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_61_0_39, sdtasdt0(all_9_0_1, xn) = all_17_0_2, yields: % 14.00/4.00 | (170) all_61_0_39 = all_17_0_2 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_61_0_39, all_65_3_44 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_65_3_44, sdtasdt0(all_9_0_1, xn) = all_61_0_39, yields: % 14.00/4.00 | (171) all_65_3_44 = all_61_0_39 % 14.00/4.00 | % 14.00/4.00 | Instantiating formula (15) with all_9_0_1, xn, all_17_2_4, all_89_1_74 and discharging atoms sdtasdt0(all_9_0_1, xn) = all_89_1_74, sdtasdt0(all_9_0_1, xn) = all_17_2_4, yields: % 14.00/4.00 | (172) all_89_1_74 = all_17_2_4 % 14.00/4.00 | % 14.00/4.00 | Combining equations (166,169) yields a new equation: % 14.00/4.00 | (173) all_67_4_50 = all_65_4_45 % 14.00/4.00 | % 14.00/4.00 | Simplifying 173 yields: % 14.00/4.00 | (174) all_67_4_50 = all_65_4_45 % 14.00/4.00 | % 14.00/4.00 | Combining equations (167,172) yields a new equation: % 14.00/4.00 | (175) all_65_3_44 = all_17_2_4 % 14.00/4.00 | % 14.00/4.00 | Simplifying 175 yields: % 14.00/4.00 | (176) all_65_3_44 = all_17_2_4 % 14.00/4.00 | % 14.00/4.00 | Combining equations (168,174) yields a new equation: % 14.00/4.01 | (177) all_65_3_44 = all_65_4_45 % 14.00/4.01 | % 14.00/4.01 | Simplifying 177 yields: % 14.00/4.01 | (178) all_65_3_44 = all_65_4_45 % 14.00/4.01 | % 14.00/4.01 | Combining equations (176,178) yields a new equation: % 14.00/4.01 | (179) all_65_4_45 = all_17_2_4 % 14.00/4.01 | % 14.00/4.01 | Combining equations (171,178) yields a new equation: % 14.00/4.01 | (180) all_65_4_45 = all_61_0_39 % 14.00/4.01 | % 14.00/4.01 | Combining equations (180,179) yields a new equation: % 14.00/4.01 | (181) all_61_0_39 = all_17_2_4 % 14.00/4.01 | % 14.00/4.01 | Simplifying 181 yields: % 14.00/4.01 | (182) all_61_0_39 = all_17_2_4 % 14.00/4.01 | % 14.00/4.01 | Combining equations (170,182) yields a new equation: % 14.00/4.01 | (183) all_17_0_2 = all_17_2_4 % 14.00/4.01 | % 14.00/4.01 | Simplifying 183 yields: % 14.00/4.01 | (184) all_17_0_2 = all_17_2_4 % 14.00/4.01 | % 14.00/4.01 | From (184) and (123) follows: % 14.00/4.01 | (185) sdtpldt0(xn, all_17_2_4) = all_0_0_0 % 14.00/4.01 | % 14.00/4.01 | From (184) and (124) follows: % 14.00/4.01 | (186) aNaturalNumber0(all_17_2_4) % 14.00/4.01 | % 14.00/4.01 | Instantiating formula (53) with all_17_2_4, all_0_0_0, xn and discharging atoms sdtpldt0(xn, all_17_2_4) = all_0_0_0, aNaturalNumber0(all_17_2_4), aNaturalNumber0(all_0_0_0), aNaturalNumber0(xn), ~ sdtlseqdt0(xn, all_0_0_0), yields: % 14.00/4.01 | (187) $false % 14.00/4.01 | % 14.00/4.01 |-The branch is then unsatisfiable % 14.00/4.01 % SZS output end Proof for theBenchmark % 14.00/4.01 % 14.00/4.01 3340ms %------------------------------------------------------------------------------