%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP004_2 : TPTP v8.1.2. Bugfixed v7.5.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n014.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 04:08:22 EDT 2023 % Result : Theorem 54.36s 8.29s % Output : Proof 56.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ITP004_2 : TPTP v8.1.2. Bugfixed v7.5.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.32 % Computer : n014.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Sun Aug 27 12:13:16 EDT 2023 % 0.10/0.32 % CPUTime : % 0.16/0.59 ________ _____ % 0.16/0.59 ___ __ \_________(_)________________________________ % 0.16/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.59 % 0.16/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.59 (2023-06-19) % 0.16/0.59 % 0.16/0.59 (c) Philipp Rümmer, 2009-2023 % 0.16/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.59 Amanda Stjerna. % 0.16/0.59 Free software under BSD-3-Clause. % 0.16/0.59 % 0.16/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.59 % 0.16/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.61 Running up to 7 provers in parallel. % 0.16/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.63/1.34 Prover 4: Preprocessing ... % 3.63/1.36 Prover 1: Preprocessing ... % 3.63/1.41 Prover 2: Preprocessing ... % 3.63/1.41 Prover 6: Preprocessing ... % 3.63/1.41 Prover 0: Preprocessing ... % 3.63/1.41 Prover 3: Preprocessing ... % 3.63/1.41 Prover 5: Preprocessing ... % 11.03/2.36 Prover 3: Constructing countermodel ... % 11.03/2.36 Prover 1: Constructing countermodel ... % 11.31/2.39 Prover 6: Proving ... % 13.34/2.73 Prover 5: Proving ... % 13.68/2.78 Prover 2: Proving ... % 14.08/2.95 Prover 4: Constructing countermodel ... % 16.63/3.16 Prover 0: Proving ... % 16.63/3.23 Prover 3: gave up % 16.63/3.24 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 17.65/3.32 Prover 7: Preprocessing ... % 18.51/3.54 Prover 7: Constructing countermodel ... % 53.29/8.05 Prover 1: gave up % 53.29/8.05 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 53.91/8.15 Prover 7: Found proof (size 120) % 53.91/8.15 Prover 7: proved (4912ms) % 53.91/8.15 Prover 2: stopped % 53.91/8.15 Prover 0: stopped % 53.91/8.15 Prover 5: stopped % 53.91/8.15 Prover 4: stopped % 53.91/8.16 Prover 6: stopped % 53.91/8.16 Prover 8: Preprocessing ... % 54.36/8.26 Prover 8: Warning: ignoring some quantifiers % 54.36/8.28 Prover 8: Constructing countermodel ... % 54.36/8.29 Prover 8: stopped % 54.36/8.29 % 54.36/8.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.36/8.29 % 54.36/8.33 % SZS output start Proof for theBenchmark % 54.36/8.33 Assumptions after simplification: % 54.36/8.33 --------------------------------- % 54.36/8.33 % 54.36/8.33 (ap_tp) % 54.36/8.37 ! [v0: del] : ! [v1: del] : ! [v2: $i] : ! [v3: del] : ! [v4: $i] : ! % 54.36/8.37 [v5: $i] : ( ~ (arr(v0, v1) = v3) | ~ (ap(v2, v4) = v5) | ~ del(v1) | ~ % 54.36/8.37 del(v0) | ~ $i(v4) | ~ $i(v2) | ~ mem(v4, v0) | ~ mem(v2, v3) | mem(v5, % 54.36/8.37 v1)) % 54.36/8.37 % 54.36/8.37 (ax_thm_2Epred__set_2EREST__DEF) % 54.36/8.38 del(bool) & ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 54.36/8.38 (c_2Epred__set_2EREST(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) | ~ % 54.36/8.38 $i(v1) | ? [v4: del] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: % 54.36/8.38 $i] : ? [v9: $i] : ((v9 = v3 & c_2Epred__set_2EDELETE(v0) = v5 & % 54.36/8.39 c_2Epred__set_2ECHOICE(v0) = v7 & ap(v7, v1) = v8 & ap(v6, v8) = v3 & % 54.36/8.39 ap(v5, v1) = v6 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v3)) | (arr(v0, % 54.36/8.39 bool) = v4 & del(v4) & ~ mem(v1, v4)))) & ! [v0: del] : ! [v1: $i] % 54.36/8.39 : ! [v2: $i] : ! [v3: $i] : ( ~ (c_2Epred__set_2EDELETE(v0) = v2) | ~ % 54.36/8.39 (ap(v2, v1) = v3) | ~ del(v0) | ~ $i(v1) | ? [v4: del] : ? [v5: $i] : ? % 54.36/8.39 [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ((v9 = v6 & % 54.36/8.39 c_2Epred__set_2EREST(v0) = v5 & c_2Epred__set_2ECHOICE(v0) = v7 & ap(v7, % 54.36/8.39 v1) = v8 & ap(v5, v1) = v6 & ap(v3, v8) = v6 & $i(v8) & $i(v7) & % 54.36/8.39 $i(v6) & $i(v5)) | (arr(v0, bool) = v4 & del(v4) & ~ mem(v1, v4)))) & % 54.36/8.39 ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 54.36/8.39 (c_2Epred__set_2ECHOICE(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) | ~ % 54.36/8.39 $i(v1) | ? [v4: del] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: % 54.36/8.39 $i] : ? [v9: $i] : ((v9 = v6 & c_2Epred__set_2EREST(v0) = v5 & % 54.36/8.39 c_2Epred__set_2EDELETE(v0) = v7 & ap(v8, v3) = v6 & ap(v7, v1) = v8 & % 54.36/8.39 ap(v5, v1) = v6 & $i(v8) & $i(v7) & $i(v6) & $i(v5)) | (arr(v0, bool) = % 54.36/8.39 v4 & del(v4) & ~ mem(v1, v4)))) % 54.36/8.39 % 54.36/8.39 (ax_thm_2Epred__set_2ESUBSET__DEF) % 54.36/8.39 del(bool) & ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 54.36/8.39 (c_2Epred__set_2ESUBSET(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) | ~ % 54.36/8.39 $i(v1) | ? [v4: del] : ? [v5: $i] : (arr(v0, bool) = v4 & del(v4) & ( ~ % 54.36/8.39 mem(v1, v4) | (c_2Ebool_2EIN(v0) = v5 & $i(v5) & ! [v6: $i] : ! [v7: % 54.36/8.39 $i] : ! [v8: $i] : ! [v9: $i] : ( ~ (ap(v5, v8) = v9) | ~ (ap(v3, % 54.36/8.39 v6) = v7) | ~ $i(v8) | ~ $i(v6) | ~ p(v7) | ~ mem(v8, v0) | % 54.36/8.39 ~ mem(v6, v4) | ? [v10: $i] : ? [v11: $i] : ((ap(v9, v6) = v11 & % 54.36/8.39 $i(v11) & p(v11)) | (ap(v9, v1) = v10 & $i(v10) & ~ p(v10)))) & % 54.36/8.39 ! [v6: $i] : ! [v7: $i] : ( ~ (ap(v3, v6) = v7) | ~ $i(v6) | ~ % 54.36/8.39 mem(v6, v4) | p(v7) | ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? % 54.36/8.39 [v11: $i] : (ap(v9, v6) = v11 & ap(v9, v1) = v10 & ap(v5, v8) = v9 & % 54.36/8.39 $i(v11) & $i(v10) & $i(v9) & $i(v8) & p(v10) & mem(v8, v0) & ~ % 54.36/8.39 p(v11))))))) % 54.36/8.39 % 54.36/8.39 (conj_thm_2Epred__set_2EIN__DELETE) % 54.36/8.40 del(bool) & ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 54.36/8.40 (c_2Epred__set_2EDELETE(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) | ~ % 54.36/8.40 $i(v1) | ? [v4: del] : ? [v5: $i] : ((c_2Ebool_2EIN(v0) = v5 & $i(v5) & ! % 54.36/8.40 [v6: $i] : ! [v7: $i] : ( ~ (ap(v5, v6) = v7) | ~ $i(v6) | ~ mem(v6, % 54.36/8.40 v0) | ? [v8: $i] : (ap(v7, v1) = v8 & $i(v8) & ! [v9: $i] : ! % 54.36/8.40 [v10: $i] : ( ~ (ap(v3, v9) = v10) | ~ $i(v9) | ~ mem(v9, v0) | ? % 54.36/8.40 [v11: $i] : ((v9 = v6 | ~ p(v8) | (ap(v7, v10) = v11 & $i(v11) & % 54.36/8.40 p(v11))) & (( ~ (v9 = v6) & p(v8)) | (ap(v7, v10) = v11 & % 54.36/8.40 $i(v11) & ~ p(v11)))))))) | (arr(v0, bool) = v4 & del(v4) & % 54.36/8.40 ~ mem(v1, v4)))) % 54.36/8.40 % 54.36/8.40 (conj_thm_2Epred__set_2EREST__SUBSET) % 54.36/8.40 del(bool) & ? [v0: del] : ? [v1: $i] : ? [v2: del] : ? [v3: $i] : ? [v4: % 54.36/8.40 $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (c_2Epred__set_2EREST(v0) = % 54.36/8.40 v4 & c_2Epred__set_2ESUBSET(v0) = v3 & arr(v0, bool) = v2 & ap(v6, v1) = v7 % 54.36/8.40 & ap(v4, v1) = v5 & ap(v3, v5) = v6 & del(v2) & del(v0) & $i(v7) & $i(v6) & % 54.36/8.40 $i(v5) & $i(v4) & $i(v3) & $i(v1) & mem(v1, v2) & ~ p(v7)) % 54.36/8.40 % 54.36/8.40 (mem_c_2Ebool_2EIN) % 54.36/8.41 del(bool) & ! [v0: del] : ! [v1: $i] : ( ~ (c_2Ebool_2EIN(v0) = v1) | ~ % 54.36/8.41 del(v0) | ? [v2: del] : ? [v3: del] : ? [v4: del] : (arr(v2, bool) = v3 & % 54.36/8.41 arr(v0, v3) = v4 & arr(v0, bool) = v2 & del(v4) & del(v3) & del(v2) & % 54.36/8.41 mem(v1, v4))) & ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | % 54.36/8.41 ~ del(v0) | ? [v2: $i] : ? [v3: del] : ? [v4: del] : (c_2Ebool_2EIN(v0) = % 54.36/8.41 v2 & arr(v1, bool) = v3 & arr(v0, v3) = v4 & del(v4) & del(v3) & $i(v2) & % 54.36/8.41 mem(v2, v4))) % 54.36/8.41 % 54.36/8.41 (mem_c_2Epred__set_2ECHOICE) % 54.36/8.41 del(bool) & ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2ECHOICE(v0) = v1) % 54.36/8.41 | ~ del(v0) | ? [v2: del] : ? [v3: del] : (arr(v2, v0) = v3 & arr(v0, % 54.36/8.41 bool) = v2 & del(v3) & del(v2) & mem(v1, v3))) & ! [v0: del] : ! [v1: % 54.36/8.41 del] : ( ~ (arr(v0, bool) = v1) | ~ del(v0) | ? [v2: $i] : ? [v3: del] : % 54.36/8.41 (c_2Epred__set_2ECHOICE(v0) = v2 & arr(v1, v0) = v3 & del(v3) & $i(v2) & % 54.36/8.41 mem(v2, v3))) % 54.36/8.41 % 54.36/8.41 (mem_c_2Epred__set_2EDELETE) % 54.36/8.41 del(bool) & ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2EDELETE(v0) = v1) % 54.36/8.41 | ~ del(v0) | ? [v2: del] : ? [v3: del] : ? [v4: del] : (arr(v2, v3) = % 54.36/8.41 v4 & arr(v0, v2) = v3 & arr(v0, bool) = v2 & del(v4) & del(v3) & del(v2) & % 54.36/8.41 mem(v1, v4))) & ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | % 54.36/8.41 ~ del(v0) | ? [v2: $i] : ? [v3: del] : ? [v4: del] : % 54.36/8.41 (c_2Epred__set_2EDELETE(v0) = v2 & arr(v1, v3) = v4 & arr(v0, v1) = v3 & % 54.36/8.41 del(v4) & del(v3) & $i(v2) & mem(v2, v4))) % 54.36/8.41 % 54.36/8.41 (mem_c_2Epred__set_2EREST) % 54.36/8.41 del(bool) & ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2EREST(v0) = v1) | % 54.36/8.41 ~ del(v0) | ? [v2: del] : ? [v3: del] : (arr(v2, v2) = v3 & arr(v0, bool) % 54.36/8.41 = v2 & del(v3) & del(v2) & mem(v1, v3))) & ! [v0: del] : ! [v1: del] : ( % 54.36/8.41 ~ (arr(v0, bool) = v1) | ~ del(v0) | ? [v2: $i] : ? [v3: del] : % 54.36/8.41 (c_2Epred__set_2EREST(v0) = v2 & arr(v1, v1) = v3 & del(v3) & $i(v2) & % 54.36/8.41 mem(v2, v3))) % 54.36/8.41 % 54.36/8.41 (mem_c_2Epred__set_2ESUBSET) % 54.96/8.41 del(bool) & ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2ESUBSET(v0) = v1) % 54.96/8.42 | ~ del(v0) | ? [v2: del] : ? [v3: del] : ? [v4: del] : (arr(v2, v3) = % 54.96/8.42 v4 & arr(v2, bool) = v3 & arr(v0, bool) = v2 & del(v4) & del(v3) & del(v2) % 54.96/8.42 & mem(v1, v4))) & ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | % 54.96/8.42 ~ del(v0) | ? [v2: $i] : ? [v3: del] : ? [v4: del] : % 54.96/8.42 (c_2Epred__set_2ESUBSET(v0) = v2 & arr(v1, v3) = v4 & arr(v1, bool) = v3 & % 54.96/8.42 del(v4) & del(v3) & $i(v2) & mem(v2, v4))) % 54.96/8.42 % 54.96/8.42 (function-axioms) % 54.96/8.42 ! [v0: tp__o] : ! [v1: tp__o] : ! [v2: tp__o] : ! [v3: tp__o] : (v1 = v0 | % 54.96/8.42 ~ (fo__c_2Ebool_2E_2F_5C(v3, v2) = v1) | ~ (fo__c_2Ebool_2E_2F_5C(v3, v2) % 54.96/8.42 = v0)) & ! [v0: tp__o] : ! [v1: tp__o] : ! [v2: tp__o] : ! [v3: tp__o] % 54.96/8.42 : (v1 = v0 | ~ (fo__c_2Emin_2E_3D_3D_3E(v3, v2) = v1) | ~ % 54.96/8.42 (fo__c_2Emin_2E_3D_3D_3E(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 54.96/8.42 [v2: $i] : ! [v3: del] : (v1 = v0 | ~ (k(v3, v2) = v1) | ~ (k(v3, v2) = % 54.96/8.42 v0)) & ! [v0: del] : ! [v1: del] : ! [v2: del] : ! [v3: del] : (v1 = % 54.96/8.42 v0 | ~ (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 54.96/8.42 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (ap(v3, v2) = v1) | ~ % 54.96/8.42 (ap(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | % 54.96/8.42 ~ (c_2Ebool_2E_21(v2) = v1) | ~ (c_2Ebool_2E_21(v2) = v0)) & ! [v0: $i] : % 54.96/8.42 ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ (c_2Emin_2E_3D(v2) = v1) | ~ % 54.96/8.42 (c_2Emin_2E_3D(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = % 54.96/8.42 v0 | ~ (c_2Epred__set_2EREST(v2) = v1) | ~ (c_2Epred__set_2EREST(v2) = % 54.96/8.42 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 54.96/8.42 (c_2Epred__set_2EDELETE(v2) = v1) | ~ (c_2Epred__set_2EDELETE(v2) = v0)) & % 54.96/8.42 ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 54.96/8.42 (c_2Epred__set_2ECHOICE(v2) = v1) | ~ (c_2Epred__set_2ECHOICE(v2) = v0)) & % 54.96/8.42 ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ (c_2Ebool_2EIN(v2) = % 54.96/8.42 v1) | ~ (c_2Ebool_2EIN(v2) = v0)) & ! [v0: tp__o] : ! [v1: tp__o] : ! % 54.96/8.42 [v2: tp__o] : (v1 = v0 | ~ (fo__c_2Ebool_2E_7E(v2) = v1) | ~ % 54.96/8.42 (fo__c_2Ebool_2E_7E(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: del] : % 54.96/8.42 (v1 = v0 | ~ (c_2Epred__set_2ESUBSET(v2) = v1) | ~ % 54.96/8.42 (c_2Epred__set_2ESUBSET(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 54.96/8.42 tp__o] : (v1 = v0 | ~ (inj__o(v2) = v1) | ~ (inj__o(v2) = v0)) & ! [v0: % 54.96/8.42 tp__o] : ! [v1: tp__o] : ! [v2: $i] : (v1 = v0 | ~ (surj__o(v2) = v1) | % 54.96/8.42 ~ (surj__o(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 % 54.96/8.42 | ~ (i(v2) = v1) | ~ (i(v2) = v0)) % 54.96/8.42 % 54.96/8.42 Further assumptions not needed in the proof: % 54.96/8.42 -------------------------------------------- % 54.96/8.42 ax_all_p, ax_and_p, ax_eq_p, ax_imp_p, ax_neg_p, boolext, funcext, ibeta, kbeta, % 54.96/8.42 mem_c_2Ebool_2E_21, mem_c_2Ebool_2E_2F_5C, mem_c_2Ebool_2E_7E, % 54.96/8.42 mem_c_2Emin_2E_3D, mem_c_2Emin_2E_3D_3D_3E, stp_eq_fo_c_2Ebool_2E_2F_5C, % 54.96/8.42 stp_eq_fo_c_2Ebool_2E_7E, stp_eq_fo_c_2Emin_2E_3D_3D_3E, stp_inj_mem_o, % 54.96/8.42 stp_inj_surj_o, stp_iso_mem_o % 54.96/8.42 % 54.96/8.42 Those formulas are unsatisfiable: % 54.96/8.42 --------------------------------- % 54.96/8.42 % 54.96/8.42 Begin of proof % 54.96/8.42 | % 54.96/8.42 | ALPHA: (mem_c_2Epred__set_2ESUBSET) implies: % 54.96/8.43 | (1) ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2ESUBSET(v0) = v1) | ~ % 54.96/8.43 | del(v0) | ? [v2: del] : ? [v3: del] : ? [v4: del] : (arr(v2, v3) = % 54.96/8.43 | v4 & arr(v2, bool) = v3 & arr(v0, bool) = v2 & del(v4) & del(v3) & % 54.96/8.43 | del(v2) & mem(v1, v4))) % 54.96/8.43 | % 54.96/8.43 | ALPHA: (mem_c_2Ebool_2EIN) implies: % 54.96/8.43 | (2) ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | ~ del(v0) | % 54.96/8.43 | ? [v2: $i] : ? [v3: del] : ? [v4: del] : (c_2Ebool_2EIN(v0) = v2 & % 54.96/8.43 | arr(v1, bool) = v3 & arr(v0, v3) = v4 & del(v4) & del(v3) & $i(v2) % 54.96/8.43 | & mem(v2, v4))) % 54.96/8.43 | % 54.96/8.43 | ALPHA: (mem_c_2Epred__set_2ECHOICE) implies: % 54.96/8.43 | (3) ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | ~ del(v0) | % 54.96/8.43 | ? [v2: $i] : ? [v3: del] : (c_2Epred__set_2ECHOICE(v0) = v2 & % 54.96/8.43 | arr(v1, v0) = v3 & del(v3) & $i(v2) & mem(v2, v3))) % 54.96/8.43 | % 54.96/8.43 | ALPHA: (mem_c_2Epred__set_2EDELETE) implies: % 54.96/8.43 | (4) ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | ~ del(v0) | % 54.96/8.43 | ? [v2: $i] : ? [v3: del] : ? [v4: del] : % 54.96/8.43 | (c_2Epred__set_2EDELETE(v0) = v2 & arr(v1, v3) = v4 & arr(v0, v1) = % 54.96/8.43 | v3 & del(v4) & del(v3) & $i(v2) & mem(v2, v4))) % 54.96/8.43 | % 54.96/8.43 | ALPHA: (mem_c_2Epred__set_2EREST) implies: % 54.96/8.43 | (5) ! [v0: del] : ! [v1: del] : ( ~ (arr(v0, bool) = v1) | ~ del(v0) | % 54.96/8.43 | ? [v2: $i] : ? [v3: del] : (c_2Epred__set_2EREST(v0) = v2 & arr(v1, % 54.96/8.43 | v1) = v3 & del(v3) & $i(v2) & mem(v2, v3))) % 54.96/8.43 | (6) ! [v0: del] : ! [v1: $i] : ( ~ (c_2Epred__set_2EREST(v0) = v1) | ~ % 54.96/8.43 | del(v0) | ? [v2: del] : ? [v3: del] : (arr(v2, v2) = v3 & arr(v0, % 54.96/8.43 | bool) = v2 & del(v3) & del(v2) & mem(v1, v3))) % 54.96/8.43 | % 54.96/8.43 | ALPHA: (ax_thm_2Epred__set_2ESUBSET__DEF) implies: % 54.96/8.44 | (7) ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 54.96/8.44 | (c_2Epred__set_2ESUBSET(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) % 54.96/8.44 | | ~ $i(v1) | ? [v4: del] : ? [v5: $i] : (arr(v0, bool) = v4 & % 54.96/8.44 | del(v4) & ( ~ mem(v1, v4) | (c_2Ebool_2EIN(v0) = v5 & $i(v5) & ! % 54.96/8.44 | [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ( ~ % 54.96/8.44 | (ap(v5, v8) = v9) | ~ (ap(v3, v6) = v7) | ~ $i(v8) | ~ % 54.96/8.44 | $i(v6) | ~ p(v7) | ~ mem(v8, v0) | ~ mem(v6, v4) | ? % 54.96/8.44 | [v10: $i] : ? [v11: $i] : ((ap(v9, v6) = v11 & $i(v11) & % 54.96/8.44 | p(v11)) | (ap(v9, v1) = v10 & $i(v10) & ~ p(v10)))) & ! % 54.96/8.44 | [v6: $i] : ! [v7: $i] : ( ~ (ap(v3, v6) = v7) | ~ $i(v6) | ~ % 54.96/8.44 | mem(v6, v4) | p(v7) | ? [v8: $i] : ? [v9: $i] : ? [v10: % 54.96/8.44 | $i] : ? [v11: $i] : (ap(v9, v6) = v11 & ap(v9, v1) = v10 & % 54.96/8.44 | ap(v5, v8) = v9 & $i(v11) & $i(v10) & $i(v9) & $i(v8) & % 54.96/8.44 | p(v10) & mem(v8, v0) & ~ p(v11))))))) % 54.96/8.44 | % 54.96/8.44 | ALPHA: (conj_thm_2Epred__set_2EIN__DELETE) implies: % 55.60/8.44 | (8) ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 55.60/8.44 | (c_2Epred__set_2EDELETE(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) % 55.60/8.44 | | ~ $i(v1) | ? [v4: del] : ? [v5: $i] : ((c_2Ebool_2EIN(v0) = v5 & % 55.60/8.44 | $i(v5) & ! [v6: $i] : ! [v7: $i] : ( ~ (ap(v5, v6) = v7) | ~ % 55.60/8.44 | $i(v6) | ~ mem(v6, v0) | ? [v8: $i] : (ap(v7, v1) = v8 & % 55.60/8.44 | $i(v8) & ! [v9: $i] : ! [v10: $i] : ( ~ (ap(v3, v9) = v10) % 55.60/8.44 | | ~ $i(v9) | ~ mem(v9, v0) | ? [v11: $i] : ((v9 = v6 | % 55.60/8.44 | ~ p(v8) | (ap(v7, v10) = v11 & $i(v11) & p(v11))) & (( % 55.60/8.44 | ~ (v9 = v6) & p(v8)) | (ap(v7, v10) = v11 & $i(v11) & % 55.60/8.44 | ~ p(v11)))))))) | (arr(v0, bool) = v4 & del(v4) & ~ % 55.60/8.44 | mem(v1, v4)))) % 55.60/8.44 | % 55.60/8.44 | ALPHA: (ax_thm_2Epred__set_2EREST__DEF) implies: % 55.60/8.44 | (9) ! [v0: del] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 55.60/8.44 | (c_2Epred__set_2EREST(v0) = v2) | ~ (ap(v2, v1) = v3) | ~ del(v0) | % 55.60/8.44 | ~ $i(v1) | ? [v4: del] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 55.60/8.44 | ? [v8: $i] : ? [v9: $i] : ((v9 = v3 & c_2Epred__set_2EDELETE(v0) = % 55.60/8.44 | v5 & c_2Epred__set_2ECHOICE(v0) = v7 & ap(v7, v1) = v8 & ap(v6, % 55.60/8.44 | v8) = v3 & ap(v5, v1) = v6 & $i(v8) & $i(v7) & $i(v6) & $i(v5) % 55.60/8.44 | & $i(v3)) | (arr(v0, bool) = v4 & del(v4) & ~ mem(v1, v4)))) % 55.60/8.44 | % 55.60/8.44 | ALPHA: (conj_thm_2Epred__set_2EREST__SUBSET) implies: % 55.60/8.44 | (10) ? [v0: del] : ? [v1: $i] : ? [v2: del] : ? [v3: $i] : ? [v4: $i] % 55.60/8.44 | : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (c_2Epred__set_2EREST(v0) % 55.60/8.44 | = v4 & c_2Epred__set_2ESUBSET(v0) = v3 & arr(v0, bool) = v2 & ap(v6, % 55.60/8.44 | v1) = v7 & ap(v4, v1) = v5 & ap(v3, v5) = v6 & del(v2) & del(v0) & % 55.60/8.44 | $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v1) & mem(v1, v2) & % 55.60/8.44 | ~ p(v7)) % 55.60/8.44 | % 55.60/8.44 | ALPHA: (function-axioms) implies: % 55.60/8.44 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 55.60/8.44 | (c_2Ebool_2EIN(v2) = v1) | ~ (c_2Ebool_2EIN(v2) = v0)) % 55.60/8.45 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 55.60/8.45 | (c_2Epred__set_2ECHOICE(v2) = v1) | ~ (c_2Epred__set_2ECHOICE(v2) = % 55.60/8.45 | v0)) % 55.60/8.45 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 55.60/8.45 | (c_2Epred__set_2EDELETE(v2) = v1) | ~ (c_2Epred__set_2EDELETE(v2) = % 55.60/8.45 | v0)) % 55.60/8.45 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: del] : (v1 = v0 | ~ % 55.60/8.45 | (c_2Epred__set_2EREST(v2) = v1) | ~ (c_2Epred__set_2EREST(v2) = % 55.60/8.45 | v0)) % 55.60/8.45 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 55.60/8.45 | (ap(v3, v2) = v1) | ~ (ap(v3, v2) = v0)) % 55.60/8.45 | (16) ! [v0: del] : ! [v1: del] : ! [v2: del] : ! [v3: del] : (v1 = v0 | % 55.60/8.45 | ~ (arr(v3, v2) = v1) | ~ (arr(v3, v2) = v0)) % 55.60/8.45 | % 55.60/8.45 | DELTA: instantiating (10) with fresh symbols all_40_0, all_40_1, all_40_2, % 55.60/8.45 | all_40_3, all_40_4, all_40_5, all_40_6, all_40_7 gives: % 55.60/8.45 | (17) c_2Epred__set_2EREST(all_40_7) = all_40_3 & % 55.60/8.45 | c_2Epred__set_2ESUBSET(all_40_7) = all_40_4 & arr(all_40_7, bool) = % 55.60/8.45 | all_40_5 & ap(all_40_1, all_40_6) = all_40_0 & ap(all_40_3, all_40_6) % 55.60/8.45 | = all_40_2 & ap(all_40_4, all_40_2) = all_40_1 & del(all_40_5) & % 55.60/8.45 | del(all_40_7) & $i(all_40_0) & $i(all_40_1) & $i(all_40_2) & % 55.60/8.45 | $i(all_40_3) & $i(all_40_4) & $i(all_40_6) & mem(all_40_6, all_40_5) & % 55.60/8.45 | ~ p(all_40_0) % 55.60/8.45 | % 55.60/8.45 | ALPHA: (17) implies: % 55.60/8.45 | (18) ~ p(all_40_0) % 55.60/8.45 | (19) mem(all_40_6, all_40_5) % 55.60/8.45 | (20) $i(all_40_6) % 55.60/8.45 | (21) $i(all_40_2) % 55.60/8.45 | (22) del(all_40_7) % 55.60/8.45 | (23) ap(all_40_4, all_40_2) = all_40_1 % 55.60/8.45 | (24) ap(all_40_3, all_40_6) = all_40_2 % 55.60/8.45 | (25) ap(all_40_1, all_40_6) = all_40_0 % 55.60/8.45 | (26) arr(all_40_7, bool) = all_40_5 % 55.60/8.45 | (27) c_2Epred__set_2ESUBSET(all_40_7) = all_40_4 % 55.60/8.45 | (28) c_2Epred__set_2EREST(all_40_7) = all_40_3 % 55.60/8.45 | % 55.60/8.45 | GROUND_INST: instantiating (4) with all_40_7, all_40_5, simplifying with (22), % 55.60/8.45 | (26) gives: % 55.60/8.45 | (29) ? [v0: $i] : ? [v1: del] : ? [v2: del] : % 55.60/8.45 | (c_2Epred__set_2EDELETE(all_40_7) = v0 & arr(all_40_5, v1) = v2 & % 55.60/8.45 | arr(all_40_7, all_40_5) = v1 & del(v2) & del(v1) & $i(v0) & mem(v0, % 55.60/8.45 | v2)) % 55.60/8.45 | % 55.60/8.45 | GROUND_INST: instantiating (2) with all_40_7, all_40_5, simplifying with (22), % 55.60/8.45 | (26) gives: % 55.60/8.46 | (30) ? [v0: $i] : ? [v1: del] : ? [v2: del] : (c_2Ebool_2EIN(all_40_7) = % 55.60/8.46 | v0 & arr(all_40_5, bool) = v1 & arr(all_40_7, v1) = v2 & del(v2) & % 55.60/8.46 | del(v1) & $i(v0) & mem(v0, v2)) % 55.60/8.46 | % 55.60/8.46 | GROUND_INST: instantiating (5) with all_40_7, all_40_5, simplifying with (22), % 55.60/8.46 | (26) gives: % 55.60/8.46 | (31) ? [v0: $i] : ? [v1: del] : (c_2Epred__set_2EREST(all_40_7) = v0 & % 55.60/8.46 | arr(all_40_5, all_40_5) = v1 & del(v1) & $i(v0) & mem(v0, v1)) % 55.60/8.46 | % 55.60/8.46 | GROUND_INST: instantiating (3) with all_40_7, all_40_5, simplifying with (22), % 55.60/8.46 | (26) gives: % 55.60/8.46 | (32) ? [v0: $i] : ? [v1: del] : (c_2Epred__set_2ECHOICE(all_40_7) = v0 & % 55.60/8.46 | arr(all_40_5, all_40_7) = v1 & del(v1) & $i(v0) & mem(v0, v1)) % 55.60/8.46 | % 55.60/8.46 | GROUND_INST: instantiating (7) with all_40_7, all_40_2, all_40_4, all_40_1, % 55.60/8.46 | simplifying with (21), (22), (23), (27) gives: % 55.60/8.46 | (33) ? [v0: del] : ? [v1: $i] : (arr(all_40_7, bool) = v0 & del(v0) & ( ~ % 55.60/8.46 | mem(all_40_2, v0) | (c_2Ebool_2EIN(all_40_7) = v1 & $i(v1) & ! % 55.60/8.46 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (ap(v1, % 55.60/8.46 | v4) = v5) | ~ (ap(all_40_1, v2) = v3) | ~ $i(v4) | ~ % 55.60/8.46 | $i(v2) | ~ p(v3) | ~ mem(v4, all_40_7) | ~ mem(v2, v0) | ? % 55.60/8.46 | [v6: $i] : ? [v7: $i] : ((ap(v5, v2) = v7 & $i(v7) & p(v7)) | % 55.60/8.46 | (ap(v5, all_40_2) = v6 & $i(v6) & ~ p(v6)))) & ! [v2: $i] % 55.60/8.46 | : ! [v3: $i] : ( ~ (ap(all_40_1, v2) = v3) | ~ $i(v2) | ~ % 55.60/8.46 | mem(v2, v0) | p(v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 55.60/8.46 | : ? [v7: $i] : (ap(v5, v2) = v7 & ap(v5, all_40_2) = v6 & % 55.60/8.46 | ap(v1, v4) = v5 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & p(v6) % 55.60/8.46 | & mem(v4, all_40_7) & ~ p(v7)))))) % 55.60/8.46 | % 55.60/8.46 | GROUND_INST: instantiating (1) with all_40_7, all_40_4, simplifying with (22), % 55.60/8.46 | (27) gives: % 55.60/8.46 | (34) ? [v0: del] : ? [v1: del] : ? [v2: del] : (arr(v0, v1) = v2 & % 55.60/8.46 | arr(v0, bool) = v1 & arr(all_40_7, bool) = v0 & del(v2) & del(v1) & % 55.60/8.46 | del(v0) & mem(all_40_4, v2)) % 55.60/8.46 | % 55.60/8.46 | GROUND_INST: instantiating (9) with all_40_7, all_40_6, all_40_3, all_40_2, % 55.60/8.46 | simplifying with (20), (22), (24), (28) gives: % 55.60/8.47 | (35) ? [v0: del] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 55.60/8.47 | ? [v5: int] : ((v5 = all_40_2 & c_2Epred__set_2EDELETE(all_40_7) = v1 % 55.60/8.47 | & c_2Epred__set_2ECHOICE(all_40_7) = v3 & ap(v3, all_40_6) = v4 & % 55.60/8.47 | ap(v2, v4) = all_40_2 & ap(v1, all_40_6) = v2 & $i(v4) & $i(v3) & % 55.60/8.47 | $i(v2) & $i(v1) & $i(all_40_2)) | (arr(all_40_7, bool) = v0 & % 55.60/8.47 | del(v0) & ~ mem(all_40_6, v0))) % 55.60/8.47 | % 55.60/8.47 | GROUND_INST: instantiating (6) with all_40_7, all_40_3, simplifying with (22), % 55.60/8.47 | (28) gives: % 55.60/8.47 | (36) ? [v0: del] : ? [v1: del] : (arr(v0, v0) = v1 & arr(all_40_7, bool) % 55.60/8.47 | = v0 & del(v1) & del(v0) & mem(all_40_3, v1)) % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (36) with fresh symbols all_55_0, all_55_1 gives: % 55.60/8.47 | (37) arr(all_55_1, all_55_1) = all_55_0 & arr(all_40_7, bool) = all_55_1 & % 55.60/8.47 | del(all_55_0) & del(all_55_1) & mem(all_40_3, all_55_0) % 55.60/8.47 | % 55.60/8.47 | ALPHA: (37) implies: % 55.60/8.47 | (38) del(all_55_1) % 55.60/8.47 | (39) arr(all_40_7, bool) = all_55_1 % 55.60/8.47 | (40) arr(all_55_1, all_55_1) = all_55_0 % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (32) with fresh symbols all_65_0, all_65_1 gives: % 55.60/8.47 | (41) c_2Epred__set_2ECHOICE(all_40_7) = all_65_1 & arr(all_40_5, all_40_7) % 55.60/8.47 | = all_65_0 & del(all_65_0) & $i(all_65_1) & mem(all_65_1, all_65_0) % 55.60/8.47 | % 55.60/8.47 | ALPHA: (41) implies: % 55.60/8.47 | (42) mem(all_65_1, all_65_0) % 55.60/8.47 | (43) arr(all_40_5, all_40_7) = all_65_0 % 55.60/8.47 | (44) c_2Epred__set_2ECHOICE(all_40_7) = all_65_1 % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (31) with fresh symbols all_69_0, all_69_1 gives: % 55.60/8.47 | (45) c_2Epred__set_2EREST(all_40_7) = all_69_1 & arr(all_40_5, all_40_5) = % 55.60/8.47 | all_69_0 & del(all_69_0) & $i(all_69_1) & mem(all_69_1, all_69_0) % 55.60/8.47 | % 55.60/8.47 | ALPHA: (45) implies: % 55.60/8.47 | (46) mem(all_69_1, all_69_0) % 55.60/8.47 | (47) $i(all_69_1) % 55.60/8.47 | (48) arr(all_40_5, all_40_5) = all_69_0 % 55.60/8.47 | (49) c_2Epred__set_2EREST(all_40_7) = all_69_1 % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (34) with fresh symbols all_73_0, all_73_1, all_73_2 % 55.60/8.47 | gives: % 55.60/8.47 | (50) arr(all_73_2, all_73_1) = all_73_0 & arr(all_73_2, bool) = all_73_1 & % 55.60/8.47 | arr(all_40_7, bool) = all_73_2 & del(all_73_0) & del(all_73_1) & % 55.60/8.47 | del(all_73_2) & mem(all_40_4, all_73_0) % 55.60/8.47 | % 55.60/8.47 | ALPHA: (50) implies: % 55.60/8.47 | (51) arr(all_40_7, bool) = all_73_2 % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (30) with fresh symbols all_81_0, all_81_1, all_81_2 % 55.60/8.47 | gives: % 55.60/8.47 | (52) c_2Ebool_2EIN(all_40_7) = all_81_2 & arr(all_40_5, bool) = all_81_1 & % 55.60/8.47 | arr(all_40_7, all_81_1) = all_81_0 & del(all_81_0) & del(all_81_1) & % 55.60/8.47 | $i(all_81_2) & mem(all_81_2, all_81_0) % 55.60/8.47 | % 55.60/8.47 | ALPHA: (52) implies: % 55.60/8.47 | (53) c_2Ebool_2EIN(all_40_7) = all_81_2 % 55.60/8.47 | % 55.60/8.47 | DELTA: instantiating (29) with fresh symbols all_83_0, all_83_1, all_83_2 % 55.60/8.47 | gives: % 55.60/8.47 | (54) c_2Epred__set_2EDELETE(all_40_7) = all_83_2 & arr(all_40_5, all_83_1) % 55.60/8.47 | = all_83_0 & arr(all_40_7, all_40_5) = all_83_1 & del(all_83_0) & % 55.60/8.47 | del(all_83_1) & $i(all_83_2) & mem(all_83_2, all_83_0) % 55.60/8.47 | % 55.78/8.47 | ALPHA: (54) implies: % 55.78/8.47 | (55) c_2Epred__set_2EDELETE(all_40_7) = all_83_2 % 55.78/8.47 | % 55.78/8.47 | DELTA: instantiating (35) with fresh symbols all_87_0, all_87_1, all_87_2, % 55.78/8.47 | all_87_3, all_87_4, all_87_5 gives: % 55.78/8.48 | (56) (all_87_0 = all_40_2 & c_2Epred__set_2EDELETE(all_40_7) = all_87_4 & % 55.78/8.48 | c_2Epred__set_2ECHOICE(all_40_7) = all_87_2 & ap(all_87_2, all_40_6) % 55.78/8.48 | = all_87_1 & ap(all_87_3, all_87_1) = all_40_2 & ap(all_87_4, % 55.78/8.48 | all_40_6) = all_87_3 & $i(all_87_1) & $i(all_87_2) & $i(all_87_3) % 55.78/8.48 | & $i(all_87_4) & $i(all_40_2)) | (arr(all_40_7, bool) = all_87_5 & % 55.78/8.48 | del(all_87_5) & ~ mem(all_40_6, all_87_5)) % 55.78/8.48 | % 55.78/8.48 | DELTA: instantiating (33) with fresh symbols all_88_0, all_88_1 gives: % 55.78/8.48 | (57) arr(all_40_7, bool) = all_88_1 & del(all_88_1) & ( ~ mem(all_40_2, % 55.78/8.48 | all_88_1) | (c_2Ebool_2EIN(all_40_7) = all_88_0 & $i(all_88_0) & % 55.78/8.48 | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 55.78/8.48 | (ap(all_88_0, v2) = v3) | ~ (ap(all_40_1, v0) = v1) | ~ $i(v2) % 55.78/8.48 | | ~ $i(v0) | ~ p(v1) | ~ mem(v2, all_40_7) | ~ mem(v0, % 55.78/8.48 | all_88_1) | ? [v4: $i] : ? [v5: $i] : ((ap(v3, v0) = v5 & % 55.78/8.48 | $i(v5) & p(v5)) | (ap(v3, all_40_2) = v4 & $i(v4) & ~ % 55.78/8.48 | p(v4)))) & ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_40_1, v0) % 55.78/8.48 | = v1) | ~ $i(v0) | ~ mem(v0, all_88_1) | p(v1) | ? [v2: $i] % 55.78/8.48 | : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (ap(v3, v0) = v5 & % 55.78/8.48 | ap(v3, all_40_2) = v4 & ap(all_88_0, v2) = v3 & $i(v5) & % 55.78/8.48 | $i(v4) & $i(v3) & $i(v2) & p(v4) & mem(v2, all_40_7) & ~ % 55.78/8.48 | p(v5))))) % 55.78/8.48 | % 55.78/8.48 | ALPHA: (57) implies: % 55.78/8.48 | (58) arr(all_40_7, bool) = all_88_1 % 55.78/8.48 | (59) ~ mem(all_40_2, all_88_1) | (c_2Ebool_2EIN(all_40_7) = all_88_0 & % 55.78/8.48 | $i(all_88_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 55.78/8.48 | : ( ~ (ap(all_88_0, v2) = v3) | ~ (ap(all_40_1, v0) = v1) | ~ % 55.78/8.48 | $i(v2) | ~ $i(v0) | ~ p(v1) | ~ mem(v2, all_40_7) | ~ mem(v0, % 55.78/8.48 | all_88_1) | ? [v4: $i] : ? [v5: $i] : ((ap(v3, v0) = v5 & % 55.78/8.48 | $i(v5) & p(v5)) | (ap(v3, all_40_2) = v4 & $i(v4) & ~ % 55.78/8.48 | p(v4)))) & ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_40_1, v0) = % 55.78/8.48 | v1) | ~ $i(v0) | ~ mem(v0, all_88_1) | p(v1) | ? [v2: $i] : % 55.78/8.48 | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (ap(v3, v0) = v5 & ap(v3, % 55.78/8.48 | all_40_2) = v4 & ap(all_88_0, v2) = v3 & $i(v5) & $i(v4) & % 55.78/8.48 | $i(v3) & $i(v2) & p(v4) & mem(v2, all_40_7) & ~ p(v5)))) % 55.78/8.48 | % 55.78/8.48 | GROUND_INST: instantiating (16) with all_40_5, all_73_2, bool, all_40_7, % 55.78/8.48 | simplifying with (26), (51) gives: % 55.78/8.48 | (60) all_73_2 = all_40_5 % 55.78/8.48 | % 55.78/8.48 | GROUND_INST: instantiating (16) with all_73_2, all_88_1, bool, all_40_7, % 55.78/8.48 | simplifying with (51), (58) gives: % 55.78/8.48 | (61) all_88_1 = all_73_2 % 55.78/8.48 | % 55.78/8.49 | GROUND_INST: instantiating (16) with all_55_1, all_88_1, bool, all_40_7, % 55.78/8.49 | simplifying with (39), (58) gives: % 55.78/8.49 | (62) all_88_1 = all_55_1 % 55.78/8.49 | % 55.78/8.49 | GROUND_INST: instantiating (14) with all_40_3, all_69_1, all_40_7, simplifying % 55.78/8.49 | with (28), (49) gives: % 55.78/8.49 | (63) all_69_1 = all_40_3 % 55.78/8.49 | % 55.78/8.49 | COMBINE_EQS: (61), (62) imply: % 55.78/8.49 | (64) all_73_2 = all_55_1 % 55.78/8.49 | % 55.78/8.49 | SIMP: (64) implies: % 55.78/8.49 | (65) all_73_2 = all_55_1 % 55.78/8.49 | % 55.78/8.49 | COMBINE_EQS: (60), (65) imply: % 55.78/8.49 | (66) all_55_1 = all_40_5 % 55.78/8.49 | % 55.78/8.49 | SIMP: (66) implies: % 55.78/8.49 | (67) all_55_1 = all_40_5 % 55.78/8.49 | % 55.78/8.49 | COMBINE_EQS: (62), (67) imply: % 55.78/8.49 | (68) all_88_1 = all_40_5 % 55.78/8.49 | % 55.78/8.49 | REDUCE: (40), (67) imply: % 55.78/8.49 | (69) arr(all_40_5, all_40_5) = all_55_0 % 55.78/8.49 | % 55.78/8.49 | REDUCE: (38), (67) imply: % 55.78/8.49 | (70) del(all_40_5) % 55.78/8.49 | % 55.78/8.49 | REDUCE: (47), (63) imply: % 55.78/8.49 | (71) $i(all_40_3) % 55.78/8.49 | % 55.78/8.49 | REDUCE: (46), (63) imply: % 55.78/8.49 | (72) mem(all_40_3, all_69_0) % 55.78/8.49 | % 55.78/8.49 | BETA: splitting (56) gives: % 55.78/8.49 | % 55.78/8.49 | Case 1: % 55.78/8.49 | | % 55.78/8.49 | | (73) all_87_0 = all_40_2 & c_2Epred__set_2EDELETE(all_40_7) = all_87_4 & % 55.78/8.49 | | c_2Epred__set_2ECHOICE(all_40_7) = all_87_2 & ap(all_87_2, all_40_6) % 55.78/8.49 | | = all_87_1 & ap(all_87_3, all_87_1) = all_40_2 & ap(all_87_4, % 55.78/8.49 | | all_40_6) = all_87_3 & $i(all_87_1) & $i(all_87_2) & $i(all_87_3) % 55.78/8.49 | | & $i(all_87_4) & $i(all_40_2) % 55.78/8.49 | | % 55.78/8.49 | | ALPHA: (73) implies: % 55.78/8.49 | | (74) $i(all_87_2) % 55.78/8.49 | | (75) $i(all_87_1) % 55.78/8.49 | | (76) ap(all_87_4, all_40_6) = all_87_3 % 55.78/8.49 | | (77) ap(all_87_3, all_87_1) = all_40_2 % 55.78/8.49 | | (78) ap(all_87_2, all_40_6) = all_87_1 % 55.78/8.49 | | (79) c_2Epred__set_2ECHOICE(all_40_7) = all_87_2 % 55.78/8.49 | | (80) c_2Epred__set_2EDELETE(all_40_7) = all_87_4 % 55.78/8.49 | | % 55.78/8.49 | | GROUND_INST: instantiating (16) with all_69_0, all_55_0, all_40_5, all_40_5, % 55.78/8.49 | | simplifying with (48), (69) gives: % 55.78/8.49 | | (81) all_69_0 = all_55_0 % 55.78/8.49 | | % 55.78/8.49 | | GROUND_INST: instantiating (12) with all_65_1, all_87_2, all_40_7, % 55.78/8.49 | | simplifying with (44), (79) gives: % 55.78/8.49 | | (82) all_87_2 = all_65_1 % 55.78/8.49 | | % 55.78/8.49 | | GROUND_INST: instantiating (13) with all_83_2, all_87_4, all_40_7, % 55.78/8.49 | | simplifying with (55), (80) gives: % 55.78/8.49 | | (83) all_87_4 = all_83_2 % 55.78/8.49 | | % 55.78/8.49 | | REDUCE: (78), (82) imply: % 55.78/8.49 | | (84) ap(all_65_1, all_40_6) = all_87_1 % 55.78/8.49 | | % 55.78/8.49 | | REDUCE: (76), (83) imply: % 55.78/8.49 | | (85) ap(all_83_2, all_40_6) = all_87_3 % 55.78/8.50 | | % 55.78/8.50 | | REDUCE: (74), (82) imply: % 55.78/8.50 | | (86) $i(all_65_1) % 55.78/8.50 | | % 55.78/8.50 | | REDUCE: (72), (81) imply: % 55.78/8.50 | | (87) mem(all_40_3, all_55_0) % 55.78/8.50 | | % 55.78/8.50 | | GROUND_INST: instantiating (ap_tp) with all_40_5, all_40_7, all_65_1, % 55.78/8.50 | | all_65_0, all_40_6, all_87_1, simplifying with (19), (20), % 55.78/8.50 | | (22), (42), (43), (70), (84), (86) gives: % 55.78/8.50 | | (88) mem(all_87_1, all_40_7) % 55.78/8.50 | | % 55.78/8.50 | | GROUND_INST: instantiating (ap_tp) with all_40_5, all_40_5, all_40_3, % 55.78/8.50 | | all_55_0, all_40_6, all_40_2, simplifying with (19), (20), % 55.78/8.50 | | (24), (69), (70), (71), (87) gives: % 55.78/8.50 | | (89) mem(all_40_2, all_40_5) % 55.78/8.50 | | % 55.78/8.50 | | GROUND_INST: instantiating (8) with all_40_7, all_40_6, all_83_2, all_87_3, % 55.78/8.50 | | simplifying with (20), (22), (55), (85) gives: % 55.78/8.50 | | (90) ? [v0: del] : ? [v1: $i] : ((c_2Ebool_2EIN(all_40_7) = v1 & $i(v1) % 55.78/8.50 | | & ! [v2: $i] : ! [v3: $i] : ( ~ (ap(v1, v2) = v3) | ~ $i(v2) % 55.78/8.50 | | | ~ mem(v2, all_40_7) | ? [v4: $i] : (ap(v3, all_40_6) = v4 % 55.78/8.50 | | & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ (ap(all_87_3, v5) % 55.78/8.50 | | = v6) | ~ $i(v5) | ~ mem(v5, all_40_7) | ? [v7: $i] : % 55.78/8.50 | | ((v5 = v2 | ~ p(v4) | (ap(v3, v6) = v7 & $i(v7) & p(v7))) % 55.78/8.50 | | & (( ~ (v5 = v2) & p(v4)) | (ap(v3, v6) = v7 & $i(v7) & % 55.78/8.50 | | ~ p(v7)))))))) | (arr(all_40_7, bool) = v0 & del(v0) % 55.78/8.50 | | & ~ mem(all_40_6, v0))) % 55.78/8.50 | | % 55.78/8.50 | | DELTA: instantiating (90) with fresh symbols all_140_0, all_140_1 gives: % 55.78/8.50 | | (91) (c_2Ebool_2EIN(all_40_7) = all_140_0 & $i(all_140_0) & ! [v0: $i] : % 55.78/8.50 | | ! [v1: $i] : ( ~ (ap(all_140_0, v0) = v1) | ~ $i(v0) | ~ % 55.78/8.50 | | mem(v0, all_40_7) | ? [v2: $i] : (ap(v1, all_40_6) = v2 & % 55.78/8.50 | | $i(v2) & ! [v3: $i] : ! [v4: $i] : ( ~ (ap(all_87_3, v3) = % 55.78/8.50 | | v4) | ~ $i(v3) | ~ mem(v3, all_40_7) | ? [v5: $i] : % 55.78/8.50 | | ((v3 = v0 | ~ p(v2) | (ap(v1, v4) = v5 & $i(v5) & p(v5))) & % 55.78/8.50 | | (( ~ (v3 = v0) & p(v2)) | (ap(v1, v4) = v5 & $i(v5) & ~ % 55.78/8.50 | | p(v5)))))))) | (arr(all_40_7, bool) = all_140_1 & % 55.78/8.50 | | del(all_140_1) & ~ mem(all_40_6, all_140_1)) % 55.78/8.50 | | % 55.78/8.50 | | BETA: splitting (59) gives: % 55.78/8.50 | | % 55.78/8.50 | | Case 1: % 55.78/8.50 | | | % 55.78/8.50 | | | (92) ~ mem(all_40_2, all_88_1) % 55.78/8.50 | | | % 55.78/8.50 | | | REDUCE: (68), (92) imply: % 55.78/8.50 | | | (93) ~ mem(all_40_2, all_40_5) % 55.78/8.50 | | | % 55.78/8.50 | | | PRED_UNIFY: (89), (93) imply: % 55.78/8.50 | | | (94) $false % 55.78/8.50 | | | % 55.78/8.50 | | | CLOSE: (94) is inconsistent. % 55.78/8.50 | | | % 55.78/8.50 | | Case 2: % 55.78/8.50 | | | % 55.78/8.51 | | | (95) c_2Ebool_2EIN(all_40_7) = all_88_0 & $i(all_88_0) & ! [v0: $i] : % 55.78/8.51 | | | ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (ap(all_88_0, v2) = % 55.78/8.51 | | | v3) | ~ (ap(all_40_1, v0) = v1) | ~ $i(v2) | ~ $i(v0) | ~ % 55.78/8.51 | | | p(v1) | ~ mem(v2, all_40_7) | ~ mem(v0, all_88_1) | ? [v4: % 55.78/8.51 | | | $i] : ? [v5: $i] : ((ap(v3, v0) = v5 & $i(v5) & p(v5)) | % 55.78/8.51 | | | (ap(v3, all_40_2) = v4 & $i(v4) & ~ p(v4)))) & ! [v0: $i] : % 55.78/8.51 | | | ! [v1: $i] : ( ~ (ap(all_40_1, v0) = v1) | ~ $i(v0) | ~ mem(v0, % 55.78/8.51 | | | all_88_1) | p(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 55.78/8.51 | | | ? [v5: $i] : (ap(v3, v0) = v5 & ap(v3, all_40_2) = v4 & % 55.78/8.51 | | | ap(all_88_0, v2) = v3 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 55.78/8.51 | | | p(v4) & mem(v2, all_40_7) & ~ p(v5))) % 55.78/8.51 | | | % 55.78/8.51 | | | ALPHA: (95) implies: % 55.78/8.51 | | | (96) c_2Ebool_2EIN(all_40_7) = all_88_0 % 55.78/8.51 | | | (97) ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_40_1, v0) = v1) | ~ % 55.78/8.51 | | | $i(v0) | ~ mem(v0, all_88_1) | p(v1) | ? [v2: $i] : ? [v3: % 55.78/8.51 | | | $i] : ? [v4: $i] : ? [v5: $i] : (ap(v3, v0) = v5 & ap(v3, % 55.78/8.51 | | | all_40_2) = v4 & ap(all_88_0, v2) = v3 & $i(v5) & $i(v4) & % 55.78/8.51 | | | $i(v3) & $i(v2) & p(v4) & mem(v2, all_40_7) & ~ p(v5))) % 55.78/8.51 | | | % 55.78/8.51 | | | GROUND_INST: instantiating (97) with all_40_6, all_40_0, simplifying with % 55.78/8.51 | | | (18), (20), (25) gives: % 55.78/8.51 | | | (98) ~ mem(all_40_6, all_88_1) | ? [v0: $i] : ? [v1: $i] : ? [v2: % 55.78/8.51 | | | $i] : ? [v3: $i] : (ap(v1, all_40_2) = v2 & ap(v1, all_40_6) = % 55.78/8.51 | | | v3 & ap(all_88_0, v0) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 55.78/8.51 | | | p(v2) & mem(v0, all_40_7) & ~ p(v3)) % 55.78/8.51 | | | % 55.78/8.51 | | | BETA: splitting (91) gives: % 55.78/8.51 | | | % 55.78/8.51 | | | Case 1: % 55.78/8.51 | | | | % 55.78/8.51 | | | | (99) c_2Ebool_2EIN(all_40_7) = all_140_0 & $i(all_140_0) & ! [v0: % 55.78/8.51 | | | | $i] : ! [v1: $i] : ( ~ (ap(all_140_0, v0) = v1) | ~ $i(v0) | % 55.78/8.51 | | | | ~ mem(v0, all_40_7) | ? [v2: $i] : (ap(v1, all_40_6) = v2 & % 55.78/8.51 | | | | $i(v2) & ! [v3: $i] : ! [v4: $i] : ( ~ (ap(all_87_3, v3) = % 55.78/8.51 | | | | v4) | ~ $i(v3) | ~ mem(v3, all_40_7) | ? [v5: $i] : % 55.78/8.51 | | | | ((v3 = v0 | ~ p(v2) | (ap(v1, v4) = v5 & $i(v5) & p(v5))) % 55.78/8.51 | | | | & (( ~ (v3 = v0) & p(v2)) | (ap(v1, v4) = v5 & $i(v5) & % 55.78/8.51 | | | | ~ p(v5))))))) % 55.78/8.51 | | | | % 55.78/8.51 | | | | ALPHA: (99) implies: % 55.78/8.51 | | | | (100) c_2Ebool_2EIN(all_40_7) = all_140_0 % 55.78/8.51 | | | | (101) ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_140_0, v0) = v1) | ~ % 55.78/8.51 | | | | $i(v0) | ~ mem(v0, all_40_7) | ? [v2: $i] : (ap(v1, % 55.78/8.51 | | | | all_40_6) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ( ~ % 55.78/8.51 | | | | (ap(all_87_3, v3) = v4) | ~ $i(v3) | ~ mem(v3, % 55.78/8.51 | | | | all_40_7) | ? [v5: $i] : ((v3 = v0 | ~ p(v2) | % 55.78/8.51 | | | | (ap(v1, v4) = v5 & $i(v5) & p(v5))) & (( ~ (v3 = v0) % 55.78/8.51 | | | | & p(v2)) | (ap(v1, v4) = v5 & $i(v5) & ~ % 55.78/8.51 | | | | p(v5))))))) % 55.78/8.51 | | | | % 55.78/8.51 | | | | BETA: splitting (98) gives: % 55.78/8.51 | | | | % 55.78/8.51 | | | | Case 1: % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | (102) ~ mem(all_40_6, all_88_1) % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | REDUCE: (68), (102) imply: % 55.78/8.51 | | | | | (103) ~ mem(all_40_6, all_40_5) % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | PRED_UNIFY: (19), (103) imply: % 55.78/8.51 | | | | | (104) $false % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | CLOSE: (104) is inconsistent. % 55.78/8.51 | | | | | % 55.78/8.51 | | | | Case 2: % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | (105) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 55.78/8.51 | | | | | (ap(v1, all_40_2) = v2 & ap(v1, all_40_6) = v3 & ap(all_88_0, % 55.78/8.51 | | | | | v0) = v1 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & p(v2) & % 55.78/8.51 | | | | | mem(v0, all_40_7) & ~ p(v3)) % 55.78/8.51 | | | | | % 55.78/8.51 | | | | | DELTA: instantiating (105) with fresh symbols all_154_0, all_154_1, % 55.78/8.51 | | | | | all_154_2, all_154_3 gives: % 55.78/8.51 | | | | | (106) ap(all_154_2, all_40_2) = all_154_1 & ap(all_154_2, all_40_6) % 55.78/8.51 | | | | | = all_154_0 & ap(all_88_0, all_154_3) = all_154_2 & % 55.78/8.51 | | | | | $i(all_154_0) & $i(all_154_1) & $i(all_154_2) & $i(all_154_3) % 55.78/8.52 | | | | | & p(all_154_1) & mem(all_154_3, all_40_7) & ~ p(all_154_0) % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | ALPHA: (106) implies: % 55.78/8.52 | | | | | (107) ~ p(all_154_0) % 55.78/8.52 | | | | | (108) mem(all_154_3, all_40_7) % 55.78/8.52 | | | | | (109) p(all_154_1) % 55.78/8.52 | | | | | (110) $i(all_154_3) % 55.78/8.52 | | | | | (111) ap(all_88_0, all_154_3) = all_154_2 % 55.78/8.52 | | | | | (112) ap(all_154_2, all_40_6) = all_154_0 % 55.78/8.52 | | | | | (113) ap(all_154_2, all_40_2) = all_154_1 % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | GROUND_INST: instantiating (11) with all_81_2, all_140_0, all_40_7, % 55.78/8.52 | | | | | simplifying with (53), (100) gives: % 55.78/8.52 | | | | | (114) all_140_0 = all_81_2 % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | GROUND_INST: instantiating (11) with all_88_0, all_140_0, all_40_7, % 55.78/8.52 | | | | | simplifying with (96), (100) gives: % 55.78/8.52 | | | | | (115) all_140_0 = all_88_0 % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | COMBINE_EQS: (114), (115) imply: % 55.78/8.52 | | | | | (116) all_88_0 = all_81_2 % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | REDUCE: (111), (116) imply: % 55.78/8.52 | | | | | (117) ap(all_81_2, all_154_3) = all_154_2 % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | GROUND_INST: instantiating (101) with all_154_3, all_154_2, % 55.78/8.52 | | | | | simplifying with (108), (110) gives: % 55.78/8.52 | | | | | (118) ~ (ap(all_140_0, all_154_3) = all_154_2) | ? [v0: $i] : % 55.78/8.52 | | | | | (ap(all_154_2, all_40_6) = v0 & $i(v0) & ! [v1: $i] : ! % 55.78/8.52 | | | | | [v2: $i] : ( ~ (ap(all_87_3, v1) = v2) | ~ $i(v1) | ~ % 55.78/8.52 | | | | | mem(v1, all_40_7) | ? [v3: $i] : ((v1 = all_154_3 | ~ % 55.78/8.52 | | | | | p(v0) | (ap(all_154_2, v2) = v3 & $i(v3) & p(v3))) & % 55.78/8.52 | | | | | (( ~ (v1 = all_154_3) & p(v0)) | (ap(all_154_2, v2) = % 55.78/8.52 | | | | | v3 & $i(v3) & ~ p(v3)))))) % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | BETA: splitting (118) gives: % 55.78/8.52 | | | | | % 55.78/8.52 | | | | | Case 1: % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | (119) ~ (ap(all_140_0, all_154_3) = all_154_2) % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | REDUCE: (114), (119) imply: % 55.78/8.52 | | | | | | (120) ~ (ap(all_81_2, all_154_3) = all_154_2) % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | PRED_UNIFY: (117), (120) imply: % 55.78/8.52 | | | | | | (121) $false % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | CLOSE: (121) is inconsistent. % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | Case 2: % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | (122) ? [v0: $i] : (ap(all_154_2, all_40_6) = v0 & $i(v0) & ! % 55.78/8.52 | | | | | | [v1: $i] : ! [v2: $i] : ( ~ (ap(all_87_3, v1) = v2) | ~ % 55.78/8.52 | | | | | | $i(v1) | ~ mem(v1, all_40_7) | ? [v3: $i] : ((v1 = % 55.78/8.52 | | | | | | all_154_3 | ~ p(v0) | (ap(all_154_2, v2) = v3 & % 55.78/8.52 | | | | | | $i(v3) & p(v3))) & (( ~ (v1 = all_154_3) & p(v0)) % 55.78/8.52 | | | | | | | (ap(all_154_2, v2) = v3 & $i(v3) & ~ p(v3)))))) % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | DELTA: instantiating (122) with fresh symbol all_207_0 gives: % 55.78/8.52 | | | | | | (123) ap(all_154_2, all_40_6) = all_207_0 & $i(all_207_0) & ! % 55.78/8.52 | | | | | | [v0: $i] : ! [v1: $i] : ( ~ (ap(all_87_3, v0) = v1) | ~ % 55.78/8.52 | | | | | | $i(v0) | ~ mem(v0, all_40_7) | ? [v2: $i] : ((v0 = % 55.78/8.52 | | | | | | all_154_3 | ~ p(all_207_0) | (ap(all_154_2, v1) = v2 % 55.78/8.52 | | | | | | & $i(v2) & p(v2))) & (( ~ (v0 = all_154_3) & % 55.78/8.52 | | | | | | p(all_207_0)) | (ap(all_154_2, v1) = v2 & $i(v2) & % 55.78/8.52 | | | | | | ~ p(v2))))) % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | ALPHA: (123) implies: % 55.78/8.52 | | | | | | (124) ap(all_154_2, all_40_6) = all_207_0 % 55.78/8.52 | | | | | | (125) ! [v0: $i] : ! [v1: $i] : ( ~ (ap(all_87_3, v0) = v1) | % 55.78/8.52 | | | | | | ~ $i(v0) | ~ mem(v0, all_40_7) | ? [v2: $i] : ((v0 = % 55.78/8.52 | | | | | | all_154_3 | ~ p(all_207_0) | (ap(all_154_2, v1) = v2 % 55.78/8.52 | | | | | | & $i(v2) & p(v2))) & (( ~ (v0 = all_154_3) & % 55.78/8.52 | | | | | | p(all_207_0)) | (ap(all_154_2, v1) = v2 & $i(v2) & % 55.78/8.52 | | | | | | ~ p(v2))))) % 55.78/8.52 | | | | | | % 55.78/8.52 | | | | | | GROUND_INST: instantiating (125) with all_87_1, all_40_2, % 55.78/8.52 | | | | | | simplifying with (75), (77), (88) gives: % 55.78/8.53 | | | | | | (126) ? [v0: $i] : ((all_154_3 = all_87_1 | ~ p(all_207_0) | % 55.78/8.53 | | | | | | (ap(all_154_2, all_40_2) = v0 & $i(v0) & p(v0))) & (( ~ % 55.78/8.53 | | | | | | (all_154_3 = all_87_1) & p(all_207_0)) | % 55.78/8.53 | | | | | | (ap(all_154_2, all_40_2) = v0 & $i(v0) & ~ p(v0)))) % 55.78/8.53 | | | | | | % 55.78/8.53 | | | | | | DELTA: instantiating (126) with fresh symbol all_210_0 gives: % 55.78/8.53 | | | | | | (127) (all_154_3 = all_87_1 | ~ p(all_207_0) | (ap(all_154_2, % 55.78/8.53 | | | | | | all_40_2) = all_210_0 & $i(all_210_0) & % 55.78/8.53 | | | | | | p(all_210_0))) & (( ~ (all_154_3 = all_87_1) & % 55.78/8.53 | | | | | | p(all_207_0)) | (ap(all_154_2, all_40_2) = all_210_0 & % 55.78/8.53 | | | | | | $i(all_210_0) & ~ p(all_210_0))) % 55.78/8.53 | | | | | | % 55.78/8.53 | | | | | | ALPHA: (127) implies: % 55.78/8.53 | | | | | | (128) ( ~ (all_154_3 = all_87_1) & p(all_207_0)) | (ap(all_154_2, % 55.78/8.53 | | | | | | all_40_2) = all_210_0 & $i(all_210_0) & ~ % 55.78/8.53 | | | | | | p(all_210_0)) % 55.78/8.53 | | | | | | % 55.78/8.53 | | | | | | BETA: splitting (128) gives: % 55.78/8.53 | | | | | | % 55.78/8.53 | | | | | | Case 1: % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | (129) ~ (all_154_3 = all_87_1) & p(all_207_0) % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | ALPHA: (129) implies: % 55.78/8.53 | | | | | | | (130) p(all_207_0) % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | PRED_UNIFY: (107), (130) imply: % 55.78/8.53 | | | | | | | (131) ~ (all_207_0 = all_154_0) % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | GROUND_INST: instantiating (15) with all_154_0, all_207_0, % 55.78/8.53 | | | | | | | all_40_6, all_154_2, simplifying with (112), (124) % 55.78/8.53 | | | | | | | gives: % 55.78/8.53 | | | | | | | (132) all_207_0 = all_154_0 % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | REDUCE: (131), (132) imply: % 55.78/8.53 | | | | | | | (133) $false % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | CLOSE: (133) is inconsistent. % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | Case 2: % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | (134) ap(all_154_2, all_40_2) = all_210_0 & $i(all_210_0) & ~ % 55.78/8.53 | | | | | | | p(all_210_0) % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | ALPHA: (134) implies: % 55.78/8.53 | | | | | | | (135) ~ p(all_210_0) % 55.78/8.53 | | | | | | | (136) ap(all_154_2, all_40_2) = all_210_0 % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | GROUND_INST: instantiating (15) with all_154_1, all_210_0, % 55.78/8.53 | | | | | | | all_40_2, all_154_2, simplifying with (113), (136) % 55.78/8.53 | | | | | | | gives: % 55.78/8.53 | | | | | | | (137) all_210_0 = all_154_1 % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | PRED_UNIFY: (109), (135) imply: % 55.78/8.53 | | | | | | | (138) ~ (all_210_0 = all_154_1) % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | REDUCE: (137), (138) imply: % 55.78/8.53 | | | | | | | (139) $false % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | | CLOSE: (139) is inconsistent. % 55.78/8.53 | | | | | | | % 55.78/8.53 | | | | | | End of split % 55.78/8.53 | | | | | | % 55.78/8.53 | | | | | End of split % 55.78/8.53 | | | | | % 55.78/8.53 | | | | End of split % 55.78/8.53 | | | | % 55.78/8.53 | | | Case 2: % 55.78/8.53 | | | | % 55.78/8.53 | | | | (140) arr(all_40_7, bool) = all_140_1 & del(all_140_1) & ~ % 55.78/8.53 | | | | mem(all_40_6, all_140_1) % 55.78/8.53 | | | | % 55.78/8.53 | | | | ALPHA: (140) implies: % 55.78/8.53 | | | | (141) ~ mem(all_40_6, all_140_1) % 55.78/8.53 | | | | (142) arr(all_40_7, bool) = all_140_1 % 55.78/8.53 | | | | % 55.78/8.53 | | | | GROUND_INST: instantiating (16) with all_40_5, all_140_1, bool, % 55.78/8.53 | | | | all_40_7, simplifying with (26), (142) gives: % 55.78/8.53 | | | | (143) all_140_1 = all_40_5 % 55.78/8.53 | | | | % 55.78/8.53 | | | | PRED_UNIFY: (19), (141) imply: % 55.78/8.53 | | | | (144) ~ (all_140_1 = all_40_5) % 55.78/8.53 | | | | % 55.78/8.53 | | | | REDUCE: (143), (144) imply: % 55.78/8.53 | | | | (145) $false % 55.78/8.53 | | | | % 55.78/8.53 | | | | CLOSE: (145) is inconsistent. % 55.78/8.53 | | | | % 55.78/8.53 | | | End of split % 55.78/8.53 | | | % 55.78/8.53 | | End of split % 55.78/8.53 | | % 55.78/8.53 | Case 2: % 55.78/8.53 | | % 55.78/8.53 | | (146) arr(all_40_7, bool) = all_87_5 & del(all_87_5) & ~ mem(all_40_6, % 55.78/8.53 | | all_87_5) % 55.78/8.53 | | % 55.78/8.53 | | ALPHA: (146) implies: % 55.78/8.53 | | (147) ~ mem(all_40_6, all_87_5) % 55.78/8.53 | | (148) arr(all_40_7, bool) = all_87_5 % 55.78/8.53 | | % 55.78/8.53 | | GROUND_INST: instantiating (16) with all_40_5, all_87_5, bool, all_40_7, % 55.78/8.53 | | simplifying with (26), (148) gives: % 55.78/8.53 | | (149) all_87_5 = all_40_5 % 55.78/8.53 | | % 56.07/8.53 | | PRED_UNIFY: (19), (147) imply: % 56.07/8.53 | | (150) ~ (all_87_5 = all_40_5) % 56.07/8.53 | | % 56.07/8.54 | | REDUCE: (149), (150) imply: % 56.07/8.54 | | (151) $false % 56.07/8.54 | | % 56.07/8.54 | | CLOSE: (151) is inconsistent. % 56.07/8.54 | | % 56.07/8.54 | End of split % 56.07/8.54 | % 56.07/8.54 End of proof % 56.07/8.54 % SZS output end Proof for theBenchmark % 56.07/8.54 % 56.07/8.54 7943ms %------------------------------------------------------------------------------