%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM925+1 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n022.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 11:50:50 EDT 2023 % Result : Theorem 13.86s 2.75s % Output : Proof 24.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM925+1 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.34 % Computer : n022.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Fri Aug 25 08:19:25 EDT 2023 % 0.15/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.52/1.24 Prover 4: Preprocessing ... % 3.52/1.25 Prover 1: Preprocessing ... % 3.92/1.29 Prover 5: Preprocessing ... % 3.92/1.29 Prover 3: Preprocessing ... % 3.92/1.29 Prover 2: Preprocessing ... % 3.92/1.29 Prover 6: Preprocessing ... % 3.92/1.29 Prover 0: Preprocessing ... % 11.74/2.42 Prover 3: Constructing countermodel ... % 12.03/2.43 Prover 6: Constructing countermodel ... % 12.11/2.48 Prover 1: Constructing countermodel ... % 12.61/2.53 Prover 5: Proving ... % 12.61/2.53 Prover 0: Proving ... % 13.07/2.57 Prover 4: Constructing countermodel ... % 13.07/2.60 Prover 2: Proving ... % 13.86/2.74 Prover 3: proved (2103ms) % 13.86/2.75 % 13.86/2.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.86/2.75 % 13.86/2.75 Prover 6: stopped % 13.86/2.76 Prover 2: stopped % 13.86/2.77 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 13.86/2.77 Prover 5: stopped % 13.86/2.78 Prover 0: stopped % 13.86/2.78 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.86/2.78 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 13.86/2.78 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 13.86/2.78 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.86/2.88 Prover 10: Preprocessing ... % 15.38/2.91 Prover 7: Preprocessing ... % 15.38/2.92 Prover 8: Preprocessing ... % 15.38/2.92 Prover 11: Preprocessing ... % 15.38/2.94 Prover 13: Preprocessing ... % 17.68/3.22 Prover 10: Warning: ignoring some quantifiers % 17.68/3.24 Prover 10: Constructing countermodel ... % 18.05/3.29 Prover 7: Warning: ignoring some quantifiers % 18.05/3.30 Prover 8: Warning: ignoring some quantifiers % 18.05/3.31 Prover 7: Constructing countermodel ... % 18.05/3.32 Prover 8: Constructing countermodel ... % 18.73/3.37 Prover 13: Warning: ignoring some quantifiers % 18.73/3.40 Prover 13: Constructing countermodel ... % 18.73/3.41 Prover 11: Constructing countermodel ... % 22.62/3.89 Prover 1: Found proof (size 306) % 22.62/3.89 Prover 1: proved (3255ms) % 22.62/3.89 Prover 10: stopped % 22.62/3.89 Prover 7: stopped % 22.62/3.89 Prover 11: stopped % 22.62/3.90 Prover 4: stopped % 22.62/3.90 Prover 13: stopped % 22.62/3.90 Prover 8: stopped % 22.62/3.90 % 22.62/3.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 22.62/3.90 % 22.99/4.02 % SZS output start Proof for theBenchmark % 22.99/4.02 Assumptions after simplification: % 22.99/4.02 --------------------------------- % 22.99/4.03 % 22.99/4.03 (conj_0) % 22.99/4.05 $i(pls) & $i(n) & $i(one_one_int) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: % 22.99/4.05 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (bit1(pls) = v2 & bit0(v2) = % 22.99/4.05 v3 & number_number_of_nat(v3) = v4 & power_power_int(v1, v4) = zero_zero_int % 22.99/4.05 & semiri1621563631at_int(n) = v0 & plus_plus_int(one_one_int, v0) = v1 & % 22.99/4.05 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.05 % 22.99/4.05 (fact_0_n1pos) % 22.99/4.05 $i(n) & $i(one_one_int) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : % 22.99/4.05 (semiri1621563631at_int(n) = v0 & plus_plus_int(one_one_int, v0) = v1 & % 22.99/4.05 ord_less_int(zero_zero_int, v1) = 0 & $i(v1) & $i(v0)) % 22.99/4.05 % 22.99/4.05 (fact_103_zero__less__power2) % 22.99/4.06 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.06 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & % 22.99/4.06 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : (v3 = zero_zero_int | ~ % 22.99/4.06 (power_power_int(v3, v2) = v4) | ~ $i(v3) | ord_less_int(zero_zero_int, % 22.99/4.06 v4) = 0) & ! [v3: $i] : ( ~ (power_power_int(zero_zero_int, v2) = v3) | % 22.99/4.06 ? [v4: int] : ( ~ (v4 = 0) & ord_less_int(zero_zero_int, v3) = v4))) % 22.99/4.06 % 22.99/4.06 (fact_104_power2__less__0) % 22.99/4.06 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.06 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & % 22.99/4.06 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ( ~ (power_power_int(v3, v2) = % 22.99/4.06 v4) | ~ $i(v3) | ? [v5: int] : ( ~ (v5 = 0) & ord_less_int(v4, % 22.99/4.06 zero_zero_int) = v5))) % 22.99/4.06 % 22.99/4.06 (fact_105_sum__power2__gt__zero__iff) % 22.99/4.06 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.06 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & % 22.99/4.06 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 22.99/4.06 [v7: $i] : ( ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) % 22.99/4.06 = v5) | ~ (plus_plus_int(v5, v6) = v7) | ~ $i(v4) | ~ $i(v3) | % 22.99/4.06 ord_less_int(zero_zero_int, v7) = 0 | (v4 = zero_zero_int & v3 = % 22.99/4.06 zero_zero_int)) & ! [v3: $i] : ! [v4: $i] : ( ~ % 22.99/4.06 (power_power_int(zero_zero_int, v2) = v3) | ~ (plus_plus_int(v3, v3) = % 22.99/4.06 v4) | ? [v5: int] : ( ~ (v5 = 0) & ord_less_int(zero_zero_int, v4) = % 22.99/4.06 v5))) % 22.99/4.06 % 22.99/4.06 (fact_10_one__add__one__is__two) % 22.99/4.07 $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.07 (number_number_of_int(v2) = v0 & bit1(pls) = v1 & bit0(v1) = v2 & % 22.99/4.07 plus_plus_int(one_one_int, one_one_int) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_11_semiring__one__add__one__is__two) % 22.99/4.07 $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.07 (number_number_of_int(v2) = v0 & bit1(pls) = v1 & bit0(v1) = v2 & % 22.99/4.07 plus_plus_int(one_one_int, one_one_int) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_12_semiring__one__add__one__is__two) % 22.99/4.07 $i(one_one_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.07 (plus_plus_nat(one_one_nat, one_one_nat) = v0 & bit1(pls) = v1 & bit0(v1) = v2 % 22.99/4.07 & number_number_of_nat(v2) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_13_quartic__square__square) % 22.99/4.07 $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 22.99/4.07 : (bit1(pls) = v0 & bit0(v1) = v3 & bit0(v0) = v1 & number_number_of_nat(v3) = % 22.99/4.07 v4 & number_number_of_nat(v1) = v2 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 22.99/4.07 $i(v0) & ! [v5: $i] : ! [v6: $i] : ( ~ (power_power_int(v5, v4) = v6) | ~ % 22.99/4.07 $i(v5) | ? [v7: $i] : (power_power_int(v7, v2) = v6 & power_power_int(v5, % 22.99/4.07 v2) = v7 & $i(v7) & $i(v6)))) % 22.99/4.07 % 22.99/4.07 (fact_16_semiring__norm_I110_J) % 22.99/4.07 $i(pls) & $i(one_one_int) & ? [v0: $i] : (number_number_of_int(v0) = % 22.99/4.07 one_one_int & bit1(pls) = v0 & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_17_numeral__1__eq__1) % 22.99/4.07 $i(pls) & $i(one_one_int) & ? [v0: $i] : (number_number_of_int(v0) = % 22.99/4.07 one_one_int & bit1(pls) = v0 & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_2_sum__power2__eq__zero__iff) % 22.99/4.07 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.07 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & % 22.99/4.07 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( % 22.99/4.07 ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = v5) | ~ % 22.99/4.07 (plus_plus_int(v5, v6) = zero_zero_int) | ~ $i(v4) | ~ $i(v3) | (v4 = % 22.99/4.07 zero_zero_int & v3 = zero_zero_int)) & ! [v3: $i] : ! [v4: $i] : (v4 = % 22.99/4.07 zero_zero_int | ~ (power_power_int(zero_zero_int, v2) = v3) | ~ % 22.99/4.07 (plus_plus_int(v3, v3) = v4))) % 22.99/4.07 % 22.99/4.07 (fact_33_nat__1__add__1) % 22.99/4.07 $i(one_one_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.07 (plus_plus_nat(one_one_nat, one_one_nat) = v0 & bit1(pls) = v1 & bit0(v1) = v2 % 22.99/4.07 & number_number_of_nat(v2) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.07 % 22.99/4.07 (fact_36_rel__simps_I2_J) % 22.99/4.07 $i(pls) & ? [v0: int] : ( ~ (v0 = 0) & ord_less_int(pls, pls) = v0) % 22.99/4.07 % 22.99/4.07 (fact_3_one__power2) % 22.99/4.08 $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.08 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & % 22.99/4.08 power_power_int(one_one_int, v2) = one_one_int & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_41_one__is__num__one) % 22.99/4.08 $i(pls) & $i(one_one_int) & ? [v0: $i] : (number_number_of_int(v0) = % 22.99/4.08 one_one_int & bit1(pls) = v0 & $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_42_nat__numeral__1__eq__1) % 22.99/4.08 $i(one_one_nat) & $i(pls) & ? [v0: $i] : (bit1(pls) = v0 & % 22.99/4.08 number_number_of_nat(v0) = one_one_nat & $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_43_Numeral1__eq1__nat) % 22.99/4.08 $i(one_one_nat) & $i(pls) & ? [v0: $i] : (bit1(pls) = v0 & % 22.99/4.08 number_number_of_nat(v0) = one_one_nat & $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_4_one__power2) % 22.99/4.08 $i(one_one_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.08 (power_power_nat(one_one_nat, v2) = one_one_nat & bit1(pls) = v0 & bit0(v0) = % 22.99/4.08 v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_52_zadd__commute) % 22.99/4.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (plus_plus_int(v0, v1) = v2) | % 22.99/4.08 ~ $i(v1) | ~ $i(v0) | (plus_plus_int(v1, v0) = v2 & $i(v2))) % 22.99/4.08 % 22.99/4.08 (fact_5_zero__power2) % 22.99/4.08 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.08 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & % 22.99/4.08 power_power_int(zero_zero_int, v2) = zero_zero_int & $i(v2) & $i(v1) & % 22.99/4.08 $i(v0)) % 22.99/4.08 % 22.99/4.08 (fact_62_bin__less__0__simps_I1_J) % 22.99/4.08 $i(pls) & $i(zero_zero_int) & ? [v0: int] : ( ~ (v0 = 0) & ord_less_int(pls, % 22.99/4.08 zero_zero_int) = v0) % 22.99/4.08 % 22.99/4.08 (fact_67_less__special_I4_J) % 22.99/4.08 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 22.99/4.08 $i] : ! [v2: int] : (v2 = 0 | ~ (ord_less_int(v1, v0) = v2) | ~ $i(v1) % 22.99/4.08 | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & number_number_of_int(v1) = % 22.99/4.08 v3 & ord_less_int(v3, one_one_int) = v4 & $i(v3))) & ! [v1: $i] : ( ~ % 22.99/4.08 (ord_less_int(v1, v0) = 0) | ~ $i(v1) | ? [v2: $i] : % 22.99/4.08 (number_number_of_int(v1) = v2 & ord_less_int(v2, one_one_int) = 0 & % 22.99/4.08 $i(v2)))) % 22.99/4.08 % 22.99/4.08 (fact_68_less__special_I2_J) % 22.99/4.08 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 22.99/4.08 $i] : ! [v2: int] : (v2 = 0 | ~ (ord_less_int(v0, v1) = v2) | ~ $i(v1) % 22.99/4.08 | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & number_number_of_int(v1) = % 22.99/4.08 v3 & ord_less_int(one_one_int, v3) = v4 & $i(v3))) & ! [v1: $i] : ( ~ % 22.99/4.08 (ord_less_int(v0, v1) = 0) | ~ $i(v1) | ? [v2: $i] : % 22.99/4.08 (number_number_of_int(v1) = v2 & ord_less_int(one_one_int, v2) = 0 & % 22.99/4.08 $i(v2)))) % 22.99/4.08 % 22.99/4.08 (fact_6_zero__power2) % 22.99/4.09 $i(zero_zero_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.09 (power_power_nat(zero_zero_nat, v2) = zero_zero_nat & bit1(pls) = v0 & % 22.99/4.09 bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.09 % 22.99/4.09 (fact_78_Pls__def) % 22.99/4.09 pls = zero_zero_int & $i(zero_zero_int) % 22.99/4.09 % 22.99/4.09 (fact_7_zero__eq__power2) % 22.99/4.09 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.09 (bit1(pls) = v0 & bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & % 22.99/4.09 $i(v1) & $i(v0) & ! [v3: $i] : (v3 = zero_zero_int | ~ % 22.99/4.09 (power_power_int(v3, v2) = zero_zero_int) | ~ $i(v3)) & ! [v3: $i] : (v3 % 22.99/4.09 = zero_zero_int | ~ (power_power_int(zero_zero_int, v2) = v3))) % 22.99/4.09 % 22.99/4.09 (fact_8_add__special_I2_J) % 22.99/4.09 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 22.99/4.09 $i] : ! [v2: $i] : ( ~ (plus_plus_int(v0, v1) = v2) | ~ $i(v1) | ? [v3: % 22.99/4.09 $i] : ? [v4: $i] : (number_number_of_int(v2) = v4 & % 22.99/4.09 number_number_of_int(v1) = v3 & plus_plus_int(one_one_int, v3) = v4 & % 22.99/4.09 $i(v4) & $i(v3)))) % 22.99/4.09 % 22.99/4.09 (fact_92_power__eq__0__iff__number__of) % 22.99/4.09 $i(zero_zero_nat) & $i(zero_zero_int) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 22.99/4.09 $i] : (v2 = zero_zero_int | v1 = zero_zero_nat | ~ % 22.99/4.09 (number_number_of_nat(v0) = v1) | ~ (power_power_int(zero_zero_int, v1) = % 22.99/4.09 v2) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 22.99/4.09 (number_number_of_nat(v1) = v2) | ~ (power_power_int(v0, v2) = % 22.99/4.09 zero_zero_int) | ~ $i(v1) | ~ $i(v0) | (v0 = zero_zero_int & ~ (v2 = % 22.99/4.09 zero_zero_nat))) % 22.99/4.09 % 22.99/4.09 (fact_9_add__special_I3_J) % 22.99/4.09 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 22.99/4.09 $i] : ! [v2: $i] : ( ~ (plus_plus_int(v1, v0) = v2) | ~ $i(v1) | ? [v3: % 22.99/4.09 $i] : ? [v4: $i] : (number_number_of_int(v2) = v4 & % 22.99/4.09 number_number_of_int(v1) = v3 & plus_plus_int(v3, one_one_int) = v4 & % 22.99/4.09 $i(v4) & $i(v3)))) % 22.99/4.09 % 22.99/4.09 (function-axioms) % 22.99/4.09 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 22.99/4.09 [v3: $i] : (v1 = v0 | ~ (ord_less_nat(v3, v2) = v1) | ~ (ord_less_nat(v3, % 22.99/4.09 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 22.99/4.09 = v0 | ~ (plus_plus_nat(v3, v2) = v1) | ~ (plus_plus_nat(v3, v2) = v0)) & % 22.99/4.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.99/4.09 (power_power_nat(v3, v2) = v1) | ~ (power_power_nat(v3, v2) = v0)) & ! % 22.99/4.09 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.99/4.09 (power_power_int(v3, v2) = v1) | ~ (power_power_int(v3, v2) = v0)) & ! % 22.99/4.09 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.99/4.09 (plus_plus_int(v3, v2) = v1) | ~ (plus_plus_int(v3, v2) = v0)) & ! [v0: % 22.99/4.09 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 22.99/4.09 : (v1 = v0 | ~ (ord_less_int(v3, v2) = v1) | ~ (ord_less_int(v3, v2) = v0)) % 22.99/4.09 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.99/4.09 (semiri984289939at_nat(v2) = v1) | ~ (semiri984289939at_nat(v2) = v0)) & ! % 22.99/4.09 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (number_number_of_int(v2) % 22.99/4.09 = v1) | ~ (number_number_of_int(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 22.99/4.09 ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = v1) | ~ (bit1(v2) = v0)) & ! [v0: $i] % 22.99/4.09 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit0(v2) = v1) | ~ (bit0(v2) = % 22.99/4.09 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.99/4.09 (number_number_of_nat(v2) = v1) | ~ (number_number_of_nat(v2) = v0)) & ! % 22.99/4.09 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.99/4.09 (semiri1621563631at_int(v2) = v1) | ~ (semiri1621563631at_int(v2) = v0)) % 22.99/4.09 % 22.99/4.09 Further assumptions not needed in the proof: % 22.99/4.09 -------------------------------------------- % 22.99/4.10 fact_100_odd__nonzero, fact_101_number__of__int, fact_102_number__of__int, % 22.99/4.10 fact_14_power__0__left__number__of, fact_15_power__0__left__number__of, % 22.99/4.10 fact_18_n0, fact_19_zless__linear, fact_1_t1, % 22.99/4.10 fact_20_less__number__of__int__code, fact_21_plus__numeral__code_I9_J, % 22.99/4.10 fact_22_less__number__of, fact_23_zero__is__num__zero, fact_24_zpower__int, % 22.99/4.10 fact_25_int__power, fact_26_zadd__int__left, fact_27_zadd__int, fact_28_int__1, % 22.99/4.10 fact_29_nat__number__of__Pls, fact_30_semiring__norm_I113_J, % 22.99/4.10 fact_31_int__eq__0__conv, fact_32_int__0, fact_34_less__int__code_I16_J, % 22.99/4.10 fact_35_rel__simps_I17_J, fact_37_less__int__code_I13_J, % 22.99/4.10 fact_38_rel__simps_I14_J, fact_39_zadd__strict__right__mono, % 22.99/4.10 fact_40_add__nat__number__of, fact_44_eq__number__of, % 22.99/4.10 fact_45_number__of__reorient, fact_46_number__of__reorient, % 22.99/4.10 fact_47_rel__simps_I51_J, fact_48_rel__simps_I48_J, fact_49_even__less__0__iff, % 22.99/4.10 fact_50_zadd__assoc, fact_51_zadd__left__commute, fact_53_int__int__eq, % 22.99/4.10 fact_54_less__special_I3_J, fact_55_less__special_I1_J, % 22.99/4.10 fact_56_rel__simps_I12_J, fact_57_less__int__code_I15_J, % 22.99/4.10 fact_58_rel__simps_I16_J, fact_59_rel__simps_I10_J, fact_60_rel__simps_I4_J, % 22.99/4.10 fact_61_bin__less__0__simps_I4_J, fact_63_bin__less__0__simps_I3_J, % 22.99/4.10 fact_64_int__0__less__1, fact_65_zless__add1__eq, fact_66_int__less__0__conv, % 22.99/4.10 fact_69_odd__less__0, fact_70_double__eq__0__iff, fact_71_rel__simps_I46_J, % 22.99/4.10 fact_72_rel__simps_I39_J, fact_73_rel__simps_I50_J, fact_74_rel__simps_I49_J, % 22.99/4.10 fact_75_rel__simps_I44_J, fact_76_rel__simps_I38_J, fact_77_Bit0__Pls, % 22.99/4.10 fact_79_int__0__neq__1, fact_80_add__Pls__right, fact_81_add__Pls, % 22.99/4.10 fact_82_add__Bit0__Bit0, fact_83_Bit0__def, fact_84_zadd__0__right, % 22.99/4.10 fact_85_zadd__0, fact_86_semiring__numeral__0__eq__0, % 22.99/4.10 fact_87_semiring__numeral__0__eq__0, fact_88_number__of__Pls, % 22.99/4.10 fact_89_semiring__norm_I112_J, fact_90_add__numeral__0, % 22.99/4.10 fact_91_add__numeral__0__right, fact_93_power__eq__0__iff__number__of, % 22.99/4.10 fact_94_add__number__of__left, fact_95_add__number__of__eq, % 22.99/4.10 fact_96_number__of__add, fact_97_add__Bit1__Bit0, fact_98_add__Bit0__Bit1, % 22.99/4.10 fact_99_Bit1__def % 22.99/4.10 % 22.99/4.10 Those formulas are unsatisfiable: % 22.99/4.10 --------------------------------- % 22.99/4.10 % 22.99/4.10 Begin of proof % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_0_n1pos) implies: % 22.99/4.10 | (1) ? [v0: $i] : ? [v1: $i] : (semiri1621563631at_int(n) = v0 & % 22.99/4.10 | plus_plus_int(one_one_int, v0) = v1 & ord_less_int(zero_zero_int, v1) % 22.99/4.10 | = 0 & $i(v1) & $i(v0)) % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_2_sum__power2__eq__zero__iff) implies: % 22.99/4.10 | (2) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.10 | v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0) & ! % 22.99/4.10 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ % 22.99/4.10 | (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = v5) % 22.99/4.10 | | ~ (plus_plus_int(v5, v6) = zero_zero_int) | ~ $i(v4) | ~ % 22.99/4.10 | $i(v3) | (v4 = zero_zero_int & v3 = zero_zero_int)) & ! [v3: $i] : % 22.99/4.10 | ! [v4: $i] : (v4 = zero_zero_int | ~ % 22.99/4.10 | (power_power_int(zero_zero_int, v2) = v3) | ~ (plus_plus_int(v3, % 22.99/4.10 | v3) = v4))) % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_3_one__power2) implies: % 22.99/4.10 | (3) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.10 | v1 & number_number_of_nat(v1) = v2 & power_power_int(one_one_int, v2) % 22.99/4.10 | = one_one_int & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_4_one__power2) implies: % 22.99/4.10 | (4) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (power_power_nat(one_one_nat, % 22.99/4.10 | v2) = one_one_nat & bit1(pls) = v0 & bit0(v0) = v1 & % 22.99/4.10 | number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_5_zero__power2) implies: % 22.99/4.10 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.10 | v1 & number_number_of_nat(v1) = v2 & power_power_int(zero_zero_int, % 22.99/4.10 | v2) = zero_zero_int & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.10 | % 22.99/4.10 | ALPHA: (fact_6_zero__power2) implies: % 22.99/4.10 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.99/4.10 | (power_power_nat(zero_zero_nat, v2) = zero_zero_nat & bit1(pls) = v0 & % 22.99/4.11 | bit0(v0) = v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & % 22.99/4.11 | $i(v0)) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_7_zero__eq__power2) implies: % 22.99/4.11 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.11 | v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0) & ! % 22.99/4.11 | [v3: $i] : (v3 = zero_zero_int | ~ (power_power_int(v3, v2) = % 22.99/4.11 | zero_zero_int) | ~ $i(v3)) & ! [v3: $i] : (v3 = zero_zero_int | % 22.99/4.11 | ~ (power_power_int(zero_zero_int, v2) = v3))) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_8_add__special_I2_J) implies: % 22.99/4.11 | (8) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 22.99/4.11 | ~ (plus_plus_int(v0, v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: % 22.99/4.11 | $i] : (number_number_of_int(v2) = v4 & number_number_of_int(v1) = % 22.99/4.11 | v3 & plus_plus_int(one_one_int, v3) = v4 & $i(v4) & $i(v3)))) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_9_add__special_I3_J) implies: % 22.99/4.11 | (9) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 22.99/4.11 | ~ (plus_plus_int(v1, v0) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: % 22.99/4.11 | $i] : (number_number_of_int(v2) = v4 & number_number_of_int(v1) = % 22.99/4.11 | v3 & plus_plus_int(v3, one_one_int) = v4 & $i(v4) & $i(v3)))) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_11_semiring__one__add__one__is__two) implies: % 22.99/4.11 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_int(v2) = % 22.99/4.11 | v0 & bit1(pls) = v1 & bit0(v1) = v2 & plus_plus_int(one_one_int, % 22.99/4.11 | one_one_int) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_13_quartic__square__square) implies: % 22.99/4.11 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 22.99/4.11 | (bit1(pls) = v0 & bit0(v1) = v3 & bit0(v0) = v1 & % 22.99/4.11 | number_number_of_nat(v3) = v4 & number_number_of_nat(v1) = v2 & % 22.99/4.11 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: % 22.99/4.11 | $i] : ( ~ (power_power_int(v5, v4) = v6) | ~ $i(v5) | ? [v7: $i] % 22.99/4.11 | : (power_power_int(v7, v2) = v6 & power_power_int(v5, v2) = v7 & % 22.99/4.11 | $i(v7) & $i(v6)))) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_33_nat__1__add__1) implies: % 22.99/4.11 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (plus_plus_nat(one_one_nat, % 22.99/4.11 | one_one_nat) = v0 & bit1(pls) = v1 & bit0(v1) = v2 & % 22.99/4.11 | number_number_of_nat(v2) = v0 & $i(v2) & $i(v1) & $i(v0)) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_36_rel__simps_I2_J) implies: % 22.99/4.11 | (13) ? [v0: int] : ( ~ (v0 = 0) & ord_less_int(pls, pls) = v0) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_41_one__is__num__one) implies: % 22.99/4.11 | (14) ? [v0: $i] : (number_number_of_int(v0) = one_one_int & bit1(pls) = v0 % 22.99/4.11 | & $i(v0)) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_43_Numeral1__eq1__nat) implies: % 22.99/4.11 | (15) ? [v0: $i] : (bit1(pls) = v0 & number_number_of_nat(v0) = one_one_nat % 22.99/4.11 | & $i(v0)) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_62_bin__less__0__simps_I1_J) implies: % 22.99/4.11 | (16) ? [v0: int] : ( ~ (v0 = 0) & ord_less_int(pls, zero_zero_int) = v0) % 22.99/4.11 | % 22.99/4.11 | ALPHA: (fact_67_less__special_I4_J) implies: % 22.99/4.12 | (17) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: int] : % 22.99/4.12 | (v2 = 0 | ~ (ord_less_int(v1, v0) = v2) | ~ $i(v1) | ? [v3: $i] : % 22.99/4.12 | ? [v4: int] : ( ~ (v4 = 0) & number_number_of_int(v1) = v3 & % 22.99/4.12 | ord_less_int(v3, one_one_int) = v4 & $i(v3))) & ! [v1: $i] : ( % 22.99/4.12 | ~ (ord_less_int(v1, v0) = 0) | ~ $i(v1) | ? [v2: $i] : % 22.99/4.12 | (number_number_of_int(v1) = v2 & ord_less_int(v2, one_one_int) = 0 % 22.99/4.12 | & $i(v2)))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_68_less__special_I2_J) implies: % 22.99/4.12 | (18) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: int] : % 22.99/4.12 | (v2 = 0 | ~ (ord_less_int(v0, v1) = v2) | ~ $i(v1) | ? [v3: $i] : % 22.99/4.12 | ? [v4: int] : ( ~ (v4 = 0) & number_number_of_int(v1) = v3 & % 22.99/4.12 | ord_less_int(one_one_int, v3) = v4 & $i(v3))) & ! [v1: $i] : ( % 22.99/4.12 | ~ (ord_less_int(v0, v1) = 0) | ~ $i(v1) | ? [v2: $i] : % 22.99/4.12 | (number_number_of_int(v1) = v2 & ord_less_int(one_one_int, v2) = 0 % 22.99/4.12 | & $i(v2)))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_78_Pls__def) implies: % 22.99/4.12 | (19) pls = zero_zero_int % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_92_power__eq__0__iff__number__of) implies: % 22.99/4.12 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 22.99/4.12 | (number_number_of_nat(v1) = v2) | ~ (power_power_int(v0, v2) = % 22.99/4.12 | zero_zero_int) | ~ $i(v1) | ~ $i(v0) | (v0 = zero_zero_int & ~ % 22.99/4.12 | (v2 = zero_zero_nat))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_103_zero__less__power2) implies: % 22.99/4.12 | (21) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.12 | v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0) & ! % 22.99/4.12 | [v3: $i] : ! [v4: $i] : (v3 = zero_zero_int | ~ % 22.99/4.12 | (power_power_int(v3, v2) = v4) | ~ $i(v3) | % 22.99/4.12 | ord_less_int(zero_zero_int, v4) = 0) & ! [v3: $i] : ( ~ % 22.99/4.12 | (power_power_int(zero_zero_int, v2) = v3) | ? [v4: int] : ( ~ (v4 % 22.99/4.12 | = 0) & ord_less_int(zero_zero_int, v3) = v4))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_104_power2__less__0) implies: % 22.99/4.12 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.12 | v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0) & ! % 22.99/4.12 | [v3: $i] : ! [v4: $i] : ( ~ (power_power_int(v3, v2) = v4) | ~ % 22.99/4.12 | $i(v3) | ? [v5: int] : ( ~ (v5 = 0) & ord_less_int(v4, % 22.99/4.12 | zero_zero_int) = v5))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (fact_105_sum__power2__gt__zero__iff) implies: % 22.99/4.12 | (23) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (bit1(pls) = v0 & bit0(v0) = % 22.99/4.12 | v1 & number_number_of_nat(v1) = v2 & $i(v2) & $i(v1) & $i(v0) & ! % 22.99/4.12 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( % 22.99/4.12 | ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = % 22.99/4.12 | v5) | ~ (plus_plus_int(v5, v6) = v7) | ~ $i(v4) | ~ $i(v3) | % 22.99/4.12 | ord_less_int(zero_zero_int, v7) = 0 | (v4 = zero_zero_int & v3 = % 22.99/4.12 | zero_zero_int)) & ! [v3: $i] : ! [v4: $i] : ( ~ % 22.99/4.12 | (power_power_int(zero_zero_int, v2) = v3) | ~ (plus_plus_int(v3, % 22.99/4.12 | v3) = v4) | ? [v5: int] : ( ~ (v5 = 0) & % 22.99/4.12 | ord_less_int(zero_zero_int, v4) = v5))) % 22.99/4.12 | % 22.99/4.12 | ALPHA: (conj_0) implies: % 23.78/4.12 | (24) $i(one_one_int) % 23.78/4.13 | (25) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 23.78/4.13 | (bit1(pls) = v2 & bit0(v2) = v3 & number_number_of_nat(v3) = v4 & % 23.78/4.13 | power_power_int(v1, v4) = zero_zero_int & semiri1621563631at_int(n) % 23.78/4.13 | = v0 & plus_plus_int(one_one_int, v0) = v1 & $i(v4) & $i(v3) & % 23.78/4.13 | $i(v2) & $i(v1) & $i(v0)) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (function-axioms) implies: % 23.78/4.13 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 23.78/4.13 | (semiri1621563631at_int(v2) = v1) | ~ (semiri1621563631at_int(v2) = % 23.78/4.13 | v0)) % 23.78/4.13 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 23.78/4.13 | (number_number_of_nat(v2) = v1) | ~ (number_number_of_nat(v2) = % 23.78/4.13 | v0)) % 23.78/4.13 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit0(v2) = % 23.78/4.13 | v1) | ~ (bit0(v2) = v0)) % 23.78/4.13 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = % 23.78/4.13 | v1) | ~ (bit1(v2) = v0)) % 23.78/4.13 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.78/4.13 | : ! [v3: $i] : (v1 = v0 | ~ (ord_less_int(v3, v2) = v1) | ~ % 23.78/4.13 | (ord_less_int(v3, v2) = v0)) % 23.78/4.13 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.78/4.13 | (plus_plus_int(v3, v2) = v1) | ~ (plus_plus_int(v3, v2) = v0)) % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (16) with fresh symbol all_65_0 gives: % 23.78/4.13 | (32) ~ (all_65_0 = 0) & ord_less_int(pls, zero_zero_int) = all_65_0 % 23.78/4.13 | % 23.78/4.13 | ALPHA: (32) implies: % 23.78/4.13 | (33) ord_less_int(pls, zero_zero_int) = all_65_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (13) with fresh symbol all_67_0 gives: % 23.78/4.13 | (34) ~ (all_67_0 = 0) & ord_less_int(pls, pls) = all_67_0 % 23.78/4.13 | % 23.78/4.13 | ALPHA: (34) implies: % 23.78/4.13 | (35) ~ (all_67_0 = 0) % 23.78/4.13 | (36) ord_less_int(pls, pls) = all_67_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (14) with fresh symbol all_69_0 gives: % 23.78/4.13 | (37) number_number_of_int(all_69_0) = one_one_int & bit1(pls) = all_69_0 & % 23.78/4.13 | $i(all_69_0) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (37) implies: % 23.78/4.13 | (38) bit1(pls) = all_69_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (15) with fresh symbol all_73_0 gives: % 23.78/4.13 | (39) bit1(pls) = all_73_0 & number_number_of_nat(all_73_0) = one_one_nat & % 23.78/4.13 | $i(all_73_0) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (39) implies: % 23.78/4.13 | (40) bit1(pls) = all_73_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (14) with fresh symbol all_75_0 gives: % 23.78/4.13 | (41) number_number_of_int(all_75_0) = one_one_int & bit1(pls) = all_75_0 & % 23.78/4.13 | $i(all_75_0) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (41) implies: % 23.78/4.13 | (42) bit1(pls) = all_75_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (14) with fresh symbol all_77_0 gives: % 23.78/4.13 | (43) number_number_of_int(all_77_0) = one_one_int & bit1(pls) = all_77_0 & % 23.78/4.13 | $i(all_77_0) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (43) implies: % 23.78/4.13 | (44) bit1(pls) = all_77_0 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (1) with fresh symbols all_82_0, all_82_1 gives: % 23.78/4.13 | (45) semiri1621563631at_int(n) = all_82_1 & plus_plus_int(one_one_int, % 23.78/4.13 | all_82_1) = all_82_0 & ord_less_int(zero_zero_int, all_82_0) = 0 & % 23.78/4.13 | $i(all_82_0) & $i(all_82_1) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (45) implies: % 23.78/4.13 | (46) ord_less_int(zero_zero_int, all_82_0) = 0 % 23.78/4.13 | (47) plus_plus_int(one_one_int, all_82_1) = all_82_0 % 23.78/4.13 | (48) semiri1621563631at_int(n) = all_82_1 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (10) with fresh symbols all_87_0, all_87_1, all_87_2 % 23.78/4.13 | gives: % 23.78/4.13 | (49) number_number_of_int(all_87_0) = all_87_2 & bit1(pls) = all_87_1 & % 23.78/4.13 | bit0(all_87_1) = all_87_0 & plus_plus_int(one_one_int, one_one_int) = % 23.78/4.13 | all_87_2 & $i(all_87_0) & $i(all_87_1) & $i(all_87_2) % 23.78/4.13 | % 23.78/4.13 | ALPHA: (49) implies: % 23.78/4.13 | (50) bit0(all_87_1) = all_87_0 % 23.78/4.13 | (51) bit1(pls) = all_87_1 % 23.78/4.13 | % 23.78/4.13 | DELTA: instantiating (3) with fresh symbols all_89_0, all_89_1, all_89_2 % 23.78/4.13 | gives: % 23.78/4.14 | (52) bit1(pls) = all_89_2 & bit0(all_89_2) = all_89_1 & % 23.78/4.14 | number_number_of_nat(all_89_1) = all_89_0 & % 23.78/4.14 | power_power_int(one_one_int, all_89_0) = one_one_int & $i(all_89_0) & % 23.78/4.14 | $i(all_89_1) & $i(all_89_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (52) implies: % 23.78/4.14 | (53) $i(all_89_1) % 23.78/4.14 | (54) number_number_of_nat(all_89_1) = all_89_0 % 23.78/4.14 | (55) bit0(all_89_2) = all_89_1 % 23.78/4.14 | (56) bit1(pls) = all_89_2 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (10) with fresh symbols all_91_0, all_91_1, all_91_2 % 23.78/4.14 | gives: % 23.78/4.14 | (57) number_number_of_int(all_91_0) = all_91_2 & bit1(pls) = all_91_1 & % 23.78/4.14 | bit0(all_91_1) = all_91_0 & plus_plus_int(one_one_int, one_one_int) = % 23.78/4.14 | all_91_2 & $i(all_91_0) & $i(all_91_1) & $i(all_91_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (57) implies: % 23.78/4.14 | (58) bit0(all_91_1) = all_91_0 % 23.78/4.14 | (59) bit1(pls) = all_91_1 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (4) with fresh symbols all_93_0, all_93_1, all_93_2 % 23.78/4.14 | gives: % 23.78/4.14 | (60) power_power_nat(one_one_nat, all_93_0) = one_one_nat & bit1(pls) = % 23.78/4.14 | all_93_2 & bit0(all_93_2) = all_93_1 & number_number_of_nat(all_93_1) % 23.78/4.14 | = all_93_0 & $i(all_93_0) & $i(all_93_1) & $i(all_93_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (60) implies: % 23.78/4.14 | (61) number_number_of_nat(all_93_1) = all_93_0 % 23.78/4.14 | (62) bit0(all_93_2) = all_93_1 % 23.78/4.14 | (63) bit1(pls) = all_93_2 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (12) with fresh symbols all_95_0, all_95_1, all_95_2 % 23.78/4.14 | gives: % 23.78/4.14 | (64) plus_plus_nat(one_one_nat, one_one_nat) = all_95_2 & bit1(pls) = % 23.78/4.14 | all_95_1 & bit0(all_95_1) = all_95_0 & number_number_of_nat(all_95_0) % 23.78/4.14 | = all_95_2 & $i(all_95_0) & $i(all_95_1) & $i(all_95_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (64) implies: % 23.78/4.14 | (65) number_number_of_nat(all_95_0) = all_95_2 % 23.78/4.14 | (66) bit0(all_95_1) = all_95_0 % 23.78/4.14 | (67) bit1(pls) = all_95_1 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (6) with fresh symbols all_97_0, all_97_1, all_97_2 % 23.78/4.14 | gives: % 23.78/4.14 | (68) power_power_nat(zero_zero_nat, all_97_0) = zero_zero_nat & bit1(pls) = % 23.78/4.14 | all_97_2 & bit0(all_97_2) = all_97_1 & number_number_of_nat(all_97_1) % 23.78/4.14 | = all_97_0 & $i(all_97_0) & $i(all_97_1) & $i(all_97_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (68) implies: % 23.78/4.14 | (69) number_number_of_nat(all_97_1) = all_97_0 % 23.78/4.14 | (70) bit0(all_97_2) = all_97_1 % 23.78/4.14 | (71) bit1(pls) = all_97_2 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (5) with fresh symbols all_99_0, all_99_1, all_99_2 % 23.78/4.14 | gives: % 23.78/4.14 | (72) bit1(pls) = all_99_2 & bit0(all_99_2) = all_99_1 & % 23.78/4.14 | number_number_of_nat(all_99_1) = all_99_0 & % 23.78/4.14 | power_power_int(zero_zero_int, all_99_0) = zero_zero_int & % 23.78/4.14 | $i(all_99_0) & $i(all_99_1) & $i(all_99_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (72) implies: % 23.78/4.14 | (73) number_number_of_nat(all_99_1) = all_99_0 % 23.78/4.14 | (74) bit0(all_99_2) = all_99_1 % 23.78/4.14 | (75) bit1(pls) = all_99_2 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (12) with fresh symbols all_101_0, all_101_1, all_101_2 % 23.78/4.14 | gives: % 23.78/4.14 | (76) plus_plus_nat(one_one_nat, one_one_nat) = all_101_2 & bit1(pls) = % 23.78/4.14 | all_101_1 & bit0(all_101_1) = all_101_0 & % 23.78/4.14 | number_number_of_nat(all_101_0) = all_101_2 & $i(all_101_0) & % 23.78/4.14 | $i(all_101_1) & $i(all_101_2) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (76) implies: % 23.78/4.14 | (77) bit0(all_101_1) = all_101_0 % 23.78/4.14 | (78) bit1(pls) = all_101_1 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (9) with fresh symbol all_103_0 gives: % 23.78/4.14 | (79) bit1(pls) = all_103_0 & $i(all_103_0) & ! [v0: $i] : ! [v1: $i] : ( % 23.78/4.14 | ~ (plus_plus_int(v0, all_103_0) = v1) | ~ $i(v0) | ? [v2: $i] : ? % 23.78/4.14 | [v3: $i] : (number_number_of_int(v1) = v3 & number_number_of_int(v0) % 23.78/4.14 | = v2 & plus_plus_int(v2, one_one_int) = v3 & $i(v3) & $i(v2))) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (79) implies: % 23.78/4.14 | (80) bit1(pls) = all_103_0 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (8) with fresh symbol all_106_0 gives: % 23.78/4.14 | (81) bit1(pls) = all_106_0 & $i(all_106_0) & ! [v0: $i] : ! [v1: $i] : ( % 23.78/4.14 | ~ (plus_plus_int(all_106_0, v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? % 23.78/4.14 | [v3: $i] : (number_number_of_int(v1) = v3 & number_number_of_int(v0) % 23.78/4.14 | = v2 & plus_plus_int(one_one_int, v2) = v3 & $i(v3) & $i(v2))) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (81) implies: % 23.78/4.14 | (82) bit1(pls) = all_106_0 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (22) with fresh symbols all_109_0, all_109_1, all_109_2 % 23.78/4.14 | gives: % 23.78/4.14 | (83) bit1(pls) = all_109_2 & bit0(all_109_2) = all_109_1 & % 23.78/4.14 | number_number_of_nat(all_109_1) = all_109_0 & $i(all_109_0) & % 23.78/4.14 | $i(all_109_1) & $i(all_109_2) & ! [v0: $i] : ! [v1: $i] : ( ~ % 23.78/4.14 | (power_power_int(v0, all_109_0) = v1) | ~ $i(v0) | ? [v2: int] : ( % 23.78/4.14 | ~ (v2 = 0) & ord_less_int(v1, zero_zero_int) = v2)) % 23.78/4.14 | % 23.78/4.14 | ALPHA: (83) implies: % 23.78/4.14 | (84) number_number_of_nat(all_109_1) = all_109_0 % 23.78/4.14 | (85) bit0(all_109_2) = all_109_1 % 23.78/4.14 | (86) bit1(pls) = all_109_2 % 23.78/4.14 | % 23.78/4.14 | DELTA: instantiating (7) with fresh symbols all_112_0, all_112_1, all_112_2 % 23.78/4.14 | gives: % 23.78/4.15 | (87) bit1(pls) = all_112_2 & bit0(all_112_2) = all_112_1 & % 23.78/4.15 | number_number_of_nat(all_112_1) = all_112_0 & $i(all_112_0) & % 23.78/4.15 | $i(all_112_1) & $i(all_112_2) & ! [v0: $i] : (v0 = zero_zero_int | ~ % 23.78/4.15 | (power_power_int(v0, all_112_0) = zero_zero_int) | ~ $i(v0)) & ! % 23.78/4.15 | [v0: $i] : (v0 = zero_zero_int | ~ (power_power_int(zero_zero_int, % 23.78/4.15 | all_112_0) = v0)) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (87) implies: % 23.78/4.15 | (88) number_number_of_nat(all_112_1) = all_112_0 % 23.78/4.15 | (89) bit0(all_112_2) = all_112_1 % 23.78/4.15 | (90) bit1(pls) = all_112_2 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (25) with fresh symbols all_115_0, all_115_1, all_115_2, % 23.78/4.15 | all_115_3, all_115_4 gives: % 23.78/4.15 | (91) bit1(pls) = all_115_2 & bit0(all_115_2) = all_115_1 & % 23.78/4.15 | number_number_of_nat(all_115_1) = all_115_0 & % 23.78/4.15 | power_power_int(all_115_3, all_115_0) = zero_zero_int & % 23.78/4.15 | semiri1621563631at_int(n) = all_115_4 & plus_plus_int(one_one_int, % 23.78/4.15 | all_115_4) = all_115_3 & $i(all_115_0) & $i(all_115_1) & % 23.78/4.15 | $i(all_115_2) & $i(all_115_3) & $i(all_115_4) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (91) implies: % 23.78/4.15 | (92) $i(all_115_4) % 23.78/4.15 | (93) plus_plus_int(one_one_int, all_115_4) = all_115_3 % 23.78/4.15 | (94) semiri1621563631at_int(n) = all_115_4 % 23.78/4.15 | (95) power_power_int(all_115_3, all_115_0) = zero_zero_int % 23.78/4.15 | (96) number_number_of_nat(all_115_1) = all_115_0 % 23.78/4.15 | (97) bit0(all_115_2) = all_115_1 % 23.78/4.15 | (98) bit1(pls) = all_115_2 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (21) with fresh symbols all_117_0, all_117_1, all_117_2 % 23.78/4.15 | gives: % 23.78/4.15 | (99) bit1(pls) = all_117_2 & bit0(all_117_2) = all_117_1 & % 23.78/4.15 | number_number_of_nat(all_117_1) = all_117_0 & $i(all_117_0) & % 23.78/4.15 | $i(all_117_1) & $i(all_117_2) & ! [v0: $i] : ! [v1: $i] : (v0 = % 23.78/4.15 | zero_zero_int | ~ (power_power_int(v0, all_117_0) = v1) | ~ $i(v0) % 23.78/4.15 | | ord_less_int(zero_zero_int, v1) = 0) & ! [v0: $i] : ( ~ % 23.78/4.15 | (power_power_int(zero_zero_int, all_117_0) = v0) | ? [v1: int] : ( % 23.78/4.15 | ~ (v1 = 0) & ord_less_int(zero_zero_int, v0) = v1)) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (99) implies: % 23.78/4.15 | (100) number_number_of_nat(all_117_1) = all_117_0 % 23.78/4.15 | (101) bit0(all_117_2) = all_117_1 % 23.78/4.15 | (102) bit1(pls) = all_117_2 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (18) with fresh symbol all_120_0 gives: % 23.78/4.15 | (103) bit1(pls) = all_120_0 & $i(all_120_0) & ! [v0: $i] : ! [v1: int] : % 23.78/4.15 | (v1 = 0 | ~ (ord_less_int(all_120_0, v0) = v1) | ~ $i(v0) | ? [v2: % 23.78/4.15 | $i] : ? [v3: int] : ( ~ (v3 = 0) & number_number_of_int(v0) = v2 % 23.78/4.15 | & ord_less_int(one_one_int, v2) = v3 & $i(v2))) & ! [v0: $i] : ( % 23.78/4.15 | ~ (ord_less_int(all_120_0, v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 23.78/4.15 | (number_number_of_int(v0) = v1 & ord_less_int(one_one_int, v1) = 0 % 23.78/4.15 | & $i(v1))) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (103) implies: % 23.78/4.15 | (104) bit1(pls) = all_120_0 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (17) with fresh symbol all_123_0 gives: % 23.78/4.15 | (105) bit1(pls) = all_123_0 & $i(all_123_0) & ! [v0: $i] : ! [v1: int] : % 23.78/4.15 | (v1 = 0 | ~ (ord_less_int(v0, all_123_0) = v1) | ~ $i(v0) | ? [v2: % 23.78/4.15 | $i] : ? [v3: int] : ( ~ (v3 = 0) & number_number_of_int(v0) = v2 % 23.78/4.15 | & ord_less_int(v2, one_one_int) = v3 & $i(v2))) & ! [v0: $i] : ( % 23.78/4.15 | ~ (ord_less_int(v0, all_123_0) = 0) | ~ $i(v0) | ? [v1: $i] : % 23.78/4.15 | (number_number_of_int(v0) = v1 & ord_less_int(v1, one_one_int) = 0 % 23.78/4.15 | & $i(v1))) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (105) implies: % 23.78/4.15 | (106) bit1(pls) = all_123_0 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (11) with fresh symbols all_126_0, all_126_1, all_126_2, % 23.78/4.15 | all_126_3, all_126_4 gives: % 23.78/4.15 | (107) bit1(pls) = all_126_4 & bit0(all_126_3) = all_126_1 & bit0(all_126_4) % 23.78/4.15 | = all_126_3 & number_number_of_nat(all_126_1) = all_126_0 & % 23.78/4.15 | number_number_of_nat(all_126_3) = all_126_2 & $i(all_126_0) & % 23.78/4.15 | $i(all_126_1) & $i(all_126_2) & $i(all_126_3) & $i(all_126_4) & ! % 23.78/4.15 | [v0: $i] : ! [v1: $i] : ( ~ (power_power_int(v0, all_126_0) = v1) | % 23.78/4.15 | ~ $i(v0) | ? [v2: $i] : (power_power_int(v2, all_126_2) = v1 & % 23.78/4.15 | power_power_int(v0, all_126_2) = v2 & $i(v2) & $i(v1))) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (107) implies: % 23.78/4.15 | (108) number_number_of_nat(all_126_3) = all_126_2 % 23.78/4.15 | (109) bit0(all_126_4) = all_126_3 % 23.78/4.15 | (110) bit1(pls) = all_126_4 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (2) with fresh symbols all_129_0, all_129_1, all_129_2 % 23.78/4.15 | gives: % 23.78/4.15 | (111) bit1(pls) = all_129_2 & bit0(all_129_2) = all_129_1 & % 23.78/4.15 | number_number_of_nat(all_129_1) = all_129_0 & $i(all_129_0) & % 23.78/4.15 | $i(all_129_1) & $i(all_129_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 23.78/4.15 | $i] : ! [v3: $i] : ( ~ (power_power_int(v1, all_129_0) = v3) | ~ % 23.78/4.15 | (power_power_int(v0, all_129_0) = v2) | ~ (plus_plus_int(v2, v3) = % 23.78/4.15 | zero_zero_int) | ~ $i(v1) | ~ $i(v0) | (v1 = zero_zero_int & v0 % 23.78/4.15 | = zero_zero_int)) & ! [v0: $i] : ! [v1: $i] : (v1 = % 23.78/4.15 | zero_zero_int | ~ (power_power_int(zero_zero_int, all_129_0) = v0) % 23.78/4.15 | | ~ (plus_plus_int(v0, v0) = v1)) % 23.78/4.15 | % 23.78/4.15 | ALPHA: (111) implies: % 23.78/4.15 | (112) number_number_of_nat(all_129_1) = all_129_0 % 23.78/4.15 | (113) bit0(all_129_2) = all_129_1 % 23.78/4.15 | (114) bit1(pls) = all_129_2 % 23.78/4.15 | % 23.78/4.15 | DELTA: instantiating (23) with fresh symbols all_132_0, all_132_1, all_132_2 % 23.78/4.15 | gives: % 23.78/4.16 | (115) bit1(pls) = all_132_2 & bit0(all_132_2) = all_132_1 & % 23.78/4.16 | number_number_of_nat(all_132_1) = all_132_0 & $i(all_132_0) & % 23.78/4.16 | $i(all_132_1) & $i(all_132_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 23.78/4.16 | $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (power_power_int(v1, % 23.78/4.16 | all_132_0) = v3) | ~ (power_power_int(v0, all_132_0) = v2) | % 23.78/4.16 | ~ (plus_plus_int(v2, v3) = v4) | ~ $i(v1) | ~ $i(v0) | % 23.78/4.16 | ord_less_int(zero_zero_int, v4) = 0 | (v1 = zero_zero_int & v0 = % 23.78/4.16 | zero_zero_int)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 23.78/4.16 | (power_power_int(zero_zero_int, all_132_0) = v0) | ~ % 23.78/4.16 | (plus_plus_int(v0, v0) = v1) | ? [v2: int] : ( ~ (v2 = 0) & % 23.78/4.16 | ord_less_int(zero_zero_int, v1) = v2)) % 23.78/4.16 | % 23.78/4.16 | ALPHA: (115) implies: % 23.78/4.16 | (116) number_number_of_nat(all_132_1) = all_132_0 % 23.78/4.16 | (117) bit0(all_132_2) = all_132_1 % 23.78/4.16 | (118) bit1(pls) = all_132_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (118) imply: % 23.78/4.16 | (119) bit1(zero_zero_int) = all_132_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (114) imply: % 23.78/4.16 | (120) bit1(zero_zero_int) = all_129_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (110) imply: % 23.78/4.16 | (121) bit1(zero_zero_int) = all_126_4 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (106) imply: % 23.78/4.16 | (122) bit1(zero_zero_int) = all_123_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (104) imply: % 23.78/4.16 | (123) bit1(zero_zero_int) = all_120_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (102) imply: % 23.78/4.16 | (124) bit1(zero_zero_int) = all_117_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (98) imply: % 23.78/4.16 | (125) bit1(zero_zero_int) = all_115_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (90) imply: % 23.78/4.16 | (126) bit1(zero_zero_int) = all_112_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (86) imply: % 23.78/4.16 | (127) bit1(zero_zero_int) = all_109_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (82) imply: % 23.78/4.16 | (128) bit1(zero_zero_int) = all_106_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (80) imply: % 23.78/4.16 | (129) bit1(zero_zero_int) = all_103_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (78) imply: % 23.78/4.16 | (130) bit1(zero_zero_int) = all_101_1 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (75) imply: % 23.78/4.16 | (131) bit1(zero_zero_int) = all_99_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (71) imply: % 23.78/4.16 | (132) bit1(zero_zero_int) = all_97_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (67) imply: % 23.78/4.16 | (133) bit1(zero_zero_int) = all_95_1 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (63) imply: % 23.78/4.16 | (134) bit1(zero_zero_int) = all_93_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (59) imply: % 23.78/4.16 | (135) bit1(zero_zero_int) = all_91_1 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (56) imply: % 23.78/4.16 | (136) bit1(zero_zero_int) = all_89_2 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (51) imply: % 23.78/4.16 | (137) bit1(zero_zero_int) = all_87_1 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (44) imply: % 23.78/4.16 | (138) bit1(zero_zero_int) = all_77_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (42) imply: % 23.78/4.16 | (139) bit1(zero_zero_int) = all_75_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (40) imply: % 23.78/4.16 | (140) bit1(zero_zero_int) = all_73_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (38) imply: % 23.78/4.16 | (141) bit1(zero_zero_int) = all_69_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (36) imply: % 23.78/4.16 | (142) ord_less_int(zero_zero_int, zero_zero_int) = all_67_0 % 23.78/4.16 | % 23.78/4.16 | REDUCE: (19), (33) imply: % 23.78/4.16 | (143) ord_less_int(zero_zero_int, zero_zero_int) = all_65_0 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (30) with all_65_0, all_67_0, zero_zero_int, % 23.78/4.16 | zero_zero_int, simplifying with (142), (143) gives: % 23.78/4.16 | (144) all_67_0 = all_65_0 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (26) with all_82_1, all_115_4, n, simplifying with % 23.78/4.16 | (48), (94) gives: % 23.78/4.16 | (145) all_115_4 = all_82_1 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_77_0, all_87_1, zero_zero_int, % 23.78/4.16 | simplifying with (137), (138) gives: % 23.78/4.16 | (146) all_87_1 = all_77_0 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_77_0, all_89_2, zero_zero_int, % 23.78/4.16 | simplifying with (136), (138) gives: % 23.78/4.16 | (147) all_89_2 = all_77_0 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_87_1, all_95_1, zero_zero_int, % 23.78/4.16 | simplifying with (133), (137) gives: % 23.78/4.16 | (148) all_95_1 = all_87_1 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_95_1, all_97_2, zero_zero_int, % 23.78/4.16 | simplifying with (132), (133) gives: % 23.78/4.16 | (149) all_97_2 = all_95_1 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_97_2, all_101_1, zero_zero_int, % 23.78/4.16 | simplifying with (130), (132) gives: % 23.78/4.16 | (150) all_101_1 = all_97_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_101_1, all_106_0, zero_zero_int, % 23.78/4.16 | simplifying with (128), (130) gives: % 23.78/4.16 | (151) all_106_0 = all_101_1 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_93_2, all_106_0, zero_zero_int, % 23.78/4.16 | simplifying with (128), (134) gives: % 23.78/4.16 | (152) all_106_0 = all_93_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_109_2, all_115_2, zero_zero_int, % 23.78/4.16 | simplifying with (125), (127) gives: % 23.78/4.16 | (153) all_115_2 = all_109_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_99_2, all_117_2, zero_zero_int, % 23.78/4.16 | simplifying with (124), (131) gives: % 23.78/4.16 | (154) all_117_2 = all_99_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_91_1, all_117_2, zero_zero_int, % 23.78/4.16 | simplifying with (124), (135) gives: % 23.78/4.16 | (155) all_117_2 = all_91_1 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_89_2, all_117_2, zero_zero_int, % 23.78/4.16 | simplifying with (124), (136) gives: % 23.78/4.16 | (156) all_117_2 = all_89_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_109_2, all_120_0, zero_zero_int, % 23.78/4.16 | simplifying with (123), (127) gives: % 23.78/4.16 | (157) all_120_0 = all_109_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_99_2, all_120_0, zero_zero_int, % 23.78/4.16 | simplifying with (123), (131) gives: % 23.78/4.16 | (158) all_120_0 = all_99_2 % 23.78/4.16 | % 23.78/4.16 | GROUND_INST: instantiating (29) with all_112_2, all_123_0, zero_zero_int, % 23.78/4.16 | simplifying with (122), (126) gives: % 23.78/4.17 | (159) all_123_0 = all_112_2 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_77_0, all_123_0, zero_zero_int, % 23.78/4.17 | simplifying with (122), (138) gives: % 23.78/4.17 | (160) all_123_0 = all_77_0 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_73_0, all_123_0, zero_zero_int, % 23.78/4.17 | simplifying with (122), (140) gives: % 23.78/4.17 | (161) all_123_0 = all_73_0 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_120_0, all_126_4, zero_zero_int, % 23.78/4.17 | simplifying with (121), (123) gives: % 23.78/4.17 | (162) all_126_4 = all_120_0 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_103_0, all_126_4, zero_zero_int, % 23.78/4.17 | simplifying with (121), (129) gives: % 23.78/4.17 | (163) all_126_4 = all_103_0 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_115_2, all_129_2, zero_zero_int, % 23.78/4.17 | simplifying with (120), (125) gives: % 23.78/4.17 | (164) all_129_2 = all_115_2 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_75_0, all_129_2, zero_zero_int, % 23.78/4.17 | simplifying with (120), (139) gives: % 23.78/4.17 | (165) all_129_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_95_1, all_132_2, zero_zero_int, % 23.78/4.17 | simplifying with (119), (133) gives: % 23.78/4.17 | (166) all_132_2 = all_95_1 % 23.78/4.17 | % 23.78/4.17 | GROUND_INST: instantiating (29) with all_69_0, all_132_2, zero_zero_int, % 23.78/4.17 | simplifying with (119), (141) gives: % 23.78/4.17 | (167) all_132_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (166), (167) imply: % 23.78/4.17 | (168) all_95_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (168) implies: % 23.78/4.17 | (169) all_95_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (164), (165) imply: % 23.78/4.17 | (170) all_115_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (170) implies: % 23.78/4.17 | (171) all_115_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (162), (163) imply: % 23.78/4.17 | (172) all_120_0 = all_103_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (172) implies: % 23.78/4.17 | (173) all_120_0 = all_103_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (159), (161) imply: % 23.78/4.17 | (174) all_112_2 = all_73_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (159), (160) imply: % 23.78/4.17 | (175) all_112_2 = all_77_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (157), (173) imply: % 23.78/4.17 | (176) all_109_2 = all_103_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (176) implies: % 23.78/4.17 | (177) all_109_2 = all_103_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (158), (173) imply: % 23.78/4.17 | (178) all_103_0 = all_99_2 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (154), (155) imply: % 23.78/4.17 | (179) all_99_2 = all_91_1 % 23.78/4.17 | % 23.78/4.17 | SIMP: (179) implies: % 23.78/4.17 | (180) all_99_2 = all_91_1 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (155), (156) imply: % 23.78/4.17 | (181) all_91_1 = all_89_2 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (153), (171) imply: % 23.78/4.17 | (182) all_109_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (182) implies: % 23.78/4.17 | (183) all_109_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (174), (175) imply: % 23.78/4.17 | (184) all_77_0 = all_73_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (184) implies: % 23.78/4.17 | (185) all_77_0 = all_73_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (177), (183) imply: % 23.78/4.17 | (186) all_103_0 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (186) implies: % 23.78/4.17 | (187) all_103_0 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (151), (152) imply: % 23.78/4.17 | (188) all_101_1 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | SIMP: (188) implies: % 23.78/4.17 | (189) all_101_1 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (178), (187) imply: % 23.78/4.17 | (190) all_99_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (190) implies: % 23.78/4.17 | (191) all_99_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (150), (189) imply: % 23.78/4.17 | (192) all_97_2 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | SIMP: (192) implies: % 23.78/4.17 | (193) all_97_2 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (180), (191) imply: % 23.78/4.17 | (194) all_91_1 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (194) implies: % 23.78/4.17 | (195) all_91_1 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (149), (193) imply: % 23.78/4.17 | (196) all_95_1 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | SIMP: (196) implies: % 23.78/4.17 | (197) all_95_1 = all_93_2 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (148), (197) imply: % 23.78/4.17 | (198) all_93_2 = all_87_1 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (169), (197) imply: % 23.78/4.17 | (199) all_93_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (198), (199) imply: % 23.78/4.17 | (200) all_87_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (200) implies: % 23.78/4.17 | (201) all_87_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (181), (195) imply: % 23.78/4.17 | (202) all_89_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (202) implies: % 23.78/4.17 | (203) all_89_2 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (147), (203) imply: % 23.78/4.17 | (204) all_77_0 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (204) implies: % 23.78/4.17 | (205) all_77_0 = all_75_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (146), (201) imply: % 23.78/4.17 | (206) all_77_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (206) implies: % 23.78/4.17 | (207) all_77_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (185), (205) imply: % 23.78/4.17 | (208) all_75_0 = all_73_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (205), (207) imply: % 23.78/4.17 | (209) all_75_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (208), (209) imply: % 23.78/4.17 | (210) all_73_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | SIMP: (210) implies: % 23.78/4.17 | (211) all_73_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (203), (209) imply: % 23.78/4.17 | (212) all_89_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (195), (209) imply: % 23.78/4.17 | (213) all_91_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (193), (199) imply: % 23.78/4.17 | (214) all_97_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (191), (209) imply: % 23.78/4.17 | (215) all_99_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (189), (199) imply: % 23.78/4.17 | (216) all_101_1 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (187), (209) imply: % 23.78/4.17 | (217) all_103_0 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (183), (209) imply: % 23.78/4.17 | (218) all_109_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (174), (211) imply: % 23.78/4.17 | (219) all_112_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (171), (209) imply: % 23.78/4.17 | (220) all_115_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (155), (213) imply: % 23.78/4.17 | (221) all_117_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (163), (217) imply: % 23.78/4.17 | (222) all_126_4 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | COMBINE_EQS: (165), (209) imply: % 23.78/4.17 | (223) all_129_2 = all_69_0 % 23.78/4.17 | % 23.78/4.17 | REDUCE: (35), (144) imply: % 23.78/4.17 | (224) ~ (all_65_0 = 0) % 23.78/4.17 | % 23.78/4.17 | REDUCE: (117), (167) imply: % 23.78/4.17 | (225) bit0(all_69_0) = all_132_1 % 23.78/4.17 | % 23.78/4.17 | REDUCE: (113), (223) imply: % 23.78/4.17 | (226) bit0(all_69_0) = all_129_1 % 23.78/4.17 | % 23.78/4.17 | REDUCE: (109), (222) imply: % 23.78/4.17 | (227) bit0(all_69_0) = all_126_3 % 23.78/4.17 | % 23.78/4.17 | REDUCE: (101), (221) imply: % 23.78/4.17 | (228) bit0(all_69_0) = all_117_1 % 23.78/4.17 | % 23.78/4.18 | REDUCE: (97), (220) imply: % 23.78/4.18 | (229) bit0(all_69_0) = all_115_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (89), (219) imply: % 23.78/4.18 | (230) bit0(all_69_0) = all_112_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (85), (218) imply: % 23.78/4.18 | (231) bit0(all_69_0) = all_109_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (77), (216) imply: % 23.78/4.18 | (232) bit0(all_69_0) = all_101_0 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (74), (215) imply: % 23.78/4.18 | (233) bit0(all_69_0) = all_99_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (70), (214) imply: % 23.78/4.18 | (234) bit0(all_69_0) = all_97_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (66), (169) imply: % 23.78/4.18 | (235) bit0(all_69_0) = all_95_0 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (62), (199) imply: % 23.78/4.18 | (236) bit0(all_69_0) = all_93_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (58), (213) imply: % 23.78/4.18 | (237) bit0(all_69_0) = all_91_0 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (55), (212) imply: % 23.78/4.18 | (238) bit0(all_69_0) = all_89_1 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (50), (201) imply: % 23.78/4.18 | (239) bit0(all_69_0) = all_87_0 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (93), (145) imply: % 23.78/4.18 | (240) plus_plus_int(one_one_int, all_82_1) = all_115_3 % 23.78/4.18 | % 23.78/4.18 | REDUCE: (92), (145) imply: % 23.78/4.18 | (241) $i(all_82_1) % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (31) with all_82_0, all_115_3, all_82_1, % 23.78/4.18 | one_one_int, simplifying with (47), (240) gives: % 23.78/4.18 | (242) all_115_3 = all_82_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_91_0, all_93_1, all_69_0, simplifying % 23.78/4.18 | with (236), (237) gives: % 23.78/4.18 | (243) all_93_1 = all_91_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_91_0, all_95_0, all_69_0, simplifying % 23.78/4.18 | with (235), (237) gives: % 23.78/4.18 | (244) all_95_0 = all_91_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_93_1, all_97_1, all_69_0, simplifying % 23.78/4.18 | with (234), (236) gives: % 23.78/4.18 | (245) all_97_1 = all_93_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_101_0, all_109_1, all_69_0, % 23.78/4.18 | simplifying with (231), (232) gives: % 23.78/4.18 | (246) all_109_1 = all_101_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_99_1, all_109_1, all_69_0, % 23.78/4.18 | simplifying with (231), (233) gives: % 23.78/4.18 | (247) all_109_1 = all_99_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_97_1, all_109_1, all_69_0, % 23.78/4.18 | simplifying with (231), (234) gives: % 23.78/4.18 | (248) all_109_1 = all_97_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_101_0, all_112_1, all_69_0, % 23.78/4.18 | simplifying with (230), (232) gives: % 23.78/4.18 | (249) all_112_1 = all_101_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_95_0, all_115_1, all_69_0, % 23.78/4.18 | simplifying with (229), (235) gives: % 23.78/4.18 | (250) all_115_1 = all_95_0 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_112_1, all_117_1, all_69_0, % 23.78/4.18 | simplifying with (228), (230) gives: % 23.78/4.18 | (251) all_117_1 = all_112_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_117_1, all_126_3, all_69_0, % 23.78/4.18 | simplifying with (227), (228) gives: % 23.78/4.18 | (252) all_126_3 = all_117_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_115_1, all_129_1, all_69_0, % 23.78/4.18 | simplifying with (226), (229) gives: % 23.78/4.18 | (253) all_129_1 = all_115_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_89_1, all_129_1, all_69_0, % 23.78/4.18 | simplifying with (226), (238) gives: % 23.78/4.18 | (254) all_129_1 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_126_3, all_132_1, all_69_0, % 23.78/4.18 | simplifying with (225), (227) gives: % 23.78/4.18 | (255) all_132_1 = all_126_3 % 23.78/4.18 | % 23.78/4.18 | GROUND_INST: instantiating (28) with all_87_0, all_132_1, all_69_0, % 23.78/4.18 | simplifying with (225), (239) gives: % 23.78/4.18 | (256) all_132_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (255), (256) imply: % 23.78/4.18 | (257) all_126_3 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (257) implies: % 23.78/4.18 | (258) all_126_3 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (253), (254) imply: % 23.78/4.18 | (259) all_115_1 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | SIMP: (259) implies: % 23.78/4.18 | (260) all_115_1 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (252), (258) imply: % 23.78/4.18 | (261) all_117_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (261) implies: % 23.78/4.18 | (262) all_117_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (251), (262) imply: % 23.78/4.18 | (263) all_112_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (263) implies: % 23.78/4.18 | (264) all_112_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (250), (260) imply: % 23.78/4.18 | (265) all_95_0 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | SIMP: (265) implies: % 23.78/4.18 | (266) all_95_0 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (249), (264) imply: % 23.78/4.18 | (267) all_101_0 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (267) implies: % 23.78/4.18 | (268) all_101_0 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (246), (247) imply: % 23.78/4.18 | (269) all_101_0 = all_99_1 % 23.78/4.18 | % 23.78/4.18 | SIMP: (269) implies: % 23.78/4.18 | (270) all_101_0 = all_99_1 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (247), (248) imply: % 23.78/4.18 | (271) all_99_1 = all_97_1 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (268), (270) imply: % 23.78/4.18 | (272) all_99_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (272) implies: % 23.78/4.18 | (273) all_99_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (271), (273) imply: % 23.78/4.18 | (274) all_97_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (274) implies: % 23.78/4.18 | (275) all_97_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (245), (275) imply: % 23.78/4.18 | (276) all_93_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (276) implies: % 23.78/4.18 | (277) all_93_1 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (244), (266) imply: % 23.78/4.18 | (278) all_91_0 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | SIMP: (278) implies: % 23.78/4.18 | (279) all_91_0 = all_89_1 % 23.78/4.18 | % 23.78/4.18 | COMBINE_EQS: (243), (277) imply: % 23.78/4.18 | (280) all_91_0 = all_87_0 % 23.78/4.18 | % 23.78/4.18 | SIMP: (280) implies: % 23.78/4.18 | (281) all_91_0 = all_87_0 % 23.78/4.18 | % 24.10/4.18 | COMBINE_EQS: (279), (281) imply: % 24.10/4.18 | (282) all_89_1 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | SIMP: (282) implies: % 24.10/4.18 | (283) all_89_1 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | COMBINE_EQS: (266), (283) imply: % 24.10/4.18 | (284) all_95_0 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | COMBINE_EQS: (247), (273) imply: % 24.10/4.18 | (285) all_109_1 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | COMBINE_EQS: (260), (283) imply: % 24.10/4.18 | (286) all_115_1 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | COMBINE_EQS: (254), (283) imply: % 24.10/4.18 | (287) all_129_1 = all_87_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (116), (256) imply: % 24.10/4.18 | (288) number_number_of_nat(all_87_0) = all_132_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (112), (287) imply: % 24.10/4.18 | (289) number_number_of_nat(all_87_0) = all_129_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (108), (258) imply: % 24.10/4.18 | (290) number_number_of_nat(all_87_0) = all_126_2 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (100), (262) imply: % 24.10/4.18 | (291) number_number_of_nat(all_87_0) = all_117_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (96), (286) imply: % 24.10/4.18 | (292) number_number_of_nat(all_87_0) = all_115_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (88), (264) imply: % 24.10/4.18 | (293) number_number_of_nat(all_87_0) = all_112_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (84), (285) imply: % 24.10/4.18 | (294) number_number_of_nat(all_87_0) = all_109_0 % 24.10/4.18 | % 24.10/4.18 | REDUCE: (73), (273) imply: % 24.10/4.18 | (295) number_number_of_nat(all_87_0) = all_99_0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (69), (275) imply: % 24.10/4.19 | (296) number_number_of_nat(all_87_0) = all_97_0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (65), (284) imply: % 24.10/4.19 | (297) number_number_of_nat(all_87_0) = all_95_2 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (61), (277) imply: % 24.10/4.19 | (298) number_number_of_nat(all_87_0) = all_93_0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (54), (283) imply: % 24.10/4.19 | (299) number_number_of_nat(all_87_0) = all_89_0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (95), (242) imply: % 24.10/4.19 | (300) power_power_int(all_82_0, all_115_0) = zero_zero_int % 24.10/4.19 | % 24.10/4.19 | REDUCE: (53), (283) imply: % 24.10/4.19 | (301) $i(all_87_0) % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_93_0, all_95_2, all_87_0, simplifying % 24.10/4.19 | with (297), (298) gives: % 24.10/4.19 | (302) all_95_2 = all_93_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_95_2, all_97_0, all_87_0, simplifying % 24.10/4.19 | with (296), (297) gives: % 24.10/4.19 | (303) all_97_0 = all_95_2 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_97_0, all_99_0, all_87_0, simplifying % 24.10/4.19 | with (295), (296) gives: % 24.10/4.19 | (304) all_99_0 = all_97_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_99_0, all_109_0, all_87_0, % 24.10/4.19 | simplifying with (294), (295) gives: % 24.10/4.19 | (305) all_109_0 = all_99_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_109_0, all_112_0, all_87_0, % 24.10/4.19 | simplifying with (293), (294) gives: % 24.10/4.19 | (306) all_112_0 = all_109_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_117_0, all_126_2, all_87_0, % 24.10/4.19 | simplifying with (290), (291) gives: % 24.10/4.19 | (307) all_126_2 = all_117_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_117_0, all_129_0, all_87_0, % 24.10/4.19 | simplifying with (289), (291) gives: % 24.10/4.19 | (308) all_129_0 = all_117_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_115_0, all_129_0, all_87_0, % 24.10/4.19 | simplifying with (289), (292) gives: % 24.10/4.19 | (309) all_129_0 = all_115_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_112_0, all_129_0, all_87_0, % 24.10/4.19 | simplifying with (289), (293) gives: % 24.10/4.19 | (310) all_129_0 = all_112_0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_126_2, all_132_0, all_87_0, % 24.10/4.19 | simplifying with (288), (290) gives: % 24.10/4.19 | (311) all_132_0 = all_126_2 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (27) with all_89_0, all_132_0, all_87_0, % 24.10/4.19 | simplifying with (288), (299) gives: % 24.10/4.19 | (312) all_132_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (311), (312) imply: % 24.10/4.19 | (313) all_126_2 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (313) implies: % 24.10/4.19 | (314) all_126_2 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (308), (309) imply: % 24.10/4.19 | (315) all_117_0 = all_115_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (315) implies: % 24.10/4.19 | (316) all_117_0 = all_115_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (309), (310) imply: % 24.10/4.19 | (317) all_115_0 = all_112_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (307), (314) imply: % 24.10/4.19 | (318) all_117_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (318) implies: % 24.10/4.19 | (319) all_117_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (316), (319) imply: % 24.10/4.19 | (320) all_115_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (320) implies: % 24.10/4.19 | (321) all_115_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (317), (321) imply: % 24.10/4.19 | (322) all_112_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (322) implies: % 24.10/4.19 | (323) all_112_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (306), (323) imply: % 24.10/4.19 | (324) all_109_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (324) implies: % 24.10/4.19 | (325) all_109_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (305), (325) imply: % 24.10/4.19 | (326) all_99_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (326) implies: % 24.10/4.19 | (327) all_99_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (304), (327) imply: % 24.10/4.19 | (328) all_97_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (328) implies: % 24.10/4.19 | (329) all_97_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (303), (329) imply: % 24.10/4.19 | (330) all_95_2 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (330) implies: % 24.10/4.19 | (331) all_95_2 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | COMBINE_EQS: (302), (331) imply: % 24.10/4.19 | (332) all_93_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | SIMP: (332) implies: % 24.10/4.19 | (333) all_93_0 = all_89_0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (300), (321) imply: % 24.10/4.19 | (334) power_power_int(all_82_0, all_89_0) = zero_zero_int % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (fact_52_zadd__commute) with one_one_int, all_82_1, % 24.10/4.19 | all_82_0, simplifying with (24), (47), (241) gives: % 24.10/4.19 | (335) plus_plus_int(all_82_1, one_one_int) = all_82_0 & $i(all_82_0) % 24.10/4.19 | % 24.10/4.19 | ALPHA: (335) implies: % 24.10/4.19 | (336) $i(all_82_0) % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (20) with all_82_0, all_87_0, all_89_0, simplifying % 24.10/4.19 | with (299), (301), (334), (336) gives: % 24.10/4.19 | (337) all_82_0 = zero_zero_int & ~ (all_89_0 = zero_zero_nat) % 24.10/4.19 | % 24.10/4.19 | ALPHA: (337) implies: % 24.10/4.19 | (338) all_82_0 = zero_zero_int % 24.10/4.19 | % 24.10/4.19 | REDUCE: (46), (338) imply: % 24.10/4.19 | (339) ord_less_int(zero_zero_int, zero_zero_int) = 0 % 24.10/4.19 | % 24.10/4.19 | GROUND_INST: instantiating (30) with all_65_0, 0, zero_zero_int, % 24.10/4.19 | zero_zero_int, simplifying with (143), (339) gives: % 24.10/4.19 | (340) all_65_0 = 0 % 24.10/4.19 | % 24.10/4.19 | REDUCE: (224), (340) imply: % 24.10/4.19 | (341) $false % 24.10/4.19 | % 24.10/4.19 | CLOSE: (341) is inconsistent. % 24.10/4.19 | % 24.10/4.19 End of proof % 24.10/4.19 % SZS output end Proof for theBenchmark % 24.10/4.19 % 24.10/4.19 3581ms %------------------------------------------------------------------------------