%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM924+5 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n015.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:49 EDT 2023 % Result : Theorem 31.35s 5.20s % Output : Proof 61.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : NUM924+5 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.10 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n015.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Fri Aug 25 14:08:07 EDT 2023 % 0.10/0.31 % CPUTime : % 0.16/0.60 ________ _____ % 0.16/0.60 ___ __ \_________(_)________________________________ % 0.16/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.60 % 0.16/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.60 (2023-06-19) % 0.16/0.60 % 0.16/0.60 (c) Philipp Rümmer, 2009-2023 % 0.16/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.60 Amanda Stjerna. % 0.16/0.60 Free software under BSD-3-Clause. % 0.16/0.60 % 0.16/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.60 % 0.16/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.62 Running up to 7 provers in parallel. % 0.16/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.16/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 5.61/1.63 Prover 1: Preprocessing ... % 5.61/1.63 Prover 4: Preprocessing ... % 6.21/1.67 Prover 3: Preprocessing ... % 6.21/1.67 Prover 5: Preprocessing ... % 6.21/1.67 Prover 2: Preprocessing ... % 6.21/1.67 Prover 0: Preprocessing ... % 6.21/1.67 Prover 6: Preprocessing ... % 22.32/3.86 Prover 3: Constructing countermodel ... % 22.41/3.87 Prover 1: Constructing countermodel ... % 22.41/3.90 Prover 6: Proving ... % 23.98/4.13 Prover 5: Proving ... % 24.47/4.34 Prover 2: Proving ... % 26.48/4.50 Prover 0: Proving ... % 26.48/4.51 Prover 4: Constructing countermodel ... % 31.35/5.19 Prover 3: proved (4556ms) % 31.35/5.19 % 31.35/5.20 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.35/5.20 % 31.35/5.20 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 31.35/5.20 Prover 6: stopped % 31.35/5.20 Prover 5: stopped % 31.35/5.21 Prover 0: stopped % 32.24/5.23 Prover 2: stopped % 32.24/5.24 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 32.24/5.24 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 32.24/5.24 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 32.24/5.25 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.86/5.57 Prover 8: Preprocessing ... % 34.86/5.58 Prover 7: Preprocessing ... % 35.47/5.65 Prover 11: Preprocessing ... % 35.72/5.69 Prover 10: Preprocessing ... % 35.72/5.76 Prover 13: Preprocessing ... % 38.90/6.14 Prover 7: Warning: ignoring some quantifiers % 38.90/6.14 Prover 8: Warning: ignoring some quantifiers % 39.37/6.19 Prover 8: Constructing countermodel ... % 39.37/6.19 Prover 7: Constructing countermodel ... % 40.71/6.35 Prover 10: Warning: ignoring some quantifiers % 40.71/6.40 Prover 10: Constructing countermodel ... % 42.35/6.59 Prover 13: Warning: ignoring some quantifiers % 42.35/6.66 Prover 13: Constructing countermodel ... % 44.84/6.97 Prover 11: Constructing countermodel ... % 55.39/8.35 Prover 1: Found proof (size 623) % 55.39/8.35 Prover 1: proved (7720ms) % 55.39/8.35 Prover 13: stopped % 55.39/8.35 Prover 7: stopped % 55.39/8.35 Prover 8: stopped % 55.39/8.35 Prover 4: stopped % 55.39/8.36 Prover 11: stopped % 55.39/8.41 Prover 10: Found proof (size 542) % 55.39/8.41 Prover 10: proved (3195ms) % 55.39/8.41 % 55.39/8.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.39/8.41 % 59.53/9.25 % SZS output start Proof for theBenchmark % 59.53/9.26 Assumptions after simplification: % 59.53/9.26 --------------------------------- % 59.53/9.26 % 59.53/9.26 (arity_Nat_Onat___Int_Onumber) % 59.53/9.31 number(nat) = 0 & $i(nat) % 59.53/9.31 % 59.53/9.31 (arity_Nat_Onat___Int_Onumber__semiring) % 59.53/9.31 number_semiring(nat) = 0 & $i(nat) % 59.53/9.31 % 59.53/9.31 (arity_Nat_Onat___Orderings_Olinorder) % 59.53/9.31 linorder(nat) = 0 & $i(nat) % 59.53/9.31 % 59.53/9.31 (conj_0) % 59.92/9.31 $i(s) & $i(nat) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] % 59.92/9.31 : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ( ~ % 59.92/9.31 (v7 = 0) & power_power(int, s, v2) = v3 & ord_less(int, v5, v6) = v7 & % 59.92/9.31 number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & % 59.92/9.31 zero_zero(int) = v6 & plus_plus(int, v3, v4) = v5 & one_one(int) = v4 & % 59.92/9.31 $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 59.92/9.31 % 59.92/9.31 (fact_0__096t_A_060_A0_096) % 59.92/9.32 $i(t) & $i(int) & ? [v0: $i] : (ord_less(int, t, v0) = 0 & zero_zero(int) = % 59.92/9.32 v0 & $i(v0)) % 59.92/9.32 % 59.92/9.32 (fact_10_power2__less__0) % 59.92/9.32 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.32 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.32 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | % 59.92/9.32 ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( % 59.92/9.32 ~ (power_power(v3, v5, v2) = v6) | ~ (ord_less(v3, v6, v4) = 0) | ~ % 59.92/9.32 $i(v5))))) % 59.92/9.32 % 59.92/9.32 (fact_11_zero__less__power2) % 59.92/9.32 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.32 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.32 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | % 59.92/9.32 ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! % 59.92/9.32 [v7: int] : (v7 = 0 | ~ (power_power(v3, v5, v2) = v6) | ~ % 59.92/9.32 (ord_less(v3, v4, v6) = v7) | ~ $i(v5) | ti(v3, v5) = v4) & ! [v5: % 59.92/9.32 $i] : ! [v6: $i] : ( ~ (power_power(v3, v5, v2) = v6) | ~ % 59.92/9.32 (ord_less(v3, v4, v6) = 0) | ~ $i(v5) | ? [v7: $i] : ( ~ (v7 = v4) & % 59.92/9.32 ti(v3, v5) = v7 & $i(v7)))))) % 59.92/9.32 % 59.92/9.32 (fact_12_one__power2) % 59.92/9.32 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.33 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.33 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ % 59.92/9.33 (power_power(v3, v4, v2) = v5) | ~ (one_one(v3) = v4) | ~ $i(v3) | ? % 59.92/9.33 [v6: int] : ( ~ (v6 = 0) & semiring_1(v3) = v6))) % 59.92/9.33 % 59.92/9.33 (fact_13_zero__power2) % 59.92/9.33 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.33 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.33 $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ % 59.92/9.33 (power_power(v3, v4, v2) = v5) | ~ (zero_zero(v3) = v4) | ~ $i(v3) | ? % 59.92/9.33 [v6: int] : ( ~ (v6 = 0) & semiring_1(v3) = v6))) % 59.92/9.33 % 59.92/9.33 (fact_14_zero__eq__power2) % 59.92/9.33 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.33 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.33 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (ring_11004092258visors(v3) = 0) | ~ % 59.92/9.33 $i(v3) | ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! % 59.92/9.33 [v6: $i] : (v6 = v4 | ~ (power_power(v3, v5, v2) = v6) | ~ $i(v5) | ? % 59.92/9.33 [v7: $i] : ( ~ (v7 = v4) & ti(v3, v5) = v7 & $i(v7))) & ! [v5: $i] : % 59.92/9.33 ( ~ (power_power(v3, v5, v2) = v4) | ~ $i(v5) | ti(v3, v5) = v4)))) % 59.92/9.33 % 59.92/9.33 (fact_15_add__special_I2_J) % 59.92/9.33 $i(pls) & $i(int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 59.92/9.33 (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: $i] : (one_one(v1) = v2 & % 59.92/9.33 $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 59.92/9.33 (number_number_of(v1, v4) = v5) | ~ (plus_plus(int, v0, v3) = v4) | % 59.92/9.33 ~ $i(v3) | ? [v6: $i] : (number_number_of(v1, v3) = v6 & % 59.92/9.33 plus_plus(v1, v2, v6) = v5 & $i(v6) & $i(v5)))))) % 59.92/9.33 % 59.92/9.33 (fact_16_add__special_I3_J) % 59.92/9.33 $i(pls) & $i(int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 59.92/9.33 (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: $i] : (one_one(v1) = v2 & % 59.92/9.33 $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 59.92/9.33 (number_number_of(v1, v4) = v5) | ~ (plus_plus(int, v3, v0) = v4) | % 59.92/9.33 ~ $i(v3) | ? [v6: $i] : (number_number_of(v1, v3) = v6 & % 59.92/9.33 plus_plus(v1, v6, v2) = v5 & $i(v6) & $i(v5)))))) % 59.92/9.33 % 59.92/9.33 (fact_17_t__l__p) % 59.92/9.33 $i(t) & $i(m) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.33 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (ord_less(int, t, v6) = % 59.92/9.33 0 & number_number_of(int, v2) = v3 & bit1(pls) = v0 & bit0(v1) = v2 & % 59.92/9.33 bit0(v0) = v1 & times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & % 59.92/9.33 one_one(int) = v5 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 59.92/9.33 $i(v0)) % 59.92/9.33 % 59.92/9.33 (fact_18__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_) % 59.92/9.34 $i(s) & $i(m) & $i(nat) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? % 59.92/9.34 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 59.92/9.34 : ? [v8: $i] : ? [v9: $i] : (power_power(int, s, v2) = v3 & % 59.92/9.34 number_number_of(nat, v1) = v2 & number_number_of(int, v6) = v7 & bit1(pls) % 59.92/9.34 = v0 & bit0(v1) = v6 & bit0(v0) = v1 & times_times(int, v7, m) = v8 & % 59.92/9.34 plus_plus(int, v8, v4) = v9 & plus_plus(int, v3, v4) = v5 & one_one(int) = % 59.92/9.34 v4 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 59.92/9.34 $i(v1) & $i(v0) & ? [v10: $i] : (times_times(int, v9, v10) = v5 & $i(v10))) % 59.92/9.34 % 59.92/9.34 (fact_19_p) % 59.92/9.34 $i(m) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 59.92/9.34 $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (number_number_of(int, v2) = % 59.92/9.34 v3 & bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & zprime(v6) = 0 & % 59.92/9.34 times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & one_one(int) = % 59.92/9.34 v5 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 59.92/9.34 % 59.92/9.34 (fact_1_calculation_I1_J) % 59.92/9.34 $i(t) & $i(int) & ? [v0: $i] : (ord_less(int, t, v0) = 0 & one_one(int) = v0 % 59.92/9.34 & $i(v0)) % 59.92/9.34 % 59.92/9.34 (fact_20_qf1pt) % 59.92/9.34 $i(t) & $i(m) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.34 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 59.92/9.34 (twoSqu33214720sum2sq(v7) = 0 & number_number_of(int, v2) = v3 & bit1(pls) = % 59.92/9.34 v0 & bit0(v1) = v2 & bit0(v0) = v1 & times_times(int, v6, t) = v7 & % 59.92/9.34 times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & one_one(int) = % 59.92/9.34 v5 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 59.92/9.34 % 59.92/9.34 (fact_22_number__of__is__id) % 59.92/9.34 $i(int) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (number_number_of(int, v0) % 59.92/9.34 = v1) | ~ $i(v0)) % 59.92/9.34 % 59.92/9.34 (fact_23_zmult__commute) % 59.92/9.35 $i(int) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (times_times(int, v0, % 59.92/9.35 v1) = v2) | ~ $i(v1) | ~ $i(v0) | (times_times(int, v1, v0) = v2 & % 59.92/9.35 $i(v2))) % 59.92/9.35 % 59.92/9.35 (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) % 59.92/9.35 $i(t) & $i(m) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.35 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: % 59.92/9.35 $i] : ? [v9: $i] : (ord_less(int, v7, v9) = 0 & number_number_of(int, v2) = % 59.92/9.35 v3 & bit1(pls) = v0 & bit0(v1) = v2 & bit0(v0) = v1 & zero_zero(int) = v8 & % 59.92/9.35 times_times(int, v6, v8) = v9 & times_times(int, v6, t) = v7 & % 59.92/9.35 times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & one_one(int) = % 59.92/9.35 v5 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 59.92/9.35 $i(v1) & $i(v0)) % 59.92/9.35 % 59.92/9.35 (fact_34_rel__simps_I19_J) % 59.92/9.35 ord_less_eq(int, pls, pls) = 0 & $i(pls) & $i(int) % 59.92/9.35 % 59.92/9.35 (fact_3_t) % 59.92/9.35 $i(t) & $i(s) & $i(m) & $i(nat) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: % 59.92/9.35 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 59.92/9.35 ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : (power_power(int, s, v2) = v3 & % 59.92/9.35 number_number_of(nat, v1) = v2 & number_number_of(int, v6) = v7 & bit1(pls) % 59.92/9.35 = v0 & bit0(v1) = v6 & bit0(v0) = v1 & times_times(int, v9, t) = v5 & % 59.92/9.35 times_times(int, v7, m) = v8 & plus_plus(int, v8, v4) = v9 & plus_plus(int, % 59.92/9.35 v3, v4) = v5 & one_one(int) = v4 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 59.92/9.35 $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 59.92/9.35 % 59.92/9.35 (fact_4_calculation_I2_J) % 59.92/9.36 $i(t) & $i(s) & $i(nat) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? % 59.92/9.36 [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 59.92/9.36 (power_power(int, s, v3) = v4 & number_number_of(nat, v2) = v3 & bit1(pls) = % 59.92/9.36 v1 & bit0(v1) = v2 & zero_zero(int) = v0 & plus_plus(int, v4, v5) = v6 & % 59.92/9.36 one_one(int) = v5 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 59.92/9.36 $i(v0) & ( ~ (v0 = t) | v6 = t)) % 59.92/9.36 % 59.92/9.36 (fact_50_le__number__of__eq__not__less) % 59.92/9.36 ! [v0: $i] : ( ~ (linorder(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) % 59.92/9.36 & number(v0) = v1) | ( ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 59.92/9.36 $i] : ! [v5: int] : (v5 = 0 | ~ (ord_less(v0, v3, v4) = v5) | ~ % 59.92/9.36 (number_number_of(v0, v2) = v3) | ~ (number_number_of(v0, v1) = v4) | % 59.92/9.36 ~ $i(v2) | ~ $i(v1) | ord_less_eq(v0, v4, v3) = 0) & ! [v1: $i] : ! % 59.92/9.36 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (ord_less(v0, v4, v3) = 0) | ~ % 59.92/9.36 (number_number_of(v0, v2) = v4) | ~ (number_number_of(v0, v1) = v3) | % 59.92/9.36 ~ $i(v2) | ~ $i(v1) | ? [v5: int] : ( ~ (v5 = 0) & ord_less_eq(v0, v3, % 59.92/9.36 v4) = v5)))) % 59.92/9.36 % 59.92/9.36 (fact_51_rel__simps_I22_J) % 59.92/9.36 $i(pls) & $i(int) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ % 59.92/9.36 (ord_less_eq(int, pls, v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: int] : % 59.92/9.36 ( ~ (v3 = 0) & ord_less_eq(int, pls, v2) = v3 & bit1(v0) = v2 & $i(v2))) & % 59.92/9.36 ! [v0: $i] : ( ~ (ord_less_eq(int, pls, v0) = 0) | ~ $i(v0) | ? [v1: $i] : % 59.92/9.36 (ord_less_eq(int, pls, v1) = 0 & bit1(v0) = v1 & $i(v1))) % 59.92/9.36 % 59.92/9.36 (fact_59_le__special_I4_J) % 59.92/9.37 $i(pls) & $i(int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 59.92/9.37 (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: any] : ? [v3: $i] : % 59.92/9.37 (linordered_idom(v1) = v2 & one_one(v1) = v3 & $i(v3) & ( ~ (v2 = 0) | ( ! % 59.92/9.37 [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (ord_less_eq(int, v4, v0) = % 59.92/9.37 v5) | ~ $i(v4) | ? [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & % 59.92/9.37 ord_less_eq(v1, v6, v3) = v7 & number_number_of(v1, v4) = v6 & % 59.92/9.37 $i(v6))) & ! [v4: $i] : ( ~ (ord_less_eq(int, v4, v0) = 0) | ~ % 59.92/9.37 $i(v4) | ? [v5: $i] : (ord_less_eq(v1, v5, v3) = 0 & % 59.92/9.37 number_number_of(v1, v4) = v5 & $i(v5)))))))) % 59.92/9.37 % 59.92/9.37 (fact_5__096_126_A1_A_060_061_At_096) % 59.92/9.37 $i(t) & $i(int) & ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & ord_less_eq(int, % 59.92/9.37 v0, t) = v1 & one_one(int) = v0 & $i(v0)) % 59.92/9.37 % 59.92/9.37 (fact_60_le__special_I2_J) % 59.92/9.37 $i(pls) & $i(int) & ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 59.92/9.37 (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: any] : ? [v3: $i] : % 59.92/9.37 (linordered_idom(v1) = v2 & one_one(v1) = v3 & $i(v3) & ( ~ (v2 = 0) | ( ! % 59.92/9.37 [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (ord_less_eq(int, v0, v4) = % 59.92/9.37 v5) | ~ $i(v4) | ? [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & % 59.92/9.37 ord_less_eq(v1, v3, v6) = v7 & number_number_of(v1, v4) = v6 & % 59.92/9.37 $i(v6))) & ! [v4: $i] : ( ~ (ord_less_eq(int, v0, v4) = 0) | ~ % 59.92/9.37 $i(v4) | ? [v5: $i] : (ord_less_eq(v1, v3, v5) = 0 & % 59.92/9.37 number_number_of(v1, v4) = v5 & $i(v5)))))))) % 59.92/9.37 % 59.92/9.37 (fact_61_nat__1__add__1) % 59.92/9.37 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 59.92/9.37 (number_number_of(nat, v3) = v1 & bit1(pls) = v2 & bit0(v2) = v3 & % 59.92/9.37 plus_plus(nat, v0, v0) = v1 & one_one(nat) = v0 & $i(v3) & $i(v2) & $i(v1) & % 59.92/9.37 $i(v0)) % 59.92/9.37 % 59.92/9.37 (fact_62_mult__Pls) % 59.92/9.37 $i(pls) & $i(int) & ! [v0: $i] : ! [v1: $i] : (v1 = pls | ~ % 59.92/9.37 (times_times(int, pls, v0) = v1) | ~ $i(v0)) % 59.92/9.37 % 59.92/9.37 (fact_65_zmult__1__right) % 59.92/9.37 $i(int) & ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 59.92/9.37 $i] : (v2 = v1 | ~ (times_times(int, v1, v0) = v2) | ~ $i(v1))) % 59.92/9.37 % 59.92/9.37 (fact_66_zmult__1) % 59.92/9.37 $i(int) & ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 59.92/9.37 $i] : (v2 = v1 | ~ (times_times(int, v0, v1) = v2) | ~ $i(v1))) % 59.92/9.37 % 59.92/9.37 (fact_6_p0) % 59.92/9.38 $i(m) & $i(pls) & $i(int) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 59.92/9.38 $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (ord_less(int, % 59.92/9.38 v0, v7) = 0 & number_number_of(int, v3) = v4 & bit1(pls) = v1 & bit0(v2) = % 59.92/9.38 v3 & bit0(v1) = v2 & zero_zero(int) = v0 & times_times(int, v4, m) = v5 & % 59.92/9.38 plus_plus(int, v5, v6) = v7 & one_one(int) = v6 & $i(v7) & $i(v6) & $i(v5) & % 59.92/9.38 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 59.92/9.38 % 59.92/9.38 (fact_77_int__one__le__iff__zero__less) % 59.92/9.38 $i(int) & ? [v0: $i] : ? [v1: $i] : (zero_zero(int) = v1 & one_one(int) = v0 % 59.92/9.38 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (ord_less(int, % 59.92/9.38 v1, v2) = v3) | ~ $i(v2) | ? [v4: int] : ( ~ (v4 = 0) & % 59.92/9.38 ord_less_eq(int, v0, v2) = v4)) & ! [v2: $i] : ( ~ (ord_less(int, v1, % 59.92/9.38 v2) = 0) | ~ $i(v2) | ord_less_eq(int, v0, v2) = 0)) % 59.92/9.38 % 59.92/9.38 (fact_78_nat__numeral__1__eq__1) % 59.92/9.38 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : (number_number_of(nat, v0) = % 59.92/9.38 v1 & bit1(pls) = v0 & one_one(nat) = v1 & $i(v1) & $i(v0)) % 59.92/9.38 % 59.92/9.38 (fact_79_Numeral1__eq1__nat) % 59.92/9.38 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : (number_number_of(nat, v1) = % 59.92/9.38 v0 & bit1(pls) = v1 & one_one(nat) = v0 & $i(v1) & $i(v0)) % 59.92/9.38 % 59.92/9.38 (fact_7_not__sum__power2__lt__zero) % 59.92/9.38 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 59.92/9.38 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 59.92/9.38 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | % 59.92/9.38 ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! % 59.92/9.38 [v7: $i] : ! [v8: $i] : ! [v9: $i] : ( ~ (power_power(v3, v6, v2) = % 59.92/9.38 v8) | ~ (power_power(v3, v5, v2) = v7) | ~ (ord_less(v3, v9, v4) = % 59.92/9.38 0) | ~ (plus_plus(v3, v7, v8) = v9) | ~ $i(v6) | ~ $i(v5))))) % 59.92/9.38 % 59.92/9.38 (fact_80_zless__imp__add1__zle) % 59.92/9.38 $i(int) & ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 59.92/9.38 $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less_eq(int, v3, v2) % 59.92/9.38 = v4) | ~ (plus_plus(int, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ? % 59.92/9.38 [v5: int] : ( ~ (v5 = 0) & ord_less(int, v1, v2) = v5))) % 59.92/9.38 % 59.92/9.38 (fact_81_add1__zle__eq) % 59.92/9.38 $i(int) & ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 59.92/9.38 $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less_eq(int, v3, v2) % 59.92/9.38 = v4) | ~ (plus_plus(int, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ? % 59.92/9.38 [v5: int] : ( ~ (v5 = 0) & ord_less(int, v1, v2) = v5)) & ! [v1: $i] : ! % 59.92/9.38 [v2: $i] : ! [v3: $i] : ( ~ (ord_less_eq(int, v3, v2) = 0) | ~ % 59.92/9.38 (plus_plus(int, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ord_less(int, v1, % 59.92/9.38 v2) = 0)) % 59.92/9.38 % 59.92/9.38 (fact_82_zle__add1__eq__le) % 59.92/9.39 $i(int) & ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 59.92/9.39 $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less(int, v1, v3) = % 59.92/9.39 v4) | ~ (plus_plus(int, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ? [v5: % 59.92/9.39 int] : ( ~ (v5 = 0) & ord_less_eq(int, v1, v2) = v5)) & ! [v1: $i] : ! % 59.92/9.39 [v2: $i] : ! [v3: $i] : ( ~ (ord_less(int, v1, v3) = 0) | ~ % 59.92/9.39 (plus_plus(int, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ord_less_eq(int, % 59.92/9.39 v1, v2) = 0)) % 59.92/9.39 % 59.92/9.39 (fact_83_semiring__add__number__of) % 59.92/9.39 $i(pls) & $i(int) & ! [v0: $i] : ( ~ (number_semiring(v0) = 0) | ~ $i(v0) | % 59.92/9.39 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 59.92/9.39 (number_number_of(v0, v2) = v3) | ~ (number_number_of(v0, v1) = v4) | ~ % 59.92/9.39 (plus_plus(v0, v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ? [v6: any] : ? % 59.92/9.39 [v7: any] : ? [v8: $i] : ? [v9: $i] : (ord_less_eq(int, pls, v2) = v6 & % 59.92/9.39 ord_less_eq(int, pls, v1) = v7 & number_number_of(v0, v8) = v9 & % 59.92/9.39 plus_plus(int, v2, v1) = v8 & $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = % 59.92/9.39 0) | v9 = v5)))) % 59.92/9.39 % 59.92/9.39 (fact_85_le__imp__0__less) % 59.92/9.39 $i(int) & ? [v0: $i] : ? [v1: $i] : (zero_zero(int) = v0 & one_one(int) = v1 % 59.92/9.39 & $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ (plus_plus(int, v1, v2) % 59.92/9.39 = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : (ord_less_eq(int, v0, % 59.92/9.39 v2) = v4 & ord_less(int, v0, v3) = v5 & ( ~ (v4 = 0) | v5 = 0)))) % 59.92/9.39 % 59.92/9.39 (fact_8_sum__power2__gt__zero__iff) % 60.32/9.39 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 60.32/9.39 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 60.32/9.39 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | % 60.32/9.39 ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! % 60.32/9.39 [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: int] : (v10 = 0 | ~ % 60.32/9.39 (power_power(v3, v6, v2) = v8) | ~ (power_power(v3, v5, v2) = v7) | % 60.32/9.39 ~ (ord_less(v3, v4, v9) = v10) | ~ (plus_plus(v3, v7, v8) = v9) | ~ % 60.32/9.39 $i(v6) | ~ $i(v5) | (ti(v3, v6) = v4 & ti(v3, v5) = v4)) & ! [v5: % 60.32/9.39 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ( ~ % 60.32/9.39 (power_power(v3, v6, v2) = v8) | ~ (power_power(v3, v5, v2) = v7) | % 60.32/9.39 ~ (ord_less(v3, v4, v9) = 0) | ~ (plus_plus(v3, v7, v8) = v9) | ~ % 60.32/9.40 $i(v6) | ~ $i(v5) | ? [v10: $i] : ? [v11: $i] : (ti(v3, v6) = v11 & % 60.32/9.40 ti(v3, v5) = v10 & $i(v11) & $i(v10) & ( ~ (v11 = v4) | ~ (v10 = % 60.32/9.40 v4))))))) % 60.32/9.40 % 60.32/9.40 (fact_96_zadd__commute) % 60.32/9.40 $i(int) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (plus_plus(int, v0, % 60.32/9.40 v1) = v2) | ~ $i(v1) | ~ $i(v0) | (plus_plus(int, v1, v0) = v2 & % 60.32/9.40 $i(v2))) % 60.32/9.40 % 60.32/9.40 (fact_97_zero__is__num__zero) % 60.32/9.40 $i(pls) & $i(int) & ? [v0: $i] : (number_number_of(int, pls) = v0 & % 60.32/9.40 zero_zero(int) = v0 & $i(v0)) % 60.32/9.40 % 60.32/9.40 (fact_9_sum__power2__eq__zero__iff) % 60.32/9.40 $i(nat) & $i(pls) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 60.32/9.40 (number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & % 60.32/9.40 $i(v1) & $i(v0) & ! [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | % 60.32/9.40 ? [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! % 60.32/9.40 [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v9 = v4 | ~ (power_power(v3, % 60.32/9.40 v6, v2) = v8) | ~ (power_power(v3, v5, v2) = v7) | ~ % 60.32/9.40 (plus_plus(v3, v7, v8) = v9) | ~ $i(v6) | ~ $i(v5) | ? [v10: $i] : % 60.32/9.40 ? [v11: $i] : (ti(v3, v6) = v11 & ti(v3, v5) = v10 & $i(v11) & $i(v10) % 60.32/9.40 & ( ~ (v11 = v4) | ~ (v10 = v4)))) & ! [v5: $i] : ! [v6: $i] : ! % 60.32/9.40 [v7: $i] : ! [v8: $i] : ( ~ (power_power(v3, v6, v2) = v8) | ~ % 60.32/9.40 (power_power(v3, v5, v2) = v7) | ~ (plus_plus(v3, v7, v8) = v4) | ~ % 60.32/9.40 $i(v6) | ~ $i(v5) | (ti(v3, v6) = v4 & ti(v3, v5) = v4))))) % 60.32/9.40 % 60.32/9.40 (tsy_c_Int_OBit1_res) % 60.32/9.40 $i(int) & ! [v0: $i] : ! [v1: $i] : ( ~ (bit1(v0) = v1) | ~ $i(v0) | % 60.32/9.40 (ti(int, v1) = v1 & $i(v1))) % 60.32/9.40 % 60.32/9.40 (function-axioms) % 60.32/9.41 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 60.32/9.41 | ~ (power_power(v4, v3, v2) = v1) | ~ (power_power(v4, v3, v2) = v0)) & % 60.32/9.41 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 60.32/9.41 $i] : ! [v4: $i] : (v1 = v0 | ~ (ord_less_eq(v4, v3, v2) = v1) | ~ % 60.32/9.41 (ord_less_eq(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.32/9.41 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 60.32/9.42 (ord_less(v4, v3, v2) = v1) | ~ (ord_less(v4, v3, v2) = v0)) & ! [v0: $i] % 60.32/9.42 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 60.32/9.42 (times_times(v4, v3, v2) = v1) | ~ (times_times(v4, v3, v2) = v0)) & ! % 60.32/9.42 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 60.32/9.42 ~ (plus_plus(v4, v3, v2) = v1) | ~ (plus_plus(v4, v3, v2) = v0)) & ! [v0: % 60.32/9.42 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 60.32/9.42 (number_number_of(v3, v2) = v1) | ~ (number_number_of(v3, v2) = v0)) & ! % 60.32/9.42 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (ti(v3, v2) % 60.32/9.42 = v1) | ~ (ti(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.32/9.42 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (ring_char_0(v2) = v1) | ~ % 60.32/9.42 (ring_char_0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.32/9.42 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (linord581940658strict(v2) % 60.32/9.42 = v1) | ~ (linord581940658strict(v2) = v0)) & ! [v0: MultipleValueBool] % 60.32/9.42 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ % 60.32/9.42 (number_semiring(v2) = v1) | ~ (number_semiring(v2) = v0)) & ! [v0: % 60.32/9.42 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 60.32/9.42 ~ (number_ring(v2) = v1) | ~ (number_ring(v2) = v0)) & ! [v0: % 60.32/9.42 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 60.32/9.42 ~ (ring_11004092258visors(v2) = v1) | ~ (ring_11004092258visors(v2) = v0)) % 60.32/9.42 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 60.32/9.42 = v0 | ~ (twoSqu33214720sum2sq(v2) = v1) | ~ (twoSqu33214720sum2sq(v2) = % 60.32/9.42 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.32/9.42 $i] : (v1 = v0 | ~ (linordered_idom(v2) = v1) | ~ (linordered_idom(v2) = % 60.32/9.42 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.32/9.42 $i] : (v1 = v0 | ~ (linorder(v2) = v1) | ~ (linorder(v2) = v0)) & ! [v0: % 60.32/9.42 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = v1) | ~ % 60.32/9.42 (bit1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 60.32/9.42 (bit0(v2) = v1) | ~ (bit0(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.32/9.42 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (zprime(v2) = v1) | ~ % 60.32/9.42 (zprime(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 60.32/9.42 (undefined(v2) = v1) | ~ (undefined(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 60.32/9.42 : ! [v2: $i] : (v1 = v0 | ~ (zero_zero(v2) = v1) | ~ (zero_zero(v2) = v0)) % 60.32/9.42 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 % 60.32/9.42 = v0 | ~ (linordered_ring(v2) = v1) | ~ (linordered_ring(v2) = v0)) & ! % 60.32/9.42 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 % 60.32/9.42 | ~ (number(v2) = v1) | ~ (number(v2) = v0)) & ! [v0: MultipleValueBool] % 60.32/9.42 : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (semiring(v2) = v1) % 60.32/9.42 | ~ (semiring(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 60.32/9.42 v0 | ~ (one_one(v2) = v1) | ~ (one_one(v2) = v0)) & ! [v0: % 60.32/9.42 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 60.32/9.42 ~ (semiring_1(v2) = v1) | ~ (semiring_1(v2) = v0)) % 60.32/9.42 % 60.32/9.42 Further assumptions not needed in the proof: % 60.32/9.42 -------------------------------------------- % 60.32/9.42 arity_Int_Oint___Int_Onumber, arity_Int_Oint___Int_Onumber__ring, % 60.32/9.42 arity_Int_Oint___Int_Onumber__semiring, arity_Int_Oint___Int_Oring__char__0, % 60.32/9.42 arity_Int_Oint___Orderings_Olinorder, arity_Int_Oint___Rings_Olinordered__idom, % 60.32/9.42 arity_Int_Oint___Rings_Olinordered__ring, % 60.32/9.42 arity_Int_Oint___Rings_Olinordered__ring__strict, % 60.32/9.42 arity_Int_Oint___Rings_Oring__1__no__zero__divisors, % 60.32/9.42 arity_Int_Oint___Rings_Osemiring, arity_Int_Oint___Rings_Osemiring__1, % 60.32/9.42 arity_Nat_Onat___Rings_Osemiring, arity_Nat_Onat___Rings_Osemiring__1, % 60.32/9.42 fact_21_zle__refl, fact_24_zle__linear, fact_25_times__numeral__code_I5_J, % 60.32/9.42 fact_26_less__eq__number__of__int__code, fact_27_le__number__of, % 60.32/9.42 fact_28_zmult__assoc, fact_29_zle__trans, fact_30_zle__antisym, % 60.32/9.42 fact_31_zpower__zadd__distrib, fact_32_less__eq__int__code_I16_J, % 60.32/9.42 fact_33_rel__simps_I34_J, fact_35_less__eq__int__code_I13_J, % 60.32/9.42 fact_36_rel__simps_I31_J, fact_37_zless__le, fact_38_zadd__left__mono, % 60.32/9.42 fact_39_eq__number__of__0, fact_40_eq__0__number__of, % 60.32/9.42 fact_41_semiring__mult__number__of, fact_42_mult__number__of__left, % 60.32/9.42 fact_43_arith__simps_I32_J, fact_44_number__of__mult, % 60.32/9.42 fact_45_sum__squares__le__zero__iff, fact_46_sum__squares__ge__zero, % 60.32/9.42 fact_47_le__special_I3_J, fact_48_le__special_I1_J, fact_49_less__0__number__of, % 60.32/9.42 fact_52_less__eq__int__code_I14_J, fact_53_rel__simps_I32_J, % 60.32/9.42 fact_54_rel__simps_I27_J, fact_55_rel__simps_I21_J, fact_56_zadd__zless__mono, % 60.32/9.42 fact_57_nat__number__of__Pls, fact_58_semiring__norm_I113_J, fact_63_mult__Bit0, % 60.32/9.42 fact_64_less__number__of__int__code, fact_67_plus__numeral__code_I9_J, % 60.32/9.42 fact_68_zadd__zmult__distrib, fact_69_zadd__zmult__distrib2, % 60.32/9.42 fact_70_rel__simps_I29_J, fact_71_rel__simps_I5_J, % 60.32/9.42 fact_72_less__eq__int__code_I15_J, fact_73_rel__simps_I33_J, % 60.32/9.42 fact_74_less__int__code_I14_J, fact_75_rel__simps_I15_J, % 60.32/9.42 fact_76_less__nat__number__of, fact_84_add__nat__number__of, % 60.32/9.42 fact_86_eq__number__of, fact_87_number__of__reorient, fact_88_rel__simps_I51_J, % 60.32/9.42 fact_89_rel__simps_I48_J, fact_90_zless__linear, % 60.32/9.42 fact_91_sum__squares__eq__zero__iff, fact_92_left__distrib__number__of, % 60.32/9.42 fact_93_right__distrib__number__of, fact_94_zadd__assoc, % 60.32/9.42 fact_95_zadd__left__commute, help_ti_idem, tsy_c_Groups_Oone__class_Oone_res, % 60.32/9.42 tsy_c_Groups_Oplus__class_Oplus_0_arg1, tsy_c_Groups_Oplus__class_Oplus_0_arg2, % 60.32/9.42 tsy_c_Groups_Oplus__class_Oplus_0_res, tsy_c_Groups_Oplus__class_Oplus_1_arg1, % 60.32/9.42 tsy_c_Groups_Oplus__class_Oplus_1_arg2, tsy_c_Groups_Oplus__class_Oplus_1_res, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_0_arg1, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_0_arg2, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_0_res, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_1_arg1, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_1_arg2, % 60.32/9.42 tsy_c_Groups_Otimes__class_Otimes_1_res, tsy_c_Groups_Ozero__class_Ozero_0_res, % 60.32/9.42 tsy_c_Groups_Ozero__class_Ozero_1_res, tsy_c_HOL_Oundefined_res, % 60.32/9.42 tsy_c_IntPrimes_Ozprime_arg1, tsy_c_Int_OBit0_arg1, tsy_c_Int_OBit0_res, % 60.32/9.42 tsy_c_Int_OBit1_arg1, tsy_c_Int_OPls_res, % 60.32/9.42 tsy_c_Int_Onumber__class_Onumber__of_arg1, % 60.32/9.42 tsy_c_Int_Onumber__class_Onumber__of_res, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless_0_arg1, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless_0_arg2, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless_1_arg1, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless_1_arg2, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless__eq_0_arg1, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless__eq_0_arg2, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless__eq_1_arg1, % 60.32/9.42 tsy_c_Orderings_Oord__class_Oless__eq_1_arg2, % 60.32/9.42 tsy_c_Power_Opower__class_Opower_arg1, tsy_c_Power_Opower__class_Opower_arg2, % 60.32/9.42 tsy_c_Power_Opower__class_Opower_res, % 60.32/9.42 tsy_c_TwoSquares__Mirabelle__vsgmegnqdl_Ois__sum2sq_arg1, tsy_v_m_res, % 60.32/9.42 tsy_v_s_____res, tsy_v_t_____res % 60.32/9.42 % 60.32/9.42 Those formulas are unsatisfiable: % 60.32/9.42 --------------------------------- % 60.32/9.42 % 60.32/9.42 Begin of proof % 60.32/9.42 | % 60.32/9.42 | ALPHA: (tsy_c_Int_OBit1_res) implies: % 60.32/9.43 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (bit1(v0) = v1) | ~ $i(v0) | (ti(int, % 60.32/9.43 | v1) = v1 & $i(v1))) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_0__096t_A_060_A0_096) implies: % 60.32/9.43 | (2) ? [v0: $i] : (ord_less(int, t, v0) = 0 & zero_zero(int) = v0 & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_1_calculation_I1_J) implies: % 60.32/9.43 | (3) ? [v0: $i] : (ord_less(int, t, v0) = 0 & one_one(int) = v0 & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | 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) % 60.32/9.43 | implies: % 60.32/9.43 | (4) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.43 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 60.32/9.43 | (ord_less(int, v7, v9) = 0 & number_number_of(int, v2) = v3 & bit1(pls) % 60.32/9.43 | = v0 & bit0(v1) = v2 & bit0(v0) = v1 & zero_zero(int) = v8 & % 60.32/9.43 | times_times(int, v6, v8) = v9 & times_times(int, v6, t) = v7 & % 60.32/9.43 | times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & % 60.32/9.43 | one_one(int) = v5 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 60.32/9.43 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_3_t) implies: % 60.32/9.43 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.43 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 60.32/9.43 | (power_power(int, s, v2) = v3 & number_number_of(nat, v1) = v2 & % 60.32/9.43 | number_number_of(int, v6) = v7 & bit1(pls) = v0 & bit0(v1) = v6 & % 60.32/9.43 | bit0(v0) = v1 & times_times(int, v9, t) = v5 & times_times(int, v7, % 60.32/9.43 | m) = v8 & plus_plus(int, v8, v4) = v9 & plus_plus(int, v3, v4) = v5 % 60.32/9.43 | & one_one(int) = v4 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 60.32/9.43 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_4_calculation_I2_J) implies: % 60.32/9.43 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.43 | ? [v5: $i] : ? [v6: $i] : (power_power(int, s, v3) = v4 & % 60.32/9.43 | number_number_of(nat, v2) = v3 & bit1(pls) = v1 & bit0(v1) = v2 & % 60.32/9.43 | zero_zero(int) = v0 & plus_plus(int, v4, v5) = v6 & one_one(int) = v5 % 60.32/9.43 | & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ % 60.32/9.43 | (v0 = t) | v6 = t)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_5__096_126_A1_A_060_061_At_096) implies: % 60.32/9.43 | (7) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & ord_less_eq(int, v0, t) = % 60.32/9.43 | v1 & one_one(int) = v0 & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_6_p0) implies: % 60.32/9.43 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.43 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (ord_less(int, v0, v7) = 0 & % 60.32/9.43 | number_number_of(int, v3) = v4 & bit1(pls) = v1 & bit0(v2) = v3 & % 60.32/9.43 | bit0(v1) = v2 & zero_zero(int) = v0 & times_times(int, v4, m) = v5 & % 60.32/9.43 | plus_plus(int, v5, v6) = v7 & one_one(int) = v6 & $i(v7) & $i(v6) & % 60.32/9.43 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_7_not__sum__power2__lt__zero) implies: % 60.32/9.43 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.43 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.43 | [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | ? [v4: $i] : % 60.32/9.43 | (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 60.32/9.43 | $i] : ! [v8: $i] : ! [v9: $i] : ( ~ (power_power(v3, v6, v2) % 60.32/9.43 | = v8) | ~ (power_power(v3, v5, v2) = v7) | ~ (ord_less(v3, % 60.32/9.43 | v9, v4) = 0) | ~ (plus_plus(v3, v7, v8) = v9) | ~ $i(v6) % 60.32/9.43 | | ~ $i(v5))))) % 60.32/9.43 | % 60.32/9.43 | ALPHA: (fact_8_sum__power2__gt__zero__iff) implies: % 60.32/9.44 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | ? [v4: $i] : % 60.32/9.44 | (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 60.32/9.44 | $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: int] : (v10 = 0 | % 60.32/9.44 | ~ (power_power(v3, v6, v2) = v8) | ~ (power_power(v3, v5, v2) % 60.32/9.44 | = v7) | ~ (ord_less(v3, v4, v9) = v10) | ~ (plus_plus(v3, % 60.32/9.44 | v7, v8) = v9) | ~ $i(v6) | ~ $i(v5) | (ti(v3, v6) = v4 & % 60.32/9.44 | ti(v3, v5) = v4)) & ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 60.32/9.44 | : ! [v8: $i] : ! [v9: $i] : ( ~ (power_power(v3, v6, v2) = v8) % 60.32/9.44 | | ~ (power_power(v3, v5, v2) = v7) | ~ (ord_less(v3, v4, v9) % 60.32/9.44 | = 0) | ~ (plus_plus(v3, v7, v8) = v9) | ~ $i(v6) | ~ % 60.32/9.44 | $i(v5) | ? [v10: $i] : ? [v11: $i] : (ti(v3, v6) = v11 & % 60.32/9.44 | ti(v3, v5) = v10 & $i(v11) & $i(v10) & ( ~ (v11 = v4) | ~ % 60.32/9.44 | (v10 = v4))))))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_9_sum__power2__eq__zero__iff) implies: % 60.32/9.44 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | ? [v4: $i] : % 60.32/9.44 | (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 60.32/9.44 | $i] : ! [v8: $i] : ! [v9: $i] : (v9 = v4 | ~ % 60.32/9.44 | (power_power(v3, v6, v2) = v8) | ~ (power_power(v3, v5, v2) = % 60.32/9.44 | v7) | ~ (plus_plus(v3, v7, v8) = v9) | ~ $i(v6) | ~ % 60.32/9.44 | $i(v5) | ? [v10: $i] : ? [v11: $i] : (ti(v3, v6) = v11 & % 60.32/9.44 | ti(v3, v5) = v10 & $i(v11) & $i(v10) & ( ~ (v11 = v4) | ~ % 60.32/9.44 | (v10 = v4)))) & ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 60.32/9.44 | ! [v8: $i] : ( ~ (power_power(v3, v6, v2) = v8) | ~ % 60.32/9.44 | (power_power(v3, v5, v2) = v7) | ~ (plus_plus(v3, v7, v8) = % 60.32/9.44 | v4) | ~ $i(v6) | ~ $i(v5) | (ti(v3, v6) = v4 & ti(v3, v5) % 60.32/9.44 | = v4))))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_10_power2__less__0) implies: % 60.32/9.44 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | ? [v4: $i] : % 60.32/9.44 | (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ % 60.32/9.44 | (power_power(v3, v5, v2) = v6) | ~ (ord_less(v3, v6, v4) = 0) % 60.32/9.44 | | ~ $i(v5))))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_11_zero__less__power2) implies: % 60.32/9.44 | (13) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ( ~ (linordered_idom(v3) = 0) | ~ $i(v3) | ? [v4: $i] : % 60.32/9.44 | (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 60.32/9.44 | int] : (v7 = 0 | ~ (power_power(v3, v5, v2) = v6) | ~ % 60.32/9.44 | (ord_less(v3, v4, v6) = v7) | ~ $i(v5) | ti(v3, v5) = v4) & % 60.32/9.44 | ! [v5: $i] : ! [v6: $i] : ( ~ (power_power(v3, v5, v2) = v6) | % 60.32/9.44 | ~ (ord_less(v3, v4, v6) = 0) | ~ $i(v5) | ? [v7: $i] : ( ~ % 60.32/9.44 | (v7 = v4) & ti(v3, v5) = v7 & $i(v7)))))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_12_one__power2) implies: % 60.32/9.44 | (14) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ % 60.32/9.44 | (power_power(v3, v4, v2) = v5) | ~ (one_one(v3) = v4) | ~ $i(v3) % 60.32/9.44 | | ? [v6: int] : ( ~ (v6 = 0) & semiring_1(v3) = v6))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_13_zero__power2) implies: % 60.32/9.44 | (15) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | ~ % 60.32/9.44 | (power_power(v3, v4, v2) = v5) | ~ (zero_zero(v3) = v4) | ~ % 60.32/9.44 | $i(v3) | ? [v6: int] : ( ~ (v6 = 0) & semiring_1(v3) = v6))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_14_zero__eq__power2) implies: % 60.32/9.44 | (16) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (number_number_of(nat, v1) = % 60.32/9.44 | v2 & bit1(pls) = v0 & bit0(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ! % 60.32/9.44 | [v3: $i] : ( ~ (ring_11004092258visors(v3) = 0) | ~ $i(v3) | ? % 60.32/9.44 | [v4: $i] : (zero_zero(v3) = v4 & $i(v4) & ! [v5: $i] : ! [v6: % 60.32/9.44 | $i] : (v6 = v4 | ~ (power_power(v3, v5, v2) = v6) | ~ $i(v5) % 60.32/9.44 | | ? [v7: $i] : ( ~ (v7 = v4) & ti(v3, v5) = v7 & $i(v7))) & % 60.32/9.44 | ! [v5: $i] : ( ~ (power_power(v3, v5, v2) = v4) | ~ $i(v5) | % 60.32/9.44 | ti(v3, v5) = v4)))) % 60.32/9.44 | % 60.32/9.44 | ALPHA: (fact_15_add__special_I2_J) implies: % 60.32/9.45 | (17) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 60.32/9.45 | (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: $i] : (one_one(v1) = % 60.32/9.45 | v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 60.32/9.45 | (number_number_of(v1, v4) = v5) | ~ (plus_plus(int, v0, v3) = % 60.32/9.45 | v4) | ~ $i(v3) | ? [v6: $i] : (number_number_of(v1, v3) = % 60.32/9.45 | v6 & plus_plus(v1, v2, v6) = v5 & $i(v6) & $i(v5)))))) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_16_add__special_I3_J) implies: % 60.32/9.45 | (18) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 60.32/9.45 | (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: $i] : (one_one(v1) = % 60.32/9.45 | v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 60.32/9.45 | (number_number_of(v1, v4) = v5) | ~ (plus_plus(int, v3, v0) = % 60.32/9.45 | v4) | ~ $i(v3) | ? [v6: $i] : (number_number_of(v1, v3) = % 60.32/9.45 | v6 & plus_plus(v1, v6, v2) = v5 & $i(v6) & $i(v5)))))) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_17_t__l__p) implies: % 60.32/9.45 | (19) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.45 | ? [v5: $i] : ? [v6: $i] : (ord_less(int, t, v6) = 0 & % 60.32/9.45 | number_number_of(int, v2) = v3 & bit1(pls) = v0 & bit0(v1) = v2 & % 60.32/9.45 | bit0(v0) = v1 & times_times(int, v3, m) = v4 & plus_plus(int, v4, % 60.32/9.45 | v5) = v6 & one_one(int) = v5 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 60.32/9.45 | $i(v2) & $i(v1) & $i(v0)) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_18__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_) % 60.32/9.45 | implies: % 60.32/9.45 | (20) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.45 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 60.32/9.45 | (power_power(int, s, v2) = v3 & number_number_of(nat, v1) = v2 & % 60.32/9.45 | number_number_of(int, v6) = v7 & bit1(pls) = v0 & bit0(v1) = v6 & % 60.32/9.45 | bit0(v0) = v1 & times_times(int, v7, m) = v8 & plus_plus(int, v8, % 60.32/9.45 | v4) = v9 & plus_plus(int, v3, v4) = v5 & one_one(int) = v4 & % 60.32/9.45 | $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 60.32/9.45 | $i(v2) & $i(v1) & $i(v0) & ? [v10: $i] : (times_times(int, v9, v10) % 60.32/9.45 | = v5 & $i(v10))) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_19_p) implies: % 60.32/9.45 | (21) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.45 | ? [v5: $i] : ? [v6: $i] : (number_number_of(int, v2) = v3 & bit1(pls) % 60.32/9.45 | = v0 & bit0(v1) = v2 & bit0(v0) = v1 & zprime(v6) = 0 & % 60.32/9.45 | times_times(int, v3, m) = v4 & plus_plus(int, v4, v5) = v6 & % 60.32/9.45 | one_one(int) = v5 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 60.32/9.45 | $i(v1) & $i(v0)) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_20_qf1pt) implies: % 60.32/9.45 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.32/9.45 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : (twoSqu33214720sum2sq(v7) = 0 % 60.32/9.45 | & number_number_of(int, v2) = v3 & bit1(pls) = v0 & bit0(v1) = v2 & % 60.32/9.45 | bit0(v0) = v1 & times_times(int, v6, t) = v7 & times_times(int, v3, % 60.32/9.45 | m) = v4 & plus_plus(int, v4, v5) = v6 & one_one(int) = v5 & $i(v7) % 60.32/9.45 | & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_22_number__of__is__id) implies: % 60.32/9.45 | (23) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (number_number_of(int, v0) = % 60.32/9.45 | v1) | ~ $i(v0)) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_23_zmult__commute) implies: % 60.32/9.45 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (times_times(int, v0, % 60.32/9.45 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | (times_times(int, v1, v0) = % 60.32/9.45 | v2 & $i(v2))) % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_34_rel__simps_I19_J) implies: % 60.32/9.45 | (25) ord_less_eq(int, pls, pls) = 0 % 60.32/9.45 | % 60.32/9.45 | ALPHA: (fact_51_rel__simps_I22_J) implies: % 60.32/9.46 | (26) ! [v0: $i] : ( ~ (ord_less_eq(int, pls, v0) = 0) | ~ $i(v0) | ? % 60.32/9.46 | [v1: $i] : (ord_less_eq(int, pls, v1) = 0 & bit1(v0) = v1 & $i(v1))) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_59_le__special_I4_J) implies: % 60.32/9.46 | (27) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 60.32/9.46 | (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: any] : ? [v3: $i] : % 60.32/9.46 | (linordered_idom(v1) = v2 & one_one(v1) = v3 & $i(v3) & ( ~ (v2 = % 60.32/9.46 | 0) | ( ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ % 60.32/9.46 | (ord_less_eq(int, v4, v0) = v5) | ~ $i(v4) | ? [v6: $i] % 60.32/9.46 | : ? [v7: int] : ( ~ (v7 = 0) & ord_less_eq(v1, v6, v3) = % 60.32/9.46 | v7 & number_number_of(v1, v4) = v6 & $i(v6))) & ! [v4: % 60.32/9.46 | $i] : ( ~ (ord_less_eq(int, v4, v0) = 0) | ~ $i(v4) | ? % 60.32/9.46 | [v5: $i] : (ord_less_eq(v1, v5, v3) = 0 & % 60.32/9.46 | number_number_of(v1, v4) = v5 & $i(v5)))))))) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_60_le__special_I2_J) implies: % 60.32/9.46 | (28) ? [v0: $i] : (bit1(pls) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 60.32/9.46 | (number_ring(v1) = 0) | ~ $i(v1) | ? [v2: any] : ? [v3: $i] : % 60.32/9.46 | (linordered_idom(v1) = v2 & one_one(v1) = v3 & $i(v3) & ( ~ (v2 = % 60.32/9.46 | 0) | ( ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ % 60.32/9.46 | (ord_less_eq(int, v0, v4) = v5) | ~ $i(v4) | ? [v6: $i] % 60.32/9.46 | : ? [v7: int] : ( ~ (v7 = 0) & ord_less_eq(v1, v3, v6) = % 60.32/9.46 | v7 & number_number_of(v1, v4) = v6 & $i(v6))) & ! [v4: % 60.32/9.46 | $i] : ( ~ (ord_less_eq(int, v0, v4) = 0) | ~ $i(v4) | ? % 60.32/9.46 | [v5: $i] : (ord_less_eq(v1, v3, v5) = 0 & % 60.32/9.46 | number_number_of(v1, v4) = v5 & $i(v5)))))))) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_61_nat__1__add__1) implies: % 60.32/9.46 | (29) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 60.32/9.46 | (number_number_of(nat, v3) = v1 & bit1(pls) = v2 & bit0(v2) = v3 & % 60.32/9.46 | plus_plus(nat, v0, v0) = v1 & one_one(nat) = v0 & $i(v3) & $i(v2) & % 60.32/9.46 | $i(v1) & $i(v0)) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_62_mult__Pls) implies: % 60.32/9.46 | (30) ! [v0: $i] : ! [v1: $i] : (v1 = pls | ~ (times_times(int, pls, v0) % 60.32/9.46 | = v1) | ~ $i(v0)) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_65_zmult__1__right) implies: % 60.32/9.46 | (31) ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 60.32/9.46 | : (v2 = v1 | ~ (times_times(int, v1, v0) = v2) | ~ $i(v1))) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_66_zmult__1) implies: % 60.32/9.46 | (32) ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 60.32/9.46 | : (v2 = v1 | ~ (times_times(int, v0, v1) = v2) | ~ $i(v1))) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_77_int__one__le__iff__zero__less) implies: % 60.32/9.46 | (33) ? [v0: $i] : ? [v1: $i] : (zero_zero(int) = v1 & one_one(int) = v0 & % 60.32/9.46 | $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 60.32/9.46 | (ord_less(int, v1, v2) = v3) | ~ $i(v2) | ? [v4: int] : ( ~ (v4 % 60.32/9.46 | = 0) & ord_less_eq(int, v0, v2) = v4)) & ! [v2: $i] : ( ~ % 60.32/9.46 | (ord_less(int, v1, v2) = 0) | ~ $i(v2) | ord_less_eq(int, v0, v2) % 60.32/9.46 | = 0)) % 60.32/9.46 | % 60.32/9.46 | ALPHA: (fact_78_nat__numeral__1__eq__1) implies: % 60.32/9.47 | (34) ? [v0: $i] : ? [v1: $i] : (number_number_of(nat, v0) = v1 & % 60.32/9.47 | bit1(pls) = v0 & one_one(nat) = v1 & $i(v1) & $i(v0)) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_79_Numeral1__eq1__nat) implies: % 60.32/9.47 | (35) ? [v0: $i] : ? [v1: $i] : (number_number_of(nat, v1) = v0 & % 60.32/9.47 | bit1(pls) = v1 & one_one(nat) = v0 & $i(v1) & $i(v0)) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_80_zless__imp__add1__zle) implies: % 60.32/9.47 | (36) ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 60.32/9.47 | : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less_eq(int, v3, % 60.32/9.47 | v2) = v4) | ~ (plus_plus(int, v1, v0) = v3) | ~ $i(v2) | ~ % 60.32/9.47 | $i(v1) | ? [v5: int] : ( ~ (v5 = 0) & ord_less(int, v1, v2) = % 60.32/9.47 | v5))) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_81_add1__zle__eq) implies: % 60.32/9.47 | (37) ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 60.32/9.47 | : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less_eq(int, v3, % 60.32/9.47 | v2) = v4) | ~ (plus_plus(int, v1, v0) = v3) | ~ $i(v2) | ~ % 60.32/9.47 | $i(v1) | ? [v5: int] : ( ~ (v5 = 0) & ord_less(int, v1, v2) = % 60.32/9.47 | v5)) & ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 60.32/9.47 | (ord_less_eq(int, v3, v2) = 0) | ~ (plus_plus(int, v1, v0) = v3) % 60.32/9.47 | | ~ $i(v2) | ~ $i(v1) | ord_less(int, v1, v2) = 0)) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_82_zle__add1__eq__le) implies: % 60.32/9.47 | (38) ? [v0: $i] : (one_one(int) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] % 60.32/9.47 | : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (ord_less(int, v1, v3) = % 60.32/9.47 | v4) | ~ (plus_plus(int, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | % 60.32/9.47 | ? [v5: int] : ( ~ (v5 = 0) & ord_less_eq(int, v1, v2) = v5)) & ! % 60.32/9.47 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (ord_less(int, v1, v3) = % 60.32/9.47 | 0) | ~ (plus_plus(int, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | % 60.32/9.47 | ord_less_eq(int, v1, v2) = 0)) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_83_semiring__add__number__of) implies: % 60.32/9.47 | (39) ! [v0: $i] : ( ~ (number_semiring(v0) = 0) | ~ $i(v0) | ! [v1: $i] % 60.32/9.47 | : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 60.32/9.47 | (number_number_of(v0, v2) = v3) | ~ (number_number_of(v0, v1) = % 60.32/9.47 | v4) | ~ (plus_plus(v0, v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | % 60.32/9.47 | ? [v6: any] : ? [v7: any] : ? [v8: $i] : ? [v9: $i] : % 60.32/9.47 | (ord_less_eq(int, pls, v2) = v6 & ord_less_eq(int, pls, v1) = v7 & % 60.32/9.47 | number_number_of(v0, v8) = v9 & plus_plus(int, v2, v1) = v8 & % 60.32/9.47 | $i(v9) & $i(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = v5)))) % 60.32/9.47 | % 60.32/9.47 | ALPHA: (fact_85_le__imp__0__less) implies: % 60.32/9.47 | (40) ? [v0: $i] : ? [v1: $i] : (zero_zero(int) = v0 & one_one(int) = v1 & % 60.70/9.47 | $i(v1) & $i(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ (plus_plus(int, % 60.70/9.47 | v1, v2) = v3) | ~ $i(v2) | ? [v4: any] : ? [v5: any] : % 60.70/9.47 | (ord_less_eq(int, v0, v2) = v4 & ord_less(int, v0, v3) = v5 & ( ~ % 60.70/9.47 | (v4 = 0) | v5 = 0)))) % 60.70/9.47 | % 60.70/9.47 | ALPHA: (fact_96_zadd__commute) implies: % 60.70/9.48 | (41) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (plus_plus(int, v0, v1) % 60.70/9.48 | = v2) | ~ $i(v1) | ~ $i(v0) | (plus_plus(int, v1, v0) = v2 & % 60.70/9.48 | $i(v2))) % 60.70/9.48 | % 60.70/9.48 | ALPHA: (fact_97_zero__is__num__zero) implies: % 60.70/9.48 | (42) ? [v0: $i] : (number_number_of(int, pls) = v0 & zero_zero(int) = v0 & % 60.70/9.48 | $i(v0)) % 60.70/9.48 | % 60.70/9.48 | ALPHA: (arity_Nat_Onat___Int_Onumber__semiring) implies: % 60.70/9.48 | (43) number_semiring(nat) = 0 % 60.70/9.48 | % 60.70/9.48 | ALPHA: (arity_Nat_Onat___Orderings_Olinorder) implies: % 60.70/9.48 | (44) linorder(nat) = 0 % 60.70/9.48 | % 60.70/9.48 | ALPHA: (arity_Nat_Onat___Int_Onumber) implies: % 60.70/9.48 | (45) number(nat) = 0 % 60.70/9.48 | % 60.70/9.48 | ALPHA: (conj_0) implies: % 60.70/9.48 | (46) $i(pls) % 60.70/9.48 | (47) $i(nat) % 60.70/9.48 | (48) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.70/9.48 | ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ( ~ (v7 = 0) & % 60.70/9.48 | power_power(int, s, v2) = v3 & ord_less(int, v5, v6) = v7 & % 60.70/9.48 | number_number_of(nat, v1) = v2 & bit1(pls) = v0 & bit0(v0) = v1 & % 60.70/9.48 | zero_zero(int) = v6 & plus_plus(int, v3, v4) = v5 & one_one(int) = % 60.70/9.48 | v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.70/9.48 | % 60.70/9.48 | ALPHA: (function-axioms) implies: % 60.73/9.48 | (49) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (one_one(v2) = % 60.73/9.48 | v1) | ~ (one_one(v2) = v0)) % 60.73/9.48 | (50) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 60.73/9.48 | : (v1 = v0 | ~ (number(v2) = v1) | ~ (number(v2) = v0)) % 60.73/9.48 | (51) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (zero_zero(v2) % 60.73/9.48 | = v1) | ~ (zero_zero(v2) = v0)) % 60.73/9.48 | (52) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit0(v2) = % 60.73/9.48 | v1) | ~ (bit0(v2) = v0)) % 60.73/9.48 | (53) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bit1(v2) = % 60.73/9.48 | v1) | ~ (bit1(v2) = v0)) % 60.73/9.48 | (54) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 60.73/9.48 | (number_number_of(v3, v2) = v1) | ~ (number_number_of(v3, v2) = % 60.73/9.48 | v0)) % 60.73/9.48 | (55) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 60.73/9.48 | (v1 = v0 | ~ (plus_plus(v4, v3, v2) = v1) | ~ (plus_plus(v4, v3, v2) % 60.73/9.48 | = v0)) % 60.73/9.48 | (56) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 60.73/9.48 | (v1 = v0 | ~ (times_times(v4, v3, v2) = v1) | ~ (times_times(v4, v3, % 60.73/9.48 | v2) = v0)) % 60.73/9.48 | (57) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 60.73/9.48 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (ord_less(v4, v3, v2) = % 60.73/9.48 | v1) | ~ (ord_less(v4, v3, v2) = v0)) % 60.73/9.49 | (58) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 60.73/9.49 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (ord_less_eq(v4, v3, v2) = % 60.73/9.49 | v1) | ~ (ord_less_eq(v4, v3, v2) = v0)) % 60.73/9.49 | (59) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 60.73/9.49 | (v1 = v0 | ~ (power_power(v4, v3, v2) = v1) | ~ (power_power(v4, v3, % 60.73/9.49 | v2) = v0)) % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (42) with fresh symbol all_97_0 gives: % 60.73/9.49 | (60) number_number_of(int, pls) = all_97_0 & zero_zero(int) = all_97_0 & % 60.73/9.49 | $i(all_97_0) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (60) implies: % 60.73/9.49 | (61) zero_zero(int) = all_97_0 % 60.73/9.49 | (62) number_number_of(int, pls) = all_97_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (2) with fresh symbol all_103_0 gives: % 60.73/9.49 | (63) ord_less(int, t, all_103_0) = 0 & zero_zero(int) = all_103_0 & % 60.73/9.49 | $i(all_103_0) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (63) implies: % 60.73/9.49 | (64) $i(all_103_0) % 60.73/9.49 | (65) zero_zero(int) = all_103_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (3) with fresh symbol all_105_0 gives: % 60.73/9.49 | (66) ord_less(int, t, all_105_0) = 0 & one_one(int) = all_105_0 & % 60.73/9.49 | $i(all_105_0) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (66) implies: % 60.73/9.49 | (67) one_one(int) = all_105_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (7) with fresh symbols all_107_0, all_107_1 gives: % 60.73/9.49 | (68) ~ (all_107_0 = 0) & ord_less_eq(int, all_107_1, t) = all_107_0 & % 60.73/9.49 | one_one(int) = all_107_1 & $i(all_107_1) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (68) implies: % 60.73/9.49 | (69) $i(all_107_1) % 60.73/9.49 | (70) one_one(int) = all_107_1 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (35) with fresh symbols all_109_0, all_109_1 gives: % 60.73/9.49 | (71) number_number_of(nat, all_109_0) = all_109_1 & bit1(pls) = all_109_0 & % 60.73/9.49 | one_one(nat) = all_109_1 & $i(all_109_0) & $i(all_109_1) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (71) implies: % 60.73/9.49 | (72) one_one(nat) = all_109_1 % 60.73/9.49 | (73) bit1(pls) = all_109_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (32) with fresh symbol all_111_0 gives: % 60.73/9.49 | (74) one_one(int) = all_111_0 & $i(all_111_0) & ! [v0: $i] : ! [v1: $i] : % 60.73/9.49 | (v1 = v0 | ~ (times_times(int, all_111_0, v0) = v1) | ~ $i(v0)) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (74) implies: % 60.73/9.49 | (75) one_one(int) = all_111_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (34) with fresh symbols all_114_0, all_114_1 gives: % 60.73/9.49 | (76) number_number_of(nat, all_114_1) = all_114_0 & bit1(pls) = all_114_1 & % 60.73/9.49 | one_one(nat) = all_114_0 & $i(all_114_0) & $i(all_114_1) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (76) implies: % 60.73/9.49 | (77) one_one(nat) = all_114_0 % 60.73/9.49 | (78) bit1(pls) = all_114_1 % 60.73/9.49 | (79) number_number_of(nat, all_114_1) = all_114_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (31) with fresh symbol all_116_0 gives: % 60.73/9.49 | (80) one_one(int) = all_116_0 & $i(all_116_0) & ! [v0: $i] : ! [v1: $i] : % 60.73/9.49 | (v1 = v0 | ~ (times_times(int, v0, all_116_0) = v1) | ~ $i(v0)) % 60.73/9.49 | % 60.73/9.49 | ALPHA: (80) implies: % 60.73/9.49 | (81) one_one(int) = all_116_0 % 60.73/9.49 | % 60.73/9.49 | DELTA: instantiating (36) with fresh symbol all_119_0 gives: % 60.73/9.50 | (82) one_one(int) = all_119_0 & $i(all_119_0) & ! [v0: $i] : ! [v1: $i] : % 60.73/9.50 | ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (ord_less_eq(int, v2, v1) = % 60.73/9.50 | v3) | ~ (plus_plus(int, v0, all_119_0) = v2) | ~ $i(v1) | ~ % 60.73/9.50 | $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & ord_less(int, v0, v1) = v4)) % 60.73/9.50 | % 60.73/9.50 | ALPHA: (82) implies: % 60.73/9.50 | (83) one_one(int) = all_119_0 % 60.73/9.50 | % 60.73/9.50 | DELTA: instantiating (29) with fresh symbols all_122_0, all_122_1, all_122_2, % 60.73/9.50 | all_122_3 gives: % 60.73/9.50 | (84) number_number_of(nat, all_122_0) = all_122_2 & bit1(pls) = all_122_1 & % 60.73/9.50 | bit0(all_122_1) = all_122_0 & plus_plus(nat, all_122_3, all_122_3) = % 60.73/9.50 | all_122_2 & one_one(nat) = all_122_3 & $i(all_122_0) & $i(all_122_1) & % 60.73/9.50 | $i(all_122_2) & $i(all_122_3) % 60.73/9.50 | % 60.73/9.50 | ALPHA: (84) implies: % 60.73/9.50 | (85) one_one(nat) = all_122_3 % 60.73/9.50 | (86) plus_plus(nat, all_122_3, all_122_3) = all_122_2 % 60.73/9.50 | (87) bit0(all_122_1) = all_122_0 % 60.73/9.50 | (88) bit1(pls) = all_122_1 % 60.73/9.50 | (89) number_number_of(nat, all_122_0) = all_122_2 % 60.73/9.50 | % 60.73/9.50 | DELTA: instantiating (40) with fresh symbols all_124_0, all_124_1 gives: % 60.73/9.50 | (90) zero_zero(int) = all_124_1 & one_one(int) = all_124_0 & $i(all_124_0) % 60.73/9.50 | & $i(all_124_1) & ! [v0: $i] : ! [v1: $i] : ( ~ (plus_plus(int, % 60.73/9.50 | all_124_0, v0) = v1) | ~ $i(v0) | ? [v2: any] : ? [v3: any] : % 60.73/9.50 | (ord_less_eq(int, all_124_1, v0) = v2 & ord_less(int, all_124_1, v1) % 60.73/9.50 | = v3 & ( ~ (v2 = 0) | v3 = 0))) % 60.73/9.50 | % 60.73/9.50 | ALPHA: (90) implies: % 60.73/9.50 | (91) one_one(int) = all_124_0 % 60.73/9.50 | (92) zero_zero(int) = all_124_1 % 60.73/9.50 | % 60.73/9.50 | DELTA: instantiating (14) with fresh symbols all_133_0, all_133_1, all_133_2 % 60.73/9.50 | gives: % 60.73/9.50 | (93) number_number_of(nat, all_133_1) = all_133_0 & bit1(pls) = all_133_2 & % 60.73/9.50 | bit0(all_133_2) = all_133_1 & $i(all_133_0) & $i(all_133_1) & % 60.73/9.50 | $i(all_133_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | % 60.73/9.50 | ~ (power_power(v0, v1, all_133_0) = v2) | ~ (one_one(v0) = v1) | ~ % 60.73/9.50 | $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & semiring_1(v0) = v3)) % 60.73/9.50 | % 60.73/9.50 | ALPHA: (93) implies: % 60.73/9.50 | (94) bit0(all_133_2) = all_133_1 % 60.73/9.50 | (95) bit1(pls) = all_133_2 % 60.73/9.50 | (96) number_number_of(nat, all_133_1) = all_133_0 % 60.73/9.50 | % 60.83/9.50 | DELTA: instantiating (33) with fresh symbols all_136_0, all_136_1 gives: % 60.83/9.50 | (97) zero_zero(int) = all_136_0 & one_one(int) = all_136_1 & $i(all_136_0) % 60.83/9.50 | & $i(all_136_1) & ! [v0: $i] : ! [v1: int] : (v1 = 0 | ~ % 60.83/9.50 | (ord_less(int, all_136_0, v0) = v1) | ~ $i(v0) | ? [v2: int] : ( ~ % 60.83/9.50 | (v2 = 0) & ord_less_eq(int, all_136_1, v0) = v2)) & ! [v0: $i] : % 60.83/9.50 | ( ~ (ord_less(int, all_136_0, v0) = 0) | ~ $i(v0) | ord_less_eq(int, % 60.83/9.50 | all_136_1, v0) = 0) % 60.83/9.50 | % 60.83/9.50 | ALPHA: (97) implies: % 60.83/9.50 | (98) one_one(int) = all_136_1 % 60.83/9.50 | (99) zero_zero(int) = all_136_0 % 60.83/9.50 | % 60.83/9.50 | DELTA: instantiating (15) with fresh symbols all_139_0, all_139_1, all_139_2 % 60.83/9.50 | gives: % 60.83/9.51 | (100) number_number_of(nat, all_139_1) = all_139_0 & bit1(pls) = all_139_2 % 60.83/9.51 | & bit0(all_139_2) = all_139_1 & $i(all_139_0) & $i(all_139_1) & % 60.83/9.51 | $i(all_139_2) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | % 60.83/9.51 | ~ (power_power(v0, v1, all_139_0) = v2) | ~ (zero_zero(v0) = v1) | % 60.83/9.51 | ~ $i(v0) | ? [v3: int] : ( ~ (v3 = 0) & semiring_1(v0) = v3)) % 60.83/9.51 | % 60.83/9.51 | ALPHA: (100) implies: % 60.83/9.51 | (101) bit0(all_139_2) = all_139_1 % 60.83/9.51 | (102) bit1(pls) = all_139_2 % 60.83/9.51 | (103) number_number_of(nat, all_139_1) = all_139_0 % 60.83/9.51 | % 60.83/9.51 | DELTA: instantiating (18) with fresh symbol all_142_0 gives: % 60.83/9.51 | (104) bit1(pls) = all_142_0 & $i(all_142_0) & ! [v0: $i] : ( ~ % 60.83/9.51 | (number_ring(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (one_one(v0) = v1 % 60.83/9.51 | & $i(v1) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 60.83/9.51 | (number_number_of(v0, v3) = v4) | ~ (plus_plus(int, v2, % 60.83/9.51 | all_142_0) = v3) | ~ $i(v2) | ? [v5: $i] : % 60.83/9.51 | (number_number_of(v0, v2) = v5 & plus_plus(v0, v5, v1) = v4 & % 60.83/9.51 | $i(v5) & $i(v4))))) % 60.83/9.51 | % 60.83/9.51 | ALPHA: (104) implies: % 60.83/9.51 | (105) bit1(pls) = all_142_0 % 60.83/9.51 | % 60.83/9.51 | DELTA: instantiating (17) with fresh symbol all_145_0 gives: % 60.83/9.51 | (106) bit1(pls) = all_145_0 & $i(all_145_0) & ! [v0: $i] : ( ~ % 60.83/9.51 | (number_ring(v0) = 0) | ~ $i(v0) | ? [v1: $i] : (one_one(v0) = v1 % 60.83/9.51 | & $i(v1) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 60.83/9.51 | (number_number_of(v0, v3) = v4) | ~ (plus_plus(int, all_145_0, % 60.83/9.51 | v2) = v3) | ~ $i(v2) | ? [v5: $i] : (number_number_of(v0, % 60.83/9.51 | v2) = v5 & plus_plus(v0, v1, v5) = v4 & $i(v5) & $i(v4))))) % 60.83/9.51 | % 60.83/9.51 | ALPHA: (106) implies: % 60.83/9.51 | (107) bit1(pls) = all_145_0 % 60.83/9.51 | % 60.83/9.51 | DELTA: instantiating (12) with fresh symbols all_148_0, all_148_1, all_148_2 % 60.83/9.51 | gives: % 60.83/9.51 | (108) number_number_of(nat, all_148_1) = all_148_0 & bit1(pls) = all_148_2 % 60.83/9.51 | & bit0(all_148_2) = all_148_1 & $i(all_148_0) & $i(all_148_1) & % 60.83/9.51 | $i(all_148_2) & ! [v0: $i] : ( ~ (linordered_idom(v0) = 0) | ~ % 60.83/9.51 | $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] : % 60.83/9.51 | ! [v3: $i] : ( ~ (power_power(v0, v2, all_148_0) = v3) | ~ % 60.83/9.51 | (ord_less(v0, v3, v1) = 0) | ~ $i(v2)))) % 60.83/9.51 | % 60.83/9.51 | ALPHA: (108) implies: % 60.83/9.51 | (109) bit0(all_148_2) = all_148_1 % 60.83/9.51 | (110) bit1(pls) = all_148_2 % 60.83/9.51 | (111) number_number_of(nat, all_148_1) = all_148_0 % 60.83/9.51 | % 60.83/9.51 | DELTA: instantiating (37) with fresh symbol all_151_0 gives: % 60.83/9.52 | (112) one_one(int) = all_151_0 & $i(all_151_0) & ! [v0: $i] : ! [v1: $i] % 60.83/9.52 | : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (ord_less_eq(int, v2, v1) % 60.83/9.52 | = v3) | ~ (plus_plus(int, v0, all_151_0) = v2) | ~ $i(v1) | ~ % 60.83/9.52 | $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & ord_less(int, v0, v1) = v4)) % 60.83/9.52 | & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (ord_less_eq(int, v2, % 60.83/9.52 | v1) = 0) | ~ (plus_plus(int, v0, all_151_0) = v2) | ~ $i(v1) % 60.83/9.52 | | ~ $i(v0) | ord_less(int, v0, v1) = 0) % 60.83/9.52 | % 60.83/9.52 | ALPHA: (112) implies: % 60.83/9.52 | (113) one_one(int) = all_151_0 % 60.83/9.52 | % 60.83/9.52 | DELTA: instantiating (38) with fresh symbol all_154_0 gives: % 60.83/9.52 | (114) one_one(int) = all_154_0 & $i(all_154_0) & ! [v0: $i] : ! [v1: $i] % 60.83/9.52 | : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (ord_less(int, v0, v2) = % 60.83/9.52 | v3) | ~ (plus_plus(int, v1, all_154_0) = v2) | ~ $i(v1) | ~ % 60.83/9.52 | $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & ord_less_eq(int, v0, v1) = % 60.83/9.52 | v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.83/9.52 | (ord_less(int, v0, v2) = 0) | ~ (plus_plus(int, v1, all_154_0) = % 60.83/9.52 | v2) | ~ $i(v1) | ~ $i(v0) | ord_less_eq(int, v0, v1) = 0) % 60.83/9.52 | % 60.83/9.52 | ALPHA: (114) implies: % 60.83/9.52 | (115) one_one(int) = all_154_0 % 60.83/9.52 | % 60.83/9.52 | DELTA: instantiating (19) with fresh symbols all_160_0, all_160_1, all_160_2, % 60.83/9.52 | all_160_3, all_160_4, all_160_5, all_160_6 gives: % 60.89/9.52 | (116) ord_less(int, t, all_160_0) = 0 & number_number_of(int, all_160_4) = % 60.89/9.52 | all_160_3 & bit1(pls) = all_160_6 & bit0(all_160_5) = all_160_4 & % 60.89/9.52 | bit0(all_160_6) = all_160_5 & times_times(int, all_160_3, m) = % 60.89/9.52 | all_160_2 & plus_plus(int, all_160_2, all_160_1) = all_160_0 & % 60.89/9.52 | one_one(int) = all_160_1 & $i(all_160_0) & $i(all_160_1) & % 60.89/9.52 | $i(all_160_2) & $i(all_160_3) & $i(all_160_4) & $i(all_160_5) & % 60.89/9.52 | $i(all_160_6) % 60.89/9.52 | % 60.89/9.52 | ALPHA: (116) implies: % 60.89/9.52 | (117) one_one(int) = all_160_1 % 60.89/9.52 | (118) plus_plus(int, all_160_2, all_160_1) = all_160_0 % 60.89/9.52 | (119) times_times(int, all_160_3, m) = all_160_2 % 60.89/9.52 | (120) bit0(all_160_6) = all_160_5 % 60.89/9.52 | (121) bit0(all_160_5) = all_160_4 % 60.89/9.52 | (122) bit1(pls) = all_160_6 % 60.89/9.52 | (123) number_number_of(int, all_160_4) = all_160_3 % 60.89/9.52 | % 60.89/9.52 | DELTA: instantiating (21) with fresh symbols all_162_0, all_162_1, all_162_2, % 60.89/9.52 | all_162_3, all_162_4, all_162_5, all_162_6 gives: % 60.89/9.52 | (124) number_number_of(int, all_162_4) = all_162_3 & bit1(pls) = all_162_6 % 60.89/9.52 | & bit0(all_162_5) = all_162_4 & bit0(all_162_6) = all_162_5 & % 60.89/9.52 | zprime(all_162_0) = 0 & times_times(int, all_162_3, m) = all_162_2 & % 60.89/9.52 | plus_plus(int, all_162_2, all_162_1) = all_162_0 & one_one(int) = % 60.89/9.52 | all_162_1 & $i(all_162_0) & $i(all_162_1) & $i(all_162_2) & % 60.89/9.52 | $i(all_162_3) & $i(all_162_4) & $i(all_162_5) & $i(all_162_6) % 60.89/9.52 | % 60.89/9.52 | ALPHA: (124) implies: % 60.89/9.52 | (125) $i(all_162_2) % 60.89/9.52 | (126) one_one(int) = all_162_1 % 60.89/9.52 | (127) plus_plus(int, all_162_2, all_162_1) = all_162_0 % 60.89/9.52 | (128) times_times(int, all_162_3, m) = all_162_2 % 60.89/9.52 | (129) bit0(all_162_6) = all_162_5 % 60.89/9.52 | (130) bit0(all_162_5) = all_162_4 % 60.89/9.52 | (131) bit1(pls) = all_162_6 % 60.89/9.52 | (132) number_number_of(int, all_162_4) = all_162_3 % 60.89/9.52 | % 60.89/9.52 | DELTA: instantiating (48) with fresh symbols all_164_0, all_164_1, all_164_2, % 60.89/9.53 | all_164_3, all_164_4, all_164_5, all_164_6, all_164_7 gives: % 60.89/9.53 | (133) ~ (all_164_0 = 0) & power_power(int, s, all_164_5) = all_164_4 & % 60.89/9.53 | ord_less(int, all_164_2, all_164_1) = all_164_0 & % 60.89/9.53 | number_number_of(nat, all_164_6) = all_164_5 & bit1(pls) = all_164_7 % 60.89/9.53 | & bit0(all_164_7) = all_164_6 & zero_zero(int) = all_164_1 & % 60.89/9.53 | plus_plus(int, all_164_4, all_164_3) = all_164_2 & one_one(int) = % 60.89/9.53 | all_164_3 & $i(all_164_1) & $i(all_164_2) & $i(all_164_3) & % 60.89/9.53 | $i(all_164_4) & $i(all_164_5) & $i(all_164_6) & $i(all_164_7) % 60.89/9.53 | % 60.89/9.53 | ALPHA: (133) implies: % 60.89/9.53 | (134) ~ (all_164_0 = 0) % 60.89/9.53 | (135) one_one(int) = all_164_3 % 60.89/9.53 | (136) plus_plus(int, all_164_4, all_164_3) = all_164_2 % 60.89/9.53 | (137) zero_zero(int) = all_164_1 % 60.89/9.53 | (138) bit0(all_164_7) = all_164_6 % 60.89/9.53 | (139) bit1(pls) = all_164_7 % 60.89/9.53 | (140) number_number_of(nat, all_164_6) = all_164_5 % 60.89/9.53 | (141) ord_less(int, all_164_2, all_164_1) = all_164_0 % 60.89/9.53 | (142) power_power(int, s, all_164_5) = all_164_4 % 60.89/9.53 | % 60.89/9.53 | DELTA: instantiating (9) with fresh symbols all_166_0, all_166_1, all_166_2 % 60.89/9.53 | gives: % 60.89/9.53 | (143) number_number_of(nat, all_166_1) = all_166_0 & bit1(pls) = all_166_2 % 60.89/9.53 | & bit0(all_166_2) = all_166_1 & $i(all_166_0) & $i(all_166_1) & % 60.89/9.53 | $i(all_166_2) & ! [v0: $i] : ( ~ (linordered_idom(v0) = 0) | ~ % 60.89/9.53 | $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] : % 60.89/9.53 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ % 60.89/9.53 | (power_power(v0, v3, all_166_0) = v5) | ~ (power_power(v0, v2, % 60.89/9.53 | all_166_0) = v4) | ~ (ord_less(v0, v6, v1) = 0) | ~ % 60.89/9.53 | (plus_plus(v0, v4, v5) = v6) | ~ $i(v3) | ~ $i(v2)))) % 60.89/9.53 | % 60.89/9.53 | ALPHA: (143) implies: % 60.89/9.53 | (144) bit0(all_166_2) = all_166_1 % 60.89/9.53 | (145) bit1(pls) = all_166_2 % 60.89/9.53 | (146) number_number_of(nat, all_166_1) = all_166_0 % 60.89/9.53 | % 60.89/9.53 | DELTA: instantiating (6) with fresh symbols all_169_0, all_169_1, all_169_2, % 60.89/9.53 | all_169_3, all_169_4, all_169_5, all_169_6 gives: % 60.89/9.53 | (147) power_power(int, s, all_169_3) = all_169_2 & number_number_of(nat, % 60.89/9.53 | all_169_4) = all_169_3 & bit1(pls) = all_169_5 & bit0(all_169_5) = % 60.89/9.53 | all_169_4 & zero_zero(int) = all_169_6 & plus_plus(int, all_169_2, % 60.89/9.53 | all_169_1) = all_169_0 & one_one(int) = all_169_1 & $i(all_169_0) & % 60.89/9.53 | $i(all_169_1) & $i(all_169_2) & $i(all_169_3) & $i(all_169_4) & % 60.89/9.53 | $i(all_169_5) & $i(all_169_6) & ( ~ (all_169_6 = t) | all_169_0 = t) % 60.89/9.53 | % 60.89/9.53 | ALPHA: (147) implies: % 60.89/9.53 | (148) one_one(int) = all_169_1 % 60.89/9.53 | (149) plus_plus(int, all_169_2, all_169_1) = all_169_0 % 60.89/9.53 | (150) zero_zero(int) = all_169_6 % 60.89/9.53 | (151) bit0(all_169_5) = all_169_4 % 60.89/9.53 | (152) bit1(pls) = all_169_5 % 60.89/9.54 | (153) number_number_of(nat, all_169_4) = all_169_3 % 60.89/9.54 | (154) power_power(int, s, all_169_3) = all_169_2 % 60.89/9.54 | % 60.89/9.54 | DELTA: instantiating (22) with fresh symbols all_171_0, all_171_1, all_171_2, % 60.89/9.54 | all_171_3, all_171_4, all_171_5, all_171_6, all_171_7 gives: % 60.89/9.54 | (155) twoSqu33214720sum2sq(all_171_0) = 0 & number_number_of(int, % 60.89/9.54 | all_171_5) = all_171_4 & bit1(pls) = all_171_7 & bit0(all_171_6) = % 60.89/9.54 | all_171_5 & bit0(all_171_7) = all_171_6 & times_times(int, all_171_1, % 60.89/9.54 | t) = all_171_0 & times_times(int, all_171_4, m) = all_171_3 & % 60.89/9.54 | plus_plus(int, all_171_3, all_171_2) = all_171_1 & one_one(int) = % 60.89/9.54 | all_171_2 & $i(all_171_0) & $i(all_171_1) & $i(all_171_2) & % 60.89/9.54 | $i(all_171_3) & $i(all_171_4) & $i(all_171_5) & $i(all_171_6) & % 60.89/9.54 | $i(all_171_7) % 60.89/9.54 | % 60.89/9.54 | ALPHA: (155) implies: % 60.89/9.54 | (156) one_one(int) = all_171_2 % 60.89/9.54 | (157) plus_plus(int, all_171_3, all_171_2) = all_171_1 % 60.89/9.54 | (158) times_times(int, all_171_4, m) = all_171_3 % 60.89/9.54 | (159) bit0(all_171_7) = all_171_6 % 60.89/9.54 | (160) bit0(all_171_6) = all_171_5 % 60.89/9.54 | (161) bit1(pls) = all_171_7 % 60.89/9.54 | (162) number_number_of(int, all_171_5) = all_171_4 % 60.89/9.54 | % 60.89/9.54 | DELTA: instantiating (8) with fresh symbols all_173_0, all_173_1, all_173_2, % 60.89/9.54 | all_173_3, all_173_4, all_173_5, all_173_6, all_173_7 gives: % 60.89/9.54 | (163) ord_less(int, all_173_7, all_173_0) = 0 & number_number_of(int, % 60.89/9.54 | all_173_4) = all_173_3 & bit1(pls) = all_173_6 & bit0(all_173_5) = % 60.89/9.54 | all_173_4 & bit0(all_173_6) = all_173_5 & zero_zero(int) = all_173_7 % 60.89/9.54 | & times_times(int, all_173_3, m) = all_173_2 & plus_plus(int, % 60.89/9.54 | all_173_2, all_173_1) = all_173_0 & one_one(int) = all_173_1 & % 60.89/9.54 | $i(all_173_0) & $i(all_173_1) & $i(all_173_2) & $i(all_173_3) & % 60.89/9.54 | $i(all_173_4) & $i(all_173_5) & $i(all_173_6) & $i(all_173_7) % 60.89/9.54 | % 60.89/9.54 | ALPHA: (163) implies: % 60.89/9.54 | (164) one_one(int) = all_173_1 % 60.89/9.54 | (165) plus_plus(int, all_173_2, all_173_1) = all_173_0 % 60.89/9.54 | (166) times_times(int, all_173_3, m) = all_173_2 % 60.89/9.54 | (167) zero_zero(int) = all_173_7 % 60.89/9.54 | (168) bit0(all_173_6) = all_173_5 % 60.89/9.54 | (169) bit0(all_173_5) = all_173_4 % 60.89/9.54 | (170) bit1(pls) = all_173_6 % 60.89/9.54 | (171) number_number_of(int, all_173_4) = all_173_3 % 60.89/9.54 | % 60.89/9.54 | DELTA: instantiating (16) with fresh symbols all_175_0, all_175_1, all_175_2 % 60.89/9.54 | gives: % 60.89/9.54 | (172) number_number_of(nat, all_175_1) = all_175_0 & bit1(pls) = all_175_2 % 60.89/9.54 | & bit0(all_175_2) = all_175_1 & $i(all_175_0) & $i(all_175_1) & % 60.89/9.54 | $i(all_175_2) & ! [v0: $i] : ( ~ (ring_11004092258visors(v0) = 0) | % 60.89/9.54 | ~ $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] % 60.89/9.54 | : ! [v3: $i] : (v3 = v1 | ~ (power_power(v0, v2, all_175_0) = % 60.89/9.54 | v3) | ~ $i(v2) | ? [v4: $i] : ( ~ (v4 = v1) & ti(v0, v2) = % 60.89/9.54 | v4 & $i(v4))) & ! [v2: $i] : ( ~ (power_power(v0, v2, % 60.89/9.54 | all_175_0) = v1) | ~ $i(v2) | ti(v0, v2) = v1))) % 60.89/9.54 | % 60.89/9.54 | ALPHA: (172) implies: % 60.89/9.55 | (173) bit0(all_175_2) = all_175_1 % 60.89/9.55 | (174) bit1(pls) = all_175_2 % 60.89/9.55 | (175) number_number_of(nat, all_175_1) = all_175_0 % 60.89/9.55 | % 60.89/9.55 | DELTA: instantiating (28) with fresh symbol all_178_0 gives: % 60.89/9.55 | (176) bit1(pls) = all_178_0 & $i(all_178_0) & ! [v0: $i] : ( ~ % 60.89/9.55 | (number_ring(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? [v2: $i] : % 60.89/9.55 | (linordered_idom(v0) = v1 & one_one(v0) = v2 & $i(v2) & ( ~ (v1 = % 60.89/9.55 | 0) | ( ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 60.89/9.55 | (ord_less_eq(int, all_178_0, v3) = v4) | ~ $i(v3) | ? % 60.89/9.55 | [v5: $i] : ? [v6: int] : ( ~ (v6 = 0) & ord_less_eq(v0, % 60.89/9.55 | v2, v5) = v6 & number_number_of(v0, v3) = v5 & $i(v5))) % 60.89/9.55 | & ! [v3: $i] : ( ~ (ord_less_eq(int, all_178_0, v3) = 0) | % 60.89/9.55 | ~ $i(v3) | ? [v4: $i] : (ord_less_eq(v0, v2, v4) = 0 & % 60.89/9.55 | number_number_of(v0, v3) = v4 & $i(v4))))))) % 60.89/9.55 | % 60.89/9.55 | ALPHA: (176) implies: % 60.89/9.55 | (177) bit1(pls) = all_178_0 % 60.89/9.55 | % 60.89/9.55 | DELTA: instantiating (27) with fresh symbol all_181_0 gives: % 60.89/9.55 | (178) bit1(pls) = all_181_0 & $i(all_181_0) & ! [v0: $i] : ( ~ % 60.89/9.55 | (number_ring(v0) = 0) | ~ $i(v0) | ? [v1: any] : ? [v2: $i] : % 60.89/9.55 | (linordered_idom(v0) = v1 & one_one(v0) = v2 & $i(v2) & ( ~ (v1 = % 60.89/9.55 | 0) | ( ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 60.89/9.55 | (ord_less_eq(int, v3, all_181_0) = v4) | ~ $i(v3) | ? % 60.89/9.55 | [v5: $i] : ? [v6: int] : ( ~ (v6 = 0) & ord_less_eq(v0, % 60.89/9.55 | v5, v2) = v6 & number_number_of(v0, v3) = v5 & $i(v5))) % 60.89/9.55 | & ! [v3: $i] : ( ~ (ord_less_eq(int, v3, all_181_0) = 0) | % 60.89/9.55 | ~ $i(v3) | ? [v4: $i] : (ord_less_eq(v0, v4, v2) = 0 & % 60.89/9.55 | number_number_of(v0, v3) = v4 & $i(v4))))))) % 60.89/9.55 | % 60.89/9.55 | ALPHA: (178) implies: % 60.89/9.55 | (179) bit1(pls) = all_181_0 % 60.89/9.55 | % 60.89/9.55 | DELTA: instantiating (13) with fresh symbols all_184_0, all_184_1, all_184_2 % 60.89/9.55 | gives: % 60.89/9.55 | (180) number_number_of(nat, all_184_1) = all_184_0 & bit1(pls) = all_184_2 % 60.89/9.55 | & bit0(all_184_2) = all_184_1 & $i(all_184_0) & $i(all_184_1) & % 60.89/9.55 | $i(all_184_2) & ! [v0: $i] : ( ~ (linordered_idom(v0) = 0) | ~ % 60.89/9.55 | $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] : % 60.89/9.55 | ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ (power_power(v0, v2, % 60.89/9.55 | all_184_0) = v3) | ~ (ord_less(v0, v1, v3) = v4) | ~ % 60.89/9.55 | $i(v2) | ti(v0, v2) = v1) & ! [v2: $i] : ! [v3: $i] : ( ~ % 60.89/9.55 | (power_power(v0, v2, all_184_0) = v3) | ~ (ord_less(v0, v1, % 60.89/9.55 | v3) = 0) | ~ $i(v2) | ? [v4: $i] : ( ~ (v4 = v1) & ti(v0, % 60.89/9.55 | v2) = v4 & $i(v4))))) % 60.89/9.55 | % 60.89/9.55 | ALPHA: (180) implies: % 60.89/9.55 | (181) bit0(all_184_2) = all_184_1 % 60.89/9.55 | (182) bit1(pls) = all_184_2 % 60.89/9.55 | (183) number_number_of(nat, all_184_1) = all_184_0 % 60.89/9.55 | % 60.89/9.55 | DELTA: instantiating (5) with fresh symbols all_187_0, all_187_1, all_187_2, % 60.89/9.55 | all_187_3, all_187_4, all_187_5, all_187_6, all_187_7, all_187_8, % 60.89/9.55 | all_187_9 gives: % 60.89/9.55 | (184) power_power(int, s, all_187_7) = all_187_6 & number_number_of(nat, % 60.89/9.55 | all_187_8) = all_187_7 & number_number_of(int, all_187_3) = % 60.89/9.55 | all_187_2 & bit1(pls) = all_187_9 & bit0(all_187_8) = all_187_3 & % 60.89/9.55 | bit0(all_187_9) = all_187_8 & times_times(int, all_187_0, t) = % 60.89/9.55 | all_187_4 & times_times(int, all_187_2, m) = all_187_1 & % 60.89/9.55 | plus_plus(int, all_187_1, all_187_5) = all_187_0 & plus_plus(int, % 60.89/9.55 | all_187_6, all_187_5) = all_187_4 & one_one(int) = all_187_5 & % 60.89/9.55 | $i(all_187_0) & $i(all_187_1) & $i(all_187_2) & $i(all_187_3) & % 60.89/9.55 | $i(all_187_4) & $i(all_187_5) & $i(all_187_6) & $i(all_187_7) & % 60.89/9.55 | $i(all_187_8) & $i(all_187_9) % 60.89/9.55 | % 60.89/9.55 | ALPHA: (184) implies: % 60.89/9.55 | (185) one_one(int) = all_187_5 % 60.89/9.55 | (186) plus_plus(int, all_187_6, all_187_5) = all_187_4 % 60.89/9.55 | (187) plus_plus(int, all_187_1, all_187_5) = all_187_0 % 60.89/9.55 | (188) times_times(int, all_187_2, m) = all_187_1 % 60.89/9.55 | (189) times_times(int, all_187_0, t) = all_187_4 % 60.89/9.55 | (190) bit0(all_187_9) = all_187_8 % 60.89/9.55 | (191) bit0(all_187_8) = all_187_3 % 60.89/9.55 | (192) bit1(pls) = all_187_9 % 60.89/9.55 | (193) number_number_of(int, all_187_3) = all_187_2 % 60.89/9.56 | (194) number_number_of(nat, all_187_8) = all_187_7 % 60.89/9.56 | (195) power_power(int, s, all_187_7) = all_187_6 % 60.89/9.56 | % 60.89/9.56 | DELTA: instantiating (4) with fresh symbols all_189_0, all_189_1, all_189_2, % 60.89/9.56 | all_189_3, all_189_4, all_189_5, all_189_6, all_189_7, all_189_8, % 60.89/9.56 | all_189_9 gives: % 60.89/9.56 | (196) ord_less(int, all_189_2, all_189_0) = 0 & number_number_of(int, % 60.89/9.56 | all_189_7) = all_189_6 & bit1(pls) = all_189_9 & bit0(all_189_8) = % 60.89/9.56 | all_189_7 & bit0(all_189_9) = all_189_8 & zero_zero(int) = all_189_1 % 60.89/9.56 | & times_times(int, all_189_3, all_189_1) = all_189_0 & % 60.89/9.56 | times_times(int, all_189_3, t) = all_189_2 & times_times(int, % 60.89/9.56 | all_189_6, m) = all_189_5 & plus_plus(int, all_189_5, all_189_4) = % 60.89/9.56 | all_189_3 & one_one(int) = all_189_4 & $i(all_189_0) & $i(all_189_1) % 60.89/9.56 | & $i(all_189_2) & $i(all_189_3) & $i(all_189_4) & $i(all_189_5) & % 60.89/9.56 | $i(all_189_6) & $i(all_189_7) & $i(all_189_8) & $i(all_189_9) % 60.89/9.56 | % 60.89/9.56 | ALPHA: (196) implies: % 60.89/9.56 | (197) one_one(int) = all_189_4 % 60.89/9.56 | (198) plus_plus(int, all_189_5, all_189_4) = all_189_3 % 60.89/9.56 | (199) times_times(int, all_189_6, m) = all_189_5 % 60.89/9.56 | (200) times_times(int, all_189_3, t) = all_189_2 % 60.89/9.56 | (201) times_times(int, all_189_3, all_189_1) = all_189_0 % 60.89/9.56 | (202) zero_zero(int) = all_189_1 % 60.89/9.56 | (203) bit0(all_189_9) = all_189_8 % 60.89/9.56 | (204) bit0(all_189_8) = all_189_7 % 60.89/9.56 | (205) bit1(pls) = all_189_9 % 60.89/9.56 | (206) number_number_of(int, all_189_7) = all_189_6 % 60.89/9.56 | (207) ord_less(int, all_189_2, all_189_0) = 0 % 60.89/9.56 | % 60.89/9.56 | DELTA: instantiating (20) with fresh symbols all_191_0, all_191_1, all_191_2, % 60.89/9.56 | all_191_3, all_191_4, all_191_5, all_191_6, all_191_7, all_191_8, % 60.89/9.56 | all_191_9 gives: % 60.89/9.56 | (208) power_power(int, s, all_191_7) = all_191_6 & number_number_of(nat, % 60.89/9.56 | all_191_8) = all_191_7 & number_number_of(int, all_191_3) = % 60.89/9.56 | all_191_2 & bit1(pls) = all_191_9 & bit0(all_191_8) = all_191_3 & % 60.89/9.56 | bit0(all_191_9) = all_191_8 & times_times(int, all_191_2, m) = % 60.89/9.56 | all_191_1 & plus_plus(int, all_191_1, all_191_5) = all_191_0 & % 60.89/9.56 | plus_plus(int, all_191_6, all_191_5) = all_191_4 & one_one(int) = % 60.89/9.56 | all_191_5 & $i(all_191_0) & $i(all_191_1) & $i(all_191_2) & % 60.89/9.56 | $i(all_191_3) & $i(all_191_4) & $i(all_191_5) & $i(all_191_6) & % 60.89/9.56 | $i(all_191_7) & $i(all_191_8) & $i(all_191_9) & ? [v0: $i] : % 60.89/9.56 | (times_times(int, all_191_0, v0) = all_191_4 & $i(v0)) % 60.89/9.56 | % 60.89/9.56 | ALPHA: (208) implies: % 60.89/9.56 | (209) one_one(int) = all_191_5 % 60.89/9.56 | (210) plus_plus(int, all_191_6, all_191_5) = all_191_4 % 60.89/9.56 | (211) plus_plus(int, all_191_1, all_191_5) = all_191_0 % 60.89/9.56 | (212) times_times(int, all_191_2, m) = all_191_1 % 60.89/9.56 | (213) bit0(all_191_9) = all_191_8 % 60.89/9.56 | (214) bit0(all_191_8) = all_191_3 % 60.89/9.56 | (215) bit1(pls) = all_191_9 % 60.89/9.56 | (216) number_number_of(int, all_191_3) = all_191_2 % 60.89/9.56 | (217) number_number_of(nat, all_191_8) = all_191_7 % 60.89/9.56 | (218) power_power(int, s, all_191_7) = all_191_6 % 60.89/9.56 | % 60.89/9.56 | DELTA: instantiating (11) with fresh symbols all_193_0, all_193_1, all_193_2 % 60.89/9.56 | gives: % 60.89/9.56 | (219) number_number_of(nat, all_193_1) = all_193_0 & bit1(pls) = all_193_2 % 60.89/9.56 | & bit0(all_193_2) = all_193_1 & $i(all_193_0) & $i(all_193_1) & % 60.89/9.56 | $i(all_193_2) & ! [v0: $i] : ( ~ (linordered_idom(v0) = 0) | ~ % 60.89/9.56 | $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] : % 60.89/9.56 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v6 = v1 % 60.89/9.56 | | ~ (power_power(v0, v3, all_193_0) = v5) | ~ % 60.89/9.56 | (power_power(v0, v2, all_193_0) = v4) | ~ (plus_plus(v0, v4, % 60.89/9.56 | v5) = v6) | ~ $i(v3) | ~ $i(v2) | ? [v7: $i] : ? [v8: % 60.89/9.56 | $i] : (ti(v0, v3) = v8 & ti(v0, v2) = v7 & $i(v8) & $i(v7) & % 60.89/9.56 | ( ~ (v8 = v1) | ~ (v7 = v1)))) & ! [v2: $i] : ! [v3: $i] : % 60.89/9.57 | ! [v4: $i] : ! [v5: $i] : ( ~ (power_power(v0, v3, all_193_0) = % 60.89/9.57 | v5) | ~ (power_power(v0, v2, all_193_0) = v4) | ~ % 60.89/9.57 | (plus_plus(v0, v4, v5) = v1) | ~ $i(v3) | ~ $i(v2) | (ti(v0, % 60.89/9.57 | v3) = v1 & ti(v0, v2) = v1)))) % 60.89/9.57 | % 60.89/9.57 | ALPHA: (219) implies: % 60.89/9.57 | (220) bit0(all_193_2) = all_193_1 % 60.89/9.57 | (221) bit1(pls) = all_193_2 % 60.89/9.57 | (222) number_number_of(nat, all_193_1) = all_193_0 % 60.89/9.57 | % 60.89/9.57 | DELTA: instantiating (10) with fresh symbols all_196_0, all_196_1, all_196_2 % 60.89/9.57 | gives: % 60.89/9.57 | (223) number_number_of(nat, all_196_1) = all_196_0 & bit1(pls) = all_196_2 % 60.89/9.57 | & bit0(all_196_2) = all_196_1 & $i(all_196_0) & $i(all_196_1) & % 60.89/9.57 | $i(all_196_2) & ! [v0: $i] : ( ~ (linordered_idom(v0) = 0) | ~ % 60.89/9.57 | $i(v0) | ? [v1: $i] : (zero_zero(v0) = v1 & $i(v1) & ! [v2: $i] : % 60.89/9.57 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 60.89/9.57 | int] : (v7 = 0 | ~ (power_power(v0, v3, all_196_0) = v5) | ~ % 60.89/9.57 | (power_power(v0, v2, all_196_0) = v4) | ~ (ord_less(v0, v1, % 60.89/9.57 | v6) = v7) | ~ (plus_plus(v0, v4, v5) = v6) | ~ $i(v3) | % 60.89/9.57 | ~ $i(v2) | (ti(v0, v3) = v1 & ti(v0, v2) = v1)) & ! [v2: $i] : % 60.89/9.57 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ % 60.89/9.57 | (power_power(v0, v3, all_196_0) = v5) | ~ (power_power(v0, v2, % 60.89/9.57 | all_196_0) = v4) | ~ (ord_less(v0, v1, v6) = 0) | ~ % 60.89/9.57 | (plus_plus(v0, v4, v5) = v6) | ~ $i(v3) | ~ $i(v2) | ? [v7: % 60.89/9.57 | $i] : ? [v8: $i] : (ti(v0, v3) = v8 & ti(v0, v2) = v7 & % 60.89/9.57 | $i(v8) & $i(v7) & ( ~ (v8 = v1) | ~ (v7 = v1)))))) % 60.89/9.57 | % 60.89/9.57 | ALPHA: (223) implies: % 60.89/9.57 | (224) bit0(all_196_2) = all_196_1 % 60.89/9.57 | (225) bit1(pls) = all_196_2 % 60.89/9.57 | (226) number_number_of(nat, all_196_1) = all_196_0 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_116_0, all_119_0, int, simplifying % 60.89/9.57 | with (81), (83) gives: % 60.89/9.57 | (227) all_119_0 = all_116_0 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_119_0, all_124_0, int, simplifying % 60.89/9.57 | with (83), (91) gives: % 60.89/9.57 | (228) all_124_0 = all_119_0 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_136_1, all_151_0, int, simplifying % 60.89/9.57 | with (98), (113) gives: % 60.89/9.57 | (229) all_151_0 = all_136_1 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_124_0, all_151_0, int, simplifying % 60.89/9.57 | with (91), (113) gives: % 60.89/9.57 | (230) all_151_0 = all_124_0 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_116_0, all_160_1, int, simplifying % 60.89/9.57 | with (81), (117) gives: % 60.89/9.57 | (231) all_160_1 = all_116_0 % 60.89/9.57 | % 60.89/9.57 | GROUND_INST: instantiating (49) with all_107_1, all_160_1, int, simplifying % 60.89/9.57 | with (70), (117) gives: % 60.89/9.57 | (232) all_160_1 = all_107_1 % 60.89/9.57 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_160_1, all_173_1, int, simplifying % 60.89/9.58 | with (117), (164) gives: % 60.89/9.58 | (233) all_173_1 = all_160_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_111_0, all_173_1, int, simplifying % 60.89/9.58 | with (75), (164) gives: % 60.89/9.58 | (234) all_173_1 = all_111_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_173_1, all_187_5, int, simplifying % 60.89/9.58 | with (164), (185) gives: % 60.89/9.58 | (235) all_187_5 = all_173_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_164_3, all_187_5, int, simplifying % 60.89/9.58 | with (135), (185) gives: % 60.89/9.58 | (236) all_187_5 = all_164_3 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_171_2, all_189_4, int, simplifying % 60.89/9.58 | with (156), (197) gives: % 60.89/9.58 | (237) all_189_4 = all_171_2 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_169_1, all_189_4, int, simplifying % 60.89/9.58 | with (148), (197) gives: % 60.89/9.58 | (238) all_189_4 = all_169_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_105_0, all_189_4, int, simplifying % 60.89/9.58 | with (67), (197) gives: % 60.89/9.58 | (239) all_189_4 = all_105_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_189_4, all_191_5, int, simplifying % 60.89/9.58 | with (197), (209) gives: % 60.89/9.58 | (240) all_191_5 = all_189_4 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_162_1, all_191_5, int, simplifying % 60.89/9.58 | with (126), (209) gives: % 60.89/9.58 | (241) all_191_5 = all_162_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_154_0, all_191_5, int, simplifying % 60.89/9.58 | with (115), (209) gives: % 60.89/9.58 | (242) all_191_5 = all_154_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_151_0, all_191_5, int, simplifying % 60.89/9.58 | with (113), (209) gives: % 60.89/9.58 | (243) all_191_5 = all_151_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_114_0, all_122_3, nat, simplifying % 60.89/9.58 | with (77), (85) gives: % 60.89/9.58 | (244) all_122_3 = all_114_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (49) with all_109_1, all_122_3, nat, simplifying % 60.89/9.58 | with (72), (85) gives: % 60.89/9.58 | (245) all_122_3 = all_109_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_136_0, all_164_1, int, simplifying % 60.89/9.58 | with (99), (137) gives: % 60.89/9.58 | (246) all_164_1 = all_136_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_103_0, all_164_1, int, simplifying % 60.89/9.58 | with (65), (137) gives: % 60.89/9.58 | (247) all_164_1 = all_103_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_136_0, all_169_6, int, simplifying % 60.89/9.58 | with (99), (150) gives: % 60.89/9.58 | (248) all_169_6 = all_136_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_97_0, all_169_6, int, simplifying % 60.89/9.58 | with (61), (150) gives: % 60.89/9.58 | (249) all_169_6 = all_97_0 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_164_1, all_173_7, int, simplifying % 60.89/9.58 | with (137), (167) gives: % 60.89/9.58 | (250) all_173_7 = all_164_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_173_7, all_189_1, int, simplifying % 60.89/9.58 | with (167), (202) gives: % 60.89/9.58 | (251) all_189_1 = all_173_7 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (51) with all_124_1, all_189_1, int, simplifying % 60.89/9.58 | with (92), (202) gives: % 60.89/9.58 | (252) all_189_1 = all_124_1 % 60.89/9.58 | % 60.89/9.58 | GROUND_INST: instantiating (53) with all_139_2, all_145_0, pls, simplifying % 60.89/9.58 | with (102), (107) gives: % 60.89/9.59 | (253) all_145_0 = all_139_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_114_1, all_145_0, pls, simplifying % 60.89/9.59 | with (78), (107) gives: % 60.89/9.59 | (254) all_145_0 = all_114_1 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_148_2, all_162_6, pls, simplifying % 60.89/9.59 | with (110), (131) gives: % 60.89/9.59 | (255) all_162_6 = all_148_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_145_0, all_162_6, pls, simplifying % 60.89/9.59 | with (107), (131) gives: % 60.89/9.59 | (256) all_162_6 = all_145_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_133_2, all_162_6, pls, simplifying % 60.89/9.59 | with (95), (131) gives: % 60.89/9.59 | (257) all_162_6 = all_133_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_160_6, all_164_7, pls, simplifying % 60.89/9.59 | with (122), (139) gives: % 60.89/9.59 | (258) all_164_7 = all_160_6 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_164_7, all_166_2, pls, simplifying % 60.89/9.59 | with (139), (145) gives: % 60.89/9.59 | (259) all_166_2 = all_164_7 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_148_2, all_169_5, pls, simplifying % 60.89/9.59 | with (110), (152) gives: % 60.89/9.59 | (260) all_169_5 = all_148_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_169_5, all_173_6, pls, simplifying % 60.89/9.59 | with (152), (170) gives: % 60.89/9.59 | (261) all_173_6 = all_169_5 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_181_0, all_184_2, pls, simplifying % 60.89/9.59 | with (179), (182) gives: % 60.89/9.59 | (262) all_184_2 = all_181_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_160_6, all_184_2, pls, simplifying % 60.89/9.59 | with (122), (182) gives: % 60.89/9.59 | (263) all_184_2 = all_160_6 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_145_0, all_184_2, pls, simplifying % 60.89/9.59 | with (107), (182) gives: % 60.89/9.59 | (264) all_184_2 = all_145_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_142_0, all_184_2, pls, simplifying % 60.89/9.59 | with (105), (182) gives: % 60.89/9.59 | (265) all_184_2 = all_142_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_178_0, all_187_9, pls, simplifying % 60.89/9.59 | with (177), (192) gives: % 60.89/9.59 | (266) all_187_9 = all_178_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_122_1, all_187_9, pls, simplifying % 60.89/9.59 | with (88), (192) gives: % 60.89/9.59 | (267) all_187_9 = all_122_1 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_173_6, all_189_9, pls, simplifying % 60.89/9.59 | with (170), (205) gives: % 60.89/9.59 | (268) all_189_9 = all_173_6 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_189_9, all_191_9, pls, simplifying % 60.89/9.59 | with (205), (215) gives: % 60.89/9.59 | (269) all_191_9 = all_189_9 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_178_0, all_193_2, pls, simplifying % 60.89/9.59 | with (177), (221) gives: % 60.89/9.59 | (270) all_193_2 = all_178_0 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_175_2, all_193_2, pls, simplifying % 60.89/9.59 | with (174), (221) gives: % 60.89/9.59 | (271) all_193_2 = all_175_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_171_7, all_193_2, pls, simplifying % 60.89/9.59 | with (161), (221) gives: % 60.89/9.59 | (272) all_193_2 = all_171_7 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_166_2, all_193_2, pls, simplifying % 60.89/9.59 | with (145), (221) gives: % 60.89/9.59 | (273) all_193_2 = all_166_2 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_191_9, all_196_2, pls, simplifying % 60.89/9.59 | with (215), (225) gives: % 60.89/9.59 | (274) all_196_2 = all_191_9 % 60.89/9.59 | % 60.89/9.59 | GROUND_INST: instantiating (53) with all_109_0, all_196_2, pls, simplifying % 60.89/9.59 | with (73), (225) gives: % 60.89/9.59 | (275) all_196_2 = all_109_0 % 60.89/9.59 | % 60.89/9.59 | COMBINE_EQS: (274), (275) imply: % 60.89/9.60 | (276) all_191_9 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | SIMP: (276) implies: % 60.89/9.60 | (277) all_191_9 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (270), (271) imply: % 60.89/9.60 | (278) all_178_0 = all_175_2 % 60.89/9.60 | % 60.89/9.60 | SIMP: (278) implies: % 60.89/9.60 | (279) all_178_0 = all_175_2 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (271), (272) imply: % 60.89/9.60 | (280) all_175_2 = all_171_7 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (271), (273) imply: % 60.89/9.60 | (281) all_175_2 = all_166_2 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (241), (243) imply: % 60.89/9.60 | (282) all_162_1 = all_151_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (241), (242) imply: % 60.89/9.60 | (283) all_162_1 = all_154_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (240), (241) imply: % 60.89/9.60 | (284) all_189_4 = all_162_1 % 60.89/9.60 | % 60.89/9.60 | SIMP: (284) implies: % 60.89/9.60 | (285) all_189_4 = all_162_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (269), (277) imply: % 60.89/9.60 | (286) all_189_9 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | SIMP: (286) implies: % 60.89/9.60 | (287) all_189_9 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (251), (252) imply: % 60.89/9.60 | (288) all_173_7 = all_124_1 % 60.89/9.60 | % 60.89/9.60 | SIMP: (288) implies: % 60.89/9.60 | (289) all_173_7 = all_124_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (237), (238) imply: % 60.89/9.60 | (290) all_171_2 = all_169_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (237), (239) imply: % 60.89/9.60 | (291) all_171_2 = all_105_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (237), (285) imply: % 60.89/9.60 | (292) all_171_2 = all_162_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (268), (287) imply: % 60.89/9.60 | (293) all_173_6 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | SIMP: (293) implies: % 60.89/9.60 | (294) all_173_6 = all_109_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (235), (236) imply: % 60.89/9.60 | (295) all_173_1 = all_164_3 % 60.89/9.60 | % 60.89/9.60 | SIMP: (295) implies: % 60.89/9.60 | (296) all_173_1 = all_164_3 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (266), (267) imply: % 60.89/9.60 | (297) all_178_0 = all_122_1 % 60.89/9.60 | % 60.89/9.60 | SIMP: (297) implies: % 60.89/9.60 | (298) all_178_0 = all_122_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (262), (265) imply: % 60.89/9.60 | (299) all_181_0 = all_142_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (262), (264) imply: % 60.89/9.60 | (300) all_181_0 = all_145_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (262), (263) imply: % 60.89/9.60 | (301) all_181_0 = all_160_6 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (299), (300) imply: % 60.89/9.60 | (302) all_145_0 = all_142_0 % 60.89/9.60 | % 60.89/9.60 | SIMP: (302) implies: % 60.89/9.60 | (303) all_145_0 = all_142_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (299), (301) imply: % 60.89/9.60 | (304) all_160_6 = all_142_0 % 60.89/9.60 | % 60.89/9.60 | SIMP: (304) implies: % 60.89/9.60 | (305) all_160_6 = all_142_0 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (279), (298) imply: % 60.89/9.60 | (306) all_175_2 = all_122_1 % 60.89/9.60 | % 60.89/9.60 | SIMP: (306) implies: % 60.89/9.60 | (307) all_175_2 = all_122_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (280), (281) imply: % 60.89/9.60 | (308) all_171_7 = all_166_2 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (280), (307) imply: % 60.89/9.60 | (309) all_171_7 = all_122_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (233), (296) imply: % 60.89/9.60 | (310) all_164_3 = all_160_1 % 60.89/9.60 | % 60.89/9.60 | COMBINE_EQS: (234), (296) imply: % 60.89/9.60 | (311) all_164_3 = all_111_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (261), (294) imply: % 60.89/9.61 | (312) all_169_5 = all_109_0 % 60.89/9.61 | % 60.89/9.61 | SIMP: (312) implies: % 60.89/9.61 | (313) all_169_5 = all_109_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (250), (289) imply: % 60.89/9.61 | (314) all_164_1 = all_124_1 % 60.89/9.61 | % 60.89/9.61 | SIMP: (314) implies: % 60.89/9.61 | (315) all_164_1 = all_124_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (290), (291) imply: % 60.89/9.61 | (316) all_169_1 = all_105_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (290), (292) imply: % 60.89/9.61 | (317) all_169_1 = all_162_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (308), (309) imply: % 60.89/9.61 | (318) all_166_2 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | SIMP: (318) implies: % 60.89/9.61 | (319) all_166_2 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (316), (317) imply: % 60.89/9.61 | (320) all_162_1 = all_105_0 % 60.89/9.61 | % 60.89/9.61 | SIMP: (320) implies: % 60.89/9.61 | (321) all_162_1 = all_105_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (260), (313) imply: % 60.89/9.61 | (322) all_148_2 = all_109_0 % 60.89/9.61 | % 60.89/9.61 | SIMP: (322) implies: % 60.89/9.61 | (323) all_148_2 = all_109_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (248), (249) imply: % 60.89/9.61 | (324) all_136_0 = all_97_0 % 60.89/9.61 | % 60.89/9.61 | SIMP: (324) implies: % 60.89/9.61 | (325) all_136_0 = all_97_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (259), (319) imply: % 60.89/9.61 | (326) all_164_7 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | SIMP: (326) implies: % 60.89/9.61 | (327) all_164_7 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (247), (315) imply: % 60.89/9.61 | (328) all_124_1 = all_103_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (246), (315) imply: % 60.89/9.61 | (329) all_136_0 = all_124_1 % 60.89/9.61 | % 60.89/9.61 | SIMP: (329) implies: % 60.89/9.61 | (330) all_136_0 = all_124_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (310), (311) imply: % 60.89/9.61 | (331) all_160_1 = all_111_0 % 60.89/9.61 | % 60.89/9.61 | SIMP: (331) implies: % 60.89/9.61 | (332) all_160_1 = all_111_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (258), (327) imply: % 60.89/9.61 | (333) all_160_6 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | SIMP: (333) implies: % 60.89/9.61 | (334) all_160_6 = all_122_1 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (282), (283) imply: % 60.89/9.61 | (335) all_154_0 = all_151_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (283), (321) imply: % 60.89/9.61 | (336) all_154_0 = all_105_0 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (255), (257) imply: % 60.89/9.61 | (337) all_148_2 = all_133_2 % 60.89/9.61 | % 60.89/9.61 | SIMP: (337) implies: % 60.89/9.61 | (338) all_148_2 = all_133_2 % 60.89/9.61 | % 60.89/9.61 | COMBINE_EQS: (256), (257) imply: % 60.89/9.61 | (339) all_145_0 = all_133_2 % 61.28/9.61 | % 61.28/9.61 | SIMP: (339) implies: % 61.28/9.61 | (340) all_145_0 = all_133_2 % 61.28/9.61 | % 61.28/9.61 | COMBINE_EQS: (231), (332) imply: % 61.28/9.61 | (341) all_116_0 = all_111_0 % 61.28/9.61 | % 61.28/9.61 | SIMP: (341) implies: % 61.28/9.61 | (342) all_116_0 = all_111_0 % 61.28/9.61 | % 61.28/9.61 | COMBINE_EQS: (232), (332) imply: % 61.28/9.61 | (343) all_111_0 = all_107_1 % 61.28/9.61 | % 61.28/9.61 | COMBINE_EQS: (305), (334) imply: % 61.28/9.61 | (344) all_142_0 = all_122_1 % 61.28/9.61 | % 61.28/9.61 | SIMP: (344) implies: % 61.28/9.61 | (345) all_142_0 = all_122_1 % 61.28/9.61 | % 61.28/9.61 | COMBINE_EQS: (335), (336) imply: % 61.28/9.61 | (346) all_151_0 = all_105_0 % 61.28/9.61 | % 61.28/9.62 | SIMP: (346) implies: % 61.28/9.62 | (347) all_151_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (229), (230) imply: % 61.28/9.62 | (348) all_136_1 = all_124_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (229), (347) imply: % 61.28/9.62 | (349) all_136_1 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (323), (338) imply: % 61.28/9.62 | (350) all_133_2 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (350) implies: % 61.28/9.62 | (351) all_133_2 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (253), (254) imply: % 61.28/9.62 | (352) all_139_2 = all_114_1 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (253), (340) imply: % 61.28/9.62 | (353) all_139_2 = all_133_2 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (253), (303) imply: % 61.28/9.62 | (354) all_142_0 = all_139_2 % 61.28/9.62 | % 61.28/9.62 | SIMP: (354) implies: % 61.28/9.62 | (355) all_142_0 = all_139_2 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (345), (355) imply: % 61.28/9.62 | (356) all_139_2 = all_122_1 % 61.28/9.62 | % 61.28/9.62 | SIMP: (356) implies: % 61.28/9.62 | (357) all_139_2 = all_122_1 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (352), (357) imply: % 61.28/9.62 | (358) all_122_1 = all_114_1 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (353), (357) imply: % 61.28/9.62 | (359) all_133_2 = all_122_1 % 61.28/9.62 | % 61.28/9.62 | SIMP: (359) implies: % 61.28/9.62 | (360) all_133_2 = all_122_1 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (325), (330) imply: % 61.28/9.62 | (361) all_124_1 = all_97_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (361) implies: % 61.28/9.62 | (362) all_124_1 = all_97_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (348), (349) imply: % 61.28/9.62 | (363) all_124_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (363) implies: % 61.28/9.62 | (364) all_124_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (351), (360) imply: % 61.28/9.62 | (365) all_122_1 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (365) implies: % 61.28/9.62 | (366) all_122_1 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (228), (364) imply: % 61.28/9.62 | (367) all_119_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (367) implies: % 61.28/9.62 | (368) all_119_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (328), (362) imply: % 61.28/9.62 | (369) all_103_0 = all_97_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (369) implies: % 61.28/9.62 | (370) all_103_0 = all_97_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (358), (366) imply: % 61.28/9.62 | (371) all_114_1 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (371) implies: % 61.28/9.62 | (372) all_114_1 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (244), (245) imply: % 61.28/9.62 | (373) all_114_0 = all_109_1 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (227), (368) imply: % 61.28/9.62 | (374) all_116_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (374) implies: % 61.28/9.62 | (375) all_116_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (342), (375) imply: % 61.28/9.62 | (376) all_111_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (376) implies: % 61.28/9.62 | (377) all_111_0 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (343), (377) imply: % 61.28/9.62 | (378) all_107_1 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | SIMP: (378) implies: % 61.28/9.62 | (379) all_107_1 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (357), (366) imply: % 61.28/9.62 | (380) all_139_2 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (345), (366) imply: % 61.28/9.62 | (381) all_142_0 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (334), (366) imply: % 61.28/9.62 | (382) all_160_6 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (332), (377) imply: % 61.28/9.62 | (383) all_160_1 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (257), (351) imply: % 61.28/9.62 | (384) all_162_6 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (327), (366) imply: % 61.28/9.62 | (385) all_164_7 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (311), (377) imply: % 61.28/9.62 | (386) all_164_3 = all_105_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (315), (362) imply: % 61.28/9.62 | (387) all_164_1 = all_97_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (319), (366) imply: % 61.28/9.62 | (388) all_166_2 = all_109_0 % 61.28/9.62 | % 61.28/9.62 | COMBINE_EQS: (309), (366) imply: % 61.28/9.63 | (389) all_171_7 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (296), (386) imply: % 61.28/9.63 | (390) all_173_1 = all_105_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (280), (389) imply: % 61.28/9.63 | (391) all_175_2 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (299), (381) imply: % 61.28/9.63 | (392) all_181_0 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (262), (392) imply: % 61.28/9.63 | (393) all_184_2 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (267), (366) imply: % 61.28/9.63 | (394) all_187_9 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (236), (386) imply: % 61.28/9.63 | (395) all_187_5 = all_105_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (252), (362) imply: % 61.28/9.63 | (396) all_189_1 = all_97_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (241), (321) imply: % 61.28/9.63 | (397) all_191_5 = all_105_0 % 61.28/9.63 | % 61.28/9.63 | COMBINE_EQS: (271), (391) imply: % 61.28/9.63 | (398) all_193_2 = all_109_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (141), (387) imply: % 61.28/9.63 | (399) ord_less(int, all_164_2, all_97_0) = all_164_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (79), (372), (373) imply: % 61.28/9.63 | (400) number_number_of(nat, all_109_0) = all_109_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (224), (275) imply: % 61.28/9.63 | (401) bit0(all_109_0) = all_196_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (220), (398) imply: % 61.28/9.63 | (402) bit0(all_109_0) = all_193_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (213), (277) imply: % 61.28/9.63 | (403) bit0(all_109_0) = all_191_8 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (203), (287) imply: % 61.28/9.63 | (404) bit0(all_109_0) = all_189_8 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (190), (394) imply: % 61.28/9.63 | (405) bit0(all_109_0) = all_187_8 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (181), (393) imply: % 61.28/9.63 | (406) bit0(all_109_0) = all_184_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (173), (391) imply: % 61.28/9.63 | (407) bit0(all_109_0) = all_175_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (168), (294) imply: % 61.28/9.63 | (408) bit0(all_109_0) = all_173_5 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (159), (389) imply: % 61.28/9.63 | (409) bit0(all_109_0) = all_171_6 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (151), (313) imply: % 61.28/9.63 | (410) bit0(all_109_0) = all_169_4 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (144), (388) imply: % 61.28/9.63 | (411) bit0(all_109_0) = all_166_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (138), (385) imply: % 61.28/9.63 | (412) bit0(all_109_0) = all_164_6 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (129), (384) imply: % 61.28/9.63 | (413) bit0(all_109_0) = all_162_5 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (120), (382) imply: % 61.28/9.63 | (414) bit0(all_109_0) = all_160_5 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (109), (323) imply: % 61.28/9.63 | (415) bit0(all_109_0) = all_148_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (101), (380) imply: % 61.28/9.63 | (416) bit0(all_109_0) = all_139_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (94), (351) imply: % 61.28/9.63 | (417) bit0(all_109_0) = all_133_1 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (87), (366) imply: % 61.28/9.63 | (418) bit0(all_109_0) = all_122_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (201), (396) imply: % 61.28/9.63 | (419) times_times(int, all_189_3, all_97_0) = all_189_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (86), (245) imply: % 61.28/9.63 | (420) plus_plus(nat, all_109_1, all_109_1) = all_122_2 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (211), (397) imply: % 61.28/9.63 | (421) plus_plus(int, all_191_1, all_105_0) = all_191_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (210), (397) imply: % 61.28/9.63 | (422) plus_plus(int, all_191_6, all_105_0) = all_191_4 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (198), (239) imply: % 61.28/9.63 | (423) plus_plus(int, all_189_5, all_105_0) = all_189_3 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (187), (395) imply: % 61.28/9.63 | (424) plus_plus(int, all_187_1, all_105_0) = all_187_0 % 61.28/9.63 | % 61.28/9.63 | REDUCE: (186), (395) imply: % 61.28/9.63 | (425) plus_plus(int, all_187_6, all_105_0) = all_187_4 % 61.28/9.63 | % 61.28/9.64 | REDUCE: (165), (390) imply: % 61.28/9.64 | (426) plus_plus(int, all_173_2, all_105_0) = all_173_0 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (157), (291) imply: % 61.28/9.64 | (427) plus_plus(int, all_171_3, all_105_0) = all_171_1 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (149), (316) imply: % 61.28/9.64 | (428) plus_plus(int, all_169_2, all_105_0) = all_169_0 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (136), (386) imply: % 61.28/9.64 | (429) plus_plus(int, all_164_4, all_105_0) = all_164_2 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (127), (321) imply: % 61.28/9.64 | (430) plus_plus(int, all_162_2, all_105_0) = all_162_0 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (118), (383) imply: % 61.28/9.64 | (431) plus_plus(int, all_160_2, all_105_0) = all_160_0 % 61.28/9.64 | % 61.28/9.64 | REDUCE: (69), (379) imply: % 61.28/9.64 | (432) $i(all_105_0) % 61.28/9.64 | % 61.28/9.64 | REDUCE: (64), (370) imply: % 61.28/9.64 | (433) $i(all_97_0) % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_133_1, all_139_1, all_109_0, % 61.28/9.64 | simplifying with (416), (417) gives: % 61.28/9.64 | (434) all_139_1 = all_133_1 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_139_1, all_148_1, all_109_0, % 61.28/9.64 | simplifying with (415), (416) gives: % 61.28/9.64 | (435) all_148_1 = all_139_1 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_162_5, all_164_6, all_109_0, % 61.28/9.64 | simplifying with (412), (413) gives: % 61.28/9.64 | (436) all_164_6 = all_162_5 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_164_6, all_166_1, all_109_0, % 61.28/9.64 | simplifying with (411), (412) gives: % 61.28/9.64 | (437) all_166_1 = all_164_6 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_164_6, all_184_1, all_109_0, % 61.28/9.64 | simplifying with (406), (412) gives: % 61.28/9.64 | (438) all_184_1 = all_164_6 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_160_5, all_184_1, all_109_0, % 61.28/9.64 | simplifying with (406), (414) gives: % 61.28/9.64 | (439) all_184_1 = all_160_5 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_148_1, all_184_1, all_109_0, % 61.28/9.64 | simplifying with (406), (415) gives: % 61.28/9.64 | (440) all_184_1 = all_148_1 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_171_6, all_187_8, all_109_0, % 61.28/9.64 | simplifying with (405), (409) gives: % 61.28/9.64 | (441) all_187_8 = all_171_6 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_175_1, all_189_8, all_109_0, % 61.28/9.64 | simplifying with (404), (407) gives: % 61.28/9.64 | (442) all_189_8 = all_175_1 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_169_4, all_189_8, all_109_0, % 61.28/9.64 | simplifying with (404), (410) gives: % 61.28/9.64 | (443) all_189_8 = all_169_4 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_187_8, all_191_8, all_109_0, % 61.28/9.64 | simplifying with (403), (405) gives: % 61.28/9.64 | (444) all_191_8 = all_187_8 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_189_8, all_193_1, all_109_0, % 61.28/9.64 | simplifying with (402), (404) gives: % 61.28/9.64 | (445) all_193_1 = all_189_8 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_173_5, all_193_1, all_109_0, % 61.28/9.64 | simplifying with (402), (408) gives: % 61.28/9.64 | (446) all_193_1 = all_173_5 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_171_6, all_193_1, all_109_0, % 61.28/9.64 | simplifying with (402), (409) gives: % 61.28/9.64 | (447) all_193_1 = all_171_6 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_166_1, all_193_1, all_109_0, % 61.28/9.64 | simplifying with (402), (411) gives: % 61.28/9.64 | (448) all_193_1 = all_166_1 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_191_8, all_196_1, all_109_0, % 61.28/9.64 | simplifying with (401), (403) gives: % 61.28/9.64 | (449) all_196_1 = all_191_8 % 61.28/9.64 | % 61.28/9.64 | GROUND_INST: instantiating (52) with all_122_0, all_196_1, all_109_0, % 61.28/9.64 | simplifying with (401), (418) gives: % 61.28/9.64 | (450) all_196_1 = all_122_0 % 61.28/9.64 | % 61.28/9.64 | COMBINE_EQS: (449), (450) imply: % 61.28/9.64 | (451) all_191_8 = all_122_0 % 61.28/9.64 | % 61.28/9.64 | SIMP: (451) implies: % 61.28/9.64 | (452) all_191_8 = all_122_0 % 61.28/9.64 | % 61.28/9.64 | COMBINE_EQS: (445), (446) imply: % 61.28/9.64 | (453) all_189_8 = all_173_5 % 61.28/9.64 | % 61.28/9.64 | SIMP: (453) implies: % 61.28/9.64 | (454) all_189_8 = all_173_5 % 61.28/9.64 | % 61.28/9.64 | COMBINE_EQS: (446), (448) imply: % 61.28/9.64 | (455) all_173_5 = all_166_1 % 61.28/9.64 | % 61.28/9.64 | COMBINE_EQS: (446), (447) imply: % 61.28/9.64 | (456) all_173_5 = all_171_6 % 61.28/9.64 | % 61.28/9.64 | COMBINE_EQS: (444), (452) imply: % 61.28/9.64 | (457) all_187_8 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (457) implies: % 61.28/9.65 | (458) all_187_8 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (442), (443) imply: % 61.28/9.65 | (459) all_175_1 = all_169_4 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (442), (454) imply: % 61.28/9.65 | (460) all_175_1 = all_173_5 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (441), (458) imply: % 61.28/9.65 | (461) all_171_6 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (461) implies: % 61.28/9.65 | (462) all_171_6 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (438), (439) imply: % 61.28/9.65 | (463) all_164_6 = all_160_5 % 61.28/9.65 | % 61.28/9.65 | SIMP: (463) implies: % 61.28/9.65 | (464) all_164_6 = all_160_5 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (439), (440) imply: % 61.28/9.65 | (465) all_160_5 = all_148_1 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (459), (460) imply: % 61.28/9.65 | (466) all_173_5 = all_169_4 % 61.28/9.65 | % 61.28/9.65 | SIMP: (466) implies: % 61.28/9.65 | (467) all_173_5 = all_169_4 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (456), (467) imply: % 61.28/9.65 | (468) all_171_6 = all_169_4 % 61.28/9.65 | % 61.28/9.65 | SIMP: (468) implies: % 61.28/9.65 | (469) all_171_6 = all_169_4 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (455), (467) imply: % 61.28/9.65 | (470) all_169_4 = all_166_1 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (462), (469) imply: % 61.28/9.65 | (471) all_169_4 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (471) implies: % 61.28/9.65 | (472) all_169_4 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (470), (472) imply: % 61.28/9.65 | (473) all_166_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (473) implies: % 61.28/9.65 | (474) all_166_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (437), (474) imply: % 61.28/9.65 | (475) all_164_6 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (475) implies: % 61.28/9.65 | (476) all_164_6 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (436), (476) imply: % 61.28/9.65 | (477) all_162_5 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (436), (464) imply: % 61.28/9.65 | (478) all_162_5 = all_160_5 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (477), (478) imply: % 61.28/9.65 | (479) all_160_5 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (479) implies: % 61.28/9.65 | (480) all_160_5 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (465), (480) imply: % 61.28/9.65 | (481) all_148_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (481) implies: % 61.28/9.65 | (482) all_148_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (435), (482) imply: % 61.28/9.65 | (483) all_139_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (483) implies: % 61.28/9.65 | (484) all_139_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (434), (484) imply: % 61.28/9.65 | (485) all_133_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | SIMP: (485) implies: % 61.28/9.65 | (486) all_133_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (467), (472) imply: % 61.28/9.65 | (487) all_173_5 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (459), (472) imply: % 61.28/9.65 | (488) all_175_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (439), (480) imply: % 61.28/9.65 | (489) all_184_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (442), (488) imply: % 61.28/9.65 | (490) all_189_8 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | COMBINE_EQS: (446), (487) imply: % 61.28/9.65 | (491) all_193_1 = all_122_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (226), (450) imply: % 61.28/9.65 | (492) number_number_of(nat, all_122_0) = all_196_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (222), (491) imply: % 61.28/9.65 | (493) number_number_of(nat, all_122_0) = all_193_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (217), (452) imply: % 61.28/9.65 | (494) number_number_of(nat, all_122_0) = all_191_7 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (194), (458) imply: % 61.28/9.65 | (495) number_number_of(nat, all_122_0) = all_187_7 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (183), (489) imply: % 61.28/9.65 | (496) number_number_of(nat, all_122_0) = all_184_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (175), (488) imply: % 61.28/9.65 | (497) number_number_of(nat, all_122_0) = all_175_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (153), (472) imply: % 61.28/9.65 | (498) number_number_of(nat, all_122_0) = all_169_3 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (146), (474) imply: % 61.28/9.65 | (499) number_number_of(nat, all_122_0) = all_166_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (140), (476) imply: % 61.28/9.65 | (500) number_number_of(nat, all_122_0) = all_164_5 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (111), (482) imply: % 61.28/9.65 | (501) number_number_of(nat, all_122_0) = all_148_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (103), (484) imply: % 61.28/9.65 | (502) number_number_of(nat, all_122_0) = all_139_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (96), (486) imply: % 61.28/9.65 | (503) number_number_of(nat, all_122_0) = all_133_0 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (214), (452) imply: % 61.28/9.65 | (504) bit0(all_122_0) = all_191_3 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (204), (490) imply: % 61.28/9.65 | (505) bit0(all_122_0) = all_189_7 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (191), (458) imply: % 61.28/9.65 | (506) bit0(all_122_0) = all_187_3 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (169), (487) imply: % 61.28/9.65 | (507) bit0(all_122_0) = all_173_4 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (160), (462) imply: % 61.28/9.65 | (508) bit0(all_122_0) = all_171_5 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (130), (477) imply: % 61.28/9.65 | (509) bit0(all_122_0) = all_162_4 % 61.28/9.65 | % 61.28/9.65 | REDUCE: (121), (480) imply: % 61.28/9.65 | (510) bit0(all_122_0) = all_160_4 % 61.28/9.65 | % 61.28/9.65 | GROUND_INST: instantiating (52) with all_171_5, all_173_4, all_122_0, % 61.28/9.65 | simplifying with (507), (508) gives: % 61.28/9.65 | (511) all_173_4 = all_171_5 % 61.28/9.65 | % 61.28/9.65 | GROUND_INST: instantiating (52) with all_173_4, all_187_3, all_122_0, % 61.28/9.65 | simplifying with (506), (507) gives: % 61.28/9.65 | (512) all_187_3 = all_173_4 % 61.28/9.65 | % 61.28/9.65 | GROUND_INST: instantiating (52) with all_160_4, all_187_3, all_122_0, % 61.28/9.65 | simplifying with (506), (510) gives: % 61.28/9.65 | (513) all_187_3 = all_160_4 % 61.28/9.65 | % 61.28/9.65 | GROUND_INST: instantiating (52) with all_171_5, all_189_7, all_122_0, % 61.28/9.65 | simplifying with (505), (508) gives: % 61.28/9.65 | (514) all_189_7 = all_171_5 % 61.28/9.65 | % 61.28/9.65 | GROUND_INST: instantiating (52) with all_189_7, all_191_3, all_122_0, % 61.28/9.66 | simplifying with (504), (505) gives: % 61.28/9.66 | (515) all_191_3 = all_189_7 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (52) with all_162_4, all_191_3, all_122_0, % 61.28/9.66 | simplifying with (504), (509) gives: % 61.28/9.66 | (516) all_191_3 = all_162_4 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_166_0, all_169_3, all_122_0, nat, % 61.28/9.66 | simplifying with (498), (499) gives: % 61.28/9.66 | (517) all_169_3 = all_166_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_164_5, all_169_3, all_122_0, nat, % 61.28/9.66 | simplifying with (498), (500) gives: % 61.28/9.66 | (518) all_169_3 = all_164_5 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_139_0, all_169_3, all_122_0, nat, % 61.28/9.66 | simplifying with (498), (502) gives: % 61.28/9.66 | (519) all_169_3 = all_139_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_184_0, all_187_7, all_122_0, nat, % 61.28/9.66 | simplifying with (495), (496) gives: % 61.28/9.66 | (520) all_187_7 = all_184_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_175_0, all_187_7, all_122_0, nat, % 61.28/9.66 | simplifying with (495), (497) gives: % 61.28/9.66 | (521) all_187_7 = all_175_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_169_3, all_187_7, all_122_0, nat, % 61.28/9.66 | simplifying with (495), (498) gives: % 61.28/9.66 | (522) all_187_7 = all_169_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_169_3, all_191_7, all_122_0, nat, % 61.28/9.66 | simplifying with (494), (498) gives: % 61.28/9.66 | (523) all_191_7 = all_169_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_148_0, all_191_7, all_122_0, nat, % 61.28/9.66 | simplifying with (494), (501) gives: % 61.28/9.66 | (524) all_191_7 = all_148_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_122_2, all_193_0, all_122_0, nat, % 61.28/9.66 | simplifying with (89), (493) gives: % 61.28/9.66 | (525) all_193_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_139_0, all_193_0, all_122_0, nat, % 61.28/9.66 | simplifying with (493), (502) gives: % 61.28/9.66 | (526) all_193_0 = all_139_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_184_0, all_196_0, all_122_0, nat, % 61.28/9.66 | simplifying with (492), (496) gives: % 61.28/9.66 | (527) all_196_0 = all_184_0 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_133_0, all_196_0, all_122_0, nat, % 61.28/9.66 | simplifying with (492), (503) gives: % 61.28/9.66 | (528) all_196_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (527), (528) imply: % 61.28/9.66 | (529) all_184_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (529) implies: % 61.28/9.66 | (530) all_184_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (525), (526) imply: % 61.28/9.66 | (531) all_139_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | SIMP: (531) implies: % 61.28/9.66 | (532) all_139_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (515), (516) imply: % 61.28/9.66 | (533) all_189_7 = all_162_4 % 61.28/9.66 | % 61.28/9.66 | SIMP: (533) implies: % 61.28/9.66 | (534) all_189_7 = all_162_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (523), (524) imply: % 61.28/9.66 | (535) all_169_3 = all_148_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (535) implies: % 61.28/9.66 | (536) all_169_3 = all_148_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (514), (534) imply: % 61.28/9.66 | (537) all_171_5 = all_162_4 % 61.28/9.66 | % 61.28/9.66 | SIMP: (537) implies: % 61.28/9.66 | (538) all_171_5 = all_162_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (512), (513) imply: % 61.28/9.66 | (539) all_173_4 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | SIMP: (539) implies: % 61.28/9.66 | (540) all_173_4 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (520), (521) imply: % 61.28/9.66 | (541) all_184_0 = all_175_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (541) implies: % 61.28/9.66 | (542) all_184_0 = all_175_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (521), (522) imply: % 61.28/9.66 | (543) all_175_0 = all_169_3 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (530), (542) imply: % 61.28/9.66 | (544) all_175_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (544) implies: % 61.28/9.66 | (545) all_175_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (543), (545) imply: % 61.28/9.66 | (546) all_169_3 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (546) implies: % 61.28/9.66 | (547) all_169_3 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (511), (540) imply: % 61.28/9.66 | (548) all_171_5 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | SIMP: (548) implies: % 61.28/9.66 | (549) all_171_5 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (538), (549) imply: % 61.28/9.66 | (550) all_162_4 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (517), (536) imply: % 61.28/9.66 | (551) all_166_0 = all_148_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (517), (518) imply: % 61.28/9.66 | (552) all_166_0 = all_164_5 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (517), (547) imply: % 61.28/9.66 | (553) all_166_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (517), (519) imply: % 61.28/9.66 | (554) all_166_0 = all_139_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (552), (554) imply: % 61.28/9.66 | (555) all_164_5 = all_139_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (551), (552) imply: % 61.28/9.66 | (556) all_164_5 = all_148_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (552), (553) imply: % 61.28/9.66 | (557) all_164_5 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (555), (556) imply: % 61.28/9.66 | (558) all_148_0 = all_139_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (556), (557) imply: % 61.28/9.66 | (559) all_148_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (558), (559) imply: % 61.28/9.66 | (560) all_139_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | SIMP: (560) implies: % 61.28/9.66 | (561) all_139_0 = all_133_0 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (532), (561) imply: % 61.28/9.66 | (562) all_133_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | SIMP: (562) implies: % 61.28/9.66 | (563) all_133_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (559), (563) imply: % 61.28/9.66 | (564) all_148_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (556), (564) imply: % 61.28/9.66 | (565) all_164_5 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (552), (565) imply: % 61.28/9.66 | (566) all_166_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (517), (566) imply: % 61.28/9.66 | (567) all_169_3 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (545), (563) imply: % 61.28/9.66 | (568) all_175_0 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (521), (568) imply: % 61.28/9.66 | (569) all_187_7 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (534), (550) imply: % 61.28/9.66 | (570) all_189_7 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (524), (564) imply: % 61.28/9.66 | (571) all_191_7 = all_122_2 % 61.28/9.66 | % 61.28/9.66 | COMBINE_EQS: (516), (550) imply: % 61.28/9.66 | (572) all_191_3 = all_160_4 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (218), (571) imply: % 61.28/9.66 | (573) power_power(int, s, all_122_2) = all_191_6 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (195), (569) imply: % 61.28/9.66 | (574) power_power(int, s, all_122_2) = all_187_6 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (154), (567) imply: % 61.28/9.66 | (575) power_power(int, s, all_122_2) = all_169_2 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (142), (565) imply: % 61.28/9.66 | (576) power_power(int, s, all_122_2) = all_164_4 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (216), (572) imply: % 61.28/9.66 | (577) number_number_of(int, all_160_4) = all_191_2 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (206), (570) imply: % 61.28/9.66 | (578) number_number_of(int, all_160_4) = all_189_6 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (193), (513) imply: % 61.28/9.66 | (579) number_number_of(int, all_160_4) = all_187_2 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (171), (540) imply: % 61.28/9.66 | (580) number_number_of(int, all_160_4) = all_173_3 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (162), (549) imply: % 61.28/9.66 | (581) number_number_of(int, all_160_4) = all_171_4 % 61.28/9.66 | % 61.28/9.66 | REDUCE: (132), (550) imply: % 61.28/9.66 | (582) number_number_of(int, all_160_4) = all_162_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_160_3, all_173_3, all_160_4, int, % 61.28/9.66 | simplifying with (123), (580) gives: % 61.28/9.66 | (583) all_173_3 = all_160_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_173_3, all_187_2, all_160_4, int, % 61.28/9.66 | simplifying with (579), (580) gives: % 61.28/9.66 | (584) all_187_2 = all_173_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_162_3, all_187_2, all_160_4, int, % 61.28/9.66 | simplifying with (579), (582) gives: % 61.28/9.66 | (585) all_187_2 = all_162_3 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_187_2, all_189_6, all_160_4, int, % 61.28/9.66 | simplifying with (578), (579) gives: % 61.28/9.66 | (586) all_189_6 = all_187_2 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_189_6, all_191_2, all_160_4, int, % 61.28/9.66 | simplifying with (577), (578) gives: % 61.28/9.66 | (587) all_191_2 = all_189_6 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (54) with all_171_4, all_191_2, all_160_4, int, % 61.28/9.66 | simplifying with (577), (581) gives: % 61.28/9.66 | (588) all_191_2 = all_171_4 % 61.28/9.66 | % 61.28/9.66 | GROUND_INST: instantiating (59) with all_164_4, all_187_6, all_122_2, s, int, % 61.28/9.66 | simplifying with (574), (576) gives: % 61.28/9.67 | (589) all_187_6 = all_164_4 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (59) with all_187_6, all_191_6, all_122_2, s, int, % 61.28/9.67 | simplifying with (573), (574) gives: % 61.28/9.67 | (590) all_191_6 = all_187_6 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (59) with all_169_2, all_191_6, all_122_2, s, int, % 61.28/9.67 | simplifying with (573), (575) gives: % 61.28/9.67 | (591) all_191_6 = all_169_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (587), (588) imply: % 61.28/9.67 | (592) all_189_6 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | SIMP: (592) implies: % 61.28/9.67 | (593) all_189_6 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (590), (591) imply: % 61.28/9.67 | (594) all_187_6 = all_169_2 % 61.28/9.67 | % 61.28/9.67 | SIMP: (594) implies: % 61.28/9.67 | (595) all_187_6 = all_169_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (586), (593) imply: % 61.28/9.67 | (596) all_187_2 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | SIMP: (596) implies: % 61.28/9.67 | (597) all_187_2 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (585), (597) imply: % 61.28/9.67 | (598) all_171_4 = all_162_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (584), (597) imply: % 61.28/9.67 | (599) all_173_3 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | SIMP: (599) implies: % 61.28/9.67 | (600) all_173_3 = all_171_4 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (589), (595) imply: % 61.28/9.67 | (601) all_169_2 = all_164_4 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (583), (600) imply: % 61.28/9.67 | (602) all_171_4 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | SIMP: (602) implies: % 61.28/9.67 | (603) all_171_4 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (598), (603) imply: % 61.28/9.67 | (604) all_162_3 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (597), (603) imply: % 61.28/9.67 | (605) all_187_2 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (593), (603) imply: % 61.28/9.67 | (606) all_189_6 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (591), (601) imply: % 61.28/9.67 | (607) all_191_6 = all_164_4 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (588), (603) imply: % 61.28/9.67 | (608) all_191_2 = all_160_3 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (212), (608) imply: % 61.28/9.67 | (609) times_times(int, all_160_3, m) = all_191_1 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (199), (606) imply: % 61.28/9.67 | (610) times_times(int, all_160_3, m) = all_189_5 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (188), (605) imply: % 61.28/9.67 | (611) times_times(int, all_160_3, m) = all_187_1 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (166), (583) imply: % 61.28/9.67 | (612) times_times(int, all_160_3, m) = all_173_2 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (158), (603) imply: % 61.28/9.67 | (613) times_times(int, all_160_3, m) = all_171_3 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (128), (604) imply: % 61.28/9.67 | (614) times_times(int, all_160_3, m) = all_162_2 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (422), (607) imply: % 61.28/9.67 | (615) plus_plus(int, all_164_4, all_105_0) = all_191_4 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (425), (589) imply: % 61.28/9.67 | (616) plus_plus(int, all_164_4, all_105_0) = all_187_4 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (428), (601) imply: % 61.28/9.67 | (617) plus_plus(int, all_164_4, all_105_0) = all_169_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_164_2, all_187_4, all_105_0, % 61.28/9.67 | all_164_4, int, simplifying with (429), (616) gives: % 61.28/9.67 | (618) all_187_4 = all_164_2 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_187_4, all_191_4, all_105_0, % 61.28/9.67 | all_164_4, int, simplifying with (615), (616) gives: % 61.28/9.67 | (619) all_191_4 = all_187_4 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_169_0, all_191_4, all_105_0, % 61.28/9.67 | all_164_4, int, simplifying with (615), (617) gives: % 61.28/9.67 | (620) all_191_4 = all_169_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_173_2, all_187_1, m, all_160_3, int, % 61.28/9.67 | simplifying with (611), (612) gives: % 61.28/9.67 | (621) all_187_1 = all_173_2 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_160_2, all_189_5, m, all_160_3, int, % 61.28/9.67 | simplifying with (119), (610) gives: % 61.28/9.67 | (622) all_189_5 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_173_2, all_189_5, m, all_160_3, int, % 61.28/9.67 | simplifying with (610), (612) gives: % 61.28/9.67 | (623) all_189_5 = all_173_2 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_171_3, all_189_5, m, all_160_3, int, % 61.28/9.67 | simplifying with (610), (613) gives: % 61.28/9.67 | (624) all_189_5 = all_171_3 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_187_1, all_191_1, m, all_160_3, int, % 61.28/9.67 | simplifying with (609), (611) gives: % 61.28/9.67 | (625) all_191_1 = all_187_1 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (56) with all_162_2, all_191_1, m, all_160_3, int, % 61.28/9.67 | simplifying with (609), (614) gives: % 61.28/9.67 | (626) all_191_1 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (625), (626) imply: % 61.28/9.67 | (627) all_187_1 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | SIMP: (627) implies: % 61.28/9.67 | (628) all_187_1 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (619), (620) imply: % 61.28/9.67 | (629) all_187_4 = all_169_0 % 61.28/9.67 | % 61.28/9.67 | SIMP: (629) implies: % 61.28/9.67 | (630) all_187_4 = all_169_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (623), (624) imply: % 61.28/9.67 | (631) all_173_2 = all_171_3 % 61.28/9.67 | % 61.28/9.67 | SIMP: (631) implies: % 61.28/9.67 | (632) all_173_2 = all_171_3 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (622), (624) imply: % 61.28/9.67 | (633) all_171_3 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (621), (628) imply: % 61.28/9.67 | (634) all_173_2 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | SIMP: (634) implies: % 61.28/9.67 | (635) all_173_2 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (618), (630) imply: % 61.28/9.67 | (636) all_169_0 = all_164_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (632), (635) imply: % 61.28/9.67 | (637) all_171_3 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | SIMP: (637) implies: % 61.28/9.67 | (638) all_171_3 = all_162_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (633), (638) imply: % 61.28/9.67 | (639) all_162_2 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | SIMP: (639) implies: % 61.28/9.67 | (640) all_162_2 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (635), (640) imply: % 61.28/9.67 | (641) all_173_2 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (628), (640) imply: % 61.28/9.67 | (642) all_187_1 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (626), (640) imply: % 61.28/9.67 | (643) all_191_1 = all_160_2 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (189), (618) imply: % 61.28/9.67 | (644) times_times(int, all_187_0, t) = all_164_2 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (421), (643) imply: % 61.28/9.67 | (645) plus_plus(int, all_160_2, all_105_0) = all_191_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (423), (622) imply: % 61.28/9.67 | (646) plus_plus(int, all_160_2, all_105_0) = all_189_3 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (424), (642) imply: % 61.28/9.67 | (647) plus_plus(int, all_160_2, all_105_0) = all_187_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (426), (641) imply: % 61.28/9.67 | (648) plus_plus(int, all_160_2, all_105_0) = all_173_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (427), (633) imply: % 61.28/9.67 | (649) plus_plus(int, all_160_2, all_105_0) = all_171_1 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (430), (640) imply: % 61.28/9.67 | (650) plus_plus(int, all_160_2, all_105_0) = all_162_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (125), (640) imply: % 61.28/9.67 | (651) $i(all_160_2) % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_160_0, all_187_0, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (431), (647) gives: % 61.28/9.67 | (652) all_187_0 = all_160_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_187_0, all_189_3, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (646), (647) gives: % 61.28/9.67 | (653) all_189_3 = all_187_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_173_0, all_189_3, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (646), (648) gives: % 61.28/9.67 | (654) all_189_3 = all_173_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_171_1, all_189_3, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (646), (649) gives: % 61.28/9.67 | (655) all_189_3 = all_171_1 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_173_0, all_191_0, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (645), (648) gives: % 61.28/9.67 | (656) all_191_0 = all_173_0 % 61.28/9.67 | % 61.28/9.67 | GROUND_INST: instantiating (55) with all_162_0, all_191_0, all_105_0, % 61.28/9.67 | all_160_2, int, simplifying with (645), (650) gives: % 61.28/9.67 | (657) all_191_0 = all_162_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (656), (657) imply: % 61.28/9.67 | (658) all_173_0 = all_162_0 % 61.28/9.67 | % 61.28/9.67 | SIMP: (658) implies: % 61.28/9.67 | (659) all_173_0 = all_162_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (654), (655) imply: % 61.28/9.67 | (660) all_173_0 = all_171_1 % 61.28/9.67 | % 61.28/9.67 | SIMP: (660) implies: % 61.28/9.67 | (661) all_173_0 = all_171_1 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (653), (655) imply: % 61.28/9.67 | (662) all_187_0 = all_171_1 % 61.28/9.67 | % 61.28/9.67 | SIMP: (662) implies: % 61.28/9.67 | (663) all_187_0 = all_171_1 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (652), (663) imply: % 61.28/9.67 | (664) all_171_1 = all_160_0 % 61.28/9.67 | % 61.28/9.67 | SIMP: (664) implies: % 61.28/9.67 | (665) all_171_1 = all_160_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (659), (661) imply: % 61.28/9.67 | (666) all_171_1 = all_162_0 % 61.28/9.67 | % 61.28/9.67 | SIMP: (666) implies: % 61.28/9.67 | (667) all_171_1 = all_162_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (665), (667) imply: % 61.28/9.67 | (668) all_162_0 = all_160_0 % 61.28/9.67 | % 61.28/9.67 | COMBINE_EQS: (655), (665) imply: % 61.28/9.67 | (669) all_189_3 = all_160_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (419), (669) imply: % 61.28/9.67 | (670) times_times(int, all_160_0, all_97_0) = all_189_0 % 61.28/9.67 | % 61.28/9.67 | REDUCE: (200), (669) imply: % 61.28/9.67 | (671) times_times(int, all_160_0, t) = all_189_2 % 61.28/9.68 | % 61.28/9.68 | REDUCE: (644), (652) imply: % 61.28/9.68 | (672) times_times(int, all_160_0, t) = all_164_2 % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (56) with all_164_2, all_189_2, t, all_160_0, int, % 61.28/9.68 | simplifying with (671), (672) gives: % 61.28/9.68 | (673) all_189_2 = all_164_2 % 61.28/9.68 | % 61.28/9.68 | REDUCE: (207), (673) imply: % 61.28/9.68 | (674) ord_less(int, all_164_2, all_189_0) = 0 % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (41) with all_160_2, all_105_0, all_160_0, % 61.28/9.68 | simplifying with (431), (432), (651) gives: % 61.28/9.68 | (675) plus_plus(int, all_105_0, all_160_2) = all_160_0 & $i(all_160_0) % 61.28/9.68 | % 61.28/9.68 | ALPHA: (675) implies: % 61.28/9.68 | (676) $i(all_160_0) % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (24) with all_160_0, all_97_0, all_189_0, % 61.28/9.68 | simplifying with (433), (670), (676) gives: % 61.28/9.68 | (677) times_times(int, all_97_0, all_160_0) = all_189_0 & $i(all_189_0) % 61.28/9.68 | % 61.28/9.68 | ALPHA: (677) implies: % 61.28/9.68 | (678) times_times(int, all_97_0, all_160_0) = all_189_0 % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (1) with pls, all_109_0, simplifying with (46), % 61.28/9.68 | (73) gives: % 61.28/9.68 | (679) ti(int, all_109_0) = all_109_0 & $i(all_109_0) % 61.28/9.68 | % 61.28/9.68 | ALPHA: (679) implies: % 61.28/9.68 | (680) $i(all_109_0) % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (23) with pls, all_97_0, simplifying with (46), % 61.28/9.68 | (62) gives: % 61.28/9.68 | (681) all_97_0 = pls % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (fact_50_le__number__of__eq__not__less) with nat, % 61.28/9.68 | simplifying with (44), (47) gives: % 61.28/9.68 | (682) ? [v0: int] : ( ~ (v0 = 0) & number(nat) = v0) | ( ! [v0: $i] : ! % 61.28/9.68 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 61.28/9.68 | (ord_less(nat, v2, v3) = v4) | ~ (number_number_of(nat, v1) = % 61.28/9.68 | v2) | ~ (number_number_of(nat, v0) = v3) | ~ $i(v1) | ~ % 61.28/9.68 | $i(v0) | ord_less_eq(nat, v3, v2) = 0) & ! [v0: $i] : ! [v1: % 61.28/9.68 | $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (ord_less(nat, v3, v2) = 0) % 61.28/9.68 | | ~ (number_number_of(nat, v1) = v3) | ~ (number_number_of(nat, % 61.28/9.68 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = % 61.28/9.68 | 0) & ord_less_eq(nat, v2, v3) = v4))) % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (26) with pls, simplifying with (25), (46) gives: % 61.28/9.68 | (683) ? [v0: $i] : (ord_less_eq(int, pls, v0) = 0 & bit1(pls) = v0 & % 61.28/9.68 | $i(v0)) % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (39) with nat, simplifying with (43), (47) gives: % 61.28/9.68 | (684) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 61.28/9.68 | ( ~ (number_number_of(nat, v1) = v2) | ~ (number_number_of(nat, v0) % 61.28/9.68 | = v3) | ~ (plus_plus(nat, v2, v3) = v4) | ~ $i(v1) | ~ $i(v0) % 61.28/9.68 | | ? [v5: any] : ? [v6: any] : ? [v7: $i] : ? [v8: $i] : % 61.28/9.68 | (ord_less_eq(int, pls, v1) = v5 & ord_less_eq(int, pls, v0) = v6 & % 61.28/9.68 | number_number_of(nat, v7) = v8 & plus_plus(int, v1, v0) = v7 & % 61.28/9.68 | $i(v8) & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | v8 = v4))) % 61.28/9.68 | % 61.28/9.68 | GROUND_INST: instantiating (684) with all_109_0, all_109_0, all_109_1, % 61.28/9.68 | all_109_1, all_122_2, simplifying with (400), (420), (680) gives: % 61.28/9.68 | (685) ? [v0: any] : ? [v1: any] : ? [v2: $i] : ? [v3: $i] : % 61.28/9.68 | (ord_less_eq(int, pls, all_109_0) = v1 & ord_less_eq(int, pls, % 61.28/9.68 | all_109_0) = v0 & number_number_of(nat, v2) = v3 & plus_plus(int, % 61.28/9.68 | all_109_0, all_109_0) = v2 & $i(v3) & $i(v2) & ( ~ (v1 = 0) | ~ % 61.28/9.68 | (v0 = 0) | v3 = all_122_2)) % 61.28/9.68 | % 61.28/9.68 | DELTA: instantiating (683) with fresh symbol all_257_0 gives: % 61.28/9.68 | (686) ord_less_eq(int, pls, all_257_0) = 0 & bit1(pls) = all_257_0 & % 61.28/9.68 | $i(all_257_0) % 61.28/9.68 | % 61.28/9.68 | ALPHA: (686) implies: % 61.28/9.68 | (687) bit1(pls) = all_257_0 % 61.28/9.68 | (688) ord_less_eq(int, pls, all_257_0) = 0 % 61.28/9.68 | % 61.28/9.68 | DELTA: instantiating (685) with fresh symbols all_299_0, all_299_1, all_299_2, % 61.28/9.68 | all_299_3 gives: % 61.28/9.68 | (689) ord_less_eq(int, pls, all_109_0) = all_299_2 & ord_less_eq(int, pls, % 61.28/9.68 | all_109_0) = all_299_3 & number_number_of(nat, all_299_1) = % 61.28/9.68 | all_299_0 & plus_plus(int, all_109_0, all_109_0) = all_299_1 & % 61.28/9.68 | $i(all_299_0) & $i(all_299_1) & ( ~ (all_299_2 = 0) | ~ (all_299_3 = % 61.28/9.68 | 0) | all_299_0 = all_122_2) % 61.28/9.68 | % 61.28/9.68 | ALPHA: (689) implies: % 61.28/9.68 | (690) ord_less_eq(int, pls, all_109_0) = all_299_3 % 61.28/9.68 | (691) ord_less_eq(int, pls, all_109_0) = all_299_2 % 61.28/9.68 | (692) ~ (all_299_2 = 0) | ~ (all_299_3 = 0) | all_299_0 = all_122_2 % 61.28/9.68 | % 61.28/9.68 | REDUCE: (399), (681) imply: % 61.28/9.68 | (693) ord_less(int, all_164_2, pls) = all_164_0 % 61.28/9.68 | % 61.28/9.68 | REDUCE: (678), (681) imply: % 61.28/9.68 | (694) times_times(int, pls, all_160_0) = all_189_0 % 61.28/9.68 | % 61.28/9.68 | BETA: splitting (682) gives: % 61.28/9.68 | % 61.28/9.68 | Case 1: % 61.28/9.68 | | % 61.28/9.68 | | (695) ? [v0: int] : ( ~ (v0 = 0) & number(nat) = v0) % 61.28/9.68 | | % 61.28/9.68 | | DELTA: instantiating (695) with fresh symbol all_338_0 gives: % 61.28/9.68 | | (696) ~ (all_338_0 = 0) & number(nat) = all_338_0 % 61.28/9.68 | | % 61.28/9.68 | | ALPHA: (696) implies: % 61.28/9.68 | | (697) ~ (all_338_0 = 0) % 61.28/9.68 | | (698) number(nat) = all_338_0 % 61.28/9.68 | | % 61.28/9.68 | | DELTA: instantiating (695) with fresh symbol all_340_0 gives: % 61.28/9.68 | | (699) ~ (all_340_0 = 0) & number(nat) = all_340_0 % 61.28/9.68 | | % 61.28/9.68 | | ALPHA: (699) implies: % 61.28/9.68 | | (700) number(nat) = all_340_0 % 61.28/9.68 | | % 61.28/9.68 | | GROUND_INST: instantiating (50) with 0, all_340_0, nat, simplifying with % 61.28/9.68 | | (45), (700) gives: % 61.28/9.68 | | (701) all_340_0 = 0 % 61.28/9.68 | | % 61.28/9.68 | | GROUND_INST: instantiating (50) with all_338_0, all_340_0, nat, simplifying % 61.28/9.68 | | with (698), (700) gives: % 61.28/9.68 | | (702) all_340_0 = all_338_0 % 61.28/9.68 | | % 61.28/9.68 | | COMBINE_EQS: (701), (702) imply: % 61.28/9.68 | | (703) all_338_0 = 0 % 61.28/9.68 | | % 61.28/9.68 | | REDUCE: (697), (703) imply: % 61.28/9.68 | | (704) $false % 61.28/9.68 | | % 61.28/9.68 | | CLOSE: (704) is inconsistent. % 61.28/9.68 | | % 61.28/9.69 | Case 2: % 61.28/9.69 | | % 61.28/9.69 | | % 61.28/9.69 | | GROUND_INST: instantiating (53) with all_109_0, all_257_0, pls, simplifying % 61.28/9.69 | | with (73), (687) gives: % 61.28/9.69 | | (705) all_257_0 = all_109_0 % 61.28/9.69 | | % 61.28/9.69 | | GROUND_INST: instantiating (58) with all_299_3, all_299_2, all_109_0, pls, % 61.28/9.69 | | int, simplifying with (690), (691) gives: % 61.28/9.69 | | (706) all_299_2 = all_299_3 % 61.28/9.69 | | % 61.28/9.69 | | REDUCE: (688), (705) imply: % 61.28/9.69 | | (707) ord_less_eq(int, pls, all_109_0) = 0 % 61.28/9.69 | | % 61.28/9.69 | | GROUND_INST: instantiating (58) with all_299_3, 0, all_109_0, pls, int, % 61.28/9.69 | | simplifying with (690), (707) gives: % 61.28/9.69 | | (708) all_299_3 = 0 % 61.28/9.69 | | % 61.28/9.69 | | COMBINE_EQS: (706), (708) imply: % 61.28/9.69 | | (709) all_299_2 = 0 % 61.28/9.69 | | % 61.28/9.69 | | BETA: splitting (692) gives: % 61.28/9.69 | | % 61.28/9.69 | | Case 1: % 61.28/9.69 | | | % 61.28/9.69 | | | (710) ~ (all_299_2 = 0) % 61.28/9.69 | | | % 61.28/9.69 | | | REDUCE: (709), (710) imply: % 61.28/9.69 | | | (711) $false % 61.28/9.69 | | | % 61.28/9.69 | | | CLOSE: (711) is inconsistent. % 61.28/9.69 | | | % 61.28/9.69 | | Case 2: % 61.28/9.69 | | | % 61.28/9.69 | | | % 61.28/9.69 | | | GROUND_INST: instantiating (30) with all_160_0, all_189_0, simplifying % 61.28/9.69 | | | with (676), (694) gives: % 61.28/9.69 | | | (712) all_189_0 = pls % 61.28/9.69 | | | % 61.28/9.69 | | | REDUCE: (674), (712) imply: % 61.28/9.69 | | | (713) ord_less(int, all_164_2, pls) = 0 % 61.28/9.69 | | | % 61.28/9.69 | | | GROUND_INST: instantiating (57) with all_164_0, 0, pls, all_164_2, int, % 61.28/9.69 | | | simplifying with (693), (713) gives: % 61.28/9.69 | | | (714) all_164_0 = 0 % 61.28/9.69 | | | % 61.28/9.69 | | | REDUCE: (134), (714) imply: % 61.28/9.69 | | | (715) $false % 61.28/9.69 | | | % 61.28/9.69 | | | CLOSE: (715) is inconsistent. % 61.28/9.69 | | | % 61.28/9.69 | | End of split % 61.28/9.69 | | % 61.28/9.69 | End of split % 61.28/9.69 | % 61.28/9.69 End of proof % 61.28/9.69 % SZS output end Proof for theBenchmark % 61.28/9.69 % 61.28/9.69 9085ms %------------------------------------------------------------------------------