%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SET708+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 : n024.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:05 EDT 2023 % Result : Theorem 11.87s 2.28s % Output : Proof 18.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SET708+4 : TPTP v8.1.2. Bugfixed v2.2.1. % 0.08/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n024.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sat Aug 26 11:26:54 EDT 2023 % 0.14/0.35 % CPUTime : % 0.20/0.63 ________ _____ % 0.20/0.63 ___ __ \_________(_)________________________________ % 0.20/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.63 % 0.20/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.63 (2023-06-19) % 0.20/0.63 % 0.20/0.63 (c) Philipp Rümmer, 2009-2023 % 0.20/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.63 Amanda Stjerna. % 0.20/0.63 Free software under BSD-3-Clause. % 0.20/0.63 % 0.20/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.63 % 0.20/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.64 Running up to 7 provers in parallel. % 0.20/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.74/1.19 Prover 1: Preprocessing ... % 3.74/1.19 Prover 4: Preprocessing ... % 3.74/1.23 Prover 0: Preprocessing ... % 3.74/1.23 Prover 3: Preprocessing ... % 3.74/1.23 Prover 5: Preprocessing ... % 3.74/1.24 Prover 6: Preprocessing ... % 3.74/1.24 Prover 2: Preprocessing ... % 9.11/1.90 Prover 5: Proving ... % 9.11/1.92 Prover 2: Proving ... % 9.11/1.93 Prover 6: Proving ... % 9.11/1.97 Prover 3: Constructing countermodel ... % 9.86/2.01 Prover 1: Constructing countermodel ... % 11.87/2.27 Prover 3: proved (1616ms) % 11.87/2.28 % 11.87/2.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.87/2.28 % 11.87/2.28 Prover 6: stopped % 11.87/2.28 Prover 2: stopped % 11.87/2.28 Prover 5: stopped % 11.87/2.28 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.87/2.28 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.87/2.28 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 11.87/2.29 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.36/2.35 Prover 7: Preprocessing ... % 12.36/2.36 Prover 11: Preprocessing ... % 12.36/2.36 Prover 8: Preprocessing ... % 12.36/2.37 Prover 10: Preprocessing ... % 13.59/2.51 Prover 10: Warning: ignoring some quantifiers % 13.59/2.52 Prover 7: Warning: ignoring some quantifiers % 13.59/2.54 Prover 10: Constructing countermodel ... % 14.15/2.57 Prover 7: Constructing countermodel ... % 14.15/2.60 Prover 4: Constructing countermodel ... % 14.69/2.65 Prover 8: Warning: ignoring some quantifiers % 14.69/2.68 Prover 8: Constructing countermodel ... % 14.69/2.71 Prover 10: gave up % 14.69/2.71 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.69/2.73 Prover 0: Proving ... % 14.69/2.73 Prover 0: stopped % 14.69/2.73 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.69/2.77 Prover 16: Preprocessing ... % 14.69/2.77 Prover 13: Preprocessing ... % 15.96/2.88 Prover 1: Found proof (size 131) % 15.96/2.88 Prover 1: proved (2229ms) % 15.96/2.88 Prover 4: stopped % 15.96/2.88 Prover 8: stopped % 16.58/2.88 Prover 7: stopped % 16.58/2.89 Prover 16: Warning: ignoring some quantifiers % 16.58/2.90 Prover 16: Constructing countermodel ... % 16.58/2.90 Prover 13: Warning: ignoring some quantifiers % 16.58/2.91 Prover 16: stopped % 16.58/2.92 Prover 13: Constructing countermodel ... % 16.58/2.93 Prover 13: stopped % 17.23/3.03 Prover 11: Constructing countermodel ... % 17.37/3.05 Prover 11: stopped % 17.37/3.05 % 17.37/3.05 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.37/3.05 % 17.37/3.06 % SZS output start Proof for theBenchmark % 17.37/3.06 Assumptions after simplification: % 17.37/3.06 --------------------------------- % 17.37/3.06 % 17.37/3.06 (compose_predicate) % 17.37/3.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 17.37/3.10 $i] : ! [v6: int] : (v6 = 0 | ~ (compose_predicate(v0, v1, v2, v3, v4, v5) % 17.37/3.10 = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 17.37/3.10 $i(v0) | ? [v7: $i] : ? [v8: $i] : ? [v9: any] : (apply(v0, v7, v8) = v9 % 17.37/3.10 & member(v8, v5) = 0 & member(v7, v3) = 0 & $i(v8) & $i(v7) & ( ~ (v9 = 0) % 17.37/3.10 | ! [v10: $i] : ( ~ (apply(v1, v10, v8) = 0) | ~ $i(v10) | ? [v11: % 17.37/3.10 any] : ? [v12: any] : (apply(v2, v7, v10) = v12 & member(v10, v4) = % 17.37/3.10 v11 & ( ~ (v12 = 0) | ~ (v11 = 0))))) & (v9 = 0 | ? [v10: $i] : % 17.37/3.10 (apply(v2, v7, v10) = 0 & apply(v1, v10, v8) = 0 & member(v10, v4) = 0 & % 17.37/3.10 $i(v10))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 17.37/3.10 ! [v4: $i] : ! [v5: $i] : ( ~ (compose_predicate(v0, v1, v2, v3, v4, v5) = 0) % 17.37/3.10 | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ! % 17.37/3.10 [v6: $i] : ! [v7: $i] : ! [v8: any] : ( ~ (apply(v0, v6, v7) = v8) | ~ % 17.37/3.10 $i(v7) | ~ $i(v6) | ? [v9: any] : ? [v10: any] : (member(v7, v5) = v10 % 17.37/3.10 & member(v6, v3) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0))) | (( ~ (v8 = 0) | % 17.37/3.10 ? [v9: $i] : (apply(v2, v6, v9) = 0 & apply(v1, v9, v7) = 0 & % 17.37/3.10 member(v9, v4) = 0 & $i(v9))) & (v8 = 0 | ! [v9: $i] : ( ~ % 17.37/3.10 (apply(v1, v9, v7) = 0) | ~ $i(v9) | ? [v10: any] : ? [v11: any] % 17.37/3.10 : (apply(v2, v6, v9) = v11 & member(v9, v4) = v10 & ( ~ (v11 = 0) | % 17.37/3.10 ~ (v10 = 0)))))))) % 17.37/3.10 % 17.37/3.10 (equal_maps) % 17.37/3.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 17.37/3.10 | ~ (equal_maps(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 17.37/3.10 ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ( ~ (v7 = v6) & % 17.37/3.10 apply(v1, v5, v7) = 0 & apply(v0, v5, v6) = 0 & member(v7, v3) = 0 & % 17.37/3.10 member(v6, v3) = 0 & member(v5, v2) = 0 & $i(v7) & $i(v6) & $i(v5))) & ! % 17.37/3.10 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (equal_maps(v0, v1, % 17.37/3.10 v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ! [v4: % 17.37/3.10 $i] : ! [v5: $i] : ! [v6: $i] : (v6 = v5 | ~ (apply(v1, v4, v6) = 0) | % 17.37/3.10 ~ (apply(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ? [v7: % 17.37/3.10 any] : ? [v8: any] : ? [v9: any] : (member(v6, v3) = v9 & member(v5, % 17.37/3.10 v3) = v8 & member(v4, v2) = v7 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = % 17.37/3.10 0))))) % 17.37/3.10 % 17.37/3.10 (maps) % 17.37/3.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 17.37/3.10 (maps(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : % 17.37/3.10 ? [v5: $i] : ? [v6: $i] : ( ~ (v6 = v5) & apply(v0, v4, v6) = 0 & apply(v0, % 17.37/3.10 v4, v5) = 0 & member(v6, v2) = 0 & member(v5, v2) = 0 & member(v4, v1) = % 17.37/3.10 0 & $i(v6) & $i(v5) & $i(v4)) | ? [v4: $i] : (member(v4, v1) = 0 & $i(v4) % 17.37/3.10 & ! [v5: $i] : ( ~ (apply(v0, v4, v5) = 0) | ~ $i(v5) | ? [v6: int] : ( % 17.37/3.10 ~ (v6 = 0) & member(v5, v2) = v6)))) & ! [v0: $i] : ! [v1: $i] : ! % 17.37/3.10 [v2: $i] : ( ~ (maps(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ( % 17.37/3.10 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ (apply(v0, v3, v5) % 17.37/3.10 = 0) | ~ (apply(v0, v3, v4) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) % 17.37/3.10 | ? [v6: any] : ? [v7: any] : ? [v8: any] : (member(v5, v2) = v8 & % 17.37/3.10 member(v4, v2) = v7 & member(v3, v1) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) % 17.37/3.10 | ~ (v6 = 0)))) & ! [v3: $i] : ( ~ (member(v3, v1) = 0) | ~ % 17.37/3.10 $i(v3) | ? [v4: $i] : (apply(v0, v3, v4) = 0 & member(v4, v2) = 0 & % 17.37/3.10 $i(v4))))) % 17.37/3.10 % 17.37/3.10 (thII01a) % 17.37/3.11 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 17.37/3.11 $i] : ? [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & equal_maps(v2, v3, v4, v6) % 17.37/3.11 = v7 & compose_predicate(v3, v1, v0, v4, v5, v6) = 0 & compose_predicate(v2, % 17.37/3.11 v1, v0, v4, v5, v6) = 0 & maps(v1, v5, v6) = 0 & maps(v0, v4, v5) = 0 & % 17.37/3.11 $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 17.37/3.11 % 17.37/3.11 (function-axioms) % 17.37/3.12 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 17.37/3.12 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | % 17.37/3.12 ~ (compose_predicate(v7, v6, v5, v4, v3, v2) = v1) | ~ % 17.37/3.12 (compose_predicate(v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: % 17.37/3.12 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.37/3.12 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (isomorphism(v6, v5, % 17.37/3.12 v4, v3, v2) = v1) | ~ (isomorphism(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 17.37/3.12 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.37/3.12 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (decreasing(v6, v5, % 17.37/3.12 v4, v3, v2) = v1) | ~ (decreasing(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 17.37/3.12 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.37/3.12 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (increasing(v6, v5, % 17.37/3.12 v4, v3, v2) = v1) | ~ (increasing(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 17.37/3.12 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 17.37/3.12 ! [v6: $i] : (v1 = v0 | ~ (compose_function(v6, v5, v4, v3, v2) = v1) | ~ % 17.37/3.12 (compose_function(v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 17.37/3.12 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 17.37/3.12 $i] : (v1 = v0 | ~ (inverse_predicate(v5, v4, v3, v2) = v1) | ~ % 17.37/3.12 (inverse_predicate(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 17.37/3.12 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 17.37/3.12 $i] : (v1 = v0 | ~ (equal_maps(v5, v4, v3, v2) = v1) | ~ (equal_maps(v5, % 17.37/3.12 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 17.37/3.12 $i] : ! [v4: $i] : (v1 = v0 | ~ (inverse_image3(v4, v3, v2) = v1) | ~ % 17.37/3.12 (inverse_image3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 17.37/3.12 : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (image3(v4, v3, v2) = v1) | ~ % 17.37/3.12 (image3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 17.37/3.12 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (inverse_function(v4, v3, v2) = v1) | % 17.37/3.12 ~ (inverse_function(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 17.37/3.12 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 17.37/3.12 ~ (one_to_one(v4, v3, v2) = v1) | ~ (one_to_one(v4, v3, v2) = v0)) & ! % 17.37/3.12 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 17.37/3.12 $i] : ! [v4: $i] : (v1 = v0 | ~ (surjective(v4, v3, v2) = v1) | ~ % 17.37/3.12 (surjective(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.37/3.12 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 17.37/3.12 (injective(v4, v3, v2) = v1) | ~ (injective(v4, v3, v2) = v0)) & ! [v0: % 17.37/3.12 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 17.37/3.12 : ! [v4: $i] : (v1 = v0 | ~ (maps(v4, v3, v2) = v1) | ~ (maps(v4, v3, v2) = % 17.37/3.12 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.37/3.12 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (apply(v4, v3, v2) = v1) | % 17.37/3.12 ~ (apply(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 17.37/3.12 [v3: $i] : (v1 = v0 | ~ (inverse_image2(v3, v2) = v1) | ~ % 17.37/3.12 (inverse_image2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 17.37/3.12 ! [v3: $i] : (v1 = v0 | ~ (image2(v3, v2) = v1) | ~ (image2(v3, v2) = v0)) & % 17.37/3.12 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 17.37/3.12 [v3: $i] : (v1 = v0 | ~ (identity(v3, v2) = v1) | ~ (identity(v3, v2) = v0)) % 17.37/3.12 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.37/3.12 (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0: % 17.37/3.12 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.37/3.12 (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0: $i] : ! % 17.37/3.12 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (union(v3, v2) = v1) | ~ % 17.37/3.12 (union(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 17.37/3.12 $i] : (v1 = v0 | ~ (intersection(v3, v2) = v1) | ~ (intersection(v3, v2) = % 17.37/3.12 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 17.37/3.12 $i] : ! [v3: $i] : (v1 = v0 | ~ (equal_set(v3, v2) = v1) | ~ % 17.37/3.12 (equal_set(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.37/3.12 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (subset(v3, % 17.37/3.12 v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 17.37/3.12 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 17.37/3.12 (member(v3, v2) = v1) | ~ (member(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 17.37/3.12 $i] : ! [v2: $i] : (v1 = v0 | ~ (product(v2) = v1) | ~ (product(v2) = % 17.37/3.12 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (sum(v2) = % 17.37/3.12 v1) | ~ (sum(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 17.37/3.12 v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0: $i] : ! % 17.37/3.12 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (power_set(v2) = v1) | ~ % 17.37/3.12 (power_set(v2) = v0)) % 17.37/3.12 % 17.37/3.12 Further assumptions not needed in the proof: % 17.37/3.12 -------------------------------------------- % 17.37/3.12 compose_function, decreasing_function, difference, empty_set, equal_set, % 17.37/3.12 identity, image2, image3, increasing_function, injective, intersection, % 17.37/3.12 inverse_function, inverse_image2, inverse_image3, inverse_predicate, % 17.37/3.12 isomorphism, one_to_one, power_set, product, singleton, subset, sum, surjective, % 17.37/3.12 union, unordered_pair % 17.37/3.12 % 17.37/3.12 Those formulas are unsatisfiable: % 17.37/3.12 --------------------------------- % 17.37/3.12 % 17.37/3.12 Begin of proof % 17.37/3.12 | % 17.37/3.12 | ALPHA: (maps) implies: % 17.37/3.12 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (maps(v0, v1, v2) = 0) | % 17.37/3.12 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ( ! [v3: $i] : ! [v4: $i] : ! % 17.37/3.12 | [v5: $i] : (v5 = v4 | ~ (apply(v0, v3, v5) = 0) | ~ (apply(v0, % 17.37/3.12 | v3, v4) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ? [v6: % 17.37/3.12 | any] : ? [v7: any] : ? [v8: any] : (member(v5, v2) = v8 & % 17.37/3.12 | member(v4, v2) = v7 & member(v3, v1) = v6 & ( ~ (v8 = 0) | ~ % 17.37/3.12 | (v7 = 0) | ~ (v6 = 0)))) & ! [v3: $i] : ( ~ (member(v3, v1) % 17.37/3.12 | = 0) | ~ $i(v3) | ? [v4: $i] : (apply(v0, v3, v4) = 0 & % 17.37/3.12 | member(v4, v2) = 0 & $i(v4))))) % 17.37/3.12 | % 17.37/3.12 | ALPHA: (compose_predicate) implies: % 17.37/3.12 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 17.37/3.12 | ! [v5: $i] : ( ~ (compose_predicate(v0, v1, v2, v3, v4, v5) = 0) | ~ % 17.37/3.12 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 17.37/3.12 | ! [v6: $i] : ! [v7: $i] : ! [v8: any] : ( ~ (apply(v0, v6, v7) = % 17.37/3.12 | v8) | ~ $i(v7) | ~ $i(v6) | ? [v9: any] : ? [v10: any] : % 17.37/3.12 | (member(v7, v5) = v10 & member(v6, v3) = v9 & ( ~ (v10 = 0) | ~ % 17.37/3.12 | (v9 = 0))) | (( ~ (v8 = 0) | ? [v9: $i] : (apply(v2, v6, v9) = % 17.37/3.12 | 0 & apply(v1, v9, v7) = 0 & member(v9, v4) = 0 & $i(v9))) & % 17.37/3.12 | (v8 = 0 | ! [v9: $i] : ( ~ (apply(v1, v9, v7) = 0) | ~ $i(v9) | % 17.37/3.12 | ? [v10: any] : ? [v11: any] : (apply(v2, v6, v9) = v11 & % 17.37/3.12 | member(v9, v4) = v10 & ( ~ (v11 = 0) | ~ (v10 = 0)))))))) % 17.37/3.12 | % 17.37/3.12 | ALPHA: (equal_maps) implies: % 17.37/3.12 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 17.37/3.12 | (v4 = 0 | ~ (equal_maps(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) % 17.37/3.12 | | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ( % 17.37/3.12 | ~ (v7 = v6) & apply(v1, v5, v7) = 0 & apply(v0, v5, v6) = 0 & % 17.37/3.12 | member(v7, v3) = 0 & member(v6, v3) = 0 & member(v5, v2) = 0 & % 17.37/3.12 | $i(v7) & $i(v6) & $i(v5))) % 17.37/3.12 | % 17.37/3.12 | ALPHA: (function-axioms) implies: % 17.37/3.12 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 17.37/3.12 | ! [v3: $i] : (v1 = v0 | ~ (member(v3, v2) = v1) | ~ (member(v3, v2) % 17.37/3.12 | = v0)) % 17.37/3.13 | % 17.37/3.13 | DELTA: instantiating (thII01a) with fresh symbols all_32_0, all_32_1, % 17.37/3.13 | all_32_2, all_32_3, all_32_4, all_32_5, all_32_6, all_32_7 gives: % 17.37/3.13 | (5) ~ (all_32_0 = 0) & equal_maps(all_32_5, all_32_4, all_32_3, all_32_1) % 17.37/3.13 | = all_32_0 & compose_predicate(all_32_4, all_32_6, all_32_7, all_32_3, % 17.37/3.13 | all_32_2, all_32_1) = 0 & compose_predicate(all_32_5, all_32_6, % 17.37/3.13 | all_32_7, all_32_3, all_32_2, all_32_1) = 0 & maps(all_32_6, % 17.37/3.13 | all_32_2, all_32_1) = 0 & maps(all_32_7, all_32_3, all_32_2) = 0 & % 17.37/3.13 | $i(all_32_1) & $i(all_32_2) & $i(all_32_3) & $i(all_32_4) & % 17.37/3.13 | $i(all_32_5) & $i(all_32_6) & $i(all_32_7) % 17.37/3.13 | % 17.37/3.13 | ALPHA: (5) implies: % 17.37/3.13 | (6) ~ (all_32_0 = 0) % 17.37/3.13 | (7) $i(all_32_7) % 17.37/3.13 | (8) $i(all_32_6) % 17.79/3.13 | (9) $i(all_32_5) % 17.79/3.13 | (10) $i(all_32_4) % 17.79/3.13 | (11) $i(all_32_3) % 17.79/3.13 | (12) $i(all_32_2) % 17.79/3.13 | (13) $i(all_32_1) % 17.79/3.13 | (14) maps(all_32_7, all_32_3, all_32_2) = 0 % 17.79/3.13 | (15) maps(all_32_6, all_32_2, all_32_1) = 0 % 17.79/3.13 | (16) compose_predicate(all_32_5, all_32_6, all_32_7, all_32_3, all_32_2, % 17.79/3.13 | all_32_1) = 0 % 17.79/3.13 | (17) compose_predicate(all_32_4, all_32_6, all_32_7, all_32_3, all_32_2, % 17.79/3.13 | all_32_1) = 0 % 17.79/3.13 | (18) equal_maps(all_32_5, all_32_4, all_32_3, all_32_1) = all_32_0 % 17.79/3.13 | % 17.79/3.13 | GROUND_INST: instantiating (1) with all_32_7, all_32_3, all_32_2, simplifying % 17.79/3.13 | with (7), (11), (12), (14) gives: % 17.79/3.13 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 17.79/3.13 | (apply(all_32_7, v0, v2) = 0) | ~ (apply(all_32_7, v0, v1) = 0) | % 17.79/3.13 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 17.79/3.13 | [v5: any] : (member(v2, all_32_2) = v5 & member(v1, all_32_2) = v4 & % 17.79/3.13 | member(v0, all_32_3) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 17.79/3.13 | 0)))) & ! [v0: $i] : ( ~ (member(v0, all_32_3) = 0) | ~ % 17.79/3.13 | $i(v0) | ? [v1: $i] : (apply(all_32_7, v0, v1) = 0 & member(v1, % 17.79/3.13 | all_32_2) = 0 & $i(v1))) % 17.79/3.13 | % 17.79/3.13 | ALPHA: (19) implies: % 17.79/3.13 | (20) ! [v0: $i] : ( ~ (member(v0, all_32_3) = 0) | ~ $i(v0) | ? [v1: $i] % 17.79/3.13 | : (apply(all_32_7, v0, v1) = 0 & member(v1, all_32_2) = 0 & $i(v1))) % 17.79/3.13 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 17.79/3.13 | (apply(all_32_7, v0, v2) = 0) | ~ (apply(all_32_7, v0, v1) = 0) | % 17.79/3.13 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 17.79/3.13 | [v5: any] : (member(v2, all_32_2) = v5 & member(v1, all_32_2) = v4 & % 17.79/3.13 | member(v0, all_32_3) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 17.79/3.13 | 0)))) % 17.79/3.13 | % 17.79/3.13 | GROUND_INST: instantiating (1) with all_32_6, all_32_2, all_32_1, simplifying % 17.79/3.13 | with (8), (12), (13), (15) gives: % 17.79/3.14 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 17.79/3.14 | (apply(all_32_6, v0, v2) = 0) | ~ (apply(all_32_6, v0, v1) = 0) | % 17.79/3.14 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 17.79/3.14 | [v5: any] : (member(v2, all_32_1) = v5 & member(v1, all_32_1) = v4 & % 17.79/3.14 | member(v0, all_32_2) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 17.79/3.14 | 0)))) & ! [v0: $i] : ( ~ (member(v0, all_32_2) = 0) | ~ % 17.79/3.14 | $i(v0) | ? [v1: $i] : (apply(all_32_6, v0, v1) = 0 & member(v1, % 17.79/3.14 | all_32_1) = 0 & $i(v1))) % 17.79/3.14 | % 17.79/3.14 | ALPHA: (22) implies: % 17.79/3.14 | (23) ! [v0: $i] : ( ~ (member(v0, all_32_2) = 0) | ~ $i(v0) | ? [v1: $i] % 17.79/3.14 | : (apply(all_32_6, v0, v1) = 0 & member(v1, all_32_1) = 0 & $i(v1))) % 17.79/3.14 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ % 17.79/3.14 | (apply(all_32_6, v0, v2) = 0) | ~ (apply(all_32_6, v0, v1) = 0) | % 17.79/3.14 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 17.79/3.14 | [v5: any] : (member(v2, all_32_1) = v5 & member(v1, all_32_1) = v4 & % 17.79/3.14 | member(v0, all_32_2) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = % 17.79/3.14 | 0)))) % 17.79/3.14 | % 17.79/3.14 | GROUND_INST: instantiating (2) with all_32_5, all_32_6, all_32_7, all_32_3, % 17.79/3.14 | all_32_2, all_32_1, simplifying with (7), (8), (9), (11), (12), % 17.79/3.14 | (13), (16) gives: % 17.79/3.14 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_32_5, v0, % 17.79/3.14 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 17.79/3.14 | : (member(v1, all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 = % 17.79/3.14 | 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) | ? [v3: $i] : % 17.79/3.14 | (apply(all_32_6, v3, v1) = 0 & apply(all_32_7, v0, v3) = 0 & % 17.79/3.14 | member(v3, all_32_2) = 0 & $i(v3))) & (v2 = 0 | ! [v3: $i] : % 17.79/3.14 | ( ~ (apply(all_32_6, v3, v1) = 0) | ~ $i(v3) | ? [v4: any] : % 17.79/3.14 | ? [v5: any] : (apply(all_32_7, v0, v3) = v5 & member(v3, % 17.79/3.14 | all_32_2) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))))) % 17.79/3.14 | % 17.79/3.14 | GROUND_INST: instantiating (2) with all_32_4, all_32_6, all_32_7, all_32_3, % 17.79/3.14 | all_32_2, all_32_1, simplifying with (7), (8), (10), (11), (12), % 17.79/3.14 | (13), (17) gives: % 17.79/3.14 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (apply(all_32_4, v0, % 17.79/3.14 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] % 17.79/3.14 | : (member(v1, all_32_1) = v4 & member(v0, all_32_3) = v3 & ( ~ (v4 = % 17.79/3.14 | 0) | ~ (v3 = 0))) | (( ~ (v2 = 0) | ? [v3: $i] : % 17.79/3.14 | (apply(all_32_6, v3, v1) = 0 & apply(all_32_7, v0, v3) = 0 & % 17.79/3.14 | member(v3, all_32_2) = 0 & $i(v3))) & (v2 = 0 | ! [v3: $i] : % 17.79/3.14 | ( ~ (apply(all_32_6, v3, v1) = 0) | ~ $i(v3) | ? [v4: any] : % 17.79/3.14 | ? [v5: any] : (apply(all_32_7, v0, v3) = v5 & member(v3, % 17.79/3.14 | all_32_2) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0))))))) % 17.79/3.14 | % 17.79/3.14 | GROUND_INST: instantiating (3) with all_32_5, all_32_4, all_32_3, all_32_1, % 17.79/3.14 | all_32_0, simplifying with (9), (10), (11), (13), (18) gives: % 17.79/3.14 | (27) all_32_0 = 0 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = v1) % 17.79/3.14 | & apply(all_32_4, v0, v2) = 0 & apply(all_32_5, v0, v1) = 0 & % 17.79/3.14 | member(v2, all_32_1) = 0 & member(v1, all_32_1) = 0 & member(v0, % 17.79/3.14 | all_32_3) = 0 & $i(v2) & $i(v1) & $i(v0)) % 17.79/3.14 | % 17.79/3.14 | BETA: splitting (27) gives: % 17.79/3.14 | % 17.79/3.14 | Case 1: % 17.79/3.14 | | % 17.79/3.14 | | (28) all_32_0 = 0 % 17.79/3.14 | | % 17.79/3.14 | | REDUCE: (6), (28) imply: % 17.79/3.14 | | (29) $false % 17.79/3.15 | | % 17.79/3.15 | | CLOSE: (29) is inconsistent. % 17.79/3.15 | | % 17.79/3.15 | Case 2: % 17.79/3.15 | | % 17.79/3.15 | | (30) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = v1) & % 17.79/3.15 | | apply(all_32_4, v0, v2) = 0 & apply(all_32_5, v0, v1) = 0 & % 17.79/3.15 | | member(v2, all_32_1) = 0 & member(v1, all_32_1) = 0 & member(v0, % 17.79/3.15 | | all_32_3) = 0 & $i(v2) & $i(v1) & $i(v0)) % 17.79/3.15 | | % 17.79/3.15 | | DELTA: instantiating (30) with fresh symbols all_46_0, all_46_1, all_46_2 % 17.79/3.15 | | gives: % 17.79/3.15 | | (31) ~ (all_46_0 = all_46_1) & apply(all_32_4, all_46_2, all_46_0) = 0 & % 17.79/3.15 | | apply(all_32_5, all_46_2, all_46_1) = 0 & member(all_46_0, all_32_1) % 17.79/3.15 | | = 0 & member(all_46_1, all_32_1) = 0 & member(all_46_2, all_32_3) = % 17.79/3.15 | | 0 & $i(all_46_0) & $i(all_46_1) & $i(all_46_2) % 17.79/3.15 | | % 17.79/3.15 | | ALPHA: (31) implies: % 17.79/3.15 | | (32) ~ (all_46_0 = all_46_1) % 17.79/3.15 | | (33) $i(all_46_2) % 17.79/3.15 | | (34) $i(all_46_1) % 17.79/3.15 | | (35) $i(all_46_0) % 17.79/3.15 | | (36) member(all_46_2, all_32_3) = 0 % 17.79/3.15 | | (37) member(all_46_1, all_32_1) = 0 % 17.79/3.15 | | (38) member(all_46_0, all_32_1) = 0 % 17.79/3.15 | | (39) apply(all_32_5, all_46_2, all_46_1) = 0 % 17.79/3.15 | | (40) apply(all_32_4, all_46_2, all_46_0) = 0 % 17.79/3.15 | | % 17.79/3.15 | | GROUND_INST: instantiating (20) with all_46_2, simplifying with (33), (36) % 17.79/3.15 | | gives: % 17.79/3.15 | | (41) ? [v0: $i] : (apply(all_32_7, all_46_2, v0) = 0 & member(v0, % 17.79/3.15 | | all_32_2) = 0 & $i(v0)) % 17.79/3.15 | | % 17.79/3.15 | | GROUND_INST: instantiating (25) with all_46_2, all_46_1, 0, simplifying with % 17.79/3.15 | | (33), (34), (39) gives: % 17.79/3.15 | | (42) ? [v0: any] : ? [v1: any] : (member(all_46_1, all_32_1) = v1 & % 17.79/3.15 | | member(all_46_2, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | % 17.79/3.15 | | ? [v0: $i] : (apply(all_32_6, v0, all_46_1) = 0 & apply(all_32_7, % 17.79/3.15 | | all_46_2, v0) = 0 & member(v0, all_32_2) = 0 & $i(v0)) % 17.79/3.15 | | % 17.79/3.15 | | GROUND_INST: instantiating (26) with all_46_2, all_46_0, 0, simplifying with % 17.79/3.15 | | (33), (35), (40) gives: % 17.79/3.15 | | (43) ? [v0: any] : ? [v1: any] : (member(all_46_0, all_32_1) = v1 & % 17.79/3.15 | | member(all_46_2, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) | % 17.79/3.15 | | ? [v0: $i] : (apply(all_32_6, v0, all_46_0) = 0 & apply(all_32_7, % 17.79/3.15 | | all_46_2, v0) = 0 & member(v0, all_32_2) = 0 & $i(v0)) % 17.79/3.15 | | % 17.79/3.15 | | DELTA: instantiating (41) with fresh symbol all_53_0 gives: % 17.79/3.15 | | (44) apply(all_32_7, all_46_2, all_53_0) = 0 & member(all_53_0, all_32_2) % 17.79/3.15 | | = 0 & $i(all_53_0) % 17.79/3.15 | | % 17.79/3.15 | | ALPHA: (44) implies: % 17.79/3.15 | | (45) $i(all_53_0) % 17.79/3.15 | | (46) member(all_53_0, all_32_2) = 0 % 17.79/3.15 | | (47) apply(all_32_7, all_46_2, all_53_0) = 0 % 17.79/3.15 | | % 17.79/3.15 | | BETA: splitting (43) gives: % 17.79/3.15 | | % 17.79/3.15 | | Case 1: % 17.79/3.15 | | | % 17.79/3.15 | | | (48) ? [v0: any] : ? [v1: any] : (member(all_46_0, all_32_1) = v1 & % 17.79/3.15 | | | member(all_46_2, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.15 | | | % 17.79/3.15 | | | DELTA: instantiating (48) with fresh symbols all_58_0, all_58_1 gives: % 17.79/3.15 | | | (49) member(all_46_0, all_32_1) = all_58_0 & member(all_46_2, all_32_3) % 17.79/3.15 | | | = all_58_1 & ( ~ (all_58_0 = 0) | ~ (all_58_1 = 0)) % 17.79/3.15 | | | % 17.79/3.15 | | | ALPHA: (49) implies: % 17.79/3.15 | | | (50) member(all_46_2, all_32_3) = all_58_1 % 17.79/3.15 | | | (51) member(all_46_0, all_32_1) = all_58_0 % 17.79/3.15 | | | (52) ~ (all_58_0 = 0) | ~ (all_58_1 = 0) % 17.79/3.15 | | | % 17.79/3.16 | | | GROUND_INST: instantiating (4) with 0, all_58_1, all_32_3, all_46_2, % 17.79/3.16 | | | simplifying with (36), (50) gives: % 17.79/3.16 | | | (53) all_58_1 = 0 % 17.79/3.16 | | | % 17.79/3.16 | | | GROUND_INST: instantiating (4) with 0, all_58_0, all_32_1, all_46_0, % 17.79/3.16 | | | simplifying with (38), (51) gives: % 17.79/3.16 | | | (54) all_58_0 = 0 % 17.79/3.16 | | | % 17.79/3.16 | | | BETA: splitting (52) gives: % 17.79/3.16 | | | % 17.79/3.16 | | | Case 1: % 17.79/3.16 | | | | % 17.79/3.16 | | | | (55) ~ (all_58_0 = 0) % 17.79/3.16 | | | | % 17.79/3.16 | | | | REDUCE: (54), (55) imply: % 17.79/3.16 | | | | (56) $false % 17.79/3.16 | | | | % 17.79/3.16 | | | | CLOSE: (56) is inconsistent. % 17.79/3.16 | | | | % 17.79/3.16 | | | Case 2: % 17.79/3.16 | | | | % 17.79/3.16 | | | | (57) ~ (all_58_1 = 0) % 17.79/3.16 | | | | % 17.79/3.16 | | | | REDUCE: (53), (57) imply: % 17.79/3.16 | | | | (58) $false % 17.79/3.16 | | | | % 17.79/3.16 | | | | CLOSE: (58) is inconsistent. % 17.79/3.16 | | | | % 17.79/3.16 | | | End of split % 17.79/3.16 | | | % 17.79/3.16 | | Case 2: % 17.79/3.16 | | | % 17.79/3.16 | | | (59) ? [v0: $i] : (apply(all_32_6, v0, all_46_0) = 0 & apply(all_32_7, % 17.79/3.16 | | | all_46_2, v0) = 0 & member(v0, all_32_2) = 0 & $i(v0)) % 17.79/3.16 | | | % 17.79/3.16 | | | DELTA: instantiating (59) with fresh symbol all_58_0 gives: % 17.79/3.16 | | | (60) apply(all_32_6, all_58_0, all_46_0) = 0 & apply(all_32_7, % 17.79/3.16 | | | all_46_2, all_58_0) = 0 & member(all_58_0, all_32_2) = 0 & % 17.79/3.16 | | | $i(all_58_0) % 17.79/3.16 | | | % 17.79/3.16 | | | ALPHA: (60) implies: % 17.79/3.16 | | | (61) $i(all_58_0) % 17.79/3.16 | | | (62) member(all_58_0, all_32_2) = 0 % 17.79/3.16 | | | (63) apply(all_32_7, all_46_2, all_58_0) = 0 % 17.79/3.16 | | | (64) apply(all_32_6, all_58_0, all_46_0) = 0 % 17.79/3.16 | | | % 17.79/3.16 | | | BETA: splitting (42) gives: % 17.79/3.16 | | | % 17.79/3.16 | | | Case 1: % 17.79/3.16 | | | | % 17.79/3.16 | | | | (65) ? [v0: any] : ? [v1: any] : (member(all_46_1, all_32_1) = v1 & % 17.79/3.16 | | | | member(all_46_2, all_32_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.16 | | | | % 17.79/3.16 | | | | DELTA: instantiating (65) with fresh symbols all_62_0, all_62_1 gives: % 17.79/3.16 | | | | (66) member(all_46_1, all_32_1) = all_62_0 & member(all_46_2, % 17.79/3.16 | | | | all_32_3) = all_62_1 & ( ~ (all_62_0 = 0) | ~ (all_62_1 = 0)) % 17.79/3.16 | | | | % 17.79/3.16 | | | | ALPHA: (66) implies: % 17.79/3.16 | | | | (67) member(all_46_2, all_32_3) = all_62_1 % 17.79/3.16 | | | | (68) member(all_46_1, all_32_1) = all_62_0 % 17.79/3.16 | | | | (69) ~ (all_62_0 = 0) | ~ (all_62_1 = 0) % 17.79/3.16 | | | | % 17.79/3.16 | | | | GROUND_INST: instantiating (4) with 0, all_62_1, all_32_3, all_46_2, % 17.79/3.16 | | | | simplifying with (36), (67) gives: % 17.79/3.16 | | | | (70) all_62_1 = 0 % 17.79/3.16 | | | | % 17.79/3.16 | | | | GROUND_INST: instantiating (4) with 0, all_62_0, all_32_1, all_46_1, % 17.79/3.16 | | | | simplifying with (37), (68) gives: % 17.79/3.16 | | | | (71) all_62_0 = 0 % 17.79/3.16 | | | | % 17.79/3.16 | | | | BETA: splitting (69) gives: % 17.79/3.16 | | | | % 17.79/3.16 | | | | Case 1: % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | (72) ~ (all_62_0 = 0) % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | REDUCE: (71), (72) imply: % 17.79/3.16 | | | | | (73) $false % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | CLOSE: (73) is inconsistent. % 17.79/3.16 | | | | | % 17.79/3.16 | | | | Case 2: % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | (74) ~ (all_62_1 = 0) % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | REDUCE: (70), (74) imply: % 17.79/3.16 | | | | | (75) $false % 17.79/3.16 | | | | | % 17.79/3.16 | | | | | CLOSE: (75) is inconsistent. % 17.79/3.16 | | | | | % 17.79/3.16 | | | | End of split % 17.79/3.16 | | | | % 17.79/3.16 | | | Case 2: % 17.79/3.16 | | | | % 17.79/3.16 | | | | (76) ? [v0: $i] : (apply(all_32_6, v0, all_46_1) = 0 & % 17.79/3.16 | | | | apply(all_32_7, all_46_2, v0) = 0 & member(v0, all_32_2) = 0 & % 17.79/3.16 | | | | $i(v0)) % 17.79/3.16 | | | | % 17.79/3.16 | | | | DELTA: instantiating (76) with fresh symbol all_62_0 gives: % 17.79/3.16 | | | | (77) apply(all_32_6, all_62_0, all_46_1) = 0 & apply(all_32_7, % 17.79/3.16 | | | | all_46_2, all_62_0) = 0 & member(all_62_0, all_32_2) = 0 & % 17.79/3.16 | | | | $i(all_62_0) % 17.79/3.16 | | | | % 17.79/3.16 | | | | ALPHA: (77) implies: % 17.79/3.16 | | | | (78) $i(all_62_0) % 17.79/3.16 | | | | (79) member(all_62_0, all_32_2) = 0 % 17.79/3.16 | | | | (80) apply(all_32_7, all_46_2, all_62_0) = 0 % 17.79/3.16 | | | | (81) apply(all_32_6, all_62_0, all_46_1) = 0 % 17.79/3.16 | | | | % 17.79/3.16 | | | | GROUND_INST: instantiating (23) with all_58_0, simplifying with (61), % 17.79/3.16 | | | | (62) gives: % 17.79/3.16 | | | | (82) ? [v0: $i] : (apply(all_32_6, all_58_0, v0) = 0 & member(v0, % 17.79/3.16 | | | | all_32_1) = 0 & $i(v0)) % 17.79/3.16 | | | | % 17.79/3.16 | | | | GROUND_INST: instantiating (21) with all_46_2, all_58_0, all_62_0, % 17.79/3.16 | | | | simplifying with (33), (61), (63), (78), (80) gives: % 17.79/3.16 | | | | (83) all_62_0 = all_58_0 | ? [v0: any] : ? [v1: any] : ? [v2: any] % 17.79/3.16 | | | | : (member(all_62_0, all_32_2) = v2 & member(all_58_0, all_32_2) % 17.79/3.16 | | | | = v1 & member(all_46_2, all_32_3) = v0 & ( ~ (v2 = 0) | ~ (v1 % 17.79/3.16 | | | | = 0) | ~ (v0 = 0))) % 17.79/3.16 | | | | % 17.79/3.16 | | | | GROUND_INST: instantiating (21) with all_46_2, all_53_0, all_62_0, % 17.79/3.16 | | | | simplifying with (33), (45), (47), (78), (80) gives: % 17.79/3.16 | | | | (84) all_62_0 = all_53_0 | ? [v0: any] : ? [v1: any] : ? [v2: any] % 17.79/3.16 | | | | : (member(all_62_0, all_32_2) = v2 & member(all_53_0, all_32_2) % 17.79/3.16 | | | | = v1 & member(all_46_2, all_32_3) = v0 & ( ~ (v2 = 0) | ~ (v1 % 17.79/3.16 | | | | = 0) | ~ (v0 = 0))) % 17.79/3.17 | | | | % 17.79/3.17 | | | | DELTA: instantiating (82) with fresh symbol all_71_0 gives: % 17.79/3.17 | | | | (85) apply(all_32_6, all_58_0, all_71_0) = 0 & member(all_71_0, % 17.79/3.17 | | | | all_32_1) = 0 & $i(all_71_0) % 17.79/3.17 | | | | % 17.79/3.17 | | | | ALPHA: (85) implies: % 17.79/3.17 | | | | (86) $i(all_71_0) % 17.79/3.17 | | | | (87) member(all_71_0, all_32_1) = 0 % 17.79/3.17 | | | | (88) apply(all_32_6, all_58_0, all_71_0) = 0 % 17.79/3.17 | | | | % 17.79/3.17 | | | | BETA: splitting (84) gives: % 17.79/3.17 | | | | % 17.79/3.17 | | | | Case 1: % 17.79/3.17 | | | | | % 17.79/3.17 | | | | | (89) all_62_0 = all_53_0 % 17.79/3.17 | | | | | % 17.79/3.17 | | | | | REDUCE: (81), (89) imply: % 17.79/3.17 | | | | | (90) apply(all_32_6, all_53_0, all_46_1) = 0 % 17.79/3.17 | | | | | % 17.79/3.17 | | | | | BETA: splitting (83) gives: % 17.79/3.17 | | | | | % 17.79/3.17 | | | | | Case 1: % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | (91) all_62_0 = all_58_0 % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | COMBINE_EQS: (89), (91) imply: % 17.79/3.17 | | | | | | (92) all_58_0 = all_53_0 % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | SIMP: (92) implies: % 17.79/3.17 | | | | | | (93) all_58_0 = all_53_0 % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | REDUCE: (88), (93) imply: % 17.79/3.17 | | | | | | (94) apply(all_32_6, all_53_0, all_71_0) = 0 % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | REDUCE: (64), (93) imply: % 17.79/3.17 | | | | | | (95) apply(all_32_6, all_53_0, all_46_0) = 0 % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | GROUND_INST: instantiating (24) with all_53_0, all_71_0, all_46_0, % 17.79/3.17 | | | | | | simplifying with (35), (45), (86), (94), (95) gives: % 17.79/3.17 | | | | | | (96) all_71_0 = all_46_0 | ? [v0: any] : ? [v1: any] : ? [v2: % 17.79/3.17 | | | | | | any] : (member(all_71_0, all_32_1) = v1 & member(all_53_0, % 17.79/3.17 | | | | | | all_32_2) = v0 & member(all_46_0, all_32_1) = v2 & ( ~ % 17.79/3.17 | | | | | | (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | GROUND_INST: instantiating (24) with all_53_0, all_71_0, all_46_1, % 17.79/3.17 | | | | | | simplifying with (34), (45), (86), (90), (94) gives: % 17.79/3.17 | | | | | | (97) all_71_0 = all_46_1 | ? [v0: any] : ? [v1: any] : ? [v2: % 17.79/3.17 | | | | | | any] : (member(all_71_0, all_32_1) = v1 & member(all_53_0, % 17.79/3.17 | | | | | | all_32_2) = v0 & member(all_46_1, all_32_1) = v2 & ( ~ % 17.79/3.17 | | | | | | (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | BETA: splitting (97) gives: % 17.79/3.17 | | | | | | % 17.79/3.17 | | | | | | Case 1: % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | (98) all_71_0 = all_46_1 % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | BETA: splitting (96) gives: % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | Case 1: % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | (99) all_71_0 = all_46_0 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | COMBINE_EQS: (98), (99) imply: % 17.79/3.17 | | | | | | | | (100) all_46_0 = all_46_1 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | REDUCE: (32), (100) imply: % 17.79/3.17 | | | | | | | | (101) $false % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | CLOSE: (101) is inconsistent. % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | Case 2: % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | (102) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 17.79/3.17 | | | | | | | | (member(all_71_0, all_32_1) = v1 & member(all_53_0, % 17.79/3.17 | | | | | | | | all_32_2) = v0 & member(all_46_0, all_32_1) = v2 & % 17.79/3.17 | | | | | | | | ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | DELTA: instantiating (102) with fresh symbols all_102_0, % 17.79/3.17 | | | | | | | | all_102_1, all_102_2 gives: % 17.79/3.17 | | | | | | | | (103) member(all_71_0, all_32_1) = all_102_1 & % 17.79/3.17 | | | | | | | | member(all_53_0, all_32_2) = all_102_2 & % 17.79/3.17 | | | | | | | | member(all_46_0, all_32_1) = all_102_0 & ( ~ (all_102_0 % 17.79/3.17 | | | | | | | | = 0) | ~ (all_102_1 = 0) | ~ (all_102_2 = 0)) % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | ALPHA: (103) implies: % 17.79/3.17 | | | | | | | | (104) member(all_46_0, all_32_1) = all_102_0 % 17.79/3.17 | | | | | | | | (105) member(all_53_0, all_32_2) = all_102_2 % 17.79/3.17 | | | | | | | | (106) member(all_71_0, all_32_1) = all_102_1 % 17.79/3.17 | | | | | | | | (107) ~ (all_102_0 = 0) | ~ (all_102_1 = 0) | ~ (all_102_2 % 17.79/3.17 | | | | | | | | = 0) % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | REDUCE: (98), (106) imply: % 17.79/3.17 | | | | | | | | (108) member(all_46_1, all_32_1) = all_102_1 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | GROUND_INST: instantiating (4) with 0, all_102_1, all_32_1, % 17.79/3.17 | | | | | | | | all_46_1, simplifying with (37), (108) gives: % 17.79/3.17 | | | | | | | | (109) all_102_1 = 0 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | GROUND_INST: instantiating (4) with 0, all_102_0, all_32_1, % 17.79/3.17 | | | | | | | | all_46_0, simplifying with (38), (104) gives: % 17.79/3.17 | | | | | | | | (110) all_102_0 = 0 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | GROUND_INST: instantiating (4) with 0, all_102_2, all_32_2, % 17.79/3.17 | | | | | | | | all_53_0, simplifying with (46), (105) gives: % 17.79/3.17 | | | | | | | | (111) all_102_2 = 0 % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | BETA: splitting (107) gives: % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | | Case 1: % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | (112) ~ (all_102_0 = 0) % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | REDUCE: (110), (112) imply: % 17.79/3.17 | | | | | | | | | (113) $false % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | CLOSE: (113) is inconsistent. % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | Case 2: % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | (114) ~ (all_102_1 = 0) | ~ (all_102_2 = 0) % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | BETA: splitting (114) gives: % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | | Case 1: % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | (115) ~ (all_102_1 = 0) % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | REDUCE: (109), (115) imply: % 17.79/3.17 | | | | | | | | | | (116) $false % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | CLOSE: (116) is inconsistent. % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | Case 2: % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | (117) ~ (all_102_2 = 0) % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | REDUCE: (111), (117) imply: % 17.79/3.17 | | | | | | | | | | (118) $false % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | | CLOSE: (118) is inconsistent. % 17.79/3.17 | | | | | | | | | | % 17.79/3.17 | | | | | | | | | End of split % 17.79/3.17 | | | | | | | | | % 17.79/3.17 | | | | | | | | End of split % 17.79/3.17 | | | | | | | | % 17.79/3.17 | | | | | | | End of split % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | Case 2: % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | (119) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 17.79/3.17 | | | | | | | (member(all_71_0, all_32_1) = v1 & member(all_53_0, % 17.79/3.17 | | | | | | | all_32_2) = v0 & member(all_46_1, all_32_1) = v2 & ( % 17.79/3.17 | | | | | | | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | DELTA: instantiating (119) with fresh symbols all_98_0, all_98_1, % 17.79/3.17 | | | | | | | all_98_2 gives: % 17.79/3.17 | | | | | | | (120) member(all_71_0, all_32_1) = all_98_1 & member(all_53_0, % 17.79/3.17 | | | | | | | all_32_2) = all_98_2 & member(all_46_1, all_32_1) = % 17.79/3.17 | | | | | | | all_98_0 & ( ~ (all_98_0 = 0) | ~ (all_98_1 = 0) | ~ % 17.79/3.17 | | | | | | | (all_98_2 = 0)) % 17.79/3.17 | | | | | | | % 17.79/3.17 | | | | | | | ALPHA: (120) implies: % 17.79/3.17 | | | | | | | (121) member(all_46_1, all_32_1) = all_98_0 % 17.79/3.17 | | | | | | | (122) member(all_53_0, all_32_2) = all_98_2 % 17.79/3.17 | | | | | | | (123) member(all_71_0, all_32_1) = all_98_1 % 17.79/3.17 | | | | | | | (124) ~ (all_98_0 = 0) | ~ (all_98_1 = 0) | ~ (all_98_2 = 0) % 17.79/3.17 | | | | | | | % 17.79/3.18 | | | | | | | GROUND_INST: instantiating (4) with 0, all_98_0, all_32_1, % 17.79/3.18 | | | | | | | all_46_1, simplifying with (37), (121) gives: % 17.79/3.18 | | | | | | | (125) all_98_0 = 0 % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | GROUND_INST: instantiating (4) with 0, all_98_2, all_32_2, % 17.79/3.18 | | | | | | | all_53_0, simplifying with (46), (122) gives: % 17.79/3.18 | | | | | | | (126) all_98_2 = 0 % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | GROUND_INST: instantiating (4) with 0, all_98_1, all_32_1, % 17.79/3.18 | | | | | | | all_71_0, simplifying with (87), (123) gives: % 17.79/3.18 | | | | | | | (127) all_98_1 = 0 % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | BETA: splitting (124) gives: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | Case 1: % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | (128) ~ (all_98_0 = 0) % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | REDUCE: (125), (128) imply: % 17.79/3.18 | | | | | | | | (129) $false % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | CLOSE: (129) is inconsistent. % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | Case 2: % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | (130) ~ (all_98_1 = 0) | ~ (all_98_2 = 0) % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | BETA: splitting (130) gives: % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | Case 1: % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | (131) ~ (all_98_1 = 0) % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | REDUCE: (127), (131) imply: % 17.79/3.18 | | | | | | | | | (132) $false % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | CLOSE: (132) is inconsistent. % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | Case 2: % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | (133) ~ (all_98_2 = 0) % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | REDUCE: (126), (133) imply: % 17.79/3.18 | | | | | | | | | (134) $false % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | | CLOSE: (134) is inconsistent. % 17.79/3.18 | | | | | | | | | % 17.79/3.18 | | | | | | | | End of split % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | End of split % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | End of split % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | Case 2: % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | (135) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 17.79/3.18 | | | | | | (member(all_62_0, all_32_2) = v2 & member(all_58_0, % 17.79/3.18 | | | | | | all_32_2) = v1 & member(all_46_2, all_32_3) = v0 & ( ~ % 17.79/3.18 | | | | | | (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | DELTA: instantiating (135) with fresh symbols all_83_0, all_83_1, % 17.79/3.18 | | | | | | all_83_2 gives: % 17.79/3.18 | | | | | | (136) member(all_62_0, all_32_2) = all_83_0 & member(all_58_0, % 17.79/3.18 | | | | | | all_32_2) = all_83_1 & member(all_46_2, all_32_3) = % 17.79/3.18 | | | | | | all_83_2 & ( ~ (all_83_0 = 0) | ~ (all_83_1 = 0) | ~ % 17.79/3.18 | | | | | | (all_83_2 = 0)) % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | ALPHA: (136) implies: % 17.79/3.18 | | | | | | (137) member(all_46_2, all_32_3) = all_83_2 % 17.79/3.18 | | | | | | (138) member(all_58_0, all_32_2) = all_83_1 % 17.79/3.18 | | | | | | (139) member(all_62_0, all_32_2) = all_83_0 % 17.79/3.18 | | | | | | (140) ~ (all_83_0 = 0) | ~ (all_83_1 = 0) | ~ (all_83_2 = 0) % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | REDUCE: (89), (139) imply: % 17.79/3.18 | | | | | | (141) member(all_53_0, all_32_2) = all_83_0 % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | GROUND_INST: instantiating (4) with 0, all_83_2, all_32_3, all_46_2, % 17.79/3.18 | | | | | | simplifying with (36), (137) gives: % 17.79/3.18 | | | | | | (142) all_83_2 = 0 % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | GROUND_INST: instantiating (4) with 0, all_83_0, all_32_2, all_53_0, % 17.79/3.18 | | | | | | simplifying with (46), (141) gives: % 17.79/3.18 | | | | | | (143) all_83_0 = 0 % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | GROUND_INST: instantiating (4) with 0, all_83_1, all_32_2, all_58_0, % 17.79/3.18 | | | | | | simplifying with (62), (138) gives: % 17.79/3.18 | | | | | | (144) all_83_1 = 0 % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | BETA: splitting (140) gives: % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | Case 1: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | (145) ~ (all_83_0 = 0) % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | REDUCE: (143), (145) imply: % 17.79/3.18 | | | | | | | (146) $false % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | CLOSE: (146) is inconsistent. % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | Case 2: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | (147) ~ (all_83_1 = 0) | ~ (all_83_2 = 0) % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | BETA: splitting (147) gives: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | Case 1: % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | (148) ~ (all_83_1 = 0) % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | REDUCE: (144), (148) imply: % 17.79/3.18 | | | | | | | | (149) $false % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | CLOSE: (149) is inconsistent. % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | Case 2: % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | (150) ~ (all_83_2 = 0) % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | REDUCE: (142), (150) imply: % 17.79/3.18 | | | | | | | | (151) $false % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | | CLOSE: (151) is inconsistent. % 17.79/3.18 | | | | | | | | % 17.79/3.18 | | | | | | | End of split % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | End of split % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | End of split % 17.79/3.18 | | | | | % 17.79/3.18 | | | | Case 2: % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | (152) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 17.79/3.18 | | | | | (member(all_62_0, all_32_2) = v2 & member(all_53_0, all_32_2) % 17.79/3.18 | | | | | = v1 & member(all_46_2, all_32_3) = v0 & ( ~ (v2 = 0) | ~ % 17.79/3.18 | | | | | (v1 = 0) | ~ (v0 = 0))) % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | DELTA: instantiating (152) with fresh symbols all_79_0, all_79_1, % 17.79/3.18 | | | | | all_79_2 gives: % 17.79/3.18 | | | | | (153) member(all_62_0, all_32_2) = all_79_0 & member(all_53_0, % 17.79/3.18 | | | | | all_32_2) = all_79_1 & member(all_46_2, all_32_3) = % 17.79/3.18 | | | | | all_79_2 & ( ~ (all_79_0 = 0) | ~ (all_79_1 = 0) | ~ % 17.79/3.18 | | | | | (all_79_2 = 0)) % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | ALPHA: (153) implies: % 17.79/3.18 | | | | | (154) member(all_46_2, all_32_3) = all_79_2 % 17.79/3.18 | | | | | (155) member(all_53_0, all_32_2) = all_79_1 % 17.79/3.18 | | | | | (156) member(all_62_0, all_32_2) = all_79_0 % 17.79/3.18 | | | | | (157) ~ (all_79_0 = 0) | ~ (all_79_1 = 0) | ~ (all_79_2 = 0) % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | GROUND_INST: instantiating (4) with 0, all_79_2, all_32_3, all_46_2, % 17.79/3.18 | | | | | simplifying with (36), (154) gives: % 17.79/3.18 | | | | | (158) all_79_2 = 0 % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | GROUND_INST: instantiating (4) with 0, all_79_1, all_32_2, all_53_0, % 17.79/3.18 | | | | | simplifying with (46), (155) gives: % 17.79/3.18 | | | | | (159) all_79_1 = 0 % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | GROUND_INST: instantiating (4) with 0, all_79_0, all_32_2, all_62_0, % 17.79/3.18 | | | | | simplifying with (79), (156) gives: % 17.79/3.18 | | | | | (160) all_79_0 = 0 % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | BETA: splitting (157) gives: % 17.79/3.18 | | | | | % 17.79/3.18 | | | | | Case 1: % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | (161) ~ (all_79_0 = 0) % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | REDUCE: (160), (161) imply: % 17.79/3.18 | | | | | | (162) $false % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | CLOSE: (162) is inconsistent. % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | Case 2: % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | (163) ~ (all_79_1 = 0) | ~ (all_79_2 = 0) % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | BETA: splitting (163) gives: % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | | Case 1: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | (164) ~ (all_79_1 = 0) % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | REDUCE: (159), (164) imply: % 17.79/3.18 | | | | | | | (165) $false % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | CLOSE: (165) is inconsistent. % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | Case 2: % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | (166) ~ (all_79_2 = 0) % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | REDUCE: (158), (166) imply: % 17.79/3.18 | | | | | | | (167) $false % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | | CLOSE: (167) is inconsistent. % 17.79/3.18 | | | | | | | % 17.79/3.18 | | | | | | End of split % 17.79/3.18 | | | | | | % 17.79/3.18 | | | | | End of split % 17.79/3.18 | | | | | % 17.79/3.18 | | | | End of split % 17.79/3.18 | | | | % 17.79/3.18 | | | End of split % 17.79/3.18 | | | % 17.79/3.18 | | End of split % 17.79/3.18 | | % 17.79/3.18 | End of split % 17.79/3.18 | % 17.79/3.18 End of proof % 18.07/3.18 % SZS output end Proof for theBenchmark % 18.07/3.18 % 18.07/3.18 2551ms %------------------------------------------------------------------------------