%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : LAT385+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%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 : 300s % DateTime : Thu Aug 31 06:25:18 EDT 2023 % Result : Theorem 153.35s 21.22s % Output : Proof 154.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : LAT385+4 : TPTP v8.1.2. Released v4.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n013.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Aug 24 07:14:47 EDT 2023 % 0.12/0.35 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 3.75/1.26 Prover 1: Preprocessing ... % 3.75/1.26 Prover 4: Preprocessing ... % 3.75/1.30 Prover 2: Preprocessing ... % 3.75/1.30 Prover 0: Preprocessing ... % 3.75/1.30 Prover 5: Preprocessing ... % 3.75/1.30 Prover 6: Preprocessing ... % 3.75/1.30 Prover 3: Preprocessing ... % 9.15/2.08 Prover 5: Proving ... % 9.15/2.11 Prover 2: Proving ... % 9.15/2.14 Prover 1: Constructing countermodel ... % 9.15/2.17 Prover 6: Proving ... % 9.15/2.18 Prover 3: Constructing countermodel ... % 11.79/2.41 Prover 3: gave up % 11.79/2.42 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.79/2.48 Prover 4: Constructing countermodel ... % 11.79/2.50 Prover 7: Preprocessing ... % 13.21/2.62 Prover 0: Proving ... % 13.21/2.63 Prover 7: Constructing countermodel ... % 14.53/2.85 Prover 1: gave up % 14.53/2.86 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.57/2.92 Prover 8: Preprocessing ... % 17.79/3.20 Prover 8: Warning: ignoring some quantifiers % 17.90/3.23 Prover 8: Constructing countermodel ... % 20.98/3.67 Prover 8: gave up % 20.98/3.67 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 21.60/3.73 Prover 9: Preprocessing ... % 26.40/4.34 Prover 9: Constructing countermodel ... % 60.99/8.88 Prover 2: stopped % 60.99/8.89 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 61.69/8.98 Prover 10: Preprocessing ... % 61.69/9.06 Prover 10: Constructing countermodel ... % 99.33/13.96 Prover 5: stopped % 99.33/13.96 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 100.56/14.07 Prover 11: Preprocessing ... % 101.87/14.29 Prover 11: Constructing countermodel ... % 128.35/17.87 Prover 6: stopped % 128.35/17.87 Prover 12: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=2024365391 % 128.76/17.92 Prover 12: Preprocessing ... % 129.77/18.10 Prover 12: Proving ... % 138.53/19.21 Prover 12: stopped % 138.53/19.22 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 139.22/19.27 Prover 13: Preprocessing ... % 139.57/19.31 Prover 13: Constructing countermodel ... % 153.35/21.18 Prover 13: Found proof (size 24) % 153.35/21.19 Prover 13: proved (1964ms) % 153.35/21.19 Prover 9: stopped % 153.35/21.19 Prover 10: stopped % 153.35/21.19 Prover 0: stopped % 153.35/21.19 Prover 7: stopped % 153.35/21.22 Prover 4: stopped % 153.35/21.22 Prover 11: stopped % 153.35/21.22 % 153.35/21.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 153.35/21.22 % 153.35/21.22 % SZS output start Proof for theBenchmark % 153.35/21.23 Assumptions after simplification: % 153.35/21.23 --------------------------------- % 153.35/21.23 % 153.35/21.23 (mDefSub) % 153.35/21.23 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 153.35/21.23 ~ aSubsetOf0(v1, v0) | ~ aElementOf0(v2, v1) | ~ aSet0(v0) | % 153.35/21.23 aElementOf0(v2, v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | % 153.35/21.23 ~ aSubsetOf0(v1, v0) | ~ aSet0(v0) | aSet0(v1)) & ! [v0: $i] : ! [v1: $i] % 153.35/21.23 : ( ~ $i(v1) | ~ $i(v0) | ~ aSet0(v1) | ~ aSet0(v0) | aSubsetOf0(v1, v0) | % 153.35/21.23 ? [v2: $i] : ($i(v2) & aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) % 153.35/21.23 % 153.35/21.23 (m__) % 153.35/21.24 $i(xP) & $i(xU) & ! [v0: $i] : ( ~ $i(v0) | ~ aInfimumOfIn0(v0, xP, xU)) & % 153.35/21.24 ! [v0: $i] : ( ~ $i(v0) | ~ aLowerBoundOfIn0(v0, xP, xU) | ~ aElementOf0(v0, % 153.35/21.24 xU) | ? [v1: $i] : ($i(v1) & aLowerBoundOfIn0(v1, xP, xU) & % 153.35/21.24 aElementOf0(v1, xU) & ~ sdtlseqdt0(v1, v0) & ! [v2: $i] : ( ~ $i(v2) | % 153.35/21.24 ~ aElementOf0(v2, xP) | sdtlseqdt0(v1, v2)))) & ! [v0: $i] : ( ~ $i(v0) % 153.35/21.24 | ~ aElementOf0(v0, xU) | ? [v1: $i] : ($i(v1) & ((aLowerBoundOfIn0(v1, % 153.35/21.24 xP, xU) & aElementOf0(v1, xU) & ~ sdtlseqdt0(v1, v0) & ! [v2: $i] % 153.35/21.24 : ( ~ $i(v2) | ~ aElementOf0(v2, xP) | sdtlseqdt0(v1, v2))) | % 153.35/21.24 (aElementOf0(v1, xP) & ~ sdtlseqdt0(v0, v1))))) % 153.35/21.24 % 153.35/21.24 (m__1123) % 153.84/21.27 szRzazndt0(xf) = xU & szDzozmdt0(xf) = xU & $i(xf) & $i(xU) & isMonotone0(xf) % 153.84/21.27 & isOn0(xf, xU) & aFunction0(xf) & aCompleteLattice0(xU) & aSet0(xU) & ! [v0: % 153.84/21.27 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (sdtlpdtrp0(xf, v1) = % 153.84/21.27 v3) | ~ (sdtlpdtrp0(xf, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 153.84/21.27 sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, xU) | ~ aElementOf0(v0, xU) | % 153.84/21.27 sdtlseqdt0(v2, v3)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | % 153.84/21.27 ~ sdtlseqdt0(v0, v1) | ~ aElementOf0(v1, xU) | ~ aElementOf0(v0, xU) | ? % 153.84/21.27 [v2: $i] : ? [v3: $i] : (sdtlpdtrp0(xf, v1) = v3 & sdtlpdtrp0(xf, v0) = v2 % 153.84/21.27 & $i(v3) & $i(v2) & sdtlseqdt0(v2, v3))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 153.84/21.27 aSubsetOf0(v0, xU) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 153.84/21.27 aSupremumOfIn0(v2, v0, xU) & aInfimumOfIn0(v1, v0, xU) & % 153.84/21.27 aUpperBoundOfIn0(v2, v0, xU) & aLowerBoundOfIn0(v1, v0, xU) & % 153.84/21.27 aElementOf0(v2, xU) & aElementOf0(v1, xU) & ! [v3: $i] : ( ~ $i(v3) | ~ % 153.84/21.27 aUpperBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v2, v3)) & ! [v3: $i] : ( ~ % 153.84/21.27 $i(v3) | ~ aLowerBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v3, v1)) & ! [v3: % 153.84/21.27 $i] : ( ~ $i(v3) | ~ aElementOf0(v3, v0) | sdtlseqdt0(v3, v2)) & ! % 153.84/21.27 [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, v0) | sdtlseqdt0(v1, v3)) & ! % 153.84/21.27 [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, xU) | sdtlseqdt0(v3, v1) | ? % 153.84/21.27 [v4: $i] : ($i(v4) & aElementOf0(v4, v0) & ~ sdtlseqdt0(v3, v4))) & ! % 153.84/21.27 [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, xU) | sdtlseqdt0(v2, v3) | ? % 153.84/21.27 [v4: $i] : ($i(v4) & aElementOf0(v4, v0) & ~ sdtlseqdt0(v4, v3))))) & % 153.84/21.27 ! [v0: $i] : ( ~ $i(v0) | ~ aSet0(v0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & % 153.84/21.27 $i(v1) & ((aSupremumOfIn0(v2, v0, xU) & aInfimumOfIn0(v1, v0, xU) & % 153.84/21.27 aUpperBoundOfIn0(v2, v0, xU) & aLowerBoundOfIn0(v1, v0, xU) & % 153.84/21.27 aElementOf0(v2, xU) & aElementOf0(v1, xU) & ! [v3: $i] : ( ~ $i(v3) | % 153.84/21.27 ~ aUpperBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v2, v3)) & ! [v3: $i] % 153.84/21.27 : ( ~ $i(v3) | ~ aLowerBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v3, v1)) & % 153.84/21.27 ! [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, v0) | sdtlseqdt0(v3, % 153.84/21.27 v2)) & ! [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, v0) | % 153.84/21.27 sdtlseqdt0(v1, v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, % 153.84/21.27 xU) | sdtlseqdt0(v3, v1) | ? [v4: $i] : ($i(v4) & aElementOf0(v4, % 153.84/21.27 v0) & ~ sdtlseqdt0(v3, v4))) & ! [v3: $i] : ( ~ $i(v3) | ~ % 153.84/21.27 aElementOf0(v3, xU) | sdtlseqdt0(v2, v3) | ? [v4: $i] : ($i(v4) & % 153.84/21.27 aElementOf0(v4, v0) & ~ sdtlseqdt0(v4, v3)))) | (aElementOf0(v1, % 153.84/21.27 v0) & ~ aElementOf0(v1, xU))))) % 153.84/21.27 % 153.84/21.27 (m__1144) % 153.84/21.28 $i(xS) & $i(xf) & ? [v0: $i] : (cS1142(xf) = xS & szDzozmdt0(xf) = v0 & % 153.84/21.28 $i(v0) & aSet0(xS) & ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 153.84/21.28 (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ aElementOf0(v1, xS)) & ! [v1: % 153.84/21.28 $i] : ! [v2: $i] : ( ~ (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ % 153.84/21.28 aFixedPointOf0(v1, xf) | aElementOf0(v1, xS)) & ! [v1: $i] : ! [v2: $i] % 153.84/21.28 : ( ~ (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ aElementOf0(v1, xS) | % 153.84/21.28 aFixedPointOf0(v1, xf)) & ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlpdtrp0(xf, % 153.84/21.28 v1) = v2) | ~ $i(v1) | ~ aElementOf0(v1, xS) | aElementOf0(v1, v0)) % 153.84/21.28 & ! [v1: $i] : ( ~ (sdtlpdtrp0(xf, v1) = v1) | ~ $i(v1) | ~ % 153.84/21.28 aElementOf0(v1, v0) | aElementOf0(v1, xS)) & ! [v1: $i] : ( ~ $i(v1) | ~ % 153.84/21.28 aFixedPointOf0(v1, xf) | aElementOf0(v1, xS)) & ! [v1: $i] : ( ~ $i(v1) | % 153.84/21.28 ~ aElementOf0(v1, v0) | aElementOf0(v1, xS) | ? [v2: $i] : ( ~ (v2 = v1) % 153.84/21.28 & sdtlpdtrp0(xf, v1) = v2 & $i(v2))) & ! [v1: $i] : ( ~ $i(v1) | ~ % 153.84/21.28 aElementOf0(v1, xS) | sdtlpdtrp0(xf, v1) = v1) & ! [v1: $i] : ( ~ $i(v1) % 153.84/21.28 | ~ aElementOf0(v1, xS) | aFixedPointOf0(v1, xf)) & ! [v1: $i] : ( ~ % 153.84/21.28 $i(v1) | ~ aElementOf0(v1, xS) | aElementOf0(v1, v0))) % 153.84/21.28 % 153.84/21.28 (m__1244) % 153.84/21.28 cS1241(xU, xf, xT) = xP & $i(xP) & $i(xT) & $i(xf) & $i(xU) & aSet0(xP) & ! % 153.84/21.28 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sdtlpdtrp0(xf, v0) = v1) | ~ % 153.84/21.28 $i(v2) | ~ $i(v0) | ~ aElementOf0(v2, xT) | ~ aElementOf0(v0, xP) | % 153.84/21.28 sdtlseqdt0(v2, v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlpdtrp0(xf, v0) = % 153.84/21.28 v1) | ~ $i(v0) | ~ aUpperBoundOfIn0(v0, xT, xU) | ~ sdtlseqdt0(v1, v0) % 153.84/21.28 | ~ aElementOf0(v0, xU) | aElementOf0(v0, xP)) & ! [v0: $i] : ! [v1: $i] % 153.84/21.28 : ( ~ (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ sdtlseqdt0(v1, v0) | ~ % 153.84/21.28 aElementOf0(v0, xU) | aElementOf0(v0, xP) | ? [v2: $i] : ($i(v2) & % 153.84/21.28 aElementOf0(v2, xT) & ~ sdtlseqdt0(v2, v0))) & ! [v0: $i] : ! [v1: $i] % 153.84/21.28 : ( ~ (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ aElementOf0(v0, xP) | % 153.84/21.28 aUpperBoundOfIn0(v0, xT, xU)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 153.84/21.28 (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ aElementOf0(v0, xP) | % 153.84/21.28 sdtlseqdt0(v1, v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sdtlpdtrp0(xf, v0) = % 153.84/21.28 v1) | ~ $i(v0) | ~ aElementOf0(v0, xP) | aElementOf0(v0, xU)) & ! [v0: % 153.84/21.28 $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ aElementOf0(v1, xT) | ~ % 153.84/21.28 aElementOf0(v0, xP) | sdtlseqdt0(v1, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 153.84/21.28 aUpperBoundOfIn0(v0, xT, xU) | ~ aElementOf0(v0, xU) | aElementOf0(v0, xP) % 153.84/21.28 | ? [v1: $i] : (sdtlpdtrp0(xf, v0) = v1 & $i(v1) & ~ sdtlseqdt0(v1, v0))) % 153.84/21.28 & ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xP) | aUpperBoundOfIn0(v0, xT, % 153.84/21.28 xU)) & ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xP) | aElementOf0(v0, % 153.84/21.28 xU)) & ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xP) | ? [v1: $i] : % 153.84/21.28 (sdtlpdtrp0(xf, v0) = v1 & $i(v1) & sdtlseqdt0(v1, v0))) & ! [v0: $i] : ( ~ % 153.84/21.28 $i(v0) | ~ aElementOf0(v0, xU) | aElementOf0(v0, xP) | ? [v1: $i] : ? % 153.84/21.28 [v2: $i] : ($i(v2) & ((sdtlpdtrp0(xf, v0) = v1 & $i(v1) & ~ sdtlseqdt0(v1, % 153.84/21.28 v0)) | (aElementOf0(v2, xT) & ~ sdtlseqdt0(v2, v0))))) % 153.84/21.28 % 153.84/21.28 (function-axioms) % 153.84/21.29 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 153.84/21.29 | ~ (cS1241(v4, v3, v2) = v1) | ~ (cS1241(v4, v3, v2) = v0)) & ! [v0: $i] % 153.84/21.29 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sdtlpdtrp0(v3, v2) % 153.84/21.29 = v1) | ~ (sdtlpdtrp0(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 153.84/21.29 [v2: $i] : (v1 = v0 | ~ (cS1142(v2) = v1) | ~ (cS1142(v2) = v0)) & ! [v0: % 153.84/21.29 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (szRzazndt0(v2) = v1) | ~ % 153.84/21.29 (szRzazndt0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 153.84/21.29 | ~ (szDzozmdt0(v2) = v1) | ~ (szDzozmdt0(v2) = v0)) % 153.84/21.29 % 153.84/21.29 Further assumptions not needed in the proof: % 153.84/21.29 -------------------------------------------- % 153.84/21.29 mARefl, mASymm, mConMap, mDefCLat, mDefDom, mDefEmpty, mDefFix, mDefInf, mDefLB, % 153.84/21.29 mDefMonot, mDefSup, mDefUB, mDomSort, mEOfElem, mElmSort, mImgSort, mInfUn, % 153.84/21.29 mLessRel, mRanSort, mSetSort, mSupUn, mTrans, m__1173 % 153.84/21.29 % 153.84/21.29 Those formulas are unsatisfiable: % 153.84/21.29 --------------------------------- % 153.84/21.29 % 153.84/21.29 Begin of proof % 153.84/21.29 | % 153.84/21.29 | ALPHA: (mDefSub) implies: % 153.84/21.29 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ aSet0(v1) | ~ % 153.84/21.29 | aSet0(v0) | aSubsetOf0(v1, v0) | ? [v2: $i] : ($i(v2) & % 153.84/21.29 | aElementOf0(v2, v1) & ~ aElementOf0(v2, v0))) % 153.84/21.29 | % 153.84/21.29 | ALPHA: (m__1123) implies: % 153.84/21.29 | (2) aSet0(xU) % 153.84/21.29 | (3) szDzozmdt0(xf) = xU % 154.09/21.29 | (4) ! [v0: $i] : ( ~ $i(v0) | ~ aSubsetOf0(v0, xU) | ? [v1: $i] : ? % 154.09/21.29 | [v2: $i] : ($i(v2) & $i(v1) & aSupremumOfIn0(v2, v0, xU) & % 154.09/21.29 | aInfimumOfIn0(v1, v0, xU) & aUpperBoundOfIn0(v2, v0, xU) & % 154.09/21.29 | aLowerBoundOfIn0(v1, v0, xU) & aElementOf0(v2, xU) & % 154.09/21.29 | aElementOf0(v1, xU) & ! [v3: $i] : ( ~ $i(v3) | ~ % 154.09/21.29 | aUpperBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v2, v3)) & ! [v3: $i] % 154.09/21.29 | : ( ~ $i(v3) | ~ aLowerBoundOfIn0(v3, v0, xU) | sdtlseqdt0(v3, % 154.09/21.29 | v1)) & ! [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, v0) | % 154.09/21.29 | sdtlseqdt0(v3, v2)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 154.09/21.29 | aElementOf0(v3, v0) | sdtlseqdt0(v1, v3)) & ! [v3: $i] : ( ~ % 154.09/21.29 | $i(v3) | ~ aElementOf0(v3, xU) | sdtlseqdt0(v3, v1) | ? [v4: % 154.09/21.29 | $i] : ($i(v4) & aElementOf0(v4, v0) & ~ sdtlseqdt0(v3, v4))) & % 154.09/21.29 | ! [v3: $i] : ( ~ $i(v3) | ~ aElementOf0(v3, xU) | sdtlseqdt0(v2, % 154.09/21.29 | v3) | ? [v4: $i] : ($i(v4) & aElementOf0(v4, v0) & ~ % 154.09/21.29 | sdtlseqdt0(v4, v3))))) % 154.09/21.29 | % 154.09/21.29 | ALPHA: (m__1144) implies: % 154.09/21.30 | (5) ? [v0: $i] : (cS1142(xf) = xS & szDzozmdt0(xf) = v0 & $i(v0) & % 154.09/21.30 | aSet0(xS) & ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (sdtlpdtrp0(xf, % 154.09/21.30 | v1) = v2) | ~ $i(v1) | ~ aElementOf0(v1, xS)) & ! [v1: $i] : % 154.09/21.30 | ! [v2: $i] : ( ~ (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ % 154.09/21.30 | aFixedPointOf0(v1, xf) | aElementOf0(v1, xS)) & ! [v1: $i] : ! % 154.09/21.30 | [v2: $i] : ( ~ (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ % 154.09/21.30 | aElementOf0(v1, xS) | aFixedPointOf0(v1, xf)) & ! [v1: $i] : ! % 154.09/21.30 | [v2: $i] : ( ~ (sdtlpdtrp0(xf, v1) = v2) | ~ $i(v1) | ~ % 154.09/21.30 | aElementOf0(v1, xS) | aElementOf0(v1, v0)) & ! [v1: $i] : ( ~ % 154.09/21.30 | (sdtlpdtrp0(xf, v1) = v1) | ~ $i(v1) | ~ aElementOf0(v1, v0) | % 154.09/21.30 | aElementOf0(v1, xS)) & ! [v1: $i] : ( ~ $i(v1) | ~ % 154.09/21.30 | aFixedPointOf0(v1, xf) | aElementOf0(v1, xS)) & ! [v1: $i] : ( ~ % 154.09/21.30 | $i(v1) | ~ aElementOf0(v1, v0) | aElementOf0(v1, xS) | ? [v2: $i] % 154.09/21.30 | : ( ~ (v2 = v1) & sdtlpdtrp0(xf, v1) = v2 & $i(v2))) & ! [v1: $i] % 154.09/21.30 | : ( ~ $i(v1) | ~ aElementOf0(v1, xS) | sdtlpdtrp0(xf, v1) = v1) & ! % 154.09/21.30 | [v1: $i] : ( ~ $i(v1) | ~ aElementOf0(v1, xS) | aFixedPointOf0(v1, % 154.09/21.30 | xf)) & ! [v1: $i] : ( ~ $i(v1) | ~ aElementOf0(v1, xS) | % 154.09/21.30 | aElementOf0(v1, v0))) % 154.09/21.30 | % 154.09/21.30 | ALPHA: (m__1244) implies: % 154.09/21.30 | (6) aSet0(xP) % 154.09/21.30 | (7) ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xP) | aElementOf0(v0, % 154.09/21.30 | xU)) % 154.09/21.30 | % 154.09/21.30 | ALPHA: (m__) implies: % 154.09/21.30 | (8) $i(xP) % 154.09/21.30 | (9) ! [v0: $i] : ( ~ $i(v0) | ~ aInfimumOfIn0(v0, xP, xU)) % 154.09/21.30 | % 154.09/21.30 | ALPHA: (function-axioms) implies: % 154.09/21.30 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 154.09/21.30 | (szDzozmdt0(v2) = v1) | ~ (szDzozmdt0(v2) = v0)) % 154.09/21.30 | % 154.09/21.30 | DELTA: instantiating (5) with fresh symbol all_27_0 gives: % 154.09/21.30 | (11) cS1142(xf) = xS & szDzozmdt0(xf) = all_27_0 & $i(all_27_0) & aSet0(xS) % 154.09/21.30 | & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (sdtlpdtrp0(xf, v0) = v1) % 154.09/21.30 | | ~ $i(v0) | ~ aElementOf0(v0, xS)) & ! [v0: $i] : ! [v1: $i] : % 154.09/21.30 | ( ~ (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ aFixedPointOf0(v0, xf) % 154.09/21.30 | | aElementOf0(v0, xS)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 154.09/21.30 | (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ aElementOf0(v0, xS) | % 154.09/21.30 | aFixedPointOf0(v0, xf)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 154.09/21.30 | (sdtlpdtrp0(xf, v0) = v1) | ~ $i(v0) | ~ aElementOf0(v0, xS) | % 154.09/21.30 | aElementOf0(v0, all_27_0)) & ! [v0: $i] : ( ~ (sdtlpdtrp0(xf, v0) = % 154.09/21.30 | v0) | ~ $i(v0) | ~ aElementOf0(v0, all_27_0) | aElementOf0(v0, % 154.09/21.30 | xS)) & ! [v0: $i] : ( ~ $i(v0) | ~ aFixedPointOf0(v0, xf) | % 154.09/21.30 | aElementOf0(v0, xS)) & ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, % 154.09/21.30 | all_27_0) | aElementOf0(v0, xS) | ? [v1: $i] : ( ~ (v1 = v0) & % 154.09/21.30 | sdtlpdtrp0(xf, v0) = v1 & $i(v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 154.09/21.30 | aElementOf0(v0, xS) | sdtlpdtrp0(xf, v0) = v0) & ! [v0: $i] : ( ~ % 154.09/21.30 | $i(v0) | ~ aElementOf0(v0, xS) | aFixedPointOf0(v0, xf)) & ! [v0: % 154.09/21.30 | $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xS) | aElementOf0(v0, % 154.09/21.30 | all_27_0)) % 154.09/21.30 | % 154.09/21.30 | ALPHA: (11) implies: % 154.09/21.30 | (12) $i(all_27_0) % 154.09/21.30 | (13) szDzozmdt0(xf) = all_27_0 % 154.09/21.30 | % 154.09/21.30 | GROUND_INST: instantiating (10) with xU, all_27_0, xf, simplifying with (3), % 154.09/21.30 | (13) gives: % 154.09/21.30 | (14) all_27_0 = xU % 154.09/21.30 | % 154.09/21.30 | REDUCE: (12), (14) imply: % 154.09/21.30 | (15) $i(xU) % 154.09/21.30 | % 154.09/21.30 | GROUND_INST: instantiating (1) with xU, xP, simplifying with (2), (6), (8), % 154.09/21.30 | (15) gives: % 154.09/21.30 | (16) aSubsetOf0(xP, xU) | ? [v0: $i] : ($i(v0) & aElementOf0(v0, xP) & ~ % 154.09/21.30 | aElementOf0(v0, xU)) % 154.09/21.30 | % 154.09/21.30 | BETA: splitting (16) gives: % 154.09/21.30 | % 154.09/21.30 | Case 1: % 154.09/21.30 | | % 154.09/21.30 | | (17) aSubsetOf0(xP, xU) % 154.09/21.30 | | % 154.09/21.30 | | GROUND_INST: instantiating (4) with xP, simplifying with (8), (17) gives: % 154.09/21.31 | | (18) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & aSupremumOfIn0(v1, % 154.09/21.31 | | xP, xU) & aInfimumOfIn0(v0, xP, xU) & aUpperBoundOfIn0(v1, xP, % 154.09/21.31 | | xU) & aLowerBoundOfIn0(v0, xP, xU) & aElementOf0(v1, xU) & % 154.09/21.31 | | aElementOf0(v0, xU) & ! [v2: $i] : ( ~ $i(v2) | ~ % 154.09/21.31 | | aUpperBoundOfIn0(v2, xP, xU) | sdtlseqdt0(v1, v2)) & ! [v2: $i] % 154.09/21.31 | | : ( ~ $i(v2) | ~ aLowerBoundOfIn0(v2, xP, xU) | sdtlseqdt0(v2, % 154.09/21.31 | | v0)) & ! [v2: $i] : ( ~ $i(v2) | ~ aElementOf0(v2, xP) | % 154.09/21.31 | | sdtlseqdt0(v2, v1)) & ! [v2: $i] : ( ~ $i(v2) | ~ % 154.09/21.31 | | aElementOf0(v2, xP) | sdtlseqdt0(v0, v2)) & ! [v2: $i] : ( ~ % 154.09/21.31 | | $i(v2) | ~ aElementOf0(v2, xU) | sdtlseqdt0(v2, v0) | ? [v3: % 154.09/21.31 | | $i] : ($i(v3) & aElementOf0(v3, xP) & ~ sdtlseqdt0(v2, v3))) % 154.09/21.31 | | & ! [v2: $i] : ( ~ $i(v2) | ~ aElementOf0(v2, xU) | % 154.09/21.31 | | sdtlseqdt0(v1, v2) | ? [v3: $i] : ($i(v3) & aElementOf0(v3, xP) % 154.09/21.31 | | & ~ sdtlseqdt0(v3, v2)))) % 154.09/21.31 | | % 154.09/21.31 | | DELTA: instantiating (18) with fresh symbols all_288_0, all_288_1 gives: % 154.09/21.31 | | (19) $i(all_288_0) & $i(all_288_1) & aSupremumOfIn0(all_288_0, xP, xU) & % 154.09/21.31 | | aInfimumOfIn0(all_288_1, xP, xU) & aUpperBoundOfIn0(all_288_0, xP, % 154.09/21.31 | | xU) & aLowerBoundOfIn0(all_288_1, xP, xU) & aElementOf0(all_288_0, % 154.09/21.31 | | xU) & aElementOf0(all_288_1, xU) & ! [v0: $i] : ( ~ $i(v0) | ~ % 154.09/21.31 | | aUpperBoundOfIn0(v0, xP, xU) | sdtlseqdt0(all_288_0, v0)) & ! % 154.09/21.31 | | [v0: $i] : ( ~ $i(v0) | ~ aLowerBoundOfIn0(v0, xP, xU) | % 154.09/21.31 | | sdtlseqdt0(v0, all_288_1)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 154.09/21.31 | | aElementOf0(v0, xP) | sdtlseqdt0(v0, all_288_0)) & ! [v0: $i] : ( % 154.09/21.31 | | ~ $i(v0) | ~ aElementOf0(v0, xP) | sdtlseqdt0(all_288_1, v0)) & % 154.09/21.31 | | ! [v0: $i] : ( ~ $i(v0) | ~ aElementOf0(v0, xU) | sdtlseqdt0(v0, % 154.09/21.31 | | all_288_1) | ? [v1: $i] : ($i(v1) & aElementOf0(v1, xP) & ~ % 154.09/21.31 | | sdtlseqdt0(v0, v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 154.09/21.31 | | aElementOf0(v0, xU) | sdtlseqdt0(all_288_0, v0) | ? [v1: $i] : % 154.09/21.31 | | ($i(v1) & aElementOf0(v1, xP) & ~ sdtlseqdt0(v1, v0))) % 154.09/21.31 | | % 154.09/21.31 | | ALPHA: (19) implies: % 154.09/21.31 | | (20) aInfimumOfIn0(all_288_1, xP, xU) % 154.09/21.31 | | (21) $i(all_288_1) % 154.09/21.31 | | % 154.09/21.31 | | GROUND_INST: instantiating (9) with all_288_1, simplifying with (20), (21) % 154.09/21.31 | | gives: % 154.09/21.31 | | (22) $false % 154.09/21.31 | | % 154.09/21.31 | | CLOSE: (22) is inconsistent. % 154.09/21.31 | | % 154.09/21.31 | Case 2: % 154.09/21.31 | | % 154.09/21.31 | | (23) ? [v0: $i] : ($i(v0) & aElementOf0(v0, xP) & ~ aElementOf0(v0, % 154.09/21.31 | | xU)) % 154.09/21.31 | | % 154.09/21.31 | | DELTA: instantiating (23) with fresh symbol all_256_0 gives: % 154.09/21.31 | | (24) $i(all_256_0) & aElementOf0(all_256_0, xP) & ~ % 154.09/21.31 | | aElementOf0(all_256_0, xU) % 154.09/21.31 | | % 154.09/21.31 | | ALPHA: (24) implies: % 154.09/21.31 | | (25) ~ aElementOf0(all_256_0, xU) % 154.09/21.31 | | (26) aElementOf0(all_256_0, xP) % 154.09/21.31 | | (27) $i(all_256_0) % 154.09/21.31 | | % 154.09/21.31 | | GROUND_INST: instantiating (7) with all_256_0, simplifying with (25), (26), % 154.09/21.31 | | (27) gives: % 154.09/21.31 | | (28) $false % 154.09/21.31 | | % 154.09/21.31 | | CLOSE: (28) is inconsistent. % 154.09/21.31 | | % 154.09/21.31 | End of split % 154.09/21.31 | % 154.09/21.31 End of proof % 154.09/21.31 % SZS output end Proof for theBenchmark % 154.09/21.31 % 154.09/21.31 20710ms %------------------------------------------------------------------------------