%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM924+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 : n017.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:46 EDT 2023 % Result : Theorem 16.68s 2.93s % Output : Proof 46.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM924+1 : TPTP v8.1.2. Released v5.3.0. % 0.07/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n017.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Aug 25 10:21:40 EDT 2023 % 0.13/0.35 % CPUTime : % 0.21/0.64 ________ _____ % 0.21/0.64 ___ __ \_________(_)________________________________ % 0.21/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.64 % 0.21/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.64 (2023-06-19) % 0.21/0.64 % 0.21/0.64 (c) Philipp Rümmer, 2009-2023 % 0.21/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.64 Amanda Stjerna. % 0.21/0.64 Free software under BSD-3-Clause. % 0.21/0.64 % 0.21/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.64 % 0.21/0.64 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.65 Running up to 7 provers in parallel. % 0.21/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.64/1.23 Prover 1: Preprocessing ... % 3.64/1.24 Prover 4: Preprocessing ... % 4.31/1.28 Prover 5: Preprocessing ... % 4.31/1.28 Prover 2: Preprocessing ... % 4.31/1.28 Prover 6: Preprocessing ... % 4.31/1.28 Prover 0: Preprocessing ... % 4.31/1.28 Prover 3: Preprocessing ... % 11.90/2.30 Prover 6: Constructing countermodel ... % 11.90/2.35 Prover 3: Constructing countermodel ... % 11.90/2.36 Prover 1: Constructing countermodel ... % 12.86/2.42 Prover 5: Proving ... % 13.77/2.60 Prover 4: Constructing countermodel ... % 13.77/2.61 Prover 2: Proving ... % 13.77/2.62 Prover 0: Proving ... % 16.68/2.93 Prover 3: proved (2269ms) % 16.68/2.93 % 16.68/2.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.68/2.93 % 16.68/2.93 Prover 2: stopped % 16.68/2.93 Prover 0: stopped % 16.68/2.94 Prover 5: stopped % 16.68/2.95 Prover 6: stopped % 17.00/2.96 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 17.00/2.96 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 17.00/2.96 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 17.00/2.96 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 17.00/2.96 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 17.69/3.07 Prover 7: Preprocessing ... % 18.04/3.09 Prover 8: Preprocessing ... % 18.04/3.12 Prover 10: Preprocessing ... % 18.49/3.16 Prover 11: Preprocessing ... % 18.49/3.17 Prover 13: Preprocessing ... % 19.96/3.41 Prover 10: Warning: ignoring some quantifiers % 20.61/3.44 Prover 7: Warning: ignoring some quantifiers % 20.61/3.46 Prover 10: Constructing countermodel ... % 20.61/3.46 Prover 8: Warning: ignoring some quantifiers % 20.61/3.47 Prover 7: Constructing countermodel ... % 21.08/3.50 Prover 8: Constructing countermodel ... % 21.08/3.55 Prover 13: Warning: ignoring some quantifiers % 21.84/3.58 Prover 13: Constructing countermodel ... % 22.28/3.69 Prover 11: Constructing countermodel ... % 43.41/6.43 Prover 10: Found proof (size 453) % 43.41/6.44 Prover 10: proved (3492ms) % 43.41/6.44 Prover 11: stopped % 43.41/6.44 Prover 8: stopped % 43.41/6.44 Prover 1: stopped % 43.41/6.44 Prover 13: stopped % 43.41/6.44 Prover 4: stopped % 43.41/6.44 Prover 7: stopped % 43.41/6.44 % 43.41/6.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 43.41/6.44 % 45.53/6.81 % SZS output start Proof for theBenchmark % 45.53/6.81 Assumptions after simplification: % 45.53/6.81 --------------------------------- % 45.53/6.81 % 45.53/6.81 (conj_0) % 45.71/6.84 $i(s) & $i(pls) & $i(one_one_int) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: % 45.71/6.84 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (number_number_of_nat(v1) = % 45.71/6.84 v2 & power_power_int(s, v2) = v3 & bit1(pls) = v0 & bit0(v0) = v1 & % 45.71/6.84 plus_plus_int(v3, one_one_int) = v4 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 45.71/6.84 $i(v0) & ~ ord_less_int(v4, zero_zero_int)) % 45.71/6.84 % 45.71/6.84 (fact_104_zadd__commute) % 45.71/6.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (plus_plus_int(v0, v1) = v2) | % 45.71/6.84 ~ $i(v1) | ~ $i(v0) | (plus_plus_int(v1, v0) = v2 & $i(v2))) % 45.71/6.84 % 45.71/6.84 (fact_105_zero__is__num__zero) % 45.71/6.84 number_number_of_int(pls) = zero_zero_int & $i(pls) & $i(zero_zero_int) % 45.71/6.84 % 45.71/6.84 (fact_10_power2__less__0) % 45.71/6.85 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.85 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.85 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ( ~ (power_power_int(v3, v2) = % 45.71/6.85 v4) | ~ $i(v3) | ~ ord_less_int(v4, zero_zero_int))) % 45.71/6.85 % 45.71/6.85 (fact_11_zero__less__power2) % 45.71/6.85 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.85 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.85 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : (v3 = zero_zero_int | ~ % 45.71/6.85 (power_power_int(v3, v2) = v4) | ~ $i(v3) | ord_less_int(zero_zero_int, % 45.71/6.85 v4)) & ! [v3: $i] : ( ~ (power_power_int(zero_zero_int, v2) = v3) | ~ % 45.71/6.85 ord_less_int(zero_zero_int, v3))) % 45.71/6.85 % 45.71/6.85 (fact_12_one__power2) % 45.71/6.85 $i(one_one_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.85 (power_power_nat(one_one_nat, v2) = one_one_nat & number_number_of_nat(v1) = % 45.71/6.85 v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.85 % 45.71/6.85 (fact_13_one__power2) % 45.71/6.85 $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.85 (number_number_of_nat(v1) = v2 & power_power_int(one_one_int, v2) = % 45.71/6.85 one_one_int & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.85 % 45.71/6.85 (fact_14_zero__power2) % 45.71/6.85 $i(zero_zero_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.85 (power_power_nat(zero_zero_nat, v2) = zero_zero_nat & number_number_of_nat(v1) % 45.71/6.85 = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.85 % 45.71/6.85 (fact_15_zero__power2) % 45.71/6.86 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.86 (number_number_of_nat(v1) = v2 & power_power_int(zero_zero_int, v2) = % 45.71/6.86 zero_zero_int & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.86 % 45.71/6.86 (fact_16_zero__eq__power2) % 45.71/6.86 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.86 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.86 $i(v1) & $i(v0) & ! [v3: $i] : (v3 = zero_zero_int | ~ % 45.71/6.86 (power_power_int(v3, v2) = zero_zero_int) | ~ $i(v3)) & ! [v3: $i] : (v3 % 45.71/6.86 = zero_zero_int | ~ (power_power_int(zero_zero_int, v2) = v3))) % 45.71/6.86 % 45.71/6.86 (fact_17_add__special_I2_J) % 45.71/6.86 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 45.71/6.86 $i] : ! [v2: $i] : ( ~ (plus_plus_int(v0, v1) = v2) | ~ $i(v1) | ? [v3: % 45.71/6.86 $i] : ? [v4: $i] : (number_number_of_int(v2) = v4 & % 45.71/6.86 number_number_of_int(v1) = v3 & plus_plus_int(one_one_int, v3) = v4 & % 45.71/6.86 $i(v4) & $i(v3)))) % 45.71/6.86 % 45.71/6.86 (fact_18_add__special_I3_J) % 45.71/6.86 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 45.71/6.86 $i] : ! [v2: $i] : ( ~ (plus_plus_int(v1, v0) = v2) | ~ $i(v1) | ? [v3: % 45.71/6.86 $i] : ? [v4: $i] : (number_number_of_int(v2) = v4 & % 45.71/6.86 number_number_of_int(v1) = v3 & plus_plus_int(v3, one_one_int) = v4 & % 45.71/6.86 $i(v4) & $i(v3)))) % 45.71/6.86 % 45.71/6.86 (fact_19_t__l__p) % 45.71/6.86 $i(m) & $i(pls) & $i(one_one_int) & $i(t) & ? [v0: $i] : ? [v1: $i] : ? % 45.71/6.86 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (bit1(pls) = v0 & % 45.71/6.86 bit0(v1) = v2 & bit0(v0) = v1 & number_number_of_int(v2) = v3 & % 45.71/6.86 plus_plus_int(v4, one_one_int) = v5 & times_times_int(v3, m) = v4 & $i(v5) & % 45.71/6.86 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ord_less_int(t, v5)) % 45.71/6.86 % 45.71/6.86 (fact_20__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_) % 45.71/6.87 $i(s) & $i(m) & $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? % 45.71/6.87 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 45.71/6.87 : ? [v8: $i] : ? [v9: $i] : (number_number_of_nat(v1) = v2 & % 45.71/6.87 power_power_int(s, v2) = v3 & bit1(pls) = v0 & bit0(v1) = v5 & bit0(v0) = v1 % 45.71/6.87 & number_number_of_int(v5) = v6 & plus_plus_int(v7, one_one_int) = v8 & % 45.71/6.87 plus_plus_int(v3, one_one_int) = v4 & times_times_int(v8, v9) = v4 & % 45.71/6.87 times_times_int(v6, m) = v7 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 45.71/6.87 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.87 % 45.71/6.87 (fact_21_p) % 45.71/6.87 $i(m) & $i(pls) & $i(one_one_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.87 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & % 45.71/6.87 bit0(v0) = v1 & number_number_of_int(v2) = v3 & plus_plus_int(v4, % 45.71/6.87 one_one_int) = v5 & times_times_int(v3, m) = v4 & $i(v5) & $i(v4) & $i(v3) % 45.71/6.87 & $i(v2) & $i(v1) & $i(v0) & zprime(v5)) % 45.71/6.87 % 45.71/6.87 (fact_22_qf1pt) % 45.71/6.87 $i(m) & $i(pls) & $i(one_one_int) & $i(t) & ? [v0: $i] : ? [v1: $i] : ? % 45.71/6.87 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (bit1(pls) % 45.71/6.87 = v0 & bit0(v1) = v2 & bit0(v0) = v1 & number_number_of_int(v2) = v3 & % 45.71/6.87 plus_plus_int(v4, one_one_int) = v5 & times_times_int(v5, t) = v6 & % 45.71/6.87 times_times_int(v3, m) = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 45.71/6.87 $i(v1) & $i(v0) & twoSqu526106917sum2sq(v6)) % 45.71/6.87 % 45.71/6.87 (fact_24_number__of__is__id) % 45.71/6.87 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (number_number_of_int(v0) = v1) | ~ % 45.71/6.87 $i(v0)) % 45.71/6.87 % 45.71/6.87 (fact_25_zmult__commute) % 45.71/6.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (times_times_int(v0, v1) = v2) | % 45.71/6.87 ~ $i(v1) | ~ $i(v0) | (times_times_int(v1, v0) = v2 & $i(v2))) % 45.71/6.87 % 45.71/6.87 (fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) % 45.71/6.88 $i(m) & $i(pls) & $i(one_one_int) & $i(zero_zero_int) & $i(t) & ? [v0: $i] : % 45.71/6.88 ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: % 45.71/6.88 $i] : ? [v7: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & % 45.71/6.88 number_number_of_int(v2) = v3 & plus_plus_int(v4, one_one_int) = v5 & % 45.71/6.88 times_times_int(v5, zero_zero_int) = v7 & times_times_int(v5, t) = v6 & % 45.71/6.88 times_times_int(v3, m) = v4 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 45.71/6.88 $i(v2) & $i(v1) & $i(v0) & ord_less_int(v6, v7)) % 45.71/6.88 % 45.71/6.88 (fact_3_t) % 45.71/6.88 $i(s) & $i(m) & $i(pls) & $i(one_one_int) & $i(t) & ? [v0: $i] : ? [v1: $i] % 45.71/6.88 : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? % 45.71/6.88 [v7: $i] : ? [v8: $i] : (number_number_of_nat(v1) = v2 & power_power_int(s, % 45.71/6.88 v2) = v3 & bit1(pls) = v0 & bit0(v1) = v5 & bit0(v0) = v1 & % 45.71/6.88 number_number_of_int(v5) = v6 & plus_plus_int(v7, one_one_int) = v8 & % 45.71/6.88 plus_plus_int(v3, one_one_int) = v4 & times_times_int(v8, t) = v4 & % 45.71/6.88 times_times_int(v6, m) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 45.71/6.88 $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.88 % 45.71/6.88 (fact_63_le__special_I4_J) % 45.71/6.88 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 45.71/6.88 $i] : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 45.71/6.88 ord_less_eq_int(v2, one_one_int) | ord_less_eq_int(v1, v0)) & ! [v1: $i] % 45.71/6.88 : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 45.71/6.88 ord_less_eq_int(v1, v0) | ord_less_eq_int(v2, one_one_int))) % 45.71/6.88 % 45.71/6.88 (fact_64_le__special_I2_J) % 45.71/6.88 $i(pls) & $i(one_one_int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: % 45.71/6.88 $i] : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 45.71/6.88 ord_less_eq_int(v0, v1) | ord_less_eq_int(one_one_int, v2)) & ! [v1: $i] % 45.71/6.88 : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 45.71/6.88 ord_less_eq_int(one_one_int, v2) | ord_less_eq_int(v0, v1))) % 45.71/6.88 % 45.71/6.88 (fact_65_nat__1__add__1) % 45.71/6.88 $i(one_one_nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.88 (plus_plus_nat(one_one_nat, one_one_nat) = v0 & number_number_of_nat(v2) = v0 % 45.71/6.88 & bit1(pls) = v1 & bit0(v1) = v2 & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.88 % 45.71/6.88 (fact_66_mult__Pls) % 45.71/6.88 $i(pls) & ! [v0: $i] : ! [v1: $i] : (v1 = pls | ~ (times_times_int(pls, v0) % 45.71/6.88 = v1) | ~ $i(v0)) % 45.71/6.88 % 45.71/6.88 (fact_6_p0) % 45.71/6.89 $i(m) & $i(pls) & $i(one_one_int) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: % 45.71/6.89 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (bit1(pls) = % 45.71/6.89 v0 & bit0(v1) = v2 & bit0(v0) = v1 & number_number_of_int(v2) = v3 & % 45.71/6.89 plus_plus_int(v4, one_one_int) = v5 & times_times_int(v3, m) = v4 & $i(v5) & % 45.71/6.89 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ord_less_int(zero_zero_int, % 45.71/6.89 v5)) % 45.71/6.89 % 45.71/6.89 (fact_7_not__sum__power2__lt__zero) % 45.71/6.89 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.89 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.89 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 45.71/6.89 [v7: $i] : ( ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) % 45.71/6.89 = v5) | ~ (plus_plus_int(v5, v6) = v7) | ~ $i(v4) | ~ $i(v3) | ~ % 45.71/6.89 ord_less_int(v7, zero_zero_int))) % 45.71/6.89 % 45.71/6.89 (fact_82_nat__numeral__1__eq__1) % 45.71/6.89 $i(one_one_nat) & $i(pls) & ? [v0: $i] : (number_number_of_nat(v0) = % 45.71/6.89 one_one_nat & bit1(pls) = v0 & $i(v0)) % 45.71/6.89 % 45.71/6.89 (fact_83_Numeral1__eq1__nat) % 45.71/6.89 $i(one_one_nat) & $i(pls) & ? [v0: $i] : (number_number_of_nat(v0) = % 45.71/6.89 one_one_nat & bit1(pls) = v0 & $i(v0)) % 45.71/6.89 % 45.71/6.89 (fact_8_sum__power2__gt__zero__iff) % 45.71/6.89 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.89 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.89 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 45.71/6.89 [v7: $i] : (v4 = zero_zero_int | ~ (power_power_int(v4, v2) = v6) | ~ % 45.71/6.89 (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = v7) | ~ % 45.71/6.89 $i(v4) | ~ $i(v3) | ord_less_int(zero_zero_int, v7)) & ! [v3: $i] : ! % 45.71/6.89 [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v3 = zero_zero_int | % 45.71/6.89 ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = v5) | ~ % 45.71/6.89 (plus_plus_int(v5, v6) = v7) | ~ $i(v4) | ~ $i(v3) | % 45.71/6.89 ord_less_int(zero_zero_int, v7)) & ! [v3: $i] : ! [v4: $i] : ( ~ % 45.71/6.89 (power_power_int(zero_zero_int, v2) = v3) | ~ (plus_plus_int(v3, v3) = % 45.71/6.89 v4) | ~ ord_less_int(zero_zero_int, v4))) % 45.71/6.89 % 45.71/6.89 (fact_9_sum__power2__eq__zero__iff) % 45.71/6.89 $i(pls) & $i(zero_zero_int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.71/6.89 (number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 45.71/6.89 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 45.71/6.89 (v4 = zero_zero_int | ~ (power_power_int(v4, v2) = v6) | ~ % 45.71/6.89 (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = % 45.71/6.89 zero_zero_int) | ~ $i(v4) | ~ $i(v3)) & ! [v3: $i] : ! [v4: $i] : ! % 45.71/6.89 [v5: $i] : ! [v6: $i] : (v3 = zero_zero_int | ~ (power_power_int(v4, v2) = % 45.71/6.89 v6) | ~ (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = % 45.71/6.89 zero_zero_int) | ~ $i(v4) | ~ $i(v3)) & ! [v3: $i] : ! [v4: $i] : % 45.71/6.89 (v4 = zero_zero_int | ~ (power_power_int(zero_zero_int, v2) = v3) | ~ % 45.71/6.89 (plus_plus_int(v3, v3) = v4))) % 45.71/6.89 % 45.71/6.89 (function-axioms) % 45.71/6.90 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (times_times_nat(v3, v2) = v1) | ~ (times_times_nat(v3, v2) = v0)) & ! % 45.71/6.90 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (plus_plus_nat(v3, v2) = v1) | ~ (plus_plus_nat(v3, v2) = v0)) & ! [v0: % 45.71/6.90 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (power_power_nat(v3, v2) = v1) | ~ (power_power_nat(v3, v2) = v0)) & ! % 45.71/6.90 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (power_power_int(v3, v2) = v1) | ~ (power_power_int(v3, v2) = v0)) & ! % 45.71/6.90 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (plus_plus_int(v3, v2) = v1) | ~ (plus_plus_int(v3, v2) = v0)) & ! [v0: % 45.71/6.90 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 45.71/6.90 (times_times_int(v3, v2) = v1) | ~ (times_times_int(v3, v2) = v0)) & ! % 45.71/6.90 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (number_number_of_nat(v2) % 45.71/6.90 = v1) | ~ (number_number_of_nat(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 45.71/6.90 ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = v1) | ~ (bit1(v2) = v0)) & ! [v0: $i] % 45.71/6.90 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit0(v2) = v1) | ~ (bit0(v2) = % 45.71/6.90 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 45.71/6.90 (number_number_of_int(v2) = v1) | ~ (number_number_of_int(v2) = v0)) % 45.71/6.90 % 45.71/6.90 Further assumptions not needed in the proof: % 45.71/6.90 -------------------------------------------- % 45.71/6.90 fact_0__096t_A_060_A0_096, fact_100_right__distrib__number__of, % 45.71/6.90 fact_101_right__distrib__number__of, fact_102_zadd__assoc, % 45.71/6.90 fact_103_zadd__left__commute, fact_1_calculation_I1_J, fact_23_zle__refl, % 45.71/6.90 fact_26_zle__linear, fact_27_times__numeral__code_I5_J, % 45.71/6.90 fact_28_less__eq__number__of__int__code, fact_29_le__number__of, % 45.71/6.90 fact_30_zmult__assoc, fact_31_zle__trans, fact_32_zle__antisym, % 45.71/6.90 fact_33_zpower__zadd__distrib, fact_34_less__eq__int__code_I16_J, % 45.71/6.90 fact_35_rel__simps_I34_J, fact_36_rel__simps_I19_J, % 45.71/6.90 fact_37_less__eq__int__code_I13_J, fact_38_rel__simps_I31_J, fact_39_zless__le, % 45.71/6.90 fact_40_zadd__left__mono, fact_41_eq__number__of__0, fact_42_eq__0__number__of, % 45.71/6.90 fact_43_semiring__mult__number__of, fact_44_semiring__mult__number__of, % 45.71/6.90 fact_45_mult__number__of__left, fact_46_arith__simps_I32_J, % 45.71/6.90 fact_47_number__of__mult, fact_48_sum__squares__le__zero__iff, % 45.71/6.90 fact_49_sum__squares__ge__zero, fact_4_calculation_I2_J, % 45.71/6.90 fact_50_le__special_I3_J, fact_51_le__special_I1_J, fact_52_less__0__number__of, % 45.71/6.90 fact_53_le__number__of__eq__not__less, fact_54_le__number__of__eq__not__less, % 45.71/6.90 fact_55_rel__simps_I22_J, fact_56_less__eq__int__code_I14_J, % 45.71/6.90 fact_57_rel__simps_I32_J, fact_58_rel__simps_I27_J, fact_59_rel__simps_I21_J, % 45.71/6.90 fact_5__096_126_A1_A_060_061_At_096, fact_60_zadd__zless__mono, % 45.71/6.90 fact_61_nat__number__of__Pls, fact_62_semiring__norm_I113_J, fact_67_mult__Bit0, % 45.71/6.90 fact_68_less__number__of__int__code, fact_69_zmult__1__right, fact_70_zmult__1, % 45.71/6.90 fact_71_plus__numeral__code_I9_J, fact_72_zadd__zmult__distrib, % 45.71/6.90 fact_73_zadd__zmult__distrib2, fact_74_rel__simps_I29_J, % 45.71/6.90 fact_75_rel__simps_I5_J, fact_76_less__eq__int__code_I15_J, % 45.71/6.90 fact_77_rel__simps_I33_J, fact_78_less__int__code_I14_J, % 45.71/6.90 fact_79_rel__simps_I15_J, fact_80_less__nat__number__of, % 45.71/6.90 fact_81_int__one__le__iff__zero__less, fact_84_zless__imp__add1__zle, % 45.71/6.90 fact_85_add1__zle__eq, fact_86_zle__add1__eq__le, % 45.71/6.90 fact_87_semiring__add__number__of, fact_88_semiring__add__number__of, % 45.71/6.90 fact_89_add__nat__number__of, fact_90_le__imp__0__less, fact_91_eq__number__of, % 45.71/6.90 fact_92_number__of__reorient, fact_93_number__of__reorient, % 45.71/6.90 fact_94_rel__simps_I51_J, fact_95_rel__simps_I48_J, fact_96_zless__linear, % 45.71/6.90 fact_97_sum__squares__eq__zero__iff, fact_98_left__distrib__number__of, % 45.71/6.90 fact_99_left__distrib__number__of % 45.71/6.90 % 45.71/6.90 Those formulas are unsatisfiable: % 45.71/6.90 --------------------------------- % 45.71/6.90 % 45.71/6.90 Begin of proof % 45.71/6.90 | % 45.71/6.90 | ALPHA: (fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) % 45.71/6.90 | implies: % 45.71/6.90 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 45.71/6.90 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (bit1(pls) = v0 & bit0(v1) = % 45.71/6.90 | v2 & bit0(v0) = v1 & number_number_of_int(v2) = v3 & % 45.71/6.90 | plus_plus_int(v4, one_one_int) = v5 & times_times_int(v5, % 45.71/6.90 | zero_zero_int) = v7 & times_times_int(v5, t) = v6 & % 45.71/6.90 | times_times_int(v3, m) = v4 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 45.71/6.90 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ord_less_int(v6, v7)) % 45.71/6.90 | % 45.71/6.90 | ALPHA: (fact_3_t) implies: % 45.71/6.90 | (2) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 45.71/6.90 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 45.71/6.90 | (number_number_of_nat(v1) = v2 & power_power_int(s, v2) = v3 & % 45.71/6.90 | bit1(pls) = v0 & bit0(v1) = v5 & bit0(v0) = v1 & % 45.71/6.90 | number_number_of_int(v5) = v6 & plus_plus_int(v7, one_one_int) = v8 & % 45.71/6.90 | plus_plus_int(v3, one_one_int) = v4 & times_times_int(v8, t) = v4 & % 45.71/6.90 | times_times_int(v6, m) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 45.71/6.90 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 45.71/6.91 | % 45.71/6.91 | ALPHA: (fact_6_p0) implies: % 45.71/6.91 | (3) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 45.71/6.91 | ? [v5: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & % 45.71/6.91 | number_number_of_int(v2) = v3 & plus_plus_int(v4, one_one_int) = v5 & % 45.71/6.91 | times_times_int(v3, m) = v4 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 45.71/6.91 | $i(v1) & $i(v0) & ord_less_int(zero_zero_int, v5)) % 45.71/6.91 | % 45.71/6.91 | ALPHA: (fact_7_not__sum__power2__lt__zero) implies: % 46.10/6.91 | (4) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.91 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.91 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( % 46.10/6.91 | ~ (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = % 46.10/6.91 | v5) | ~ (plus_plus_int(v5, v6) = v7) | ~ $i(v4) | ~ $i(v3) | % 46.10/6.91 | ~ ord_less_int(v7, zero_zero_int))) % 46.10/6.91 | % 46.10/6.91 | ALPHA: (fact_8_sum__power2__gt__zero__iff) implies: % 46.10/6.91 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.91 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.91 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 46.10/6.91 | (v4 = zero_zero_int | ~ (power_power_int(v4, v2) = v6) | ~ % 46.10/6.91 | (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = v7) | % 46.10/6.91 | ~ $i(v4) | ~ $i(v3) | ord_less_int(zero_zero_int, v7)) & ! [v3: % 46.10/6.91 | $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v3 = % 46.10/6.91 | zero_zero_int | ~ (power_power_int(v4, v2) = v6) | ~ % 46.10/6.91 | (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = v7) | % 46.10/6.91 | ~ $i(v4) | ~ $i(v3) | ord_less_int(zero_zero_int, v7)) & ! [v3: % 46.10/6.91 | $i] : ! [v4: $i] : ( ~ (power_power_int(zero_zero_int, v2) = v3) | % 46.10/6.91 | ~ (plus_plus_int(v3, v3) = v4) | ~ ord_less_int(zero_zero_int, % 46.10/6.91 | v4))) % 46.10/6.91 | % 46.10/6.91 | ALPHA: (fact_9_sum__power2__eq__zero__iff) implies: % 46.10/6.91 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.91 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.91 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v4 = % 46.10/6.91 | zero_zero_int | ~ (power_power_int(v4, v2) = v6) | ~ % 46.10/6.91 | (power_power_int(v3, v2) = v5) | ~ (plus_plus_int(v5, v6) = % 46.10/6.91 | zero_zero_int) | ~ $i(v4) | ~ $i(v3)) & ! [v3: $i] : ! [v4: % 46.10/6.91 | $i] : ! [v5: $i] : ! [v6: $i] : (v3 = zero_zero_int | ~ % 46.10/6.91 | (power_power_int(v4, v2) = v6) | ~ (power_power_int(v3, v2) = v5) % 46.10/6.91 | | ~ (plus_plus_int(v5, v6) = zero_zero_int) | ~ $i(v4) | ~ % 46.10/6.91 | $i(v3)) & ! [v3: $i] : ! [v4: $i] : (v4 = zero_zero_int | ~ % 46.10/6.91 | (power_power_int(zero_zero_int, v2) = v3) | ~ (plus_plus_int(v3, % 46.10/6.91 | v3) = v4))) % 46.10/6.91 | % 46.10/6.91 | ALPHA: (fact_10_power2__less__0) implies: % 46.10/6.91 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.91 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.91 | [v3: $i] : ! [v4: $i] : ( ~ (power_power_int(v3, v2) = v4) | ~ % 46.10/6.91 | $i(v3) | ~ ord_less_int(v4, zero_zero_int))) % 46.10/6.91 | % 46.10/6.91 | ALPHA: (fact_11_zero__less__power2) implies: % 46.10/6.91 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.91 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.91 | [v3: $i] : ! [v4: $i] : (v3 = zero_zero_int | ~ % 46.10/6.91 | (power_power_int(v3, v2) = v4) | ~ $i(v3) | % 46.10/6.92 | ord_less_int(zero_zero_int, v4)) & ! [v3: $i] : ( ~ % 46.10/6.92 | (power_power_int(zero_zero_int, v2) = v3) | ~ % 46.10/6.92 | ord_less_int(zero_zero_int, v3))) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_12_one__power2) implies: % 46.10/6.92 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (power_power_nat(one_one_nat, % 46.10/6.92 | v2) = one_one_nat & number_number_of_nat(v1) = v2 & bit1(pls) = v0 % 46.10/6.92 | & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_13_one__power2) implies: % 46.10/6.92 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.92 | v2 & power_power_int(one_one_int, v2) = one_one_int & bit1(pls) = v0 % 46.10/6.92 | & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_14_zero__power2) implies: % 46.10/6.92 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 46.10/6.92 | (power_power_nat(zero_zero_nat, v2) = zero_zero_nat & % 46.10/6.92 | number_number_of_nat(v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & % 46.10/6.92 | $i(v2) & $i(v1) & $i(v0)) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_15_zero__power2) implies: % 46.10/6.92 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.92 | v2 & power_power_int(zero_zero_int, v2) = zero_zero_int & bit1(pls) % 46.10/6.92 | = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0)) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_16_zero__eq__power2) implies: % 46.10/6.92 | (13) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of_nat(v1) = % 46.10/6.92 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 46.10/6.92 | [v3: $i] : (v3 = zero_zero_int | ~ (power_power_int(v3, v2) = % 46.10/6.92 | zero_zero_int) | ~ $i(v3)) & ! [v3: $i] : (v3 = zero_zero_int % 46.10/6.92 | | ~ (power_power_int(zero_zero_int, v2) = v3))) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_17_add__special_I2_J) implies: % 46.10/6.92 | (14) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 46.10/6.92 | ~ (plus_plus_int(v0, v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: % 46.10/6.92 | $i] : (number_number_of_int(v2) = v4 & number_number_of_int(v1) % 46.10/6.92 | = v3 & plus_plus_int(one_one_int, v3) = v4 & $i(v4) & $i(v3)))) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_18_add__special_I3_J) implies: % 46.10/6.92 | (15) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 46.10/6.92 | ~ (plus_plus_int(v1, v0) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: % 46.10/6.92 | $i] : (number_number_of_int(v2) = v4 & number_number_of_int(v1) % 46.10/6.92 | = v3 & plus_plus_int(v3, one_one_int) = v4 & $i(v4) & $i(v3)))) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_19_t__l__p) implies: % 46.10/6.92 | (16) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 46.10/6.92 | ? [v5: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & % 46.10/6.92 | number_number_of_int(v2) = v3 & plus_plus_int(v4, one_one_int) = v5 % 46.10/6.92 | & times_times_int(v3, m) = v4 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 46.10/6.92 | $i(v1) & $i(v0) & ord_less_int(t, v5)) % 46.10/6.92 | % 46.10/6.92 | ALPHA: (fact_20__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_) % 46.10/6.92 | implies: % 46.10/6.92 | (17) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 46.10/6.92 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 46.10/6.92 | (number_number_of_nat(v1) = v2 & power_power_int(s, v2) = v3 & % 46.10/6.92 | bit1(pls) = v0 & bit0(v1) = v5 & bit0(v0) = v1 & % 46.10/6.92 | number_number_of_int(v5) = v6 & plus_plus_int(v7, one_one_int) = v8 % 46.10/6.92 | & plus_plus_int(v3, one_one_int) = v4 & times_times_int(v8, v9) = v4 % 46.10/6.92 | & times_times_int(v6, m) = v7 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 46.10/6.93 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_21_p) implies: % 46.10/6.93 | (18) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 46.10/6.93 | ? [v5: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & % 46.10/6.93 | number_number_of_int(v2) = v3 & plus_plus_int(v4, one_one_int) = v5 % 46.10/6.93 | & times_times_int(v3, m) = v4 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 46.10/6.93 | $i(v1) & $i(v0) & zprime(v5)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_22_qf1pt) implies: % 46.10/6.93 | (19) $i(m) % 46.10/6.93 | (20) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 46.10/6.93 | ? [v5: $i] : ? [v6: $i] : (bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) % 46.10/6.93 | = v1 & number_number_of_int(v2) = v3 & plus_plus_int(v4, % 46.10/6.93 | one_one_int) = v5 & times_times_int(v5, t) = v6 & % 46.10/6.93 | times_times_int(v3, m) = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 46.10/6.93 | $i(v2) & $i(v1) & $i(v0) & twoSqu526106917sum2sq(v6)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_63_le__special_I4_J) implies: % 46.10/6.93 | (21) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 46.10/6.93 | ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 46.10/6.93 | ord_less_eq_int(v2, one_one_int) | ord_less_eq_int(v1, v0)) & ! % 46.10/6.93 | [v1: $i] : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ % 46.10/6.93 | $i(v1) | ~ ord_less_eq_int(v1, v0) | ord_less_eq_int(v2, % 46.10/6.93 | one_one_int))) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_64_le__special_I2_J) implies: % 46.10/6.93 | (22) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ( % 46.10/6.93 | ~ (number_number_of_int(v1) = v2) | ~ $i(v1) | ~ % 46.10/6.93 | ord_less_eq_int(v0, v1) | ord_less_eq_int(one_one_int, v2)) & ! % 46.10/6.93 | [v1: $i] : ! [v2: $i] : ( ~ (number_number_of_int(v1) = v2) | ~ % 46.10/6.93 | $i(v1) | ~ ord_less_eq_int(one_one_int, v2) | ord_less_eq_int(v0, % 46.10/6.93 | v1))) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_65_nat__1__add__1) implies: % 46.10/6.93 | (23) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (plus_plus_nat(one_one_nat, % 46.10/6.93 | one_one_nat) = v0 & number_number_of_nat(v2) = v0 & bit1(pls) = v1 % 46.10/6.93 | & bit0(v1) = v2 & $i(v2) & $i(v1) & $i(v0)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_66_mult__Pls) implies: % 46.10/6.93 | (24) ! [v0: $i] : ! [v1: $i] : (v1 = pls | ~ (times_times_int(pls, v0) = % 46.10/6.93 | v1) | ~ $i(v0)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_83_Numeral1__eq1__nat) implies: % 46.10/6.93 | (25) ? [v0: $i] : (number_number_of_nat(v0) = one_one_nat & bit1(pls) = v0 % 46.10/6.93 | & $i(v0)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (fact_105_zero__is__num__zero) implies: % 46.10/6.93 | (26) number_number_of_int(pls) = zero_zero_int % 46.10/6.93 | % 46.10/6.93 | ALPHA: (conj_0) implies: % 46.10/6.93 | (27) $i(zero_zero_int) % 46.10/6.93 | (28) $i(one_one_int) % 46.10/6.93 | (29) $i(pls) % 46.10/6.93 | (30) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 46.10/6.93 | (number_number_of_nat(v1) = v2 & power_power_int(s, v2) = v3 & % 46.10/6.93 | bit1(pls) = v0 & bit0(v0) = v1 & plus_plus_int(v3, one_one_int) = v4 % 46.10/6.93 | & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ ord_less_int(v4, % 46.10/6.93 | zero_zero_int)) % 46.10/6.93 | % 46.10/6.93 | ALPHA: (function-axioms) implies: % 46.10/6.94 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 46.10/6.94 | (number_number_of_int(v2) = v1) | ~ (number_number_of_int(v2) = % 46.10/6.94 | v0)) % 46.10/6.94 | (32) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit0(v2) = % 46.10/6.94 | v1) | ~ (bit0(v2) = v0)) % 46.10/6.94 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = % 46.10/6.94 | v1) | ~ (bit1(v2) = v0)) % 46.10/6.94 | (34) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 46.10/6.94 | (number_number_of_nat(v2) = v1) | ~ (number_number_of_nat(v2) = % 46.10/6.94 | v0)) % 46.10/6.94 | (35) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 46.10/6.94 | (times_times_int(v3, v2) = v1) | ~ (times_times_int(v3, v2) = v0)) % 46.10/6.94 | (36) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 46.10/6.94 | (plus_plus_int(v3, v2) = v1) | ~ (plus_plus_int(v3, v2) = v0)) % 46.10/6.94 | (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 46.10/6.94 | (power_power_int(v3, v2) = v1) | ~ (power_power_int(v3, v2) = v0)) % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (25) with fresh symbol all_74_0 gives: % 46.10/6.94 | (38) number_number_of_nat(all_74_0) = one_one_nat & bit1(pls) = all_74_0 & % 46.10/6.94 | $i(all_74_0) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (38) implies: % 46.10/6.94 | (39) bit1(pls) = all_74_0 % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (25) with fresh symbol all_76_0 gives: % 46.10/6.94 | (40) number_number_of_nat(all_76_0) = one_one_nat & bit1(pls) = all_76_0 & % 46.10/6.94 | $i(all_76_0) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (40) implies: % 46.10/6.94 | (41) bit1(pls) = all_76_0 % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (9) with fresh symbols all_80_0, all_80_1, all_80_2 % 46.10/6.94 | gives: % 46.10/6.94 | (42) power_power_nat(one_one_nat, all_80_0) = one_one_nat & % 46.10/6.94 | number_number_of_nat(all_80_1) = all_80_0 & bit1(pls) = all_80_2 & % 46.10/6.94 | bit0(all_80_2) = all_80_1 & $i(all_80_0) & $i(all_80_1) & $i(all_80_2) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (42) implies: % 46.10/6.94 | (43) bit0(all_80_2) = all_80_1 % 46.10/6.94 | (44) bit1(pls) = all_80_2 % 46.10/6.94 | (45) number_number_of_nat(all_80_1) = all_80_0 % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (23) with fresh symbols all_82_0, all_82_1, all_82_2 % 46.10/6.94 | gives: % 46.10/6.94 | (46) plus_plus_nat(one_one_nat, one_one_nat) = all_82_2 & % 46.10/6.94 | number_number_of_nat(all_82_0) = all_82_2 & bit1(pls) = all_82_1 & % 46.10/6.94 | bit0(all_82_1) = all_82_0 & $i(all_82_0) & $i(all_82_1) & $i(all_82_2) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (46) implies: % 46.10/6.94 | (47) bit0(all_82_1) = all_82_0 % 46.10/6.94 | (48) bit1(pls) = all_82_1 % 46.10/6.94 | (49) number_number_of_nat(all_82_0) = all_82_2 % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (10) with fresh symbols all_84_0, all_84_1, all_84_2 % 46.10/6.94 | gives: % 46.10/6.94 | (50) number_number_of_nat(all_84_1) = all_84_0 & % 46.10/6.94 | power_power_int(one_one_int, all_84_0) = one_one_int & bit1(pls) = % 46.10/6.94 | all_84_2 & bit0(all_84_2) = all_84_1 & $i(all_84_0) & $i(all_84_1) & % 46.10/6.94 | $i(all_84_2) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (50) implies: % 46.10/6.94 | (51) bit0(all_84_2) = all_84_1 % 46.10/6.94 | (52) bit1(pls) = all_84_2 % 46.10/6.94 | (53) number_number_of_nat(all_84_1) = all_84_0 % 46.10/6.94 | % 46.10/6.94 | DELTA: instantiating (12) with fresh symbols all_86_0, all_86_1, all_86_2 % 46.10/6.94 | gives: % 46.10/6.94 | (54) number_number_of_nat(all_86_1) = all_86_0 & % 46.10/6.94 | power_power_int(zero_zero_int, all_86_0) = zero_zero_int & bit1(pls) = % 46.10/6.94 | all_86_2 & bit0(all_86_2) = all_86_1 & $i(all_86_0) & $i(all_86_1) & % 46.10/6.94 | $i(all_86_2) % 46.10/6.94 | % 46.10/6.94 | ALPHA: (54) implies: % 46.10/6.95 | (55) bit0(all_86_2) = all_86_1 % 46.10/6.95 | (56) bit1(pls) = all_86_2 % 46.10/6.95 | (57) power_power_int(zero_zero_int, all_86_0) = zero_zero_int % 46.10/6.95 | (58) number_number_of_nat(all_86_1) = all_86_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (11) with fresh symbols all_88_0, all_88_1, all_88_2 % 46.10/6.95 | gives: % 46.10/6.95 | (59) power_power_nat(zero_zero_nat, all_88_0) = zero_zero_nat & % 46.10/6.95 | number_number_of_nat(all_88_1) = all_88_0 & bit1(pls) = all_88_2 & % 46.10/6.95 | bit0(all_88_2) = all_88_1 & $i(all_88_0) & $i(all_88_1) & $i(all_88_2) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (59) implies: % 46.10/6.95 | (60) bit0(all_88_2) = all_88_1 % 46.10/6.95 | (61) bit1(pls) = all_88_2 % 46.10/6.95 | (62) number_number_of_nat(all_88_1) = all_88_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (14) with fresh symbol all_90_0 gives: % 46.10/6.95 | (63) bit1(pls) = all_90_0 & $i(all_90_0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 46.10/6.95 | (plus_plus_int(all_90_0, v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? % 46.10/6.95 | [v3: $i] : (number_number_of_int(v1) = v3 & number_number_of_int(v0) % 46.10/6.95 | = v2 & plus_plus_int(one_one_int, v2) = v3 & $i(v3) & $i(v2))) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (63) implies: % 46.10/6.95 | (64) bit1(pls) = all_90_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (15) with fresh symbol all_93_0 gives: % 46.10/6.95 | (65) bit1(pls) = all_93_0 & $i(all_93_0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 46.10/6.95 | (plus_plus_int(v0, all_93_0) = v1) | ~ $i(v0) | ? [v2: $i] : ? % 46.10/6.95 | [v3: $i] : (number_number_of_int(v1) = v3 & number_number_of_int(v0) % 46.10/6.95 | = v2 & plus_plus_int(v2, one_one_int) = v3 & $i(v3) & $i(v2))) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (65) implies: % 46.10/6.95 | (66) bit1(pls) = all_93_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (7) with fresh symbols all_96_0, all_96_1, all_96_2 % 46.10/6.95 | gives: % 46.10/6.95 | (67) number_number_of_nat(all_96_1) = all_96_0 & bit1(pls) = all_96_2 & % 46.10/6.95 | bit0(all_96_2) = all_96_1 & $i(all_96_0) & $i(all_96_1) & $i(all_96_2) % 46.10/6.95 | & ! [v0: $i] : ! [v1: $i] : ( ~ (power_power_int(v0, all_96_0) = v1) % 46.10/6.95 | | ~ $i(v0) | ~ ord_less_int(v1, zero_zero_int)) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (67) implies: % 46.10/6.95 | (68) bit0(all_96_2) = all_96_1 % 46.10/6.95 | (69) bit1(pls) = all_96_2 % 46.10/6.95 | (70) number_number_of_nat(all_96_1) = all_96_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (22) with fresh symbol all_99_0 gives: % 46.10/6.95 | (71) bit1(pls) = all_99_0 & $i(all_99_0) & ! [v0: $i] : ! [v1: $i] : ( ~ % 46.10/6.95 | (number_number_of_int(v0) = v1) | ~ $i(v0) | ~ % 46.10/6.95 | ord_less_eq_int(all_99_0, v0) | ord_less_eq_int(one_one_int, v1)) & % 46.10/6.95 | ! [v0: $i] : ! [v1: $i] : ( ~ (number_number_of_int(v0) = v1) | ~ % 46.10/6.95 | $i(v0) | ~ ord_less_eq_int(one_one_int, v1) | % 46.10/6.95 | ord_less_eq_int(all_99_0, v0)) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (71) implies: % 46.10/6.95 | (72) bit1(pls) = all_99_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (21) with fresh symbol all_102_0 gives: % 46.10/6.95 | (73) bit1(pls) = all_102_0 & $i(all_102_0) & ! [v0: $i] : ! [v1: $i] : ( % 46.10/6.95 | ~ (number_number_of_int(v0) = v1) | ~ $i(v0) | ~ % 46.10/6.95 | ord_less_eq_int(v1, one_one_int) | ord_less_eq_int(v0, all_102_0)) & % 46.10/6.95 | ! [v0: $i] : ! [v1: $i] : ( ~ (number_number_of_int(v0) = v1) | ~ % 46.10/6.95 | $i(v0) | ~ ord_less_eq_int(v0, all_102_0) | ord_less_eq_int(v1, % 46.10/6.95 | one_one_int)) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (73) implies: % 46.10/6.95 | (74) bit1(pls) = all_102_0 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (30) with fresh symbols all_105_0, all_105_1, all_105_2, % 46.10/6.95 | all_105_3, all_105_4 gives: % 46.10/6.95 | (75) number_number_of_nat(all_105_3) = all_105_2 & power_power_int(s, % 46.10/6.95 | all_105_2) = all_105_1 & bit1(pls) = all_105_4 & bit0(all_105_4) = % 46.10/6.95 | all_105_3 & plus_plus_int(all_105_1, one_one_int) = all_105_0 & % 46.10/6.95 | $i(all_105_0) & $i(all_105_1) & $i(all_105_2) & $i(all_105_3) & % 46.10/6.95 | $i(all_105_4) & ~ ord_less_int(all_105_0, zero_zero_int) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (75) implies: % 46.10/6.95 | (76) ~ ord_less_int(all_105_0, zero_zero_int) % 46.10/6.95 | (77) plus_plus_int(all_105_1, one_one_int) = all_105_0 % 46.10/6.95 | (78) bit0(all_105_4) = all_105_3 % 46.10/6.95 | (79) bit1(pls) = all_105_4 % 46.10/6.95 | (80) power_power_int(s, all_105_2) = all_105_1 % 46.10/6.95 | (81) number_number_of_nat(all_105_3) = all_105_2 % 46.10/6.95 | % 46.10/6.95 | DELTA: instantiating (13) with fresh symbols all_108_0, all_108_1, all_108_2 % 46.10/6.95 | gives: % 46.10/6.95 | (82) number_number_of_nat(all_108_1) = all_108_0 & bit1(pls) = all_108_2 & % 46.10/6.95 | bit0(all_108_2) = all_108_1 & $i(all_108_0) & $i(all_108_1) & % 46.10/6.95 | $i(all_108_2) & ! [v0: $i] : (v0 = zero_zero_int | ~ % 46.10/6.95 | (power_power_int(v0, all_108_0) = zero_zero_int) | ~ $i(v0)) & ! % 46.10/6.95 | [v0: $i] : (v0 = zero_zero_int | ~ (power_power_int(zero_zero_int, % 46.10/6.95 | all_108_0) = v0)) % 46.10/6.95 | % 46.10/6.95 | ALPHA: (82) implies: % 46.10/6.95 | (83) bit0(all_108_2) = all_108_1 % 46.10/6.96 | (84) bit1(pls) = all_108_2 % 46.10/6.96 | (85) number_number_of_nat(all_108_1) = all_108_0 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (4) with fresh symbols all_111_0, all_111_1, all_111_2 % 46.10/6.96 | gives: % 46.10/6.96 | (86) number_number_of_nat(all_111_1) = all_111_0 & bit1(pls) = all_111_2 & % 46.10/6.96 | bit0(all_111_2) = all_111_1 & $i(all_111_0) & $i(all_111_1) & % 46.10/6.96 | $i(all_111_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 46.10/6.96 | : ! [v4: $i] : ( ~ (power_power_int(v1, all_111_0) = v3) | ~ % 46.10/6.96 | (power_power_int(v0, all_111_0) = v2) | ~ (plus_plus_int(v2, v3) = % 46.10/6.96 | v4) | ~ $i(v1) | ~ $i(v0) | ~ ord_less_int(v4, zero_zero_int)) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (86) implies: % 46.10/6.96 | (87) bit0(all_111_2) = all_111_1 % 46.10/6.96 | (88) bit1(pls) = all_111_2 % 46.10/6.96 | (89) number_number_of_nat(all_111_1) = all_111_0 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (8) with fresh symbols all_114_0, all_114_1, all_114_2 % 46.10/6.96 | gives: % 46.10/6.96 | (90) number_number_of_nat(all_114_1) = all_114_0 & bit1(pls) = all_114_2 & % 46.10/6.96 | bit0(all_114_2) = all_114_1 & $i(all_114_0) & $i(all_114_1) & % 46.10/6.96 | $i(all_114_2) & ! [v0: $i] : ! [v1: $i] : (v0 = zero_zero_int | ~ % 46.10/6.96 | (power_power_int(v0, all_114_0) = v1) | ~ $i(v0) | % 46.10/6.96 | ord_less_int(zero_zero_int, v1)) & ! [v0: $i] : ( ~ % 46.10/6.96 | (power_power_int(zero_zero_int, all_114_0) = v0) | ~ % 46.10/6.96 | ord_less_int(zero_zero_int, v0)) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (90) implies: % 46.10/6.96 | (91) bit0(all_114_2) = all_114_1 % 46.10/6.96 | (92) bit1(pls) = all_114_2 % 46.10/6.96 | (93) number_number_of_nat(all_114_1) = all_114_0 % 46.10/6.96 | (94) ! [v0: $i] : ( ~ (power_power_int(zero_zero_int, all_114_0) = v0) | % 46.10/6.96 | ~ ord_less_int(zero_zero_int, v0)) % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (3) with fresh symbols all_117_0, all_117_1, all_117_2, % 46.10/6.96 | all_117_3, all_117_4, all_117_5 gives: % 46.10/6.96 | (95) bit1(pls) = all_117_5 & bit0(all_117_4) = all_117_3 & bit0(all_117_5) % 46.10/6.96 | = all_117_4 & number_number_of_int(all_117_3) = all_117_2 & % 46.10/6.96 | plus_plus_int(all_117_1, one_one_int) = all_117_0 & % 46.10/6.96 | times_times_int(all_117_2, m) = all_117_1 & $i(all_117_0) & % 46.10/6.96 | $i(all_117_1) & $i(all_117_2) & $i(all_117_3) & $i(all_117_4) & % 46.10/6.96 | $i(all_117_5) & ord_less_int(zero_zero_int, all_117_0) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (95) implies: % 46.10/6.96 | (96) times_times_int(all_117_2, m) = all_117_1 % 46.10/6.96 | (97) plus_plus_int(all_117_1, one_one_int) = all_117_0 % 46.10/6.96 | (98) number_number_of_int(all_117_3) = all_117_2 % 46.10/6.96 | (99) bit0(all_117_5) = all_117_4 % 46.10/6.96 | (100) bit0(all_117_4) = all_117_3 % 46.10/6.96 | (101) bit1(pls) = all_117_5 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (18) with fresh symbols all_119_0, all_119_1, all_119_2, % 46.10/6.96 | all_119_3, all_119_4, all_119_5 gives: % 46.10/6.96 | (102) bit1(pls) = all_119_5 & bit0(all_119_4) = all_119_3 & bit0(all_119_5) % 46.10/6.96 | = all_119_4 & number_number_of_int(all_119_3) = all_119_2 & % 46.10/6.96 | plus_plus_int(all_119_1, one_one_int) = all_119_0 & % 46.10/6.96 | times_times_int(all_119_2, m) = all_119_1 & $i(all_119_0) & % 46.10/6.96 | $i(all_119_1) & $i(all_119_2) & $i(all_119_3) & $i(all_119_4) & % 46.10/6.96 | $i(all_119_5) & zprime(all_119_0) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (102) implies: % 46.10/6.96 | (103) $i(all_119_2) % 46.10/6.96 | (104) $i(all_119_0) % 46.10/6.96 | (105) times_times_int(all_119_2, m) = all_119_1 % 46.10/6.96 | (106) plus_plus_int(all_119_1, one_one_int) = all_119_0 % 46.10/6.96 | (107) number_number_of_int(all_119_3) = all_119_2 % 46.10/6.96 | (108) bit0(all_119_5) = all_119_4 % 46.10/6.96 | (109) bit0(all_119_4) = all_119_3 % 46.10/6.96 | (110) bit1(pls) = all_119_5 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (16) with fresh symbols all_121_0, all_121_1, all_121_2, % 46.10/6.96 | all_121_3, all_121_4, all_121_5 gives: % 46.10/6.96 | (111) bit1(pls) = all_121_5 & bit0(all_121_4) = all_121_3 & bit0(all_121_5) % 46.10/6.96 | = all_121_4 & number_number_of_int(all_121_3) = all_121_2 & % 46.10/6.96 | plus_plus_int(all_121_1, one_one_int) = all_121_0 & % 46.10/6.96 | times_times_int(all_121_2, m) = all_121_1 & $i(all_121_0) & % 46.10/6.96 | $i(all_121_1) & $i(all_121_2) & $i(all_121_3) & $i(all_121_4) & % 46.10/6.96 | $i(all_121_5) & ord_less_int(t, all_121_0) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (111) implies: % 46.10/6.96 | (112) times_times_int(all_121_2, m) = all_121_1 % 46.10/6.96 | (113) plus_plus_int(all_121_1, one_one_int) = all_121_0 % 46.10/6.96 | (114) number_number_of_int(all_121_3) = all_121_2 % 46.10/6.96 | (115) bit0(all_121_5) = all_121_4 % 46.10/6.96 | (116) bit0(all_121_4) = all_121_3 % 46.10/6.96 | (117) bit1(pls) = all_121_5 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (20) with fresh symbols all_123_0, all_123_1, all_123_2, % 46.10/6.96 | all_123_3, all_123_4, all_123_5, all_123_6 gives: % 46.10/6.96 | (118) bit1(pls) = all_123_6 & bit0(all_123_5) = all_123_4 & bit0(all_123_6) % 46.10/6.96 | = all_123_5 & number_number_of_int(all_123_4) = all_123_3 & % 46.10/6.96 | plus_plus_int(all_123_2, one_one_int) = all_123_1 & % 46.10/6.96 | times_times_int(all_123_1, t) = all_123_0 & % 46.10/6.96 | times_times_int(all_123_3, m) = all_123_2 & $i(all_123_0) & % 46.10/6.96 | $i(all_123_1) & $i(all_123_2) & $i(all_123_3) & $i(all_123_4) & % 46.10/6.96 | $i(all_123_5) & $i(all_123_6) & twoSqu526106917sum2sq(all_123_0) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (118) implies: % 46.10/6.96 | (119) times_times_int(all_123_3, m) = all_123_2 % 46.10/6.96 | (120) plus_plus_int(all_123_2, one_one_int) = all_123_1 % 46.10/6.96 | (121) number_number_of_int(all_123_4) = all_123_3 % 46.10/6.96 | (122) bit0(all_123_6) = all_123_5 % 46.10/6.96 | (123) bit0(all_123_5) = all_123_4 % 46.10/6.96 | (124) bit1(pls) = all_123_6 % 46.10/6.96 | % 46.10/6.96 | DELTA: instantiating (1) with fresh symbols all_125_0, all_125_1, all_125_2, % 46.10/6.96 | all_125_3, all_125_4, all_125_5, all_125_6, all_125_7 gives: % 46.10/6.96 | (125) bit1(pls) = all_125_7 & bit0(all_125_6) = all_125_5 & bit0(all_125_7) % 46.10/6.96 | = all_125_6 & number_number_of_int(all_125_5) = all_125_4 & % 46.10/6.96 | plus_plus_int(all_125_3, one_one_int) = all_125_2 & % 46.10/6.96 | times_times_int(all_125_2, zero_zero_int) = all_125_0 & % 46.10/6.96 | times_times_int(all_125_2, t) = all_125_1 & % 46.10/6.96 | times_times_int(all_125_4, m) = all_125_3 & $i(all_125_0) & % 46.10/6.96 | $i(all_125_1) & $i(all_125_2) & $i(all_125_3) & $i(all_125_4) & % 46.10/6.96 | $i(all_125_5) & $i(all_125_6) & $i(all_125_7) & % 46.10/6.96 | ord_less_int(all_125_1, all_125_0) % 46.10/6.96 | % 46.10/6.96 | ALPHA: (125) implies: % 46.10/6.96 | (126) ord_less_int(all_125_1, all_125_0) % 46.10/6.96 | (127) times_times_int(all_125_4, m) = all_125_3 % 46.10/6.96 | (128) times_times_int(all_125_2, t) = all_125_1 % 46.10/6.97 | (129) times_times_int(all_125_2, zero_zero_int) = all_125_0 % 46.10/6.97 | (130) plus_plus_int(all_125_3, one_one_int) = all_125_2 % 46.10/6.97 | (131) number_number_of_int(all_125_5) = all_125_4 % 46.10/6.97 | (132) bit0(all_125_7) = all_125_6 % 46.10/6.97 | (133) bit0(all_125_6) = all_125_5 % 46.10/6.97 | (134) bit1(pls) = all_125_7 % 46.10/6.97 | % 46.10/6.97 | DELTA: instantiating (2) with fresh symbols all_127_0, all_127_1, all_127_2, % 46.10/6.97 | all_127_3, all_127_4, all_127_5, all_127_6, all_127_7, all_127_8 gives: % 46.10/6.97 | (135) number_number_of_nat(all_127_7) = all_127_6 & power_power_int(s, % 46.10/6.97 | all_127_6) = all_127_5 & bit1(pls) = all_127_8 & bit0(all_127_7) = % 46.10/6.97 | all_127_3 & bit0(all_127_8) = all_127_7 & % 46.10/6.97 | number_number_of_int(all_127_3) = all_127_2 & % 46.10/6.97 | plus_plus_int(all_127_1, one_one_int) = all_127_0 & % 46.10/6.97 | plus_plus_int(all_127_5, one_one_int) = all_127_4 & % 46.10/6.97 | times_times_int(all_127_0, t) = all_127_4 & % 46.10/6.97 | times_times_int(all_127_2, m) = all_127_1 & $i(all_127_0) & % 46.10/6.97 | $i(all_127_1) & $i(all_127_2) & $i(all_127_3) & $i(all_127_4) & % 46.10/6.97 | $i(all_127_5) & $i(all_127_6) & $i(all_127_7) & $i(all_127_8) % 46.10/6.97 | % 46.10/6.97 | ALPHA: (135) implies: % 46.10/6.97 | (136) times_times_int(all_127_2, m) = all_127_1 % 46.10/6.97 | (137) times_times_int(all_127_0, t) = all_127_4 % 46.10/6.97 | (138) plus_plus_int(all_127_5, one_one_int) = all_127_4 % 46.10/6.97 | (139) plus_plus_int(all_127_1, one_one_int) = all_127_0 % 46.10/6.97 | (140) number_number_of_int(all_127_3) = all_127_2 % 46.10/6.97 | (141) bit0(all_127_8) = all_127_7 % 46.10/6.97 | (142) bit0(all_127_7) = all_127_3 % 46.10/6.97 | (143) bit1(pls) = all_127_8 % 46.10/6.97 | (144) power_power_int(s, all_127_6) = all_127_5 % 46.10/6.97 | (145) number_number_of_nat(all_127_7) = all_127_6 % 46.10/6.97 | % 46.10/6.97 | DELTA: instantiating (17) with fresh symbols all_129_0, all_129_1, all_129_2, % 46.10/6.97 | all_129_3, all_129_4, all_129_5, all_129_6, all_129_7, all_129_8, % 46.10/6.97 | all_129_9 gives: % 46.10/6.97 | (146) number_number_of_nat(all_129_8) = all_129_7 & power_power_int(s, % 46.10/6.97 | all_129_7) = all_129_6 & bit1(pls) = all_129_9 & bit0(all_129_8) = % 46.10/6.97 | all_129_4 & bit0(all_129_9) = all_129_8 & % 46.10/6.97 | number_number_of_int(all_129_4) = all_129_3 & % 46.10/6.97 | plus_plus_int(all_129_2, one_one_int) = all_129_1 & % 46.10/6.97 | plus_plus_int(all_129_6, one_one_int) = all_129_5 & % 46.10/6.97 | times_times_int(all_129_1, all_129_0) = all_129_5 & % 46.10/6.97 | times_times_int(all_129_3, m) = all_129_2 & $i(all_129_0) & % 46.10/6.97 | $i(all_129_1) & $i(all_129_2) & $i(all_129_3) & $i(all_129_4) & % 46.10/6.97 | $i(all_129_5) & $i(all_129_6) & $i(all_129_7) & $i(all_129_8) & % 46.10/6.97 | $i(all_129_9) % 46.10/6.97 | % 46.10/6.97 | ALPHA: (146) implies: % 46.10/6.97 | (147) times_times_int(all_129_3, m) = all_129_2 % 46.10/6.97 | (148) plus_plus_int(all_129_6, one_one_int) = all_129_5 % 46.10/6.97 | (149) plus_plus_int(all_129_2, one_one_int) = all_129_1 % 46.10/6.97 | (150) number_number_of_int(all_129_4) = all_129_3 % 46.10/6.97 | (151) bit0(all_129_9) = all_129_8 % 46.10/6.97 | (152) bit0(all_129_8) = all_129_4 % 46.10/6.97 | (153) bit1(pls) = all_129_9 % 46.10/6.97 | (154) power_power_int(s, all_129_7) = all_129_6 % 46.10/6.97 | (155) number_number_of_nat(all_129_8) = all_129_7 % 46.10/6.97 | % 46.10/6.97 | DELTA: instantiating (6) with fresh symbols all_131_0, all_131_1, all_131_2 % 46.10/6.97 | gives: % 46.10/6.97 | (156) number_number_of_nat(all_131_1) = all_131_0 & bit1(pls) = all_131_2 & % 46.10/6.97 | bit0(all_131_2) = all_131_1 & $i(all_131_0) & $i(all_131_1) & % 46.10/6.97 | $i(all_131_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 46.10/6.97 | : (v1 = zero_zero_int | ~ (power_power_int(v1, all_131_0) = v3) | ~ % 46.10/6.97 | (power_power_int(v0, all_131_0) = v2) | ~ (plus_plus_int(v2, v3) = % 46.10/6.97 | zero_zero_int) | ~ $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: % 46.10/6.97 | $i] : ! [v2: $i] : ! [v3: $i] : (v0 = zero_zero_int | ~ % 46.10/6.97 | (power_power_int(v1, all_131_0) = v3) | ~ (power_power_int(v0, % 46.10/6.97 | all_131_0) = v2) | ~ (plus_plus_int(v2, v3) = zero_zero_int) | % 46.10/6.97 | ~ $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : (v1 = % 46.10/6.97 | zero_zero_int | ~ (power_power_int(zero_zero_int, all_131_0) = v0) % 46.10/6.97 | | ~ (plus_plus_int(v0, v0) = v1)) % 46.10/6.97 | % 46.10/6.97 | ALPHA: (156) implies: % 46.10/6.97 | (157) bit0(all_131_2) = all_131_1 % 46.10/6.97 | (158) bit1(pls) = all_131_2 % 46.10/6.97 | (159) number_number_of_nat(all_131_1) = all_131_0 % 46.10/6.97 | % 46.10/6.97 | DELTA: instantiating (5) with fresh symbols all_134_0, all_134_1, all_134_2 % 46.10/6.97 | gives: % 46.10/6.97 | (160) number_number_of_nat(all_134_1) = all_134_0 & bit1(pls) = all_134_2 & % 46.10/6.97 | bit0(all_134_2) = all_134_1 & $i(all_134_0) & $i(all_134_1) & % 46.10/6.97 | $i(all_134_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 46.10/6.97 | : ! [v4: $i] : (v1 = zero_zero_int | ~ (power_power_int(v1, % 46.10/6.97 | all_134_0) = v3) | ~ (power_power_int(v0, all_134_0) = v2) | % 46.10/6.97 | ~ (plus_plus_int(v2, v3) = v4) | ~ $i(v1) | ~ $i(v0) | % 46.10/6.97 | ord_less_int(zero_zero_int, v4)) & ! [v0: $i] : ! [v1: $i] : ! % 46.10/6.97 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v0 = zero_zero_int | ~ % 46.10/6.97 | (power_power_int(v1, all_134_0) = v3) | ~ (power_power_int(v0, % 46.10/6.97 | all_134_0) = v2) | ~ (plus_plus_int(v2, v3) = v4) | ~ $i(v1) % 46.10/6.97 | | ~ $i(v0) | ord_less_int(zero_zero_int, v4)) & ! [v0: $i] : ! % 46.10/6.97 | [v1: $i] : ( ~ (power_power_int(zero_zero_int, all_134_0) = v0) | ~ % 46.10/6.97 | (plus_plus_int(v0, v0) = v1) | ~ ord_less_int(zero_zero_int, v1)) % 46.10/6.97 | % 46.10/6.97 | ALPHA: (160) implies: % 46.10/6.97 | (161) bit0(all_134_2) = all_134_1 % 46.10/6.97 | (162) bit1(pls) = all_134_2 % 46.10/6.97 | (163) number_number_of_nat(all_134_1) = all_134_0 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_82_1, all_84_2, pls, simplifying with % 46.10/6.97 | (48), (52) gives: % 46.10/6.97 | (164) all_84_2 = all_82_1 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_84_2, all_88_2, pls, simplifying with % 46.10/6.97 | (52), (61) gives: % 46.10/6.97 | (165) all_88_2 = all_84_2 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_88_2, all_96_2, pls, simplifying with % 46.10/6.97 | (61), (69) gives: % 46.10/6.97 | (166) all_96_2 = all_88_2 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_96_2, all_99_0, pls, simplifying with % 46.10/6.97 | (69), (72) gives: % 46.10/6.97 | (167) all_99_0 = all_96_2 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_102_0, all_105_4, pls, simplifying % 46.10/6.97 | with (74), (79) gives: % 46.10/6.97 | (168) all_105_4 = all_102_0 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_93_0, all_105_4, pls, simplifying % 46.10/6.97 | with (66), (79) gives: % 46.10/6.97 | (169) all_105_4 = all_93_0 % 46.10/6.97 | % 46.10/6.97 | GROUND_INST: instantiating (33) with all_99_0, all_108_2, pls, simplifying % 46.10/6.97 | with (72), (84) gives: % 46.43/6.97 | (170) all_108_2 = all_99_0 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_102_0, all_111_2, pls, simplifying % 46.43/6.98 | with (74), (88) gives: % 46.43/6.98 | (171) all_111_2 = all_102_0 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_82_1, all_114_2, pls, simplifying % 46.43/6.98 | with (48), (92) gives: % 46.43/6.98 | (172) all_114_2 = all_82_1 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_80_2, all_114_2, pls, simplifying % 46.43/6.98 | with (44), (92) gives: % 46.43/6.98 | (173) all_114_2 = all_80_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_111_2, all_117_5, pls, simplifying % 46.43/6.98 | with (88), (101) gives: % 46.43/6.98 | (174) all_117_5 = all_111_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_114_2, all_119_5, pls, simplifying % 46.43/6.98 | with (92), (110) gives: % 46.43/6.98 | (175) all_119_5 = all_114_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_76_0, all_119_5, pls, simplifying % 46.43/6.98 | with (41), (110) gives: % 46.43/6.98 | (176) all_119_5 = all_76_0 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_105_4, all_123_6, pls, simplifying % 46.43/6.98 | with (79), (124) gives: % 46.43/6.98 | (177) all_123_6 = all_105_4 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_88_2, all_123_6, pls, simplifying % 46.43/6.98 | with (61), (124) gives: % 46.43/6.98 | (178) all_123_6 = all_88_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_125_7, all_127_8, pls, simplifying % 46.43/6.98 | with (134), (143) gives: % 46.43/6.98 | (179) all_127_8 = all_125_7 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_121_5, all_127_8, pls, simplifying % 46.43/6.98 | with (117), (143) gives: % 46.43/6.98 | (180) all_127_8 = all_121_5 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_117_5, all_127_8, pls, simplifying % 46.43/6.98 | with (101), (143) gives: % 46.43/6.98 | (181) all_127_8 = all_117_5 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_123_6, all_129_9, pls, simplifying % 46.43/6.98 | with (124), (153) gives: % 46.43/6.98 | (182) all_129_9 = all_123_6 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_90_0, all_129_9, pls, simplifying % 46.43/6.98 | with (64), (153) gives: % 46.43/6.98 | (183) all_129_9 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_108_2, all_131_2, pls, simplifying % 46.43/6.98 | with (84), (158) gives: % 46.43/6.98 | (184) all_131_2 = all_108_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_86_2, all_131_2, pls, simplifying % 46.43/6.98 | with (56), (158) gives: % 46.43/6.98 | (185) all_131_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_125_7, all_134_2, pls, simplifying % 46.43/6.98 | with (134), (162) gives: % 46.43/6.98 | (186) all_134_2 = all_125_7 % 46.43/6.98 | % 46.43/6.98 | GROUND_INST: instantiating (33) with all_74_0, all_134_2, pls, simplifying % 46.43/6.98 | with (39), (162) gives: % 46.43/6.98 | (187) all_134_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (186), (187) imply: % 46.43/6.98 | (188) all_125_7 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (188) implies: % 46.43/6.98 | (189) all_125_7 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (184), (185) imply: % 46.43/6.98 | (190) all_108_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | SIMP: (190) implies: % 46.43/6.98 | (191) all_108_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (182), (183) imply: % 46.43/6.98 | (192) all_123_6 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (192) implies: % 46.43/6.98 | (193) all_123_6 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (180), (181) imply: % 46.43/6.98 | (194) all_121_5 = all_117_5 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (179), (180) imply: % 46.43/6.98 | (195) all_125_7 = all_121_5 % 46.43/6.98 | % 46.43/6.98 | SIMP: (195) implies: % 46.43/6.98 | (196) all_125_7 = all_121_5 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (189), (196) imply: % 46.43/6.98 | (197) all_121_5 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (197) implies: % 46.43/6.98 | (198) all_121_5 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (177), (193) imply: % 46.43/6.98 | (199) all_105_4 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (199) implies: % 46.43/6.98 | (200) all_105_4 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (178), (193) imply: % 46.43/6.98 | (201) all_90_0 = all_88_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (194), (198) imply: % 46.43/6.98 | (202) all_117_5 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (202) implies: % 46.43/6.98 | (203) all_117_5 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (175), (176) imply: % 46.43/6.98 | (204) all_114_2 = all_76_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (204) implies: % 46.43/6.98 | (205) all_114_2 = all_76_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (174), (203) imply: % 46.43/6.98 | (206) all_111_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (206) implies: % 46.43/6.98 | (207) all_111_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (172), (173) imply: % 46.43/6.98 | (208) all_82_1 = all_80_2 % 46.43/6.98 | % 46.43/6.98 | SIMP: (208) implies: % 46.43/6.98 | (209) all_82_1 = all_80_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (173), (205) imply: % 46.43/6.98 | (210) all_80_2 = all_76_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (171), (207) imply: % 46.43/6.98 | (211) all_102_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (211) implies: % 46.43/6.98 | (212) all_102_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (170), (191) imply: % 46.43/6.98 | (213) all_99_0 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | SIMP: (213) implies: % 46.43/6.98 | (214) all_99_0 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (168), (169) imply: % 46.43/6.98 | (215) all_102_0 = all_93_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (215) implies: % 46.43/6.98 | (216) all_102_0 = all_93_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (169), (200) imply: % 46.43/6.98 | (217) all_93_0 = all_90_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (212), (216) imply: % 46.43/6.98 | (218) all_93_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (218) implies: % 46.43/6.98 | (219) all_93_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (167), (214) imply: % 46.43/6.98 | (220) all_96_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | SIMP: (220) implies: % 46.43/6.98 | (221) all_96_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (166), (221) imply: % 46.43/6.98 | (222) all_88_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | SIMP: (222) implies: % 46.43/6.98 | (223) all_88_2 = all_86_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (217), (219) imply: % 46.43/6.98 | (224) all_90_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (224) implies: % 46.43/6.98 | (225) all_90_0 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (201), (225) imply: % 46.43/6.98 | (226) all_88_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (226) implies: % 46.43/6.98 | (227) all_88_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (165), (223) imply: % 46.43/6.98 | (228) all_86_2 = all_84_2 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (223), (227) imply: % 46.43/6.98 | (229) all_86_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (228), (229) imply: % 46.43/6.98 | (230) all_84_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | SIMP: (230) implies: % 46.43/6.98 | (231) all_84_2 = all_74_0 % 46.43/6.98 | % 46.43/6.98 | COMBINE_EQS: (164), (231) imply: % 46.43/6.99 | (232) all_82_1 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | SIMP: (232) implies: % 46.43/6.99 | (233) all_82_1 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (209), (233) imply: % 46.43/6.99 | (234) all_80_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | SIMP: (234) implies: % 46.43/6.99 | (235) all_80_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (210), (235) imply: % 46.43/6.99 | (236) all_76_0 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | SIMP: (236) implies: % 46.43/6.99 | (237) all_76_0 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (221), (229) imply: % 46.43/6.99 | (238) all_96_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (169), (219) imply: % 46.43/6.99 | (239) all_105_4 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (191), (229) imply: % 46.43/6.99 | (240) all_108_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (173), (235) imply: % 46.43/6.99 | (241) all_114_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (176), (237) imply: % 46.43/6.99 | (242) all_119_5 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (193), (225) imply: % 46.43/6.99 | (243) all_123_6 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (180), (198) imply: % 46.43/6.99 | (244) all_127_8 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (183), (225) imply: % 46.43/6.99 | (245) all_129_9 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (185), (229) imply: % 46.43/6.99 | (246) all_131_2 = all_74_0 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (161), (187) imply: % 46.43/6.99 | (247) bit0(all_74_0) = all_134_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (157), (246) imply: % 46.43/6.99 | (248) bit0(all_74_0) = all_131_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (151), (245) imply: % 46.43/6.99 | (249) bit0(all_74_0) = all_129_8 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (141), (244) imply: % 46.43/6.99 | (250) bit0(all_74_0) = all_127_7 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (132), (189) imply: % 46.43/6.99 | (251) bit0(all_74_0) = all_125_6 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (122), (243) imply: % 46.43/6.99 | (252) bit0(all_74_0) = all_123_5 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (115), (198) imply: % 46.43/6.99 | (253) bit0(all_74_0) = all_121_4 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (108), (242) imply: % 46.43/6.99 | (254) bit0(all_74_0) = all_119_4 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (99), (203) imply: % 46.43/6.99 | (255) bit0(all_74_0) = all_117_4 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (91), (241) imply: % 46.43/6.99 | (256) bit0(all_74_0) = all_114_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (87), (207) imply: % 46.43/6.99 | (257) bit0(all_74_0) = all_111_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (83), (240) imply: % 46.43/6.99 | (258) bit0(all_74_0) = all_108_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (78), (239) imply: % 46.43/6.99 | (259) bit0(all_74_0) = all_105_3 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (68), (238) imply: % 46.43/6.99 | (260) bit0(all_74_0) = all_96_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (60), (227) imply: % 46.43/6.99 | (261) bit0(all_74_0) = all_88_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (55), (229) imply: % 46.43/6.99 | (262) bit0(all_74_0) = all_86_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (51), (231) imply: % 46.43/6.99 | (263) bit0(all_74_0) = all_84_1 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (47), (233) imply: % 46.43/6.99 | (264) bit0(all_74_0) = all_82_0 % 46.43/6.99 | % 46.43/6.99 | REDUCE: (43), (235) imply: % 46.43/6.99 | (265) bit0(all_74_0) = all_80_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_96_1, all_111_1, all_74_0, % 46.43/6.99 | simplifying with (257), (260) gives: % 46.43/6.99 | (266) all_111_1 = all_96_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_88_1, all_111_1, all_74_0, % 46.43/6.99 | simplifying with (257), (261) gives: % 46.43/6.99 | (267) all_111_1 = all_88_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_114_1, all_117_4, all_74_0, % 46.43/6.99 | simplifying with (255), (256) gives: % 46.43/6.99 | (268) all_117_4 = all_114_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_117_4, all_119_4, all_74_0, % 46.43/6.99 | simplifying with (254), (255) gives: % 46.43/6.99 | (269) all_119_4 = all_117_4 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_111_1, all_121_4, all_74_0, % 46.43/6.99 | simplifying with (253), (257) gives: % 46.43/6.99 | (270) all_121_4 = all_111_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_117_4, all_123_5, all_74_0, % 46.43/6.99 | simplifying with (252), (255) gives: % 46.43/6.99 | (271) all_123_5 = all_117_4 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_108_1, all_123_5, all_74_0, % 46.43/6.99 | simplifying with (252), (258) gives: % 46.43/6.99 | (272) all_123_5 = all_108_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_96_1, all_123_5, all_74_0, % 46.43/6.99 | simplifying with (252), (260) gives: % 46.43/6.99 | (273) all_123_5 = all_96_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_119_4, all_125_6, all_74_0, % 46.43/6.99 | simplifying with (251), (254) gives: % 46.43/6.99 | (274) all_125_6 = all_119_4 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_111_1, all_127_7, all_74_0, % 46.43/6.99 | simplifying with (250), (257) gives: % 46.43/6.99 | (275) all_127_7 = all_111_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_86_1, all_127_7, all_74_0, % 46.43/6.99 | simplifying with (250), (262) gives: % 46.43/6.99 | (276) all_127_7 = all_86_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_84_1, all_127_7, all_74_0, % 46.43/6.99 | simplifying with (250), (263) gives: % 46.43/6.99 | (277) all_127_7 = all_84_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_121_4, all_129_8, all_74_0, % 46.43/6.99 | simplifying with (249), (253) gives: % 46.43/6.99 | (278) all_129_8 = all_121_4 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_105_3, all_129_8, all_74_0, % 46.43/6.99 | simplifying with (249), (259) gives: % 46.43/6.99 | (279) all_129_8 = all_105_3 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_84_1, all_131_1, all_74_0, % 46.43/6.99 | simplifying with (248), (263) gives: % 46.43/6.99 | (280) all_131_1 = all_84_1 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_82_0, all_131_1, all_74_0, % 46.43/6.99 | simplifying with (248), (264) gives: % 46.43/6.99 | (281) all_131_1 = all_82_0 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_125_6, all_134_1, all_74_0, % 46.43/6.99 | simplifying with (247), (251) gives: % 46.43/6.99 | (282) all_134_1 = all_125_6 % 46.43/6.99 | % 46.43/6.99 | GROUND_INST: instantiating (32) with all_80_1, all_134_1, all_74_0, % 46.43/6.99 | simplifying with (247), (265) gives: % 46.43/6.99 | (283) all_134_1 = all_80_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (282), (283) imply: % 46.43/6.99 | (284) all_125_6 = all_80_1 % 46.43/6.99 | % 46.43/6.99 | SIMP: (284) implies: % 46.43/6.99 | (285) all_125_6 = all_80_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (280), (281) imply: % 46.43/6.99 | (286) all_84_1 = all_82_0 % 46.43/6.99 | % 46.43/6.99 | SIMP: (286) implies: % 46.43/6.99 | (287) all_84_1 = all_82_0 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (278), (279) imply: % 46.43/6.99 | (288) all_121_4 = all_105_3 % 46.43/6.99 | % 46.43/6.99 | SIMP: (288) implies: % 46.43/6.99 | (289) all_121_4 = all_105_3 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (276), (277) imply: % 46.43/6.99 | (290) all_86_1 = all_84_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (275), (276) imply: % 46.43/6.99 | (291) all_111_1 = all_86_1 % 46.43/6.99 | % 46.43/6.99 | SIMP: (291) implies: % 46.43/6.99 | (292) all_111_1 = all_86_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (274), (285) imply: % 46.43/6.99 | (293) all_119_4 = all_80_1 % 46.43/6.99 | % 46.43/6.99 | SIMP: (293) implies: % 46.43/6.99 | (294) all_119_4 = all_80_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (272), (273) imply: % 46.43/6.99 | (295) all_108_1 = all_96_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (271), (272) imply: % 46.43/6.99 | (296) all_117_4 = all_108_1 % 46.43/6.99 | % 46.43/6.99 | SIMP: (296) implies: % 46.43/6.99 | (297) all_117_4 = all_108_1 % 46.43/6.99 | % 46.43/6.99 | COMBINE_EQS: (270), (289) imply: % 46.43/7.00 | (298) all_111_1 = all_105_3 % 46.43/7.00 | % 46.43/7.00 | SIMP: (298) implies: % 46.43/7.00 | (299) all_111_1 = all_105_3 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (269), (294) imply: % 46.43/7.00 | (300) all_117_4 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (300) implies: % 46.43/7.00 | (301) all_117_4 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (268), (297) imply: % 46.43/7.00 | (302) all_114_1 = all_108_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (268), (301) imply: % 46.43/7.00 | (303) all_114_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (302), (303) imply: % 46.43/7.00 | (304) all_108_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (304) implies: % 46.43/7.00 | (305) all_108_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (267), (299) imply: % 46.43/7.00 | (306) all_105_3 = all_88_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (266), (299) imply: % 46.43/7.00 | (307) all_105_3 = all_96_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (292), (299) imply: % 46.43/7.00 | (308) all_105_3 = all_86_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (295), (305) imply: % 46.43/7.00 | (309) all_96_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (309) implies: % 46.43/7.00 | (310) all_96_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (306), (307) imply: % 46.43/7.00 | (311) all_96_1 = all_88_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (311) implies: % 46.43/7.00 | (312) all_96_1 = all_88_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (306), (308) imply: % 46.43/7.00 | (313) all_88_1 = all_86_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (310), (312) imply: % 46.43/7.00 | (314) all_88_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (314) implies: % 46.43/7.00 | (315) all_88_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (313), (315) imply: % 46.43/7.00 | (316) all_86_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (316) implies: % 46.43/7.00 | (317) all_86_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (290), (317) imply: % 46.43/7.00 | (318) all_84_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (318) implies: % 46.43/7.00 | (319) all_84_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (287), (319) imply: % 46.43/7.00 | (320) all_82_0 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | SIMP: (320) implies: % 46.43/7.00 | (321) all_82_0 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (306), (315) imply: % 46.43/7.00 | (322) all_105_3 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (299), (322) imply: % 46.43/7.00 | (323) all_111_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (289), (322) imply: % 46.43/7.00 | (324) all_121_4 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (272), (305) imply: % 46.43/7.00 | (325) all_123_5 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (276), (317) imply: % 46.43/7.00 | (326) all_127_7 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (279), (322) imply: % 46.43/7.00 | (327) all_129_8 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (281), (321) imply: % 46.43/7.00 | (328) all_131_1 = all_80_1 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (163), (283) imply: % 46.43/7.00 | (329) number_number_of_nat(all_80_1) = all_134_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (159), (328) imply: % 46.43/7.00 | (330) number_number_of_nat(all_80_1) = all_131_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (155), (327) imply: % 46.43/7.00 | (331) number_number_of_nat(all_80_1) = all_129_7 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (145), (326) imply: % 46.43/7.00 | (332) number_number_of_nat(all_80_1) = all_127_6 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (93), (303) imply: % 46.43/7.00 | (333) number_number_of_nat(all_80_1) = all_114_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (89), (323) imply: % 46.43/7.00 | (334) number_number_of_nat(all_80_1) = all_111_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (85), (305) imply: % 46.43/7.00 | (335) number_number_of_nat(all_80_1) = all_108_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (81), (322) imply: % 46.43/7.00 | (336) number_number_of_nat(all_80_1) = all_105_2 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (70), (310) imply: % 46.43/7.00 | (337) number_number_of_nat(all_80_1) = all_96_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (62), (315) imply: % 46.43/7.00 | (338) number_number_of_nat(all_80_1) = all_88_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (58), (317) imply: % 46.43/7.00 | (339) number_number_of_nat(all_80_1) = all_86_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (53), (319) imply: % 46.43/7.00 | (340) number_number_of_nat(all_80_1) = all_84_0 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (49), (321) imply: % 46.43/7.00 | (341) number_number_of_nat(all_80_1) = all_82_2 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (152), (327) imply: % 46.43/7.00 | (342) bit0(all_80_1) = all_129_4 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (142), (326) imply: % 46.43/7.00 | (343) bit0(all_80_1) = all_127_3 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (133), (285) imply: % 46.43/7.00 | (344) bit0(all_80_1) = all_125_5 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (123), (325) imply: % 46.43/7.00 | (345) bit0(all_80_1) = all_123_4 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (116), (324) imply: % 46.43/7.00 | (346) bit0(all_80_1) = all_121_3 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (109), (294) imply: % 46.43/7.00 | (347) bit0(all_80_1) = all_119_3 % 46.43/7.00 | % 46.43/7.00 | REDUCE: (100), (301) imply: % 46.43/7.00 | (348) bit0(all_80_1) = all_117_3 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_121_3, all_123_4, all_80_1, % 46.43/7.00 | simplifying with (345), (346) gives: % 46.43/7.00 | (349) all_123_4 = all_121_3 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_125_5, all_127_3, all_80_1, % 46.43/7.00 | simplifying with (343), (344) gives: % 46.43/7.00 | (350) all_127_3 = all_125_5 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_121_3, all_127_3, all_80_1, % 46.43/7.00 | simplifying with (343), (346) gives: % 46.43/7.00 | (351) all_127_3 = all_121_3 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_117_3, all_127_3, all_80_1, % 46.43/7.00 | simplifying with (343), (348) gives: % 46.43/7.00 | (352) all_127_3 = all_117_3 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_123_4, all_129_4, all_80_1, % 46.43/7.00 | simplifying with (342), (345) gives: % 46.43/7.00 | (353) all_129_4 = all_123_4 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (32) with all_119_3, all_129_4, all_80_1, % 46.43/7.00 | simplifying with (342), (347) gives: % 46.43/7.00 | (354) all_129_4 = all_119_3 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_80_0, all_84_0, all_80_1, simplifying % 46.43/7.00 | with (45), (340) gives: % 46.43/7.00 | (355) all_84_0 = all_80_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_84_0, all_86_0, all_80_1, simplifying % 46.43/7.00 | with (339), (340) gives: % 46.43/7.00 | (356) all_86_0 = all_84_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_105_2, all_108_0, all_80_1, % 46.43/7.00 | simplifying with (335), (336) gives: % 46.43/7.00 | (357) all_108_0 = all_105_2 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_96_0, all_108_0, all_80_1, % 46.43/7.00 | simplifying with (335), (337) gives: % 46.43/7.00 | (358) all_108_0 = all_96_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_96_0, all_114_0, all_80_1, % 46.43/7.00 | simplifying with (333), (337) gives: % 46.43/7.00 | (359) all_114_0 = all_96_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_88_0, all_114_0, all_80_1, % 46.43/7.00 | simplifying with (333), (338) gives: % 46.43/7.00 | (360) all_114_0 = all_88_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_86_0, all_114_0, all_80_1, % 46.43/7.00 | simplifying with (333), (339) gives: % 46.43/7.00 | (361) all_114_0 = all_86_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_114_0, all_127_6, all_80_1, % 46.43/7.00 | simplifying with (332), (333) gives: % 46.43/7.00 | (362) all_127_6 = all_114_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_111_0, all_127_6, all_80_1, % 46.43/7.00 | simplifying with (332), (334) gives: % 46.43/7.00 | (363) all_127_6 = all_111_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_108_0, all_129_7, all_80_1, % 46.43/7.00 | simplifying with (331), (335) gives: % 46.43/7.00 | (364) all_129_7 = all_108_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_129_7, all_131_0, all_80_1, % 46.43/7.00 | simplifying with (330), (331) gives: % 46.43/7.00 | (365) all_131_0 = all_129_7 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_131_0, all_134_0, all_80_1, % 46.43/7.00 | simplifying with (329), (330) gives: % 46.43/7.00 | (366) all_134_0 = all_131_0 % 46.43/7.00 | % 46.43/7.00 | GROUND_INST: instantiating (34) with all_82_2, all_134_0, all_80_1, % 46.43/7.00 | simplifying with (329), (341) gives: % 46.43/7.00 | (367) all_134_0 = all_82_2 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (366), (367) imply: % 46.43/7.00 | (368) all_131_0 = all_82_2 % 46.43/7.00 | % 46.43/7.00 | SIMP: (368) implies: % 46.43/7.00 | (369) all_131_0 = all_82_2 % 46.43/7.00 | % 46.43/7.00 | COMBINE_EQS: (365), (369) imply: % 46.43/7.00 | (370) all_129_7 = all_82_2 % 46.43/7.00 | % 46.43/7.00 | SIMP: (370) implies: % 46.43/7.00 | (371) all_129_7 = all_82_2 % 46.43/7.00 | % 46.43/7.01 | COMBINE_EQS: (353), (354) imply: % 46.43/7.01 | (372) all_123_4 = all_119_3 % 46.43/7.01 | % 46.43/7.01 | SIMP: (372) implies: % 46.43/7.01 | (373) all_123_4 = all_119_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (364), (371) imply: % 46.43/7.01 | (374) all_108_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (374) implies: % 46.43/7.01 | (375) all_108_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (350), (351) imply: % 46.43/7.01 | (376) all_125_5 = all_121_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (350), (352) imply: % 46.43/7.01 | (377) all_125_5 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (362), (363) imply: % 46.43/7.01 | (378) all_114_0 = all_111_0 % 46.43/7.01 | % 46.43/7.01 | SIMP: (378) implies: % 46.43/7.01 | (379) all_114_0 = all_111_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (376), (377) imply: % 46.43/7.01 | (380) all_121_3 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | SIMP: (380) implies: % 46.43/7.01 | (381) all_121_3 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (349), (373) imply: % 46.43/7.01 | (382) all_121_3 = all_119_3 % 46.43/7.01 | % 46.43/7.01 | SIMP: (382) implies: % 46.43/7.01 | (383) all_121_3 = all_119_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (381), (383) imply: % 46.43/7.01 | (384) all_119_3 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | SIMP: (384) implies: % 46.43/7.01 | (385) all_119_3 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (360), (379) imply: % 46.43/7.01 | (386) all_111_0 = all_88_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (361), (379) imply: % 46.43/7.01 | (387) all_111_0 = all_86_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (359), (379) imply: % 46.43/7.01 | (388) all_111_0 = all_96_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (386), (388) imply: % 46.43/7.01 | (389) all_96_0 = all_88_0 % 46.43/7.01 | % 46.43/7.01 | SIMP: (389) implies: % 46.43/7.01 | (390) all_96_0 = all_88_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (386), (387) imply: % 46.43/7.01 | (391) all_88_0 = all_86_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (357), (358) imply: % 46.43/7.01 | (392) all_105_2 = all_96_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (357), (375) imply: % 46.43/7.01 | (393) all_105_2 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (392), (393) imply: % 46.43/7.01 | (394) all_96_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (394) implies: % 46.43/7.01 | (395) all_96_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (390), (395) imply: % 46.43/7.01 | (396) all_88_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (396) implies: % 46.43/7.01 | (397) all_88_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (391), (397) imply: % 46.43/7.01 | (398) all_86_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (398) implies: % 46.43/7.01 | (399) all_86_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (356), (399) imply: % 46.43/7.01 | (400) all_84_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (400) implies: % 46.43/7.01 | (401) all_84_0 = all_82_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (355), (401) imply: % 46.43/7.01 | (402) all_82_2 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (399), (402) imply: % 46.43/7.01 | (403) all_86_0 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (397), (402) imply: % 46.43/7.01 | (404) all_88_0 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (393), (402) imply: % 46.43/7.01 | (405) all_105_2 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (386), (404) imply: % 46.43/7.01 | (406) all_111_0 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (379), (406) imply: % 46.43/7.01 | (407) all_114_0 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (373), (385) imply: % 46.43/7.01 | (408) all_123_4 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (363), (406) imply: % 46.43/7.01 | (409) all_127_6 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (371), (402) imply: % 46.43/7.01 | (410) all_129_7 = all_80_0 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (354), (385) imply: % 46.43/7.01 | (411) all_129_4 = all_117_3 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (154), (410) imply: % 46.43/7.01 | (412) power_power_int(s, all_80_0) = all_129_6 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (144), (409) imply: % 46.43/7.01 | (413) power_power_int(s, all_80_0) = all_127_5 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (80), (405) imply: % 46.43/7.01 | (414) power_power_int(s, all_80_0) = all_105_1 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (57), (403) imply: % 46.43/7.01 | (415) power_power_int(zero_zero_int, all_80_0) = zero_zero_int % 46.43/7.01 | % 46.43/7.01 | REDUCE: (150), (411) imply: % 46.43/7.01 | (416) number_number_of_int(all_117_3) = all_129_3 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (140), (352) imply: % 46.43/7.01 | (417) number_number_of_int(all_117_3) = all_127_2 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (131), (377) imply: % 46.43/7.01 | (418) number_number_of_int(all_117_3) = all_125_4 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (121), (408) imply: % 46.43/7.01 | (419) number_number_of_int(all_117_3) = all_123_3 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (114), (381) imply: % 46.43/7.01 | (420) number_number_of_int(all_117_3) = all_121_2 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (107), (385) imply: % 46.43/7.01 | (421) number_number_of_int(all_117_3) = all_119_2 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_119_2, all_125_4, all_117_3, % 46.43/7.01 | simplifying with (418), (421) gives: % 46.43/7.01 | (422) all_125_4 = all_119_2 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_125_4, all_127_2, all_117_3, % 46.43/7.01 | simplifying with (417), (418) gives: % 46.43/7.01 | (423) all_127_2 = all_125_4 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_123_3, all_127_2, all_117_3, % 46.43/7.01 | simplifying with (417), (419) gives: % 46.43/7.01 | (424) all_127_2 = all_123_3 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_117_2, all_129_3, all_117_3, % 46.43/7.01 | simplifying with (98), (416) gives: % 46.43/7.01 | (425) all_129_3 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_125_4, all_129_3, all_117_3, % 46.43/7.01 | simplifying with (416), (418) gives: % 46.43/7.01 | (426) all_129_3 = all_125_4 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (31) with all_121_2, all_129_3, all_117_3, % 46.43/7.01 | simplifying with (416), (420) gives: % 46.43/7.01 | (427) all_129_3 = all_121_2 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (37) with all_127_5, all_129_6, all_80_0, s, % 46.43/7.01 | simplifying with (412), (413) gives: % 46.43/7.01 | (428) all_129_6 = all_127_5 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (37) with all_105_1, all_129_6, all_80_0, s, % 46.43/7.01 | simplifying with (412), (414) gives: % 46.43/7.01 | (429) all_129_6 = all_105_1 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (426), (427) imply: % 46.43/7.01 | (430) all_125_4 = all_121_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (430) implies: % 46.43/7.01 | (431) all_125_4 = all_121_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (425), (427) imply: % 46.43/7.01 | (432) all_121_2 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (428), (429) imply: % 46.43/7.01 | (433) all_127_5 = all_105_1 % 46.43/7.01 | % 46.43/7.01 | SIMP: (433) implies: % 46.43/7.01 | (434) all_127_5 = all_105_1 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (423), (424) imply: % 46.43/7.01 | (435) all_125_4 = all_123_3 % 46.43/7.01 | % 46.43/7.01 | SIMP: (435) implies: % 46.43/7.01 | (436) all_125_4 = all_123_3 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (422), (436) imply: % 46.43/7.01 | (437) all_123_3 = all_119_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (431), (436) imply: % 46.43/7.01 | (438) all_123_3 = all_121_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (437), (438) imply: % 46.43/7.01 | (439) all_121_2 = all_119_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (439) implies: % 46.43/7.01 | (440) all_121_2 = all_119_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (432), (440) imply: % 46.43/7.01 | (441) all_119_2 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | SIMP: (441) implies: % 46.43/7.01 | (442) all_119_2 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (437), (442) imply: % 46.43/7.01 | (443) all_123_3 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (436), (443) imply: % 46.43/7.01 | (444) all_125_4 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | COMBINE_EQS: (424), (443) imply: % 46.43/7.01 | (445) all_127_2 = all_117_2 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (148), (429) imply: % 46.43/7.01 | (446) plus_plus_int(all_105_1, one_one_int) = all_129_5 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (138), (434) imply: % 46.43/7.01 | (447) plus_plus_int(all_105_1, one_one_int) = all_127_4 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (147), (425) imply: % 46.43/7.01 | (448) times_times_int(all_117_2, m) = all_129_2 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (136), (445) imply: % 46.43/7.01 | (449) times_times_int(all_117_2, m) = all_127_1 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (127), (444) imply: % 46.43/7.01 | (450) times_times_int(all_117_2, m) = all_125_3 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (119), (443) imply: % 46.43/7.01 | (451) times_times_int(all_117_2, m) = all_123_2 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (112), (432) imply: % 46.43/7.01 | (452) times_times_int(all_117_2, m) = all_121_1 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (105), (442) imply: % 46.43/7.01 | (453) times_times_int(all_117_2, m) = all_119_1 % 46.43/7.01 | % 46.43/7.01 | REDUCE: (103), (442) imply: % 46.43/7.01 | (454) $i(all_117_2) % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_117_1, all_125_3, m, all_117_2, % 46.43/7.01 | simplifying with (96), (450) gives: % 46.43/7.01 | (455) all_125_3 = all_117_1 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_119_1, all_125_3, m, all_117_2, % 46.43/7.01 | simplifying with (450), (453) gives: % 46.43/7.01 | (456) all_125_3 = all_119_1 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_125_3, all_127_1, m, all_117_2, % 46.43/7.01 | simplifying with (449), (450) gives: % 46.43/7.01 | (457) all_127_1 = all_125_3 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_123_2, all_127_1, m, all_117_2, % 46.43/7.01 | simplifying with (449), (451) gives: % 46.43/7.01 | (458) all_127_1 = all_123_2 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_125_3, all_129_2, m, all_117_2, % 46.43/7.01 | simplifying with (448), (450) gives: % 46.43/7.01 | (459) all_129_2 = all_125_3 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (35) with all_121_1, all_129_2, m, all_117_2, % 46.43/7.01 | simplifying with (448), (452) gives: % 46.43/7.01 | (460) all_129_2 = all_121_1 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (36) with all_105_0, all_129_5, one_one_int, % 46.43/7.01 | all_105_1, simplifying with (77), (446) gives: % 46.43/7.01 | (461) all_129_5 = all_105_0 % 46.43/7.01 | % 46.43/7.01 | GROUND_INST: instantiating (36) with all_127_4, all_129_5, one_one_int, % 46.43/7.01 | all_105_1, simplifying with (446), (447) gives: % 46.43/7.01 | (462) all_129_5 = all_127_4 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (459), (460) imply: % 46.43/7.02 | (463) all_125_3 = all_121_1 % 46.43/7.02 | % 46.43/7.02 | SIMP: (463) implies: % 46.43/7.02 | (464) all_125_3 = all_121_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (461), (462) imply: % 46.43/7.02 | (465) all_127_4 = all_105_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (457), (458) imply: % 46.43/7.02 | (466) all_125_3 = all_123_2 % 46.43/7.02 | % 46.43/7.02 | SIMP: (466) implies: % 46.43/7.02 | (467) all_125_3 = all_123_2 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (455), (467) imply: % 46.43/7.02 | (468) all_123_2 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (456), (467) imply: % 46.43/7.02 | (469) all_123_2 = all_119_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (464), (467) imply: % 46.43/7.02 | (470) all_123_2 = all_121_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (469), (470) imply: % 46.43/7.02 | (471) all_121_1 = all_119_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (468), (470) imply: % 46.43/7.02 | (472) all_121_1 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (471), (472) imply: % 46.43/7.02 | (473) all_119_1 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | SIMP: (473) implies: % 46.43/7.02 | (474) all_119_1 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (458), (468) imply: % 46.43/7.02 | (475) all_127_1 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (460), (472) imply: % 46.43/7.02 | (476) all_129_2 = all_117_1 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (149), (476) imply: % 46.43/7.02 | (477) plus_plus_int(all_117_1, one_one_int) = all_129_1 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (139), (475) imply: % 46.43/7.02 | (478) plus_plus_int(all_117_1, one_one_int) = all_127_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (130), (455) imply: % 46.43/7.02 | (479) plus_plus_int(all_117_1, one_one_int) = all_125_2 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (120), (468) imply: % 46.43/7.02 | (480) plus_plus_int(all_117_1, one_one_int) = all_123_1 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (113), (472) imply: % 46.43/7.02 | (481) plus_plus_int(all_117_1, one_one_int) = all_121_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (106), (474) imply: % 46.43/7.02 | (482) plus_plus_int(all_117_1, one_one_int) = all_119_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (137), (465) imply: % 46.43/7.02 | (483) times_times_int(all_127_0, t) = all_105_0 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_117_0, all_125_2, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (97), (479) gives: % 46.43/7.02 | (484) all_125_2 = all_117_0 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_125_2, all_127_0, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (478), (479) gives: % 46.43/7.02 | (485) all_127_0 = all_125_2 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_123_1, all_127_0, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (478), (480) gives: % 46.43/7.02 | (486) all_127_0 = all_123_1 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_121_0, all_127_0, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (478), (481) gives: % 46.43/7.02 | (487) all_127_0 = all_121_0 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_123_1, all_129_1, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (477), (480) gives: % 46.43/7.02 | (488) all_129_1 = all_123_1 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (36) with all_119_0, all_129_1, one_one_int, % 46.43/7.02 | all_117_1, simplifying with (477), (482) gives: % 46.43/7.02 | (489) all_129_1 = all_119_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (488), (489) imply: % 46.43/7.02 | (490) all_123_1 = all_119_0 % 46.43/7.02 | % 46.43/7.02 | SIMP: (490) implies: % 46.43/7.02 | (491) all_123_1 = all_119_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (486), (487) imply: % 46.43/7.02 | (492) all_123_1 = all_121_0 % 46.43/7.02 | % 46.43/7.02 | SIMP: (492) implies: % 46.43/7.02 | (493) all_123_1 = all_121_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (485), (487) imply: % 46.43/7.02 | (494) all_125_2 = all_121_0 % 46.43/7.02 | % 46.43/7.02 | SIMP: (494) implies: % 46.43/7.02 | (495) all_125_2 = all_121_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (484), (495) imply: % 46.43/7.02 | (496) all_121_0 = all_117_0 % 46.43/7.02 | % 46.43/7.02 | SIMP: (496) implies: % 46.43/7.02 | (497) all_121_0 = all_117_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (491), (493) imply: % 46.43/7.02 | (498) all_121_0 = all_119_0 % 46.43/7.02 | % 46.43/7.02 | SIMP: (498) implies: % 46.43/7.02 | (499) all_121_0 = all_119_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (497), (499) imply: % 46.43/7.02 | (500) all_119_0 = all_117_0 % 46.43/7.02 | % 46.43/7.02 | COMBINE_EQS: (487), (497) imply: % 46.43/7.02 | (501) all_127_0 = all_117_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (483), (501) imply: % 46.43/7.02 | (502) times_times_int(all_117_0, t) = all_105_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (129), (484) imply: % 46.43/7.02 | (503) times_times_int(all_117_0, zero_zero_int) = all_125_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (128), (484) imply: % 46.43/7.02 | (504) times_times_int(all_117_0, t) = all_125_1 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (104), (500) imply: % 46.43/7.02 | (505) $i(all_117_0) % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (35) with all_105_0, all_125_1, t, all_117_0, % 46.43/7.02 | simplifying with (502), (504) gives: % 46.43/7.02 | (506) all_125_1 = all_105_0 % 46.43/7.02 | % 46.43/7.02 | REDUCE: (126), (506) imply: % 46.43/7.02 | (507) ord_less_int(all_105_0, all_125_0) % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (fact_25_zmult__commute) with all_117_2, m, % 46.43/7.02 | all_117_1, simplifying with (19), (96), (454) gives: % 46.43/7.02 | (508) times_times_int(m, all_117_2) = all_117_1 & $i(all_117_1) % 46.43/7.02 | % 46.43/7.02 | ALPHA: (508) implies: % 46.43/7.02 | (509) $i(all_117_1) % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (fact_25_zmult__commute) with all_117_0, % 46.43/7.02 | zero_zero_int, all_125_0, simplifying with (27), (503), (505) % 46.43/7.02 | gives: % 46.43/7.02 | (510) times_times_int(zero_zero_int, all_117_0) = all_125_0 & $i(all_125_0) % 46.43/7.02 | % 46.43/7.02 | ALPHA: (510) implies: % 46.43/7.02 | (511) times_times_int(zero_zero_int, all_117_0) = all_125_0 % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (fact_104_zadd__commute) with all_117_1, % 46.43/7.02 | one_one_int, all_117_0, simplifying with (28), (97), (509) gives: % 46.43/7.02 | (512) plus_plus_int(one_one_int, all_117_1) = all_117_0 & $i(all_117_0) % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (fact_24_number__of__is__id) with pls, % 46.43/7.02 | zero_zero_int, simplifying with (26), (29) gives: % 46.43/7.02 | (513) pls = zero_zero_int % 46.43/7.02 | % 46.43/7.02 | GROUND_INST: instantiating (94) with zero_zero_int gives: % 46.43/7.02 | (514) ~ (power_power_int(zero_zero_int, all_114_0) = zero_zero_int) | ~ % 46.43/7.02 | ord_less_int(zero_zero_int, zero_zero_int) % 46.43/7.02 | % 46.43/7.02 | BETA: splitting (514) gives: % 46.43/7.02 | % 46.43/7.02 | Case 1: % 46.43/7.02 | | % 46.43/7.02 | | (515) ~ (power_power_int(zero_zero_int, all_114_0) = zero_zero_int) % 46.43/7.02 | | % 46.43/7.02 | | REDUCE: (407), (515) imply: % 46.43/7.02 | | (516) ~ (power_power_int(zero_zero_int, all_80_0) = zero_zero_int) % 46.43/7.02 | | % 46.43/7.02 | | PRED_UNIFY: (415), (516) imply: % 46.43/7.02 | | (517) $false % 46.43/7.02 | | % 46.43/7.02 | | CLOSE: (517) is inconsistent. % 46.43/7.02 | | % 46.43/7.02 | Case 2: % 46.43/7.02 | | % 46.43/7.02 | | % 46.43/7.02 | | GROUND_INST: instantiating (24) with all_117_0, all_125_0, simplifying with % 46.43/7.02 | | (505) gives: % 46.43/7.02 | | (518) all_125_0 = pls | ~ (times_times_int(pls, all_117_0) = all_125_0) % 46.43/7.02 | | % 46.43/7.02 | | BETA: splitting (518) gives: % 46.43/7.02 | | % 46.43/7.02 | | Case 1: % 46.43/7.02 | | | % 46.43/7.02 | | | (519) ~ (times_times_int(pls, all_117_0) = all_125_0) % 46.43/7.02 | | | % 46.43/7.02 | | | REDUCE: (513), (519) imply: % 46.43/7.02 | | | (520) ~ (times_times_int(zero_zero_int, all_117_0) = all_125_0) % 46.43/7.02 | | | % 46.43/7.02 | | | PRED_UNIFY: (511), (520) imply: % 46.43/7.02 | | | (521) $false % 46.43/7.02 | | | % 46.43/7.02 | | | CLOSE: (521) is inconsistent. % 46.43/7.02 | | | % 46.43/7.02 | | Case 2: % 46.43/7.02 | | | % 46.43/7.02 | | | (522) all_125_0 = pls % 46.43/7.02 | | | % 46.43/7.02 | | | COMBINE_EQS: (513), (522) imply: % 46.43/7.02 | | | (523) all_125_0 = zero_zero_int % 46.43/7.02 | | | % 46.43/7.02 | | | REDUCE: (507), (523) imply: % 46.43/7.02 | | | (524) ord_less_int(all_105_0, zero_zero_int) % 46.43/7.02 | | | % 46.43/7.02 | | | PRED_UNIFY: (76), (524) imply: % 46.43/7.02 | | | (525) $false % 46.43/7.02 | | | % 46.43/7.02 | | | CLOSE: (525) is inconsistent. % 46.43/7.02 | | | % 46.43/7.02 | | End of split % 46.43/7.02 | | % 46.43/7.02 | End of split % 46.43/7.02 | % 46.43/7.02 End of proof % 46.43/7.02 % SZS output end Proof for theBenchmark % 46.43/7.02 % 46.43/7.02 6387ms %------------------------------------------------------------------------------