%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 08:45:10 EDT 2022 % Result : Theorem 21.50s 6.69s % Output : Proof 49.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jul 7 14:09:44 EDT 2022 % 0.12/0.34 % CPUTime : % 0.64/0.64 ____ _ % 0.64/0.64 ___ / __ \_____(_)___ ________ __________ % 0.64/0.64 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.64/0.64 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.64/0.64 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.64/0.64 % 0.64/0.64 A Theorem Prover for First-Order Logic % 0.64/0.64 (ePrincess v.1.0) % 0.64/0.64 % 0.64/0.64 (c) Philipp Rümmer, 2009-2015 % 0.64/0.64 (c) Peter Backeman, 2014-2015 % 0.64/0.64 (contributions by Angelo Brillout, Peter Baumgartner) % 0.64/0.64 Free software under GNU Lesser General Public License (LGPL). % 0.64/0.64 Bug reports to peter@backeman.se % 0.64/0.64 % 0.64/0.64 For more information, visit http://user.uu.se/~petba168/breu/ % 0.64/0.64 % 0.64/0.64 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.80/0.69 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.99/1.06 Prover 0: Preprocessing ... % 3.92/1.58 Prover 0: Constructing countermodel ... % 18.57/5.98 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.91/6.07 Prover 1: Preprocessing ... % 19.67/6.24 Prover 1: Constructing countermodel ... % 21.50/6.69 Prover 1: proved (708ms) % 21.50/6.69 Prover 0: stopped % 21.50/6.69 % 21.50/6.69 No countermodel exists, formula is valid % 21.50/6.69 % SZS status Theorem for theBenchmark % 21.50/6.69 % 21.50/6.69 Generating proof ... found it (size 304) % 48.67/15.36 % 48.67/15.36 % SZS output start Proof for theBenchmark % 48.67/15.36 Assumed formulas after preprocessing and simplification: % 48.67/15.36 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & ~ (v3 = 0) & ~ (xk = sz10) & ~ (xk = sz00) & ~ (xp = xm) & ~ (xp = xn) & ~ (sz10 = sz00) & isPrime0(xp) = 0 & sdtsldt0(v2, xp) = xk & doDivides0(xp, v2) = 0 & sdtlseqdt0(xp, xm) = v4 & sdtlseqdt0(xp, xn) = v3 & sdtlseqdt0(xm, xp) = 0 & sdtlseqdt0(xn, xp) = 0 & sdtasdt0(xn, xm) = v2 & sdtpldt0(v0, xp) = v1 & sdtpldt0(xn, xm) = v0 & aNaturalNumber0(xp) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xn) = 0 & aNaturalNumber0(sz10) = 0 & aNaturalNumber0(sz00) = 0 & ~ (isPrime0(sz10) = 0) & ~ (isPrime0(sz00) = 0) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | v5 = sz00 | ~ (sdtlseqdt0(v8, v9) = v10) | ~ (sdtasdt0(v5, v7) = v9) | ~ (sdtasdt0(v5, v6) = v8) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (sdtlseqdt0(v15, v16) = v17 & sdtlseqdt0(v6, v7) = v14 & sdtasdt0(v7, v5) = v16 & sdtasdt0(v6, v5) = v15 & aNaturalNumber0(v7) = v13 & aNaturalNumber0(v6) = v12 & aNaturalNumber0(v5) = v11 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | (v17 = 0 & v10 = 0 & ~ (v16 = v15) & ~ (v9 = v8))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v6 = v5 | ~ (sdtlseqdt0(v8, v9) = v10) | ~ (sdtlseqdt0(v5, v6) = 0) | ~ (sdtpldt0(v6, v7) = v9) | ~ (sdtpldt0(v5, v7) = v8) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ((sdtlseqdt0(v12, v13) = v14 & sdtpldt0(v7, v6) = v13 & sdtpldt0(v7, v5) = v12 & aNaturalNumber0(v7) = v11 & ( ~ (v11 = 0) | (v14 = 0 & v10 = 0 & ~ (v13 = v12) & ~ (v9 = v8)))) | (aNaturalNumber0(v6) = v12 & aNaturalNumber0(v5) = v11 & ( ~ (v12 = 0) | ~ (v11 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v5 = sz00 | ~ (sdtsldt0(v9, v5) = v10) | ~ (sdtsldt0(v6, v5) = v7) | ~ (sdtasdt0(v8, v6) = v9) | ? [v11] : ? [v12] : ? [v13] : ((doDivides0(v5, v6) = v13 & aNaturalNumber0(v6) = v12 & aNaturalNumber0(v5) = v11 & ( ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0))) | (sdtasdt0(v8, v7) = v12 & aNaturalNumber0(v8) = v11 & ( ~ (v11 = 0) | v12 = v10)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ( ~ (sdtasdt0(v5, v7) = v9) | ~ (sdtasdt0(v5, v6) = v8) | ~ (sdtpldt0(v8, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : (sdtasdt0(v14, v5) = v16 & sdtasdt0(v7, v5) = v18 & sdtasdt0(v6, v5) = v17 & sdtasdt0(v5, v14) = v15 & sdtpldt0(v17, v18) = v19 & sdtpldt0(v6, v7) = v14 & aNaturalNumber0(v7) = v13 & aNaturalNumber0(v6) = v12 & aNaturalNumber0(v5) = v11 & ( ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | (v19 = v16 & v15 = v10)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (doDivides0(v5, v8) = v9) | ~ (sdtpldt0(v6, v7) = v8) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (doDivides0(v5, v7) = v14 & doDivides0(v5, v6) = v13 & aNaturalNumber0(v7) = v12 & aNaturalNumber0(v6) = v11 & aNaturalNumber0(v5) = v10 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | v5 = sz00 | ~ (sdtasdt0(v5, v7) = v9) | ~ (sdtasdt0(v5, v6) = v8) | ~ (aNaturalNumber0(v5) = 0) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : (sdtasdt0(v7, v5) = v13 & sdtasdt0(v6, v5) = v12 & aNaturalNumber0(v7) = v11 & aNaturalNumber0(v6) = v10 & ( ~ (v11 = 0) | ~ (v10 = 0) | ( ~ (v13 = v12) & ~ (v9 = v8))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (sdtpldt0(v5, v7) = v9) | ~ (sdtpldt0(v5, v6) = v8) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtpldt0(v7, v5) = v14 & sdtpldt0(v6, v5) = v13 & aNaturalNumber0(v7) = v12 & aNaturalNumber0(v6) = v11 & aNaturalNumber0(v5) = v10 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ( ~ (v14 = v13) & ~ (v9 = v8))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtasdt0(v8, v7) = v9) | ~ (sdtasdt0(v5, v6) = v8) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v6, v7) = v13 & sdtasdt0(v5, v13) = v14 & aNaturalNumber0(v7) = v12 & aNaturalNumber0(v6) = v11 & aNaturalNumber0(v5) = v10 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | v14 = v9))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (sdtpldt0(v8, v7) = v9) | ~ (sdtpldt0(v5, v6) = v8) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtpldt0(v6, v7) = v13 & sdtpldt0(v5, v13) = v14 & aNaturalNumber0(v7) = v12 & aNaturalNumber0(v6) = v11 & aNaturalNumber0(v5) = v10 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | v14 = v9))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v7 | v5 = sz00 | ~ (sdtsldt0(v6, v5) = v7) | ~ (sdtasdt0(v5, v8) = v6) | ? [v9] : ? [v10] : ? [v11] : (( ~ (v9 = 0) & aNaturalNumber0(v8) = v9) | (doDivides0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v7 | ~ (sdtmndt0(v6, v5) = v7) | ~ (sdtpldt0(v5, v8) = v6) | ? [v9] : ? [v10] : ? [v11] : (( ~ (v9 = 0) & aNaturalNumber0(v8) = v9) | (sdtlseqdt0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v6 | v5 = sz00 | ~ (sdtsldt0(v6, v5) = v7) | ~ (sdtasdt0(v5, v7) = v8) | ? [v9] : ? [v10] : ? [v11] : (doDivides0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = v6 | ~ (sdtmndt0(v6, v5) = v7) | ~ (sdtpldt0(v5, v7) = v8) | ? [v9] : ? [v10] : ? [v11] : (sdtlseqdt0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v5 = sz00 | ~ (sdtlseqdt0(v6, v7) = v8) | ~ (sdtasdt0(v6, v5) = v7) | ? [v9] : ? [v10] : (aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (doDivides0(v5, v7) = v8) | ~ (doDivides0(v5, v6) = 0) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : (doDivides0(v6, v7) = v12 & aNaturalNumber0(v7) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (sdtlseqdt0(v5, v7) = v8) | ~ (sdtlseqdt0(v5, v6) = 0) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtlseqdt0(v6, v7) = v12 & aNaturalNumber0(v7) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0)))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (doDivides0(v5, v6) = v7) | ~ (sdtasdt0(v5, v8) = v6) | ? [v9] : ? [v10] : (( ~ (v9 = 0) & aNaturalNumber0(v8) = v9) | (aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v7 = 0 | ~ (sdtlseqdt0(v5, v6) = v7) | ~ (sdtpldt0(v5, v8) = v6) | ? [v9] : ? [v10] : (( ~ (v9 = 0) & aNaturalNumber0(v8) = v9) | (aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (sdtsldt0(v8, v7) = v6) | ~ (sdtsldt0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (doDivides0(v8, v7) = v6) | ~ (doDivides0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (iLess0(v8, v7) = v6) | ~ (iLess0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (sdtmndt0(v8, v7) = v6) | ~ (sdtmndt0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (sdtlseqdt0(v8, v7) = v6) | ~ (sdtlseqdt0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (sdtasdt0(v8, v7) = v6) | ~ (sdtasdt0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v6 = v5 | ~ (sdtpldt0(v8, v7) = v6) | ~ (sdtpldt0(v8, v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v5 = sz00 | ~ (sdtsldt0(v6, v5) = v7) | ~ (sdtasdt0(v5, v7) = v8) | ? [v9] : ? [v10] : ? [v11] : ((v9 = 0 & aNaturalNumber0(v7) = 0) | (doDivides0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (doDivides0(v7, v8) = 0) | ~ (sdtasdt0(v5, v6) = v8) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (isPrime0(v7) = v12 & doDivides0(v7, v6) = v17 & doDivides0(v7, v5) = v16 & iLess0(v14, v1) = v15 & sdtpldt0(v13, v7) = v14 & sdtpldt0(v5, v6) = v13 & aNaturalNumber0(v7) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v15 = 0) | ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | v17 = 0 | v16 = 0))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (doDivides0(v5, v8) = 0) | ~ (sdtpldt0(v6, v7) = v8) | ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : (doDivides0(v5, v7) = v13 & doDivides0(v5, v6) = v12 & aNaturalNumber0(v7) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v12 = 0) | ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0) | v13 = 0))) & ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (sdtmndt0(v6, v5) = v7) | ~ (sdtpldt0(v5, v7) = v8) | ? [v9] : ? [v10] : ? [v11] : ((v9 = 0 & aNaturalNumber0(v7) = 0) | (sdtlseqdt0(v5, v6) = v11 & aNaturalNumber0(v6) = v10 & aNaturalNumber0(v5) = v9 & ( ~ (v11 = 0) | ~ (v10 = 0) | ~ (v9 = 0))))) & ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = v5 | ~ (iLess0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (sdtlseqdt0(v5, v6) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0)))) & ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (sdtlseqdt0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (sdtlseqdt0(v6, v5) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | (v10 = 0 & ~ (v6 = v5))))) & ! [v5] : ! [v6] : ! [v7] : (v6 = v5 | ~ (isPrime0(v7) = v6) | ~ (isPrime0(v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : (v6 = v5 | ~ (aNaturalNumber0(v7) = v6) | ~ (aNaturalNumber0(v7) = v5)) & ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtasdt0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (sdtasdt0(v6, v5) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v10 = v7))) & ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtasdt0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (aNaturalNumber0(v7) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v10 = 0))) & ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtpldt0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (sdtpldt0(v6, v5) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v10 = v7))) & ! [v5] : ! [v6] : ! [v7] : ( ~ (sdtpldt0(v5, v6) = v7) | ? [v8] : ? [v9] : ? [v10] : (aNaturalNumber0(v7) = v10 & aNaturalNumber0(v6) = v9 & aNaturalNumber0(v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v10 = 0))) & ! [v5] : ! [v6] : (v6 = v5 | v6 = sz10 | ~ (isPrime0(v5) = 0) | ~ (doDivides0(v6, v5) = 0) | ? [v7] : (( ~ (v7 = 0) & aNaturalNumber0(v6) = v7) | ( ~ (v7 = 0) & aNaturalNumber0(v5) = v7))) & ! [v5] : ! [v6] : (v6 = v5 | ~ (sdtlseqdt0(v5, v6) = 0) | ? [v7] : ? [v8] : ? [v9] : (sdtlseqdt0(v6, v5) = v9 & aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v5] : ! [v6] : (v6 = sz00 | v5 = sz00 | ~ (sdtasdt0(v5, v6) = sz00) | ? [v7] : ? [v8] : (aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v5] : ! [v6] : (v6 = sz00 | ~ (doDivides0(v5, v6) = 0) | ? [v7] : ? [v8] : ? [v9] : (sdtlseqdt0(v5, v6) = v9 & aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | v9 = 0))) & ! [v5] : ! [v6] : (v6 = sz00 | ~ (sdtpldt0(v5, v6) = sz00) | ? [v7] : ? [v8] : (aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v5] : ! [v6] : (v6 = 0 | v5 = sz10 | v5 = sz00 | ~ (isPrime0(v5) = v6) | ? [v7] : ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & ~ (v7 = v5) & ~ (v7 = sz10) & doDivides0(v7, v5) = 0 & aNaturalNumber0(v7) = 0) | ( ~ (v7 = 0) & aNaturalNumber0(v5) = v7))) & ! [v5] : ! [v6] : (v6 = 0 | v5 = sz10 | v5 = sz00 | ~ (sdtlseqdt0(sz10, v5) = v6) | ? [v7] : ( ~ (v7 = 0) & aNaturalNumber0(v5) = v7)) & ! [v5] : ! [v6] : (v6 = 0 | ~ (sdtlseqdt0(v5, v5) = v6) | ? [v7] : ( ~ (v7 = 0) & aNaturalNumber0(v5) = v7)) & ! [v5] : ! [v6] : (v5 = sz00 | ~ (sdtpldt0(v5, v6) = sz00) | ? [v7] : ? [v8] : (aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v5] : ! [v6] : ( ~ (doDivides0(v5, v6) = 0) | ? [v7] : ? [v8] : ? [v9] : ((v9 = v6 & v8 = 0 & sdtasdt0(v5, v7) = v6 & aNaturalNumber0(v7) = 0) | (aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0))))) & ! [v5] : ! [v6] : ( ~ (sdtlseqdt0(v5, v6) = 0) | ? [v7] : ? [v8] : ? [v9] : ((v9 = v6 & v8 = 0 & sdtpldt0(v5, v7) = v6 & aNaturalNumber0(v7) = 0) | (aNaturalNumber0(v6) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0))))) & ! [v5] : ! [v6] : ( ~ (sdtasdt0(sz10, v5) = v6) | ? [v7] : ? [v8] : (sdtasdt0(v5, sz10) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v7 = 0) | (v8 = v5 & v6 = v5)))) & ! [v5] : ! [v6] : ( ~ (sdtasdt0(sz00, v5) = v6) | ? [v7] : ? [v8] : (sdtasdt0(v5, sz00) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v7 = 0) | (v8 = sz00 & v6 = sz00)))) & ! [v5] : ! [v6] : ( ~ (sdtpldt0(sz00, v5) = v6) | ? [v7] : ? [v8] : (sdtpldt0(v5, sz00) = v8 & aNaturalNumber0(v5) = v7 & ( ~ (v7 = 0) | (v8 = v5 & v6 = v5)))) & ! [v5] : (v5 = sz10 | v5 = sz00 | ~ (aNaturalNumber0(v5) = 0) | ? [v6] : (isPrime0(v6) = 0 & doDivides0(v6, v5) = 0 & aNaturalNumber0(v6) = 0)) & ! [v5] : ( ~ (doDivides0(v5, xk) = 0) | ? [v6] : ? [v7] : (isPrime0(v5) = v7 & aNaturalNumber0(v5) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0))))) % 48.79/15.44 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4 yields: % 48.79/15.44 | (1) ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0) & ~ (xk = sz10) & ~ (xk = sz00) & ~ (xp = xm) & ~ (xp = xn) & ~ (sz10 = sz00) & isPrime0(xp) = 0 & sdtsldt0(all_0_2_2, xp) = xk & doDivides0(xp, all_0_2_2) = 0 & sdtlseqdt0(xp, xm) = all_0_0_0 & sdtlseqdt0(xp, xn) = all_0_1_1 & sdtlseqdt0(xm, xp) = 0 & sdtlseqdt0(xn, xp) = 0 & sdtasdt0(xn, xm) = all_0_2_2 & sdtpldt0(all_0_4_4, xp) = all_0_3_3 & sdtpldt0(xn, xm) = all_0_4_4 & aNaturalNumber0(xp) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xn) = 0 & aNaturalNumber0(sz10) = 0 & aNaturalNumber0(sz00) = 0 & ~ (isPrime0(sz10) = 0) & ~ (isPrime0(sz00) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v2 = v1 | v0 = sz00 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtlseqdt0(v10, v11) = v12 & sdtlseqdt0(v1, v2) = v9 & sdtasdt0(v2, v0) = v11 & sdtasdt0(v1, v0) = v10 & aNaturalNumber0(v2) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v12 = 0 & v5 = 0 & ~ (v11 = v10) & ~ (v4 = v3))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ (sdtlseqdt0(v0, v1) = 0) | ~ (sdtpldt0(v1, v2) = v4) | ~ (sdtpldt0(v0, v2) = v3) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((sdtlseqdt0(v7, v8) = v9 & sdtpldt0(v2, v1) = v8 & sdtpldt0(v2, v0) = v7 & aNaturalNumber0(v2) = v6 & ( ~ (v6 = 0) | (v9 = 0 & v5 = 0 & ~ (v8 = v7) & ~ (v4 = v3)))) | (aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v0 = sz00 | ~ (sdtsldt0(v4, v0) = v5) | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v3, v1) = v4) | ? [v6] : ? [v7] : ? [v8] : ((doDivides0(v0, v1) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0))) | (sdtasdt0(v3, v2) = v7 & aNaturalNumber0(v3) = v6 & ( ~ (v6 = 0) | v7 = v5)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 & aNaturalNumber0(v2) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (doDivides0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (doDivides0(v0, v2) = v9 & doDivides0(v0, v1) = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (aNaturalNumber0(v0) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = v3))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtpldt0(v2, v0) = v9 & sdtpldt0(v1, v0) = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v9 = v8) & ~ (v4 = v3))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ? [v4] : ? [v5] : ? [v6] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ? [v4] : ? [v5] : ? [v6] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v0 = sz00 | ~ (sdtlseqdt0(v1, v2) = v3) | ~ (sdtasdt0(v1, v0) = v2) | ? [v4] : ? [v5] : (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (doDivides0(v0, v1) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ? [v4] : ? [v5] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ? [v4] : ? [v5] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(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] : (v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & aNaturalNumber0(v2) = 0) | (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (doDivides0(v2, v3) = 0) | ~ (sdtasdt0(v0, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (isPrime0(v2) = v7 & doDivides0(v2, v1) = v12 & doDivides0(v2, v0) = v11 & iLess0(v9, all_0_3_3) = v10 & sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v10 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v12 = 0 | v11 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (doDivides0(v0, v3) = 0) | ~ (sdtpldt0(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (doDivides0(v0, v2) = v8 & doDivides0(v0, v1) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v8 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & aNaturalNumber0(v2) = 0) | (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | v1 = v0 | ~ (iLess0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v5 = 0 & ~ (v1 = v0))))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isPrime0(v2) = v1) | ~ (isPrime0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : (v1 = v0 | v1 = sz10 | ~ (isPrime0(v0) = 0) | ~ (doDivides0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & aNaturalNumber0(v1) = v2) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v1, v0) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (doDivides0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v0, v1) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | v4 = 0))) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | v0 = sz10 | v0 = sz00 | ~ (isPrime0(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & ~ (v2 = v0) & ~ (v2 = sz10) & doDivides0(v2, v0) = 0 & aNaturalNumber0(v2) = 0) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) & ! [v0] : ! [v1] : (v1 = 0 | v0 = sz10 | v0 = sz00 | ~ (sdtlseqdt0(sz10, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) & ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : ( ~ (doDivides0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & v3 = 0 & sdtasdt0(v0, v2) = v1 & aNaturalNumber0(v2) = 0) | (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))))) & ! [v0] : ! [v1] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & v3 = 0 & sdtpldt0(v0, v2) = v1 & aNaturalNumber0(v2) = 0) | (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz10) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = sz00 & v1 = sz00)))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtpldt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) & ! [v0] : (v0 = sz10 | v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ? [v1] : (isPrime0(v1) = 0 & doDivides0(v1, v0) = 0 & aNaturalNumber0(v1) = 0)) & ! [v0] : ( ~ (doDivides0(v0, xk) = 0) | ? [v1] : ? [v2] : (isPrime0(v0) = v2 & aNaturalNumber0(v0) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0)))) % 49.20/15.47 | % 49.20/15.47 | Applying alpha-rule on (1) yields: % 49.20/15.47 | (2) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz10) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 49.20/15.47 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (doDivides0(v0, v2) = v3) | ~ (doDivides0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (doDivides0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.20/15.47 | (4) ~ (all_0_1_1 = 0) % 49.20/15.47 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | v0 = sz00 | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (aNaturalNumber0(v0) = 0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (sdtasdt0(v2, v0) = v8 & sdtasdt0(v1, v0) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v8 = v7) & ~ (v4 = v3))))) % 49.20/15.47 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) % 49.20/15.47 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ? [v4] : ? [v5] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 49.20/15.47 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v8 & sdtasdt0(v0, v8) = v9 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 49.20/15.47 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (doDivides0(v0, v1) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ? [v4] : ? [v5] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 49.20/15.47 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v0 = sz00 | ~ (sdtsldt0(v4, v0) = v5) | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v3, v1) = v4) | ? [v6] : ? [v7] : ? [v8] : ((doDivides0(v0, v1) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0))) | (sdtasdt0(v3, v2) = v7 & aNaturalNumber0(v3) = v6 & ( ~ (v6 = 0) | v7 = v5)))) % 49.20/15.47 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtasdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 49.20/15.47 | (12) aNaturalNumber0(sz10) = 0 % 49.20/15.47 | (13) sdtlseqdt0(xp, xn) = all_0_1_1 % 49.20/15.47 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.20/15.47 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) % 49.20/15.47 | (16) aNaturalNumber0(xn) = 0 % 49.20/15.47 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (doDivides0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (doDivides0(v0, v2) = v9 & doDivides0(v0, v1) = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0)))) % 49.20/15.47 | (18) ~ (xk = sz00) % 49.20/15.47 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & aNaturalNumber0(v2) = 0) | (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) % 49.20/15.47 | (20) ! [v0] : ! [v1] : (v1 = 0 | v0 = sz10 | v0 = sz00 | ~ (sdtlseqdt0(sz10, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) % 49.20/15.47 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (sdtpldt0(v0, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtpldt0(v2, v0) = v9 & sdtpldt0(v1, v0) = v8 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ( ~ (v9 = v8) & ~ (v4 = v3))))) % 49.20/15.48 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 49.20/15.48 | (23) aNaturalNumber0(xp) = 0 % 49.20/15.48 | (24) ~ (isPrime0(sz10) = 0) % 49.20/15.48 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (aNaturalNumber0(v2) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 49.20/15.48 | (26) sdtpldt0(all_0_4_4, xp) = all_0_3_3 % 49.20/15.48 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtpldt0(v1, v2) = v8 & sdtpldt0(v0, v8) = v9 & aNaturalNumber0(v2) = v7 & aNaturalNumber0(v1) = v6 & aNaturalNumber0(v0) = v5 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | v9 = v4))) % 49.20/15.48 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) % 49.20/15.48 | (29) sdtsldt0(all_0_2_2, xp) = xk % 49.20/15.48 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 49.20/15.48 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ((v4 = 0 & aNaturalNumber0(v2) = 0) | (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) % 49.20/15.48 | (32) ! [v0] : (v0 = sz10 | v0 = sz00 | ~ (aNaturalNumber0(v0) = 0) | ? [v1] : (isPrime0(v1) = 0 & doDivides0(v1, v0) = 0 & aNaturalNumber0(v1) = 0)) % 49.20/15.48 | (33) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 49.20/15.48 | (34) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | v1 = v0 | ~ (iLess0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v0, v1) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0)))) % 49.20/15.48 | (35) sdtlseqdt0(xm, xp) = 0 % 49.20/15.48 | (36) ~ (isPrime0(sz00) = 0) % 49.20/15.48 | (37) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (sdtlseqdt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtlseqdt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v5 = 0 & ~ (v1 = v0))))) % 49.20/15.48 | (38) ~ (all_0_0_0 = 0) % 49.20/15.48 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) % 49.20/15.48 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (doDivides0(v2, v3) = 0) | ~ (sdtasdt0(v0, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (isPrime0(v2) = v7 & doDivides0(v2, v1) = v12 & doDivides0(v2, v0) = v11 & iLess0(v9, all_0_3_3) = v10 & sdtpldt0(v8, v2) = v9 & sdtpldt0(v0, v1) = v8 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v10 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v12 = 0 | v11 = 0))) % 49.20/15.48 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 49.20/15.48 | (42) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = sz00 & v1 = sz00)))) % 49.20/15.48 | (43) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isPrime0(v2) = v1) | ~ (isPrime0(v2) = v0)) % 49.20/15.48 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | v0 = sz00 | ~ (sdtlseqdt0(v1, v2) = v3) | ~ (sdtasdt0(v1, v0) = v2) | ? [v4] : ? [v5] : (aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0)))) % 49.32/15.48 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : (sdtasdt0(v9, v0) = v11 & sdtasdt0(v2, v0) = v13 & sdtasdt0(v1, v0) = v12 & sdtasdt0(v0, v9) = v10 & sdtpldt0(v12, v13) = v14 & sdtpldt0(v1, v2) = v9 & aNaturalNumber0(v2) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v14 = v11 & v10 = v5)))) % 49.32/15.48 | (46) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v1, v0) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v4 = 0) | ~ (v3 = 0) | ~ (v2 = 0)))) % 49.32/15.49 | (47) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (sdtpldt0(v1, v0) = v5 & aNaturalNumber0(v1) = v4 & aNaturalNumber0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = v2))) % 49.32/15.49 | (48) aNaturalNumber0(xm) = 0 % 49.32/15.49 | (49) doDivides0(xp, all_0_2_2) = 0 % 49.32/15.49 | (50) isPrime0(xp) = 0 % 49.32/15.49 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v3) = v1) | ? [v4] : ? [v5] : ? [v6] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) % 49.32/15.49 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (sdtmndt0(v1, v0) = v2) | ~ (sdtpldt0(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : (sdtlseqdt0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.32/15.49 | (53) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 49.32/15.49 | (54) ! [v0] : ! [v1] : (v1 = 0 | v0 = sz10 | v0 = sz00 | ~ (isPrime0(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & ~ (v2 = v0) & ~ (v2 = sz10) & doDivides0(v2, v0) = 0 & aNaturalNumber0(v2) = 0) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) % 49.32/15.49 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (sdtlseqdt0(v0, v2) = v3) | ~ (sdtlseqdt0(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (sdtlseqdt0(v1, v2) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.32/15.49 | (56) ~ (sz10 = sz00) % 49.32/15.49 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 49.32/15.49 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) % 49.32/15.49 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ (sdtlseqdt0(v0, v1) = 0) | ~ (sdtpldt0(v1, v2) = v4) | ~ (sdtpldt0(v0, v2) = v3) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ((sdtlseqdt0(v7, v8) = v9 & sdtpldt0(v2, v1) = v8 & sdtpldt0(v2, v0) = v7 & aNaturalNumber0(v2) = v6 & ( ~ (v6 = 0) | (v9 = 0 & v5 = 0 & ~ (v8 = v7) & ~ (v4 = v3)))) | (aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0))))) % 49.32/15.49 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v2 = v1 | v0 = sz00 | ~ (sdtlseqdt0(v3, v4) = v5) | ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : (sdtlseqdt0(v10, v11) = v12 & sdtlseqdt0(v1, v2) = v9 & sdtasdt0(v2, v0) = v11 & sdtasdt0(v1, v0) = v10 & aNaturalNumber0(v2) = v8 & aNaturalNumber0(v1) = v7 & aNaturalNumber0(v0) = v6 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | (v12 = 0 & v5 = 0 & ~ (v11 = v10) & ~ (v4 = v3))))) % 49.32/15.49 | (61) ! [v0] : ! [v1] : ( ~ (doDivides0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & v3 = 0 & sdtasdt0(v0, v2) = v1 & aNaturalNumber0(v2) = 0) | (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))))) % 49.32/15.49 | (62) ! [v0] : ! [v1] : ( ~ (sdtlseqdt0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ((v4 = v1 & v3 = 0 & sdtpldt0(v0, v2) = v1 & aNaturalNumber0(v2) = 0) | (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0))))) % 49.32/15.49 | (63) ~ (xk = sz10) % 49.32/15.49 | (64) ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) % 49.32/15.49 | (65) sdtasdt0(xn, xm) = all_0_2_2 % 49.32/15.49 | (66) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 49.32/15.49 | (67) ~ (xp = xn) % 49.32/15.49 | (68) sdtlseqdt0(xp, xm) = all_0_0_0 % 49.32/15.49 | (69) ! [v0] : ! [v1] : (v1 = v0 | v1 = sz10 | ~ (isPrime0(v0) = 0) | ~ (doDivides0(v1, v0) = 0) | ? [v2] : (( ~ (v2 = 0) & aNaturalNumber0(v1) = v2) | ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2))) % 49.32/15.49 | (70) sdtpldt0(xn, xm) = all_0_4_4 % 49.32/15.49 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v0 = sz00 | ~ (sdtsldt0(v1, v0) = v2) | ~ (sdtasdt0(v0, v3) = v1) | ? [v4] : ? [v5] : ? [v6] : (( ~ (v4 = 0) & aNaturalNumber0(v3) = v4) | (doDivides0(v0, v1) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0))))) % 49.32/15.50 | (72) ! [v0] : ! [v1] : (v1 = sz00 | ~ (doDivides0(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (sdtlseqdt0(v0, v1) = v4 & aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0) | v4 = 0))) % 49.32/15.50 | (73) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtpldt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 49.32/15.50 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (doDivides0(v0, v3) = 0) | ~ (sdtpldt0(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (doDivides0(v0, v2) = v8 & doDivides0(v0, v1) = v7 & aNaturalNumber0(v2) = v6 & aNaturalNumber0(v1) = v5 & aNaturalNumber0(v0) = v4 & ( ~ (v7 = 0) | ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | v8 = 0))) % 49.32/15.50 | (75) aNaturalNumber0(sz00) = 0 % 49.32/15.50 | (76) sdtlseqdt0(xn, xp) = 0 % 49.32/15.50 | (77) ~ (xp = xm) % 49.32/15.50 | (78) ! [v0] : ( ~ (doDivides0(v0, xk) = 0) | ? [v1] : ? [v2] : (isPrime0(v0) = v2 & aNaturalNumber0(v0) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0)))) % 49.32/15.50 | % 49.32/15.50 | Using (50) and (24) yields: % 49.32/15.50 | (79) ~ (xp = sz10) % 49.32/15.50 | % 49.32/15.50 | Using (50) and (36) yields: % 49.32/15.50 | (80) ~ (xp = sz00) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (61) with all_0_2_2, xp and discharging atoms doDivides0(xp, all_0_2_2) = 0, yields: % 49.32/15.50 | (81) ? [v0] : ? [v1] : ? [v2] : ((v2 = all_0_2_2 & v1 = 0 & sdtasdt0(xp, v0) = all_0_2_2 & aNaturalNumber0(v0) = 0) | (aNaturalNumber0(all_0_2_2) = v1 & aNaturalNumber0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (62) with xp, xm and discharging atoms sdtlseqdt0(xm, xp) = 0, yields: % 49.32/15.50 | (82) ? [v0] : ? [v1] : ? [v2] : ((v2 = xp & v1 = 0 & sdtpldt0(xm, v0) = xp & aNaturalNumber0(v0) = 0) | (aNaturalNumber0(xp) = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (62) with xp, xn and discharging atoms sdtlseqdt0(xn, xp) = 0, yields: % 49.32/15.50 | (83) ? [v0] : ? [v1] : ? [v2] : ((v2 = xp & v1 = 0 & sdtpldt0(xn, v0) = xp & aNaturalNumber0(v0) = 0) | (aNaturalNumber0(xp) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0)))) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (40) with all_0_2_2, xp, xm, xn and discharging atoms doDivides0(xp, all_0_2_2) = 0, sdtasdt0(xn, xm) = all_0_2_2, yields: % 49.32/15.50 | (84) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (isPrime0(xp) = v3 & doDivides0(xp, xm) = v8 & doDivides0(xp, xn) = v7 & iLess0(v5, all_0_3_3) = v6 & sdtpldt0(v4, xp) = v5 & sdtpldt0(xn, xm) = v4 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v6 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v8 = 0 | v7 = 0)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (11) with all_0_2_2, xm, xn and discharging atoms sdtasdt0(xn, xm) = all_0_2_2, yields: % 49.32/15.50 | (85) ? [v0] : ? [v1] : ? [v2] : (sdtasdt0(xm, xn) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_2_2)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (22) with all_0_2_2, xm, xn and discharging atoms sdtasdt0(xn, xm) = all_0_2_2, yields: % 49.32/15.50 | (86) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_0_2_2) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (47) with all_0_3_3, xp, all_0_4_4 and discharging atoms sdtpldt0(all_0_4_4, xp) = all_0_3_3, yields: % 49.32/15.50 | (87) ? [v0] : ? [v1] : ? [v2] : (sdtpldt0(xp, all_0_4_4) = v2 & aNaturalNumber0(all_0_4_4) = v0 & aNaturalNumber0(xp) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_3_3)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (25) with all_0_3_3, xp, all_0_4_4 and discharging atoms sdtpldt0(all_0_4_4, xp) = all_0_3_3, yields: % 49.32/15.50 | (88) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_0_3_3) = v2 & aNaturalNumber0(all_0_4_4) = v0 & aNaturalNumber0(xp) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (27) with all_0_3_3, all_0_4_4, xp, xm, xn and discharging atoms sdtpldt0(all_0_4_4, xp) = all_0_3_3, sdtpldt0(xn, xm) = all_0_4_4, yields: % 49.32/15.50 | (89) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtpldt0(xm, xp) = v3 & sdtpldt0(xn, v3) = v4 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = all_0_3_3)) % 49.32/15.50 | % 49.32/15.50 | Instantiating formula (47) with all_0_4_4, xm, xn and discharging atoms sdtpldt0(xn, xm) = all_0_4_4, yields: % 49.32/15.50 | (90) ? [v0] : ? [v1] : ? [v2] : (sdtpldt0(xm, xn) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_4_4)) % 49.32/15.51 | % 49.32/15.51 | Instantiating formula (25) with all_0_4_4, xm, xn and discharging atoms sdtpldt0(xn, xm) = all_0_4_4, yields: % 49.32/15.51 | (91) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_0_4_4) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.32/15.51 | % 49.32/15.51 | Instantiating formula (32) with xp and discharging atoms aNaturalNumber0(xp) = 0, yields: % 49.32/15.51 | (92) xp = sz10 | xp = sz00 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, xp) = 0 & aNaturalNumber0(v0) = 0) % 49.32/15.51 | % 49.32/15.51 | Instantiating (91) with all_12_0_5, all_12_1_6, all_12_2_7 yields: % 49.32/15.51 | (93) aNaturalNumber0(all_0_4_4) = all_12_0_5 & aNaturalNumber0(xm) = all_12_1_6 & aNaturalNumber0(xn) = all_12_2_7 & ( ~ (all_12_1_6 = 0) | ~ (all_12_2_7 = 0) | all_12_0_5 = 0) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (93) yields: % 49.32/15.51 | (94) aNaturalNumber0(all_0_4_4) = all_12_0_5 % 49.32/15.51 | (95) aNaturalNumber0(xm) = all_12_1_6 % 49.32/15.51 | (96) aNaturalNumber0(xn) = all_12_2_7 % 49.32/15.51 | (97) ~ (all_12_1_6 = 0) | ~ (all_12_2_7 = 0) | all_12_0_5 = 0 % 49.32/15.51 | % 49.32/15.51 | Instantiating (88) with all_14_0_8, all_14_1_9, all_14_2_10 yields: % 49.32/15.51 | (98) aNaturalNumber0(all_0_3_3) = all_14_0_8 & aNaturalNumber0(all_0_4_4) = all_14_2_10 & aNaturalNumber0(xp) = all_14_1_9 & ( ~ (all_14_1_9 = 0) | ~ (all_14_2_10 = 0) | all_14_0_8 = 0) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (98) yields: % 49.32/15.51 | (99) aNaturalNumber0(all_0_3_3) = all_14_0_8 % 49.32/15.51 | (100) aNaturalNumber0(all_0_4_4) = all_14_2_10 % 49.32/15.51 | (101) aNaturalNumber0(xp) = all_14_1_9 % 49.32/15.51 | (102) ~ (all_14_1_9 = 0) | ~ (all_14_2_10 = 0) | all_14_0_8 = 0 % 49.32/15.51 | % 49.32/15.51 | Instantiating (90) with all_16_0_11, all_16_1_12, all_16_2_13 yields: % 49.32/15.51 | (103) sdtpldt0(xm, xn) = all_16_0_11 & aNaturalNumber0(xm) = all_16_1_12 & aNaturalNumber0(xn) = all_16_2_13 & ( ~ (all_16_1_12 = 0) | ~ (all_16_2_13 = 0) | all_16_0_11 = all_0_4_4) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (103) yields: % 49.32/15.51 | (104) sdtpldt0(xm, xn) = all_16_0_11 % 49.32/15.51 | (105) aNaturalNumber0(xm) = all_16_1_12 % 49.32/15.51 | (106) aNaturalNumber0(xn) = all_16_2_13 % 49.32/15.51 | (107) ~ (all_16_1_12 = 0) | ~ (all_16_2_13 = 0) | all_16_0_11 = all_0_4_4 % 49.32/15.51 | % 49.32/15.51 | Instantiating (86) with all_18_0_14, all_18_1_15, all_18_2_16 yields: % 49.32/15.51 | (108) aNaturalNumber0(all_0_2_2) = all_18_0_14 & aNaturalNumber0(xm) = all_18_1_15 & aNaturalNumber0(xn) = all_18_2_16 & ( ~ (all_18_1_15 = 0) | ~ (all_18_2_16 = 0) | all_18_0_14 = 0) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (108) yields: % 49.32/15.51 | (109) aNaturalNumber0(all_0_2_2) = all_18_0_14 % 49.32/15.51 | (110) aNaturalNumber0(xm) = all_18_1_15 % 49.32/15.51 | (111) aNaturalNumber0(xn) = all_18_2_16 % 49.32/15.51 | (112) ~ (all_18_1_15 = 0) | ~ (all_18_2_16 = 0) | all_18_0_14 = 0 % 49.32/15.51 | % 49.32/15.51 | Instantiating (83) with all_20_0_17, all_20_1_18, all_20_2_19 yields: % 49.32/15.51 | (113) (all_20_0_17 = xp & all_20_1_18 = 0 & sdtpldt0(xn, all_20_2_19) = xp & aNaturalNumber0(all_20_2_19) = 0) | (aNaturalNumber0(xp) = all_20_1_18 & aNaturalNumber0(xn) = all_20_2_19 & ( ~ (all_20_1_18 = 0) | ~ (all_20_2_19 = 0))) % 49.32/15.51 | % 49.32/15.51 | Instantiating (82) with all_21_0_20, all_21_1_21, all_21_2_22 yields: % 49.32/15.51 | (114) (all_21_0_20 = xp & all_21_1_21 = 0 & sdtpldt0(xm, all_21_2_22) = xp & aNaturalNumber0(all_21_2_22) = 0) | (aNaturalNumber0(xp) = all_21_1_21 & aNaturalNumber0(xm) = all_21_2_22 & ( ~ (all_21_1_21 = 0) | ~ (all_21_2_22 = 0))) % 49.32/15.51 | % 49.32/15.51 | Instantiating (81) with all_22_0_23, all_22_1_24, all_22_2_25 yields: % 49.32/15.51 | (115) (all_22_0_23 = all_0_2_2 & all_22_1_24 = 0 & sdtasdt0(xp, all_22_2_25) = all_0_2_2 & aNaturalNumber0(all_22_2_25) = 0) | (aNaturalNumber0(all_0_2_2) = all_22_1_24 & aNaturalNumber0(xp) = all_22_2_25 & ( ~ (all_22_1_24 = 0) | ~ (all_22_2_25 = 0))) % 49.32/15.51 | % 49.32/15.51 | Instantiating (85) with all_23_0_26, all_23_1_27, all_23_2_28 yields: % 49.32/15.51 | (116) sdtasdt0(xm, xn) = all_23_0_26 & aNaturalNumber0(xm) = all_23_1_27 & aNaturalNumber0(xn) = all_23_2_28 & ( ~ (all_23_1_27 = 0) | ~ (all_23_2_28 = 0) | all_23_0_26 = all_0_2_2) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (116) yields: % 49.32/15.51 | (117) sdtasdt0(xm, xn) = all_23_0_26 % 49.32/15.51 | (118) aNaturalNumber0(xm) = all_23_1_27 % 49.32/15.51 | (119) aNaturalNumber0(xn) = all_23_2_28 % 49.32/15.51 | (120) ~ (all_23_1_27 = 0) | ~ (all_23_2_28 = 0) | all_23_0_26 = all_0_2_2 % 49.32/15.51 | % 49.32/15.51 | Instantiating (89) with all_25_0_29, all_25_1_30, all_25_2_31, all_25_3_32, all_25_4_33 yields: % 49.32/15.51 | (121) sdtpldt0(xm, xp) = all_25_1_30 & sdtpldt0(xn, all_25_1_30) = all_25_0_29 & aNaturalNumber0(xp) = all_25_2_31 & aNaturalNumber0(xm) = all_25_3_32 & aNaturalNumber0(xn) = all_25_4_33 & ( ~ (all_25_2_31 = 0) | ~ (all_25_3_32 = 0) | ~ (all_25_4_33 = 0) | all_25_0_29 = all_0_3_3) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (121) yields: % 49.32/15.51 | (122) sdtpldt0(xm, xp) = all_25_1_30 % 49.32/15.51 | (123) aNaturalNumber0(xm) = all_25_3_32 % 49.32/15.51 | (124) sdtpldt0(xn, all_25_1_30) = all_25_0_29 % 49.32/15.51 | (125) ~ (all_25_2_31 = 0) | ~ (all_25_3_32 = 0) | ~ (all_25_4_33 = 0) | all_25_0_29 = all_0_3_3 % 49.32/15.51 | (126) aNaturalNumber0(xp) = all_25_2_31 % 49.32/15.51 | (127) aNaturalNumber0(xn) = all_25_4_33 % 49.32/15.51 | % 49.32/15.51 | Instantiating (87) with all_27_0_34, all_27_1_35, all_27_2_36 yields: % 49.32/15.51 | (128) sdtpldt0(xp, all_0_4_4) = all_27_0_34 & aNaturalNumber0(all_0_4_4) = all_27_2_36 & aNaturalNumber0(xp) = all_27_1_35 & ( ~ (all_27_1_35 = 0) | ~ (all_27_2_36 = 0) | all_27_0_34 = all_0_3_3) % 49.32/15.51 | % 49.32/15.51 | Applying alpha-rule on (128) yields: % 49.32/15.51 | (129) sdtpldt0(xp, all_0_4_4) = all_27_0_34 % 49.32/15.51 | (130) aNaturalNumber0(all_0_4_4) = all_27_2_36 % 49.32/15.51 | (131) aNaturalNumber0(xp) = all_27_1_35 % 49.32/15.51 | (132) ~ (all_27_1_35 = 0) | ~ (all_27_2_36 = 0) | all_27_0_34 = all_0_3_3 % 49.32/15.51 | % 49.32/15.51 | Instantiating (84) with all_29_0_37, all_29_1_38, all_29_2_39, all_29_3_40, all_29_4_41, all_29_5_42, all_29_6_43, all_29_7_44, all_29_8_45 yields: % 49.32/15.51 | (133) isPrime0(xp) = all_29_5_42 & doDivides0(xp, xm) = all_29_0_37 & doDivides0(xp, xn) = all_29_1_38 & iLess0(all_29_3_40, all_0_3_3) = all_29_2_39 & sdtpldt0(all_29_4_41, xp) = all_29_3_40 & sdtpldt0(xn, xm) = all_29_4_41 & aNaturalNumber0(xp) = all_29_6_43 & aNaturalNumber0(xm) = all_29_7_44 & aNaturalNumber0(xn) = all_29_8_45 & ( ~ (all_29_2_39 = 0) | ~ (all_29_5_42 = 0) | ~ (all_29_6_43 = 0) | ~ (all_29_7_44 = 0) | ~ (all_29_8_45 = 0) | all_29_0_37 = 0 | all_29_1_38 = 0) % 49.32/15.52 | % 49.32/15.52 | Applying alpha-rule on (133) yields: % 49.32/15.52 | (134) doDivides0(xp, xn) = all_29_1_38 % 49.32/15.52 | (135) doDivides0(xp, xm) = all_29_0_37 % 49.32/15.52 | (136) aNaturalNumber0(xn) = all_29_8_45 % 49.32/15.52 | (137) aNaturalNumber0(xp) = all_29_6_43 % 49.32/15.52 | (138) isPrime0(xp) = all_29_5_42 % 49.32/15.52 | (139) sdtpldt0(xn, xm) = all_29_4_41 % 49.32/15.52 | (140) iLess0(all_29_3_40, all_0_3_3) = all_29_2_39 % 49.32/15.52 | (141) ~ (all_29_2_39 = 0) | ~ (all_29_5_42 = 0) | ~ (all_29_6_43 = 0) | ~ (all_29_7_44 = 0) | ~ (all_29_8_45 = 0) | all_29_0_37 = 0 | all_29_1_38 = 0 % 49.32/15.52 | (142) sdtpldt0(all_29_4_41, xp) = all_29_3_40 % 49.32/15.52 | (143) aNaturalNumber0(xm) = all_29_7_44 % 49.32/15.52 | % 49.32/15.52 +-Applying beta-rule and splitting (92), into two cases. % 49.32/15.52 |-Branch one: % 49.32/15.52 | (144) xp = sz00 % 49.32/15.52 | % 49.32/15.52 | Equations (144) can reduce 80 to: % 49.32/15.52 | (145) $false % 49.32/15.52 | % 49.32/15.52 |-The branch is then unsatisfiable % 49.32/15.52 |-Branch two: % 49.32/15.52 | (80) ~ (xp = sz00) % 49.32/15.52 | (147) xp = sz10 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, xp) = 0 & aNaturalNumber0(v0) = 0) % 49.32/15.52 | % 49.32/15.52 +-Applying beta-rule and splitting (147), into two cases. % 49.32/15.52 |-Branch one: % 49.32/15.52 | (148) xp = sz10 % 49.32/15.52 | % 49.32/15.52 | Equations (148) can reduce 79 to: % 49.32/15.52 | (145) $false % 49.32/15.52 | % 49.32/15.52 |-The branch is then unsatisfiable % 49.32/15.52 |-Branch two: % 49.32/15.52 | (79) ~ (xp = sz10) % 49.32/15.52 | (151) ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, xp) = 0 & aNaturalNumber0(v0) = 0) % 49.32/15.52 | % 49.32/15.52 | Instantiating (151) with all_39_0_46 yields: % 49.32/15.52 | (152) isPrime0(all_39_0_46) = 0 & doDivides0(all_39_0_46, xp) = 0 & aNaturalNumber0(all_39_0_46) = 0 % 49.32/15.52 | % 49.32/15.52 | Applying alpha-rule on (152) yields: % 49.32/15.52 | (153) isPrime0(all_39_0_46) = 0 % 49.32/15.52 | (154) doDivides0(all_39_0_46, xp) = 0 % 49.32/15.52 | (155) aNaturalNumber0(all_39_0_46) = 0 % 49.32/15.52 | % 49.32/15.52 | Using (153) and (24) yields: % 49.32/15.52 | (156) ~ (all_39_0_46 = sz10) % 49.32/15.52 | % 49.32/15.52 | Using (153) and (36) yields: % 49.32/15.52 | (157) ~ (all_39_0_46 = sz00) % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (43) with xp, all_29_5_42, 0 and discharging atoms isPrime0(xp) = all_29_5_42, isPrime0(xp) = 0, yields: % 49.32/15.52 | (158) all_29_5_42 = 0 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (30) with all_0_4_4, xp, all_29_3_40, all_0_3_3 and discharging atoms sdtpldt0(all_0_4_4, xp) = all_0_3_3, yields: % 49.32/15.52 | (159) all_29_3_40 = all_0_3_3 | ~ (sdtpldt0(all_0_4_4, xp) = all_29_3_40) % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (30) with xn, xm, all_29_4_41, all_0_4_4 and discharging atoms sdtpldt0(xn, xm) = all_29_4_41, sdtpldt0(xn, xm) = all_0_4_4, yields: % 49.32/15.52 | (160) all_29_4_41 = all_0_4_4 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xp, all_27_1_35, 0 and discharging atoms aNaturalNumber0(xp) = all_27_1_35, aNaturalNumber0(xp) = 0, yields: % 49.32/15.52 | (161) all_27_1_35 = 0 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xp, all_27_1_35, all_29_6_43 and discharging atoms aNaturalNumber0(xp) = all_29_6_43, aNaturalNumber0(xp) = all_27_1_35, yields: % 49.32/15.52 | (162) all_29_6_43 = all_27_1_35 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xp, all_25_2_31, all_29_6_43 and discharging atoms aNaturalNumber0(xp) = all_29_6_43, aNaturalNumber0(xp) = all_25_2_31, yields: % 49.32/15.52 | (163) all_29_6_43 = all_25_2_31 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xp, all_14_1_9, all_27_1_35 and discharging atoms aNaturalNumber0(xp) = all_27_1_35, aNaturalNumber0(xp) = all_14_1_9, yields: % 49.32/15.52 | (164) all_27_1_35 = all_14_1_9 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xm, all_25_3_32, 0 and discharging atoms aNaturalNumber0(xm) = all_25_3_32, aNaturalNumber0(xm) = 0, yields: % 49.32/15.52 | (165) all_25_3_32 = 0 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xm, all_23_1_27, all_25_3_32 and discharging atoms aNaturalNumber0(xm) = all_25_3_32, aNaturalNumber0(xm) = all_23_1_27, yields: % 49.32/15.52 | (166) all_25_3_32 = all_23_1_27 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xm, all_18_1_15, all_29_7_44 and discharging atoms aNaturalNumber0(xm) = all_29_7_44, aNaturalNumber0(xm) = all_18_1_15, yields: % 49.32/15.52 | (167) all_29_7_44 = all_18_1_15 % 49.32/15.52 | % 49.32/15.52 | Instantiating formula (58) with xm, all_16_1_12, all_23_1_27 and discharging atoms aNaturalNumber0(xm) = all_23_1_27, aNaturalNumber0(xm) = all_16_1_12, yields: % 49.32/15.53 | (168) all_23_1_27 = all_16_1_12 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xm, all_16_1_12, all_18_1_15 and discharging atoms aNaturalNumber0(xm) = all_18_1_15, aNaturalNumber0(xm) = all_16_1_12, yields: % 49.32/15.53 | (169) all_18_1_15 = all_16_1_12 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xm, all_12_1_6, all_29_7_44 and discharging atoms aNaturalNumber0(xm) = all_29_7_44, aNaturalNumber0(xm) = all_12_1_6, yields: % 49.32/15.53 | (170) all_29_7_44 = all_12_1_6 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_25_4_33, all_29_8_45 and discharging atoms aNaturalNumber0(xn) = all_29_8_45, aNaturalNumber0(xn) = all_25_4_33, yields: % 49.32/15.53 | (171) all_29_8_45 = all_25_4_33 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_23_2_28, 0 and discharging atoms aNaturalNumber0(xn) = all_23_2_28, aNaturalNumber0(xn) = 0, yields: % 49.32/15.53 | (172) all_23_2_28 = 0 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_23_2_28, all_29_8_45 and discharging atoms aNaturalNumber0(xn) = all_29_8_45, aNaturalNumber0(xn) = all_23_2_28, yields: % 49.32/15.53 | (173) all_29_8_45 = all_23_2_28 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_18_2_16, all_25_4_33 and discharging atoms aNaturalNumber0(xn) = all_25_4_33, aNaturalNumber0(xn) = all_18_2_16, yields: % 49.32/15.53 | (174) all_25_4_33 = all_18_2_16 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_16_2_13, all_29_8_45 and discharging atoms aNaturalNumber0(xn) = all_29_8_45, aNaturalNumber0(xn) = all_16_2_13, yields: % 49.32/15.53 | (175) all_29_8_45 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Instantiating formula (58) with xn, all_12_2_7, all_25_4_33 and discharging atoms aNaturalNumber0(xn) = all_25_4_33, aNaturalNumber0(xn) = all_12_2_7, yields: % 49.32/15.53 | (176) all_25_4_33 = all_12_2_7 % 49.32/15.53 | % 49.32/15.53 | Combining equations (162,163) yields a new equation: % 49.32/15.53 | (177) all_27_1_35 = all_25_2_31 % 49.32/15.53 | % 49.32/15.53 | Simplifying 177 yields: % 49.32/15.53 | (178) all_27_1_35 = all_25_2_31 % 49.32/15.53 | % 49.32/15.53 | Combining equations (167,170) yields a new equation: % 49.32/15.53 | (179) all_18_1_15 = all_12_1_6 % 49.32/15.53 | % 49.32/15.53 | Simplifying 179 yields: % 49.32/15.53 | (180) all_18_1_15 = all_12_1_6 % 49.32/15.53 | % 49.32/15.53 | Combining equations (171,175) yields a new equation: % 49.32/15.53 | (181) all_25_4_33 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Simplifying 181 yields: % 49.32/15.53 | (182) all_25_4_33 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Combining equations (173,175) yields a new equation: % 49.32/15.53 | (183) all_23_2_28 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Simplifying 183 yields: % 49.32/15.53 | (184) all_23_2_28 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Combining equations (161,178) yields a new equation: % 49.32/15.53 | (185) all_25_2_31 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (164,178) yields a new equation: % 49.32/15.53 | (186) all_25_2_31 = all_14_1_9 % 49.32/15.53 | % 49.32/15.53 | Combining equations (185,186) yields a new equation: % 49.32/15.53 | (187) all_14_1_9 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (166,165) yields a new equation: % 49.32/15.53 | (188) all_23_1_27 = 0 % 49.32/15.53 | % 49.32/15.53 | Simplifying 188 yields: % 49.32/15.53 | (189) all_23_1_27 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (182,174) yields a new equation: % 49.32/15.53 | (190) all_18_2_16 = all_16_2_13 % 49.32/15.53 | % 49.32/15.53 | Combining equations (176,174) yields a new equation: % 49.32/15.53 | (191) all_18_2_16 = all_12_2_7 % 49.32/15.53 | % 49.32/15.53 | Combining equations (168,189) yields a new equation: % 49.32/15.53 | (192) all_16_1_12 = 0 % 49.32/15.53 | % 49.32/15.53 | Simplifying 192 yields: % 49.32/15.53 | (193) all_16_1_12 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (184,172) yields a new equation: % 49.32/15.53 | (194) all_16_2_13 = 0 % 49.32/15.53 | % 49.32/15.53 | Simplifying 194 yields: % 49.32/15.53 | (195) all_16_2_13 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (169,180) yields a new equation: % 49.32/15.53 | (196) all_16_1_12 = all_12_1_6 % 49.32/15.53 | % 49.32/15.53 | Simplifying 196 yields: % 49.32/15.53 | (197) all_16_1_12 = all_12_1_6 % 49.32/15.53 | % 49.32/15.53 | Combining equations (190,191) yields a new equation: % 49.32/15.53 | (198) all_16_2_13 = all_12_2_7 % 49.32/15.53 | % 49.32/15.53 | Simplifying 198 yields: % 49.32/15.53 | (199) all_16_2_13 = all_12_2_7 % 49.32/15.53 | % 49.32/15.53 | Combining equations (197,193) yields a new equation: % 49.32/15.53 | (200) all_12_1_6 = 0 % 49.32/15.53 | % 49.32/15.53 | Simplifying 200 yields: % 49.32/15.53 | (201) all_12_1_6 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (195,199) yields a new equation: % 49.32/15.53 | (202) all_12_2_7 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (202,199) yields a new equation: % 49.32/15.53 | (195) all_16_2_13 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (202,191) yields a new equation: % 49.32/15.53 | (204) all_18_2_16 = 0 % 49.32/15.53 | % 49.32/15.53 | Combining equations (201,180) yields a new equation: % 49.32/15.53 | (205) all_18_1_15 = 0 % 49.32/15.53 | % 49.32/15.53 | From (158) and (138) follows: % 49.32/15.53 | (50) isPrime0(xp) = 0 % 49.32/15.53 | % 49.32/15.53 | From (160) and (142) follows: % 49.32/15.53 | (207) sdtpldt0(all_0_4_4, xp) = all_29_3_40 % 49.32/15.53 | % 49.32/15.53 | From (187) and (101) follows: % 49.32/15.53 | (23) aNaturalNumber0(xp) = 0 % 49.32/15.53 | % 49.32/15.53 | From (201) and (95) follows: % 49.32/15.53 | (48) aNaturalNumber0(xm) = 0 % 49.32/15.53 | % 49.32/15.53 | From (202) and (96) follows: % 49.32/15.53 | (16) aNaturalNumber0(xn) = 0 % 49.32/15.53 | % 49.32/15.53 +-Applying beta-rule and splitting (114), into two cases. % 49.32/15.53 |-Branch one: % 49.32/15.53 | (211) all_21_0_20 = xp & all_21_1_21 = 0 & sdtpldt0(xm, all_21_2_22) = xp & aNaturalNumber0(all_21_2_22) = 0 % 49.32/15.53 | % 49.32/15.53 | Applying alpha-rule on (211) yields: % 49.32/15.53 | (212) all_21_0_20 = xp % 49.32/15.53 | (213) all_21_1_21 = 0 % 49.32/15.53 | (214) sdtpldt0(xm, all_21_2_22) = xp % 49.32/15.53 | (215) aNaturalNumber0(all_21_2_22) = 0 % 49.32/15.53 | % 49.32/15.53 +-Applying beta-rule and splitting (159), into two cases. % 49.32/15.53 |-Branch one: % 49.32/15.53 | (216) ~ (sdtpldt0(all_0_4_4, xp) = all_29_3_40) % 49.32/15.53 | % 49.32/15.53 | Using (207) and (216) yields: % 49.32/15.53 | (217) $false % 49.32/15.53 | % 49.32/15.53 |-The branch is then unsatisfiable % 49.32/15.53 |-Branch two: % 49.32/15.53 | (207) sdtpldt0(all_0_4_4, xp) = all_29_3_40 % 49.32/15.53 | (219) all_29_3_40 = all_0_3_3 % 49.32/15.53 | % 49.32/15.53 | From (219) and (207) follows: % 49.32/15.53 | (26) sdtpldt0(all_0_4_4, xp) = all_0_3_3 % 49.32/15.53 | % 49.32/15.53 +-Applying beta-rule and splitting (113), into two cases. % 49.32/15.53 |-Branch one: % 49.32/15.53 | (221) all_20_0_17 = xp & all_20_1_18 = 0 & sdtpldt0(xn, all_20_2_19) = xp & aNaturalNumber0(all_20_2_19) = 0 % 49.32/15.53 | % 49.32/15.53 | Applying alpha-rule on (221) yields: % 49.32/15.53 | (222) all_20_0_17 = xp % 49.32/15.53 | (223) all_20_1_18 = 0 % 49.32/15.53 | (224) sdtpldt0(xn, all_20_2_19) = xp % 49.32/15.53 | (225) aNaturalNumber0(all_20_2_19) = 0 % 49.32/15.53 | % 49.32/15.54 +-Applying beta-rule and splitting (107), into two cases. % 49.32/15.54 |-Branch one: % 49.32/15.54 | (226) ~ (all_16_1_12 = 0) % 49.32/15.54 | % 49.32/15.54 | Equations (193) can reduce 226 to: % 49.32/15.54 | (145) $false % 49.32/15.54 | % 49.32/15.54 |-The branch is then unsatisfiable % 49.32/15.54 |-Branch two: % 49.32/15.54 | (193) all_16_1_12 = 0 % 49.32/15.54 | (229) ~ (all_16_2_13 = 0) | all_16_0_11 = all_0_4_4 % 49.32/15.54 | % 49.32/15.54 +-Applying beta-rule and splitting (112), into two cases. % 49.32/15.54 |-Branch one: % 49.32/15.54 | (230) ~ (all_18_1_15 = 0) % 49.32/15.54 | % 49.32/15.54 | Equations (205) can reduce 230 to: % 49.32/15.54 | (145) $false % 49.32/15.54 | % 49.32/15.54 |-The branch is then unsatisfiable % 49.32/15.54 |-Branch two: % 49.32/15.54 | (205) all_18_1_15 = 0 % 49.32/15.54 | (233) ~ (all_18_2_16 = 0) | all_18_0_14 = 0 % 49.32/15.54 | % 49.32/15.54 +-Applying beta-rule and splitting (233), into two cases. % 49.32/15.54 |-Branch one: % 49.32/15.54 | (234) ~ (all_18_2_16 = 0) % 49.32/15.54 | % 49.32/15.54 | Equations (204) can reduce 234 to: % 49.32/15.54 | (145) $false % 49.32/15.54 | % 49.32/15.54 |-The branch is then unsatisfiable % 49.32/15.54 |-Branch two: % 49.32/15.54 | (204) all_18_2_16 = 0 % 49.32/15.54 | (237) all_18_0_14 = 0 % 49.32/15.54 | % 49.32/15.54 | From (237) and (109) follows: % 49.58/15.54 | (238) aNaturalNumber0(all_0_2_2) = 0 % 49.58/15.54 | % 49.58/15.54 +-Applying beta-rule and splitting (115), into two cases. % 49.58/15.54 |-Branch one: % 49.58/15.54 | (239) all_22_0_23 = all_0_2_2 & all_22_1_24 = 0 & sdtasdt0(xp, all_22_2_25) = all_0_2_2 & aNaturalNumber0(all_22_2_25) = 0 % 49.58/15.54 | % 49.58/15.54 | Applying alpha-rule on (239) yields: % 49.58/15.54 | (240) all_22_0_23 = all_0_2_2 % 49.58/15.54 | (241) all_22_1_24 = 0 % 49.58/15.54 | (242) sdtasdt0(xp, all_22_2_25) = all_0_2_2 % 49.58/15.54 | (243) aNaturalNumber0(all_22_2_25) = 0 % 49.58/15.54 | % 49.58/15.54 +-Applying beta-rule and splitting (229), into two cases. % 49.58/15.54 |-Branch one: % 49.58/15.54 | (244) ~ (all_16_2_13 = 0) % 49.58/15.54 | % 49.58/15.54 | Equations (195) can reduce 244 to: % 49.58/15.54 | (145) $false % 49.58/15.54 | % 49.58/15.54 |-The branch is then unsatisfiable % 49.58/15.54 |-Branch two: % 49.58/15.54 | (195) all_16_2_13 = 0 % 49.58/15.54 | (247) all_16_0_11 = all_0_4_4 % 49.58/15.54 | % 49.58/15.54 | From (247) and (104) follows: % 49.58/15.54 | (248) sdtpldt0(xm, xn) = all_0_4_4 % 49.58/15.54 | % 49.58/15.54 +-Applying beta-rule and splitting (120), into two cases. % 49.58/15.54 |-Branch one: % 49.58/15.54 | (249) ~ (all_23_1_27 = 0) % 49.58/15.54 | % 49.58/15.54 | Equations (189) can reduce 249 to: % 49.58/15.54 | (145) $false % 49.58/15.54 | % 49.58/15.54 |-The branch is then unsatisfiable % 49.58/15.54 |-Branch two: % 49.58/15.54 | (189) all_23_1_27 = 0 % 49.58/15.54 | (252) ~ (all_23_2_28 = 0) | all_23_0_26 = all_0_2_2 % 49.58/15.54 | % 49.58/15.54 +-Applying beta-rule and splitting (252), into two cases. % 49.58/15.54 |-Branch one: % 49.58/15.54 | (253) ~ (all_23_2_28 = 0) % 49.58/15.54 | % 49.58/15.54 | Equations (172) can reduce 253 to: % 49.58/15.54 | (145) $false % 49.58/15.54 | % 49.58/15.54 |-The branch is then unsatisfiable % 49.58/15.54 |-Branch two: % 49.58/15.54 | (172) all_23_2_28 = 0 % 49.58/15.54 | (256) all_23_0_26 = all_0_2_2 % 49.58/15.54 | % 49.58/15.54 | From (256) and (117) follows: % 49.58/15.54 | (257) sdtasdt0(xm, xn) = all_0_2_2 % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (69) with all_39_0_46, xp and discharging atoms isPrime0(xp) = 0, doDivides0(all_39_0_46, xp) = 0, yields: % 49.58/15.54 | (258) all_39_0_46 = xp | all_39_0_46 = sz10 | ? [v0] : (( ~ (v0 = 0) & aNaturalNumber0(all_39_0_46) = v0) | ( ~ (v0 = 0) & aNaturalNumber0(xp) = v0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (72) with xp, all_39_0_46 and discharging atoms doDivides0(all_39_0_46, xp) = 0, yields: % 49.58/15.54 | (259) xp = sz00 | ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_39_0_46, xp) = v2 & aNaturalNumber0(all_39_0_46) = v0 & aNaturalNumber0(xp) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (71) with all_22_2_25, xk, all_0_2_2, xp and discharging atoms sdtsldt0(all_0_2_2, xp) = xk, sdtasdt0(xp, all_22_2_25) = all_0_2_2, yields: % 49.58/15.54 | (260) all_22_2_25 = xk | xp = sz00 | ? [v0] : ? [v1] : ? [v2] : (( ~ (v0 = 0) & aNaturalNumber0(all_22_2_25) = v0) | (doDivides0(xp, all_0_2_2) = v2 & aNaturalNumber0(all_0_2_2) = v1 & aNaturalNumber0(xp) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0)))) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (40) with all_0_2_2, xp, all_22_2_25, xp and discharging atoms doDivides0(xp, all_0_2_2) = 0, sdtasdt0(xp, all_22_2_25) = all_0_2_2, yields: % 49.58/15.54 | (261) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (isPrime0(xp) = v3 & doDivides0(xp, all_22_2_25) = v8 & doDivides0(xp, xp) = v7 & iLess0(v5, all_0_3_3) = v6 & sdtpldt0(v4, xp) = v5 & sdtpldt0(xp, all_22_2_25) = v4 & aNaturalNumber0(all_22_2_25) = v1 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xp) = v0 & ( ~ (v6 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v8 = 0 | v7 = 0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (11) with all_0_2_2, all_22_2_25, xp and discharging atoms sdtasdt0(xp, all_22_2_25) = all_0_2_2, yields: % 49.58/15.54 | (262) ? [v0] : ? [v1] : ? [v2] : (sdtasdt0(all_22_2_25, xp) = v2 & aNaturalNumber0(all_22_2_25) = v1 & aNaturalNumber0(xp) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_2_2)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (40) with all_0_2_2, xp, xn, xm and discharging atoms doDivides0(xp, all_0_2_2) = 0, sdtasdt0(xm, xn) = all_0_2_2, yields: % 49.58/15.54 | (263) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (isPrime0(xp) = v3 & doDivides0(xp, xm) = v7 & doDivides0(xp, xn) = v8 & iLess0(v5, all_0_3_3) = v6 & sdtpldt0(v4, xp) = v5 & sdtpldt0(xm, xn) = v4 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & ( ~ (v6 = 0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v8 = 0 | v7 = 0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (74) with xp, all_21_2_22, xm, all_39_0_46 and discharging atoms doDivides0(all_39_0_46, xp) = 0, sdtpldt0(xm, all_21_2_22) = xp, yields: % 49.58/15.54 | (264) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (doDivides0(all_39_0_46, all_21_2_22) = v4 & doDivides0(all_39_0_46, xm) = v3 & aNaturalNumber0(all_39_0_46) = v0 & aNaturalNumber0(all_21_2_22) = v2 & aNaturalNumber0(xm) = v1 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = 0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (47) with all_25_1_30, xp, xm and discharging atoms sdtpldt0(xm, xp) = all_25_1_30, yields: % 49.58/15.54 | (265) ? [v0] : ? [v1] : ? [v2] : (sdtpldt0(xp, xm) = v2 & aNaturalNumber0(xp) = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_25_1_30)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (25) with all_25_1_30, xp, xm and discharging atoms sdtpldt0(xm, xp) = all_25_1_30, yields: % 49.58/15.54 | (266) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_25_1_30) = v2 & aNaturalNumber0(xp) = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (27) with all_0_3_3, all_0_4_4, xp, xn, xm and discharging atoms sdtpldt0(all_0_4_4, xp) = all_0_3_3, sdtpldt0(xm, xn) = all_0_4_4, yields: % 49.58/15.54 | (267) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtpldt0(xm, v3) = v4 & sdtpldt0(xn, xp) = v3 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = all_0_3_3)) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (21) with all_25_1_30, all_0_4_4, xp, xn, xm and discharging atoms sdtpldt0(xm, xp) = all_25_1_30, sdtpldt0(xm, xn) = all_0_4_4, yields: % 49.58/15.54 | (268) xp = xn | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtpldt0(xp, xm) = v4 & sdtpldt0(xn, xm) = v3 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v4 = v3) & ~ (all_25_1_30 = all_0_4_4)))) % 49.58/15.54 | % 49.58/15.54 | Instantiating formula (74) with xp, all_20_2_19, xn, all_39_0_46 and discharging atoms doDivides0(all_39_0_46, xp) = 0, sdtpldt0(xn, all_20_2_19) = xp, yields: % 49.58/15.54 | (269) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (doDivides0(all_39_0_46, all_20_2_19) = v4 & doDivides0(all_39_0_46, xn) = v3 & aNaturalNumber0(all_39_0_46) = v0 & aNaturalNumber0(all_20_2_19) = v2 & aNaturalNumber0(xn) = v1 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = 0)) % 49.58/15.55 | % 49.58/15.55 | Instantiating formula (32) with all_39_0_46 and discharging atoms aNaturalNumber0(all_39_0_46) = 0, yields: % 49.58/15.55 | (270) all_39_0_46 = sz10 | all_39_0_46 = sz00 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_39_0_46) = 0 & aNaturalNumber0(v0) = 0) % 49.58/15.55 | % 49.58/15.55 | Instantiating formula (32) with all_22_2_25 and discharging atoms aNaturalNumber0(all_22_2_25) = 0, yields: % 49.58/15.55 | (271) all_22_2_25 = sz10 | all_22_2_25 = sz00 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_22_2_25) = 0 & aNaturalNumber0(v0) = 0) % 49.58/15.55 | % 49.58/15.55 | Instantiating (267) with all_142_0_55, all_142_1_56, all_142_2_57, all_142_3_58, all_142_4_59 yields: % 49.58/15.55 | (272) sdtpldt0(xm, all_142_1_56) = all_142_0_55 & sdtpldt0(xn, xp) = all_142_1_56 & aNaturalNumber0(xp) = all_142_2_57 & aNaturalNumber0(xm) = all_142_4_59 & aNaturalNumber0(xn) = all_142_3_58 & ( ~ (all_142_2_57 = 0) | ~ (all_142_3_58 = 0) | ~ (all_142_4_59 = 0) | all_142_0_55 = all_0_3_3) % 49.58/15.55 | % 49.58/15.55 | Applying alpha-rule on (272) yields: % 49.58/15.55 | (273) sdtpldt0(xm, all_142_1_56) = all_142_0_55 % 49.58/15.55 | (274) sdtpldt0(xn, xp) = all_142_1_56 % 49.58/15.55 | (275) aNaturalNumber0(xm) = all_142_4_59 % 49.58/15.55 | (276) aNaturalNumber0(xn) = all_142_3_58 % 49.58/15.55 | (277) aNaturalNumber0(xp) = all_142_2_57 % 49.58/15.55 | (278) ~ (all_142_2_57 = 0) | ~ (all_142_3_58 = 0) | ~ (all_142_4_59 = 0) | all_142_0_55 = all_0_3_3 % 49.58/15.55 | % 49.58/15.55 | Instantiating (266) with all_144_0_60, all_144_1_61, all_144_2_62 yields: % 49.58/15.55 | (279) aNaturalNumber0(all_25_1_30) = all_144_0_60 & aNaturalNumber0(xp) = all_144_1_61 & aNaturalNumber0(xm) = all_144_2_62 & ( ~ (all_144_1_61 = 0) | ~ (all_144_2_62 = 0) | all_144_0_60 = 0) % 49.58/15.55 | % 49.58/15.55 | Applying alpha-rule on (279) yields: % 49.58/15.55 | (280) aNaturalNumber0(all_25_1_30) = all_144_0_60 % 49.58/15.55 | (281) aNaturalNumber0(xp) = all_144_1_61 % 49.58/15.55 | (282) aNaturalNumber0(xm) = all_144_2_62 % 49.58/15.55 | (283) ~ (all_144_1_61 = 0) | ~ (all_144_2_62 = 0) | all_144_0_60 = 0 % 49.58/15.55 | % 49.58/15.55 | Instantiating (265) with all_146_0_63, all_146_1_64, all_146_2_65 yields: % 49.58/15.55 | (284) sdtpldt0(xp, xm) = all_146_0_63 & aNaturalNumber0(xp) = all_146_1_64 & aNaturalNumber0(xm) = all_146_2_65 & ( ~ (all_146_1_64 = 0) | ~ (all_146_2_65 = 0) | all_146_0_63 = all_25_1_30) % 49.58/15.55 | % 49.58/15.55 | Applying alpha-rule on (284) yields: % 49.58/15.55 | (285) sdtpldt0(xp, xm) = all_146_0_63 % 49.58/15.55 | (286) aNaturalNumber0(xp) = all_146_1_64 % 49.58/15.55 | (287) aNaturalNumber0(xm) = all_146_2_65 % 49.58/15.55 | (288) ~ (all_146_1_64 = 0) | ~ (all_146_2_65 = 0) | all_146_0_63 = all_25_1_30 % 49.58/15.55 | % 49.58/15.55 | Instantiating (264) with all_150_0_69, all_150_1_70, all_150_2_71, all_150_3_72, all_150_4_73 yields: % 49.58/15.55 | (289) doDivides0(all_39_0_46, all_21_2_22) = all_150_0_69 & doDivides0(all_39_0_46, xm) = all_150_1_70 & aNaturalNumber0(all_39_0_46) = all_150_4_73 & aNaturalNumber0(all_21_2_22) = all_150_2_71 & aNaturalNumber0(xm) = all_150_3_72 & ( ~ (all_150_1_70 = 0) | ~ (all_150_2_71 = 0) | ~ (all_150_3_72 = 0) | ~ (all_150_4_73 = 0) | all_150_0_69 = 0) % 49.58/15.55 | % 49.58/15.55 | Applying alpha-rule on (289) yields: % 49.58/15.55 | (290) aNaturalNumber0(all_21_2_22) = all_150_2_71 % 49.58/15.55 | (291) aNaturalNumber0(xm) = all_150_3_72 % 49.58/15.55 | (292) doDivides0(all_39_0_46, xm) = all_150_1_70 % 49.58/15.55 | (293) doDivides0(all_39_0_46, all_21_2_22) = all_150_0_69 % 49.58/15.55 | (294) ~ (all_150_1_70 = 0) | ~ (all_150_2_71 = 0) | ~ (all_150_3_72 = 0) | ~ (all_150_4_73 = 0) | all_150_0_69 = 0 % 49.58/15.55 | (295) aNaturalNumber0(all_39_0_46) = all_150_4_73 % 49.58/15.55 | % 49.58/15.55 | Instantiating (269) with all_152_0_74, all_152_1_75, all_152_2_76, all_152_3_77, all_152_4_78 yields: % 49.58/15.55 | (296) doDivides0(all_39_0_46, all_20_2_19) = all_152_0_74 & doDivides0(all_39_0_46, xn) = all_152_1_75 & aNaturalNumber0(all_39_0_46) = all_152_4_78 & aNaturalNumber0(all_20_2_19) = all_152_2_76 & aNaturalNumber0(xn) = all_152_3_77 & ( ~ (all_152_1_75 = 0) | ~ (all_152_2_76 = 0) | ~ (all_152_3_77 = 0) | ~ (all_152_4_78 = 0) | all_152_0_74 = 0) % 49.58/15.55 | % 49.58/15.55 | Applying alpha-rule on (296) yields: % 49.58/15.55 | (297) aNaturalNumber0(xn) = all_152_3_77 % 49.58/15.55 | (298) doDivides0(all_39_0_46, xn) = all_152_1_75 % 49.58/15.55 | (299) aNaturalNumber0(all_20_2_19) = all_152_2_76 % 49.58/15.55 | (300) doDivides0(all_39_0_46, all_20_2_19) = all_152_0_74 % 49.58/15.55 | (301) aNaturalNumber0(all_39_0_46) = all_152_4_78 % 49.66/15.55 | (302) ~ (all_152_1_75 = 0) | ~ (all_152_2_76 = 0) | ~ (all_152_3_77 = 0) | ~ (all_152_4_78 = 0) | all_152_0_74 = 0 % 49.66/15.55 | % 49.66/15.55 | Instantiating (262) with all_158_0_87, all_158_1_88, all_158_2_89 yields: % 49.66/15.55 | (303) sdtasdt0(all_22_2_25, xp) = all_158_0_87 & aNaturalNumber0(all_22_2_25) = all_158_1_88 & aNaturalNumber0(xp) = all_158_2_89 & ( ~ (all_158_1_88 = 0) | ~ (all_158_2_89 = 0) | all_158_0_87 = all_0_2_2) % 49.66/15.55 | % 49.66/15.55 | Applying alpha-rule on (303) yields: % 49.66/15.55 | (304) sdtasdt0(all_22_2_25, xp) = all_158_0_87 % 49.66/15.55 | (305) aNaturalNumber0(all_22_2_25) = all_158_1_88 % 49.66/15.55 | (306) aNaturalNumber0(xp) = all_158_2_89 % 49.66/15.55 | (307) ~ (all_158_1_88 = 0) | ~ (all_158_2_89 = 0) | all_158_0_87 = all_0_2_2 % 49.66/15.55 | % 49.66/15.55 | Instantiating (261) with all_160_0_90, all_160_1_91, all_160_2_92, all_160_3_93, all_160_4_94, all_160_5_95, all_160_6_96, all_160_7_97, all_160_8_98 yields: % 49.66/15.55 | (308) isPrime0(xp) = all_160_5_95 & doDivides0(xp, all_22_2_25) = all_160_0_90 & doDivides0(xp, xp) = all_160_1_91 & iLess0(all_160_3_93, all_0_3_3) = all_160_2_92 & sdtpldt0(all_160_4_94, xp) = all_160_3_93 & sdtpldt0(xp, all_22_2_25) = all_160_4_94 & aNaturalNumber0(all_22_2_25) = all_160_7_97 & aNaturalNumber0(xp) = all_160_6_96 & aNaturalNumber0(xp) = all_160_8_98 & ( ~ (all_160_2_92 = 0) | ~ (all_160_5_95 = 0) | ~ (all_160_6_96 = 0) | ~ (all_160_7_97 = 0) | ~ (all_160_8_98 = 0) | all_160_0_90 = 0 | all_160_1_91 = 0) % 49.66/15.55 | % 49.66/15.55 | Applying alpha-rule on (308) yields: % 49.66/15.55 | (309) ~ (all_160_2_92 = 0) | ~ (all_160_5_95 = 0) | ~ (all_160_6_96 = 0) | ~ (all_160_7_97 = 0) | ~ (all_160_8_98 = 0) | all_160_0_90 = 0 | all_160_1_91 = 0 % 49.66/15.55 | (310) isPrime0(xp) = all_160_5_95 % 49.66/15.55 | (311) doDivides0(xp, xp) = all_160_1_91 % 49.66/15.55 | (312) sdtpldt0(all_160_4_94, xp) = all_160_3_93 % 49.66/15.55 | (313) aNaturalNumber0(all_22_2_25) = all_160_7_97 % 49.66/15.55 | (314) aNaturalNumber0(xp) = all_160_8_98 % 49.66/15.55 | (315) iLess0(all_160_3_93, all_0_3_3) = all_160_2_92 % 49.66/15.55 | (316) sdtpldt0(xp, all_22_2_25) = all_160_4_94 % 49.66/15.55 | (317) doDivides0(xp, all_22_2_25) = all_160_0_90 % 49.66/15.55 | (318) aNaturalNumber0(xp) = all_160_6_96 % 49.66/15.55 | % 49.66/15.55 | Instantiating (263) with all_163_0_102, all_163_1_103, all_163_2_104, all_163_3_105, all_163_4_106, all_163_5_107, all_163_6_108, all_163_7_109, all_163_8_110 yields: % 49.66/15.55 | (319) isPrime0(xp) = all_163_5_107 & doDivides0(xp, xm) = all_163_1_103 & doDivides0(xp, xn) = all_163_0_102 & iLess0(all_163_3_105, all_0_3_3) = all_163_2_104 & sdtpldt0(all_163_4_106, xp) = all_163_3_105 & sdtpldt0(xm, xn) = all_163_4_106 & aNaturalNumber0(xp) = all_163_6_108 & aNaturalNumber0(xm) = all_163_8_110 & aNaturalNumber0(xn) = all_163_7_109 & ( ~ (all_163_2_104 = 0) | ~ (all_163_5_107 = 0) | ~ (all_163_6_108 = 0) | ~ (all_163_7_109 = 0) | ~ (all_163_8_110 = 0) | all_163_0_102 = 0 | all_163_1_103 = 0) % 49.66/15.55 | % 49.66/15.55 | Applying alpha-rule on (319) yields: % 49.66/15.55 | (320) doDivides0(xp, xn) = all_163_0_102 % 49.66/15.55 | (321) aNaturalNumber0(xm) = all_163_8_110 % 49.66/15.55 | (322) ~ (all_163_2_104 = 0) | ~ (all_163_5_107 = 0) | ~ (all_163_6_108 = 0) | ~ (all_163_7_109 = 0) | ~ (all_163_8_110 = 0) | all_163_0_102 = 0 | all_163_1_103 = 0 % 49.66/15.55 | (323) sdtpldt0(xm, xn) = all_163_4_106 % 49.66/15.55 | (324) sdtpldt0(all_163_4_106, xp) = all_163_3_105 % 49.66/15.55 | (325) aNaturalNumber0(xn) = all_163_7_109 % 49.66/15.55 | (326) isPrime0(xp) = all_163_5_107 % 49.66/15.55 | (327) doDivides0(xp, xm) = all_163_1_103 % 49.66/15.55 | (328) iLess0(all_163_3_105, all_0_3_3) = all_163_2_104 % 49.66/15.55 | (329) aNaturalNumber0(xp) = all_163_6_108 % 49.66/15.55 | % 49.66/15.55 +-Applying beta-rule and splitting (259), into two cases. % 49.66/15.55 |-Branch one: % 49.66/15.55 | (144) xp = sz00 % 49.66/15.55 | % 49.66/15.55 | Equations (144) can reduce 80 to: % 49.66/15.55 | (145) $false % 49.66/15.55 | % 49.66/15.55 |-The branch is then unsatisfiable % 49.66/15.55 |-Branch two: % 49.66/15.55 | (80) ~ (xp = sz00) % 49.66/15.55 | (333) ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_39_0_46, xp) = v2 & aNaturalNumber0(all_39_0_46) = v0 & aNaturalNumber0(xp) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.66/15.55 | % 49.66/15.55 | Instantiating (333) with all_171_0_114, all_171_1_115, all_171_2_116 yields: % 49.66/15.55 | (334) sdtlseqdt0(all_39_0_46, xp) = all_171_0_114 & aNaturalNumber0(all_39_0_46) = all_171_2_116 & aNaturalNumber0(xp) = all_171_1_115 & ( ~ (all_171_1_115 = 0) | ~ (all_171_2_116 = 0) | all_171_0_114 = 0) % 49.66/15.55 | % 49.66/15.55 | Applying alpha-rule on (334) yields: % 49.66/15.55 | (335) sdtlseqdt0(all_39_0_46, xp) = all_171_0_114 % 49.66/15.56 | (336) aNaturalNumber0(all_39_0_46) = all_171_2_116 % 49.66/15.56 | (337) aNaturalNumber0(xp) = all_171_1_115 % 49.66/15.56 | (338) ~ (all_171_1_115 = 0) | ~ (all_171_2_116 = 0) | all_171_0_114 = 0 % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (270), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (339) all_39_0_46 = sz00 % 49.66/15.56 | % 49.66/15.56 | Equations (339) can reduce 157 to: % 49.66/15.56 | (145) $false % 49.66/15.56 | % 49.66/15.56 |-The branch is then unsatisfiable % 49.66/15.56 |-Branch two: % 49.66/15.56 | (157) ~ (all_39_0_46 = sz00) % 49.66/15.56 | (342) all_39_0_46 = sz10 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_39_0_46) = 0 & aNaturalNumber0(v0) = 0) % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (342), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (343) all_39_0_46 = sz10 % 49.66/15.56 | % 49.66/15.56 | Equations (343) can reduce 156 to: % 49.66/15.56 | (145) $false % 49.66/15.56 | % 49.66/15.56 |-The branch is then unsatisfiable % 49.66/15.56 |-Branch two: % 49.66/15.56 | (156) ~ (all_39_0_46 = sz10) % 49.66/15.56 | (346) ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_39_0_46) = 0 & aNaturalNumber0(v0) = 0) % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with all_39_0_46, all_171_2_116, 0 and discharging atoms aNaturalNumber0(all_39_0_46) = all_171_2_116, aNaturalNumber0(all_39_0_46) = 0, yields: % 49.66/15.56 | (347) all_171_2_116 = 0 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with all_39_0_46, all_152_4_78, all_171_2_116 and discharging atoms aNaturalNumber0(all_39_0_46) = all_171_2_116, aNaturalNumber0(all_39_0_46) = all_152_4_78, yields: % 49.66/15.56 | (348) all_171_2_116 = all_152_4_78 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with all_39_0_46, all_150_4_73, all_171_2_116 and discharging atoms aNaturalNumber0(all_39_0_46) = all_171_2_116, aNaturalNumber0(all_39_0_46) = all_150_4_73, yields: % 49.66/15.56 | (349) all_171_2_116 = all_150_4_73 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with all_22_2_25, all_160_7_97, 0 and discharging atoms aNaturalNumber0(all_22_2_25) = all_160_7_97, aNaturalNumber0(all_22_2_25) = 0, yields: % 49.66/15.56 | (350) all_160_7_97 = 0 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with all_22_2_25, all_158_1_88, all_160_7_97 and discharging atoms aNaturalNumber0(all_22_2_25) = all_160_7_97, aNaturalNumber0(all_22_2_25) = all_158_1_88, yields: % 49.66/15.56 | (351) all_160_7_97 = all_158_1_88 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_160_6_96, 0 and discharging atoms aNaturalNumber0(xp) = all_160_6_96, aNaturalNumber0(xp) = 0, yields: % 49.66/15.56 | (352) all_160_6_96 = 0 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_160_8_98, all_163_6_108 and discharging atoms aNaturalNumber0(xp) = all_163_6_108, aNaturalNumber0(xp) = all_160_8_98, yields: % 49.66/15.56 | (353) all_163_6_108 = all_160_8_98 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_158_2_89, all_171_1_115 and discharging atoms aNaturalNumber0(xp) = all_171_1_115, aNaturalNumber0(xp) = all_158_2_89, yields: % 49.66/15.56 | (354) all_171_1_115 = all_158_2_89 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_158_2_89, all_160_8_98 and discharging atoms aNaturalNumber0(xp) = all_160_8_98, aNaturalNumber0(xp) = all_158_2_89, yields: % 49.66/15.56 | (355) all_160_8_98 = all_158_2_89 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_146_1_64, all_171_1_115 and discharging atoms aNaturalNumber0(xp) = all_171_1_115, aNaturalNumber0(xp) = all_146_1_64, yields: % 49.66/15.56 | (356) all_171_1_115 = all_146_1_64 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_144_1_61, all_160_6_96 and discharging atoms aNaturalNumber0(xp) = all_160_6_96, aNaturalNumber0(xp) = all_144_1_61, yields: % 49.66/15.56 | (357) all_160_6_96 = all_144_1_61 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_144_1_61, all_158_2_89 and discharging atoms aNaturalNumber0(xp) = all_158_2_89, aNaturalNumber0(xp) = all_144_1_61, yields: % 49.66/15.56 | (358) all_158_2_89 = all_144_1_61 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_142_2_57, all_163_6_108 and discharging atoms aNaturalNumber0(xp) = all_163_6_108, aNaturalNumber0(xp) = all_142_2_57, yields: % 49.66/15.56 | (359) all_163_6_108 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Combining equations (354,356) yields a new equation: % 49.66/15.56 | (360) all_158_2_89 = all_146_1_64 % 49.66/15.56 | % 49.66/15.56 | Simplifying 360 yields: % 49.66/15.56 | (361) all_158_2_89 = all_146_1_64 % 49.66/15.56 | % 49.66/15.56 | Combining equations (349,348) yields a new equation: % 49.66/15.56 | (362) all_152_4_78 = all_150_4_73 % 49.66/15.56 | % 49.66/15.56 | Combining equations (347,348) yields a new equation: % 49.66/15.56 | (363) all_152_4_78 = 0 % 49.66/15.56 | % 49.66/15.56 | Combining equations (353,359) yields a new equation: % 49.66/15.56 | (364) all_160_8_98 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Simplifying 364 yields: % 49.66/15.56 | (365) all_160_8_98 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Combining equations (357,352) yields a new equation: % 49.66/15.56 | (366) all_144_1_61 = 0 % 49.66/15.56 | % 49.66/15.56 | Simplifying 366 yields: % 49.66/15.56 | (367) all_144_1_61 = 0 % 49.66/15.56 | % 49.66/15.56 | Combining equations (350,351) yields a new equation: % 49.66/15.56 | (368) all_158_1_88 = 0 % 49.66/15.56 | % 49.66/15.56 | Combining equations (355,365) yields a new equation: % 49.66/15.56 | (369) all_158_2_89 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Simplifying 369 yields: % 49.66/15.56 | (370) all_158_2_89 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Combining equations (370,361) yields a new equation: % 49.66/15.56 | (371) all_146_1_64 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Combining equations (358,361) yields a new equation: % 49.66/15.56 | (372) all_146_1_64 = all_144_1_61 % 49.66/15.56 | % 49.66/15.56 | Combining equations (363,362) yields a new equation: % 49.66/15.56 | (373) all_150_4_73 = 0 % 49.66/15.56 | % 49.66/15.56 | Combining equations (372,371) yields a new equation: % 49.66/15.56 | (374) all_144_1_61 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Simplifying 374 yields: % 49.66/15.56 | (375) all_144_1_61 = all_142_2_57 % 49.66/15.56 | % 49.66/15.56 | Combining equations (367,375) yields a new equation: % 49.66/15.56 | (376) all_142_2_57 = 0 % 49.66/15.56 | % 49.66/15.56 | From (373) and (295) follows: % 49.66/15.56 | (155) aNaturalNumber0(all_39_0_46) = 0 % 49.66/15.56 | % 49.66/15.56 | From (368) and (305) follows: % 49.66/15.56 | (243) aNaturalNumber0(all_22_2_25) = 0 % 49.66/15.56 | % 49.66/15.56 | From (376) and (277) follows: % 49.66/15.56 | (23) aNaturalNumber0(xp) = 0 % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (268), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (380) xp = xn % 49.66/15.56 | % 49.66/15.56 | Equations (380) can reduce 67 to: % 49.66/15.56 | (145) $false % 49.66/15.56 | % 49.66/15.56 |-The branch is then unsatisfiable % 49.66/15.56 |-Branch two: % 49.66/15.56 | (67) ~ (xp = xn) % 49.66/15.56 | (383) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtpldt0(xp, xm) = v4 & sdtpldt0(xn, xm) = v3 & aNaturalNumber0(xp) = v2 & aNaturalNumber0(xm) = v0 & aNaturalNumber0(xn) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | ( ~ (v4 = v3) & ~ (all_25_1_30 = all_0_4_4)))) % 49.66/15.56 | % 49.66/15.56 | Instantiating (383) with all_206_0_118, all_206_1_119, all_206_2_120, all_206_3_121, all_206_4_122 yields: % 49.66/15.56 | (384) sdtpldt0(xp, xm) = all_206_0_118 & sdtpldt0(xn, xm) = all_206_1_119 & aNaturalNumber0(xp) = all_206_2_120 & aNaturalNumber0(xm) = all_206_4_122 & aNaturalNumber0(xn) = all_206_3_121 & ( ~ (all_206_2_120 = 0) | ~ (all_206_3_121 = 0) | ~ (all_206_4_122 = 0) | ( ~ (all_206_0_118 = all_206_1_119) & ~ (all_25_1_30 = all_0_4_4))) % 49.66/15.56 | % 49.66/15.56 | Applying alpha-rule on (384) yields: % 49.66/15.56 | (385) aNaturalNumber0(xp) = all_206_2_120 % 49.66/15.56 | (386) aNaturalNumber0(xm) = all_206_4_122 % 49.66/15.56 | (387) sdtpldt0(xn, xm) = all_206_1_119 % 49.66/15.56 | (388) aNaturalNumber0(xn) = all_206_3_121 % 49.66/15.56 | (389) ~ (all_206_2_120 = 0) | ~ (all_206_3_121 = 0) | ~ (all_206_4_122 = 0) | ( ~ (all_206_0_118 = all_206_1_119) & ~ (all_25_1_30 = all_0_4_4)) % 49.66/15.56 | (390) sdtpldt0(xp, xm) = all_206_0_118 % 49.66/15.56 | % 49.66/15.56 | Instantiating formula (58) with xp, all_206_2_120, 0 and discharging atoms aNaturalNumber0(xp) = all_206_2_120, aNaturalNumber0(xp) = 0, yields: % 49.66/15.56 | (391) all_206_2_120 = 0 % 49.66/15.56 | % 49.66/15.56 | From (391) and (385) follows: % 49.66/15.56 | (23) aNaturalNumber0(xp) = 0 % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (258), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (393) all_39_0_46 = xp % 49.66/15.56 | % 49.66/15.56 | Equations (393) can reduce 157 to: % 49.66/15.56 | (80) ~ (xp = sz00) % 49.66/15.56 | % 49.66/15.56 | From (393) and (155) follows: % 49.66/15.56 | (23) aNaturalNumber0(xp) = 0 % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (260), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (144) xp = sz00 % 49.66/15.56 | % 49.66/15.56 | Equations (144) can reduce 80 to: % 49.66/15.56 | (145) $false % 49.66/15.56 | % 49.66/15.56 |-The branch is then unsatisfiable % 49.66/15.56 |-Branch two: % 49.66/15.56 | (80) ~ (xp = sz00) % 49.66/15.56 | (399) all_22_2_25 = xk | ? [v0] : ? [v1] : ? [v2] : (( ~ (v0 = 0) & aNaturalNumber0(all_22_2_25) = v0) | (doDivides0(xp, all_0_2_2) = v2 & aNaturalNumber0(all_0_2_2) = v1 & aNaturalNumber0(xp) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0)))) % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (399), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (400) all_22_2_25 = xk % 49.66/15.56 | % 49.66/15.56 +-Applying beta-rule and splitting (271), into two cases. % 49.66/15.56 |-Branch one: % 49.66/15.56 | (401) all_22_2_25 = sz00 % 49.66/15.56 | % 49.66/15.56 | Combining equations (400,401) yields a new equation: % 49.66/15.56 | (402) xk = sz00 % 49.66/15.56 | % 49.66/15.56 | Simplifying 402 yields: % 49.66/15.56 | (403) xk = sz00 % 49.66/15.57 | % 49.66/15.57 | Equations (403) can reduce 18 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (405) ~ (all_22_2_25 = sz00) % 49.66/15.57 | (406) all_22_2_25 = sz10 | ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_22_2_25) = 0 & aNaturalNumber0(v0) = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (400) can reduce 405 to: % 49.66/15.57 | (18) ~ (xk = sz00) % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (406), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (408) all_22_2_25 = sz10 % 49.66/15.57 | % 49.66/15.57 | Combining equations (400,408) yields a new equation: % 49.66/15.57 | (409) xk = sz10 % 49.66/15.57 | % 49.66/15.57 | Simplifying 409 yields: % 49.66/15.57 | (410) xk = sz10 % 49.66/15.57 | % 49.66/15.57 | Equations (410) can reduce 63 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (412) ~ (all_22_2_25 = sz10) % 49.66/15.57 | (413) ? [v0] : (isPrime0(v0) = 0 & doDivides0(v0, all_22_2_25) = 0 & aNaturalNumber0(v0) = 0) % 49.66/15.57 | % 49.66/15.57 | Instantiating (413) with all_375_0_123 yields: % 49.66/15.57 | (414) isPrime0(all_375_0_123) = 0 & doDivides0(all_375_0_123, all_22_2_25) = 0 & aNaturalNumber0(all_375_0_123) = 0 % 49.66/15.57 | % 49.66/15.57 | Applying alpha-rule on (414) yields: % 49.66/15.57 | (415) isPrime0(all_375_0_123) = 0 % 49.66/15.57 | (416) doDivides0(all_375_0_123, all_22_2_25) = 0 % 49.66/15.57 | (417) aNaturalNumber0(all_375_0_123) = 0 % 49.66/15.57 | % 49.66/15.57 | From (400) and (416) follows: % 49.66/15.57 | (418) doDivides0(all_375_0_123, xk) = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (78) with all_375_0_123 and discharging atoms doDivides0(all_375_0_123, xk) = 0, yields: % 49.66/15.57 | (419) ? [v0] : ? [v1] : (isPrime0(all_375_0_123) = v1 & aNaturalNumber0(all_375_0_123) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (72) with xk, all_375_0_123 and discharging atoms doDivides0(all_375_0_123, xk) = 0, yields: % 49.66/15.57 | (420) xk = sz00 | ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_375_0_123, xk) = v2 & aNaturalNumber0(all_375_0_123) = v0 & aNaturalNumber0(xk) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.66/15.57 | % 49.66/15.57 | Instantiating (419) with all_930_0_301, all_930_1_302 yields: % 49.66/15.57 | (421) isPrime0(all_375_0_123) = all_930_0_301 & aNaturalNumber0(all_375_0_123) = all_930_1_302 & ( ~ (all_930_0_301 = 0) | ~ (all_930_1_302 = 0)) % 49.66/15.57 | % 49.66/15.57 | Applying alpha-rule on (421) yields: % 49.66/15.57 | (422) isPrime0(all_375_0_123) = all_930_0_301 % 49.66/15.57 | (423) aNaturalNumber0(all_375_0_123) = all_930_1_302 % 49.66/15.57 | (424) ~ (all_930_0_301 = 0) | ~ (all_930_1_302 = 0) % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (420), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (403) xk = sz00 % 49.66/15.57 | % 49.66/15.57 | Equations (403) can reduce 18 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (18) ~ (xk = sz00) % 49.66/15.57 | (428) ? [v0] : ? [v1] : ? [v2] : (sdtlseqdt0(all_375_0_123, xk) = v2 & aNaturalNumber0(all_375_0_123) = v0 & aNaturalNumber0(xk) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 49.66/15.57 | % 49.66/15.57 | Instantiating (428) with all_976_0_340, all_976_1_341, all_976_2_342 yields: % 49.66/15.57 | (429) sdtlseqdt0(all_375_0_123, xk) = all_976_0_340 & aNaturalNumber0(all_375_0_123) = all_976_2_342 & aNaturalNumber0(xk) = all_976_1_341 & ( ~ (all_976_1_341 = 0) | ~ (all_976_2_342 = 0) | all_976_0_340 = 0) % 49.66/15.57 | % 49.66/15.57 | Applying alpha-rule on (429) yields: % 49.66/15.57 | (430) sdtlseqdt0(all_375_0_123, xk) = all_976_0_340 % 49.66/15.57 | (431) aNaturalNumber0(all_375_0_123) = all_976_2_342 % 49.66/15.57 | (432) aNaturalNumber0(xk) = all_976_1_341 % 49.66/15.57 | (433) ~ (all_976_1_341 = 0) | ~ (all_976_2_342 = 0) | all_976_0_340 = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (43) with all_375_0_123, all_930_0_301, 0 and discharging atoms isPrime0(all_375_0_123) = all_930_0_301, isPrime0(all_375_0_123) = 0, yields: % 49.66/15.57 | (434) all_930_0_301 = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (58) with all_375_0_123, all_976_2_342, 0 and discharging atoms aNaturalNumber0(all_375_0_123) = all_976_2_342, aNaturalNumber0(all_375_0_123) = 0, yields: % 49.66/15.57 | (435) all_976_2_342 = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (58) with all_375_0_123, all_930_1_302, all_976_2_342 and discharging atoms aNaturalNumber0(all_375_0_123) = all_976_2_342, aNaturalNumber0(all_375_0_123) = all_930_1_302, yields: % 49.66/15.57 | (436) all_976_2_342 = all_930_1_302 % 49.66/15.57 | % 49.66/15.57 | Combining equations (435,436) yields a new equation: % 49.66/15.57 | (437) all_930_1_302 = 0 % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (424), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (438) ~ (all_930_0_301 = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (434) can reduce 438 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (434) all_930_0_301 = 0 % 49.66/15.57 | (441) ~ (all_930_1_302 = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (437) can reduce 441 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (443) ~ (all_22_2_25 = xk) % 49.66/15.57 | (444) ? [v0] : ? [v1] : ? [v2] : (( ~ (v0 = 0) & aNaturalNumber0(all_22_2_25) = v0) | (doDivides0(xp, all_0_2_2) = v2 & aNaturalNumber0(all_0_2_2) = v1 & aNaturalNumber0(xp) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0)))) % 49.66/15.57 | % 49.66/15.57 | Instantiating (444) with all_352_0_372, all_352_1_373, all_352_2_374 yields: % 49.66/15.57 | (445) ( ~ (all_352_2_374 = 0) & aNaturalNumber0(all_22_2_25) = all_352_2_374) | (doDivides0(xp, all_0_2_2) = all_352_0_372 & aNaturalNumber0(all_0_2_2) = all_352_1_373 & aNaturalNumber0(xp) = all_352_2_374 & ( ~ (all_352_0_372 = 0) | ~ (all_352_1_373 = 0) | ~ (all_352_2_374 = 0))) % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (445), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (446) ~ (all_352_2_374 = 0) & aNaturalNumber0(all_22_2_25) = all_352_2_374 % 49.66/15.57 | % 49.66/15.57 | Applying alpha-rule on (446) yields: % 49.66/15.57 | (447) ~ (all_352_2_374 = 0) % 49.66/15.57 | (448) aNaturalNumber0(all_22_2_25) = all_352_2_374 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (58) with all_22_2_25, all_352_2_374, 0 and discharging atoms aNaturalNumber0(all_22_2_25) = all_352_2_374, aNaturalNumber0(all_22_2_25) = 0, yields: % 49.66/15.57 | (449) all_352_2_374 = 0 % 49.66/15.57 | % 49.66/15.57 | Equations (449) can reduce 447 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (451) doDivides0(xp, all_0_2_2) = all_352_0_372 & aNaturalNumber0(all_0_2_2) = all_352_1_373 & aNaturalNumber0(xp) = all_352_2_374 & ( ~ (all_352_0_372 = 0) | ~ (all_352_1_373 = 0) | ~ (all_352_2_374 = 0)) % 49.66/15.57 | % 49.66/15.57 | Applying alpha-rule on (451) yields: % 49.66/15.57 | (452) doDivides0(xp, all_0_2_2) = all_352_0_372 % 49.66/15.57 | (453) aNaturalNumber0(all_0_2_2) = all_352_1_373 % 49.66/15.57 | (454) aNaturalNumber0(xp) = all_352_2_374 % 49.66/15.57 | (455) ~ (all_352_0_372 = 0) | ~ (all_352_1_373 = 0) | ~ (all_352_2_374 = 0) % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (6) with xp, all_0_2_2, all_352_0_372, 0 and discharging atoms doDivides0(xp, all_0_2_2) = all_352_0_372, doDivides0(xp, all_0_2_2) = 0, yields: % 49.66/15.57 | (456) all_352_0_372 = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (58) with all_0_2_2, all_352_1_373, 0 and discharging atoms aNaturalNumber0(all_0_2_2) = all_352_1_373, aNaturalNumber0(all_0_2_2) = 0, yields: % 49.66/15.57 | (457) all_352_1_373 = 0 % 49.66/15.57 | % 49.66/15.57 | Instantiating formula (58) with xp, all_352_2_374, 0 and discharging atoms aNaturalNumber0(xp) = all_352_2_374, aNaturalNumber0(xp) = 0, yields: % 49.66/15.57 | (449) all_352_2_374 = 0 % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (455), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (459) ~ (all_352_0_372 = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (456) can reduce 459 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (456) all_352_0_372 = 0 % 49.66/15.57 | (462) ~ (all_352_1_373 = 0) | ~ (all_352_2_374 = 0) % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (462), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (463) ~ (all_352_1_373 = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (457) can reduce 463 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (457) all_352_1_373 = 0 % 49.66/15.57 | (447) ~ (all_352_2_374 = 0) % 49.66/15.57 | % 49.66/15.57 | Equations (449) can reduce 447 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (468) ~ (all_39_0_46 = xp) % 49.66/15.57 | (469) all_39_0_46 = sz10 | ? [v0] : (( ~ (v0 = 0) & aNaturalNumber0(all_39_0_46) = v0) | ( ~ (v0 = 0) & aNaturalNumber0(xp) = v0)) % 49.66/15.57 | % 49.66/15.57 +-Applying beta-rule and splitting (469), into two cases. % 49.66/15.57 |-Branch one: % 49.66/15.57 | (343) all_39_0_46 = sz10 % 49.66/15.57 | % 49.66/15.57 | Equations (343) can reduce 156 to: % 49.66/15.57 | (145) $false % 49.66/15.57 | % 49.66/15.57 |-The branch is then unsatisfiable % 49.66/15.57 |-Branch two: % 49.66/15.57 | (156) ~ (all_39_0_46 = sz10) % 49.66/15.58 | (473) ? [v0] : (( ~ (v0 = 0) & aNaturalNumber0(all_39_0_46) = v0) | ( ~ (v0 = 0) & aNaturalNumber0(xp) = v0)) % 49.66/15.58 | % 49.66/15.58 | Instantiating (473) with all_363_0_375 yields: % 49.66/15.58 | (474) ( ~ (all_363_0_375 = 0) & aNaturalNumber0(all_39_0_46) = all_363_0_375) | ( ~ (all_363_0_375 = 0) & aNaturalNumber0(xp) = all_363_0_375) % 49.66/15.58 | % 49.66/15.58 +-Applying beta-rule and splitting (474), into two cases. % 49.66/15.58 |-Branch one: % 49.66/15.58 | (475) ~ (all_363_0_375 = 0) & aNaturalNumber0(all_39_0_46) = all_363_0_375 % 49.66/15.58 | % 49.66/15.58 | Applying alpha-rule on (475) yields: % 49.66/15.58 | (476) ~ (all_363_0_375 = 0) % 49.66/15.58 | (477) aNaturalNumber0(all_39_0_46) = all_363_0_375 % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with all_39_0_46, all_363_0_375, 0 and discharging atoms aNaturalNumber0(all_39_0_46) = all_363_0_375, aNaturalNumber0(all_39_0_46) = 0, yields: % 49.66/15.58 | (478) all_363_0_375 = 0 % 49.66/15.58 | % 49.66/15.58 | Equations (478) can reduce 476 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (480) ~ (all_363_0_375 = 0) & aNaturalNumber0(xp) = all_363_0_375 % 49.66/15.58 | % 49.66/15.58 | Applying alpha-rule on (480) yields: % 49.66/15.58 | (476) ~ (all_363_0_375 = 0) % 49.66/15.58 | (482) aNaturalNumber0(xp) = all_363_0_375 % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xp, all_363_0_375, 0 and discharging atoms aNaturalNumber0(xp) = all_363_0_375, aNaturalNumber0(xp) = 0, yields: % 49.66/15.58 | (478) all_363_0_375 = 0 % 49.66/15.58 | % 49.66/15.58 | Equations (478) can reduce 476 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (485) aNaturalNumber0(all_0_2_2) = all_22_1_24 & aNaturalNumber0(xp) = all_22_2_25 & ( ~ (all_22_1_24 = 0) | ~ (all_22_2_25 = 0)) % 49.66/15.58 | % 49.66/15.58 | Applying alpha-rule on (485) yields: % 49.66/15.58 | (486) aNaturalNumber0(all_0_2_2) = all_22_1_24 % 49.66/15.58 | (487) aNaturalNumber0(xp) = all_22_2_25 % 49.66/15.58 | (488) ~ (all_22_1_24 = 0) | ~ (all_22_2_25 = 0) % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with all_0_2_2, all_22_1_24, 0 and discharging atoms aNaturalNumber0(all_0_2_2) = all_22_1_24, aNaturalNumber0(all_0_2_2) = 0, yields: % 49.66/15.58 | (241) all_22_1_24 = 0 % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xp, all_22_2_25, 0 and discharging atoms aNaturalNumber0(xp) = all_22_2_25, aNaturalNumber0(xp) = 0, yields: % 49.66/15.58 | (490) all_22_2_25 = 0 % 49.66/15.58 | % 49.66/15.58 +-Applying beta-rule and splitting (488), into two cases. % 49.66/15.58 |-Branch one: % 49.66/15.58 | (491) ~ (all_22_1_24 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (241) can reduce 491 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (241) all_22_1_24 = 0 % 49.66/15.58 | (494) ~ (all_22_2_25 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (490) can reduce 494 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (496) aNaturalNumber0(xp) = all_20_1_18 & aNaturalNumber0(xn) = all_20_2_19 & ( ~ (all_20_1_18 = 0) | ~ (all_20_2_19 = 0)) % 49.66/15.58 | % 49.66/15.58 | Applying alpha-rule on (496) yields: % 49.66/15.58 | (497) aNaturalNumber0(xp) = all_20_1_18 % 49.66/15.58 | (498) aNaturalNumber0(xn) = all_20_2_19 % 49.66/15.58 | (499) ~ (all_20_1_18 = 0) | ~ (all_20_2_19 = 0) % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xp, all_20_1_18, 0 and discharging atoms aNaturalNumber0(xp) = all_20_1_18, aNaturalNumber0(xp) = 0, yields: % 49.66/15.58 | (223) all_20_1_18 = 0 % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xn, all_20_2_19, 0 and discharging atoms aNaturalNumber0(xn) = all_20_2_19, aNaturalNumber0(xn) = 0, yields: % 49.66/15.58 | (501) all_20_2_19 = 0 % 49.66/15.58 | % 49.66/15.58 +-Applying beta-rule and splitting (499), into two cases. % 49.66/15.58 |-Branch one: % 49.66/15.58 | (502) ~ (all_20_1_18 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (223) can reduce 502 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (223) all_20_1_18 = 0 % 49.66/15.58 | (505) ~ (all_20_2_19 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (501) can reduce 505 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (507) aNaturalNumber0(xp) = all_21_1_21 & aNaturalNumber0(xm) = all_21_2_22 & ( ~ (all_21_1_21 = 0) | ~ (all_21_2_22 = 0)) % 49.66/15.58 | % 49.66/15.58 | Applying alpha-rule on (507) yields: % 49.66/15.58 | (508) aNaturalNumber0(xp) = all_21_1_21 % 49.66/15.58 | (509) aNaturalNumber0(xm) = all_21_2_22 % 49.66/15.58 | (510) ~ (all_21_1_21 = 0) | ~ (all_21_2_22 = 0) % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xp, all_21_1_21, 0 and discharging atoms aNaturalNumber0(xp) = all_21_1_21, aNaturalNumber0(xp) = 0, yields: % 49.66/15.58 | (213) all_21_1_21 = 0 % 49.66/15.58 | % 49.66/15.58 | Instantiating formula (58) with xm, all_21_2_22, 0 and discharging atoms aNaturalNumber0(xm) = all_21_2_22, aNaturalNumber0(xm) = 0, yields: % 49.66/15.58 | (512) all_21_2_22 = 0 % 49.66/15.58 | % 49.66/15.58 +-Applying beta-rule and splitting (510), into two cases. % 49.66/15.58 |-Branch one: % 49.66/15.58 | (513) ~ (all_21_1_21 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (213) can reduce 513 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 |-Branch two: % 49.66/15.58 | (213) all_21_1_21 = 0 % 49.66/15.58 | (516) ~ (all_21_2_22 = 0) % 49.66/15.58 | % 49.66/15.58 | Equations (512) can reduce 516 to: % 49.66/15.58 | (145) $false % 49.66/15.58 | % 49.66/15.58 |-The branch is then unsatisfiable % 49.66/15.58 % SZS output end Proof for theBenchmark % 49.66/15.58 % 49.66/15.58 14934ms %------------------------------------------------------------------------------