%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU146+2 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.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 17:42:46 EDT 2023 % Result : Theorem 30.13s 5.16s % Output : Proof 83.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SEU146+2 : TPTP v8.1.2. Released v3.3.0. % 0.00/0.10 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.30 % Computer : n006.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Wed Aug 23 13:33:23 EDT 2023 % 0.10/0.30 % CPUTime : % 0.16/0.56 ________ _____ % 0.16/0.56 ___ __ \_________(_)________________________________ % 0.16/0.56 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.56 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.56 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.56 % 0.16/0.56 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.56 (2023-06-19) % 0.16/0.56 % 0.16/0.56 (c) Philipp Rümmer, 2009-2023 % 0.16/0.56 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.56 Amanda Stjerna. % 0.16/0.56 Free software under BSD-3-Clause. % 0.16/0.56 % 0.16/0.56 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.56 % 0.16/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.58 Running up to 7 provers in parallel. % 0.16/0.60 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.60 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.60 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.60 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.60 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.60 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.20/1.18 Prover 1: Preprocessing ... % 3.20/1.18 Prover 4: Preprocessing ... % 3.49/1.23 Prover 6: Preprocessing ... % 3.49/1.23 Prover 5: Preprocessing ... % 3.49/1.23 Prover 0: Preprocessing ... % 3.67/1.24 Prover 3: Preprocessing ... % 3.67/1.24 Prover 2: Preprocessing ... % 9.66/2.15 Prover 1: Warning: ignoring some quantifiers % 9.66/2.16 Prover 5: Proving ... % 10.80/2.26 Prover 1: Constructing countermodel ... % 10.80/2.28 Prover 6: Proving ... % 11.02/2.31 Prover 3: Warning: ignoring some quantifiers % 11.32/2.35 Prover 3: Constructing countermodel ... % 11.32/2.36 Prover 2: Proving ... % 11.79/2.42 Prover 4: Warning: ignoring some quantifiers % 12.90/2.59 Prover 4: Constructing countermodel ... % 13.19/2.61 Prover 0: Proving ... % 14.34/2.88 Prover 3: gave up % 15.20/2.89 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.71/3.01 Prover 7: Preprocessing ... % 18.00/3.27 Prover 7: Warning: ignoring some quantifiers % 18.00/3.29 Prover 1: gave up % 18.00/3.31 Prover 7: Constructing countermodel ... % 18.00/3.31 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 18.41/3.40 Prover 8: Preprocessing ... % 22.31/3.88 Prover 8: Warning: ignoring some quantifiers % 22.75/3.92 Prover 8: Constructing countermodel ... % 24.10/4.12 Prover 7: gave up % 24.10/4.13 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 24.10/4.22 Prover 9: Preprocessing ... % 28.10/4.69 Prover 9: Warning: ignoring some quantifiers % 28.56/4.72 Prover 9: Constructing countermodel ... % 30.13/5.16 Prover 2: proved (4565ms) % 30.13/5.16 % 30.13/5.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.13/5.16 % 31.62/5.17 Prover 9: stopped % 31.62/5.19 Prover 0: stopped % 31.62/5.19 Prover 6: stopped % 31.62/5.19 Prover 5: stopped % 31.62/5.21 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 31.62/5.21 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.62/5.21 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 31.62/5.21 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 31.62/5.21 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 31.62/5.25 Prover 10: Preprocessing ... % 31.62/5.26 Prover 11: Preprocessing ... % 32.82/5.30 Prover 13: Preprocessing ... % 32.82/5.31 Prover 16: Preprocessing ... % 32.82/5.32 Prover 8: gave up % 33.27/5.33 Prover 19: Preprocessing ... % 33.48/5.38 Prover 10: Warning: ignoring some quantifiers % 33.48/5.39 Prover 10: Constructing countermodel ... % 33.99/5.45 Prover 13: Warning: ignoring some quantifiers % 34.29/5.48 Prover 13: Constructing countermodel ... % 34.29/5.52 Prover 16: Warning: ignoring some quantifiers % 34.84/5.53 Prover 11: Warning: ignoring some quantifiers % 34.84/5.54 Prover 16: Constructing countermodel ... % 34.84/5.55 Prover 11: Constructing countermodel ... % 34.84/5.56 Prover 19: Warning: ignoring some quantifiers % 34.84/5.56 Prover 10: gave up % 35.11/5.57 Prover 19: Constructing countermodel ... % 36.20/5.95 Prover 19: gave up % 37.37/5.99 Prover 13: gave up % 39.74/6.29 Prover 16: gave up % 81.63/15.65 Prover 11: Found proof (size 425) % 81.63/15.65 Prover 11: proved (10461ms) % 81.63/15.65 Prover 4: stopped % 81.63/15.65 % 81.63/15.65 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.63/15.65 % 82.12/15.69 % SZS output start Proof for theBenchmark % 82.12/15.70 Assumptions after simplification: % 82.12/15.70 --------------------------------- % 82.12/15.70 % 82.12/15.70 (commutativity_k2_xboole_0) % 82.12/15.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v1, v0) = v2) | ~ % 82.12/15.75 $i(v1) | ~ $i(v0) | (set_union2(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! % 82.12/15.75 [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 82.12/15.75 | (set_union2(v1, v0) = v2 & $i(v2))) % 82.12/15.75 % 82.12/15.75 (commutativity_k3_xboole_0) % 82.12/15.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_intersection2(v1, v0) = v2) % 82.12/15.75 | ~ $i(v1) | ~ $i(v0) | (set_intersection2(v0, v1) = v2 & $i(v2))) & ! % 82.12/15.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_intersection2(v0, v1) = v2) | % 82.12/15.75 ~ $i(v1) | ~ $i(v0) | (set_intersection2(v1, v0) = v2 & $i(v2))) % 82.12/15.75 % 82.12/15.75 (d10_xboole_0) % 82.12/15.76 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (subset(v1, v0) = 0) | ~ $i(v1) | % 82.12/15.76 ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & subset(v0, v1) = v2)) & ! [v0: $i] % 82.12/15.76 : ! [v1: $i] : (v1 = v0 | ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | % 82.12/15.76 ? [v2: int] : ( ~ (v2 = 0) & subset(v1, v0) = v2)) & ! [v0: $i] : ! [v1: % 82.12/15.76 int] : (v1 = 0 | ~ (subset(v0, v0) = v1) | ~ $i(v0)) % 82.12/15.76 % 82.12/15.76 (d1_tarski) % 82.12/15.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (singleton(v0) = v1) | % 82.12/15.77 ~ (in(v2, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! % 82.12/15.77 [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (singleton(v0) = v1) | ~ (in(v0, v1) = % 82.12/15.77 v2) | ~ $i(v1) | ~ $i(v0)) & ? [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 82.12/15.77 (v2 = v0 | ~ (singleton(v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? % 82.12/15.77 [v4: int] : ($i(v3) & ( ~ (v3 = v1) | ( ~ (v4 = 0) & in(v1, v0) = v4)) & (v3 % 82.12/15.77 = v1 | (v4 = 0 & in(v3, v0) = 0)))) % 82.12/15.77 % 82.12/15.77 (d2_tarski) % 82.12/15.78 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v1 | v3 = v0 | % 82.12/15.78 ~ (unordered_pair(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ $i(v3) | ~ % 82.12/15.78 $i(v2) | ~ $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 82.12/15.78 ! [v3: int] : (v3 = 0 | ~ (unordered_pair(v0, v1) = v2) | ~ (in(v1, v2) = % 82.12/15.78 v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! % 82.12/15.78 [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (unordered_pair(v0, v1) = v2) | ~ % 82.12/15.78 (in(v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) & ? [v0: $i] : ! % 82.12/15.78 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 | ~ (unordered_pair(v1, v2) = % 82.12/15.78 v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: int] : % 82.12/15.78 ($i(v4) & (v4 = v2 | v4 = v1 | (v5 = 0 & in(v4, v0) = 0)) & (( ~ (v5 = 0) & % 82.12/15.78 in(v4, v0) = v5) | ( ~ (v4 = v2) & ~ (v4 = v1))))) % 82.12/15.78 % 82.12/15.78 (d2_xboole_0) % 82.12/15.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 82.12/15.79 | ~ (set_union2(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ~ $i(v3) | ~ % 82.12/15.79 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) % 82.12/15.79 & ~ (v5 = 0) & in(v3, v1) = v6 & in(v3, v0) = v5)) & ! [v0: $i] : ! % 82.12/15.79 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 82.12/15.79 (set_union2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | ~ $i(v2) | % 82.12/15.79 ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & in(v3, v0) = % 82.12/15.79 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0: $i] : ! [v1: $i] : ! % 82.12/15.79 [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (set_union2(v0, v1) = v2) % 82.12/15.79 | ~ (in(v3, v0) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 82.12/15.79 [v5: int] : ? [v6: int] : ((v6 = 0 & in(v3, v1) = 0) | ( ~ (v5 = 0) & % 82.12/15.79 in(v3, v2) = v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 82.12/15.79 $i] : ! [v4: any] : ( ~ (set_union2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | % 82.12/15.79 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : % 82.12/15.79 ((v6 = 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & in(v3, v0) = v5))) % 82.12/15.79 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ % 82.12/15.79 (set_union2(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ~ $i(v3) | ~ $i(v2) | % 82.12/15.79 ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & in(v3, v2) = % 82.12/15.79 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & in(v3, v1) = v5))) & ! [v0: $i] : ! % 82.12/15.79 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (set_union2(v0, v1) = v2) | ~ % 82.12/15.79 (in(v3, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 82.12/15.79 int] : ? [v5: int] : ((v5 = 0 & in(v3, v1) = 0) | (v4 = 0 & in(v3, v0) = % 82.12/15.79 0))) & ? [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 % 82.12/15.79 | ~ (set_union2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 82.12/15.79 $i] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ($i(v4) & ((v7 = 0 & % 82.12/15.79 in(v4, v2) = 0) | (v6 = 0 & in(v4, v1) = 0) | (v5 = 0 & in(v4, v0) = % 82.12/15.79 0)) & (( ~ (v7 = 0) & ~ (v6 = 0) & in(v4, v2) = v7 & in(v4, v1) = v6) % 82.12/15.79 | ( ~ (v5 = 0) & in(v4, v0) = v5)))) % 82.12/15.79 % 82.12/15.79 (d3_tarski) % 82.12/15.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 82.12/15.80 (subset(v0, v1) = 0) | ~ (in(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 82.12/15.80 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & in(v2, v0) = v4)) & ! [v0: $i] : ! % 82.12/15.80 [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ~ $i(v1) | ~ % 82.12/15.80 $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & in(v3, v1) = v4 & % 82.12/15.80 in(v3, v0) = 0 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 82.12/15.80 (subset(v0, v1) = 0) | ~ (in(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 82.12/15.80 $i(v0) | in(v2, v1) = 0) % 82.12/15.80 % 82.12/15.80 (d3_xboole_0) % 82.12/15.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 82.12/15.81 | ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ~ $i(v3) | % 82.12/15.81 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : (( ~ (v6 = % 82.12/15.81 0) & in(v3, v1) = v6) | ( ~ (v5 = 0) & in(v3, v0) = v5))) & ! [v0: % 82.12/15.81 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ % 82.12/15.81 (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | ~ % 82.12/15.81 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & v4 % 82.12/15.81 = 0 & in(v3, v0) = 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0: $i] % 82.12/15.81 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ % 82.12/15.81 (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ~ $i(v3) | ~ % 82.12/15.81 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & v4 % 82.12/15.81 = 0 & in(v3, v1) = 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0: $i] % 82.12/15.81 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (set_intersection2(v0, v1) = % 82.12/15.81 v2) | ~ (in(v3, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 82.12/15.81 | (in(v3, v1) = 0 & in(v3, v0) = 0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 82.12/15.81 $i] : ! [v3: $i] : ( ~ (set_intersection2(v0, v1) = v2) | ~ (in(v3, v1) = % 82.12/15.81 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ? % 82.12/15.81 [v5: int] : ((v5 = 0 & in(v3, v2) = 0) | ( ~ (v4 = 0) & in(v3, v0) = v4))) & % 82.12/15.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 82.12/15.81 (set_intersection2(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ~ $i(v3) | ~ % 82.12/15.81 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: int] : ((v5 = 0 & % 82.12/15.81 in(v3, v2) = 0) | ( ~ (v4 = 0) & in(v3, v1) = v4))) & ? [v0: $i] : ! % 82.12/15.81 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 | ~ (set_intersection2(v1, % 82.12/15.81 v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: % 82.12/15.81 int] : ? [v6: int] : ? [v7: int] : ($i(v4) & ((v7 = 0 & v6 = 0 & in(v4, % 82.12/15.81 v2) = 0 & in(v4, v1) = 0) | (v5 = 0 & in(v4, v0) = 0)) & (( ~ (v7 = % 82.12/15.81 0) & in(v4, v2) = v7) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v5 = % 82.12/15.81 0) & in(v4, v0) = v5)))) % 82.12/15.81 % 82.12/15.81 (d4_xboole_0) % 82.12/15.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 82.12/15.82 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = v4) | ~ $i(v3) | ~ % 82.12/15.82 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & % 82.12/15.82 in(v3, v1) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) & ! [v0: $i] : ! % 82.12/15.82 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 82.12/15.82 (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | ~ $i(v2) % 82.12/15.82 | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & in(v3, % 82.12/15.82 v2) = 0) | ( ~ (v5 = 0) & in(v3, v0) = v5))) & ! [v0: $i] : ! [v1: % 82.12/15.82 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ (set_difference(v0, v1) % 82.12/15.82 = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 82.12/15.82 $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = 0 & ~ (v4 = 0) & in(v3, v0) = % 82.12/15.82 0) | ( ~ (v5 = 0) & in(v3, v2) = v5))) & ! [v0: $i] : ! [v1: $i] : ! % 82.12/15.82 [v2: $i] : ! [v3: $i] : ! [v4: any] : ( ~ (set_difference(v0, v1) = v2) | ~ % 82.12/15.82 (in(v3, v0) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 82.12/15.82 int] : ? [v6: int] : ((v4 = 0 & ~ (v6 = 0) & in(v3, v1) = v6) | ( ~ (v5 % 82.12/15.82 = 0) & in(v3, v2) = v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 82.12/15.82 ! [v3: $i] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ % 82.12/15.82 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & % 82.12/15.82 in(v3, v1) = v4 & in(v3, v0) = 0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 82.12/15.82 $i] : ! [v3: $i] : ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = 0) % 82.12/15.82 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: % 82.12/15.82 int] : ((v5 = 0 & in(v3, v2) = 0) | (v4 = 0 & in(v3, v1) = 0))) & ? [v0: % 82.12/15.82 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 | ~ % 82.12/15.82 (set_difference(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 82.12/15.82 $i] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ($i(v4) & ((v7 = 0 & % 82.12/15.82 in(v4, v2) = 0) | ( ~ (v6 = 0) & in(v4, v1) = v6) | ( ~ (v5 = 0) & % 82.12/15.82 in(v4, v0) = v5)) & ((v6 = 0 & ~ (v7 = 0) & in(v4, v2) = v7 & in(v4, % 82.12/15.82 v1) = 0) | (v5 = 0 & in(v4, v0) = 0)))) % 82.12/15.82 % 82.12/15.82 (l2_zfmisc_1) % 82.12/15.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 82.12/15.83 (singleton(v0) = v2) | ~ (subset(v2, v1) = v3) | ~ $i(v1) | ~ $i(v0) | ? % 82.12/15.83 [v4: int] : ( ~ (v4 = 0) & in(v0, v1) = v4)) & ! [v0: $i] : ! [v1: $i] : % 82.12/15.83 ! [v2: int] : (v2 = 0 | ~ (in(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 82.12/15.83 $i] : ? [v4: int] : ( ~ (v4 = 0) & singleton(v0) = v3 & subset(v3, v1) = % 82.12/15.83 v4 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 82.12/15.83 (singleton(v0) = v2) | ~ (subset(v2, v1) = 0) | ~ $i(v1) | ~ $i(v0) | % 82.12/15.83 in(v0, v1) = 0) & ! [v0: $i] : ! [v1: $i] : ( ~ (in(v0, v1) = 0) | ~ % 82.12/15.83 $i(v1) | ~ $i(v0) | ? [v2: $i] : (singleton(v0) = v2 & subset(v2, v1) = 0 % 82.12/15.83 & $i(v2))) % 82.12/15.83 % 82.12/15.83 (l32_xboole_1) % 82.12/15.83 $i(empty_set) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = empty_set | ~ % 82.12/15.83 (set_difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ % 82.12/15.83 (v3 = 0) & subset(v0, v1) = v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 82.12/15.83 int] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 82.12/15.83 $i] : ( ~ (v3 = empty_set) & set_difference(v0, v1) = v3 & $i(v3))) & ! % 82.12/15.83 [v0: $i] : ! [v1: $i] : ( ~ (set_difference(v0, v1) = empty_set) | ~ $i(v1) % 82.12/15.83 | ~ $i(v0) | subset(v0, v1) = 0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 82.12/15.83 (subset(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | set_difference(v0, v1) = % 82.12/15.83 empty_set) % 82.12/15.83 % 82.12/15.83 (l4_zfmisc_1) % 82.12/15.83 $i(empty_set) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : % 82.12/15.83 (singleton(v1) = v2 & subset(v0, v2) = v3 & $i(v2) & $i(v1) & $i(v0) & ((v3 = % 82.12/15.83 0 & ~ (v2 = v0) & ~ (v0 = empty_set)) | ( ~ (v3 = 0) & (v2 = v0 | v0 = % 82.12/15.83 empty_set)))) % 82.12/15.83 % 82.12/15.83 (rc1_xboole_0) % 82.12/15.83 ? [v0: $i] : (empty(v0) = 0 & $i(v0)) % 82.12/15.83 % 82.12/15.83 (t12_xboole_1) % 82.12/15.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (set_union2(v0, v1) = % 82.12/15.83 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & subset(v0, v1) % 82.12/15.83 = v3)) & ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) % 82.12/15.83 | ~ $i(v0) | set_union2(v0, v1) = v1) % 82.12/15.83 % 82.12/15.83 (t28_xboole_1) % 82.12/15.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (set_intersection2(v0, % 82.12/15.83 v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & % 82.12/15.83 subset(v0, v1) = v3)) & ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = % 82.12/15.83 0) | ~ $i(v1) | ~ $i(v0) | set_intersection2(v0, v1) = v0) % 82.12/15.83 % 82.12/15.83 (t36_xboole_1) % 82.12/15.83 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v0, v1) = v2) | % 82.12/15.83 ~ $i(v1) | ~ $i(v0) | subset(v2, v0) = 0) % 82.12/15.83 % 82.12/15.83 (t37_xboole_1) % 82.12/15.84 $i(empty_set) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = empty_set | ~ % 82.12/15.84 (set_difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ % 82.12/15.84 (v3 = 0) & subset(v0, v1) = v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 82.12/15.84 int] : (v2 = 0 | ~ (subset(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 82.12/15.84 $i] : ( ~ (v3 = empty_set) & set_difference(v0, v1) = v3 & $i(v3))) & ! % 82.12/15.84 [v0: $i] : ! [v1: $i] : ( ~ (set_difference(v0, v1) = empty_set) | ~ $i(v1) % 82.12/15.84 | ~ $i(v0) | subset(v0, v1) = 0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 82.12/15.84 (subset(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | set_difference(v0, v1) = % 82.12/15.84 empty_set) % 82.12/15.84 % 82.12/15.84 (t39_xboole_1) % 82.12/15.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v1, v0) = v2) | % 82.12/15.84 ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_union2(v0, v2) = v3 & % 82.12/15.84 set_union2(v0, v1) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 82.12/15.84 $i] : ( ~ (set_union2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 82.12/15.84 (set_difference(v1, v0) = v3 & set_union2(v0, v3) = v2 & $i(v3) & $i(v2))) % 82.12/15.84 % 82.12/15.84 (t40_xboole_1) % 82.12/15.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v0, v1) = v2) | % 82.12/15.84 ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v3, v1) = v2 & % 82.12/15.84 set_union2(v0, v1) = v3 & $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: $i] : % 82.12/15.84 ! [v2: $i] : ( ~ (set_union2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 82.12/15.84 $i] : (set_difference(v2, v1) = v3 & set_difference(v0, v1) = v3 & % 82.12/15.84 $i(v3))) % 82.12/15.84 % 82.12/15.84 (t45_xboole_1) % 82.12/15.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v1, v0) = v2) | % 82.12/15.84 ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ? [v4: $i] : ((v4 = v1 & % 82.12/15.84 set_union2(v0, v2) = v1) | ( ~ (v3 = 0) & subset(v0, v1) = v3))) & ! % 82.12/15.84 [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 82.12/15.84 [v2: $i] : (set_difference(v1, v0) = v2 & set_union2(v0, v2) = v1 & $i(v2))) % 82.12/15.84 % 82.12/15.84 (t48_xboole_1) % 82.12/15.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v0, v1) = v2) | % 82.12/15.84 ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v0, v2) = v3 & % 82.12/15.84 set_intersection2(v0, v1) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! % 82.12/15.84 [v2: $i] : ( ~ (set_intersection2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 82.12/15.84 [v3: $i] : (set_difference(v0, v3) = v2 & set_difference(v0, v1) = v3 & % 82.12/15.84 $i(v3) & $i(v2))) % 82.12/15.84 % 82.12/15.84 (t4_xboole_0) % 82.12/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 82.12/15.85 (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ $i(v3) | ~ % 82.12/15.85 $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & disjoint(v0, v1) = v4)) & % 82.12/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (disjoint(v0, v1) = % 82.12/15.85 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 82.12/15.85 (set_intersection2(v0, v1) = v3 & in(v4, v3) = 0 & $i(v4) & $i(v3))) & ! % 82.12/15.85 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_intersection2(v0, v1) = v2) | % 82.12/15.85 ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ? [v4: $i] : ? [v5: int] : ($i(v4) & % 82.12/15.85 ((v5 = 0 & in(v4, v2) = 0) | (v3 = 0 & disjoint(v0, v1) = 0)))) & ! [v0: % 82.12/15.85 $i] : ! [v1: $i] : ( ~ (disjoint(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 82.12/15.85 [v2: $i] : (set_intersection2(v0, v1) = v2 & $i(v2) & ! [v3: $i] : ( ~ % 82.12/15.85 (in(v3, v2) = 0) | ~ $i(v3)))) % 82.12/15.85 % 82.12/15.85 (t69_enumset1) % 82.12/15.85 ! [v0: $i] : ! [v1: $i] : ( ~ (singleton(v0) = v1) | ~ $i(v0) | % 82.12/15.85 (unordered_pair(v0, v0) = v1 & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 82.12/15.85 (unordered_pair(v0, v0) = v1) | ~ $i(v0) | (singleton(v0) = v1 & $i(v1))) % 82.12/15.85 % 82.12/15.85 (t6_boole) % 82.12/15.85 $i(empty_set) & ! [v0: $i] : (v0 = empty_set | ~ (empty(v0) = 0) | ~ % 82.12/15.85 $i(v0)) % 82.12/15.85 % 82.12/15.85 (t7_xboole_1) % 82.12/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v0, v1) = v2) | ~ % 82.12/15.85 $i(v1) | ~ $i(v0) | subset(v0, v2) = 0) % 82.12/15.85 % 82.12/15.85 (t83_xboole_1) % 82.12/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (set_difference(v0, % 82.12/15.85 v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & % 82.12/15.85 disjoint(v0, v1) = v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = % 82.12/15.85 0 | ~ (disjoint(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ( ~ % 82.12/15.85 (v3 = v0) & set_difference(v0, v1) = v3 & $i(v3))) & ! [v0: $i] : ! [v1: % 82.12/15.85 $i] : ( ~ (disjoint(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | % 82.12/15.85 set_difference(v0, v1) = v0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 82.12/15.85 (set_difference(v0, v1) = v0) | ~ $i(v1) | ~ $i(v0) | disjoint(v0, v1) = % 82.12/15.85 0) % 82.12/15.85 % 82.12/15.85 (function-axioms) % 82.12/15.86 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 82.12/15.86 [v3: $i] : (v1 = v0 | ~ (disjoint(v3, v2) = v1) | ~ (disjoint(v3, v2) = v0)) % 82.12/15.86 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 82.12/15.86 (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) & ! [v0: % 82.12/15.86 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 82.12/15.86 : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) & ! [v0: % 82.12/15.86 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 82.12/15.86 (set_intersection2(v3, v2) = v1) | ~ (set_intersection2(v3, v2) = v0)) & ! % 82.12/15.86 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 82.12/15.86 (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) & ! [v0: $i] : ! % 82.12/15.86 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (unordered_pair(v3, v2) = % 82.12/15.86 v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 82.12/15.86 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 82.12/15.86 (proper_subset(v3, v2) = v1) | ~ (proper_subset(v3, v2) = v0)) & ! [v0: % 82.12/15.86 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 82.12/15.86 : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0: % 82.12/15.86 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 82.12/15.86 ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 82.12/15.86 [v2: $i] : (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) % 82.12/15.86 % 82.12/15.86 Further assumptions not needed in the proof: % 82.12/15.86 -------------------------------------------- % 82.12/15.86 antisymmetry_r2_hidden, antisymmetry_r2_xboole_0, commutativity_k2_tarski, % 82.12/15.86 d1_xboole_0, d7_xboole_0, d8_xboole_0, dt_k1_tarski, dt_k1_xboole_0, % 82.12/15.86 dt_k2_tarski, dt_k2_xboole_0, dt_k3_xboole_0, dt_k4_xboole_0, fc1_xboole_0, % 82.12/15.86 fc2_xboole_0, fc3_xboole_0, idempotence_k2_xboole_0, idempotence_k3_xboole_0, % 82.12/15.86 irreflexivity_r2_xboole_0, l1_zfmisc_1, l3_zfmisc_1, rc2_xboole_0, % 82.12/15.86 reflexivity_r1_tarski, symmetry_r1_xboole_0, t17_xboole_1, t19_xboole_1, % 82.12/15.86 t1_boole, t1_xboole_1, t26_xboole_1, t2_boole, t2_tarski, t2_xboole_1, % 82.12/15.86 t33_xboole_1, t3_boole, t3_xboole_0, t3_xboole_1, t4_boole, t60_xboole_1, % 82.12/15.86 t63_xboole_1, t7_boole, t8_boole, t8_xboole_1 % 82.12/15.86 % 82.12/15.86 Those formulas are unsatisfiable: % 82.12/15.86 --------------------------------- % 82.12/15.86 % 82.12/15.86 Begin of proof % 82.12/15.86 | % 82.12/15.86 | ALPHA: (commutativity_k2_xboole_0) implies: % 82.12/15.86 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v1, v0) = v2) % 82.12/15.86 | | ~ $i(v1) | ~ $i(v0) | (set_union2(v0, v1) = v2 & $i(v2))) % 82.12/15.86 | % 82.12/15.86 | ALPHA: (commutativity_k3_xboole_0) implies: % 82.12/15.86 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_intersection2(v1, % 82.12/15.86 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | (set_intersection2(v0, v1) = % 82.12/15.86 | v2 & $i(v2))) % 82.12/15.86 | % 82.12/15.86 | ALPHA: (d10_xboole_0) implies: % 82.12/15.86 | (3) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (subset(v1, v0) = 0) | ~ % 82.12/15.86 | $i(v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & subset(v0, v1) = % 82.12/15.86 | v2)) % 82.12/15.86 | % 82.12/15.86 | ALPHA: (d1_tarski) implies: % 82.12/15.86 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (singleton(v0) % 82.12/15.86 | = v1) | ~ (in(v2, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 82.12/15.86 | % 82.12/15.86 | ALPHA: (d2_tarski) implies: % 82.12/15.87 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v1 | v3 = % 82.12/15.87 | v0 | ~ (unordered_pair(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ % 82.12/15.87 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 82.12/15.87 | % 82.12/15.87 | ALPHA: (d2_xboole_0) implies: % 82.12/15.87 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : % 82.12/15.87 | ( ~ (set_union2(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ~ $i(v3) | ~ % 82.12/15.87 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = % 82.12/15.87 | 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & in(v3, v1) = % 82.12/15.87 | v5))) % 82.12/15.87 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : % 82.12/15.87 | ( ~ (set_union2(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | ~ % 82.12/15.87 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ((v6 = % 82.12/15.87 | 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & ~ (v4 = 0) & in(v3, v0) = % 82.12/15.87 | v5))) % 82.12/15.87 | % 82.12/15.87 | ALPHA: (d3_tarski) implies: % 82.12/15.87 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (subset(v0, v1) = 0) | ~ % 82.12/15.87 | (in(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | in(v2, v1) = % 82.12/15.87 | 0) % 82.12/15.87 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subset(v0, v1) % 82.12/15.87 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ % 82.12/15.87 | (v4 = 0) & in(v3, v1) = v4 & in(v3, v0) = 0 & $i(v3))) % 82.12/15.87 | % 82.12/15.87 | ALPHA: (d3_xboole_0) implies: % 82.12/15.87 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 82.12/15.87 | (set_intersection2(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ $i(v3) | % 82.12/15.87 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | (in(v3, v1) = 0 & in(v3, v0) = % 82.12/15.87 | 0)) % 82.12/15.87 | % 82.12/15.87 | ALPHA: (d4_xboole_0) implies: % 82.12/15.87 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 82.12/15.87 | (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = 0) | ~ $i(v3) | ~ % 82.12/15.87 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: int] : ((v5 % 82.12/15.87 | = 0 & in(v3, v2) = 0) | (v4 = 0 & in(v3, v1) = 0))) % 82.12/15.87 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 82.12/15.87 | (set_difference(v0, v1) = v2) | ~ (in(v3, v2) = 0) | ~ $i(v3) | ~ % 82.12/15.87 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & % 82.12/15.87 | in(v3, v1) = v4 & in(v3, v0) = 0)) % 82.12/15.88 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : % 82.12/15.88 | ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v0) = v4) | ~ $i(v3) | % 82.12/15.88 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : % 82.12/15.88 | ((v4 = 0 & ~ (v6 = 0) & in(v3, v1) = v6) | ( ~ (v5 = 0) & in(v3, % 82.12/15.88 | v2) = v5))) % 82.12/15.88 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: any] : % 82.12/15.88 | ( ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ $i(v3) | % 82.12/15.88 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : % 82.12/15.88 | ((v6 = 0 & ~ (v4 = 0) & in(v3, v0) = 0) | ( ~ (v5 = 0) & in(v3, v2) % 82.12/15.88 | = v5))) % 82.12/15.88 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 82.12/15.88 | (v4 = 0 | ~ (set_difference(v0, v1) = v2) | ~ (in(v3, v1) = v4) | ~ % 82.12/15.88 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: % 82.12/15.88 | int] : ((v6 = 0 & in(v3, v2) = 0) | ( ~ (v5 = 0) & in(v3, v0) = % 82.12/15.88 | v5))) % 82.12/15.88 | % 82.12/15.88 | ALPHA: (l2_zfmisc_1) implies: % 82.12/15.88 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ (in(v0, v1) = 0) | ~ $i(v1) | ~ % 82.12/15.88 | $i(v0) | ? [v2: $i] : (singleton(v0) = v2 & subset(v2, v1) = 0 & % 82.12/15.88 | $i(v2))) % 82.12/15.88 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (in(v0, v1) = % 82.12/15.88 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 % 82.12/15.88 | = 0) & singleton(v0) = v3 & subset(v3, v1) = v4 & $i(v3))) % 82.69/15.88 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 82.69/15.88 | (singleton(v0) = v2) | ~ (subset(v2, v1) = v3) | ~ $i(v1) | ~ % 82.69/15.88 | $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & in(v0, v1) = v4)) % 82.69/15.88 | % 82.69/15.88 | ALPHA: (t12_xboole_1) implies: % 82.69/15.88 | (19) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ % 82.69/15.88 | $i(v0) | set_union2(v0, v1) = v1) % 82.69/15.88 | % 82.69/15.88 | ALPHA: (t28_xboole_1) implies: % 82.69/15.88 | (20) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ % 82.69/15.88 | $i(v0) | set_intersection2(v0, v1) = v0) % 82.69/15.88 | % 82.69/15.88 | ALPHA: (t37_xboole_1) implies: % 82.69/15.88 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ % 82.69/15.88 | $i(v0) | set_difference(v0, v1) = empty_set) % 82.69/15.88 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subset(v0, % 82.69/15.88 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ( ~ (v3 = % 82.69/15.88 | empty_set) & set_difference(v0, v1) = v3 & $i(v3))) % 82.69/15.88 | % 82.69/15.88 | ALPHA: (t39_xboole_1) implies: % 82.69/15.89 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v0, v1) = % 82.69/15.89 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v1, % 82.69/15.89 | v0) = v3 & set_union2(v0, v3) = v2 & $i(v3) & $i(v2))) % 82.69/15.89 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v1, v0) % 82.69/15.89 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_union2(v0, v2) % 82.69/15.89 | = v3 & set_union2(v0, v1) = v3 & $i(v3))) % 82.69/15.89 | % 82.69/15.89 | ALPHA: (t40_xboole_1) implies: % 82.69/15.89 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_union2(v0, v1) = % 82.69/15.89 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v2, % 82.69/15.89 | v1) = v3 & set_difference(v0, v1) = v3 & $i(v3))) % 82.69/15.89 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v0, v1) % 82.69/15.89 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v3, % 82.69/15.89 | v1) = v2 & set_union2(v0, v1) = v3 & $i(v3) & $i(v2))) % 82.69/15.89 | % 82.69/15.89 | ALPHA: (t45_xboole_1) implies: % 82.69/15.89 | (27) ! [v0: $i] : ! [v1: $i] : ( ~ (subset(v0, v1) = 0) | ~ $i(v1) | ~ % 82.69/15.89 | $i(v0) | ? [v2: $i] : (set_difference(v1, v0) = v2 & set_union2(v0, % 82.69/15.89 | v2) = v1 & $i(v2))) % 83.03/15.89 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v1, v0) % 83.03/15.89 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ? [v4: $i] : ((v4 % 83.03/15.89 | = v1 & set_union2(v0, v2) = v1) | ( ~ (v3 = 0) & subset(v0, v1) % 83.03/15.89 | = v3))) % 83.03/15.89 | % 83.03/15.89 | ALPHA: (t48_xboole_1) implies: % 83.03/15.89 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_difference(v0, v1) % 83.03/15.89 | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (set_difference(v0, % 83.03/15.89 | v2) = v3 & set_intersection2(v0, v1) = v3 & $i(v3))) % 83.03/15.89 | % 83.03/15.89 | ALPHA: (t4_xboole_0) implies: % 83.03/15.89 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (set_intersection2(v0, % 83.03/15.89 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] : ? [v4: $i] : % 83.03/15.89 | ? [v5: int] : ($i(v4) & ((v5 = 0 & in(v4, v2) = 0) | (v3 = 0 & % 83.03/15.89 | disjoint(v0, v1) = 0)))) % 83.03/15.89 | % 83.03/15.89 | ALPHA: (t69_enumset1) implies: % 83.03/15.90 | (31) ! [v0: $i] : ! [v1: $i] : ( ~ (singleton(v0) = v1) | ~ $i(v0) | % 83.03/15.90 | (unordered_pair(v0, v0) = v1 & $i(v1))) % 83.03/15.90 | % 83.03/15.90 | ALPHA: (t6_boole) implies: % 83.03/15.90 | (32) ! [v0: $i] : (v0 = empty_set | ~ (empty(v0) = 0) | ~ $i(v0)) % 83.03/15.90 | % 83.03/15.90 | ALPHA: (t83_xboole_1) implies: % 83.03/15.90 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ % 83.03/15.90 | (set_difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: int] % 83.03/15.90 | : ( ~ (v3 = 0) & disjoint(v0, v1) = v3)) % 83.03/15.90 | % 83.03/15.90 | ALPHA: (l4_zfmisc_1) implies: % 83.03/15.90 | (34) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : % 83.03/15.90 | (singleton(v1) = v2 & subset(v0, v2) = v3 & $i(v2) & $i(v1) & $i(v0) & % 83.03/15.90 | ((v3 = 0 & ~ (v2 = v0) & ~ (v0 = empty_set)) | ( ~ (v3 = 0) & (v2 % 83.03/15.90 | = v0 | v0 = empty_set)))) % 83.03/15.90 | % 83.03/15.90 | ALPHA: (function-axioms) implies: % 83.03/15.90 | (35) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (singleton(v2) % 83.03/15.90 | = v1) | ~ (singleton(v2) = v0)) % 83.03/15.90 | (36) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 83.03/15.90 | : ! [v3: $i] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = % 83.03/15.90 | v0)) % 83.03/15.90 | (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 83.03/15.90 | (set_union2(v3, v2) = v1) | ~ (set_union2(v3, v2) = v0)) % 83.03/15.90 | (38) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 83.03/15.90 | (set_intersection2(v3, v2) = v1) | ~ (set_intersection2(v3, v2) = % 83.03/15.90 | v0)) % 83.03/15.90 | (39) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 83.03/15.90 | : ! [v3: $i] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, % 83.03/15.90 | v2) = v0)) % 83.03/15.90 | (40) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 83.03/15.90 | (set_difference(v3, v2) = v1) | ~ (set_difference(v3, v2) = v0)) % 83.03/15.90 | (41) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 83.03/15.90 | : ! [v3: $i] : (v1 = v0 | ~ (disjoint(v3, v2) = v1) | ~ % 83.03/15.90 | (disjoint(v3, v2) = v0)) % 83.03/15.90 | % 83.03/15.90 | DELTA: instantiating (rc1_xboole_0) with fresh symbol all_60_0 gives: % 83.03/15.90 | (42) empty(all_60_0) = 0 & $i(all_60_0) % 83.03/15.90 | % 83.03/15.90 | ALPHA: (42) implies: % 83.03/15.90 | (43) $i(all_60_0) % 83.03/15.90 | (44) empty(all_60_0) = 0 % 83.03/15.90 | % 83.03/15.90 | DELTA: instantiating (34) with fresh symbols all_67_0, all_67_1, all_67_2, % 83.03/15.90 | all_67_3 gives: % 83.03/15.91 | (45) singleton(all_67_2) = all_67_1 & subset(all_67_3, all_67_1) = all_67_0 % 83.03/15.91 | & $i(all_67_1) & $i(all_67_2) & $i(all_67_3) & ((all_67_0 = 0 & ~ % 83.03/15.91 | (all_67_1 = all_67_3) & ~ (all_67_3 = empty_set)) | ( ~ (all_67_0 % 83.03/15.91 | = 0) & (all_67_1 = all_67_3 | all_67_3 = empty_set))) % 83.03/15.91 | % 83.03/15.91 | ALPHA: (45) implies: % 83.03/15.91 | (46) $i(all_67_3) % 83.03/15.91 | (47) $i(all_67_2) % 83.03/15.91 | (48) $i(all_67_1) % 83.03/15.91 | (49) subset(all_67_3, all_67_1) = all_67_0 % 83.03/15.91 | (50) singleton(all_67_2) = all_67_1 % 83.03/15.91 | (51) (all_67_0 = 0 & ~ (all_67_1 = all_67_3) & ~ (all_67_3 = empty_set)) % 83.03/15.91 | | ( ~ (all_67_0 = 0) & (all_67_1 = all_67_3 | all_67_3 = empty_set)) % 83.03/15.91 | % 83.03/15.91 | GROUND_INST: instantiating (9) with all_67_3, all_67_1, all_67_0, simplifying % 83.03/15.91 | with (46), (48), (49) gives: % 83.03/15.91 | (52) all_67_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & in(v0, % 83.03/15.91 | all_67_1) = v1 & in(v0, all_67_3) = 0 & $i(v0)) % 83.03/15.91 | % 83.03/15.91 | GROUND_INST: instantiating (22) with all_67_3, all_67_1, all_67_0, simplifying % 83.03/15.91 | with (46), (48), (49) gives: % 83.03/15.91 | (53) all_67_0 = 0 | ? [v0: $i] : ( ~ (v0 = empty_set) & % 83.03/15.91 | set_difference(all_67_3, all_67_1) = v0 & $i(v0)) % 83.03/15.91 | % 83.03/15.91 | GROUND_INST: instantiating (31) with all_67_2, all_67_1, simplifying with % 83.03/15.91 | (47), (50) gives: % 83.03/15.91 | (54) unordered_pair(all_67_2, all_67_2) = all_67_1 & $i(all_67_1) % 83.03/15.91 | % 83.03/15.91 | GROUND_INST: instantiating (32) with all_60_0, simplifying with (43), (44) % 83.03/15.91 | gives: % 83.03/15.91 | (55) all_60_0 = empty_set % 83.03/15.91 | % 83.03/15.91 | REDUCE: (43), (55) imply: % 83.03/15.91 | (56) $i(empty_set) % 83.03/15.91 | % 83.03/15.91 | BETA: splitting (51) gives: % 83.03/15.91 | % 83.03/15.91 | Case 1: % 83.03/15.91 | | % 83.03/15.91 | | (57) all_67_0 = 0 & ~ (all_67_1 = all_67_3) & ~ (all_67_3 = empty_set) % 83.03/15.91 | | % 83.03/15.91 | | ALPHA: (57) implies: % 83.03/15.91 | | (58) all_67_0 = 0 % 83.03/15.91 | | (59) ~ (all_67_3 = empty_set) % 83.03/15.91 | | (60) ~ (all_67_1 = all_67_3) % 83.03/15.91 | | % 83.03/15.91 | | REDUCE: (49), (58) imply: % 83.03/15.91 | | (61) subset(all_67_3, all_67_1) = 0 % 83.03/15.91 | | % 83.03/15.91 | | GROUND_INST: instantiating (3) with all_67_1, all_67_3, simplifying with % 83.03/15.91 | | (46), (48), (61) gives: % 83.03/15.91 | | (62) all_67_1 = all_67_3 | ? [v0: int] : ( ~ (v0 = 0) & subset(all_67_1, % 83.03/15.91 | | all_67_3) = v0) % 83.03/15.91 | | % 83.03/15.91 | | GROUND_INST: instantiating (21) with all_67_3, all_67_1, simplifying with % 83.03/15.91 | | (46), (48), (61) gives: % 83.03/15.91 | | (63) set_difference(all_67_3, all_67_1) = empty_set % 83.03/15.91 | | % 83.03/15.91 | | GROUND_INST: instantiating (20) with all_67_3, all_67_1, simplifying with % 83.03/15.91 | | (46), (48), (61) gives: % 83.03/15.91 | | (64) set_intersection2(all_67_3, all_67_1) = all_67_3 % 83.03/15.91 | | % 83.03/15.91 | | GROUND_INST: instantiating (19) with all_67_3, all_67_1, simplifying with % 83.03/15.91 | | (46), (48), (61) gives: % 83.03/15.91 | | (65) set_union2(all_67_3, all_67_1) = all_67_1 % 83.03/15.91 | | % 83.03/15.91 | | GROUND_INST: instantiating (27) with all_67_3, all_67_1, simplifying with % 83.03/15.91 | | (46), (48), (61) gives: % 83.03/15.91 | | (66) ? [v0: $i] : (set_difference(all_67_1, all_67_3) = v0 & % 83.03/15.91 | | set_union2(all_67_3, v0) = all_67_1 & $i(v0)) % 83.03/15.91 | | % 83.03/15.92 | | DELTA: instantiating (66) with fresh symbol all_106_0 gives: % 83.03/15.92 | | (67) set_difference(all_67_1, all_67_3) = all_106_0 & % 83.03/15.92 | | set_union2(all_67_3, all_106_0) = all_67_1 & $i(all_106_0) % 83.03/15.92 | | % 83.03/15.92 | | ALPHA: (67) implies: % 83.03/15.92 | | (68) $i(all_106_0) % 83.03/15.92 | | (69) set_union2(all_67_3, all_106_0) = all_67_1 % 83.03/15.92 | | (70) set_difference(all_67_1, all_67_3) = all_106_0 % 83.03/15.92 | | % 83.03/15.92 | | BETA: splitting (62) gives: % 83.03/15.92 | | % 83.03/15.92 | | Case 1: % 83.03/15.92 | | | % 83.03/15.92 | | | (71) all_67_1 = all_67_3 % 83.03/15.92 | | | % 83.03/15.92 | | | REDUCE: (60), (71) imply: % 83.03/15.92 | | | (72) $false % 83.03/15.92 | | | % 83.03/15.92 | | | CLOSE: (72) is inconsistent. % 83.03/15.92 | | | % 83.03/15.92 | | Case 2: % 83.03/15.92 | | | % 83.03/15.92 | | | (73) ? [v0: int] : ( ~ (v0 = 0) & subset(all_67_1, all_67_3) = v0) % 83.03/15.92 | | | % 83.03/15.92 | | | DELTA: instantiating (73) with fresh symbol all_116_0 gives: % 83.03/15.92 | | | (74) ~ (all_116_0 = 0) & subset(all_67_1, all_67_3) = all_116_0 % 83.03/15.92 | | | % 83.03/15.92 | | | ALPHA: (74) implies: % 83.03/15.92 | | | (75) ~ (all_116_0 = 0) % 83.03/15.92 | | | (76) subset(all_67_1, all_67_3) = all_116_0 % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (1) with all_67_1, all_67_3, all_67_1, % 83.03/15.92 | | | simplifying with (46), (48), (65) gives: % 83.03/15.92 | | | (77) set_union2(all_67_1, all_67_3) = all_67_1 % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (1) with all_106_0, all_67_3, all_67_1, % 83.03/15.92 | | | simplifying with (46), (68), (69) gives: % 83.03/15.92 | | | (78) set_union2(all_106_0, all_67_3) = all_67_1 & $i(all_67_1) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (25) with all_67_3, all_106_0, all_67_1, % 83.03/15.92 | | | simplifying with (46), (68), (69) gives: % 83.03/15.92 | | | (79) ? [v0: $i] : (set_difference(all_67_1, all_106_0) = v0 & % 83.03/15.92 | | | set_difference(all_67_3, all_106_0) = v0 & $i(v0)) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (23) with all_67_3, all_106_0, all_67_1, % 83.03/15.92 | | | simplifying with (46), (68), (69) gives: % 83.03/15.92 | | | (80) ? [v0: $i] : (set_difference(all_106_0, all_67_3) = v0 & % 83.03/15.92 | | | set_union2(all_67_3, v0) = all_67_1 & $i(v0) & $i(all_67_1)) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (2) with all_67_1, all_67_3, all_67_3, % 83.03/15.92 | | | simplifying with (46), (48), (64) gives: % 83.03/15.92 | | | (81) set_intersection2(all_67_1, all_67_3) = all_67_3 % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (30) with all_67_3, all_67_1, all_67_3, % 83.03/15.92 | | | simplifying with (46), (48), (64) gives: % 83.03/15.92 | | | (82) ? [v0: int] : ? [v1: $i] : ? [v2: int] : ($i(v1) & ((v2 = 0 & % 83.03/15.92 | | | in(v1, all_67_3) = 0) | (v0 = 0 & disjoint(all_67_3, % 83.03/15.92 | | | all_67_1) = 0))) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (18) with all_67_2, all_67_3, all_67_1, % 83.03/15.92 | | | all_116_0, simplifying with (46), (47), (50), (76) gives: % 83.03/15.92 | | | (83) all_116_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & in(all_67_2, % 83.03/15.92 | | | all_67_3) = v0) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (9) with all_67_1, all_67_3, all_116_0, % 83.03/15.92 | | | simplifying with (46), (48), (76) gives: % 83.03/15.92 | | | (84) all_116_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & in(v0, % 83.03/15.92 | | | all_67_1) = 0 & in(v0, all_67_3) = v1 & $i(v0)) % 83.03/15.92 | | | % 83.03/15.92 | | | GROUND_INST: instantiating (22) with all_67_1, all_67_3, all_116_0, % 83.03/15.92 | | | simplifying with (46), (48), (76) gives: % 83.03/15.93 | | | (85) all_116_0 = 0 | ? [v0: $i] : ( ~ (v0 = empty_set) & % 83.03/15.93 | | | set_difference(all_67_1, all_67_3) = v0 & $i(v0)) % 83.03/15.93 | | | % 83.03/15.93 | | | GROUND_INST: instantiating (33) with all_67_3, all_67_1, empty_set, % 83.03/15.93 | | | simplifying with (46), (48), (63) gives: % 83.03/15.93 | | | (86) all_67_3 = empty_set | ? [v0: int] : ( ~ (v0 = 0) & % 83.03/15.93 | | | disjoint(all_67_3, all_67_1) = v0) % 83.03/15.93 | | | % 83.03/15.93 | | | GROUND_INST: instantiating (24) with all_67_1, all_67_3, empty_set, % 83.03/15.93 | | | simplifying with (46), (48), (63) gives: % 83.03/15.93 | | | (87) ? [v0: $i] : (set_union2(all_67_1, all_67_3) = v0 & % 83.03/15.93 | | | set_union2(all_67_1, empty_set) = v0 & $i(v0)) % 83.03/15.93 | | | % 83.03/15.93 | | | GROUND_INST: instantiating (26) with all_67_1, all_67_3, all_106_0, % 83.03/15.93 | | | simplifying with (46), (48), (70) gives: % 83.03/15.93 | | | (88) ? [v0: $i] : (set_difference(v0, all_67_3) = all_106_0 & % 83.03/15.93 | | | set_union2(all_67_1, all_67_3) = v0 & $i(v0) & $i(all_106_0)) % 83.03/15.93 | | | % 83.03/15.93 | | | GROUND_INST: instantiating (29) with all_67_1, all_67_3, all_106_0, % 83.03/15.93 | | | simplifying with (46), (48), (70) gives: % 83.03/15.93 | | | (89) ? [v0: $i] : (set_difference(all_67_1, all_106_0) = v0 & % 83.03/15.93 | | | set_intersection2(all_67_1, all_67_3) = v0 & $i(v0)) % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (79) with fresh symbol all_124_0 gives: % 83.03/15.93 | | | (90) set_difference(all_67_1, all_106_0) = all_124_0 & % 83.03/15.93 | | | set_difference(all_67_3, all_106_0) = all_124_0 & $i(all_124_0) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (90) implies: % 83.03/15.93 | | | (91) $i(all_124_0) % 83.03/15.93 | | | (92) set_difference(all_67_1, all_106_0) = all_124_0 % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (89) with fresh symbol all_128_0 gives: % 83.03/15.93 | | | (93) set_difference(all_67_1, all_106_0) = all_128_0 & % 83.03/15.93 | | | set_intersection2(all_67_1, all_67_3) = all_128_0 & $i(all_128_0) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (93) implies: % 83.03/15.93 | | | (94) set_intersection2(all_67_1, all_67_3) = all_128_0 % 83.03/15.93 | | | (95) set_difference(all_67_1, all_106_0) = all_128_0 % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (87) with fresh symbol all_130_0 gives: % 83.03/15.93 | | | (96) set_union2(all_67_1, all_67_3) = all_130_0 & set_union2(all_67_1, % 83.03/15.93 | | | empty_set) = all_130_0 & $i(all_130_0) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (96) implies: % 83.03/15.93 | | | (97) $i(all_130_0) % 83.03/15.93 | | | (98) set_union2(all_67_1, all_67_3) = all_130_0 % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (80) with fresh symbol all_136_0 gives: % 83.03/15.93 | | | (99) set_difference(all_106_0, all_67_3) = all_136_0 & % 83.03/15.93 | | | set_union2(all_67_3, all_136_0) = all_67_1 & $i(all_136_0) & % 83.03/15.93 | | | $i(all_67_1) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (99) implies: % 83.03/15.93 | | | (100) $i(all_136_0) % 83.03/15.93 | | | (101) set_union2(all_67_3, all_136_0) = all_67_1 % 83.03/15.93 | | | (102) set_difference(all_106_0, all_67_3) = all_136_0 % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (88) with fresh symbol all_143_0 gives: % 83.03/15.93 | | | (103) set_difference(all_143_0, all_67_3) = all_106_0 & % 83.03/15.93 | | | set_union2(all_67_1, all_67_3) = all_143_0 & $i(all_143_0) & % 83.03/15.93 | | | $i(all_106_0) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (103) implies: % 83.03/15.93 | | | (104) set_union2(all_67_1, all_67_3) = all_143_0 % 83.03/15.93 | | | % 83.03/15.93 | | | DELTA: instantiating (82) with fresh symbols all_146_0, all_146_1, % 83.03/15.93 | | | all_146_2 gives: % 83.03/15.93 | | | (105) $i(all_146_1) & ((all_146_0 = 0 & in(all_146_1, all_67_3) = 0) | % 83.03/15.93 | | | (all_146_2 = 0 & disjoint(all_67_3, all_67_1) = 0)) % 83.03/15.93 | | | % 83.03/15.93 | | | ALPHA: (105) implies: % 83.03/15.93 | | | (106) $i(all_146_1) % 83.03/15.93 | | | (107) (all_146_0 = 0 & in(all_146_1, all_67_3) = 0) | (all_146_2 = 0 & % 83.03/15.93 | | | disjoint(all_67_3, all_67_1) = 0) % 83.03/15.93 | | | % 83.03/15.93 | | | BETA: splitting (85) gives: % 83.03/15.93 | | | % 83.03/15.93 | | | Case 1: % 83.03/15.93 | | | | % 83.03/15.93 | | | | (108) all_116_0 = 0 % 83.03/15.93 | | | | % 83.03/15.93 | | | | REDUCE: (75), (108) imply: % 83.03/15.93 | | | | (109) $false % 83.03/15.93 | | | | % 83.03/15.93 | | | | CLOSE: (109) is inconsistent. % 83.03/15.93 | | | | % 83.03/15.93 | | | Case 2: % 83.03/15.93 | | | | % 83.03/15.93 | | | | (110) ? [v0: $i] : ( ~ (v0 = empty_set) & set_difference(all_67_1, % 83.03/15.93 | | | | all_67_3) = v0 & $i(v0)) % 83.03/15.93 | | | | % 83.03/15.93 | | | | DELTA: instantiating (110) with fresh symbol all_152_0 gives: % 83.03/15.93 | | | | (111) ~ (all_152_0 = empty_set) & set_difference(all_67_1, all_67_3) % 83.03/15.93 | | | | = all_152_0 & $i(all_152_0) % 83.03/15.93 | | | | % 83.03/15.93 | | | | ALPHA: (111) implies: % 83.03/15.93 | | | | (112) $i(all_152_0) % 83.03/15.93 | | | | (113) set_difference(all_67_1, all_67_3) = all_152_0 % 83.03/15.93 | | | | % 83.03/15.93 | | | | BETA: splitting (86) gives: % 83.03/15.93 | | | | % 83.03/15.93 | | | | Case 1: % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | (114) all_67_3 = empty_set % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | REDUCE: (59), (114) imply: % 83.03/15.93 | | | | | (115) $false % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | CLOSE: (115) is inconsistent. % 83.03/15.93 | | | | | % 83.03/15.93 | | | | Case 2: % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | (116) ? [v0: int] : ( ~ (v0 = 0) & disjoint(all_67_3, all_67_1) = % 83.03/15.93 | | | | | v0) % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | DELTA: instantiating (116) with fresh symbol all_157_0 gives: % 83.03/15.93 | | | | | (117) ~ (all_157_0 = 0) & disjoint(all_67_3, all_67_1) = all_157_0 % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | ALPHA: (117) implies: % 83.03/15.93 | | | | | (118) ~ (all_157_0 = 0) % 83.03/15.93 | | | | | (119) disjoint(all_67_3, all_67_1) = all_157_0 % 83.03/15.93 | | | | | % 83.03/15.93 | | | | | BETA: splitting (84) gives: % 83.03/15.94 | | | | | % 83.03/15.94 | | | | | Case 1: % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | (120) all_116_0 = 0 % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | REDUCE: (75), (120) imply: % 83.03/15.94 | | | | | | (121) $false % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | CLOSE: (121) is inconsistent. % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | Case 2: % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | (122) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & in(v0, % 83.03/15.94 | | | | | | all_67_1) = 0 & in(v0, all_67_3) = v1 & $i(v0)) % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | DELTA: instantiating (122) with fresh symbols all_170_0, all_170_1 % 83.03/15.94 | | | | | | gives: % 83.03/15.94 | | | | | | (123) ~ (all_170_0 = 0) & in(all_170_1, all_67_1) = 0 & % 83.03/15.94 | | | | | | in(all_170_1, all_67_3) = all_170_0 & $i(all_170_1) % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | ALPHA: (123) implies: % 83.03/15.94 | | | | | | (124) ~ (all_170_0 = 0) % 83.03/15.94 | | | | | | (125) $i(all_170_1) % 83.03/15.94 | | | | | | (126) in(all_170_1, all_67_3) = all_170_0 % 83.03/15.94 | | | | | | (127) in(all_170_1, all_67_1) = 0 % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | BETA: splitting (83) gives: % 83.03/15.94 | | | | | | % 83.03/15.94 | | | | | | Case 1: % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | (128) all_116_0 = 0 % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | REDUCE: (75), (128) imply: % 83.03/15.94 | | | | | | | (129) $false % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | CLOSE: (129) is inconsistent. % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | Case 2: % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | (130) ? [v0: int] : ( ~ (v0 = 0) & in(all_67_2, all_67_3) = % 83.03/15.94 | | | | | | | v0) % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | DELTA: instantiating (130) with fresh symbol all_179_0 gives: % 83.03/15.94 | | | | | | | (131) ~ (all_179_0 = 0) & in(all_67_2, all_67_3) = all_179_0 % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | ALPHA: (131) implies: % 83.03/15.94 | | | | | | | (132) ~ (all_179_0 = 0) % 83.03/15.94 | | | | | | | (133) in(all_67_2, all_67_3) = all_179_0 % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | BETA: splitting (107) gives: % 83.03/15.94 | | | | | | | % 83.03/15.94 | | | | | | | Case 1: % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | (134) all_146_0 = 0 & in(all_146_1, all_67_3) = 0 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | ALPHA: (134) implies: % 83.03/15.94 | | | | | | | | (135) in(all_146_1, all_67_3) = 0 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (37) with all_130_0, all_143_0, % 83.03/15.94 | | | | | | | | all_67_3, all_67_1, simplifying with (98), (104) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (136) all_143_0 = all_130_0 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (37) with all_67_1, all_143_0, % 83.03/15.94 | | | | | | | | all_67_3, all_67_1, simplifying with (77), (104) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (137) all_143_0 = all_67_1 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (38) with all_67_3, all_128_0, % 83.03/15.94 | | | | | | | | all_67_3, all_67_1, simplifying with (81), (94) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (138) all_128_0 = all_67_3 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (40) with all_106_0, all_152_0, % 83.03/15.94 | | | | | | | | all_67_3, all_67_1, simplifying with (70), (113) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (139) all_152_0 = all_106_0 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (40) with all_124_0, all_128_0, % 83.03/15.94 | | | | | | | | all_106_0, all_67_1, simplifying with (92), (95) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (140) all_128_0 = all_124_0 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | COMBINE_EQS: (136), (137) imply: % 83.03/15.94 | | | | | | | | (141) all_130_0 = all_67_1 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | SIMP: (141) implies: % 83.03/15.94 | | | | | | | | (142) all_130_0 = all_67_1 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | COMBINE_EQS: (138), (140) imply: % 83.03/15.94 | | | | | | | | (143) all_124_0 = all_67_3 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | SIMP: (143) implies: % 83.03/15.94 | | | | | | | | (144) all_124_0 = all_67_3 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | REDUCE: (92), (144) imply: % 83.03/15.94 | | | | | | | | (145) set_difference(all_67_1, all_106_0) = all_67_3 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (17) with all_170_1, all_67_3, % 83.03/15.94 | | | | | | | | all_170_0, simplifying with (46), (125), (126) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (146) all_170_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = % 83.03/15.94 | | | | | | | | 0) & singleton(all_170_1) = v0 & subset(v0, % 83.03/15.94 | | | | | | | | all_67_3) = v1 & $i(v0)) % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (13) with all_67_1, all_67_3, % 83.03/15.94 | | | | | | | | all_106_0, all_170_1, 0, simplifying with (46), % 83.03/15.94 | | | | | | | | (48), (68), (70), (125), (127) gives: % 83.03/15.94 | | | | | | | | (147) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & % 83.03/15.94 | | | | | | | | in(all_170_1, all_67_3) = v1) | ( ~ (v0 = 0) & % 83.03/15.94 | | | | | | | | in(all_170_1, all_106_0) = v0)) % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (4) with all_67_2, all_67_1, % 83.03/15.94 | | | | | | | | all_170_1, simplifying with (47), (48), (50), % 83.03/15.94 | | | | | | | | (125), (127) gives: % 83.03/15.94 | | | | | | | | (148) all_170_1 = all_67_2 % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (16) with all_170_1, all_67_1, % 83.03/15.94 | | | | | | | | simplifying with (48), (125), (127) gives: % 83.03/15.94 | | | | | | | | (149) ? [v0: $i] : (singleton(all_170_1) = v0 & subset(v0, % 83.03/15.94 | | | | | | | | all_67_1) = 0 & $i(v0)) % 83.03/15.94 | | | | | | | | % 83.03/15.94 | | | | | | | | GROUND_INST: instantiating (1) with all_136_0, all_67_3, % 83.03/15.94 | | | | | | | | all_67_1, simplifying with (46), (100), (101) % 83.03/15.94 | | | | | | | | gives: % 83.03/15.94 | | | | | | | | (150) set_union2(all_136_0, all_67_3) = all_67_1 & % 83.03/15.94 | | | | | | | | $i(all_67_1) % 83.03/15.94 | | | | | | | | % 83.03/15.95 | | | | | | | | GROUND_INST: instantiating (11) with all_67_1, all_106_0, % 83.03/15.95 | | | | | | | | all_67_3, all_170_1, simplifying with (46), (48), % 83.03/15.95 | | | | | | | | (68), (125), (127), (145) gives: % 83.03/15.95 | | | | | | | | (151) ? [v0: int] : ? [v1: int] : ((v1 = 0 & in(all_170_1, % 83.03/15.95 | | | | | | | | all_67_3) = 0) | (v0 = 0 & in(all_170_1, % 83.03/15.95 | | | | | | | | all_106_0) = 0)) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | GROUND_INST: instantiating (13) with all_67_1, all_106_0, % 83.03/15.95 | | | | | | | | all_67_3, all_170_1, 0, simplifying with (46), % 83.03/15.95 | | | | | | | | (48), (68), (125), (127), (145) gives: % 83.03/15.95 | | | | | | | | (152) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & % 83.03/15.95 | | | | | | | | in(all_170_1, all_106_0) = v1) | ( ~ (v0 = 0) & % 83.03/15.95 | | | | | | | | in(all_170_1, all_67_3) = v0)) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | GROUND_INST: instantiating (12) with all_67_1, all_106_0, % 83.03/15.95 | | | | | | | | all_67_3, all_146_1, simplifying with (46), (48), % 83.03/15.95 | | | | | | | | (68), (106), (135), (145) gives: % 83.03/15.95 | | | | | | | | (153) ? [v0: int] : ( ~ (v0 = 0) & in(all_146_1, all_106_0) % 83.03/15.95 | | | | | | | | = v0 & in(all_146_1, all_67_1) = 0) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | GROUND_INST: instantiating (14) with all_106_0, all_67_3, % 83.03/15.95 | | | | | | | | all_136_0, all_170_1, all_170_0, simplifying with % 83.03/15.95 | | | | | | | | (46), (68), (100), (102), (125), (126) gives: % 83.03/15.95 | | | | | | | | (154) ? [v0: int] : ? [v1: int] : ((v1 = 0 & ~ (all_170_0 % 83.03/15.95 | | | | | | | | = 0) & in(all_170_1, all_106_0) = 0) | ( ~ (v0 = % 83.03/15.95 | | | | | | | | 0) & in(all_170_1, all_136_0) = v0)) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | GROUND_INST: instantiating (15) with all_106_0, all_67_3, % 83.03/15.95 | | | | | | | | all_136_0, all_67_2, all_179_0, simplifying with % 83.03/15.95 | | | | | | | | (46), (47), (68), (100), (102), (133) gives: % 83.03/15.95 | | | | | | | | (155) all_179_0 = 0 | ? [v0: int] : ? [v1: int] : ((v1 = 0 % 83.03/15.95 | | | | | | | | & in(all_67_2, all_136_0) = 0) | ( ~ (v0 = 0) & % 83.03/15.95 | | | | | | | | in(all_67_2, all_106_0) = v0)) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (149) with fresh symbol all_235_0 gives: % 83.03/15.95 | | | | | | | | (156) singleton(all_170_1) = all_235_0 & subset(all_235_0, % 83.03/15.95 | | | | | | | | all_67_1) = 0 & $i(all_235_0) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | ALPHA: (156) implies: % 83.03/15.95 | | | | | | | | (157) $i(all_235_0) % 83.03/15.95 | | | | | | | | (158) singleton(all_170_1) = all_235_0 % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (153) with fresh symbol all_263_0 gives: % 83.03/15.95 | | | | | | | | (159) ~ (all_263_0 = 0) & in(all_146_1, all_106_0) = % 83.03/15.95 | | | | | | | | all_263_0 & in(all_146_1, all_67_1) = 0 % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | ALPHA: (159) implies: % 83.03/15.95 | | | | | | | | (160) in(all_146_1, all_67_1) = 0 % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (147) with fresh symbols all_271_0, % 83.03/15.95 | | | | | | | | all_271_1 gives: % 83.03/15.95 | | | | | | | | (161) ( ~ (all_271_0 = 0) & in(all_170_1, all_67_3) = % 83.03/15.95 | | | | | | | | all_271_0) | ( ~ (all_271_1 = 0) & in(all_170_1, % 83.03/15.95 | | | | | | | | all_106_0) = all_271_1) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (152) with fresh symbols all_278_0, % 83.03/15.95 | | | | | | | | all_278_1 gives: % 83.03/15.95 | | | | | | | | (162) ( ~ (all_278_0 = 0) & in(all_170_1, all_106_0) = % 83.03/15.95 | | | | | | | | all_278_0) | ( ~ (all_278_1 = 0) & in(all_170_1, % 83.03/15.95 | | | | | | | | all_67_3) = all_278_1) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (151) with fresh symbols all_291_0, % 83.03/15.95 | | | | | | | | all_291_1 gives: % 83.03/15.95 | | | | | | | | (163) (all_291_0 = 0 & in(all_170_1, all_67_3) = 0) | % 83.03/15.95 | | | | | | | | (all_291_1 = 0 & in(all_170_1, all_106_0) = 0) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | DELTA: instantiating (154) with fresh symbols all_295_0, % 83.03/15.95 | | | | | | | | all_295_1 gives: % 83.03/15.95 | | | | | | | | (164) (all_295_0 = 0 & ~ (all_170_0 = 0) & in(all_170_1, % 83.03/15.95 | | | | | | | | all_106_0) = 0) | ( ~ (all_295_1 = 0) & % 83.03/15.95 | | | | | | | | in(all_170_1, all_136_0) = all_295_1) % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | REDUCE: (148), (158) imply: % 83.03/15.95 | | | | | | | | (165) singleton(all_67_2) = all_235_0 % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | REDUCE: (126), (148) imply: % 83.03/15.95 | | | | | | | | (166) in(all_67_2, all_67_3) = all_170_0 % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | BETA: splitting (146) gives: % 83.03/15.95 | | | | | | | | % 83.03/15.95 | | | | | | | | Case 1: % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | (167) all_170_0 = 0 % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | REDUCE: (124), (167) imply: % 83.03/15.95 | | | | | | | | | (168) $false % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | CLOSE: (168) is inconsistent. % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | Case 2: % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | (169) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 83.03/15.95 | | | | | | | | | singleton(all_170_1) = v0 & subset(v0, all_67_3) = % 83.03/15.95 | | | | | | | | | v1 & $i(v0)) % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | DELTA: instantiating (169) with fresh symbols all_379_0, % 83.03/15.95 | | | | | | | | | all_379_1 gives: % 83.03/15.95 | | | | | | | | | (170) ~ (all_379_0 = 0) & singleton(all_170_1) = all_379_1 % 83.03/15.95 | | | | | | | | | & subset(all_379_1, all_67_3) = all_379_0 & % 83.03/15.95 | | | | | | | | | $i(all_379_1) % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | ALPHA: (170) implies: % 83.03/15.95 | | | | | | | | | (171) singleton(all_170_1) = all_379_1 % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | REDUCE: (148), (171) imply: % 83.03/15.95 | | | | | | | | | (172) singleton(all_67_2) = all_379_1 % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | BETA: splitting (155) gives: % 83.03/15.95 | | | | | | | | | % 83.03/15.95 | | | | | | | | | Case 1: % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | (173) all_179_0 = 0 % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | REDUCE: (132), (173) imply: % 83.03/15.95 | | | | | | | | | | (174) $false % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | CLOSE: (174) is inconsistent. % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | Case 2: % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | (175) ? [v0: int] : ? [v1: int] : ((v1 = 0 & % 83.03/15.95 | | | | | | | | | | in(all_67_2, all_136_0) = 0) | ( ~ (v0 = 0) & % 83.03/15.95 | | | | | | | | | | in(all_67_2, all_106_0) = v0)) % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | DELTA: instantiating (175) with fresh symbols all_398_0, % 83.03/15.95 | | | | | | | | | | all_398_1 gives: % 83.03/15.95 | | | | | | | | | | (176) (all_398_0 = 0 & in(all_67_2, all_136_0) = 0) | ( ~ % 83.03/15.95 | | | | | | | | | | (all_398_1 = 0) & in(all_67_2, all_106_0) = % 83.03/15.95 | | | | | | | | | | all_398_1) % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | BETA: splitting (163) gives: % 83.03/15.95 | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | Case 1: % 83.03/15.95 | | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | | (177) all_291_0 = 0 & in(all_170_1, all_67_3) = 0 % 83.03/15.95 | | | | | | | | | | | % 83.03/15.95 | | | | | | | | | | | ALPHA: (177) implies: % 83.03/15.95 | | | | | | | | | | | (178) in(all_170_1, all_67_3) = 0 % 83.03/15.95 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | REDUCE: (148), (178) imply: % 83.03/15.96 | | | | | | | | | | | (179) in(all_67_2, all_67_3) = 0 % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | REF_CLOSE: (36), (124), (133), (166), (179) are inconsistent % 83.03/15.96 | | | | | | | | | | | by sub-proof #1. % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | Case 2: % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | (180) all_291_1 = 0 & in(all_170_1, all_106_0) = 0 % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | ALPHA: (180) implies: % 83.03/15.96 | | | | | | | | | | | (181) in(all_170_1, all_106_0) = 0 % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | REDUCE: (148), (181) imply: % 83.03/15.96 | | | | | | | | | | | (182) in(all_67_2, all_106_0) = 0 % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | BETA: splitting (176) gives: % 83.03/15.96 | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | Case 1: % 83.03/15.96 | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | (183) all_398_0 = 0 & in(all_67_2, all_136_0) = 0 % 83.03/15.96 | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | ALPHA: (183) implies: % 83.03/15.96 | | | | | | | | | | | | (184) in(all_67_2, all_136_0) = 0 % 83.03/15.96 | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | BETA: splitting (161) gives: % 83.03/15.96 | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | Case 1: % 83.03/15.96 | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | (185) ~ (all_271_0 = 0) & in(all_170_1, all_67_3) = % 83.03/15.96 | | | | | | | | | | | | | all_271_0 % 83.03/15.96 | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | ALPHA: (185) implies: % 83.03/15.96 | | | | | | | | | | | | | (186) in(all_170_1, all_67_3) = all_271_0 % 83.03/15.96 | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | REDUCE: (148), (186) imply: % 83.03/15.96 | | | | | | | | | | | | | (187) in(all_67_2, all_67_3) = all_271_0 % 83.03/15.96 | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | BETA: splitting (162) gives: % 83.03/15.96 | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | Case 1: % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | (188) ~ (all_278_0 = 0) & in(all_170_1, all_106_0) = % 83.03/15.96 | | | | | | | | | | | | | | all_278_0 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | ALPHA: (188) implies: % 83.03/15.96 | | | | | | | | | | | | | | (189) ~ (all_278_0 = 0) % 83.03/15.96 | | | | | | | | | | | | | | (190) in(all_170_1, all_106_0) = all_278_0 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | REDUCE: (148), (190) imply: % 83.03/15.96 | | | | | | | | | | | | | | (191) in(all_67_2, all_106_0) = all_278_0 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_278_0, all_106_0, % 83.03/15.96 | | | | | | | | | | | | | | all_67_2, simplifying with (182), (191) gives: % 83.03/15.96 | | | | | | | | | | | | | | (192) all_278_0 = 0 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | REDUCE: (189), (192) imply: % 83.03/15.96 | | | | | | | | | | | | | | (193) $false % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | CLOSE: (193) is inconsistent. % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | Case 2: % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | (194) ~ (all_278_1 = 0) & in(all_170_1, all_67_3) = % 83.03/15.96 | | | | | | | | | | | | | | all_278_1 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | ALPHA: (194) implies: % 83.03/15.96 | | | | | | | | | | | | | | (195) in(all_170_1, all_67_3) = all_278_1 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | REDUCE: (148), (195) imply: % 83.03/15.96 | | | | | | | | | | | | | | (196) in(all_67_2, all_67_3) = all_278_1 % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | BETA: splitting (164) gives: % 83.03/15.96 | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | Case 1: % 83.03/15.96 | | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | | % 83.03/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_170_0, all_271_0, % 83.03/15.96 | | | | | | | | | | | | | | | all_67_3, all_67_2, simplifying with (166), (187) % 83.03/15.96 | | | | | | | | | | | | | | | gives: % 83.36/15.96 | | | | | | | | | | | | | | | (197) all_271_0 = all_170_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_179_0, all_278_1, % 83.36/15.96 | | | | | | | | | | | | | | | all_67_3, all_67_2, simplifying with (133), (196) % 83.36/15.96 | | | | | | | | | | | | | | | gives: % 83.36/15.96 | | | | | | | | | | | | | | | (198) all_278_1 = all_179_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_271_0, all_278_1, % 83.36/15.96 | | | | | | | | | | | | | | | all_67_3, all_67_2, simplifying with (187), (196) % 83.36/15.96 | | | | | | | | | | | | | | | gives: % 83.36/15.96 | | | | | | | | | | | | | | | (199) all_278_1 = all_271_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (35) with all_67_1, all_379_1, % 83.36/15.96 | | | | | | | | | | | | | | | all_67_2, simplifying with (50), (172) gives: % 83.36/15.96 | | | | | | | | | | | | | | | (200) all_379_1 = all_67_1 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (35) with all_235_0, all_379_1, % 83.36/15.96 | | | | | | | | | | | | | | | all_67_2, simplifying with (165), (172) gives: % 83.36/15.96 | | | | | | | | | | | | | | | (201) all_379_1 = all_235_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | COMBINE_EQS: (200), (201) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (202) all_235_0 = all_67_1 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | COMBINE_EQS: (198), (199) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (203) all_271_0 = all_179_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | SIMP: (203) implies: % 83.36/15.96 | | | | | | | | | | | | | | | (204) all_271_0 = all_179_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | COMBINE_EQS: (197), (204) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (205) all_179_0 = all_170_0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_67_2, all_67_1, % 83.36/15.96 | | | | | | | | | | | | | | | all_146_1, simplifying with (47), (48), (50), % 83.36/15.96 | | | | | | | | | | | | | | | (106), (160) gives: % 83.36/15.96 | | | | | | | | | | | | | | | (206) all_146_1 = all_67_2 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | REDUCE: (135), (206) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (207) in(all_67_2, all_67_3) = 0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | REF_CLOSE: (36), (124), (133), (166), (207) are inconsistent % 83.36/15.96 | | | | | | | | | | | | | | | by sub-proof #1. % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | Case 2: % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | (208) ~ (all_295_1 = 0) & in(all_170_1, all_136_0) = % 83.36/15.96 | | | | | | | | | | | | | | | all_295_1 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | ALPHA: (208) implies: % 83.36/15.96 | | | | | | | | | | | | | | | (209) ~ (all_295_1 = 0) % 83.36/15.96 | | | | | | | | | | | | | | | (210) in(all_170_1, all_136_0) = all_295_1 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | REDUCE: (148), (210) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (211) in(all_67_2, all_136_0) = all_295_1 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_295_1, all_136_0, % 83.36/15.96 | | | | | | | | | | | | | | | all_67_2, simplifying with (184), (211) gives: % 83.36/15.96 | | | | | | | | | | | | | | | (212) all_295_1 = 0 % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | REDUCE: (209), (212) imply: % 83.36/15.96 | | | | | | | | | | | | | | | (213) $false % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | | CLOSE: (213) is inconsistent. % 83.36/15.96 | | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | | End of split % 83.36/15.96 | | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | | End of split % 83.36/15.96 | | | | | | | | | | | | | % 83.36/15.96 | | | | | | | | | | | | Case 2: % 83.36/15.96 | | | | | | | | | | | | | % 83.38/15.96 | | | | | | | | | | | | | (214) ~ (all_271_1 = 0) & in(all_170_1, all_106_0) = % 83.38/15.96 | | | | | | | | | | | | | all_271_1 % 83.38/15.96 | | | | | | | | | | | | | % 83.38/15.96 | | | | | | | | | | | | | ALPHA: (214) implies: % 83.38/15.96 | | | | | | | | | | | | | (215) ~ (all_271_1 = 0) % 83.38/15.97 | | | | | | | | | | | | | (216) in(all_170_1, all_106_0) = all_271_1 % 83.38/15.97 | | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | | REDUCE: (148), (216) imply: % 83.38/15.97 | | | | | | | | | | | | | (217) in(all_67_2, all_106_0) = all_271_1 % 83.38/15.97 | | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_271_1, all_106_0, % 83.38/15.97 | | | | | | | | | | | | | all_67_2, simplifying with (182), (217) gives: % 83.38/15.97 | | | | | | | | | | | | | (218) all_271_1 = 0 % 83.38/15.97 | | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | | REDUCE: (215), (218) imply: % 83.38/15.97 | | | | | | | | | | | | | (219) $false % 83.38/15.97 | | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | | CLOSE: (219) is inconsistent. % 83.38/15.97 | | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | End of split % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | Case 2: % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | (220) ~ (all_398_1 = 0) & in(all_67_2, all_106_0) = % 83.38/15.97 | | | | | | | | | | | | all_398_1 % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | ALPHA: (220) implies: % 83.38/15.97 | | | | | | | | | | | | (221) ~ (all_398_1 = 0) % 83.38/15.97 | | | | | | | | | | | | (222) in(all_67_2, all_106_0) = all_398_1 % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_398_1, all_106_0, % 83.38/15.97 | | | | | | | | | | | | all_67_2, simplifying with (182), (222) gives: % 83.38/15.97 | | | | | | | | | | | | (223) all_398_1 = 0 % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | REDUCE: (221), (223) imply: % 83.38/15.97 | | | | | | | | | | | | (224) $false % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | | CLOSE: (224) is inconsistent. % 83.38/15.97 | | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | | End of split % 83.38/15.97 | | | | | | | | | | | % 83.38/15.97 | | | | | | | | | | End of split % 83.38/15.97 | | | | | | | | | | % 83.38/15.97 | | | | | | | | | End of split % 83.38/15.97 | | | | | | | | | % 83.38/15.97 | | | | | | | | End of split % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | Case 2: % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | | (225) all_146_2 = 0 & disjoint(all_67_3, all_67_1) = 0 % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | | ALPHA: (225) implies: % 83.38/15.97 | | | | | | | | (226) disjoint(all_67_3, all_67_1) = 0 % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | | GROUND_INST: instantiating (41) with 0, all_157_0, all_67_1, % 83.38/15.97 | | | | | | | | all_67_3, simplifying with (119), (226) gives: % 83.38/15.97 | | | | | | | | (227) all_157_0 = 0 % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | | REDUCE: (118), (227) imply: % 83.38/15.97 | | | | | | | | (228) $false % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | | CLOSE: (228) is inconsistent. % 83.38/15.97 | | | | | | | | % 83.38/15.97 | | | | | | | End of split % 83.38/15.97 | | | | | | | % 83.38/15.97 | | | | | | End of split % 83.38/15.97 | | | | | | % 83.38/15.97 | | | | | End of split % 83.38/15.97 | | | | | % 83.38/15.97 | | | | End of split % 83.38/15.97 | | | | % 83.38/15.97 | | | End of split % 83.38/15.97 | | | % 83.38/15.97 | | End of split % 83.38/15.97 | | % 83.38/15.97 | Case 2: % 83.38/15.97 | | % 83.38/15.97 | | (229) ~ (all_67_0 = 0) & (all_67_1 = all_67_3 | all_67_3 = empty_set) % 83.38/15.97 | | % 83.38/15.97 | | ALPHA: (229) implies: % 83.38/15.97 | | (230) ~ (all_67_0 = 0) % 83.38/15.97 | | (231) all_67_1 = all_67_3 | all_67_3 = empty_set % 83.38/15.97 | | % 83.38/15.97 | | BETA: splitting (53) gives: % 83.38/15.97 | | % 83.38/15.97 | | Case 1: % 83.38/15.97 | | | % 83.38/15.97 | | | (232) all_67_0 = 0 % 83.38/15.97 | | | % 83.38/15.97 | | | REDUCE: (230), (232) imply: % 83.38/15.97 | | | (233) $false % 83.38/15.97 | | | % 83.38/15.97 | | | CLOSE: (233) is inconsistent. % 83.38/15.97 | | | % 83.38/15.97 | | Case 2: % 83.38/15.97 | | | % 83.38/15.97 | | | (234) ? [v0: $i] : ( ~ (v0 = empty_set) & set_difference(all_67_3, % 83.38/15.97 | | | all_67_1) = v0 & $i(v0)) % 83.38/15.97 | | | % 83.38/15.97 | | | DELTA: instantiating (234) with fresh symbol all_102_0 gives: % 83.38/15.97 | | | (235) ~ (all_102_0 = empty_set) & set_difference(all_67_3, all_67_1) = % 83.38/15.97 | | | all_102_0 & $i(all_102_0) % 83.38/15.97 | | | % 83.38/15.97 | | | ALPHA: (235) implies: % 83.38/15.97 | | | (236) $i(all_102_0) % 83.38/15.97 | | | (237) set_difference(all_67_3, all_67_1) = all_102_0 % 83.38/15.97 | | | % 83.38/15.97 | | | BETA: splitting (52) gives: % 83.38/15.97 | | | % 83.38/15.97 | | | Case 1: % 83.38/15.97 | | | | % 83.38/15.97 | | | | (238) all_67_0 = 0 % 83.38/15.97 | | | | % 83.38/15.97 | | | | REDUCE: (230), (238) imply: % 83.38/15.97 | | | | (239) $false % 83.38/15.97 | | | | % 83.38/15.97 | | | | CLOSE: (239) is inconsistent. % 83.38/15.97 | | | | % 83.38/15.97 | | | Case 2: % 83.38/15.97 | | | | % 83.38/15.97 | | | | (240) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & in(v0, all_67_1) = % 83.38/15.97 | | | | v1 & in(v0, all_67_3) = 0 & $i(v0)) % 83.38/15.97 | | | | % 83.38/15.97 | | | | DELTA: instantiating (240) with fresh symbols all_107_0, all_107_1 % 83.38/15.97 | | | | gives: % 83.38/15.97 | | | | (241) ~ (all_107_0 = 0) & in(all_107_1, all_67_1) = all_107_0 & % 83.38/15.97 | | | | in(all_107_1, all_67_3) = 0 & $i(all_107_1) % 83.38/15.97 | | | | % 83.38/15.97 | | | | ALPHA: (241) implies: % 83.38/15.97 | | | | (242) ~ (all_107_0 = 0) % 83.38/15.97 | | | | (243) $i(all_107_1) % 83.38/15.97 | | | | (244) in(all_107_1, all_67_3) = 0 % 83.38/15.97 | | | | (245) in(all_107_1, all_67_1) = all_107_0 % 83.38/15.97 | | | | % 83.38/15.97 | | | | GROUND_INST: instantiating (16) with all_107_1, all_67_3, simplifying % 83.38/15.97 | | | | with (46), (243), (244) gives: % 83.38/15.97 | | | | (246) ? [v0: $i] : (singleton(all_107_1) = v0 & subset(v0, all_67_3) % 83.38/15.97 | | | | = 0 & $i(v0)) % 83.38/15.97 | | | | % 83.38/15.97 | | | | GROUND_INST: instantiating (17) with all_107_1, all_67_1, all_107_0, % 83.38/15.97 | | | | simplifying with (48), (243), (245) gives: % 83.38/15.97 | | | | (247) all_107_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 83.38/15.97 | | | | singleton(all_107_1) = v0 & subset(v0, all_67_1) = v1 & % 83.38/15.97 | | | | $i(v0)) % 83.38/15.97 | | | | % 83.38/15.97 | | | | GROUND_INST: instantiating (11) with all_67_3, all_67_1, all_102_0, % 83.38/15.97 | | | | all_107_1, simplifying with (46), (48), (236), (237), % 83.38/15.97 | | | | (243), (244) gives: % 83.38/15.97 | | | | (248) ? [v0: int] : ? [v1: int] : ((v1 = 0 & in(all_107_1, % 83.38/15.97 | | | | all_102_0) = 0) | (v0 = 0 & in(all_107_1, all_67_1) = 0)) % 83.38/15.97 | | | | % 83.38/15.97 | | | | GROUND_INST: instantiating (13) with all_67_3, all_67_1, all_102_0, % 83.38/15.97 | | | | all_107_1, 0, simplifying with (46), (48), (236), (237), % 83.38/15.97 | | | | (243), (244) gives: % 83.38/15.97 | | | | (249) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & in(all_107_1, % 83.38/15.97 | | | | all_67_1) = v1) | ( ~ (v0 = 0) & in(all_107_1, all_102_0) % 83.38/15.97 | | | | = v0)) % 83.38/15.97 | | | | % 83.38/15.97 | | | | GROUND_INST: instantiating (24) with all_67_1, all_67_3, all_102_0, % 83.38/15.97 | | | | simplifying with (46), (48), (237) gives: % 83.38/15.97 | | | | (250) ? [v0: $i] : (set_union2(all_67_1, all_102_0) = v0 & % 83.38/15.98 | | | | set_union2(all_67_1, all_67_3) = v0 & $i(v0)) % 83.38/15.98 | | | | % 83.38/15.98 | | | | GROUND_INST: instantiating (t36_xboole_1) with all_67_3, all_67_1, % 83.38/15.98 | | | | all_102_0, simplifying with (46), (48), (237) gives: % 83.38/15.98 | | | | (251) subset(all_102_0, all_67_3) = 0 % 83.38/15.98 | | | | % 83.38/15.98 | | | | GROUND_INST: instantiating (26) with all_67_3, all_67_1, all_102_0, % 83.38/15.98 | | | | simplifying with (46), (48), (237) gives: % 83.38/15.98 | | | | (252) ? [v0: $i] : (set_difference(v0, all_67_1) = all_102_0 & % 83.38/15.98 | | | | set_union2(all_67_3, all_67_1) = v0 & $i(v0) & $i(all_102_0)) % 83.38/15.98 | | | | % 83.38/15.98 | | | | GROUND_INST: instantiating (29) with all_67_3, all_67_1, all_102_0, % 83.38/15.98 | | | | simplifying with (46), (48), (237) gives: % 83.38/15.98 | | | | (253) ? [v0: $i] : (set_difference(all_67_3, all_102_0) = v0 & % 83.38/15.98 | | | | set_intersection2(all_67_3, all_67_1) = v0 & $i(v0)) % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (250) with fresh symbol all_124_0 gives: % 83.38/15.98 | | | | (254) set_union2(all_67_1, all_102_0) = all_124_0 & % 83.38/15.98 | | | | set_union2(all_67_1, all_67_3) = all_124_0 & $i(all_124_0) % 83.38/15.98 | | | | % 83.38/15.98 | | | | ALPHA: (254) implies: % 83.38/15.98 | | | | (255) set_union2(all_67_1, all_67_3) = all_124_0 % 83.38/15.98 | | | | (256) set_union2(all_67_1, all_102_0) = all_124_0 % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (246) with fresh symbol all_126_0 gives: % 83.38/15.98 | | | | (257) singleton(all_107_1) = all_126_0 & subset(all_126_0, all_67_3) % 83.38/15.98 | | | | = 0 & $i(all_126_0) % 83.38/15.98 | | | | % 83.38/15.98 | | | | ALPHA: (257) implies: % 83.38/15.98 | | | | (258) subset(all_126_0, all_67_3) = 0 % 83.38/15.98 | | | | (259) singleton(all_107_1) = all_126_0 % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (253) with fresh symbol all_128_0 gives: % 83.38/15.98 | | | | (260) set_difference(all_67_3, all_102_0) = all_128_0 & % 83.38/15.98 | | | | set_intersection2(all_67_3, all_67_1) = all_128_0 & % 83.38/15.98 | | | | $i(all_128_0) % 83.38/15.98 | | | | % 83.38/15.98 | | | | ALPHA: (260) implies: % 83.38/15.98 | | | | (261) set_difference(all_67_3, all_102_0) = all_128_0 % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (252) with fresh symbol all_130_0 gives: % 83.38/15.98 | | | | (262) set_difference(all_130_0, all_67_1) = all_102_0 & % 83.38/15.98 | | | | set_union2(all_67_3, all_67_1) = all_130_0 & $i(all_130_0) & % 83.38/15.98 | | | | $i(all_102_0) % 83.38/15.98 | | | | % 83.38/15.98 | | | | ALPHA: (262) implies: % 83.38/15.98 | | | | (263) set_union2(all_67_3, all_67_1) = all_130_0 % 83.38/15.98 | | | | (264) set_difference(all_130_0, all_67_1) = all_102_0 % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (249) with fresh symbols all_133_0, all_133_1 % 83.38/15.98 | | | | gives: % 83.38/15.98 | | | | (265) ( ~ (all_133_0 = 0) & in(all_107_1, all_67_1) = all_133_0) | ( % 83.38/15.98 | | | | ~ (all_133_1 = 0) & in(all_107_1, all_102_0) = all_133_1) % 83.38/15.98 | | | | % 83.38/15.98 | | | | DELTA: instantiating (248) with fresh symbols all_134_0, all_134_1 % 83.38/15.98 | | | | gives: % 83.38/15.98 | | | | (266) (all_134_0 = 0 & in(all_107_1, all_102_0) = 0) | (all_134_1 = 0 % 83.38/15.98 | | | | & in(all_107_1, all_67_1) = 0) % 83.38/15.98 | | | | % 83.38/15.98 | | | | BETA: splitting (247) gives: % 83.38/15.98 | | | | % 83.38/15.98 | | | | Case 1: % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | (267) all_107_0 = 0 % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | REDUCE: (242), (267) imply: % 83.38/15.98 | | | | | (268) $false % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | CLOSE: (268) is inconsistent. % 83.38/15.98 | | | | | % 83.38/15.98 | | | | Case 2: % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | (269) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 83.38/15.98 | | | | | singleton(all_107_1) = v0 & subset(v0, all_67_1) = v1 & % 83.38/15.98 | | | | | $i(v0)) % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | DELTA: instantiating (269) with fresh symbols all_144_0, all_144_1 % 83.38/15.98 | | | | | gives: % 83.38/15.98 | | | | | (270) ~ (all_144_0 = 0) & singleton(all_107_1) = all_144_1 & % 83.38/15.98 | | | | | subset(all_144_1, all_67_1) = all_144_0 & $i(all_144_1) % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | ALPHA: (270) implies: % 83.38/15.98 | | | | | (271) ~ (all_144_0 = 0) % 83.38/15.98 | | | | | (272) $i(all_144_1) % 83.38/15.98 | | | | | (273) subset(all_144_1, all_67_1) = all_144_0 % 83.38/15.98 | | | | | (274) singleton(all_107_1) = all_144_1 % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | BETA: splitting (266) gives: % 83.38/15.98 | | | | | % 83.38/15.98 | | | | | Case 1: % 83.38/15.98 | | | | | | % 83.38/15.98 | | | | | | (275) all_134_0 = 0 & in(all_107_1, all_102_0) = 0 % 83.38/15.98 | | | | | | % 83.38/15.98 | | | | | | ALPHA: (275) implies: % 83.38/15.98 | | | | | | (276) in(all_107_1, all_102_0) = 0 % 83.38/15.98 | | | | | | % 83.38/15.98 | | | | | | BETA: splitting (265) gives: % 83.38/15.98 | | | | | | % 83.38/15.98 | | | | | | Case 1: % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (35) with all_126_0, all_144_1, % 83.38/15.98 | | | | | | | all_107_1, simplifying with (259), (274) gives: % 83.38/15.98 | | | | | | | (277) all_144_1 = all_126_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | REDUCE: (273), (277) imply: % 83.38/15.98 | | | | | | | (278) subset(all_126_0, all_67_1) = all_144_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | REDUCE: (272), (277) imply: % 83.38/15.98 | | | | | | | (279) $i(all_126_0) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (16) with all_107_1, all_102_0, % 83.38/15.98 | | | | | | | simplifying with (236), (243), (276) gives: % 83.38/15.98 | | | | | | | (280) ? [v0: $i] : (singleton(all_107_1) = v0 & subset(v0, % 83.38/15.98 | | | | | | | all_102_0) = 0 & $i(v0)) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (1) with all_67_1, all_67_3, all_130_0, % 83.38/15.98 | | | | | | | simplifying with (46), (48), (263) gives: % 83.38/15.98 | | | | | | | (281) set_union2(all_67_1, all_67_3) = all_130_0 & % 83.38/15.98 | | | | | | | $i(all_130_0) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | ALPHA: (281) implies: % 83.38/15.98 | | | | | | | (282) $i(all_130_0) % 83.38/15.98 | | | | | | | (283) set_union2(all_67_1, all_67_3) = all_130_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (1) with all_102_0, all_67_1, % 83.38/15.98 | | | | | | | all_124_0, simplifying with (48), (236), (256) gives: % 83.38/15.98 | | | | | | | (284) set_union2(all_102_0, all_67_1) = all_124_0 & % 83.38/15.98 | | | | | | | $i(all_124_0) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | ALPHA: (284) implies: % 83.38/15.98 | | | | | | | (285) set_union2(all_102_0, all_67_1) = all_124_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (t7_xboole_1) with all_67_1, all_102_0, % 83.38/15.98 | | | | | | | all_124_0, simplifying with (48), (236), (256) gives: % 83.38/15.98 | | | | | | | (286) subset(all_67_1, all_124_0) = 0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (25) with all_67_1, all_102_0, % 83.38/15.98 | | | | | | | all_124_0, simplifying with (48), (236), (256) gives: % 83.38/15.98 | | | | | | | (287) ? [v0: $i] : (set_difference(all_124_0, all_102_0) = v0 % 83.38/15.98 | | | | | | | & set_difference(all_67_1, all_102_0) = v0 & $i(v0)) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (23) with all_67_1, all_102_0, % 83.38/15.98 | | | | | | | all_124_0, simplifying with (48), (236), (256) gives: % 83.38/15.98 | | | | | | | (288) ? [v0: $i] : (set_difference(all_102_0, all_67_1) = v0 & % 83.38/15.98 | | | | | | | set_union2(all_67_1, v0) = all_124_0 & $i(v0) & % 83.38/15.98 | | | | | | | $i(all_124_0)) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (21) with all_102_0, all_67_3, % 83.38/15.98 | | | | | | | simplifying with (46), (236), (251) gives: % 83.38/15.98 | | | | | | | (289) set_difference(all_102_0, all_67_3) = empty_set % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (21) with all_126_0, all_67_3, % 83.38/15.98 | | | | | | | simplifying with (46), (258), (279) gives: % 83.38/15.98 | | | | | | | (290) set_difference(all_126_0, all_67_3) = empty_set % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (20) with all_126_0, all_67_3, % 83.38/15.98 | | | | | | | simplifying with (46), (258), (279) gives: % 83.38/15.98 | | | | | | | (291) set_intersection2(all_126_0, all_67_3) = all_126_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (27) with all_126_0, all_67_3, % 83.38/15.98 | | | | | | | simplifying with (46), (258), (279) gives: % 83.38/15.98 | | | | | | | (292) ? [v0: $i] : (set_difference(all_67_3, all_126_0) = v0 & % 83.38/15.98 | | | | | | | set_union2(all_126_0, v0) = all_67_3 & $i(v0)) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (9) with all_126_0, all_67_1, % 83.38/15.98 | | | | | | | all_144_0, simplifying with (48), (278), (279) gives: % 83.38/15.98 | | | | | | | (293) all_144_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) % 83.38/15.98 | | | | | | | & in(v0, all_126_0) = 0 & in(v0, all_67_1) = v1 & % 83.38/15.98 | | | | | | | $i(v0)) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (31) with all_107_1, all_126_0, % 83.38/15.98 | | | | | | | simplifying with (243), (259) gives: % 83.38/15.98 | | | | | | | (294) unordered_pair(all_107_1, all_107_1) = all_126_0 & % 83.38/15.98 | | | | | | | $i(all_126_0) % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | ALPHA: (294) implies: % 83.38/15.98 | | | | | | | (295) unordered_pair(all_107_1, all_107_1) = all_126_0 % 83.38/15.98 | | | | | | | % 83.38/15.98 | | | | | | | GROUND_INST: instantiating (28) with all_102_0, all_67_3, % 83.38/15.98 | | | | | | | all_128_0, simplifying with (46), (236), (261) gives: % 83.38/15.99 | | | | | | | (296) ? [v0: int] : ? [v1: int] : ((v1 = all_67_3 & % 83.38/15.99 | | | | | | | set_union2(all_102_0, all_128_0) = all_67_3) | ( ~ % 83.38/15.99 | | | | | | | (v0 = 0) & subset(all_102_0, all_67_3) = v0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | GROUND_INST: instantiating (24) with all_102_0, all_67_3, % 83.38/15.99 | | | | | | | all_128_0, simplifying with (46), (236), (261) gives: % 83.38/15.99 | | | | | | | (297) ? [v0: $i] : (set_union2(all_102_0, all_128_0) = v0 & % 83.38/15.99 | | | | | | | set_union2(all_102_0, all_67_3) = v0 & $i(v0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | GROUND_INST: instantiating (26) with all_67_3, all_102_0, % 83.38/15.99 | | | | | | | all_128_0, simplifying with (46), (236), (261) gives: % 83.38/15.99 | | | | | | | (298) ? [v0: $i] : (set_difference(v0, all_102_0) = all_128_0 % 83.38/15.99 | | | | | | | & set_union2(all_67_3, all_102_0) = v0 & $i(v0) & % 83.38/15.99 | | | | | | | $i(all_128_0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | GROUND_INST: instantiating (28) with all_67_1, all_130_0, % 83.38/15.99 | | | | | | | all_102_0, simplifying with (48), (264), (282) gives: % 83.38/15.99 | | | | | | | (299) ? [v0: int] : ? [v1: int] : ((v1 = all_130_0 & % 83.38/15.99 | | | | | | | set_union2(all_67_1, all_102_0) = all_130_0) | ( ~ % 83.38/15.99 | | | | | | | (v0 = 0) & subset(all_67_1, all_130_0) = v0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | GROUND_INST: instantiating (26) with all_130_0, all_67_1, % 83.38/15.99 | | | | | | | all_102_0, simplifying with (48), (264), (282) gives: % 83.38/15.99 | | | | | | | (300) ? [v0: $i] : (set_difference(v0, all_67_1) = all_102_0 & % 83.38/15.99 | | | | | | | set_union2(all_130_0, all_67_1) = v0 & $i(v0) & % 83.38/15.99 | | | | | | | $i(all_102_0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | GROUND_INST: instantiating (29) with all_130_0, all_67_1, % 83.38/15.99 | | | | | | | all_102_0, simplifying with (48), (264), (282) gives: % 83.38/15.99 | | | | | | | (301) ? [v0: $i] : (set_difference(all_130_0, all_102_0) = v0 % 83.38/15.99 | | | | | | | & set_intersection2(all_130_0, all_67_1) = v0 & $i(v0)) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (287) with fresh symbol all_182_0 gives: % 83.38/15.99 | | | | | | | (302) set_difference(all_124_0, all_102_0) = all_182_0 & % 83.38/15.99 | | | | | | | set_difference(all_67_1, all_102_0) = all_182_0 & % 83.38/15.99 | | | | | | | $i(all_182_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (302) implies: % 83.38/15.99 | | | | | | | (303) set_difference(all_67_1, all_102_0) = all_182_0 % 83.38/15.99 | | | | | | | (304) set_difference(all_124_0, all_102_0) = all_182_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (280) with fresh symbol all_184_0 gives: % 83.38/15.99 | | | | | | | (305) singleton(all_107_1) = all_184_0 & subset(all_184_0, % 83.38/15.99 | | | | | | | all_102_0) = 0 & $i(all_184_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (305) implies: % 83.38/15.99 | | | | | | | (306) $i(all_184_0) % 83.38/15.99 | | | | | | | (307) subset(all_184_0, all_102_0) = 0 % 83.38/15.99 | | | | | | | (308) singleton(all_107_1) = all_184_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (301) with fresh symbol all_190_0 gives: % 83.38/15.99 | | | | | | | (309) set_difference(all_130_0, all_102_0) = all_190_0 & % 83.38/15.99 | | | | | | | set_intersection2(all_130_0, all_67_1) = all_190_0 & % 83.38/15.99 | | | | | | | $i(all_190_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (309) implies: % 83.38/15.99 | | | | | | | (310) set_intersection2(all_130_0, all_67_1) = all_190_0 % 83.38/15.99 | | | | | | | (311) set_difference(all_130_0, all_102_0) = all_190_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (297) with fresh symbol all_198_0 gives: % 83.38/15.99 | | | | | | | (312) set_union2(all_102_0, all_128_0) = all_198_0 & % 83.38/15.99 | | | | | | | set_union2(all_102_0, all_67_3) = all_198_0 & % 83.38/15.99 | | | | | | | $i(all_198_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (312) implies: % 83.38/15.99 | | | | | | | (313) $i(all_198_0) % 83.38/15.99 | | | | | | | (314) set_union2(all_102_0, all_67_3) = all_198_0 % 83.38/15.99 | | | | | | | (315) set_union2(all_102_0, all_128_0) = all_198_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (292) with fresh symbol all_200_0 gives: % 83.38/15.99 | | | | | | | (316) set_difference(all_67_3, all_126_0) = all_200_0 & % 83.38/15.99 | | | | | | | set_union2(all_126_0, all_200_0) = all_67_3 & % 83.38/15.99 | | | | | | | $i(all_200_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (316) implies: % 83.38/15.99 | | | | | | | (317) $i(all_200_0) % 83.38/15.99 | | | | | | | (318) set_union2(all_126_0, all_200_0) = all_67_3 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (300) with fresh symbol all_202_0 gives: % 83.38/15.99 | | | | | | | (319) set_difference(all_202_0, all_67_1) = all_102_0 & % 83.38/15.99 | | | | | | | set_union2(all_130_0, all_67_1) = all_202_0 & % 83.38/15.99 | | | | | | | $i(all_202_0) & $i(all_102_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (296) with fresh symbols all_204_0, all_204_1 % 83.38/15.99 | | | | | | | gives: % 83.38/15.99 | | | | | | | (320) (all_204_0 = all_67_3 & set_union2(all_102_0, all_128_0) % 83.38/15.99 | | | | | | | = all_67_3) | ( ~ (all_204_1 = 0) & subset(all_102_0, % 83.38/15.99 | | | | | | | all_67_3) = all_204_1) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (299) with fresh symbols all_206_0, all_206_1 % 83.38/15.99 | | | | | | | gives: % 83.38/15.99 | | | | | | | (321) (all_206_0 = all_130_0 & set_union2(all_67_1, all_102_0) % 83.38/15.99 | | | | | | | = all_130_0) | ( ~ (all_206_1 = 0) & subset(all_67_1, % 83.38/15.99 | | | | | | | all_130_0) = all_206_1) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (298) with fresh symbol all_208_0 gives: % 83.38/15.99 | | | | | | | (322) set_difference(all_208_0, all_102_0) = all_128_0 & % 83.38/15.99 | | | | | | | set_union2(all_67_3, all_102_0) = all_208_0 & % 83.38/15.99 | | | | | | | $i(all_208_0) & $i(all_128_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (322) implies: % 83.38/15.99 | | | | | | | (323) $i(all_208_0) % 83.38/15.99 | | | | | | | (324) set_union2(all_67_3, all_102_0) = all_208_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | DELTA: instantiating (288) with fresh symbol all_214_0 gives: % 83.38/15.99 | | | | | | | (325) set_difference(all_102_0, all_67_1) = all_214_0 & % 83.38/15.99 | | | | | | | set_union2(all_67_1, all_214_0) = all_124_0 & % 83.38/15.99 | | | | | | | $i(all_214_0) & $i(all_124_0) % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | ALPHA: (325) implies: % 83.38/15.99 | | | | | | | (326) $i(all_214_0) % 83.38/15.99 | | | | | | | (327) set_union2(all_67_1, all_214_0) = all_124_0 % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | BETA: splitting (293) gives: % 83.38/15.99 | | | | | | | % 83.38/15.99 | | | | | | | Case 1: % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | (328) all_144_0 = 0 % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | REDUCE: (271), (328) imply: % 83.38/15.99 | | | | | | | | (329) $false % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | CLOSE: (329) is inconsistent. % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | Case 2: % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | (330) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & in(v0, % 83.38/15.99 | | | | | | | | all_126_0) = 0 & in(v0, all_67_1) = v1 & $i(v0)) % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | DELTA: instantiating (330) with fresh symbols all_253_0, % 83.38/15.99 | | | | | | | | all_253_1 gives: % 83.38/15.99 | | | | | | | | (331) ~ (all_253_0 = 0) & in(all_253_1, all_126_0) = 0 & % 83.38/15.99 | | | | | | | | in(all_253_1, all_67_1) = all_253_0 & $i(all_253_1) % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | ALPHA: (331) implies: % 83.38/15.99 | | | | | | | | (332) $i(all_253_1) % 83.38/15.99 | | | | | | | | (333) in(all_253_1, all_67_1) = all_253_0 % 83.38/15.99 | | | | | | | | (334) in(all_253_1, all_126_0) = 0 % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | BETA: splitting (320) gives: % 83.38/15.99 | | | | | | | | % 83.38/15.99 | | | | | | | | Case 1: % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | (335) all_204_0 = all_67_3 & set_union2(all_102_0, % 83.38/15.99 | | | | | | | | | all_128_0) = all_67_3 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | ALPHA: (335) implies: % 83.38/15.99 | | | | | | | | | (336) set_union2(all_102_0, all_128_0) = all_67_3 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | GROUND_INST: instantiating (37) with all_124_0, all_130_0, % 83.38/15.99 | | | | | | | | | all_67_3, all_67_1, simplifying with (255), (283) % 83.38/15.99 | | | | | | | | | gives: % 83.38/15.99 | | | | | | | | | (337) all_130_0 = all_124_0 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | GROUND_INST: instantiating (37) with all_67_3, all_198_0, % 83.38/15.99 | | | | | | | | | all_128_0, all_102_0, simplifying with (315), % 83.38/15.99 | | | | | | | | | (336) gives: % 83.38/15.99 | | | | | | | | | (338) all_198_0 = all_67_3 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | GROUND_INST: instantiating (35) with all_126_0, all_184_0, % 83.38/15.99 | | | | | | | | | all_107_1, simplifying with (259), (308) gives: % 83.38/15.99 | | | | | | | | | (339) all_184_0 = all_126_0 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | REDUCE: (311), (337) imply: % 83.38/15.99 | | | | | | | | | (340) set_difference(all_124_0, all_102_0) = all_190_0 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | REDUCE: (307), (339) imply: % 83.38/15.99 | | | | | | | | | (341) subset(all_126_0, all_102_0) = 0 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | REDUCE: (310), (337) imply: % 83.38/15.99 | | | | | | | | | (342) set_intersection2(all_124_0, all_67_1) = all_190_0 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | REDUCE: (314), (338) imply: % 83.38/15.99 | | | | | | | | | (343) set_union2(all_102_0, all_67_3) = all_67_3 % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | BETA: splitting (321) gives: % 83.38/15.99 | | | | | | | | | % 83.38/15.99 | | | | | | | | | Case 1: % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (40) with all_182_0, all_190_0, % 83.38/15.99 | | | | | | | | | | all_102_0, all_124_0, simplifying with (304), % 83.38/15.99 | | | | | | | | | | (340) gives: % 83.38/15.99 | | | | | | | | | | (344) all_190_0 = all_182_0 % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | REDUCE: (342), (344) imply: % 83.38/15.99 | | | | | | | | | | (345) set_intersection2(all_124_0, all_67_1) = all_182_0 % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (5) with all_107_1, all_107_1, % 83.38/15.99 | | | | | | | | | | all_126_0, all_253_1, simplifying with (243), % 83.38/15.99 | | | | | | | | | | (279), (295), (332), (334) gives: % 83.38/15.99 | | | | | | | | | | (346) all_253_1 = all_107_1 % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (6) with all_67_3, all_102_0, % 83.38/15.99 | | | | | | | | | | all_208_0, all_107_1, 0, simplifying with (46), % 83.38/15.99 | | | | | | | | | | (236), (243), (244), (323), (324) gives: % 83.38/15.99 | | | | | | | | | | (347) in(all_107_1, all_208_0) = 0 % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (1) with all_214_0, all_67_1, % 83.38/15.99 | | | | | | | | | | all_124_0, simplifying with (48), (326), (327) % 83.38/15.99 | | | | | | | | | | gives: % 83.38/15.99 | | | | | | | | | | (348) set_union2(all_214_0, all_67_1) = all_124_0 & % 83.38/15.99 | | | | | | | | | | $i(all_124_0) % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | ALPHA: (348) implies: % 83.38/15.99 | | | | | | | | | | (349) $i(all_124_0) % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (1) with all_67_3, all_102_0, % 83.38/15.99 | | | | | | | | | | all_67_3, simplifying with (46), (236), (343) % 83.38/15.99 | | | | | | | | | | gives: % 83.38/15.99 | | | | | | | | | | (350) set_union2(all_67_3, all_102_0) = all_67_3 % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (7) with all_102_0, all_67_1, % 83.38/15.99 | | | | | | | | | | all_124_0, all_253_1, all_253_0, simplifying with % 83.38/15.99 | | | | | | | | | | (48), (236), (285), (332), (333), (349) gives: % 83.38/15.99 | | | | | | | | | | (351) ? [v0: int] : ? [v1: int] : ((v1 = 0 & % 83.38/15.99 | | | | | | | | | | in(all_253_1, all_124_0) = 0) | ( ~ (v0 = 0) & % 83.38/15.99 | | | | | | | | | | ~ (all_253_0 = 0) & in(all_253_1, all_102_0) = % 83.38/15.99 | | | | | | | | | | v0)) % 83.38/15.99 | | | | | | | | | | % 83.38/15.99 | | | | | | | | | | GROUND_INST: instantiating (1) with all_200_0, all_126_0, % 83.38/16.00 | | | | | | | | | | all_67_3, simplifying with (279), (317), (318) % 83.38/16.00 | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | (352) set_union2(all_200_0, all_126_0) = all_67_3 & % 83.38/16.00 | | | | | | | | | | $i(all_67_3) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (2) with all_67_1, all_124_0, % 83.38/16.00 | | | | | | | | | | all_182_0, simplifying with (48), (345), (349) % 83.38/16.00 | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | (353) set_intersection2(all_67_1, all_124_0) = all_182_0 % 83.38/16.00 | | | | | | | | | | & $i(all_182_0) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | ALPHA: (353) implies: % 83.38/16.00 | | | | | | | | | | (354) set_intersection2(all_67_1, all_124_0) = all_182_0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (10) with all_126_0, all_67_3, % 83.38/16.00 | | | | | | | | | | all_126_0, all_253_1, simplifying with (46), % 83.38/16.00 | | | | | | | | | | (279), (291), (332), (334) gives: % 83.38/16.00 | | | | | | | | | | (355) in(all_253_1, all_67_3) = 0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (20) with all_67_1, all_124_0, % 83.38/16.00 | | | | | | | | | | simplifying with (48), (286), (349) gives: % 83.38/16.00 | | | | | | | | | | (356) set_intersection2(all_67_1, all_124_0) = all_67_1 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (8) with all_126_0, all_102_0, % 83.38/16.00 | | | | | | | | | | all_253_1, simplifying with (236), (279), (332), % 83.38/16.00 | | | | | | | | | | (334), (341) gives: % 83.38/16.00 | | | | | | | | | | (357) in(all_253_1, all_102_0) = 0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (t36_xboole_1) with all_67_1, % 83.38/16.00 | | | | | | | | | | all_102_0, all_182_0, simplifying with (48), % 83.38/16.00 | | | | | | | | | | (236), (303) gives: % 83.38/16.00 | | | | | | | | | | (358) subset(all_182_0, all_67_1) = 0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (13) with all_102_0, all_67_3, % 83.38/16.00 | | | | | | | | | | empty_set, all_107_1, 0, simplifying with (46), % 83.38/16.00 | | | | | | | | | | (56), (236), (243), (276), (289) gives: % 83.38/16.00 | | | | | | | | | | (359) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & % 83.38/16.00 | | | | | | | | | | in(all_107_1, all_67_3) = v1) | ( ~ (v0 = 0) & % 83.38/16.00 | | | | | | | | | | in(all_107_1, empty_set) = v0)) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (24) with all_67_3, all_102_0, % 83.38/16.00 | | | | | | | | | | empty_set, simplifying with (46), (236), (289) % 83.38/16.00 | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | (360) ? [v0: $i] : (set_union2(all_67_3, all_102_0) = v0 % 83.38/16.00 | | | | | | | | | | & set_union2(all_67_3, empty_set) = v0 & $i(v0)) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (14) with all_126_0, all_67_3, % 83.38/16.00 | | | | | | | | | | empty_set, all_107_1, 0, simplifying with (46), % 83.38/16.00 | | | | | | | | | | (56), (243), (244), (279), (290) gives: % 83.38/16.00 | | | | | | | | | | (361) ? [v0: int] : ( ~ (v0 = 0) & in(all_107_1, % 83.38/16.00 | | | | | | | | | | empty_set) = v0) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | GROUND_INST: instantiating (13) with all_126_0, all_67_3, % 83.38/16.00 | | | | | | | | | | empty_set, all_253_1, 0, simplifying with (46), % 83.38/16.00 | | | | | | | | | | (56), (279), (290), (332), (334) gives: % 83.38/16.00 | | | | | | | | | | (362) ? [v0: int] : ? [v1: int] : (( ~ (v1 = 0) & % 83.38/16.00 | | | | | | | | | | in(all_253_1, all_67_3) = v1) | ( ~ (v0 = 0) & % 83.38/16.00 | | | | | | | | | | in(all_253_1, empty_set) = v0)) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | DELTA: instantiating (361) with fresh symbol all_323_0 % 83.38/16.00 | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | (363) ~ (all_323_0 = 0) & in(all_107_1, empty_set) = % 83.38/16.00 | | | | | | | | | | all_323_0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | ALPHA: (363) implies: % 83.38/16.00 | | | | | | | | | | (364) in(all_107_1, empty_set) = all_323_0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | DELTA: instantiating (360) with fresh symbol all_422_0 % 83.38/16.00 | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | (365) set_union2(all_67_3, all_102_0) = all_422_0 & % 83.38/16.00 | | | | | | | | | | set_union2(all_67_3, empty_set) = all_422_0 & % 83.38/16.00 | | | | | | | | | | $i(all_422_0) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | ALPHA: (365) implies: % 83.38/16.00 | | | | | | | | | | (366) set_union2(all_67_3, all_102_0) = all_422_0 % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | DELTA: instantiating (362) with fresh symbols all_487_0, % 83.38/16.00 | | | | | | | | | | all_487_1 gives: % 83.38/16.00 | | | | | | | | | | (367) ( ~ (all_487_0 = 0) & in(all_253_1, all_67_3) = % 83.38/16.00 | | | | | | | | | | all_487_0) | ( ~ (all_487_1 = 0) & in(all_253_1, % 83.38/16.00 | | | | | | | | | | empty_set) = all_487_1) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | DELTA: instantiating (359) with fresh symbols all_501_0, % 83.38/16.00 | | | | | | | | | | all_501_1 gives: % 83.38/16.00 | | | | | | | | | | (368) ( ~ (all_501_0 = 0) & in(all_107_1, all_67_3) = % 83.38/16.00 | | | | | | | | | | all_501_0) | ( ~ (all_501_1 = 0) & in(all_107_1, % 83.38/16.00 | | | | | | | | | | empty_set) = all_501_1) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | DELTA: instantiating (351) with fresh symbols all_517_0, % 83.38/16.00 | | | | | | | | | | all_517_1 gives: % 83.38/16.00 | | | | | | | | | | (369) (all_517_0 = 0 & in(all_253_1, all_124_0) = 0) | ( % 83.38/16.00 | | | | | | | | | | ~ (all_517_1 = 0) & ~ (all_253_0 = 0) & % 83.38/16.00 | | | | | | | | | | in(all_253_1, all_102_0) = all_517_1) % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | BETA: splitting (367) gives: % 83.38/16.00 | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | Case 1: % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | (370) ~ (all_487_0 = 0) & in(all_253_1, all_67_3) = % 83.38/16.00 | | | | | | | | | | | all_487_0 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | ALPHA: (370) implies: % 83.38/16.00 | | | | | | | | | | | (371) ~ (all_487_0 = 0) % 83.38/16.00 | | | | | | | | | | | (372) in(all_253_1, all_67_3) = all_487_0 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | REDUCE: (346), (372) imply: % 83.38/16.00 | | | | | | | | | | | (373) in(all_107_1, all_67_3) = all_487_0 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_487_0, all_67_3, % 83.38/16.00 | | | | | | | | | | | all_107_1, simplifying with (244), (373) gives: % 83.38/16.00 | | | | | | | | | | | (374) all_487_0 = 0 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | REDUCE: (371), (374) imply: % 83.38/16.00 | | | | | | | | | | | (375) $false % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | CLOSE: (375) is inconsistent. % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | Case 2: % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | (376) ~ (all_487_1 = 0) & in(all_253_1, empty_set) = % 83.38/16.00 | | | | | | | | | | | all_487_1 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | ALPHA: (376) implies: % 83.38/16.00 | | | | | | | | | | | (377) ~ (all_487_1 = 0) % 83.38/16.00 | | | | | | | | | | | (378) in(all_253_1, empty_set) = all_487_1 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | REDUCE: (346), (378) imply: % 83.38/16.00 | | | | | | | | | | | (379) in(all_107_1, empty_set) = all_487_1 % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | BETA: splitting (368) gives: % 83.38/16.00 | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | Case 1: % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | (380) ~ (all_501_0 = 0) & in(all_107_1, all_67_3) = % 83.38/16.00 | | | | | | | | | | | | all_501_0 % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | ALPHA: (380) implies: % 83.38/16.00 | | | | | | | | | | | | (381) ~ (all_501_0 = 0) % 83.38/16.00 | | | | | | | | | | | | (382) in(all_107_1, all_67_3) = all_501_0 % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_501_0, all_67_3, % 83.38/16.00 | | | | | | | | | | | | all_107_1, simplifying with (244), (382) gives: % 83.38/16.00 | | | | | | | | | | | | (383) all_501_0 = 0 % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | REDUCE: (381), (383) imply: % 83.38/16.00 | | | | | | | | | | | | (384) $false % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | CLOSE: (384) is inconsistent. % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | Case 2: % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | (385) ~ (all_501_1 = 0) & in(all_107_1, empty_set) = % 83.38/16.00 | | | | | | | | | | | | all_501_1 % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | ALPHA: (385) implies: % 83.38/16.00 | | | | | | | | | | | | (386) in(all_107_1, empty_set) = all_501_1 % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | BETA: splitting (369) gives: % 83.38/16.00 | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | Case 1: % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_487_1, all_501_1, % 83.38/16.00 | | | | | | | | | | | | | empty_set, all_107_1, simplifying with (379), % 83.38/16.00 | | | | | | | | | | | | | (386) gives: % 83.38/16.00 | | | | | | | | | | | | | (387) all_501_1 = all_487_1 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_323_0, all_501_1, % 83.38/16.00 | | | | | | | | | | | | | empty_set, all_107_1, simplifying with (364), % 83.38/16.00 | | | | | | | | | | | | | (386) gives: % 83.38/16.00 | | | | | | | | | | | | | (388) all_501_1 = all_323_0 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | GROUND_INST: instantiating (37) with all_208_0, all_422_0, % 83.38/16.00 | | | | | | | | | | | | | all_102_0, all_67_3, simplifying with (324), (366) % 83.38/16.00 | | | | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | | | | (389) all_422_0 = all_208_0 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | GROUND_INST: instantiating (37) with all_67_3, all_422_0, % 83.38/16.00 | | | | | | | | | | | | | all_102_0, all_67_3, simplifying with (350), (366) % 83.38/16.00 | | | | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | | | | (390) all_422_0 = all_67_3 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | GROUND_INST: instantiating (38) with all_67_1, all_182_0, % 83.38/16.00 | | | | | | | | | | | | | all_124_0, all_67_1, simplifying with (354), (356) % 83.38/16.00 | | | | | | | | | | | | | gives: % 83.38/16.00 | | | | | | | | | | | | | (391) all_182_0 = all_67_1 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | COMBINE_EQS: (387), (388) imply: % 83.38/16.00 | | | | | | | | | | | | | (392) all_487_1 = all_323_0 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | SIMP: (392) implies: % 83.38/16.00 | | | | | | | | | | | | | (393) all_487_1 = all_323_0 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | COMBINE_EQS: (389), (390) imply: % 83.38/16.00 | | | | | | | | | | | | | (394) all_208_0 = all_67_3 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | SIMP: (394) implies: % 83.38/16.00 | | | | | | | | | | | | | (395) all_208_0 = all_67_3 % 83.38/16.00 | | | | | | | | | | | | | % 83.38/16.00 | | | | | | | | | | | | | REDUCE: (377), (393) imply: % 83.55/16.00 | | | | | | | | | | | | | (396) ~ (all_323_0 = 0) % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | REDUCE: (358), (391) imply: % 83.55/16.00 | | | | | | | | | | | | | (397) subset(all_67_1, all_67_1) = 0 % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | BETA: splitting (231) gives: % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | Case 1: % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | (398) all_67_3 = empty_set % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | REDUCE: (244), (398) imply: % 83.55/16.00 | | | | | | | | | | | | | | (399) in(all_107_1, empty_set) = 0 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_323_0, empty_set, % 83.55/16.00 | | | | | | | | | | | | | | all_107_1, simplifying with (364), (399) gives: % 83.55/16.00 | | | | | | | | | | | | | | (400) all_323_0 = 0 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | REDUCE: (396), (400) imply: % 83.55/16.00 | | | | | | | | | | | | | | (401) $false % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | CLOSE: (401) is inconsistent. % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | Case 2: % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | (402) all_67_1 = all_67_3 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | REDUCE: (397), (402) imply: % 83.55/16.00 | | | | | | | | | | | | | | (403) subset(all_67_3, all_67_3) = 0 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | REDUCE: (49), (402) imply: % 83.55/16.00 | | | | | | | | | | | | | | (404) subset(all_67_3, all_67_3) = all_67_0 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | GROUND_INST: instantiating (39) with 0, all_67_0, all_67_3, % 83.55/16.00 | | | | | | | | | | | | | | all_67_3, simplifying with (403), (404) gives: % 83.55/16.00 | | | | | | | | | | | | | | (405) all_67_0 = 0 % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | REDUCE: (230), (405) imply: % 83.55/16.00 | | | | | | | | | | | | | | (406) $false % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | | CLOSE: (406) is inconsistent. % 83.55/16.00 | | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | End of split % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | Case 2: % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | (407) ~ (all_517_1 = 0) & ~ (all_253_0 = 0) & % 83.55/16.00 | | | | | | | | | | | | | in(all_253_1, all_102_0) = all_517_1 % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | ALPHA: (407) implies: % 83.55/16.00 | | | | | | | | | | | | | (408) ~ (all_517_1 = 0) % 83.55/16.00 | | | | | | | | | | | | | (409) in(all_253_1, all_102_0) = all_517_1 % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.00 | | | | | | | | | | | | | REDUCE: (346), (409) imply: % 83.55/16.00 | | | | | | | | | | | | | (410) in(all_107_1, all_102_0) = all_517_1 % 83.55/16.00 | | | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_517_1, all_102_0, % 83.55/16.01 | | | | | | | | | | | | | all_107_1, simplifying with (276), (410) gives: % 83.55/16.01 | | | | | | | | | | | | | (411) all_517_1 = 0 % 83.55/16.01 | | | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | | | | REDUCE: (408), (411) imply: % 83.55/16.01 | | | | | | | | | | | | | (412) $false % 83.55/16.01 | | | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | | | | CLOSE: (412) is inconsistent. % 83.55/16.01 | | | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | | | End of split % 83.55/16.01 | | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | | End of split % 83.55/16.01 | | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | End of split % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | Case 2: % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | (413) ~ (all_206_1 = 0) & subset(all_67_1, all_130_0) = % 83.55/16.01 | | | | | | | | | | all_206_1 % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | ALPHA: (413) implies: % 83.55/16.01 | | | | | | | | | | (414) ~ (all_206_1 = 0) % 83.55/16.01 | | | | | | | | | | (415) subset(all_67_1, all_130_0) = all_206_1 % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | REDUCE: (337), (415) imply: % 83.55/16.01 | | | | | | | | | | (416) subset(all_67_1, all_124_0) = all_206_1 % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | GROUND_INST: instantiating (39) with 0, all_206_1, all_124_0, % 83.55/16.01 | | | | | | | | | | all_67_1, simplifying with (286), (416) gives: % 83.55/16.01 | | | | | | | | | | (417) all_206_1 = 0 % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | REDUCE: (414), (417) imply: % 83.55/16.01 | | | | | | | | | | (418) $false % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | | CLOSE: (418) is inconsistent. % 83.55/16.01 | | | | | | | | | | % 83.55/16.01 | | | | | | | | | End of split % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | Case 2: % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | | (419) ~ (all_204_1 = 0) & subset(all_102_0, all_67_3) = % 83.55/16.01 | | | | | | | | | all_204_1 % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | | ALPHA: (419) implies: % 83.55/16.01 | | | | | | | | | (420) ~ (all_204_1 = 0) % 83.55/16.01 | | | | | | | | | (421) subset(all_102_0, all_67_3) = all_204_1 % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | | GROUND_INST: instantiating (39) with 0, all_204_1, all_67_3, % 83.55/16.01 | | | | | | | | | all_102_0, simplifying with (251), (421) gives: % 83.55/16.01 | | | | | | | | | (422) all_204_1 = 0 % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | | REDUCE: (420), (422) imply: % 83.55/16.01 | | | | | | | | | (423) $false % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | | CLOSE: (423) is inconsistent. % 83.55/16.01 | | | | | | | | | % 83.55/16.01 | | | | | | | | End of split % 83.55/16.01 | | | | | | | | % 83.55/16.01 | | | | | | | End of split % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | Case 2: % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | | (424) ~ (all_133_1 = 0) & in(all_107_1, all_102_0) = all_133_1 % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | | ALPHA: (424) implies: % 83.55/16.01 | | | | | | | (425) ~ (all_133_1 = 0) % 83.55/16.01 | | | | | | | (426) in(all_107_1, all_102_0) = all_133_1 % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | | GROUND_INST: instantiating (36) with 0, all_133_1, all_102_0, % 83.55/16.01 | | | | | | | all_107_1, simplifying with (276), (426) gives: % 83.55/16.01 | | | | | | | (427) all_133_1 = 0 % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | | REDUCE: (425), (427) imply: % 83.55/16.01 | | | | | | | (428) $false % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | | CLOSE: (428) is inconsistent. % 83.55/16.01 | | | | | | | % 83.55/16.01 | | | | | | End of split % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | Case 2: % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | | (429) all_134_1 = 0 & in(all_107_1, all_67_1) = 0 % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | | ALPHA: (429) implies: % 83.55/16.01 | | | | | | (430) in(all_107_1, all_67_1) = 0 % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | | GROUND_INST: instantiating (36) with all_107_0, 0, all_67_1, % 83.55/16.01 | | | | | | all_107_1, simplifying with (245), (430) gives: % 83.55/16.01 | | | | | | (431) all_107_0 = 0 % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | | REDUCE: (242), (431) imply: % 83.55/16.01 | | | | | | (432) $false % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | | CLOSE: (432) is inconsistent. % 83.55/16.01 | | | | | | % 83.55/16.01 | | | | | End of split % 83.55/16.01 | | | | | % 83.55/16.01 | | | | End of split % 83.55/16.01 | | | | % 83.55/16.01 | | | End of split % 83.55/16.01 | | | % 83.55/16.01 | | End of split % 83.55/16.01 | | % 83.55/16.01 | End of split % 83.55/16.01 | % 83.55/16.01 End of proof % 83.55/16.01 % 83.55/16.01 Sub-proof #1 shows that the following formulas are inconsistent: % 83.55/16.01 ---------------------------------------------------------------- % 83.55/16.01 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 83.55/16.01 ! [v3: $i] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 83.55/16.01 (2) in(all_67_2, all_67_3) = 0 % 83.55/16.01 (3) ~ (all_170_0 = 0) % 83.55/16.01 (4) in(all_67_2, all_67_3) = all_170_0 % 83.55/16.01 (5) in(all_67_2, all_67_3) = all_179_0 % 83.55/16.01 % 83.55/16.01 Begin of proof % 83.55/16.01 | % 83.55/16.01 | GROUND_INST: instantiating (1) with all_179_0, 0, all_67_3, all_67_2, % 83.55/16.01 | simplifying with (2), (5) gives: % 83.55/16.01 | (6) all_179_0 = 0 % 83.55/16.01 | % 83.55/16.01 | GROUND_INST: instantiating (1) with all_179_0, all_170_0, all_67_3, all_67_2, % 83.55/16.01 | simplifying with (4), (5) gives: % 83.55/16.01 | (7) all_179_0 = all_170_0 % 83.55/16.01 | % 83.55/16.01 | COMBINE_EQS: (6), (7) imply: % 83.55/16.01 | (8) all_170_0 = 0 % 83.55/16.01 | % 83.55/16.01 | SIMP: (8) implies: % 83.55/16.01 | (9) all_170_0 = 0 % 83.55/16.01 | % 83.55/16.01 | REDUCE: (3), (9) imply: % 83.55/16.01 | (10) $false % 83.55/16.01 | % 83.55/16.01 | CLOSE: (10) is inconsistent. % 83.55/16.01 | % 83.55/16.01 End of proof % 83.55/16.01 % SZS output end Proof for theBenchmark % 83.55/16.01 % 83.55/16.01 15445ms %------------------------------------------------------------------------------