%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM487+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n003.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:45:01 EDT 2022 % Result : Theorem 43.42s 16.61s % Output : Proof 82.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM487+1 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n003.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jul 6 13:31:41 EDT 2022 % 0.13/0.33 % CPUTime : % 0.19/0.58 ____ _ % 0.19/0.58 ___ / __ \_____(_)___ ________ __________ % 0.19/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.19/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.19/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic % 0.19/0.58 (ePrincess v.1.0) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2015 % 0.19/0.58 (c) Peter Backeman, 2014-2015 % 0.19/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.19/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.19/0.59 Bug reports to peter@backeman.se % 0.19/0.59 % 0.19/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.19/0.59 % 0.19/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.69/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.89/1.03 Prover 0: Preprocessing ... % 3.87/1.53 Prover 0: Constructing countermodel ... % 19.64/5.95 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.12/6.04 Prover 1: Preprocessing ... % 20.52/6.20 Prover 1: Constructing countermodel ... % 29.98/8.55 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 30.31/8.61 Prover 2: Preprocessing ... % 30.67/8.78 Prover 2: Warning: ignoring some quantifiers % 30.67/8.79 Prover 2: Constructing countermodel ... % 36.68/11.56 Prover 0: stopped % 36.99/11.76 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 36.99/11.79 Prover 3: Preprocessing ... % 37.29/11.84 Prover 3: Constructing countermodel ... % 43.33/16.61 Prover 3: proved (4845ms) % 43.42/16.61 Prover 1: stopped % 43.42/16.61 Prover 2: stopped % 43.42/16.61 % 43.42/16.61 No countermodel exists, formula is valid % 43.42/16.61 % SZS status Theorem for theBenchmark % 43.42/16.61 % 43.42/16.61 Generating proof ... found it (size 804) % 81.88/42.90 % 81.88/42.90 % SZS output start Proof for theBenchmark % 81.88/42.90 Assumed formulas after preprocessing and simplification: % 81.88/42.90 | (0) ? [v0] : ? [v1] : ? [v2] : ( ~ (sz10 = sz00) & sdtmndt0(xn, xp) = xr & sdtasdt0(xn, xm) = v2 & sdtpldt0(v0, xp) = v1 & sdtpldt0(xn, xm) = v0 & isPrime0(xp) & doDivides0(xp, v2) & sdtlseqdt0(xp, xn) & aNaturalNumber0(xp) & aNaturalNumber0(xm) & aNaturalNumber0(xn) & aNaturalNumber0(sz10) & aNaturalNumber0(sz00) & ~ isPrime0(sz10) & ~ isPrime0(sz00) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v3 = sz00 | ~ (sdtsldt0(v7, v3) = v8) | ~ (sdtsldt0(v4, v3) = v5) | ~ (sdtasdt0(v6, v4) = v7) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v6) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtasdt0(v6, v5) = v8) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtasdt0(v3, v5) = v7) | ~ (sdtasdt0(v3, v4) = v6) | ~ (sdtpldt0(v6, v7) = v8) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtasdt0(v9, v3) = v10 & sdtasdt0(v5, v3) = v12 & sdtasdt0(v4, v3) = v11 & sdtasdt0(v3, v9) = v8 & sdtpldt0(v11, v12) = v10 & sdtpldt0(v4, v5) = v9)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | v3 = sz00 | ~ (sdtasdt0(v3, v5) = v7) | ~ (sdtasdt0(v3, v4) = v6) | ~ sdtlseqdt0(v4, v5) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v6, v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | v3 = sz00 | ~ (sdtasdt0(v3, v5) = v7) | ~ (sdtasdt0(v3, v4) = v6) | ~ sdtlseqdt0(v4, v5) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v8] : ? [v9] : ( ~ (v9 = v8) & sdtasdt0(v5, v3) = v9 & sdtasdt0(v4, v3) = v8 & sdtlseqdt0(v8, v9))) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | v3 = sz00 | ~ (sdtasdt0(v3, v5) = v7) | ~ (sdtasdt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v8] : ? [v9] : ( ~ (v9 = v8) & sdtasdt0(v5, v3) = v9 & sdtasdt0(v4, v3) = v8)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (sdtpldt0(v3, v5) = v7) | ~ (sdtpldt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v8] : ? [v9] : ( ~ (v9 = v8) & sdtpldt0(v5, v3) = v9 & sdtpldt0(v4, v3) = v8)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtasdt0(v6, v5) = v7) | ~ (sdtasdt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v8] : (sdtasdt0(v4, v5) = v8 & sdtasdt0(v3, v8) = v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v5) = v7) | ~ (sdtpldt0(v3, v4) = v6) | ~ isPrime0(v5) | ~ iLess0(v7, v1) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | doDivides0(v5, v4) | doDivides0(v5, v3) | ? [v8] : (sdtasdt0(v3, v4) = v8 & ~ doDivides0(v5, v8))) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtpldt0(v6, v5) = v7) | ~ (sdtpldt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v8] : (sdtpldt0(v4, v5) = v8 & sdtpldt0(v3, v8) = v7)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v5 | v3 = sz00 | ~ (sdtsldt0(v4, v3) = v5) | ~ (sdtasdt0(v3, v6) = v4) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v6) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v5 | ~ (sdtmndt0(v4, v3) = v5) | ~ (sdtpldt0(v3, v6) = v4) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v6) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v4 | v3 = sz00 | ~ (sdtsldt0(v4, v3) = v5) | ~ (sdtasdt0(v3, v5) = v6) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v4 | ~ (sdtmndt0(v4, v3) = v5) | ~ (sdtpldt0(v3, v5) = v6) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | v3 = sz00 | ~ (sdtasdt0(v3, v5) = v6) | ~ (sdtasdt0(v3, v4) = v6) | ~ sdtlseqdt0(v4, v5) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | v3 = sz00 | ~ (sdtasdt0(v3, v5) = v6) | ~ (sdtasdt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (sdtpldt0(v3, v5) = v6) | ~ (sdtpldt0(v3, v4) = v6) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (sdtsldt0(v6, v5) = v4) | ~ (sdtsldt0(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (sdtmndt0(v6, v5) = v4) | ~ (sdtmndt0(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (sdtasdt0(v6, v5) = v4) | ~ (sdtasdt0(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (sdtpldt0(v6, v5) = v4) | ~ (sdtpldt0(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (sdtpldt0(v3, v5) = v6) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v7] : ? [v8] : ? [v9] : ( ~ (v9 = v6) & ~ (v8 = v7) & sdtpldt0(v5, v4) = v8 & sdtpldt0(v5, v3) = v7 & sdtpldt0(v4, v5) = v9 & sdtlseqdt0(v7, v8) & sdtlseqdt0(v6, v9))) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v3 = sz00 | ~ (sdtsldt0(v4, v3) = v5) | ~ (sdtasdt0(v3, v5) = v6) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | aNaturalNumber0(v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtmndt0(v4, v3) = v5) | ~ (sdtpldt0(v3, v5) = v6) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | aNaturalNumber0(v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ doDivides0(v3, v6) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | doDivides0(v3, v5)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtpldt0(v4, v5) = v6) | ~ doDivides0(v3, v5) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | doDivides0(v3, v6)) & ! [v3] : ! [v4] : ! [v5] : (v3 = sz00 | ~ (sdtasdt0(v4, v3) = v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v4, v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v3, v5) = v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | doDivides0(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v3, v4) = v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtasdt0(v4, v3) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v3, v4) = v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | aNaturalNumber0(v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v3, v5) = v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v3, v4)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtpldt0(v4, v3) = v5) & ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtpldt0(v3, v4) = v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | aNaturalNumber0(v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ doDivides0(v4, v5) | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | doDivides0(v3, v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ sdtlseqdt0(v4, v5) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v5) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v3, v5)) & ! [v3] : ! [v4] : (v4 = v3 | v4 = sz10 | ~ isPrime0(v3) | ~ doDivides0(v4, v3) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtasdt0(sz10, v3) = v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = v3 | ~ (sdtpldt0(sz00, v3) = v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = v3 | ~ sdtlseqdt0(v4, v3) | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = v3 | ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | iLess0(v3, v4)) & ! [v3] : ! [v4] : (v4 = sz00 | v3 = sz00 | ~ (sdtasdt0(v3, v4) = sz00) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = sz00 | ~ (sdtasdt0(sz00, v3) = v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = sz00 | ~ (sdtpldt0(v3, v4) = sz00) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : (v4 = sz00 | ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v3, v4)) & ! [v3] : ! [v4] : (v3 = sz00 | ~ (sdtpldt0(v3, v4) = sz00) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3)) & ! [v3] : ! [v4] : ( ~ (sdtasdt0(sz10, v3) = v4) | ~ aNaturalNumber0(v3) | sdtasdt0(v3, sz10) = v3) & ! [v3] : ! [v4] : ( ~ (sdtasdt0(sz00, v3) = v4) | ~ aNaturalNumber0(v3) | sdtasdt0(v3, sz00) = sz00) & ! [v3] : ! [v4] : ( ~ (sdtpldt0(sz00, v3) = v4) | ~ aNaturalNumber0(v3) | sdtpldt0(v3, sz00) = v3) & ! [v3] : ! [v4] : ( ~ doDivides0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v5] : (sdtasdt0(v3, v5) = v4 & aNaturalNumber0(v5))) & ! [v3] : ! [v4] : ( ~ sdtlseqdt0(v3, v4) | ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | ? [v5] : (sdtpldt0(v3, v5) = v4 & aNaturalNumber0(v5))) & ! [v3] : ! [v4] : ( ~ aNaturalNumber0(v4) | ~ aNaturalNumber0(v3) | sdtlseqdt0(v4, v3) | sdtlseqdt0(v3, v4)) & ! [v3] : (v3 = sz10 | v3 = sz00 | ~ aNaturalNumber0(v3) | isPrime0(v3) | ? [v4] : ( ~ (v4 = v3) & ~ (v4 = sz10) & doDivides0(v4, v3) & aNaturalNumber0(v4))) & ! [v3] : (v3 = sz10 | v3 = sz00 | ~ aNaturalNumber0(v3) | sdtlseqdt0(sz10, v3)) & ! [v3] : (v3 = sz10 | v3 = sz00 | ~ aNaturalNumber0(v3) | ? [v4] : (isPrime0(v4) & doDivides0(v4, v3) & aNaturalNumber0(v4))) & ! [v3] : ( ~ aNaturalNumber0(v3) | sdtlseqdt0(v3, v3)) & (xr = xn | ~ sdtlseqdt0(xr, xn))) % 81.88/42.96 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2 yields: % 81.88/42.96 | (1) ~ (sz10 = sz00) & sdtmndt0(xn, xp) = xr & sdtasdt0(xn, xm) = all_0_0_0 & sdtpldt0(all_0_2_2, xp) = all_0_1_1 & sdtpldt0(xn, xm) = all_0_2_2 & isPrime0(xp) & doDivides0(xp, all_0_0_0) & sdtlseqdt0(xp, xn) & aNaturalNumber0(xp) & aNaturalNumber0(xm) & aNaturalNumber0(xn) & aNaturalNumber0(sz10) & aNaturalNumber0(sz00) & ~ isPrime0(sz10) & ~ isPrime0(sz00) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v0 = sz00 | ~ (sdtsldt0(v4, v0) = v5) | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v3, v1) = v4) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v3, v2) = v5) & ! [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(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(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] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ isPrime0(v2) | ~ iLess0(v4, all_0_1_1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v2, v1) | doDivides0(v2, v0) | ? [v5] : (sdtasdt0(v0, v1) = v5 & ~ doDivides0(v2, v5))) & ! [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] : (v3 = v2 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [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 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ doDivides0(v0, v1) | ~ 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(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(v0, v2) = v3) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = 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(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] : (v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ doDivides0(v0, v3) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ doDivides0(v0, v2) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : (v0 = sz00 | ~ (sdtasdt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v1)) & ! [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(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] : ( ~ doDivides0(v1, v2) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v2)) & ! [v0] : ! [v1] : (v1 = v0 | v1 = sz10 | ~ isPrime0(v0) | ~ doDivides0(v1, v0) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = 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 = v0 | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) & ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aNaturalNumber0(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] : (v1 = sz00 | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) & ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) & ! [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(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, sz00) = v0) & ! [v0] : ! [v1] : ( ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2] : (sdtasdt0(v0, v2) = v1 & aNaturalNumber0(v2))) & ! [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) | isPrime0(v0) | ? [v1] : ( ~ (v1 = v0) & ~ (v1 = sz10) & doDivides0(v1, v0) & aNaturalNumber0(v1))) & ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | sdtlseqdt0(sz10, v0)) & ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (isPrime0(v1) & doDivides0(v1, v0) & aNaturalNumber0(v1))) & ! [v0] : ( ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v0)) & (xr = xn | ~ sdtlseqdt0(xr, xn)) % 81.88/42.97 | % 81.88/42.97 | Applying alpha-rule on (1) yields: % 81.88/42.97 | (2) ! [v0] : ! [v1] : ( ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2] : (sdtpldt0(v0, v2) = v1 & aNaturalNumber0(v2))) % 81.88/42.97 | (3) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (4) sdtpldt0(all_0_2_2, xp) = all_0_1_1 % 81.88/42.98 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ doDivides0(v0, v2) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v3)) % 81.88/42.98 | (6) ! [v0] : ! [v1] : (v1 = v0 | v1 = sz10 | ~ isPrime0(v0) | ~ doDivides0(v1, v0) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (7) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (8) ! [v0] : ! [v1] : (v1 = sz00 | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) % 81.88/42.98 | (9) doDivides0(xp, all_0_0_0) % 81.88/42.98 | (10) aNaturalNumber0(sz10) % 81.88/42.98 | (11) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v1, v0) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (12) ~ isPrime0(sz00) % 81.88/42.98 | (13) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v2) = v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v1)) % 81.88/42.98 | (14) ! [v0] : ( ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v0)) % 81.88/42.98 | (15) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (16) aNaturalNumber0(xm) % 81.88/42.98 | (17) aNaturalNumber0(xp) % 81.88/42.98 | (18) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz00) = sz00) % 81.88/42.98 | (19) aNaturalNumber0(sz00) % 81.88/42.98 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) % 81.88/42.98 | (21) ! [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))) % 81.88/42.98 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (23) ! [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)) % 81.88/42.98 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 81.88/42.98 | (25) ~ (sz10 = sz00) % 81.88/42.98 | (26) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v0, sz00) = v0) % 81.88/42.98 | (27) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (28) sdtpldt0(xn, xm) = all_0_2_2 % 81.88/42.98 | (29) ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | ? [v1] : (isPrime0(v1) & doDivides0(v1, v0) & aNaturalNumber0(v1))) % 81.88/42.98 | (30) xr = xn | ~ sdtlseqdt0(xr, xn) % 81.88/42.98 | (31) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (32) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v2) = v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v1)) % 81.88/42.98 | (33) ! [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)) % 81.88/42.98 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ doDivides0(v1, v2) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v2)) % 81.88/42.98 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 81.88/42.98 | (36) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 81.88/42.98 | (37) ~ isPrime0(sz10) % 81.88/42.98 | (38) aNaturalNumber0(xn) % 81.88/42.98 | (39) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v0, sz10) = v0) % 81.88/42.98 | (40) ! [v0] : ! [v1] : (v1 = v0 | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | iLess0(v0, v1)) % 81.88/42.98 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v3) | ~ (sdtpldt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.98 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 81.88/42.99 | (43) ! [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)) % 81.88/42.99 | (44) ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | sdtlseqdt0(sz10, v0)) % 81.88/42.99 | (45) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 81.88/42.99 | (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)) % 81.88/42.99 | (47) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aNaturalNumber0(v0)) % 81.88/42.99 | (48) ! [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)) % 81.88/42.99 | (49) ! [v0] : (v0 = sz10 | v0 = sz00 | ~ aNaturalNumber0(v0) | isPrime0(v0) | ? [v1] : ( ~ (v1 = v0) & ~ (v1 = sz10) & doDivides0(v1, v0) & aNaturalNumber0(v1))) % 82.26/42.99 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | aNaturalNumber0(v2)) % 82.26/42.99 | (51) sdtlseqdt0(xp, xn) % 82.26/42.99 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 82.26/42.99 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ isPrime0(v2) | ~ iLess0(v4, all_0_1_1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v2, v1) | doDivides0(v2, v0) | ? [v5] : (sdtasdt0(v0, v1) = v5 & ~ doDivides0(v2, v5))) % 82.26/42.99 | (54) ! [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)) % 82.26/42.99 | (55) ! [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))) % 82.26/42.99 | (56) sdtmndt0(xn, xp) = xr % 82.26/42.99 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ doDivides0(v0, v3) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | doDivides0(v0, v2)) % 82.26/42.99 | (58) ! [v0] : ! [v1] : ( ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | ? [v2] : (sdtasdt0(v0, v2) = v1 & aNaturalNumber0(v2))) % 82.26/42.99 | (59) ! [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)) % 82.26/42.99 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 82.26/42.99 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtasdt0(v0, v1) = v3) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 82.26/42.99 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v0 = sz00 | ~ (sdtsldt0(v4, v0) = v5) | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v3, v1) = v4) | ~ doDivides0(v0, v1) | ~ aNaturalNumber0(v3) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v3, v2) = v5) % 82.26/42.99 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 82.26/42.99 | (64) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtlseqdt0(v1, v2) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v0, v2)) % 82.26/42.99 | (65) ! [v0] : ! [v1] : ( ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v1, v0) | sdtlseqdt0(v0, v1)) % 82.26/42.99 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ~ sdtlseqdt0(v0, v1) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0)) % 82.26/42.99 | (67) ! [v0] : ! [v1] : ! [v2] : (v0 = sz00 | ~ (sdtasdt0(v1, v0) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtlseqdt0(v1, v2)) % 82.26/42.99 | (68) isPrime0(xp) % 82.26/42.99 | (69) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtpldt0(v1, v0) = v2) % 82.26/43.00 | (70) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aNaturalNumber0(v1) | ~ aNaturalNumber0(v0) | sdtasdt0(v1, v0) = v2) % 82.26/43.00 | (71) sdtasdt0(xn, xm) = all_0_0_0 % 82.26/43.00 | % 82.26/43.00 | Using (68) and (37) yields: % 82.26/43.00 | (72) ~ (xp = sz10) % 82.26/43.00 | % 82.26/43.00 | Using (68) and (12) yields: % 82.26/43.00 | (73) ~ (xp = sz00) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (58) with xp, xp and discharging atoms aNaturalNumber0(xp), yields: % 82.26/43.00 | (74) ~ doDivides0(xp, xp) | ? [v0] : (sdtasdt0(xp, v0) = xp & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (2) with xn, xn and discharging atoms aNaturalNumber0(xn), yields: % 82.26/43.00 | (75) ~ sdtlseqdt0(xn, xn) | ? [v0] : (sdtpldt0(xn, v0) = xn & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (65) with xp, xp and discharging atoms aNaturalNumber0(xp), yields: % 82.26/43.00 | (76) sdtlseqdt0(xp, xp) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (44) with xp and discharging atoms aNaturalNumber0(xp), yields: % 82.26/43.00 | (77) xp = sz10 | xp = sz00 | sdtlseqdt0(sz10, xp) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (29) with xp and discharging atoms aNaturalNumber0(xp), yields: % 82.26/43.00 | (78) xp = sz10 | xp = sz00 | ? [v0] : (isPrime0(v0) & doDivides0(v0, xp) & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (70) with all_0_0_0, xm, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.00 | (79) sdtasdt0(xm, xn) = all_0_0_0 % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (45) with all_0_0_0, xm, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.00 | (80) aNaturalNumber0(all_0_0_0) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (69) with all_0_2_2, xm, xn and discharging atoms sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.00 | (81) sdtpldt0(xm, xn) = all_0_2_2 % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (36) with all_0_2_2, xm, xn and discharging atoms sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.00 | (82) aNaturalNumber0(all_0_2_2) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (2) with xn, xp and discharging atoms sdtlseqdt0(xp, xn), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.00 | (83) ? [v0] : (sdtpldt0(xp, v0) = xn & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (65) with xm, xm and discharging atoms aNaturalNumber0(xm), yields: % 82.26/43.00 | (84) sdtlseqdt0(xm, xm) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (54) with all_0_1_1, all_0_2_2, xp, xm, xn and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.00 | (85) ? [v0] : (sdtpldt0(xm, xp) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (65) with xn, xn and discharging atoms aNaturalNumber0(xn), yields: % 82.26/43.00 | (86) sdtlseqdt0(xn, xn) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (65) with sz00, xm and discharging atoms aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.26/43.00 | (87) sdtlseqdt0(xm, sz00) | sdtlseqdt0(sz00, xm) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (65) with sz00, sz00 and discharging atoms aNaturalNumber0(sz00), yields: % 82.26/43.00 | (88) sdtlseqdt0(sz00, sz00) % 82.26/43.00 | % 82.26/43.00 | Instantiating (83) with all_13_0_3 yields: % 82.26/43.00 | (89) sdtpldt0(xp, all_13_0_3) = xn & aNaturalNumber0(all_13_0_3) % 82.26/43.00 | % 82.26/43.00 | Applying alpha-rule on (89) yields: % 82.26/43.00 | (90) sdtpldt0(xp, all_13_0_3) = xn % 82.26/43.00 | (91) aNaturalNumber0(all_13_0_3) % 82.26/43.00 | % 82.26/43.00 | Instantiating (85) with all_15_0_4 yields: % 82.26/43.00 | (92) sdtpldt0(xm, xp) = all_15_0_4 & sdtpldt0(xn, all_15_0_4) = all_0_1_1 % 82.26/43.00 | % 82.26/43.00 | Applying alpha-rule on (92) yields: % 82.26/43.00 | (93) sdtpldt0(xm, xp) = all_15_0_4 % 82.26/43.00 | (94) sdtpldt0(xn, all_15_0_4) = all_0_1_1 % 82.26/43.00 | % 82.26/43.00 +-Applying beta-rule and splitting (77), into two cases. % 82.26/43.00 |-Branch one: % 82.26/43.00 | (95) sdtlseqdt0(sz10, xp) % 82.26/43.00 | % 82.26/43.00 +-Applying beta-rule and splitting (75), into two cases. % 82.26/43.00 |-Branch one: % 82.26/43.00 | (96) ~ sdtlseqdt0(xn, xn) % 82.26/43.00 | % 82.26/43.00 | Using (86) and (96) yields: % 82.26/43.00 | (97) $false % 82.26/43.00 | % 82.26/43.00 |-The branch is then unsatisfiable % 82.26/43.00 |-Branch two: % 82.26/43.00 | (86) sdtlseqdt0(xn, xn) % 82.26/43.00 | (99) ? [v0] : (sdtpldt0(xn, v0) = xn & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating (99) with all_25_0_5 yields: % 82.26/43.00 | (100) sdtpldt0(xn, all_25_0_5) = xn & aNaturalNumber0(all_25_0_5) % 82.26/43.00 | % 82.26/43.00 | Applying alpha-rule on (100) yields: % 82.26/43.00 | (101) sdtpldt0(xn, all_25_0_5) = xn % 82.26/43.00 | (102) aNaturalNumber0(all_25_0_5) % 82.26/43.00 | % 82.26/43.00 +-Applying beta-rule and splitting (78), into two cases. % 82.26/43.00 |-Branch one: % 82.26/43.00 | (103) xp = sz00 % 82.26/43.00 | % 82.26/43.00 | Equations (103) can reduce 73 to: % 82.26/43.00 | (104) $false % 82.26/43.00 | % 82.26/43.00 |-The branch is then unsatisfiable % 82.26/43.00 |-Branch two: % 82.26/43.00 | (73) ~ (xp = sz00) % 82.26/43.00 | (106) xp = sz10 | ? [v0] : (isPrime0(v0) & doDivides0(v0, xp) & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 +-Applying beta-rule and splitting (106), into two cases. % 82.26/43.00 |-Branch one: % 82.26/43.00 | (107) xp = sz10 % 82.26/43.00 | % 82.26/43.00 | Equations (107) can reduce 72 to: % 82.26/43.00 | (104) $false % 82.26/43.00 | % 82.26/43.00 |-The branch is then unsatisfiable % 82.26/43.00 |-Branch two: % 82.26/43.00 | (72) ~ (xp = sz10) % 82.26/43.00 | (110) ? [v0] : (isPrime0(v0) & doDivides0(v0, xp) & aNaturalNumber0(v0)) % 82.26/43.00 | % 82.26/43.00 | Instantiating (110) with all_34_0_6 yields: % 82.26/43.00 | (111) isPrime0(all_34_0_6) & doDivides0(all_34_0_6, xp) & aNaturalNumber0(all_34_0_6) % 82.26/43.00 | % 82.26/43.00 | Applying alpha-rule on (111) yields: % 82.26/43.00 | (112) isPrime0(all_34_0_6) % 82.26/43.00 | (113) doDivides0(all_34_0_6, xp) % 82.26/43.00 | (114) aNaturalNumber0(all_34_0_6) % 82.26/43.00 | % 82.26/43.00 | Instantiating formula (31) with xp, xm and discharging atoms aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.00 | (115) xp = sz00 | ~ (sdtpldt0(xm, xp) = sz00) % 82.26/43.01 | % 82.26/43.01 | Using (112) and (37) yields: % 82.26/43.01 | (116) ~ (all_34_0_6 = sz10) % 82.26/43.01 | % 82.26/43.01 | Using (112) and (12) yields: % 82.26/43.01 | (117) ~ (all_34_0_6 = sz00) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (52) with all_13_0_3, xr, xn, xp and discharging atoms sdtmndt0(xn, xp) = xr, sdtpldt0(xp, all_13_0_3) = xn, sdtlseqdt0(xp, xn), aNaturalNumber0(all_13_0_3), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.01 | (118) all_13_0_3 = xr % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (6) with all_34_0_6, xp and discharging atoms isPrime0(xp), doDivides0(all_34_0_6, xp), aNaturalNumber0(all_34_0_6), aNaturalNumber0(xp), yields: % 82.26/43.01 | (119) all_34_0_6 = xp | all_34_0_6 = sz10 % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (7) with all_13_0_3, xp and discharging atoms aNaturalNumber0(all_13_0_3), aNaturalNumber0(xp), yields: % 82.26/43.01 | (120) xp = sz00 | ~ (sdtpldt0(xp, all_13_0_3) = sz00) % 82.26/43.01 | % 82.26/43.01 | From (118) and (90) follows: % 82.26/43.01 | (121) sdtpldt0(xp, xr) = xn % 82.26/43.01 | % 82.26/43.01 | From (118) and (91) follows: % 82.26/43.01 | (122) aNaturalNumber0(xr) % 82.26/43.01 | % 82.26/43.01 +-Applying beta-rule and splitting (120), into two cases. % 82.26/43.01 |-Branch one: % 82.26/43.01 | (123) ~ (sdtpldt0(xp, all_13_0_3) = sz00) % 82.26/43.01 | % 82.26/43.01 | From (118) and (123) follows: % 82.26/43.01 | (124) ~ (sdtpldt0(xp, xr) = sz00) % 82.26/43.01 | % 82.26/43.01 +-Applying beta-rule and splitting (119), into two cases. % 82.26/43.01 |-Branch one: % 82.26/43.01 | (125) all_34_0_6 = xp % 82.26/43.01 | % 82.26/43.01 | Equations (125) can reduce 117 to: % 82.26/43.01 | (73) ~ (xp = sz00) % 82.26/43.01 | % 82.26/43.01 | From (125) and (113) follows: % 82.26/43.01 | (127) doDivides0(xp, xp) % 82.26/43.01 | % 82.26/43.01 | From (125) and (114) follows: % 82.26/43.01 | (17) aNaturalNumber0(xp) % 82.26/43.01 | % 82.26/43.01 +-Applying beta-rule and splitting (74), into two cases. % 82.26/43.01 |-Branch one: % 82.26/43.01 | (129) ~ doDivides0(xp, xp) % 82.26/43.01 | % 82.26/43.01 | Using (127) and (129) yields: % 82.26/43.01 | (97) $false % 82.26/43.01 | % 82.26/43.01 |-The branch is then unsatisfiable % 82.26/43.01 |-Branch two: % 82.26/43.01 | (127) doDivides0(xp, xp) % 82.26/43.01 | (132) ? [v0] : (sdtasdt0(xp, v0) = xp & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating (132) with all_59_0_7 yields: % 82.26/43.01 | (133) sdtasdt0(xp, all_59_0_7) = xp & aNaturalNumber0(all_59_0_7) % 82.26/43.01 | % 82.26/43.01 | Applying alpha-rule on (133) yields: % 82.26/43.01 | (134) sdtasdt0(xp, all_59_0_7) = xp % 82.26/43.01 | (135) aNaturalNumber0(all_59_0_7) % 82.26/43.01 | % 82.26/43.01 +-Applying beta-rule and splitting (115), into two cases. % 82.26/43.01 |-Branch one: % 82.26/43.01 | (136) ~ (sdtpldt0(xm, xp) = sz00) % 82.26/43.01 | % 82.26/43.01 | Using (121) and (124) yields: % 82.26/43.01 | (137) ~ (xn = sz00) % 82.26/43.01 | % 82.26/43.01 | Using (93) and (136) yields: % 82.26/43.01 | (138) ~ (all_15_0_4 = sz00) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (54) with xm, xm, xp, xp, xm and discharging atoms aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.01 | (139) ~ (sdtpldt0(xm, xp) = xm) | ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xm, v0) = xm) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (69) with all_15_0_4, xp, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.01 | (140) sdtpldt0(xp, xm) = all_15_0_4 % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (36) with all_15_0_4, xp, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.01 | (141) aNaturalNumber0(all_15_0_4) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (54) with all_0_1_1, all_0_2_2, xp, xn, xm and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, sdtpldt0(xm, xn) = all_0_2_2, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.01 | (142) ? [v0] : (sdtpldt0(xm, v0) = all_0_1_1 & sdtpldt0(xn, xp) = v0) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (54) with all_0_2_2, xn, xm, xp, xn and discharging atoms sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.01 | (143) ~ (sdtpldt0(xn, xp) = xn) | ? [v0] : (sdtpldt0(xp, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (2) with xp, xp and discharging atoms sdtlseqdt0(xp, xp), aNaturalNumber0(xp), yields: % 82.26/43.01 | (144) ? [v0] : (sdtpldt0(xp, v0) = xp & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (2) with xm, xm and discharging atoms sdtlseqdt0(xm, xm), aNaturalNumber0(xm), yields: % 82.26/43.01 | (145) ? [v0] : (sdtpldt0(xm, v0) = xm & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (2) with sz00, sz00 and discharging atoms sdtlseqdt0(sz00, sz00), aNaturalNumber0(sz00), yields: % 82.26/43.01 | (146) ? [v0] : (sdtpldt0(sz00, v0) = sz00 & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (64) with xn, xp, sz10 and discharging atoms sdtlseqdt0(xp, xn), sdtlseqdt0(sz10, xp), aNaturalNumber0(xp), aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 82.26/43.01 | (147) sdtlseqdt0(sz10, xn) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (2) with xp, sz10 and discharging atoms sdtlseqdt0(sz10, xp), aNaturalNumber0(xp), aNaturalNumber0(sz10), yields: % 82.26/43.01 | (148) ? [v0] : (sdtpldt0(sz10, v0) = xp & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (2) with xn, sz10 and discharging atoms aNaturalNumber0(xn), aNaturalNumber0(sz10), yields: % 82.26/43.01 | (149) ~ sdtlseqdt0(sz10, xn) | ? [v0] : (sdtpldt0(sz10, v0) = xn & aNaturalNumber0(v0)) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (13) with xm, all_0_0_0, xn and discharging atoms sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(all_0_0_0), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.01 | (150) doDivides0(xn, all_0_0_0) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (70) with xp, all_59_0_7, xp and discharging atoms sdtasdt0(xp, all_59_0_7) = xp, aNaturalNumber0(all_59_0_7), aNaturalNumber0(xp), yields: % 82.26/43.01 | (151) sdtasdt0(all_59_0_7, xp) = xp % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (13) with xn, all_0_0_0, xm and discharging atoms sdtasdt0(xm, xn) = all_0_0_0, aNaturalNumber0(all_0_0_0), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.01 | (152) doDivides0(xm, all_0_0_0) % 82.26/43.01 | % 82.26/43.01 | Instantiating formula (36) with all_0_1_1, xp, all_0_2_2 and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, aNaturalNumber0(all_0_2_2), aNaturalNumber0(xp), yields: % 82.26/43.01 | (153) aNaturalNumber0(all_0_1_1) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with all_0_2_2, xn, xm, xr, xp and discharging atoms sdtpldt0(xp, xr) = xn, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xr), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.02 | (154) ? [v0] : (sdtpldt0(xr, xm) = v0 & sdtpldt0(xp, v0) = all_0_2_2) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with all_0_2_2, xn, xm, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.02 | (155) ? [v0] : (sdtpldt0(all_25_0_5, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (32) with xm, all_0_2_2, xn and discharging atoms sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(all_0_2_2), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.02 | (156) sdtlseqdt0(xn, all_0_2_2) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (69) with xn, xr, xp and discharging atoms sdtpldt0(xp, xr) = xn, aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.02 | (157) sdtpldt0(xr, xp) = xn % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (32) with xp, all_15_0_4, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.02 | (158) ~ aNaturalNumber0(all_15_0_4) | sdtlseqdt0(xm, all_15_0_4) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (69) with xn, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.02 | (159) sdtpldt0(all_25_0_5, xn) = xn % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (69) with all_0_1_1, all_15_0_4, xn and discharging atoms sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(xn), yields: % 82.26/43.02 | (160) ~ aNaturalNumber0(all_15_0_4) | sdtpldt0(all_15_0_4, xn) = all_0_1_1 % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with xn, xn, xp, xp, xn and discharging atoms aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.02 | (161) ~ (sdtpldt0(xn, xp) = xn) | ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with xn, xn, all_25_0_5, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.02 | (162) ? [v0] : (sdtpldt0(all_25_0_5, all_25_0_5) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with xn, xn, all_25_0_5, xr, xp and discharging atoms sdtpldt0(xp, xr) = xn, sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.02 | (163) ? [v0] : (sdtpldt0(xr, all_25_0_5) = v0 & sdtpldt0(xp, v0) = xn) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with all_0_1_1, xn, all_15_0_4, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.02 | (164) ~ aNaturalNumber0(all_15_0_4) | ? [v0] : (sdtpldt0(all_25_0_5, all_15_0_4) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (65) with all_25_0_5, all_25_0_5 and discharging atoms aNaturalNumber0(all_25_0_5), yields: % 82.26/43.02 | (165) sdtlseqdt0(all_25_0_5, all_25_0_5) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (58) with all_0_0_0, xm and discharging atoms aNaturalNumber0(all_0_0_0), aNaturalNumber0(xm), yields: % 82.26/43.02 | (166) ~ doDivides0(xm, all_0_0_0) | ? [v0] : (sdtasdt0(xm, v0) = all_0_0_0 & aNaturalNumber0(v0)) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (58) with all_0_0_0, xn and discharging atoms aNaturalNumber0(all_0_0_0), aNaturalNumber0(xn), yields: % 82.26/43.02 | (167) ~ doDivides0(xn, all_0_0_0) | ? [v0] : (sdtasdt0(xn, v0) = all_0_0_0 & aNaturalNumber0(v0)) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with all_0_2_2, all_0_2_2, xp, xp, all_0_2_2 and discharging atoms aNaturalNumber0(all_0_2_2), aNaturalNumber0(xp), yields: % 82.26/43.02 | (168) ~ (sdtpldt0(all_0_2_2, xp) = all_0_2_2) | ? [v0] : (sdtpldt0(all_0_2_2, v0) = all_0_2_2 & sdtpldt0(xp, xp) = v0) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (32) with xp, all_0_1_1, all_0_2_2 and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, aNaturalNumber0(all_0_2_2), aNaturalNumber0(xp), yields: % 82.26/43.02 | (169) ~ aNaturalNumber0(all_0_1_1) | sdtlseqdt0(all_0_2_2, all_0_1_1) % 82.26/43.02 | % 82.26/43.02 | Instantiating formula (54) with all_0_1_1, xn, all_15_0_4, xr, xp and discharging atoms sdtpldt0(xp, xr) = xn, sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.02 | (170) ~ aNaturalNumber0(all_15_0_4) | ? [v0] : (sdtpldt0(xr, all_15_0_4) = v0 & sdtpldt0(xp, v0) = all_0_1_1) % 82.26/43.02 | % 82.26/43.02 | Instantiating (163) with all_89_0_9 yields: % 82.26/43.02 | (171) sdtpldt0(xr, all_25_0_5) = all_89_0_9 & sdtpldt0(xp, all_89_0_9) = xn % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (171) yields: % 82.26/43.02 | (172) sdtpldt0(xr, all_25_0_5) = all_89_0_9 % 82.26/43.02 | (173) sdtpldt0(xp, all_89_0_9) = xn % 82.26/43.02 | % 82.26/43.02 | Instantiating (162) with all_91_0_10 yields: % 82.26/43.02 | (174) sdtpldt0(all_25_0_5, all_25_0_5) = all_91_0_10 & sdtpldt0(xn, all_91_0_10) = xn % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (174) yields: % 82.26/43.02 | (175) sdtpldt0(all_25_0_5, all_25_0_5) = all_91_0_10 % 82.26/43.02 | (176) sdtpldt0(xn, all_91_0_10) = xn % 82.26/43.02 | % 82.26/43.02 | Instantiating (146) with all_93_0_11 yields: % 82.26/43.02 | (177) sdtpldt0(sz00, all_93_0_11) = sz00 & aNaturalNumber0(all_93_0_11) % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (177) yields: % 82.26/43.02 | (178) sdtpldt0(sz00, all_93_0_11) = sz00 % 82.26/43.02 | (179) aNaturalNumber0(all_93_0_11) % 82.26/43.02 | % 82.26/43.02 | Instantiating (142) with all_97_0_13 yields: % 82.26/43.02 | (180) sdtpldt0(xm, all_97_0_13) = all_0_1_1 & sdtpldt0(xn, xp) = all_97_0_13 % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (180) yields: % 82.26/43.02 | (181) sdtpldt0(xm, all_97_0_13) = all_0_1_1 % 82.26/43.02 | (182) sdtpldt0(xn, xp) = all_97_0_13 % 82.26/43.02 | % 82.26/43.02 | Instantiating (154) with all_101_0_15 yields: % 82.26/43.02 | (183) sdtpldt0(xr, xm) = all_101_0_15 & sdtpldt0(xp, all_101_0_15) = all_0_2_2 % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (183) yields: % 82.26/43.02 | (184) sdtpldt0(xr, xm) = all_101_0_15 % 82.26/43.02 | (185) sdtpldt0(xp, all_101_0_15) = all_0_2_2 % 82.26/43.02 | % 82.26/43.02 | Instantiating (155) with all_103_0_16 yields: % 82.26/43.02 | (186) sdtpldt0(all_25_0_5, xm) = all_103_0_16 & sdtpldt0(xn, all_103_0_16) = all_0_2_2 % 82.26/43.02 | % 82.26/43.02 | Applying alpha-rule on (186) yields: % 82.26/43.02 | (187) sdtpldt0(all_25_0_5, xm) = all_103_0_16 % 82.26/43.02 | (188) sdtpldt0(xn, all_103_0_16) = all_0_2_2 % 82.26/43.02 | % 82.26/43.02 | Instantiating (148) with all_105_0_17 yields: % 82.26/43.02 | (189) sdtpldt0(sz10, all_105_0_17) = xp & aNaturalNumber0(all_105_0_17) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (189) yields: % 82.26/43.03 | (190) sdtpldt0(sz10, all_105_0_17) = xp % 82.26/43.03 | (191) aNaturalNumber0(all_105_0_17) % 82.26/43.03 | % 82.26/43.03 | Instantiating (145) with all_107_0_18 yields: % 82.26/43.03 | (192) sdtpldt0(xm, all_107_0_18) = xm & aNaturalNumber0(all_107_0_18) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (192) yields: % 82.26/43.03 | (193) sdtpldt0(xm, all_107_0_18) = xm % 82.26/43.03 | (194) aNaturalNumber0(all_107_0_18) % 82.26/43.03 | % 82.26/43.03 | Instantiating (144) with all_109_0_19 yields: % 82.26/43.03 | (195) sdtpldt0(xp, all_109_0_19) = xp & aNaturalNumber0(all_109_0_19) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (195) yields: % 82.26/43.03 | (196) sdtpldt0(xp, all_109_0_19) = xp % 82.26/43.03 | (197) aNaturalNumber0(all_109_0_19) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (158), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (198) ~ aNaturalNumber0(all_15_0_4) % 82.26/43.03 | % 82.26/43.03 | Using (141) and (198) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (141) aNaturalNumber0(all_15_0_4) % 82.26/43.03 | (201) sdtlseqdt0(xm, all_15_0_4) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (164), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (198) ~ aNaturalNumber0(all_15_0_4) % 82.26/43.03 | % 82.26/43.03 | Using (141) and (198) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (141) aNaturalNumber0(all_15_0_4) % 82.26/43.03 | (205) ? [v0] : (sdtpldt0(all_25_0_5, all_15_0_4) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.03 | % 82.26/43.03 | Instantiating (205) with all_122_0_20 yields: % 82.26/43.03 | (206) sdtpldt0(all_25_0_5, all_15_0_4) = all_122_0_20 & sdtpldt0(xn, all_122_0_20) = all_0_1_1 % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (206) yields: % 82.26/43.03 | (207) sdtpldt0(all_25_0_5, all_15_0_4) = all_122_0_20 % 82.26/43.03 | (208) sdtpldt0(xn, all_122_0_20) = all_0_1_1 % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (149), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (209) ~ sdtlseqdt0(sz10, xn) % 82.26/43.03 | % 82.26/43.03 | Using (147) and (209) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (147) sdtlseqdt0(sz10, xn) % 82.26/43.03 | (212) ? [v0] : (sdtpldt0(sz10, v0) = xn & aNaturalNumber0(v0)) % 82.26/43.03 | % 82.26/43.03 | Instantiating (212) with all_127_0_21 yields: % 82.26/43.03 | (213) sdtpldt0(sz10, all_127_0_21) = xn & aNaturalNumber0(all_127_0_21) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (213) yields: % 82.26/43.03 | (214) sdtpldt0(sz10, all_127_0_21) = xn % 82.26/43.03 | (215) aNaturalNumber0(all_127_0_21) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (167), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (216) ~ doDivides0(xn, all_0_0_0) % 82.26/43.03 | % 82.26/43.03 | Using (150) and (216) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (150) doDivides0(xn, all_0_0_0) % 82.26/43.03 | (219) ? [v0] : (sdtasdt0(xn, v0) = all_0_0_0 & aNaturalNumber0(v0)) % 82.26/43.03 | % 82.26/43.03 | Instantiating (219) with all_132_0_22 yields: % 82.26/43.03 | (220) sdtasdt0(xn, all_132_0_22) = all_0_0_0 & aNaturalNumber0(all_132_0_22) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (220) yields: % 82.26/43.03 | (221) sdtasdt0(xn, all_132_0_22) = all_0_0_0 % 82.26/43.03 | (222) aNaturalNumber0(all_132_0_22) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (166), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (223) ~ doDivides0(xm, all_0_0_0) % 82.26/43.03 | % 82.26/43.03 | Using (152) and (223) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (152) doDivides0(xm, all_0_0_0) % 82.26/43.03 | (226) ? [v0] : (sdtasdt0(xm, v0) = all_0_0_0 & aNaturalNumber0(v0)) % 82.26/43.03 | % 82.26/43.03 | Instantiating (226) with all_137_0_23 yields: % 82.26/43.03 | (227) sdtasdt0(xm, all_137_0_23) = all_0_0_0 & aNaturalNumber0(all_137_0_23) % 82.26/43.03 | % 82.26/43.03 | Applying alpha-rule on (227) yields: % 82.26/43.03 | (228) sdtasdt0(xm, all_137_0_23) = all_0_0_0 % 82.26/43.03 | (229) aNaturalNumber0(all_137_0_23) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (170), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (198) ~ aNaturalNumber0(all_15_0_4) % 82.26/43.03 | % 82.26/43.03 | Using (141) and (198) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (141) aNaturalNumber0(all_15_0_4) % 82.26/43.03 | (233) ? [v0] : (sdtpldt0(xr, all_15_0_4) = v0 & sdtpldt0(xp, v0) = all_0_1_1) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (169), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (234) ~ aNaturalNumber0(all_0_1_1) % 82.26/43.03 | % 82.26/43.03 | Using (153) and (234) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (153) aNaturalNumber0(all_0_1_1) % 82.26/43.03 | (237) sdtlseqdt0(all_0_2_2, all_0_1_1) % 82.26/43.03 | % 82.26/43.03 +-Applying beta-rule and splitting (160), into two cases. % 82.26/43.03 |-Branch one: % 82.26/43.03 | (198) ~ aNaturalNumber0(all_15_0_4) % 82.26/43.03 | % 82.26/43.03 | Using (141) and (198) yields: % 82.26/43.03 | (97) $false % 82.26/43.03 | % 82.26/43.03 |-The branch is then unsatisfiable % 82.26/43.03 |-Branch two: % 82.26/43.03 | (141) aNaturalNumber0(all_15_0_4) % 82.26/43.03 | (241) sdtpldt0(all_15_0_4, xn) = all_0_1_1 % 82.26/43.03 | % 82.26/43.03 | Instantiating formula (24) with xm, xn, all_0_1_1, all_0_2_2 and discharging atoms sdtpldt0(xm, xn) = all_0_2_2, yields: % 82.26/43.03 | (242) all_0_1_1 = all_0_2_2 | ~ (sdtpldt0(xm, xn) = all_0_1_1) % 82.26/43.03 | % 82.26/43.03 | Instantiating formula (41) with xn, all_25_0_5, xp, xr and discharging atoms sdtpldt0(xr, xp) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.03 | (243) all_25_0_5 = xp | ~ (sdtpldt0(xr, all_25_0_5) = xn) % 82.26/43.03 | % 82.26/43.03 | Instantiating formula (24) with xr, xp, xn, all_89_0_9 and discharging atoms sdtpldt0(xr, xp) = xn, yields: % 82.26/43.03 | (244) all_89_0_9 = xn | ~ (sdtpldt0(xr, xp) = all_89_0_9) % 82.26/43.03 | % 82.26/43.03 | Instantiating formula (24) with xm, xp, xm, all_15_0_4 and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, yields: % 82.26/43.03 | (245) all_15_0_4 = xm | ~ (sdtpldt0(xm, xp) = xm) % 82.26/43.03 | % 82.26/43.03 | Instantiating formula (41) with xn, all_25_0_5, sz00, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), aNaturalNumber0(sz00), yields: % 82.26/43.03 | (246) all_25_0_5 = sz00 | ~ (sdtpldt0(xn, sz00) = xn) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (24) with xn, xp, all_97_0_13, xn and discharging atoms sdtpldt0(xn, xp) = all_97_0_13, yields: % 82.26/43.04 | (247) all_97_0_13 = xn | ~ (sdtpldt0(xn, xp) = xn) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (61) with all_0_0_0, xn, all_137_0_23, xm and discharging atoms sdtasdt0(xm, all_137_0_23) = all_0_0_0, sdtasdt0(xm, xn) = all_0_0_0, aNaturalNumber0(all_137_0_23), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.04 | (248) all_137_0_23 = xn | xm = sz00 % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (61) with all_0_0_0, xm, all_132_0_22, xn and discharging atoms sdtasdt0(xn, all_132_0_22) = all_0_0_0, sdtasdt0(xn, xm) = all_0_0_0, aNaturalNumber0(all_132_0_22), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.04 | (249) all_132_0_22 = xm | xn = sz00 % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (41) with xn, all_25_0_5, all_91_0_10, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.04 | (250) all_91_0_10 = all_25_0_5 | ~ aNaturalNumber0(all_91_0_10) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (41) with all_0_2_2, xm, all_103_0_16, xn and discharging atoms sdtpldt0(xn, all_103_0_16) = all_0_2_2, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.04 | (251) all_103_0_16 = xm | ~ aNaturalNumber0(all_103_0_16) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (3) with sz00, all_93_0_11 and discharging atoms sdtpldt0(sz00, all_93_0_11) = sz00, aNaturalNumber0(all_93_0_11), yields: % 82.26/43.04 | (252) all_93_0_11 = sz00 % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (41) with xm, xp, all_107_0_18, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.04 | (253) all_107_0_18 = xp | ~ (sdtpldt0(xm, xp) = xm) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (41) with all_0_1_1, all_15_0_4, all_122_0_20, xn and discharging atoms sdtpldt0(xn, all_122_0_20) = all_0_1_1, sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(all_15_0_4), aNaturalNumber0(xn), yields: % 82.26/43.04 | (254) all_122_0_20 = all_15_0_4 | ~ aNaturalNumber0(all_122_0_20) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (31) with all_15_0_4, all_25_0_5 and discharging atoms aNaturalNumber0(all_25_0_5), aNaturalNumber0(all_15_0_4), yields: % 82.26/43.04 | (255) all_15_0_4 = sz00 | ~ (sdtpldt0(all_25_0_5, all_15_0_4) = sz00) % 82.26/43.04 | % 82.26/43.04 | From (252) and (179) follows: % 82.26/43.04 | (19) aNaturalNumber0(sz00) % 82.26/43.04 | % 82.26/43.04 +-Applying beta-rule and splitting (249), into two cases. % 82.26/43.04 |-Branch one: % 82.26/43.04 | (257) xn = sz00 % 82.26/43.04 | % 82.26/43.04 | Equations (257) can reduce 137 to: % 82.26/43.04 | (104) $false % 82.26/43.04 | % 82.26/43.04 |-The branch is then unsatisfiable % 82.26/43.04 |-Branch two: % 82.26/43.04 | (137) ~ (xn = sz00) % 82.26/43.04 | (260) all_132_0_22 = xm % 82.26/43.04 | % 82.26/43.04 | From (260) and (222) follows: % 82.26/43.04 | (16) aNaturalNumber0(xm) % 82.26/43.04 | % 82.26/43.04 +-Applying beta-rule and splitting (255), into two cases. % 82.26/43.04 |-Branch one: % 82.26/43.04 | (262) ~ (sdtpldt0(all_25_0_5, all_15_0_4) = sz00) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (54) with xn, xp, xr, all_25_0_5, all_25_0_5 and discharging atoms sdtpldt0(xp, xr) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), yields: % 82.26/43.04 | (263) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = xp) | ? [v0] : (sdtpldt0(all_25_0_5, v0) = xn & sdtpldt0(all_25_0_5, xr) = v0) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (36) with all_91_0_10, all_25_0_5, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, all_25_0_5) = all_91_0_10, aNaturalNumber0(all_25_0_5), yields: % 82.26/43.04 | (264) aNaturalNumber0(all_91_0_10) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (69) with all_122_0_20, all_15_0_4, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, all_15_0_4) = all_122_0_20, aNaturalNumber0(all_25_0_5), aNaturalNumber0(all_15_0_4), yields: % 82.26/43.04 | (265) sdtpldt0(all_15_0_4, all_25_0_5) = all_122_0_20 % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (36) with all_122_0_20, all_15_0_4, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, all_15_0_4) = all_122_0_20, aNaturalNumber0(all_25_0_5), aNaturalNumber0(all_15_0_4), yields: % 82.26/43.04 | (266) aNaturalNumber0(all_122_0_20) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (54) with all_103_0_16, all_25_0_5, xm, all_25_0_5, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, xm) = all_103_0_16, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), yields: % 82.26/43.04 | (267) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5) | ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_103_0_16 & sdtpldt0(all_25_0_5, xm) = v0) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (69) with all_103_0_16, xm, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, xm) = all_103_0_16, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), yields: % 82.26/43.04 | (268) sdtpldt0(xm, all_25_0_5) = all_103_0_16 % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (36) with all_103_0_16, xm, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, xm) = all_103_0_16, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), yields: % 82.26/43.04 | (269) aNaturalNumber0(all_103_0_16) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (54) with xn, xn, xp, xn, xp and discharging atoms aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.04 | (270) ~ (sdtpldt0(xp, xn) = xn) | ~ (sdtpldt0(xn, xp) = xn) | ? [v0] : (sdtpldt0(xp, v0) = xn & sdtpldt0(xn, xp) = v0) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (36) with all_89_0_9, all_25_0_5, xr and discharging atoms sdtpldt0(xr, all_25_0_5) = all_89_0_9, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), yields: % 82.26/43.04 | (271) aNaturalNumber0(all_89_0_9) % 82.26/43.04 | % 82.26/43.04 | Instantiating formula (54) with xn, xn, all_25_0_5, xp, xr and discharging atoms sdtpldt0(xr, xp) = xn, sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (272) ? [v0] : (sdtpldt0(xr, v0) = xn & sdtpldt0(xp, all_25_0_5) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_0_1_1, xn, all_15_0_4, xp, xr and discharging atoms sdtpldt0(xr, xp) = xn, sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(all_15_0_4), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (273) ? [v0] : (sdtpldt0(xr, v0) = all_0_1_1 & sdtpldt0(xp, all_15_0_4) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (32) with xp, xn, xr and discharging atoms sdtpldt0(xr, xp) = xn, aNaturalNumber0(xr), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.05 | (274) sdtlseqdt0(xr, xn) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (23) with xp, xp, xp, all_59_0_7, all_59_0_7, xp and discharging atoms sdtasdt0(xp, all_59_0_7) = xp, aNaturalNumber0(all_59_0_7), aNaturalNumber0(xp), yields: % 82.26/43.05 | (275) ~ (sdtpldt0(xp, xp) = xp) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v0, xp) = v1 & sdtasdt0(all_59_0_7, xp) = v3 & sdtasdt0(all_59_0_7, xp) = v2 & sdtasdt0(xp, v0) = xp & sdtpldt0(v2, v3) = v1 & sdtpldt0(all_59_0_7, all_59_0_7) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (23) with xp, xp, xp, xp, xp, all_59_0_7 and discharging atoms sdtasdt0(all_59_0_7, xp) = xp, aNaturalNumber0(all_59_0_7), aNaturalNumber0(xp), yields: % 82.26/43.05 | (276) ~ (sdtpldt0(xp, xp) = xp) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v0, all_59_0_7) = v1 & sdtasdt0(all_59_0_7, v0) = xp & sdtasdt0(xp, all_59_0_7) = v3 & sdtasdt0(xp, all_59_0_7) = v2 & sdtpldt0(v2, v3) = v1 & sdtpldt0(xp, xp) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with xn, xp, xr, all_25_0_5, xp and discharging atoms sdtpldt0(xp, xr) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (277) ~ (sdtpldt0(xp, all_25_0_5) = xp) | ? [v0] : (sdtpldt0(all_25_0_5, xr) = v0 & sdtpldt0(xp, v0) = xn) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_15_0_4, xp, xm, all_25_0_5, all_25_0_5 and discharging atoms sdtpldt0(xp, xm) = all_15_0_4, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), yields: % 82.26/43.05 | (278) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = xp) | ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_15_0_4 & sdtpldt0(all_25_0_5, xm) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_15_0_4, xp, xm, all_25_0_5, xp and discharging atoms sdtpldt0(xp, xm) = all_15_0_4, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.05 | (279) ~ (sdtpldt0(xp, all_25_0_5) = xp) | ? [v0] : (sdtpldt0(all_25_0_5, xm) = v0 & sdtpldt0(xp, v0) = all_15_0_4) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_15_0_4, xp, xm, xp, xp and discharging atoms sdtpldt0(xp, xm) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.05 | (280) ~ (sdtpldt0(xp, xp) = xp) | ? [v0] : (sdtpldt0(xp, v0) = all_15_0_4 & sdtpldt0(xp, xm) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_15_0_4, xm, xp, all_25_0_5, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.05 | (281) ~ (sdtpldt0(xm, all_25_0_5) = xm) | ? [v0] : (sdtpldt0(all_25_0_5, xp) = v0 & sdtpldt0(xm, v0) = all_15_0_4) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_15_0_4, xm, xp, xp, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.05 | (282) ~ (sdtpldt0(xm, xp) = xm) | ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xm, v0) = all_15_0_4) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_97_0_13, xn, xp, xr, xp and discharging atoms sdtpldt0(xp, xr) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (283) ? [v0] : (sdtpldt0(xr, xp) = v0 & sdtpldt0(xp, v0) = all_97_0_13) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_97_0_13, xn, xp, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.05 | (284) ? [v0] : (sdtpldt0(all_25_0_5, xp) = v0 & sdtpldt0(xn, v0) = all_97_0_13) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_97_0_13, xn, xp, xn, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, xn) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.05 | (285) ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_97_0_13 & sdtpldt0(xn, xp) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_97_0_13, xn, xp, all_25_0_5, xr and discharging atoms sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (286) ~ (sdtpldt0(xr, all_25_0_5) = xn) | ? [v0] : (sdtpldt0(all_25_0_5, xp) = v0 & sdtpldt0(xr, v0) = all_97_0_13) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_97_0_13, xn, xp, xp, xr and discharging atoms sdtpldt0(xr, xp) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.05 | (287) ? [v0] : (sdtpldt0(xr, v0) = all_97_0_13 & sdtpldt0(xp, xp) = v0) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with xn, xr, xp, xp, xn and discharging atoms sdtpldt0(xr, xp) = xn, aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.05 | (288) ~ (sdtpldt0(xn, xp) = xr) | ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (54) with all_101_0_15, xr, xm, xp, xn and discharging atoms sdtpldt0(xr, xm) = all_101_0_15, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.05 | (289) ~ (sdtpldt0(xn, xp) = xr) | ? [v0] : (sdtpldt0(xp, xm) = v0 & sdtpldt0(xn, v0) = all_101_0_15) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (2) with all_25_0_5, all_25_0_5 and discharging atoms sdtlseqdt0(all_25_0_5, all_25_0_5), aNaturalNumber0(all_25_0_5), yields: % 82.26/43.05 | (290) ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_25_0_5 & aNaturalNumber0(v0)) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (55) with all_15_0_4, xp, sz00, xm and discharging atoms sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.26/43.05 | (291) xm = sz00 | ~ sdtlseqdt0(xm, sz00) | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_15_0_4) & ~ (v1 = v0) & sdtpldt0(xp, xm) = v0 & sdtpldt0(xp, sz00) = v1 & sdtpldt0(sz00, xp) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_15_0_4, v2)) % 82.26/43.05 | % 82.26/43.05 | Instantiating formula (55) with all_0_2_2, xn, sz00, xm and discharging atoms sdtpldt0(xm, xn) = all_0_2_2, aNaturalNumber0(xm), aNaturalNumber0(xn), aNaturalNumber0(sz00), yields: % 82.26/43.06 | (292) xm = sz00 | ~ sdtlseqdt0(xm, sz00) | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_0_2_2) & ~ (v1 = v0) & sdtpldt0(xn, xm) = v0 & sdtpldt0(xn, sz00) = v1 & sdtpldt0(sz00, xn) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_0_2_2, v2)) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (40) with sz00, xm and discharging atoms aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.26/43.06 | (293) xm = sz00 | ~ sdtlseqdt0(xm, sz00) | iLess0(xm, sz00) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (2) with sz00, xm and discharging atoms aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.26/43.06 | (294) ~ sdtlseqdt0(xm, sz00) | ? [v0] : (sdtpldt0(xm, v0) = sz00 & aNaturalNumber0(v0)) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (2) with all_0_2_2, xn and discharging atoms sdtlseqdt0(xn, all_0_2_2), aNaturalNumber0(all_0_2_2), aNaturalNumber0(xn), yields: % 82.26/43.06 | (295) ? [v0] : (sdtpldt0(xn, v0) = all_0_2_2 & aNaturalNumber0(v0)) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_1_1, all_0_2_2, xp, all_103_0_16, xn and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, sdtpldt0(xn, all_103_0_16) = all_0_2_2, aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.06 | (296) ~ aNaturalNumber0(all_103_0_16) | ? [v0] : (sdtpldt0(all_103_0_16, xp) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_15_0_4, xm, xp, all_107_0_18, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, sdtpldt0(xm, xp) = all_15_0_4, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.06 | (297) ? [v0] : (sdtpldt0(all_107_0_18, xp) = v0 & sdtpldt0(xm, v0) = all_15_0_4) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_2_2, xn, xm, all_91_0_10, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.06 | (298) ~ aNaturalNumber0(all_91_0_10) | ? [v0] : (sdtpldt0(all_91_0_10, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_15_0_4, xp, xm, all_109_0_19, xp and discharging atoms sdtpldt0(xp, all_109_0_19) = xp, sdtpldt0(xp, xm) = all_15_0_4, aNaturalNumber0(all_109_0_19), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.06 | (299) ? [v0] : (sdtpldt0(all_109_0_19, xm) = v0 & sdtpldt0(xp, v0) = all_15_0_4) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (69) with xm, all_107_0_18, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xm), yields: % 82.26/43.06 | (300) sdtpldt0(all_107_0_18, xm) = xm % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_1_1, xn, all_122_0_20, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_122_0_20) = all_0_1_1, sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.06 | (301) ~ aNaturalNumber0(all_122_0_20) | ? [v0] : (sdtpldt0(all_25_0_5, all_122_0_20) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (69) with all_0_1_1, all_122_0_20, xn and discharging atoms sdtpldt0(xn, all_122_0_20) = all_0_1_1, aNaturalNumber0(xn), yields: % 82.26/43.06 | (302) ~ aNaturalNumber0(all_122_0_20) | sdtpldt0(all_122_0_20, xn) = all_0_1_1 % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (69) with all_0_2_2, all_103_0_16, xn and discharging atoms sdtpldt0(xn, all_103_0_16) = all_0_2_2, aNaturalNumber0(xn), yields: % 82.26/43.06 | (303) ~ aNaturalNumber0(all_103_0_16) | sdtpldt0(all_103_0_16, xn) = all_0_2_2 % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xn, xn, all_91_0_10, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.06 | (304) ~ aNaturalNumber0(all_91_0_10) | ? [v0] : (sdtpldt0(all_25_0_5, all_91_0_10) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xn, xn, all_91_0_10, xp, xr and discharging atoms sdtpldt0(xr, xp) = xn, sdtpldt0(xn, all_91_0_10) = xn, aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.06 | (305) ~ aNaturalNumber0(all_91_0_10) | ? [v0] : (sdtpldt0(xr, v0) = xn & sdtpldt0(xp, all_91_0_10) = v0) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (69) with xn, all_91_0_10, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, aNaturalNumber0(xn), yields: % 82.26/43.06 | (306) ~ aNaturalNumber0(all_91_0_10) | sdtpldt0(all_91_0_10, xn) = xn % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_97_0_13, xn, xp, all_89_0_9, xp and discharging atoms sdtpldt0(xp, all_89_0_9) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(xp), yields: % 82.26/43.06 | (307) ~ aNaturalNumber0(all_89_0_9) | ? [v0] : (sdtpldt0(all_89_0_9, xp) = v0 & sdtpldt0(xp, v0) = all_97_0_13) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_97_0_13, xn, xp, all_91_0_10, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, sdtpldt0(xn, xp) = all_97_0_13, aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.06 | (308) ~ aNaturalNumber0(all_91_0_10) | ? [v0] : (sdtpldt0(all_91_0_10, xp) = v0 & sdtpldt0(xn, v0) = all_97_0_13) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xn, xn, xp, all_127_0_21, sz10 and discharging atoms sdtpldt0(sz10, all_127_0_21) = xn, aNaturalNumber0(all_127_0_21), aNaturalNumber0(xp), aNaturalNumber0(sz10), yields: % 82.26/43.06 | (309) ~ (sdtpldt0(xn, xp) = xn) | ? [v0] : (sdtpldt0(all_127_0_21, xp) = v0 & sdtpldt0(sz10, v0) = xn) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_2_2, xn, xm, all_109_0_19, xn and discharging atoms sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(all_109_0_19), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.06 | (310) ~ (sdtpldt0(xn, all_109_0_19) = xn) | ? [v0] : (sdtpldt0(all_109_0_19, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (29) with all_109_0_19 and discharging atoms aNaturalNumber0(all_109_0_19), yields: % 82.26/43.06 | (311) all_109_0_19 = sz10 | all_109_0_19 = sz00 | ? [v0] : (isPrime0(v0) & doDivides0(v0, all_109_0_19) & aNaturalNumber0(v0)) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xp, xp, all_107_0_18, all_107_0_18, xp and discharging atoms aNaturalNumber0(all_107_0_18), aNaturalNumber0(xp), yields: % 82.26/43.06 | (312) ~ (sdtpldt0(xp, all_107_0_18) = xp) | ? [v0] : (sdtpldt0(all_107_0_18, all_107_0_18) = v0 & sdtpldt0(xp, v0) = xp) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_15_0_4, xp, xm, all_107_0_18, xp and discharging atoms sdtpldt0(xp, xm) = all_15_0_4, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.06 | (313) ~ (sdtpldt0(xp, all_107_0_18) = xp) | ? [v0] : (sdtpldt0(all_107_0_18, xm) = v0 & sdtpldt0(xp, v0) = all_15_0_4) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xm, xm, all_25_0_5, all_25_0_5, xm and discharging atoms aNaturalNumber0(all_25_0_5), aNaturalNumber0(xm), yields: % 82.26/43.06 | (314) ~ (sdtpldt0(xm, all_25_0_5) = xm) | ? [v0] : (sdtpldt0(all_25_0_5, all_25_0_5) = v0 & sdtpldt0(xm, v0) = xm) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xm, xm, all_107_0_18, xp, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xp), aNaturalNumber0(xm), yields: % 82.26/43.06 | (315) ~ (sdtpldt0(xm, xp) = xm) | ? [v0] : (sdtpldt0(xp, all_107_0_18) = v0 & sdtpldt0(xm, v0) = xm) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xn, xn, all_107_0_18, all_25_0_5, xn and discharging atoms sdtpldt0(xn, all_25_0_5) = xn, aNaturalNumber0(all_107_0_18), aNaturalNumber0(all_25_0_5), aNaturalNumber0(xn), yields: % 82.26/43.06 | (316) ~ (sdtpldt0(xn, all_107_0_18) = xn) | ? [v0] : (sdtpldt0(all_25_0_5, all_107_0_18) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (55) with xm, all_107_0_18, sz00, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.26/43.06 | (317) xm = sz00 | ~ sdtlseqdt0(xm, sz00) | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xm) & ~ (v1 = v0) & sdtpldt0(all_107_0_18, xm) = v0 & sdtpldt0(all_107_0_18, sz00) = v1 & sdtpldt0(sz00, all_107_0_18) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(xm, v2)) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_1_1, xm, all_97_0_13, all_107_0_18, xm and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, sdtpldt0(xm, all_97_0_13) = all_0_1_1, aNaturalNumber0(all_107_0_18), aNaturalNumber0(xm), yields: % 82.26/43.06 | (318) ~ aNaturalNumber0(all_97_0_13) | ? [v0] : (sdtpldt0(all_107_0_18, all_97_0_13) = v0 & sdtpldt0(xm, v0) = all_0_1_1) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with xp, xp, all_107_0_18, all_105_0_17, sz10 and discharging atoms sdtpldt0(sz10, all_105_0_17) = xp, aNaturalNumber0(all_107_0_18), aNaturalNumber0(all_105_0_17), aNaturalNumber0(sz10), yields: % 82.26/43.06 | (319) ~ (sdtpldt0(xp, all_107_0_18) = xp) | ? [v0] : (sdtpldt0(all_105_0_17, all_107_0_18) = v0 & sdtpldt0(sz10, v0) = xp) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_2_2, all_0_2_2, xp, xn, all_15_0_4 and discharging atoms aNaturalNumber0(all_15_0_4), aNaturalNumber0(xp), aNaturalNumber0(xn), yields: % 82.26/43.06 | (320) ~ (sdtpldt0(all_15_0_4, xn) = all_0_2_2) | ~ (sdtpldt0(all_0_2_2, xp) = all_0_2_2) | ? [v0] : (sdtpldt0(all_15_0_4, v0) = all_0_2_2 & sdtpldt0(xn, xp) = v0) % 82.26/43.06 | % 82.26/43.06 | Instantiating formula (54) with all_0_1_1, all_0_2_2, xp, all_15_0_4, xr and discharging atoms sdtpldt0(all_0_2_2, xp) = all_0_1_1, aNaturalNumber0(all_15_0_4), aNaturalNumber0(xr), aNaturalNumber0(xp), yields: % 82.26/43.06 | (321) ~ (sdtpldt0(xr, all_15_0_4) = all_0_2_2) | ? [v0] : (sdtpldt0(all_15_0_4, xp) = v0 & sdtpldt0(xr, v0) = all_0_1_1) % 82.26/43.06 | % 82.26/43.07 | Instantiating formula (54) with all_0_1_1, xn, all_15_0_4, all_91_0_10, xn and discharging atoms sdtpldt0(xn, all_91_0_10) = xn, sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(all_15_0_4), aNaturalNumber0(xn), yields: % 82.26/43.07 | (322) ~ aNaturalNumber0(all_91_0_10) | ? [v0] : (sdtpldt0(all_91_0_10, all_15_0_4) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (32) with all_15_0_4, all_0_1_1, xn and discharging atoms sdtpldt0(xn, all_15_0_4) = all_0_1_1, aNaturalNumber0(all_15_0_4), aNaturalNumber0(all_0_1_1), aNaturalNumber0(xn), yields: % 82.26/43.07 | (323) sdtlseqdt0(xn, all_0_1_1) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (54) with all_122_0_20, all_25_0_5, all_15_0_4, all_25_0_5, all_25_0_5 and discharging atoms sdtpldt0(all_25_0_5, all_15_0_4) = all_122_0_20, aNaturalNumber0(all_25_0_5), aNaturalNumber0(all_15_0_4), yields: % 82.26/43.07 | (324) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5) | ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_122_0_20 & sdtpldt0(all_25_0_5, all_15_0_4) = v0) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (26) with all_122_0_20, all_15_0_4 and discharging atoms aNaturalNumber0(all_15_0_4), yields: % 82.26/43.07 | (325) ~ (sdtpldt0(sz00, all_15_0_4) = all_122_0_20) | sdtpldt0(all_15_0_4, sz00) = all_15_0_4 % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (54) with all_0_1_1, xm, xn, xp, xm and discharging atoms aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.26/43.07 | (326) ~ (sdtpldt0(xm, xp) = xm) | ~ (sdtpldt0(xm, xn) = all_0_1_1) | ? [v0] : (sdtpldt0(xp, xn) = v0 & sdtpldt0(xm, v0) = all_0_1_1) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (54) with xm, xm, all_107_0_18, all_15_0_4, all_25_0_5 and discharging atoms sdtpldt0(xm, all_107_0_18) = xm, aNaturalNumber0(all_107_0_18), aNaturalNumber0(all_25_0_5), aNaturalNumber0(all_15_0_4), yields: % 82.26/43.07 | (327) ~ (sdtpldt0(all_25_0_5, all_15_0_4) = xm) | ? [v0] : (sdtpldt0(all_25_0_5, v0) = xm & sdtpldt0(all_15_0_4, all_107_0_18) = v0) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (40) with all_15_0_4, sz00 and discharging atoms aNaturalNumber0(all_15_0_4), aNaturalNumber0(sz00), yields: % 82.26/43.07 | (328) all_15_0_4 = sz00 | ~ sdtlseqdt0(sz00, all_15_0_4) | iLess0(sz00, all_15_0_4) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (2) with all_15_0_4, sz00 and discharging atoms aNaturalNumber0(all_15_0_4), aNaturalNumber0(sz00), yields: % 82.26/43.07 | (329) ~ sdtlseqdt0(sz00, all_15_0_4) | ? [v0] : (sdtpldt0(sz00, v0) = all_15_0_4 & aNaturalNumber0(v0)) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (2) with all_0_1_1, xr and discharging atoms aNaturalNumber0(all_0_1_1), aNaturalNumber0(xr), yields: % 82.26/43.07 | (330) ~ sdtlseqdt0(xr, all_0_1_1) | ? [v0] : (sdtpldt0(xr, v0) = all_0_1_1 & aNaturalNumber0(v0)) % 82.26/43.07 | % 82.26/43.07 | Instantiating formula (2) with all_0_1_1, xn and discharging atoms aNaturalNumber0(all_0_1_1), aNaturalNumber0(xn), yields: % 82.26/43.07 | (331) ~ sdtlseqdt0(xn, all_0_1_1) | ? [v0] : (sdtpldt0(xn, v0) = all_0_1_1 & aNaturalNumber0(v0)) % 82.26/43.07 | % 82.26/43.07 | Instantiating (299) with all_238_0_25 yields: % 82.26/43.07 | (332) sdtpldt0(all_109_0_19, xm) = all_238_0_25 & sdtpldt0(xp, all_238_0_25) = all_15_0_4 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (332) yields: % 82.26/43.07 | (333) sdtpldt0(all_109_0_19, xm) = all_238_0_25 % 82.26/43.07 | (334) sdtpldt0(xp, all_238_0_25) = all_15_0_4 % 82.26/43.07 | % 82.26/43.07 | Instantiating (284) with all_250_0_31 yields: % 82.26/43.07 | (335) sdtpldt0(all_25_0_5, xp) = all_250_0_31 & sdtpldt0(xn, all_250_0_31) = all_97_0_13 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (335) yields: % 82.26/43.07 | (336) sdtpldt0(all_25_0_5, xp) = all_250_0_31 % 82.26/43.07 | (337) sdtpldt0(xn, all_250_0_31) = all_97_0_13 % 82.26/43.07 | % 82.26/43.07 | Instantiating (297) with all_262_0_37 yields: % 82.26/43.07 | (338) sdtpldt0(all_107_0_18, xp) = all_262_0_37 & sdtpldt0(xm, all_262_0_37) = all_15_0_4 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (338) yields: % 82.26/43.07 | (339) sdtpldt0(all_107_0_18, xp) = all_262_0_37 % 82.26/43.07 | (340) sdtpldt0(xm, all_262_0_37) = all_15_0_4 % 82.26/43.07 | % 82.26/43.07 | Instantiating (287) with all_268_0_40 yields: % 82.26/43.07 | (341) sdtpldt0(xr, all_268_0_40) = all_97_0_13 & sdtpldt0(xp, xp) = all_268_0_40 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (341) yields: % 82.26/43.07 | (342) sdtpldt0(xr, all_268_0_40) = all_97_0_13 % 82.26/43.07 | (343) sdtpldt0(xp, xp) = all_268_0_40 % 82.26/43.07 | % 82.26/43.07 | Instantiating (295) with all_270_0_41 yields: % 82.26/43.07 | (344) sdtpldt0(xn, all_270_0_41) = all_0_2_2 & aNaturalNumber0(all_270_0_41) % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (344) yields: % 82.26/43.07 | (345) sdtpldt0(xn, all_270_0_41) = all_0_2_2 % 82.26/43.07 | (346) aNaturalNumber0(all_270_0_41) % 82.26/43.07 | % 82.26/43.07 | Instantiating (290) with all_284_0_48 yields: % 82.26/43.07 | (347) sdtpldt0(all_25_0_5, all_284_0_48) = all_25_0_5 & aNaturalNumber0(all_284_0_48) % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (347) yields: % 82.26/43.07 | (348) sdtpldt0(all_25_0_5, all_284_0_48) = all_25_0_5 % 82.26/43.07 | (349) aNaturalNumber0(all_284_0_48) % 82.26/43.07 | % 82.26/43.07 | Instantiating (285) with all_294_0_53 yields: % 82.26/43.07 | (350) sdtpldt0(all_25_0_5, all_294_0_53) = all_97_0_13 & sdtpldt0(xn, xp) = all_294_0_53 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (350) yields: % 82.26/43.07 | (351) sdtpldt0(all_25_0_5, all_294_0_53) = all_97_0_13 % 82.26/43.07 | (352) sdtpldt0(xn, xp) = all_294_0_53 % 82.26/43.07 | % 82.26/43.07 | Instantiating (283) with all_296_0_54 yields: % 82.26/43.07 | (353) sdtpldt0(xr, xp) = all_296_0_54 & sdtpldt0(xp, all_296_0_54) = all_97_0_13 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (353) yields: % 82.26/43.07 | (354) sdtpldt0(xr, xp) = all_296_0_54 % 82.26/43.07 | (355) sdtpldt0(xp, all_296_0_54) = all_97_0_13 % 82.26/43.07 | % 82.26/43.07 | Instantiating (272) with all_306_0_59 yields: % 82.26/43.07 | (356) sdtpldt0(xr, all_306_0_59) = xn & sdtpldt0(xp, all_25_0_5) = all_306_0_59 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (356) yields: % 82.26/43.07 | (357) sdtpldt0(xr, all_306_0_59) = xn % 82.26/43.07 | (358) sdtpldt0(xp, all_25_0_5) = all_306_0_59 % 82.26/43.07 | % 82.26/43.07 | Instantiating (273) with all_310_0_61 yields: % 82.26/43.07 | (359) sdtpldt0(xr, all_310_0_61) = all_0_1_1 & sdtpldt0(xp, all_15_0_4) = all_310_0_61 % 82.26/43.07 | % 82.26/43.07 | Applying alpha-rule on (359) yields: % 82.26/43.07 | (360) sdtpldt0(xr, all_310_0_61) = all_0_1_1 % 82.26/43.07 | (361) sdtpldt0(xp, all_15_0_4) = all_310_0_61 % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (303), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (362) ~ aNaturalNumber0(all_103_0_16) % 82.26/43.07 | % 82.26/43.07 | Using (269) and (362) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (269) aNaturalNumber0(all_103_0_16) % 82.26/43.07 | (365) sdtpldt0(all_103_0_16, xn) = all_0_2_2 % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (306), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.26/43.07 | % 82.26/43.07 | Using (264) and (366) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (264) aNaturalNumber0(all_91_0_10) % 82.26/43.07 | (369) sdtpldt0(all_91_0_10, xn) = xn % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (30), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (370) ~ sdtlseqdt0(xr, xn) % 82.26/43.07 | % 82.26/43.07 | Using (274) and (370) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (274) sdtlseqdt0(xr, xn) % 82.26/43.07 | (373) xr = xn % 82.26/43.07 | % 82.26/43.07 | From (373) and (172) follows: % 82.26/43.07 | (374) sdtpldt0(xn, all_25_0_5) = all_89_0_9 % 82.26/43.07 | % 82.26/43.07 | From (373) and (354) follows: % 82.26/43.07 | (375) sdtpldt0(xn, xp) = all_296_0_54 % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (251), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (362) ~ aNaturalNumber0(all_103_0_16) % 82.26/43.07 | % 82.26/43.07 | Using (269) and (362) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (269) aNaturalNumber0(all_103_0_16) % 82.26/43.07 | (379) all_103_0_16 = xm % 82.26/43.07 | % 82.26/43.07 | From (379) and (268) follows: % 82.26/43.07 | (380) sdtpldt0(xm, all_25_0_5) = xm % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (243), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (381) ~ (sdtpldt0(xr, all_25_0_5) = xn) % 82.26/43.07 | % 82.26/43.07 | From (373) and (381) follows: % 82.26/43.07 | (382) ~ (sdtpldt0(xn, all_25_0_5) = xn) % 82.26/43.07 | % 82.26/43.07 | Using (101) and (382) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (384) sdtpldt0(xr, all_25_0_5) = xn % 82.26/43.07 | (385) all_25_0_5 = xp % 82.26/43.07 | % 82.26/43.07 | From (385)(385) and (348) follows: % 82.26/43.07 | (386) sdtpldt0(xp, all_284_0_48) = xp % 82.26/43.07 | % 82.26/43.07 | From (385)(385) and (175) follows: % 82.26/43.07 | (387) sdtpldt0(xp, xp) = all_91_0_10 % 82.26/43.07 | % 82.26/43.07 | From (385) and (336) follows: % 82.26/43.07 | (388) sdtpldt0(xp, xp) = all_250_0_31 % 82.26/43.07 | % 82.26/43.07 | From (385) and (265) follows: % 82.26/43.07 | (389) sdtpldt0(all_15_0_4, xp) = all_122_0_20 % 82.26/43.07 | % 82.26/43.07 | From (385) and (358) follows: % 82.26/43.07 | (390) sdtpldt0(xp, xp) = all_306_0_59 % 82.26/43.07 | % 82.26/43.07 | From (385) and (380) follows: % 82.26/43.07 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.07 | % 82.26/43.07 | From (385) and (374) follows: % 82.26/43.07 | (392) sdtpldt0(xn, xp) = all_89_0_9 % 82.26/43.07 | % 82.26/43.07 | From (385) and (101) follows: % 82.26/43.07 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.07 | % 82.26/43.07 | From (385) and (262) follows: % 82.26/43.07 | (394) ~ (sdtpldt0(xp, all_15_0_4) = sz00) % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (247), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.26/43.07 | % 82.26/43.07 | Using (393) and (395) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.07 | (398) all_97_0_13 = xn % 82.26/43.07 | % 82.26/43.07 | From (398) and (181) follows: % 82.26/43.07 | (399) sdtpldt0(xm, xn) = all_0_1_1 % 82.26/43.07 | % 82.26/43.07 | From (398) and (337) follows: % 82.26/43.07 | (400) sdtpldt0(xn, all_250_0_31) = xn % 82.26/43.07 | % 82.26/43.07 +-Applying beta-rule and splitting (304), into two cases. % 82.26/43.07 |-Branch one: % 82.26/43.07 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.26/43.07 | % 82.26/43.07 | Using (264) and (366) yields: % 82.26/43.07 | (97) $false % 82.26/43.07 | % 82.26/43.07 |-The branch is then unsatisfiable % 82.26/43.07 |-Branch two: % 82.26/43.07 | (264) aNaturalNumber0(all_91_0_10) % 82.26/43.08 | (404) ? [v0] : (sdtpldt0(all_25_0_5, all_91_0_10) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.08 | % 82.26/43.08 | Instantiating (404) with all_347_0_66 yields: % 82.26/43.08 | (405) sdtpldt0(all_25_0_5, all_91_0_10) = all_347_0_66 & sdtpldt0(xn, all_347_0_66) = xn % 82.26/43.08 | % 82.26/43.08 | Applying alpha-rule on (405) yields: % 82.26/43.08 | (406) sdtpldt0(all_25_0_5, all_91_0_10) = all_347_0_66 % 82.26/43.08 | (407) sdtpldt0(xn, all_347_0_66) = xn % 82.26/43.08 | % 82.26/43.08 | From (385) and (406) follows: % 82.26/43.08 | (408) sdtpldt0(xp, all_91_0_10) = all_347_0_66 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (305), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.26/43.08 | % 82.26/43.08 | Using (264) and (366) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (264) aNaturalNumber0(all_91_0_10) % 82.26/43.08 | (412) ? [v0] : (sdtpldt0(xr, v0) = xn & sdtpldt0(xp, all_91_0_10) = v0) % 82.26/43.08 | % 82.26/43.08 | Instantiating (412) with all_352_0_67 yields: % 82.26/43.08 | (413) sdtpldt0(xr, all_352_0_67) = xn & sdtpldt0(xp, all_91_0_10) = all_352_0_67 % 82.26/43.08 | % 82.26/43.08 | Applying alpha-rule on (413) yields: % 82.26/43.08 | (414) sdtpldt0(xr, all_352_0_67) = xn % 82.26/43.08 | (415) sdtpldt0(xp, all_91_0_10) = all_352_0_67 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (307), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (416) ~ aNaturalNumber0(all_89_0_9) % 82.26/43.08 | % 82.26/43.08 | Using (271) and (416) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (271) aNaturalNumber0(all_89_0_9) % 82.26/43.08 | (419) ? [v0] : (sdtpldt0(all_89_0_9, xp) = v0 & sdtpldt0(xp, v0) = all_97_0_13) % 82.26/43.08 | % 82.26/43.08 | Instantiating (419) with all_357_0_68 yields: % 82.26/43.08 | (420) sdtpldt0(all_89_0_9, xp) = all_357_0_68 & sdtpldt0(xp, all_357_0_68) = all_97_0_13 % 82.26/43.08 | % 82.26/43.08 | Applying alpha-rule on (420) yields: % 82.26/43.08 | (421) sdtpldt0(all_89_0_9, xp) = all_357_0_68 % 82.26/43.08 | (422) sdtpldt0(xp, all_357_0_68) = all_97_0_13 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (242), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (423) ~ (sdtpldt0(xm, xn) = all_0_1_1) % 82.26/43.08 | % 82.26/43.08 | Using (399) and (423) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (399) sdtpldt0(xm, xn) = all_0_1_1 % 82.26/43.08 | (426) all_0_1_1 = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 | From (426) and (4) follows: % 82.26/43.08 | (427) sdtpldt0(all_0_2_2, xp) = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 | From (426) and (208) follows: % 82.26/43.08 | (428) sdtpldt0(xn, all_122_0_20) = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 | From (426) and (323) follows: % 82.26/43.08 | (156) sdtlseqdt0(xn, all_0_2_2) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (244), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (430) ~ (sdtpldt0(xr, xp) = all_89_0_9) % 82.26/43.08 | % 82.26/43.08 | From (373) and (430) follows: % 82.26/43.08 | (431) ~ (sdtpldt0(xn, xp) = all_89_0_9) % 82.26/43.08 | % 82.26/43.08 | Using (392) and (431) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (433) sdtpldt0(xr, xp) = all_89_0_9 % 82.26/43.08 | (434) all_89_0_9 = xn % 82.26/43.08 | % 82.26/43.08 | From (434) and (421) follows: % 82.26/43.08 | (435) sdtpldt0(xn, xp) = all_357_0_68 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (246), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (436) ~ (sdtpldt0(xn, sz00) = xn) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (245), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.26/43.08 | % 82.26/43.08 | Using (391) and (437) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.08 | (440) all_15_0_4 = xm % 82.26/43.08 | % 82.26/43.08 | Equations (440) can reduce 138 to: % 82.26/43.08 | (441) ~ (xm = sz00) % 82.26/43.08 | % 82.26/43.08 | From (440) and (389) follows: % 82.26/43.08 | (442) sdtpldt0(xm, xp) = all_122_0_20 % 82.26/43.08 | % 82.26/43.08 | From (440) and (361) follows: % 82.26/43.08 | (443) sdtpldt0(xp, xm) = all_310_0_61 % 82.26/43.08 | % 82.26/43.08 | From (440) and (93) follows: % 82.26/43.08 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.08 | % 82.26/43.08 | From (440) and (394) follows: % 82.26/43.08 | (445) ~ (sdtpldt0(xp, xm) = sz00) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (248), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (446) xm = sz00 % 82.26/43.08 | % 82.26/43.08 | Equations (446) can reduce 441 to: % 82.26/43.08 | (104) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (441) ~ (xm = sz00) % 82.26/43.08 | (449) all_137_0_23 = xn % 82.26/43.08 | % 82.26/43.08 | From (449) and (229) follows: % 82.26/43.08 | (38) aNaturalNumber0(xn) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (139), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.26/43.08 | % 82.26/43.08 | Using (391) and (437) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.08 | (454) ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xm, v0) = xm) % 82.26/43.08 | % 82.26/43.08 | Instantiating (454) with all_426_0_73 yields: % 82.26/43.08 | (455) sdtpldt0(xp, xp) = all_426_0_73 & sdtpldt0(xm, all_426_0_73) = xm % 82.26/43.08 | % 82.26/43.08 | Applying alpha-rule on (455) yields: % 82.26/43.08 | (456) sdtpldt0(xp, xp) = all_426_0_73 % 82.26/43.08 | (457) sdtpldt0(xm, all_426_0_73) = xm % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (302), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (458) ~ aNaturalNumber0(all_122_0_20) % 82.26/43.08 | % 82.26/43.08 | Using (266) and (458) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (266) aNaturalNumber0(all_122_0_20) % 82.26/43.08 | (461) sdtpldt0(all_122_0_20, xn) = all_0_1_1 % 82.26/43.08 | % 82.26/43.08 | From (426) and (461) follows: % 82.26/43.08 | (462) sdtpldt0(all_122_0_20, xn) = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (254), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (458) ~ aNaturalNumber0(all_122_0_20) % 82.26/43.08 | % 82.26/43.08 | Using (266) and (458) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (266) aNaturalNumber0(all_122_0_20) % 82.26/43.08 | (466) all_122_0_20 = all_15_0_4 % 82.26/43.08 | % 82.26/43.08 | Combining equations (440,466) yields a new equation: % 82.26/43.08 | (467) all_122_0_20 = xm % 82.26/43.08 | % 82.26/43.08 | From (467) and (462) follows: % 82.26/43.08 | (81) sdtpldt0(xm, xn) = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 | From (467) and (442) follows: % 82.26/43.08 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.08 | % 82.26/43.08 | From (467) and (428) follows: % 82.26/43.08 | (28) sdtpldt0(xn, xm) = all_0_2_2 % 82.26/43.08 | % 82.26/43.08 | From (467) and (266) follows: % 82.26/43.08 | (16) aNaturalNumber0(xm) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (250), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.26/43.08 | % 82.26/43.08 | Using (264) and (366) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (264) aNaturalNumber0(all_91_0_10) % 82.26/43.08 | (475) all_91_0_10 = all_25_0_5 % 82.26/43.08 | % 82.26/43.08 | Combining equations (385,475) yields a new equation: % 82.26/43.08 | (476) all_91_0_10 = xp % 82.26/43.08 | % 82.26/43.08 | From (476) and (369) follows: % 82.26/43.08 | (477) sdtpldt0(xp, xn) = xn % 82.26/43.08 | % 82.26/43.08 | From (476) and (415) follows: % 82.26/43.08 | (478) sdtpldt0(xp, xp) = all_352_0_67 % 82.26/43.08 | % 82.26/43.08 | From (476) and (408) follows: % 82.26/43.08 | (479) sdtpldt0(xp, xp) = all_347_0_66 % 82.26/43.08 | % 82.26/43.08 | From (476) and (387) follows: % 82.26/43.08 | (480) sdtpldt0(xp, xp) = xp % 82.26/43.08 | % 82.26/43.08 | From (476) and (176) follows: % 82.26/43.08 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.08 | % 82.26/43.08 | From (476) and (264) follows: % 82.26/43.08 | (17) aNaturalNumber0(xp) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (168), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (483) ~ (sdtpldt0(all_0_2_2, xp) = all_0_2_2) % 82.26/43.08 | % 82.26/43.08 | Using (427) and (483) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (427) sdtpldt0(all_0_2_2, xp) = all_0_2_2 % 82.26/43.08 | (486) ? [v0] : (sdtpldt0(all_0_2_2, v0) = all_0_2_2 & sdtpldt0(xp, xp) = v0) % 82.26/43.08 | % 82.26/43.08 | Instantiating (486) with all_460_0_77 yields: % 82.26/43.08 | (487) sdtpldt0(all_0_2_2, all_460_0_77) = all_0_2_2 & sdtpldt0(xp, xp) = all_460_0_77 % 82.26/43.08 | % 82.26/43.08 | Applying alpha-rule on (487) yields: % 82.26/43.08 | (488) sdtpldt0(all_0_2_2, all_460_0_77) = all_0_2_2 % 82.26/43.08 | (489) sdtpldt0(xp, xp) = all_460_0_77 % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (277), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (490) ~ (sdtpldt0(xp, all_25_0_5) = xp) % 82.26/43.08 | % 82.26/43.08 | From (385) and (490) follows: % 82.26/43.08 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.26/43.08 | % 82.26/43.08 | Using (480) and (491) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (493) sdtpldt0(xp, all_25_0_5) = xp % 82.26/43.08 | (494) ? [v0] : (sdtpldt0(all_25_0_5, xr) = v0 & sdtpldt0(xp, v0) = xn) % 82.26/43.08 | % 82.26/43.08 | From (385) and (493) follows: % 82.26/43.08 | (480) sdtpldt0(xp, xp) = xp % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (280), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.26/43.08 | % 82.26/43.08 | Using (480) and (491) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (480) sdtpldt0(xp, xp) = xp % 82.26/43.08 | (499) ? [v0] : (sdtpldt0(xp, v0) = all_15_0_4 & sdtpldt0(xp, xm) = v0) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (309), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.26/43.08 | % 82.26/43.08 | Using (393) and (395) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.08 | (503) ? [v0] : (sdtpldt0(all_127_0_21, xp) = v0 & sdtpldt0(sz10, v0) = xn) % 82.26/43.08 | % 82.26/43.08 +-Applying beta-rule and splitting (288), into two cases. % 82.26/43.08 |-Branch one: % 82.26/43.08 | (504) ~ (sdtpldt0(xn, xp) = xr) % 82.26/43.08 | % 82.26/43.08 | From (373) and (504) follows: % 82.26/43.08 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.26/43.08 | % 82.26/43.08 | Using (393) and (395) yields: % 82.26/43.08 | (97) $false % 82.26/43.08 | % 82.26/43.08 |-The branch is then unsatisfiable % 82.26/43.08 |-Branch two: % 82.26/43.08 | (507) sdtpldt0(xn, xp) = xr % 82.26/43.08 | (508) ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xn, v0) = xn) % 82.26/43.08 | % 82.26/43.09 | Instantiating (508) with all_520_0_82 yields: % 82.26/43.09 | (509) sdtpldt0(xp, xp) = all_520_0_82 & sdtpldt0(xn, all_520_0_82) = xn % 82.26/43.09 | % 82.26/43.09 | Applying alpha-rule on (509) yields: % 82.26/43.09 | (510) sdtpldt0(xp, xp) = all_520_0_82 % 82.26/43.09 | (511) sdtpldt0(xn, all_520_0_82) = xn % 82.26/43.09 | % 82.26/43.09 | From (373) and (507) follows: % 82.26/43.09 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.09 | % 82.26/43.09 +-Applying beta-rule and splitting (282), into two cases. % 82.26/43.09 |-Branch one: % 82.26/43.09 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.26/43.09 | % 82.26/43.09 | Using (391) and (437) yields: % 82.26/43.09 | (97) $false % 82.26/43.09 | % 82.26/43.09 |-The branch is then unsatisfiable % 82.26/43.09 |-Branch two: % 82.26/43.09 | (391) sdtpldt0(xm, xp) = xm % 82.26/43.09 | (516) ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xm, v0) = all_15_0_4) % 82.26/43.09 | % 82.26/43.09 | Instantiating (516) with all_531_0_84 yields: % 82.26/43.09 | (517) sdtpldt0(xp, xp) = all_531_0_84 & sdtpldt0(xm, all_531_0_84) = all_15_0_4 % 82.26/43.09 | % 82.26/43.09 | Applying alpha-rule on (517) yields: % 82.26/43.09 | (518) sdtpldt0(xp, xp) = all_531_0_84 % 82.26/43.09 | (519) sdtpldt0(xm, all_531_0_84) = all_15_0_4 % 82.26/43.09 | % 82.26/43.09 +-Applying beta-rule and splitting (143), into two cases. % 82.26/43.09 |-Branch one: % 82.26/43.09 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.26/43.09 | % 82.26/43.09 | Using (393) and (395) yields: % 82.26/43.09 | (97) $false % 82.26/43.09 | % 82.26/43.09 |-The branch is then unsatisfiable % 82.26/43.09 |-Branch two: % 82.26/43.09 | (393) sdtpldt0(xn, xp) = xn % 82.26/43.09 | (523) ? [v0] : (sdtpldt0(xp, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.26/43.09 | % 82.26/43.09 | Instantiating (523) with all_537_0_85 yields: % 82.26/43.09 | (524) sdtpldt0(xp, xm) = all_537_0_85 & sdtpldt0(xn, all_537_0_85) = all_0_2_2 % 82.26/43.09 | % 82.73/43.09 | Applying alpha-rule on (524) yields: % 82.73/43.09 | (525) sdtpldt0(xp, xm) = all_537_0_85 % 82.73/43.09 | (526) sdtpldt0(xn, all_537_0_85) = all_0_2_2 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (267), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (527) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5) % 82.73/43.09 | % 82.73/43.09 | From (385)(385)(385) and (527) follows: % 82.73/43.09 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.73/43.09 | % 82.73/43.09 | Using (480) and (491) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (530) sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5 % 82.73/43.09 | (531) ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_103_0_16 & sdtpldt0(all_25_0_5, xm) = v0) % 82.73/43.09 | % 82.73/43.09 | Instantiating (531) with all_543_0_86 yields: % 82.73/43.09 | (532) sdtpldt0(all_25_0_5, all_543_0_86) = all_103_0_16 & sdtpldt0(all_25_0_5, xm) = all_543_0_86 % 82.73/43.09 | % 82.73/43.09 | Applying alpha-rule on (532) yields: % 82.73/43.09 | (533) sdtpldt0(all_25_0_5, all_543_0_86) = all_103_0_16 % 82.73/43.09 | (534) sdtpldt0(all_25_0_5, xm) = all_543_0_86 % 82.73/43.09 | % 82.73/43.09 | From (385)(385)(385) and (530) follows: % 82.73/43.09 | (480) sdtpldt0(xp, xp) = xp % 82.73/43.09 | % 82.73/43.09 | From (385) and (534) follows: % 82.73/43.09 | (536) sdtpldt0(xp, xm) = all_543_0_86 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (322), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.73/43.09 | % 82.73/43.09 | From (476) and (366) follows: % 82.73/43.09 | (538) ~ aNaturalNumber0(xp) % 82.73/43.09 | % 82.73/43.09 | Using (17) and (538) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (264) aNaturalNumber0(all_91_0_10) % 82.73/43.09 | (541) ? [v0] : (sdtpldt0(all_91_0_10, all_15_0_4) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 | Instantiating (541) with all_557_0_87 yields: % 82.73/43.09 | (542) sdtpldt0(all_91_0_10, all_15_0_4) = all_557_0_87 & sdtpldt0(xn, all_557_0_87) = all_0_1_1 % 82.73/43.09 | % 82.73/43.09 | Applying alpha-rule on (542) yields: % 82.73/43.09 | (543) sdtpldt0(all_91_0_10, all_15_0_4) = all_557_0_87 % 82.73/43.09 | (544) sdtpldt0(xn, all_557_0_87) = all_0_1_1 % 82.73/43.09 | % 82.73/43.09 | From (476)(440) and (543) follows: % 82.73/43.09 | (545) sdtpldt0(xp, xm) = all_557_0_87 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (326), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (423) ~ (sdtpldt0(xm, xn) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 | From (426) and (423) follows: % 82.73/43.09 | (547) ~ (sdtpldt0(xm, xn) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | Using (81) and (547) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (399) sdtpldt0(xm, xn) = all_0_1_1 % 82.73/43.09 | (550) ~ (sdtpldt0(xm, xp) = xm) | ? [v0] : (sdtpldt0(xp, xn) = v0 & sdtpldt0(xm, v0) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 | From (426) and (399) follows: % 82.73/43.09 | (81) sdtpldt0(xm, xn) = all_0_2_2 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (550), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.73/43.09 | % 82.73/43.09 | Using (391) and (437) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (391) sdtpldt0(xm, xp) = xm % 82.73/43.09 | (555) ? [v0] : (sdtpldt0(xp, xn) = v0 & sdtpldt0(xm, v0) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (324), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (527) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5) % 82.73/43.09 | % 82.73/43.09 | From (385)(385)(385) and (527) follows: % 82.73/43.09 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.73/43.09 | % 82.73/43.09 | Using (480) and (491) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (530) sdtpldt0(all_25_0_5, all_25_0_5) = all_25_0_5 % 82.73/43.09 | (560) ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_122_0_20 & sdtpldt0(all_25_0_5, all_15_0_4) = v0) % 82.73/43.09 | % 82.73/43.09 | Instantiating (560) with all_584_0_93 yields: % 82.73/43.09 | (561) sdtpldt0(all_25_0_5, all_584_0_93) = all_122_0_20 & sdtpldt0(all_25_0_5, all_15_0_4) = all_584_0_93 % 82.73/43.09 | % 82.73/43.09 | Applying alpha-rule on (561) yields: % 82.73/43.09 | (562) sdtpldt0(all_25_0_5, all_584_0_93) = all_122_0_20 % 82.73/43.09 | (563) sdtpldt0(all_25_0_5, all_15_0_4) = all_584_0_93 % 82.73/43.09 | % 82.73/43.09 | From (385)(385)(385) and (530) follows: % 82.73/43.09 | (480) sdtpldt0(xp, xp) = xp % 82.73/43.09 | % 82.73/43.09 | From (385)(440) and (563) follows: % 82.73/43.09 | (565) sdtpldt0(xp, xm) = all_584_0_93 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (321), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (566) ~ (sdtpldt0(xr, all_15_0_4) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | From (373)(440) and (566) follows: % 82.73/43.09 | (567) ~ (sdtpldt0(xn, xm) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | Using (28) and (567) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (569) sdtpldt0(xr, all_15_0_4) = all_0_2_2 % 82.73/43.09 | (570) ? [v0] : (sdtpldt0(all_15_0_4, xp) = v0 & sdtpldt0(xr, v0) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 | From (373)(440) and (569) follows: % 82.73/43.09 | (28) sdtpldt0(xn, xm) = all_0_2_2 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (301), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (458) ~ aNaturalNumber0(all_122_0_20) % 82.73/43.09 | % 82.73/43.09 | From (467) and (458) follows: % 82.73/43.09 | (573) ~ aNaturalNumber0(xm) % 82.73/43.09 | % 82.73/43.09 | Using (16) and (573) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (266) aNaturalNumber0(all_122_0_20) % 82.73/43.09 | (576) ? [v0] : (sdtpldt0(all_25_0_5, all_122_0_20) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.73/43.09 | % 82.73/43.09 | Instantiating (576) with all_596_0_95 yields: % 82.73/43.09 | (577) sdtpldt0(all_25_0_5, all_122_0_20) = all_596_0_95 & sdtpldt0(xn, all_596_0_95) = all_0_1_1 % 82.73/43.09 | % 82.73/43.09 | Applying alpha-rule on (577) yields: % 82.73/43.09 | (578) sdtpldt0(all_25_0_5, all_122_0_20) = all_596_0_95 % 82.73/43.09 | (579) sdtpldt0(xn, all_596_0_95) = all_0_1_1 % 82.73/43.09 | % 82.73/43.09 | From (385)(467) and (578) follows: % 82.73/43.09 | (580) sdtpldt0(xp, xm) = all_596_0_95 % 82.73/43.09 | % 82.73/43.09 | From (467) and (266) follows: % 82.73/43.09 | (16) aNaturalNumber0(xm) % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (320), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (582) ~ (sdtpldt0(all_15_0_4, xn) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | From (440) and (582) follows: % 82.73/43.09 | (547) ~ (sdtpldt0(xm, xn) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | Using (81) and (547) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (585) sdtpldt0(all_15_0_4, xn) = all_0_2_2 % 82.73/43.09 | (586) ~ (sdtpldt0(all_0_2_2, xp) = all_0_2_2) | ? [v0] : (sdtpldt0(all_15_0_4, v0) = all_0_2_2 & sdtpldt0(xn, xp) = v0) % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (586), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (483) ~ (sdtpldt0(all_0_2_2, xp) = all_0_2_2) % 82.73/43.09 | % 82.73/43.09 | Using (427) and (483) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (427) sdtpldt0(all_0_2_2, xp) = all_0_2_2 % 82.73/43.09 | (590) ? [v0] : (sdtpldt0(all_15_0_4, v0) = all_0_2_2 & sdtpldt0(xn, xp) = v0) % 82.73/43.09 | % 82.73/43.09 | Instantiating (590) with all_606_0_96 yields: % 82.73/43.09 | (591) sdtpldt0(all_15_0_4, all_606_0_96) = all_0_2_2 & sdtpldt0(xn, xp) = all_606_0_96 % 82.73/43.09 | % 82.73/43.09 | Applying alpha-rule on (591) yields: % 82.73/43.09 | (592) sdtpldt0(all_15_0_4, all_606_0_96) = all_0_2_2 % 82.73/43.09 | (593) sdtpldt0(xn, xp) = all_606_0_96 % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (253), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.73/43.09 | % 82.73/43.09 | Using (391) and (437) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.09 |-The branch is then unsatisfiable % 82.73/43.09 |-Branch two: % 82.73/43.09 | (391) sdtpldt0(xm, xp) = xm % 82.73/43.09 | (597) all_107_0_18 = xp % 82.73/43.09 | % 82.73/43.09 | From (597) and (339) follows: % 82.73/43.09 | (598) sdtpldt0(xp, xp) = all_262_0_37 % 82.73/43.09 | % 82.73/43.09 | From (597) and (300) follows: % 82.73/43.09 | (599) sdtpldt0(xp, xm) = xm % 82.73/43.09 | % 82.73/43.09 | From (597) and (193) follows: % 82.73/43.09 | (391) sdtpldt0(xm, xp) = xm % 82.73/43.09 | % 82.73/43.09 | From (597) and (194) follows: % 82.73/43.09 | (17) aNaturalNumber0(xp) % 82.73/43.09 | % 82.73/43.09 +-Applying beta-rule and splitting (161), into two cases. % 82.73/43.09 |-Branch one: % 82.73/43.09 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.73/43.09 | % 82.73/43.09 | Using (393) and (395) yields: % 82.73/43.09 | (97) $false % 82.73/43.09 | % 82.73/43.10 |-The branch is then unsatisfiable % 82.73/43.10 |-Branch two: % 82.73/43.10 | (393) sdtpldt0(xn, xp) = xn % 82.73/43.10 | (508) ? [v0] : (sdtpldt0(xp, xp) = v0 & sdtpldt0(xn, v0) = xn) % 82.73/43.10 | % 82.73/43.10 | Instantiating (508) with all_616_0_97 yields: % 82.73/43.10 | (606) sdtpldt0(xp, xp) = all_616_0_97 & sdtpldt0(xn, all_616_0_97) = xn % 82.73/43.10 | % 82.73/43.10 | Applying alpha-rule on (606) yields: % 82.73/43.10 | (607) sdtpldt0(xp, xp) = all_616_0_97 % 82.73/43.10 | (608) sdtpldt0(xn, all_616_0_97) = xn % 82.73/43.10 | % 82.73/43.10 +-Applying beta-rule and splitting (279), into two cases. % 82.73/43.10 |-Branch one: % 82.73/43.10 | (490) ~ (sdtpldt0(xp, all_25_0_5) = xp) % 82.73/43.10 | % 82.73/43.10 | From (385) and (490) follows: % 82.73/43.10 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.73/43.10 | % 82.73/43.10 | Using (480) and (491) yields: % 82.73/43.10 | (97) $false % 82.73/43.10 | % 82.73/43.10 |-The branch is then unsatisfiable % 82.73/43.10 |-Branch two: % 82.73/43.10 | (493) sdtpldt0(xp, all_25_0_5) = xp % 82.73/43.10 | (613) ? [v0] : (sdtpldt0(all_25_0_5, xm) = v0 & sdtpldt0(xp, v0) = all_15_0_4) % 82.73/43.10 | % 82.73/43.10 | From (385) and (493) follows: % 82.73/43.10 | (480) sdtpldt0(xp, xp) = xp % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (289), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (504) ~ (sdtpldt0(xn, xp) = xr) % 82.77/43.10 | % 82.77/43.10 | From (373) and (504) follows: % 82.77/43.10 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.77/43.10 | % 82.77/43.10 | Using (393) and (395) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (507) sdtpldt0(xn, xp) = xr % 82.77/43.10 | (619) ? [v0] : (sdtpldt0(xp, xm) = v0 & sdtpldt0(xn, v0) = all_101_0_15) % 82.77/43.10 | % 82.77/43.10 | Instantiating (619) with all_636_0_100 yields: % 82.77/43.10 | (620) sdtpldt0(xp, xm) = all_636_0_100 & sdtpldt0(xn, all_636_0_100) = all_101_0_15 % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (620) yields: % 82.77/43.10 | (621) sdtpldt0(xp, xm) = all_636_0_100 % 82.77/43.10 | (622) sdtpldt0(xn, all_636_0_100) = all_101_0_15 % 82.77/43.10 | % 82.77/43.10 | From (373) and (507) follows: % 82.77/43.10 | (393) sdtpldt0(xn, xp) = xn % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (263), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (624) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = xp) % 82.77/43.10 | % 82.77/43.10 | From (385)(385) and (624) follows: % 82.77/43.10 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.77/43.10 | % 82.77/43.10 | Using (480) and (491) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (627) sdtpldt0(all_25_0_5, all_25_0_5) = xp % 82.77/43.10 | (628) ? [v0] : (sdtpldt0(all_25_0_5, v0) = xn & sdtpldt0(all_25_0_5, xr) = v0) % 82.77/43.10 | % 82.77/43.10 | From (385)(385) and (627) follows: % 82.77/43.10 | (480) sdtpldt0(xp, xp) = xp % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (276), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.77/43.10 | % 82.77/43.10 | Using (480) and (491) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (480) sdtpldt0(xp, xp) = xp % 82.77/43.10 | (633) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v0, all_59_0_7) = v1 & sdtasdt0(all_59_0_7, v0) = xp & sdtasdt0(xp, all_59_0_7) = v3 & sdtasdt0(xp, all_59_0_7) = v2 & sdtpldt0(v2, v3) = v1 & sdtpldt0(xp, xp) = v0) % 82.77/43.10 | % 82.77/43.10 | Instantiating (633) with all_665_0_103, all_665_1_104, all_665_2_105, all_665_3_106 yields: % 82.77/43.10 | (634) sdtasdt0(all_665_3_106, all_59_0_7) = all_665_2_105 & sdtasdt0(all_59_0_7, all_665_3_106) = xp & sdtasdt0(xp, all_59_0_7) = all_665_0_103 & sdtasdt0(xp, all_59_0_7) = all_665_1_104 & sdtpldt0(all_665_1_104, all_665_0_103) = all_665_2_105 & sdtpldt0(xp, xp) = all_665_3_106 % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (634) yields: % 82.77/43.10 | (635) sdtasdt0(xp, all_59_0_7) = all_665_1_104 % 82.77/43.10 | (636) sdtasdt0(xp, all_59_0_7) = all_665_0_103 % 82.77/43.10 | (637) sdtasdt0(all_665_3_106, all_59_0_7) = all_665_2_105 % 82.77/43.10 | (638) sdtpldt0(all_665_1_104, all_665_0_103) = all_665_2_105 % 82.77/43.10 | (639) sdtasdt0(all_59_0_7, all_665_3_106) = xp % 82.77/43.10 | (640) sdtpldt0(xp, xp) = all_665_3_106 % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (275), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.77/43.10 | % 82.77/43.10 | Using (480) and (491) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (480) sdtpldt0(xp, xp) = xp % 82.77/43.10 | (644) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v0, xp) = v1 & sdtasdt0(all_59_0_7, xp) = v3 & sdtasdt0(all_59_0_7, xp) = v2 & sdtasdt0(xp, v0) = xp & sdtpldt0(v2, v3) = v1 & sdtpldt0(all_59_0_7, all_59_0_7) = v0) % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (286), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (381) ~ (sdtpldt0(xr, all_25_0_5) = xn) % 82.77/43.10 | % 82.77/43.10 | From (373)(385) and (381) follows: % 82.77/43.10 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.77/43.10 | % 82.77/43.10 | Using (393) and (395) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (384) sdtpldt0(xr, all_25_0_5) = xn % 82.77/43.10 | (649) ? [v0] : (sdtpldt0(all_25_0_5, xp) = v0 & sdtpldt0(xr, v0) = all_97_0_13) % 82.77/43.10 | % 82.77/43.10 | Instantiating (649) with all_676_0_111 yields: % 82.77/43.10 | (650) sdtpldt0(all_25_0_5, xp) = all_676_0_111 & sdtpldt0(xr, all_676_0_111) = all_97_0_13 % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (650) yields: % 82.77/43.10 | (651) sdtpldt0(all_25_0_5, xp) = all_676_0_111 % 82.77/43.10 | (652) sdtpldt0(xr, all_676_0_111) = all_97_0_13 % 82.77/43.10 | % 82.77/43.10 | From (385) and (651) follows: % 82.77/43.10 | (653) sdtpldt0(xp, xp) = all_676_0_111 % 82.77/43.10 | % 82.77/43.10 | From (373)(385) and (384) follows: % 82.77/43.10 | (393) sdtpldt0(xn, xp) = xn % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (281), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (655) ~ (sdtpldt0(xm, all_25_0_5) = xm) % 82.77/43.10 | % 82.77/43.10 | From (385) and (655) follows: % 82.77/43.10 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.77/43.10 | % 82.77/43.10 | Using (391) and (437) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (380) sdtpldt0(xm, all_25_0_5) = xm % 82.77/43.10 | (659) ? [v0] : (sdtpldt0(all_25_0_5, xp) = v0 & sdtpldt0(xm, v0) = all_15_0_4) % 82.77/43.10 | % 82.77/43.10 | Instantiating (659) with all_682_0_112 yields: % 82.77/43.10 | (660) sdtpldt0(all_25_0_5, xp) = all_682_0_112 & sdtpldt0(xm, all_682_0_112) = all_15_0_4 % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (660) yields: % 82.77/43.10 | (661) sdtpldt0(all_25_0_5, xp) = all_682_0_112 % 82.77/43.10 | (662) sdtpldt0(xm, all_682_0_112) = all_15_0_4 % 82.77/43.10 | % 82.77/43.10 | From (385) and (661) follows: % 82.77/43.10 | (663) sdtpldt0(xp, xp) = all_682_0_112 % 82.77/43.10 | % 82.77/43.10 | From (385) and (380) follows: % 82.77/43.10 | (391) sdtpldt0(xm, xp) = xm % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (319), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (665) ~ (sdtpldt0(xp, all_107_0_18) = xp) % 82.77/43.10 | % 82.77/43.10 | From (597) and (665) follows: % 82.77/43.10 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.77/43.10 | % 82.77/43.10 | Using (480) and (491) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (668) sdtpldt0(xp, all_107_0_18) = xp % 82.77/43.10 | (669) ? [v0] : (sdtpldt0(all_105_0_17, all_107_0_18) = v0 & sdtpldt0(sz10, v0) = xp) % 82.77/43.10 | % 82.77/43.10 | From (597) and (668) follows: % 82.77/43.10 | (480) sdtpldt0(xp, xp) = xp % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (270), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (671) ~ (sdtpldt0(xp, xn) = xn) % 82.77/43.10 | % 82.77/43.10 | Using (477) and (671) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (477) sdtpldt0(xp, xn) = xn % 82.77/43.10 | (674) ~ (sdtpldt0(xn, xp) = xn) | ? [v0] : (sdtpldt0(xp, v0) = xn & sdtpldt0(xn, xp) = v0) % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (674), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.77/43.10 | % 82.77/43.10 | Using (393) and (395) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (393) sdtpldt0(xn, xp) = xn % 82.77/43.10 | (678) ? [v0] : (sdtpldt0(xp, v0) = xn & sdtpldt0(xn, xp) = v0) % 82.77/43.10 | % 82.77/43.10 | Instantiating (678) with all_697_0_114 yields: % 82.77/43.10 | (679) sdtpldt0(xp, all_697_0_114) = xn & sdtpldt0(xn, xp) = all_697_0_114 % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (679) yields: % 82.77/43.10 | (680) sdtpldt0(xp, all_697_0_114) = xn % 82.77/43.10 | (681) sdtpldt0(xn, xp) = all_697_0_114 % 82.77/43.10 | % 82.77/43.10 +-Applying beta-rule and splitting (316), into two cases. % 82.77/43.10 |-Branch one: % 82.77/43.10 | (682) ~ (sdtpldt0(xn, all_107_0_18) = xn) % 82.77/43.10 | % 82.77/43.10 | From (597) and (682) follows: % 82.77/43.10 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.77/43.10 | % 82.77/43.10 | Using (393) and (395) yields: % 82.77/43.10 | (97) $false % 82.77/43.10 | % 82.77/43.10 |-The branch is then unsatisfiable % 82.77/43.10 |-Branch two: % 82.77/43.10 | (685) sdtpldt0(xn, all_107_0_18) = xn % 82.77/43.10 | (686) ? [v0] : (sdtpldt0(all_25_0_5, all_107_0_18) = v0 & sdtpldt0(xn, v0) = xn) % 82.77/43.10 | % 82.77/43.10 | Instantiating (686) with all_703_0_115 yields: % 82.77/43.10 | (687) sdtpldt0(all_25_0_5, all_107_0_18) = all_703_0_115 & sdtpldt0(xn, all_703_0_115) = xn % 82.77/43.10 | % 82.77/43.10 | Applying alpha-rule on (687) yields: % 82.77/43.10 | (688) sdtpldt0(all_25_0_5, all_107_0_18) = all_703_0_115 % 82.77/43.10 | (689) sdtpldt0(xn, all_703_0_115) = xn % 82.77/43.11 | % 82.77/43.11 | From (385)(597) and (688) follows: % 82.77/43.11 | (690) sdtpldt0(xp, xp) = all_703_0_115 % 82.77/43.11 | % 82.77/43.11 | From (597) and (685) follows: % 82.77/43.11 | (393) sdtpldt0(xn, xp) = xn % 82.77/43.11 | % 82.77/43.11 +-Applying beta-rule and splitting (327), into two cases. % 82.77/43.11 |-Branch one: % 82.77/43.11 | (692) ~ (sdtpldt0(all_25_0_5, all_15_0_4) = xm) % 82.77/43.11 | % 82.77/43.11 | From (385)(440) and (692) follows: % 82.77/43.11 | (693) ~ (sdtpldt0(xp, xm) = xm) % 82.77/43.11 | % 82.77/43.11 | Using (599) and (693) yields: % 82.77/43.11 | (97) $false % 82.77/43.11 | % 82.77/43.11 |-The branch is then unsatisfiable % 82.77/43.11 |-Branch two: % 82.77/43.11 | (695) sdtpldt0(all_25_0_5, all_15_0_4) = xm % 82.77/43.11 | (696) ? [v0] : (sdtpldt0(all_25_0_5, v0) = xm & sdtpldt0(all_15_0_4, all_107_0_18) = v0) % 82.77/43.11 | % 82.77/43.11 | From (385)(440) and (695) follows: % 82.77/43.11 | (599) sdtpldt0(xp, xm) = xm % 82.77/43.11 | % 82.77/43.11 +-Applying beta-rule and splitting (318), into two cases. % 82.77/43.11 |-Branch one: % 82.77/43.11 | (698) ~ aNaturalNumber0(all_97_0_13) % 82.77/43.11 | % 82.77/43.11 | From (398) and (698) follows: % 82.77/43.11 | (699) ~ aNaturalNumber0(xn) % 82.81/43.11 | % 82.81/43.11 | Using (38) and (699) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (701) aNaturalNumber0(all_97_0_13) % 82.81/43.11 | (702) ? [v0] : (sdtpldt0(all_107_0_18, all_97_0_13) = v0 & sdtpldt0(xm, v0) = all_0_1_1) % 82.81/43.11 | % 82.81/43.11 | From (398) and (701) follows: % 82.81/43.11 | (38) aNaturalNumber0(xn) % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (314), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (655) ~ (sdtpldt0(xm, all_25_0_5) = xm) % 82.81/43.11 | % 82.81/43.11 | From (385) and (655) follows: % 82.81/43.11 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.81/43.11 | % 82.81/43.11 | Using (391) and (437) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (380) sdtpldt0(xm, all_25_0_5) = xm % 82.81/43.11 | (708) ? [v0] : (sdtpldt0(all_25_0_5, all_25_0_5) = v0 & sdtpldt0(xm, v0) = xm) % 82.81/43.11 | % 82.81/43.11 | Instantiating (708) with all_721_0_118 yields: % 82.81/43.11 | (709) sdtpldt0(all_25_0_5, all_25_0_5) = all_721_0_118 & sdtpldt0(xm, all_721_0_118) = xm % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (709) yields: % 82.81/43.11 | (710) sdtpldt0(all_25_0_5, all_25_0_5) = all_721_0_118 % 82.81/43.11 | (711) sdtpldt0(xm, all_721_0_118) = xm % 82.81/43.11 | % 82.81/43.11 | From (385)(385) and (710) follows: % 82.81/43.11 | (712) sdtpldt0(xp, xp) = all_721_0_118 % 82.81/43.11 | % 82.81/43.11 | From (385) and (380) follows: % 82.81/43.11 | (391) sdtpldt0(xm, xp) = xm % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (278), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (624) ~ (sdtpldt0(all_25_0_5, all_25_0_5) = xp) % 82.81/43.11 | % 82.81/43.11 | From (385)(385) and (624) follows: % 82.81/43.11 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.81/43.11 | % 82.81/43.11 | Using (480) and (491) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (627) sdtpldt0(all_25_0_5, all_25_0_5) = xp % 82.81/43.11 | (718) ? [v0] : (sdtpldt0(all_25_0_5, v0) = all_15_0_4 & sdtpldt0(all_25_0_5, xm) = v0) % 82.81/43.11 | % 82.81/43.11 | Instantiating (718) with all_727_0_119 yields: % 82.81/43.11 | (719) sdtpldt0(all_25_0_5, all_727_0_119) = all_15_0_4 & sdtpldt0(all_25_0_5, xm) = all_727_0_119 % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (719) yields: % 82.81/43.11 | (720) sdtpldt0(all_25_0_5, all_727_0_119) = all_15_0_4 % 82.81/43.11 | (721) sdtpldt0(all_25_0_5, xm) = all_727_0_119 % 82.81/43.11 | % 82.81/43.11 | From (385)(385) and (627) follows: % 82.81/43.11 | (480) sdtpldt0(xp, xp) = xp % 82.81/43.11 | % 82.81/43.11 | From (385) and (721) follows: % 82.81/43.11 | (723) sdtpldt0(xp, xm) = all_727_0_119 % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (330), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (724) ~ sdtlseqdt0(xr, all_0_1_1) % 82.81/43.11 | % 82.81/43.11 | From (373)(426) and (724) follows: % 82.81/43.11 | (725) ~ sdtlseqdt0(xn, all_0_2_2) % 82.81/43.11 | % 82.81/43.11 | Using (156) and (725) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (727) sdtlseqdt0(xr, all_0_1_1) % 82.81/43.11 | (728) ? [v0] : (sdtpldt0(xr, v0) = all_0_1_1 & aNaturalNumber0(v0)) % 82.81/43.11 | % 82.81/43.11 | Instantiating (728) with all_747_0_123 yields: % 82.81/43.11 | (729) sdtpldt0(xr, all_747_0_123) = all_0_1_1 & aNaturalNumber0(all_747_0_123) % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (729) yields: % 82.81/43.11 | (730) sdtpldt0(xr, all_747_0_123) = all_0_1_1 % 82.81/43.11 | (731) aNaturalNumber0(all_747_0_123) % 82.81/43.11 | % 82.81/43.11 | From (373)(426) and (730) follows: % 82.81/43.11 | (732) sdtpldt0(xn, all_747_0_123) = all_0_2_2 % 82.81/43.11 | % 82.81/43.11 | From (373)(426) and (727) follows: % 82.81/43.11 | (156) sdtlseqdt0(xn, all_0_2_2) % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (331), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (734) ~ sdtlseqdt0(xn, all_0_1_1) % 82.81/43.11 | % 82.81/43.11 | From (426) and (734) follows: % 82.81/43.11 | (725) ~ sdtlseqdt0(xn, all_0_2_2) % 82.81/43.11 | % 82.81/43.11 | Using (156) and (725) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (323) sdtlseqdt0(xn, all_0_1_1) % 82.81/43.11 | (738) ? [v0] : (sdtpldt0(xn, v0) = all_0_1_1 & aNaturalNumber0(v0)) % 82.81/43.11 | % 82.81/43.11 | Instantiating (738) with all_752_0_124 yields: % 82.81/43.11 | (739) sdtpldt0(xn, all_752_0_124) = all_0_1_1 & aNaturalNumber0(all_752_0_124) % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (739) yields: % 82.81/43.11 | (740) sdtpldt0(xn, all_752_0_124) = all_0_1_1 % 82.81/43.11 | (741) aNaturalNumber0(all_752_0_124) % 82.81/43.11 | % 82.81/43.11 | From (426) and (740) follows: % 82.81/43.11 | (742) sdtpldt0(xn, all_752_0_124) = all_0_2_2 % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (308), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.81/43.11 | % 82.81/43.11 | From (476) and (366) follows: % 82.81/43.11 | (538) ~ aNaturalNumber0(xp) % 82.81/43.11 | % 82.81/43.11 | Using (17) and (538) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (264) aNaturalNumber0(all_91_0_10) % 82.81/43.11 | (747) ? [v0] : (sdtpldt0(all_91_0_10, xp) = v0 & sdtpldt0(xn, v0) = all_97_0_13) % 82.81/43.11 | % 82.81/43.11 | Instantiating (747) with all_768_0_129 yields: % 82.81/43.11 | (748) sdtpldt0(all_91_0_10, xp) = all_768_0_129 & sdtpldt0(xn, all_768_0_129) = all_97_0_13 % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (748) yields: % 82.81/43.11 | (749) sdtpldt0(all_91_0_10, xp) = all_768_0_129 % 82.81/43.11 | (750) sdtpldt0(xn, all_768_0_129) = all_97_0_13 % 82.81/43.11 | % 82.81/43.11 | From (476) and (749) follows: % 82.81/43.11 | (751) sdtpldt0(xp, xp) = all_768_0_129 % 82.81/43.11 | % 82.81/43.11 | From (476) and (264) follows: % 82.81/43.11 | (17) aNaturalNumber0(xp) % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (315), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (437) ~ (sdtpldt0(xm, xp) = xm) % 82.81/43.11 | % 82.81/43.11 | Using (391) and (437) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (391) sdtpldt0(xm, xp) = xm % 82.81/43.11 | (756) ? [v0] : (sdtpldt0(xp, all_107_0_18) = v0 & sdtpldt0(xm, v0) = xm) % 82.81/43.11 | % 82.81/43.11 | Instantiating (756) with all_774_0_130 yields: % 82.81/43.11 | (757) sdtpldt0(xp, all_107_0_18) = all_774_0_130 & sdtpldt0(xm, all_774_0_130) = xm % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (757) yields: % 82.81/43.11 | (758) sdtpldt0(xp, all_107_0_18) = all_774_0_130 % 82.81/43.11 | (759) sdtpldt0(xm, all_774_0_130) = xm % 82.81/43.11 | % 82.81/43.11 | From (597) and (758) follows: % 82.81/43.11 | (760) sdtpldt0(xp, xp) = all_774_0_130 % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (296), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (362) ~ aNaturalNumber0(all_103_0_16) % 82.81/43.11 | % 82.81/43.11 | From (379) and (362) follows: % 82.81/43.11 | (573) ~ aNaturalNumber0(xm) % 82.81/43.11 | % 82.81/43.11 | Using (16) and (573) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (269) aNaturalNumber0(all_103_0_16) % 82.81/43.11 | (765) ? [v0] : (sdtpldt0(all_103_0_16, xp) = v0 & sdtpldt0(xn, v0) = all_0_1_1) % 82.81/43.11 | % 82.81/43.11 | From (379) and (269) follows: % 82.81/43.11 | (16) aNaturalNumber0(xm) % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (298), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (366) ~ aNaturalNumber0(all_91_0_10) % 82.81/43.11 | % 82.81/43.11 | From (476) and (366) follows: % 82.81/43.11 | (538) ~ aNaturalNumber0(xp) % 82.81/43.11 | % 82.81/43.11 | Using (17) and (538) yields: % 82.81/43.11 | (97) $false % 82.81/43.11 | % 82.81/43.11 |-The branch is then unsatisfiable % 82.81/43.11 |-Branch two: % 82.81/43.11 | (264) aNaturalNumber0(all_91_0_10) % 82.81/43.11 | (771) ? [v0] : (sdtpldt0(all_91_0_10, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.81/43.11 | % 82.81/43.11 | Instantiating (771) with all_786_0_132 yields: % 82.81/43.11 | (772) sdtpldt0(all_91_0_10, xm) = all_786_0_132 & sdtpldt0(xn, all_786_0_132) = all_0_2_2 % 82.81/43.11 | % 82.81/43.11 | Applying alpha-rule on (772) yields: % 82.81/43.11 | (773) sdtpldt0(all_91_0_10, xm) = all_786_0_132 % 82.81/43.11 | (774) sdtpldt0(xn, all_786_0_132) = all_0_2_2 % 82.81/43.11 | % 82.81/43.11 | From (476) and (773) follows: % 82.81/43.11 | (775) sdtpldt0(xp, xm) = all_786_0_132 % 82.81/43.11 | % 82.81/43.11 | From (476) and (264) follows: % 82.81/43.11 | (17) aNaturalNumber0(xp) % 82.81/43.11 | % 82.81/43.11 +-Applying beta-rule and splitting (312), into two cases. % 82.81/43.11 |-Branch one: % 82.81/43.11 | (665) ~ (sdtpldt0(xp, all_107_0_18) = xp) % 82.81/43.11 | % 82.81/43.11 | From (597) and (665) follows: % 82.81/43.11 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.81/43.12 | % 82.81/43.12 | Using (480) and (491) yields: % 82.81/43.12 | (97) $false % 82.81/43.12 | % 82.81/43.12 |-The branch is then unsatisfiable % 82.81/43.12 |-Branch two: % 82.81/43.12 | (668) sdtpldt0(xp, all_107_0_18) = xp % 82.81/43.12 | (781) ? [v0] : (sdtpldt0(all_107_0_18, all_107_0_18) = v0 & sdtpldt0(xp, v0) = xp) % 82.81/43.12 | % 82.81/43.12 | Instantiating (781) with all_792_0_133 yields: % 82.81/43.12 | (782) sdtpldt0(all_107_0_18, all_107_0_18) = all_792_0_133 & sdtpldt0(xp, all_792_0_133) = xp % 82.81/43.12 | % 82.81/43.12 | Applying alpha-rule on (782) yields: % 82.81/43.12 | (783) sdtpldt0(all_107_0_18, all_107_0_18) = all_792_0_133 % 82.81/43.12 | (784) sdtpldt0(xp, all_792_0_133) = xp % 82.81/43.12 | % 82.81/43.12 | From (597)(597) and (783) follows: % 82.81/43.12 | (785) sdtpldt0(xp, xp) = all_792_0_133 % 82.81/43.12 | % 82.81/43.12 | From (597) and (668) follows: % 82.81/43.12 | (480) sdtpldt0(xp, xp) = xp % 82.81/43.12 | % 82.81/43.12 +-Applying beta-rule and splitting (313), into two cases. % 82.81/43.12 |-Branch one: % 82.81/43.12 | (665) ~ (sdtpldt0(xp, all_107_0_18) = xp) % 82.81/43.12 | % 82.81/43.12 | From (597) and (665) follows: % 82.81/43.12 | (491) ~ (sdtpldt0(xp, xp) = xp) % 82.81/43.12 | % 82.81/43.12 | Using (480) and (491) yields: % 82.81/43.12 | (97) $false % 82.81/43.12 | % 82.81/43.12 |-The branch is then unsatisfiable % 82.81/43.12 |-Branch two: % 82.81/43.12 | (668) sdtpldt0(xp, all_107_0_18) = xp % 82.81/43.12 | (791) ? [v0] : (sdtpldt0(all_107_0_18, xm) = v0 & sdtpldt0(xp, v0) = all_15_0_4) % 82.81/43.12 | % 82.81/43.12 | Instantiating (791) with all_798_0_134 yields: % 82.81/43.12 | (792) sdtpldt0(all_107_0_18, xm) = all_798_0_134 & sdtpldt0(xp, all_798_0_134) = all_15_0_4 % 82.81/43.12 | % 82.81/43.12 | Applying alpha-rule on (792) yields: % 82.81/43.12 | (793) sdtpldt0(all_107_0_18, xm) = all_798_0_134 % 82.81/43.12 | (794) sdtpldt0(xp, all_798_0_134) = all_15_0_4 % 82.81/43.12 | % 82.81/43.12 | From (597) and (793) follows: % 82.81/43.12 | (795) sdtpldt0(xp, xm) = all_798_0_134 % 82.81/43.12 | % 82.81/43.12 | From (597) and (668) follows: % 82.81/43.12 | (480) sdtpldt0(xp, xp) = xp % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_768_0_129, all_774_0_130 and discharging atoms sdtpldt0(xp, xp) = all_774_0_130, sdtpldt0(xp, xp) = all_768_0_129, yields: % 82.81/43.12 | (797) all_774_0_130 = all_768_0_129 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_721_0_118, all_774_0_130 and discharging atoms sdtpldt0(xp, xp) = all_774_0_130, sdtpldt0(xp, xp) = all_721_0_118, yields: % 82.81/43.12 | (798) all_774_0_130 = all_721_0_118 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_703_0_115, xp and discharging atoms sdtpldt0(xp, xp) = all_703_0_115, sdtpldt0(xp, xp) = xp, yields: % 82.81/43.12 | (799) all_703_0_115 = xp % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_682_0_112, all_792_0_133 and discharging atoms sdtpldt0(xp, xp) = all_792_0_133, sdtpldt0(xp, xp) = all_682_0_112, yields: % 82.81/43.12 | (800) all_792_0_133 = all_682_0_112 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_676_0_111, all_682_0_112 and discharging atoms sdtpldt0(xp, xp) = all_682_0_112, sdtpldt0(xp, xp) = all_676_0_111, yields: % 82.81/43.12 | (801) all_682_0_112 = all_676_0_111 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_665_3_106, all_676_0_111 and discharging atoms sdtpldt0(xp, xp) = all_676_0_111, sdtpldt0(xp, xp) = all_665_3_106, yields: % 82.81/43.12 | (802) all_676_0_111 = all_665_3_106 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_616_0_97, all_768_0_129 and discharging atoms sdtpldt0(xp, xp) = all_768_0_129, sdtpldt0(xp, xp) = all_616_0_97, yields: % 82.81/43.12 | (803) all_768_0_129 = all_616_0_97 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_616_0_97, all_665_3_106 and discharging atoms sdtpldt0(xp, xp) = all_665_3_106, sdtpldt0(xp, xp) = all_616_0_97, yields: % 82.81/43.12 | (804) all_665_3_106 = all_616_0_97 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_531_0_84, all_792_0_133 and discharging atoms sdtpldt0(xp, xp) = all_792_0_133, sdtpldt0(xp, xp) = all_531_0_84, yields: % 82.81/43.12 | (805) all_792_0_133 = all_531_0_84 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_520_0_82, all_616_0_97 and discharging atoms sdtpldt0(xp, xp) = all_616_0_97, sdtpldt0(xp, xp) = all_520_0_82, yields: % 82.81/43.12 | (806) all_616_0_97 = all_520_0_82 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_460_0_77, all_520_0_82 and discharging atoms sdtpldt0(xp, xp) = all_520_0_82, sdtpldt0(xp, xp) = all_460_0_77, yields: % 82.81/43.12 | (807) all_520_0_82 = all_460_0_77 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_426_0_73, all_460_0_77 and discharging atoms sdtpldt0(xp, xp) = all_460_0_77, sdtpldt0(xp, xp) = all_426_0_73, yields: % 82.81/43.12 | (808) all_460_0_77 = all_426_0_73 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_352_0_67, all_703_0_115 and discharging atoms sdtpldt0(xp, xp) = all_703_0_115, sdtpldt0(xp, xp) = all_352_0_67, yields: % 82.81/43.12 | (809) all_703_0_115 = all_352_0_67 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_352_0_67, all_426_0_73 and discharging atoms sdtpldt0(xp, xp) = all_426_0_73, sdtpldt0(xp, xp) = all_352_0_67, yields: % 82.81/43.12 | (810) all_426_0_73 = all_352_0_67 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_347_0_66, all_768_0_129 and discharging atoms sdtpldt0(xp, xp) = all_768_0_129, sdtpldt0(xp, xp) = all_347_0_66, yields: % 82.81/43.12 | (811) all_768_0_129 = all_347_0_66 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_306_0_59, all_352_0_67 and discharging atoms sdtpldt0(xp, xp) = all_352_0_67, sdtpldt0(xp, xp) = all_306_0_59, yields: % 82.81/43.12 | (812) all_352_0_67 = all_306_0_59 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_268_0_40, all_306_0_59 and discharging atoms sdtpldt0(xp, xp) = all_306_0_59, sdtpldt0(xp, xp) = all_268_0_40, yields: % 82.81/43.12 | (813) all_306_0_59 = all_268_0_40 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_262_0_37, all_268_0_40 and discharging atoms sdtpldt0(xp, xp) = all_268_0_40, sdtpldt0(xp, xp) = all_262_0_37, yields: % 82.81/43.12 | (814) all_268_0_40 = all_262_0_37 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xp, all_250_0_31, all_262_0_37 and discharging atoms sdtpldt0(xp, xp) = all_262_0_37, sdtpldt0(xp, xp) = all_250_0_31, yields: % 82.81/43.12 | (815) all_262_0_37 = all_250_0_31 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_727_0_119, xm and discharging atoms sdtpldt0(xp, xm) = all_727_0_119, sdtpldt0(xp, xm) = xm, yields: % 82.81/43.12 | (816) all_727_0_119 = xm % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_727_0_119, all_786_0_132 and discharging atoms sdtpldt0(xp, xm) = all_786_0_132, sdtpldt0(xp, xm) = all_727_0_119, yields: % 82.81/43.12 | (817) all_786_0_132 = all_727_0_119 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_636_0_100, all_786_0_132 and discharging atoms sdtpldt0(xp, xm) = all_786_0_132, sdtpldt0(xp, xm) = all_636_0_100, yields: % 82.81/43.12 | (818) all_786_0_132 = all_636_0_100 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_596_0_95, all_786_0_132 and discharging atoms sdtpldt0(xp, xm) = all_786_0_132, sdtpldt0(xp, xm) = all_596_0_95, yields: % 82.81/43.12 | (819) all_786_0_132 = all_596_0_95 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_584_0_93, all_596_0_95 and discharging atoms sdtpldt0(xp, xm) = all_596_0_95, sdtpldt0(xp, xm) = all_584_0_93, yields: % 82.81/43.12 | (820) all_596_0_95 = all_584_0_93 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_557_0_87, all_238_0_25 and discharging atoms sdtpldt0(xp, xm) = all_557_0_87, yields: % 82.81/43.12 | (821) all_557_0_87 = all_238_0_25 | ~ (sdtpldt0(xp, xm) = all_238_0_25) % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_557_0_87, all_798_0_134 and discharging atoms sdtpldt0(xp, xm) = all_798_0_134, sdtpldt0(xp, xm) = all_557_0_87, yields: % 82.81/43.12 | (822) all_798_0_134 = all_557_0_87 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_543_0_86, all_584_0_93 and discharging atoms sdtpldt0(xp, xm) = all_584_0_93, sdtpldt0(xp, xm) = all_543_0_86, yields: % 82.81/43.12 | (823) all_584_0_93 = all_543_0_86 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_543_0_86, all_557_0_87 and discharging atoms sdtpldt0(xp, xm) = all_557_0_87, sdtpldt0(xp, xm) = all_543_0_86, yields: % 82.81/43.12 | (824) all_557_0_87 = all_543_0_86 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_537_0_85, all_557_0_87 and discharging atoms sdtpldt0(xp, xm) = all_557_0_87, sdtpldt0(xp, xm) = all_537_0_85, yields: % 82.81/43.12 | (825) all_557_0_87 = all_537_0_85 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xp, xm, all_310_0_61, all_798_0_134 and discharging atoms sdtpldt0(xp, xm) = all_798_0_134, sdtpldt0(xp, xm) = all_310_0_61, yields: % 82.81/43.12 | (826) all_798_0_134 = all_310_0_61 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with xm, xp, sz00, xm and discharging atoms sdtpldt0(xm, xp) = xm, aNaturalNumber0(xp), aNaturalNumber0(xm), aNaturalNumber0(sz00), yields: % 82.81/43.12 | (827) xp = sz00 | ~ (sdtpldt0(xm, sz00) = xm) % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xn, xp, all_697_0_114, xn and discharging atoms sdtpldt0(xn, xp) = all_697_0_114, sdtpldt0(xn, xp) = xn, yields: % 82.81/43.12 | (828) all_697_0_114 = xn % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xn, xp, all_357_0_68, all_697_0_114 and discharging atoms sdtpldt0(xn, xp) = all_697_0_114, sdtpldt0(xn, xp) = all_357_0_68, yields: % 82.81/43.12 | (829) all_697_0_114 = all_357_0_68 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xn, xp, all_357_0_68, all_606_0_96 and discharging atoms sdtpldt0(xn, xp) = all_606_0_96, sdtpldt0(xn, xp) = all_357_0_68, yields: % 82.81/43.12 | (830) all_606_0_96 = all_357_0_68 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xn, xp, all_296_0_54, all_606_0_96 and discharging atoms sdtpldt0(xn, xp) = all_606_0_96, sdtpldt0(xn, xp) = all_296_0_54, yields: % 82.81/43.12 | (831) all_606_0_96 = all_296_0_54 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (24) with xn, xp, all_294_0_53, all_606_0_96 and discharging atoms sdtpldt0(xn, xp) = all_606_0_96, sdtpldt0(xn, xp) = all_294_0_53, yields: % 82.81/43.12 | (832) all_606_0_96 = all_294_0_53 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with xp, all_109_0_19, all_284_0_48, xp and discharging atoms sdtpldt0(xp, all_284_0_48) = xp, sdtpldt0(xp, all_109_0_19) = xp, aNaturalNumber0(all_284_0_48), aNaturalNumber0(all_109_0_19), aNaturalNumber0(xp), yields: % 82.81/43.12 | (833) all_284_0_48 = all_109_0_19 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with all_0_2_2, xm, all_747_0_123, xn and discharging atoms sdtpldt0(xn, all_747_0_123) = all_0_2_2, sdtpldt0(xn, xm) = all_0_2_2, aNaturalNumber0(all_747_0_123), aNaturalNumber0(xm), aNaturalNumber0(xn), yields: % 82.81/43.12 | (834) all_747_0_123 = xm % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with xp, all_284_0_48, xp, xp and discharging atoms sdtpldt0(xp, all_284_0_48) = xp, sdtpldt0(xp, xp) = xp, aNaturalNumber0(all_284_0_48), aNaturalNumber0(xp), yields: % 82.81/43.12 | (835) all_284_0_48 = xp % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with all_0_2_2, all_752_0_124, all_747_0_123, xn and discharging atoms sdtpldt0(xn, all_752_0_124) = all_0_2_2, sdtpldt0(xn, all_747_0_123) = all_0_2_2, aNaturalNumber0(all_752_0_124), aNaturalNumber0(all_747_0_123), aNaturalNumber0(xn), yields: % 82.81/43.12 | (836) all_752_0_124 = all_747_0_123 % 82.81/43.12 | % 82.81/43.12 | Instantiating formula (41) with all_0_2_2, all_752_0_124, all_270_0_41, xn and discharging atoms sdtpldt0(xn, all_752_0_124) = all_0_2_2, sdtpldt0(xn, all_270_0_41) = all_0_2_2, aNaturalNumber0(all_752_0_124), aNaturalNumber0(all_270_0_41), aNaturalNumber0(xn), yields: % 82.81/43.12 | (837) all_752_0_124 = all_270_0_41 % 82.81/43.12 | % 82.81/43.12 | Using (400) and (436) yields: % 82.81/43.12 | (838) ~ (all_250_0_31 = sz00) % 82.81/43.12 | % 82.81/43.12 | Combining equations (822,826) yields a new equation: % 82.81/43.12 | (839) all_557_0_87 = all_310_0_61 % 82.81/43.12 | % 82.81/43.12 | Simplifying 839 yields: % 82.81/43.12 | (840) all_557_0_87 = all_310_0_61 % 82.81/43.12 | % 82.81/43.12 | Combining equations (800,805) yields a new equation: % 82.81/43.12 | (841) all_682_0_112 = all_531_0_84 % 82.81/43.12 | % 82.81/43.12 | Simplifying 841 yields: % 82.81/43.12 | (842) all_682_0_112 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Combining equations (817,818) yields a new equation: % 82.81/43.13 | (843) all_727_0_119 = all_636_0_100 % 82.81/43.13 | % 82.81/43.13 | Simplifying 843 yields: % 82.81/43.13 | (844) all_727_0_119 = all_636_0_100 % 82.81/43.13 | % 82.81/43.13 | Combining equations (819,818) yields a new equation: % 82.81/43.13 | (845) all_636_0_100 = all_596_0_95 % 82.81/43.13 | % 82.81/43.13 | Combining equations (797,798) yields a new equation: % 82.81/43.13 | (846) all_768_0_129 = all_721_0_118 % 82.81/43.13 | % 82.81/43.13 | Simplifying 846 yields: % 82.81/43.13 | (847) all_768_0_129 = all_721_0_118 % 82.81/43.13 | % 82.81/43.13 | Combining equations (803,847) yields a new equation: % 82.81/43.13 | (848) all_721_0_118 = all_616_0_97 % 82.81/43.13 | % 82.81/43.13 | Combining equations (811,847) yields a new equation: % 82.81/43.13 | (849) all_721_0_118 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (836,837) yields a new equation: % 82.81/43.13 | (850) all_747_0_123 = all_270_0_41 % 82.81/43.13 | % 82.81/43.13 | Simplifying 850 yields: % 82.81/43.13 | (851) all_747_0_123 = all_270_0_41 % 82.81/43.13 | % 82.81/43.13 | Combining equations (851,834) yields a new equation: % 82.81/43.13 | (852) all_270_0_41 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 852 yields: % 82.81/43.13 | (853) all_270_0_41 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (844,816) yields a new equation: % 82.81/43.13 | (854) all_636_0_100 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 854 yields: % 82.81/43.13 | (855) all_636_0_100 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (848,849) yields a new equation: % 82.81/43.13 | (856) all_616_0_97 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Simplifying 856 yields: % 82.81/43.13 | (857) all_616_0_97 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (809,799) yields a new equation: % 82.81/43.13 | (858) all_352_0_67 = xp % 82.81/43.13 | % 82.81/43.13 | Simplifying 858 yields: % 82.81/43.13 | (859) all_352_0_67 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (829,828) yields a new equation: % 82.81/43.13 | (860) all_357_0_68 = xn % 82.81/43.13 | % 82.81/43.13 | Simplifying 860 yields: % 82.81/43.13 | (861) all_357_0_68 = xn % 82.81/43.13 | % 82.81/43.13 | Combining equations (801,842) yields a new equation: % 82.81/43.13 | (862) all_676_0_111 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Simplifying 862 yields: % 82.81/43.13 | (863) all_676_0_111 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Combining equations (802,863) yields a new equation: % 82.81/43.13 | (864) all_665_3_106 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Simplifying 864 yields: % 82.81/43.13 | (865) all_665_3_106 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Combining equations (804,865) yields a new equation: % 82.81/43.13 | (866) all_616_0_97 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Simplifying 866 yields: % 82.81/43.13 | (867) all_616_0_97 = all_531_0_84 % 82.81/43.13 | % 82.81/43.13 | Combining equations (845,855) yields a new equation: % 82.81/43.13 | (868) all_596_0_95 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 868 yields: % 82.81/43.13 | (869) all_596_0_95 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (806,867) yields a new equation: % 82.81/43.13 | (870) all_531_0_84 = all_520_0_82 % 82.81/43.13 | % 82.81/43.13 | Combining equations (857,867) yields a new equation: % 82.81/43.13 | (871) all_531_0_84 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (832,831) yields a new equation: % 82.81/43.13 | (872) all_296_0_54 = all_294_0_53 % 82.81/43.13 | % 82.81/43.13 | Combining equations (830,831) yields a new equation: % 82.81/43.13 | (873) all_357_0_68 = all_296_0_54 % 82.81/43.13 | % 82.81/43.13 | Simplifying 873 yields: % 82.81/43.13 | (874) all_357_0_68 = all_296_0_54 % 82.81/43.13 | % 82.81/43.13 | Combining equations (820,869) yields a new equation: % 82.81/43.13 | (875) all_584_0_93 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 875 yields: % 82.81/43.13 | (876) all_584_0_93 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (823,876) yields a new equation: % 82.81/43.13 | (877) all_543_0_86 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 877 yields: % 82.81/43.13 | (878) all_543_0_86 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (824,825) yields a new equation: % 82.81/43.13 | (879) all_543_0_86 = all_537_0_85 % 82.81/43.13 | % 82.81/43.13 | Simplifying 879 yields: % 82.81/43.13 | (880) all_543_0_86 = all_537_0_85 % 82.81/43.13 | % 82.81/43.13 | Combining equations (840,825) yields a new equation: % 82.81/43.13 | (881) all_537_0_85 = all_310_0_61 % 82.81/43.13 | % 82.81/43.13 | Combining equations (880,878) yields a new equation: % 82.81/43.13 | (882) all_537_0_85 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 882 yields: % 82.81/43.13 | (883) all_537_0_85 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (883,881) yields a new equation: % 82.81/43.13 | (884) all_310_0_61 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (870,871) yields a new equation: % 82.81/43.13 | (885) all_520_0_82 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Simplifying 885 yields: % 82.81/43.13 | (886) all_520_0_82 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (807,886) yields a new equation: % 82.81/43.13 | (887) all_460_0_77 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Simplifying 887 yields: % 82.81/43.13 | (888) all_460_0_77 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (808,888) yields a new equation: % 82.81/43.13 | (889) all_426_0_73 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Simplifying 889 yields: % 82.81/43.13 | (890) all_426_0_73 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (810,890) yields a new equation: % 82.81/43.13 | (891) all_352_0_67 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Simplifying 891 yields: % 82.81/43.13 | (892) all_352_0_67 = all_347_0_66 % 82.81/43.13 | % 82.81/43.13 | Combining equations (874,861) yields a new equation: % 82.81/43.13 | (893) all_296_0_54 = xn % 82.81/43.13 | % 82.81/43.13 | Simplifying 893 yields: % 82.81/43.13 | (894) all_296_0_54 = xn % 82.81/43.13 | % 82.81/43.13 | Combining equations (859,892) yields a new equation: % 82.81/43.13 | (895) all_347_0_66 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (812,892) yields a new equation: % 82.81/43.13 | (896) all_347_0_66 = all_306_0_59 % 82.81/43.13 | % 82.81/43.13 | Combining equations (896,895) yields a new equation: % 82.81/43.13 | (897) all_306_0_59 = xp % 82.81/43.13 | % 82.81/43.13 | Simplifying 897 yields: % 82.81/43.13 | (898) all_306_0_59 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (813,898) yields a new equation: % 82.81/43.13 | (899) all_268_0_40 = xp % 82.81/43.13 | % 82.81/43.13 | Simplifying 899 yields: % 82.81/43.13 | (900) all_268_0_40 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (872,894) yields a new equation: % 82.81/43.13 | (901) all_294_0_53 = xn % 82.81/43.13 | % 82.81/43.13 | Simplifying 901 yields: % 82.81/43.13 | (902) all_294_0_53 = xn % 82.81/43.13 | % 82.81/43.13 | Combining equations (835,833) yields a new equation: % 82.81/43.13 | (903) all_109_0_19 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (814,900) yields a new equation: % 82.81/43.13 | (904) all_262_0_37 = xp % 82.81/43.13 | % 82.81/43.13 | Simplifying 904 yields: % 82.81/43.13 | (905) all_262_0_37 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (815,905) yields a new equation: % 82.81/43.13 | (906) all_250_0_31 = xp % 82.81/43.13 | % 82.81/43.13 | Simplifying 906 yields: % 82.81/43.13 | (907) all_250_0_31 = xp % 82.81/43.13 | % 82.81/43.13 | Combining equations (884,881) yields a new equation: % 82.81/43.13 | (883) all_537_0_85 = xm % 82.81/43.13 | % 82.81/43.13 | Combining equations (883,825) yields a new equation: % 82.81/43.13 | (909) all_557_0_87 = xm % 82.81/43.13 | % 82.81/43.13 | Equations (907) can reduce 838 to: % 82.81/43.13 | (73) ~ (xp = sz00) % 82.81/43.13 | % 82.81/43.13 | From (903) and (333) follows: % 82.81/43.13 | (911) sdtpldt0(xp, xm) = all_238_0_25 % 82.81/43.13 | % 82.81/43.13 | From (902) and (352) follows: % 82.81/43.13 | (393) sdtpldt0(xn, xp) = xn % 82.81/43.13 | % 82.81/43.13 | From (853) and (346) follows: % 82.81/43.13 | (16) aNaturalNumber0(xm) % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (311), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (914) all_109_0_19 = sz00 % 82.81/43.13 | % 82.81/43.13 | Combining equations (903,914) yields a new equation: % 82.81/43.13 | (915) xp = sz00 % 82.81/43.13 | % 82.81/43.13 | Simplifying 915 yields: % 82.81/43.13 | (103) xp = sz00 % 82.81/43.13 | % 82.81/43.13 | Equations (103) can reduce 73 to: % 82.81/43.13 | (104) $false % 82.81/43.13 | % 82.81/43.13 |-The branch is then unsatisfiable % 82.81/43.13 |-Branch two: % 82.81/43.13 | (918) ~ (all_109_0_19 = sz00) % 82.81/43.13 | (919) all_109_0_19 = sz10 | ? [v0] : (isPrime0(v0) & doDivides0(v0, all_109_0_19) & aNaturalNumber0(v0)) % 82.81/43.13 | % 82.81/43.13 | Equations (903) can reduce 918 to: % 82.81/43.13 | (73) ~ (xp = sz00) % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (310), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (921) ~ (sdtpldt0(xn, all_109_0_19) = xn) % 82.81/43.13 | % 82.81/43.13 | From (903) and (921) follows: % 82.81/43.13 | (395) ~ (sdtpldt0(xn, xp) = xn) % 82.81/43.13 | % 82.81/43.13 | Using (393) and (395) yields: % 82.81/43.13 | (97) $false % 82.81/43.13 | % 82.81/43.13 |-The branch is then unsatisfiable % 82.81/43.13 |-Branch two: % 82.81/43.13 | (924) sdtpldt0(xn, all_109_0_19) = xn % 82.81/43.13 | (925) ? [v0] : (sdtpldt0(all_109_0_19, xm) = v0 & sdtpldt0(xn, v0) = all_0_2_2) % 82.81/43.13 | % 82.81/43.13 | Instantiating (925) with all_840_0_138 yields: % 82.81/43.13 | (926) sdtpldt0(all_109_0_19, xm) = all_840_0_138 & sdtpldt0(xn, all_840_0_138) = all_0_2_2 % 82.81/43.13 | % 82.81/43.13 | Applying alpha-rule on (926) yields: % 82.81/43.13 | (927) sdtpldt0(all_109_0_19, xm) = all_840_0_138 % 82.81/43.13 | (928) sdtpldt0(xn, all_840_0_138) = all_0_2_2 % 82.81/43.13 | % 82.81/43.13 | From (903) and (927) follows: % 82.81/43.13 | (929) sdtpldt0(xp, xm) = all_840_0_138 % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (821), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (930) ~ (sdtpldt0(xp, xm) = all_238_0_25) % 82.81/43.13 | % 82.81/43.13 | Using (911) and (930) yields: % 82.81/43.13 | (97) $false % 82.81/43.13 | % 82.81/43.13 |-The branch is then unsatisfiable % 82.81/43.13 |-Branch two: % 82.81/43.13 | (911) sdtpldt0(xp, xm) = all_238_0_25 % 82.81/43.13 | (933) all_557_0_87 = all_238_0_25 % 82.81/43.13 | % 82.81/43.13 | Combining equations (933,909) yields a new equation: % 82.81/43.13 | (934) all_238_0_25 = xm % 82.81/43.13 | % 82.81/43.13 | Simplifying 934 yields: % 82.81/43.13 | (935) all_238_0_25 = xm % 82.81/43.13 | % 82.81/43.13 | From (935) and (911) follows: % 82.81/43.13 | (599) sdtpldt0(xp, xm) = xm % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (827), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (937) ~ (sdtpldt0(xm, sz00) = xm) % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (325), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (938) ~ (sdtpldt0(sz00, all_15_0_4) = all_122_0_20) % 82.81/43.13 | % 82.81/43.13 | From (440)(467) and (938) follows: % 82.81/43.13 | (939) ~ (sdtpldt0(sz00, xm) = xm) % 82.81/43.13 | % 82.81/43.13 | Instantiating formula (24) with xp, xm, all_840_0_138, xm and discharging atoms sdtpldt0(xp, xm) = all_840_0_138, sdtpldt0(xp, xm) = xm, yields: % 82.81/43.13 | (940) all_840_0_138 = xm % 82.81/43.13 | % 82.81/43.13 | Using (929) and (445) yields: % 82.81/43.13 | (941) ~ (all_840_0_138 = sz00) % 82.81/43.13 | % 82.81/43.13 | Equations (940) can reduce 941 to: % 82.81/43.13 | (441) ~ (xm = sz00) % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (87), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.13 | % 82.81/43.13 +-Applying beta-rule and splitting (293), into two cases. % 82.81/43.13 |-Branch one: % 82.81/43.13 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.13 | % 82.81/43.13 | Using (943) and (944) yields: % 82.81/43.13 | (97) $false % 82.81/43.13 | % 82.81/43.13 |-The branch is then unsatisfiable % 82.81/43.13 |-Branch two: % 82.81/43.13 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.13 | (947) xm = sz00 | iLess0(xm, sz00) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (292), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.14 | % 82.81/43.14 | Using (943) and (944) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.14 | (951) xm = sz00 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_0_2_2) & ~ (v1 = v0) & sdtpldt0(xn, xm) = v0 & sdtpldt0(xn, sz00) = v1 & sdtpldt0(sz00, xn) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_0_2_2, v2)) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (291), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.14 | % 82.81/43.14 | Using (943) and (944) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.14 | (955) xm = sz00 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_15_0_4) & ~ (v1 = v0) & sdtpldt0(xp, xm) = v0 & sdtpldt0(xp, sz00) = v1 & sdtpldt0(sz00, xp) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_15_0_4, v2)) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (317), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.14 | % 82.81/43.14 | Using (943) and (944) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.14 | (959) xm = sz00 | ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xm) & ~ (v1 = v0) & sdtpldt0(all_107_0_18, xm) = v0 & sdtpldt0(all_107_0_18, sz00) = v1 & sdtpldt0(sz00, all_107_0_18) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(xm, v2)) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (294), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.14 | % 82.81/43.14 | Using (943) and (944) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (943) sdtlseqdt0(xm, sz00) % 82.81/43.14 | (963) ? [v0] : (sdtpldt0(xm, v0) = sz00 & aNaturalNumber0(v0)) % 82.81/43.14 | % 82.81/43.14 | Instantiating (963) with all_1130_0_141 yields: % 82.81/43.14 | (964) sdtpldt0(xm, all_1130_0_141) = sz00 & aNaturalNumber0(all_1130_0_141) % 82.81/43.14 | % 82.81/43.14 | Applying alpha-rule on (964) yields: % 82.81/43.14 | (965) sdtpldt0(xm, all_1130_0_141) = sz00 % 82.81/43.14 | (966) aNaturalNumber0(all_1130_0_141) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (951), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (446) xm = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (446) can reduce 441 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (441) ~ (xm = sz00) % 82.81/43.14 | (970) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_0_2_2) & ~ (v1 = v0) & sdtpldt0(xn, xm) = v0 & sdtpldt0(xn, sz00) = v1 & sdtpldt0(sz00, xn) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_0_2_2, v2)) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (955), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (446) xm = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (446) can reduce 441 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (441) ~ (xm = sz00) % 82.81/43.14 | (974) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_15_0_4) & ~ (v1 = v0) & sdtpldt0(xp, xm) = v0 & sdtpldt0(xp, sz00) = v1 & sdtpldt0(sz00, xp) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(all_15_0_4, v2)) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (959), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (446) xm = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (446) can reduce 441 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (441) ~ (xm = sz00) % 82.81/43.14 | (978) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = xm) & ~ (v1 = v0) & sdtpldt0(all_107_0_18, xm) = v0 & sdtpldt0(all_107_0_18, sz00) = v1 & sdtpldt0(sz00, all_107_0_18) = v2 & sdtlseqdt0(v0, v1) & sdtlseqdt0(xm, v2)) % 82.81/43.14 | % 82.81/43.14 | Instantiating formula (7) with all_1130_0_141, xm and discharging atoms sdtpldt0(xm, all_1130_0_141) = sz00, aNaturalNumber0(all_1130_0_141), aNaturalNumber0(xm), yields: % 82.81/43.14 | (446) xm = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (446) can reduce 441 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (944) ~ sdtlseqdt0(xm, sz00) % 82.81/43.14 | (982) sdtlseqdt0(sz00, xm) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (328), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (983) ~ sdtlseqdt0(sz00, all_15_0_4) % 82.81/43.14 | % 82.81/43.14 | From (440) and (983) follows: % 82.81/43.14 | (984) ~ sdtlseqdt0(sz00, xm) % 82.81/43.14 | % 82.81/43.14 | Using (982) and (984) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (986) sdtlseqdt0(sz00, all_15_0_4) % 82.81/43.14 | (987) all_15_0_4 = sz00 | iLess0(sz00, all_15_0_4) % 82.81/43.14 | % 82.81/43.14 | From (440) and (986) follows: % 82.81/43.14 | (982) sdtlseqdt0(sz00, xm) % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (329), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (983) ~ sdtlseqdt0(sz00, all_15_0_4) % 82.81/43.14 | % 82.81/43.14 | From (440) and (983) follows: % 82.81/43.14 | (984) ~ sdtlseqdt0(sz00, xm) % 82.81/43.14 | % 82.81/43.14 | Using (982) and (984) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (986) sdtlseqdt0(sz00, all_15_0_4) % 82.81/43.14 | (993) ? [v0] : (sdtpldt0(sz00, v0) = all_15_0_4 & aNaturalNumber0(v0)) % 82.81/43.14 | % 82.81/43.14 | Instantiating (993) with all_1121_0_151 yields: % 82.81/43.14 | (994) sdtpldt0(sz00, all_1121_0_151) = all_15_0_4 & aNaturalNumber0(all_1121_0_151) % 82.81/43.14 | % 82.81/43.14 | Applying alpha-rule on (994) yields: % 82.81/43.14 | (995) sdtpldt0(sz00, all_1121_0_151) = all_15_0_4 % 82.81/43.14 | (996) aNaturalNumber0(all_1121_0_151) % 82.81/43.14 | % 82.81/43.14 | From (440) and (995) follows: % 82.81/43.14 | (997) sdtpldt0(sz00, all_1121_0_151) = xm % 82.81/43.14 | % 82.81/43.14 | Using (997) and (939) yields: % 82.81/43.14 | (998) ~ (all_1121_0_151 = xm) % 82.81/43.14 | % 82.81/43.14 | Instantiating formula (3) with xm, all_1121_0_151 and discharging atoms sdtpldt0(sz00, all_1121_0_151) = xm, aNaturalNumber0(all_1121_0_151), yields: % 82.81/43.14 | (999) all_1121_0_151 = xm % 82.81/43.14 | % 82.81/43.14 | Equations (999) can reduce 998 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1001) sdtpldt0(sz00, all_15_0_4) = all_122_0_20 % 82.81/43.14 | (1002) sdtpldt0(all_15_0_4, sz00) = all_15_0_4 % 82.81/43.14 | % 82.81/43.14 | From (440)(440) and (1002) follows: % 82.81/43.14 | (1003) sdtpldt0(xm, sz00) = xm % 82.81/43.14 | % 82.81/43.14 | Using (1003) and (937) yields: % 82.81/43.14 | (97) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1003) sdtpldt0(xm, sz00) = xm % 82.81/43.14 | (103) xp = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (103) can reduce 73 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1008) sdtpldt0(xn, sz00) = xn % 82.81/43.14 | (1009) all_25_0_5 = sz00 % 82.81/43.14 | % 82.81/43.14 | Combining equations (385,1009) yields a new equation: % 82.81/43.14 | (915) xp = sz00 % 82.81/43.14 | % 82.81/43.14 | Simplifying 915 yields: % 82.81/43.14 | (103) xp = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (103) can reduce 73 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1013) sdtpldt0(all_25_0_5, all_15_0_4) = sz00 % 82.81/43.14 | (1014) all_15_0_4 = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (1014) can reduce 138 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1016) sdtpldt0(xm, xp) = sz00 % 82.81/43.14 | (103) xp = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (103) can reduce 73 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1019) ~ (all_34_0_6 = xp) % 82.81/43.14 | (1020) all_34_0_6 = sz10 % 82.81/43.14 | % 82.81/43.14 | Equations (1020) can reduce 116 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1022) sdtpldt0(xp, all_13_0_3) = sz00 % 82.81/43.14 | (103) xp = sz00 % 82.81/43.14 | % 82.81/43.14 | Equations (103) can reduce 73 to: % 82.81/43.14 | (104) $false % 82.81/43.14 | % 82.81/43.14 |-The branch is then unsatisfiable % 82.81/43.14 |-Branch two: % 82.81/43.14 | (1025) ~ sdtlseqdt0(sz10, xp) % 82.81/43.14 | (1026) xp = sz10 | xp = sz00 % 82.81/43.14 | % 82.81/43.14 +-Applying beta-rule and splitting (1026), into two cases. % 82.81/43.14 |-Branch one: % 82.81/43.14 | (103) xp = sz00 % 82.81/43.15 | % 82.81/43.15 | Equations (103) can reduce 73 to: % 82.81/43.15 | (104) $false % 82.81/43.15 | % 82.81/43.15 |-The branch is then unsatisfiable % 82.81/43.15 |-Branch two: % 82.81/43.15 | (73) ~ (xp = sz00) % 82.81/43.15 | (107) xp = sz10 % 82.81/43.15 | % 82.81/43.15 | Equations (107) can reduce 72 to: % 82.81/43.15 | (104) $false % 82.81/43.15 | % 82.81/43.15 |-The branch is then unsatisfiable % 82.81/43.15 % SZS output end Proof for theBenchmark % 82.81/43.15 % 82.81/43.15 42544ms %------------------------------------------------------------------------------