%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SET730+4 : TPTP v8.1.2. Bugfixed v2.2.1. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n002.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 15:26:11 EDT 2023 % Result : Theorem 18.37s 3.28s % Output : Proof 23.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SET730+4 : TPTP v8.1.2. Bugfixed v2.2.1. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n002.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Aug 26 14:36:48 EDT 2023 % 0.13/0.34 % 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/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.42/1.19 Prover 4: Preprocessing ... % 3.42/1.21 Prover 1: Preprocessing ... % 3.42/1.25 Prover 2: Preprocessing ... % 3.42/1.25 Prover 5: Preprocessing ... % 3.42/1.25 Prover 3: Preprocessing ... % 3.92/1.26 Prover 6: Preprocessing ... % 3.92/1.26 Prover 0: Preprocessing ... % 8.01/1.93 Prover 5: Proving ... % 8.86/1.95 Prover 2: Proving ... % 8.86/2.02 Prover 6: Proving ... % 10.18/2.12 Prover 1: Constructing countermodel ... % 10.18/2.13 Prover 3: Constructing countermodel ... % 12.73/2.48 Prover 3: gave up % 12.73/2.48 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.73/2.52 Prover 4: Constructing countermodel ... % 12.73/2.54 Prover 0: Proving ... % 12.73/2.56 Prover 7: Preprocessing ... % 13.88/2.69 Prover 7: Warning: ignoring some quantifiers % 14.55/2.73 Prover 7: Constructing countermodel ... % 14.55/2.74 Prover 1: gave up % 14.96/2.78 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 14.96/2.82 Prover 8: Preprocessing ... % 17.27/3.10 Prover 8: Warning: ignoring some quantifiers % 17.27/3.11 Prover 8: Constructing countermodel ... % 18.37/3.28 Prover 0: proved (2653ms) % 18.37/3.28 % 18.37/3.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.37/3.28 % 18.37/3.28 Prover 2: stopped % 18.37/3.30 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 18.37/3.30 Prover 5: stopped % 18.37/3.30 Prover 6: stopped % 19.20/3.31 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 19.20/3.31 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 19.20/3.32 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 19.20/3.35 Prover 10: Preprocessing ... % 19.62/3.37 Prover 11: Preprocessing ... % 19.62/3.39 Prover 16: Preprocessing ... % 19.62/3.40 Prover 13: Preprocessing ... % 20.29/3.46 Prover 10: Warning: ignoring some quantifiers % 20.29/3.48 Prover 8: gave up % 20.55/3.49 Prover 10: Constructing countermodel ... % 20.55/3.49 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 20.55/3.49 Prover 16: Warning: ignoring some quantifiers % 20.90/3.54 Prover 16: Constructing countermodel ... % 21.01/3.56 Prover 19: Preprocessing ... % 21.01/3.56 Prover 13: Warning: ignoring some quantifiers % 21.01/3.58 Prover 13: Constructing countermodel ... % 21.53/3.62 Prover 10: gave up % 21.95/3.68 Prover 4: Found proof (size 311) % 21.95/3.68 Prover 4: proved (3046ms) % 21.95/3.68 Prover 7: stopped % 21.95/3.68 Prover 16: stopped % 21.95/3.68 Prover 11: stopped % 21.95/3.68 Prover 13: stopped % 22.41/3.77 Prover 19: Warning: ignoring some quantifiers % 22.55/3.79 Prover 19: Constructing countermodel ... % 22.55/3.80 Prover 19: stopped % 22.55/3.80 % 22.55/3.80 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 22.55/3.80 % 22.55/3.82 % SZS output start Proof for theBenchmark % 22.55/3.82 Assumptions after simplification: % 22.55/3.82 --------------------------------- % 22.55/3.82 % 22.55/3.82 (equal_set) % 22.55/3.85 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (equal_set(v0, v1) = % 22.55/3.85 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (subset(v1, % 22.55/3.85 v0) = v4 & subset(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0: % 22.55/3.85 $i] : ! [v1: $i] : ! [v2: any] : ( ~ (subset(v1, v0) = v2) | ~ $i(v1) | % 22.55/3.85 ~ $i(v0) | ? [v3: any] : ? [v4: any] : (equal_set(v0, v1) = v3 & % 22.55/3.85 subset(v0, v1) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : % 22.55/3.85 ! [v1: $i] : ! [v2: any] : ( ~ (subset(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 22.55/3.85 | ? [v3: any] : ? [v4: any] : (equal_set(v0, v1) = v3 & subset(v1, v0) = % 22.55/3.85 v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = 0)))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 22.55/3.85 (equal_set(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | (subset(v1, v0) = 0 & % 22.55/3.85 subset(v0, v1) = 0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v1, v0) = % 22.55/3.85 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : (equal_set(v0, % 22.55/3.85 v1) = v3 & subset(v0, v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: $i] % 22.55/3.85 : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: % 22.55/3.85 any] : ? [v3: any] : (equal_set(v0, v1) = v3 & subset(v1, v0) = v2 & ( ~ % 22.55/3.85 (v2 = 0) | v3 = 0))) % 22.55/3.85 % 22.55/3.85 (image2) % 22.55/3.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : ! [v5: % 22.55/3.85 $i] : (v4 = 0 | ~ (image2(v0, v1) = v3) | ~ (apply(v0, v5, v2) = 0) | ~ % 22.55/3.85 (member(v2, v3) = v4) | ~ $i(v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 22.55/3.85 [v6: int] : ( ~ (v6 = 0) & member(v5, v1) = v6)) & ! [v0: $i] : ! [v1: $i] % 22.55/3.85 : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : ! [v5: $i] : (v4 = 0 | ~ % 22.55/3.85 (image2(v0, v1) = v3) | ~ (member(v5, v1) = 0) | ~ (member(v2, v3) = v4) | % 22.55/3.85 ~ $i(v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) % 22.55/3.85 & apply(v0, v5, v2) = v6)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 22.55/3.85 [v3: $i] : ( ~ (image2(v0, v1) = v3) | ~ (member(v2, v3) = 0) | ~ $i(v2) | % 22.55/3.85 ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : (apply(v0, v4, v2) = 0 & member(v4, v1) % 22.55/3.85 = 0 & $i(v4))) % 22.55/3.85 % 22.55/3.85 (maps) % 22.55/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 22.55/3.86 $i] : (v5 = v4 | ~ (maps(v0, v1, v2) = 0) | ~ (apply(v0, v3, v5) = 0) | ~ % 22.55/3.86 (apply(v0, v3, v4) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 22.55/3.86 $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : % 22.55/3.86 (member(v5, v2) = v8 & member(v4, v2) = v7 & member(v3, v1) = v6 & ( ~ (v8 = % 22.55/3.86 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 22.55/3.86 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ (maps(v0, % 22.55/3.86 v1, v2) = 0) | ~ (apply(v0, v3, v5) = 0) | ~ (member(v4, v2) = 0) | ~ % 22.55/3.86 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: % 22.55/3.86 any] : ? [v7: any] : ? [v8: any] : (apply(v0, v3, v4) = v8 & member(v5, % 22.55/3.86 v2) = v7 & member(v3, v1) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = % 22.55/3.86 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 22.55/3.86 [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ (maps(v0, v1, v2) = 0) | ~ (apply(v0, % 22.55/3.86 v3, v4) = 0) | ~ (member(v5, v2) = 0) | ~ $i(v5) | ~ $i(v4) | ~ % 22.55/3.86 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : % 22.55/3.86 ? [v8: any] : (apply(v0, v3, v5) = v8 & member(v4, v2) = v7 & member(v3, v1) % 22.55/3.86 = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: % 22.55/3.86 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ % 22.55/3.86 (maps(v0, v1, v2) = 0) | ~ (member(v5, v2) = 0) | ~ (member(v4, v2) = 0) | % 22.55/3.86 ~ (member(v3, v1) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 22.55/3.86 $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : (apply(v0, v3, v5) = v7 & % 22.55/3.86 apply(v0, v3, v4) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! % 22.55/3.86 [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (maps(v0, v1, v2) = v3) | % 22.55/3.86 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] % 22.55/3.86 : ? [v7: int] : ? [v8: int] : ? [v9: int] : ? [v10: int] : ? [v11: int] % 22.55/3.86 : ? [v12: $i] : ? [v13: int] : ($i(v12) & $i(v6) & $i(v5) & $i(v4) & ((v13 % 22.55/3.86 = 0 & member(v12, v1) = 0 & ! [v14: $i] : ( ~ (apply(v0, v12, v14) = % 22.55/3.86 0) | ~ $i(v14) | ? [v15: int] : ( ~ (v15 = 0) & member(v14, v2) % 22.55/3.86 = v15)) & ! [v14: $i] : ( ~ (member(v14, v2) = 0) | ~ $i(v14) | % 22.55/3.86 ? [v15: int] : ( ~ (v15 = 0) & apply(v0, v12, v14) = v15))) | (v11 = % 22.55/3.86 0 & v10 = 0 & v9 = 0 & v8 = 0 & v7 = 0 & ~ (v6 = v5) & apply(v0, v4, % 22.55/3.86 v6) = 0 & apply(v0, v4, v5) = 0 & member(v6, v2) = 0 & member(v5, % 22.55/3.86 v2) = 0 & member(v4, v1) = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 22.55/3.86 [v2: $i] : ! [v3: $i] : ( ~ (maps(v0, v1, v2) = 0) | ~ (member(v3, v1) = 0) % 22.55/3.86 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : (apply(v0, % 22.55/3.86 v3, v4) = 0 & member(v4, v2) = 0 & $i(v4))) % 22.55/3.86 % 22.55/3.86 (subset) % 22.55/3.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 22.55/3.86 (subset(v0, v1) = 0) | ~ (member(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 22.55/3.86 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & member(v2, v0) = v4)) & ! [v0: $i] : % 22.55/3.86 ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ~ $i(v1) | % 22.55/3.86 ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & member(v3, v1) = v4 & % 22.55/3.86 member(v3, v0) = 0 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 22.55/3.86 ( ~ (subset(v0, v1) = 0) | ~ (member(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | % 22.55/3.86 ~ $i(v0) | member(v2, v1) = 0) % 22.55/3.86 % 22.55/3.86 (thII21) % 22.55/3.87 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 22.55/3.87 int] : ( ~ (v5 = 0) & image2(v0, v2) = v4 & maps(v1, v2, v4) = v5 & maps(v0, % 22.55/3.87 v2, v3) = 0 & subset(v4, v3) = 0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 22.55/3.87 $i(v0) & ! [v6: $i] : ! [v7: $i] : ! [v8: any] : ( ~ (apply(v1, v6, v7) = % 22.55/3.87 v8) | ~ $i(v7) | ~ $i(v6) | ? [v9: any] : ? [v10: any] : ? [v11: % 22.55/3.87 any] : (apply(v0, v6, v7) = v11 & member(v7, v4) = v10 & member(v6, v2) % 22.55/3.87 = v9 & ( ~ (v10 = 0) | ~ (v9 = 0) | (( ~ (v11 = 0) | v8 = 0) & ( ~ (v8 % 22.55/3.87 = 0) | v11 = 0))))) & ! [v6: $i] : ! [v7: $i] : ! [v8: any] : % 22.55/3.87 ( ~ (apply(v0, v6, v7) = v8) | ~ $i(v7) | ~ $i(v6) | ? [v9: any] : ? % 22.55/3.87 [v10: any] : ? [v11: any] : (apply(v1, v6, v7) = v11 & member(v7, v4) = % 22.55/3.87 v10 & member(v6, v2) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0) | (( ~ (v11 = 0) % 22.55/3.87 | v8 = 0) & ( ~ (v8 = 0) | v11 = 0)))))) % 22.55/3.87 % 22.55/3.87 (function-axioms) % 22.55/3.87 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 22.55/3.87 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | % 22.55/3.87 ~ (compose_predicate(v7, v6, v5, v4, v3, v2) = v1) | ~ % 22.55/3.87 (compose_predicate(v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: % 22.55/3.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 22.55/3.87 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (isomorphism(v6, v5, % 22.55/3.87 v4, v3, v2) = v1) | ~ (isomorphism(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 22.55/3.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 22.55/3.87 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (decreasing(v6, v5, % 22.55/3.87 v4, v3, v2) = v1) | ~ (decreasing(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 22.55/3.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 22.55/3.87 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (increasing(v6, v5, % 22.55/3.87 v4, v3, v2) = v1) | ~ (increasing(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 22.55/3.87 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 22.55/3.87 ! [v6: $i] : (v1 = v0 | ~ (compose_function(v6, v5, v4, v3, v2) = v1) | ~ % 22.55/3.87 (compose_function(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 22.55/3.87 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 22.55/3.87 $i] : (v1 = v0 | ~ (inverse_predicate(v5, v4, v3, v2) = v1) | ~ % 22.55/3.87 (inverse_predicate(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 22.55/3.87 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 22.55/3.87 $i] : (v1 = v0 | ~ (equal_maps(v5, v4, v3, v2) = v1) | ~ (equal_maps(v5, % 22.55/3.87 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 22.55/3.87 $i] : ! [v4: $i] : (v1 = v0 | ~ (inverse_image3(v4, v3, v2) = v1) | ~ % 22.55/3.87 (inverse_image3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 22.55/3.87 : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (image3(v4, v3, v2) = v1) | ~ % 22.55/3.87 (image3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 22.55/3.87 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (inverse_function(v4, v3, v2) = v1) | % 22.55/3.87 ~ (inverse_function(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 22.55/3.87 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 22.55/3.87 ~ (one_to_one(v4, v3, v2) = v1) | ~ (one_to_one(v4, v3, v2) = v0)) & ! % 22.55/3.87 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 22.55/3.87 $i] : ! [v4: $i] : (v1 = v0 | ~ (surjective(v4, v3, v2) = v1) | ~ % 22.55/3.87 (surjective(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.55/3.87 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 22.55/3.87 (injective(v4, v3, v2) = v1) | ~ (injective(v4, v3, v2) = v0)) & ! [v0: % 22.55/3.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 22.55/3.87 : ! [v4: $i] : (v1 = v0 | ~ (maps(v4, v3, v2) = v1) | ~ (maps(v4, v3, v2) = % 22.55/3.87 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 22.55/3.87 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = v1) | % 22.55/3.87 ~ (apply(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 22.55/3.87 [v3: $i] : (v1 = v0 | ~ (inverse_image2(v3, v2) = v1) | ~ % 22.55/3.87 (inverse_image2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 22.55/3.87 ! [v3: $i] : (v1 = v0 | ~ (image2(v3, v2) = v1) | ~ (image2(v3, v2) = v0)) & % 22.55/3.87 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 22.55/3.87 [v3: $i] : (v1 = v0 | ~ (identity(v3, v2) = v1) | ~ (identity(v3, v2) = v0)) % 22.55/3.87 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.55/3.87 (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0: % 22.55/3.87 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.55/3.87 (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0: $i] : ! % 22.55/3.87 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (union(v3, v2) = v1) | ~ % 22.55/3.87 (union(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 22.55/3.87 $i] : (v1 = v0 | ~ (intersection(v3, v2) = v1) | ~ (intersection(v3, v2) = % 22.55/3.87 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 22.55/3.87 $i] : ! [v3: $i] : (v1 = v0 | ~ (equal_set(v3, v2) = v1) | ~ % 22.55/3.87 (equal_set(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.55/3.87 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (subset(v3, % 22.55/3.87 v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 22.55/3.88 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.55/3.88 (member(v3, v2) = v1) | ~ (member(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 22.55/3.88 $i] : ! [v2: $i] : (v1 = v0 | ~ (product(v2) = v1) | ~ (product(v2) = % 22.55/3.88 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sum(v2) = % 22.55/3.88 v1) | ~ (sum(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 22.55/3.88 v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0: $i] : ! % 22.55/3.88 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (power_set(v2) = v1) | ~ % 22.55/3.88 (power_set(v2) = v0)) % 22.55/3.88 % 22.55/3.88 Further assumptions not needed in the proof: % 22.55/3.88 -------------------------------------------- % 22.55/3.88 compose_function, compose_predicate, decreasing_function, difference, empty_set, % 22.55/3.88 equal_maps, identity, image3, increasing_function, injective, intersection, % 22.55/3.88 inverse_function, inverse_image2, inverse_image3, inverse_predicate, % 22.55/3.88 isomorphism, one_to_one, power_set, product, singleton, sum, surjective, union, % 22.55/3.88 unordered_pair % 22.55/3.88 % 22.55/3.88 Those formulas are unsatisfiable: % 22.55/3.88 --------------------------------- % 22.55/3.88 % 22.55/3.88 Begin of proof % 22.55/3.88 | % 22.55/3.88 | ALPHA: (subset) implies: % 22.55/3.88 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (subset(v0, v1) = 0) | ~ % 22.55/3.88 | (member(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | member(v2, % 22.55/3.88 | v1) = 0) % 22.55/3.88 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subset(v0, v1) % 22.55/3.88 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ % 22.55/3.88 | (v4 = 0) & member(v3, v1) = v4 & member(v3, v0) = 0 & $i(v3))) % 22.55/3.88 | % 22.55/3.88 | ALPHA: (equal_set) implies: % 22.55/3.88 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ % 22.55/3.88 | $i(v0) | ? [v2: any] : ? [v3: any] : (equal_set(v0, v1) = v3 & % 22.55/3.88 | subset(v1, v0) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 22.55/3.88 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v1, v0) = 0) | ~ $i(v1) | ~ % 22.55/3.88 | $i(v0) | ? [v2: any] : ? [v3: any] : (equal_set(v0, v1) = v3 & % 22.55/3.88 | subset(v0, v1) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 22.55/3.88 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (subset(v0, v1) = v2) | % 22.55/3.88 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (equal_set(v0, % 22.55/3.88 | v1) = v3 & subset(v1, v0) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = % 22.55/3.88 | 0)))) % 22.55/3.88 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (subset(v1, v0) = v2) | % 22.55/3.88 | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (equal_set(v0, % 22.55/3.88 | v1) = v3 & subset(v0, v1) = v4 & ( ~ (v3 = 0) | (v4 = 0 & v2 = % 22.55/3.88 | 0)))) % 22.55/3.88 | % 22.55/3.88 | ALPHA: (maps) implies: % 22.55/3.88 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (maps(v0, % 22.55/3.88 | v1, v2) = 0) | ~ (member(v3, v1) = 0) | ~ $i(v3) | ~ $i(v2) | % 22.55/3.88 | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : (apply(v0, v3, v4) = 0 & % 22.55/3.88 | member(v4, v2) = 0 & $i(v4))) % 22.55/3.88 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 22.55/3.88 | (maps(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 22.55/3.88 | $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ? [v8: int] : ? % 22.55/3.88 | [v9: int] : ? [v10: int] : ? [v11: int] : ? [v12: $i] : ? [v13: % 22.55/3.88 | int] : ($i(v12) & $i(v6) & $i(v5) & $i(v4) & ((v13 = 0 & % 22.55/3.88 | member(v12, v1) = 0 & ! [v14: $i] : ( ~ (apply(v0, v12, v14) = % 22.55/3.88 | 0) | ~ $i(v14) | ? [v15: int] : ( ~ (v15 = 0) & % 22.55/3.88 | member(v14, v2) = v15)) & ! [v14: $i] : ( ~ (member(v14, % 22.55/3.88 | v2) = 0) | ~ $i(v14) | ? [v15: int] : ( ~ (v15 = 0) & % 22.55/3.88 | apply(v0, v12, v14) = v15))) | (v11 = 0 & v10 = 0 & v9 = 0 % 22.55/3.88 | & v8 = 0 & v7 = 0 & ~ (v6 = v5) & apply(v0, v4, v6) = 0 & % 22.55/3.88 | apply(v0, v4, v5) = 0 & member(v6, v2) = 0 & member(v5, v2) = 0 % 22.55/3.88 | & member(v4, v1) = 0)))) % 22.55/3.89 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 22.55/3.89 | ! [v5: $i] : (v5 = v4 | ~ (maps(v0, v1, v2) = 0) | ~ (member(v5, v2) % 22.55/3.89 | = 0) | ~ (member(v4, v2) = 0) | ~ (member(v3, v1) = 0) | ~ % 22.55/3.89 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 22.55/3.89 | ? [v6: any] : ? [v7: any] : (apply(v0, v3, v5) = v7 & apply(v0, v3, % 22.55/3.89 | v4) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) % 22.55/3.89 | % 22.55/3.89 | ALPHA: (image2) implies: % 22.55/3.89 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 22.55/3.89 | (image2(v0, v1) = v3) | ~ (member(v2, v3) = 0) | ~ $i(v2) | ~ % 22.55/3.89 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (apply(v0, v4, v2) = 0 & % 22.55/3.89 | member(v4, v1) = 0 & $i(v4))) % 22.55/3.89 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 22.55/3.89 | ! [v5: $i] : (v4 = 0 | ~ (image2(v0, v1) = v3) | ~ (member(v5, v1) % 22.55/3.89 | = 0) | ~ (member(v2, v3) = v4) | ~ $i(v5) | ~ $i(v2) | ~ % 22.55/3.89 | $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & apply(v0, v5, v2) % 22.55/3.89 | = v6)) % 22.55/3.89 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 22.55/3.89 | ! [v5: $i] : (v4 = 0 | ~ (image2(v0, v1) = v3) | ~ (apply(v0, v5, % 22.55/3.89 | v2) = 0) | ~ (member(v2, v3) = v4) | ~ $i(v5) | ~ $i(v2) | ~ % 22.55/3.89 | $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & member(v5, v1) = % 22.55/3.89 | v6)) % 22.55/3.89 | % 22.55/3.89 | ALPHA: (function-axioms) implies: % 22.55/3.89 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 22.55/3.89 | : ! [v3: $i] : (v1 = v0 | ~ (member(v3, v2) = v1) | ~ (member(v3, % 22.55/3.89 | v2) = v0)) % 22.55/3.89 | (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 22.55/3.89 | : ! [v3: $i] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, % 22.55/3.89 | v2) = v0)) % 22.55/3.89 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 22.55/3.89 | : ! [v3: $i] : (v1 = v0 | ~ (equal_set(v3, v2) = v1) | ~ % 22.55/3.89 | (equal_set(v3, v2) = v0)) % 22.55/3.89 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 22.55/3.89 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = v1) | % 22.55/3.89 | ~ (apply(v4, v3, v2) = v0)) % 22.55/3.89 | % 22.55/3.89 | DELTA: instantiating (thII21) with fresh symbols all_32_0, all_32_1, all_32_2, % 22.55/3.89 | all_32_3, all_32_4, all_32_5 gives: % 22.93/3.89 | (17) ~ (all_32_0 = 0) & image2(all_32_5, all_32_3) = all_32_1 & % 22.93/3.89 | maps(all_32_4, all_32_3, all_32_1) = all_32_0 & maps(all_32_5, % 22.93/3.89 | all_32_3, all_32_2) = 0 & subset(all_32_1, all_32_2) = 0 & % 22.93/3.89 | $i(all_32_1) & $i(all_32_2) & $i(all_32_3) & $i(all_32_4) & % 22.93/3.89 | $i(all_32_5) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 22.93/3.89 | (apply(all_32_4, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 22.93/3.89 | any] : ? [v4: any] : ? [v5: any] : (apply(all_32_5, v0, v1) = v5 % 22.93/3.89 | & member(v1, all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 % 22.93/3.89 | = 0) | ~ (v3 = 0) | (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | % 22.93/3.89 | v5 = 0))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 22.93/3.89 | (apply(all_32_5, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 22.93/3.89 | any] : ? [v4: any] : ? [v5: any] : (apply(all_32_4, v0, v1) = v5 % 22.93/3.89 | & member(v1, all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 % 22.93/3.89 | = 0) | ~ (v3 = 0) | (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | % 22.93/3.89 | v5 = 0))))) % 22.93/3.89 | % 22.93/3.89 | ALPHA: (17) implies: % 22.93/3.89 | (18) ~ (all_32_0 = 0) % 22.93/3.89 | (19) $i(all_32_5) % 22.93/3.89 | (20) $i(all_32_4) % 22.93/3.89 | (21) $i(all_32_3) % 22.93/3.89 | (22) $i(all_32_2) % 22.93/3.89 | (23) $i(all_32_1) % 22.93/3.89 | (24) subset(all_32_1, all_32_2) = 0 % 22.93/3.89 | (25) maps(all_32_5, all_32_3, all_32_2) = 0 % 22.93/3.90 | (26) maps(all_32_4, all_32_3, all_32_1) = all_32_0 % 22.93/3.90 | (27) image2(all_32_5, all_32_3) = all_32_1 % 22.93/3.90 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_32_5, v0, % 22.93/3.90 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 22.93/3.90 | : ? [v5: any] : (apply(all_32_4, v0, v1) = v5 & member(v1, % 22.93/3.90 | all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 = 0) | ~ % 22.93/3.90 | (v3 = 0) | (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) % 22.93/3.90 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_32_4, v0, % 22.93/3.90 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 22.93/3.90 | : ? [v5: any] : (apply(all_32_5, v0, v1) = v5 & member(v1, % 22.93/3.90 | all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 = 0) | ~ % 22.93/3.90 | (v3 = 0) | (( ~ (v5 = 0) | v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) % 22.93/3.90 | % 22.93/3.90 | GROUND_INST: instantiating (4) with all_32_2, all_32_1, simplifying with (22), % 22.93/3.90 | (23), (24) gives: % 22.93/3.90 | (30) ? [v0: any] : ? [v1: any] : (equal_set(all_32_2, all_32_1) = v1 & % 22.93/3.90 | subset(all_32_2, all_32_1) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 22.93/3.90 | % 22.93/3.90 | GROUND_INST: instantiating (3) with all_32_1, all_32_2, simplifying with (22), % 22.93/3.90 | (23), (24) gives: % 22.93/3.90 | (31) ? [v0: any] : ? [v1: any] : (equal_set(all_32_1, all_32_2) = v1 & % 22.93/3.90 | subset(all_32_2, all_32_1) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 22.93/3.90 | % 22.93/3.90 | GROUND_INST: instantiating (6) with all_32_2, all_32_1, 0, simplifying with % 22.93/3.90 | (22), (23), (24) gives: % 22.93/3.90 | (32) ? [v0: any] : ? [v1: any] : (equal_set(all_32_2, all_32_1) = v0 & % 22.93/3.90 | subset(all_32_2, all_32_1) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 22.93/3.90 | % 22.93/3.90 | GROUND_INST: instantiating (5) with all_32_1, all_32_2, 0, simplifying with % 22.93/3.90 | (22), (23), (24) gives: % 22.93/3.90 | (33) ? [v0: any] : ? [v1: any] : (equal_set(all_32_1, all_32_2) = v0 & % 22.93/3.90 | subset(all_32_2, all_32_1) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 22.93/3.90 | % 22.93/3.90 | GROUND_INST: instantiating (8) with all_32_4, all_32_3, all_32_1, all_32_0, % 22.93/3.90 | simplifying with (20), (21), (23), (26) gives: % 22.93/3.90 | (34) all_32_0 = 0 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] % 22.93/3.90 | : ? [v4: int] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: % 22.93/3.90 | $i] : ? [v9: int] : ($i(v8) & $i(v2) & $i(v1) & $i(v0) & ((v9 = 0 & % 22.93/3.90 | member(v8, all_32_3) = 0 & ! [v10: $i] : ( ~ (apply(all_32_4, % 22.93/3.90 | v8, v10) = 0) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = 0) % 22.93/3.90 | & member(v10, all_32_1) = v11)) & ! [v10: $i] : ( ~ % 22.93/3.90 | (member(v10, all_32_1) = 0) | ~ $i(v10) | ? [v11: int] : ( ~ % 22.93/3.90 | (v11 = 0) & apply(all_32_4, v8, v10) = v11))) | (v7 = 0 & v6 % 22.93/3.90 | = 0 & v5 = 0 & v4 = 0 & v3 = 0 & ~ (v2 = v1) & apply(all_32_4, % 22.93/3.90 | v0, v2) = 0 & apply(all_32_4, v0, v1) = 0 & member(v2, % 22.93/3.90 | all_32_1) = 0 & member(v1, all_32_1) = 0 & member(v0, % 22.93/3.90 | all_32_3) = 0))) % 22.93/3.90 | % 22.93/3.90 | DELTA: instantiating (33) with fresh symbols all_42_0, all_42_1 gives: % 22.93/3.90 | (35) equal_set(all_32_1, all_32_2) = all_42_1 & subset(all_32_2, all_32_1) % 22.93/3.90 | = all_42_0 & ( ~ (all_42_1 = 0) | all_42_0 = 0) % 22.93/3.90 | % 22.93/3.90 | ALPHA: (35) implies: % 22.93/3.90 | (36) subset(all_32_2, all_32_1) = all_42_0 % 22.93/3.90 | (37) equal_set(all_32_1, all_32_2) = all_42_1 % 22.93/3.90 | (38) ~ (all_42_1 = 0) | all_42_0 = 0 % 22.93/3.90 | % 22.93/3.90 | DELTA: instantiating (31) with fresh symbols all_44_0, all_44_1 gives: % 22.93/3.90 | (39) equal_set(all_32_1, all_32_2) = all_44_0 & subset(all_32_2, all_32_1) % 22.93/3.90 | = all_44_1 & ( ~ (all_44_1 = 0) | all_44_0 = 0) % 22.93/3.90 | % 22.93/3.90 | ALPHA: (39) implies: % 22.93/3.90 | (40) subset(all_32_2, all_32_1) = all_44_1 % 22.93/3.90 | (41) equal_set(all_32_1, all_32_2) = all_44_0 % 22.93/3.90 | (42) ~ (all_44_1 = 0) | all_44_0 = 0 % 23.12/3.90 | % 23.12/3.90 | DELTA: instantiating (30) with fresh symbols all_46_0, all_46_1 gives: % 23.12/3.90 | (43) equal_set(all_32_2, all_32_1) = all_46_0 & subset(all_32_2, all_32_1) % 23.12/3.90 | = all_46_1 & ( ~ (all_46_1 = 0) | all_46_0 = 0) % 23.12/3.90 | % 23.12/3.90 | ALPHA: (43) implies: % 23.12/3.91 | (44) subset(all_32_2, all_32_1) = all_46_1 % 23.12/3.91 | % 23.12/3.91 | DELTA: instantiating (32) with fresh symbols all_48_0, all_48_1 gives: % 23.12/3.91 | (45) equal_set(all_32_2, all_32_1) = all_48_1 & subset(all_32_2, all_32_1) % 23.12/3.91 | = all_48_0 & ( ~ (all_48_1 = 0) | all_48_0 = 0) % 23.12/3.91 | % 23.12/3.91 | ALPHA: (45) implies: % 23.12/3.91 | (46) subset(all_32_2, all_32_1) = all_48_0 % 23.12/3.91 | % 23.12/3.91 | BETA: splitting (34) gives: % 23.12/3.91 | % 23.12/3.91 | Case 1: % 23.12/3.91 | | % 23.12/3.91 | | (47) all_32_0 = 0 % 23.12/3.91 | | % 23.12/3.91 | | REDUCE: (18), (47) imply: % 23.12/3.91 | | (48) $false % 23.12/3.91 | | % 23.12/3.91 | | CLOSE: (48) is inconsistent. % 23.12/3.91 | | % 23.12/3.91 | Case 2: % 23.12/3.91 | | % 23.12/3.91 | | (49) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ? [v4: % 23.12/3.91 | | int] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: $i] : % 23.12/3.91 | | ? [v9: int] : ($i(v8) & $i(v2) & $i(v1) & $i(v0) & ((v9 = 0 & % 23.12/3.91 | | member(v8, all_32_3) = 0 & ! [v10: $i] : ( ~ (apply(all_32_4, % 23.12/3.91 | | v8, v10) = 0) | ~ $i(v10) | ? [v11: int] : ( ~ (v11 = % 23.12/3.91 | | 0) & member(v10, all_32_1) = v11)) & ! [v10: $i] : ( ~ % 23.12/3.91 | | (member(v10, all_32_1) = 0) | ~ $i(v10) | ? [v11: int] : ( % 23.12/3.91 | | ~ (v11 = 0) & apply(all_32_4, v8, v10) = v11))) | (v7 = 0 % 23.12/3.91 | | & v6 = 0 & v5 = 0 & v4 = 0 & v3 = 0 & ~ (v2 = v1) & % 23.12/3.91 | | apply(all_32_4, v0, v2) = 0 & apply(all_32_4, v0, v1) = 0 & % 23.12/3.91 | | member(v2, all_32_1) = 0 & member(v1, all_32_1) = 0 & % 23.12/3.91 | | member(v0, all_32_3) = 0))) % 23.12/3.91 | | % 23.12/3.91 | | DELTA: instantiating (49) with fresh symbols all_54_0, all_54_1, all_54_2, % 23.12/3.91 | | all_54_3, all_54_4, all_54_5, all_54_6, all_54_7, all_54_8, all_54_9 % 23.12/3.91 | | gives: % 23.12/3.91 | | (50) $i(all_54_1) & $i(all_54_7) & $i(all_54_8) & $i(all_54_9) & % 23.12/3.91 | | ((all_54_0 = 0 & member(all_54_1, all_32_3) = 0 & ! [v0: $i] : ( ~ % 23.12/3.91 | | (apply(all_32_4, all_54_1, v0) = 0) | ~ $i(v0) | ? [v1: int] % 23.12/3.91 | | : ( ~ (v1 = 0) & member(v0, all_32_1) = v1)) & ! [v0: $i] : ( % 23.12/3.91 | | ~ (member(v0, all_32_1) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ % 23.12/3.91 | | (v1 = 0) & apply(all_32_4, all_54_1, v0) = v1))) | (all_54_2 % 23.12/3.91 | | = 0 & all_54_3 = 0 & all_54_4 = 0 & all_54_5 = 0 & all_54_6 = 0 % 23.12/3.91 | | & ~ (all_54_7 = all_54_8) & apply(all_32_4, all_54_9, all_54_7) % 23.12/3.91 | | = 0 & apply(all_32_4, all_54_9, all_54_8) = 0 & member(all_54_7, % 23.12/3.91 | | all_32_1) = 0 & member(all_54_8, all_32_1) = 0 & % 23.12/3.91 | | member(all_54_9, all_32_3) = 0)) % 23.12/3.91 | | % 23.12/3.91 | | ALPHA: (50) implies: % 23.12/3.91 | | (51) $i(all_54_9) % 23.12/3.91 | | (52) $i(all_54_8) % 23.12/3.91 | | (53) $i(all_54_7) % 23.12/3.91 | | (54) $i(all_54_1) % 23.12/3.91 | | (55) (all_54_0 = 0 & member(all_54_1, all_32_3) = 0 & ! [v0: $i] : ( ~ % 23.12/3.91 | | (apply(all_32_4, all_54_1, v0) = 0) | ~ $i(v0) | ? [v1: int] : % 23.12/3.91 | | ( ~ (v1 = 0) & member(v0, all_32_1) = v1)) & ! [v0: $i] : ( ~ % 23.12/3.91 | | (member(v0, all_32_1) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 23.12/3.91 | | = 0) & apply(all_32_4, all_54_1, v0) = v1))) | (all_54_2 = 0 % 23.12/3.91 | | & all_54_3 = 0 & all_54_4 = 0 & all_54_5 = 0 & all_54_6 = 0 & ~ % 23.12/3.91 | | (all_54_7 = all_54_8) & apply(all_32_4, all_54_9, all_54_7) = 0 & % 23.12/3.91 | | apply(all_32_4, all_54_9, all_54_8) = 0 & member(all_54_7, % 23.12/3.91 | | all_32_1) = 0 & member(all_54_8, all_32_1) = 0 & % 23.12/3.91 | | member(all_54_9, all_32_3) = 0) % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (14) with all_44_1, all_46_1, all_32_1, all_32_2, % 23.12/3.91 | | simplifying with (40), (44) gives: % 23.12/3.91 | | (56) all_46_1 = all_44_1 % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (14) with all_46_1, all_48_0, all_32_1, all_32_2, % 23.12/3.91 | | simplifying with (44), (46) gives: % 23.12/3.91 | | (57) all_48_0 = all_46_1 % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (14) with all_42_0, all_48_0, all_32_1, all_32_2, % 23.12/3.91 | | simplifying with (36), (46) gives: % 23.12/3.91 | | (58) all_48_0 = all_42_0 % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (15) with all_42_1, all_44_0, all_32_2, all_32_1, % 23.12/3.91 | | simplifying with (37), (41) gives: % 23.12/3.91 | | (59) all_44_0 = all_42_1 % 23.12/3.91 | | % 23.12/3.91 | | COMBINE_EQS: (57), (58) imply: % 23.12/3.91 | | (60) all_46_1 = all_42_0 % 23.12/3.91 | | % 23.12/3.91 | | SIMP: (60) implies: % 23.12/3.91 | | (61) all_46_1 = all_42_0 % 23.12/3.91 | | % 23.12/3.91 | | COMBINE_EQS: (56), (61) imply: % 23.12/3.91 | | (62) all_44_1 = all_42_0 % 23.12/3.91 | | % 23.12/3.91 | | SIMP: (62) implies: % 23.12/3.91 | | (63) all_44_1 = all_42_0 % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (2) with all_32_2, all_32_1, all_42_0, % 23.12/3.91 | | simplifying with (22), (23), (36) gives: % 23.12/3.91 | | (64) all_42_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 23.12/3.91 | | member(v0, all_32_1) = v1 & member(v0, all_32_2) = 0 & $i(v0)) % 23.12/3.91 | | % 23.12/3.91 | | GROUND_INST: instantiating (6) with all_32_1, all_32_2, all_42_0, % 23.12/3.92 | | simplifying with (22), (23), (36) gives: % 23.12/3.92 | | (65) ? [v0: any] : ? [v1: any] : (equal_set(all_32_1, all_32_2) = v0 & % 23.12/3.92 | | subset(all_32_1, all_32_2) = v1 & ( ~ (v0 = 0) | (v1 = 0 & % 23.12/3.92 | | all_42_0 = 0))) % 23.12/3.92 | | % 23.12/3.92 | | GROUND_INST: instantiating (5) with all_32_2, all_32_1, all_42_0, % 23.12/3.92 | | simplifying with (22), (23), (36) gives: % 23.12/3.92 | | (66) ? [v0: any] : ? [v1: any] : (equal_set(all_32_2, all_32_1) = v0 & % 23.12/3.92 | | subset(all_32_1, all_32_2) = v1 & ( ~ (v0 = 0) | (v1 = 0 & % 23.12/3.92 | | all_42_0 = 0))) % 23.12/3.92 | | % 23.12/3.92 | | DELTA: instantiating (66) with fresh symbols all_65_0, all_65_1 gives: % 23.12/3.92 | | (67) equal_set(all_32_2, all_32_1) = all_65_1 & subset(all_32_1, % 23.12/3.92 | | all_32_2) = all_65_0 & ( ~ (all_65_1 = 0) | (all_65_0 = 0 & % 23.12/3.92 | | all_42_0 = 0)) % 23.12/3.92 | | % 23.12/3.92 | | ALPHA: (67) implies: % 23.12/3.92 | | (68) subset(all_32_1, all_32_2) = all_65_0 % 23.12/3.92 | | % 23.12/3.92 | | DELTA: instantiating (65) with fresh symbols all_67_0, all_67_1 gives: % 23.12/3.92 | | (69) equal_set(all_32_1, all_32_2) = all_67_1 & subset(all_32_1, % 23.12/3.92 | | all_32_2) = all_67_0 & ( ~ (all_67_1 = 0) | (all_67_0 = 0 & % 23.12/3.92 | | all_42_0 = 0)) % 23.12/3.92 | | % 23.12/3.92 | | ALPHA: (69) implies: % 23.12/3.92 | | (70) subset(all_32_1, all_32_2) = all_67_0 % 23.12/3.92 | | % 23.12/3.92 | | GROUND_INST: instantiating (14) with 0, all_67_0, all_32_2, all_32_1, % 23.12/3.92 | | simplifying with (24), (70) gives: % 23.12/3.92 | | (71) all_67_0 = 0 % 23.12/3.92 | | % 23.12/3.92 | | GROUND_INST: instantiating (14) with all_65_0, all_67_0, all_32_2, all_32_1, % 23.12/3.92 | | simplifying with (68), (70) gives: % 23.12/3.92 | | (72) all_67_0 = all_65_0 % 23.12/3.92 | | % 23.12/3.92 | | COMBINE_EQS: (71), (72) imply: % 23.12/3.92 | | (73) all_65_0 = 0 % 23.12/3.92 | | % 23.12/3.92 | | BETA: splitting (38) gives: % 23.12/3.92 | | % 23.12/3.92 | | Case 1: % 23.12/3.92 | | | % 23.12/3.92 | | | (74) ~ (all_42_1 = 0) % 23.12/3.92 | | | % 23.12/3.92 | | | BETA: splitting (42) gives: % 23.12/3.92 | | | % 23.12/3.92 | | | Case 1: % 23.12/3.92 | | | | % 23.12/3.92 | | | | (75) ~ (all_44_1 = 0) % 23.12/3.92 | | | | % 23.12/3.92 | | | | REDUCE: (63), (75) imply: % 23.12/3.92 | | | | (76) ~ (all_42_0 = 0) % 23.12/3.92 | | | | % 23.12/3.92 | | | | BETA: splitting (64) gives: % 23.12/3.92 | | | | % 23.12/3.92 | | | | Case 1: % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | (77) all_42_0 = 0 % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | REDUCE: (76), (77) imply: % 23.12/3.92 | | | | | (78) $false % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | CLOSE: (78) is inconsistent. % 23.12/3.92 | | | | | % 23.12/3.92 | | | | Case 2: % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | (79) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & member(v0, % 23.12/3.92 | | | | | all_32_1) = v1 & member(v0, all_32_2) = 0 & $i(v0)) % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | DELTA: instantiating (79) with fresh symbols all_92_0, all_92_1 gives: % 23.12/3.92 | | | | | (80) ~ (all_92_0 = 0) & member(all_92_1, all_32_1) = all_92_0 & % 23.12/3.92 | | | | | member(all_92_1, all_32_2) = 0 & $i(all_92_1) % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | ALPHA: (80) implies: % 23.12/3.92 | | | | | (81) ~ (all_92_0 = 0) % 23.12/3.92 | | | | | (82) $i(all_92_1) % 23.12/3.92 | | | | | (83) member(all_92_1, all_32_1) = all_92_0 % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | BETA: splitting (55) gives: % 23.12/3.92 | | | | | % 23.12/3.92 | | | | | Case 1: % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | (84) all_54_0 = 0 & member(all_54_1, all_32_3) = 0 & ! [v0: $i] % 23.12/3.92 | | | | | | : ( ~ (apply(all_32_4, all_54_1, v0) = 0) | ~ $i(v0) | ? % 23.12/3.92 | | | | | | [v1: int] : ( ~ (v1 = 0) & member(v0, all_32_1) = v1)) & % 23.12/3.92 | | | | | | ! [v0: $i] : ( ~ (member(v0, all_32_1) = 0) | ~ $i(v0) | ? % 23.12/3.92 | | | | | | [v1: int] : ( ~ (v1 = 0) & apply(all_32_4, all_54_1, v0) = % 23.12/3.92 | | | | | | v1)) % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | ALPHA: (84) implies: % 23.12/3.92 | | | | | | (85) member(all_54_1, all_32_3) = 0 % 23.12/3.92 | | | | | | (86) ! [v0: $i] : ( ~ (apply(all_32_4, all_54_1, v0) = 0) | ~ % 23.12/3.92 | | | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & member(v0, % 23.12/3.92 | | | | | | all_32_1) = v1)) % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | GROUND_INST: instantiating (7) with all_32_5, all_32_3, all_32_2, % 23.12/3.92 | | | | | | all_54_1, simplifying with (19), (21), (22), (25), % 23.12/3.92 | | | | | | (54), (85) gives: % 23.12/3.92 | | | | | | (87) ? [v0: $i] : (apply(all_32_5, all_54_1, v0) = 0 & % 23.12/3.92 | | | | | | member(v0, all_32_2) = 0 & $i(v0)) % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | GROUND_INST: instantiating (11) with all_32_5, all_32_3, all_92_1, % 23.12/3.92 | | | | | | all_32_1, all_92_0, all_54_1, simplifying with (19), % 23.12/3.92 | | | | | | (21), (27), (54), (82), (83), (85) gives: % 23.12/3.92 | | | | | | (88) all_92_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & apply(all_32_5, % 23.12/3.92 | | | | | | all_54_1, all_92_1) = v0) % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | DELTA: instantiating (87) with fresh symbol all_112_0 gives: % 23.12/3.92 | | | | | | (89) apply(all_32_5, all_54_1, all_112_0) = 0 & member(all_112_0, % 23.12/3.92 | | | | | | all_32_2) = 0 & $i(all_112_0) % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | ALPHA: (89) implies: % 23.12/3.92 | | | | | | (90) $i(all_112_0) % 23.12/3.92 | | | | | | (91) apply(all_32_5, all_54_1, all_112_0) = 0 % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | BETA: splitting (88) gives: % 23.12/3.92 | | | | | | % 23.12/3.92 | | | | | | Case 1: % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | (92) all_92_0 = 0 % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | REDUCE: (81), (92) imply: % 23.12/3.92 | | | | | | | (93) $false % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | CLOSE: (93) is inconsistent. % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | Case 2: % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | (94) ? [v0: int] : ( ~ (v0 = 0) & apply(all_32_5, all_54_1, % 23.12/3.92 | | | | | | | all_92_1) = v0) % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | DELTA: instantiating (94) with fresh symbol all_118_0 gives: % 23.12/3.92 | | | | | | | (95) ~ (all_118_0 = 0) & apply(all_32_5, all_54_1, all_92_1) = % 23.12/3.92 | | | | | | | all_118_0 % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | ALPHA: (95) implies: % 23.12/3.92 | | | | | | | (96) apply(all_32_5, all_54_1, all_92_1) = all_118_0 % 23.12/3.92 | | | | | | | % 23.12/3.92 | | | | | | | GROUND_INST: instantiating (28) with all_54_1, all_92_1, % 23.12/3.92 | | | | | | | all_118_0, simplifying with (54), (82), (96) gives: % 23.12/3.93 | | | | | | | (97) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.12/3.93 | | | | | | | (apply(all_32_4, all_54_1, all_92_1) = v2 & % 23.12/3.93 | | | | | | | member(all_92_1, all_32_1) = v1 & member(all_54_1, % 23.12/3.93 | | | | | | | all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (( ~ (v2 % 23.12/3.93 | | | | | | | = 0) | all_118_0 = 0) & ( ~ (all_118_0 = 0) | v2 % 23.12/3.93 | | | | | | | = 0)))) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (28) with all_54_1, all_112_0, 0, % 23.12/3.93 | | | | | | | simplifying with (54), (90), (91) gives: % 23.12/3.93 | | | | | | | (98) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.12/3.93 | | | | | | | (apply(all_32_4, all_54_1, all_112_0) = v2 & % 23.12/3.93 | | | | | | | member(all_112_0, all_32_1) = v1 & member(all_54_1, % 23.12/3.93 | | | | | | | all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | DELTA: instantiating (98) with fresh symbols all_125_0, all_125_1, % 23.12/3.93 | | | | | | | all_125_2 gives: % 23.12/3.93 | | | | | | | (99) apply(all_32_4, all_54_1, all_112_0) = all_125_0 & % 23.12/3.93 | | | | | | | member(all_112_0, all_32_1) = all_125_1 & member(all_54_1, % 23.12/3.93 | | | | | | | all_32_3) = all_125_2 & ( ~ (all_125_1 = 0) | ~ % 23.12/3.93 | | | | | | | (all_125_2 = 0) | all_125_0 = 0) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | ALPHA: (99) implies: % 23.12/3.93 | | | | | | | (100) member(all_54_1, all_32_3) = all_125_2 % 23.12/3.93 | | | | | | | (101) member(all_112_0, all_32_1) = all_125_1 % 23.12/3.93 | | | | | | | (102) apply(all_32_4, all_54_1, all_112_0) = all_125_0 % 23.12/3.93 | | | | | | | (103) ~ (all_125_1 = 0) | ~ (all_125_2 = 0) | all_125_0 = 0 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | DELTA: instantiating (97) with fresh symbols all_127_0, all_127_1, % 23.12/3.93 | | | | | | | all_127_2 gives: % 23.12/3.93 | | | | | | | (104) apply(all_32_4, all_54_1, all_92_1) = all_127_0 & % 23.12/3.93 | | | | | | | member(all_92_1, all_32_1) = all_127_1 & member(all_54_1, % 23.12/3.93 | | | | | | | all_32_3) = all_127_2 & ( ~ (all_127_1 = 0) | ~ % 23.12/3.93 | | | | | | | (all_127_2 = 0) | (( ~ (all_127_0 = 0) | all_118_0 = 0) % 23.12/3.93 | | | | | | | & ( ~ (all_118_0 = 0) | all_127_0 = 0))) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | ALPHA: (104) implies: % 23.12/3.93 | | | | | | | (105) member(all_54_1, all_32_3) = all_127_2 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (13) with 0, all_127_2, all_32_3, % 23.12/3.93 | | | | | | | all_54_1, simplifying with (85), (105) gives: % 23.12/3.93 | | | | | | | (106) all_127_2 = 0 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (13) with all_125_2, all_127_2, % 23.12/3.93 | | | | | | | all_32_3, all_54_1, simplifying with (100), (105) % 23.12/3.93 | | | | | | | gives: % 23.12/3.93 | | | | | | | (107) all_127_2 = all_125_2 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | COMBINE_EQS: (106), (107) imply: % 23.12/3.93 | | | | | | | (108) all_125_2 = 0 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (12) with all_32_5, all_32_3, % 23.12/3.93 | | | | | | | all_112_0, all_32_1, all_125_1, all_54_1, simplifying % 23.12/3.93 | | | | | | | with (19), (21), (27), (54), (90), (91), (101) gives: % 23.12/3.93 | | | | | | | (109) all_125_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 23.12/3.93 | | | | | | | member(all_54_1, all_32_3) = v0) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (29) with all_54_1, all_112_0, % 23.12/3.93 | | | | | | | all_125_0, simplifying with (54), (90), (102) gives: % 23.12/3.93 | | | | | | | (110) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.12/3.93 | | | | | | | (apply(all_32_5, all_54_1, all_112_0) = v2 & % 23.12/3.93 | | | | | | | member(all_112_0, all_32_1) = v1 & member(all_54_1, % 23.12/3.93 | | | | | | | all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (( ~ % 23.12/3.93 | | | | | | | (v2 = 0) | all_125_0 = 0) & ( ~ (all_125_0 = 0) | % 23.12/3.93 | | | | | | | v2 = 0)))) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | DELTA: instantiating (110) with fresh symbols all_138_0, % 23.12/3.93 | | | | | | | all_138_1, all_138_2 gives: % 23.12/3.93 | | | | | | | (111) apply(all_32_5, all_54_1, all_112_0) = all_138_0 & % 23.12/3.93 | | | | | | | member(all_112_0, all_32_1) = all_138_1 & % 23.12/3.93 | | | | | | | member(all_54_1, all_32_3) = all_138_2 & ( ~ (all_138_1 = % 23.12/3.93 | | | | | | | 0) | ~ (all_138_2 = 0) | (( ~ (all_138_0 = 0) | % 23.12/3.93 | | | | | | | all_125_0 = 0) & ( ~ (all_125_0 = 0) | all_138_0 = % 23.12/3.93 | | | | | | | 0))) % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | ALPHA: (111) implies: % 23.12/3.93 | | | | | | | (112) member(all_54_1, all_32_3) = all_138_2 % 23.12/3.93 | | | | | | | (113) member(all_112_0, all_32_1) = all_138_1 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (13) with 0, all_138_2, all_32_3, % 23.12/3.93 | | | | | | | all_54_1, simplifying with (85), (112) gives: % 23.12/3.93 | | | | | | | (114) all_138_2 = 0 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | GROUND_INST: instantiating (13) with all_125_1, all_138_1, % 23.12/3.93 | | | | | | | all_32_1, all_112_0, simplifying with (101), (113) % 23.12/3.93 | | | | | | | gives: % 23.12/3.93 | | | | | | | (115) all_138_1 = all_125_1 % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | BETA: splitting (109) gives: % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | | Case 1: % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | (116) all_125_1 = 0 % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | REDUCE: (101), (116) imply: % 23.12/3.93 | | | | | | | | (117) member(all_112_0, all_32_1) = 0 % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | BETA: splitting (103) gives: % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | Case 1: % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | (118) ~ (all_125_1 = 0) % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | REDUCE: (116), (118) imply: % 23.12/3.93 | | | | | | | | | (119) $false % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | CLOSE: (119) is inconsistent. % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | Case 2: % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | (120) ~ (all_125_2 = 0) | all_125_0 = 0 % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | BETA: splitting (120) gives: % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | | Case 1: % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | (121) ~ (all_125_2 = 0) % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | REDUCE: (108), (121) imply: % 23.12/3.93 | | | | | | | | | | (122) $false % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | CLOSE: (122) is inconsistent. % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | Case 2: % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | (123) all_125_0 = 0 % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | REDUCE: (102), (123) imply: % 23.12/3.93 | | | | | | | | | | (124) apply(all_32_4, all_54_1, all_112_0) = 0 % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | GROUND_INST: instantiating (86) with all_112_0, simplifying % 23.12/3.93 | | | | | | | | | | with (90), (124) gives: % 23.12/3.93 | | | | | | | | | | (125) ? [v0: int] : ( ~ (v0 = 0) & member(all_112_0, % 23.12/3.93 | | | | | | | | | | all_32_1) = v0) % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | DELTA: instantiating (125) with fresh symbol all_165_0 % 23.12/3.93 | | | | | | | | | | gives: % 23.12/3.93 | | | | | | | | | | (126) ~ (all_165_0 = 0) & member(all_112_0, all_32_1) = % 23.12/3.93 | | | | | | | | | | all_165_0 % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | ALPHA: (126) implies: % 23.12/3.93 | | | | | | | | | | (127) ~ (all_165_0 = 0) % 23.12/3.93 | | | | | | | | | | (128) member(all_112_0, all_32_1) = all_165_0 % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | GROUND_INST: instantiating (13) with 0, all_165_0, all_32_1, % 23.12/3.93 | | | | | | | | | | all_112_0, simplifying with (117), (128) gives: % 23.12/3.93 | | | | | | | | | | (129) all_165_0 = 0 % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | REDUCE: (127), (129) imply: % 23.12/3.93 | | | | | | | | | | (130) $false % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | | CLOSE: (130) is inconsistent. % 23.12/3.93 | | | | | | | | | | % 23.12/3.93 | | | | | | | | | End of split % 23.12/3.93 | | | | | | | | | % 23.12/3.93 | | | | | | | | End of split % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | Case 2: % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | (131) ? [v0: int] : ( ~ (v0 = 0) & member(all_54_1, % 23.12/3.93 | | | | | | | | all_32_3) = v0) % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | DELTA: instantiating (131) with fresh symbol all_148_0 gives: % 23.12/3.93 | | | | | | | | (132) ~ (all_148_0 = 0) & member(all_54_1, all_32_3) = % 23.12/3.93 | | | | | | | | all_148_0 % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | ALPHA: (132) implies: % 23.12/3.93 | | | | | | | | (133) ~ (all_148_0 = 0) % 23.12/3.93 | | | | | | | | (134) member(all_54_1, all_32_3) = all_148_0 % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | GROUND_INST: instantiating (13) with 0, all_148_0, all_32_3, % 23.12/3.93 | | | | | | | | all_54_1, simplifying with (85), (134) gives: % 23.12/3.93 | | | | | | | | (135) all_148_0 = 0 % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | REDUCE: (133), (135) imply: % 23.12/3.93 | | | | | | | | (136) $false % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | | CLOSE: (136) is inconsistent. % 23.12/3.93 | | | | | | | | % 23.12/3.93 | | | | | | | End of split % 23.12/3.93 | | | | | | | % 23.12/3.93 | | | | | | End of split % 23.12/3.93 | | | | | | % 23.12/3.93 | | | | | Case 2: % 23.12/3.93 | | | | | | % 23.12/3.93 | | | | | | (137) all_54_2 = 0 & all_54_3 = 0 & all_54_4 = 0 & all_54_5 = 0 & % 23.12/3.93 | | | | | | all_54_6 = 0 & ~ (all_54_7 = all_54_8) & apply(all_32_4, % 23.12/3.93 | | | | | | all_54_9, all_54_7) = 0 & apply(all_32_4, all_54_9, % 23.12/3.93 | | | | | | all_54_8) = 0 & member(all_54_7, all_32_1) = 0 & % 23.12/3.93 | | | | | | member(all_54_8, all_32_1) = 0 & member(all_54_9, all_32_3) % 23.12/3.93 | | | | | | = 0 % 23.12/3.93 | | | | | | % 23.12/3.93 | | | | | | ALPHA: (137) implies: % 23.12/3.93 | | | | | | (138) ~ (all_54_7 = all_54_8) % 23.12/3.93 | | | | | | (139) member(all_54_9, all_32_3) = 0 % 23.12/3.93 | | | | | | (140) member(all_54_8, all_32_1) = 0 % 23.12/3.93 | | | | | | (141) member(all_54_7, all_32_1) = 0 % 23.12/3.93 | | | | | | (142) apply(all_32_4, all_54_9, all_54_8) = 0 % 23.12/3.93 | | | | | | (143) apply(all_32_4, all_54_9, all_54_7) = 0 % 23.12/3.93 | | | | | | % 23.12/3.94 | | | | | | REF_CLOSE: (1), (7), (9), (10), (13), (16), (19), (21), (22), (23), % 23.12/3.94 | | | | | | (24), (25), (27), (29), (51), (52), (53), (138), (139), % 23.12/3.94 | | | | | | (140), (141), (142), (143) are inconsistent by sub-proof % 23.12/3.94 | | | | | | #1. % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | End of split % 23.12/3.94 | | | | | % 23.12/3.94 | | | | End of split % 23.12/3.94 | | | | % 23.12/3.94 | | | Case 2: % 23.12/3.94 | | | | % 23.12/3.94 | | | | (144) all_44_0 = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | COMBINE_EQS: (59), (144) imply: % 23.12/3.94 | | | | (145) all_42_1 = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | REDUCE: (74), (145) imply: % 23.12/3.94 | | | | (146) $false % 23.12/3.94 | | | | % 23.12/3.94 | | | | CLOSE: (146) is inconsistent. % 23.12/3.94 | | | | % 23.12/3.94 | | | End of split % 23.12/3.94 | | | % 23.12/3.94 | | Case 2: % 23.12/3.94 | | | % 23.12/3.94 | | | (147) all_42_0 = 0 % 23.12/3.94 | | | % 23.12/3.94 | | | REDUCE: (36), (147) imply: % 23.12/3.94 | | | (148) subset(all_32_2, all_32_1) = 0 % 23.12/3.94 | | | % 23.12/3.94 | | | BETA: splitting (55) gives: % 23.12/3.94 | | | % 23.12/3.94 | | | Case 1: % 23.12/3.94 | | | | % 23.12/3.94 | | | | (149) all_54_0 = 0 & member(all_54_1, all_32_3) = 0 & ! [v0: $i] : ( % 23.12/3.94 | | | | ~ (apply(all_32_4, all_54_1, v0) = 0) | ~ $i(v0) | ? [v1: % 23.12/3.94 | | | | int] : ( ~ (v1 = 0) & member(v0, all_32_1) = v1)) & ! [v0: % 23.12/3.94 | | | | $i] : ( ~ (member(v0, all_32_1) = 0) | ~ $i(v0) | ? [v1: % 23.12/3.94 | | | | int] : ( ~ (v1 = 0) & apply(all_32_4, all_54_1, v0) = v1)) % 23.12/3.94 | | | | % 23.12/3.94 | | | | ALPHA: (149) implies: % 23.12/3.94 | | | | (150) member(all_54_1, all_32_3) = 0 % 23.12/3.94 | | | | (151) ! [v0: $i] : ( ~ (apply(all_32_4, all_54_1, v0) = 0) | ~ % 23.12/3.94 | | | | $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & member(v0, all_32_1) = % 23.12/3.94 | | | | v1)) % 23.12/3.94 | | | | % 23.12/3.94 | | | | GROUND_INST: instantiating (7) with all_32_5, all_32_3, all_32_2, % 23.12/3.94 | | | | all_54_1, simplifying with (19), (21), (22), (25), (54), % 23.12/3.94 | | | | (150) gives: % 23.12/3.94 | | | | (152) ? [v0: $i] : (apply(all_32_5, all_54_1, v0) = 0 & member(v0, % 23.12/3.94 | | | | all_32_2) = 0 & $i(v0)) % 23.12/3.94 | | | | % 23.12/3.94 | | | | DELTA: instantiating (152) with fresh symbol all_104_0 gives: % 23.12/3.94 | | | | (153) apply(all_32_5, all_54_1, all_104_0) = 0 & member(all_104_0, % 23.12/3.94 | | | | all_32_2) = 0 & $i(all_104_0) % 23.12/3.94 | | | | % 23.12/3.94 | | | | ALPHA: (153) implies: % 23.12/3.94 | | | | (154) $i(all_104_0) % 23.12/3.94 | | | | (155) member(all_104_0, all_32_2) = 0 % 23.12/3.94 | | | | (156) apply(all_32_5, all_54_1, all_104_0) = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | GROUND_INST: instantiating (1) with all_32_2, all_32_1, all_104_0, % 23.12/3.94 | | | | simplifying with (22), (23), (148), (154), (155) gives: % 23.12/3.94 | | | | (157) member(all_104_0, all_32_1) = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | GROUND_INST: instantiating (28) with all_54_1, all_104_0, 0, simplifying % 23.12/3.94 | | | | with (54), (154), (156) gives: % 23.12/3.94 | | | | (158) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_32_4, % 23.12/3.94 | | | | all_54_1, all_104_0) = v2 & member(all_104_0, all_32_1) = % 23.12/3.94 | | | | v1 & member(all_54_1, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 % 23.12/3.94 | | | | = 0) | v2 = 0)) % 23.12/3.94 | | | | % 23.12/3.94 | | | | DELTA: instantiating (158) with fresh symbols all_112_0, all_112_1, % 23.12/3.94 | | | | all_112_2 gives: % 23.12/3.94 | | | | (159) apply(all_32_4, all_54_1, all_104_0) = all_112_0 & % 23.12/3.94 | | | | member(all_104_0, all_32_1) = all_112_1 & member(all_54_1, % 23.12/3.94 | | | | all_32_3) = all_112_2 & ( ~ (all_112_1 = 0) | ~ (all_112_2 = % 23.12/3.94 | | | | 0) | all_112_0 = 0) % 23.12/3.94 | | | | % 23.12/3.94 | | | | ALPHA: (159) implies: % 23.12/3.94 | | | | (160) member(all_54_1, all_32_3) = all_112_2 % 23.12/3.94 | | | | (161) member(all_104_0, all_32_1) = all_112_1 % 23.12/3.94 | | | | (162) apply(all_32_4, all_54_1, all_104_0) = all_112_0 % 23.12/3.94 | | | | (163) ~ (all_112_1 = 0) | ~ (all_112_2 = 0) | all_112_0 = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | GROUND_INST: instantiating (13) with 0, all_112_2, all_32_3, all_54_1, % 23.12/3.94 | | | | simplifying with (150), (160) gives: % 23.12/3.94 | | | | (164) all_112_2 = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | GROUND_INST: instantiating (13) with 0, all_112_1, all_32_1, all_104_0, % 23.12/3.94 | | | | simplifying with (157), (161) gives: % 23.12/3.94 | | | | (165) all_112_1 = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | BETA: splitting (163) gives: % 23.12/3.94 | | | | % 23.12/3.94 | | | | Case 1: % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | (166) ~ (all_112_1 = 0) % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | REDUCE: (165), (166) imply: % 23.12/3.94 | | | | | (167) $false % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | CLOSE: (167) is inconsistent. % 23.12/3.94 | | | | | % 23.12/3.94 | | | | Case 2: % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | (168) ~ (all_112_2 = 0) | all_112_0 = 0 % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | BETA: splitting (168) gives: % 23.12/3.94 | | | | | % 23.12/3.94 | | | | | Case 1: % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | (169) ~ (all_112_2 = 0) % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | REDUCE: (164), (169) imply: % 23.12/3.94 | | | | | | (170) $false % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | CLOSE: (170) is inconsistent. % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | Case 2: % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | (171) all_112_0 = 0 % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | REDUCE: (162), (171) imply: % 23.12/3.94 | | | | | | (172) apply(all_32_4, all_54_1, all_104_0) = 0 % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | GROUND_INST: instantiating (151) with all_104_0, simplifying with % 23.12/3.94 | | | | | | (154), (172) gives: % 23.12/3.94 | | | | | | (173) ? [v0: int] : ( ~ (v0 = 0) & member(all_104_0, all_32_1) = % 23.12/3.94 | | | | | | v0) % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | DELTA: instantiating (173) with fresh symbol all_131_0 gives: % 23.12/3.94 | | | | | | (174) ~ (all_131_0 = 0) & member(all_104_0, all_32_1) = % 23.12/3.94 | | | | | | all_131_0 % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | ALPHA: (174) implies: % 23.12/3.94 | | | | | | (175) ~ (all_131_0 = 0) % 23.12/3.94 | | | | | | (176) member(all_104_0, all_32_1) = all_131_0 % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | GROUND_INST: instantiating (13) with 0, all_131_0, all_32_1, % 23.12/3.94 | | | | | | all_104_0, simplifying with (157), (176) gives: % 23.12/3.94 | | | | | | (177) all_131_0 = 0 % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | REDUCE: (175), (177) imply: % 23.12/3.94 | | | | | | (178) $false % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | | CLOSE: (178) is inconsistent. % 23.12/3.94 | | | | | | % 23.12/3.94 | | | | | End of split % 23.12/3.94 | | | | | % 23.12/3.94 | | | | End of split % 23.12/3.94 | | | | % 23.12/3.94 | | | Case 2: % 23.12/3.94 | | | | % 23.12/3.94 | | | | (179) all_54_2 = 0 & all_54_3 = 0 & all_54_4 = 0 & all_54_5 = 0 & % 23.12/3.94 | | | | all_54_6 = 0 & ~ (all_54_7 = all_54_8) & apply(all_32_4, % 23.12/3.94 | | | | all_54_9, all_54_7) = 0 & apply(all_32_4, all_54_9, all_54_8) % 23.12/3.94 | | | | = 0 & member(all_54_7, all_32_1) = 0 & member(all_54_8, % 23.12/3.94 | | | | all_32_1) = 0 & member(all_54_9, all_32_3) = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | ALPHA: (179) implies: % 23.12/3.94 | | | | (180) ~ (all_54_7 = all_54_8) % 23.12/3.94 | | | | (181) member(all_54_9, all_32_3) = 0 % 23.12/3.94 | | | | (182) member(all_54_8, all_32_1) = 0 % 23.12/3.94 | | | | (183) member(all_54_7, all_32_1) = 0 % 23.12/3.94 | | | | (184) apply(all_32_4, all_54_9, all_54_8) = 0 % 23.12/3.94 | | | | (185) apply(all_32_4, all_54_9, all_54_7) = 0 % 23.12/3.94 | | | | % 23.12/3.94 | | | | REF_CLOSE: (1), (7), (9), (10), (13), (16), (19), (21), (22), (23), % 23.12/3.94 | | | | (24), (25), (27), (29), (51), (52), (53), (180), (181), % 23.12/3.94 | | | | (182), (183), (184), (185) are inconsistent by sub-proof #1. % 23.12/3.94 | | | | % 23.12/3.94 | | | End of split % 23.12/3.94 | | | % 23.12/3.94 | | End of split % 23.12/3.94 | | % 23.12/3.94 | End of split % 23.12/3.94 | % 23.12/3.94 End of proof % 23.12/3.94 % 23.12/3.94 Sub-proof #1 shows that the following formulas are inconsistent: % 23.12/3.94 ---------------------------------------------------------------- % 23.12/3.95 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.12/3.95 ! [v3: $i] : (v1 = v0 | ~ (member(v3, v2) = v1) | ~ (member(v3, v2) = % 23.12/3.95 v0)) % 23.12/3.95 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (subset(v0, v1) = 0) | ~ % 23.12/3.95 (member(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | member(v2, % 23.12/3.95 v1) = 0) % 23.12/3.95 (3) member(all_54_9, all_32_3) = 0 % 23.12/3.95 (4) $i(all_32_3) % 23.12/3.95 (5) $i(all_54_7) % 23.12/3.95 (6) ~ (all_54_7 = all_54_8) % 23.12/3.95 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (maps(v0, v1, % 23.12/3.95 v2) = 0) | ~ (member(v3, v1) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 23.12/3.95 $i(v1) | ~ $i(v0) | ? [v4: $i] : (apply(v0, v3, v4) = 0 & member(v4, % 23.12/3.95 v2) = 0 & $i(v4))) % 23.12/3.95 (8) $i(all_32_5) % 23.12/3.95 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (image2(v0, % 23.12/3.95 v1) = v3) | ~ (member(v2, v3) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 23.12/3.95 $i(v0) | ? [v4: $i] : (apply(v0, v4, v2) = 0 & member(v4, v1) = 0 & % 23.12/3.95 $i(v4))) % 23.12/3.95 (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 23.12/3.95 [v5: $i] : (v5 = v4 | ~ (maps(v0, v1, v2) = 0) | ~ (member(v5, v2) = % 23.12/3.95 0) | ~ (member(v4, v2) = 0) | ~ (member(v3, v1) = 0) | ~ $i(v5) | % 23.12/3.95 ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: % 23.12/3.95 any] : ? [v7: any] : (apply(v0, v3, v5) = v7 & apply(v0, v3, v4) = % 23.12/3.95 v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) % 23.12/3.95 (11) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_32_4, v0, v1) % 23.12/3.95 = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 23.12/3.95 [v5: any] : (apply(all_32_5, v0, v1) = v5 & member(v1, all_32_1) = v4 % 23.12/3.95 & member(v0, all_32_3) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | (( ~ (v5 % 23.12/3.95 = 0) | v2 = 0) & ( ~ (v2 = 0) | v5 = 0))))) % 23.12/3.95 (12) $i(all_32_1) % 23.12/3.95 (13) member(all_54_7, all_32_1) = 0 % 23.12/3.95 (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.12/3.95 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = v1) | ~ % 23.12/3.95 (apply(v4, v3, v2) = v0)) % 23.12/3.95 (15) $i(all_54_8) % 23.12/3.95 (16) image2(all_32_5, all_32_3) = all_32_1 % 23.12/3.95 (17) apply(all_32_4, all_54_9, all_54_7) = 0 % 23.12/3.95 (18) member(all_54_8, all_32_1) = 0 % 23.12/3.95 (19) apply(all_32_4, all_54_9, all_54_8) = 0 % 23.12/3.95 (20) maps(all_32_5, all_32_3, all_32_2) = 0 % 23.12/3.95 (21) subset(all_32_1, all_32_2) = 0 % 23.12/3.95 (22) $i(all_54_9) % 23.12/3.95 (23) $i(all_32_2) % 23.12/3.95 % 23.12/3.95 Begin of proof % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (7) with all_32_5, all_32_3, all_32_2, all_54_9, % 23.12/3.95 | simplifying with (3), (4), (8), (20), (22), (23) gives: % 23.12/3.95 | (24) ? [v0: $i] : (apply(all_32_5, all_54_9, v0) = 0 & member(v0, % 23.12/3.95 | all_32_2) = 0 & $i(v0)) % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (9) with all_32_5, all_32_3, all_54_8, all_32_1, % 23.12/3.95 | simplifying with (4), (8), (15), (16), (18) gives: % 23.12/3.95 | (25) ? [v0: $i] : (apply(all_32_5, v0, all_54_8) = 0 & member(v0, % 23.12/3.95 | all_32_3) = 0 & $i(v0)) % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (2) with all_32_1, all_32_2, all_54_8, simplifying % 23.12/3.95 | with (12), (15), (18), (21), (23) gives: % 23.12/3.95 | (26) member(all_54_8, all_32_2) = 0 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (2) with all_32_1, all_32_2, all_54_7, simplifying % 23.12/3.95 | with (5), (12), (13), (21), (23) gives: % 23.12/3.95 | (27) member(all_54_7, all_32_2) = 0 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (11) with all_54_9, all_54_8, 0, simplifying with % 23.12/3.95 | (15), (19), (22) gives: % 23.12/3.95 | (28) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_32_5, % 23.12/3.95 | all_54_9, all_54_8) = v2 & member(all_54_8, all_32_1) = v1 & % 23.12/3.95 | member(all_54_9, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = % 23.12/3.95 | 0)) % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (11) with all_54_9, all_54_7, 0, simplifying with % 23.12/3.95 | (5), (17), (22) gives: % 23.12/3.95 | (29) ? [v0: any] : ? [v1: any] : ? [v2: any] : (apply(all_32_5, % 23.12/3.95 | all_54_9, all_54_7) = v2 & member(all_54_7, all_32_1) = v1 & % 23.12/3.95 | member(all_54_9, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = % 23.12/3.95 | 0)) % 23.12/3.95 | % 23.12/3.95 | DELTA: instantiating (25) with fresh symbol all_104_0 gives: % 23.12/3.95 | (30) apply(all_32_5, all_104_0, all_54_8) = 0 & member(all_104_0, all_32_3) % 23.12/3.95 | = 0 & $i(all_104_0) % 23.12/3.95 | % 23.12/3.95 | ALPHA: (30) implies: % 23.12/3.95 | (31) $i(all_104_0) % 23.12/3.95 | (32) member(all_104_0, all_32_3) = 0 % 23.12/3.95 | % 23.12/3.95 | DELTA: instantiating (24) with fresh symbol all_106_0 gives: % 23.12/3.95 | (33) apply(all_32_5, all_54_9, all_106_0) = 0 & member(all_106_0, all_32_2) % 23.12/3.95 | = 0 & $i(all_106_0) % 23.12/3.95 | % 23.12/3.95 | ALPHA: (33) implies: % 23.12/3.95 | (34) $i(all_106_0) % 23.12/3.95 | (35) member(all_106_0, all_32_2) = 0 % 23.12/3.95 | (36) apply(all_32_5, all_54_9, all_106_0) = 0 % 23.12/3.95 | % 23.12/3.95 | DELTA: instantiating (29) with fresh symbols all_110_0, all_110_1, all_110_2 % 23.12/3.95 | gives: % 23.12/3.95 | (37) apply(all_32_5, all_54_9, all_54_7) = all_110_0 & member(all_54_7, % 23.12/3.95 | all_32_1) = all_110_1 & member(all_54_9, all_32_3) = all_110_2 & ( ~ % 23.12/3.95 | (all_110_1 = 0) | ~ (all_110_2 = 0) | all_110_0 = 0) % 23.12/3.95 | % 23.12/3.95 | ALPHA: (37) implies: % 23.12/3.95 | (38) member(all_54_9, all_32_3) = all_110_2 % 23.12/3.95 | (39) member(all_54_7, all_32_1) = all_110_1 % 23.12/3.95 | (40) apply(all_32_5, all_54_9, all_54_7) = all_110_0 % 23.12/3.95 | (41) ~ (all_110_1 = 0) | ~ (all_110_2 = 0) | all_110_0 = 0 % 23.12/3.95 | % 23.12/3.95 | DELTA: instantiating (28) with fresh symbols all_112_0, all_112_1, all_112_2 % 23.12/3.95 | gives: % 23.12/3.95 | (42) apply(all_32_5, all_54_9, all_54_8) = all_112_0 & member(all_54_8, % 23.12/3.95 | all_32_1) = all_112_1 & member(all_54_9, all_32_3) = all_112_2 & ( ~ % 23.12/3.95 | (all_112_1 = 0) | ~ (all_112_2 = 0) | all_112_0 = 0) % 23.12/3.95 | % 23.12/3.95 | ALPHA: (42) implies: % 23.12/3.95 | (43) member(all_54_9, all_32_3) = all_112_2 % 23.12/3.95 | (44) member(all_54_8, all_32_1) = all_112_1 % 23.12/3.95 | (45) apply(all_32_5, all_54_9, all_54_8) = all_112_0 % 23.12/3.95 | (46) ~ (all_112_1 = 0) | ~ (all_112_2 = 0) | all_112_0 = 0 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (1) with 0, all_112_2, all_32_3, all_54_9, % 23.12/3.95 | simplifying with (3), (43) gives: % 23.12/3.95 | (47) all_112_2 = 0 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (1) with all_110_2, all_112_2, all_32_3, all_54_9, % 23.12/3.95 | simplifying with (38), (43) gives: % 23.12/3.95 | (48) all_112_2 = all_110_2 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (1) with 0, all_112_1, all_32_1, all_54_8, % 23.12/3.95 | simplifying with (18), (44) gives: % 23.12/3.95 | (49) all_112_1 = 0 % 23.12/3.95 | % 23.12/3.95 | GROUND_INST: instantiating (1) with 0, all_110_1, all_32_1, all_54_7, % 23.12/3.95 | simplifying with (13), (39) gives: % 23.12/3.95 | (50) all_110_1 = 0 % 23.12/3.95 | % 23.12/3.95 | COMBINE_EQS: (47), (48) imply: % 23.12/3.95 | (51) all_110_2 = 0 % 23.12/3.95 | % 23.12/3.95 | SIMP: (51) implies: % 23.12/3.95 | (52) all_110_2 = 0 % 23.12/3.95 | % 23.12/3.95 | BETA: splitting (46) gives: % 23.12/3.95 | % 23.12/3.95 | Case 1: % 23.12/3.95 | | % 23.12/3.95 | | (53) ~ (all_112_1 = 0) % 23.12/3.95 | | % 23.12/3.95 | | REDUCE: (49), (53) imply: % 23.12/3.95 | | (54) $false % 23.12/3.95 | | % 23.12/3.95 | | CLOSE: (54) is inconsistent. % 23.12/3.95 | | % 23.12/3.95 | Case 2: % 23.12/3.95 | | % 23.12/3.95 | | (55) ~ (all_112_2 = 0) | all_112_0 = 0 % 23.12/3.95 | | % 23.12/3.95 | | BETA: splitting (55) gives: % 23.12/3.95 | | % 23.12/3.95 | | Case 1: % 23.12/3.95 | | | % 23.12/3.95 | | | (56) ~ (all_112_2 = 0) % 23.12/3.95 | | | % 23.12/3.95 | | | REDUCE: (47), (56) imply: % 23.12/3.95 | | | (57) $false % 23.12/3.95 | | | % 23.12/3.95 | | | CLOSE: (57) is inconsistent. % 23.12/3.95 | | | % 23.12/3.95 | | Case 2: % 23.12/3.95 | | | % 23.12/3.95 | | | (58) all_112_0 = 0 % 23.12/3.95 | | | % 23.12/3.95 | | | REDUCE: (45), (58) imply: % 23.12/3.95 | | | (59) apply(all_32_5, all_54_9, all_54_8) = 0 % 23.12/3.95 | | | % 23.12/3.95 | | | BETA: splitting (41) gives: % 23.12/3.95 | | | % 23.12/3.95 | | | Case 1: % 23.12/3.95 | | | | % 23.12/3.95 | | | | (60) ~ (all_110_1 = 0) % 23.12/3.95 | | | | % 23.12/3.95 | | | | REDUCE: (50), (60) imply: % 23.12/3.96 | | | | (61) $false % 23.12/3.96 | | | | % 23.12/3.96 | | | | CLOSE: (61) is inconsistent. % 23.12/3.96 | | | | % 23.12/3.96 | | | Case 2: % 23.12/3.96 | | | | % 23.12/3.96 | | | | (62) ~ (all_110_2 = 0) | all_110_0 = 0 % 23.12/3.96 | | | | % 23.12/3.96 | | | | BETA: splitting (62) gives: % 23.12/3.96 | | | | % 23.12/3.96 | | | | Case 1: % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | (63) ~ (all_110_2 = 0) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | REDUCE: (52), (63) imply: % 23.12/3.96 | | | | | (64) $false % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | CLOSE: (64) is inconsistent. % 23.12/3.96 | | | | | % 23.12/3.96 | | | | Case 2: % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | (65) all_110_0 = 0 % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | REDUCE: (40), (65) imply: % 23.12/3.96 | | | | | (66) apply(all_32_5, all_54_9, all_54_7) = 0 % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | GROUND_INST: instantiating (10) with all_32_5, all_32_3, all_32_2, % 23.12/3.96 | | | | | all_54_9, all_54_7, all_54_8, simplifying with (3), (4), % 23.12/3.96 | | | | | (5), (8), (15), (20), (22), (23), (26), (27) gives: % 23.12/3.96 | | | | | (67) all_54_7 = all_54_8 | ? [v0: any] : ? [v1: any] : % 23.12/3.96 | | | | | (apply(all_32_5, all_54_9, all_54_7) = v0 & apply(all_32_5, % 23.12/3.96 | | | | | all_54_9, all_54_8) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | GROUND_INST: instantiating (10) with all_32_5, all_32_3, all_32_2, % 23.12/3.96 | | | | | all_104_0, all_54_7, all_54_8, simplifying with (4), (5), % 23.12/3.96 | | | | | (8), (15), (20), (23), (26), (27), (31), (32) gives: % 23.12/3.96 | | | | | (68) all_54_7 = all_54_8 | ? [v0: any] : ? [v1: any] : % 23.12/3.96 | | | | | (apply(all_32_5, all_104_0, all_54_7) = v0 & apply(all_32_5, % 23.12/3.96 | | | | | all_104_0, all_54_8) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | GROUND_INST: instantiating (10) with all_32_5, all_32_3, all_32_2, % 23.12/3.96 | | | | | all_54_9, all_54_7, all_106_0, simplifying with (3), (4), % 23.12/3.96 | | | | | (5), (8), (20), (22), (23), (27), (34), (35) gives: % 23.12/3.96 | | | | | (69) all_106_0 = all_54_7 | ? [v0: any] : ? [v1: any] : % 23.12/3.96 | | | | | (apply(all_32_5, all_54_9, all_106_0) = v1 & apply(all_32_5, % 23.12/3.96 | | | | | all_54_9, all_54_7) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | GROUND_INST: instantiating (10) with all_32_5, all_32_3, all_32_2, % 23.12/3.96 | | | | | all_54_9, all_54_8, all_106_0, simplifying with (3), (4), % 23.12/3.96 | | | | | (8), (15), (20), (22), (23), (26), (34), (35) gives: % 23.12/3.96 | | | | | (70) all_106_0 = all_54_8 | ? [v0: any] : ? [v1: any] : % 23.12/3.96 | | | | | (apply(all_32_5, all_54_9, all_106_0) = v1 & apply(all_32_5, % 23.12/3.96 | | | | | all_54_9, all_54_8) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | GROUND_INST: instantiating (10) with all_32_5, all_32_3, all_32_2, % 23.12/3.96 | | | | | all_104_0, all_54_8, all_106_0, simplifying with (4), % 23.12/3.96 | | | | | (8), (15), (20), (23), (26), (31), (32), (34), (35) % 23.12/3.96 | | | | | gives: % 23.12/3.96 | | | | | (71) all_106_0 = all_54_8 | ? [v0: any] : ? [v1: any] : % 23.12/3.96 | | | | | (apply(all_32_5, all_104_0, all_106_0) = v1 & apply(all_32_5, % 23.12/3.96 | | | | | all_104_0, all_54_8) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | BETA: splitting (69) gives: % 23.12/3.96 | | | | | % 23.12/3.96 | | | | | Case 1: % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | (72) all_106_0 = all_54_7 % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | BETA: splitting (70) gives: % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | Case 1: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | (73) all_106_0 = all_54_8 % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | COMBINE_EQS: (72), (73) imply: % 23.12/3.96 | | | | | | | (74) all_54_7 = all_54_8 % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | REDUCE: (6), (74) imply: % 23.12/3.96 | | | | | | | (75) $false % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | CLOSE: (75) is inconsistent. % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | Case 2: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | (76) ~ (all_106_0 = all_54_8) % 23.12/3.96 | | | | | | | (77) ? [v0: any] : ? [v1: any] : (apply(all_32_5, all_54_9, % 23.12/3.96 | | | | | | | all_106_0) = v1 & apply(all_32_5, all_54_9, all_54_8) % 23.12/3.96 | | | | | | | = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | DELTA: instantiating (77) with fresh symbols all_175_0, all_175_1 % 23.12/3.96 | | | | | | | gives: % 23.12/3.96 | | | | | | | (78) apply(all_32_5, all_54_9, all_106_0) = all_175_0 & % 23.12/3.96 | | | | | | | apply(all_32_5, all_54_9, all_54_8) = all_175_1 & ( ~ % 23.12/3.96 | | | | | | | (all_175_0 = 0) | ~ (all_175_1 = 0)) % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | ALPHA: (78) implies: % 23.12/3.96 | | | | | | | (79) apply(all_32_5, all_54_9, all_54_8) = all_175_1 % 23.12/3.96 | | | | | | | (80) apply(all_32_5, all_54_9, all_106_0) = all_175_0 % 23.12/3.96 | | | | | | | (81) ~ (all_175_0 = 0) | ~ (all_175_1 = 0) % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | REDUCE: (72), (80) imply: % 23.12/3.96 | | | | | | | (82) apply(all_32_5, all_54_9, all_54_7) = all_175_0 % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | BETA: splitting (71) gives: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | Case 1: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | (83) all_106_0 = all_54_8 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | COMBINE_EQS: (72), (83) imply: % 23.12/3.96 | | | | | | | | (84) all_54_7 = all_54_8 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | REDUCE: (6), (84) imply: % 23.12/3.96 | | | | | | | | (85) $false % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | CLOSE: (85) is inconsistent. % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | Case 2: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | GROUND_INST: instantiating (14) with 0, all_175_1, all_54_8, % 23.12/3.96 | | | | | | | | all_54_9, all_32_5, simplifying with (59), (79) % 23.12/3.96 | | | | | | | | gives: % 23.12/3.96 | | | | | | | | (86) all_175_1 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | GROUND_INST: instantiating (14) with 0, all_175_0, all_54_7, % 23.12/3.96 | | | | | | | | all_54_9, all_32_5, simplifying with (66), (82) % 23.12/3.96 | | | | | | | | gives: % 23.12/3.96 | | | | | | | | (87) all_175_0 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | BETA: splitting (81) gives: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | Case 1: % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | (88) ~ (all_175_0 = 0) % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | REDUCE: (87), (88) imply: % 23.12/3.96 | | | | | | | | | (89) $false % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | CLOSE: (89) is inconsistent. % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | Case 2: % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | (90) ~ (all_175_1 = 0) % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | REDUCE: (86), (90) imply: % 23.12/3.96 | | | | | | | | | (91) $false % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | CLOSE: (91) is inconsistent. % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | End of split % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | End of split % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | End of split % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | Case 2: % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | (92) ? [v0: any] : ? [v1: any] : (apply(all_32_5, all_54_9, % 23.12/3.96 | | | | | | all_106_0) = v1 & apply(all_32_5, all_54_9, all_54_7) = % 23.12/3.96 | | | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | DELTA: instantiating (92) with fresh symbols all_154_0, all_154_1 % 23.12/3.96 | | | | | | gives: % 23.12/3.96 | | | | | | (93) apply(all_32_5, all_54_9, all_106_0) = all_154_0 & % 23.12/3.96 | | | | | | apply(all_32_5, all_54_9, all_54_7) = all_154_1 & ( ~ % 23.12/3.96 | | | | | | (all_154_0 = 0) | ~ (all_154_1 = 0)) % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | ALPHA: (93) implies: % 23.12/3.96 | | | | | | (94) apply(all_32_5, all_54_9, all_54_7) = all_154_1 % 23.12/3.96 | | | | | | (95) apply(all_32_5, all_54_9, all_106_0) = all_154_0 % 23.12/3.96 | | | | | | (96) ~ (all_154_0 = 0) | ~ (all_154_1 = 0) % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | BETA: splitting (67) gives: % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | | Case 1: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | (97) all_54_7 = all_54_8 % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | REDUCE: (6), (97) imply: % 23.12/3.96 | | | | | | | (98) $false % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | CLOSE: (98) is inconsistent. % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | Case 2: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | (99) ? [v0: any] : ? [v1: any] : (apply(all_32_5, all_54_9, % 23.12/3.96 | | | | | | | all_54_7) = v0 & apply(all_32_5, all_54_9, all_54_8) = % 23.12/3.96 | | | | | | | v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | DELTA: instantiating (99) with fresh symbols all_176_0, all_176_1 % 23.12/3.96 | | | | | | | gives: % 23.12/3.96 | | | | | | | (100) apply(all_32_5, all_54_9, all_54_7) = all_176_1 & % 23.12/3.96 | | | | | | | apply(all_32_5, all_54_9, all_54_8) = all_176_0 & ( ~ % 23.12/3.96 | | | | | | | (all_176_0 = 0) | ~ (all_176_1 = 0)) % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | ALPHA: (100) implies: % 23.12/3.96 | | | | | | | (101) apply(all_32_5, all_54_9, all_54_7) = all_176_1 % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | BETA: splitting (68) gives: % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | | Case 1: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | (102) all_54_7 = all_54_8 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | REDUCE: (6), (102) imply: % 23.12/3.96 | | | | | | | | (103) $false % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | CLOSE: (103) is inconsistent. % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | Case 2: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | GROUND_INST: instantiating (14) with 0, all_176_1, all_54_7, % 23.12/3.96 | | | | | | | | all_54_9, all_32_5, simplifying with (66), (101) % 23.12/3.96 | | | | | | | | gives: % 23.12/3.96 | | | | | | | | (104) all_176_1 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | GROUND_INST: instantiating (14) with all_154_1, all_176_1, % 23.12/3.96 | | | | | | | | all_54_7, all_54_9, all_32_5, simplifying with % 23.12/3.96 | | | | | | | | (94), (101) gives: % 23.12/3.96 | | | | | | | | (105) all_176_1 = all_154_1 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | GROUND_INST: instantiating (14) with 0, all_154_0, all_106_0, % 23.12/3.96 | | | | | | | | all_54_9, all_32_5, simplifying with (36), (95) % 23.12/3.96 | | | | | | | | gives: % 23.12/3.96 | | | | | | | | (106) all_154_0 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | COMBINE_EQS: (104), (105) imply: % 23.12/3.96 | | | | | | | | (107) all_154_1 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | SIMP: (107) implies: % 23.12/3.96 | | | | | | | | (108) all_154_1 = 0 % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | BETA: splitting (96) gives: % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | | Case 1: % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | (109) ~ (all_154_0 = 0) % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | REDUCE: (106), (109) imply: % 23.12/3.96 | | | | | | | | | (110) $false % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | CLOSE: (110) is inconsistent. % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | Case 2: % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | (111) ~ (all_154_1 = 0) % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | REDUCE: (108), (111) imply: % 23.12/3.96 | | | | | | | | | (112) $false % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | | CLOSE: (112) is inconsistent. % 23.12/3.96 | | | | | | | | | % 23.12/3.96 | | | | | | | | End of split % 23.12/3.96 | | | | | | | | % 23.12/3.96 | | | | | | | End of split % 23.12/3.96 | | | | | | | % 23.12/3.96 | | | | | | End of split % 23.12/3.96 | | | | | | % 23.12/3.96 | | | | | End of split % 23.12/3.96 | | | | | % 23.12/3.96 | | | | End of split % 23.12/3.96 | | | | % 23.12/3.96 | | | End of split % 23.12/3.96 | | | % 23.12/3.96 | | End of split % 23.12/3.96 | | % 23.12/3.96 | End of split % 23.12/3.96 | % 23.12/3.96 End of proof % 23.12/3.96 % SZS output end Proof for theBenchmark % 23.12/3.96 % 23.12/3.96 3363ms %------------------------------------------------------------------------------