%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV398+1 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n003.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 22:56:10 EDT 2023 % Result : Theorem 17.91s 3.16s % Output : Proof 21.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWV398+1 : TPTP v8.1.2. Released v3.3.0. % 0.04/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Aug 29 08:09:40 EDT 2023 % 0.13/0.34 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.65/0.63 Running up to 7 provers in parallel. % 0.65/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.65/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.65/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.65/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.65/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.65/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.65/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.87/1.20 Prover 1: Preprocessing ... % 3.49/1.21 Prover 4: Preprocessing ... % 3.49/1.25 Prover 2: Preprocessing ... % 3.49/1.25 Prover 5: Preprocessing ... % 3.49/1.25 Prover 0: Preprocessing ... % 3.49/1.25 Prover 6: Preprocessing ... % 3.49/1.25 Prover 3: Preprocessing ... % 7.27/1.76 Prover 1: Warning: ignoring some quantifiers % 7.99/1.86 Prover 3: Warning: ignoring some quantifiers % 7.99/1.87 Prover 1: Constructing countermodel ... % 7.99/1.88 Prover 5: Proving ... % 7.99/1.89 Prover 3: Constructing countermodel ... % 7.99/1.89 Prover 6: Proving ... % 8.71/1.92 Prover 0: Proving ... % 8.93/1.94 Prover 4: Constructing countermodel ... % 8.93/1.97 Prover 2: Proving ... % 11.96/2.34 Prover 3: gave up % 11.96/2.34 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 12.38/2.40 Prover 7: Preprocessing ... % 13.69/2.62 Prover 7: Warning: ignoring some quantifiers % 14.28/2.66 Prover 7: Constructing countermodel ... % 16.60/2.95 Prover 7: gave up % 16.60/2.96 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.85/3.02 Prover 8: Preprocessing ... % 17.91/3.15 Prover 8: Warning: ignoring some quantifiers % 17.91/3.16 Prover 0: proved (2525ms) % 17.91/3.16 % 17.91/3.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.91/3.16 % 17.91/3.16 Prover 6: stopped % 17.91/3.17 Prover 2: stopped % 17.91/3.17 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 17.91/3.17 Prover 5: stopped % 17.91/3.17 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 17.91/3.17 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 17.91/3.17 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.43/3.18 Prover 8: Constructing countermodel ... % 18.43/3.21 Prover 11: Preprocessing ... % 18.43/3.21 Prover 13: Preprocessing ... % 18.43/3.22 Prover 10: Preprocessing ... % 18.43/3.26 Prover 16: Preprocessing ... % 19.52/3.36 Prover 10: Warning: ignoring some quantifiers % 19.52/3.37 Prover 16: Warning: ignoring some quantifiers % 19.52/3.37 Prover 10: Constructing countermodel ... % 19.52/3.38 Prover 16: Constructing countermodel ... % 20.20/3.45 Prover 11: Constructing countermodel ... % 20.20/3.46 Prover 13: Warning: ignoring some quantifiers % 20.20/3.46 Prover 4: Found proof (size 240) % 20.20/3.46 Prover 4: proved (2827ms) % 20.20/3.46 Prover 8: stopped % 20.20/3.46 Prover 10: stopped % 20.20/3.47 Prover 1: stopped % 20.20/3.47 Prover 13: Constructing countermodel ... % 20.20/3.47 Prover 11: stopped % 20.20/3.47 Prover 16: stopped % 20.20/3.48 Prover 13: stopped % 20.20/3.48 % 20.20/3.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.20/3.48 % 20.68/3.50 % SZS output start Proof for theBenchmark % 20.68/3.50 Assumptions after simplification: % 20.68/3.50 --------------------------------- % 20.68/3.50 % 20.68/3.50 (ax36) % 20.68/3.53 $i(create_slb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (triple(v0, % 20.68/3.53 create_slb, v1) = v2) | ~ $i(v1) | ~ $i(v0) | check_cpq(v2) = 0) % 20.68/3.53 % 20.68/3.53 (ax47) % 20.68/3.53 $i(bad) & $i(create_slb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 20.68/3.53 $i] : ! [v4: $i] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ % 20.68/3.53 (findmin_cpq_eff(v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] % 20.68/3.53 : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : (findmin_pqp_res(v0) = v5 & % 20.68/3.53 triple(v0, v7, bad) = v8 & update_slb(v1, v5) = v7 & contains_slb(v1, v5) % 20.68/3.53 = v6 & $i(v8) & $i(v7) & $i(v5) & (v8 = v4 | v6 = 0))) % 20.68/3.53 % 20.68/3.53 (ax48) % 20.68/3.53 $i(bad) & $i(create_slb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 20.68/3.53 $i] : ! [v4: $i] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ % 20.68/3.53 (findmin_cpq_eff(v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] % 20.68/3.53 : ? [v6: any] : ? [v7: $i] : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : % 20.68/3.53 (findmin_pqp_res(v0) = v5 & triple(v0, v9, bad) = v10 & update_slb(v1, v5) = % 20.68/3.53 v9 & lookup_slb(v1, v5) = v7 & contains_slb(v1, v5) = v6 & % 20.68/3.53 strictly_less_than(v5, v7) = v8 & $i(v10) & $i(v9) & $i(v7) & $i(v5) & ( ~ % 20.68/3.53 (v8 = 0) | ~ (v6 = 0) | v10 = v4))) % 20.68/3.53 % 20.68/3.53 (ax49) % 20.68/3.54 $i(create_slb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 20.68/3.54 [v4: $i] : ! [v5: $i] : (v1 = create_slb | ~ (findmin_pqp_res(v0) = v3) | ~ % 20.68/3.54 (triple(v0, v4, v2) = v5) | ~ (update_slb(v1, v3) = v4) | ~ $i(v2) | ~ % 20.68/3.54 $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: $i] : ? [v8: any] : ? [v9: $i] % 20.68/3.54 : ? [v10: $i] : (triple(v0, v1, v2) = v9 & findmin_cpq_eff(v9) = v10 & % 20.68/3.54 lookup_slb(v1, v3) = v7 & contains_slb(v1, v3) = v6 & less_than(v7, v3) = % 20.68/3.54 v8 & $i(v10) & $i(v9) & $i(v7) & ( ~ (v8 = 0) | ~ (v6 = 0) | v10 = v5))) % 20.68/3.54 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 20.68/3.54 create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | % 20.68/3.54 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: any] : ? [v7: $i] % 20.68/3.54 : ? [v8: any] : ? [v9: $i] : ? [v10: $i] : (findmin_pqp_res(v0) = v5 & % 20.68/3.54 triple(v0, v9, v2) = v10 & update_slb(v1, v5) = v9 & lookup_slb(v1, v5) = % 20.68/3.54 v7 & contains_slb(v1, v5) = v6 & less_than(v7, v5) = v8 & $i(v10) & $i(v9) % 20.68/3.54 & $i(v7) & $i(v5) & ( ~ (v8 = 0) | ~ (v6 = 0) | v10 = v4))) % 20.68/3.54 % 20.68/3.54 (ax51) % 20.68/3.54 $i(create_slb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 20.68/3.54 [v4: $i] : (v1 = create_slb | ~ (findmin_cpq_res(v3) = v4) | ~ (triple(v0, % 20.68/3.54 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | (findmin_pqp_res(v0) % 20.68/3.54 = v4 & $i(v4))) % 20.68/3.54 % 20.68/3.54 (ax52) % 20.68/3.54 ! [v0: $i] : ! [v1: $i] : ( ~ (findmin_cpq_res(v0) = v1) | ~ $i(v0) | ? % 20.68/3.54 [v2: $i] : ? [v3: $i] : (removemin_cpq_eff(v0) = v2 & findmin_cpq_eff(v0) = % 20.68/3.54 v3 & remove_cpq(v3, v1) = v2 & $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: % 20.68/3.54 $i] : ( ~ (removemin_cpq_eff(v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: % 20.68/3.54 $i] : (findmin_cpq_res(v0) = v3 & findmin_cpq_eff(v0) = v2 & % 20.68/3.54 remove_cpq(v2, v3) = v1 & $i(v3) & $i(v2) & $i(v1))) & ! [v0: $i] : ! % 20.68/3.54 [v1: $i] : ( ~ (findmin_cpq_eff(v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: % 20.68/3.54 $i] : (findmin_cpq_res(v0) = v3 & removemin_cpq_eff(v0) = v2 & % 20.68/3.54 remove_cpq(v1, v3) = v2 & $i(v3) & $i(v2))) % 20.68/3.54 % 20.68/3.54 (l24_co) % 20.68/3.54 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ? [v5: % 20.68/3.54 $i] : ( ~ (v4 = 0) & triple(v0, v1, v2) = v3 & check_cpq(v5) = 0 & % 20.68/3.54 check_cpq(v3) = v4 & findmin_cpq_eff(v3) = v5 & $i(v5) & $i(v3) & $i(v2) & % 20.68/3.54 $i(v1) & $i(v0)) % 20.68/3.54 % 20.68/3.54 (l26_li4142) % 20.68/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 20.68/3.55 $i] : ! [v6: int] : (v6 = 0 | ~ (triple(v0, v1, v2) = v3) | ~ % 20.68/3.55 (less_than(v5, v4) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ~ $i(v1) | % 20.68/3.55 ~ $i(v0) | ? [v7: int] : (( ~ (v7 = 0) & check_cpq(v3) = v7) | ( ~ (v7 = 0) % 20.68/3.55 & pair_in_list(v1, v4, v5) = v7))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 20.68/3.55 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (triple(v0, v1, v2) = % 20.68/3.55 v3) | ~ (pair_in_list(v1, v4, v5) = 0) | ~ $i(v5) | ~ $i(v4) | ~ % 20.68/3.55 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : ((v6 = 0 & less_than(v5, v4) % 20.68/3.55 = 0) | ( ~ (v6 = 0) & check_cpq(v3) = v6))) & ! [v0: $i] : ! [v1: $i] % 20.68/3.55 : ! [v2: $i] : ! [v3: $i] : ( ~ (triple(v0, v1, v2) = v3) | ~ $i(v2) | ~ % 20.68/3.55 $i(v1) | ~ $i(v0) | ? [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] % 20.68/3.55 : ? [v8: int] : ($i(v6) & $i(v5) & ((v7 = 0 & ~ (v8 = 0) & % 20.68/3.55 pair_in_list(v1, v5, v6) = 0 & less_than(v6, v5) = v8) | (v4 = 0 & % 20.68/3.55 check_cpq(v3) = 0)))) % 20.68/3.55 % 20.68/3.55 (l34_l35) % 20.68/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 20.68/3.55 (update_slb(v0, v1) = v2) | ~ (pair_in_list(v0, v3, v4) = 0) | ~ $i(v4) | % 20.68/3.55 ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: int] % 20.68/3.55 : ? [v8: int] : ? [v9: int] : ($i(v6) & $i(v5) & ((v8 = 0 & v7 = 0 & % 20.68/3.55 pair_in_list(v2, v5, v6) = 0 & strictly_less_than(v5, v6) = 0) | ( ~ % 20.68/3.55 (v9 = 0) & strictly_less_than(v3, v4) = v9)))) & ! [v0: $i] : ! [v1: % 20.68/3.55 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (update_slb(v0, v1) = % 20.68/3.55 v2) | ~ (strictly_less_than(v3, v4) = 0) | ~ $i(v4) | ~ $i(v3) | ~ % 20.68/3.55 $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ? [v8: int] % 20.68/3.55 : ? [v9: int] : ($i(v6) & $i(v5) & ((v8 = 0 & v7 = 0 & pair_in_list(v2, v5, % 20.68/3.55 v6) = 0 & strictly_less_than(v5, v6) = 0) | ( ~ (v9 = 0) & % 20.68/3.55 pair_in_list(v0, v3, v4) = v9)))) % 20.68/3.55 % 20.68/3.55 (stricly_smaller_definition) % 20.68/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 20.68/3.55 (strictly_less_than(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 20.68/3.55 ? [v4: any] : (less_than(v1, v0) = v4 & less_than(v0, v1) = v3 & ( ~ (v3 = % 20.68/3.55 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | % 20.68/3.55 ~ (less_than(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 20.68/3.55 any] : (strictly_less_than(v0, v1) = v4 & less_than(v0, v1) = v3 & ( ~ (v3 % 20.68/3.55 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ % 20.68/3.55 (less_than(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 20.68/3.55 any] : (strictly_less_than(v0, v1) = v3 & less_than(v0, v1) = v4 & ( ~ (v3 % 20.68/3.55 = 0) | (v4 = 0 & ~ (v2 = 0))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 20.68/3.55 any] : ( ~ (less_than(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 20.68/3.55 ? [v4: any] : (strictly_less_than(v0, v1) = v3 & less_than(v1, v0) = v4 & ( % 20.68/3.55 ~ (v3 = 0) | (v2 = 0 & ~ (v4 = 0))))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 20.68/3.55 (strictly_less_than(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: int] : ( % 20.68/3.55 ~ (v2 = 0) & less_than(v1, v0) = v2 & less_than(v0, v1) = 0)) & ! [v0: % 20.68/3.55 $i] : ! [v1: $i] : ( ~ (less_than(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? % 20.68/3.55 [v2: any] : ? [v3: any] : (strictly_less_than(v0, v1) = v3 & less_than(v1, % 20.68/3.55 v0) = v2 & (v3 = 0 | v2 = 0))) % 20.68/3.55 % 20.68/3.55 (totality) % 20.68/3.55 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (less_than(v1, v0) = % 20.68/3.55 v2) | ~ $i(v1) | ~ $i(v0) | less_than(v0, v1) = 0) & ! [v0: $i] : ! % 20.68/3.55 [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (less_than(v0, v1) = v2) | ~ $i(v1) | % 20.68/3.55 ~ $i(v0) | less_than(v1, v0) = 0) % 20.68/3.55 % 20.68/3.55 (function-axioms) % 20.68/3.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 20.68/3.56 | ~ (triple(v4, v3, v2) = v1) | ~ (triple(v4, v3, v2) = v0)) & ! [v0: % 20.68/3.56 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 20.68/3.56 : ! [v4: $i] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) | ~ % 20.68/3.56 (pair_in_list(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 20.68/3.56 ! [v3: $i] : (v1 = v0 | ~ (remove_pqp(v3, v2) = v1) | ~ (remove_pqp(v3, v2) % 20.68/3.56 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 20.68/3.56 | ~ (insert_pqp(v3, v2) = v1) | ~ (insert_pqp(v3, v2) = v0)) & ! [v0: % 20.68/3.56 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 20.68/3.56 : (v1 = v0 | ~ (contains_cpq(v3, v2) = v1) | ~ (contains_cpq(v3, v2) = v0)) % 20.68/3.56 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 20.68/3.56 (remove_cpq(v3, v2) = v1) | ~ (remove_cpq(v3, v2) = v0)) & ! [v0: $i] : ! % 20.68/3.56 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_cpq(v3, v2) = v1) % 20.68/3.56 | ~ (insert_cpq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.68/3.56 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (succ_cpq(v3, % 20.68/3.56 v2) = v1) | ~ (succ_cpq(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 20.68/3.56 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (update_slb(v3, v2) = v1) | ~ % 20.68/3.56 (update_slb(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 20.68/3.56 [v3: $i] : (v1 = v0 | ~ (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = % 20.68/3.56 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 20.68/3.56 ~ (remove_slb(v3, v2) = v1) | ~ (remove_slb(v3, v2) = v0)) & ! [v0: % 20.68/3.56 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 20.68/3.56 : (v1 = v0 | ~ (contains_slb(v3, v2) = v1) | ~ (contains_slb(v3, v2) = v0)) % 20.68/3.56 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 20.68/3.56 (pair(v3, v2) = v1) | ~ (pair(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 20.68/3.56 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_slb(v3, v2) = v1) | ~ % 20.68/3.56 (insert_slb(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.68/3.56 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 20.68/3.56 (strictly_less_than(v3, v2) = v1) | ~ (strictly_less_than(v3, v2) = v0)) & % 20.68/3.56 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 20.68/3.56 $i] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ (less_than(v3, v2) = v0)) % 20.68/3.56 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 20.68/3.56 (removemin_cpq_res(v2) = v1) | ~ (removemin_cpq_res(v2) = v0)) & ! [v0: % 20.68/3.56 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (findmin_cpq_res(v2) = v1) | % 20.68/3.56 ~ (findmin_cpq_res(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 20.68/3.56 (v1 = v0 | ~ (findmin_pqp_res(v2) = v1) | ~ (findmin_pqp_res(v2) = v0)) & ! % 20.68/3.56 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 20.68/3.56 | ~ (ok(v2) = v1) | ~ (ok(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 20.68/3.56 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (check_cpq(v2) = v1) | % 20.68/3.56 ~ (check_cpq(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 20.68/3.56 | ~ (removemin_cpq_eff(v2) = v1) | ~ (removemin_cpq_eff(v2) = v0)) & ! % 20.68/3.56 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (findmin_cpq_eff(v2) = % 20.68/3.56 v1) | ~ (findmin_cpq_eff(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 20.68/3.56 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (isnonempty_slb(v2) = % 20.68/3.56 v1) | ~ (isnonempty_slb(v2) = v0)) % 20.68/3.56 % 20.68/3.56 Further assumptions not needed in the proof: % 20.68/3.56 -------------------------------------------- % 20.68/3.56 ax18, ax19, ax20, ax21, ax22, ax23, ax24, ax25, ax26, ax27, ax28, ax29, ax30, % 20.68/3.56 ax31, ax32, ax33, ax34, ax35, ax37, ax38, ax39, ax40, ax41, ax42, ax43, ax44, % 20.68/3.56 ax45, ax46, ax50, ax53, bottom_smallest, reflexivity, transitivity % 20.68/3.56 % 20.68/3.56 Those formulas are unsatisfiable: % 20.68/3.56 --------------------------------- % 20.68/3.56 % 20.68/3.56 Begin of proof % 20.68/3.56 | % 20.68/3.56 | ALPHA: (totality) implies: % 20.68/3.56 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (less_than(v1, % 20.68/3.56 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | less_than(v0, v1) = 0) % 20.68/3.56 | % 20.68/3.56 | ALPHA: (stricly_smaller_definition) implies: % 20.68/3.56 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (strictly_less_than(v0, v1) = 0) | ~ % 20.68/3.56 | $i(v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & less_than(v1, v0) % 20.68/3.56 | = v2 & less_than(v0, v1) = 0)) % 20.68/3.56 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (less_than(v0, v1) = v2) % 20.68/3.56 | | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 20.68/3.56 | (strictly_less_than(v0, v1) = v3 & less_than(v1, v0) = v4 & ( ~ (v3 = % 20.68/3.56 | 0) | (v2 = 0 & ~ (v4 = 0))))) % 20.68/3.56 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: any] : ( ~ (less_than(v1, v0) = v2) % 20.68/3.56 | | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 20.68/3.56 | (strictly_less_than(v0, v1) = v3 & less_than(v0, v1) = v4 & ( ~ (v3 = % 20.68/3.56 | 0) | (v4 = 0 & ~ (v2 = 0))))) % 20.68/3.56 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (less_than(v1, % 20.68/3.56 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 20.68/3.56 | (strictly_less_than(v0, v1) = v4 & less_than(v0, v1) = v3 & ( ~ (v3 = % 20.68/3.56 | 0) | v4 = 0))) % 20.68/3.56 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 20.68/3.56 | (strictly_less_than(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 20.68/3.56 | any] : ? [v4: any] : (less_than(v1, v0) = v4 & less_than(v0, v1) = % 20.68/3.56 | v3 & ( ~ (v3 = 0) | v4 = 0))) % 20.68/3.56 | % 20.68/3.56 | ALPHA: (ax36) implies: % 21.07/3.56 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (triple(v0, create_slb, % 21.07/3.56 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | check_cpq(v2) = 0) % 21.07/3.56 | % 21.07/3.56 | ALPHA: (ax47) implies: % 21.07/3.57 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ % 21.07/3.57 | (findmin_cpq_eff(v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 21.07/3.57 | [v5: $i] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 21.07/3.57 | (findmin_pqp_res(v0) = v5 & triple(v0, v7, bad) = v8 & update_slb(v1, % 21.07/3.57 | v5) = v7 & contains_slb(v1, v5) = v6 & $i(v8) & $i(v7) & $i(v5) & % 21.07/3.57 | (v8 = v4 | v6 = 0))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (ax48) implies: % 21.07/3.57 | (9) $i(bad) % 21.07/3.57 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ % 21.07/3.57 | (findmin_cpq_eff(v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 21.07/3.57 | [v5: $i] : ? [v6: any] : ? [v7: $i] : ? [v8: any] : ? [v9: $i] : % 21.07/3.57 | ? [v10: $i] : (findmin_pqp_res(v0) = v5 & triple(v0, v9, bad) = v10 % 21.07/3.57 | & update_slb(v1, v5) = v9 & lookup_slb(v1, v5) = v7 & % 21.07/3.57 | contains_slb(v1, v5) = v6 & strictly_less_than(v5, v7) = v8 & % 21.07/3.57 | $i(v10) & $i(v9) & $i(v7) & $i(v5) & ( ~ (v8 = 0) | ~ (v6 = 0) | % 21.07/3.57 | v10 = v4))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (ax49) implies: % 21.07/3.57 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ % 21.07/3.57 | (findmin_cpq_eff(v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 21.07/3.57 | [v5: $i] : ? [v6: any] : ? [v7: $i] : ? [v8: any] : ? [v9: $i] : % 21.07/3.57 | ? [v10: $i] : (findmin_pqp_res(v0) = v5 & triple(v0, v9, v2) = v10 % 21.07/3.57 | & update_slb(v1, v5) = v9 & lookup_slb(v1, v5) = v7 & % 21.07/3.57 | contains_slb(v1, v5) = v6 & less_than(v7, v5) = v8 & $i(v10) & % 21.07/3.57 | $i(v9) & $i(v7) & $i(v5) & ( ~ (v8 = 0) | ~ (v6 = 0) | v10 = % 21.07/3.57 | v4))) % 21.07/3.57 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | ! [v5: $i] : (v1 = create_slb | ~ (findmin_pqp_res(v0) = v3) | ~ % 21.07/3.57 | (triple(v0, v4, v2) = v5) | ~ (update_slb(v1, v3) = v4) | ~ $i(v2) % 21.07/3.57 | | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: $i] : ? [v8: any] % 21.07/3.57 | : ? [v9: $i] : ? [v10: $i] : (triple(v0, v1, v2) = v9 & % 21.07/3.57 | findmin_cpq_eff(v9) = v10 & lookup_slb(v1, v3) = v7 & % 21.07/3.57 | contains_slb(v1, v3) = v6 & less_than(v7, v3) = v8 & $i(v10) & % 21.07/3.57 | $i(v9) & $i(v7) & ( ~ (v8 = 0) | ~ (v6 = 0) | v10 = v5))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (ax51) implies: % 21.07/3.57 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | (v1 = create_slb | ~ (findmin_cpq_res(v3) = v4) | ~ (triple(v0, v1, % 21.07/3.57 | v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 21.07/3.57 | (findmin_pqp_res(v0) = v4 & $i(v4))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (ax52) implies: % 21.07/3.57 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (findmin_cpq_eff(v0) = v1) | ~ $i(v0) % 21.07/3.57 | | ? [v2: $i] : ? [v3: $i] : (findmin_cpq_res(v0) = v3 & % 21.07/3.57 | removemin_cpq_eff(v0) = v2 & remove_cpq(v1, v3) = v2 & $i(v3) & % 21.07/3.57 | $i(v2))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (l26_li4142) implies: % 21.07/3.57 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 21.07/3.57 | (triple(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 21.07/3.57 | [v4: int] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ? [v8: int] % 21.07/3.57 | : ($i(v6) & $i(v5) & ((v7 = 0 & ~ (v8 = 0) & pair_in_list(v1, v5, % 21.07/3.57 | v6) = 0 & less_than(v6, v5) = v8) | (v4 = 0 & check_cpq(v3) % 21.07/3.57 | = 0)))) % 21.07/3.57 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | ! [v5: $i] : ( ~ (triple(v0, v1, v2) = v3) | ~ (pair_in_list(v1, v4, % 21.07/3.57 | v5) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ~ $i(v1) | ~ % 21.07/3.57 | $i(v0) | ? [v6: int] : ((v6 = 0 & less_than(v5, v4) = 0) | ( ~ (v6 % 21.07/3.57 | = 0) & check_cpq(v3) = v6))) % 21.07/3.57 | % 21.07/3.57 | ALPHA: (l34_l35) implies: % 21.07/3.57 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.57 | ( ~ (update_slb(v0, v1) = v2) | ~ (strictly_less_than(v3, v4) = 0) | % 21.07/3.57 | ~ $i(v4) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: % 21.07/3.57 | $i] : ? [v7: int] : ? [v8: int] : ? [v9: int] : ($i(v6) & % 21.07/3.57 | $i(v5) & ((v8 = 0 & v7 = 0 & pair_in_list(v2, v5, v6) = 0 & % 21.07/3.57 | strictly_less_than(v5, v6) = 0) | ( ~ (v9 = 0) & % 21.07/3.57 | pair_in_list(v0, v3, v4) = v9)))) % 21.07/3.57 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.58 | ( ~ (update_slb(v0, v1) = v2) | ~ (pair_in_list(v0, v3, v4) = 0) | ~ % 21.07/3.58 | $i(v4) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: % 21.07/3.58 | $i] : ? [v7: int] : ? [v8: int] : ? [v9: int] : ($i(v6) & % 21.07/3.58 | $i(v5) & ((v8 = 0 & v7 = 0 & pair_in_list(v2, v5, v6) = 0 & % 21.07/3.58 | strictly_less_than(v5, v6) = 0) | ( ~ (v9 = 0) & % 21.07/3.58 | strictly_less_than(v3, v4) = v9)))) % 21.07/3.58 | % 21.07/3.58 | ALPHA: (function-axioms) implies: % 21.07/3.58 | (19) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.07/3.58 | : (v1 = v0 | ~ (check_cpq(v2) = v1) | ~ (check_cpq(v2) = v0)) % 21.07/3.58 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 21.07/3.58 | (findmin_pqp_res(v2) = v1) | ~ (findmin_pqp_res(v2) = v0)) % 21.07/3.58 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.07/3.58 | : ! [v3: $i] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ % 21.07/3.58 | (less_than(v3, v2) = v0)) % 21.07/3.58 | (22) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.07/3.58 | : ! [v3: $i] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ % 21.07/3.58 | (strictly_less_than(v3, v2) = v0)) % 21.07/3.58 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.07/3.58 | : ! [v3: $i] : (v1 = v0 | ~ (contains_slb(v3, v2) = v1) | ~ % 21.07/3.58 | (contains_slb(v3, v2) = v0)) % 21.07/3.58 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.07/3.58 | (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = v0)) % 21.07/3.58 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.07/3.58 | (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) = v0)) % 21.07/3.58 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 21.07/3.58 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) % 21.07/3.58 | = v1) | ~ (pair_in_list(v4, v3, v2) = v0)) % 21.07/3.58 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.07/3.58 | (v1 = v0 | ~ (triple(v4, v3, v2) = v1) | ~ (triple(v4, v3, v2) = % 21.07/3.58 | v0)) % 21.07/3.58 | % 21.14/3.58 | DELTA: instantiating (l24_co) with fresh symbols all_48_0, all_48_1, all_48_2, % 21.14/3.58 | all_48_3, all_48_4, all_48_5 gives: % 21.14/3.58 | (28) ~ (all_48_1 = 0) & triple(all_48_5, all_48_4, all_48_3) = all_48_2 & % 21.14/3.58 | check_cpq(all_48_0) = 0 & check_cpq(all_48_2) = all_48_1 & % 21.14/3.58 | findmin_cpq_eff(all_48_2) = all_48_0 & $i(all_48_0) & $i(all_48_2) & % 21.14/3.58 | $i(all_48_3) & $i(all_48_4) & $i(all_48_5) % 21.14/3.58 | % 21.14/3.58 | ALPHA: (28) implies: % 21.14/3.58 | (29) ~ (all_48_1 = 0) % 21.14/3.58 | (30) $i(all_48_5) % 21.14/3.58 | (31) $i(all_48_4) % 21.14/3.58 | (32) $i(all_48_3) % 21.14/3.58 | (33) $i(all_48_2) % 21.14/3.58 | (34) findmin_cpq_eff(all_48_2) = all_48_0 % 21.14/3.58 | (35) check_cpq(all_48_2) = all_48_1 % 21.14/3.58 | (36) check_cpq(all_48_0) = 0 % 21.14/3.58 | (37) triple(all_48_5, all_48_4, all_48_3) = all_48_2 % 21.14/3.58 | % 21.14/3.58 | GROUND_INST: instantiating (14) with all_48_2, all_48_0, simplifying with % 21.14/3.58 | (33), (34) gives: % 21.14/3.58 | (38) ? [v0: $i] : ? [v1: $i] : (findmin_cpq_res(all_48_2) = v1 & % 21.14/3.58 | removemin_cpq_eff(all_48_2) = v0 & remove_cpq(all_48_0, v1) = v0 & % 21.14/3.58 | $i(v1) & $i(v0)) % 21.14/3.58 | % 21.14/3.58 | GROUND_INST: instantiating (11) with all_48_5, all_48_4, all_48_3, all_48_2, % 21.14/3.58 | all_48_0, simplifying with (30), (31), (32), (34), (37) gives: % 21.14/3.58 | (39) all_48_4 = create_slb | ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? % 21.14/3.58 | [v3: any] : ? [v4: $i] : ? [v5: $i] : (findmin_pqp_res(all_48_5) = % 21.14/3.58 | v0 & triple(all_48_5, v4, all_48_3) = v5 & update_slb(all_48_4, v0) % 21.14/3.58 | = v4 & lookup_slb(all_48_4, v0) = v2 & contains_slb(all_48_4, v0) = % 21.14/3.58 | v1 & less_than(v2, v0) = v3 & $i(v5) & $i(v4) & $i(v2) & $i(v0) & ( % 21.14/3.58 | ~ (v3 = 0) | ~ (v1 = 0) | v5 = all_48_0)) % 21.14/3.58 | % 21.14/3.58 | GROUND_INST: instantiating (10) with all_48_5, all_48_4, all_48_3, all_48_2, % 21.14/3.58 | all_48_0, simplifying with (30), (31), (32), (34), (37) gives: % 21.14/3.59 | (40) all_48_4 = create_slb | ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? % 21.14/3.59 | [v3: any] : ? [v4: $i] : ? [v5: $i] : (findmin_pqp_res(all_48_5) = % 21.14/3.59 | v0 & triple(all_48_5, v4, bad) = v5 & update_slb(all_48_4, v0) = v4 % 21.14/3.59 | & lookup_slb(all_48_4, v0) = v2 & contains_slb(all_48_4, v0) = v1 & % 21.14/3.59 | strictly_less_than(v0, v2) = v3 & $i(v5) & $i(v4) & $i(v2) & $i(v0) % 21.14/3.59 | & ( ~ (v3 = 0) | ~ (v1 = 0) | v5 = all_48_0)) % 21.14/3.59 | % 21.14/3.59 | GROUND_INST: instantiating (8) with all_48_5, all_48_4, all_48_3, all_48_2, % 21.14/3.59 | all_48_0, simplifying with (30), (31), (32), (34), (37) gives: % 21.14/3.59 | (41) all_48_4 = create_slb | ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? % 21.14/3.59 | [v3: $i] : (findmin_pqp_res(all_48_5) = v0 & triple(all_48_5, v2, bad) % 21.14/3.59 | = v3 & update_slb(all_48_4, v0) = v2 & contains_slb(all_48_4, v0) = % 21.14/3.59 | v1 & $i(v3) & $i(v2) & $i(v0) & (v3 = all_48_0 | v1 = 0)) % 21.14/3.59 | % 21.14/3.59 | GROUND_INST: instantiating (15) with all_48_5, all_48_4, all_48_3, all_48_2, % 21.14/3.59 | simplifying with (30), (31), (32), (37) gives: % 21.14/3.59 | (42) ? [v0: int] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ? [v4: int] % 21.14/3.59 | : ($i(v2) & $i(v1) & ((v3 = 0 & ~ (v4 = 0) & pair_in_list(all_48_4, % 21.14/3.59 | v1, v2) = 0 & less_than(v2, v1) = v4) | (v0 = 0 & % 21.14/3.59 | check_cpq(all_48_2) = 0))) % 21.14/3.59 | % 21.14/3.59 | DELTA: instantiating (38) with fresh symbols all_55_0, all_55_1 gives: % 21.14/3.59 | (43) findmin_cpq_res(all_48_2) = all_55_0 & removemin_cpq_eff(all_48_2) = % 21.14/3.59 | all_55_1 & remove_cpq(all_48_0, all_55_0) = all_55_1 & $i(all_55_0) & % 21.14/3.59 | $i(all_55_1) % 21.14/3.59 | % 21.14/3.59 | ALPHA: (43) implies: % 21.14/3.59 | (44) findmin_cpq_res(all_48_2) = all_55_0 % 21.14/3.59 | % 21.14/3.59 | DELTA: instantiating (42) with fresh symbols all_57_0, all_57_1, all_57_2, % 21.14/3.59 | all_57_3, all_57_4 gives: % 21.14/3.59 | (45) $i(all_57_2) & $i(all_57_3) & ((all_57_1 = 0 & ~ (all_57_0 = 0) & % 21.14/3.59 | pair_in_list(all_48_4, all_57_3, all_57_2) = 0 & % 21.14/3.59 | less_than(all_57_2, all_57_3) = all_57_0) | (all_57_4 = 0 & % 21.14/3.59 | check_cpq(all_48_2) = 0)) % 21.14/3.59 | % 21.14/3.59 | ALPHA: (45) implies: % 21.14/3.59 | (46) $i(all_57_3) % 21.14/3.59 | (47) $i(all_57_2) % 21.14/3.59 | (48) (all_57_1 = 0 & ~ (all_57_0 = 0) & pair_in_list(all_48_4, all_57_3, % 21.14/3.59 | all_57_2) = 0 & less_than(all_57_2, all_57_3) = all_57_0) | % 21.14/3.59 | (all_57_4 = 0 & check_cpq(all_48_2) = 0) % 21.14/3.59 | % 21.14/3.59 | BETA: splitting (48) gives: % 21.14/3.59 | % 21.14/3.59 | Case 1: % 21.14/3.59 | | % 21.14/3.59 | | (49) all_57_1 = 0 & ~ (all_57_0 = 0) & pair_in_list(all_48_4, all_57_3, % 21.14/3.59 | | all_57_2) = 0 & less_than(all_57_2, all_57_3) = all_57_0 % 21.14/3.59 | | % 21.14/3.59 | | ALPHA: (49) implies: % 21.14/3.59 | | (50) ~ (all_57_0 = 0) % 21.14/3.59 | | (51) less_than(all_57_2, all_57_3) = all_57_0 % 21.14/3.59 | | (52) pair_in_list(all_48_4, all_57_3, all_57_2) = 0 % 21.14/3.59 | | % 21.14/3.59 | | GROUND_INST: instantiating (1) with all_57_3, all_57_2, all_57_0, % 21.14/3.59 | | simplifying with (46), (47), (51) gives: % 21.14/3.59 | | (53) all_57_0 = 0 | less_than(all_57_3, all_57_2) = 0 % 21.14/3.59 | | % 21.14/3.59 | | GROUND_INST: instantiating (5) with all_57_3, all_57_2, all_57_0, % 21.14/3.59 | | simplifying with (46), (47), (51) gives: % 21.14/3.59 | | (54) all_57_0 = 0 | ? [v0: any] : ? [v1: any] : % 21.14/3.59 | | (strictly_less_than(all_57_3, all_57_2) = v1 & less_than(all_57_3, % 21.14/3.59 | | all_57_2) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 21.14/3.59 | | % 21.14/3.59 | | GROUND_INST: instantiating (4) with all_57_3, all_57_2, all_57_0, % 21.14/3.59 | | simplifying with (46), (47), (51) gives: % 21.14/3.59 | | (55) ? [v0: any] : ? [v1: any] : (strictly_less_than(all_57_3, % 21.14/3.59 | | all_57_2) = v0 & less_than(all_57_3, all_57_2) = v1 & ( ~ (v0 = % 21.14/3.59 | | 0) | (v1 = 0 & ~ (all_57_0 = 0)))) % 21.14/3.59 | | % 21.14/3.59 | | GROUND_INST: instantiating (3) with all_57_2, all_57_3, all_57_0, % 21.14/3.59 | | simplifying with (46), (47), (51) gives: % 21.14/3.59 | | (56) ? [v0: any] : ? [v1: any] : (strictly_less_than(all_57_2, % 21.14/3.59 | | all_57_3) = v0 & less_than(all_57_3, all_57_2) = v1 & ( ~ (v0 = % 21.14/3.59 | | 0) | (all_57_0 = 0 & ~ (v1 = 0)))) % 21.14/3.59 | | % 21.14/3.59 | | GROUND_INST: instantiating (13) with all_48_5, all_48_4, all_48_3, all_48_2, % 21.14/3.59 | | all_55_0, simplifying with (30), (31), (32), (37), (44) gives: % 21.14/3.59 | | (57) all_48_4 = create_slb | (findmin_pqp_res(all_48_5) = all_55_0 & % 21.14/3.59 | | $i(all_55_0)) % 21.14/3.59 | | % 21.14/3.59 | | DELTA: instantiating (56) with fresh symbols all_69_0, all_69_1 gives: % 21.14/3.59 | | (58) strictly_less_than(all_57_2, all_57_3) = all_69_1 & % 21.14/3.59 | | less_than(all_57_3, all_57_2) = all_69_0 & ( ~ (all_69_1 = 0) | % 21.14/3.59 | | (all_57_0 = 0 & ~ (all_69_0 = 0))) % 21.14/3.59 | | % 21.14/3.59 | | ALPHA: (58) implies: % 21.14/3.59 | | (59) less_than(all_57_3, all_57_2) = all_69_0 % 21.14/3.59 | | % 21.14/3.59 | | DELTA: instantiating (55) with fresh symbols all_71_0, all_71_1 gives: % 21.14/3.59 | | (60) strictly_less_than(all_57_3, all_57_2) = all_71_1 & % 21.14/3.59 | | less_than(all_57_3, all_57_2) = all_71_0 & ( ~ (all_71_1 = 0) | % 21.14/3.59 | | (all_71_0 = 0 & ~ (all_57_0 = 0))) % 21.14/3.59 | | % 21.14/3.59 | | ALPHA: (60) implies: % 21.14/3.60 | | (61) less_than(all_57_3, all_57_2) = all_71_0 % 21.14/3.60 | | (62) strictly_less_than(all_57_3, all_57_2) = all_71_1 % 21.14/3.60 | | % 21.14/3.60 | | BETA: splitting (53) gives: % 21.14/3.60 | | % 21.14/3.60 | | Case 1: % 21.14/3.60 | | | % 21.14/3.60 | | | (63) less_than(all_57_3, all_57_2) = 0 % 21.14/3.60 | | | % 21.14/3.60 | | | GROUND_INST: instantiating (21) with all_69_0, all_71_0, all_57_2, % 21.14/3.60 | | | all_57_3, simplifying with (59), (61) gives: % 21.14/3.60 | | | (64) all_71_0 = all_69_0 % 21.14/3.60 | | | % 21.14/3.60 | | | GROUND_INST: instantiating (21) with 0, all_71_0, all_57_2, all_57_3, % 21.14/3.60 | | | simplifying with (61), (63) gives: % 21.14/3.60 | | | (65) all_71_0 = 0 % 21.14/3.60 | | | % 21.14/3.60 | | | COMBINE_EQS: (64), (65) imply: % 21.14/3.60 | | | (66) all_69_0 = 0 % 21.14/3.60 | | | % 21.14/3.60 | | | SIMP: (66) implies: % 21.14/3.60 | | | (67) all_69_0 = 0 % 21.14/3.60 | | | % 21.14/3.60 | | | BETA: splitting (54) gives: % 21.14/3.60 | | | % 21.14/3.60 | | | Case 1: % 21.14/3.60 | | | | % 21.14/3.60 | | | | (68) all_57_0 = 0 % 21.14/3.60 | | | | % 21.14/3.60 | | | | REDUCE: (50), (68) imply: % 21.14/3.60 | | | | (69) $false % 21.14/3.60 | | | | % 21.14/3.60 | | | | CLOSE: (69) is inconsistent. % 21.14/3.60 | | | | % 21.14/3.60 | | | Case 2: % 21.14/3.60 | | | | % 21.14/3.60 | | | | (70) ? [v0: any] : ? [v1: any] : (strictly_less_than(all_57_3, % 21.14/3.60 | | | | all_57_2) = v1 & less_than(all_57_3, all_57_2) = v0 & ( ~ % 21.14/3.60 | | | | (v0 = 0) | v1 = 0)) % 21.14/3.60 | | | | % 21.14/3.60 | | | | DELTA: instantiating (70) with fresh symbols all_89_0, all_89_1 gives: % 21.14/3.60 | | | | (71) strictly_less_than(all_57_3, all_57_2) = all_89_0 & % 21.14/3.60 | | | | less_than(all_57_3, all_57_2) = all_89_1 & ( ~ (all_89_1 = 0) | % 21.14/3.60 | | | | all_89_0 = 0) % 21.14/3.60 | | | | % 21.14/3.60 | | | | ALPHA: (71) implies: % 21.14/3.60 | | | | (72) less_than(all_57_3, all_57_2) = all_89_1 % 21.14/3.60 | | | | (73) strictly_less_than(all_57_3, all_57_2) = all_89_0 % 21.14/3.60 | | | | (74) ~ (all_89_1 = 0) | all_89_0 = 0 % 21.14/3.60 | | | | % 21.14/3.60 | | | | GROUND_INST: instantiating (21) with 0, all_89_1, all_57_2, all_57_3, % 21.14/3.60 | | | | simplifying with (63), (72) gives: % 21.14/3.60 | | | | (75) all_89_1 = 0 % 21.14/3.60 | | | | % 21.14/3.60 | | | | GROUND_INST: instantiating (22) with all_71_1, all_89_0, all_57_2, % 21.14/3.60 | | | | all_57_3, simplifying with (62), (73) gives: % 21.14/3.60 | | | | (76) all_89_0 = all_71_1 % 21.14/3.60 | | | | % 21.14/3.60 | | | | BETA: splitting (74) gives: % 21.14/3.60 | | | | % 21.14/3.60 | | | | Case 1: % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | (77) ~ (all_89_1 = 0) % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | REDUCE: (75), (77) imply: % 21.14/3.60 | | | | | (78) $false % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | CLOSE: (78) is inconsistent. % 21.14/3.60 | | | | | % 21.14/3.60 | | | | Case 2: % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | (79) all_89_0 = 0 % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | COMBINE_EQS: (76), (79) imply: % 21.14/3.60 | | | | | (80) all_71_1 = 0 % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | REDUCE: (62), (80) imply: % 21.14/3.60 | | | | | (81) strictly_less_than(all_57_3, all_57_2) = 0 % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | BETA: splitting (39) gives: % 21.14/3.60 | | | | | % 21.14/3.60 | | | | | Case 1: % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | (82) all_48_4 = create_slb % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | REDUCE: (37), (82) imply: % 21.14/3.60 | | | | | | (83) triple(all_48_5, create_slb, all_48_3) = all_48_2 % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | GROUND_INST: instantiating (7) with all_48_5, all_48_3, all_48_2, % 21.14/3.60 | | | | | | simplifying with (30), (32), (83) gives: % 21.14/3.60 | | | | | | (84) check_cpq(all_48_2) = 0 % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | GROUND_INST: instantiating (19) with all_48_1, 0, all_48_2, % 21.14/3.60 | | | | | | simplifying with (35), (84) gives: % 21.14/3.60 | | | | | | (85) all_48_1 = 0 % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | REDUCE: (29), (85) imply: % 21.14/3.60 | | | | | | (86) $false % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | CLOSE: (86) is inconsistent. % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | Case 2: % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | (87) ~ (all_48_4 = create_slb) % 21.14/3.60 | | | | | | (88) ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? [v3: any] : ? % 21.14/3.60 | | | | | | [v4: $i] : ? [v5: $i] : (findmin_pqp_res(all_48_5) = v0 & % 21.14/3.60 | | | | | | triple(all_48_5, v4, all_48_3) = v5 & update_slb(all_48_4, % 21.14/3.60 | | | | | | v0) = v4 & lookup_slb(all_48_4, v0) = v2 & % 21.14/3.60 | | | | | | contains_slb(all_48_4, v0) = v1 & less_than(v2, v0) = v3 & % 21.14/3.60 | | | | | | $i(v5) & $i(v4) & $i(v2) & $i(v0) & ( ~ (v3 = 0) | ~ (v1 % 21.14/3.60 | | | | | | = 0) | v5 = all_48_0)) % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | DELTA: instantiating (88) with fresh symbols all_106_0, all_106_1, % 21.14/3.60 | | | | | | all_106_2, all_106_3, all_106_4, all_106_5 gives: % 21.14/3.60 | | | | | | (89) findmin_pqp_res(all_48_5) = all_106_5 & triple(all_48_5, % 21.14/3.60 | | | | | | all_106_1, all_48_3) = all_106_0 & update_slb(all_48_4, % 21.14/3.60 | | | | | | all_106_5) = all_106_1 & lookup_slb(all_48_4, all_106_5) = % 21.14/3.60 | | | | | | all_106_3 & contains_slb(all_48_4, all_106_5) = all_106_4 & % 21.14/3.60 | | | | | | less_than(all_106_3, all_106_5) = all_106_2 & $i(all_106_0) % 21.14/3.60 | | | | | | & $i(all_106_1) & $i(all_106_3) & $i(all_106_5) & ( ~ % 21.14/3.60 | | | | | | (all_106_2 = 0) | ~ (all_106_4 = 0) | all_106_0 = % 21.14/3.60 | | | | | | all_48_0) % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | ALPHA: (89) implies: % 21.14/3.60 | | | | | | (90) $i(all_106_5) % 21.14/3.60 | | | | | | (91) less_than(all_106_3, all_106_5) = all_106_2 % 21.14/3.60 | | | | | | (92) contains_slb(all_48_4, all_106_5) = all_106_4 % 21.14/3.60 | | | | | | (93) lookup_slb(all_48_4, all_106_5) = all_106_3 % 21.14/3.60 | | | | | | (94) update_slb(all_48_4, all_106_5) = all_106_1 % 21.14/3.60 | | | | | | (95) triple(all_48_5, all_106_1, all_48_3) = all_106_0 % 21.14/3.60 | | | | | | (96) findmin_pqp_res(all_48_5) = all_106_5 % 21.14/3.60 | | | | | | (97) ~ (all_106_2 = 0) | ~ (all_106_4 = 0) | all_106_0 = % 21.14/3.60 | | | | | | all_48_0 % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | BETA: splitting (57) gives: % 21.14/3.60 | | | | | | % 21.14/3.60 | | | | | | Case 1: % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | | (98) all_48_4 = create_slb % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | | REDUCE: (87), (98) imply: % 21.14/3.60 | | | | | | | (99) $false % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | | CLOSE: (99) is inconsistent. % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | Case 2: % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | | (100) findmin_pqp_res(all_48_5) = all_55_0 & $i(all_55_0) % 21.14/3.60 | | | | | | | % 21.14/3.60 | | | | | | | ALPHA: (100) implies: % 21.14/3.61 | | | | | | | (101) findmin_pqp_res(all_48_5) = all_55_0 % 21.14/3.61 | | | | | | | % 21.14/3.61 | | | | | | | BETA: splitting (41) gives: % 21.14/3.61 | | | | | | | % 21.14/3.61 | | | | | | | Case 1: % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | (102) all_48_4 = create_slb % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | REDUCE: (87), (102) imply: % 21.14/3.61 | | | | | | | | (103) $false % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | CLOSE: (103) is inconsistent. % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | Case 2: % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | (104) ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] % 21.14/3.61 | | | | | | | | : (findmin_pqp_res(all_48_5) = v0 & triple(all_48_5, % 21.14/3.61 | | | | | | | | v2, bad) = v3 & update_slb(all_48_4, v0) = v2 & % 21.14/3.61 | | | | | | | | contains_slb(all_48_4, v0) = v1 & $i(v3) & $i(v2) & % 21.14/3.61 | | | | | | | | $i(v0) & (v3 = all_48_0 | v1 = 0)) % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | DELTA: instantiating (104) with fresh symbols all_115_0, % 21.14/3.61 | | | | | | | | all_115_1, all_115_2, all_115_3 gives: % 21.14/3.61 | | | | | | | | (105) findmin_pqp_res(all_48_5) = all_115_3 & % 21.14/3.61 | | | | | | | | triple(all_48_5, all_115_1, bad) = all_115_0 & % 21.14/3.61 | | | | | | | | update_slb(all_48_4, all_115_3) = all_115_1 & % 21.14/3.61 | | | | | | | | contains_slb(all_48_4, all_115_3) = all_115_2 & % 21.14/3.61 | | | | | | | | $i(all_115_0) & $i(all_115_1) & $i(all_115_3) & % 21.14/3.61 | | | | | | | | (all_115_0 = all_48_0 | all_115_2 = 0) % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | ALPHA: (105) implies: % 21.14/3.61 | | | | | | | | (106) $i(all_115_1) % 21.14/3.61 | | | | | | | | (107) contains_slb(all_48_4, all_115_3) = all_115_2 % 21.14/3.61 | | | | | | | | (108) update_slb(all_48_4, all_115_3) = all_115_1 % 21.14/3.61 | | | | | | | | (109) triple(all_48_5, all_115_1, bad) = all_115_0 % 21.14/3.61 | | | | | | | | (110) findmin_pqp_res(all_48_5) = all_115_3 % 21.14/3.61 | | | | | | | | (111) all_115_0 = all_48_0 | all_115_2 = 0 % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | BETA: splitting (40) gives: % 21.14/3.61 | | | | | | | | % 21.14/3.61 | | | | | | | | Case 1: % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | (112) all_48_4 = create_slb % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (87), (112) imply: % 21.14/3.61 | | | | | | | | | (113) $false % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | CLOSE: (113) is inconsistent. % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | Case 2: % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | (114) ? [v0: $i] : ? [v1: any] : ? [v2: $i] : ? [v3: % 21.14/3.61 | | | | | | | | | any] : ? [v4: $i] : ? [v5: $i] : % 21.14/3.61 | | | | | | | | | (findmin_pqp_res(all_48_5) = v0 & triple(all_48_5, % 21.14/3.61 | | | | | | | | | v4, bad) = v5 & update_slb(all_48_4, v0) = v4 & % 21.14/3.61 | | | | | | | | | lookup_slb(all_48_4, v0) = v2 & % 21.14/3.61 | | | | | | | | | contains_slb(all_48_4, v0) = v1 & % 21.14/3.61 | | | | | | | | | strictly_less_than(v0, v2) = v3 & $i(v5) & $i(v4) & % 21.14/3.61 | | | | | | | | | $i(v2) & $i(v0) & ( ~ (v3 = 0) | ~ (v1 = 0) | v5 = % 21.14/3.61 | | | | | | | | | all_48_0)) % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | DELTA: instantiating (114) with fresh symbols all_120_0, % 21.14/3.61 | | | | | | | | | all_120_1, all_120_2, all_120_3, all_120_4, all_120_5 % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (115) findmin_pqp_res(all_48_5) = all_120_5 & % 21.14/3.61 | | | | | | | | | triple(all_48_5, all_120_1, bad) = all_120_0 & % 21.14/3.61 | | | | | | | | | update_slb(all_48_4, all_120_5) = all_120_1 & % 21.14/3.61 | | | | | | | | | lookup_slb(all_48_4, all_120_5) = all_120_3 & % 21.14/3.61 | | | | | | | | | contains_slb(all_48_4, all_120_5) = all_120_4 & % 21.14/3.61 | | | | | | | | | strictly_less_than(all_120_5, all_120_3) = all_120_2 % 21.14/3.61 | | | | | | | | | & $i(all_120_0) & $i(all_120_1) & $i(all_120_3) & % 21.14/3.61 | | | | | | | | | $i(all_120_5) & ( ~ (all_120_2 = 0) | ~ (all_120_4 = % 21.14/3.61 | | | | | | | | | 0) | all_120_0 = all_48_0) % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | ALPHA: (115) implies: % 21.14/3.61 | | | | | | | | | (116) $i(all_120_3) % 21.14/3.61 | | | | | | | | | (117) strictly_less_than(all_120_5, all_120_3) = all_120_2 % 21.14/3.61 | | | | | | | | | (118) contains_slb(all_48_4, all_120_5) = all_120_4 % 21.14/3.61 | | | | | | | | | (119) lookup_slb(all_48_4, all_120_5) = all_120_3 % 21.14/3.61 | | | | | | | | | (120) update_slb(all_48_4, all_120_5) = all_120_1 % 21.14/3.61 | | | | | | | | | (121) triple(all_48_5, all_120_1, bad) = all_120_0 % 21.14/3.61 | | | | | | | | | (122) findmin_pqp_res(all_48_5) = all_120_5 % 21.14/3.61 | | | | | | | | | (123) ~ (all_120_2 = 0) | ~ (all_120_4 = 0) | all_120_0 = % 21.14/3.61 | | | | | | | | | all_48_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (20) with all_106_5, all_115_3, % 21.14/3.61 | | | | | | | | | all_48_5, simplifying with (96), (110) gives: % 21.14/3.61 | | | | | | | | | (124) all_115_3 = all_106_5 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (20) with all_115_3, all_120_5, % 21.14/3.61 | | | | | | | | | all_48_5, simplifying with (110), (122) gives: % 21.14/3.61 | | | | | | | | | (125) all_120_5 = all_115_3 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (20) with all_55_0, all_120_5, % 21.14/3.61 | | | | | | | | | all_48_5, simplifying with (101), (122) gives: % 21.14/3.61 | | | | | | | | | (126) all_120_5 = all_55_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | COMBINE_EQS: (125), (126) imply: % 21.14/3.61 | | | | | | | | | (127) all_115_3 = all_55_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | SIMP: (127) implies: % 21.14/3.61 | | | | | | | | | (128) all_115_3 = all_55_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | COMBINE_EQS: (124), (128) imply: % 21.14/3.61 | | | | | | | | | (129) all_106_5 = all_55_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (120), (126) imply: % 21.14/3.61 | | | | | | | | | (130) update_slb(all_48_4, all_55_0) = all_120_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (108), (128) imply: % 21.14/3.61 | | | | | | | | | (131) update_slb(all_48_4, all_55_0) = all_115_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (94), (129) imply: % 21.14/3.61 | | | | | | | | | (132) update_slb(all_48_4, all_55_0) = all_106_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (119), (126) imply: % 21.14/3.61 | | | | | | | | | (133) lookup_slb(all_48_4, all_55_0) = all_120_3 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (93), (129) imply: % 21.14/3.61 | | | | | | | | | (134) lookup_slb(all_48_4, all_55_0) = all_106_3 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (118), (126) imply: % 21.14/3.61 | | | | | | | | | (135) contains_slb(all_48_4, all_55_0) = all_120_4 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (107), (128) imply: % 21.14/3.61 | | | | | | | | | (136) contains_slb(all_48_4, all_55_0) = all_115_2 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (92), (129) imply: % 21.14/3.61 | | | | | | | | | (137) contains_slb(all_48_4, all_55_0) = all_106_4 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (117), (126) imply: % 21.14/3.61 | | | | | | | | | (138) strictly_less_than(all_55_0, all_120_3) = all_120_2 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (91), (129) imply: % 21.14/3.61 | | | | | | | | | (139) less_than(all_106_3, all_55_0) = all_106_2 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (90), (129) imply: % 21.14/3.61 | | | | | | | | | (140) $i(all_55_0) % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (23) with all_115_2, all_120_4, % 21.14/3.61 | | | | | | | | | all_55_0, all_48_4, simplifying with (135), (136) % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (141) all_120_4 = all_115_2 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (23) with all_106_4, all_120_4, % 21.14/3.61 | | | | | | | | | all_55_0, all_48_4, simplifying with (135), (137) % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (142) all_120_4 = all_106_4 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (24) with all_106_3, all_120_3, % 21.14/3.61 | | | | | | | | | all_55_0, all_48_4, simplifying with (133), (134) % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (143) all_120_3 = all_106_3 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (25) with all_115_1, all_120_1, % 21.14/3.61 | | | | | | | | | all_55_0, all_48_4, simplifying with (130), (131) % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (144) all_120_1 = all_115_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | GROUND_INST: instantiating (25) with all_106_1, all_120_1, % 21.14/3.61 | | | | | | | | | all_55_0, all_48_4, simplifying with (130), (132) % 21.14/3.61 | | | | | | | | | gives: % 21.14/3.61 | | | | | | | | | (145) all_120_1 = all_106_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | COMBINE_EQS: (144), (145) imply: % 21.14/3.61 | | | | | | | | | (146) all_115_1 = all_106_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | SIMP: (146) implies: % 21.14/3.61 | | | | | | | | | (147) all_115_1 = all_106_1 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | COMBINE_EQS: (141), (142) imply: % 21.14/3.61 | | | | | | | | | (148) all_115_2 = all_106_4 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | SIMP: (148) implies: % 21.14/3.61 | | | | | | | | | (149) all_115_2 = all_106_4 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (121), (145) imply: % 21.14/3.61 | | | | | | | | | (150) triple(all_48_5, all_106_1, bad) = all_120_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.61 | | | | | | | | | REDUCE: (109), (147) imply: % 21.14/3.61 | | | | | | | | | (151) triple(all_48_5, all_106_1, bad) = all_115_0 % 21.14/3.61 | | | | | | | | | % 21.14/3.62 | | | | | | | | | REDUCE: (138), (143) imply: % 21.14/3.62 | | | | | | | | | (152) strictly_less_than(all_55_0, all_106_3) = all_120_2 % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | REDUCE: (116), (143) imply: % 21.14/3.62 | | | | | | | | | (153) $i(all_106_3) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | REDUCE: (106), (147) imply: % 21.14/3.62 | | | | | | | | | (154) $i(all_106_1) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (27) with all_115_0, all_120_0, bad, % 21.14/3.62 | | | | | | | | | all_106_1, all_48_5, simplifying with (150), (151) % 21.14/3.62 | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | (155) all_120_0 = all_115_0 % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (1) with all_55_0, all_106_3, % 21.14/3.62 | | | | | | | | | all_106_2, simplifying with (139), (140), (153) % 21.14/3.62 | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | (156) all_106_2 = 0 | less_than(all_55_0, all_106_3) = 0 % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (5) with all_55_0, all_106_3, % 21.14/3.62 | | | | | | | | | all_106_2, simplifying with (139), (140), (153) % 21.14/3.62 | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | (157) all_106_2 = 0 | ? [v0: any] : ? [v1: any] : % 21.14/3.62 | | | | | | | | | (strictly_less_than(all_55_0, all_106_3) = v1 & % 21.14/3.62 | | | | | | | | | less_than(all_55_0, all_106_3) = v0 & ( ~ (v0 = 0) % 21.14/3.62 | | | | | | | | | | v1 = 0)) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (6) with all_55_0, all_106_3, % 21.14/3.62 | | | | | | | | | all_120_2, simplifying with (140), (152), (153) % 21.14/3.62 | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | (158) all_120_2 = 0 | ? [v0: any] : ? [v1: any] : % 21.14/3.62 | | | | | | | | | (less_than(all_106_3, all_55_0) = v1 & % 21.14/3.62 | | | | | | | | | less_than(all_55_0, all_106_3) = v0 & ( ~ (v0 = 0) % 21.14/3.62 | | | | | | | | | | v1 = 0)) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (18) with all_48_4, all_55_0, % 21.14/3.62 | | | | | | | | | all_106_1, all_57_3, all_57_2, simplifying with % 21.14/3.62 | | | | | | | | | (31), (46), (47), (52), (132), (140) gives: % 21.14/3.62 | | | | | | | | | (159) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ? [v3: % 21.14/3.62 | | | | | | | | | int] : ? [v4: int] : ($i(v1) & $i(v0) & ((v3 = 0 & % 21.14/3.62 | | | | | | | | | v2 = 0 & pair_in_list(all_106_1, v0, v1) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(v0, v1) = 0) | ( ~ (v4 = 0) % 21.14/3.62 | | | | | | | | | & strictly_less_than(all_57_3, all_57_2) = % 21.14/3.62 | | | | | | | | | v4))) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (17) with all_48_4, all_55_0, % 21.14/3.62 | | | | | | | | | all_106_1, all_57_3, all_57_2, simplifying with % 21.14/3.62 | | | | | | | | | (31), (46), (47), (81), (132), (140) gives: % 21.14/3.62 | | | | | | | | | (160) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ? [v3: % 21.14/3.62 | | | | | | | | | int] : ? [v4: int] : ($i(v1) & $i(v0) & ((v3 = 0 & % 21.14/3.62 | | | | | | | | | v2 = 0 & pair_in_list(all_106_1, v0, v1) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(v0, v1) = 0) | ( ~ (v4 = 0) % 21.14/3.62 | | | | | | | | | & pair_in_list(all_48_4, all_57_3, all_57_2) = % 21.14/3.62 | | | | | | | | | v4))) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | GROUND_INST: instantiating (12) with all_48_5, all_48_4, bad, % 21.14/3.62 | | | | | | | | | all_55_0, all_106_1, all_115_0, simplifying with % 21.14/3.62 | | | | | | | | | (9), (30), (31), (101), (132), (151) gives: % 21.14/3.62 | | | | | | | | | (161) all_48_4 = create_slb | ? [v0: any] : ? [v1: $i] : % 21.14/3.62 | | | | | | | | | ? [v2: any] : ? [v3: $i] : ? [v4: $i] : % 21.14/3.62 | | | | | | | | | (triple(all_48_5, all_48_4, bad) = v3 & % 21.14/3.62 | | | | | | | | | findmin_cpq_eff(v3) = v4 & lookup_slb(all_48_4, % 21.14/3.62 | | | | | | | | | all_55_0) = v1 & contains_slb(all_48_4, all_55_0) % 21.14/3.62 | | | | | | | | | = v0 & less_than(v1, all_55_0) = v2 & $i(v4) & % 21.14/3.62 | | | | | | | | | $i(v3) & $i(v1) & ( ~ (v2 = 0) | ~ (v0 = 0) | v4 = % 21.14/3.62 | | | | | | | | | all_115_0)) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | DELTA: instantiating (160) with fresh symbols all_147_0, % 21.14/3.62 | | | | | | | | | all_147_1, all_147_2, all_147_3, all_147_4 gives: % 21.14/3.62 | | | | | | | | | (162) $i(all_147_3) & $i(all_147_4) & ((all_147_1 = 0 & % 21.14/3.62 | | | | | | | | | all_147_2 = 0 & pair_in_list(all_106_1, % 21.14/3.62 | | | | | | | | | all_147_4, all_147_3) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(all_147_4, all_147_3) = 0) | ( % 21.14/3.62 | | | | | | | | | ~ (all_147_0 = 0) & pair_in_list(all_48_4, % 21.14/3.62 | | | | | | | | | all_57_3, all_57_2) = all_147_0)) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | ALPHA: (162) implies: % 21.14/3.62 | | | | | | | | | (163) (all_147_1 = 0 & all_147_2 = 0 & % 21.14/3.62 | | | | | | | | | pair_in_list(all_106_1, all_147_4, all_147_3) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(all_147_4, all_147_3) = 0) | ( ~ % 21.14/3.62 | | | | | | | | | (all_147_0 = 0) & pair_in_list(all_48_4, all_57_3, % 21.14/3.62 | | | | | | | | | all_57_2) = all_147_0) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | DELTA: instantiating (159) with fresh symbols all_149_0, % 21.14/3.62 | | | | | | | | | all_149_1, all_149_2, all_149_3, all_149_4 gives: % 21.14/3.62 | | | | | | | | | (164) $i(all_149_3) & $i(all_149_4) & ((all_149_1 = 0 & % 21.14/3.62 | | | | | | | | | all_149_2 = 0 & pair_in_list(all_106_1, % 21.14/3.62 | | | | | | | | | all_149_4, all_149_3) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(all_149_4, all_149_3) = 0) | ( % 21.14/3.62 | | | | | | | | | ~ (all_149_0 = 0) & strictly_less_than(all_57_3, % 21.14/3.62 | | | | | | | | | all_57_2) = all_149_0)) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | ALPHA: (164) implies: % 21.14/3.62 | | | | | | | | | (165) $i(all_149_4) % 21.14/3.62 | | | | | | | | | (166) $i(all_149_3) % 21.14/3.62 | | | | | | | | | (167) (all_149_1 = 0 & all_149_2 = 0 & % 21.14/3.62 | | | | | | | | | pair_in_list(all_106_1, all_149_4, all_149_3) = 0 & % 21.14/3.62 | | | | | | | | | strictly_less_than(all_149_4, all_149_3) = 0) | ( ~ % 21.14/3.62 | | | | | | | | | (all_149_0 = 0) & strictly_less_than(all_57_3, % 21.14/3.62 | | | | | | | | | all_57_2) = all_149_0) % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | BETA: splitting (167) gives: % 21.14/3.62 | | | | | | | | | % 21.14/3.62 | | | | | | | | | Case 1: % 21.14/3.62 | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | (168) all_149_1 = 0 & all_149_2 = 0 & % 21.14/3.62 | | | | | | | | | | pair_in_list(all_106_1, all_149_4, all_149_3) = 0 & % 21.14/3.62 | | | | | | | | | | strictly_less_than(all_149_4, all_149_3) = 0 % 21.14/3.62 | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | ALPHA: (168) implies: % 21.14/3.62 | | | | | | | | | | (169) strictly_less_than(all_149_4, all_149_3) = 0 % 21.14/3.62 | | | | | | | | | | (170) pair_in_list(all_106_1, all_149_4, all_149_3) = 0 % 21.14/3.62 | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | BETA: splitting (161) gives: % 21.14/3.62 | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | Case 1: % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | (171) all_48_4 = create_slb % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | REDUCE: (87), (171) imply: % 21.14/3.62 | | | | | | | | | | | (172) $false % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | CLOSE: (172) is inconsistent. % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | Case 2: % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | (173) ? [v0: any] : ? [v1: $i] : ? [v2: any] : ? % 21.14/3.62 | | | | | | | | | | | [v3: $i] : ? [v4: $i] : (triple(all_48_5, % 21.14/3.62 | | | | | | | | | | | all_48_4, bad) = v3 & findmin_cpq_eff(v3) = v4 % 21.14/3.62 | | | | | | | | | | | & lookup_slb(all_48_4, all_55_0) = v1 & % 21.14/3.62 | | | | | | | | | | | contains_slb(all_48_4, all_55_0) = v0 & % 21.14/3.62 | | | | | | | | | | | less_than(v1, all_55_0) = v2 & $i(v4) & $i(v3) & % 21.14/3.62 | | | | | | | | | | | $i(v1) & ( ~ (v2 = 0) | ~ (v0 = 0) | v4 = % 21.14/3.62 | | | | | | | | | | | all_115_0)) % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | DELTA: instantiating (173) with fresh symbols all_160_0, % 21.14/3.62 | | | | | | | | | | | all_160_1, all_160_2, all_160_3, all_160_4 gives: % 21.14/3.62 | | | | | | | | | | | (174) triple(all_48_5, all_48_4, bad) = all_160_1 & % 21.14/3.62 | | | | | | | | | | | findmin_cpq_eff(all_160_1) = all_160_0 & % 21.14/3.62 | | | | | | | | | | | lookup_slb(all_48_4, all_55_0) = all_160_3 & % 21.14/3.62 | | | | | | | | | | | contains_slb(all_48_4, all_55_0) = all_160_4 & % 21.14/3.62 | | | | | | | | | | | less_than(all_160_3, all_55_0) = all_160_2 & % 21.14/3.62 | | | | | | | | | | | $i(all_160_0) & $i(all_160_1) & $i(all_160_3) & ( % 21.14/3.62 | | | | | | | | | | | ~ (all_160_2 = 0) | ~ (all_160_4 = 0) | % 21.14/3.62 | | | | | | | | | | | all_160_0 = all_115_0) % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | ALPHA: (174) implies: % 21.14/3.62 | | | | | | | | | | | (175) less_than(all_160_3, all_55_0) = all_160_2 % 21.14/3.62 | | | | | | | | | | | (176) lookup_slb(all_48_4, all_55_0) = all_160_3 % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | BETA: splitting (163) gives: % 21.14/3.62 | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | Case 1: % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | GROUND_INST: instantiating (24) with all_106_3, all_160_3, % 21.14/3.62 | | | | | | | | | | | | all_55_0, all_48_4, simplifying with (134), (176) % 21.14/3.62 | | | | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | | | | (177) all_160_3 = all_106_3 % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | REDUCE: (175), (177) imply: % 21.14/3.62 | | | | | | | | | | | | (178) less_than(all_106_3, all_55_0) = all_160_2 % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_106_2, all_160_2, % 21.14/3.62 | | | | | | | | | | | | all_55_0, all_106_3, simplifying with (139), (178) % 21.14/3.62 | | | | | | | | | | | | gives: % 21.14/3.62 | | | | | | | | | | | | (179) all_160_2 = all_106_2 % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | GROUND_INST: instantiating (2) with all_149_4, all_149_3, % 21.14/3.62 | | | | | | | | | | | | simplifying with (165), (166), (169) gives: % 21.14/3.62 | | | | | | | | | | | | (180) ? [v0: int] : ( ~ (v0 = 0) & less_than(all_149_3, % 21.14/3.62 | | | | | | | | | | | | all_149_4) = v0 & less_than(all_149_4, % 21.14/3.62 | | | | | | | | | | | | all_149_3) = 0) % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_48_5, all_106_1, % 21.14/3.62 | | | | | | | | | | | | all_48_3, all_106_0, all_149_4, all_149_3, % 21.14/3.62 | | | | | | | | | | | | simplifying with (30), (32), (95), (154), (165), % 21.14/3.62 | | | | | | | | | | | | (166), (170) gives: % 21.14/3.62 | | | | | | | | | | | | (181) ? [v0: int] : ((v0 = 0 & less_than(all_149_3, % 21.14/3.62 | | | | | | | | | | | | all_149_4) = 0) | ( ~ (v0 = 0) & % 21.14/3.62 | | | | | | | | | | | | check_cpq(all_106_0) = v0)) % 21.14/3.62 | | | | | | | | | | | | % 21.14/3.62 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_48_5, all_106_1, bad, % 21.14/3.62 | | | | | | | | | | | | all_115_0, all_149_4, all_149_3, simplifying with % 21.14/3.62 | | | | | | | | | | | | (9), (30), (151), (154), (165), (166), (170) % 21.14/3.63 | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | (182) ? [v0: int] : ((v0 = 0 & less_than(all_149_3, % 21.14/3.63 | | | | | | | | | | | | all_149_4) = 0) | ( ~ (v0 = 0) & % 21.14/3.63 | | | | | | | | | | | | check_cpq(all_115_0) = v0)) % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | DELTA: instantiating (180) with fresh symbol all_189_0 % 21.14/3.63 | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | (183) ~ (all_189_0 = 0) & less_than(all_149_3, % 21.14/3.63 | | | | | | | | | | | | all_149_4) = all_189_0 & less_than(all_149_4, % 21.14/3.63 | | | | | | | | | | | | all_149_3) = 0 % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | ALPHA: (183) implies: % 21.14/3.63 | | | | | | | | | | | | (184) ~ (all_189_0 = 0) % 21.14/3.63 | | | | | | | | | | | | (185) less_than(all_149_3, all_149_4) = all_189_0 % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | DELTA: instantiating (182) with fresh symbol all_193_0 % 21.14/3.63 | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | (186) (all_193_0 = 0 & less_than(all_149_3, all_149_4) = % 21.14/3.63 | | | | | | | | | | | | 0) | ( ~ (all_193_0 = 0) & check_cpq(all_115_0) % 21.14/3.63 | | | | | | | | | | | | = all_193_0) % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | DELTA: instantiating (181) with fresh symbol all_194_0 % 21.14/3.63 | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | (187) (all_194_0 = 0 & less_than(all_149_3, all_149_4) = % 21.14/3.63 | | | | | | | | | | | | 0) | ( ~ (all_194_0 = 0) & check_cpq(all_106_0) % 21.14/3.63 | | | | | | | | | | | | = all_194_0) % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | BETA: splitting (186) gives: % 21.14/3.63 | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | (188) all_193_0 = 0 & less_than(all_149_3, all_149_4) = % 21.14/3.63 | | | | | | | | | | | | | 0 % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | ALPHA: (188) implies: % 21.14/3.63 | | | | | | | | | | | | | (189) less_than(all_149_3, all_149_4) = 0 % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | REF_CLOSE: (21), (184), (185), (189) are inconsistent by % 21.14/3.63 | | | | | | | | | | | | | sub-proof #2. % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | (190) ~ (all_193_0 = 0) & check_cpq(all_115_0) = % 21.14/3.63 | | | | | | | | | | | | | all_193_0 % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | ALPHA: (190) implies: % 21.14/3.63 | | | | | | | | | | | | | (191) ~ (all_193_0 = 0) % 21.14/3.63 | | | | | | | | | | | | | (192) check_cpq(all_115_0) = all_193_0 % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | BETA: splitting (187) gives: % 21.14/3.63 | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | (193) all_194_0 = 0 & less_than(all_149_3, all_149_4) = % 21.14/3.63 | | | | | | | | | | | | | | 0 % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | ALPHA: (193) implies: % 21.14/3.63 | | | | | | | | | | | | | | (194) less_than(all_149_3, all_149_4) = 0 % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | REF_CLOSE: (21), (184), (185), (194) are inconsistent by % 21.14/3.63 | | | | | | | | | | | | | | sub-proof #2. % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | (195) ~ (all_194_0 = 0) & check_cpq(all_106_0) = % 21.14/3.63 | | | | | | | | | | | | | | all_194_0 % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | ALPHA: (195) implies: % 21.14/3.63 | | | | | | | | | | | | | | (196) ~ (all_194_0 = 0) % 21.14/3.63 | | | | | | | | | | | | | | (197) check_cpq(all_106_0) = all_194_0 % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | BETA: splitting (97) gives: % 21.14/3.63 | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | (198) ~ (all_106_2 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | BETA: splitting (156) gives: % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | (199) less_than(all_55_0, all_106_3) = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | BETA: splitting (157) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | (200) all_106_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | REDUCE: (198), (200) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | (201) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | CLOSE: (201) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | (202) ? [v0: any] : ? [v1: any] : % 21.14/3.63 | | | | | | | | | | | | | | | | | (strictly_less_than(all_55_0, all_106_3) = v1 & % 21.14/3.63 | | | | | | | | | | | | | | | | | less_than(all_55_0, all_106_3) = v0 & ( ~ (v0 = % 21.14/3.63 | | | | | | | | | | | | | | | | | 0) | v1 = 0)) % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | DELTA: instantiating (202) with fresh symbols all_433_0, % 21.14/3.63 | | | | | | | | | | | | | | | | | all_433_1 gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | (203) strictly_less_than(all_55_0, all_106_3) = % 21.14/3.63 | | | | | | | | | | | | | | | | | all_433_0 & less_than(all_55_0, all_106_3) = % 21.14/3.63 | | | | | | | | | | | | | | | | | all_433_1 & ( ~ (all_433_1 = 0) | all_433_0 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | ALPHA: (203) implies: % 21.14/3.63 | | | | | | | | | | | | | | | | | (204) less_than(all_55_0, all_106_3) = all_433_1 % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | BETA: splitting (158) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | (205) all_120_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | BETA: splitting (111) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (206) all_115_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (149), (206) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (207) all_106_4 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (142), (207) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (208) all_120_4 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | BETA: splitting (123) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | (209) ~ (all_120_2 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | REDUCE: (205), (209) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | (210) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | CLOSE: (210) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | (211) ~ (all_120_4 = 0) | all_120_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | BETA: splitting (211) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | (212) ~ (all_120_4 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | REDUCE: (208), (212) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | (213) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | CLOSE: (213) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | (214) all_120_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (155), (214) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | (215) all_115_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | REDUCE: (192), (215) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | (216) check_cpq(all_48_0) = all_193_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (19), (36), (191), (216) are inconsistent by % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | sub-proof #1. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (217) all_115_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | REDUCE: (192), (217) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (218) check_cpq(all_48_0) = all_193_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | REF_CLOSE: (19), (36), (191), (218) are inconsistent by % 21.14/3.63 | | | | | | | | | | | | | | | | | | | sub-proof #1. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | (219) ? [v0: any] : ? [v1: any] : % 21.14/3.63 | | | | | | | | | | | | | | | | | | (less_than(all_106_3, all_55_0) = v1 & % 21.14/3.63 | | | | | | | | | | | | | | | | | | less_than(all_55_0, all_106_3) = v0 & ( ~ (v0 = % 21.14/3.63 | | | | | | | | | | | | | | | | | | 0) | v1 = 0)) % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | DELTA: instantiating (219) with fresh symbols all_439_0, % 21.14/3.63 | | | | | | | | | | | | | | | | | | all_439_1 gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (220) less_than(all_106_3, all_55_0) = all_439_0 & % 21.14/3.63 | | | | | | | | | | | | | | | | | | less_than(all_55_0, all_106_3) = all_439_1 & ( ~ % 21.14/3.63 | | | | | | | | | | | | | | | | | | (all_439_1 = 0) | all_439_0 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | ALPHA: (220) implies: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (221) less_than(all_55_0, all_106_3) = all_439_1 % 21.14/3.63 | | | | | | | | | | | | | | | | | | (222) less_than(all_106_3, all_55_0) = all_439_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | (223) ~ (all_439_1 = 0) | all_439_0 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_433_1, all_439_1, % 21.14/3.63 | | | | | | | | | | | | | | | | | | all_106_3, all_55_0, simplifying with (204), (221) % 21.14/3.63 | | | | | | | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (224) all_439_1 = all_433_1 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with 0, all_439_1, all_106_3, % 21.14/3.63 | | | | | | | | | | | | | | | | | | all_55_0, simplifying with (199), (221) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (225) all_439_1 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_106_2, all_439_0, % 21.14/3.63 | | | | | | | | | | | | | | | | | | all_55_0, all_106_3, simplifying with (139), (222) % 21.14/3.63 | | | | | | | | | | | | | | | | | | gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (226) all_439_0 = all_106_2 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (224), (225) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | (227) all_433_1 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | BETA: splitting (223) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (228) ~ (all_439_1 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | REDUCE: (225), (228) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (229) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | CLOSE: (229) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (230) all_439_0 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (226), (230) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (231) all_106_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | REDUCE: (198), (231) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | | | (232) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | | CLOSE: (232) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | (233) all_106_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | REDUCE: (198), (233) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | (234) $false % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | CLOSE: (234) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | End of split % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | (235) ~ (all_106_4 = 0) | all_106_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | BETA: splitting (111) gives: % 21.14/3.63 | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | (236) all_115_2 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | COMBINE_EQS: (149), (236) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | (237) all_106_4 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | SIMP: (237) implies: % 21.14/3.63 | | | | | | | | | | | | | | | | (238) all_106_4 = 0 % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | BETA: splitting (235) gives: % 21.14/3.63 | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | Case 1: % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | (239) ~ (all_106_4 = 0) % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | REDUCE: (238), (239) imply: % 21.14/3.63 | | | | | | | | | | | | | | | | | (240) $false % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | CLOSE: (240) is inconsistent. % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | Case 2: % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | (241) all_106_0 = all_48_0 % 21.14/3.63 | | | | | | | | | | | | | | | | | % 21.14/3.63 | | | | | | | | | | | | | | | | | REDUCE: (197), (241) imply: % 21.14/3.64 | | | | | | | | | | | | | | | | | (242) check_cpq(all_48_0) = all_194_0 % 21.14/3.64 | | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (19) with 0, all_194_0, all_48_0, % 21.14/3.64 | | | | | | | | | | | | | | | | | simplifying with (36), (242) gives: % 21.14/3.64 | | | | | | | | | | | | | | | | | (243) all_194_0 = 0 % 21.14/3.64 | | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | | REDUCE: (196), (243) imply: % 21.14/3.64 | | | | | | | | | | | | | | | | | (244) $false % 21.14/3.64 | | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | | CLOSE: (244) is inconsistent. % 21.14/3.64 | | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | Case 2: % 21.14/3.64 | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | (245) all_115_0 = all_48_0 % 21.14/3.64 | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | REDUCE: (192), (245) imply: % 21.14/3.64 | | | | | | | | | | | | | | | | (246) check_cpq(all_48_0) = all_193_0 % 21.14/3.64 | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | | REF_CLOSE: (19), (36), (191), (246) are inconsistent by % 21.14/3.64 | | | | | | | | | | | | | | | | sub-proof #1. % 21.14/3.64 | | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | Case 2: % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | (247) ~ (all_147_0 = 0) & pair_in_list(all_48_4, % 21.14/3.64 | | | | | | | | | | | | all_57_3, all_57_2) = all_147_0 % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | ALPHA: (247) implies: % 21.14/3.64 | | | | | | | | | | | | (248) ~ (all_147_0 = 0) % 21.14/3.64 | | | | | | | | | | | | (249) pair_in_list(all_48_4, all_57_3, all_57_2) = % 21.14/3.64 | | | | | | | | | | | | all_147_0 % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | GROUND_INST: instantiating (26) with 0, all_147_0, all_57_2, % 21.14/3.64 | | | | | | | | | | | | all_57_3, all_48_4, simplifying with (52), (249) % 21.14/3.64 | | | | | | | | | | | | gives: % 21.14/3.64 | | | | | | | | | | | | (250) all_147_0 = 0 % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | REDUCE: (248), (250) imply: % 21.14/3.64 | | | | | | | | | | | | (251) $false % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | | CLOSE: (251) is inconsistent. % 21.14/3.64 | | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | Case 2: % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | (252) ~ (all_149_0 = 0) & strictly_less_than(all_57_3, % 21.14/3.64 | | | | | | | | | | all_57_2) = all_149_0 % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | ALPHA: (252) implies: % 21.14/3.64 | | | | | | | | | | (253) ~ (all_149_0 = 0) % 21.14/3.64 | | | | | | | | | | (254) strictly_less_than(all_57_3, all_57_2) = all_149_0 % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | GROUND_INST: instantiating (22) with 0, all_149_0, all_57_2, % 21.14/3.64 | | | | | | | | | | all_57_3, simplifying with (81), (254) gives: % 21.14/3.64 | | | | | | | | | | (255) all_149_0 = 0 % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | REDUCE: (253), (255) imply: % 21.14/3.64 | | | | | | | | | | (256) $false % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | | CLOSE: (256) is inconsistent. % 21.14/3.64 | | | | | | | | | | % 21.14/3.64 | | | | | | | | | End of split % 21.14/3.64 | | | | | | | | | % 21.14/3.64 | | | | | | | | End of split % 21.14/3.64 | | | | | | | | % 21.14/3.64 | | | | | | | End of split % 21.14/3.64 | | | | | | | % 21.14/3.64 | | | | | | End of split % 21.14/3.64 | | | | | | % 21.14/3.64 | | | | | End of split % 21.14/3.64 | | | | | % 21.14/3.64 | | | | End of split % 21.14/3.64 | | | | % 21.14/3.64 | | | End of split % 21.14/3.64 | | | % 21.14/3.64 | | Case 2: % 21.14/3.64 | | | % 21.14/3.64 | | | (257) all_57_0 = 0 % 21.14/3.64 | | | % 21.14/3.64 | | | REDUCE: (50), (257) imply: % 21.14/3.64 | | | (258) $false % 21.14/3.64 | | | % 21.14/3.64 | | | CLOSE: (258) is inconsistent. % 21.14/3.64 | | | % 21.14/3.64 | | End of split % 21.14/3.64 | | % 21.14/3.64 | Case 2: % 21.14/3.64 | | % 21.14/3.64 | | (259) all_57_4 = 0 & check_cpq(all_48_2) = 0 % 21.14/3.64 | | % 21.14/3.64 | | ALPHA: (259) implies: % 21.14/3.64 | | (260) check_cpq(all_48_2) = 0 % 21.14/3.64 | | % 21.14/3.64 | | GROUND_INST: instantiating (19) with all_48_1, 0, all_48_2, simplifying with % 21.14/3.64 | | (35), (260) gives: % 21.14/3.64 | | (261) all_48_1 = 0 % 21.14/3.64 | | % 21.14/3.64 | | REDUCE: (29), (261) imply: % 21.14/3.64 | | (262) $false % 21.14/3.64 | | % 21.14/3.64 | | CLOSE: (262) is inconsistent. % 21.14/3.64 | | % 21.14/3.64 | End of split % 21.14/3.64 | % 21.14/3.64 End of proof % 21.14/3.64 % 21.14/3.64 Sub-proof #1 shows that the following formulas are inconsistent: % 21.14/3.64 ---------------------------------------------------------------- % 21.14/3.64 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 21.14/3.64 (v1 = v0 | ~ (check_cpq(v2) = v1) | ~ (check_cpq(v2) = v0)) % 21.14/3.64 (2) check_cpq(all_48_0) = all_193_0 % 21.14/3.64 (3) check_cpq(all_48_0) = 0 % 21.14/3.64 (4) ~ (all_193_0 = 0) % 21.14/3.64 % 21.14/3.64 Begin of proof % 21.14/3.64 | % 21.14/3.64 | GROUND_INST: instantiating (1) with 0, all_193_0, all_48_0, simplifying with % 21.14/3.64 | (2), (3) gives: % 21.14/3.64 | (5) all_193_0 = 0 % 21.14/3.64 | % 21.14/3.64 | REDUCE: (4), (5) imply: % 21.14/3.64 | (6) $false % 21.14/3.64 | % 21.14/3.64 | CLOSE: (6) is inconsistent. % 21.14/3.64 | % 21.14/3.64 End of proof % 21.14/3.64 % 21.14/3.64 Sub-proof #2 shows that the following formulas are inconsistent: % 21.14/3.64 ---------------------------------------------------------------- % 21.14/3.64 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 21.14/3.64 ! [v3: $i] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ (less_than(v3, % 21.14/3.64 v2) = v0)) % 21.14/3.64 (2) less_than(all_149_3, all_149_4) = all_189_0 % 21.14/3.64 (3) less_than(all_149_3, all_149_4) = 0 % 21.14/3.64 (4) ~ (all_189_0 = 0) % 21.14/3.64 % 21.14/3.64 Begin of proof % 21.14/3.64 | % 21.14/3.64 | GROUND_INST: instantiating (1) with 0, all_189_0, all_149_4, all_149_3, % 21.14/3.64 | simplifying with (2), (3) gives: % 21.14/3.64 | (5) all_189_0 = 0 % 21.14/3.64 | % 21.14/3.64 | REDUCE: (4), (5) imply: % 21.14/3.64 | (6) $false % 21.14/3.64 | % 21.14/3.64 | CLOSE: (6) is inconsistent. % 21.14/3.64 | % 21.14/3.64 End of proof % 21.14/3.64 % SZS output end Proof for theBenchmark % 21.14/3.64 % 21.14/3.64 3027ms %------------------------------------------------------------------------------