%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM449+6 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n012.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 : 300s % DateTime : Thu Aug 31 11:47:49 EDT 2023 % Result : Theorem 14.70s 2.87s % Output : Proof 19.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM449+6 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.34 % Computer : n012.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Aug 25 17:49:41 EDT 2023 % 0.14/0.34 % CPUTime : % 0.21/0.61 ________ _____ % 0.21/0.61 ___ __ \_________(_)________________________________ % 0.21/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.61 % 0.21/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.61 (2023-06-19) % 0.21/0.61 % 0.21/0.61 (c) Philipp Rümmer, 2009-2023 % 0.21/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.61 Amanda Stjerna. % 0.21/0.61 Free software under BSD-3-Clause. % 0.21/0.61 % 0.21/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.61 % 0.21/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.62 Running up to 7 provers in parallel. % 0.21/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.00/1.25 Prover 4: Preprocessing ... % 4.00/1.25 Prover 1: Preprocessing ... % 4.15/1.29 Prover 6: Preprocessing ... % 4.15/1.29 Prover 5: Preprocessing ... % 4.15/1.29 Prover 0: Preprocessing ... % 4.15/1.29 Prover 2: Preprocessing ... % 4.46/1.33 Prover 3: Preprocessing ... % 11.48/2.30 Prover 3: Constructing countermodel ... % 11.48/2.33 Prover 1: Constructing countermodel ... % 12.17/2.38 Prover 6: Proving ... % 12.17/2.38 Prover 5: Proving ... % 13.23/2.53 Prover 2: Proving ... % 14.70/2.86 Prover 3: proved (2234ms) % 14.70/2.87 % 14.70/2.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.70/2.87 % 14.70/2.87 Prover 5: stopped % 14.70/2.87 Prover 6: stopped % 14.70/2.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.70/2.88 Prover 2: stopped % 15.70/2.90 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 15.70/2.90 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.70/2.90 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 17.58/3.13 Prover 8: Preprocessing ... % 17.58/3.16 Prover 11: Preprocessing ... % 17.89/3.17 Prover 7: Preprocessing ... % 17.89/3.17 Prover 10: Preprocessing ... % 17.89/3.18 Prover 1: Found proof (size 75) % 17.89/3.18 Prover 1: proved (2551ms) % 17.89/3.23 Prover 0: Proving ... % 17.89/3.23 Prover 0: stopped % 18.48/3.23 Prover 10: stopped % 18.48/3.24 Prover 4: Constructing countermodel ... % 18.48/3.24 Prover 7: stopped % 18.48/3.26 Prover 4: stopped % 18.72/3.32 Prover 11: stopped % 19.18/3.39 Prover 8: Warning: ignoring some quantifiers % 19.18/3.40 Prover 8: Constructing countermodel ... % 19.18/3.41 Prover 8: stopped % 19.18/3.41 % 19.18/3.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.18/3.41 % 19.18/3.42 % SZS output start Proof for theBenchmark % 19.18/3.42 Assumptions after simplification: % 19.18/3.42 --------------------------------- % 19.49/3.42 % 19.49/3.42 (mArSeqClosed) % 19.49/3.45 $i(cS1395) & $i(sz00) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | % 19.49/3.45 ~ (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 19.49/3.45 any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : (isClosed0(v2) = v6 & % 19.49/3.45 aSubsetOf0(v2, cS1395) = v5 & aInteger0(v1) = v4 & aInteger0(v0) = v3 & ( % 19.49/3.45 ~ (v4 = 0) | ~ (v3 = 0) | (v6 = 0 & v5 = 0)))) % 19.49/3.45 % 19.49/3.45 (mIntNeg) % 19.49/3.45 ! [v0: $i] : ! [v1: $i] : ( ~ (smndt0(v0) = v1) | ~ $i(v0) | ? [v2: any] : % 19.49/3.45 ? [v3: any] : (aInteger0(v1) = v3 & aInteger0(v0) = v2 & ( ~ (v2 = 0) | v3 % 19.49/3.45 = 0))) % 19.49/3.45 % 19.49/3.45 (mIntZero) % 19.49/3.45 aInteger0(sz00) = 0 & $i(sz00) % 19.49/3.45 % 19.49/3.45 (mUnionSClosed) % 19.49/3.46 $i(cS1395) & ! [v0: $i] : ( ~ (isFinite0(v0) = 0) | ~ $i(v0) | ? [v1: any] % 19.49/3.46 : ? [v2: $i] : ? [v3: any] : (isClosed0(v2) = v3 & sbsmnsldt0(v0) = v2 & % 19.49/3.46 aSet0(v0) = v1 & $i(v2) & ( ~ (v1 = 0) | v3 = 0)) | ? [v1: $i] : ? [v2: % 19.49/3.46 any] : ? [v3: any] : (isClosed0(v1) = v3 & aSubsetOf0(v1, cS1395) = v2 & % 19.49/3.46 aElementOf0(v1, v0) = 0 & $i(v1) & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 19.49/3.46 % 19.49/3.46 (m__) % 19.49/3.46 $i(xS) & $i(sz00) & ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ? [v3: int] : % 19.49/3.46 ( ~ (v3 = 0) & ~ (v2 = 0) & isClosed0(v0) = v3 & isOpen0(v1) = v2 & % 19.49/3.46 stldt0(v0) = v1 & sbsmnsldt0(xS) = v0 & aSet0(v0) = 0 & $i(v1) & $i(v0) & ! % 19.49/3.46 [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) | ~ % 19.49/3.46 $i(v4) | ? [v6: any] : ? [v7: any] : (aElementOf0(v4, v0) = v7 & % 19.49/3.46 aInteger0(v4) = v6 & ( ~ (v6 = 0) | v7 = 0))) & ! [v4: $i] : ! [v5: % 19.49/3.46 int] : (v5 = 0 | ~ (aElementOf0(v4, v0) = v5) | ~ $i(v4) | ? [v6: int] % 19.49/3.47 : ( ~ (v6 = 0) & aInteger0(v4) = v6) | ! [v6: $i] : ( ~ (aElementOf0(v6, % 19.49/3.47 xS) = 0) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = 0) & aElementOf0(v4, % 19.49/3.47 v6) = v7))) & ! [v4: $i] : ( ~ (aElementOf0(v4, v1) = 0) | ~ % 19.49/3.47 $i(v4) | ? [v5: int] : ( ~ (v5 = 0) & aElementOf0(v4, v0) = v5 & % 19.49/3.47 aInteger0(v4) = 0)) & ! [v4: $i] : ( ~ (aElementOf0(v4, v0) = 0) | ~ % 19.49/3.47 $i(v4) | (aInteger0(v4) = 0 & ? [v5: $i] : (aElementOf0(v5, xS) = 0 & % 19.49/3.47 aElementOf0(v4, v5) = 0 & $i(v5)))) & ? [v4: $i] : ? [v5: $i] : % 19.49/3.47 (aElementOf0(v4, v1) = 0 & smndt0(v4) = v5 & $i(v5) & $i(v4) & ! [v6: $i] : % 19.49/3.47 ! [v7: $i] : (v6 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v4, v6) = v7) | ~ % 19.49/3.47 $i(v6) | ? [v8: any] : ? [v9: any] : ? [v10: any] : (aSubsetOf0(v7, % 19.49/3.47 v1) = v10 & aSet0(v7) = v9 & aInteger0(v6) = v8 & ( ~ (v8 = 0) | (v9 % 19.49/3.47 = 0 & ~ (v10 = 0) & ! [v11: $i] : ! [v12: $i] : ! [v13: any] : % 19.49/3.47 ( ~ (aDivisorOf0(v6, v12) = v13) | ~ (sdtpldt0(v11, v5) = v12) | % 19.49/3.47 ~ $i(v11) | ? [v14: any] : ? [v15: any] : ? [v16: any] : % 19.49/3.47 (aElementOf0(v11, v7) = v16 & sdteqdtlpzmzozddtrp0(v11, v4, v6) % 19.49/3.47 = v15 & aInteger0(v11) = v14 & ( ~ (v14 = 0) | v16 = 0 | ( ~ % 19.49/3.47 (v15 = 0) & ~ (v13 = 0) & ! [v17: $i] : ( ~ % 19.49/3.47 (sdtasdt0(v6, v17) = v12) | ~ $i(v17) | ? [v18: int] : % 19.49/3.47 ( ~ (v18 = 0) & aInteger0(v17) = v18)))))) & ! [v11: % 19.49/3.47 $i] : ! [v12: $i] : ! [v13: any] : ( ~ (aDivisorOf0(v6, v12) = % 19.49/3.47 v13) | ~ (sdtpldt0(v11, v5) = v12) | ~ $i(v11) | ? [v14: % 19.49/3.47 any] : ? [v15: any] : ? [v16: any] : (aElementOf0(v11, v7) = % 19.49/3.47 v14 & sdteqdtlpzmzozddtrp0(v11, v4, v6) = v16 & aInteger0(v11) % 19.49/3.47 = v15 & ( ~ (v14 = 0) | (v16 = 0 & v15 = 0 & v13 = 0 & ? % 19.49/3.47 [v17: $i] : (sdtasdt0(v6, v17) = v12 & aInteger0(v17) = 0 % 19.49/3.47 & $i(v17) & $i(v12)))))) & ? [v11: $i] : ? [v12: int] % 19.49/3.47 : ( ~ (v12 = 0) & aElementOf0(v11, v7) = 0 & aElementOf0(v11, v1) % 19.49/3.47 = v12 & $i(v11)))))))) % 19.49/3.47 % 19.49/3.47 (m__2046) % 19.49/3.47 $i(cS2043) & $i(xS) & $i(sz00) & ? [v0: $i] : (cS2043 = xS & aSet0(xS) = 0 & % 19.49/3.47 smndt0(sz00) = v0 & $i(v0) & ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 19.49/3.47 (aElementOf0(v1, xS) = v2) | ~ $i(v1) | ! [v3: $i] : ! [v4: $i] : (v3 = % 19.49/3.47 sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(sz00, v3) = v4) | ~ $i(v3) | ? [v5: % 19.49/3.47 any] : ? [v6: any] : ? [v7: any] : (aSet0(v4) = v7 & isPrime0(v3) = % 19.49/3.47 v6 & aInteger0(v3) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & ~ % 19.49/3.47 (v4 = v1) & ! [v8: $i] : ! [v9: $i] : ! [v10: any] : ( ~ % 19.49/3.47 (aDivisorOf0(v3, v9) = v10) | ~ (sdtpldt0(v8, v0) = v9) | ~ % 19.49/3.47 $i(v8) | ? [v11: any] : ? [v12: any] : ? [v13: any] : % 19.49/3.47 (aElementOf0(v8, v4) = v13 & sdteqdtlpzmzozddtrp0(v8, sz00, v3) % 19.49/3.47 = v12 & aInteger0(v8) = v11 & ( ~ (v11 = 0) | v13 = 0 | ( ~ % 19.49/3.47 (v12 = 0) & ~ (v10 = 0) & ! [v14: $i] : ( ~ % 19.49/3.47 (sdtasdt0(v3, v14) = v9) | ~ $i(v14) | ? [v15: int] : % 19.49/3.47 ( ~ (v15 = 0) & aInteger0(v14) = v15)))))) & ! [v8: $i] % 19.49/3.47 : ! [v9: $i] : ! [v10: any] : ( ~ (aDivisorOf0(v3, v9) = v10) | % 19.49/3.47 ~ (sdtpldt0(v8, v0) = v9) | ~ $i(v8) | ? [v11: any] : ? [v12: % 19.49/3.47 any] : ? [v13: any] : (aElementOf0(v8, v4) = v11 & % 19.49/3.47 sdteqdtlpzmzozddtrp0(v8, sz00, v3) = v13 & aInteger0(v8) = v12 % 19.49/3.47 & ( ~ (v11 = 0) | (v13 = 0 & v12 = 0 & v10 = 0 & ? [v14: $i] % 19.49/3.47 : (sdtasdt0(v3, v14) = v9 & aInteger0(v14) = 0 & $i(v14) & % 19.49/3.47 $i(v9))))))))))) & ! [v1: $i] : ( ~ (aElementOf0(v1, % 19.49/3.47 xS) = 0) | ~ $i(v1) | ? [v2: $i] : ( ~ (v2 = sz00) & % 19.49/3.47 szAzrzSzezqlpdtcmdtrp0(sz00, v2) = v1 & aSet0(v1) = 0 & isPrime0(v2) = 0 % 19.49/3.47 & aInteger0(v2) = 0 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: any] % 19.49/3.47 : ( ~ (aDivisorOf0(v2, v4) = v5) | ~ (sdtpldt0(v3, v0) = v4) | ~ % 19.49/3.47 $i(v3) | ? [v6: any] : ? [v7: any] : ? [v8: any] : (aElementOf0(v3, % 19.49/3.47 v1) = v8 & sdteqdtlpzmzozddtrp0(v3, sz00, v2) = v7 & aInteger0(v3) % 19.49/3.47 = v6 & ( ~ (v6 = 0) | v8 = 0 | ( ~ (v7 = 0) & ~ (v5 = 0) & ! [v9: % 19.49/3.47 $i] : ( ~ (sdtasdt0(v2, v9) = v4) | ~ $i(v9) | ? [v10: int] % 19.49/3.47 : ( ~ (v10 = 0) & aInteger0(v9) = v10)))))) & ! [v3: $i] : ! % 19.49/3.47 [v4: $i] : ! [v5: any] : ( ~ (aDivisorOf0(v2, v4) = v5) | ~ % 19.49/3.47 (sdtpldt0(v3, v0) = v4) | ~ $i(v3) | ? [v6: any] : ? [v7: any] : ? % 19.49/3.47 [v8: any] : (aElementOf0(v3, v1) = v6 & sdteqdtlpzmzozddtrp0(v3, sz00, % 19.49/3.47 v2) = v8 & aInteger0(v3) = v7 & ( ~ (v6 = 0) | (v8 = 0 & v7 = 0 & % 19.49/3.47 v5 = 0 & ? [v9: $i] : (sdtasdt0(v2, v9) = v4 & aInteger0(v9) = % 19.49/3.47 0 & $i(v9) & $i(v4))))))))) % 19.49/3.47 % 19.49/3.47 (m__2079) % 19.49/3.48 $i(cS2076) & $i(xS) & $i(sz10) & ? [v0: $i] : ? [v1: $i] : (stldt0(v0) = % 19.49/3.48 cS2076 & sbsmnsldt0(xS) = v0 & aSet0(v0) = 0 & aSet0(cS2076) = 0 & % 19.49/3.48 smndt0(sz10) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | % 19.49/3.48 ~ (aElementOf0(v2, v0) = v3) | ~ $i(v2) | ? [v4: int] : ( ~ (v4 = 0) & % 19.49/3.48 aInteger0(v2) = v4) | ! [v4: $i] : ( ~ (aElementOf0(v4, xS) = 0) | ~ % 19.49/3.48 $i(v4) | ? [v5: int] : ( ~ (v5 = 0) & aElementOf0(v2, v4) = v5))) & ! % 19.49/3.48 [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (aElementOf0(v2, cS2076) = v3) | ~ % 19.49/3.48 $i(v2) | ? [v4: any] : ? [v5: any] : (aElementOf0(v2, v0) = v5 & % 19.49/3.48 aInteger0(v2) = v4 & ( ~ (v4 = 0) | v5 = 0))) & ! [v2: $i] : ! [v3: % 19.49/3.48 int] : (v3 = 0 | ~ (aElementOf0(v2, cS2076) = v3) | ~ $i(v2) | ( ~ (v2 = % 19.49/3.48 v1) & ~ (v2 = sz10))) & ! [v2: $i] : (v2 = v1 | v2 = sz10 | ~ % 19.49/3.48 (aElementOf0(v2, cS2076) = 0) | ~ $i(v2)) & ! [v2: $i] : ( ~ % 19.49/3.48 (aElementOf0(v2, v0) = 0) | ~ $i(v2) | (aInteger0(v2) = 0 & ? [v3: $i] : % 19.49/3.48 (aElementOf0(v3, xS) = 0 & aElementOf0(v2, v3) = 0 & $i(v3)))) & ! [v2: % 19.49/3.48 $i] : ( ~ (aElementOf0(v2, cS2076) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ % 19.49/3.48 (v3 = 0) & aElementOf0(v2, v0) = v3 & aInteger0(v2) = 0))) % 19.49/3.48 % 19.49/3.48 (m__2117) % 19.49/3.48 isFinite0(xS) = 0 & $i(xS) % 19.49/3.48 % 19.49/3.48 (function-axioms) % 19.49/3.48 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 19.49/3.48 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v1) % 19.49/3.48 | ~ (sdteqdtlpzmzozddtrp0(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 19.49/3.48 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v1) % 19.49/3.48 | ~ (szAzrzSzezqlpdtcmdtrp0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 19.49/3.48 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtslmnbsdt0(v3, v2) = v1) | ~ % 19.49/3.48 (sdtslmnbsdt0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 19.49/3.48 [v3: $i] : (v1 = v0 | ~ (sdtbsmnsldt0(v3, v2) = v1) | ~ (sdtbsmnsldt0(v3, % 19.49/3.48 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 19.49/3.48 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (aSubsetOf0(v3, v2) = v1) | ~ % 19.49/3.48 (aSubsetOf0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.49/3.48 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.49/3.48 (aElementOf0(v3, v2) = v1) | ~ (aElementOf0(v3, v2) = v0)) & ! [v0: % 19.49/3.48 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 19.49/3.48 : (v1 = v0 | ~ (aDivisorOf0(v3, v2) = v1) | ~ (aDivisorOf0(v3, v2) = v0)) & % 19.49/3.48 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.49/3.48 (sdtasdt0(v3, v2) = v1) | ~ (sdtasdt0(v3, v2) = v0)) & ! [v0: $i] : ! % 19.49/3.48 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtpldt0(v3, v2) = v1) | % 19.49/3.48 ~ (sdtpldt0(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.49/3.48 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isFinite0(v2) = v1) | ~ % 19.49/3.48 (isFinite0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.49/3.48 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isClosed0(v2) = v1) | ~ % 19.49/3.48 (isClosed0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.49/3.48 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isOpen0(v2) = v1) | ~ % 19.49/3.48 (isOpen0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 19.49/3.48 ~ (stldt0(v2) = v1) | ~ (stldt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 19.49/3.48 [v2: $i] : (v1 = v0 | ~ (sbsmnsldt0(v2) = v1) | ~ (sbsmnsldt0(v2) = v0)) & % 19.49/3.48 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = % 19.49/3.48 v0 | ~ (aSet0(v2) = v1) | ~ (aSet0(v2) = v0)) & ! [v0: MultipleValueBool] % 19.49/3.48 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isPrime0(v2) = v1) % 19.49/3.48 | ~ (isPrime0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 19.49/3.48 v0 | ~ (smndt0(v2) = v1) | ~ (smndt0(v2) = v0)) & ! [v0: % 19.49/3.48 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 19.49/3.48 ~ (aInteger0(v2) = v1) | ~ (aInteger0(v2) = v0)) % 19.49/3.48 % 19.49/3.48 Further assumptions not needed in the proof: % 19.49/3.48 -------------------------------------------- % 19.49/3.48 mAddAsso, mAddComm, mAddNeg, mAddZero, mArSeq, mClosed, mComplement, mDistrib, % 19.49/3.48 mDivisor, mElements, mEquMod, mEquModMul, mEquModRef, mEquModSym, mEquModTrn, % 19.49/3.48 mFinSet, mIntMult, mIntOne, mIntPlus, mIntegers, mInterOpen, mIntersection, % 19.49/3.48 mMulAsso, mMulComm, mMulMinOne, mMulOne, mMulZero, mOpen, mPrime, mPrimeDivisor, % 19.49/3.48 mSets, mSubset, mUnion, mUnionClosed, mUnionOpen, mUnionSet, mZeroDiv % 19.49/3.48 % 19.49/3.48 Those formulas are unsatisfiable: % 19.49/3.48 --------------------------------- % 19.49/3.48 % 19.49/3.48 Begin of proof % 19.49/3.49 | % 19.49/3.49 | ALPHA: (mIntZero) implies: % 19.49/3.49 | (1) aInteger0(sz00) = 0 % 19.49/3.49 | % 19.49/3.49 | ALPHA: (mUnionSClosed) implies: % 19.49/3.49 | (2) ! [v0: $i] : ( ~ (isFinite0(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? % 19.49/3.49 | [v2: $i] : ? [v3: any] : (isClosed0(v2) = v3 & sbsmnsldt0(v0) = v2 & % 19.49/3.49 | aSet0(v0) = v1 & $i(v2) & ( ~ (v1 = 0) | v3 = 0)) | ? [v1: $i] : % 19.49/3.49 | ? [v2: any] : ? [v3: any] : (isClosed0(v1) = v3 & aSubsetOf0(v1, % 19.49/3.49 | cS1395) = v2 & aElementOf0(v1, v0) = 0 & $i(v1) & ( ~ (v3 = 0) | % 19.49/3.49 | ~ (v2 = 0)))) % 19.49/3.49 | % 19.49/3.49 | ALPHA: (mArSeqClosed) implies: % 19.49/3.49 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = sz00 | ~ % 19.49/3.49 | (szAzrzSzezqlpdtcmdtrp0(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 19.49/3.49 | [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : % 19.49/3.49 | (isClosed0(v2) = v6 & aSubsetOf0(v2, cS1395) = v5 & aInteger0(v1) = % 19.49/3.49 | v4 & aInteger0(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v6 = 0 & v5 % 19.49/3.49 | = 0)))) % 19.49/3.49 | % 19.49/3.49 | ALPHA: (m__2046) implies: % 19.49/3.49 | (4) $i(cS2043) % 19.49/3.50 | (5) ? [v0: $i] : (cS2043 = xS & aSet0(xS) = 0 & smndt0(sz00) = v0 & $i(v0) % 19.49/3.50 | & ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (aElementOf0(v1, xS) = % 19.49/3.50 | v2) | ~ $i(v1) | ! [v3: $i] : ! [v4: $i] : (v3 = sz00 | ~ % 19.49/3.50 | (szAzrzSzezqlpdtcmdtrp0(sz00, v3) = v4) | ~ $i(v3) | ? [v5: % 19.49/3.50 | any] : ? [v6: any] : ? [v7: any] : (aSet0(v4) = v7 & % 19.49/3.50 | isPrime0(v3) = v6 & aInteger0(v3) = v5 & ( ~ (v6 = 0) | ~ (v5 % 19.49/3.50 | = 0) | (v7 = 0 & ~ (v4 = v1) & ! [v8: $i] : ! [v9: $i] : % 19.49/3.50 | ! [v10: any] : ( ~ (aDivisorOf0(v3, v9) = v10) | ~ % 19.49/3.50 | (sdtpldt0(v8, v0) = v9) | ~ $i(v8) | ? [v11: any] : ? % 19.49/3.50 | [v12: any] : ? [v13: any] : (aElementOf0(v8, v4) = v13 & % 19.49/3.50 | sdteqdtlpzmzozddtrp0(v8, sz00, v3) = v12 & % 19.49/3.50 | aInteger0(v8) = v11 & ( ~ (v11 = 0) | v13 = 0 | ( ~ % 19.49/3.50 | (v12 = 0) & ~ (v10 = 0) & ! [v14: $i] : ( ~ % 19.49/3.50 | (sdtasdt0(v3, v14) = v9) | ~ $i(v14) | ? [v15: % 19.49/3.50 | int] : ( ~ (v15 = 0) & aInteger0(v14) = % 19.49/3.50 | v15)))))) & ! [v8: $i] : ! [v9: $i] : ! % 19.49/3.50 | [v10: any] : ( ~ (aDivisorOf0(v3, v9) = v10) | ~ % 19.49/3.50 | (sdtpldt0(v8, v0) = v9) | ~ $i(v8) | ? [v11: any] : ? % 19.49/3.50 | [v12: any] : ? [v13: any] : (aElementOf0(v8, v4) = v11 & % 19.49/3.50 | sdteqdtlpzmzozddtrp0(v8, sz00, v3) = v13 & % 19.49/3.50 | aInteger0(v8) = v12 & ( ~ (v11 = 0) | (v13 = 0 & v12 = % 19.49/3.50 | 0 & v10 = 0 & ? [v14: $i] : (sdtasdt0(v3, v14) = % 19.49/3.50 | v9 & aInteger0(v14) = 0 & $i(v14) & % 19.49/3.50 | $i(v9))))))))))) & ! [v1: $i] : ( ~ % 19.49/3.50 | (aElementOf0(v1, xS) = 0) | ~ $i(v1) | ? [v2: $i] : ( ~ (v2 = % 19.49/3.50 | sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v2) = v1 & aSet0(v1) = 0 & % 19.49/3.50 | isPrime0(v2) = 0 & aInteger0(v2) = 0 & $i(v2) & ! [v3: $i] : ! % 19.49/3.50 | [v4: $i] : ! [v5: any] : ( ~ (aDivisorOf0(v2, v4) = v5) | ~ % 19.49/3.50 | (sdtpldt0(v3, v0) = v4) | ~ $i(v3) | ? [v6: any] : ? [v7: % 19.49/3.50 | any] : ? [v8: any] : (aElementOf0(v3, v1) = v8 & % 19.49/3.50 | sdteqdtlpzmzozddtrp0(v3, sz00, v2) = v7 & aInteger0(v3) = v6 % 19.49/3.50 | & ( ~ (v6 = 0) | v8 = 0 | ( ~ (v7 = 0) & ~ (v5 = 0) & ! % 19.49/3.50 | [v9: $i] : ( ~ (sdtasdt0(v2, v9) = v4) | ~ $i(v9) | ? % 19.49/3.50 | [v10: int] : ( ~ (v10 = 0) & aInteger0(v9) = v10)))))) % 19.49/3.50 | & ! [v3: $i] : ! [v4: $i] : ! [v5: any] : ( ~ (aDivisorOf0(v2, % 19.49/3.50 | v4) = v5) | ~ (sdtpldt0(v3, v0) = v4) | ~ $i(v3) | ? % 19.49/3.50 | [v6: any] : ? [v7: any] : ? [v8: any] : (aElementOf0(v3, v1) % 19.49/3.50 | = v6 & sdteqdtlpzmzozddtrp0(v3, sz00, v2) = v8 & % 19.49/3.50 | aInteger0(v3) = v7 & ( ~ (v6 = 0) | (v8 = 0 & v7 = 0 & v5 = 0 % 19.49/3.50 | & ? [v9: $i] : (sdtasdt0(v2, v9) = v4 & aInteger0(v9) = % 19.49/3.50 | 0 & $i(v9) & $i(v4))))))))) % 19.49/3.50 | % 19.49/3.50 | ALPHA: (m__2079) implies: % 19.49/3.50 | (6) ? [v0: $i] : ? [v1: $i] : (stldt0(v0) = cS2076 & sbsmnsldt0(xS) = v0 % 19.49/3.50 | & aSet0(v0) = 0 & aSet0(cS2076) = 0 & smndt0(sz10) = v1 & $i(v1) & % 19.49/3.50 | $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (aElementOf0(v2, % 19.49/3.50 | v0) = v3) | ~ $i(v2) | ? [v4: int] : ( ~ (v4 = 0) & % 19.49/3.50 | aInteger0(v2) = v4) | ! [v4: $i] : ( ~ (aElementOf0(v4, xS) = 0) % 19.49/3.50 | | ~ $i(v4) | ? [v5: int] : ( ~ (v5 = 0) & aElementOf0(v2, v4) = % 19.49/3.50 | v5))) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 19.49/3.50 | (aElementOf0(v2, cS2076) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: % 19.49/3.50 | any] : (aElementOf0(v2, v0) = v5 & aInteger0(v2) = v4 & ( ~ (v4 = % 19.49/3.50 | 0) | v5 = 0))) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 19.49/3.50 | (aElementOf0(v2, cS2076) = v3) | ~ $i(v2) | ( ~ (v2 = v1) & ~ (v2 % 19.49/3.50 | = sz10))) & ! [v2: $i] : (v2 = v1 | v2 = sz10 | ~ % 19.49/3.50 | (aElementOf0(v2, cS2076) = 0) | ~ $i(v2)) & ! [v2: $i] : ( ~ % 19.49/3.50 | (aElementOf0(v2, v0) = 0) | ~ $i(v2) | (aInteger0(v2) = 0 & ? % 19.49/3.50 | [v3: $i] : (aElementOf0(v3, xS) = 0 & aElementOf0(v2, v3) = 0 & % 19.49/3.50 | $i(v3)))) & ! [v2: $i] : ( ~ (aElementOf0(v2, cS2076) = 0) | % 19.49/3.50 | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = 0) & aElementOf0(v2, v0) = v3 & % 19.49/3.50 | aInteger0(v2) = 0))) % 19.49/3.50 | % 19.49/3.50 | ALPHA: (m__2117) implies: % 19.49/3.50 | (7) isFinite0(xS) = 0 % 19.49/3.50 | % 19.49/3.50 | ALPHA: (m__) implies: % 19.49/3.50 | (8) $i(sz00) % 19.49/3.51 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ? [v3: int] : ( ~ (v3 = 0) % 19.49/3.51 | & ~ (v2 = 0) & isClosed0(v0) = v3 & isOpen0(v1) = v2 & stldt0(v0) = % 19.49/3.51 | v1 & sbsmnsldt0(xS) = v0 & aSet0(v0) = 0 & $i(v1) & $i(v0) & ! [v4: % 19.49/3.51 | $i] : ! [v5: int] : (v5 = 0 | ~ (aElementOf0(v4, v1) = v5) | ~ % 19.49/3.51 | $i(v4) | ? [v6: any] : ? [v7: any] : (aElementOf0(v4, v0) = v7 & % 19.49/3.51 | aInteger0(v4) = v6 & ( ~ (v6 = 0) | v7 = 0))) & ! [v4: $i] : ! % 19.49/3.51 | [v5: int] : (v5 = 0 | ~ (aElementOf0(v4, v0) = v5) | ~ $i(v4) | ? % 19.49/3.51 | [v6: int] : ( ~ (v6 = 0) & aInteger0(v4) = v6) | ! [v6: $i] : ( ~ % 19.49/3.51 | (aElementOf0(v6, xS) = 0) | ~ $i(v6) | ? [v7: int] : ( ~ (v7 = % 19.49/3.51 | 0) & aElementOf0(v4, v6) = v7))) & ! [v4: $i] : ( ~ % 19.49/3.51 | (aElementOf0(v4, v1) = 0) | ~ $i(v4) | ? [v5: int] : ( ~ (v5 = 0) % 19.49/3.51 | & aElementOf0(v4, v0) = v5 & aInteger0(v4) = 0)) & ! [v4: $i] : % 19.49/3.51 | ( ~ (aElementOf0(v4, v0) = 0) | ~ $i(v4) | (aInteger0(v4) = 0 & ? % 19.49/3.51 | [v5: $i] : (aElementOf0(v5, xS) = 0 & aElementOf0(v4, v5) = 0 & % 19.49/3.51 | $i(v5)))) & ? [v4: $i] : ? [v5: $i] : (aElementOf0(v4, v1) = % 19.49/3.51 | 0 & smndt0(v4) = v5 & $i(v5) & $i(v4) & ! [v6: $i] : ! [v7: $i] : % 19.49/3.51 | (v6 = sz00 | ~ (szAzrzSzezqlpdtcmdtrp0(v4, v6) = v7) | ~ $i(v6) | % 19.49/3.51 | ? [v8: any] : ? [v9: any] : ? [v10: any] : (aSubsetOf0(v7, v1) % 19.49/3.51 | = v10 & aSet0(v7) = v9 & aInteger0(v6) = v8 & ( ~ (v8 = 0) | % 19.49/3.51 | (v9 = 0 & ~ (v10 = 0) & ! [v11: $i] : ! [v12: $i] : ! % 19.49/3.51 | [v13: any] : ( ~ (aDivisorOf0(v6, v12) = v13) | ~ % 19.49/3.51 | (sdtpldt0(v11, v5) = v12) | ~ $i(v11) | ? [v14: any] : % 19.49/3.51 | ? [v15: any] : ? [v16: any] : (aElementOf0(v11, v7) = % 19.49/3.51 | v16 & sdteqdtlpzmzozddtrp0(v11, v4, v6) = v15 & % 19.49/3.51 | aInteger0(v11) = v14 & ( ~ (v14 = 0) | v16 = 0 | ( ~ % 19.49/3.51 | (v15 = 0) & ~ (v13 = 0) & ! [v17: $i] : ( ~ % 19.49/3.51 | (sdtasdt0(v6, v17) = v12) | ~ $i(v17) | ? [v18: % 19.49/3.51 | int] : ( ~ (v18 = 0) & aInteger0(v17) = % 19.49/3.51 | v18)))))) & ! [v11: $i] : ! [v12: $i] : ! % 19.49/3.51 | [v13: any] : ( ~ (aDivisorOf0(v6, v12) = v13) | ~ % 19.49/3.51 | (sdtpldt0(v11, v5) = v12) | ~ $i(v11) | ? [v14: any] : % 19.49/3.51 | ? [v15: any] : ? [v16: any] : (aElementOf0(v11, v7) = % 19.49/3.51 | v14 & sdteqdtlpzmzozddtrp0(v11, v4, v6) = v16 & % 19.49/3.51 | aInteger0(v11) = v15 & ( ~ (v14 = 0) | (v16 = 0 & v15 = % 19.49/3.51 | 0 & v13 = 0 & ? [v17: $i] : (sdtasdt0(v6, v17) = % 19.49/3.51 | v12 & aInteger0(v17) = 0 & $i(v17) & $i(v12)))))) % 19.49/3.51 | & ? [v11: $i] : ? [v12: int] : ( ~ (v12 = 0) & % 19.49/3.51 | aElementOf0(v11, v7) = 0 & aElementOf0(v11, v1) = v12 & % 19.49/3.51 | $i(v11)))))))) % 19.49/3.51 | % 19.49/3.51 | ALPHA: (function-axioms) implies: % 19.49/3.51 | (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 19.49/3.51 | : (v1 = v0 | ~ (aInteger0(v2) = v1) | ~ (aInteger0(v2) = v0)) % 19.49/3.51 | (11) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 19.49/3.51 | : (v1 = v0 | ~ (aSet0(v2) = v1) | ~ (aSet0(v2) = v0)) % 19.49/3.51 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 19.49/3.51 | (sbsmnsldt0(v2) = v1) | ~ (sbsmnsldt0(v2) = v0)) % 19.49/3.51 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 19.49/3.51 | : (v1 = v0 | ~ (isClosed0(v2) = v1) | ~ (isClosed0(v2) = v0)) % 19.49/3.51 | (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 19.49/3.51 | : ! [v3: $i] : (v1 = v0 | ~ (aSubsetOf0(v3, v2) = v1) | ~ % 19.49/3.51 | (aSubsetOf0(v3, v2) = v0)) % 19.49/3.51 | % 19.49/3.51 | DELTA: instantiating (6) with fresh symbols all_42_0, all_42_1 gives: % 19.49/3.52 | (15) stldt0(all_42_1) = cS2076 & sbsmnsldt0(xS) = all_42_1 & % 19.49/3.52 | aSet0(all_42_1) = 0 & aSet0(cS2076) = 0 & smndt0(sz10) = all_42_0 & % 19.49/3.52 | $i(all_42_0) & $i(all_42_1) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | % 19.49/3.52 | ~ (aElementOf0(v0, all_42_1) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 19.49/3.52 | (v2 = 0) & aInteger0(v0) = v2) | ! [v2: $i] : ( ~ % 19.49/3.52 | (aElementOf0(v2, xS) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = % 19.49/3.52 | 0) & aElementOf0(v0, v2) = v3))) & ! [v0: $i] : ! [v1: int] % 19.49/3.52 | : (v1 = 0 | ~ (aElementOf0(v0, cS2076) = v1) | ~ $i(v0) | ? [v2: % 19.49/3.52 | any] : ? [v3: any] : (aElementOf0(v0, all_42_1) = v3 & % 19.49/3.52 | aInteger0(v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! % 19.49/3.52 | [v1: int] : (v1 = 0 | ~ (aElementOf0(v0, cS2076) = v1) | ~ $i(v0) | % 19.49/3.52 | ( ~ (v0 = all_42_0) & ~ (v0 = sz10))) & ! [v0: any] : (v0 = % 19.49/3.52 | all_42_0 | v0 = sz10 | ~ (aElementOf0(v0, cS2076) = 0) | ~ $i(v0)) % 19.49/3.52 | & ! [v0: $i] : ( ~ (aElementOf0(v0, all_42_1) = 0) | ~ $i(v0) | % 19.49/3.52 | (aInteger0(v0) = 0 & ? [v1: $i] : (aElementOf0(v1, xS) = 0 & % 19.49/3.52 | aElementOf0(v0, v1) = 0 & $i(v1)))) & ! [v0: $i] : ( ~ % 19.49/3.52 | (aElementOf0(v0, cS2076) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = % 19.49/3.52 | 0) & aElementOf0(v0, all_42_1) = v1 & aInteger0(v0) = 0)) % 19.49/3.52 | % 19.49/3.52 | ALPHA: (15) implies: % 19.49/3.52 | (16) sbsmnsldt0(xS) = all_42_1 % 19.49/3.52 | % 19.49/3.52 | DELTA: instantiating (5) with fresh symbol all_45_0 gives: % 19.49/3.52 | (17) cS2043 = xS & aSet0(xS) = 0 & smndt0(sz00) = all_45_0 & $i(all_45_0) & % 19.49/3.52 | ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ (aElementOf0(v0, xS) = v1) | % 19.49/3.52 | ~ $i(v0) | ! [v2: $i] : ! [v3: $i] : (v2 = sz00 | ~ % 19.49/3.52 | (szAzrzSzezqlpdtcmdtrp0(sz00, v2) = v3) | ~ $i(v2) | ? [v4: any] % 19.49/3.52 | : ? [v5: any] : ? [v6: any] : (aSet0(v3) = v6 & isPrime0(v2) = % 19.49/3.52 | v5 & aInteger0(v2) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v6 = 0 & % 19.49/3.52 | ~ (v3 = v0) & ! [v7: $i] : ! [v8: $i] : ! [v9: any] : ( % 19.49/3.52 | ~ (aDivisorOf0(v2, v8) = v9) | ~ (sdtpldt0(v7, all_45_0) % 19.49/3.52 | = v8) | ~ $i(v7) | ? [v10: any] : ? [v11: any] : ? % 19.49/3.52 | [v12: any] : (aElementOf0(v7, v3) = v12 & % 19.49/3.52 | sdteqdtlpzmzozddtrp0(v7, sz00, v2) = v11 & aInteger0(v7) % 19.49/3.52 | = v10 & ( ~ (v10 = 0) | v12 = 0 | ( ~ (v11 = 0) & ~ (v9 % 19.49/3.52 | = 0) & ! [v13: $i] : ( ~ (sdtasdt0(v2, v13) = v8) % 19.49/3.52 | | ~ $i(v13) | ? [v14: int] : ( ~ (v14 = 0) & % 19.49/3.52 | aInteger0(v13) = v14)))))) & ! [v7: $i] : ! % 19.49/3.52 | [v8: $i] : ! [v9: any] : ( ~ (aDivisorOf0(v2, v8) = v9) | % 19.49/3.52 | ~ (sdtpldt0(v7, all_45_0) = v8) | ~ $i(v7) | ? [v10: % 19.49/3.52 | any] : ? [v11: any] : ? [v12: any] : (aElementOf0(v7, % 19.49/3.52 | v3) = v10 & sdteqdtlpzmzozddtrp0(v7, sz00, v2) = v12 & % 19.49/3.52 | aInteger0(v7) = v11 & ( ~ (v10 = 0) | (v12 = 0 & v11 = 0 % 19.49/3.52 | & v9 = 0 & ? [v13: $i] : (sdtasdt0(v2, v13) = v8 & % 19.49/3.52 | aInteger0(v13) = 0 & $i(v13) & $i(v8))))))))))) & % 19.49/3.52 | ! [v0: $i] : ( ~ (aElementOf0(v0, xS) = 0) | ~ $i(v0) | ? [v1: $i] : % 19.49/3.52 | ( ~ (v1 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0 & aSet0(v0) % 19.49/3.52 | = 0 & isPrime0(v1) = 0 & aInteger0(v1) = 0 & $i(v1) & ! [v2: $i] % 19.49/3.52 | : ! [v3: $i] : ! [v4: any] : ( ~ (aDivisorOf0(v1, v3) = v4) | ~ % 19.49/3.52 | (sdtpldt0(v2, all_45_0) = v3) | ~ $i(v2) | ? [v5: any] : ? % 19.49/3.52 | [v6: any] : ? [v7: any] : (aElementOf0(v2, v0) = v7 & % 19.49/3.52 | sdteqdtlpzmzozddtrp0(v2, sz00, v1) = v6 & aInteger0(v2) = v5 & % 19.49/3.52 | ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v4 = 0) & ! [v8: % 19.49/3.52 | $i] : ( ~ (sdtasdt0(v1, v8) = v3) | ~ $i(v8) | ? [v9: % 19.49/3.52 | int] : ( ~ (v9 = 0) & aInteger0(v8) = v9)))))) & ! % 19.49/3.52 | [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ (aDivisorOf0(v1, v3) = % 19.49/3.52 | v4) | ~ (sdtpldt0(v2, all_45_0) = v3) | ~ $i(v2) | ? [v5: % 19.49/3.52 | any] : ? [v6: any] : ? [v7: any] : (aElementOf0(v2, v0) = v5 % 19.49/3.52 | & sdteqdtlpzmzozddtrp0(v2, sz00, v1) = v7 & aInteger0(v2) = v6 % 19.49/3.52 | & ( ~ (v5 = 0) | (v7 = 0 & v6 = 0 & v4 = 0 & ? [v8: $i] : % 19.49/3.52 | (sdtasdt0(v1, v8) = v3 & aInteger0(v8) = 0 & $i(v8) & % 19.49/3.52 | $i(v3)))))))) % 19.49/3.52 | % 19.49/3.52 | ALPHA: (17) implies: % 19.49/3.52 | (18) cS2043 = xS % 19.49/3.52 | (19) smndt0(sz00) = all_45_0 % 19.49/3.52 | (20) aSet0(xS) = 0 % 19.49/3.52 | (21) ! [v0: $i] : ( ~ (aElementOf0(v0, xS) = 0) | ~ $i(v0) | ? [v1: $i] % 19.49/3.52 | : ( ~ (v1 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v1) = v0 & % 19.49/3.52 | aSet0(v0) = 0 & isPrime0(v1) = 0 & aInteger0(v1) = 0 & $i(v1) & ! % 19.49/3.53 | [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ (aDivisorOf0(v1, v3) = % 19.49/3.53 | v4) | ~ (sdtpldt0(v2, all_45_0) = v3) | ~ $i(v2) | ? [v5: % 19.49/3.53 | any] : ? [v6: any] : ? [v7: any] : (aElementOf0(v2, v0) = v7 % 19.49/3.53 | & sdteqdtlpzmzozddtrp0(v2, sz00, v1) = v6 & aInteger0(v2) = v5 % 19.49/3.53 | & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v4 = 0) & ! [v8: % 19.49/3.53 | $i] : ( ~ (sdtasdt0(v1, v8) = v3) | ~ $i(v8) | ? [v9: % 19.49/3.53 | int] : ( ~ (v9 = 0) & aInteger0(v8) = v9)))))) & ! % 19.49/3.53 | [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ (aDivisorOf0(v1, v3) = % 19.49/3.53 | v4) | ~ (sdtpldt0(v2, all_45_0) = v3) | ~ $i(v2) | ? [v5: % 19.49/3.53 | any] : ? [v6: any] : ? [v7: any] : (aElementOf0(v2, v0) = v5 % 19.49/3.53 | & sdteqdtlpzmzozddtrp0(v2, sz00, v1) = v7 & aInteger0(v2) = v6 % 19.49/3.53 | & ( ~ (v5 = 0) | (v7 = 0 & v6 = 0 & v4 = 0 & ? [v8: $i] : % 19.49/3.53 | (sdtasdt0(v1, v8) = v3 & aInteger0(v8) = 0 & $i(v8) & % 19.49/3.53 | $i(v3)))))))) % 19.49/3.53 | % 19.49/3.53 | DELTA: instantiating (9) with fresh symbols all_48_0, all_48_1, all_48_2, % 19.49/3.53 | all_48_3 gives: % 19.49/3.53 | (22) ~ (all_48_0 = 0) & ~ (all_48_1 = 0) & isClosed0(all_48_3) = all_48_0 % 19.49/3.53 | & isOpen0(all_48_2) = all_48_1 & stldt0(all_48_3) = all_48_2 & % 19.49/3.53 | sbsmnsldt0(xS) = all_48_3 & aSet0(all_48_3) = 0 & $i(all_48_2) & % 19.49/3.53 | $i(all_48_3) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ % 19.49/3.53 | (aElementOf0(v0, all_48_2) = v1) | ~ $i(v0) | ? [v2: any] : ? % 19.49/3.53 | [v3: any] : (aElementOf0(v0, all_48_3) = v3 & aInteger0(v0) = v2 & ( % 19.49/3.53 | ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | % 19.49/3.53 | ~ (aElementOf0(v0, all_48_3) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 19.49/3.53 | (v2 = 0) & aInteger0(v0) = v2) | ! [v2: $i] : ( ~ % 19.49/3.53 | (aElementOf0(v2, xS) = 0) | ~ $i(v2) | ? [v3: int] : ( ~ (v3 = % 19.49/3.53 | 0) & aElementOf0(v0, v2) = v3))) & ! [v0: $i] : ( ~ % 19.49/3.53 | (aElementOf0(v0, all_48_2) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 19.49/3.53 | = 0) & aElementOf0(v0, all_48_3) = v1 & aInteger0(v0) = 0)) & ! % 19.49/3.53 | [v0: $i] : ( ~ (aElementOf0(v0, all_48_3) = 0) | ~ $i(v0) | % 19.49/3.53 | (aInteger0(v0) = 0 & ? [v1: $i] : (aElementOf0(v1, xS) = 0 & % 19.49/3.53 | aElementOf0(v0, v1) = 0 & $i(v1)))) & ? [v0: $i] : ? [v1: $i] % 19.49/3.53 | : (aElementOf0(v0, all_48_2) = 0 & smndt0(v0) = v1 & $i(v1) & $i(v0) & % 19.49/3.53 | ! [v2: $i] : ! [v3: $i] : (v2 = sz00 | ~ % 19.49/3.53 | (szAzrzSzezqlpdtcmdtrp0(v0, v2) = v3) | ~ $i(v2) | ? [v4: any] : % 19.49/3.53 | ? [v5: any] : ? [v6: any] : (aSubsetOf0(v3, all_48_2) = v6 & % 19.49/3.53 | aSet0(v3) = v5 & aInteger0(v2) = v4 & ( ~ (v4 = 0) | (v5 = 0 & % 19.49/3.53 | ~ (v6 = 0) & ! [v7: $i] : ! [v8: $i] : ! [v9: any] : ( ~ % 19.49/3.53 | (aDivisorOf0(v2, v8) = v9) | ~ (sdtpldt0(v7, v1) = v8) | % 19.49/3.53 | ~ $i(v7) | ? [v10: any] : ? [v11: any] : ? [v12: any] : % 19.49/3.53 | (aElementOf0(v7, v3) = v12 & sdteqdtlpzmzozddtrp0(v7, v0, % 19.49/3.53 | v2) = v11 & aInteger0(v7) = v10 & ( ~ (v10 = 0) | v12 % 19.49/3.53 | = 0 | ( ~ (v11 = 0) & ~ (v9 = 0) & ! [v13: $i] : ( ~ % 19.49/3.53 | (sdtasdt0(v2, v13) = v8) | ~ $i(v13) | ? [v14: % 19.49/3.53 | int] : ( ~ (v14 = 0) & aInteger0(v13) = % 19.49/3.53 | v14)))))) & ! [v7: $i] : ! [v8: $i] : ! [v9: % 19.49/3.53 | any] : ( ~ (aDivisorOf0(v2, v8) = v9) | ~ (sdtpldt0(v7, % 19.49/3.53 | v1) = v8) | ~ $i(v7) | ? [v10: any] : ? [v11: any] % 19.49/3.53 | : ? [v12: any] : (aElementOf0(v7, v3) = v10 & % 19.49/3.53 | sdteqdtlpzmzozddtrp0(v7, v0, v2) = v12 & aInteger0(v7) = % 19.49/3.53 | v11 & ( ~ (v10 = 0) | (v12 = 0 & v11 = 0 & v9 = 0 & ? % 19.49/3.53 | [v13: $i] : (sdtasdt0(v2, v13) = v8 & aInteger0(v13) % 19.49/3.53 | = 0 & $i(v13) & $i(v8)))))) & ? [v7: $i] : ? % 19.49/3.53 | [v8: int] : ( ~ (v8 = 0) & aElementOf0(v7, v3) = 0 & % 19.49/3.53 | aElementOf0(v7, all_48_2) = v8 & $i(v7))))))) % 19.49/3.53 | % 19.49/3.53 | ALPHA: (22) implies: % 19.49/3.53 | (23) ~ (all_48_0 = 0) % 19.49/3.53 | (24) sbsmnsldt0(xS) = all_48_3 % 19.49/3.53 | (25) isClosed0(all_48_3) = all_48_0 % 19.49/3.53 | % 19.49/3.53 | REDUCE: (4), (18) imply: % 19.49/3.53 | (26) $i(xS) % 19.49/3.53 | % 19.49/3.53 | GROUND_INST: instantiating (12) with all_42_1, all_48_3, xS, simplifying with % 19.49/3.53 | (16), (24) gives: % 19.49/3.53 | (27) all_48_3 = all_42_1 % 19.49/3.53 | % 19.49/3.53 | REDUCE: (25), (27) imply: % 19.49/3.53 | (28) isClosed0(all_42_1) = all_48_0 % 19.49/3.53 | % 19.49/3.53 | GROUND_INST: instantiating (mIntNeg) with sz00, all_45_0, simplifying with % 19.49/3.53 | (8), (19) gives: % 19.49/3.53 | (29) ? [v0: any] : ? [v1: any] : (aInteger0(all_45_0) = v1 & % 19.49/3.53 | aInteger0(sz00) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 19.49/3.53 | % 19.49/3.53 | GROUND_INST: instantiating (2) with xS, simplifying with (7), (26) gives: % 19.49/3.53 | (30) ? [v0: any] : ? [v1: $i] : ? [v2: any] : (isClosed0(v1) = v2 & % 19.49/3.53 | sbsmnsldt0(xS) = v1 & aSet0(xS) = v0 & $i(v1) & ( ~ (v0 = 0) | v2 = % 19.49/3.53 | 0)) | ? [v0: $i] : ? [v1: any] : ? [v2: any] : (isClosed0(v0) = % 19.49/3.53 | v2 & aSubsetOf0(v0, cS1395) = v1 & aElementOf0(v0, xS) = 0 & $i(v0) % 19.49/3.53 | & ( ~ (v2 = 0) | ~ (v1 = 0))) % 19.49/3.53 | % 19.49/3.53 | DELTA: instantiating (29) with fresh symbols all_75_0, all_75_1 gives: % 19.49/3.53 | (31) aInteger0(all_45_0) = all_75_0 & aInteger0(sz00) = all_75_1 & ( ~ % 19.49/3.53 | (all_75_1 = 0) | all_75_0 = 0) % 19.49/3.53 | % 19.49/3.53 | ALPHA: (31) implies: % 19.49/3.53 | (32) aInteger0(sz00) = all_75_1 % 19.49/3.53 | (33) ~ (all_75_1 = 0) | all_75_0 = 0 % 19.49/3.53 | % 19.49/3.53 | BETA: splitting (30) gives: % 19.49/3.53 | % 19.49/3.54 | Case 1: % 19.49/3.54 | | % 19.49/3.54 | | (34) ? [v0: any] : ? [v1: $i] : ? [v2: any] : (isClosed0(v1) = v2 & % 19.49/3.54 | | sbsmnsldt0(xS) = v1 & aSet0(xS) = v0 & $i(v1) & ( ~ (v0 = 0) | v2 % 19.49/3.54 | | = 0)) % 19.49/3.54 | | % 19.49/3.54 | | DELTA: instantiating (34) with fresh symbols all_84_0, all_84_1, all_84_2 % 19.49/3.54 | | gives: % 19.49/3.54 | | (35) isClosed0(all_84_1) = all_84_0 & sbsmnsldt0(xS) = all_84_1 & % 19.49/3.54 | | aSet0(xS) = all_84_2 & $i(all_84_1) & ( ~ (all_84_2 = 0) | all_84_0 % 19.49/3.54 | | = 0) % 19.49/3.54 | | % 19.49/3.54 | | ALPHA: (35) implies: % 19.49/3.54 | | (36) aSet0(xS) = all_84_2 % 19.49/3.54 | | (37) sbsmnsldt0(xS) = all_84_1 % 19.49/3.54 | | (38) isClosed0(all_84_1) = all_84_0 % 19.49/3.54 | | (39) ~ (all_84_2 = 0) | all_84_0 = 0 % 19.49/3.54 | | % 19.49/3.54 | | GROUND_INST: instantiating (11) with 0, all_84_2, xS, simplifying with (20), % 19.49/3.54 | | (36) gives: % 19.49/3.54 | | (40) all_84_2 = 0 % 19.49/3.54 | | % 19.49/3.54 | | GROUND_INST: instantiating (12) with all_42_1, all_84_1, xS, simplifying % 19.49/3.54 | | with (16), (37) gives: % 19.49/3.54 | | (41) all_84_1 = all_42_1 % 19.49/3.54 | | % 19.49/3.54 | | REDUCE: (38), (41) imply: % 19.49/3.54 | | (42) isClosed0(all_42_1) = all_84_0 % 19.49/3.54 | | % 19.49/3.54 | | BETA: splitting (39) gives: % 19.49/3.54 | | % 19.49/3.54 | | Case 1: % 19.49/3.54 | | | % 19.49/3.54 | | | (43) ~ (all_84_2 = 0) % 19.49/3.54 | | | % 19.49/3.54 | | | REDUCE: (40), (43) imply: % 19.49/3.54 | | | (44) $false % 19.49/3.54 | | | % 19.49/3.54 | | | CLOSE: (44) is inconsistent. % 19.49/3.54 | | | % 19.49/3.54 | | Case 2: % 19.49/3.54 | | | % 19.49/3.54 | | | (45) all_84_0 = 0 % 19.49/3.54 | | | % 19.49/3.54 | | | REDUCE: (42), (45) imply: % 19.49/3.54 | | | (46) isClosed0(all_42_1) = 0 % 19.49/3.54 | | | % 19.49/3.54 | | | GROUND_INST: instantiating (13) with all_48_0, 0, all_42_1, simplifying % 19.49/3.54 | | | with (28), (46) gives: % 19.49/3.54 | | | (47) all_48_0 = 0 % 19.49/3.54 | | | % 19.49/3.54 | | | REDUCE: (23), (47) imply: % 19.49/3.54 | | | (48) $false % 19.49/3.54 | | | % 19.49/3.54 | | | CLOSE: (48) is inconsistent. % 19.49/3.54 | | | % 19.49/3.54 | | End of split % 19.49/3.54 | | % 19.49/3.54 | Case 2: % 19.49/3.54 | | % 19.49/3.54 | | (49) ? [v0: $i] : ? [v1: any] : ? [v2: any] : (isClosed0(v0) = v2 & % 19.49/3.54 | | aSubsetOf0(v0, cS1395) = v1 & aElementOf0(v0, xS) = 0 & $i(v0) & ( % 19.49/3.54 | | ~ (v2 = 0) | ~ (v1 = 0))) % 19.49/3.54 | | % 19.49/3.54 | | DELTA: instantiating (49) with fresh symbols all_84_0, all_84_1, all_84_2 % 19.49/3.54 | | gives: % 19.49/3.54 | | (50) isClosed0(all_84_2) = all_84_0 & aSubsetOf0(all_84_2, cS1395) = % 19.49/3.54 | | all_84_1 & aElementOf0(all_84_2, xS) = 0 & $i(all_84_2) & ( ~ % 19.49/3.54 | | (all_84_0 = 0) | ~ (all_84_1 = 0)) % 19.49/3.54 | | % 19.49/3.54 | | ALPHA: (50) implies: % 19.49/3.54 | | (51) $i(all_84_2) % 19.49/3.54 | | (52) aElementOf0(all_84_2, xS) = 0 % 19.49/3.54 | | (53) aSubsetOf0(all_84_2, cS1395) = all_84_1 % 19.49/3.54 | | (54) isClosed0(all_84_2) = all_84_0 % 19.49/3.54 | | (55) ~ (all_84_0 = 0) | ~ (all_84_1 = 0) % 19.49/3.54 | | % 19.49/3.54 | | GROUND_INST: instantiating (10) with 0, all_75_1, sz00, simplifying with % 19.49/3.54 | | (1), (32) gives: % 19.49/3.54 | | (56) all_75_1 = 0 % 19.49/3.54 | | % 19.49/3.54 | | BETA: splitting (33) gives: % 19.49/3.54 | | % 19.49/3.54 | | Case 1: % 19.49/3.54 | | | % 19.49/3.54 | | | (57) ~ (all_75_1 = 0) % 19.49/3.54 | | | % 19.49/3.54 | | | REDUCE: (56), (57) imply: % 19.49/3.54 | | | (58) $false % 19.49/3.54 | | | % 19.49/3.54 | | | CLOSE: (58) is inconsistent. % 19.49/3.54 | | | % 19.49/3.54 | | Case 2: % 19.49/3.54 | | | % 19.49/3.54 | | | % 19.49/3.54 | | | GROUND_INST: instantiating (21) with all_84_2, simplifying with (51), (52) % 19.49/3.54 | | | gives: % 19.49/3.54 | | | (59) ? [v0: $i] : ( ~ (v0 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, v0) = % 19.49/3.54 | | | all_84_2 & aSet0(all_84_2) = 0 & isPrime0(v0) = 0 & % 19.49/3.54 | | | aInteger0(v0) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: % 19.49/3.54 | | | any] : ( ~ (aDivisorOf0(v0, v2) = v3) | ~ (sdtpldt0(v1, % 19.49/3.54 | | | all_45_0) = v2) | ~ $i(v1) | ? [v4: any] : ? [v5: any] % 19.49/3.54 | | | : ? [v6: any] : (aElementOf0(v1, all_84_2) = v6 & % 19.49/3.54 | | | sdteqdtlpzmzozddtrp0(v1, sz00, v0) = v5 & aInteger0(v1) = v4 % 19.49/3.54 | | | & ( ~ (v4 = 0) | v6 = 0 | ( ~ (v5 = 0) & ~ (v3 = 0) & ! % 19.49/3.54 | | | [v7: $i] : ( ~ (sdtasdt0(v0, v7) = v2) | ~ $i(v7) | ? % 19.49/3.54 | | | [v8: int] : ( ~ (v8 = 0) & aInteger0(v7) = v8)))))) & % 19.49/3.54 | | | ! [v1: $i] : ! [v2: $i] : ! [v3: any] : ( ~ (aDivisorOf0(v0, % 19.49/3.54 | | | v2) = v3) | ~ (sdtpldt0(v1, all_45_0) = v2) | ~ $i(v1) | % 19.49/3.54 | | | ? [v4: any] : ? [v5: any] : ? [v6: any] : (aElementOf0(v1, % 19.49/3.54 | | | all_84_2) = v4 & sdteqdtlpzmzozddtrp0(v1, sz00, v0) = v6 & % 19.49/3.54 | | | aInteger0(v1) = v5 & ( ~ (v4 = 0) | (v6 = 0 & v5 = 0 & v3 = % 19.49/3.54 | | | 0 & ? [v7: $i] : (sdtasdt0(v0, v7) = v2 & aInteger0(v7) % 19.49/3.54 | | | = 0 & $i(v7) & $i(v2))))))) % 19.49/3.54 | | | % 19.49/3.54 | | | DELTA: instantiating (59) with fresh symbol all_111_0 gives: % 19.49/3.55 | | | (60) ~ (all_111_0 = sz00) & szAzrzSzezqlpdtcmdtrp0(sz00, all_111_0) = % 19.49/3.55 | | | all_84_2 & aSet0(all_84_2) = 0 & isPrime0(all_111_0) = 0 & % 19.49/3.55 | | | aInteger0(all_111_0) = 0 & $i(all_111_0) & ! [v0: $i] : ! [v1: % 19.49/3.55 | | | $i] : ! [v2: any] : ( ~ (aDivisorOf0(all_111_0, v1) = v2) | ~ % 19.49/3.55 | | | (sdtpldt0(v0, all_45_0) = v1) | ~ $i(v0) | ? [v3: any] : ? % 19.49/3.55 | | | [v4: any] : ? [v5: any] : (aElementOf0(v0, all_84_2) = v5 & % 19.49/3.55 | | | sdteqdtlpzmzozddtrp0(v0, sz00, all_111_0) = v4 & aInteger0(v0) % 19.49/3.55 | | | = v3 & ( ~ (v3 = 0) | v5 = 0 | ( ~ (v4 = 0) & ~ (v2 = 0) & ! % 19.49/3.55 | | | [v6: $i] : ( ~ (sdtasdt0(all_111_0, v6) = v1) | ~ $i(v6) % 19.49/3.55 | | | | ? [v7: int] : ( ~ (v7 = 0) & aInteger0(v6) = v7)))))) % 19.49/3.55 | | | & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 19.49/3.55 | | | (aDivisorOf0(all_111_0, v1) = v2) | ~ (sdtpldt0(v0, all_45_0) = % 19.49/3.55 | | | v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 19.49/3.55 | | | (aElementOf0(v0, all_84_2) = v3 & sdteqdtlpzmzozddtrp0(v0, sz00, % 19.49/3.55 | | | all_111_0) = v5 & aInteger0(v0) = v4 & ( ~ (v3 = 0) | (v5 = % 19.49/3.55 | | | 0 & v4 = 0 & v2 = 0 & ? [v6: $i] : (sdtasdt0(all_111_0, % 19.49/3.55 | | | v6) = v1 & aInteger0(v6) = 0 & $i(v6) & $i(v1)))))) % 19.49/3.55 | | | % 19.49/3.55 | | | ALPHA: (60) implies: % 19.49/3.55 | | | (61) ~ (all_111_0 = sz00) % 19.49/3.55 | | | (62) $i(all_111_0) % 19.49/3.55 | | | (63) aInteger0(all_111_0) = 0 % 19.49/3.55 | | | (64) szAzrzSzezqlpdtcmdtrp0(sz00, all_111_0) = all_84_2 % 19.49/3.55 | | | % 19.49/3.55 | | | GROUND_INST: instantiating (3) with sz00, all_111_0, all_84_2, simplifying % 19.49/3.55 | | | with (8), (62), (64) gives: % 19.49/3.55 | | | (65) all_111_0 = sz00 | ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 19.49/3.55 | | | [v3: any] : (isClosed0(all_84_2) = v3 & aSubsetOf0(all_84_2, % 19.49/3.55 | | | cS1395) = v2 & aInteger0(all_111_0) = v1 & aInteger0(sz00) = % 19.49/3.55 | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & v2 = 0))) % 19.49/3.55 | | | % 19.49/3.55 | | | BETA: splitting (65) gives: % 19.49/3.55 | | | % 19.49/3.55 | | | Case 1: % 19.49/3.55 | | | | % 19.49/3.55 | | | | (66) all_111_0 = sz00 % 19.49/3.55 | | | | % 19.49/3.55 | | | | REDUCE: (61), (66) imply: % 19.49/3.55 | | | | (67) $false % 19.49/3.55 | | | | % 19.49/3.55 | | | | CLOSE: (67) is inconsistent. % 19.49/3.55 | | | | % 19.49/3.55 | | | Case 2: % 19.49/3.55 | | | | % 19.49/3.55 | | | | (68) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 19.49/3.55 | | | | (isClosed0(all_84_2) = v3 & aSubsetOf0(all_84_2, cS1395) = v2 & % 19.49/3.55 | | | | aInteger0(all_111_0) = v1 & aInteger0(sz00) = v0 & ( ~ (v1 = % 19.49/3.55 | | | | 0) | ~ (v0 = 0) | (v3 = 0 & v2 = 0))) % 19.49/3.55 | | | | % 19.49/3.55 | | | | DELTA: instantiating (68) with fresh symbols all_141_0, all_141_1, % 19.49/3.55 | | | | all_141_2, all_141_3 gives: % 19.49/3.55 | | | | (69) isClosed0(all_84_2) = all_141_0 & aSubsetOf0(all_84_2, cS1395) = % 19.49/3.55 | | | | all_141_1 & aInteger0(all_111_0) = all_141_2 & aInteger0(sz00) = % 19.49/3.55 | | | | all_141_3 & ( ~ (all_141_2 = 0) | ~ (all_141_3 = 0) | % 19.49/3.55 | | | | (all_141_0 = 0 & all_141_1 = 0)) % 19.49/3.55 | | | | % 19.49/3.55 | | | | ALPHA: (69) implies: % 19.49/3.55 | | | | (70) aInteger0(sz00) = all_141_3 % 19.49/3.55 | | | | (71) aInteger0(all_111_0) = all_141_2 % 19.49/3.55 | | | | (72) aSubsetOf0(all_84_2, cS1395) = all_141_1 % 19.49/3.55 | | | | (73) isClosed0(all_84_2) = all_141_0 % 19.49/3.55 | | | | (74) ~ (all_141_2 = 0) | ~ (all_141_3 = 0) | (all_141_0 = 0 & % 19.49/3.55 | | | | all_141_1 = 0) % 19.49/3.55 | | | | % 19.49/3.55 | | | | GROUND_INST: instantiating (10) with 0, all_141_3, sz00, simplifying % 19.49/3.55 | | | | with (1), (70) gives: % 19.49/3.55 | | | | (75) all_141_3 = 0 % 19.49/3.55 | | | | % 19.49/3.55 | | | | GROUND_INST: instantiating (10) with 0, all_141_2, all_111_0, % 19.49/3.55 | | | | simplifying with (63), (71) gives: % 19.49/3.55 | | | | (76) all_141_2 = 0 % 19.49/3.55 | | | | % 19.49/3.55 | | | | GROUND_INST: instantiating (14) with all_84_1, all_141_1, cS1395, % 19.49/3.55 | | | | all_84_2, simplifying with (53), (72) gives: % 19.49/3.55 | | | | (77) all_141_1 = all_84_1 % 19.49/3.55 | | | | % 19.49/3.55 | | | | GROUND_INST: instantiating (13) with all_84_0, all_141_0, all_84_2, % 19.49/3.55 | | | | simplifying with (54), (73) gives: % 19.49/3.55 | | | | (78) all_141_0 = all_84_0 % 19.49/3.55 | | | | % 19.49/3.55 | | | | BETA: splitting (74) gives: % 19.49/3.55 | | | | % 19.49/3.55 | | | | Case 1: % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | (79) ~ (all_141_2 = 0) % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | REDUCE: (76), (79) imply: % 19.49/3.55 | | | | | (80) $false % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | CLOSE: (80) is inconsistent. % 19.49/3.55 | | | | | % 19.49/3.55 | | | | Case 2: % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | (81) ~ (all_141_3 = 0) | (all_141_0 = 0 & all_141_1 = 0) % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | BETA: splitting (81) gives: % 19.49/3.55 | | | | | % 19.49/3.55 | | | | | Case 1: % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | (82) ~ (all_141_3 = 0) % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | REDUCE: (75), (82) imply: % 19.49/3.55 | | | | | | (83) $false % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | CLOSE: (83) is inconsistent. % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | Case 2: % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | (84) all_141_0 = 0 & all_141_1 = 0 % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | ALPHA: (84) implies: % 19.49/3.55 | | | | | | (85) all_141_1 = 0 % 19.49/3.55 | | | | | | (86) all_141_0 = 0 % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | COMBINE_EQS: (78), (86) imply: % 19.49/3.55 | | | | | | (87) all_84_0 = 0 % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | COMBINE_EQS: (77), (85) imply: % 19.49/3.55 | | | | | | (88) all_84_1 = 0 % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | SIMP: (88) implies: % 19.49/3.55 | | | | | | (89) all_84_1 = 0 % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | BETA: splitting (55) gives: % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | | Case 1: % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | (90) ~ (all_84_0 = 0) % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | REDUCE: (87), (90) imply: % 19.49/3.55 | | | | | | | (91) $false % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | CLOSE: (91) is inconsistent. % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | Case 2: % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | (92) ~ (all_84_1 = 0) % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | REDUCE: (89), (92) imply: % 19.49/3.55 | | | | | | | (93) $false % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | | CLOSE: (93) is inconsistent. % 19.49/3.55 | | | | | | | % 19.49/3.55 | | | | | | End of split % 19.49/3.55 | | | | | | % 19.49/3.55 | | | | | End of split % 19.49/3.55 | | | | | % 19.49/3.55 | | | | End of split % 19.49/3.55 | | | | % 19.49/3.55 | | | End of split % 19.49/3.55 | | | % 19.49/3.55 | | End of split % 19.49/3.55 | | % 19.49/3.55 | End of split % 19.49/3.55 | % 19.49/3.55 End of proof % 19.49/3.55 % SZS output end Proof for theBenchmark % 19.49/3.55 % 19.49/3.55 2947ms %------------------------------------------------------------------------------