%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KLE009+4 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n016.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 05:34:11 EDT 2023 % Result : Theorem 131.65s 17.69s % Output : Proof 186.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KLE009+4 : TPTP v8.1.2. Released v4.0.0. % 0.06/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n016.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Aug 29 13:01:31 EDT 2023 % 0.12/0.33 % CPUTime : % 0.47/0.59 ________ _____ % 0.47/0.59 ___ __ \_________(_)________________________________ % 0.47/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.47/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.47/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.47/0.59 % 0.47/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.47/0.59 (2023-06-19) % 0.47/0.59 % 0.47/0.59 (c) Philipp Rümmer, 2009-2023 % 0.47/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.47/0.59 Amanda Stjerna. % 0.47/0.59 Free software under BSD-3-Clause. % 0.47/0.59 % 0.47/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.47/0.59 % 0.47/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.47/0.61 Running up to 7 provers in parallel. % 0.47/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.47/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.47/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.47/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.47/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.47/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.47/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.54/1.02 Prover 4: Preprocessing ... % 2.54/1.02 Prover 1: Preprocessing ... % 2.54/1.06 Prover 6: Preprocessing ... % 2.54/1.06 Prover 3: Preprocessing ... % 2.54/1.06 Prover 5: Preprocessing ... % 2.54/1.06 Prover 2: Preprocessing ... % 2.54/1.06 Prover 0: Preprocessing ... % 5.12/1.36 Prover 1: Constructing countermodel ... % 5.22/1.37 Prover 6: Proving ... % 5.22/1.38 Prover 3: Constructing countermodel ... % 5.54/1.43 Prover 4: Constructing countermodel ... % 5.54/1.43 Prover 5: Proving ... % 5.76/1.44 Prover 0: Proving ... % 5.76/1.51 Prover 2: Proving ... % 74.54/10.29 Prover 2: stopped % 74.81/10.30 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 75.09/10.35 Prover 7: Preprocessing ... % 75.09/10.44 Prover 7: Constructing countermodel ... % 103.06/13.96 Prover 5: stopped % 103.49/13.98 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 103.49/14.01 Prover 8: Preprocessing ... % 104.41/14.11 Prover 8: Warning: ignoring some quantifiers % 104.41/14.11 Prover 8: Constructing countermodel ... % 118.87/15.97 Prover 1: stopped % 118.87/15.98 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 118.87/16.01 Prover 9: Preprocessing ... % 119.64/16.08 Prover 9: Constructing countermodel ... % 131.65/17.69 Prover 0: proved (16973ms) % 131.65/17.69 % 131.65/17.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 131.65/17.69 % 131.65/17.69 Prover 9: stopped % 131.65/17.69 Prover 3: stopped % 131.65/17.69 Prover 6: stopped % 131.65/17.69 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 131.65/17.69 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 131.65/17.69 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 131.65/17.69 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 131.65/17.72 Prover 10: Preprocessing ... % 131.65/17.72 Prover 11: Preprocessing ... % 131.65/17.72 Prover 13: Preprocessing ... % 131.65/17.73 Prover 16: Preprocessing ... % 131.65/17.75 Prover 10: Constructing countermodel ... % 132.26/17.77 Prover 13: Warning: ignoring some quantifiers % 132.26/17.77 Prover 16: Warning: ignoring some quantifiers % 132.26/17.78 Prover 16: Constructing countermodel ... % 132.26/17.78 Prover 11: Constructing countermodel ... % 132.53/17.79 Prover 13: Constructing countermodel ... % 158.53/21.28 Prover 13: stopped % 158.53/21.28 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 158.53/21.31 Prover 19: Preprocessing ... % 159.07/21.35 Prover 19: Warning: ignoring some quantifiers % 159.07/21.35 Prover 19: Constructing countermodel ... % 163.02/21.86 Prover 16: stopped % 181.37/24.42 Prover 19: stopped % 185.10/25.01 Prover 10: Found proof (size 750) % 185.10/25.01 Prover 10: proved (7319ms) % 185.10/25.01 Prover 7: stopped % 185.10/25.01 Prover 8: stopped % 185.10/25.02 Prover 11: stopped % 185.10/25.03 Prover 4: stopped % 185.10/25.03 % 185.10/25.03 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 185.10/25.03 % 185.44/25.16 % SZS output start Proof for theBenchmark % 185.44/25.17 Assumptions after simplification: % 185.44/25.17 --------------------------------- % 185.44/25.17 % 185.44/25.17 (additive_associativity) % 185.44/25.19 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 185.44/25.20 (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 185.44/25.20 | ~ $i(v0) | ? [v5: $i] : (addition(v2, v5) = v4 & addition(v1, v0) = v5 & % 185.44/25.20 $i(v5) & $i(v4))) % 185.44/25.20 % 185.44/25.20 (additive_commutativity) % 185.44/25.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | ~ % 185.44/25.20 $i(v1) | ~ $i(v0) | (addition(v1, v0) = v2 & $i(v2))) % 185.44/25.20 % 185.44/25.20 (additive_idempotence) % 185.44/25.20 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (addition(v0, v0) = v1) | ~ $i(v0)) % 185.44/25.20 % 185.44/25.20 (goals) % 185.44/25.20 $i(one) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 185.44/25.20 : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 185.44/25.20 [v10: $i] : (c(v1) = v3 & c(v0) = v6 & multiplication(v6, v3) = v9 & % 185.44/25.20 multiplication(v6, v1) = v7 & multiplication(v0, v3) = v4 & % 185.44/25.20 multiplication(v0, v1) = v2 & addition(v8, v9) = v10 & addition(v5, v7) = v8 % 185.44/25.20 & addition(v2, v4) = v5 & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 185.44/25.20 $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & test(v1) & test(v0) & % 185.44/25.20 ( ~ leq(v10, one) | ~ leq(one, v10))) % 185.44/25.20 % 185.44/25.20 (left_distributivity) % 185.44/25.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 185.44/25.20 $i] : ( ~ (multiplication(v1, v2) = v4) | ~ (multiplication(v0, v2) = v3) | % 185.44/25.20 ~ (addition(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] % 185.44/25.21 : (multiplication(v6, v2) = v5 & addition(v0, v1) = v6 & $i(v6) & $i(v5))) % 185.44/25.21 % 185.44/25.21 (multiplicative_associativity) % 185.44/25.21 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 185.44/25.21 (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ~ $i(v2) % 185.44/25.21 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (multiplication(v1, v2) = v5 & % 185.44/25.21 multiplication(v0, v5) = v4 & $i(v5) & $i(v4))) % 185.44/25.21 % 185.44/25.21 (multiplicative_left_identity) % 185.44/25.21 $i(one) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(one, v0) = % 185.44/25.21 v1) | ~ $i(v0)) % 185.44/25.21 % 185.44/25.21 (multiplicative_right_identity) % 185.44/25.21 $i(one) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(v0, one) = % 185.44/25.21 v1) | ~ $i(v0)) % 185.44/25.21 % 185.44/25.21 (order) % 185.44/25.21 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (addition(v0, v1) = % 185.44/25.21 v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v0, v1)) & ! [v0: $i] : ! [v1: $i] % 185.44/25.21 : ( ~ (addition(v0, v1) = v1) | ~ $i(v1) | ~ $i(v0) | leq(v0, v1)) % 185.44/25.21 % 185.44/25.21 (right_distributivity) % 185.44/25.21 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 185.44/25.21 $i] : ( ~ (multiplication(v0, v2) = v4) | ~ (multiplication(v0, v1) = v3) | % 185.44/25.21 ~ (addition(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] % 185.44/25.21 : (multiplication(v0, v6) = v5 & addition(v1, v2) = v6 & $i(v6) & $i(v5))) % 185.44/25.21 % 185.44/25.21 (test_2) % 185.44/25.22 $i(one) & $i(zero) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = one | ~ % 185.44/25.22 (addition(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ complement(v1, v0)) & % 185.44/25.22 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | ~ % 185.44/25.22 $i(v1) | ~ $i(v0) | ~ complement(v1, v0) | (multiplication(v1, v0) = zero % 185.44/25.22 & multiplication(v0, v1) = zero)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 185.44/25.22 (addition(v0, v1) = one) | ~ $i(v1) | ~ $i(v0) | complement(v1, v0) | ? % 185.44/25.22 [v2: $i] : ? [v3: $i] : (( ~ (v3 = zero) & multiplication(v1, v0) = v3 & % 185.44/25.22 $i(v3)) | ( ~ (v2 = zero) & multiplication(v0, v1) = v2 & $i(v2)))) % 185.44/25.22 % 185.44/25.22 (test_3) % 185.44/25.22 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (c(v0) = v2) | ~ % 185.44/25.22 $i(v1) | ~ $i(v0) | ~ complement(v0, v1) | ~ test(v0)) & ! [v0: $i] : ! % 185.44/25.22 [v1: $i] : ( ~ (c(v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ test(v0) | % 185.44/25.22 complement(v0, v1)) % 185.44/25.22 % 185.44/25.22 (test_deMorgan1) % 185.44/25.22 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 185.44/25.22 (c(v1) = v3) | ~ (c(v0) = v2) | ~ (multiplication(v2, v3) = v4) | ~ % 185.44/25.22 $i(v1) | ~ $i(v0) | ~ test(v1) | ~ test(v0) | ? [v5: $i] : (c(v5) = v4 & % 185.44/25.22 addition(v0, v1) = v5 & $i(v5) & $i(v4))) % 185.44/25.22 % 185.44/25.22 (function-axioms) % 185.44/25.23 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 185.44/25.23 (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) & ! [v0: % 185.44/25.23 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (addition(v3, % 185.44/25.23 v2) = v1) | ~ (addition(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 185.44/25.23 [v2: $i] : (v1 = v0 | ~ (c(v2) = v1) | ~ (c(v2) = v0)) % 185.44/25.23 % 185.44/25.23 Further assumptions not needed in the proof: % 185.44/25.23 -------------------------------------------- % 185.44/25.23 additive_identity, left_annihilation, right_annihilation, test_1, test_4, % 185.44/25.23 test_deMorgan2 % 185.44/25.23 % 185.44/25.23 Those formulas are unsatisfiable: % 185.44/25.23 --------------------------------- % 185.44/25.23 % 185.44/25.23 Begin of proof % 185.44/25.23 | % 185.44/25.23 | ALPHA: (multiplicative_right_identity) implies: % 185.44/25.23 | (1) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(v0, one) = % 185.44/25.23 | v1) | ~ $i(v0)) % 185.44/25.23 | % 185.44/25.23 | ALPHA: (multiplicative_left_identity) implies: % 185.44/25.23 | (2) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(one, v0) = % 185.44/25.23 | v1) | ~ $i(v0)) % 185.44/25.23 | % 185.44/25.23 | ALPHA: (order) implies: % 185.44/25.23 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (addition(v0, v1) = v1) | ~ $i(v1) | % 185.44/25.23 | ~ $i(v0) | leq(v0, v1)) % 185.44/25.23 | % 185.44/25.23 | ALPHA: (test_2) implies: % 185.44/25.23 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | % 185.44/25.23 | ~ $i(v1) | ~ $i(v0) | ~ complement(v1, v0) | (multiplication(v1, % 185.44/25.23 | v0) = zero & multiplication(v0, v1) = zero)) % 185.44/25.24 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = one | ~ (addition(v0, % 185.44/25.24 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ complement(v1, v0)) % 185.44/25.24 | % 185.44/25.24 | ALPHA: (test_3) implies: % 185.44/25.24 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (c(v0) = v1) | ~ $i(v1) | ~ $i(v0) | % 185.44/25.24 | ~ test(v0) | complement(v0, v1)) % 185.44/25.24 | % 185.44/25.24 | ALPHA: (goals) implies: % 185.44/25.24 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 185.44/25.24 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 185.44/25.24 | [v10: $i] : (c(v1) = v3 & c(v0) = v6 & multiplication(v6, v3) = v9 & % 185.44/25.24 | multiplication(v6, v1) = v7 & multiplication(v0, v3) = v4 & % 185.44/25.24 | multiplication(v0, v1) = v2 & addition(v8, v9) = v10 & addition(v5, % 185.44/25.24 | v7) = v8 & addition(v2, v4) = v5 & $i(v10) & $i(v9) & $i(v8) & % 185.44/25.24 | $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) % 185.44/25.24 | & test(v1) & test(v0) & ( ~ leq(v10, one) | ~ leq(one, v10))) % 185.44/25.24 | % 185.44/25.24 | ALPHA: (function-axioms) implies: % 185.44/25.24 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 185.44/25.24 | (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 185.44/25.24 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 185.44/25.24 | (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) % 185.44/25.24 | % 185.44/25.24 | DELTA: instantiating (7) with fresh symbols all_22_0, all_22_1, all_22_2, % 185.44/25.24 | all_22_3, all_22_4, all_22_5, all_22_6, all_22_7, all_22_8, all_22_9, % 185.44/25.24 | all_22_10 gives: % 185.44/25.25 | (10) c(all_22_9) = all_22_7 & c(all_22_10) = all_22_4 & % 185.44/25.25 | multiplication(all_22_4, all_22_7) = all_22_1 & % 185.44/25.25 | multiplication(all_22_4, all_22_9) = all_22_3 & % 185.44/25.25 | multiplication(all_22_10, all_22_7) = all_22_6 & % 185.44/25.25 | multiplication(all_22_10, all_22_9) = all_22_8 & addition(all_22_2, % 185.44/25.25 | all_22_1) = all_22_0 & addition(all_22_5, all_22_3) = all_22_2 & % 185.44/25.25 | addition(all_22_8, all_22_6) = all_22_5 & $i(all_22_0) & $i(all_22_1) % 185.44/25.25 | & $i(all_22_2) & $i(all_22_3) & $i(all_22_4) & $i(all_22_5) & % 185.44/25.25 | $i(all_22_6) & $i(all_22_7) & $i(all_22_8) & $i(all_22_9) & % 185.44/25.25 | $i(all_22_10) & test(all_22_9) & test(all_22_10) & ( ~ leq(all_22_0, % 185.44/25.25 | one) | ~ leq(one, all_22_0)) % 185.44/25.25 | % 185.44/25.25 | ALPHA: (10) implies: % 185.44/25.25 | (11) test(all_22_10) % 185.44/25.25 | (12) test(all_22_9) % 185.44/25.25 | (13) $i(all_22_10) % 185.44/25.25 | (14) $i(all_22_9) % 185.44/25.25 | (15) $i(all_22_8) % 185.44/25.25 | (16) $i(all_22_7) % 185.44/25.25 | (17) $i(all_22_6) % 185.44/25.25 | (18) $i(all_22_4) % 185.44/25.25 | (19) $i(all_22_3) % 185.44/25.25 | (20) $i(all_22_1) % 185.44/25.25 | (21) addition(all_22_8, all_22_6) = all_22_5 % 185.44/25.25 | (22) addition(all_22_5, all_22_3) = all_22_2 % 185.44/25.25 | (23) addition(all_22_2, all_22_1) = all_22_0 % 185.44/25.25 | (24) multiplication(all_22_10, all_22_9) = all_22_8 % 185.44/25.25 | (25) multiplication(all_22_10, all_22_7) = all_22_6 % 185.44/25.25 | (26) multiplication(all_22_4, all_22_9) = all_22_3 % 185.44/25.25 | (27) multiplication(all_22_4, all_22_7) = all_22_1 % 185.44/25.25 | (28) c(all_22_10) = all_22_4 % 185.44/25.25 | (29) c(all_22_9) = all_22_7 % 185.44/25.25 | (30) ~ leq(all_22_0, one) | ~ leq(one, all_22_0) % 185.44/25.25 | % 185.44/25.25 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_22_6, % 185.44/25.25 | all_22_5, simplifying with (15), (17), (21) gives: % 185.44/25.25 | (31) addition(all_22_6, all_22_8) = all_22_5 & $i(all_22_5) % 185.44/25.25 | % 185.44/25.25 | ALPHA: (31) implies: % 185.44/25.25 | (32) $i(all_22_5) % 185.44/25.25 | (33) addition(all_22_6, all_22_8) = all_22_5 % 185.44/25.25 | % 185.44/25.25 | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_22_6, % 185.44/25.25 | all_22_8, all_22_5, all_22_2, simplifying with (15), (17), (19), % 185.44/25.25 | (21), (22) gives: % 185.44/25.26 | (34) ? [v0: $i] : (addition(all_22_6, all_22_3) = v0 & addition(all_22_8, % 185.44/25.26 | v0) = all_22_2 & $i(v0) & $i(all_22_2)) % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (additive_commutativity) with all_22_5, all_22_3, % 185.44/25.26 | all_22_2, simplifying with (19), (22), (32) gives: % 185.44/25.26 | (35) addition(all_22_3, all_22_5) = all_22_2 & $i(all_22_2) % 185.44/25.26 | % 185.44/25.26 | ALPHA: (35) implies: % 185.44/25.26 | (36) addition(all_22_3, all_22_5) = all_22_2 % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_3, % 185.44/25.26 | all_22_5, all_22_2, all_22_0, simplifying with (19), (20), (22), % 185.44/25.26 | (23), (32) gives: % 185.44/25.26 | (37) ? [v0: $i] : (addition(all_22_3, all_22_1) = v0 & addition(all_22_5, % 185.44/25.26 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_22_9, % 185.44/25.26 | all_22_7, all_22_8, all_22_6, all_22_5, simplifying with (13), % 185.44/25.26 | (14), (16), (21), (24), (25) gives: % 185.44/25.26 | (38) ? [v0: $i] : (multiplication(all_22_10, v0) = all_22_5 & % 185.44/25.26 | addition(all_22_9, all_22_7) = v0 & $i(v0) & $i(all_22_5)) % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (6) with all_22_10, all_22_4, simplifying with % 185.44/25.26 | (11), (13), (18), (28) gives: % 185.44/25.26 | (39) complement(all_22_10, all_22_4) % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (test_deMorgan1) with all_22_10, all_22_9, % 185.44/25.26 | all_22_4, all_22_7, all_22_1, simplifying with (11), (12), (13), % 185.44/25.26 | (14), (27), (28), (29) gives: % 185.44/25.26 | (40) ? [v0: $i] : (c(v0) = all_22_1 & addition(all_22_10, all_22_9) = v0 & % 185.44/25.26 | $i(v0) & $i(all_22_1)) % 185.44/25.26 | % 185.44/25.26 | GROUND_INST: instantiating (6) with all_22_9, all_22_7, simplifying with (12), % 185.44/25.26 | (14), (16), (29) gives: % 185.44/25.26 | (41) complement(all_22_9, all_22_7) % 185.44/25.26 | % 185.44/25.26 | DELTA: instantiating (34) with fresh symbol all_34_0 gives: % 185.44/25.26 | (42) addition(all_22_6, all_22_3) = all_34_0 & addition(all_22_8, all_34_0) % 185.44/25.26 | = all_22_2 & $i(all_34_0) & $i(all_22_2) % 185.44/25.26 | % 185.44/25.26 | ALPHA: (42) implies: % 185.44/25.26 | (43) $i(all_34_0) % 185.44/25.26 | (44) addition(all_22_8, all_34_0) = all_22_2 % 185.44/25.26 | (45) addition(all_22_6, all_22_3) = all_34_0 % 185.44/25.26 | % 185.44/25.26 | DELTA: instantiating (40) with fresh symbol all_36_0 gives: % 185.44/25.26 | (46) c(all_36_0) = all_22_1 & addition(all_22_10, all_22_9) = all_36_0 & % 185.44/25.26 | $i(all_36_0) & $i(all_22_1) % 185.44/25.26 | % 185.44/25.26 | ALPHA: (46) implies: % 185.44/25.26 | (47) addition(all_22_10, all_22_9) = all_36_0 % 185.44/25.26 | % 185.44/25.26 | DELTA: instantiating (38) with fresh symbol all_38_0 gives: % 185.85/25.27 | (48) multiplication(all_22_10, all_38_0) = all_22_5 & addition(all_22_9, % 185.85/25.27 | all_22_7) = all_38_0 & $i(all_38_0) & $i(all_22_5) % 185.85/25.27 | % 185.85/25.27 | ALPHA: (48) implies: % 185.85/25.27 | (49) addition(all_22_9, all_22_7) = all_38_0 % 185.85/25.27 | % 185.85/25.27 | DELTA: instantiating (37) with fresh symbol all_40_0 gives: % 185.85/25.27 | (50) addition(all_22_3, all_22_1) = all_40_0 & addition(all_22_5, all_40_0) % 185.85/25.27 | = all_22_0 & $i(all_40_0) & $i(all_22_0) % 185.85/25.27 | % 185.85/25.27 | ALPHA: (50) implies: % 185.85/25.27 | (51) $i(all_40_0) % 185.85/25.27 | (52) addition(all_22_5, all_40_0) = all_22_0 % 185.85/25.27 | (53) addition(all_22_3, all_22_1) = all_40_0 % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_commutativity) with all_22_10, all_22_9, % 185.85/25.27 | all_36_0, simplifying with (13), (14), (47) gives: % 185.85/25.27 | (54) addition(all_22_9, all_22_10) = all_36_0 & $i(all_36_0) % 185.85/25.27 | % 185.85/25.27 | ALPHA: (54) implies: % 185.85/25.27 | (55) addition(all_22_9, all_22_10) = all_36_0 % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_commutativity) with all_22_9, all_22_7, % 185.85/25.27 | all_38_0, simplifying with (14), (16), (49) gives: % 185.85/25.27 | (56) addition(all_22_7, all_22_9) = all_38_0 & $i(all_38_0) % 185.85/25.27 | % 185.85/25.27 | ALPHA: (56) implies: % 185.85/25.27 | (57) addition(all_22_7, all_22_9) = all_38_0 % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_34_0, % 185.85/25.27 | all_22_8, all_22_2, all_22_0, simplifying with (15), (20), (23), % 185.85/25.27 | (43), (44) gives: % 185.85/25.27 | (58) ? [v0: $i] : (addition(all_34_0, all_22_1) = v0 & addition(all_22_8, % 185.85/25.27 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_34_0, % 185.85/25.27 | all_22_2, simplifying with (15), (43), (44) gives: % 185.85/25.27 | (59) addition(all_34_0, all_22_8) = all_22_2 & $i(all_22_2) % 185.85/25.27 | % 185.85/25.27 | ALPHA: (59) implies: % 185.85/25.27 | (60) addition(all_34_0, all_22_8) = all_22_2 % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_22_7, % 185.85/25.27 | all_22_9, all_22_6, all_22_8, all_22_5, simplifying with (13), % 185.85/25.27 | (14), (16), (24), (25), (33) gives: % 185.85/25.27 | (61) ? [v0: $i] : (multiplication(all_22_10, v0) = all_22_5 & % 185.85/25.27 | addition(all_22_7, all_22_9) = v0 & $i(v0) & $i(all_22_5)) % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_22_8, % 185.85/25.27 | all_22_6, all_22_5, all_22_2, simplifying with (15), (17), (19), % 185.85/25.27 | (22), (33) gives: % 185.85/25.27 | (62) ? [v0: $i] : (addition(all_22_6, v0) = all_22_2 & addition(all_22_8, % 185.85/25.27 | all_22_3) = v0 & $i(v0) & $i(all_22_2)) % 185.85/25.27 | % 185.85/25.27 | GROUND_INST: instantiating (additive_commutativity) with all_22_6, all_22_3, % 185.85/25.27 | all_34_0, simplifying with (17), (19), (45) gives: % 185.85/25.28 | (63) addition(all_22_3, all_22_6) = all_34_0 & $i(all_34_0) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (63) implies: % 185.85/25.28 | (64) addition(all_22_3, all_22_6) = all_34_0 % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (additive_associativity) with all_40_0, all_22_6, % 185.85/25.28 | all_22_8, all_22_5, all_22_0, simplifying with (15), (17), (21), % 185.85/25.28 | (51), (52) gives: % 185.85/25.28 | (65) ? [v0: $i] : (addition(all_22_6, all_40_0) = v0 & addition(all_22_8, % 185.85/25.28 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (additive_associativity) with all_40_0, all_22_8, % 185.85/25.28 | all_22_6, all_22_5, all_22_0, simplifying with (15), (17), (33), % 185.85/25.28 | (51), (52) gives: % 185.85/25.28 | (66) ? [v0: $i] : (addition(all_22_6, v0) = all_22_0 & addition(all_22_8, % 185.85/25.28 | all_40_0) = v0 & $i(v0) & $i(all_22_0)) % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (additive_commutativity) with all_22_5, all_40_0, % 185.85/25.28 | all_22_0, simplifying with (32), (51), (52) gives: % 185.85/25.28 | (67) addition(all_40_0, all_22_5) = all_22_0 & $i(all_22_0) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (67) implies: % 185.85/25.28 | (68) addition(all_40_0, all_22_5) = all_22_0 % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_5, % 185.85/25.28 | all_22_3, all_22_2, all_22_0, simplifying with (19), (20), (23), % 185.85/25.28 | (32), (36) gives: % 185.85/25.28 | (69) ? [v0: $i] : (addition(all_22_3, v0) = all_22_0 & addition(all_22_5, % 185.85/25.28 | all_22_1) = v0 & $i(v0) & $i(all_22_0)) % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (right_distributivity) with all_22_4, all_22_9, % 185.85/25.28 | all_22_7, all_22_3, all_22_1, all_40_0, simplifying with (14), % 185.85/25.28 | (16), (18), (26), (27), (53) gives: % 185.85/25.28 | (70) ? [v0: $i] : (multiplication(all_22_4, v0) = all_40_0 & % 185.85/25.28 | addition(all_22_9, all_22_7) = v0 & $i(v0) & $i(all_40_0)) % 185.85/25.28 | % 185.85/25.28 | GROUND_INST: instantiating (additive_commutativity) with all_22_3, all_22_1, % 185.85/25.28 | all_40_0, simplifying with (19), (20), (53) gives: % 185.85/25.28 | (71) addition(all_22_1, all_22_3) = all_40_0 & $i(all_40_0) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (71) implies: % 185.85/25.28 | (72) addition(all_22_1, all_22_3) = all_40_0 % 185.85/25.28 | % 185.85/25.28 | DELTA: instantiating (66) with fresh symbol all_48_0 gives: % 185.85/25.28 | (73) addition(all_22_6, all_48_0) = all_22_0 & addition(all_22_8, all_40_0) % 185.85/25.28 | = all_48_0 & $i(all_48_0) & $i(all_22_0) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (73) implies: % 185.85/25.28 | (74) addition(all_22_8, all_40_0) = all_48_0 % 185.85/25.28 | % 185.85/25.28 | DELTA: instantiating (65) with fresh symbol all_50_0 gives: % 185.85/25.28 | (75) addition(all_22_6, all_40_0) = all_50_0 & addition(all_22_8, all_50_0) % 185.85/25.28 | = all_22_0 & $i(all_50_0) & $i(all_22_0) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (75) implies: % 185.85/25.28 | (76) addition(all_22_6, all_40_0) = all_50_0 % 185.85/25.28 | % 185.85/25.28 | DELTA: instantiating (61) with fresh symbol all_52_0 gives: % 185.85/25.28 | (77) multiplication(all_22_10, all_52_0) = all_22_5 & addition(all_22_7, % 185.85/25.28 | all_22_9) = all_52_0 & $i(all_52_0) & $i(all_22_5) % 185.85/25.28 | % 185.85/25.28 | ALPHA: (77) implies: % 185.85/25.28 | (78) $i(all_52_0) % 185.85/25.28 | (79) addition(all_22_7, all_22_9) = all_52_0 % 185.85/25.28 | (80) multiplication(all_22_10, all_52_0) = all_22_5 % 185.85/25.28 | % 185.85/25.28 | DELTA: instantiating (70) with fresh symbol all_54_0 gives: % 185.85/25.29 | (81) multiplication(all_22_4, all_54_0) = all_40_0 & addition(all_22_9, % 185.85/25.29 | all_22_7) = all_54_0 & $i(all_54_0) & $i(all_40_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (81) implies: % 185.85/25.29 | (82) addition(all_22_9, all_22_7) = all_54_0 % 185.85/25.29 | (83) multiplication(all_22_4, all_54_0) = all_40_0 % 185.85/25.29 | % 185.85/25.29 | DELTA: instantiating (69) with fresh symbol all_56_0 gives: % 185.85/25.29 | (84) addition(all_22_3, all_56_0) = all_22_0 & addition(all_22_5, all_22_1) % 185.85/25.29 | = all_56_0 & $i(all_56_0) & $i(all_22_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (84) implies: % 185.85/25.29 | (85) addition(all_22_5, all_22_1) = all_56_0 % 185.85/25.29 | (86) addition(all_22_3, all_56_0) = all_22_0 % 185.85/25.29 | % 185.85/25.29 | DELTA: instantiating (62) with fresh symbol all_58_0 gives: % 185.85/25.29 | (87) addition(all_22_6, all_58_0) = all_22_2 & addition(all_22_8, all_22_3) % 185.85/25.29 | = all_58_0 & $i(all_58_0) & $i(all_22_2) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (87) implies: % 185.85/25.29 | (88) addition(all_22_8, all_22_3) = all_58_0 % 185.85/25.29 | (89) addition(all_22_6, all_58_0) = all_22_2 % 185.85/25.29 | % 185.85/25.29 | DELTA: instantiating (58) with fresh symbol all_60_0 gives: % 185.85/25.29 | (90) addition(all_34_0, all_22_1) = all_60_0 & addition(all_22_8, all_60_0) % 185.85/25.29 | = all_22_0 & $i(all_60_0) & $i(all_22_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (90) implies: % 185.85/25.29 | (91) $i(all_60_0) % 185.85/25.29 | (92) addition(all_22_8, all_60_0) = all_22_0 % 185.85/25.29 | (93) addition(all_34_0, all_22_1) = all_60_0 % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (8) with all_38_0, all_54_0, all_22_7, all_22_9, % 185.85/25.29 | simplifying with (49), (82) gives: % 185.85/25.29 | (94) all_54_0 = all_38_0 % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (8) with all_38_0, all_52_0, all_22_9, all_22_7, % 185.85/25.29 | simplifying with (57), (79) gives: % 185.85/25.29 | (95) all_52_0 = all_38_0 % 185.85/25.29 | % 185.85/25.29 | REDUCE: (83), (94) imply: % 185.85/25.29 | (96) multiplication(all_22_4, all_38_0) = all_40_0 % 185.85/25.29 | % 185.85/25.29 | REDUCE: (80), (95) imply: % 185.85/25.29 | (97) multiplication(all_22_10, all_38_0) = all_22_5 % 185.85/25.29 | % 185.85/25.29 | REDUCE: (78), (95) imply: % 185.85/25.29 | (98) $i(all_38_0) % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (left_distributivity) with all_22_10, all_22_4, % 185.85/25.29 | all_22_9, all_22_8, all_22_3, all_58_0, simplifying with (13), % 185.85/25.29 | (14), (18), (24), (26), (88) gives: % 185.85/25.29 | (99) ? [v0: $i] : (multiplication(v0, all_22_9) = all_58_0 & % 185.85/25.29 | addition(all_22_10, all_22_4) = v0 & $i(v0) & $i(all_58_0)) % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_22_3, % 185.85/25.29 | all_58_0, simplifying with (15), (19), (88) gives: % 185.85/25.29 | (100) addition(all_22_3, all_22_8) = all_58_0 & $i(all_58_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (100) implies: % 185.85/25.29 | (101) $i(all_58_0) % 185.85/25.29 | (102) addition(all_22_3, all_22_8) = all_58_0 % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_40_0, % 185.85/25.29 | all_48_0, simplifying with (15), (51), (74) gives: % 185.85/25.29 | (103) addition(all_40_0, all_22_8) = all_48_0 & $i(all_48_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (103) implies: % 185.85/25.29 | (104) addition(all_40_0, all_22_8) = all_48_0 % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_60_0, % 185.85/25.29 | all_22_0, simplifying with (15), (91), (92) gives: % 185.85/25.29 | (105) addition(all_60_0, all_22_8) = all_22_0 & $i(all_22_0) % 185.85/25.29 | % 185.85/25.29 | ALPHA: (105) implies: % 185.85/25.29 | (106) addition(all_60_0, all_22_8) = all_22_0 % 185.85/25.29 | % 185.85/25.29 | GROUND_INST: instantiating (5) with all_22_7, all_22_9, all_38_0, simplifying % 185.85/25.29 | with (14), (16), (41), (57) gives: % 185.85/25.29 | (107) all_38_0 = one % 185.85/25.29 | % 185.85/25.30 | GROUND_INST: instantiating (additive_commutativity) with all_22_6, all_40_0, % 185.85/25.30 | all_50_0, simplifying with (17), (51), (76) gives: % 185.85/25.30 | (108) addition(all_40_0, all_22_6) = all_50_0 & $i(all_50_0) % 185.85/25.30 | % 185.85/25.30 | ALPHA: (108) implies: % 185.85/25.30 | (109) addition(all_40_0, all_22_6) = all_50_0 % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_58_0, % 185.85/25.30 | all_22_6, all_22_2, all_22_0, simplifying with (17), (20), (23), % 185.85/25.30 | (89), (101) gives: % 185.85/25.30 | (110) ? [v0: $i] : (addition(all_58_0, all_22_1) = v0 & addition(all_22_6, % 185.85/25.30 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_commutativity) with all_22_6, all_58_0, % 185.85/25.30 | all_22_2, simplifying with (17), (89), (101) gives: % 185.85/25.30 | (111) addition(all_58_0, all_22_6) = all_22_2 & $i(all_22_2) % 185.85/25.30 | % 185.85/25.30 | ALPHA: (111) implies: % 185.85/25.30 | (112) addition(all_58_0, all_22_6) = all_22_2 % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_8, % 185.85/25.30 | all_22_6, all_22_5, all_56_0, simplifying with (15), (17), (20), % 185.85/25.30 | (33), (85) gives: % 185.85/25.30 | (113) ? [v0: $i] : (addition(all_22_6, v0) = all_56_0 & addition(all_22_8, % 185.85/25.30 | all_22_1) = v0 & $i(v0) & $i(all_56_0)) % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_6, % 185.85/25.30 | all_22_8, all_22_5, all_56_0, simplifying with (15), (17), (20), % 185.85/25.30 | (21), (85) gives: % 185.85/25.30 | (114) ? [v0: $i] : (addition(all_22_6, all_22_1) = v0 & addition(all_22_8, % 185.85/25.30 | v0) = all_56_0 & $i(v0) & $i(all_56_0)) % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_commutativity) with all_22_5, all_22_1, % 185.85/25.30 | all_56_0, simplifying with (20), (32), (85) gives: % 185.85/25.30 | (115) addition(all_22_1, all_22_5) = all_56_0 & $i(all_56_0) % 185.85/25.30 | % 185.85/25.30 | ALPHA: (115) implies: % 185.85/25.30 | (116) $i(all_56_0) % 185.85/25.30 | (117) addition(all_22_1, all_22_5) = all_56_0 % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_commutativity) with all_22_3, all_56_0, % 185.85/25.30 | all_22_0, simplifying with (19), (86), (116) gives: % 185.85/25.30 | (118) addition(all_56_0, all_22_3) = all_22_0 & $i(all_22_0) % 185.85/25.30 | % 185.85/25.30 | ALPHA: (118) implies: % 185.85/25.30 | (119) addition(all_56_0, all_22_3) = all_22_0 % 185.85/25.30 | % 185.85/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_8, % 185.85/25.30 | all_34_0, all_22_2, all_22_0, simplifying with (15), (20), (23), % 185.85/25.30 | (43), (60) gives: % 185.85/25.30 | (120) ? [v0: $i] : (addition(all_34_0, v0) = all_22_0 & addition(all_22_8, % 185.85/25.30 | all_22_1) = v0 & $i(v0) & $i(all_22_0)) % 185.85/25.30 | % 186.01/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_3, % 186.01/25.30 | all_22_6, all_34_0, all_22_2, simplifying with (15), (17), (19), % 186.01/25.30 | (45), (60) gives: % 186.01/25.30 | (121) ? [v0: $i] : (addition(all_22_3, all_22_8) = v0 & addition(all_22_6, % 186.01/25.30 | v0) = all_22_2 & $i(v0) & $i(all_22_2)) % 186.01/25.30 | % 186.01/25.30 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_3, % 186.01/25.30 | all_22_6, all_34_0, all_60_0, simplifying with (17), (19), (20), % 186.01/25.30 | (45), (93) gives: % 186.01/25.31 | (122) ? [v0: $i] : (addition(all_22_3, all_22_1) = v0 & addition(all_22_6, % 186.01/25.31 | v0) = all_60_0 & $i(v0) & $i(all_60_0)) % 186.01/25.31 | % 186.01/25.31 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_6, % 186.01/25.31 | all_22_3, all_34_0, all_60_0, simplifying with (17), (19), (20), % 186.01/25.31 | (64), (93) gives: % 186.01/25.31 | (123) ? [v0: $i] : (addition(all_22_3, v0) = all_60_0 & addition(all_22_6, % 186.01/25.31 | all_22_1) = v0 & $i(v0) & $i(all_60_0)) % 186.01/25.31 | % 186.01/25.31 | GROUND_INST: instantiating (additive_associativity) with all_22_5, all_22_1, % 186.01/25.31 | all_22_3, all_40_0, all_22_0, simplifying with (19), (20), (32), % 186.01/25.31 | (53), (68) gives: % 186.01/25.31 | (124) ? [v0: $i] : (addition(all_22_1, all_22_5) = v0 & addition(all_22_3, % 186.01/25.31 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 186.01/25.31 | % 186.01/25.31 | GROUND_INST: instantiating (left_distributivity) with all_22_10, all_22_4, % 186.01/25.31 | all_38_0, all_22_5, all_40_0, all_22_0, simplifying with (13), % 186.01/25.31 | (18), (52), (96), (97), (98) gives: % 186.01/25.31 | (125) ? [v0: $i] : (multiplication(v0, all_38_0) = all_22_0 & % 186.01/25.31 | addition(all_22_10, all_22_4) = v0 & $i(v0) & $i(all_22_0)) % 186.01/25.31 | % 186.01/25.31 | GROUND_INST: instantiating (left_distributivity) with all_22_4, all_22_10, % 186.01/25.31 | all_38_0, all_40_0, all_22_5, all_22_0, simplifying with (13), % 186.01/25.31 | (18), (68), (96), (97), (98) gives: % 186.01/25.31 | (126) ? [v0: $i] : (multiplication(v0, all_38_0) = all_22_0 & % 186.01/25.31 | addition(all_22_4, all_22_10) = v0 & $i(v0) & $i(all_22_0)) % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (99) with fresh symbol all_76_0 gives: % 186.01/25.31 | (127) multiplication(all_76_0, all_22_9) = all_58_0 & addition(all_22_10, % 186.01/25.31 | all_22_4) = all_76_0 & $i(all_76_0) & $i(all_58_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (127) implies: % 186.01/25.31 | (128) addition(all_22_10, all_22_4) = all_76_0 % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (110) with fresh symbol all_78_0 gives: % 186.01/25.31 | (129) addition(all_58_0, all_22_1) = all_78_0 & addition(all_22_6, % 186.01/25.31 | all_78_0) = all_22_0 & $i(all_78_0) & $i(all_22_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (129) implies: % 186.01/25.31 | (130) addition(all_58_0, all_22_1) = all_78_0 % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (113) with fresh symbol all_80_0 gives: % 186.01/25.31 | (131) addition(all_22_6, all_80_0) = all_56_0 & addition(all_22_8, % 186.01/25.31 | all_22_1) = all_80_0 & $i(all_80_0) & $i(all_56_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (131) implies: % 186.01/25.31 | (132) addition(all_22_8, all_22_1) = all_80_0 % 186.01/25.31 | (133) addition(all_22_6, all_80_0) = all_56_0 % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (123) with fresh symbol all_82_0 gives: % 186.01/25.31 | (134) addition(all_22_3, all_82_0) = all_60_0 & addition(all_22_6, % 186.01/25.31 | all_22_1) = all_82_0 & $i(all_82_0) & $i(all_60_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (134) implies: % 186.01/25.31 | (135) addition(all_22_6, all_22_1) = all_82_0 % 186.01/25.31 | (136) addition(all_22_3, all_82_0) = all_60_0 % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (120) with fresh symbol all_84_0 gives: % 186.01/25.31 | (137) addition(all_34_0, all_84_0) = all_22_0 & addition(all_22_8, % 186.01/25.31 | all_22_1) = all_84_0 & $i(all_84_0) & $i(all_22_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (137) implies: % 186.01/25.31 | (138) addition(all_22_8, all_22_1) = all_84_0 % 186.01/25.31 | (139) addition(all_34_0, all_84_0) = all_22_0 % 186.01/25.31 | % 186.01/25.31 | DELTA: instantiating (114) with fresh symbol all_86_0 gives: % 186.01/25.31 | (140) addition(all_22_6, all_22_1) = all_86_0 & addition(all_22_8, % 186.01/25.31 | all_86_0) = all_56_0 & $i(all_86_0) & $i(all_56_0) % 186.01/25.31 | % 186.01/25.31 | ALPHA: (140) implies: % 186.01/25.32 | (141) $i(all_86_0) % 186.01/25.32 | (142) addition(all_22_8, all_86_0) = all_56_0 % 186.01/25.32 | (143) addition(all_22_6, all_22_1) = all_86_0 % 186.01/25.32 | % 186.01/25.32 | DELTA: instantiating (126) with fresh symbol all_88_0 gives: % 186.01/25.32 | (144) multiplication(all_88_0, all_38_0) = all_22_0 & addition(all_22_4, % 186.01/25.32 | all_22_10) = all_88_0 & $i(all_88_0) & $i(all_22_0) % 186.01/25.32 | % 186.01/25.32 | ALPHA: (144) implies: % 186.01/25.32 | (145) addition(all_22_4, all_22_10) = all_88_0 % 186.01/25.32 | (146) multiplication(all_88_0, all_38_0) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | DELTA: instantiating (125) with fresh symbol all_90_0 gives: % 186.01/25.32 | (147) multiplication(all_90_0, all_38_0) = all_22_0 & addition(all_22_10, % 186.01/25.32 | all_22_4) = all_90_0 & $i(all_90_0) & $i(all_22_0) % 186.01/25.32 | % 186.01/25.32 | ALPHA: (147) implies: % 186.01/25.32 | (148) addition(all_22_10, all_22_4) = all_90_0 % 186.01/25.32 | (149) multiplication(all_90_0, all_38_0) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | DELTA: instantiating (124) with fresh symbol all_92_0 gives: % 186.01/25.32 | (150) addition(all_22_1, all_22_5) = all_92_0 & addition(all_22_3, % 186.01/25.32 | all_92_0) = all_22_0 & $i(all_92_0) & $i(all_22_0) % 186.01/25.32 | % 186.01/25.32 | ALPHA: (150) implies: % 186.01/25.32 | (151) addition(all_22_1, all_22_5) = all_92_0 % 186.01/25.32 | % 186.01/25.32 | DELTA: instantiating (122) with fresh symbol all_94_0 gives: % 186.01/25.32 | (152) addition(all_22_3, all_22_1) = all_94_0 & addition(all_22_6, % 186.01/25.32 | all_94_0) = all_60_0 & $i(all_94_0) & $i(all_60_0) % 186.01/25.32 | % 186.01/25.32 | ALPHA: (152) implies: % 186.01/25.32 | (153) addition(all_22_6, all_94_0) = all_60_0 % 186.01/25.32 | (154) addition(all_22_3, all_22_1) = all_94_0 % 186.01/25.32 | % 186.01/25.32 | DELTA: instantiating (121) with fresh symbol all_96_0 gives: % 186.01/25.32 | (155) addition(all_22_3, all_22_8) = all_96_0 & addition(all_22_6, % 186.01/25.32 | all_96_0) = all_22_2 & $i(all_96_0) & $i(all_22_2) % 186.01/25.32 | % 186.01/25.32 | ALPHA: (155) implies: % 186.01/25.32 | (156) $i(all_96_0) % 186.01/25.32 | (157) addition(all_22_6, all_96_0) = all_22_2 % 186.01/25.32 | (158) addition(all_22_3, all_22_8) = all_96_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (107), (149) imply: % 186.01/25.32 | (159) multiplication(all_90_0, one) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (107), (146) imply: % 186.01/25.32 | (160) multiplication(all_88_0, one) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (96), (107) imply: % 186.01/25.32 | (161) multiplication(all_22_4, one) = all_40_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (97), (107) imply: % 186.01/25.32 | (162) multiplication(all_22_10, one) = all_22_5 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_76_0, all_90_0, all_22_4, all_22_10, % 186.01/25.32 | simplifying with (128), (148) gives: % 186.01/25.32 | (163) all_90_0 = all_76_0 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_80_0, all_84_0, all_22_1, all_22_8, % 186.01/25.32 | simplifying with (132), (138) gives: % 186.01/25.32 | (164) all_84_0 = all_80_0 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_82_0, all_86_0, all_22_1, all_22_6, % 186.01/25.32 | simplifying with (135), (143) gives: % 186.01/25.32 | (165) all_86_0 = all_82_0 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_58_0, all_96_0, all_22_8, all_22_3, % 186.01/25.32 | simplifying with (102), (158) gives: % 186.01/25.32 | (166) all_96_0 = all_58_0 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_40_0, all_94_0, all_22_1, all_22_3, % 186.01/25.32 | simplifying with (53), (154) gives: % 186.01/25.32 | (167) all_94_0 = all_40_0 % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_56_0, all_92_0, all_22_5, all_22_1, % 186.01/25.32 | simplifying with (117), (151) gives: % 186.01/25.32 | (168) all_92_0 = all_56_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (159), (163) imply: % 186.01/25.32 | (169) multiplication(all_76_0, one) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (139), (164) imply: % 186.01/25.32 | (170) addition(all_34_0, all_80_0) = all_22_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (153), (167) imply: % 186.01/25.32 | (171) addition(all_22_6, all_40_0) = all_60_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (142), (165) imply: % 186.01/25.32 | (172) addition(all_22_8, all_82_0) = all_56_0 % 186.01/25.32 | % 186.01/25.32 | REDUCE: (141), (165) imply: % 186.01/25.32 | (173) $i(all_82_0) % 186.01/25.32 | % 186.01/25.32 | GROUND_INST: instantiating (8) with all_50_0, all_60_0, all_40_0, all_22_6, % 186.01/25.32 | simplifying with (76), (171) gives: % 186.01/25.32 | (174) all_60_0 = all_50_0 % 186.01/25.32 | % 186.01/25.33 | REDUCE: (106), (174) imply: % 186.01/25.33 | (175) addition(all_50_0, all_22_8) = all_22_0 % 186.01/25.33 | % 186.01/25.33 | REDUCE: (93), (174) imply: % 186.01/25.33 | (176) addition(all_34_0, all_22_1) = all_50_0 % 186.01/25.33 | % 186.01/25.33 | REDUCE: (136), (174) imply: % 186.01/25.33 | (177) addition(all_22_3, all_82_0) = all_50_0 % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_10, all_22_4, % 186.01/25.33 | all_76_0, simplifying with (13), (18), (128) gives: % 186.01/25.33 | (178) addition(all_22_4, all_22_10) = all_76_0 & $i(all_76_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (178) implies: % 186.01/25.33 | (179) $i(all_76_0) % 186.01/25.33 | (180) addition(all_22_4, all_22_10) = all_76_0 % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_22_1, % 186.01/25.33 | all_80_0, simplifying with (15), (20), (132) gives: % 186.01/25.33 | (181) addition(all_22_1, all_22_8) = all_80_0 & $i(all_80_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (181) implies: % 186.01/25.33 | (182) $i(all_80_0) % 186.01/25.33 | (183) addition(all_22_1, all_22_8) = all_80_0 % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_82_0, % 186.01/25.33 | all_56_0, simplifying with (15), (172), (173) gives: % 186.01/25.33 | (184) addition(all_82_0, all_22_8) = all_56_0 & $i(all_56_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (184) implies: % 186.01/25.33 | (185) addition(all_82_0, all_22_8) = all_56_0 % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (left_distributivity) with all_22_10, all_22_4, % 186.01/25.33 | all_22_7, all_22_6, all_22_1, all_82_0, simplifying with (13), % 186.01/25.33 | (16), (18), (25), (27), (135) gives: % 186.01/25.33 | (186) ? [v0: $i] : (multiplication(v0, all_22_7) = all_82_0 & % 186.01/25.33 | addition(all_22_10, all_22_4) = v0 & $i(v0) & $i(all_82_0)) % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_6, all_22_1, % 186.01/25.33 | all_82_0, simplifying with (17), (20), (135) gives: % 186.01/25.33 | (187) addition(all_22_1, all_22_6) = all_82_0 & $i(all_82_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (187) implies: % 186.01/25.33 | (188) addition(all_22_1, all_22_6) = all_82_0 % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (5) with all_22_4, all_22_10, all_88_0, simplifying % 186.01/25.33 | with (13), (18), (39), (145) gives: % 186.01/25.33 | (189) all_88_0 = one % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (4) with all_22_4, all_22_10, all_88_0, simplifying % 186.01/25.33 | with (13), (18), (39), (145) gives: % 186.01/25.33 | (190) multiplication(all_22_4, all_22_10) = zero & % 186.01/25.33 | multiplication(all_22_10, all_22_4) = zero % 186.01/25.33 | % 186.01/25.33 | ALPHA: (190) implies: % 186.01/25.33 | (191) multiplication(all_22_10, all_22_4) = zero % 186.01/25.33 | (192) multiplication(all_22_4, all_22_10) = zero % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_4, all_22_10, % 186.01/25.33 | all_88_0, simplifying with (13), (18), (145) gives: % 186.01/25.33 | (193) addition(all_22_10, all_22_4) = all_88_0 & $i(all_88_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (193) implies: % 186.01/25.33 | (194) $i(all_88_0) % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (left_distributivity) with all_22_4, all_22_10, % 186.01/25.33 | all_22_9, all_22_3, all_22_8, all_58_0, simplifying with (13), % 186.01/25.33 | (14), (18), (24), (26), (102) gives: % 186.01/25.33 | (195) ? [v0: $i] : (multiplication(v0, all_22_9) = all_58_0 & % 186.01/25.33 | addition(all_22_4, all_22_10) = v0 & $i(v0) & $i(all_58_0)) % 186.01/25.33 | % 186.01/25.33 | GROUND_INST: instantiating (additive_commutativity) with all_22_3, all_82_0, % 186.01/25.33 | all_50_0, simplifying with (19), (173), (177) gives: % 186.01/25.33 | (196) addition(all_82_0, all_22_3) = all_50_0 & $i(all_50_0) % 186.01/25.33 | % 186.01/25.33 | ALPHA: (196) implies: % 186.01/25.33 | (197) addition(all_82_0, all_22_3) = all_50_0 % 186.01/25.33 | % 186.01/25.34 | GROUND_INST: instantiating (additive_commutativity) with all_34_0, all_80_0, % 186.01/25.34 | all_22_0, simplifying with (43), (170), (182) gives: % 186.01/25.34 | (198) addition(all_80_0, all_34_0) = all_22_0 & $i(all_22_0) % 186.01/25.34 | % 186.01/25.34 | ALPHA: (198) implies: % 186.01/25.34 | (199) addition(all_80_0, all_34_0) = all_22_0 % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_3, % 186.01/25.34 | all_22_1, all_40_0, all_48_0, simplifying with (15), (19), (20), % 186.01/25.34 | (72), (104) gives: % 186.01/25.34 | (200) ? [v0: $i] : (addition(all_22_1, v0) = all_48_0 & addition(all_22_3, % 186.01/25.34 | all_22_8) = v0 & $i(v0) & $i(all_48_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_1, % 186.01/25.34 | all_22_3, all_40_0, all_48_0, simplifying with (15), (19), (20), % 186.01/25.34 | (53), (104) gives: % 186.01/25.34 | (201) ? [v0: $i] : (addition(all_22_1, all_22_8) = v0 & addition(all_22_3, % 186.01/25.34 | v0) = all_48_0 & $i(v0) & $i(all_48_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_6, all_22_1, % 186.01/25.34 | all_22_3, all_40_0, all_50_0, simplifying with (17), (19), (20), % 186.01/25.34 | (53), (109) gives: % 186.01/25.34 | (202) ? [v0: $i] : (addition(all_22_1, all_22_6) = v0 & addition(all_22_3, % 186.01/25.34 | v0) = all_50_0 & $i(v0) & $i(all_50_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_1, % 186.01/25.34 | all_34_0, all_50_0, all_22_0, simplifying with (15), (20), (43), % 186.01/25.34 | (175), (176) gives: % 186.01/25.34 | (203) ? [v0: $i] : (addition(all_34_0, v0) = all_22_0 & addition(all_22_1, % 186.01/25.34 | all_22_8) = v0 & $i(v0) & $i(all_22_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_82_0, % 186.01/25.34 | all_22_3, all_50_0, all_22_0, simplifying with (15), (19), (173), % 186.01/25.34 | (175), (177) gives: % 186.01/25.34 | (204) ? [v0: $i] : (addition(all_82_0, all_22_8) = v0 & addition(all_22_3, % 186.01/25.34 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_80_0, % 186.01/25.34 | all_22_6, all_56_0, all_22_0, simplifying with (17), (19), (119), % 186.01/25.34 | (133), (182) gives: % 186.01/25.34 | (205) ? [v0: $i] : (addition(all_80_0, all_22_3) = v0 & addition(all_22_6, % 186.01/25.34 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 186.01/25.34 | % 186.01/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_82_0, % 186.01/25.34 | all_22_8, all_56_0, all_22_0, simplifying with (15), (19), (119), % 186.01/25.34 | (172), (173) gives: % 186.01/25.34 | (206) ? [v0: $i] : (addition(all_82_0, all_22_3) = v0 & addition(all_22_8, % 186.01/25.34 | v0) = all_22_0 & $i(v0) & $i(all_22_0)) % 186.01/25.34 | % 186.22/25.34 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_6, % 186.22/25.34 | all_58_0, all_22_2, all_22_0, simplifying with (17), (20), (23), % 186.22/25.34 | (101), (112) gives: % 186.22/25.35 | (207) ? [v0: $i] : (addition(all_58_0, v0) = all_22_0 & addition(all_22_6, % 186.22/25.35 | all_22_1) = v0 & $i(v0) & $i(all_22_0)) % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_3, % 186.22/25.35 | all_22_8, all_58_0, all_78_0, simplifying with (15), (19), (20), % 186.22/25.35 | (88), (130) gives: % 186.22/25.35 | (208) ? [v0: $i] : (addition(all_22_3, all_22_1) = v0 & addition(all_22_8, % 186.22/25.35 | v0) = all_78_0 & $i(v0) & $i(all_78_0)) % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (additive_associativity) with all_22_1, all_22_8, % 186.22/25.35 | all_22_3, all_58_0, all_78_0, simplifying with (15), (19), (20), % 186.22/25.35 | (102), (130) gives: % 186.22/25.35 | (209) ? [v0: $i] : (addition(all_22_3, v0) = all_78_0 & addition(all_22_8, % 186.22/25.35 | all_22_1) = v0 & $i(v0) & $i(all_78_0)) % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (1) with all_22_10, all_22_5, simplifying with % 186.22/25.35 | (13), (162) gives: % 186.22/25.35 | (210) all_22_5 = all_22_10 % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (1) with all_22_4, all_40_0, simplifying with (18), % 186.22/25.35 | (161) gives: % 186.22/25.35 | (211) all_40_0 = all_22_4 % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (1) with all_76_0, all_22_0, simplifying with % 186.22/25.35 | (169), (179) gives: % 186.22/25.35 | (212) all_76_0 = all_22_0 % 186.22/25.35 | % 186.22/25.35 | GROUND_INST: instantiating (1) with all_88_0, all_22_0, simplifying with % 186.22/25.35 | (160), (194) gives: % 186.22/25.35 | (213) all_88_0 = all_22_0 % 186.22/25.35 | % 186.22/25.35 | COMBINE_EQS: (189), (213) imply: % 186.22/25.35 | (214) all_22_0 = one % 186.22/25.35 | % 186.22/25.35 | COMBINE_EQS: (212), (214) imply: % 186.22/25.35 | (215) all_76_0 = one % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (186) with fresh symbol all_112_0 gives: % 186.22/25.35 | (216) multiplication(all_112_0, all_22_7) = all_82_0 & addition(all_22_10, % 186.22/25.35 | all_22_4) = all_112_0 & $i(all_112_0) & $i(all_82_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (216) implies: % 186.22/25.35 | (217) addition(all_22_10, all_22_4) = all_112_0 % 186.22/25.35 | (218) multiplication(all_112_0, all_22_7) = all_82_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (206) with fresh symbol all_114_0 gives: % 186.22/25.35 | (219) addition(all_82_0, all_22_3) = all_114_0 & addition(all_22_8, % 186.22/25.35 | all_114_0) = all_22_0 & $i(all_114_0) & $i(all_22_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (219) implies: % 186.22/25.35 | (220) $i(all_114_0) % 186.22/25.35 | (221) addition(all_82_0, all_22_3) = all_114_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (204) with fresh symbol all_116_0 gives: % 186.22/25.35 | (222) addition(all_82_0, all_22_8) = all_116_0 & addition(all_22_3, % 186.22/25.35 | all_116_0) = all_22_0 & $i(all_116_0) & $i(all_22_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (222) implies: % 186.22/25.35 | (223) addition(all_22_3, all_116_0) = all_22_0 % 186.22/25.35 | (224) addition(all_82_0, all_22_8) = all_116_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (209) with fresh symbol all_118_0 gives: % 186.22/25.35 | (225) addition(all_22_3, all_118_0) = all_78_0 & addition(all_22_8, % 186.22/25.35 | all_22_1) = all_118_0 & $i(all_118_0) & $i(all_78_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (225) implies: % 186.22/25.35 | (226) $i(all_118_0) % 186.22/25.35 | (227) addition(all_22_8, all_22_1) = all_118_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (205) with fresh symbol all_120_0 gives: % 186.22/25.35 | (228) addition(all_80_0, all_22_3) = all_120_0 & addition(all_22_6, % 186.22/25.35 | all_120_0) = all_22_0 & $i(all_120_0) & $i(all_22_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (228) implies: % 186.22/25.35 | (229) addition(all_80_0, all_22_3) = all_120_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (200) with fresh symbol all_122_0 gives: % 186.22/25.35 | (230) addition(all_22_1, all_122_0) = all_48_0 & addition(all_22_3, % 186.22/25.35 | all_22_8) = all_122_0 & $i(all_122_0) & $i(all_48_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (230) implies: % 186.22/25.35 | (231) $i(all_122_0) % 186.22/25.35 | (232) addition(all_22_3, all_22_8) = all_122_0 % 186.22/25.35 | % 186.22/25.35 | DELTA: instantiating (203) with fresh symbol all_124_0 gives: % 186.22/25.35 | (233) addition(all_34_0, all_124_0) = all_22_0 & addition(all_22_1, % 186.22/25.35 | all_22_8) = all_124_0 & $i(all_124_0) & $i(all_22_0) % 186.22/25.35 | % 186.22/25.35 | ALPHA: (233) implies: % 186.22/25.36 | (234) addition(all_22_1, all_22_8) = all_124_0 % 186.22/25.36 | % 186.22/25.36 | DELTA: instantiating (202) with fresh symbol all_126_0 gives: % 186.22/25.36 | (235) addition(all_22_1, all_22_6) = all_126_0 & addition(all_22_3, % 186.22/25.36 | all_126_0) = all_50_0 & $i(all_126_0) & $i(all_50_0) % 186.22/25.36 | % 186.22/25.36 | ALPHA: (235) implies: % 186.22/25.36 | (236) $i(all_126_0) % 186.22/25.36 | (237) addition(all_22_1, all_22_6) = all_126_0 % 186.22/25.36 | % 186.22/25.36 | DELTA: instantiating (201) with fresh symbol all_128_0 gives: % 186.22/25.36 | (238) addition(all_22_1, all_22_8) = all_128_0 & addition(all_22_3, % 186.22/25.36 | all_128_0) = all_48_0 & $i(all_128_0) & $i(all_48_0) % 186.22/25.36 | % 186.22/25.36 | ALPHA: (238) implies: % 186.22/25.36 | (239) addition(all_22_1, all_22_8) = all_128_0 % 186.22/25.36 | % 186.22/25.36 | DELTA: instantiating (195) with fresh symbol all_132_0 gives: % 186.22/25.36 | (240) multiplication(all_132_0, all_22_9) = all_58_0 & addition(all_22_4, % 186.22/25.36 | all_22_10) = all_132_0 & $i(all_132_0) & $i(all_58_0) % 186.22/25.36 | % 186.22/25.36 | ALPHA: (240) implies: % 186.22/25.36 | (241) addition(all_22_4, all_22_10) = all_132_0 % 186.22/25.36 | (242) multiplication(all_132_0, all_22_9) = all_58_0 % 186.22/25.36 | % 186.22/25.36 | DELTA: instantiating (208) with fresh symbol all_134_0 gives: % 186.22/25.36 | (243) addition(all_22_3, all_22_1) = all_134_0 & addition(all_22_8, % 186.22/25.36 | all_134_0) = all_78_0 & $i(all_134_0) & $i(all_78_0) % 186.22/25.36 | % 186.22/25.36 | ALPHA: (243) implies: % 186.22/25.36 | (244) $i(all_134_0) % 186.22/25.36 | (245) addition(all_22_3, all_22_1) = all_134_0 % 186.22/25.36 | % 186.22/25.36 | DELTA: instantiating (207) with fresh symbol all_136_0 gives: % 186.22/25.36 | (246) addition(all_58_0, all_136_0) = all_22_0 & addition(all_22_6, % 186.22/25.36 | all_22_1) = all_136_0 & $i(all_136_0) & $i(all_22_0) % 186.22/25.36 | % 186.22/25.36 | ALPHA: (246) implies: % 186.22/25.36 | (247) addition(all_22_6, all_22_1) = all_136_0 % 186.22/25.36 | (248) addition(all_58_0, all_136_0) = all_22_0 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (169), (214), (215) imply: % 186.22/25.36 | (249) multiplication(one, one) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (161), (211) imply: % 186.22/25.36 | (250) multiplication(all_22_4, one) = all_22_4 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (162), (210) imply: % 186.22/25.36 | (251) multiplication(all_22_10, one) = all_22_10 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (199), (214) imply: % 186.22/25.36 | (252) addition(all_80_0, all_34_0) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (214), (248) imply: % 186.22/25.36 | (253) addition(all_58_0, all_136_0) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (119), (214) imply: % 186.22/25.36 | (254) addition(all_56_0, all_22_3) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (175), (214) imply: % 186.22/25.36 | (255) addition(all_50_0, all_22_8) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (72), (211) imply: % 186.22/25.36 | (256) addition(all_22_1, all_22_3) = all_22_4 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (117), (210) imply: % 186.22/25.36 | (257) addition(all_22_1, all_22_10) = all_56_0 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (23), (214) imply: % 186.22/25.36 | (258) addition(all_22_2, all_22_1) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (214), (223) imply: % 186.22/25.36 | (259) addition(all_22_3, all_116_0) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (53), (211) imply: % 186.22/25.36 | (260) addition(all_22_3, all_22_1) = all_22_4 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (36), (210) imply: % 186.22/25.36 | (261) addition(all_22_3, all_22_10) = all_22_2 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (180), (215) imply: % 186.22/25.36 | (262) addition(all_22_4, all_22_10) = one % 186.22/25.36 | % 186.22/25.36 | REDUCE: (33), (210) imply: % 186.22/25.36 | (263) addition(all_22_6, all_22_8) = all_22_10 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (21), (210) imply: % 186.22/25.36 | (264) addition(all_22_8, all_22_6) = all_22_10 % 186.22/25.36 | % 186.22/25.36 | REDUCE: (128), (215) imply: % 186.22/25.36 | (265) addition(all_22_10, all_22_4) = one % 186.22/25.36 | % 186.22/25.36 | BETA: splitting (30) gives: % 186.22/25.36 | % 186.22/25.36 | Case 1: % 186.22/25.36 | | % 186.22/25.36 | | (266) ~ leq(all_22_0, one) % 186.22/25.36 | | % 186.22/25.36 | | REDUCE: (214), (266) imply: % 186.22/25.37 | | (267) ~ leq(one, one) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with one, all_112_0, all_22_4, all_22_10, % 186.22/25.37 | | simplifying with (217), (265) gives: % 186.22/25.37 | | (268) all_112_0 = one % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_80_0, all_118_0, all_22_1, all_22_8, % 186.22/25.37 | | simplifying with (132), (227) gives: % 186.22/25.37 | | (269) all_118_0 = all_80_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_82_0, all_136_0, all_22_1, all_22_6, % 186.22/25.37 | | simplifying with (135), (247) gives: % 186.22/25.37 | | (270) all_136_0 = all_82_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with one, all_132_0, all_22_10, all_22_4, % 186.22/25.37 | | simplifying with (241), (262) gives: % 186.22/25.37 | | (271) all_132_0 = one % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_58_0, all_122_0, all_22_8, all_22_3, % 186.22/25.37 | | simplifying with (102), (232) gives: % 186.22/25.37 | | (272) all_122_0 = all_58_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_22_4, all_134_0, all_22_1, all_22_3, % 186.22/25.37 | | simplifying with (245), (260) gives: % 186.22/25.37 | | (273) all_134_0 = all_22_4 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_124_0, all_128_0, all_22_8, % 186.22/25.37 | | all_22_1, simplifying with (234), (239) gives: % 186.22/25.37 | | (274) all_128_0 = all_124_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_80_0, all_128_0, all_22_8, all_22_1, % 186.22/25.37 | | simplifying with (183), (239) gives: % 186.22/25.37 | | (275) all_128_0 = all_80_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_82_0, all_126_0, all_22_6, all_22_1, % 186.22/25.37 | | simplifying with (188), (237) gives: % 186.22/25.37 | | (276) all_126_0 = all_82_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_56_0, all_116_0, all_22_8, all_82_0, % 186.22/25.37 | | simplifying with (185), (224) gives: % 186.22/25.37 | | (277) all_116_0 = all_56_0 % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (8) with all_50_0, all_114_0, all_22_3, all_82_0, % 186.22/25.37 | | simplifying with (197), (221) gives: % 186.22/25.37 | | (278) all_114_0 = all_50_0 % 186.22/25.37 | | % 186.22/25.37 | | COMBINE_EQS: (274), (275) imply: % 186.22/25.37 | | (279) all_124_0 = all_80_0 % 186.22/25.37 | | % 186.22/25.37 | | SIMP: (279) implies: % 186.22/25.37 | | (280) all_124_0 = all_80_0 % 186.22/25.37 | | % 186.22/25.37 | | REDUCE: (242), (271) imply: % 186.22/25.37 | | (281) multiplication(one, all_22_9) = all_58_0 % 186.22/25.37 | | % 186.22/25.37 | | REDUCE: (218), (268) imply: % 186.22/25.37 | | (282) multiplication(one, all_22_7) = all_82_0 % 186.22/25.37 | | % 186.22/25.37 | | REDUCE: (253), (270) imply: % 186.22/25.37 | | (283) addition(all_58_0, all_82_0) = one % 186.22/25.37 | | % 186.22/25.37 | | REDUCE: (259), (277) imply: % 186.22/25.37 | | (284) addition(all_22_3, all_56_0) = one % 186.22/25.37 | | % 186.22/25.37 | | REDUCE: (220), (278) imply: % 186.22/25.37 | | (285) $i(all_50_0) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_9, all_22_6, % 186.22/25.37 | | all_22_8, all_22_10, all_36_0, simplifying with (14), (15), % 186.22/25.37 | | (17), (47), (264) gives: % 186.22/25.37 | | (286) ? [v0: $i] : (addition(all_22_6, all_22_9) = v0 & % 186.22/25.37 | | addition(all_22_8, v0) = all_36_0 & $i(v0) & $i(all_36_0)) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_9, all_22_8, % 186.22/25.37 | | all_22_6, all_22_10, all_36_0, simplifying with (14), (15), % 186.22/25.37 | | (17), (47), (263) gives: % 186.22/25.37 | | (287) ? [v0: $i] : (addition(all_22_6, v0) = all_36_0 & % 186.22/25.37 | | addition(all_22_8, all_22_9) = v0 & $i(v0) & $i(all_36_0)) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_commutativity) with all_58_0, all_82_0, % 186.22/25.37 | | one, simplifying with (101), (173), (283) gives: % 186.22/25.37 | | (288) addition(all_82_0, all_58_0) = one & $i(one) % 186.22/25.37 | | % 186.22/25.37 | | ALPHA: (288) implies: % 186.22/25.37 | | (289) $i(one) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_22_1, % 186.22/25.37 | | all_22_8, all_80_0, all_120_0, simplifying with (15), (19), % 186.22/25.37 | | (20), (132), (229) gives: % 186.22/25.37 | | (290) ? [v0: $i] : (addition(all_22_1, all_22_3) = v0 & % 186.22/25.37 | | addition(all_22_8, v0) = all_120_0 & $i(v0) & $i(all_120_0)) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_22_8, % 186.22/25.37 | | all_22_1, all_80_0, all_120_0, simplifying with (15), (19), % 186.22/25.37 | | (20), (183), (229) gives: % 186.22/25.37 | | (291) ? [v0: $i] : (addition(all_22_1, v0) = all_120_0 & % 186.22/25.37 | | addition(all_22_8, all_22_3) = v0 & $i(v0) & $i(all_120_0)) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_3, all_22_8, % 186.22/25.37 | | all_82_0, all_56_0, one, simplifying with (15), (19), (173), % 186.22/25.37 | | (185), (254) gives: % 186.22/25.37 | | (292) ? [v0: $i] : (addition(all_82_0, v0) = one & addition(all_22_8, % 186.22/25.37 | | all_22_3) = v0 & $i(v0) & $i(one)) % 186.22/25.37 | | % 186.22/25.37 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_3, % 186.22/25.37 | | all_82_0, all_50_0, one, simplifying with (15), (19), (173), % 186.22/25.37 | | (197), (255) gives: % 186.22/25.38 | | (293) ? [v0: $i] : (addition(all_82_0, v0) = one & addition(all_22_3, % 186.22/25.38 | | all_22_8) = v0 & $i(v0) & $i(one)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with one, one, % 186.22/25.38 | | all_22_9, one, all_58_0, simplifying with (14), (249), (281), % 186.22/25.38 | | (289) gives: % 186.22/25.38 | | (294) ? [v0: $i] : (multiplication(one, v0) = all_58_0 & % 186.22/25.38 | | multiplication(one, all_22_9) = v0 & $i(v0) & $i(all_58_0)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (2) with all_22_9, all_58_0, simplifying with % 186.22/25.38 | | (14), (281) gives: % 186.22/25.38 | | (295) all_58_0 = all_22_9 % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with one, one, % 186.22/25.38 | | all_22_7, one, all_82_0, simplifying with (16), (249), (282), % 186.22/25.38 | | (289) gives: % 186.22/25.38 | | (296) ? [v0: $i] : (multiplication(one, v0) = all_82_0 & % 186.22/25.38 | | multiplication(one, all_22_7) = v0 & $i(v0) & $i(all_82_0)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (2) with all_22_7, all_82_0, simplifying with % 186.22/25.38 | | (16), (282) gives: % 186.22/25.38 | | (297) all_82_0 = all_22_7 % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_10, % 186.22/25.38 | | one, all_22_7, all_22_10, all_22_6, simplifying with (13), % 186.22/25.38 | | (16), (25), (251), (289) gives: % 186.22/25.38 | | (298) ? [v0: $i] : (multiplication(all_22_10, v0) = all_22_6 & % 186.22/25.38 | | multiplication(one, all_22_7) = v0 & $i(v0) & $i(all_22_6)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_10, % 186.22/25.38 | | one, all_22_9, all_22_10, all_22_8, simplifying with (13), % 186.22/25.38 | | (14), (24), (251), (289) gives: % 186.22/25.38 | | (299) ? [v0: $i] : (multiplication(all_22_10, v0) = all_22_8 & % 186.22/25.38 | | multiplication(one, all_22_9) = v0 & $i(v0) & $i(all_22_8)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_10, % 186.22/25.38 | | one, all_22_4, all_22_10, zero, simplifying with (13), (18), % 186.22/25.38 | | (191), (251), (289) gives: % 186.22/25.38 | | (300) ? [v0: $i] : (multiplication(all_22_10, v0) = zero & % 186.22/25.38 | | multiplication(one, all_22_4) = v0 & $i(v0) & $i(zero)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_4, % 186.22/25.38 | | one, all_22_7, all_22_4, all_22_1, simplifying with (16), (18), % 186.22/25.38 | | (27), (250), (289) gives: % 186.22/25.38 | | (301) ? [v0: $i] : (multiplication(all_22_4, v0) = all_22_1 & % 186.22/25.38 | | multiplication(one, all_22_7) = v0 & $i(v0) & $i(all_22_1)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_4, % 186.22/25.38 | | one, all_22_9, all_22_4, all_22_3, simplifying with (14), (18), % 186.22/25.38 | | (26), (250), (289) gives: % 186.22/25.38 | | (302) ? [v0: $i] : (multiplication(all_22_4, v0) = all_22_3 & % 186.22/25.38 | | multiplication(one, all_22_9) = v0 & $i(v0) & $i(all_22_3)) % 186.22/25.38 | | % 186.22/25.38 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_4, % 186.22/25.38 | | one, all_22_10, all_22_4, zero, simplifying with (13), (18), % 186.22/25.38 | | (192), (250), (289) gives: % 186.22/25.38 | | (303) ? [v0: $i] : (multiplication(all_22_4, v0) = zero & % 186.22/25.38 | | multiplication(one, all_22_10) = v0 & $i(v0) & $i(zero)) % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (287) with fresh symbol all_160_0 gives: % 186.22/25.38 | | (304) addition(all_22_6, all_160_0) = all_36_0 & addition(all_22_8, % 186.22/25.38 | | all_22_9) = all_160_0 & $i(all_160_0) & $i(all_36_0) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (304) implies: % 186.22/25.38 | | (305) addition(all_22_8, all_22_9) = all_160_0 % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (293) with fresh symbol all_162_0 gives: % 186.22/25.38 | | (306) addition(all_82_0, all_162_0) = one & addition(all_22_3, all_22_8) % 186.22/25.38 | | = all_162_0 & $i(all_162_0) & $i(one) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (306) implies: % 186.22/25.38 | | (307) $i(all_162_0) % 186.22/25.38 | | (308) addition(all_22_3, all_22_8) = all_162_0 % 186.22/25.38 | | (309) addition(all_82_0, all_162_0) = one % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (301) with fresh symbol all_164_0 gives: % 186.22/25.38 | | (310) multiplication(all_22_4, all_164_0) = all_22_1 & % 186.22/25.38 | | multiplication(one, all_22_7) = all_164_0 & $i(all_164_0) & % 186.22/25.38 | | $i(all_22_1) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (310) implies: % 186.22/25.38 | | (311) $i(all_164_0) % 186.22/25.38 | | (312) multiplication(one, all_22_7) = all_164_0 % 186.22/25.38 | | (313) multiplication(all_22_4, all_164_0) = all_22_1 % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (299) with fresh symbol all_166_0 gives: % 186.22/25.38 | | (314) multiplication(all_22_10, all_166_0) = all_22_8 & % 186.22/25.38 | | multiplication(one, all_22_9) = all_166_0 & $i(all_166_0) & % 186.22/25.38 | | $i(all_22_8) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (314) implies: % 186.22/25.38 | | (315) multiplication(one, all_22_9) = all_166_0 % 186.22/25.38 | | (316) multiplication(all_22_10, all_166_0) = all_22_8 % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (298) with fresh symbol all_168_0 gives: % 186.22/25.38 | | (317) multiplication(all_22_10, all_168_0) = all_22_6 & % 186.22/25.38 | | multiplication(one, all_22_7) = all_168_0 & $i(all_168_0) & % 186.22/25.38 | | $i(all_22_6) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (317) implies: % 186.22/25.38 | | (318) multiplication(one, all_22_7) = all_168_0 % 186.22/25.38 | | (319) multiplication(all_22_10, all_168_0) = all_22_6 % 186.22/25.38 | | % 186.22/25.38 | | DELTA: instantiating (292) with fresh symbol all_170_0 gives: % 186.22/25.38 | | (320) addition(all_82_0, all_170_0) = one & addition(all_22_8, all_22_3) % 186.22/25.38 | | = all_170_0 & $i(all_170_0) & $i(one) % 186.22/25.38 | | % 186.22/25.38 | | ALPHA: (320) implies: % 186.22/25.38 | | (321) addition(all_22_8, all_22_3) = all_170_0 % 186.22/25.38 | | % 186.22/25.39 | | DELTA: instantiating (291) with fresh symbol all_172_0 gives: % 186.22/25.39 | | (322) addition(all_22_1, all_172_0) = all_120_0 & addition(all_22_8, % 186.22/25.39 | | all_22_3) = all_172_0 & $i(all_172_0) & $i(all_120_0) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (322) implies: % 186.22/25.39 | | (323) addition(all_22_8, all_22_3) = all_172_0 % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (290) with fresh symbol all_174_0 gives: % 186.22/25.39 | | (324) addition(all_22_1, all_22_3) = all_174_0 & addition(all_22_8, % 186.22/25.39 | | all_174_0) = all_120_0 & $i(all_174_0) & $i(all_120_0) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (324) implies: % 186.22/25.39 | | (325) $i(all_174_0) % 186.22/25.39 | | (326) addition(all_22_1, all_22_3) = all_174_0 % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (286) with fresh symbol all_176_0 gives: % 186.22/25.39 | | (327) addition(all_22_6, all_22_9) = all_176_0 & addition(all_22_8, % 186.22/25.39 | | all_176_0) = all_36_0 & $i(all_176_0) & $i(all_36_0) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (327) implies: % 186.22/25.39 | | (328) $i(all_176_0) % 186.22/25.39 | | (329) addition(all_22_8, all_176_0) = all_36_0 % 186.22/25.39 | | (330) addition(all_22_6, all_22_9) = all_176_0 % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (300) with fresh symbol all_178_0 gives: % 186.22/25.39 | | (331) multiplication(all_22_10, all_178_0) = zero & multiplication(one, % 186.22/25.39 | | all_22_4) = all_178_0 & $i(all_178_0) & $i(zero) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (331) implies: % 186.22/25.39 | | (332) $i(all_178_0) % 186.22/25.39 | | (333) multiplication(one, all_22_4) = all_178_0 % 186.22/25.39 | | (334) multiplication(all_22_10, all_178_0) = zero % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (303) with fresh symbol all_180_0 gives: % 186.22/25.39 | | (335) multiplication(all_22_4, all_180_0) = zero & multiplication(one, % 186.22/25.39 | | all_22_10) = all_180_0 & $i(all_180_0) & $i(zero) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (335) implies: % 186.22/25.39 | | (336) $i(all_180_0) % 186.22/25.39 | | (337) multiplication(one, all_22_10) = all_180_0 % 186.22/25.39 | | (338) multiplication(all_22_4, all_180_0) = zero % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (294) with fresh symbol all_182_0 gives: % 186.22/25.39 | | (339) multiplication(one, all_182_0) = all_58_0 & multiplication(one, % 186.22/25.39 | | all_22_9) = all_182_0 & $i(all_182_0) & $i(all_58_0) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (339) implies: % 186.22/25.39 | | (340) multiplication(one, all_22_9) = all_182_0 % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (302) with fresh symbol all_184_0 gives: % 186.22/25.39 | | (341) multiplication(all_22_4, all_184_0) = all_22_3 & % 186.22/25.39 | | multiplication(one, all_22_9) = all_184_0 & $i(all_184_0) & % 186.22/25.39 | | $i(all_22_3) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (341) implies: % 186.22/25.39 | | (342) multiplication(one, all_22_9) = all_184_0 % 186.22/25.39 | | (343) multiplication(all_22_4, all_184_0) = all_22_3 % 186.22/25.39 | | % 186.22/25.39 | | DELTA: instantiating (296) with fresh symbol all_186_0 gives: % 186.22/25.39 | | (344) multiplication(one, all_186_0) = all_82_0 & multiplication(one, % 186.22/25.39 | | all_22_7) = all_186_0 & $i(all_186_0) & $i(all_82_0) % 186.22/25.39 | | % 186.22/25.39 | | ALPHA: (344) implies: % 186.22/25.39 | | (345) multiplication(one, all_22_7) = all_186_0 % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (282), (297) imply: % 186.22/25.39 | | (346) multiplication(one, all_22_7) = all_22_7 % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (281), (295) imply: % 186.22/25.39 | | (347) multiplication(one, all_22_9) = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (297), (309) imply: % 186.22/25.39 | | (348) addition(all_22_7, all_162_0) = one % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (102), (295) imply: % 186.22/25.39 | | (349) addition(all_22_3, all_22_8) = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (89), (295) imply: % 186.22/25.39 | | (350) addition(all_22_6, all_22_9) = all_22_2 % 186.22/25.39 | | % 186.22/25.39 | | REDUCE: (88), (295) imply: % 186.22/25.39 | | (351) addition(all_22_8, all_22_3) = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (8) with all_170_0, all_172_0, all_22_3, % 186.22/25.39 | | all_22_8, simplifying with (321), (323) gives: % 186.22/25.39 | | (352) all_172_0 = all_170_0 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (8) with all_22_9, all_172_0, all_22_3, all_22_8, % 186.22/25.39 | | simplifying with (323), (351) gives: % 186.22/25.39 | | (353) all_172_0 = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (8) with all_22_2, all_176_0, all_22_9, all_22_6, % 186.22/25.39 | | simplifying with (330), (350) gives: % 186.22/25.39 | | (354) all_176_0 = all_22_2 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (8) with all_22_9, all_162_0, all_22_8, all_22_3, % 186.22/25.39 | | simplifying with (308), (349) gives: % 186.22/25.39 | | (355) all_162_0 = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (8) with all_22_4, all_174_0, all_22_3, all_22_1, % 186.22/25.39 | | simplifying with (256), (326) gives: % 186.22/25.39 | | (356) all_174_0 = all_22_4 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_182_0, all_184_0, all_22_9, one, % 186.22/25.39 | | simplifying with (340), (342) gives: % 186.22/25.39 | | (357) all_184_0 = all_182_0 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_166_0, all_184_0, all_22_9, one, % 186.22/25.39 | | simplifying with (315), (342) gives: % 186.22/25.39 | | (358) all_184_0 = all_166_0 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_22_9, all_184_0, all_22_9, one, % 186.22/25.39 | | simplifying with (342), (347) gives: % 186.22/25.39 | | (359) all_184_0 = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_164_0, all_168_0, all_22_7, one, % 186.22/25.39 | | simplifying with (312), (318) gives: % 186.22/25.39 | | (360) all_168_0 = all_164_0 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_168_0, all_186_0, all_22_7, one, % 186.22/25.39 | | simplifying with (318), (345) gives: % 186.22/25.39 | | (361) all_186_0 = all_168_0 % 186.22/25.39 | | % 186.22/25.39 | | GROUND_INST: instantiating (9) with all_22_7, all_186_0, all_22_7, one, % 186.22/25.39 | | simplifying with (345), (346) gives: % 186.22/25.39 | | (362) all_186_0 = all_22_7 % 186.22/25.39 | | % 186.22/25.39 | | COMBINE_EQS: (361), (362) imply: % 186.22/25.39 | | (363) all_168_0 = all_22_7 % 186.22/25.39 | | % 186.22/25.39 | | SIMP: (363) implies: % 186.22/25.39 | | (364) all_168_0 = all_22_7 % 186.22/25.39 | | % 186.22/25.39 | | COMBINE_EQS: (357), (359) imply: % 186.22/25.39 | | (365) all_182_0 = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | COMBINE_EQS: (357), (358) imply: % 186.22/25.39 | | (366) all_182_0 = all_166_0 % 186.22/25.39 | | % 186.22/25.39 | | COMBINE_EQS: (365), (366) imply: % 186.22/25.39 | | (367) all_166_0 = all_22_9 % 186.22/25.39 | | % 186.22/25.39 | | COMBINE_EQS: (352), (353) imply: % 186.22/25.40 | | (368) all_170_0 = all_22_9 % 186.22/25.40 | | % 186.22/25.40 | | SIMP: (368) implies: % 186.22/25.40 | | (369) all_170_0 = all_22_9 % 186.22/25.40 | | % 186.22/25.40 | | COMBINE_EQS: (360), (364) imply: % 186.22/25.41 | | (370) all_164_0 = all_22_7 % 186.22/25.41 | | % 186.22/25.41 | | SIMP: (370) implies: % 186.22/25.41 | | (371) all_164_0 = all_22_7 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (348), (355) imply: % 186.22/25.41 | | (372) addition(all_22_7, all_22_9) = one % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (329), (354) imply: % 186.22/25.41 | | (373) addition(all_22_8, all_22_2) = all_36_0 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (328), (354) imply: % 186.22/25.41 | | (374) $i(all_22_2) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_22_9, % 186.22/25.41 | | all_160_0, simplifying with (14), (15), (305) gives: % 186.22/25.41 | | (375) addition(all_22_9, all_22_8) = all_160_0 & $i(all_160_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (375) implies: % 186.22/25.41 | | (376) addition(all_22_9, all_22_8) = all_160_0 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (additive_commutativity) with all_22_8, all_22_2, % 186.22/25.41 | | all_36_0, simplifying with (15), (373), (374) gives: % 186.22/25.41 | | (377) addition(all_22_2, all_22_8) = all_36_0 & $i(all_36_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (377) implies: % 186.22/25.41 | | (378) addition(all_22_2, all_22_8) = all_36_0 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (additive_associativity) with all_22_10, % 186.22/25.41 | | all_22_8, all_22_3, all_22_9, all_36_0, simplifying with (13), % 186.22/25.41 | | (15), (19), (55), (349) gives: % 186.22/25.41 | | (379) ? [v0: $i] : (addition(all_22_3, v0) = all_36_0 & % 186.22/25.41 | | addition(all_22_8, all_22_10) = v0 & $i(v0) & $i(all_36_0)) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (multiplicative_associativity) with one, one, % 186.22/25.41 | | all_22_10, one, all_180_0, simplifying with (13), (249), (289), % 186.22/25.41 | | (337) gives: % 186.22/25.41 | | (380) ? [v0: $i] : (multiplication(one, v0) = all_180_0 & % 186.22/25.41 | | multiplication(one, all_22_10) = v0 & $i(v0) & $i(all_180_0)) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (2) with all_22_10, all_180_0, simplifying with % 186.22/25.41 | | (13), (337) gives: % 186.22/25.41 | | (381) all_180_0 = all_22_10 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (left_distributivity) with all_22_10, one, % 186.22/25.41 | | all_22_9, all_22_8, all_22_9, all_160_0, simplifying with (13), % 186.22/25.41 | | (14), (24), (289), (305), (347) gives: % 186.22/25.41 | | (382) ? [v0: $i] : (multiplication(v0, all_22_9) = all_160_0 & % 186.22/25.41 | | addition(all_22_10, one) = v0 & $i(v0) & $i(all_160_0)) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (multiplicative_associativity) with one, one, % 186.22/25.41 | | all_22_4, one, all_178_0, simplifying with (18), (249), (289), % 186.22/25.41 | | (333) gives: % 186.22/25.41 | | (383) ? [v0: $i] : (multiplication(one, v0) = all_178_0 & % 186.22/25.41 | | multiplication(one, all_22_4) = v0 & $i(v0) & $i(all_178_0)) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (2) with all_22_4, all_178_0, simplifying with % 186.22/25.41 | | (18), (333) gives: % 186.22/25.41 | | (384) all_178_0 = all_22_4 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_10, % 186.22/25.41 | | one, all_178_0, all_22_10, zero, simplifying with (13), (251), % 186.22/25.41 | | (289), (332), (334) gives: % 186.22/25.41 | | (385) ? [v0: $i] : (multiplication(all_22_10, v0) = zero & % 186.22/25.41 | | multiplication(one, all_178_0) = v0 & $i(v0) & $i(zero)) % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (multiplicative_associativity) with all_22_4, % 186.22/25.41 | | one, all_180_0, all_22_4, zero, simplifying with (18), (250), % 186.22/25.41 | | (289), (336), (338) gives: % 186.22/25.41 | | (386) ? [v0: $i] : (multiplication(all_22_4, v0) = zero & % 186.22/25.41 | | multiplication(one, all_180_0) = v0 & $i(v0) & $i(zero)) % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (385) with fresh symbol all_210_0 gives: % 186.22/25.41 | | (387) multiplication(all_22_10, all_210_0) = zero & multiplication(one, % 186.22/25.41 | | all_178_0) = all_210_0 & $i(all_210_0) & $i(zero) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (387) implies: % 186.22/25.41 | | (388) $i(all_210_0) % 186.22/25.41 | | (389) multiplication(one, all_178_0) = all_210_0 % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (380) with fresh symbol all_212_0 gives: % 186.22/25.41 | | (390) multiplication(one, all_212_0) = all_180_0 & multiplication(one, % 186.22/25.41 | | all_22_10) = all_212_0 & $i(all_212_0) & $i(all_180_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (390) implies: % 186.22/25.41 | | (391) $i(all_212_0) % 186.22/25.41 | | (392) multiplication(one, all_22_10) = all_212_0 % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (379) with fresh symbol all_214_0 gives: % 186.22/25.41 | | (393) addition(all_22_3, all_214_0) = all_36_0 & addition(all_22_8, % 186.22/25.41 | | all_22_10) = all_214_0 & $i(all_214_0) & $i(all_36_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (393) implies: % 186.22/25.41 | | (394) addition(all_22_8, all_22_10) = all_214_0 % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (383) with fresh symbol all_216_0 gives: % 186.22/25.41 | | (395) multiplication(one, all_216_0) = all_178_0 & multiplication(one, % 186.22/25.41 | | all_22_4) = all_216_0 & $i(all_216_0) & $i(all_178_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (395) implies: % 186.22/25.41 | | (396) multiplication(one, all_22_4) = all_216_0 % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (382) with fresh symbol all_218_0 gives: % 186.22/25.41 | | (397) multiplication(all_218_0, all_22_9) = all_160_0 & % 186.22/25.41 | | addition(all_22_10, one) = all_218_0 & $i(all_218_0) & % 186.22/25.41 | | $i(all_160_0) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (397) implies: % 186.22/25.41 | | (398) addition(all_22_10, one) = all_218_0 % 186.22/25.41 | | % 186.22/25.41 | | DELTA: instantiating (386) with fresh symbol all_224_0 gives: % 186.22/25.41 | | (399) multiplication(all_22_4, all_224_0) = zero & multiplication(one, % 186.22/25.41 | | all_180_0) = all_224_0 & $i(all_224_0) & $i(zero) % 186.22/25.41 | | % 186.22/25.41 | | ALPHA: (399) implies: % 186.22/25.41 | | (400) multiplication(one, all_180_0) = all_224_0 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (381), (400) imply: % 186.22/25.41 | | (401) multiplication(one, all_22_10) = all_224_0 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (384), (389) imply: % 186.22/25.41 | | (402) multiplication(one, all_22_4) = all_210_0 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (333), (384) imply: % 186.22/25.41 | | (403) multiplication(one, all_22_4) = all_22_4 % 186.22/25.41 | | % 186.22/25.41 | | REDUCE: (337), (381) imply: % 186.22/25.41 | | (404) multiplication(one, all_22_10) = all_22_10 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (9) with all_212_0, all_224_0, all_22_10, one, % 186.22/25.41 | | simplifying with (392), (401) gives: % 186.22/25.41 | | (405) all_224_0 = all_212_0 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (9) with all_22_10, all_224_0, all_22_10, one, % 186.22/25.41 | | simplifying with (401), (404) gives: % 186.22/25.41 | | (406) all_224_0 = all_22_10 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (9) with all_210_0, all_216_0, all_22_4, one, % 186.22/25.41 | | simplifying with (396), (402) gives: % 186.22/25.41 | | (407) all_216_0 = all_210_0 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (9) with all_22_4, all_216_0, all_22_4, one, % 186.22/25.41 | | simplifying with (396), (403) gives: % 186.22/25.41 | | (408) all_216_0 = all_22_4 % 186.22/25.41 | | % 186.22/25.41 | | COMBINE_EQS: (405), (406) imply: % 186.22/25.41 | | (409) all_212_0 = all_22_10 % 186.22/25.41 | | % 186.22/25.41 | | SIMP: (409) implies: % 186.22/25.41 | | (410) all_212_0 = all_22_10 % 186.22/25.41 | | % 186.22/25.41 | | COMBINE_EQS: (407), (408) imply: % 186.22/25.41 | | (411) all_210_0 = all_22_4 % 186.22/25.41 | | % 186.22/25.41 | | SIMP: (411) implies: % 186.22/25.41 | | (412) all_210_0 = all_22_4 % 186.22/25.41 | | % 186.22/25.41 | | GROUND_INST: instantiating (left_distributivity) with all_22_10, one, one, % 186.22/25.41 | | all_22_10, one, all_218_0, simplifying with (13), (249), (251), % 186.22/25.41 | | (289), (398) gives: % 186.22/25.42 | | (413) ? [v0: $i] : (multiplication(v0, one) = all_218_0 & % 186.22/25.42 | | addition(all_22_10, one) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_associativity) with one, all_22_8, % 186.22/25.42 | | all_22_6, all_22_10, all_218_0, simplifying with (15), (17), % 186.22/25.42 | | (263), (289), (398) gives: % 186.22/25.42 | | (414) ? [v0: $i] : (addition(all_22_6, v0) = all_218_0 & % 186.22/25.42 | | addition(all_22_8, one) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_commutativity) with all_22_10, one, % 186.22/25.42 | | all_218_0, simplifying with (13), (289), (398) gives: % 186.22/25.42 | | (415) addition(one, all_22_10) = all_218_0 & $i(all_218_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (415) implies: % 186.22/25.42 | | (416) addition(one, all_22_10) = all_218_0 % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (left_distributivity) with one, all_22_10, % 186.22/25.42 | | all_22_9, all_22_9, all_22_8, all_160_0, simplifying with (13), % 186.22/25.42 | | (14), (24), (289), (347), (376) gives: % 186.22/25.42 | | (417) ? [v0: $i] : (multiplication(v0, all_22_9) = all_160_0 & % 186.22/25.42 | | addition(one, all_22_10) = v0 & $i(v0) & $i(all_160_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_8, % 186.22/25.42 | | all_22_3, all_22_9, all_160_0, simplifying with (15), (19), % 186.22/25.42 | | (349), (376) gives: % 186.22/25.42 | | (418) ? [v0: $i] : (addition(all_22_3, v0) = all_160_0 & % 186.22/25.42 | | addition(all_22_8, all_22_8) = v0 & $i(v0) & $i(all_160_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_22_9, % 186.22/25.42 | | one, all_22_8, all_22_10, all_214_0, simplifying with (13), % 186.22/25.42 | | (14), (24), (251), (289), (394) gives: % 186.22/25.42 | | (419) ? [v0: $i] : (multiplication(all_22_10, v0) = all_214_0 & % 186.22/25.42 | | addition(all_22_9, one) = v0 & $i(v0) & $i(all_214_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_commutativity) with all_22_8, % 186.22/25.42 | | all_22_10, all_214_0, simplifying with (13), (15), (394) gives: % 186.22/25.42 | | (420) addition(all_22_10, all_22_8) = all_214_0 & $i(all_214_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (420) implies: % 186.22/25.42 | | (421) addition(all_22_10, all_22_8) = all_214_0 % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_8, % 186.22/25.42 | | all_34_0, all_22_2, all_36_0, simplifying with (15), (43), % 186.22/25.42 | | (60), (378) gives: % 186.22/25.42 | | (422) ? [v0: $i] : (addition(all_34_0, v0) = all_36_0 & % 186.22/25.42 | | addition(all_22_8, all_22_8) = v0 & $i(v0) & $i(all_36_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, % 186.22/25.42 | | all_22_10, all_22_3, all_22_2, all_36_0, simplifying with (13), % 186.22/25.42 | | (15), (19), (261), (378) gives: % 186.22/25.42 | | (423) ? [v0: $i] : (addition(all_22_3, v0) = all_36_0 & % 186.22/25.42 | | addition(all_22_10, all_22_8) = v0 & $i(v0) & $i(all_36_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.22/25.42 | | all_22_10, all_22_7, all_22_10, all_22_6, simplifying with % 186.22/25.42 | | (13), (16), (25), (289), (404) gives: % 186.22/25.42 | | (424) ? [v0: $i] : (multiplication(all_22_10, all_22_7) = v0 & % 186.22/25.42 | | multiplication(one, v0) = all_22_6 & $i(v0) & $i(all_22_6)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.22/25.42 | | all_22_10, all_22_9, all_22_10, all_22_8, simplifying with % 186.22/25.42 | | (13), (14), (24), (289), (404) gives: % 186.22/25.42 | | (425) ? [v0: $i] : (multiplication(all_22_10, all_22_9) = v0 & % 186.22/25.42 | | multiplication(one, v0) = all_22_8 & $i(v0) & $i(all_22_8)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_10, one, % 186.22/25.42 | | all_22_10, one, all_218_0, simplifying with (13), (249), (289), % 186.22/25.42 | | (398), (404) gives: % 186.22/25.42 | | (426) ? [v0: $i] : (multiplication(one, v0) = all_218_0 & % 186.22/25.42 | | addition(all_22_10, one) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.22/25.42 | | all_22_4, all_22_7, all_22_4, all_22_1, simplifying with (16), % 186.22/25.42 | | (18), (27), (289), (403) gives: % 186.22/25.42 | | (427) ? [v0: $i] : (multiplication(all_22_4, all_22_7) = v0 & % 186.22/25.42 | | multiplication(one, v0) = all_22_1 & $i(v0) & $i(all_22_1)) % 186.22/25.42 | | % 186.22/25.42 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.22/25.42 | | all_22_4, all_22_9, all_22_4, all_22_3, simplifying with (14), % 186.22/25.42 | | (18), (26), (289), (403) gives: % 186.22/25.42 | | (428) ? [v0: $i] : (multiplication(all_22_4, all_22_9) = v0 & % 186.22/25.42 | | multiplication(one, v0) = all_22_3 & $i(v0) & $i(all_22_3)) % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (428) with fresh symbol all_236_0 gives: % 186.22/25.42 | | (429) multiplication(all_22_4, all_22_9) = all_236_0 & % 186.22/25.42 | | multiplication(one, all_236_0) = all_22_3 & $i(all_236_0) & % 186.22/25.42 | | $i(all_22_3) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (429) implies: % 186.22/25.42 | | (430) $i(all_236_0) % 186.22/25.42 | | (431) multiplication(one, all_236_0) = all_22_3 % 186.22/25.42 | | (432) multiplication(all_22_4, all_22_9) = all_236_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (427) with fresh symbol all_238_0 gives: % 186.22/25.42 | | (433) multiplication(all_22_4, all_22_7) = all_238_0 & % 186.22/25.42 | | multiplication(one, all_238_0) = all_22_1 & $i(all_238_0) & % 186.22/25.42 | | $i(all_22_1) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (433) implies: % 186.22/25.42 | | (434) $i(all_238_0) % 186.22/25.42 | | (435) multiplication(one, all_238_0) = all_22_1 % 186.22/25.42 | | (436) multiplication(all_22_4, all_22_7) = all_238_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (426) with fresh symbol all_240_0 gives: % 186.22/25.42 | | (437) multiplication(one, all_240_0) = all_218_0 & addition(all_22_10, % 186.22/25.42 | | one) = all_240_0 & $i(all_240_0) & $i(all_218_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (437) implies: % 186.22/25.42 | | (438) addition(all_22_10, one) = all_240_0 % 186.22/25.42 | | (439) multiplication(one, all_240_0) = all_218_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (423) with fresh symbol all_242_0 gives: % 186.22/25.42 | | (440) addition(all_22_3, all_242_0) = all_36_0 & addition(all_22_10, % 186.22/25.42 | | all_22_8) = all_242_0 & $i(all_242_0) & $i(all_36_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (440) implies: % 186.22/25.42 | | (441) addition(all_22_10, all_22_8) = all_242_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (422) with fresh symbol all_244_0 gives: % 186.22/25.42 | | (442) addition(all_34_0, all_244_0) = all_36_0 & addition(all_22_8, % 186.22/25.42 | | all_22_8) = all_244_0 & $i(all_244_0) & $i(all_36_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (442) implies: % 186.22/25.42 | | (443) addition(all_22_8, all_22_8) = all_244_0 % 186.22/25.42 | | (444) addition(all_34_0, all_244_0) = all_36_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (425) with fresh symbol all_248_0 gives: % 186.22/25.42 | | (445) multiplication(all_22_10, all_22_9) = all_248_0 & % 186.22/25.42 | | multiplication(one, all_248_0) = all_22_8 & $i(all_248_0) & % 186.22/25.42 | | $i(all_22_8) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (445) implies: % 186.22/25.42 | | (446) $i(all_248_0) % 186.22/25.42 | | (447) multiplication(one, all_248_0) = all_22_8 % 186.22/25.42 | | (448) multiplication(all_22_10, all_22_9) = all_248_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (417) with fresh symbol all_252_0 gives: % 186.22/25.42 | | (449) multiplication(all_252_0, all_22_9) = all_160_0 & addition(one, % 186.22/25.42 | | all_22_10) = all_252_0 & $i(all_252_0) & $i(all_160_0) % 186.22/25.42 | | % 186.22/25.42 | | ALPHA: (449) implies: % 186.22/25.42 | | (450) addition(one, all_22_10) = all_252_0 % 186.22/25.42 | | (451) multiplication(all_252_0, all_22_9) = all_160_0 % 186.22/25.42 | | % 186.22/25.42 | | DELTA: instantiating (413) with fresh symbol all_254_0 gives: % 186.22/25.43 | | (452) multiplication(all_254_0, one) = all_218_0 & addition(all_22_10, % 186.22/25.43 | | one) = all_254_0 & $i(all_254_0) & $i(all_218_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (452) implies: % 186.22/25.43 | | (453) addition(all_22_10, one) = all_254_0 % 186.22/25.43 | | % 186.22/25.43 | | DELTA: instantiating (414) with fresh symbol all_256_0 gives: % 186.22/25.43 | | (454) addition(all_22_6, all_256_0) = all_218_0 & addition(all_22_8, one) % 186.22/25.43 | | = all_256_0 & $i(all_256_0) & $i(all_218_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (454) implies: % 186.22/25.43 | | (455) addition(all_22_8, one) = all_256_0 % 186.22/25.43 | | (456) addition(all_22_6, all_256_0) = all_218_0 % 186.22/25.43 | | % 186.22/25.43 | | DELTA: instantiating (424) with fresh symbol all_258_0 gives: % 186.22/25.43 | | (457) multiplication(all_22_10, all_22_7) = all_258_0 & % 186.22/25.43 | | multiplication(one, all_258_0) = all_22_6 & $i(all_258_0) & % 186.22/25.43 | | $i(all_22_6) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (457) implies: % 186.22/25.43 | | (458) $i(all_258_0) % 186.22/25.43 | | (459) multiplication(one, all_258_0) = all_22_6 % 186.22/25.43 | | (460) multiplication(all_22_10, all_22_7) = all_258_0 % 186.22/25.43 | | % 186.22/25.43 | | DELTA: instantiating (419) with fresh symbol all_262_0 gives: % 186.22/25.43 | | (461) multiplication(all_22_10, all_262_0) = all_214_0 & % 186.22/25.43 | | addition(all_22_9, one) = all_262_0 & $i(all_262_0) & $i(all_214_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (461) implies: % 186.22/25.43 | | (462) addition(all_22_9, one) = all_262_0 % 186.22/25.43 | | (463) multiplication(all_22_10, all_262_0) = all_214_0 % 186.22/25.43 | | % 186.22/25.43 | | DELTA: instantiating (418) with fresh symbol all_264_0 gives: % 186.22/25.43 | | (464) addition(all_22_3, all_264_0) = all_160_0 & addition(all_22_8, % 186.22/25.43 | | all_22_8) = all_264_0 & $i(all_264_0) & $i(all_160_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (464) implies: % 186.22/25.43 | | (465) $i(all_264_0) % 186.22/25.43 | | (466) addition(all_22_8, all_22_8) = all_264_0 % 186.22/25.43 | | (467) addition(all_22_3, all_264_0) = all_160_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (8) with all_218_0, all_252_0, all_22_10, one, % 186.22/25.43 | | simplifying with (416), (450) gives: % 186.22/25.43 | | (468) all_252_0 = all_218_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (8) with all_218_0, all_254_0, one, all_22_10, % 186.22/25.43 | | simplifying with (398), (453) gives: % 186.22/25.43 | | (469) all_254_0 = all_218_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (8) with all_240_0, all_254_0, one, all_22_10, % 186.22/25.43 | | simplifying with (438), (453) gives: % 186.22/25.43 | | (470) all_254_0 = all_240_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (8) with all_214_0, all_242_0, all_22_8, % 186.22/25.43 | | all_22_10, simplifying with (421), (441) gives: % 186.22/25.43 | | (471) all_242_0 = all_214_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (8) with all_244_0, all_264_0, all_22_8, % 186.22/25.43 | | all_22_8, simplifying with (443), (466) gives: % 186.22/25.43 | | (472) all_264_0 = all_244_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (9) with all_22_8, all_248_0, all_22_9, % 186.22/25.43 | | all_22_10, simplifying with (24), (448) gives: % 186.22/25.43 | | (473) all_248_0 = all_22_8 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (9) with all_22_6, all_258_0, all_22_7, % 186.22/25.43 | | all_22_10, simplifying with (25), (460) gives: % 186.22/25.43 | | (474) all_258_0 = all_22_6 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (9) with all_22_3, all_236_0, all_22_9, all_22_4, % 186.22/25.43 | | simplifying with (26), (432) gives: % 186.22/25.43 | | (475) all_236_0 = all_22_3 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (9) with all_22_1, all_238_0, all_22_7, all_22_4, % 186.22/25.43 | | simplifying with (27), (436) gives: % 186.22/25.43 | | (476) all_238_0 = all_22_1 % 186.22/25.43 | | % 186.22/25.43 | | COMBINE_EQS: (469), (470) imply: % 186.22/25.43 | | (477) all_240_0 = all_218_0 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (451), (468) imply: % 186.22/25.43 | | (478) multiplication(all_218_0, all_22_9) = all_160_0 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (459), (474) imply: % 186.22/25.43 | | (479) multiplication(one, all_22_6) = all_22_6 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (447), (473) imply: % 186.22/25.43 | | (480) multiplication(one, all_22_8) = all_22_8 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (439), (477) imply: % 186.22/25.43 | | (481) multiplication(one, all_218_0) = all_218_0 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (435), (476) imply: % 186.22/25.43 | | (482) multiplication(one, all_22_1) = all_22_1 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (431), (475) imply: % 186.22/25.43 | | (483) multiplication(one, all_22_3) = all_22_3 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (467), (472) imply: % 186.22/25.43 | | (484) addition(all_22_3, all_244_0) = all_160_0 % 186.22/25.43 | | % 186.22/25.43 | | REDUCE: (465), (472) imply: % 186.22/25.43 | | (485) $i(all_244_0) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with all_22_10, % 186.22/25.43 | | all_34_0, all_80_0, one, all_218_0, simplifying with (13), % 186.22/25.43 | | (43), (182), (252), (416) gives: % 186.22/25.43 | | (486) ? [v0: $i] : (addition(all_80_0, v0) = all_218_0 & % 186.22/25.43 | | addition(all_34_0, all_22_10) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with all_22_10, % 186.22/25.43 | | all_22_8, all_50_0, one, all_218_0, simplifying with (13), % 186.22/25.43 | | (15), (255), (285), (416) gives: % 186.22/25.43 | | (487) ? [v0: $i] : (addition(all_50_0, v0) = all_218_0 & % 186.22/25.43 | | addition(all_22_8, all_22_10) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with all_22_10, % 186.22/25.43 | | all_22_1, all_22_2, one, all_218_0, simplifying with (13), % 186.22/25.43 | | (20), (258), (374), (416) gives: % 186.22/25.43 | | (488) ? [v0: $i] : (addition(all_22_1, all_22_10) = v0 & % 186.22/25.43 | | addition(all_22_2, v0) = all_218_0 & $i(v0) & $i(all_218_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with all_22_10, % 186.22/25.43 | | all_22_10, all_22_4, one, all_218_0, simplifying with (13), % 186.22/25.43 | | (18), (262), (416) gives: % 186.22/25.43 | | (489) ? [v0: $i] : (addition(all_22_4, v0) = all_218_0 & % 186.22/25.43 | | addition(all_22_10, all_22_10) = v0 & $i(v0) & $i(all_218_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, one, % 186.22/25.43 | | all_22_9, all_22_10, all_22_8, all_214_0, simplifying with % 186.22/25.43 | | (13), (14), (24), (251), (289), (421) gives: % 186.22/25.43 | | (490) ? [v0: $i] : (multiplication(all_22_10, v0) = all_214_0 & % 186.22/25.43 | | addition(one, all_22_9) = v0 & $i(v0) & $i(all_214_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_8, % 186.22/25.43 | | all_22_6, all_22_10, all_214_0, simplifying with (15), (17), % 186.22/25.43 | | (263), (421) gives: % 186.22/25.43 | | (491) ? [v0: $i] : (addition(all_22_6, v0) = all_214_0 & % 186.22/25.43 | | addition(all_22_8, all_22_8) = v0 & $i(v0) & $i(all_214_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with one, all_22_8, % 186.22/25.43 | | all_22_3, all_22_9, all_262_0, simplifying with (15), (19), % 186.22/25.43 | | (289), (349), (462) gives: % 186.22/25.43 | | (492) ? [v0: $i] : (addition(all_22_3, v0) = all_262_0 & % 186.22/25.43 | | addition(all_22_8, one) = v0 & $i(v0) & $i(all_262_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_associativity) with one, all_22_3, % 186.22/25.43 | | all_22_8, all_22_9, all_262_0, simplifying with (15), (19), % 186.22/25.43 | | (289), (351), (462) gives: % 186.22/25.43 | | (493) ? [v0: $i] : (addition(all_22_3, one) = v0 & addition(all_22_8, % 186.22/25.43 | | v0) = all_262_0 & $i(v0) & $i(all_262_0)) % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_commutativity) with all_22_9, one, % 186.22/25.43 | | all_262_0, simplifying with (14), (289), (462) gives: % 186.22/25.43 | | (494) addition(one, all_22_9) = all_262_0 & $i(all_262_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (494) implies: % 186.22/25.43 | | (495) $i(all_262_0) % 186.22/25.43 | | (496) addition(one, all_22_9) = all_262_0 % 186.22/25.43 | | % 186.22/25.43 | | GROUND_INST: instantiating (additive_commutativity) with all_22_8, one, % 186.22/25.43 | | all_256_0, simplifying with (15), (289), (455) gives: % 186.22/25.43 | | (497) addition(one, all_22_8) = all_256_0 & $i(all_256_0) % 186.22/25.43 | | % 186.22/25.43 | | ALPHA: (497) implies: % 186.22/25.43 | | (498) $i(all_256_0) % 186.22/25.43 | | (499) addition(one, all_22_8) = all_256_0 % 186.22/25.43 | | % 186.22/25.44 | | GROUND_INST: instantiating (left_distributivity) with all_22_10, all_22_10, % 186.22/25.44 | | all_22_9, all_22_8, all_22_8, all_244_0, simplifying with (13), % 186.22/25.44 | | (14), (24), (443) gives: % 186.22/25.44 | | (500) ? [v0: $i] : (multiplication(v0, all_22_9) = all_244_0 & % 186.22/25.44 | | addition(all_22_10, all_22_10) = v0 & $i(v0) & $i(all_244_0)) % 186.22/25.44 | | % 186.22/25.44 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_22_9, % 186.22/25.44 | | all_22_9, all_22_8, all_22_8, all_244_0, simplifying with (13), % 186.22/25.44 | | (14), (24), (443) gives: % 186.22/25.44 | | (501) ? [v0: $i] : (multiplication(all_22_10, v0) = all_244_0 & % 186.22/25.44 | | addition(all_22_9, all_22_9) = v0 & $i(v0) & $i(all_244_0)) % 186.22/25.44 | | % 186.22/25.44 | | GROUND_INST: instantiating (additive_idempotence) with all_22_8, all_244_0, % 186.22/25.44 | | simplifying with (15), (443) gives: % 186.22/25.44 | | (502) all_244_0 = all_22_8 % 186.22/25.44 | | % 186.22/25.44 | | GROUND_INST: instantiating (additive_commutativity) with all_22_6, % 186.22/25.44 | | all_256_0, all_218_0, simplifying with (17), (456), (498) % 186.22/25.44 | | gives: % 186.22/25.44 | | (503) addition(all_256_0, all_22_6) = all_218_0 & $i(all_218_0) % 186.22/25.44 | | % 186.22/25.44 | | ALPHA: (503) implies: % 186.22/25.44 | | (504) $i(all_218_0) % 186.22/25.44 | | % 186.22/25.44 | | GROUND_INST: instantiating (additive_commutativity) with all_22_3, % 186.22/25.44 | | all_244_0, all_160_0, simplifying with (19), (484), (485) % 186.22/25.44 | | gives: % 186.22/25.44 | | (505) addition(all_244_0, all_22_3) = all_160_0 & $i(all_160_0) % 186.22/25.44 | | % 186.22/25.44 | | ALPHA: (505) implies: % 186.22/25.44 | | (506) addition(all_244_0, all_22_3) = all_160_0 % 186.22/25.44 | | % 186.22/25.44 | | GROUND_INST: instantiating (additive_associativity) with all_244_0, % 186.22/25.44 | | all_22_6, all_22_3, all_34_0, all_36_0, simplifying with (17), % 186.22/25.44 | | (19), (64), (444), (485) gives: % 186.66/25.44 | | (507) ? [v0: $i] : (addition(all_22_3, v0) = all_36_0 & % 186.66/25.44 | | addition(all_22_6, all_244_0) = v0 & $i(v0) & $i(all_36_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_9, % 186.66/25.44 | | all_22_8, all_22_9, all_22_8, all_160_0, simplifying with (14), % 186.66/25.44 | | (15), (289), (347), (376), (480) gives: % 186.66/25.44 | | (508) ? [v0: $i] : (multiplication(one, v0) = all_160_0 & % 186.66/25.44 | | addition(all_22_9, all_22_8) = v0 & $i(v0) & $i(all_160_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_8, % 186.66/25.44 | | all_22_10, all_22_8, all_22_10, all_214_0, simplifying with % 186.66/25.44 | | (13), (15), (289), (394), (404), (480) gives: % 186.66/25.44 | | (509) ? [v0: $i] : (multiplication(one, v0) = all_214_0 & % 186.66/25.44 | | addition(all_22_8, all_22_10) = v0 & $i(v0) & $i(all_214_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_8, one, % 186.66/25.44 | | all_22_8, one, all_256_0, simplifying with (15), (249), (289), % 186.66/25.44 | | (455), (480) gives: % 186.66/25.44 | | (510) ? [v0: $i] : (multiplication(one, v0) = all_256_0 & % 186.66/25.44 | | addition(all_22_8, one) = v0 & $i(v0) & $i(all_256_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (left_distributivity) with one, one, all_22_8, % 186.66/25.44 | | all_22_8, all_22_8, all_244_0, simplifying with (15), (289), % 186.66/25.44 | | (443), (480) gives: % 186.66/25.44 | | (511) ? [v0: $i] : (multiplication(v0, all_22_8) = all_244_0 & % 186.66/25.44 | | addition(one, one) = v0 & $i(v0) & $i(all_244_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_8, % 186.66/25.44 | | all_22_8, all_22_8, all_22_8, all_244_0, simplifying with (15), % 186.66/25.44 | | (289), (443), (480) gives: % 186.66/25.44 | | (512) ? [v0: $i] : (multiplication(one, v0) = all_244_0 & % 186.66/25.44 | | addition(all_22_8, all_22_8) = v0 & $i(v0) & $i(all_244_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_3, % 186.66/25.44 | | all_22_6, all_22_3, all_22_6, all_34_0, simplifying with (17), % 186.66/25.44 | | (19), (64), (289), (479), (483) gives: % 186.66/25.44 | | (513) ? [v0: $i] : (multiplication(one, v0) = all_34_0 & % 186.66/25.44 | | addition(all_22_3, all_22_6) = v0 & $i(v0) & $i(all_34_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_1, % 186.66/25.44 | | all_22_10, all_22_1, all_22_10, all_56_0, simplifying with % 186.66/25.44 | | (13), (20), (257), (289), (404), (482) gives: % 186.66/25.44 | | (514) ? [v0: $i] : (multiplication(one, v0) = all_56_0 & % 186.66/25.44 | | addition(all_22_1, all_22_10) = v0 & $i(v0) & $i(all_56_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_8, % 186.66/25.44 | | all_22_1, all_22_8, all_22_1, all_80_0, simplifying with (15), % 186.66/25.44 | | (20), (132), (289), (480), (482) gives: % 186.66/25.44 | | (515) ? [v0: $i] : (multiplication(one, v0) = all_80_0 & % 186.66/25.44 | | addition(all_22_8, all_22_1) = v0 & $i(v0) & $i(all_80_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.66/25.44 | | all_218_0, all_22_9, all_218_0, all_160_0, simplifying with % 186.66/25.44 | | (14), (289), (478), (481), (504) gives: % 186.66/25.44 | | (516) ? [v0: $i] : (multiplication(all_218_0, all_22_9) = v0 & % 186.66/25.44 | | multiplication(one, v0) = all_160_0 & $i(v0) & $i(all_160_0)) % 186.66/25.44 | | % 186.66/25.44 | | GROUND_INST: instantiating (multiplicative_associativity) with one, % 186.66/25.44 | | all_22_10, all_262_0, all_22_10, all_214_0, simplifying with % 186.66/25.44 | | (13), (289), (404), (463), (495) gives: % 186.66/25.44 | | (517) ? [v0: $i] : (multiplication(all_22_10, all_262_0) = v0 & % 186.66/25.44 | | multiplication(one, v0) = all_214_0 & $i(v0) & $i(all_214_0)) % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (507) with fresh symbol all_278_0 gives: % 186.66/25.44 | | (518) addition(all_22_3, all_278_0) = all_36_0 & addition(all_22_6, % 186.66/25.44 | | all_244_0) = all_278_0 & $i(all_278_0) & $i(all_36_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (518) implies: % 186.66/25.44 | | (519) addition(all_22_6, all_244_0) = all_278_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (517) with fresh symbol all_280_0 gives: % 186.66/25.44 | | (520) multiplication(all_22_10, all_262_0) = all_280_0 & % 186.66/25.44 | | multiplication(one, all_280_0) = all_214_0 & $i(all_280_0) & % 186.66/25.44 | | $i(all_214_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (520) implies: % 186.66/25.44 | | (521) $i(all_280_0) % 186.66/25.44 | | (522) multiplication(one, all_280_0) = all_214_0 % 186.66/25.44 | | (523) multiplication(all_22_10, all_262_0) = all_280_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (514) with fresh symbol all_284_0 gives: % 186.66/25.44 | | (524) multiplication(one, all_284_0) = all_56_0 & addition(all_22_1, % 186.66/25.44 | | all_22_10) = all_284_0 & $i(all_284_0) & $i(all_56_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (524) implies: % 186.66/25.44 | | (525) $i(all_284_0) % 186.66/25.44 | | (526) addition(all_22_1, all_22_10) = all_284_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (513) with fresh symbol all_288_0 gives: % 186.66/25.44 | | (527) multiplication(one, all_288_0) = all_34_0 & addition(all_22_3, % 186.66/25.44 | | all_22_6) = all_288_0 & $i(all_288_0) & $i(all_34_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (527) implies: % 186.66/25.44 | | (528) $i(all_288_0) % 186.66/25.44 | | (529) addition(all_22_3, all_22_6) = all_288_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (491) with fresh symbol all_294_0 gives: % 186.66/25.44 | | (530) addition(all_22_6, all_294_0) = all_214_0 & addition(all_22_8, % 186.66/25.44 | | all_22_8) = all_294_0 & $i(all_294_0) & $i(all_214_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (530) implies: % 186.66/25.44 | | (531) $i(all_294_0) % 186.66/25.44 | | (532) addition(all_22_8, all_22_8) = all_294_0 % 186.66/25.44 | | (533) addition(all_22_6, all_294_0) = all_214_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (490) with fresh symbol all_296_0 gives: % 186.66/25.44 | | (534) multiplication(all_22_10, all_296_0) = all_214_0 & addition(one, % 186.66/25.44 | | all_22_9) = all_296_0 & $i(all_296_0) & $i(all_214_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (534) implies: % 186.66/25.44 | | (535) addition(one, all_22_9) = all_296_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (489) with fresh symbol all_300_0 gives: % 186.66/25.44 | | (536) addition(all_22_4, all_300_0) = all_218_0 & addition(all_22_10, % 186.66/25.44 | | all_22_10) = all_300_0 & $i(all_300_0) & $i(all_218_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (536) implies: % 186.66/25.44 | | (537) addition(all_22_10, all_22_10) = all_300_0 % 186.66/25.44 | | (538) addition(all_22_4, all_300_0) = all_218_0 % 186.66/25.44 | | % 186.66/25.44 | | DELTA: instantiating (512) with fresh symbol all_326_0 gives: % 186.66/25.44 | | (539) multiplication(one, all_326_0) = all_244_0 & addition(all_22_8, % 186.66/25.44 | | all_22_8) = all_326_0 & $i(all_326_0) & $i(all_244_0) % 186.66/25.44 | | % 186.66/25.44 | | ALPHA: (539) implies: % 186.66/25.45 | | (540) addition(all_22_8, all_22_8) = all_326_0 % 186.66/25.45 | | (541) multiplication(one, all_326_0) = all_244_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (487) with fresh symbol all_328_0 gives: % 186.66/25.45 | | (542) addition(all_50_0, all_328_0) = all_218_0 & addition(all_22_8, % 186.66/25.45 | | all_22_10) = all_328_0 & $i(all_328_0) & $i(all_218_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (542) implies: % 186.66/25.45 | | (543) addition(all_22_8, all_22_10) = all_328_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (510) with fresh symbol all_332_0 gives: % 186.66/25.45 | | (544) multiplication(one, all_332_0) = all_256_0 & addition(all_22_8, % 186.66/25.45 | | one) = all_332_0 & $i(all_332_0) & $i(all_256_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (544) implies: % 186.66/25.45 | | (545) $i(all_332_0) % 186.66/25.45 | | (546) addition(all_22_8, one) = all_332_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (509) with fresh symbol all_334_0 gives: % 186.66/25.45 | | (547) multiplication(one, all_334_0) = all_214_0 & addition(all_22_8, % 186.66/25.45 | | all_22_10) = all_334_0 & $i(all_334_0) & $i(all_214_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (547) implies: % 186.66/25.45 | | (548) addition(all_22_8, all_22_10) = all_334_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (508) with fresh symbol all_336_0 gives: % 186.66/25.45 | | (549) multiplication(one, all_336_0) = all_160_0 & addition(all_22_9, % 186.66/25.45 | | all_22_8) = all_336_0 & $i(all_336_0) & $i(all_160_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (549) implies: % 186.66/25.45 | | (550) addition(all_22_9, all_22_8) = all_336_0 % 186.66/25.45 | | (551) multiplication(one, all_336_0) = all_160_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (511) with fresh symbol all_352_0 gives: % 186.66/25.45 | | (552) multiplication(all_352_0, all_22_8) = all_244_0 & addition(one, % 186.66/25.45 | | one) = all_352_0 & $i(all_352_0) & $i(all_244_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (552) implies: % 186.66/25.45 | | (553) $i(all_352_0) % 186.66/25.45 | | (554) addition(one, one) = all_352_0 % 186.66/25.45 | | (555) multiplication(all_352_0, all_22_8) = all_244_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (516) with fresh symbol all_356_0 gives: % 186.66/25.45 | | (556) multiplication(all_218_0, all_22_9) = all_356_0 & % 186.66/25.45 | | multiplication(one, all_356_0) = all_160_0 & $i(all_356_0) & % 186.66/25.45 | | $i(all_160_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (556) implies: % 186.66/25.45 | | (557) $i(all_160_0) % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (515) with fresh symbol all_358_0 gives: % 186.66/25.45 | | (558) multiplication(one, all_358_0) = all_80_0 & addition(all_22_8, % 186.66/25.45 | | all_22_1) = all_358_0 & $i(all_358_0) & $i(all_80_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (558) implies: % 186.66/25.45 | | (559) $i(all_358_0) % 186.66/25.45 | | (560) addition(all_22_8, all_22_1) = all_358_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (488) with fresh symbol all_360_0 gives: % 186.66/25.45 | | (561) addition(all_22_1, all_22_10) = all_360_0 & addition(all_22_2, % 186.66/25.45 | | all_360_0) = all_218_0 & $i(all_360_0) & $i(all_218_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (561) implies: % 186.66/25.45 | | (562) addition(all_22_1, all_22_10) = all_360_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (486) with fresh symbol all_366_0 gives: % 186.66/25.45 | | (563) addition(all_80_0, all_366_0) = all_218_0 & addition(all_34_0, % 186.66/25.45 | | all_22_10) = all_366_0 & $i(all_366_0) & $i(all_218_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (563) implies: % 186.66/25.45 | | (564) addition(all_34_0, all_22_10) = all_366_0 % 186.66/25.45 | | (565) addition(all_80_0, all_366_0) = all_218_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (492) with fresh symbol all_368_0 gives: % 186.66/25.45 | | (566) addition(all_22_3, all_368_0) = all_262_0 & addition(all_22_8, one) % 186.66/25.45 | | = all_368_0 & $i(all_368_0) & $i(all_262_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (566) implies: % 186.66/25.45 | | (567) addition(all_22_8, one) = all_368_0 % 186.66/25.45 | | (568) addition(all_22_3, all_368_0) = all_262_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (501) with fresh symbol all_378_0 gives: % 186.66/25.45 | | (569) multiplication(all_22_10, all_378_0) = all_244_0 & % 186.66/25.45 | | addition(all_22_9, all_22_9) = all_378_0 & $i(all_378_0) & % 186.66/25.45 | | $i(all_244_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (569) implies: % 186.66/25.45 | | (570) $i(all_378_0) % 186.66/25.45 | | (571) addition(all_22_9, all_22_9) = all_378_0 % 186.66/25.45 | | (572) multiplication(all_22_10, all_378_0) = all_244_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (493) with fresh symbol all_380_0 gives: % 186.66/25.45 | | (573) addition(all_22_3, one) = all_380_0 & addition(all_22_8, all_380_0) % 186.66/25.45 | | = all_262_0 & $i(all_380_0) & $i(all_262_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (573) implies: % 186.66/25.45 | | (574) addition(all_22_3, one) = all_380_0 % 186.66/25.45 | | % 186.66/25.45 | | DELTA: instantiating (500) with fresh symbol all_382_0 gives: % 186.66/25.45 | | (575) multiplication(all_382_0, all_22_9) = all_244_0 & % 186.66/25.45 | | addition(all_22_10, all_22_10) = all_382_0 & $i(all_382_0) & % 186.66/25.45 | | $i(all_244_0) % 186.66/25.45 | | % 186.66/25.45 | | ALPHA: (575) implies: % 186.66/25.45 | | (576) $i(all_382_0) % 186.66/25.45 | | (577) addition(all_22_10, all_22_10) = all_382_0 % 186.66/25.45 | | (578) multiplication(all_382_0, all_22_9) = all_244_0 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (578) imply: % 186.66/25.45 | | (579) multiplication(all_382_0, all_22_9) = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (555) imply: % 186.66/25.45 | | (580) multiplication(all_352_0, all_22_8) = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (572) imply: % 186.66/25.45 | | (581) multiplication(all_22_10, all_378_0) = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (541) imply: % 186.66/25.45 | | (582) multiplication(one, all_326_0) = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (506) imply: % 186.66/25.45 | | (583) addition(all_22_8, all_22_3) = all_160_0 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (484), (502) imply: % 186.66/25.45 | | (584) addition(all_22_3, all_22_8) = all_160_0 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (502), (519) imply: % 186.66/25.45 | | (585) addition(all_22_6, all_22_8) = all_278_0 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (443), (502) imply: % 186.66/25.45 | | (586) addition(all_22_8, all_22_8) = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_262_0, all_296_0, all_22_9, one, % 186.66/25.45 | | simplifying with (496), (535) gives: % 186.66/25.45 | | (587) all_296_0 = all_262_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_300_0, all_382_0, all_22_10, % 186.66/25.45 | | all_22_10, simplifying with (537), (577) gives: % 186.66/25.45 | | (588) all_382_0 = all_300_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_160_0, all_336_0, all_22_8, % 186.66/25.45 | | all_22_9, simplifying with (376), (550) gives: % 186.66/25.45 | | (589) all_336_0 = all_160_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_256_0, all_368_0, one, all_22_8, % 186.66/25.45 | | simplifying with (455), (567) gives: % 186.66/25.45 | | (590) all_368_0 = all_256_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_332_0, all_368_0, one, all_22_8, % 186.66/25.45 | | simplifying with (546), (567) gives: % 186.66/25.45 | | (591) all_368_0 = all_332_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_214_0, all_334_0, all_22_10, % 186.66/25.45 | | all_22_8, simplifying with (394), (548) gives: % 186.66/25.45 | | (592) all_334_0 = all_214_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_328_0, all_334_0, all_22_10, % 186.66/25.45 | | all_22_8, simplifying with (543), (548) gives: % 186.66/25.45 | | (593) all_334_0 = all_328_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_294_0, all_326_0, all_22_8, % 186.66/25.45 | | all_22_8, simplifying with (532), (540) gives: % 186.66/25.45 | | (594) all_326_0 = all_294_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_22_8, all_326_0, all_22_8, all_22_8, % 186.66/25.45 | | simplifying with (540), (586) gives: % 186.66/25.45 | | (595) all_326_0 = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_80_0, all_358_0, all_22_1, all_22_8, % 186.66/25.45 | | simplifying with (132), (560) gives: % 186.66/25.45 | | (596) all_358_0 = all_80_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_22_10, all_278_0, all_22_8, % 186.66/25.45 | | all_22_6, simplifying with (263), (585) gives: % 186.66/25.45 | | (597) all_278_0 = all_22_10 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_22_9, all_160_0, all_22_8, all_22_3, % 186.66/25.45 | | simplifying with (349), (584) gives: % 186.66/25.45 | | (598) all_160_0 = all_22_9 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_34_0, all_288_0, all_22_6, all_22_3, % 186.66/25.45 | | simplifying with (64), (529) gives: % 186.66/25.45 | | (599) all_288_0 = all_34_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_56_0, all_360_0, all_22_10, % 186.66/25.45 | | all_22_1, simplifying with (257), (562) gives: % 186.66/25.45 | | (600) all_360_0 = all_56_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (8) with all_284_0, all_360_0, all_22_10, % 186.66/25.45 | | all_22_1, simplifying with (526), (562) gives: % 186.66/25.45 | | (601) all_360_0 = all_284_0 % 186.66/25.45 | | % 186.66/25.45 | | GROUND_INST: instantiating (9) with all_214_0, all_280_0, all_262_0, % 186.66/25.45 | | all_22_10, simplifying with (463), (523) gives: % 186.66/25.45 | | (602) all_280_0 = all_214_0 % 186.66/25.45 | | % 186.66/25.45 | | COMBINE_EQS: (590), (591) imply: % 186.66/25.45 | | (603) all_332_0 = all_256_0 % 186.66/25.45 | | % 186.66/25.45 | | SIMP: (603) implies: % 186.66/25.45 | | (604) all_332_0 = all_256_0 % 186.66/25.45 | | % 186.66/25.45 | | COMBINE_EQS: (600), (601) imply: % 186.66/25.45 | | (605) all_284_0 = all_56_0 % 186.66/25.45 | | % 186.66/25.45 | | SIMP: (605) implies: % 186.66/25.45 | | (606) all_284_0 = all_56_0 % 186.66/25.45 | | % 186.66/25.45 | | COMBINE_EQS: (592), (593) imply: % 186.66/25.45 | | (607) all_328_0 = all_214_0 % 186.66/25.45 | | % 186.66/25.45 | | COMBINE_EQS: (594), (595) imply: % 186.66/25.45 | | (608) all_294_0 = all_22_8 % 186.66/25.45 | | % 186.66/25.45 | | COMBINE_EQS: (589), (598) imply: % 186.66/25.45 | | (609) all_336_0 = all_22_9 % 186.66/25.45 | | % 186.66/25.45 | | REDUCE: (579), (588) imply: % 186.66/25.46 | | (610) multiplication(all_300_0, all_22_9) = all_22_8 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (478), (598) imply: % 186.66/25.46 | | (611) multiplication(all_218_0, all_22_9) = all_22_9 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (522), (602) imply: % 186.66/25.46 | | (612) multiplication(one, all_214_0) = all_214_0 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (568), (590) imply: % 186.66/25.46 | | (613) addition(all_22_3, all_256_0) = all_262_0 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (533), (608) imply: % 186.66/25.46 | | (614) addition(all_22_6, all_22_8) = all_214_0 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (305), (598) imply: % 186.66/25.46 | | (615) addition(all_22_8, all_22_9) = all_22_9 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (376), (598) imply: % 186.66/25.46 | | (616) addition(all_22_9, all_22_8) = all_22_9 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (576), (588) imply: % 186.66/25.46 | | (617) $i(all_300_0) % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (521), (602) imply: % 186.66/25.46 | | (618) $i(all_214_0) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (8) with all_22_10, all_214_0, all_22_8, % 186.66/25.46 | | all_22_6, simplifying with (263), (614) gives: % 186.66/25.46 | | (619) all_214_0 = all_22_10 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (463), (619) imply: % 186.66/25.46 | | (620) multiplication(all_22_10, all_262_0) = all_22_10 % 186.66/25.46 | | % 186.66/25.46 | | REDUCE: (394), (619) imply: % 186.66/25.46 | | (621) addition(all_22_8, all_22_10) = all_22_10 % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (left_distributivity) with one, one, one, one, % 186.66/25.46 | | one, all_352_0, simplifying with (249), (289), (554) gives: % 186.66/25.46 | | (622) ? [v0: $i] : (multiplication(v0, one) = all_352_0 & addition(one, % 186.66/25.46 | | one) = v0 & $i(v0) & $i(all_352_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with one, one, one, one, % 186.66/25.46 | | one, all_352_0, simplifying with (249), (289), (554) gives: % 186.66/25.46 | | (623) ? [v0: $i] : (multiplication(one, v0) = all_352_0 & addition(one, % 186.66/25.46 | | one) = v0 & $i(v0) & $i(all_352_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with one, all_22_3, % 186.66/25.46 | | all_56_0, one, all_352_0, simplifying with (19), (116), (254), % 186.66/25.46 | | (289), (554) gives: % 186.66/25.46 | | (624) ? [v0: $i] : (addition(all_56_0, v0) = all_352_0 & % 186.66/25.46 | | addition(all_22_3, one) = v0 & $i(v0) & $i(all_352_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with one, all_56_0, % 186.66/25.46 | | all_22_3, one, all_352_0, simplifying with (19), (116), (284), % 186.66/25.46 | | (289), (554) gives: % 186.66/25.46 | | (625) ? [v0: $i] : (addition(all_56_0, one) = v0 & addition(all_22_3, % 186.66/25.46 | | v0) = all_352_0 & $i(v0) & $i(all_352_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_idempotence) with one, all_352_0, % 186.66/25.46 | | simplifying with (289), (554) gives: % 186.66/25.46 | | (626) all_352_0 = one % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with all_22_9, all_22_9, % 186.66/25.46 | | all_22_7, one, all_262_0, simplifying with (14), (16), (372), % 186.66/25.46 | | (496) gives: % 186.66/25.46 | | (627) ? [v0: $i] : (addition(all_22_7, v0) = all_262_0 & % 186.66/25.46 | | addition(all_22_9, all_22_9) = v0 & $i(v0) & $i(all_262_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with all_22_8, all_22_9, % 186.66/25.46 | | all_22_7, one, all_256_0, simplifying with (14), (15), (16), % 186.66/25.46 | | (372), (499) gives: % 186.66/25.46 | | (628) ? [v0: $i] : (addition(all_22_7, v0) = all_256_0 & % 186.66/25.46 | | addition(all_22_9, all_22_8) = v0 & $i(v0) & $i(all_256_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, one, one, % 186.66/25.46 | | all_22_10, all_22_10, all_300_0, simplifying with (13), (251), % 186.66/25.46 | | (289), (537) gives: % 186.66/25.46 | | (629) ? [v0: $i] : (multiplication(all_22_10, v0) = all_300_0 & % 186.66/25.46 | | addition(one, one) = v0 & $i(v0) & $i(all_300_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (left_distributivity) with one, one, all_22_10, % 186.66/25.46 | | all_22_10, all_22_10, all_300_0, simplifying with (13), (289), % 186.66/25.46 | | (404), (537) gives: % 186.66/25.46 | | (630) ? [v0: $i] : (multiplication(v0, all_22_10) = all_300_0 & % 186.66/25.46 | | addition(one, one) = v0 & $i(v0) & $i(all_300_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_idempotence) with all_22_10, all_300_0, % 186.66/25.46 | | simplifying with (13), (537) gives: % 186.66/25.46 | | (631) all_300_0 = all_22_10 % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (left_distributivity) with one, one, all_22_9, % 186.66/25.46 | | all_22_9, all_22_9, all_378_0, simplifying with (14), (289), % 186.66/25.46 | | (347), (571) gives: % 186.66/25.46 | | (632) ? [v0: $i] : (multiplication(v0, all_22_9) = all_378_0 & % 186.66/25.46 | | addition(one, one) = v0 & $i(v0) & $i(all_378_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_idempotence) with all_22_9, all_378_0, % 186.66/25.46 | | simplifying with (14), (571) gives: % 186.66/25.46 | | (633) all_378_0 = all_22_9 % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with all_22_4, % 186.66/25.46 | | all_22_10, all_22_8, all_22_10, one, simplifying with (13), % 186.66/25.46 | | (15), (18), (265), (621) gives: % 186.66/25.46 | | (634) ? [v0: $i] : (addition(all_22_8, v0) = one & addition(all_22_10, % 186.66/25.46 | | all_22_4) = v0 & $i(v0) & $i(one)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_associativity) with all_22_9, all_22_9, % 186.66/25.46 | | all_22_8, all_22_9, all_378_0, simplifying with (14), (15), % 186.66/25.46 | | (571), (615) gives: % 186.66/25.46 | | (635) ? [v0: $i] : (addition(all_22_8, v0) = all_378_0 & % 186.66/25.46 | | addition(all_22_9, all_22_9) = v0 & $i(v0) & $i(all_378_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_commutativity) with all_22_4, % 186.66/25.46 | | all_300_0, all_218_0, simplifying with (18), (538), (617) % 186.66/25.46 | | gives: % 186.66/25.46 | | (636) addition(all_300_0, all_22_4) = all_218_0 & $i(all_218_0) % 186.66/25.46 | | % 186.66/25.46 | | ALPHA: (636) implies: % 186.66/25.46 | | (637) addition(all_300_0, all_22_4) = all_218_0 % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with one, all_22_3, one, % 186.66/25.46 | | all_22_3, one, all_380_0, simplifying with (19), (249), (289), % 186.66/25.46 | | (483), (574) gives: % 186.66/25.46 | | (638) ? [v0: $i] : (multiplication(one, v0) = all_380_0 & % 186.66/25.46 | | addition(all_22_3, one) = v0 & $i(v0) & $i(all_380_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_commutativity) with all_22_3, % 186.66/25.46 | | all_256_0, all_262_0, simplifying with (19), (498), (613) % 186.66/25.46 | | gives: % 186.66/25.46 | | (639) addition(all_256_0, all_22_3) = all_262_0 & $i(all_262_0) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_commutativity) with all_34_0, % 186.66/25.46 | | all_22_10, all_366_0, simplifying with (13), (43), (564) gives: % 186.66/25.46 | | (640) addition(all_22_10, all_34_0) = all_366_0 & $i(all_366_0) % 186.66/25.46 | | % 186.66/25.46 | | ALPHA: (640) implies: % 186.66/25.46 | | (641) $i(all_366_0) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (additive_commutativity) with all_80_0, % 186.66/25.46 | | all_366_0, all_218_0, simplifying with (182), (565), (641) % 186.66/25.46 | | gives: % 186.66/25.46 | | (642) addition(all_366_0, all_80_0) = all_218_0 & $i(all_218_0) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, one, % 186.66/25.46 | | all_262_0, all_22_10, all_22_10, all_300_0, simplifying with % 186.66/25.46 | | (13), (251), (289), (495), (537), (620) gives: % 186.66/25.46 | | (643) ? [v0: $i] : (multiplication(all_22_10, v0) = all_300_0 & % 186.66/25.46 | | addition(one, all_262_0) = v0 & $i(v0) & $i(all_300_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_262_0, % 186.66/25.46 | | one, all_22_10, all_22_10, all_300_0, simplifying with (13), % 186.66/25.46 | | (251), (289), (495), (537), (620) gives: % 186.66/25.46 | | (644) ? [v0: $i] : (multiplication(all_22_10, v0) = all_300_0 & % 186.66/25.46 | | addition(all_262_0, one) = v0 & $i(v0) & $i(all_300_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_262_0, % 186.66/25.46 | | all_262_0, all_22_10, all_22_10, all_300_0, simplifying with % 186.66/25.46 | | (13), (495), (537), (620) gives: % 186.66/25.46 | | (645) ? [v0: $i] : (multiplication(all_22_10, v0) = all_300_0 & % 186.66/25.46 | | addition(all_262_0, all_262_0) = v0 & $i(v0) & $i(all_300_0)) % 186.66/25.46 | | % 186.66/25.46 | | GROUND_INST: instantiating (right_distributivity) with all_22_10, all_22_7, % 186.66/25.46 | | all_378_0, all_22_6, all_22_8, all_22_10, simplifying with % 186.66/25.46 | | (13), (16), (25), (263), (570), (581) gives: % 186.66/25.47 | | (646) ? [v0: $i] : (multiplication(all_22_10, v0) = all_22_10 & % 186.66/25.47 | | addition(all_22_7, all_378_0) = v0 & $i(v0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with one, all_218_0, % 186.66/25.47 | | all_22_9, all_22_9, all_22_9, all_378_0, simplifying with (14), % 186.66/25.47 | | (289), (347), (504), (571), (611) gives: % 186.66/25.47 | | (647) ? [v0: $i] : (multiplication(v0, all_22_9) = all_378_0 & % 186.66/25.47 | | addition(one, all_218_0) = v0 & $i(v0) & $i(all_378_0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with all_218_0, one, % 186.66/25.47 | | all_22_9, all_22_9, all_22_9, all_378_0, simplifying with (14), % 186.66/25.47 | | (289), (347), (504), (571), (611) gives: % 186.66/25.47 | | (648) ? [v0: $i] : (multiplication(v0, all_22_9) = all_378_0 & % 186.66/25.47 | | addition(all_218_0, one) = v0 & $i(v0) & $i(all_378_0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with all_218_0, all_218_0, % 186.66/25.47 | | all_22_9, all_22_9, all_22_9, all_378_0, simplifying with (14), % 186.66/25.47 | | (504), (571), (611) gives: % 186.66/25.47 | | (649) ? [v0: $i] : (multiplication(v0, all_22_9) = all_378_0 & % 186.66/25.47 | | addition(all_218_0, all_218_0) = v0 & $i(v0) & $i(all_378_0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with all_300_0, all_22_4, % 186.66/25.47 | | all_22_9, all_22_8, all_22_3, all_22_9, simplifying with (14), % 186.66/25.47 | | (18), (26), (351), (610), (617) gives: % 186.66/25.47 | | (650) ? [v0: $i] : (multiplication(v0, all_22_9) = all_22_9 & % 186.66/25.47 | | addition(all_300_0, all_22_4) = v0 & $i(v0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with one, all_352_0, % 186.66/25.47 | | all_22_8, all_22_8, all_22_8, all_22_8, simplifying with (15), % 186.66/25.47 | | (289), (480), (553), (580), (586) gives: % 186.66/25.47 | | (651) ? [v0: $i] : (multiplication(v0, all_22_8) = all_22_8 & % 186.66/25.47 | | addition(one, all_352_0) = v0 & $i(v0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with all_352_0, one, % 186.66/25.47 | | all_22_8, all_22_8, all_22_8, all_22_8, simplifying with (15), % 186.66/25.47 | | (289), (480), (553), (580), (586) gives: % 186.66/25.47 | | (652) ? [v0: $i] : (multiplication(v0, all_22_8) = all_22_8 & % 186.66/25.47 | | addition(all_352_0, one) = v0 & $i(v0)) % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (left_distributivity) with all_352_0, all_352_0, % 186.66/25.47 | | all_22_8, all_22_8, all_22_8, all_22_8, simplifying with (15), % 186.66/25.47 | | (553), (580), (586) gives: % 186.66/25.47 | | (653) ? [v0: $i] : (multiplication(v0, all_22_8) = all_22_8 & % 186.66/25.47 | | addition(all_352_0, all_352_0) = v0 & $i(v0)) % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (653) with fresh symbol all_470_0 gives: % 186.66/25.47 | | (654) multiplication(all_470_0, all_22_8) = all_22_8 & % 186.66/25.47 | | addition(all_352_0, all_352_0) = all_470_0 & $i(all_470_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (654) implies: % 186.66/25.47 | | (655) addition(all_352_0, all_352_0) = all_470_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (646) with fresh symbol all_482_0 gives: % 186.66/25.47 | | (656) multiplication(all_22_10, all_482_0) = all_22_10 & % 186.66/25.47 | | addition(all_22_7, all_378_0) = all_482_0 & $i(all_482_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (656) implies: % 186.66/25.47 | | (657) addition(all_22_7, all_378_0) = all_482_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (652) with fresh symbol all_486_0 gives: % 186.66/25.47 | | (658) multiplication(all_486_0, all_22_8) = all_22_8 & % 186.66/25.47 | | addition(all_352_0, one) = all_486_0 & $i(all_486_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (658) implies: % 186.66/25.47 | | (659) addition(all_352_0, one) = all_486_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (651) with fresh symbol all_488_0 gives: % 186.66/25.47 | | (660) multiplication(all_488_0, all_22_8) = all_22_8 & addition(one, % 186.66/25.47 | | all_352_0) = all_488_0 & $i(all_488_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (660) implies: % 186.66/25.47 | | (661) addition(one, all_352_0) = all_488_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (650) with fresh symbol all_496_0 gives: % 186.66/25.47 | | (662) multiplication(all_496_0, all_22_9) = all_22_9 & % 186.66/25.47 | | addition(all_300_0, all_22_4) = all_496_0 & $i(all_496_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (662) implies: % 186.66/25.47 | | (663) addition(all_300_0, all_22_4) = all_496_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (645) with fresh symbol all_508_0 gives: % 186.66/25.47 | | (664) multiplication(all_22_10, all_508_0) = all_300_0 & % 186.66/25.47 | | addition(all_262_0, all_262_0) = all_508_0 & $i(all_508_0) & % 186.66/25.47 | | $i(all_300_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (664) implies: % 186.66/25.47 | | (665) addition(all_262_0, all_262_0) = all_508_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (632) with fresh symbol all_514_0 gives: % 186.66/25.47 | | (666) multiplication(all_514_0, all_22_9) = all_378_0 & addition(one, % 186.66/25.47 | | one) = all_514_0 & $i(all_514_0) & $i(all_378_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (666) implies: % 186.66/25.47 | | (667) addition(one, one) = all_514_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (649) with fresh symbol all_532_0 gives: % 186.66/25.47 | | (668) multiplication(all_532_0, all_22_9) = all_378_0 & % 186.66/25.47 | | addition(all_218_0, all_218_0) = all_532_0 & $i(all_532_0) & % 186.66/25.47 | | $i(all_378_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (668) implies: % 186.66/25.47 | | (669) addition(all_218_0, all_218_0) = all_532_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (648) with fresh symbol all_536_0 gives: % 186.66/25.47 | | (670) multiplication(all_536_0, all_22_9) = all_378_0 & % 186.66/25.47 | | addition(all_218_0, one) = all_536_0 & $i(all_536_0) & % 186.66/25.47 | | $i(all_378_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (670) implies: % 186.66/25.47 | | (671) addition(all_218_0, one) = all_536_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (647) with fresh symbol all_550_0 gives: % 186.66/25.47 | | (672) multiplication(all_550_0, all_22_9) = all_378_0 & addition(one, % 186.66/25.47 | | all_218_0) = all_550_0 & $i(all_550_0) & $i(all_378_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (672) implies: % 186.66/25.47 | | (673) addition(one, all_218_0) = all_550_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (638) with fresh symbol all_580_0 gives: % 186.66/25.47 | | (674) multiplication(one, all_580_0) = all_380_0 & addition(all_22_3, % 186.66/25.47 | | one) = all_580_0 & $i(all_580_0) & $i(all_380_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (674) implies: % 186.66/25.47 | | (675) addition(all_22_3, one) = all_580_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (644) with fresh symbol all_612_0 gives: % 186.66/25.47 | | (676) multiplication(all_22_10, all_612_0) = all_300_0 & % 186.66/25.47 | | addition(all_262_0, one) = all_612_0 & $i(all_612_0) & % 186.66/25.47 | | $i(all_300_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (676) implies: % 186.66/25.47 | | (677) addition(all_262_0, one) = all_612_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (643) with fresh symbol all_614_0 gives: % 186.66/25.47 | | (678) multiplication(all_22_10, all_614_0) = all_300_0 & addition(one, % 186.66/25.47 | | all_262_0) = all_614_0 & $i(all_614_0) & $i(all_300_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (678) implies: % 186.66/25.47 | | (679) addition(one, all_262_0) = all_614_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (634) with fresh symbol all_620_0 gives: % 186.66/25.47 | | (680) addition(all_22_8, all_620_0) = one & addition(all_22_10, all_22_4) % 186.66/25.47 | | = all_620_0 & $i(all_620_0) & $i(one) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (680) implies: % 186.66/25.47 | | (681) addition(all_22_10, all_22_4) = all_620_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (630) with fresh symbol all_634_0 gives: % 186.66/25.47 | | (682) multiplication(all_634_0, all_22_10) = all_300_0 & addition(one, % 186.66/25.47 | | one) = all_634_0 & $i(all_634_0) & $i(all_300_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (682) implies: % 186.66/25.47 | | (683) addition(one, one) = all_634_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (624) with fresh symbol all_640_0 gives: % 186.66/25.47 | | (684) addition(all_56_0, all_640_0) = all_352_0 & addition(all_22_3, one) % 186.66/25.47 | | = all_640_0 & $i(all_640_0) & $i(all_352_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (684) implies: % 186.66/25.47 | | (685) addition(all_22_3, one) = all_640_0 % 186.66/25.47 | | (686) addition(all_56_0, all_640_0) = all_352_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (623) with fresh symbol all_644_0 gives: % 186.66/25.47 | | (687) multiplication(one, all_644_0) = all_352_0 & addition(one, one) = % 186.66/25.47 | | all_644_0 & $i(all_644_0) & $i(all_352_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (687) implies: % 186.66/25.47 | | (688) addition(one, one) = all_644_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (622) with fresh symbol all_648_0 gives: % 186.66/25.47 | | (689) multiplication(all_648_0, one) = all_352_0 & addition(one, one) = % 186.66/25.47 | | all_648_0 & $i(all_648_0) & $i(all_352_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (689) implies: % 186.66/25.47 | | (690) addition(one, one) = all_648_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (629) with fresh symbol all_652_0 gives: % 186.66/25.47 | | (691) multiplication(all_22_10, all_652_0) = all_300_0 & addition(one, % 186.66/25.47 | | one) = all_652_0 & $i(all_652_0) & $i(all_300_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (691) implies: % 186.66/25.47 | | (692) addition(one, one) = all_652_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (627) with fresh symbol all_750_0 gives: % 186.66/25.47 | | (693) addition(all_22_7, all_750_0) = all_262_0 & addition(all_22_9, % 186.66/25.47 | | all_22_9) = all_750_0 & $i(all_750_0) & $i(all_262_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (693) implies: % 186.66/25.47 | | (694) addition(all_22_9, all_22_9) = all_750_0 % 186.66/25.47 | | (695) addition(all_22_7, all_750_0) = all_262_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (628) with fresh symbol all_814_0 gives: % 186.66/25.47 | | (696) addition(all_22_7, all_814_0) = all_256_0 & addition(all_22_9, % 186.66/25.47 | | all_22_8) = all_814_0 & $i(all_814_0) & $i(all_256_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (696) implies: % 186.66/25.47 | | (697) addition(all_22_9, all_22_8) = all_814_0 % 186.66/25.47 | | (698) addition(all_22_7, all_814_0) = all_256_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (635) with fresh symbol all_828_0 gives: % 186.66/25.47 | | (699) addition(all_22_8, all_828_0) = all_378_0 & addition(all_22_9, % 186.66/25.47 | | all_22_9) = all_828_0 & $i(all_828_0) & $i(all_378_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (699) implies: % 186.66/25.47 | | (700) addition(all_22_9, all_22_9) = all_828_0 % 186.66/25.47 | | % 186.66/25.47 | | DELTA: instantiating (625) with fresh symbol all_840_0 gives: % 186.66/25.47 | | (701) addition(all_56_0, one) = all_840_0 & addition(all_22_3, all_840_0) % 186.66/25.47 | | = all_352_0 & $i(all_840_0) & $i(all_352_0) % 186.66/25.47 | | % 186.66/25.47 | | ALPHA: (701) implies: % 186.66/25.47 | | (702) $i(all_840_0) % 186.66/25.47 | | (703) addition(all_56_0, one) = all_840_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (626), (655) imply: % 186.66/25.47 | | (704) addition(one, one) = all_470_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (626), (659) imply: % 186.66/25.47 | | (705) addition(one, one) = all_486_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (631), (663) imply: % 186.66/25.47 | | (706) addition(all_22_10, all_22_4) = all_496_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (631), (637) imply: % 186.66/25.47 | | (707) addition(all_22_10, all_22_4) = all_218_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (626), (686) imply: % 186.66/25.47 | | (708) addition(all_56_0, all_640_0) = one % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (633), (657) imply: % 186.66/25.47 | | (709) addition(all_22_7, all_22_9) = all_482_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (571), (633) imply: % 186.66/25.47 | | (710) addition(all_22_9, all_22_9) = all_22_9 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (626), (661) imply: % 186.66/25.47 | | (711) addition(one, one) = all_488_0 % 186.66/25.47 | | % 186.66/25.47 | | REDUCE: (554), (626) imply: % 186.66/25.47 | | (712) addition(one, one) = one % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_470_0, all_486_0, one, one, % 186.66/25.47 | | simplifying with (704), (705) gives: % 186.66/25.47 | | (713) all_486_0 = all_470_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_486_0, all_488_0, one, one, % 186.66/25.47 | | simplifying with (705), (711) gives: % 186.66/25.47 | | (714) all_488_0 = all_486_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with one, all_634_0, one, one, simplifying % 186.66/25.47 | | with (683), (712) gives: % 186.66/25.47 | | (715) all_634_0 = one % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_644_0, all_648_0, one, one, % 186.66/25.47 | | simplifying with (688), (690) gives: % 186.66/25.47 | | (716) all_648_0 = all_644_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_634_0, all_648_0, one, one, % 186.66/25.47 | | simplifying with (683), (690) gives: % 186.66/25.47 | | (717) all_648_0 = all_634_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_488_0, all_648_0, one, one, % 186.66/25.47 | | simplifying with (690), (711) gives: % 186.66/25.47 | | (718) all_648_0 = all_488_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_648_0, all_652_0, one, one, % 186.66/25.47 | | simplifying with (690), (692) gives: % 186.66/25.47 | | (719) all_652_0 = all_648_0 % 186.66/25.47 | | % 186.66/25.47 | | GROUND_INST: instantiating (8) with all_514_0, all_652_0, one, one, % 186.66/25.47 | | simplifying with (667), (692) gives: % 186.66/25.47 | | (720) all_652_0 = all_514_0 % 186.66/25.47 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_218_0, all_496_0, all_22_4, % 186.66/25.48 | | all_22_10, simplifying with (706), (707) gives: % 186.66/25.48 | | (721) all_496_0 = all_218_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with one, all_620_0, all_22_4, all_22_10, % 186.66/25.48 | | simplifying with (265), (681) gives: % 186.66/25.48 | | (722) all_620_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_496_0, all_620_0, all_22_4, % 186.66/25.48 | | all_22_10, simplifying with (681), (706) gives: % 186.66/25.48 | | (723) all_620_0 = all_496_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_750_0, all_828_0, all_22_9, % 186.66/25.48 | | all_22_9, simplifying with (694), (700) gives: % 186.66/25.48 | | (724) all_828_0 = all_750_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_22_9, all_828_0, all_22_9, all_22_9, % 186.66/25.48 | | simplifying with (700), (710) gives: % 186.66/25.48 | | (725) all_828_0 = all_22_9 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_22_9, all_814_0, all_22_8, all_22_9, % 186.66/25.48 | | simplifying with (616), (697) gives: % 186.66/25.48 | | (726) all_814_0 = all_22_9 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with one, all_482_0, all_22_9, all_22_7, % 186.66/25.48 | | simplifying with (372), (709) gives: % 186.66/25.48 | | (727) all_482_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_380_0, all_640_0, one, all_22_3, % 186.66/25.48 | | simplifying with (574), (685) gives: % 186.66/25.48 | | (728) all_640_0 = all_380_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_580_0, all_640_0, one, all_22_3, % 186.66/25.48 | | simplifying with (675), (685) gives: % 186.66/25.48 | | (729) all_640_0 = all_580_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (724), (725) imply: % 186.66/25.48 | | (730) all_750_0 = all_22_9 % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (730) implies: % 186.66/25.48 | | (731) all_750_0 = all_22_9 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (719), (720) imply: % 186.66/25.48 | | (732) all_648_0 = all_514_0 % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (732) implies: % 186.66/25.48 | | (733) all_648_0 = all_514_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (716), (718) imply: % 186.66/25.48 | | (734) all_644_0 = all_488_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (716), (717) imply: % 186.66/25.48 | | (735) all_644_0 = all_634_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (716), (733) imply: % 186.66/25.48 | | (736) all_644_0 = all_514_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (734), (736) imply: % 186.66/25.48 | | (737) all_514_0 = all_488_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (735), (736) imply: % 186.66/25.48 | | (738) all_634_0 = all_514_0 % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (738) implies: % 186.66/25.48 | | (739) all_634_0 = all_514_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (728), (729) imply: % 186.66/25.48 | | (740) all_580_0 = all_380_0 % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (740) implies: % 186.66/25.48 | | (741) all_580_0 = all_380_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (715), (739) imply: % 186.66/25.48 | | (742) all_514_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (742) implies: % 186.66/25.48 | | (743) all_514_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (722), (723) imply: % 186.66/25.48 | | (744) all_496_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (744) implies: % 186.66/25.48 | | (745) all_496_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (737), (743) imply: % 186.66/25.48 | | (746) all_488_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (746) implies: % 186.66/25.48 | | (747) all_488_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (721), (745) imply: % 186.66/25.48 | | (748) all_218_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (714), (747) imply: % 186.66/25.48 | | (749) all_486_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (749) implies: % 186.66/25.48 | | (750) all_486_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (713), (750) imply: % 186.66/25.48 | | (751) all_470_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (751) implies: % 186.66/25.48 | | (752) all_470_0 = one % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (669), (748) imply: % 186.66/25.48 | | (753) addition(one, one) = all_532_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (671), (748) imply: % 186.66/25.48 | | (754) addition(one, one) = all_536_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (708), (728) imply: % 186.66/25.48 | | (755) addition(all_56_0, all_380_0) = one % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (698), (726) imply: % 186.66/25.48 | | (756) addition(all_22_7, all_22_9) = all_256_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (695), (731) imply: % 186.66/25.48 | | (757) addition(all_22_7, all_22_9) = all_262_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (673), (748) imply: % 186.66/25.48 | | (758) addition(one, one) = all_550_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with one, all_550_0, one, one, simplifying % 186.66/25.48 | | with (712), (758) gives: % 186.66/25.48 | | (759) all_550_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_536_0, all_550_0, one, one, % 186.66/25.48 | | simplifying with (754), (758) gives: % 186.66/25.48 | | (760) all_550_0 = all_536_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_532_0, all_550_0, one, one, % 186.66/25.48 | | simplifying with (753), (758) gives: % 186.66/25.48 | | (761) all_550_0 = all_532_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with one, all_262_0, all_22_9, all_22_7, % 186.66/25.48 | | simplifying with (372), (757) gives: % 186.66/25.48 | | (762) all_262_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_256_0, all_262_0, all_22_9, % 186.66/25.48 | | all_22_7, simplifying with (756), (757) gives: % 186.66/25.48 | | (763) all_262_0 = all_256_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (760), (761) imply: % 186.66/25.48 | | (764) all_536_0 = all_532_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (759), (760) imply: % 186.66/25.48 | | (765) all_536_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (764), (765) imply: % 186.66/25.48 | | (766) all_532_0 = one % 186.66/25.48 | | % 186.66/25.48 | | SIMP: (766) implies: % 186.66/25.48 | | (767) all_532_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (762), (763) imply: % 186.66/25.48 | | (768) all_256_0 = one % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (665), (762) imply: % 186.66/25.48 | | (769) addition(one, one) = all_508_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (677), (762) imply: % 186.66/25.48 | | (770) addition(one, one) = all_612_0 % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (613), (762), (768) imply: % 186.66/25.48 | | (771) addition(all_22_3, one) = one % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (679), (762) imply: % 186.66/25.48 | | (772) addition(one, one) = all_614_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with one, all_614_0, one, one, simplifying % 186.66/25.48 | | with (712), (772) gives: % 186.66/25.48 | | (773) all_614_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_612_0, all_614_0, one, one, % 186.66/25.48 | | simplifying with (770), (772) gives: % 186.66/25.48 | | (774) all_614_0 = all_612_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_508_0, all_614_0, one, one, % 186.66/25.48 | | simplifying with (769), (772) gives: % 186.66/25.48 | | (775) all_614_0 = all_508_0 % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_380_0, one, one, all_22_3, % 186.66/25.48 | | simplifying with (574), (771) gives: % 186.66/25.48 | | (776) all_380_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (773), (774) imply: % 186.66/25.48 | | (777) all_612_0 = one % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (774), (775) imply: % 186.66/25.48 | | (778) all_612_0 = all_508_0 % 186.66/25.48 | | % 186.66/25.48 | | COMBINE_EQS: (777), (778) imply: % 186.66/25.48 | | (779) all_508_0 = one % 186.66/25.48 | | % 186.66/25.48 | | REDUCE: (755), (776) imply: % 186.66/25.48 | | (780) addition(all_56_0, one) = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (8) with all_840_0, one, one, all_56_0, % 186.66/25.48 | | simplifying with (703), (780) gives: % 186.66/25.48 | | (781) all_840_0 = one % 186.66/25.48 | | % 186.66/25.48 | | GROUND_INST: instantiating (3) with one, one, simplifying with (267), (289), % 186.66/25.48 | | (712) gives: % 186.66/25.48 | | (782) $false % 186.66/25.48 | | % 186.66/25.48 | | CLOSE: (782) is inconsistent. % 186.66/25.48 | | % 186.90/25.49 | Case 2: % 186.90/25.49 | | % 186.90/25.49 | | (783) ~ leq(one, all_22_0) % 186.90/25.49 | | (784) leq(all_22_0, one) % 186.90/25.49 | | % 186.90/25.49 | | REDUCE: (214), (784) imply: % 186.90/25.49 | | (785) leq(one, one) % 186.90/25.49 | | % 186.90/25.49 | | REDUCE: (214), (783) imply: % 186.90/25.49 | | (786) ~ leq(one, one) % 186.90/25.49 | | % 186.90/25.49 | | PRED_UNIFY: (785), (786) imply: % 186.90/25.49 | | (787) $false % 186.90/25.49 | | % 186.90/25.49 | | CLOSE: (787) is inconsistent. % 186.90/25.49 | | % 186.90/25.49 | End of split % 186.90/25.49 | % 186.90/25.49 End of proof % 186.90/25.49 % SZS output end Proof for theBenchmark % 186.90/25.49 % 186.90/25.49 24897ms %------------------------------------------------------------------------------