%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM452+6 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n013.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:37 EDT 2022 % Result : Theorem 6.95s 2.26s % Output : Proof 13.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM452+6 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.35 % Computer : n013.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Wed Jul 6 03:16:59 EDT 2022 % 0.14/0.35 % CPUTime : % 0.64/0.61 ____ _ % 0.64/0.61 ___ / __ \_____(_)___ ________ __________ % 0.64/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.64/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.64/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.64/0.61 % 0.64/0.61 A Theorem Prover for First-Order Logic % 0.64/0.61 (ePrincess v.1.0) % 0.64/0.61 % 0.64/0.61 (c) Philipp Rümmer, 2009-2015 % 0.64/0.61 (c) Peter Backeman, 2014-2015 % 0.64/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.64/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.64/0.61 Bug reports to peter@backeman.se % 0.64/0.61 % 0.64/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.64/0.61 % 0.64/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.68/0.69 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.99/1.12 Prover 0: Preprocessing ... % 4.38/1.66 Prover 0: Warning: ignoring some quantifiers % 4.43/1.70 Prover 0: Constructing countermodel ... % 6.95/2.25 Prover 0: proved (1569ms) % 6.95/2.26 % 6.95/2.26 No countermodel exists, formula is valid % 6.95/2.26 % SZS status Theorem for theBenchmark % 6.95/2.26 % 6.95/2.26 Generating proof ... Warning: ignoring some quantifiers % 12.32/3.48 found it (size 142) % 12.32/3.48 % 12.32/3.48 % SZS output start Proof for theBenchmark % 12.32/3.48 Assumed formulas after preprocessing and simplification: % 12.32/3.48 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (cS2043 = xS & ~ (xp = sz00) & szAzrzSzezqlpdtcmdtrp0(sz10, xp) = v3 & stldt0(v2) = cS2076 & sbsmnsldt0(xS) = v2 & sdtpldt0(v7, v0) = v8 & sdtpldt0(v4, v0) = v5 & sdtpldt0(sz10, v6) = v7 & sdtpldt0(sz10, xp) = v4 & smndt0(xp) = v6 & smndt0(sz10) = v0 & smndt0(sz00) = v1 & isClosed0(v2) & isOpen0(cS2076) & isFinite0(xS) & aSubsetOf0(v3, cS2076) & aElementOf0(v0, cS2076) & aElementOf0(sz10, cS2076) & aSet0(v3) & aSet0(v2) & aSet0(cS2076) & aSet0(xS) & aInteger0(xp) & aInteger0(sz10) & aInteger0(sz00) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (sdtasdt0(v10, v11) = v13) | ~ (sdtasdt0(v9, v11) = v12) | ~ (sdtpldt0(v12, v13) = v14) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasdt0(v18, v11) = v14 & sdtasdt0(v9, v15) = v16 & sdtasdt0(v9, v10) = v17 & sdtpldt0(v17, v12) = v16 & sdtpldt0(v10, v11) = v15 & sdtpldt0(v9, v10) = v18)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (sdtasdt0(v9, v11) = v13) | ~ (sdtasdt0(v9, v10) = v12) | ~ (sdtpldt0(v12, v13) = v14) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasdt0(v16, v11) = v17 & sdtasdt0(v10, v11) = v18 & sdtasdt0(v9, v15) = v14 & sdtpldt0(v13, v18) = v17 & sdtpldt0(v10, v11) = v15 & sdtpldt0(v9, v10) = v16)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtasdt0(v10, v14) = v13) | ~ (sdtpldt0(v12, v1) = v13) | ~ isPrime0(v10) | ~ aInteger0(v14) | ~ aInteger0(v12) | ~ aInteger0(v10) | aElementOf0(v12, v11) | aElementOf0(v9, xS)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v12 = sz00 | v11 = sz00 | ~ (sdtasdt0(v11, v12) = v13) | ~ sdteqdtlpzmzozddtrp0(v9, v10, v13) | ~ aInteger0(v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v9, v10, v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v12 = sz00 | v11 = sz00 | ~ (sdtasdt0(v11, v12) = v13) | ~ sdteqdtlpzmzozddtrp0(v9, v10, v13) | ~ aInteger0(v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v9, v10, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = sz00 | ~ (sdtpldt0(v9, v12) = v13) | ~ (smndt0(v10) = v12) | ~ sdteqdtlpzmzozddtrp0(v9, v10, v11) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aDivisorOf0(v11, v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v11 = sz00 | ~ (sdtpldt0(v9, v12) = v13) | ~ (smndt0(v10) = v12) | ~ aDivisorOf0(v11, v13) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v9, v10, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v12, v11) = v13) | ~ (sdtasdt0(v9, v10) = v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : (sdtasdt0(v10, v11) = v14 & sdtasdt0(v9, v14) = v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v12, v11) = v13) | ~ (sdtpldt0(v9, v10) = v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasdt0(v10, v11) = v18 & sdtasdt0(v9, v14) = v15 & sdtasdt0(v9, v11) = v17 & sdtasdt0(v9, v10) = v16 & sdtpldt0(v17, v18) = v13 & sdtpldt0(v16, v17) = v15 & sdtpldt0(v10, v11) = v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v10, v11) = v12) | ~ (sdtasdt0(v9, v12) = v13) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : (sdtasdt0(v14, v11) = v13 & sdtasdt0(v9, v10) = v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v9, v12) = v13) | ~ (sdtpldt0(v10, v11) = v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (sdtasdt0(v16, v11) = v17 & sdtasdt0(v10, v11) = v18 & sdtasdt0(v9, v11) = v15 & sdtasdt0(v9, v10) = v14 & sdtpldt0(v15, v18) = v17 & sdtpldt0(v14, v15) = v13 & sdtpldt0(v9, v10) = v16)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtpldt0(v12, v11) = v13) | ~ (sdtpldt0(v9, v10) = v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : (sdtpldt0(v10, v11) = v14 & sdtpldt0(v9, v14) = v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtpldt0(v10, v11) = v12) | ~ (sdtpldt0(v9, v12) = v13) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v14] : (sdtpldt0(v14, v11) = v13 & sdtpldt0(v9, v10) = v14)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ aElementOf0(v12, v11) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS) | sdteqdtlpzmzozddtrp0(v12, sz00, v10)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ aElementOf0(v12, v11) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS) | aDivisorOf0(v10, v13)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ aElementOf0(v12, v11) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS) | aInteger0(v12)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ aElementOf0(v12, v11) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS) | ? [v14] : (sdtasdt0(v10, v14) = v13 & aInteger0(v14))) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ isPrime0(v10) | ~ sdteqdtlpzmzozddtrp0(v12, sz00, v10) | ~ aInteger0(v12) | ~ aInteger0(v10) | aElementOf0(v12, v11) | aElementOf0(v9, xS)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ (sdtpldt0(v12, v1) = v13) | ~ isPrime0(v10) | ~ aDivisorOf0(v10, v13) | ~ aInteger0(v12) | ~ aInteger0(v10) | aElementOf0(v12, v11) | aElementOf0(v9, xS)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = v11 | v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aSet0(v12) | ~ aInteger0(v10) | ~ aInteger0(v9) | ? [v13] : (( ~ aElementOf0(v13, v12) | ~ sdteqdtlpzmzozddtrp0(v13, v9, v10) | ~ aInteger0(v13)) & (aElementOf0(v13, v12) | (sdteqdtlpzmzozddtrp0(v13, v9, v10) & aInteger0(v13))))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = v11 | ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aSet0(v12) | ? [v13] : (( ~ aElementOf0(v13, v12) | ~ aElementOf0(v13, v10) | ~ aElementOf0(v13, v9) | ~ aInteger0(v13)) & (aElementOf0(v13, v12) | (aElementOf0(v13, v10) & aElementOf0(v13, v9) & aInteger0(v13))))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = v11 | ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aSet0(v12) | ? [v13] : (( ~ aElementOf0(v13, v12) | ~ aInteger0(v13) | ( ~ aElementOf0(v13, v10) & ~ aElementOf0(v13, v9))) & (aElementOf0(v13, v12) | (aInteger0(v13) & (aElementOf0(v13, v10) | aElementOf0(v13, v9)))))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v11 = sz00 | ~ sdteqdtlpzmzozddtrp0(v10, v12, v11) | ~ sdteqdtlpzmzozddtrp0(v9, v10, v11) | ~ aInteger0(v12) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v9, v12, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (szAzrzSzezqlpdtcmdtrp0(v12, v11) = v10) | ~ (szAzrzSzezqlpdtcmdtrp0(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (sdtslmnbsdt0(v12, v11) = v10) | ~ (sdtslmnbsdt0(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (sdtbsmnsldt0(v12, v11) = v10) | ~ (sdtbsmnsldt0(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (sdtasdt0(v12, v11) = v10) | ~ (sdtasdt0(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (sdtpldt0(v12, v11) = v10) | ~ (sdtpldt0(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aElementOf0(v12, v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v12, v9, v10)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aElementOf0(v12, v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aInteger0(v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ sdteqdtlpzmzozddtrp0(v12, v9, v10) | ~ aInteger0(v12) | ~ aInteger0(v10) | ~ aInteger0(v9) | aElementOf0(v12, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sbsmnsldt0(v9) = v10) | ~ aElementOf0(v12, v9) | ~ aElementOf0(v11, v12) | ~ aSet0(v9) | ~ aInteger0(v11) | aElementOf0(v11, v10) | ? [v13] : (aElementOf0(v13, v9) & ~ aSubsetOf0(v13, cS1395))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v11) | aElementOf0(v12, v10)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v11) | aElementOf0(v12, v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v11) | aInteger0(v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v10) | ~ aElementOf0(v12, v9) | ~ aInteger0(v12) | aElementOf0(v12, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v11) | aElementOf0(v12, v10) | aElementOf0(v12, v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v11) | aInteger0(v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v10) | ~ aInteger0(v12) | aElementOf0(v12, v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v12, v9) | ~ aInteger0(v12) | aElementOf0(v12, v11)) & ! [v9] : ! [v10] : ! [v11] : (v11 = v10 | ~ (stldt0(v9) = v10) | ~ aSubsetOf0(v9, cS1395) | ~ aSet0(v11) | ? [v12] : (( ~ aElementOf0(v12, v11) | ~ aInteger0(v12) | aElementOf0(v12, v9)) & (aElementOf0(v12, v11) | (aInteger0(v12) & ~ aElementOf0(v12, v9))))) & ! [v9] : ! [v10] : ! [v11] : (v11 = v10 | ~ (sbsmnsldt0(v9) = v10) | ~ aSet0(v11) | ~ aSet0(v9) | ? [v12] : ? [v13] : ((aElementOf0(v12, v9) & ~ aSubsetOf0(v12, cS1395)) | (( ~ aElementOf0(v12, v11) | ~ aInteger0(v12) | ! [v14] : ( ~ aElementOf0(v14, v9) | ~ aElementOf0(v12, v14))) & (aElementOf0(v12, v11) | (aElementOf0(v13, v9) & aElementOf0(v12, v13) & aInteger0(v12)))))) & ! [v9] : ! [v10] : ! [v11] : (v11 = sz00 | ~ (sdtpldt0(v10, v9) = v11) | ~ (smndt0(v9) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : ! [v11] : (v11 = sz00 | ~ (sdtpldt0(v9, v10) = v11) | ~ (smndt0(v9) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : ! [v11] : (v11 = sz00 | ~ sdteqdtlpzmzozddtrp0(v9, v10, v11) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v10, v9, v11)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (stldt0(v11) = v10) | ~ (stldt0(v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (sbsmnsldt0(v11) = v10) | ~ (sbsmnsldt0(v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (smndt0(v11) = v10) | ~ (smndt0(v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | isClosed0(v11)) & ! [v9] : ! [v10] : ! [v11] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aSubsetOf0(v11, cS1395)) & ! [v9] : ! [v10] : ! [v11] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aSet0(v11)) & ! [v9] : ! [v10] : ! [v11] : (v10 = sz00 | ~ (sdtasdt0(v10, v11) = v9) | ~ aInteger0(v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aDivisorOf0(v10, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (stldt0(v9) = v10) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v11, v10) | ~ aElementOf0(v11, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (stldt0(v9) = v10) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v11, v10) | aInteger0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (stldt0(v9) = v10) | ~ aSubsetOf0(v9, cS1395) | ~ aInteger0(v11) | aElementOf0(v11, v10) | aElementOf0(v11, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sbsmnsldt0(v9) = v10) | ~ aElementOf0(v11, v10) | ~ aSet0(v9) | aInteger0(v11) | ? [v12] : (aElementOf0(v12, v9) & ~ aSubsetOf0(v12, cS1395))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sbsmnsldt0(v9) = v10) | ~ aElementOf0(v11, v10) | ~ aSet0(v9) | ? [v12] : ((aElementOf0(v12, v9) & aElementOf0(v11, v12)) | (aElementOf0(v12, v9) & ~ aSubsetOf0(v12, cS1395)))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ isOpen0(v10) | ~ isOpen0(v9) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | isOpen0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtslmnbsdt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | aSet0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ isClosed0(v10) | ~ isClosed0(v9) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | isClosed0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtbsmnsldt0(v9, v10) = v11) | ~ aSubsetOf0(v10, cS1395) | ~ aSubsetOf0(v9, cS1395) | aSet0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v10, v9) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdtasdt0(v9, v10) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdtasdt0(v10, v9) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aInteger0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtasdt0(xp, v11) = v10) | ~ (sdtpldt0(v9, v0) = v10) | ~ aInteger0(v11) | ~ aInteger0(v9) | aElementOf0(v9, v3)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v10, v9) = v11) | ~ (smndt0(v9) = v10) | ~ aInteger0(v9) | sdtpldt0(v9, v10) = sz00) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v10, v9) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdtpldt0(v9, v10) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v9, v10) = v11) | ~ (smndt0(v9) = v10) | ~ aInteger0(v9) | sdtpldt0(v10, v9) = sz00) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | sdtpldt0(v10, v9) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (sdtpldt0(v9, v10) = v11) | ~ aInteger0(v10) | ~ aInteger0(v9) | aInteger0(v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ aSubsetOf0(v10, v9) | ~ aElementOf0(v11, v10) | ~ aSet0(v9) | aElementOf0(v11, v9)) & ? [v9] : ! [v10] : ! [v11] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v11) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS) | aSet0(v11)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (sdtasdt0(v9, sz10) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (sdtasdt0(sz10, v9) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (sdtpldt0(v9, sz00) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (sdtpldt0(sz00, v9) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = sz00 | v9 = sz00 | ~ (sdtasdt0(v9, v10) = sz00) | ~ aInteger0(v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v9) | ~ isPrime0(v10) | ~ aInteger0(v10) | aElementOf0(v9, xS)) & ! [v9] : ! [v10] : (v10 = sz00 | ~ (sdtasdt0(v9, sz00) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = sz00 | ~ (sdtasdt0(sz00, v9) = v10) | ~ aInteger0(v9)) & ! [v9] : ! [v10] : (v10 = sz00 | ~ aInteger0(v10) | ~ aInteger0(v9) | sdteqdtlpzmzozddtrp0(v9, v9, v10)) & ! [v9] : ! [v10] : ( ~ (stldt0(v9) = v10) | ~ isClosed0(v9) | ~ aSubsetOf0(v9, cS1395) | isOpen0(v10)) & ! [v9] : ! [v10] : ( ~ (stldt0(v9) = v10) | ~ isOpen0(v10) | ~ aSubsetOf0(v9, cS1395) | isClosed0(v9)) & ! [v9] : ! [v10] : ( ~ (stldt0(v9) = v10) | ~ aSubsetOf0(v9, cS1395) | aSet0(v10)) & ! [v9] : ! [v10] : ( ~ (sbsmnsldt0(v9) = v10) | ~ isFinite0(v9) | ~ aSet0(v9) | isClosed0(v10) | ? [v11] : (aElementOf0(v11, v9) & ( ~ isClosed0(v11) | ~ aSubsetOf0(v11, cS1395)))) & ! [v9] : ! [v10] : ( ~ (sbsmnsldt0(v9) = v10) | ~ aSet0(v9) | isOpen0(v10) | ? [v11] : (aElementOf0(v11, v9) & ( ~ isOpen0(v11) | ~ aSubsetOf0(v11, cS1395)))) & ! [v9] : ! [v10] : ( ~ (sbsmnsldt0(v9) = v10) | ~ aSet0(v9) | aSet0(v10) | ? [v11] : (aElementOf0(v11, v9) & ~ aSubsetOf0(v11, cS1395))) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(v9, v0) = v10) | ~ aInteger0(v9) | (sdtasdt0(v0, v9) = v10 & smndt0(v9) = v10)) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(v9, sz10) = v10) | ~ aInteger0(v9) | sdtasdt0(sz10, v9) = v9) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(v9, sz00) = v10) | ~ aInteger0(v9) | sdtasdt0(sz00, v9) = sz00) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(v0, v9) = v10) | ~ aInteger0(v9) | (sdtasdt0(v9, v0) = v10 & smndt0(v9) = v10)) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(sz10, v9) = v10) | ~ aInteger0(v9) | sdtasdt0(v9, sz10) = v9) & ! [v9] : ! [v10] : ( ~ (sdtasdt0(sz00, v9) = v10) | ~ aInteger0(v9) | sdtasdt0(v9, sz00) = sz00) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ aElementOf0(v9, v3) | sdteqdtlpzmzozddtrp0(v9, sz10, xp)) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ aElementOf0(v9, v3) | aDivisorOf0(xp, v10)) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ aElementOf0(v9, v3) | aInteger0(v9)) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ aElementOf0(v9, v3) | ? [v11] : (sdtasdt0(xp, v11) = v10 & aInteger0(v11))) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ sdteqdtlpzmzozddtrp0(v9, sz10, xp) | ~ aInteger0(v9) | aElementOf0(v9, v3)) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, v0) = v10) | ~ aDivisorOf0(xp, v10) | ~ aInteger0(v9) | aElementOf0(v9, v3)) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(v9, sz00) = v10) | ~ aInteger0(v9) | sdtpldt0(sz00, v9) = v9) & ! [v9] : ! [v10] : ( ~ (sdtpldt0(sz00, v9) = v10) | ~ aInteger0(v9) | sdtpldt0(v9, sz00) = v9) & ! [v9] : ! [v10] : ( ~ (smndt0(v9) = v10) | ~ aElementOf0(v9, cS2076) | ? [v11] : ? [v12] : ( ~ (v11 = sz00) & szAzrzSzezqlpdtcmdtrp0(v9, v11) = v12 & aSubsetOf0(v12, cS2076) & aSet0(v12) & aInteger0(v11) & ! [v13] : ! [v14] : ! [v15] : ( ~ (sdtasdt0(v11, v15) = v14) | ~ (sdtpldt0(v13, v10) = v14) | ~ aInteger0(v15) | ~ aInteger0(v13) | aElementOf0(v13, v12)) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ aElementOf0(v13, v12) | sdteqdtlpzmzozddtrp0(v13, v9, v11)) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ aElementOf0(v13, v12) | aDivisorOf0(v11, v14)) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ aElementOf0(v13, v12) | aInteger0(v13)) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ aElementOf0(v13, v12) | ? [v15] : (sdtasdt0(v11, v15) = v14 & aInteger0(v15))) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ sdteqdtlpzmzozddtrp0(v13, v9, v11) | ~ aInteger0(v13) | aElementOf0(v13, v12)) & ! [v13] : ! [v14] : ( ~ (sdtpldt0(v13, v10) = v14) | ~ aDivisorOf0(v11, v14) | ~ aInteger0(v13) | aElementOf0(v13, v12)) & ! [v13] : ( ~ aElementOf0(v13, v12) | aElementOf0(v13, cS2076)))) & ! [v9] : ! [v10] : ( ~ (smndt0(v9) = v10) | ~ aInteger0(v9) | aInteger0(v10)) & ! [v9] : ! [v10] : ( ~ (smndt0(v9) = v10) | ~ aInteger0(v9) | (sdtasdt0(v9, v0) = v10 & sdtasdt0(v0, v9) = v10)) & ! [v9] : ! [v10] : ( ~ isOpen0(v9) | ~ aSubsetOf0(v9, cS1395) | ~ aElementOf0(v10, v9) | ? [v11] : ? [v12] : ( ~ (v11 = sz00) & szAzrzSzezqlpdtcmdtrp0(v10, v11) = v12 & aSubsetOf0(v12, v9) & aInteger0(v11))) & ! [v9] : ! [v10] : ( ~ aSubsetOf0(v10, v9) | ~ aSet0(v9) | aSet0(v10)) & ! [v9] : ! [v10] : ( ~ aElementOf0(v10, xS) | ~ aElementOf0(v9, v10) | ~ aInteger0(v9) | aElementOf0(v9, v2)) & ! [v9] : ! [v10] : ( ~ aSet0(v10) | ~ aSet0(v9) | aSubsetOf0(v10, v9) | ? [v11] : (aElementOf0(v11, v10) & ~ aElementOf0(v11, v9))) & ! [v9] : ! [v10] : ( ~ aDivisorOf0(v10, v9) | ~ aInteger0(v9) | aInteger0(v10)) & ! [v9] : ! [v10] : ( ~ aDivisorOf0(v10, v9) | ~ aInteger0(v9) | ? [v11] : (sdtasdt0(v10, v11) = v9 & aInteger0(v11))) & ! [v9] : (v9 = v0 | v9 = sz10 | ~ aElementOf0(v9, cS2076)) & ! [v9] : (v9 = v0 | v9 = sz10 | ~ aInteger0(v9) | ? [v10] : (isPrime0(v10) & aDivisorOf0(v10, v9))) & ! [v9] : ( ~ aSubsetOf0(v9, cS1395) | isOpen0(v9) | ? [v10] : (aElementOf0(v10, v9) & ! [v11] : ! [v12] : (v11 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v10, v11) = v12) | ~ aSubsetOf0(v12, v9) | ~ aInteger0(v11)))) & ! [v9] : ( ~ aElementOf0(v9, v3) | aElementOf0(v9, cS2076)) & ! [v9] : ( ~ aElementOf0(v9, v2) | ~ aElementOf0(v9, cS2076)) & ! [v9] : ( ~ aElementOf0(v9, v2) | aInteger0(v9)) & ! [v9] : ( ~ aElementOf0(v9, v2) | ? [v10] : (aElementOf0(v10, xS) & aElementOf0(v9, v10))) & ! [v9] : ( ~ aElementOf0(v9, cS2076) | aInteger0(v9)) & ! [v9] : ( ~ aElementOf0(v9, xS) | ? [v10] : ( ~ (v10 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v10) = v9 & aSet0(v9) & isPrime0(v10) & aInteger0(v10) & ! [v11] : ! [v12] : ! [v13] : ( ~ (sdtasdt0(v10, v13) = v12) | ~ (sdtpldt0(v11, v1) = v12) | ~ aInteger0(v13) | ~ aInteger0(v11) | aElementOf0(v11, v9)) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ aElementOf0(v11, v9) | sdteqdtlpzmzozddtrp0(v11, sz00, v10)) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ aElementOf0(v11, v9) | aDivisorOf0(v10, v12)) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ aElementOf0(v11, v9) | aInteger0(v11)) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ aElementOf0(v11, v9) | ? [v13] : (sdtasdt0(v10, v13) = v12 & aInteger0(v13))) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ sdteqdtlpzmzozddtrp0(v11, sz00, v10) | ~ aInteger0(v11) | aElementOf0(v11, v9)) & ! [v11] : ! [v12] : ( ~ (sdtpldt0(v11, v1) = v12) | ~ aDivisorOf0(v10, v12) | ~ aInteger0(v11) | aElementOf0(v11, v9)))) & ! [v9] : ( ~ isPrime0(v9) | ~ aDivisorOf0(v9, v0) | ~ aInteger0(v0)) & ! [v9] : ( ~ isPrime0(v9) | ~ aDivisorOf0(v9, sz10)) & ! [v9] : ( ~ aDivisorOf0(sz00, v9) | ~ aInteger0(v9)) & ! [v9] : ( ~ aInteger0(v9) | aElementOf0(v9, v2) | aElementOf0(v9, cS2076)) & (( ~ aElementOf0(v7, v3) & ~ sdteqdtlpzmzozddtrp0(v7, sz10, xp) & ~ aDivisorOf0(xp, v8) & ! [v9] : ( ~ aInteger0(v9) | ? [v10] : ( ~ (v10 = v8) & sdtasdt0(xp, v9) = v10))) | ( ~ aElementOf0(v4, v3) & ~ sdteqdtlpzmzozddtrp0(v4, sz10, xp) & ~ aDivisorOf0(xp, v5) & ! [v9] : ( ~ aInteger0(v9) | ? [v10] : ( ~ (v10 = v5) & sdtasdt0(xp, v9) = v10))))) % 12.48/3.56 | 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 yields: % 12.48/3.56 | (1) cS2043 = xS & ~ (xp = sz00) & szAzrzSzezqlpdtcmdtrp0(sz10, xp) = all_0_5_5 & stldt0(all_0_6_6) = cS2076 & sbsmnsldt0(xS) = all_0_6_6 & sdtpldt0(all_0_1_1, all_0_8_8) = all_0_0_0 & sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3 & sdtpldt0(sz10, all_0_2_2) = all_0_1_1 & sdtpldt0(sz10, xp) = all_0_4_4 & smndt0(xp) = all_0_2_2 & smndt0(sz10) = all_0_8_8 & smndt0(sz00) = all_0_7_7 & isClosed0(all_0_6_6) & isOpen0(cS2076) & isFinite0(xS) & aSubsetOf0(all_0_5_5, cS2076) & aElementOf0(all_0_8_8, cS2076) & aElementOf0(sz10, cS2076) & aSet0(all_0_5_5) & aSet0(all_0_6_6) & aSet0(cS2076) & aSet0(xS) & aInteger0(xp) & aInteger0(sz10) & aInteger0(sz00) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v2) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v9, v2) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v3) = v7 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v9)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v4, v9) = v8 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v7)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtasdt0(v1, v5) = v4) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ aInteger0(v5) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = sz00 | v2 = sz00 | ~ (sdtasdt0(v2, v3) = v4) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = sz00 | v2 = sz00 | ~ (sdtasdt0(v2, v3) = v4) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = sz00 | ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aDivisorOf0(v2, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = sz00 | ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ aDivisorOf0(v2, v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v5) = v6 & sdtasdt0(v0, v2) = v8 & sdtasdt0(v0, v1) = v7 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v7, v8) = v6 & sdtpldt0(v1, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v6, v9) = v8 & sdtpldt0(v5, v6) = v4 & sdtpldt0(v0, v1) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | sdteqdtlpzmzozddtrp0(v3, sz00, v1)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aDivisorOf0(v1, v4)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aInteger0(v3)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | ? [v5] : (sdtasdt0(v1, v5) = v4 & aInteger0(v5))) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ sdteqdtlpzmzozddtrp0(v3, sz00, v1) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ aDivisorOf0(v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aSet0(v3) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ sdteqdtlpzmzozddtrp0(v4, v0, v1) | ~ aInteger0(v4)) & (aElementOf0(v4, v3) | (sdteqdtlpzmzozddtrp0(v4, v0, v1) & aInteger0(v4))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v3) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v1) | ~ aElementOf0(v4, v0) | ~ aInteger0(v4)) & (aElementOf0(v4, v3) | (aElementOf0(v4, v1) & aElementOf0(v4, v0) & aInteger0(v4))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v3) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aInteger0(v4) | ( ~ aElementOf0(v4, v1) & ~ aElementOf0(v4, v0))) & (aElementOf0(v4, v3) | (aInteger0(v4) & (aElementOf0(v4, v1) | aElementOf0(v4, v0)))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = sz00 | ~ sdteqdtlpzmzozddtrp0(v1, v3, v2) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v1) | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtslmnbsdt0(v3, v2) = v1) | ~ (sdtslmnbsdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtbsmnsldt0(v3, v2) = v1) | ~ (sdtbsmnsldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v3, v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ sdteqdtlpzmzozddtrp0(v3, v0, v1) | ~ aInteger0(v3) | ~ aInteger0(v1) | ~ aInteger0(v0) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v3, v0) | ~ aElementOf0(v2, v3) | ~ aSet0(v0) | ~ aInteger0(v2) | aElementOf0(v2, v1) | ? [v4] : (aElementOf0(v4, v0) & ~ aSubsetOf0(v4, cS1395))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aInteger0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v1) | ~ aElementOf0(v3, v0) | ~ aInteger0(v3) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v1) | aElementOf0(v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aInteger0(v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v1) | ~ aInteger0(v3) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v0) | ~ aInteger0(v3) | aElementOf0(v3, v2)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v2) | ? [v3] : (( ~ aElementOf0(v3, v2) | ~ aInteger0(v3) | aElementOf0(v3, v0)) & (aElementOf0(v3, v2) | (aInteger0(v3) & ~ aElementOf0(v3, v0))))) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v2) | ~ aSet0(v0) | ? [v3] : ? [v4] : ((aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395)) | (( ~ aElementOf0(v3, v2) | ~ aInteger0(v3) | ! [v5] : ( ~ aElementOf0(v5, v0) | ~ aElementOf0(v3, v5))) & (aElementOf0(v3, v2) | (aElementOf0(v4, v0) & aElementOf0(v3, v4) & aInteger0(v3)))))) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v1, v0, v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (stldt0(v2) = v1) | ~ (stldt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbsmnsldt0(v2) = v1) | ~ (sbsmnsldt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | isClosed0(v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aSubsetOf0(v2, cS1395)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (sdtasdt0(v1, v2) = v0) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aDivisorOf0(v1, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v2, v1) | aInteger0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aInteger0(v2) | aElementOf0(v2, v1) | aElementOf0(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aInteger0(v2) | ? [v3] : (aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | ? [v3] : ((aElementOf0(v3, v0) & aElementOf0(v2, v3)) | (aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ isOpen0(v1) | ~ isOpen0(v0) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | isOpen0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ isClosed0(v1) | ~ isClosed0(v0) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | isClosed0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | aSet0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtasdt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtasdt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(xp, v2) = v1) | ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aInteger0(v2) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v0, v1) = sz00) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtpldt0(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v1, v0) = sz00) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtpldt0(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v0) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aElementOf0(v2, v0)) & ? [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aSet0(v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aInteger0(v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aInteger0(v0)) & ! [v0] : ! [v1] : (v1 = sz00 | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v0, v1)) & ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ isClosed0(v0) | ~ aSubsetOf0(v0, cS1395) | isOpen0(v1)) & ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ isOpen0(v1) | ~ aSubsetOf0(v0, cS1395) | isClosed0(v0)) & ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | isClosed0(v1) | ? [v2] : (aElementOf0(v2, v0) & ( ~ isClosed0(v2) | ~ aSubsetOf0(v2, cS1395)))) & ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v0) | isOpen0(v1) | ? [v2] : (aElementOf0(v2, v0) & ( ~ isOpen0(v2) | ~ aSubsetOf0(v2, cS1395)))) & ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v0) | aSet0(v1) | ? [v2] : (aElementOf0(v2, v0) & ~ aSubsetOf0(v2, cS1395))) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, all_0_8_8) = v1) | ~ aInteger0(v0) | (sdtasdt0(all_0_8_8, v0) = v1 & smndt0(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aInteger0(v0) | sdtasdt0(sz10, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aInteger0(v0) | sdtasdt0(sz00, v0) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(all_0_8_8, v0) = v1) | ~ aInteger0(v0) | (sdtasdt0(v0, all_0_8_8) = v1 & smndt0(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aInteger0(v0) | sdtasdt0(v0, sz10) = v0) & ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aInteger0(v0) | sdtasdt0(v0, sz00) = sz00) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | sdteqdtlpzmzozddtrp0(v0, sz10, xp)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | aDivisorOf0(xp, v1)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | aInteger0(v0)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | ? [v2] : (sdtasdt0(xp, v2) = v1 & aInteger0(v2))) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ sdteqdtlpzmzozddtrp0(v0, sz10, xp) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aDivisorOf0(xp, v1) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aInteger0(v0) | sdtpldt0(sz00, v0) = v0) & ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v0, sz00) = v0) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElementOf0(v0, cS2076) | ? [v2] : ? [v3] : ( ~ (v2 = sz00) & szAzrzSzezqlpdtcmdtrp0(v0, v2) = v3 & aSubsetOf0(v3, cS2076) & aSet0(v3) & aInteger0(v2) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v2, v6) = v5) | ~ (sdtpldt0(v4, v1) = v5) | ~ aInteger0(v6) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | sdteqdtlpzmzozddtrp0(v4, v0, v2)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | aDivisorOf0(v2, v5)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | aInteger0(v4)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | ? [v6] : (sdtasdt0(v2, v6) = v5 & aInteger0(v6))) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ sdteqdtlpzmzozddtrp0(v4, v0, v2) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aDivisorOf0(v2, v5) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ( ~ aElementOf0(v4, v3) | aElementOf0(v4, cS2076)))) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | aInteger0(v1)) & ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | (sdtasdt0(v0, all_0_8_8) = v1 & sdtasdt0(all_0_8_8, v0) = v1)) & ! [v0] : ! [v1] : ( ~ isOpen0(v0) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v1, v0) | ? [v2] : ? [v3] : ( ~ (v2 = sz00) & szAzrzSzezqlpdtcmdtrp0(v1, v2) = v3 & aSubsetOf0(v3, v0) & aInteger0(v2))) & ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ aSet0(v0) | aSet0(v1)) & ! [v0] : ! [v1] : ( ~ aElementOf0(v1, xS) | ~ aElementOf0(v0, v1) | ~ aInteger0(v0) | aElementOf0(v0, all_0_6_6)) & ! [v0] : ! [v1] : ( ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v1, v0) | ? [v2] : (aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) & ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aInteger0(v0) | aInteger0(v1)) & ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aInteger0(v0) | ? [v2] : (sdtasdt0(v1, v2) = v0 & aInteger0(v2))) & ! [v0] : (v0 = all_0_8_8 | v0 = sz10 | ~ aElementOf0(v0, cS2076)) & ! [v0] : (v0 = all_0_8_8 | v0 = sz10 | ~ aInteger0(v0) | ? [v1] : (isPrime0(v1) & aDivisorOf0(v1, v0))) & ! [v0] : ( ~ aSubsetOf0(v0, cS1395) | isOpen0(v0) | ? [v1] : (aElementOf0(v1, v0) & ! [v2] : ! [v3] : (v2 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v1, v2) = v3) | ~ aSubsetOf0(v3, v0) | ~ aInteger0(v2)))) & ! [v0] : ( ~ aElementOf0(v0, all_0_5_5) | aElementOf0(v0, cS2076)) & ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | ~ aElementOf0(v0, cS2076)) & ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | aInteger0(v0)) & ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | ? [v1] : (aElementOf0(v1, xS) & aElementOf0(v0, v1))) & ! [v0] : ( ~ aElementOf0(v0, cS2076) | aInteger0(v0)) & ! [v0] : ( ~ aElementOf0(v0, xS) | ? [v1] : ( ~ (v1 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0 & aSet0(v0) & isPrime0(v1) & aInteger0(v1) & ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v4) = v3) | ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aInteger0(v4) | ~ aInteger0(v2) | aElementOf0(v2, v0)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | sdteqdtlpzmzozddtrp0(v2, sz00, v1)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | aDivisorOf0(v1, v3)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | aInteger0(v2)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | ? [v4] : (sdtasdt0(v1, v4) = v3 & aInteger0(v4))) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ sdteqdtlpzmzozddtrp0(v2, sz00, v1) | ~ aInteger0(v2) | aElementOf0(v2, v0)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aDivisorOf0(v1, v3) | ~ aInteger0(v2) | aElementOf0(v2, v0)))) & ! [v0] : ( ~ isPrime0(v0) | ~ aDivisorOf0(v0, all_0_8_8) | ~ aInteger0(all_0_8_8)) & ! [v0] : ( ~ isPrime0(v0) | ~ aDivisorOf0(v0, sz10)) & ! [v0] : ( ~ aDivisorOf0(sz00, v0) | ~ aInteger0(v0)) & ! [v0] : ( ~ aInteger0(v0) | aElementOf0(v0, all_0_6_6) | aElementOf0(v0, cS2076)) & (( ~ aElementOf0(all_0_1_1, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_1_1, sz10, xp) & ~ aDivisorOf0(xp, all_0_0_0) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_0_0) & sdtasdt0(xp, v0) = v1))) | ( ~ aElementOf0(all_0_4_4, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_4_4, sz10, xp) & ~ aDivisorOf0(xp, all_0_3_3) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_3_3) & sdtasdt0(xp, v0) = v1)))) % 12.48/3.59 | % 12.48/3.59 | Applying alpha-rule on (1) yields: % 12.48/3.59 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(xp, v2) = v1) | ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aInteger0(v2) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) % 12.48/3.59 | (3) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ isClosed0(v1) | ~ isClosed0(v0) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | isClosed0(v2)) % 12.48/3.59 | (4) ! [v0] : ( ~ isPrime0(v0) | ~ aDivisorOf0(v0, sz10)) % 12.48/3.59 | (5) stldt0(all_0_6_6) = cS2076 % 12.48/3.59 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v1)) % 12.48/3.60 | (7) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) % 12.48/3.60 | (8) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aElementOf0(v0, cS2076) | ? [v2] : ? [v3] : ( ~ (v2 = sz00) & szAzrzSzezqlpdtcmdtrp0(v0, v2) = v3 & aSubsetOf0(v3, cS2076) & aSet0(v3) & aInteger0(v2) & ! [v4] : ! [v5] : ! [v6] : ( ~ (sdtasdt0(v2, v6) = v5) | ~ (sdtpldt0(v4, v1) = v5) | ~ aInteger0(v6) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | sdteqdtlpzmzozddtrp0(v4, v0, v2)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | aDivisorOf0(v2, v5)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | aInteger0(v4)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aElementOf0(v4, v3) | ? [v6] : (sdtasdt0(v2, v6) = v5 & aInteger0(v6))) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ sdteqdtlpzmzozddtrp0(v4, v0, v2) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ! [v5] : ( ~ (sdtpldt0(v4, v1) = v5) | ~ aDivisorOf0(v2, v5) | ~ aInteger0(v4) | aElementOf0(v4, v3)) & ! [v4] : ( ~ aElementOf0(v4, v3) | aElementOf0(v4, cS2076)))) % 12.48/3.60 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v2, v1) | aInteger0(v2)) % 12.48/3.60 | (10) ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | aInteger0(v0)) % 12.48/3.60 | (11) aElementOf0(sz10, cS2076) % 12.48/3.60 | (12) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(v0, sz00) = v1) | ~ aInteger0(v0)) % 12.48/3.60 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aInteger0(v3)) % 12.48/3.60 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aSubsetOf0(v2, cS1395)) % 12.48/3.60 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | isClosed0(v2)) % 12.48/3.60 | (16) sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3 % 12.48/3.60 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v1, v0) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtasdt0(v0, v1) = v2) % 12.48/3.60 | (18) aSet0(xS) % 12.48/3.60 | (19) ! [v0] : ( ~ aElementOf0(v0, cS2076) | aInteger0(v0)) % 12.48/3.60 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtbsmnsldt0(v3, v2) = v1) | ~ (sdtbsmnsldt0(v3, v2) = v0)) % 12.48/3.60 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ sdteqdtlpzmzozddtrp0(v3, v0, v1) | ~ aInteger0(v3) | ~ aInteger0(v1) | ~ aInteger0(v0) | aElementOf0(v3, v2)) % 12.48/3.60 | (22) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | aInteger0(v0)) % 12.48/3.60 | (23) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ sdteqdtlpzmzozddtrp0(v3, sz00, v1) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) % 12.48/3.60 | (24) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aSet0(v2)) % 12.48/3.60 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v2) = v3) | ~ (sdtasdt0(v0, v3) = v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtasdt0(v5, v2) = v4 & sdtasdt0(v0, v1) = v5)) % 12.48/3.60 | (26) ! [v0] : ( ~ aInteger0(v0) | aElementOf0(v0, all_0_6_6) | aElementOf0(v0, cS2076)) % 12.48/3.60 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v0, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v6) = v5 & sdtpldt0(v4, v9) = v8 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v7)) % 12.48/3.60 | (28) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(v0, sz10) = v1) | ~ aInteger0(v0)) % 12.48/3.60 | (29) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | ? [v5] : (sdtasdt0(v1, v5) = v4 & aInteger0(v5))) % 12.48/3.60 | (30) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz00) = v1) | ~ aInteger0(v0) | sdtasdt0(sz00, v0) = sz00) % 12.48/3.60 | (31) isClosed0(all_0_6_6) % 12.48/3.60 | (32) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | sdteqdtlpzmzozddtrp0(v3, sz00, v1)) % 12.48/3.61 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = sz00 | v2 = sz00 | ~ (sdtasdt0(v2, v3) = v4) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) % 12.48/3.61 | (34) aSet0(all_0_5_5) % 12.48/3.61 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v2)) % 12.48/3.61 | (36) aSet0(all_0_6_6) % 12.48/3.61 | (37) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (stldt0(v2) = v1) | ~ (stldt0(v2) = v0)) % 12.48/3.61 | (38) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | aInteger0(v1)) % 12.48/3.61 | (39) ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v0) | aSet0(v1) | ? [v2] : (aElementOf0(v2, v0) & ~ aSubsetOf0(v2, cS1395))) % 12.48/3.61 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v0)) % 12.48/3.61 | (41) ! [v0] : ! [v1] : ( ~ (sdtpldt0(sz00, v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v0, sz00) = v0) % 12.48/3.61 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v1) | ~ aInteger0(v3) | aElementOf0(v3, v2)) % 12.48/3.61 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v1, v0) = sz00) % 12.48/3.61 | (44) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtasdt0(v1, v5) = v4) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ aInteger0(v5) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) % 12.48/3.61 | (45) ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ isClosed0(v0) | ~ aSubsetOf0(v0, cS1395) | isOpen0(v1)) % 12.48/3.61 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aInteger0(v3)) % 12.48/3.61 | (47) ! [v0] : ! [v1] : ( ~ aElementOf0(v1, xS) | ~ aElementOf0(v0, v1) | ~ aInteger0(v0) | aElementOf0(v0, all_0_6_6)) % 12.48/3.61 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtpldt0(v1, v2) = v5 & sdtpldt0(v0, v5) = v4)) % 12.48/3.61 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v2, v1) | ~ aElementOf0(v2, v0)) % 12.48/3.61 | (50) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ isOpen0(v1) | ~ isOpen0(v0) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | isOpen0(v2)) % 12.48/3.61 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) % 12.48/3.61 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtpldt0(v1, v2) = v3) | ~ (sdtpldt0(v0, v3) = v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtpldt0(v5, v2) = v4 & sdtpldt0(v0, v1) = v5)) % 12.48/3.61 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v1) | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v0)) % 12.48/3.61 | (54) sdtpldt0(sz10, all_0_2_2) = all_0_1_1 % 12.48/3.61 | (55) ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | ~ aElementOf0(v0, cS2076)) % 12.48/3.61 | (56) ! [v0] : (v0 = all_0_8_8 | v0 = sz10 | ~ aElementOf0(v0, cS2076)) % 12.48/3.61 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v2) | aElementOf0(v3, v1) | aElementOf0(v3, v0)) % 12.48/3.62 | (58) ! [v0] : ! [v1] : ( ~ isOpen0(v0) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v1, v0) | ? [v2] : ? [v3] : ( ~ (v2 = sz00) & szAzrzSzezqlpdtcmdtrp0(v1, v2) = v3 & aSubsetOf0(v3, v0) & aInteger0(v2))) % 12.48/3.62 | (59) ! [v0] : ( ~ aElementOf0(v0, all_0_6_6) | ? [v1] : (aElementOf0(v1, xS) & aElementOf0(v0, v1))) % 12.48/3.62 | (60) ! [v0] : ( ~ aElementOf0(v0, xS) | ? [v1] : ( ~ (v1 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0 & aSet0(v0) & isPrime0(v1) & aInteger0(v1) & ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v1, v4) = v3) | ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aInteger0(v4) | ~ aInteger0(v2) | aElementOf0(v2, v0)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | sdteqdtlpzmzozddtrp0(v2, sz00, v1)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | aDivisorOf0(v1, v3)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | aInteger0(v2)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aElementOf0(v2, v0) | ? [v4] : (sdtasdt0(v1, v4) = v3 & aInteger0(v4))) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ sdteqdtlpzmzozddtrp0(v2, sz00, v1) | ~ aInteger0(v2) | aElementOf0(v2, v0)) & ! [v2] : ! [v3] : ( ~ (sdtpldt0(v2, all_0_7_7) = v3) | ~ aDivisorOf0(v1, v3) | ~ aInteger0(v2) | aElementOf0(v2, v0)))) % 12.48/3.62 | (61) ( ~ aElementOf0(all_0_1_1, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_1_1, sz10, xp) & ~ aDivisorOf0(xp, all_0_0_0) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_0_0) & sdtasdt0(xp, v0) = v1))) | ( ~ aElementOf0(all_0_4_4, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_4_4, sz10, xp) & ~ aDivisorOf0(xp, all_0_3_3) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_3_3) & sdtasdt0(xp, v0) = v1))) % 12.48/3.62 | (62) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | ? [v2] : (sdtasdt0(xp, v2) = v1 & aInteger0(v2))) % 12.48/3.62 | (63) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtpldt0(v0, v1) = v2) % 12.48/3.62 | (64) aInteger0(sz00) % 12.48/3.62 | (65) ! [v0] : ! [v1] : ( ~ (sdtasdt0(all_0_8_8, v0) = v1) | ~ aInteger0(v0) | (sdtasdt0(v0, all_0_8_8) = v1 & smndt0(v0) = v1)) % 12.48/3.62 | (66) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, all_0_8_8) = v1) | ~ aInteger0(v0) | (sdtasdt0(all_0_8_8, v0) = v1 & smndt0(v0) = v1)) % 12.48/3.62 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aSet0(v3) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ sdteqdtlpzmzozddtrp0(v4, v0, v1) | ~ aInteger0(v4)) & (aElementOf0(v4, v3) | (sdteqdtlpzmzozddtrp0(v4, v0, v1) & aInteger0(v4))))) % 12.48/3.62 | (68) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ isPrime0(v1) | ~ aDivisorOf0(v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v1) | aElementOf0(v3, v2) | aElementOf0(v0, xS)) % 12.48/3.62 | (69) aInteger0(xp) % 12.48/3.62 | (70) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v3, v0) | ~ aElementOf0(v2, v3) | ~ aSet0(v0) | ~ aInteger0(v2) | aElementOf0(v2, v1) | ? [v4] : (aElementOf0(v4, v0) & ~ aSubsetOf0(v4, cS1395))) % 12.48/3.62 | (71) smndt0(sz00) = all_0_7_7 % 12.48/3.62 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v3, v0, v1)) % 12.48/3.62 | (73) sdtpldt0(sz10, xp) = all_0_4_4 % 12.48/3.62 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v1) | ~ aElementOf0(v3, v0) | ~ aInteger0(v3) | aElementOf0(v3, v2)) % 12.48/3.62 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v3) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aElementOf0(v4, v1) | ~ aElementOf0(v4, v0) | ~ aInteger0(v4)) & (aElementOf0(v4, v3) | (aElementOf0(v4, v1) & aElementOf0(v4, v0) & aInteger0(v4))))) % 12.48/3.62 | (76) ! [v0] : ! [v1] : (v1 = sz00 | v0 = sz00 | ~ (sdtasdt0(v0, v1) = sz00) | ~ aInteger0(v1) | ~ aInteger0(v0)) % 12.48/3.62 | (77) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v1, v0, v2)) % 12.48/3.62 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (sbsmnsldt0(v2) = v1) | ~ (sbsmnsldt0(v2) = v0)) % 12.48/3.62 | (79) szAzrzSzezqlpdtcmdtrp0(sz10, xp) = all_0_5_5 % 12.48/3.62 | (80) ? [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aSet0(v2)) % 12.48/3.62 | (81) ! [v0] : ! [v1] : ! [v2] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aInteger0(v2) | ? [v3] : (aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395))) % 12.48/3.62 | (82) aSubsetOf0(all_0_5_5, cS2076) % 12.48/3.62 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | aSet0(v2)) % 12.48/3.62 | (84) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | sdtpldt0(v0, v1) = sz00) % 12.48/3.62 | (85) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, sz00) = v1) | ~ aInteger0(v0) | sdtpldt0(sz00, v0) = v0) % 12.48/3.62 | (86) ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ isOpen0(v1) | ~ aSubsetOf0(v0, cS1395) | isClosed0(v0)) % 12.48/3.62 | (87) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(sz00, v0) = v1) | ~ aInteger0(v0)) % 12.48/3.62 | (88) ! [v0] : ! [v1] : ( ~ aSubsetOf0(v1, v0) | ~ aSet0(v0) | aSet0(v1)) % 12.48/3.62 | (89) sbsmnsldt0(xS) = all_0_6_6 % 12.48/3.62 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtpldt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v5) = v6 & sdtasdt0(v0, v2) = v8 & sdtasdt0(v0, v1) = v7 & sdtpldt0(v8, v9) = v4 & sdtpldt0(v7, v8) = v6 & sdtpldt0(v1, v2) = v5)) % 12.48/3.63 | (91) isFinite0(xS) % 12.48/3.63 | (92) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtpldt0(v0, sz00) = v1) | ~ aInteger0(v0)) % 12.48/3.63 | (93) cS2043 = xS % 12.48/3.63 | (94) aInteger0(sz10) % 12.48/3.63 | (95) ! [v0] : ! [v1] : (v1 = v0 | ~ (sdtasdt0(sz10, v0) = v1) | ~ aInteger0(v0)) % 12.48/3.63 | (96) ! [v0] : ! [v1] : ( ~ (sdtasdt0(v0, sz10) = v1) | ~ aInteger0(v0) | sdtasdt0(sz10, v0) = v0) % 12.48/3.63 | (97) ! [v0] : ! [v1] : ! [v2] : ( ~ aSubsetOf0(v1, v0) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | aElementOf0(v2, v0)) % 12.48/3.63 | (98) ! [v0] : ! [v1] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | aSet0(v1)) % 12.48/3.63 | (99) ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v0) | isOpen0(v1) | ? [v2] : (aElementOf0(v2, v0) & ( ~ isOpen0(v2) | ~ aSubsetOf0(v2, cS1395)))) % 12.48/3.63 | (100) ! [v0] : ( ~ aDivisorOf0(sz00, v0) | ~ aInteger0(v0)) % 12.48/3.63 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ aElementOf0(v3, v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v3)) % 12.48/3.63 | (102) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ sdteqdtlpzmzozddtrp0(v0, sz10, xp) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) % 12.48/3.63 | (103) ! [v0] : ( ~ aSubsetOf0(v0, cS1395) | isOpen0(v0) | ? [v1] : (aElementOf0(v1, v0) & ! [v2] : ! [v3] : (v2 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v1, v2) = v3) | ~ aSubsetOf0(v3, v0) | ~ aInteger0(v2)))) % 12.48/3.63 | (104) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtpldt0(v1, v0) = v2) % 12.48/3.63 | (105) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz10, v0) = v1) | ~ aInteger0(v0) | sdtasdt0(v0, sz10) = v0) % 13.05/3.63 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v3, v2) = v4) | ~ (sdtasdt0(v0, v1) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : (sdtasdt0(v1, v2) = v5 & sdtasdt0(v0, v5) = v4)) % 13.05/3.63 | (107) ! [v0] : ! [v1] : ( ~ (smndt0(v0) = v1) | ~ aInteger0(v0) | (sdtasdt0(v0, all_0_8_8) = v1 & sdtasdt0(all_0_8_8, v0) = v1)) % 13.05/3.63 | (108) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | aDivisorOf0(xp, v1)) % 13.05/3.63 | (109) ! [v0] : ! [v1] : ! [v2] : (v1 = sz00 | ~ (sdtasdt0(v1, v2) = v0) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aDivisorOf0(v1, v0)) % 13.05/3.63 | (110) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = sz00 | ~ sdteqdtlpzmzozddtrp0(v1, v3, v2) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v3, v2)) % 13.05/3.63 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aElementOf0(v3, v0) | ~ aInteger0(v3) | aElementOf0(v3, v2)) % 13.05/3.63 | (112) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (sdtasdt0(v1, v2) = v4) | ~ (sdtasdt0(v0, v2) = v3) | ~ (sdtpldt0(v3, v4) = v5) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v9, v2) = v5 & sdtasdt0(v0, v6) = v7 & sdtasdt0(v0, v1) = v8 & sdtpldt0(v8, v3) = v7 & sdtpldt0(v1, v2) = v6 & sdtpldt0(v0, v1) = v9)) % 13.05/3.63 | (113) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v0, v1) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0)) % 13.05/3.63 | (114) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = sz00 | ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ aDivisorOf0(v2, v4) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v2)) % 13.05/3.63 | (115) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtslmnbsdt0(v3, v2) = v1) | ~ (sdtslmnbsdt0(v3, v2) = v0)) % 13.05/3.63 | (116) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = sz00 | v2 = sz00 | ~ (sdtasdt0(v2, v3) = v4) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v4) | ~ aInteger0(v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v1, v3)) % 13.05/3.63 | (117) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (sbsmnsldt0(v0) = v1) | ~ aSet0(v2) | ~ aSet0(v0) | ? [v3] : ? [v4] : ((aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395)) | (( ~ aElementOf0(v3, v2) | ~ aInteger0(v3) | ! [v5] : ( ~ aElementOf0(v5, v0) | ~ aElementOf0(v3, v5))) & (aElementOf0(v3, v2) | (aElementOf0(v4, v0) & aElementOf0(v3, v4) & aInteger0(v3)))))) % 13.05/3.63 | (118) ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aInteger0(v0) | aInteger0(v1)) % 13.05/3.63 | (119) smndt0(sz10) = all_0_8_8 % 13.05/3.63 | (120) ! [v0] : ( ~ isPrime0(v0) | ~ aDivisorOf0(v0, all_0_8_8) | ~ aInteger0(all_0_8_8)) % 13.05/3.63 | (121) ! [v0] : ! [v1] : ( ~ (sdtasdt0(sz00, v0) = v1) | ~ aInteger0(v0) | sdtasdt0(v0, sz00) = sz00) % 13.05/3.63 | (122) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtslmnbsdt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | aSet0(v2)) % 13.05/3.63 | (123) ! [v0] : ! [v1] : ! [v2] : (v2 = sz00 | ~ (sdtpldt0(v1, v0) = v2) | ~ (smndt0(v0) = v1) | ~ aInteger0(v0)) % 13.05/3.63 | (124) aSet0(cS2076) % 13.05/3.63 | (125) ! [v0] : ( ~ aElementOf0(v0, all_0_5_5) | aElementOf0(v0, cS2076)) % 13.05/3.63 | (126) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (sdtasdt0(v0, v3) = v4) | ~ (sdtpldt0(v1, v2) = v3) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (sdtasdt0(v7, v2) = v8 & sdtasdt0(v1, v2) = v9 & sdtasdt0(v0, v2) = v6 & sdtasdt0(v0, v1) = v5 & sdtpldt0(v6, v9) = v8 & sdtpldt0(v5, v6) = v4 & sdtpldt0(v0, v1) = v7)) % 13.05/3.63 | (127) ! [v0] : ! [v1] : ! [v2] : ( ~ (sbsmnsldt0(v0) = v1) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | ? [v3] : ((aElementOf0(v3, v0) & aElementOf0(v2, v3)) | (aElementOf0(v3, v0) & ~ aSubsetOf0(v3, cS1395)))) % 13.05/3.63 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | ~ (sdtpldt0(v3, v2) = v0)) % 13.05/3.63 | (129) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = sz00 | ~ (sdtpldt0(v0, v3) = v4) | ~ (smndt0(v1) = v3) | ~ sdteqdtlpzmzozddtrp0(v0, v1, v2) | ~ aInteger0(v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aDivisorOf0(v2, v4)) % 13.05/3.63 | (130) sdtpldt0(all_0_1_1, all_0_8_8) = all_0_0_0 % 13.05/3.63 | (131) ! [v0] : ! [v1] : (v1 = sz00 | ~ aInteger0(v1) | ~ aInteger0(v0) | sdteqdtlpzmzozddtrp0(v0, v0, v1)) % 13.05/3.63 | (132) smndt0(xp) = all_0_2_2 % 13.05/3.63 | (133) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aDivisorOf0(xp, v1) | ~ aInteger0(v0) | aElementOf0(v0, all_0_5_5)) % 13.05/3.63 | (134) ! [v0] : ! [v1] : (v1 = sz00 | ~ (sdtasdt0(sz00, v0) = v1) | ~ aInteger0(v0)) % 13.05/3.63 | (135) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aInteger0(v3)) % 13.05/3.64 | (136) ! [v0] : ! [v1] : ( ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v1, v0) | ? [v2] : (aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) % 13.05/3.64 | (137) ! [v0] : (v0 = all_0_8_8 | v0 = sz10 | ~ aInteger0(v0) | ? [v1] : (isPrime0(v1) & aDivisorOf0(v1, v0))) % 13.05/3.64 | (138) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v2) | ~ (sdtpldt0(v3, all_0_7_7) = v4) | ~ aElementOf0(v3, v2) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS) | aDivisorOf0(v1, v4)) % 13.05/3.64 | (139) ~ (xp = sz00) % 13.05/3.64 | (140) ! [v0] : ! [v1] : ( ~ aDivisorOf0(v1, v0) | ~ aInteger0(v0) | ? [v2] : (sdtasdt0(v1, v2) = v0 & aInteger0(v2))) % 13.05/3.64 | (141) ! [v0] : ! [v1] : ! [v2] : ( ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aInteger0(v2) | aElementOf0(v2, v1) | aElementOf0(v2, v0)) % 13.05/3.64 | (142) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (sdtbsmnsldt0(v0, v1) = v2) | ~ aSubsetOf0(v1, cS1395) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v3) | ? [v4] : (( ~ aElementOf0(v4, v3) | ~ aInteger0(v4) | ( ~ aElementOf0(v4, v1) & ~ aElementOf0(v4, v0))) & (aElementOf0(v4, v3) | (aInteger0(v4) & (aElementOf0(v4, v1) | aElementOf0(v4, v0)))))) % 13.05/3.64 | (143) aElementOf0(all_0_8_8, cS2076) % 13.05/3.64 | (144) ! [v0] : ! [v1] : ( ~ (sbsmnsldt0(v0) = v1) | ~ isFinite0(v0) | ~ aSet0(v0) | isClosed0(v1) | ? [v2] : (aElementOf0(v2, v0) & ( ~ isClosed0(v2) | ~ aSubsetOf0(v2, cS1395)))) % 13.05/3.64 | (145) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtpldt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | aInteger0(v2)) % 13.05/3.64 | (146) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (stldt0(v0) = v1) | ~ aSubsetOf0(v0, cS1395) | ~ aSet0(v2) | ? [v3] : (( ~ aElementOf0(v3, v2) | ~ aInteger0(v3) | aElementOf0(v3, v0)) & (aElementOf0(v3, v2) | (aInteger0(v3) & ~ aElementOf0(v3, v0))))) % 13.05/3.64 | (147) ! [v0] : ! [v1] : (v1 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0) | ~ isPrime0(v1) | ~ aInteger0(v1) | aElementOf0(v0, xS)) % 13.05/3.64 | (148) ! [v0] : ! [v1] : ( ~ (sdtpldt0(v0, all_0_8_8) = v1) | ~ aElementOf0(v0, all_0_5_5) | sdteqdtlpzmzozddtrp0(v0, sz10, xp)) % 13.05/3.64 | (149) ! [v0] : ! [v1] : ! [v2] : ( ~ (sdtasdt0(v0, v1) = v2) | ~ aInteger0(v1) | ~ aInteger0(v0) | sdtasdt0(v1, v0) = v2) % 13.05/3.64 | (150) isOpen0(cS2076) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (38) with all_0_2_2, xp and discharging atoms smndt0(xp) = all_0_2_2, aInteger0(xp), yields: % 13.05/3.64 | (151) aInteger0(all_0_2_2) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (107) with all_0_2_2, xp and discharging atoms smndt0(xp) = all_0_2_2, aInteger0(xp), yields: % 13.05/3.64 | (152) sdtasdt0(all_0_8_8, xp) = all_0_2_2 & sdtasdt0(xp, all_0_8_8) = all_0_2_2 % 13.05/3.64 | % 13.05/3.64 | Applying alpha-rule on (152) yields: % 13.05/3.64 | (153) sdtasdt0(all_0_8_8, xp) = all_0_2_2 % 13.05/3.64 | (154) sdtasdt0(xp, all_0_8_8) = all_0_2_2 % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (63) with all_0_4_4, sz10, xp and discharging atoms sdtpldt0(sz10, xp) = all_0_4_4, aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (155) sdtpldt0(xp, sz10) = all_0_4_4 % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (145) with all_0_4_4, xp, sz10 and discharging atoms sdtpldt0(sz10, xp) = all_0_4_4, aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (156) aInteger0(all_0_4_4) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (38) with all_0_8_8, sz10 and discharging atoms smndt0(sz10) = all_0_8_8, aInteger0(sz10), yields: % 13.05/3.64 | (157) aInteger0(all_0_8_8) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (107) with all_0_8_8, sz10 and discharging atoms smndt0(sz10) = all_0_8_8, aInteger0(sz10), yields: % 13.05/3.64 | (158) sdtasdt0(all_0_8_8, sz10) = all_0_8_8 & sdtasdt0(sz10, all_0_8_8) = all_0_8_8 % 13.05/3.64 | % 13.05/3.64 | Applying alpha-rule on (158) yields: % 13.05/3.64 | (159) sdtasdt0(all_0_8_8, sz10) = all_0_8_8 % 13.05/3.64 | (160) sdtasdt0(sz10, all_0_8_8) = all_0_8_8 % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (38) with all_0_7_7, sz00 and discharging atoms smndt0(sz00) = all_0_7_7, aInteger0(sz00), yields: % 13.05/3.64 | (161) aInteger0(all_0_7_7) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (107) with all_0_7_7, sz00 and discharging atoms smndt0(sz00) = all_0_7_7, aInteger0(sz00), yields: % 13.05/3.64 | (162) sdtasdt0(all_0_8_8, sz00) = all_0_7_7 & sdtasdt0(sz00, all_0_8_8) = all_0_7_7 % 13.05/3.64 | % 13.05/3.64 | Applying alpha-rule on (162) yields: % 13.05/3.64 | (163) sdtasdt0(all_0_8_8, sz00) = all_0_7_7 % 13.05/3.64 | (164) sdtasdt0(sz00, all_0_8_8) = all_0_7_7 % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (134) with all_0_7_7, all_0_8_8 and discharging atoms sdtasdt0(sz00, all_0_8_8) = all_0_7_7, aInteger0(all_0_8_8), yields: % 13.05/3.64 | (165) all_0_7_7 = sz00 % 13.05/3.64 | % 13.05/3.64 | From (165) and (161) follows: % 13.05/3.64 | (64) aInteger0(sz00) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (63) with all_0_1_1, sz10, all_0_2_2 and discharging atoms sdtpldt0(sz10, all_0_2_2) = all_0_1_1, aInteger0(all_0_2_2), aInteger0(sz10), yields: % 13.05/3.64 | (167) sdtpldt0(all_0_2_2, sz10) = all_0_1_1 % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (106) with all_0_2_2, all_0_8_8, xp, sz10, all_0_8_8 and discharging atoms sdtasdt0(all_0_8_8, xp) = all_0_2_2, sdtasdt0(all_0_8_8, sz10) = all_0_8_8, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (168) ? [v0] : (sdtasdt0(all_0_8_8, v0) = all_0_2_2 & sdtasdt0(sz10, xp) = v0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (106) with all_0_2_2, all_0_8_8, xp, all_0_8_8, sz10 and discharging atoms sdtasdt0(all_0_8_8, xp) = all_0_2_2, sdtasdt0(sz10, all_0_8_8) = all_0_8_8, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (169) ? [v0] : (sdtasdt0(all_0_8_8, xp) = v0 & sdtasdt0(sz10, v0) = all_0_2_2) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (106) with all_0_8_8, all_0_8_8, sz10, sz10, all_0_8_8 and discharging atoms sdtasdt0(all_0_8_8, sz10) = all_0_8_8, aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.64 | (170) ? [v0] : (sdtasdt0(all_0_8_8, v0) = all_0_8_8 & sdtasdt0(sz10, sz10) = v0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (25) with all_0_2_2, all_0_8_8, sz10, all_0_8_8, xp and discharging atoms sdtasdt0(all_0_8_8, sz10) = all_0_8_8, sdtasdt0(xp, all_0_8_8) = all_0_2_2, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (171) ? [v0] : (sdtasdt0(v0, sz10) = all_0_2_2 & sdtasdt0(xp, all_0_8_8) = v0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (25) with all_0_2_2, all_0_8_8, all_0_8_8, sz10, xp and discharging atoms sdtasdt0(xp, all_0_8_8) = all_0_2_2, sdtasdt0(sz10, all_0_8_8) = all_0_8_8, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (172) ? [v0] : (sdtasdt0(v0, all_0_8_8) = all_0_2_2 & sdtasdt0(xp, sz10) = v0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (25) with all_0_8_8, all_0_8_8, all_0_8_8, sz10, sz10 and discharging atoms sdtasdt0(sz10, all_0_8_8) = all_0_8_8, aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.64 | (173) ? [v0] : (sdtasdt0(v0, all_0_8_8) = all_0_8_8 & sdtasdt0(sz10, sz10) = v0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (48) with all_0_0_0, all_0_1_1, all_0_8_8, all_0_2_2, sz10 and discharging atoms sdtpldt0(all_0_1_1, all_0_8_8) = all_0_0_0, sdtpldt0(sz10, all_0_2_2) = all_0_1_1, aInteger0(all_0_2_2), aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.64 | (174) ? [v0] : (sdtpldt0(all_0_2_2, all_0_8_8) = v0 & sdtpldt0(sz10, v0) = all_0_0_0) % 13.05/3.64 | % 13.05/3.64 | Instantiating formula (48) with all_0_3_3, all_0_4_4, all_0_8_8, xp, sz10 and discharging atoms sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3, sdtpldt0(sz10, xp) = all_0_4_4, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.64 | (175) ? [v0] : (sdtpldt0(xp, all_0_8_8) = v0 & sdtpldt0(sz10, v0) = all_0_3_3) % 13.05/3.64 | % 13.05/3.65 | Instantiating formula (48) with all_0_3_3, all_0_4_4, all_0_8_8, sz10, xp and discharging atoms sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3, sdtpldt0(xp, sz10) = all_0_4_4, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.65 | (176) ? [v0] : (sdtpldt0(xp, v0) = all_0_3_3 & sdtpldt0(sz10, all_0_8_8) = v0) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (63) with all_0_3_3, all_0_4_4, all_0_8_8 and discharging atoms sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3, aInteger0(all_0_4_4), aInteger0(all_0_8_8), yields: % 13.05/3.65 | (177) sdtpldt0(all_0_8_8, all_0_4_4) = all_0_3_3 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (145) with all_0_3_3, all_0_8_8, all_0_4_4 and discharging atoms sdtpldt0(all_0_4_4, all_0_8_8) = all_0_3_3, aInteger0(all_0_4_4), aInteger0(all_0_8_8), yields: % 13.05/3.65 | (178) aInteger0(all_0_3_3) % 13.05/3.65 | % 13.05/3.65 | Instantiating (176) with all_58_0_19 yields: % 13.05/3.65 | (179) sdtpldt0(xp, all_58_0_19) = all_0_3_3 & sdtpldt0(sz10, all_0_8_8) = all_58_0_19 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (179) yields: % 13.05/3.65 | (180) sdtpldt0(xp, all_58_0_19) = all_0_3_3 % 13.05/3.65 | (181) sdtpldt0(sz10, all_0_8_8) = all_58_0_19 % 13.05/3.65 | % 13.05/3.65 | Instantiating (174) with all_60_0_20 yields: % 13.05/3.65 | (182) sdtpldt0(all_0_2_2, all_0_8_8) = all_60_0_20 & sdtpldt0(sz10, all_60_0_20) = all_0_0_0 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (182) yields: % 13.05/3.65 | (183) sdtpldt0(all_0_2_2, all_0_8_8) = all_60_0_20 % 13.05/3.65 | (184) sdtpldt0(sz10, all_60_0_20) = all_0_0_0 % 13.05/3.65 | % 13.05/3.65 | Instantiating (175) with all_66_0_23 yields: % 13.05/3.65 | (185) sdtpldt0(xp, all_0_8_8) = all_66_0_23 & sdtpldt0(sz10, all_66_0_23) = all_0_3_3 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (185) yields: % 13.05/3.65 | (186) sdtpldt0(xp, all_0_8_8) = all_66_0_23 % 13.05/3.65 | (187) sdtpldt0(sz10, all_66_0_23) = all_0_3_3 % 13.05/3.65 | % 13.05/3.65 | Instantiating (173) with all_68_0_24 yields: % 13.05/3.65 | (188) sdtasdt0(all_68_0_24, all_0_8_8) = all_0_8_8 & sdtasdt0(sz10, sz10) = all_68_0_24 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (188) yields: % 13.05/3.65 | (189) sdtasdt0(all_68_0_24, all_0_8_8) = all_0_8_8 % 13.05/3.65 | (190) sdtasdt0(sz10, sz10) = all_68_0_24 % 13.05/3.65 | % 13.05/3.65 | Instantiating (172) with all_70_0_25 yields: % 13.05/3.65 | (191) sdtasdt0(all_70_0_25, all_0_8_8) = all_0_2_2 & sdtasdt0(xp, sz10) = all_70_0_25 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (191) yields: % 13.05/3.65 | (192) sdtasdt0(all_70_0_25, all_0_8_8) = all_0_2_2 % 13.05/3.65 | (193) sdtasdt0(xp, sz10) = all_70_0_25 % 13.05/3.65 | % 13.05/3.65 | Instantiating (170) with all_80_0_30 yields: % 13.05/3.65 | (194) sdtasdt0(all_0_8_8, all_80_0_30) = all_0_8_8 & sdtasdt0(sz10, sz10) = all_80_0_30 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (194) yields: % 13.05/3.65 | (195) sdtasdt0(all_0_8_8, all_80_0_30) = all_0_8_8 % 13.05/3.65 | (196) sdtasdt0(sz10, sz10) = all_80_0_30 % 13.05/3.65 | % 13.05/3.65 | Instantiating (171) with all_82_0_31 yields: % 13.05/3.65 | (197) sdtasdt0(all_82_0_31, sz10) = all_0_2_2 & sdtasdt0(xp, all_0_8_8) = all_82_0_31 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (197) yields: % 13.05/3.65 | (198) sdtasdt0(all_82_0_31, sz10) = all_0_2_2 % 13.05/3.65 | (199) sdtasdt0(xp, all_0_8_8) = all_82_0_31 % 13.05/3.65 | % 13.05/3.65 | Instantiating (169) with all_84_0_32 yields: % 13.05/3.65 | (200) sdtasdt0(all_0_8_8, xp) = all_84_0_32 & sdtasdt0(sz10, all_84_0_32) = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (200) yields: % 13.05/3.65 | (201) sdtasdt0(all_0_8_8, xp) = all_84_0_32 % 13.05/3.65 | (202) sdtasdt0(sz10, all_84_0_32) = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | Instantiating (168) with all_86_0_33 yields: % 13.05/3.65 | (203) sdtasdt0(all_0_8_8, all_86_0_33) = all_0_2_2 & sdtasdt0(sz10, xp) = all_86_0_33 % 13.05/3.65 | % 13.05/3.65 | Applying alpha-rule on (203) yields: % 13.05/3.65 | (204) sdtasdt0(all_0_8_8, all_86_0_33) = all_0_2_2 % 13.05/3.65 | (205) sdtasdt0(sz10, xp) = all_86_0_33 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (51) with all_0_8_8, xp, all_84_0_32, all_0_2_2 and discharging atoms sdtasdt0(all_0_8_8, xp) = all_84_0_32, sdtasdt0(all_0_8_8, xp) = all_0_2_2, yields: % 13.05/3.65 | (206) all_84_0_32 = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (51) with xp, all_0_8_8, all_82_0_31, all_0_2_2 and discharging atoms sdtasdt0(xp, all_0_8_8) = all_82_0_31, sdtasdt0(xp, all_0_8_8) = all_0_2_2, yields: % 13.05/3.65 | (207) all_82_0_31 = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (28) with all_70_0_25, xp and discharging atoms sdtasdt0(xp, sz10) = all_70_0_25, aInteger0(xp), yields: % 13.05/3.65 | (208) all_70_0_25 = xp % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (95) with all_86_0_33, xp and discharging atoms sdtasdt0(sz10, xp) = all_86_0_33, aInteger0(xp), yields: % 13.05/3.65 | (209) all_86_0_33 = xp % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (28) with all_80_0_30, sz10 and discharging atoms sdtasdt0(sz10, sz10) = all_80_0_30, aInteger0(sz10), yields: % 13.05/3.65 | (210) all_80_0_30 = sz10 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (51) with sz10, sz10, all_68_0_24, all_80_0_30 and discharging atoms sdtasdt0(sz10, sz10) = all_80_0_30, sdtasdt0(sz10, sz10) = all_68_0_24, yields: % 13.05/3.65 | (211) all_80_0_30 = all_68_0_24 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (113) with all_58_0_19, all_0_8_8, sz10 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_58_0_19, smndt0(sz10) = all_0_8_8, aInteger0(sz10), yields: % 13.05/3.65 | (212) all_58_0_19 = sz00 % 13.05/3.65 | % 13.05/3.65 | Combining equations (211,210) yields a new equation: % 13.05/3.65 | (213) all_68_0_24 = sz10 % 13.05/3.65 | % 13.05/3.65 | Simplifying 213 yields: % 13.05/3.65 | (214) all_68_0_24 = sz10 % 13.05/3.65 | % 13.05/3.65 | From (214) and (189) follows: % 13.05/3.65 | (160) sdtasdt0(sz10, all_0_8_8) = all_0_8_8 % 13.05/3.65 | % 13.05/3.65 | From (210) and (195) follows: % 13.05/3.65 | (159) sdtasdt0(all_0_8_8, sz10) = all_0_8_8 % 13.05/3.65 | % 13.05/3.65 | From (206) and (201) follows: % 13.05/3.65 | (153) sdtasdt0(all_0_8_8, xp) = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | From (207) and (199) follows: % 13.05/3.65 | (154) sdtasdt0(xp, all_0_8_8) = all_0_2_2 % 13.05/3.65 | % 13.05/3.65 | From (208) and (193) follows: % 13.05/3.65 | (219) sdtasdt0(xp, sz10) = xp % 13.05/3.65 | % 13.05/3.65 | From (209) and (205) follows: % 13.05/3.65 | (220) sdtasdt0(sz10, xp) = xp % 13.05/3.65 | % 13.05/3.65 | From (214) and (190) follows: % 13.05/3.65 | (221) sdtasdt0(sz10, sz10) = sz10 % 13.05/3.65 | % 13.05/3.65 | From (212) and (180) follows: % 13.05/3.65 | (222) sdtpldt0(xp, sz00) = all_0_3_3 % 13.05/3.65 | % 13.05/3.65 | From (212) and (181) follows: % 13.05/3.65 | (223) sdtpldt0(sz10, all_0_8_8) = sz00 % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (92) with all_0_3_3, xp and discharging atoms sdtpldt0(xp, sz00) = all_0_3_3, aInteger0(xp), yields: % 13.05/3.65 | (224) all_0_3_3 = xp % 13.05/3.65 | % 13.05/3.65 | From (224) and (16) follows: % 13.05/3.65 | (225) sdtpldt0(all_0_4_4, all_0_8_8) = xp % 13.05/3.65 | % 13.05/3.65 | From (224) and (177) follows: % 13.05/3.65 | (226) sdtpldt0(all_0_8_8, all_0_4_4) = xp % 13.05/3.65 | % 13.05/3.65 | From (224) and (222) follows: % 13.05/3.65 | (227) sdtpldt0(xp, sz00) = xp % 13.05/3.65 | % 13.05/3.65 | From (224) and (178) follows: % 13.05/3.65 | (69) aInteger0(xp) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (112) with all_60_0_20, all_0_8_8, all_0_2_2, all_0_8_8, sz10, xp and discharging atoms sdtasdt0(xp, all_0_8_8) = all_0_2_2, sdtasdt0(sz10, all_0_8_8) = all_0_8_8, sdtpldt0(all_0_2_2, all_0_8_8) = all_60_0_20, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.65 | (229) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v3, all_0_8_8) = all_60_0_20 & sdtasdt0(xp, v0) = v1 & sdtasdt0(xp, sz10) = v2 & sdtpldt0(v2, all_0_2_2) = v1 & sdtpldt0(xp, sz10) = v3 & sdtpldt0(sz10, all_0_8_8) = v0) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (48) with all_0_0_0, all_0_1_1, all_0_8_8, sz10, all_0_2_2 and discharging atoms sdtpldt0(all_0_1_1, all_0_8_8) = all_0_0_0, sdtpldt0(all_0_2_2, sz10) = all_0_1_1, aInteger0(all_0_2_2), aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.65 | (230) ? [v0] : (sdtpldt0(all_0_2_2, v0) = all_0_0_0 & sdtpldt0(sz10, all_0_8_8) = v0) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (2) with sz10, xp, all_0_4_4 and discharging atoms sdtasdt0(xp, sz10) = xp, sdtpldt0(all_0_4_4, all_0_8_8) = xp, aInteger0(all_0_4_4), aInteger0(sz10), yields: % 13.05/3.65 | (231) aElementOf0(all_0_4_4, all_0_5_5) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (126) with xp, xp, all_0_4_4, all_0_8_8, sz10 and discharging atoms sdtasdt0(sz10, xp) = xp, sdtpldt0(all_0_8_8, all_0_4_4) = xp, aInteger0(all_0_4_4), aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.65 | (232) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(v2, all_0_4_4) = v3 & sdtasdt0(all_0_8_8, all_0_4_4) = v4 & sdtasdt0(sz10, all_0_4_4) = v1 & sdtasdt0(sz10, all_0_8_8) = v0 & sdtpldt0(v1, v4) = v3 & sdtpldt0(v0, v1) = xp & sdtpldt0(sz10, all_0_8_8) = v2) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (52) with all_0_4_4, xp, all_0_4_4, all_0_8_8, sz10 and discharging atoms sdtpldt0(all_0_8_8, all_0_4_4) = xp, sdtpldt0(sz10, xp) = all_0_4_4, aInteger0(all_0_4_4), aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.65 | (233) ? [v0] : (sdtpldt0(v0, all_0_4_4) = all_0_4_4 & sdtpldt0(sz10, all_0_8_8) = v0) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (112) with all_66_0_23, all_0_8_8, xp, sz10, all_0_8_8, xp and discharging atoms sdtasdt0(all_0_8_8, sz10) = all_0_8_8, sdtasdt0(xp, sz10) = xp, sdtpldt0(xp, all_0_8_8) = all_66_0_23, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.65 | (234) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v3, sz10) = all_66_0_23 & sdtasdt0(xp, v0) = v1 & sdtasdt0(xp, all_0_8_8) = v2 & sdtpldt0(v2, xp) = v1 & sdtpldt0(all_0_8_8, sz10) = v0 & sdtpldt0(xp, all_0_8_8) = v3) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (27) with all_66_0_23, all_0_8_8, xp, all_0_8_8, xp, sz10 and discharging atoms sdtasdt0(sz10, all_0_8_8) = all_0_8_8, sdtasdt0(sz10, xp) = xp, sdtpldt0(xp, all_0_8_8) = all_66_0_23, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz10), yields: % 13.05/3.65 | (235) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v1, all_0_8_8) = v2 & sdtasdt0(xp, all_0_8_8) = v3 & sdtasdt0(sz10, v0) = all_66_0_23 & sdtpldt0(all_0_8_8, v3) = v2 & sdtpldt0(xp, all_0_8_8) = v0 & sdtpldt0(sz10, xp) = v1) % 13.05/3.65 | % 13.05/3.65 | Instantiating formula (126) with all_0_2_2, xp, sz00, xp, all_0_8_8 and discharging atoms sdtasdt0(all_0_8_8, xp) = all_0_2_2, sdtpldt0(xp, sz00) = xp, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz00), yields: % 13.05/3.65 | (236) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(v2, sz00) = v3 & sdtasdt0(all_0_8_8, xp) = v0 & sdtasdt0(all_0_8_8, sz00) = v1 & sdtasdt0(xp, sz00) = v4 & sdtpldt0(v1, v4) = v3 & sdtpldt0(v0, v1) = all_0_2_2 & sdtpldt0(all_0_8_8, xp) = v2) % 13.05/3.66 | % 13.05/3.66 | Instantiating formula (90) with all_0_2_2, xp, all_0_8_8, sz00, xp and discharging atoms sdtasdt0(xp, all_0_8_8) = all_0_2_2, sdtpldt0(xp, sz00) = xp, aInteger0(all_0_8_8), aInteger0(xp), aInteger0(sz00), yields: % 13.05/3.66 | (237) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (sdtasdt0(xp, v0) = v1 & sdtasdt0(xp, all_0_8_8) = v3 & sdtasdt0(xp, sz00) = v2 & sdtasdt0(sz00, all_0_8_8) = v4 & sdtpldt0(v3, v4) = all_0_2_2 & sdtpldt0(v2, v3) = v1 & sdtpldt0(sz00, all_0_8_8) = v0) % 13.05/3.66 | % 13.05/3.66 | Instantiating formula (112) with sz00, all_0_8_8, sz10, sz10, all_0_8_8, sz10 and discharging atoms sdtasdt0(all_0_8_8, sz10) = all_0_8_8, sdtasdt0(sz10, sz10) = sz10, sdtpldt0(sz10, all_0_8_8) = sz00, aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.66 | (238) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v3, sz10) = sz00 & sdtasdt0(sz10, v0) = v1 & sdtasdt0(sz10, all_0_8_8) = v2 & sdtpldt0(v2, sz10) = v1 & sdtpldt0(all_0_8_8, sz10) = v0 & sdtpldt0(sz10, all_0_8_8) = v3) % 13.05/3.66 | % 13.05/3.66 | Instantiating formula (27) with sz00, all_0_8_8, sz10, all_0_8_8, sz10, sz10 and discharging atoms sdtasdt0(sz10, all_0_8_8) = all_0_8_8, sdtasdt0(sz10, sz10) = sz10, sdtpldt0(sz10, all_0_8_8) = sz00, aInteger0(all_0_8_8), aInteger0(sz10), yields: % 13.05/3.66 | (239) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (sdtasdt0(v1, all_0_8_8) = v2 & sdtasdt0(sz10, v0) = sz00 & sdtasdt0(sz10, all_0_8_8) = v3 & sdtpldt0(all_0_8_8, v3) = v2 & sdtpldt0(sz10, all_0_8_8) = v0 & sdtpldt0(sz10, sz10) = v1) % 13.05/3.66 | % 13.05/3.66 | Instantiating (232) with all_164_0_35, all_164_1_36, all_164_2_37, all_164_3_38, all_164_4_39 yields: % 13.05/3.66 | (240) sdtasdt0(all_164_2_37, all_0_4_4) = all_164_1_36 & sdtasdt0(all_0_8_8, all_0_4_4) = all_164_0_35 & sdtasdt0(sz10, all_0_4_4) = all_164_3_38 & sdtasdt0(sz10, all_0_8_8) = all_164_4_39 & sdtpldt0(all_164_3_38, all_164_0_35) = all_164_1_36 & sdtpldt0(all_164_4_39, all_164_3_38) = xp & sdtpldt0(sz10, all_0_8_8) = all_164_2_37 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (240) yields: % 13.05/3.66 | (241) sdtasdt0(all_164_2_37, all_0_4_4) = all_164_1_36 % 13.05/3.66 | (242) sdtasdt0(sz10, all_0_8_8) = all_164_4_39 % 13.05/3.66 | (243) sdtasdt0(sz10, all_0_4_4) = all_164_3_38 % 13.05/3.66 | (244) sdtpldt0(all_164_3_38, all_164_0_35) = all_164_1_36 % 13.05/3.66 | (245) sdtasdt0(all_0_8_8, all_0_4_4) = all_164_0_35 % 13.05/3.66 | (246) sdtpldt0(sz10, all_0_8_8) = all_164_2_37 % 13.05/3.66 | (247) sdtpldt0(all_164_4_39, all_164_3_38) = xp % 13.05/3.66 | % 13.05/3.66 | Instantiating (235) with all_170_0_46, all_170_1_47, all_170_2_48, all_170_3_49 yields: % 13.05/3.66 | (248) sdtasdt0(all_170_2_48, all_0_8_8) = all_170_1_47 & sdtasdt0(xp, all_0_8_8) = all_170_0_46 & sdtasdt0(sz10, all_170_3_49) = all_66_0_23 & sdtpldt0(all_0_8_8, all_170_0_46) = all_170_1_47 & sdtpldt0(xp, all_0_8_8) = all_170_3_49 & sdtpldt0(sz10, xp) = all_170_2_48 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (248) yields: % 13.05/3.66 | (249) sdtasdt0(sz10, all_170_3_49) = all_66_0_23 % 13.05/3.66 | (250) sdtpldt0(sz10, xp) = all_170_2_48 % 13.05/3.66 | (251) sdtpldt0(xp, all_0_8_8) = all_170_3_49 % 13.05/3.66 | (252) sdtasdt0(xp, all_0_8_8) = all_170_0_46 % 13.05/3.66 | (253) sdtpldt0(all_0_8_8, all_170_0_46) = all_170_1_47 % 13.05/3.66 | (254) sdtasdt0(all_170_2_48, all_0_8_8) = all_170_1_47 % 13.05/3.66 | % 13.05/3.66 | Instantiating (236) with all_200_0_103, all_200_1_104, all_200_2_105, all_200_3_106, all_200_4_107 yields: % 13.05/3.66 | (255) sdtasdt0(all_200_2_105, sz00) = all_200_1_104 & sdtasdt0(all_0_8_8, xp) = all_200_4_107 & sdtasdt0(all_0_8_8, sz00) = all_200_3_106 & sdtasdt0(xp, sz00) = all_200_0_103 & sdtpldt0(all_200_3_106, all_200_0_103) = all_200_1_104 & sdtpldt0(all_200_4_107, all_200_3_106) = all_0_2_2 & sdtpldt0(all_0_8_8, xp) = all_200_2_105 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (255) yields: % 13.05/3.66 | (256) sdtpldt0(all_200_4_107, all_200_3_106) = all_0_2_2 % 13.05/3.66 | (257) sdtpldt0(all_0_8_8, xp) = all_200_2_105 % 13.05/3.66 | (258) sdtasdt0(all_200_2_105, sz00) = all_200_1_104 % 13.05/3.66 | (259) sdtasdt0(all_0_8_8, xp) = all_200_4_107 % 13.05/3.66 | (260) sdtasdt0(xp, sz00) = all_200_0_103 % 13.05/3.66 | (261) sdtpldt0(all_200_3_106, all_200_0_103) = all_200_1_104 % 13.05/3.66 | (262) sdtasdt0(all_0_8_8, sz00) = all_200_3_106 % 13.05/3.66 | % 13.05/3.66 | Instantiating (230) with all_214_0_130 yields: % 13.05/3.66 | (263) sdtpldt0(all_0_2_2, all_214_0_130) = all_0_0_0 & sdtpldt0(sz10, all_0_8_8) = all_214_0_130 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (263) yields: % 13.05/3.66 | (264) sdtpldt0(all_0_2_2, all_214_0_130) = all_0_0_0 % 13.05/3.66 | (265) sdtpldt0(sz10, all_0_8_8) = all_214_0_130 % 13.05/3.66 | % 13.05/3.66 | Instantiating (238) with all_220_0_140, all_220_1_141, all_220_2_142, all_220_3_143 yields: % 13.05/3.66 | (266) sdtasdt0(all_220_0_140, sz10) = sz00 & sdtasdt0(sz10, all_220_3_143) = all_220_2_142 & sdtasdt0(sz10, all_0_8_8) = all_220_1_141 & sdtpldt0(all_220_1_141, sz10) = all_220_2_142 & sdtpldt0(all_0_8_8, sz10) = all_220_3_143 & sdtpldt0(sz10, all_0_8_8) = all_220_0_140 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (266) yields: % 13.05/3.66 | (267) sdtpldt0(all_220_1_141, sz10) = all_220_2_142 % 13.05/3.66 | (268) sdtpldt0(all_0_8_8, sz10) = all_220_3_143 % 13.05/3.66 | (269) sdtasdt0(sz10, all_220_3_143) = all_220_2_142 % 13.05/3.66 | (270) sdtasdt0(sz10, all_0_8_8) = all_220_1_141 % 13.05/3.66 | (271) sdtpldt0(sz10, all_0_8_8) = all_220_0_140 % 13.05/3.66 | (272) sdtasdt0(all_220_0_140, sz10) = sz00 % 13.05/3.66 | % 13.05/3.66 | Instantiating (237) with all_226_0_150, all_226_1_151, all_226_2_152, all_226_3_153, all_226_4_154 yields: % 13.05/3.66 | (273) sdtasdt0(xp, all_226_4_154) = all_226_3_153 & sdtasdt0(xp, all_0_8_8) = all_226_1_151 & sdtasdt0(xp, sz00) = all_226_2_152 & sdtasdt0(sz00, all_0_8_8) = all_226_0_150 & sdtpldt0(all_226_1_151, all_226_0_150) = all_0_2_2 & sdtpldt0(all_226_2_152, all_226_1_151) = all_226_3_153 & sdtpldt0(sz00, all_0_8_8) = all_226_4_154 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (273) yields: % 13.05/3.66 | (274) sdtasdt0(xp, all_0_8_8) = all_226_1_151 % 13.05/3.66 | (275) sdtasdt0(xp, all_226_4_154) = all_226_3_153 % 13.05/3.66 | (276) sdtpldt0(all_226_2_152, all_226_1_151) = all_226_3_153 % 13.05/3.66 | (277) sdtasdt0(xp, sz00) = all_226_2_152 % 13.05/3.66 | (278) sdtpldt0(all_226_1_151, all_226_0_150) = all_0_2_2 % 13.05/3.66 | (279) sdtpldt0(sz00, all_0_8_8) = all_226_4_154 % 13.05/3.66 | (280) sdtasdt0(sz00, all_0_8_8) = all_226_0_150 % 13.05/3.66 | % 13.05/3.66 | Instantiating (239) with all_228_0_155, all_228_1_156, all_228_2_157, all_228_3_158 yields: % 13.05/3.66 | (281) sdtasdt0(all_228_2_157, all_0_8_8) = all_228_1_156 & sdtasdt0(sz10, all_228_3_158) = sz00 & sdtasdt0(sz10, all_0_8_8) = all_228_0_155 & sdtpldt0(all_0_8_8, all_228_0_155) = all_228_1_156 & sdtpldt0(sz10, all_0_8_8) = all_228_3_158 & sdtpldt0(sz10, sz10) = all_228_2_157 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (281) yields: % 13.05/3.66 | (282) sdtasdt0(sz10, all_0_8_8) = all_228_0_155 % 13.05/3.66 | (283) sdtpldt0(all_0_8_8, all_228_0_155) = all_228_1_156 % 13.05/3.66 | (284) sdtpldt0(sz10, sz10) = all_228_2_157 % 13.05/3.66 | (285) sdtasdt0(sz10, all_228_3_158) = sz00 % 13.05/3.66 | (286) sdtasdt0(all_228_2_157, all_0_8_8) = all_228_1_156 % 13.05/3.66 | (287) sdtpldt0(sz10, all_0_8_8) = all_228_3_158 % 13.05/3.66 | % 13.05/3.66 | Instantiating (234) with all_242_0_174, all_242_1_175, all_242_2_176, all_242_3_177 yields: % 13.05/3.66 | (288) sdtasdt0(all_242_0_174, sz10) = all_66_0_23 & sdtasdt0(xp, all_242_3_177) = all_242_2_176 & sdtasdt0(xp, all_0_8_8) = all_242_1_175 & sdtpldt0(all_242_1_175, xp) = all_242_2_176 & sdtpldt0(all_0_8_8, sz10) = all_242_3_177 & sdtpldt0(xp, all_0_8_8) = all_242_0_174 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (288) yields: % 13.05/3.66 | (289) sdtasdt0(all_242_0_174, sz10) = all_66_0_23 % 13.05/3.66 | (290) sdtasdt0(xp, all_242_3_177) = all_242_2_176 % 13.05/3.66 | (291) sdtpldt0(all_0_8_8, sz10) = all_242_3_177 % 13.05/3.66 | (292) sdtasdt0(xp, all_0_8_8) = all_242_1_175 % 13.05/3.66 | (293) sdtpldt0(all_242_1_175, xp) = all_242_2_176 % 13.05/3.66 | (294) sdtpldt0(xp, all_0_8_8) = all_242_0_174 % 13.05/3.66 | % 13.05/3.66 | Instantiating (233) with all_244_0_178 yields: % 13.05/3.66 | (295) sdtpldt0(all_244_0_178, all_0_4_4) = all_0_4_4 & sdtpldt0(sz10, all_0_8_8) = all_244_0_178 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (295) yields: % 13.05/3.66 | (296) sdtpldt0(all_244_0_178, all_0_4_4) = all_0_4_4 % 13.05/3.66 | (297) sdtpldt0(sz10, all_0_8_8) = all_244_0_178 % 13.05/3.66 | % 13.05/3.66 | Instantiating (229) with all_264_0_197, all_264_1_198, all_264_2_199, all_264_3_200 yields: % 13.05/3.66 | (298) sdtasdt0(all_264_0_197, all_0_8_8) = all_60_0_20 & sdtasdt0(xp, all_264_3_200) = all_264_2_199 & sdtasdt0(xp, sz10) = all_264_1_198 & sdtpldt0(all_264_1_198, all_0_2_2) = all_264_2_199 & sdtpldt0(xp, sz10) = all_264_0_197 & sdtpldt0(sz10, all_0_8_8) = all_264_3_200 % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (298) yields: % 13.05/3.66 | (299) sdtpldt0(sz10, all_0_8_8) = all_264_3_200 % 13.05/3.66 | (300) sdtpldt0(all_264_1_198, all_0_2_2) = all_264_2_199 % 13.05/3.66 | (301) sdtpldt0(xp, sz10) = all_264_0_197 % 13.05/3.66 | (302) sdtasdt0(xp, all_264_3_200) = all_264_2_199 % 13.05/3.66 | (303) sdtasdt0(xp, sz10) = all_264_1_198 % 13.05/3.66 | (304) sdtasdt0(all_264_0_197, all_0_8_8) = all_60_0_20 % 13.05/3.66 | % 13.05/3.66 +-Applying beta-rule and splitting (61), into two cases. % 13.05/3.66 |-Branch one: % 13.05/3.66 | (305) ~ aElementOf0(all_0_1_1, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_1_1, sz10, xp) & ~ aDivisorOf0(xp, all_0_0_0) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_0_0) & sdtasdt0(xp, v0) = v1)) % 13.05/3.66 | % 13.05/3.66 | Applying alpha-rule on (305) yields: % 13.05/3.66 | (306) ~ aElementOf0(all_0_1_1, all_0_5_5) % 13.05/3.66 | (307) ~ sdteqdtlpzmzozddtrp0(all_0_1_1, sz10, xp) % 13.05/3.66 | (308) ~ aDivisorOf0(xp, all_0_0_0) % 13.05/3.66 | (309) ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_0_0) & sdtasdt0(xp, v0) = v1)) % 13.05/3.66 | % 13.05/3.66 | Instantiating formula (309) with all_0_8_8 and discharging atoms aInteger0(all_0_8_8), yields: % 13.05/3.66 | (310) ? [v0] : ( ~ (v0 = all_0_0_0) & sdtasdt0(xp, all_0_8_8) = v0) % 13.05/3.66 | % 13.05/3.66 | Instantiating (310) with all_277_0_207 yields: % 13.05/3.67 | (311) ~ (all_277_0_207 = all_0_0_0) & sdtasdt0(xp, all_0_8_8) = all_277_0_207 % 13.05/3.67 | % 13.05/3.67 | Applying alpha-rule on (311) yields: % 13.05/3.67 | (312) ~ (all_277_0_207 = all_0_0_0) % 13.05/3.67 | (313) sdtasdt0(xp, all_0_8_8) = all_277_0_207 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (51) with all_0_8_8, xp, all_200_4_107, all_0_2_2 and discharging atoms sdtasdt0(all_0_8_8, xp) = all_200_4_107, sdtasdt0(all_0_8_8, xp) = all_0_2_2, yields: % 13.05/3.67 | (314) all_200_4_107 = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (12) with all_200_3_106, all_0_8_8 and discharging atoms sdtasdt0(all_0_8_8, sz00) = all_200_3_106, aInteger0(all_0_8_8), yields: % 13.05/3.67 | (315) all_200_3_106 = sz00 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (51) with xp, all_0_8_8, all_242_1_175, all_277_0_207 and discharging atoms sdtasdt0(xp, all_0_8_8) = all_277_0_207, sdtasdt0(xp, all_0_8_8) = all_242_1_175, yields: % 13.05/3.67 | (316) all_277_0_207 = all_242_1_175 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (51) with xp, all_0_8_8, all_226_1_151, all_0_2_2 and discharging atoms sdtasdt0(xp, all_0_8_8) = all_226_1_151, sdtasdt0(xp, all_0_8_8) = all_0_2_2, yields: % 13.05/3.67 | (317) all_226_1_151 = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (51) with xp, all_0_8_8, all_226_1_151, all_242_1_175 and discharging atoms sdtasdt0(xp, all_0_8_8) = all_242_1_175, sdtasdt0(xp, all_0_8_8) = all_226_1_151, yields: % 13.05/3.67 | (318) all_242_1_175 = all_226_1_151 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (51) with xp, all_0_8_8, all_170_0_46, all_277_0_207 and discharging atoms sdtasdt0(xp, all_0_8_8) = all_277_0_207, sdtasdt0(xp, all_0_8_8) = all_170_0_46, yields: % 13.05/3.67 | (319) all_277_0_207 = all_170_0_46 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (113) with all_264_3_200, all_0_8_8, sz10 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_264_3_200, smndt0(sz10) = all_0_8_8, aInteger0(sz10), yields: % 13.05/3.67 | (320) all_264_3_200 = sz00 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with sz10, all_0_8_8, all_228_3_158, all_264_3_200 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_264_3_200, sdtpldt0(sz10, all_0_8_8) = all_228_3_158, yields: % 13.05/3.67 | (321) all_264_3_200 = all_228_3_158 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with sz10, all_0_8_8, all_220_0_140, all_228_3_158 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_228_3_158, sdtpldt0(sz10, all_0_8_8) = all_220_0_140, yields: % 13.05/3.67 | (322) all_228_3_158 = all_220_0_140 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with sz10, all_0_8_8, all_214_0_130, all_244_0_178 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_244_0_178, sdtpldt0(sz10, all_0_8_8) = all_214_0_130, yields: % 13.05/3.67 | (323) all_244_0_178 = all_214_0_130 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with sz10, all_0_8_8, all_214_0_130, all_220_0_140 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_220_0_140, sdtpldt0(sz10, all_0_8_8) = all_214_0_130, yields: % 13.05/3.67 | (324) all_220_0_140 = all_214_0_130 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with sz10, all_0_8_8, all_164_2_37, all_244_0_178 and discharging atoms sdtpldt0(sz10, all_0_8_8) = all_244_0_178, sdtpldt0(sz10, all_0_8_8) = all_164_2_37, yields: % 13.05/3.67 | (325) all_244_0_178 = all_164_2_37 % 13.05/3.67 | % 13.05/3.67 | Combining equations (316,319) yields a new equation: % 13.05/3.67 | (326) all_242_1_175 = all_170_0_46 % 13.05/3.67 | % 13.05/3.67 | Simplifying 326 yields: % 13.05/3.67 | (327) all_242_1_175 = all_170_0_46 % 13.05/3.67 | % 13.05/3.67 | Combining equations (321,320) yields a new equation: % 13.05/3.67 | (328) all_228_3_158 = sz00 % 13.05/3.67 | % 13.05/3.67 | Simplifying 328 yields: % 13.05/3.67 | (329) all_228_3_158 = sz00 % 13.05/3.67 | % 13.05/3.67 | Combining equations (323,325) yields a new equation: % 13.05/3.67 | (330) all_214_0_130 = all_164_2_37 % 13.05/3.67 | % 13.05/3.67 | Simplifying 330 yields: % 13.05/3.67 | (331) all_214_0_130 = all_164_2_37 % 13.05/3.67 | % 13.05/3.67 | Combining equations (318,327) yields a new equation: % 13.05/3.67 | (332) all_226_1_151 = all_170_0_46 % 13.05/3.67 | % 13.05/3.67 | Simplifying 332 yields: % 13.05/3.67 | (333) all_226_1_151 = all_170_0_46 % 13.05/3.67 | % 13.05/3.67 | Combining equations (322,329) yields a new equation: % 13.05/3.67 | (334) all_220_0_140 = sz00 % 13.05/3.67 | % 13.05/3.67 | Simplifying 334 yields: % 13.05/3.67 | (335) all_220_0_140 = sz00 % 13.05/3.67 | % 13.05/3.67 | Combining equations (317,333) yields a new equation: % 13.05/3.67 | (336) all_170_0_46 = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | Combining equations (324,335) yields a new equation: % 13.05/3.67 | (337) all_214_0_130 = sz00 % 13.05/3.67 | % 13.05/3.67 | Simplifying 337 yields: % 13.05/3.67 | (338) all_214_0_130 = sz00 % 13.05/3.67 | % 13.05/3.67 | Combining equations (338,331) yields a new equation: % 13.05/3.67 | (339) all_164_2_37 = sz00 % 13.05/3.67 | % 13.05/3.67 | Combining equations (339,331) yields a new equation: % 13.05/3.67 | (338) all_214_0_130 = sz00 % 13.05/3.67 | % 13.05/3.67 | Combining equations (336,319) yields a new equation: % 13.05/3.67 | (341) all_277_0_207 = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | Equations (341) can reduce 312 to: % 13.05/3.67 | (342) ~ (all_0_0_0 = all_0_2_2) % 13.05/3.67 | % 13.05/3.67 | Simplifying 342 yields: % 13.05/3.67 | (343) ~ (all_0_0_0 = all_0_2_2) % 13.05/3.67 | % 13.05/3.67 | From (314)(315) and (256) follows: % 13.05/3.67 | (344) sdtpldt0(all_0_2_2, sz00) = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | From (338) and (264) follows: % 13.05/3.67 | (345) sdtpldt0(all_0_2_2, sz00) = all_0_0_0 % 13.05/3.67 | % 13.05/3.67 | Instantiating formula (128) with all_0_2_2, sz00, all_0_2_2, all_0_0_0 and discharging atoms sdtpldt0(all_0_2_2, sz00) = all_0_0_0, sdtpldt0(all_0_2_2, sz00) = all_0_2_2, yields: % 13.05/3.67 | (346) all_0_0_0 = all_0_2_2 % 13.05/3.67 | % 13.05/3.67 | Equations (346) can reduce 343 to: % 13.05/3.67 | (347) $false % 13.05/3.67 | % 13.05/3.67 |-The branch is then unsatisfiable % 13.05/3.67 |-Branch two: % 13.05/3.67 | (348) ~ aElementOf0(all_0_4_4, all_0_5_5) & ~ sdteqdtlpzmzozddtrp0(all_0_4_4, sz10, xp) & ~ aDivisorOf0(xp, all_0_3_3) & ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_3_3) & sdtasdt0(xp, v0) = v1)) % 13.05/3.67 | % 13.05/3.67 | Applying alpha-rule on (348) yields: % 13.05/3.67 | (349) ~ aElementOf0(all_0_4_4, all_0_5_5) % 13.05/3.67 | (350) ~ sdteqdtlpzmzozddtrp0(all_0_4_4, sz10, xp) % 13.05/3.67 | (351) ~ aDivisorOf0(xp, all_0_3_3) % 13.05/3.67 | (352) ! [v0] : ( ~ aInteger0(v0) | ? [v1] : ( ~ (v1 = all_0_3_3) & sdtasdt0(xp, v0) = v1)) % 13.05/3.67 | % 13.05/3.67 | Using (231) and (349) yields: % 13.05/3.67 | (353) $false % 13.05/3.67 | % 13.05/3.67 |-The branch is then unsatisfiable % 13.05/3.67 % SZS output end Proof for theBenchmark % 13.05/3.67 % 13.05/3.67 3045ms %------------------------------------------------------------------------------