%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM476+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 08:44:54 EDT 2022 % Result : Theorem 21.83s 6.29s % Output : Proof 27.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM476+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n018.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jul 7 08:55:39 EDT 2022 % 0.13/0.34 % CPUTime : % 0.57/0.59 ____ _ % 0.57/0.59 ___ / __ \_____(_)___ ________ __________ % 0.57/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.59 % 0.57/0.59 A Theorem Prover for First-Order Logic % 0.57/0.59 (ePrincess v.1.0) % 0.57/0.59 % 0.57/0.59 (c) Philipp Rümmer, 2009-2015 % 0.57/0.59 (c) Peter Backeman, 2014-2015 % 0.57/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.59 Bug reports to peter@backeman.se % 0.57/0.59 % 0.57/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.59 % 0.57/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.79/1.00 Prover 0: Preprocessing ... % 3.28/1.46 Prover 0: Constructing countermodel ... % 20.16/5.93 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.52/6.02 Prover 1: Preprocessing ... % 20.97/6.14 Prover 1: Constructing countermodel ... % 21.83/6.29 Prover 1: proved (359ms) % 21.83/6.29 Prover 0: stopped % 21.83/6.29 % 21.83/6.29 No countermodel exists, formula is valid % 21.83/6.29 % SZS status Theorem for theBenchmark % 21.83/6.29 % 21.83/6.29 Generating proof ... found it (size 88) % 27.02/7.50 % 27.02/7.50 % SZS output start Proof for theBenchmark % 27.02/7.50 Assumed formulas after preprocessing and simplification: % 27.02/7.50 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ( ~ (v3 = 0) & ~ (sz10 = sz00) & sdtsldt0(v0, xl) = v2 & sdtsldt0(xm, xl) = v1 & doDivides0(xl, v0) = 0 & doDivides0(xl, xn) = v3 & doDivides0(xl, xm) = 0 & sdtasdt0(xl, v22) = xm & sdtasdt0(xl, v21) = v0 & sdtpldt0(xm, xn) = v0 & aNaturalNumber0(v22) = 0 & aNaturalNumber0(v21) = 0 & aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & aNaturalNumber0(sz10) = 0 & aNaturalNumber0(sz00) = 0 & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : ! [v28] : (v25 = v24 | v23 = sz00 | ~ (sdtlseqdt0(v26, v27) = v28) | ~ (sdtasdt0(v23, v25) = v27) | ~ (sdtasdt0(v23, v24) = v26) | ? [v29] : ? [v30] : ? [v31] : ? [v32] : ? [v33] : ? [v34] : ? [v35] : (sdtlseqdt0(v33, v34) = v35 & sdtlseqdt0(v24, v25) = v32 & sdtasdt0(v25, v23) = v34 & sdtasdt0(v24, v23) = v33 & aNaturalNumber0(v25) = v31 & aNaturalNumber0(v24) = v30 & aNaturalNumber0(v23) = v29 & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | (v35 = 0 & v28 = 0 & ~ (v34 = v33) & ~ (v27 = v26))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : ! [v28] : (v24 = v23 | ~ (sdtlseqdt0(v26, v27) = v28) | ~ (sdtlseqdt0(v23, v24) = 0) | ~ (sdtpldt0(v24, v25) = v27) | ~ (sdtpldt0(v23, v25) = v26) | ? [v29] : ? [v30] : ? [v31] : ? [v32] : ((sdtlseqdt0(v30, v31) = v32 & sdtpldt0(v25, v24) = v31 & sdtpldt0(v25, v23) = v30 & aNaturalNumber0(v25) = v29 & ( ~ (v29 = 0) | (v32 = 0 & v28 = 0 & ~ (v31 = v30) & ~ (v27 = v26)))) | (aNaturalNumber0(v24) = v30 & aNaturalNumber0(v23) = v29 & ( ~ (v30 = 0) | ~ (v29 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : ! [v28] : ( ~ (sdtasdt0(v23, v25) = v27) | ~ (sdtasdt0(v23, v24) = v26) | ~ (sdtpldt0(v26, v27) = v28) | ? [v29] : ? [v30] : ? [v31] : ? [v32] : ? [v33] : ? [v34] : ? [v35] : ? [v36] : ? [v37] : (sdtasdt0(v32, v23) = v34 & sdtasdt0(v25, v23) = v36 & sdtasdt0(v24, v23) = v35 & sdtasdt0(v23, v32) = v33 & sdtpldt0(v35, v36) = v37 & sdtpldt0(v24, v25) = v32 & aNaturalNumber0(v25) = v31 & aNaturalNumber0(v24) = v30 & aNaturalNumber0(v23) = v29 & ( ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | (v37 = v34 & v33 = v28)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v27 = 0 | ~ (doDivides0(v23, v26) = v27) | ~ (sdtpldt0(v24, v25) = v26) | ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : (doDivides0(v23, v25) = v32 & doDivides0(v23, v24) = v31 & aNaturalNumber0(v25) = v30 & aNaturalNumber0(v24) = v29 & aNaturalNumber0(v23) = v28 & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | v23 = sz00 | ~ (sdtasdt0(v23, v25) = v27) | ~ (sdtasdt0(v23, v24) = v26) | ~ (aNaturalNumber0(v23) = 0) | ? [v28] : ? [v29] : ? [v30] : ? [v31] : (sdtasdt0(v25, v23) = v31 & sdtasdt0(v24, v23) = v30 & aNaturalNumber0(v25) = v29 & aNaturalNumber0(v24) = v28 & ( ~ (v29 = 0) | ~ (v28 = 0) | ( ~ (v31 = v30) & ~ (v27 = v26))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (sdtpldt0(v23, v25) = v27) | ~ (sdtpldt0(v23, v24) = v26) | ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : (sdtpldt0(v25, v23) = v32 & sdtpldt0(v24, v23) = v31 & aNaturalNumber0(v25) = v30 & aNaturalNumber0(v24) = v29 & aNaturalNumber0(v23) = v28 & ( ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0) | ( ~ (v32 = v31) & ~ (v27 = v26))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : ( ~ (sdtasdt0(v26, v25) = v27) | ~ (sdtasdt0(v23, v24) = v26) | ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : (sdtasdt0(v24, v25) = v31 & sdtasdt0(v23, v31) = v32 & aNaturalNumber0(v25) = v30 & aNaturalNumber0(v24) = v29 & aNaturalNumber0(v23) = v28 & ( ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0) | v32 = v27))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ! [v27] : ( ~ (sdtpldt0(v26, v25) = v27) | ~ (sdtpldt0(v23, v24) = v26) | ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : (sdtpldt0(v24, v25) = v31 & sdtpldt0(v23, v31) = v32 & aNaturalNumber0(v25) = v30 & aNaturalNumber0(v24) = v29 & aNaturalNumber0(v23) = v28 & ( ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0) | v32 = v27))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = v25 | v23 = sz00 | ~ (sdtsldt0(v24, v23) = v25) | ~ (sdtasdt0(v23, v26) = v24) | ? [v27] : ? [v28] : ? [v29] : (( ~ (v27 = 0) & aNaturalNumber0(v26) = v27) | (doDivides0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = v25 | ~ (sdtmndt0(v24, v23) = v25) | ~ (sdtpldt0(v23, v26) = v24) | ? [v27] : ? [v28] : ? [v29] : (( ~ (v27 = 0) & aNaturalNumber0(v26) = v27) | (sdtlseqdt0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = v24 | v23 = sz00 | ~ (sdtsldt0(v24, v23) = v25) | ~ (sdtasdt0(v23, v25) = v26) | ? [v27] : ? [v28] : ? [v29] : (doDivides0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = v24 | ~ (sdtmndt0(v24, v23) = v25) | ~ (sdtpldt0(v23, v25) = v26) | ? [v27] : ? [v28] : ? [v29] : (sdtlseqdt0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | v23 = sz00 | ~ (sdtlseqdt0(v24, v25) = v26) | ~ (sdtasdt0(v24, v23) = v25) | ? [v27] : ? [v28] : (aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v28 = 0) | ~ (v27 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (doDivides0(v23, v25) = v26) | ~ (doDivides0(v23, v24) = 0) | ? [v27] : ? [v28] : ? [v29] : ? [v30] : (doDivides0(v24, v25) = v30 & aNaturalNumber0(v25) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v26 = 0 | ~ (sdtlseqdt0(v23, v25) = v26) | ~ (sdtlseqdt0(v23, v24) = 0) | ? [v27] : ? [v28] : ? [v29] : ? [v30] : (sdtlseqdt0(v24, v25) = v30 & aNaturalNumber0(v25) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v30 = 0) | ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0)))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (doDivides0(v23, v24) = v25) | ~ (sdtasdt0(v23, v26) = v24) | ? [v27] : ? [v28] : (( ~ (v27 = 0) & aNaturalNumber0(v26) = v27) | (aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v25 = 0 | ~ (sdtlseqdt0(v23, v24) = v25) | ~ (sdtpldt0(v23, v26) = v24) | ? [v27] : ? [v28] : (( ~ (v27 = 0) & aNaturalNumber0(v26) = v27) | (aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (sdtsldt0(v26, v25) = v24) | ~ (sdtsldt0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (doDivides0(v26, v25) = v24) | ~ (doDivides0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (iLess0(v26, v25) = v24) | ~ (iLess0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (sdtmndt0(v26, v25) = v24) | ~ (sdtmndt0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (sdtlseqdt0(v26, v25) = v24) | ~ (sdtlseqdt0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (sdtasdt0(v26, v25) = v24) | ~ (sdtasdt0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v24 = v23 | ~ (sdtpldt0(v26, v25) = v24) | ~ (sdtpldt0(v26, v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : (v23 = sz00 | ~ (sdtsldt0(v24, v23) = v25) | ~ (sdtasdt0(v23, v25) = v26) | ? [v27] : ? [v28] : ? [v29] : ((v27 = 0 & aNaturalNumber0(v25) = 0) | (doDivides0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : ! [v26] : ( ~ (sdtmndt0(v24, v23) = v25) | ~ (sdtpldt0(v23, v25) = v26) | ? [v27] : ? [v28] : ? [v29] : ((v27 = 0 & aNaturalNumber0(v25) = 0) | (sdtlseqdt0(v23, v24) = v29 & aNaturalNumber0(v24) = v28 & aNaturalNumber0(v23) = v27 & ( ~ (v29 = 0) | ~ (v28 = 0) | ~ (v27 = 0))))) & ! [v23] : ! [v24] : ! [v25] : (v25 = 0 | v24 = v23 | ~ (iLess0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (sdtlseqdt0(v23, v24) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v28 = 0) | ~ (v27 = 0) | ~ (v26 = 0)))) & ! [v23] : ! [v24] : ! [v25] : (v25 = 0 | ~ (sdtlseqdt0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (sdtlseqdt0(v24, v23) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v27 = 0) | ~ (v26 = 0) | (v28 = 0 & ~ (v24 = v23))))) & ! [v23] : ! [v24] : ! [v25] : (v24 = v23 | ~ (aNaturalNumber0(v25) = v24) | ~ (aNaturalNumber0(v25) = v23)) & ! [v23] : ! [v24] : ! [v25] : ( ~ (sdtasdt0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (sdtasdt0(v24, v23) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v27 = 0) | ~ (v26 = 0) | v28 = v25))) & ! [v23] : ! [v24] : ! [v25] : ( ~ (sdtasdt0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (aNaturalNumber0(v25) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v27 = 0) | ~ (v26 = 0) | v28 = 0))) & ! [v23] : ! [v24] : ! [v25] : ( ~ (sdtpldt0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (sdtpldt0(v24, v23) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v27 = 0) | ~ (v26 = 0) | v28 = v25))) & ! [v23] : ! [v24] : ! [v25] : ( ~ (sdtpldt0(v23, v24) = v25) | ? [v26] : ? [v27] : ? [v28] : (aNaturalNumber0(v25) = v28 & aNaturalNumber0(v24) = v27 & aNaturalNumber0(v23) = v26 & ( ~ (v27 = 0) | ~ (v26 = 0) | v28 = 0))) & ! [v23] : ! [v24] : (v24 = v23 | ~ (sdtlseqdt0(v23, v24) = 0) | ? [v25] : ? [v26] : ? [v27] : (sdtlseqdt0(v24, v23) = v27 & aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v27 = 0) | ~ (v26 = 0) | ~ (v25 = 0)))) & ! [v23] : ! [v24] : (v24 = sz00 | v23 = sz00 | ~ (sdtasdt0(v23, v24) = sz00) | ? [v25] : ? [v26] : (aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v26 = 0) | ~ (v25 = 0)))) & ! [v23] : ! [v24] : (v24 = sz00 | ~ (sdtpldt0(v23, v24) = sz00) | ? [v25] : ? [v26] : (aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v26 = 0) | ~ (v25 = 0)))) & ! [v23] : ! [v24] : (v24 = 0 | v23 = sz10 | v23 = sz00 | ~ (sdtlseqdt0(sz10, v23) = v24) | ? [v25] : ( ~ (v25 = 0) & aNaturalNumber0(v23) = v25)) & ! [v23] : ! [v24] : (v24 = 0 | ~ (sdtlseqdt0(v23, v23) = v24) | ? [v25] : ( ~ (v25 = 0) & aNaturalNumber0(v23) = v25)) & ! [v23] : ! [v24] : (v23 = sz00 | ~ (sdtpldt0(v23, v24) = sz00) | ? [v25] : ? [v26] : (aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v26 = 0) | ~ (v25 = 0)))) & ! [v23] : ! [v24] : ( ~ (doDivides0(v23, v24) = 0) | ? [v25] : ? [v26] : ? [v27] : ((v27 = v24 & v26 = 0 & sdtasdt0(v23, v25) = v24 & aNaturalNumber0(v25) = 0) | (aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v26 = 0) | ~ (v25 = 0))))) & ! [v23] : ! [v24] : ( ~ (sdtlseqdt0(v23, v24) = 0) | ? [v25] : ? [v26] : ? [v27] : ((v27 = v24 & v26 = 0 & sdtpldt0(v23, v25) = v24 & aNaturalNumber0(v25) = 0) | (aNaturalNumber0(v24) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v26 = 0) | ~ (v25 = 0))))) & ! [v23] : ! [v24] : ( ~ (sdtasdt0(sz10, v23) = v24) | ? [v25] : ? [v26] : (sdtasdt0(v23, sz10) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v25 = 0) | (v26 = v23 & v24 = v23)))) & ! [v23] : ! [v24] : ( ~ (sdtasdt0(sz00, v23) = v24) | ? [v25] : ? [v26] : (sdtasdt0(v23, sz00) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v25 = 0) | (v26 = sz00 & v24 = sz00)))) & ! [v23] : ! [v24] : ( ~ (sdtpldt0(sz00, v23) = v24) | ? [v25] : ? [v26] : (sdtpldt0(v23, sz00) = v26 & aNaturalNumber0(v23) = v25 & ( ~ (v25 = 0) | (v26 = v23 & v24 = v23)))) & ! [v23] : ( ~ (sdtasdt0(xl, v23) = xn) | ? [v24] : ( ~ (v24 = 0) & aNaturalNumber0(v23) = v24)) & (xl = sz00 | (v20 = v2 & v19 = 0 & v17 = v0 & v16 = xn & v15 = v2 & v14 = 0 & v13 = v12 & v11 = 0 & v10 = v0 & v9 = 0 & v8 = v2 & v7 = v0 & v6 = xm & v5 = 0 & v4 = v1 & sdtmndt0(v2, v1) = v12 & sdtlseqdt0(v1, v2) = 0 & sdtasdt0(xl, v12) = xn & sdtasdt0(xl, v2) = v0 & sdtasdt0(xl, v1) = xm & sdtpldt0(v1, v18) = v2 & sdtpldt0(v1, v12) = v2 & aNaturalNumber0(v18) = 0 & aNaturalNumber0(v12) = 0 & aNaturalNumber0(v2) = 0 & aNaturalNumber0(v1) = 0))) % 27.23/7.57 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19, all_0_20_20, all_0_21_21, all_0_22_22 yields: % 27.23/7.57 | (1) ~ (all_0_19_19 = 0) & ~ (sz10 = sz00) & sdtsldt0(all_0_22_22, xl) = all_0_20_20 & sdtsldt0(xm, xl) = all_0_21_21 & doDivides0(xl, all_0_22_22) = 0 & doDivides0(xl, xn) = all_0_19_19 & doDivides0(xl, xm) = 0 & sdtasdt0(xl, all_0_0_0) = xm & sdtasdt0(xl, all_0_1_1) = all_0_22_22 & sdtpldt0(xm, xn) = all_0_22_22 & aNaturalNumber0(all_0_0_0) = 0 & aNaturalNumber0(all_0_1_1) = 0 & aNaturalNumber0(xn) = 0 & aNaturalNumber0(xm) = 0 & aNaturalNumber0(xl) = 0 & aNaturalNumber0(sz10) = 0 & aNaturalNumber0(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] : ( ~ (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] : ( ~ (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 | ~ (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 | ~ (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 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [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] : ( ~ (sdtasdt0(xl, v0) = xn) | ? [v1] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) & (xl = sz00 | (all_0_2_2 = all_0_20_20 & all_0_3_3 = 0 & all_0_5_5 = all_0_22_22 & all_0_6_6 = xn & all_0_7_7 = all_0_20_20 & all_0_8_8 = 0 & all_0_9_9 = all_0_10_10 & all_0_11_11 = 0 & all_0_12_12 = all_0_22_22 & all_0_13_13 = 0 & all_0_14_14 = all_0_20_20 & all_0_15_15 = all_0_22_22 & all_0_16_16 = xm & all_0_17_17 = 0 & all_0_18_18 = all_0_21_21 & sdtmndt0(all_0_20_20, all_0_21_21) = all_0_10_10 & sdtlseqdt0(all_0_21_21, all_0_20_20) = 0 & sdtasdt0(xl, all_0_10_10) = xn & sdtasdt0(xl, all_0_20_20) = all_0_22_22 & sdtasdt0(xl, all_0_21_21) = xm & sdtpldt0(all_0_21_21, all_0_4_4) = all_0_20_20 & sdtpldt0(all_0_21_21, all_0_10_10) = all_0_20_20 & aNaturalNumber0(all_0_4_4) = 0 & aNaturalNumber0(all_0_10_10) = 0 & aNaturalNumber0(all_0_20_20) = 0 & aNaturalNumber0(all_0_21_21) = 0)) % 27.23/7.59 | % 27.23/7.59 | Applying alpha-rule on (1) yields: % 27.23/7.59 | (2) ! [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))) % 27.23/7.59 | (3) ! [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))) % 27.23/7.59 | (4) ! [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))))) % 27.23/7.60 | (5) xl = sz00 | (all_0_2_2 = all_0_20_20 & all_0_3_3 = 0 & all_0_5_5 = all_0_22_22 & all_0_6_6 = xn & all_0_7_7 = all_0_20_20 & all_0_8_8 = 0 & all_0_9_9 = all_0_10_10 & all_0_11_11 = 0 & all_0_12_12 = all_0_22_22 & all_0_13_13 = 0 & all_0_14_14 = all_0_20_20 & all_0_15_15 = all_0_22_22 & all_0_16_16 = xm & all_0_17_17 = 0 & all_0_18_18 = all_0_21_21 & sdtmndt0(all_0_20_20, all_0_21_21) = all_0_10_10 & sdtlseqdt0(all_0_21_21, all_0_20_20) = 0 & sdtasdt0(xl, all_0_10_10) = xn & sdtasdt0(xl, all_0_20_20) = all_0_22_22 & sdtasdt0(xl, all_0_21_21) = xm & sdtpldt0(all_0_21_21, all_0_4_4) = all_0_20_20 & sdtpldt0(all_0_21_21, all_0_10_10) = all_0_20_20 & aNaturalNumber0(all_0_4_4) = 0 & aNaturalNumber0(all_0_10_10) = 0 & aNaturalNumber0(all_0_20_20) = 0 & aNaturalNumber0(all_0_21_21) = 0) % 27.23/7.60 | (6) ! [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))))) % 27.23/7.60 | (7) ~ (all_0_19_19 = 0) % 27.23/7.60 | (8) ! [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)))) % 27.23/7.60 | (9) ! [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))))) % 27.23/7.60 | (10) ! [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))))) % 27.23/7.60 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtlseqdt0(v3, v2) = v1) | ~ (sdtlseqdt0(v3, v2) = v0)) % 27.23/7.60 | (12) aNaturalNumber0(xn) = 0 % 27.23/7.60 | (13) sdtsldt0(xm, xl) = all_0_21_21 % 27.23/7.60 | (14) doDivides0(xl, xm) = 0 % 27.23/7.60 | (15) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.23/7.60 | (16) ! [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))))) % 27.23/7.60 | (17) aNaturalNumber0(sz10) = 0 % 27.23/7.60 | (18) ! [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))) % 27.23/7.60 | (19) ! [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))))) % 27.23/7.60 | (20) aNaturalNumber0(xm) = 0 % 27.23/7.60 | (21) aNaturalNumber0(sz00) = 0 % 27.23/7.60 | (22) aNaturalNumber0(all_0_0_0) = 0 % 27.23/7.60 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 27.23/7.60 | (24) doDivides0(xl, xn) = all_0_19_19 % 27.23/7.60 | (25) ! [v0] : ! [v1] : (v0 = sz00 | ~ (sdtpldt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.23/7.60 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (aNaturalNumber0(v2) = v1) | ~ (aNaturalNumber0(v2) = v0)) % 27.23/7.60 | (27) ! [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)))) % 27.23/7.60 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 27.23/7.60 | (29) ! [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)))) % 27.23/7.60 | (30) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz10) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 27.23/7.60 | (31) ! [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)))) % 27.23/7.60 | (32) ! [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))) % 27.23/7.60 | (33) ! [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)))) % 27.23/7.60 | (34) ! [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))))) % 27.23/7.61 | (35) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtpldt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = v0 & v1 = v0)))) % 27.23/7.61 | (36) ! [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))))) % 27.23/7.61 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtmndt0(v3, v2) = v1) | ~ (sdtmndt0(v3, v2) = v0)) % 27.23/7.61 | (38) sdtpldt0(xm, xn) = all_0_22_22 % 27.23/7.61 | (39) aNaturalNumber0(all_0_1_1) = 0 % 27.23/7.61 | (40) sdtasdt0(xl, all_0_1_1) = all_0_22_22 % 27.23/7.61 | (41) ! [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))) % 27.23/7.61 | (42) ! [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))) % 27.23/7.61 | (43) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ? [v2] : ? [v3] : (aNaturalNumber0(v1) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.23/7.61 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (iLess0(v3, v2) = v1) | ~ (iLess0(v3, v2) = v0)) % 27.23/7.61 | (45) sdtsldt0(all_0_22_22, xl) = all_0_20_20 % 27.23/7.61 | (46) ~ (sz10 = sz00) % 27.23/7.61 | (47) ! [v0] : ! [v1] : (v1 = 0 | ~ (sdtlseqdt0(v0, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) % 27.23/7.61 | (48) ! [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)))) % 27.23/7.61 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtsldt0(v3, v2) = v1) | ~ (sdtsldt0(v3, v2) = v0)) % 27.23/7.61 | (50) ! [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)))) % 27.23/7.61 | (51) ! [v0] : ( ~ (sdtasdt0(xl, v0) = xn) | ? [v1] : ( ~ (v1 = 0) & aNaturalNumber0(v0) = v1)) % 27.23/7.61 | (52) ! [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))))) % 27.23/7.61 | (53) ! [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))))) % 27.23/7.61 | (54) ! [v0] : ! [v1] : (v1 = 0 | v0 = sz10 | v0 = sz00 | ~ (sdtlseqdt0(sz10, v0) = v1) | ? [v2] : ( ~ (v2 = 0) & aNaturalNumber0(v0) = v2)) % 27.23/7.61 | (55) aNaturalNumber0(xl) = 0 % 27.23/7.61 | (56) ! [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))))) % 27.23/7.61 | (57) ! [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))))) % 27.23/7.61 | (58) ! [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)))) % 27.23/7.61 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (doDivides0(v3, v2) = v1) | ~ (doDivides0(v3, v2) = v0)) % 27.23/7.61 | (60) sdtasdt0(xl, all_0_0_0) = xm % 27.23/7.61 | (61) ! [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)))) % 27.23/7.61 | (62) ! [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))))) % 27.23/7.61 | (63) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ? [v2] : ? [v3] : (sdtasdt0(v0, sz00) = v3 & aNaturalNumber0(v0) = v2 & ( ~ (v2 = 0) | (v3 = sz00 & v1 = sz00)))) % 27.23/7.61 | (64) doDivides0(xl, all_0_22_22) = 0 % 27.23/7.61 | % 27.68/7.61 | Instantiating formula (50) with all_0_19_19, xn, all_0_22_22, xl and discharging atoms doDivides0(xl, all_0_22_22) = 0, doDivides0(xl, xn) = all_0_19_19, yields: % 27.68/7.62 | (65) all_0_19_19 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (doDivides0(all_0_22_22, xn) = v3 & aNaturalNumber0(all_0_22_22) = v1 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (50) with all_0_19_19, xn, xm, xl and discharging atoms doDivides0(xl, xn) = all_0_19_19, doDivides0(xl, xm) = 0, yields: % 27.68/7.62 | (66) all_0_19_19 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (63) with xm, all_0_0_0 yields: % 27.68/7.62 | (67) ~ (sdtasdt0(sz00, all_0_0_0) = xm) | ? [v0] : ? [v1] : (sdtasdt0(all_0_0_0, sz00) = v1 & aNaturalNumber0(all_0_0_0) = v0 & ( ~ (v0 = 0) | (v1 = sz00 & xm = sz00))) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (32) with xm, all_0_0_0, xl and discharging atoms sdtasdt0(xl, all_0_0_0) = xm, yields: % 27.68/7.62 | (68) ? [v0] : ? [v1] : ? [v2] : (sdtasdt0(all_0_0_0, xl) = v2 & aNaturalNumber0(all_0_0_0) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = xm)) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (51) with all_0_1_1 yields: % 27.68/7.62 | (69) ~ (sdtasdt0(xl, all_0_1_1) = xn) | ? [v0] : ( ~ (v0 = 0) & aNaturalNumber0(all_0_1_1) = v0) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (32) with all_0_22_22, all_0_1_1, xl and discharging atoms sdtasdt0(xl, all_0_1_1) = all_0_22_22, yields: % 27.68/7.62 | (70) ? [v0] : ? [v1] : ? [v2] : (sdtasdt0(all_0_1_1, xl) = v2 & aNaturalNumber0(all_0_1_1) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_22_22)) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (2) with all_0_22_22, all_0_1_1, xl and discharging atoms sdtasdt0(xl, all_0_1_1) = all_0_22_22, yields: % 27.68/7.62 | (71) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_0_1_1) = v1 & aNaturalNumber0(all_0_22_22) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (35) with all_0_22_22, xn yields: % 27.68/7.62 | (72) ~ (sdtpldt0(sz00, xn) = all_0_22_22) | ? [v0] : ? [v1] : (sdtpldt0(xn, sz00) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v0 = 0) | (v1 = xn & all_0_22_22 = xn))) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (41) with all_0_22_22, xn, xm and discharging atoms sdtpldt0(xm, xn) = all_0_22_22, yields: % 27.68/7.62 | (73) ? [v0] : ? [v1] : ? [v2] : (sdtpldt0(xn, xm) = v2 & aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = all_0_22_22)) % 27.68/7.62 | % 27.68/7.62 | Instantiating formula (3) with all_0_22_22, xn, xm and discharging atoms sdtpldt0(xm, xn) = all_0_22_22, yields: % 27.68/7.62 | (74) ? [v0] : ? [v1] : ? [v2] : (aNaturalNumber0(all_0_22_22) = v2 & aNaturalNumber0(xn) = v1 & aNaturalNumber0(xm) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 27.68/7.62 | % 27.68/7.62 | Instantiating (74) with all_8_0_23, all_8_1_24, all_8_2_25 yields: % 27.68/7.62 | (75) aNaturalNumber0(all_0_22_22) = all_8_0_23 & aNaturalNumber0(xn) = all_8_1_24 & aNaturalNumber0(xm) = all_8_2_25 & ( ~ (all_8_1_24 = 0) | ~ (all_8_2_25 = 0) | all_8_0_23 = 0) % 27.68/7.62 | % 27.68/7.62 | Applying alpha-rule on (75) yields: % 27.68/7.62 | (76) aNaturalNumber0(all_0_22_22) = all_8_0_23 % 27.68/7.62 | (77) aNaturalNumber0(xn) = all_8_1_24 % 27.68/7.62 | (78) aNaturalNumber0(xm) = all_8_2_25 % 27.68/7.62 | (79) ~ (all_8_1_24 = 0) | ~ (all_8_2_25 = 0) | all_8_0_23 = 0 % 27.68/7.62 | % 27.68/7.62 | Instantiating (73) with all_10_0_26, all_10_1_27, all_10_2_28 yields: % 27.68/7.62 | (80) sdtpldt0(xn, xm) = all_10_0_26 & aNaturalNumber0(xn) = all_10_1_27 & aNaturalNumber0(xm) = all_10_2_28 & ( ~ (all_10_1_27 = 0) | ~ (all_10_2_28 = 0) | all_10_0_26 = all_0_22_22) % 27.68/7.62 | % 27.68/7.62 | Applying alpha-rule on (80) yields: % 27.68/7.62 | (81) sdtpldt0(xn, xm) = all_10_0_26 % 27.68/7.62 | (82) aNaturalNumber0(xn) = all_10_1_27 % 27.68/7.62 | (83) aNaturalNumber0(xm) = all_10_2_28 % 27.68/7.62 | (84) ~ (all_10_1_27 = 0) | ~ (all_10_2_28 = 0) | all_10_0_26 = all_0_22_22 % 27.68/7.62 | % 27.68/7.62 | Instantiating (68) with all_12_0_29, all_12_1_30, all_12_2_31 yields: % 27.68/7.62 | (85) sdtasdt0(all_0_0_0, xl) = all_12_0_29 & aNaturalNumber0(all_0_0_0) = all_12_1_30 & aNaturalNumber0(xl) = all_12_2_31 & ( ~ (all_12_1_30 = 0) | ~ (all_12_2_31 = 0) | all_12_0_29 = xm) % 27.68/7.62 | % 27.68/7.62 | Applying alpha-rule on (85) yields: % 27.68/7.62 | (86) sdtasdt0(all_0_0_0, xl) = all_12_0_29 % 27.68/7.62 | (87) aNaturalNumber0(all_0_0_0) = all_12_1_30 % 27.68/7.62 | (88) aNaturalNumber0(xl) = all_12_2_31 % 27.68/7.62 | (89) ~ (all_12_1_30 = 0) | ~ (all_12_2_31 = 0) | all_12_0_29 = xm % 27.68/7.62 | % 27.68/7.62 | Instantiating (71) with all_16_0_38, all_16_1_39, all_16_2_40 yields: % 27.68/7.62 | (90) aNaturalNumber0(all_0_1_1) = all_16_1_39 & aNaturalNumber0(all_0_22_22) = all_16_0_38 & aNaturalNumber0(xl) = all_16_2_40 & ( ~ (all_16_1_39 = 0) | ~ (all_16_2_40 = 0) | all_16_0_38 = 0) % 27.68/7.62 | % 27.68/7.62 | Applying alpha-rule on (90) yields: % 27.68/7.62 | (91) aNaturalNumber0(all_0_1_1) = all_16_1_39 % 27.68/7.62 | (92) aNaturalNumber0(all_0_22_22) = all_16_0_38 % 27.68/7.62 | (93) aNaturalNumber0(xl) = all_16_2_40 % 27.68/7.62 | (94) ~ (all_16_1_39 = 0) | ~ (all_16_2_40 = 0) | all_16_0_38 = 0 % 27.68/7.62 | % 27.68/7.62 | Instantiating (70) with all_18_0_41, all_18_1_42, all_18_2_43 yields: % 27.68/7.62 | (95) sdtasdt0(all_0_1_1, xl) = all_18_0_41 & aNaturalNumber0(all_0_1_1) = all_18_1_42 & aNaturalNumber0(xl) = all_18_2_43 & ( ~ (all_18_1_42 = 0) | ~ (all_18_2_43 = 0) | all_18_0_41 = all_0_22_22) % 27.68/7.62 | % 27.68/7.62 | Applying alpha-rule on (95) yields: % 27.68/7.62 | (96) sdtasdt0(all_0_1_1, xl) = all_18_0_41 % 27.68/7.62 | (97) aNaturalNumber0(all_0_1_1) = all_18_1_42 % 27.68/7.62 | (98) aNaturalNumber0(xl) = all_18_2_43 % 27.68/7.62 | (99) ~ (all_18_1_42 = 0) | ~ (all_18_2_43 = 0) | all_18_0_41 = all_0_22_22 % 27.68/7.62 | % 27.68/7.62 +-Applying beta-rule and splitting (66), into two cases. % 27.68/7.62 |-Branch one: % 27.68/7.62 | (100) all_0_19_19 = 0 % 27.68/7.62 | % 27.68/7.62 | Equations (100) can reduce 7 to: % 27.68/7.62 | (101) $false % 27.68/7.62 | % 27.68/7.62 |-The branch is then unsatisfiable % 27.68/7.62 |-Branch two: % 27.68/7.62 | (7) ~ (all_0_19_19 = 0) % 27.68/7.63 | (103) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (doDivides0(xm, xn) = v3 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xm) = v1 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 27.68/7.63 | % 27.68/7.63 | Instantiating (103) with all_24_0_44, all_24_1_45, all_24_2_46, all_24_3_47 yields: % 27.68/7.63 | (104) doDivides0(xm, xn) = all_24_0_44 & aNaturalNumber0(xn) = all_24_1_45 & aNaturalNumber0(xm) = all_24_2_46 & aNaturalNumber0(xl) = all_24_3_47 & ( ~ (all_24_0_44 = 0) | ~ (all_24_1_45 = 0) | ~ (all_24_2_46 = 0) | ~ (all_24_3_47 = 0)) % 27.68/7.63 | % 27.68/7.63 | Applying alpha-rule on (104) yields: % 27.68/7.63 | (105) ~ (all_24_0_44 = 0) | ~ (all_24_1_45 = 0) | ~ (all_24_2_46 = 0) | ~ (all_24_3_47 = 0) % 27.68/7.63 | (106) doDivides0(xm, xn) = all_24_0_44 % 27.68/7.63 | (107) aNaturalNumber0(xl) = all_24_3_47 % 27.68/7.63 | (108) aNaturalNumber0(xm) = all_24_2_46 % 27.68/7.63 | (109) aNaturalNumber0(xn) = all_24_1_45 % 27.68/7.63 | % 27.68/7.63 +-Applying beta-rule and splitting (65), into two cases. % 27.68/7.63 |-Branch one: % 27.68/7.63 | (100) all_0_19_19 = 0 % 27.68/7.63 | % 27.68/7.63 | Equations (100) can reduce 7 to: % 27.68/7.63 | (101) $false % 27.68/7.63 | % 27.68/7.63 |-The branch is then unsatisfiable % 27.68/7.63 |-Branch two: % 27.68/7.63 | (7) ~ (all_0_19_19 = 0) % 27.68/7.63 | (113) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (doDivides0(all_0_22_22, xn) = v3 & aNaturalNumber0(all_0_22_22) = v1 & aNaturalNumber0(xn) = v2 & aNaturalNumber0(xl) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 27.68/7.63 | % 27.68/7.63 | Instantiating (113) with all_29_0_48, all_29_1_49, all_29_2_50, all_29_3_51 yields: % 27.68/7.63 | (114) doDivides0(all_0_22_22, xn) = all_29_0_48 & aNaturalNumber0(all_0_22_22) = all_29_2_50 & aNaturalNumber0(xn) = all_29_1_49 & aNaturalNumber0(xl) = all_29_3_51 & ( ~ (all_29_0_48 = 0) | ~ (all_29_1_49 = 0) | ~ (all_29_2_50 = 0) | ~ (all_29_3_51 = 0)) % 27.68/7.63 | % 27.68/7.63 | Applying alpha-rule on (114) yields: % 27.68/7.63 | (115) ~ (all_29_0_48 = 0) | ~ (all_29_1_49 = 0) | ~ (all_29_2_50 = 0) | ~ (all_29_3_51 = 0) % 27.68/7.63 | (116) aNaturalNumber0(xn) = all_29_1_49 % 27.68/7.63 | (117) aNaturalNumber0(all_0_22_22) = all_29_2_50 % 27.68/7.63 | (118) aNaturalNumber0(xl) = all_29_3_51 % 27.68/7.63 | (119) doDivides0(all_0_22_22, xn) = all_29_0_48 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with all_0_0_0, all_12_1_30, 0 and discharging atoms aNaturalNumber0(all_0_0_0) = all_12_1_30, aNaturalNumber0(all_0_0_0) = 0, yields: % 27.68/7.63 | (120) all_12_1_30 = 0 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with all_0_1_1, all_18_1_42, 0 and discharging atoms aNaturalNumber0(all_0_1_1) = all_18_1_42, aNaturalNumber0(all_0_1_1) = 0, yields: % 27.68/7.63 | (121) all_18_1_42 = 0 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with all_0_1_1, all_16_1_39, all_18_1_42 and discharging atoms aNaturalNumber0(all_0_1_1) = all_18_1_42, aNaturalNumber0(all_0_1_1) = all_16_1_39, yields: % 27.68/7.63 | (122) all_18_1_42 = all_16_1_39 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with xn, all_24_1_45, all_29_1_49 and discharging atoms aNaturalNumber0(xn) = all_29_1_49, aNaturalNumber0(xn) = all_24_1_45, yields: % 27.68/7.63 | (123) all_29_1_49 = all_24_1_45 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with xn, all_10_1_27, 0 and discharging atoms aNaturalNumber0(xn) = all_10_1_27, aNaturalNumber0(xn) = 0, yields: % 27.68/7.63 | (124) all_10_1_27 = 0 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with xn, all_10_1_27, all_24_1_45 and discharging atoms aNaturalNumber0(xn) = all_24_1_45, aNaturalNumber0(xn) = all_10_1_27, yields: % 27.68/7.63 | (125) all_24_1_45 = all_10_1_27 % 27.68/7.63 | % 27.68/7.63 | Instantiating formula (26) with xn, all_8_1_24, all_29_1_49 and discharging atoms aNaturalNumber0(xn) = all_29_1_49, aNaturalNumber0(xn) = all_8_1_24, yields: % 27.68/7.63 | (126) all_29_1_49 = all_8_1_24 % 27.68/7.63 | % 27.68/7.63 | Combining equations (123,126) yields a new equation: % 27.68/7.63 | (127) all_24_1_45 = all_8_1_24 % 27.68/7.63 | % 27.68/7.63 | Simplifying 127 yields: % 27.68/7.63 | (128) all_24_1_45 = all_8_1_24 % 27.68/7.63 | % 27.68/7.63 | Combining equations (125,128) yields a new equation: % 27.68/7.63 | (129) all_10_1_27 = all_8_1_24 % 27.68/7.63 | % 27.68/7.63 | Simplifying 129 yields: % 27.68/7.63 | (130) all_10_1_27 = all_8_1_24 % 27.68/7.63 | % 27.68/7.63 | Combining equations (122,121) yields a new equation: % 27.68/7.63 | (131) all_16_1_39 = 0 % 27.68/7.63 | % 27.68/7.63 | Simplifying 131 yields: % 27.68/7.63 | (132) all_16_1_39 = 0 % 27.68/7.63 | % 27.68/7.63 | Combining equations (124,130) yields a new equation: % 27.68/7.63 | (133) all_8_1_24 = 0 % 27.68/7.63 | % 27.68/7.63 | From (120) and (87) follows: % 27.68/7.63 | (22) aNaturalNumber0(all_0_0_0) = 0 % 27.68/7.63 | % 27.68/7.63 | From (132) and (91) follows: % 27.68/7.63 | (39) aNaturalNumber0(all_0_1_1) = 0 % 27.68/7.63 | % 27.68/7.63 | From (133) and (77) follows: % 27.68/7.63 | (12) aNaturalNumber0(xn) = 0 % 27.68/7.63 | % 27.68/7.63 +-Applying beta-rule and splitting (69), into two cases. % 27.68/7.63 |-Branch one: % 27.68/7.63 | (137) ~ (sdtasdt0(xl, all_0_1_1) = xn) % 27.68/7.63 | % 27.68/7.63 | Using (40) and (137) yields: % 27.68/7.63 | (138) ~ (all_0_22_22 = xn) % 27.68/7.63 | % 27.68/7.63 +-Applying beta-rule and splitting (72), into two cases. % 27.68/7.63 |-Branch one: % 27.68/7.63 | (139) ~ (sdtpldt0(sz00, xn) = all_0_22_22) % 27.68/7.63 | % 27.68/7.63 | Using (38) and (139) yields: % 27.68/7.63 | (140) ~ (xm = sz00) % 27.68/7.63 | % 27.68/7.63 +-Applying beta-rule and splitting (67), into two cases. % 27.68/7.63 |-Branch one: % 27.68/7.63 | (141) ~ (sdtasdt0(sz00, all_0_0_0) = xm) % 27.68/7.63 | % 27.68/7.63 | Using (60) and (141) yields: % 27.68/7.63 | (142) ~ (xl = sz00) % 27.68/7.63 | % 27.68/7.63 +-Applying beta-rule and splitting (5), into two cases. % 27.68/7.63 |-Branch one: % 27.68/7.63 | (143) xl = sz00 % 27.68/7.63 | % 27.68/7.63 | Equations (143) can reduce 142 to: % 27.68/7.63 | (101) $false % 27.68/7.63 | % 27.68/7.63 |-The branch is then unsatisfiable % 27.68/7.63 |-Branch two: % 27.68/7.63 | (142) ~ (xl = sz00) % 27.68/7.63 | (146) all_0_2_2 = all_0_20_20 & all_0_3_3 = 0 & all_0_5_5 = all_0_22_22 & all_0_6_6 = xn & all_0_7_7 = all_0_20_20 & all_0_8_8 = 0 & all_0_9_9 = all_0_10_10 & all_0_11_11 = 0 & all_0_12_12 = all_0_22_22 & all_0_13_13 = 0 & all_0_14_14 = all_0_20_20 & all_0_15_15 = all_0_22_22 & all_0_16_16 = xm & all_0_17_17 = 0 & all_0_18_18 = all_0_21_21 & sdtmndt0(all_0_20_20, all_0_21_21) = all_0_10_10 & sdtlseqdt0(all_0_21_21, all_0_20_20) = 0 & sdtasdt0(xl, all_0_10_10) = xn & sdtasdt0(xl, all_0_20_20) = all_0_22_22 & sdtasdt0(xl, all_0_21_21) = xm & sdtpldt0(all_0_21_21, all_0_4_4) = all_0_20_20 & sdtpldt0(all_0_21_21, all_0_10_10) = all_0_20_20 & aNaturalNumber0(all_0_4_4) = 0 & aNaturalNumber0(all_0_10_10) = 0 & aNaturalNumber0(all_0_20_20) = 0 & aNaturalNumber0(all_0_21_21) = 0 % 27.68/7.63 | % 27.68/7.63 | Applying alpha-rule on (146) yields: % 27.68/7.63 | (147) all_0_3_3 = 0 % 27.68/7.63 | (148) all_0_5_5 = all_0_22_22 % 27.68/7.63 | (149) sdtasdt0(xl, all_0_10_10) = xn % 27.68/7.63 | (150) aNaturalNumber0(all_0_21_21) = 0 % 27.68/7.63 | (151) all_0_8_8 = 0 % 27.68/7.63 | (152) sdtpldt0(all_0_21_21, all_0_4_4) = all_0_20_20 % 27.68/7.63 | (153) sdtpldt0(all_0_21_21, all_0_10_10) = all_0_20_20 % 27.68/7.63 | (154) all_0_15_15 = all_0_22_22 % 27.68/7.63 | (155) sdtmndt0(all_0_20_20, all_0_21_21) = all_0_10_10 % 27.68/7.63 | (156) sdtasdt0(xl, all_0_20_20) = all_0_22_22 % 27.68/7.63 | (157) all_0_6_6 = xn % 27.68/7.63 | (158) aNaturalNumber0(all_0_4_4) = 0 % 27.68/7.63 | (159) all_0_13_13 = 0 % 27.68/7.64 | (160) aNaturalNumber0(all_0_10_10) = 0 % 27.68/7.64 | (161) sdtlseqdt0(all_0_21_21, all_0_20_20) = 0 % 27.68/7.64 | (162) all_0_11_11 = 0 % 27.68/7.64 | (163) all_0_7_7 = all_0_20_20 % 27.68/7.64 | (164) all_0_12_12 = all_0_22_22 % 27.68/7.64 | (165) all_0_14_14 = all_0_20_20 % 27.68/7.64 | (166) all_0_2_2 = all_0_20_20 % 27.68/7.64 | (167) all_0_18_18 = all_0_21_21 % 27.68/7.64 | (168) all_0_9_9 = all_0_10_10 % 27.68/7.64 | (169) all_0_16_16 = xm % 27.68/7.64 | (170) all_0_17_17 = 0 % 27.68/7.64 | (171) sdtasdt0(xl, all_0_21_21) = xm % 27.68/7.64 | (172) aNaturalNumber0(all_0_20_20) = 0 % 27.68/7.64 | % 27.68/7.64 | Instantiating formula (51) with all_0_10_10 and discharging atoms sdtasdt0(xl, all_0_10_10) = xn, yields: % 27.68/7.64 | (173) ? [v0] : ( ~ (v0 = 0) & aNaturalNumber0(all_0_10_10) = v0) % 27.68/7.64 | % 27.68/7.64 | Instantiating (173) with all_162_0_85 yields: % 27.68/7.64 | (174) ~ (all_162_0_85 = 0) & aNaturalNumber0(all_0_10_10) = all_162_0_85 % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (174) yields: % 27.68/7.64 | (175) ~ (all_162_0_85 = 0) % 27.68/7.64 | (176) aNaturalNumber0(all_0_10_10) = all_162_0_85 % 27.68/7.64 | % 27.68/7.64 | Instantiating formula (26) with all_0_10_10, all_162_0_85, 0 and discharging atoms aNaturalNumber0(all_0_10_10) = all_162_0_85, aNaturalNumber0(all_0_10_10) = 0, yields: % 27.68/7.64 | (177) all_162_0_85 = 0 % 27.68/7.64 | % 27.68/7.64 | Equations (177) can reduce 175 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 |-Branch two: % 27.68/7.64 | (179) sdtasdt0(sz00, all_0_0_0) = xm % 27.68/7.64 | (180) ? [v0] : ? [v1] : (sdtasdt0(all_0_0_0, sz00) = v1 & aNaturalNumber0(all_0_0_0) = v0 & ( ~ (v0 = 0) | (v1 = sz00 & xm = sz00))) % 27.68/7.64 | % 27.68/7.64 | Instantiating (180) with all_115_0_109, all_115_1_110 yields: % 27.68/7.64 | (181) sdtasdt0(all_0_0_0, sz00) = all_115_0_109 & aNaturalNumber0(all_0_0_0) = all_115_1_110 & ( ~ (all_115_1_110 = 0) | (all_115_0_109 = sz00 & xm = sz00)) % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (181) yields: % 27.68/7.64 | (182) sdtasdt0(all_0_0_0, sz00) = all_115_0_109 % 27.68/7.64 | (183) aNaturalNumber0(all_0_0_0) = all_115_1_110 % 27.68/7.64 | (184) ~ (all_115_1_110 = 0) | (all_115_0_109 = sz00 & xm = sz00) % 27.68/7.64 | % 27.68/7.64 +-Applying beta-rule and splitting (184), into two cases. % 27.68/7.64 |-Branch one: % 27.68/7.64 | (185) ~ (all_115_1_110 = 0) % 27.68/7.64 | % 27.68/7.64 | Instantiating formula (26) with all_0_0_0, all_115_1_110, 0 and discharging atoms aNaturalNumber0(all_0_0_0) = all_115_1_110, aNaturalNumber0(all_0_0_0) = 0, yields: % 27.68/7.64 | (186) all_115_1_110 = 0 % 27.68/7.64 | % 27.68/7.64 | Equations (186) can reduce 185 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 |-Branch two: % 27.68/7.64 | (186) all_115_1_110 = 0 % 27.68/7.64 | (189) all_115_0_109 = sz00 & xm = sz00 % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (189) yields: % 27.68/7.64 | (190) all_115_0_109 = sz00 % 27.68/7.64 | (191) xm = sz00 % 27.68/7.64 | % 27.68/7.64 | Equations (191) can reduce 140 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 |-Branch two: % 27.68/7.64 | (193) sdtpldt0(sz00, xn) = all_0_22_22 % 27.68/7.64 | (194) ? [v0] : ? [v1] : (sdtpldt0(xn, sz00) = v1 & aNaturalNumber0(xn) = v0 & ( ~ (v0 = 0) | (v1 = xn & all_0_22_22 = xn))) % 27.68/7.64 | % 27.68/7.64 | Instantiating (194) with all_103_0_111, all_103_1_112 yields: % 27.68/7.64 | (195) sdtpldt0(xn, sz00) = all_103_0_111 & aNaturalNumber0(xn) = all_103_1_112 & ( ~ (all_103_1_112 = 0) | (all_103_0_111 = xn & all_0_22_22 = xn)) % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (195) yields: % 27.68/7.64 | (196) sdtpldt0(xn, sz00) = all_103_0_111 % 27.68/7.64 | (197) aNaturalNumber0(xn) = all_103_1_112 % 27.68/7.64 | (198) ~ (all_103_1_112 = 0) | (all_103_0_111 = xn & all_0_22_22 = xn) % 27.68/7.64 | % 27.68/7.64 +-Applying beta-rule and splitting (198), into two cases. % 27.68/7.64 |-Branch one: % 27.68/7.64 | (199) ~ (all_103_1_112 = 0) % 27.68/7.64 | % 27.68/7.64 | Instantiating formula (26) with xn, all_103_1_112, 0 and discharging atoms aNaturalNumber0(xn) = all_103_1_112, aNaturalNumber0(xn) = 0, yields: % 27.68/7.64 | (200) all_103_1_112 = 0 % 27.68/7.64 | % 27.68/7.64 | Equations (200) can reduce 199 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 |-Branch two: % 27.68/7.64 | (200) all_103_1_112 = 0 % 27.68/7.64 | (203) all_103_0_111 = xn & all_0_22_22 = xn % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (203) yields: % 27.68/7.64 | (204) all_103_0_111 = xn % 27.68/7.64 | (205) all_0_22_22 = xn % 27.68/7.64 | % 27.68/7.64 | Equations (205) can reduce 138 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 |-Branch two: % 27.68/7.64 | (207) sdtasdt0(xl, all_0_1_1) = xn % 27.68/7.64 | (208) ? [v0] : ( ~ (v0 = 0) & aNaturalNumber0(all_0_1_1) = v0) % 27.68/7.64 | % 27.68/7.64 | Instantiating (208) with all_51_0_113 yields: % 27.68/7.64 | (209) ~ (all_51_0_113 = 0) & aNaturalNumber0(all_0_1_1) = all_51_0_113 % 27.68/7.64 | % 27.68/7.64 | Applying alpha-rule on (209) yields: % 27.68/7.64 | (210) ~ (all_51_0_113 = 0) % 27.68/7.64 | (211) aNaturalNumber0(all_0_1_1) = all_51_0_113 % 27.68/7.64 | % 27.68/7.64 | Instantiating formula (26) with all_0_1_1, all_51_0_113, 0 and discharging atoms aNaturalNumber0(all_0_1_1) = all_51_0_113, aNaturalNumber0(all_0_1_1) = 0, yields: % 27.68/7.64 | (212) all_51_0_113 = 0 % 27.68/7.64 | % 27.68/7.64 | Equations (212) can reduce 210 to: % 27.68/7.64 | (101) $false % 27.68/7.64 | % 27.68/7.64 |-The branch is then unsatisfiable % 27.68/7.64 % SZS output end Proof for theBenchmark % 27.68/7.64 % 27.68/7.64 7045ms %------------------------------------------------------------------------------