%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KLE010+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.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 115.57s 15.77s % Output : Proof 117.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KLE010+1 : TPTP v8.1.2. Released v4.0.0. % 0.03/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n023.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Aug 29 12:14:40 EDT 2023 % 0.12/0.34 % CPUTime : % 0.52/0.60 ________ _____ % 0.52/0.60 ___ __ \_________(_)________________________________ % 0.52/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.52/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.52/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.52/0.60 % 0.52/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.52/0.60 (2023-06-19) % 0.52/0.60 % 0.52/0.60 (c) Philipp Rümmer, 2009-2023 % 0.52/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.52/0.60 Amanda Stjerna. % 0.52/0.60 Free software under BSD-3-Clause. % 0.52/0.60 % 0.52/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.52/0.61 % 0.52/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.52/0.62 Running up to 7 provers in parallel. % 0.52/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.52/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.52/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.52/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.52/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.52/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.52/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.25/1.02 Prover 4: Preprocessing ... % 2.25/1.03 Prover 1: Preprocessing ... % 2.71/1.06 Prover 3: Preprocessing ... % 2.71/1.06 Prover 2: Preprocessing ... % 2.71/1.06 Prover 5: Preprocessing ... % 2.71/1.06 Prover 0: Preprocessing ... % 2.71/1.06 Prover 6: Preprocessing ... % 5.08/1.39 Prover 3: Constructing countermodel ... % 5.08/1.39 Prover 6: Proving ... % 5.08/1.39 Prover 5: Proving ... % 5.08/1.39 Prover 1: Constructing countermodel ... % 5.08/1.40 Prover 4: Constructing countermodel ... % 5.08/1.43 Prover 0: Proving ... % 5.70/1.46 Prover 2: Proving ... % 14.38/2.60 Prover 3: gave up % 14.38/2.61 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.38/2.64 Prover 7: Preprocessing ... % 15.58/2.75 Prover 7: Constructing countermodel ... % 67.48/9.47 Prover 2: stopped % 67.48/9.47 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 67.76/9.49 Prover 8: Preprocessing ... % 68.32/9.60 Prover 8: Warning: ignoring some quantifiers % 68.32/9.61 Prover 8: Constructing countermodel ... % 76.07/10.59 Prover 8: gave up % 76.07/10.59 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 76.07/10.60 Prover 9: Preprocessing ... % 76.70/10.67 Prover 9: Constructing countermodel ... % 101.74/13.96 Prover 5: stopped % 101.74/13.96 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 102.09/14.04 Prover 10: Preprocessing ... % 102.94/14.09 Prover 10: Constructing countermodel ... % 114.96/15.72 Prover 10: Found proof (size 643) % 114.96/15.72 Prover 10: proved (1755ms) % 115.57/15.72 Prover 6: stopped % 115.57/15.72 Prover 9: stopped % 115.57/15.72 Prover 7: stopped % 115.57/15.72 Prover 4: stopped % 115.57/15.73 Prover 1: stopped % 115.57/15.77 Prover 0: stopped % 115.57/15.77 % 115.57/15.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.57/15.77 % 116.07/15.98 % SZS output start Proof for theBenchmark % 116.07/15.99 Assumptions after simplification: % 116.07/15.99 --------------------------------- % 116.07/15.99 % 116.07/15.99 (additive_associativity) % 116.07/16.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 116.07/16.01 (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 116.07/16.01 | ~ $i(v0) | ? [v5: $i] : (addition(v2, v5) = v4 & addition(v1, v0) = v5 & % 116.07/16.01 $i(v5) & $i(v4))) % 116.07/16.01 % 116.07/16.01 (additive_commutativity) % 116.07/16.02 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | ~ % 116.07/16.02 $i(v1) | ~ $i(v0) | (addition(v1, v0) = v2 & $i(v2))) % 116.07/16.02 % 116.07/16.02 (additive_idempotence) % 116.07/16.02 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (addition(v0, v0) = v1) | ~ $i(v0)) % 116.07/16.02 % 116.07/16.02 (goals) % 116.07/16.02 $i(one) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 116.07/16.02 : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 116.07/16.02 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ( ~ (v12 = one) & c(v1) = v3 & c(v0) % 116.07/16.02 = v8 & multiplication(v8, v3) = v11 & multiplication(v8, v1) = v9 & % 116.07/16.02 multiplication(v3, v0) = v4 & multiplication(v1, v0) = v2 & % 116.07/16.02 multiplication(v0, v1) = v6 & addition(v10, v11) = v12 & addition(v7, v9) = % 116.07/16.02 v10 & addition(v5, v6) = v7 & addition(v2, v4) = v5 & $i(v12) & $i(v11) & % 116.07/16.02 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 116.07/16.02 $i(v2) & $i(v1) & $i(v0) & test(v1) & test(v0)) % 116.07/16.02 % 116.07/16.02 (left_distributivity) % 116.07/16.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 116.07/16.03 $i] : ( ~ (multiplication(v1, v2) = v4) | ~ (multiplication(v0, v2) = v3) | % 116.07/16.03 ~ (addition(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] % 116.07/16.03 : (multiplication(v6, v2) = v5 & addition(v0, v1) = v6 & $i(v6) & $i(v5))) % 116.07/16.03 % 116.07/16.03 (multiplicative_associativity) % 116.07/16.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 116.07/16.03 (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ~ $i(v2) % 116.07/16.03 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (multiplication(v1, v2) = v5 & % 116.07/16.03 multiplication(v0, v5) = v4 & $i(v5) & $i(v4))) % 116.07/16.03 % 116.07/16.03 (multiplicative_left_identity) % 116.07/16.03 $i(one) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(one, v0) = % 116.07/16.03 v1) | ~ $i(v0)) % 116.07/16.03 % 116.07/16.03 (multiplicative_right_identity) % 116.31/16.03 $i(one) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(v0, one) = % 116.31/16.03 v1) | ~ $i(v0)) % 116.31/16.03 % 116.31/16.03 (right_distributivity) % 116.31/16.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 116.31/16.03 $i] : ( ~ (multiplication(v0, v2) = v4) | ~ (multiplication(v0, v1) = v3) | % 116.31/16.03 ~ (addition(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] % 116.31/16.03 : (multiplication(v0, v6) = v5 & addition(v1, v2) = v6 & $i(v6) & $i(v5))) % 116.31/16.03 % 116.31/16.03 (test_2) % 116.31/16.04 $i(one) & $i(zero) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = one | ~ % 116.31/16.04 (addition(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ complement(v1, v0)) & % 116.31/16.04 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | ~ % 116.31/16.04 $i(v1) | ~ $i(v0) | ~ complement(v1, v0) | (multiplication(v1, v0) = zero % 116.31/16.04 & multiplication(v0, v1) = zero)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 116.31/16.04 (addition(v0, v1) = one) | ~ $i(v1) | ~ $i(v0) | complement(v1, v0) | ? % 116.31/16.04 [v2: $i] : ? [v3: $i] : (( ~ (v3 = zero) & multiplication(v1, v0) = v3 & % 116.31/16.04 $i(v3)) | ( ~ (v2 = zero) & multiplication(v0, v1) = v2 & $i(v2)))) % 116.31/16.04 % 116.31/16.04 (test_3) % 116.31/16.04 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ (c(v0) = v2) | ~ % 116.31/16.04 $i(v1) | ~ $i(v0) | ~ complement(v0, v1) | ~ test(v0)) & ! [v0: $i] : ! % 116.31/16.04 [v1: $i] : ( ~ (c(v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ test(v0) | % 116.31/16.04 complement(v0, v1)) % 116.31/16.04 % 116.31/16.04 (function-axioms) % 116.31/16.04 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 116.31/16.04 (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) & ! [v0: % 116.31/16.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (addition(v3, % 116.31/16.04 v2) = v1) | ~ (addition(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 116.31/16.04 [v2: $i] : (v1 = v0 | ~ (c(v2) = v1) | ~ (c(v2) = v0)) % 116.31/16.04 % 116.31/16.04 Further assumptions not needed in the proof: % 116.31/16.04 -------------------------------------------- % 116.31/16.04 additive_identity, left_annihilation, order, right_annihilation, test_1, test_4 % 116.31/16.04 % 116.31/16.04 Those formulas are unsatisfiable: % 116.31/16.04 --------------------------------- % 116.31/16.04 % 116.31/16.04 Begin of proof % 116.31/16.05 | % 116.31/16.05 | ALPHA: (multiplicative_right_identity) implies: % 116.31/16.05 | (1) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(v0, one) = % 116.31/16.05 | v1) | ~ $i(v0)) % 116.31/16.05 | % 116.31/16.05 | ALPHA: (multiplicative_left_identity) implies: % 116.31/16.05 | (2) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (multiplication(one, v0) = % 116.31/16.05 | v1) | ~ $i(v0)) % 116.31/16.05 | % 116.31/16.05 | ALPHA: (test_2) implies: % 116.31/16.05 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = one | ~ (addition(v0, % 116.31/16.05 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ complement(v1, v0)) % 116.31/16.05 | % 116.31/16.05 | ALPHA: (test_3) implies: % 116.31/16.05 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (c(v0) = v1) | ~ $i(v1) | ~ $i(v0) | % 116.31/16.05 | ~ test(v0) | complement(v0, v1)) % 116.31/16.05 | % 116.31/16.05 | ALPHA: (goals) implies: % 116.31/16.05 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 116.31/16.05 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 116.31/16.05 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ( ~ (v12 = one) & c(v1) = v3 % 116.31/16.06 | & c(v0) = v8 & multiplication(v8, v3) = v11 & multiplication(v8, v1) % 116.31/16.06 | = v9 & multiplication(v3, v0) = v4 & multiplication(v1, v0) = v2 & % 116.31/16.06 | multiplication(v0, v1) = v6 & addition(v10, v11) = v12 & addition(v7, % 116.31/16.06 | v9) = v10 & addition(v5, v6) = v7 & addition(v2, v4) = v5 & $i(v12) % 116.31/16.06 | & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 116.31/16.06 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & test(v1) & test(v0)) % 116.31/16.06 | % 116.31/16.06 | ALPHA: (function-axioms) implies: % 116.31/16.06 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 116.31/16.06 | (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 116.31/16.06 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 116.31/16.06 | (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) % 116.31/16.06 | % 116.31/16.06 | DELTA: instantiating (5) with fresh symbols all_20_0, all_20_1, all_20_2, % 116.31/16.06 | all_20_3, all_20_4, all_20_5, all_20_6, all_20_7, all_20_8, all_20_9, % 116.31/16.06 | all_20_10, all_20_11, all_20_12 gives: % 116.31/16.06 | (8) ~ (all_20_0 = one) & c(all_20_11) = all_20_9 & c(all_20_12) = all_20_4 % 116.31/16.06 | & multiplication(all_20_4, all_20_9) = all_20_1 & % 116.31/16.06 | multiplication(all_20_4, all_20_11) = all_20_3 & % 116.31/16.06 | multiplication(all_20_9, all_20_12) = all_20_8 & % 116.31/16.06 | multiplication(all_20_11, all_20_12) = all_20_10 & % 116.31/16.06 | multiplication(all_20_12, all_20_11) = all_20_6 & addition(all_20_2, % 116.31/16.06 | all_20_1) = all_20_0 & addition(all_20_5, all_20_3) = all_20_2 & % 116.31/16.06 | addition(all_20_7, all_20_6) = all_20_5 & addition(all_20_10, all_20_8) % 116.31/16.06 | = all_20_7 & $i(all_20_0) & $i(all_20_1) & $i(all_20_2) & $i(all_20_3) % 116.31/16.06 | & $i(all_20_4) & $i(all_20_5) & $i(all_20_6) & $i(all_20_7) & % 116.31/16.06 | $i(all_20_8) & $i(all_20_9) & $i(all_20_10) & $i(all_20_11) & % 116.31/16.06 | $i(all_20_12) & test(all_20_11) & test(all_20_12) % 116.31/16.06 | % 116.31/16.06 | ALPHA: (8) implies: % 116.31/16.06 | (9) ~ (all_20_0 = one) % 116.31/16.06 | (10) test(all_20_12) % 116.31/16.06 | (11) test(all_20_11) % 116.31/16.06 | (12) $i(all_20_12) % 116.31/16.06 | (13) $i(all_20_11) % 116.31/16.06 | (14) $i(all_20_10) % 116.31/16.06 | (15) $i(all_20_9) % 116.31/16.06 | (16) $i(all_20_8) % 116.31/16.06 | (17) $i(all_20_6) % 116.31/16.06 | (18) $i(all_20_4) % 116.31/16.06 | (19) $i(all_20_3) % 116.31/16.06 | (20) $i(all_20_1) % 116.31/16.06 | (21) addition(all_20_10, all_20_8) = all_20_7 % 116.31/16.06 | (22) addition(all_20_7, all_20_6) = all_20_5 % 116.31/16.06 | (23) addition(all_20_5, all_20_3) = all_20_2 % 116.31/16.06 | (24) addition(all_20_2, all_20_1) = all_20_0 % 116.31/16.06 | (25) multiplication(all_20_12, all_20_11) = all_20_6 % 116.31/16.06 | (26) multiplication(all_20_11, all_20_12) = all_20_10 % 116.31/16.06 | (27) multiplication(all_20_9, all_20_12) = all_20_8 % 116.31/16.07 | (28) multiplication(all_20_4, all_20_11) = all_20_3 % 116.31/16.07 | (29) multiplication(all_20_4, all_20_9) = all_20_1 % 116.31/16.07 | (30) c(all_20_12) = all_20_4 % 116.31/16.07 | (31) c(all_20_11) = all_20_9 % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_20_8, % 116.31/16.07 | all_20_7, simplifying with (14), (16), (21) gives: % 116.31/16.07 | (32) addition(all_20_8, all_20_10) = all_20_7 & $i(all_20_7) % 116.31/16.07 | % 116.31/16.07 | ALPHA: (32) implies: % 116.31/16.07 | (33) $i(all_20_7) % 116.31/16.07 | (34) addition(all_20_8, all_20_10) = all_20_7 % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_8, % 116.31/16.07 | all_20_10, all_20_7, all_20_5, simplifying with (14), (16), (17), % 116.31/16.07 | (21), (22) gives: % 116.31/16.07 | (35) ? [v0: $i] : (addition(all_20_8, all_20_6) = v0 & addition(all_20_10, % 116.31/16.07 | v0) = all_20_5 & $i(v0) & $i(all_20_5)) % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_commutativity) with all_20_7, all_20_6, % 116.31/16.07 | all_20_5, simplifying with (17), (22), (33) gives: % 116.31/16.07 | (36) addition(all_20_6, all_20_7) = all_20_5 & $i(all_20_5) % 116.31/16.07 | % 116.31/16.07 | ALPHA: (36) implies: % 116.31/16.07 | (37) $i(all_20_5) % 116.31/16.07 | (38) addition(all_20_6, all_20_7) = all_20_5 % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_6, % 116.31/16.07 | all_20_7, all_20_5, all_20_2, simplifying with (17), (19), (22), % 116.31/16.07 | (23), (33) gives: % 116.31/16.07 | (39) ? [v0: $i] : (addition(all_20_6, all_20_3) = v0 & addition(all_20_7, % 116.31/16.07 | v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_commutativity) with all_20_5, all_20_3, % 116.31/16.07 | all_20_2, simplifying with (19), (23), (37) gives: % 116.31/16.07 | (40) addition(all_20_3, all_20_5) = all_20_2 & $i(all_20_2) % 116.31/16.07 | % 116.31/16.07 | ALPHA: (40) implies: % 116.31/16.07 | (41) addition(all_20_3, all_20_5) = all_20_2 % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 116.31/16.07 | all_20_5, all_20_2, all_20_0, simplifying with (19), (20), (23), % 116.31/16.07 | (24), (37) gives: % 116.31/16.07 | (42) ? [v0: $i] : (addition(all_20_3, all_20_1) = v0 & addition(all_20_5, % 116.31/16.07 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.31/16.07 | % 116.31/16.07 | GROUND_INST: instantiating (left_distributivity) with all_20_11, all_20_9, % 116.31/16.07 | all_20_12, all_20_10, all_20_8, all_20_7, simplifying with (12), % 116.31/16.07 | (13), (15), (21), (26), (27) gives: % 116.31/16.07 | (43) ? [v0: $i] : (multiplication(v0, all_20_12) = all_20_7 & % 116.31/16.07 | addition(all_20_11, all_20_9) = v0 & $i(v0) & $i(all_20_7)) % 116.31/16.07 | % 116.31/16.08 | GROUND_INST: instantiating (4) with all_20_12, all_20_4, simplifying with % 116.31/16.08 | (10), (12), (18), (30) gives: % 116.31/16.08 | (44) complement(all_20_12, all_20_4) % 116.31/16.08 | % 116.31/16.08 | GROUND_INST: instantiating (4) with all_20_11, all_20_9, simplifying with % 116.31/16.08 | (11), (13), (15), (31) gives: % 116.31/16.08 | (45) complement(all_20_11, all_20_9) % 116.31/16.08 | % 116.31/16.08 | DELTA: instantiating (43) with fresh symbol all_32_0 gives: % 116.31/16.08 | (46) multiplication(all_32_0, all_20_12) = all_20_7 & addition(all_20_11, % 116.31/16.08 | all_20_9) = all_32_0 & $i(all_32_0) & $i(all_20_7) % 116.31/16.08 | % 116.31/16.08 | ALPHA: (46) implies: % 116.31/16.08 | (47) addition(all_20_11, all_20_9) = all_32_0 % 116.31/16.08 | % 116.31/16.08 | DELTA: instantiating (39) with fresh symbol all_34_0 gives: % 116.31/16.08 | (48) addition(all_20_6, all_20_3) = all_34_0 & addition(all_20_7, all_34_0) % 116.31/16.08 | = all_20_2 & $i(all_34_0) & $i(all_20_2) % 116.31/16.08 | % 116.31/16.08 | ALPHA: (48) implies: % 116.55/16.08 | (49) $i(all_34_0) % 116.55/16.08 | (50) addition(all_20_7, all_34_0) = all_20_2 % 116.55/16.08 | (51) addition(all_20_6, all_20_3) = all_34_0 % 116.55/16.08 | % 116.55/16.08 | DELTA: instantiating (42) with fresh symbol all_36_0 gives: % 116.55/16.08 | (52) addition(all_20_3, all_20_1) = all_36_0 & addition(all_20_5, all_36_0) % 116.55/16.08 | = all_20_0 & $i(all_36_0) & $i(all_20_0) % 116.55/16.08 | % 116.55/16.08 | ALPHA: (52) implies: % 116.55/16.08 | (53) $i(all_36_0) % 116.55/16.08 | (54) addition(all_20_5, all_36_0) = all_20_0 % 116.55/16.08 | (55) addition(all_20_3, all_20_1) = all_36_0 % 116.55/16.08 | % 116.55/16.08 | DELTA: instantiating (35) with fresh symbol all_38_0 gives: % 116.55/16.08 | (56) addition(all_20_8, all_20_6) = all_38_0 & addition(all_20_10, % 116.55/16.08 | all_38_0) = all_20_5 & $i(all_38_0) & $i(all_20_5) % 116.55/16.08 | % 116.55/16.08 | ALPHA: (56) implies: % 116.55/16.08 | (57) $i(all_38_0) % 116.55/16.08 | (58) addition(all_20_10, all_38_0) = all_20_5 % 116.55/16.08 | (59) addition(all_20_8, all_20_6) = all_38_0 % 116.55/16.08 | % 116.55/16.08 | GROUND_INST: instantiating (additive_commutativity) with all_20_11, all_20_9, % 116.55/16.08 | all_32_0, simplifying with (13), (15), (47) gives: % 116.55/16.08 | (60) addition(all_20_9, all_20_11) = all_32_0 & $i(all_32_0) % 116.55/16.08 | % 116.55/16.08 | ALPHA: (60) implies: % 116.55/16.08 | (61) addition(all_20_9, all_20_11) = all_32_0 % 116.55/16.08 | % 116.55/16.08 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_38_0, % 116.55/16.08 | all_20_10, all_20_5, all_20_2, simplifying with (14), (19), (23), % 116.55/16.08 | (57), (58) gives: % 116.55/16.08 | (62) ? [v0: $i] : (addition(all_38_0, all_20_3) = v0 & addition(all_20_10, % 116.55/16.08 | v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.55/16.08 | % 116.55/16.08 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_38_0, % 116.55/16.08 | all_20_5, simplifying with (14), (57), (58) gives: % 116.55/16.08 | (63) addition(all_38_0, all_20_10) = all_20_5 & $i(all_20_5) % 116.55/16.08 | % 116.55/16.08 | ALPHA: (63) implies: % 116.55/16.08 | (64) addition(all_38_0, all_20_10) = all_20_5 % 116.55/16.08 | % 116.55/16.08 | GROUND_INST: instantiating (left_distributivity) with all_20_9, all_20_11, % 116.55/16.08 | all_20_12, all_20_8, all_20_10, all_20_7, simplifying with (12), % 116.55/16.08 | (13), (15), (26), (27), (34) gives: % 116.55/16.08 | (65) ? [v0: $i] : (multiplication(v0, all_20_12) = all_20_7 & % 116.55/16.08 | addition(all_20_9, all_20_11) = v0 & $i(v0) & $i(all_20_7)) % 116.55/16.08 | % 116.55/16.08 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_10, % 116.55/16.08 | all_20_8, all_20_7, all_20_5, simplifying with (14), (16), (17), % 116.55/16.08 | (22), (34) gives: % 116.55/16.09 | (66) ? [v0: $i] : (addition(all_20_8, v0) = all_20_5 & addition(all_20_10, % 116.55/16.09 | all_20_6) = v0 & $i(v0) & $i(all_20_5)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_20_6, % 116.55/16.09 | all_38_0, simplifying with (16), (17), (59) gives: % 116.55/16.09 | (67) addition(all_20_6, all_20_8) = all_38_0 & $i(all_38_0) % 116.55/16.09 | % 116.55/16.09 | ALPHA: (67) implies: % 116.55/16.09 | (68) addition(all_20_6, all_20_8) = all_38_0 % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_34_0, % 116.55/16.09 | all_20_7, all_20_2, all_20_0, simplifying with (20), (24), (33), % 116.55/16.09 | (49), (50) gives: % 116.55/16.09 | (69) ? [v0: $i] : (addition(all_34_0, all_20_1) = v0 & addition(all_20_7, % 116.55/16.09 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_associativity) with all_34_0, all_20_8, % 116.55/16.09 | all_20_10, all_20_7, all_20_2, simplifying with (14), (16), (21), % 116.55/16.09 | (49), (50) gives: % 116.55/16.09 | (70) ? [v0: $i] : (addition(all_20_8, all_34_0) = v0 & addition(all_20_10, % 116.55/16.09 | v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_associativity) with all_34_0, all_20_10, % 116.55/16.09 | all_20_8, all_20_7, all_20_2, simplifying with (14), (16), (34), % 116.55/16.09 | (49), (50) gives: % 116.55/16.09 | (71) ? [v0: $i] : (addition(all_20_8, v0) = all_20_2 & addition(all_20_10, % 116.55/16.09 | all_34_0) = v0 & $i(v0) & $i(all_20_2)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_commutativity) with all_20_7, all_34_0, % 116.55/16.09 | all_20_2, simplifying with (33), (49), (50) gives: % 116.55/16.09 | (72) addition(all_34_0, all_20_7) = all_20_2 & $i(all_20_2) % 116.55/16.09 | % 116.55/16.09 | ALPHA: (72) implies: % 116.55/16.09 | (73) addition(all_34_0, all_20_7) = all_20_2 % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_7, % 116.55/16.09 | all_20_6, all_20_5, all_20_2, simplifying with (17), (19), (23), % 116.55/16.09 | (33), (38) gives: % 116.55/16.09 | (74) ? [v0: $i] : (addition(all_20_6, v0) = all_20_2 & addition(all_20_7, % 116.55/16.09 | all_20_3) = v0 & $i(v0) & $i(all_20_2)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (left_distributivity) with all_20_12, all_20_4, % 116.55/16.09 | all_20_11, all_20_6, all_20_3, all_34_0, simplifying with (12), % 116.55/16.09 | (13), (18), (25), (28), (51) gives: % 116.55/16.09 | (75) ? [v0: $i] : (multiplication(v0, all_20_11) = all_34_0 & % 116.55/16.09 | addition(all_20_12, all_20_4) = v0 & $i(v0) & $i(all_34_0)) % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_commutativity) with all_20_6, all_20_3, % 116.55/16.09 | all_34_0, simplifying with (17), (19), (51) gives: % 116.55/16.09 | (76) addition(all_20_3, all_20_6) = all_34_0 & $i(all_34_0) % 116.55/16.09 | % 116.55/16.09 | ALPHA: (76) implies: % 116.55/16.09 | (77) addition(all_20_3, all_20_6) = all_34_0 % 116.55/16.09 | % 116.55/16.09 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_6, % 116.55/16.09 | all_20_7, all_20_5, all_20_0, simplifying with (17), (22), (33), % 116.55/16.09 | (53), (54) gives: % 116.55/16.10 | (78) ? [v0: $i] : (addition(all_20_6, all_36_0) = v0 & addition(all_20_7, % 116.55/16.10 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.10 | % 116.55/16.10 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_7, % 116.55/16.10 | all_20_6, all_20_5, all_20_0, simplifying with (17), (33), (38), % 116.55/16.10 | (53), (54) gives: % 116.55/16.10 | (79) ? [v0: $i] : (addition(all_20_6, v0) = all_20_0 & addition(all_20_7, % 116.55/16.10 | all_36_0) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.10 | % 116.55/16.10 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_38_0, % 116.55/16.10 | all_20_10, all_20_5, all_20_0, simplifying with (14), (53), (54), % 116.55/16.10 | (57), (58) gives: % 116.55/16.10 | (80) ? [v0: $i] : (addition(all_38_0, all_36_0) = v0 & addition(all_20_10, % 116.55/16.10 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.10 | % 116.55/16.10 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_5, % 116.55/16.10 | all_20_3, all_20_2, all_20_0, simplifying with (19), (20), (24), % 116.55/16.10 | (37), (41) gives: % 116.55/16.10 | (81) ? [v0: $i] : (addition(all_20_3, v0) = all_20_0 & addition(all_20_5, % 116.55/16.10 | all_20_1) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.10 | % 116.55/16.10 | GROUND_INST: instantiating (right_distributivity) with all_20_4, all_20_11, % 116.55/16.10 | all_20_9, all_20_3, all_20_1, all_36_0, simplifying with (13), % 116.55/16.10 | (15), (18), (28), (29), (55) gives: % 116.55/16.10 | (82) ? [v0: $i] : (multiplication(all_20_4, v0) = all_36_0 & % 116.55/16.10 | addition(all_20_11, all_20_9) = v0 & $i(v0) & $i(all_36_0)) % 116.55/16.10 | % 116.55/16.10 | GROUND_INST: instantiating (additive_commutativity) with all_20_3, all_20_1, % 116.55/16.10 | all_36_0, simplifying with (19), (20), (55) gives: % 116.55/16.10 | (83) addition(all_20_1, all_20_3) = all_36_0 & $i(all_36_0) % 116.55/16.10 | % 116.55/16.10 | ALPHA: (83) implies: % 116.55/16.10 | (84) addition(all_20_1, all_20_3) = all_36_0 % 116.55/16.10 | % 116.55/16.10 | DELTA: instantiating (78) with fresh symbol all_46_0 gives: % 116.55/16.10 | (85) addition(all_20_6, all_36_0) = all_46_0 & addition(all_20_7, all_46_0) % 116.55/16.10 | = all_20_0 & $i(all_46_0) & $i(all_20_0) % 116.55/16.10 | % 116.55/16.10 | ALPHA: (85) implies: % 116.55/16.10 | (86) $i(all_46_0) % 116.55/16.10 | (87) addition(all_20_7, all_46_0) = all_20_0 % 116.55/16.10 | (88) addition(all_20_6, all_36_0) = all_46_0 % 116.55/16.10 | % 116.55/16.10 | DELTA: instantiating (71) with fresh symbol all_48_0 gives: % 116.55/16.10 | (89) addition(all_20_8, all_48_0) = all_20_2 & addition(all_20_10, % 116.55/16.10 | all_34_0) = all_48_0 & $i(all_48_0) & $i(all_20_2) % 116.55/16.10 | % 116.55/16.10 | ALPHA: (89) implies: % 116.55/16.10 | (90) addition(all_20_10, all_34_0) = all_48_0 % 116.55/16.10 | (91) addition(all_20_8, all_48_0) = all_20_2 % 116.55/16.10 | % 116.55/16.10 | DELTA: instantiating (81) with fresh symbol all_50_0 gives: % 116.55/16.10 | (92) addition(all_20_3, all_50_0) = all_20_0 & addition(all_20_5, all_20_1) % 116.55/16.10 | = all_50_0 & $i(all_50_0) & $i(all_20_0) % 116.55/16.10 | % 116.55/16.10 | ALPHA: (92) implies: % 116.55/16.10 | (93) addition(all_20_5, all_20_1) = all_50_0 % 116.55/16.10 | (94) addition(all_20_3, all_50_0) = all_20_0 % 116.55/16.10 | % 116.55/16.10 | DELTA: instantiating (75) with fresh symbol all_52_0 gives: % 116.55/16.10 | (95) multiplication(all_52_0, all_20_11) = all_34_0 & addition(all_20_12, % 116.55/16.10 | all_20_4) = all_52_0 & $i(all_52_0) & $i(all_34_0) % 116.55/16.10 | % 116.55/16.10 | ALPHA: (95) implies: % 116.55/16.11 | (96) addition(all_20_12, all_20_4) = all_52_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (82) with fresh symbol all_54_0 gives: % 116.55/16.11 | (97) multiplication(all_20_4, all_54_0) = all_36_0 & addition(all_20_11, % 116.55/16.11 | all_20_9) = all_54_0 & $i(all_54_0) & $i(all_36_0) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (97) implies: % 116.55/16.11 | (98) addition(all_20_11, all_20_9) = all_54_0 % 116.55/16.11 | (99) multiplication(all_20_4, all_54_0) = all_36_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (70) with fresh symbol all_56_0 gives: % 116.55/16.11 | (100) addition(all_20_8, all_34_0) = all_56_0 & addition(all_20_10, % 116.55/16.11 | all_56_0) = all_20_2 & $i(all_56_0) & $i(all_20_2) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (100) implies: % 116.55/16.11 | (101) $i(all_56_0) % 116.55/16.11 | (102) addition(all_20_10, all_56_0) = all_20_2 % 116.55/16.11 | (103) addition(all_20_8, all_34_0) = all_56_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (69) with fresh symbol all_58_0 gives: % 116.55/16.11 | (104) addition(all_34_0, all_20_1) = all_58_0 & addition(all_20_7, % 116.55/16.11 | all_58_0) = all_20_0 & $i(all_58_0) & $i(all_20_0) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (104) implies: % 116.55/16.11 | (105) $i(all_58_0) % 116.55/16.11 | (106) addition(all_20_7, all_58_0) = all_20_0 % 116.55/16.11 | (107) addition(all_34_0, all_20_1) = all_58_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (80) with fresh symbol all_60_0 gives: % 116.55/16.11 | (108) addition(all_38_0, all_36_0) = all_60_0 & addition(all_20_10, % 116.55/16.11 | all_60_0) = all_20_0 & $i(all_60_0) & $i(all_20_0) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (108) implies: % 116.55/16.11 | (109) $i(all_60_0) % 116.55/16.11 | (110) addition(all_20_10, all_60_0) = all_20_0 % 116.55/16.11 | (111) addition(all_38_0, all_36_0) = all_60_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (66) with fresh symbol all_62_0 gives: % 116.55/16.11 | (112) addition(all_20_8, all_62_0) = all_20_5 & addition(all_20_10, % 116.55/16.11 | all_20_6) = all_62_0 & $i(all_62_0) & $i(all_20_5) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (112) implies: % 116.55/16.11 | (113) addition(all_20_10, all_20_6) = all_62_0 % 116.55/16.11 | (114) addition(all_20_8, all_62_0) = all_20_5 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (62) with fresh symbol all_64_0 gives: % 116.55/16.11 | (115) addition(all_38_0, all_20_3) = all_64_0 & addition(all_20_10, % 116.55/16.11 | all_64_0) = all_20_2 & $i(all_64_0) & $i(all_20_2) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (115) implies: % 116.55/16.11 | (116) $i(all_64_0) % 116.55/16.11 | (117) addition(all_20_10, all_64_0) = all_20_2 % 116.55/16.11 | (118) addition(all_38_0, all_20_3) = all_64_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (65) with fresh symbol all_66_0 gives: % 116.55/16.11 | (119) multiplication(all_66_0, all_20_12) = all_20_7 & addition(all_20_9, % 116.55/16.11 | all_20_11) = all_66_0 & $i(all_66_0) & $i(all_20_7) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (119) implies: % 116.55/16.11 | (120) addition(all_20_9, all_20_11) = all_66_0 % 116.55/16.11 | (121) multiplication(all_66_0, all_20_12) = all_20_7 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (79) with fresh symbol all_68_0 gives: % 116.55/16.11 | (122) addition(all_20_6, all_68_0) = all_20_0 & addition(all_20_7, % 116.55/16.11 | all_36_0) = all_68_0 & $i(all_68_0) & $i(all_20_0) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (122) implies: % 116.55/16.11 | (123) addition(all_20_7, all_36_0) = all_68_0 % 116.55/16.11 | % 116.55/16.11 | DELTA: instantiating (74) with fresh symbol all_70_0 gives: % 116.55/16.11 | (124) addition(all_20_6, all_70_0) = all_20_2 & addition(all_20_7, % 116.55/16.11 | all_20_3) = all_70_0 & $i(all_70_0) & $i(all_20_2) % 116.55/16.11 | % 116.55/16.11 | ALPHA: (124) implies: % 116.55/16.11 | (125) addition(all_20_7, all_20_3) = all_70_0 % 116.55/16.11 | (126) addition(all_20_6, all_70_0) = all_20_2 % 116.55/16.11 | % 116.55/16.11 | GROUND_INST: instantiating (6) with all_32_0, all_54_0, all_20_9, all_20_11, % 116.55/16.11 | simplifying with (47), (98) gives: % 116.55/16.11 | (127) all_54_0 = all_32_0 % 116.55/16.11 | % 116.55/16.11 | GROUND_INST: instantiating (6) with all_32_0, all_66_0, all_20_11, all_20_9, % 116.55/16.11 | simplifying with (61), (120) gives: % 116.55/16.11 | (128) all_66_0 = all_32_0 % 116.55/16.12 | % 116.55/16.12 | REDUCE: (121), (128) imply: % 116.55/16.12 | (129) multiplication(all_32_0, all_20_12) = all_20_7 % 116.55/16.12 | % 116.55/16.12 | REDUCE: (99), (127) imply: % 116.55/16.12 | (130) multiplication(all_20_4, all_32_0) = all_36_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_12, all_20_4, % 116.55/16.12 | all_52_0, simplifying with (12), (18), (96) gives: % 116.55/16.12 | (131) addition(all_20_4, all_20_12) = all_52_0 & $i(all_52_0) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (131) implies: % 116.55/16.12 | (132) addition(all_20_4, all_20_12) = all_52_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_20_6, % 116.55/16.12 | all_62_0, simplifying with (14), (17), (113) gives: % 116.55/16.12 | (133) addition(all_20_6, all_20_10) = all_62_0 & $i(all_62_0) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (133) implies: % 116.55/16.12 | (134) $i(all_62_0) % 116.55/16.12 | (135) addition(all_20_6, all_20_10) = all_62_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_34_0, % 116.55/16.12 | all_48_0, simplifying with (14), (49), (90) gives: % 116.55/16.12 | (136) addition(all_34_0, all_20_10) = all_48_0 & $i(all_48_0) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (136) implies: % 116.55/16.12 | (137) $i(all_48_0) % 116.55/16.12 | (138) addition(all_34_0, all_20_10) = all_48_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_56_0, % 116.55/16.12 | all_20_10, all_20_2, all_20_0, simplifying with (14), (20), (24), % 116.55/16.12 | (101), (102) gives: % 116.55/16.12 | (139) ? [v0: $i] : (addition(all_56_0, all_20_1) = v0 & % 116.55/16.12 | addition(all_20_10, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_60_0, % 116.55/16.12 | all_20_0, simplifying with (14), (109), (110) gives: % 116.55/16.12 | (140) addition(all_60_0, all_20_10) = all_20_0 & $i(all_20_0) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (140) implies: % 116.55/16.12 | (141) addition(all_60_0, all_20_10) = all_20_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_64_0, % 116.55/16.12 | all_20_10, all_20_2, all_20_0, simplifying with (14), (20), (24), % 116.55/16.12 | (116), (117) gives: % 116.55/16.12 | (142) ? [v0: $i] : (addition(all_64_0, all_20_1) = v0 & % 116.55/16.12 | addition(all_20_10, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_64_0, % 116.55/16.12 | all_20_2, simplifying with (14), (116), (117) gives: % 116.55/16.12 | (143) addition(all_64_0, all_20_10) = all_20_2 & $i(all_20_2) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (143) implies: % 116.55/16.12 | (144) addition(all_64_0, all_20_10) = all_20_2 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (3) with all_20_9, all_20_11, all_32_0, simplifying % 116.55/16.12 | with (13), (15), (45), (61) gives: % 116.55/16.12 | (145) all_32_0 = one % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_34_0, % 116.55/16.12 | all_56_0, simplifying with (16), (49), (103) gives: % 116.55/16.12 | (146) addition(all_34_0, all_20_8) = all_56_0 & $i(all_56_0) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (146) implies: % 116.55/16.12 | (147) addition(all_34_0, all_20_8) = all_56_0 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_48_0, % 116.55/16.12 | all_20_8, all_20_2, all_20_0, simplifying with (16), (20), (24), % 116.55/16.12 | (91), (137) gives: % 116.55/16.12 | (148) ? [v0: $i] : (addition(all_48_0, all_20_1) = v0 & addition(all_20_8, % 116.55/16.12 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_48_0, % 116.55/16.12 | all_20_2, simplifying with (16), (91), (137) gives: % 116.55/16.12 | (149) addition(all_48_0, all_20_8) = all_20_2 & $i(all_20_2) % 116.55/16.12 | % 116.55/16.12 | ALPHA: (149) implies: % 116.55/16.12 | (150) addition(all_48_0, all_20_8) = all_20_2 % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_62_0, % 116.55/16.12 | all_20_8, all_20_5, all_20_0, simplifying with (16), (53), (54), % 116.55/16.12 | (114), (134) gives: % 116.55/16.12 | (151) ? [v0: $i] : (addition(all_62_0, all_36_0) = v0 & addition(all_20_8, % 116.55/16.12 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.12 | % 116.55/16.12 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_62_0, % 116.55/16.12 | all_20_8, all_20_5, all_20_2, simplifying with (16), (19), (23), % 116.55/16.12 | (114), (134) gives: % 116.55/16.13 | (152) ? [v0: $i] : (addition(all_62_0, all_20_3) = v0 & addition(all_20_8, % 116.55/16.13 | v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_62_0, % 116.55/16.13 | all_20_5, simplifying with (16), (114), (134) gives: % 116.55/16.13 | (153) addition(all_62_0, all_20_8) = all_20_5 & $i(all_20_5) % 116.55/16.13 | % 116.55/16.13 | ALPHA: (153) implies: % 116.55/16.13 | (154) addition(all_62_0, all_20_8) = all_20_5 % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_10, % 116.55/16.13 | all_20_8, all_20_7, all_70_0, simplifying with (14), (16), (19), % 116.55/16.13 | (34), (125) gives: % 116.55/16.13 | (155) ? [v0: $i] : (addition(all_20_8, v0) = all_70_0 & % 116.55/16.13 | addition(all_20_10, all_20_3) = v0 & $i(v0) & $i(all_70_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_8, % 116.55/16.13 | all_20_10, all_20_7, all_70_0, simplifying with (14), (16), (19), % 116.55/16.13 | (21), (125) gives: % 116.55/16.13 | (156) ? [v0: $i] : (addition(all_20_8, all_20_3) = v0 & % 116.55/16.13 | addition(all_20_10, v0) = all_70_0 & $i(v0) & $i(all_70_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_commutativity) with all_20_7, all_20_3, % 116.55/16.13 | all_70_0, simplifying with (19), (33), (125) gives: % 116.55/16.13 | (157) addition(all_20_3, all_20_7) = all_70_0 & $i(all_70_0) % 116.55/16.13 | % 116.55/16.13 | ALPHA: (157) implies: % 116.55/16.13 | (158) $i(all_70_0) % 116.55/16.13 | (159) addition(all_20_3, all_20_7) = all_70_0 % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_10, % 116.55/16.13 | all_20_8, all_20_7, all_68_0, simplifying with (14), (16), (34), % 116.55/16.13 | (53), (123) gives: % 116.55/16.13 | (160) ? [v0: $i] : (addition(all_20_8, v0) = all_68_0 & % 116.55/16.13 | addition(all_20_10, all_36_0) = v0 & $i(v0) & $i(all_68_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_commutativity) with all_20_7, all_36_0, % 116.55/16.13 | all_68_0, simplifying with (33), (53), (123) gives: % 116.55/16.13 | (161) addition(all_36_0, all_20_7) = all_68_0 & $i(all_68_0) % 116.55/16.13 | % 116.55/16.13 | ALPHA: (161) implies: % 116.55/16.13 | (162) addition(all_36_0, all_20_7) = all_68_0 % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_46_0, all_20_10, % 116.55/16.13 | all_20_8, all_20_7, all_20_0, simplifying with (14), (16), (34), % 116.55/16.13 | (86), (87) gives: % 116.55/16.13 | (163) ? [v0: $i] : (addition(all_20_8, v0) = all_20_0 & % 116.55/16.13 | addition(all_20_10, all_46_0) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_46_0, all_20_8, % 116.55/16.13 | all_20_10, all_20_7, all_20_0, simplifying with (14), (16), (21), % 116.55/16.13 | (86), (87) gives: % 116.55/16.13 | (164) ? [v0: $i] : (addition(all_20_8, all_46_0) = v0 & % 116.55/16.13 | addition(all_20_10, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_58_0, all_20_10, % 116.55/16.13 | all_20_8, all_20_7, all_20_0, simplifying with (14), (16), (34), % 116.55/16.13 | (105), (106) gives: % 116.55/16.13 | (165) ? [v0: $i] : (addition(all_20_8, v0) = all_20_0 & % 116.55/16.13 | addition(all_20_10, all_58_0) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_58_0, all_20_8, % 116.55/16.13 | all_20_10, all_20_7, all_20_0, simplifying with (14), (16), (21), % 116.55/16.13 | (105), (106) gives: % 116.55/16.13 | (166) ? [v0: $i] : (addition(all_20_8, all_58_0) = v0 & % 116.55/16.13 | addition(all_20_10, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_70_0, % 116.55/16.13 | all_20_6, all_20_2, all_20_0, simplifying with (17), (20), (24), % 116.55/16.13 | (126), (158) gives: % 116.55/16.13 | (167) ? [v0: $i] : (addition(all_70_0, all_20_1) = v0 & addition(all_20_6, % 116.55/16.13 | v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_commutativity) with all_20_6, all_70_0, % 116.55/16.13 | all_20_2, simplifying with (17), (126), (158) gives: % 116.55/16.13 | (168) addition(all_70_0, all_20_6) = all_20_2 & $i(all_20_2) % 116.55/16.13 | % 116.55/16.13 | ALPHA: (168) implies: % 116.55/16.13 | (169) addition(all_70_0, all_20_6) = all_20_2 % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_7, % 116.55/16.13 | all_20_6, all_20_5, all_50_0, simplifying with (17), (20), (33), % 116.55/16.13 | (38), (93) gives: % 116.55/16.13 | (170) ? [v0: $i] : (addition(all_20_6, v0) = all_50_0 & addition(all_20_7, % 116.55/16.13 | all_20_1) = v0 & $i(v0) & $i(all_50_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_6, % 116.55/16.13 | all_20_7, all_20_5, all_50_0, simplifying with (17), (20), (22), % 116.55/16.13 | (33), (93) gives: % 116.55/16.13 | (171) ? [v0: $i] : (addition(all_20_6, all_20_1) = v0 & addition(all_20_7, % 116.55/16.13 | v0) = all_50_0 & $i(v0) & $i(all_50_0)) % 116.55/16.13 | % 116.55/16.13 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_38_0, % 116.55/16.13 | all_20_10, all_20_5, all_50_0, simplifying with (14), (20), (57), % 116.55/16.13 | (58), (93) gives: % 116.55/16.14 | (172) ? [v0: $i] : (addition(all_38_0, all_20_1) = v0 & % 116.55/16.14 | addition(all_20_10, v0) = all_50_0 & $i(v0) & $i(all_50_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_62_0, % 116.55/16.14 | all_20_8, all_20_5, all_50_0, simplifying with (16), (20), (93), % 116.55/16.14 | (114), (134) gives: % 116.55/16.14 | (173) ? [v0: $i] : (addition(all_62_0, all_20_1) = v0 & addition(all_20_8, % 116.55/16.14 | v0) = all_50_0 & $i(v0) & $i(all_50_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_commutativity) with all_20_5, all_20_1, % 116.55/16.14 | all_50_0, simplifying with (20), (37), (93) gives: % 116.55/16.14 | (174) addition(all_20_1, all_20_5) = all_50_0 & $i(all_50_0) % 116.55/16.14 | % 116.55/16.14 | ALPHA: (174) implies: % 116.55/16.14 | (175) $i(all_50_0) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (left_distributivity) with all_20_4, all_20_12, % 116.55/16.14 | all_20_11, all_20_3, all_20_6, all_34_0, simplifying with (12), % 116.55/16.14 | (13), (18), (25), (28), (77) gives: % 116.55/16.14 | (176) ? [v0: $i] : (multiplication(v0, all_20_11) = all_34_0 & % 116.55/16.14 | addition(all_20_4, all_20_12) = v0 & $i(v0) & $i(all_34_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_commutativity) with all_20_3, all_50_0, % 116.55/16.14 | all_20_0, simplifying with (19), (94), (175) gives: % 116.55/16.14 | (177) addition(all_50_0, all_20_3) = all_20_0 & $i(all_20_0) % 116.55/16.14 | % 116.55/16.14 | ALPHA: (177) implies: % 116.55/16.14 | (178) addition(all_50_0, all_20_3) = all_20_0 % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_7, % 116.55/16.14 | all_34_0, all_20_2, all_20_0, simplifying with (20), (24), (33), % 116.55/16.14 | (49), (73) gives: % 116.55/16.14 | (179) ? [v0: $i] : (addition(all_34_0, v0) = all_20_0 & addition(all_20_7, % 116.55/16.14 | all_20_1) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_7, all_20_3, % 116.55/16.14 | all_20_6, all_34_0, all_20_2, simplifying with (17), (19), (33), % 116.55/16.14 | (51), (73) gives: % 116.55/16.14 | (180) ? [v0: $i] : (addition(all_20_3, all_20_7) = v0 & addition(all_20_6, % 116.55/16.14 | v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 116.55/16.14 | all_20_6, all_34_0, all_58_0, simplifying with (17), (19), (20), % 116.55/16.14 | (51), (107) gives: % 116.55/16.14 | (181) ? [v0: $i] : (addition(all_20_3, all_20_1) = v0 & addition(all_20_6, % 116.55/16.14 | v0) = all_58_0 & $i(v0) & $i(all_58_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_6, % 116.55/16.14 | all_20_3, all_34_0, all_58_0, simplifying with (17), (19), (20), % 116.55/16.14 | (77), (107) gives: % 116.55/16.14 | (182) ? [v0: $i] : (addition(all_20_3, v0) = all_58_0 & addition(all_20_6, % 116.55/16.14 | all_20_1) = v0 & $i(v0) & $i(all_58_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_10, % 116.55/16.14 | all_38_0, all_20_5, all_20_0, simplifying with (14), (53), (54), % 116.55/16.14 | (57), (64) gives: % 116.55/16.14 | (183) ? [v0: $i] : (addition(all_38_0, v0) = all_20_0 & % 116.55/16.14 | addition(all_20_10, all_36_0) = v0 & $i(v0) & $i(all_20_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_10, % 116.55/16.14 | all_38_0, all_20_5, all_20_2, simplifying with (14), (19), (23), % 116.55/16.14 | (57), (64) gives: % 116.55/16.14 | (184) ? [v0: $i] : (addition(all_38_0, v0) = all_20_2 & % 116.55/16.14 | addition(all_20_10, all_20_3) = v0 & $i(v0) & $i(all_20_2)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_20_6, % 116.55/16.14 | all_20_8, all_38_0, all_20_5, simplifying with (14), (16), (17), % 116.55/16.14 | (59), (64) gives: % 116.55/16.14 | (185) ? [v0: $i] : (addition(all_20_6, all_20_10) = v0 & % 116.55/16.14 | addition(all_20_8, v0) = all_20_5 & $i(v0) & $i(all_20_5)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_10, % 116.55/16.14 | all_38_0, all_20_5, all_50_0, simplifying with (14), (20), (57), % 116.55/16.14 | (64), (93) gives: % 116.55/16.14 | (186) ? [v0: $i] : (addition(all_38_0, v0) = all_50_0 & % 116.55/16.14 | addition(all_20_10, all_20_1) = v0 & $i(v0) & $i(all_50_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_6, % 116.55/16.14 | all_20_8, all_38_0, all_64_0, simplifying with (16), (17), (19), % 116.55/16.14 | (59), (118) gives: % 116.55/16.14 | (187) ? [v0: $i] : (addition(all_20_6, all_20_3) = v0 & addition(all_20_8, % 116.55/16.14 | v0) = all_64_0 & $i(v0) & $i(all_64_0)) % 116.55/16.14 | % 116.55/16.14 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_8, % 116.55/16.14 | all_20_6, all_38_0, all_64_0, simplifying with (16), (17), (19), % 116.55/16.14 | (68), (118) gives: % 116.88/16.14 | (188) ? [v0: $i] : (addition(all_20_6, v0) = all_64_0 & addition(all_20_8, % 116.88/16.14 | all_20_3) = v0 & $i(v0) & $i(all_64_0)) % 116.88/16.14 | % 116.88/16.14 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_6, % 116.88/16.14 | all_20_8, all_38_0, all_60_0, simplifying with (16), (17), (53), % 116.88/16.14 | (59), (111) gives: % 116.88/16.14 | (189) ? [v0: $i] : (addition(all_20_6, all_36_0) = v0 & addition(all_20_8, % 116.88/16.14 | v0) = all_60_0 & $i(v0) & $i(all_60_0)) % 116.88/16.14 | % 116.88/16.14 | DELTA: instantiating (151) with fresh symbol all_86_0 gives: % 116.88/16.15 | (190) addition(all_62_0, all_36_0) = all_86_0 & addition(all_20_8, % 116.88/16.15 | all_86_0) = all_20_0 & $i(all_86_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (190) implies: % 116.88/16.15 | (191) addition(all_62_0, all_36_0) = all_86_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (142) with fresh symbol all_88_0 gives: % 116.88/16.15 | (192) addition(all_64_0, all_20_1) = all_88_0 & addition(all_20_10, % 116.88/16.15 | all_88_0) = all_20_0 & $i(all_88_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (192) implies: % 116.88/16.15 | (193) addition(all_64_0, all_20_1) = all_88_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (165) with fresh symbol all_90_0 gives: % 116.88/16.15 | (194) addition(all_20_8, all_90_0) = all_20_0 & addition(all_20_10, % 116.88/16.15 | all_58_0) = all_90_0 & $i(all_90_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (194) implies: % 116.88/16.15 | (195) addition(all_20_10, all_58_0) = all_90_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (160) with fresh symbol all_94_0 gives: % 116.88/16.15 | (196) addition(all_20_8, all_94_0) = all_68_0 & addition(all_20_10, % 116.88/16.15 | all_36_0) = all_94_0 & $i(all_94_0) & $i(all_68_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (196) implies: % 116.88/16.15 | (197) addition(all_20_10, all_36_0) = all_94_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (181) with fresh symbol all_96_0 gives: % 116.88/16.15 | (198) addition(all_20_3, all_20_1) = all_96_0 & addition(all_20_6, % 116.88/16.15 | all_96_0) = all_58_0 & $i(all_96_0) & $i(all_58_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (198) implies: % 116.88/16.15 | (199) $i(all_96_0) % 116.88/16.15 | (200) addition(all_20_6, all_96_0) = all_58_0 % 116.88/16.15 | (201) addition(all_20_3, all_20_1) = all_96_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (180) with fresh symbol all_98_0 gives: % 116.88/16.15 | (202) addition(all_20_3, all_20_7) = all_98_0 & addition(all_20_6, % 116.88/16.15 | all_98_0) = all_20_2 & $i(all_98_0) & $i(all_20_2) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (202) implies: % 116.88/16.15 | (203) addition(all_20_3, all_20_7) = all_98_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (152) with fresh symbol all_100_0 gives: % 116.88/16.15 | (204) addition(all_62_0, all_20_3) = all_100_0 & addition(all_20_8, % 116.88/16.15 | all_100_0) = all_20_2 & $i(all_100_0) & $i(all_20_2) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (204) implies: % 116.88/16.15 | (205) addition(all_62_0, all_20_3) = all_100_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (189) with fresh symbol all_104_0 gives: % 116.88/16.15 | (206) addition(all_20_6, all_36_0) = all_104_0 & addition(all_20_8, % 116.88/16.15 | all_104_0) = all_60_0 & $i(all_104_0) & $i(all_60_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (206) implies: % 116.88/16.15 | (207) addition(all_20_8, all_104_0) = all_60_0 % 116.88/16.15 | (208) addition(all_20_6, all_36_0) = all_104_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (148) with fresh symbol all_106_0 gives: % 116.88/16.15 | (209) addition(all_48_0, all_20_1) = all_106_0 & addition(all_20_8, % 116.88/16.15 | all_106_0) = all_20_0 & $i(all_106_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (209) implies: % 116.88/16.15 | (210) addition(all_48_0, all_20_1) = all_106_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (139) with fresh symbol all_108_0 gives: % 116.88/16.15 | (211) addition(all_56_0, all_20_1) = all_108_0 & addition(all_20_10, % 116.88/16.15 | all_108_0) = all_20_0 & $i(all_108_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (211) implies: % 116.88/16.15 | (212) addition(all_56_0, all_20_1) = all_108_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (156) with fresh symbol all_110_0 gives: % 116.88/16.15 | (213) addition(all_20_8, all_20_3) = all_110_0 & addition(all_20_10, % 116.88/16.15 | all_110_0) = all_70_0 & $i(all_110_0) & $i(all_70_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (213) implies: % 116.88/16.15 | (214) addition(all_20_10, all_110_0) = all_70_0 % 116.88/16.15 | (215) addition(all_20_8, all_20_3) = all_110_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (164) with fresh symbol all_112_0 gives: % 116.88/16.15 | (216) addition(all_20_8, all_46_0) = all_112_0 & addition(all_20_10, % 116.88/16.15 | all_112_0) = all_20_0 & $i(all_112_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (216) implies: % 116.88/16.15 | (217) addition(all_20_8, all_46_0) = all_112_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (163) with fresh symbol all_114_0 gives: % 116.88/16.15 | (218) addition(all_20_8, all_114_0) = all_20_0 & addition(all_20_10, % 116.88/16.15 | all_46_0) = all_114_0 & $i(all_114_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (218) implies: % 116.88/16.15 | (219) addition(all_20_10, all_46_0) = all_114_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (166) with fresh symbol all_116_0 gives: % 116.88/16.15 | (220) addition(all_20_8, all_58_0) = all_116_0 & addition(all_20_10, % 116.88/16.15 | all_116_0) = all_20_0 & $i(all_116_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (220) implies: % 116.88/16.15 | (221) addition(all_20_8, all_58_0) = all_116_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (171) with fresh symbol all_118_0 gives: % 116.88/16.15 | (222) addition(all_20_6, all_20_1) = all_118_0 & addition(all_20_7, % 116.88/16.15 | all_118_0) = all_50_0 & $i(all_118_0) & $i(all_50_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (222) implies: % 116.88/16.15 | (223) addition(all_20_7, all_118_0) = all_50_0 % 116.88/16.15 | (224) addition(all_20_6, all_20_1) = all_118_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (182) with fresh symbol all_120_0 gives: % 116.88/16.15 | (225) addition(all_20_3, all_120_0) = all_58_0 & addition(all_20_6, % 116.88/16.15 | all_20_1) = all_120_0 & $i(all_120_0) & $i(all_58_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (225) implies: % 116.88/16.15 | (226) addition(all_20_6, all_20_1) = all_120_0 % 116.88/16.15 | (227) addition(all_20_3, all_120_0) = all_58_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (179) with fresh symbol all_122_0 gives: % 116.88/16.15 | (228) addition(all_34_0, all_122_0) = all_20_0 & addition(all_20_7, % 116.88/16.15 | all_20_1) = all_122_0 & $i(all_122_0) & $i(all_20_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (228) implies: % 116.88/16.15 | (229) addition(all_20_7, all_20_1) = all_122_0 % 116.88/16.15 | (230) addition(all_34_0, all_122_0) = all_20_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (155) with fresh symbol all_124_0 gives: % 116.88/16.15 | (231) addition(all_20_8, all_124_0) = all_70_0 & addition(all_20_10, % 116.88/16.15 | all_20_3) = all_124_0 & $i(all_124_0) & $i(all_70_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (231) implies: % 116.88/16.15 | (232) addition(all_20_10, all_20_3) = all_124_0 % 116.88/16.15 | (233) addition(all_20_8, all_124_0) = all_70_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (188) with fresh symbol all_126_0 gives: % 116.88/16.15 | (234) addition(all_20_6, all_126_0) = all_64_0 & addition(all_20_8, % 116.88/16.15 | all_20_3) = all_126_0 & $i(all_126_0) & $i(all_64_0) % 116.88/16.15 | % 116.88/16.15 | ALPHA: (234) implies: % 116.88/16.15 | (235) addition(all_20_8, all_20_3) = all_126_0 % 116.88/16.15 | (236) addition(all_20_6, all_126_0) = all_64_0 % 116.88/16.15 | % 116.88/16.15 | DELTA: instantiating (170) with fresh symbol all_128_0 gives: % 116.88/16.15 | (237) addition(all_20_6, all_128_0) = all_50_0 & addition(all_20_7, % 116.88/16.15 | all_20_1) = all_128_0 & $i(all_128_0) & $i(all_50_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (237) implies: % 116.88/16.16 | (238) addition(all_20_7, all_20_1) = all_128_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (187) with fresh symbol all_130_0 gives: % 116.88/16.16 | (239) addition(all_20_6, all_20_3) = all_130_0 & addition(all_20_8, % 116.88/16.16 | all_130_0) = all_64_0 & $i(all_130_0) & $i(all_64_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (239) implies: % 116.88/16.16 | (240) $i(all_130_0) % 116.88/16.16 | (241) addition(all_20_8, all_130_0) = all_64_0 % 116.88/16.16 | (242) addition(all_20_6, all_20_3) = all_130_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (185) with fresh symbol all_132_0 gives: % 116.88/16.16 | (243) addition(all_20_6, all_20_10) = all_132_0 & addition(all_20_8, % 116.88/16.16 | all_132_0) = all_20_5 & $i(all_132_0) & $i(all_20_5) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (243) implies: % 116.88/16.16 | (244) $i(all_132_0) % 116.88/16.16 | (245) addition(all_20_6, all_20_10) = all_132_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (176) with fresh symbol all_134_0 gives: % 116.88/16.16 | (246) multiplication(all_134_0, all_20_11) = all_34_0 & addition(all_20_4, % 116.88/16.16 | all_20_12) = all_134_0 & $i(all_134_0) & $i(all_34_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (246) implies: % 116.88/16.16 | (247) addition(all_20_4, all_20_12) = all_134_0 % 116.88/16.16 | (248) multiplication(all_134_0, all_20_11) = all_34_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (183) with fresh symbol all_136_0 gives: % 116.88/16.16 | (249) addition(all_38_0, all_136_0) = all_20_0 & addition(all_20_10, % 116.88/16.16 | all_36_0) = all_136_0 & $i(all_136_0) & $i(all_20_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (249) implies: % 116.88/16.16 | (250) addition(all_20_10, all_36_0) = all_136_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (173) with fresh symbol all_140_0 gives: % 116.88/16.16 | (251) addition(all_62_0, all_20_1) = all_140_0 & addition(all_20_8, % 116.88/16.16 | all_140_0) = all_50_0 & $i(all_140_0) & $i(all_50_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (251) implies: % 116.88/16.16 | (252) addition(all_62_0, all_20_1) = all_140_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (167) with fresh symbol all_142_0 gives: % 116.88/16.16 | (253) addition(all_70_0, all_20_1) = all_142_0 & addition(all_20_6, % 116.88/16.16 | all_142_0) = all_20_0 & $i(all_142_0) & $i(all_20_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (253) implies: % 116.88/16.16 | (254) $i(all_142_0) % 116.88/16.16 | (255) addition(all_20_6, all_142_0) = all_20_0 % 116.88/16.16 | (256) addition(all_70_0, all_20_1) = all_142_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (172) with fresh symbol all_144_0 gives: % 116.88/16.16 | (257) addition(all_38_0, all_20_1) = all_144_0 & addition(all_20_10, % 116.88/16.16 | all_144_0) = all_50_0 & $i(all_144_0) & $i(all_50_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (257) implies: % 116.88/16.16 | (258) addition(all_38_0, all_20_1) = all_144_0 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (184) with fresh symbol all_146_0 gives: % 116.88/16.16 | (259) addition(all_38_0, all_146_0) = all_20_2 & addition(all_20_10, % 116.88/16.16 | all_20_3) = all_146_0 & $i(all_146_0) & $i(all_20_2) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (259) implies: % 116.88/16.16 | (260) addition(all_20_10, all_20_3) = all_146_0 % 116.88/16.16 | (261) addition(all_38_0, all_146_0) = all_20_2 % 116.88/16.16 | % 116.88/16.16 | DELTA: instantiating (186) with fresh symbol all_148_0 gives: % 116.88/16.16 | (262) addition(all_38_0, all_148_0) = all_50_0 & addition(all_20_10, % 116.88/16.16 | all_20_1) = all_148_0 & $i(all_148_0) & $i(all_50_0) % 116.88/16.16 | % 116.88/16.16 | ALPHA: (262) implies: % 116.88/16.16 | (263) addition(all_20_10, all_20_1) = all_148_0 % 116.88/16.16 | (264) addition(all_38_0, all_148_0) = all_50_0 % 116.88/16.16 | % 116.88/16.16 | REDUCE: (129), (145) imply: % 116.88/16.16 | (265) multiplication(one, all_20_12) = all_20_7 % 116.88/16.16 | % 116.88/16.16 | REDUCE: (130), (145) imply: % 116.88/16.16 | (266) multiplication(all_20_4, one) = all_36_0 % 116.88/16.16 | % 116.88/16.16 | REDUCE: (61), (145) imply: % 116.88/16.16 | (267) addition(all_20_9, all_20_11) = one % 116.88/16.16 | % 116.88/16.16 | REDUCE: (47), (145) imply: % 116.88/16.16 | (268) addition(all_20_11, all_20_9) = one % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_124_0, all_146_0, all_20_3, all_20_10, % 116.88/16.16 | simplifying with (232), (260) gives: % 116.88/16.16 | (269) all_146_0 = all_124_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_94_0, all_136_0, all_36_0, all_20_10, % 116.88/16.16 | simplifying with (197), (250) gives: % 116.88/16.16 | (270) all_136_0 = all_94_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_110_0, all_126_0, all_20_3, all_20_8, % 116.88/16.16 | simplifying with (215), (235) gives: % 116.88/16.16 | (271) all_126_0 = all_110_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_122_0, all_128_0, all_20_1, all_20_7, % 116.88/16.16 | simplifying with (229), (238) gives: % 116.88/16.16 | (272) all_128_0 = all_122_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_62_0, all_132_0, all_20_10, all_20_6, % 116.88/16.16 | simplifying with (135), (245) gives: % 116.88/16.16 | (273) all_132_0 = all_62_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_34_0, all_130_0, all_20_3, all_20_6, % 116.88/16.16 | simplifying with (51), (242) gives: % 116.88/16.16 | (274) all_130_0 = all_34_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_118_0, all_120_0, all_20_1, all_20_6, % 116.88/16.16 | simplifying with (224), (226) gives: % 116.88/16.16 | (275) all_120_0 = all_118_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_46_0, all_104_0, all_36_0, all_20_6, % 116.88/16.16 | simplifying with (88), (208) gives: % 116.88/16.16 | (276) all_104_0 = all_46_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_52_0, all_134_0, all_20_12, all_20_4, % 116.88/16.16 | simplifying with (132), (247) gives: % 116.88/16.16 | (277) all_134_0 = all_52_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_70_0, all_98_0, all_20_7, all_20_3, % 116.88/16.16 | simplifying with (159), (203) gives: % 116.88/16.16 | (278) all_98_0 = all_70_0 % 116.88/16.16 | % 116.88/16.16 | GROUND_INST: instantiating (6) with all_36_0, all_96_0, all_20_1, all_20_3, % 116.88/16.16 | simplifying with (55), (201) gives: % 116.88/16.16 | (279) all_96_0 = all_36_0 % 116.88/16.16 | % 116.88/16.16 | REDUCE: (248), (277) imply: % 116.88/16.16 | (280) multiplication(all_52_0, all_20_11) = all_34_0 % 116.88/16.16 | % 116.88/16.16 | REDUCE: (261), (269) imply: % 116.88/16.16 | (281) addition(all_38_0, all_124_0) = all_20_2 % 116.97/16.16 | % 116.97/16.16 | REDUCE: (227), (275) imply: % 116.97/16.16 | (282) addition(all_20_3, all_118_0) = all_58_0 % 116.97/16.16 | % 116.97/16.16 | REDUCE: (236), (271) imply: % 116.97/16.16 | (283) addition(all_20_6, all_110_0) = all_64_0 % 116.97/16.16 | % 116.97/16.16 | REDUCE: (200), (279) imply: % 116.97/16.16 | (284) addition(all_20_6, all_36_0) = all_58_0 % 116.97/16.16 | % 116.97/16.16 | REDUCE: (241), (274) imply: % 116.97/16.16 | (285) addition(all_20_8, all_34_0) = all_64_0 % 116.97/16.16 | % 116.97/16.16 | REDUCE: (207), (276) imply: % 116.97/16.16 | (286) addition(all_20_8, all_46_0) = all_60_0 % 116.97/16.16 | % 116.97/16.16 | GROUND_INST: instantiating (6) with all_56_0, all_64_0, all_34_0, all_20_8, % 116.97/16.16 | simplifying with (103), (285) gives: % 116.97/16.16 | (287) all_64_0 = all_56_0 % 116.97/16.16 | % 116.97/16.16 | GROUND_INST: instantiating (6) with all_112_0, all_60_0, all_46_0, all_20_8, % 116.97/16.16 | simplifying with (217), (286) gives: % 116.97/16.16 | (288) all_112_0 = all_60_0 % 116.97/16.16 | % 116.97/16.16 | GROUND_INST: instantiating (6) with all_46_0, all_58_0, all_36_0, all_20_6, % 116.97/16.16 | simplifying with (88), (284) gives: % 116.97/16.17 | (289) all_58_0 = all_46_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (193), (287) imply: % 116.97/16.17 | (290) addition(all_56_0, all_20_1) = all_88_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (144), (287) imply: % 116.97/16.17 | (291) addition(all_56_0, all_20_10) = all_20_2 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (118), (287) imply: % 116.97/16.17 | (292) addition(all_38_0, all_20_3) = all_56_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (107), (289) imply: % 116.97/16.17 | (293) addition(all_34_0, all_20_1) = all_46_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (282), (289) imply: % 116.97/16.17 | (294) addition(all_20_3, all_118_0) = all_46_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (283), (287) imply: % 116.97/16.17 | (295) addition(all_20_6, all_110_0) = all_56_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (221), (289) imply: % 116.97/16.17 | (296) addition(all_20_8, all_46_0) = all_116_0 % 116.97/16.17 | % 116.97/16.17 | REDUCE: (195), (289) imply: % 116.97/16.17 | (297) addition(all_20_10, all_46_0) = all_90_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (6) with all_114_0, all_90_0, all_46_0, all_20_10, % 116.97/16.17 | simplifying with (219), (297) gives: % 116.97/16.17 | (298) all_114_0 = all_90_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (6) with all_60_0, all_116_0, all_46_0, all_20_8, % 116.97/16.17 | simplifying with (286), (296) gives: % 116.97/16.17 | (299) all_116_0 = all_60_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (6) with all_108_0, all_88_0, all_20_1, all_56_0, % 116.97/16.17 | simplifying with (212), (290) gives: % 116.97/16.17 | (300) all_108_0 = all_88_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_20_3, % 116.97/16.17 | all_124_0, simplifying with (14), (19), (232) gives: % 116.97/16.17 | (301) addition(all_20_3, all_20_10) = all_124_0 & $i(all_124_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (301) implies: % 116.97/16.17 | (302) $i(all_124_0) % 116.97/16.17 | (303) addition(all_20_3, all_20_10) = all_124_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_20_1, % 116.97/16.17 | all_148_0, simplifying with (14), (20), (263) gives: % 116.97/16.17 | (304) addition(all_20_1, all_20_10) = all_148_0 & $i(all_148_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (304) implies: % 116.97/16.17 | (305) $i(all_148_0) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_36_0, % 116.97/16.17 | all_94_0, simplifying with (14), (53), (197) gives: % 116.97/16.17 | (306) addition(all_36_0, all_20_10) = all_94_0 & $i(all_94_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (306) implies: % 116.97/16.17 | (307) addition(all_36_0, all_20_10) = all_94_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_10, all_46_0, % 116.97/16.17 | all_90_0, simplifying with (14), (86), (297) gives: % 116.97/16.17 | (308) addition(all_46_0, all_20_10) = all_90_0 & $i(all_90_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (308) implies: % 116.97/16.17 | (309) addition(all_46_0, all_20_10) = all_90_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_20_3, % 116.97/16.17 | all_110_0, simplifying with (16), (19), (215) gives: % 116.97/16.17 | (310) addition(all_20_3, all_20_8) = all_110_0 & $i(all_110_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (310) implies: % 116.97/16.17 | (311) $i(all_110_0) % 116.97/16.17 | (312) addition(all_20_3, all_20_8) = all_110_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_124_0, % 116.97/16.17 | all_70_0, simplifying with (16), (233), (302) gives: % 116.97/16.17 | (313) addition(all_124_0, all_20_8) = all_70_0 & $i(all_70_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (313) implies: % 116.97/16.17 | (314) addition(all_124_0, all_20_8) = all_70_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_10, % 116.97/16.17 | all_20_8, all_20_7, all_122_0, simplifying with (14), (16), (20), % 116.97/16.17 | (34), (229) gives: % 116.97/16.17 | (315) ? [v0: $i] : (addition(all_20_8, v0) = all_122_0 & % 116.97/16.17 | addition(all_20_10, all_20_1) = v0 & $i(v0) & $i(all_122_0)) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 116.97/16.17 | all_20_10, all_20_7, all_122_0, simplifying with (14), (16), % 116.97/16.17 | (20), (21), (229) gives: % 116.97/16.17 | (316) ? [v0: $i] : (addition(all_20_8, all_20_1) = v0 & % 116.97/16.17 | addition(all_20_10, v0) = all_122_0 & $i(v0) & $i(all_122_0)) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_7, all_20_1, % 116.97/16.17 | all_122_0, simplifying with (20), (33), (229) gives: % 116.97/16.17 | (317) addition(all_20_1, all_20_7) = all_122_0 & $i(all_122_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (317) implies: % 116.97/16.17 | (318) $i(all_122_0) % 116.97/16.17 | (319) addition(all_20_1, all_20_7) = all_122_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_6, all_20_1, % 116.97/16.17 | all_118_0, simplifying with (17), (20), (224) gives: % 116.97/16.17 | (320) addition(all_20_1, all_20_6) = all_118_0 & $i(all_118_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (320) implies: % 116.97/16.17 | (321) $i(all_118_0) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_6, all_110_0, % 116.97/16.17 | all_56_0, simplifying with (17), (295), (311) gives: % 116.97/16.17 | (322) addition(all_110_0, all_20_6) = all_56_0 & $i(all_56_0) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_6, all_142_0, % 116.97/16.17 | all_20_0, simplifying with (17), (254), (255) gives: % 116.97/16.17 | (323) addition(all_142_0, all_20_6) = all_20_0 & $i(all_20_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (323) implies: % 116.97/16.17 | (324) addition(all_142_0, all_20_6) = all_20_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (3) with all_20_4, all_20_12, all_52_0, simplifying % 116.97/16.17 | with (12), (18), (44), (132) gives: % 116.97/16.17 | (325) all_52_0 = one % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_commutativity) with all_20_3, all_118_0, % 116.97/16.17 | all_46_0, simplifying with (19), (294), (321) gives: % 116.97/16.17 | (326) addition(all_118_0, all_20_3) = all_46_0 & $i(all_46_0) % 116.97/16.17 | % 116.97/16.17 | ALPHA: (326) implies: % 116.97/16.17 | (327) addition(all_118_0, all_20_3) = all_46_0 % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_20_3, % 116.97/16.17 | all_20_6, all_34_0, all_48_0, simplifying with (14), (17), (19), % 116.97/16.17 | (51), (138) gives: % 116.97/16.17 | (328) ? [v0: $i] : (addition(all_20_3, all_20_10) = v0 & % 116.97/16.17 | addition(all_20_6, v0) = all_48_0 & $i(v0) & $i(all_48_0)) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_20_8, all_20_3, % 116.97/16.17 | all_20_6, all_34_0, all_56_0, simplifying with (16), (17), (19), % 116.97/16.17 | (51), (147) gives: % 116.97/16.17 | (329) ? [v0: $i] : (addition(all_20_3, all_20_8) = v0 & addition(all_20_6, % 116.97/16.17 | v0) = all_56_0 & $i(v0) & $i(all_56_0)) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_122_0, all_20_3, % 116.97/16.17 | all_20_6, all_34_0, all_20_0, simplifying with (17), (19), (51), % 116.97/16.17 | (230), (318) gives: % 116.97/16.17 | (330) ? [v0: $i] : (addition(all_20_3, all_122_0) = v0 & % 116.97/16.17 | addition(all_20_6, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.97/16.17 | % 116.97/16.17 | GROUND_INST: instantiating (additive_associativity) with all_20_7, all_20_1, % 116.97/16.17 | all_20_3, all_36_0, all_68_0, simplifying with (19), (20), (33), % 116.97/16.17 | (55), (162) gives: % 116.97/16.18 | (331) ? [v0: $i] : (addition(all_20_1, all_20_7) = v0 & addition(all_20_3, % 116.97/16.18 | v0) = all_68_0 & $i(v0) & $i(all_68_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 116.97/16.18 | all_20_6, all_38_0, all_144_0, simplifying with (16), (17), (20), % 116.97/16.18 | (68), (258) gives: % 116.97/16.18 | (332) ? [v0: $i] : (addition(all_20_6, v0) = all_144_0 & % 116.97/16.18 | addition(all_20_8, all_20_1) = v0 & $i(v0) & $i(all_144_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_6, % 116.97/16.18 | all_20_8, all_38_0, all_144_0, simplifying with (16), (17), (20), % 116.97/16.18 | (59), (258) gives: % 116.97/16.18 | (333) ? [v0: $i] : (addition(all_20_6, all_20_1) = v0 & addition(all_20_8, % 116.97/16.18 | v0) = all_144_0 & $i(v0) & $i(all_144_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_124_0, % 116.97/16.18 | all_38_0, all_20_2, all_20_0, simplifying with (20), (24), (57), % 116.97/16.18 | (281), (302) gives: % 116.97/16.18 | (334) ? [v0: $i] : (addition(all_124_0, all_20_1) = v0 & % 116.97/16.18 | addition(all_38_0, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_124_0, all_20_6, % 116.97/16.18 | all_20_8, all_38_0, all_20_2, simplifying with (16), (17), (59), % 116.97/16.18 | (281), (302) gives: % 116.97/16.18 | (335) ? [v0: $i] : (addition(all_20_6, all_124_0) = v0 & % 116.97/16.18 | addition(all_20_8, v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_148_0, all_20_8, % 116.97/16.18 | all_20_6, all_38_0, all_50_0, simplifying with (16), (17), (68), % 116.97/16.18 | (264), (305) gives: % 116.97/16.18 | (336) ? [v0: $i] : (addition(all_20_6, v0) = all_50_0 & addition(all_20_8, % 116.97/16.18 | all_148_0) = v0 & $i(v0) & $i(all_50_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 116.97/16.18 | all_48_0, all_20_2, all_20_0, simplifying with (16), (20), (24), % 116.97/16.18 | (137), (150) gives: % 116.97/16.18 | (337) ? [v0: $i] : (addition(all_48_0, v0) = all_20_0 & addition(all_20_8, % 116.97/16.18 | all_20_1) = v0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_34_0, % 116.97/16.18 | all_20_10, all_48_0, all_106_0, simplifying with (14), (20), % 116.97/16.18 | (49), (90), (210) gives: % 116.97/16.18 | (338) ? [v0: $i] : (addition(all_34_0, all_20_1) = v0 & % 116.97/16.18 | addition(all_20_10, v0) = all_106_0 & $i(v0) & $i(all_106_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_10, % 116.97/16.18 | all_34_0, all_48_0, all_106_0, simplifying with (14), (20), (49), % 116.97/16.18 | (138), (210) gives: % 116.97/16.18 | (339) ? [v0: $i] : (addition(all_34_0, v0) = all_106_0 & % 116.97/16.18 | addition(all_20_10, all_20_1) = v0 & $i(v0) & $i(all_106_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_118_0, % 116.97/16.18 | all_20_7, all_50_0, all_20_0, simplifying with (19), (33), (178), % 116.97/16.18 | (223), (321) gives: % 116.97/16.18 | (340) ? [v0: $i] : (addition(all_118_0, all_20_3) = v0 & % 116.97/16.18 | addition(all_20_7, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_10, % 116.97/16.18 | all_56_0, all_20_2, all_20_0, simplifying with (14), (20), (24), % 116.97/16.18 | (101), (291) gives: % 116.97/16.18 | (341) ? [v0: $i] : (addition(all_56_0, v0) = all_20_0 & % 116.97/16.18 | addition(all_20_10, all_20_1) = v0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_20_3, % 116.97/16.18 | all_38_0, all_56_0, all_20_2, simplifying with (14), (19), (57), % 116.97/16.18 | (291), (292) gives: % 116.97/16.18 | (342) ? [v0: $i] : (addition(all_38_0, v0) = all_20_2 & addition(all_20_3, % 116.97/16.18 | all_20_10) = v0 & $i(v0) & $i(all_20_2)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_34_0, % 116.97/16.18 | all_20_8, all_56_0, all_88_0, simplifying with (16), (20), (49), % 116.97/16.18 | (103), (290) gives: % 116.97/16.18 | (343) ? [v0: $i] : (addition(all_34_0, all_20_1) = v0 & addition(all_20_8, % 116.97/16.18 | v0) = all_88_0 & $i(v0) & $i(all_88_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 116.97/16.18 | all_38_0, all_56_0, all_88_0, simplifying with (19), (20), (57), % 116.97/16.18 | (290), (292) gives: % 116.97/16.18 | (344) ? [v0: $i] : (addition(all_38_0, v0) = all_88_0 & addition(all_20_3, % 116.97/16.18 | all_20_1) = v0 & $i(v0) & $i(all_88_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 116.97/16.18 | all_34_0, all_56_0, all_88_0, simplifying with (16), (20), (49), % 116.97/16.18 | (147), (290) gives: % 116.97/16.18 | (345) ? [v0: $i] : (addition(all_34_0, v0) = all_88_0 & addition(all_20_8, % 116.97/16.18 | all_20_1) = v0 & $i(v0) & $i(all_88_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_110_0, % 116.97/16.18 | all_20_6, all_56_0, all_88_0, simplifying with (17), (20), (290), % 116.97/16.18 | (295), (311) gives: % 116.97/16.18 | (346) ? [v0: $i] : (addition(all_110_0, all_20_1) = v0 & % 116.97/16.18 | addition(all_20_6, v0) = all_88_0 & $i(v0) & $i(all_88_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_36_0, % 116.97/16.18 | all_38_0, all_60_0, all_20_0, simplifying with (14), (53), (57), % 116.97/16.18 | (111), (141) gives: % 116.97/16.18 | (347) ? [v0: $i] : (addition(all_38_0, v0) = all_20_0 & addition(all_36_0, % 116.97/16.18 | all_20_10) = v0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_46_0, % 116.97/16.18 | all_20_8, all_60_0, all_20_0, simplifying with (14), (16), (86), % 116.97/16.18 | (141), (286) gives: % 116.97/16.18 | (348) ? [v0: $i] : (addition(all_46_0, all_20_10) = v0 & % 116.97/16.18 | addition(all_20_8, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 116.97/16.18 | all_62_0, all_20_5, all_50_0, simplifying with (16), (20), (93), % 116.97/16.18 | (134), (154) gives: % 116.97/16.18 | (349) ? [v0: $i] : (addition(all_62_0, v0) = all_50_0 & addition(all_20_8, % 116.97/16.18 | all_20_1) = v0 & $i(v0) & $i(all_50_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_8, % 116.97/16.18 | all_62_0, all_20_5, all_20_2, simplifying with (16), (19), (23), % 116.97/16.18 | (134), (154) gives: % 116.97/16.18 | (350) ? [v0: $i] : (addition(all_62_0, v0) = all_20_2 & addition(all_20_8, % 116.97/16.18 | all_20_3) = v0 & $i(v0) & $i(all_20_2)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_6, % 116.97/16.18 | all_20_10, all_62_0, all_100_0, simplifying with (14), (17), % 116.97/16.18 | (19), (113), (205) gives: % 116.97/16.18 | (351) ? [v0: $i] : (addition(all_20_6, all_20_3) = v0 & % 116.97/16.18 | addition(all_20_10, v0) = all_100_0 & $i(v0) & $i(all_100_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_3, all_20_10, % 116.97/16.18 | all_20_6, all_62_0, all_100_0, simplifying with (14), (17), (19), % 116.97/16.18 | (135), (205) gives: % 116.97/16.18 | (352) ? [v0: $i] : (addition(all_20_6, v0) = all_100_0 & % 116.97/16.18 | addition(all_20_10, all_20_3) = v0 & $i(v0) & $i(all_100_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_6, % 116.97/16.18 | all_20_10, all_62_0, all_140_0, simplifying with (14), (17), % 116.97/16.18 | (20), (113), (252) gives: % 116.97/16.18 | (353) ? [v0: $i] : (addition(all_20_6, all_20_1) = v0 & % 116.97/16.18 | addition(all_20_10, v0) = all_140_0 & $i(v0) & $i(all_140_0)) % 116.97/16.18 | % 116.97/16.18 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_10, % 116.97/16.18 | all_20_6, all_62_0, all_140_0, simplifying with (14), (17), (20), % 116.97/16.18 | (135), (252) gives: % 116.97/16.18 | (354) ? [v0: $i] : (addition(all_20_6, v0) = all_140_0 & % 116.97/16.18 | addition(all_20_10, all_20_1) = v0 & $i(v0) & $i(all_140_0)) % 116.97/16.18 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_36_0, all_20_6, % 116.97/16.19 | all_20_10, all_62_0, all_86_0, simplifying with (14), (17), (53), % 116.97/16.19 | (113), (191) gives: % 116.97/16.19 | (355) ? [v0: $i] : (addition(all_20_6, all_36_0) = v0 & % 116.97/16.19 | addition(all_20_10, v0) = all_86_0 & $i(v0) & $i(all_86_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_6, % 116.97/16.19 | all_70_0, all_20_2, all_20_0, simplifying with (17), (20), (24), % 116.97/16.19 | (158), (169) gives: % 116.97/16.19 | (356) ? [v0: $i] : (addition(all_70_0, v0) = all_20_0 & addition(all_20_6, % 116.97/16.19 | all_20_1) = v0 & $i(v0) & $i(all_20_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_124_0, % 116.97/16.19 | all_20_8, all_70_0, all_20_2, simplifying with (16), (17), (169), % 116.97/16.19 | (233), (302) gives: % 116.97/16.19 | (357) ? [v0: $i] : (addition(all_124_0, all_20_6) = v0 & % 116.97/16.19 | addition(all_20_8, v0) = all_20_2 & $i(v0) & $i(all_20_2)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 116.97/16.19 | all_20_7, all_70_0, all_142_0, simplifying with (19), (20), (33), % 116.97/16.19 | (125), (256) gives: % 116.97/16.19 | (358) ? [v0: $i] : (addition(all_20_3, all_20_1) = v0 & addition(all_20_7, % 116.97/16.19 | v0) = all_142_0 & $i(v0) & $i(all_142_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_7, % 116.97/16.19 | all_20_3, all_70_0, all_142_0, simplifying with (19), (20), (33), % 116.97/16.19 | (159), (256) gives: % 116.97/16.19 | (359) ? [v0: $i] : (addition(all_20_3, v0) = all_142_0 & % 116.97/16.19 | addition(all_20_7, all_20_1) = v0 & $i(v0) & $i(all_142_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_124_0, % 116.97/16.19 | all_20_8, all_70_0, all_142_0, simplifying with (16), (20), % 116.97/16.19 | (233), (256), (302) gives: % 116.97/16.19 | (360) ? [v0: $i] : (addition(all_124_0, all_20_1) = v0 & % 116.97/16.19 | addition(all_20_8, v0) = all_142_0 & $i(v0) & $i(all_142_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_110_0, % 116.97/16.19 | all_20_10, all_70_0, all_142_0, simplifying with (14), (20), % 116.97/16.19 | (214), (256), (311) gives: % 116.97/16.19 | (361) ? [v0: $i] : (addition(all_110_0, all_20_1) = v0 & % 116.97/16.19 | addition(all_20_10, v0) = all_142_0 & $i(v0) & $i(all_142_0)) % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (2) with all_20_12, all_20_7, simplifying with % 116.97/16.19 | (12), (265) gives: % 116.97/16.19 | (362) all_20_7 = all_20_12 % 116.97/16.19 | % 116.97/16.19 | GROUND_INST: instantiating (1) with all_20_4, all_36_0, simplifying with (18), % 116.97/16.19 | (266) gives: % 116.97/16.19 | (363) all_36_0 = all_20_4 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (346) with fresh symbol all_170_0 gives: % 116.97/16.19 | (364) addition(all_110_0, all_20_1) = all_170_0 & addition(all_20_6, % 116.97/16.19 | all_170_0) = all_88_0 & $i(all_170_0) & $i(all_88_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (364) implies: % 116.97/16.19 | (365) addition(all_110_0, all_20_1) = all_170_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (335) with fresh symbol all_178_0 gives: % 116.97/16.19 | (366) addition(all_20_6, all_124_0) = all_178_0 & addition(all_20_8, % 116.97/16.19 | all_178_0) = all_20_2 & $i(all_178_0) & $i(all_20_2) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (366) implies: % 116.97/16.19 | (367) addition(all_20_6, all_124_0) = all_178_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (358) with fresh symbol all_180_0 gives: % 116.97/16.19 | (368) addition(all_20_3, all_20_1) = all_180_0 & addition(all_20_7, % 116.97/16.19 | all_180_0) = all_142_0 & $i(all_180_0) & $i(all_142_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (368) implies: % 116.97/16.19 | (369) $i(all_180_0) % 116.97/16.19 | (370) addition(all_20_3, all_20_1) = all_180_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (357) with fresh symbol all_182_0 gives: % 116.97/16.19 | (371) addition(all_124_0, all_20_6) = all_182_0 & addition(all_20_8, % 116.97/16.19 | all_182_0) = all_20_2 & $i(all_182_0) & $i(all_20_2) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (371) implies: % 116.97/16.19 | (372) addition(all_124_0, all_20_6) = all_182_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (349) with fresh symbol all_184_0 gives: % 116.97/16.19 | (373) addition(all_62_0, all_184_0) = all_50_0 & addition(all_20_8, % 116.97/16.19 | all_20_1) = all_184_0 & $i(all_184_0) & $i(all_50_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (373) implies: % 116.97/16.19 | (374) addition(all_20_8, all_20_1) = all_184_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (356) with fresh symbol all_188_0 gives: % 116.97/16.19 | (375) addition(all_70_0, all_188_0) = all_20_0 & addition(all_20_6, % 116.97/16.19 | all_20_1) = all_188_0 & $i(all_188_0) & $i(all_20_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (375) implies: % 116.97/16.19 | (376) $i(all_188_0) % 116.97/16.19 | (377) addition(all_20_6, all_20_1) = all_188_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (360) with fresh symbol all_190_0 gives: % 116.97/16.19 | (378) addition(all_124_0, all_20_1) = all_190_0 & addition(all_20_8, % 116.97/16.19 | all_190_0) = all_142_0 & $i(all_190_0) & $i(all_142_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (378) implies: % 116.97/16.19 | (379) addition(all_124_0, all_20_1) = all_190_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (359) with fresh symbol all_192_0 gives: % 116.97/16.19 | (380) addition(all_20_3, all_192_0) = all_142_0 & addition(all_20_7, % 116.97/16.19 | all_20_1) = all_192_0 & $i(all_192_0) & $i(all_142_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (380) implies: % 116.97/16.19 | (381) addition(all_20_7, all_20_1) = all_192_0 % 116.97/16.19 | (382) addition(all_20_3, all_192_0) = all_142_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (328) with fresh symbol all_196_0 gives: % 116.97/16.19 | (383) addition(all_20_3, all_20_10) = all_196_0 & addition(all_20_6, % 116.97/16.19 | all_196_0) = all_48_0 & $i(all_196_0) & $i(all_48_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (383) implies: % 116.97/16.19 | (384) $i(all_196_0) % 116.97/16.19 | (385) addition(all_20_6, all_196_0) = all_48_0 % 116.97/16.19 | (386) addition(all_20_3, all_20_10) = all_196_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (334) with fresh symbol all_200_0 gives: % 116.97/16.19 | (387) addition(all_124_0, all_20_1) = all_200_0 & addition(all_38_0, % 116.97/16.19 | all_200_0) = all_20_0 & $i(all_200_0) & $i(all_20_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (387) implies: % 116.97/16.19 | (388) addition(all_124_0, all_20_1) = all_200_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (331) with fresh symbol all_208_0 gives: % 116.97/16.19 | (389) addition(all_20_1, all_20_7) = all_208_0 & addition(all_20_3, % 116.97/16.19 | all_208_0) = all_68_0 & $i(all_208_0) & $i(all_68_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (389) implies: % 116.97/16.19 | (390) addition(all_20_3, all_208_0) = all_68_0 % 116.97/16.19 | (391) addition(all_20_1, all_20_7) = all_208_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (347) with fresh symbol all_210_0 gives: % 116.97/16.19 | (392) addition(all_38_0, all_210_0) = all_20_0 & addition(all_36_0, % 116.97/16.19 | all_20_10) = all_210_0 & $i(all_210_0) & $i(all_20_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (392) implies: % 116.97/16.19 | (393) addition(all_36_0, all_20_10) = all_210_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (348) with fresh symbol all_212_0 gives: % 116.97/16.19 | (394) addition(all_46_0, all_20_10) = all_212_0 & addition(all_20_8, % 116.97/16.19 | all_212_0) = all_20_0 & $i(all_212_0) & $i(all_20_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (394) implies: % 116.97/16.19 | (395) addition(all_46_0, all_20_10) = all_212_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (339) with fresh symbol all_222_0 gives: % 116.97/16.19 | (396) addition(all_34_0, all_222_0) = all_106_0 & addition(all_20_10, % 116.97/16.19 | all_20_1) = all_222_0 & $i(all_222_0) & $i(all_106_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (396) implies: % 116.97/16.19 | (397) $i(all_222_0) % 116.97/16.19 | (398) addition(all_20_10, all_20_1) = all_222_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (338) with fresh symbol all_224_0 gives: % 116.97/16.19 | (399) addition(all_34_0, all_20_1) = all_224_0 & addition(all_20_10, % 116.97/16.19 | all_224_0) = all_106_0 & $i(all_224_0) & $i(all_106_0) % 116.97/16.19 | % 116.97/16.19 | ALPHA: (399) implies: % 116.97/16.19 | (400) addition(all_20_10, all_224_0) = all_106_0 % 116.97/16.19 | (401) addition(all_34_0, all_20_1) = all_224_0 % 116.97/16.19 | % 116.97/16.19 | DELTA: instantiating (316) with fresh symbol all_226_0 gives: % 116.97/16.20 | (402) addition(all_20_8, all_20_1) = all_226_0 & addition(all_20_10, % 116.97/16.20 | all_226_0) = all_122_0 & $i(all_226_0) & $i(all_122_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (402) implies: % 116.97/16.20 | (403) addition(all_20_8, all_20_1) = all_226_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (315) with fresh symbol all_228_0 gives: % 116.97/16.20 | (404) addition(all_20_8, all_228_0) = all_122_0 & addition(all_20_10, % 116.97/16.20 | all_20_1) = all_228_0 & $i(all_228_0) & $i(all_122_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (404) implies: % 116.97/16.20 | (405) addition(all_20_10, all_20_1) = all_228_0 % 116.97/16.20 | (406) addition(all_20_8, all_228_0) = all_122_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (345) with fresh symbol all_230_0 gives: % 116.97/16.20 | (407) addition(all_34_0, all_230_0) = all_88_0 & addition(all_20_8, % 116.97/16.20 | all_20_1) = all_230_0 & $i(all_230_0) & $i(all_88_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (407) implies: % 116.97/16.20 | (408) addition(all_20_8, all_20_1) = all_230_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (343) with fresh symbol all_232_0 gives: % 116.97/16.20 | (409) addition(all_34_0, all_20_1) = all_232_0 & addition(all_20_8, % 116.97/16.20 | all_232_0) = all_88_0 & $i(all_232_0) & $i(all_88_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (409) implies: % 116.97/16.20 | (410) addition(all_34_0, all_20_1) = all_232_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (351) with fresh symbol all_236_0 gives: % 116.97/16.20 | (411) addition(all_20_6, all_20_3) = all_236_0 & addition(all_20_10, % 116.97/16.20 | all_236_0) = all_100_0 & $i(all_236_0) & $i(all_100_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (411) implies: % 116.97/16.20 | (412) addition(all_20_6, all_20_3) = all_236_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (361) with fresh symbol all_238_0 gives: % 116.97/16.20 | (413) addition(all_110_0, all_20_1) = all_238_0 & addition(all_20_10, % 116.97/16.20 | all_238_0) = all_142_0 & $i(all_238_0) & $i(all_142_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (413) implies: % 116.97/16.20 | (414) addition(all_110_0, all_20_1) = all_238_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (344) with fresh symbol all_240_0 gives: % 116.97/16.20 | (415) addition(all_38_0, all_240_0) = all_88_0 & addition(all_20_3, % 116.97/16.20 | all_20_1) = all_240_0 & $i(all_240_0) & $i(all_88_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (415) implies: % 116.97/16.20 | (416) addition(all_20_3, all_20_1) = all_240_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (350) with fresh symbol all_242_0 gives: % 116.97/16.20 | (417) addition(all_62_0, all_242_0) = all_20_2 & addition(all_20_8, % 116.97/16.20 | all_20_3) = all_242_0 & $i(all_242_0) & $i(all_20_2) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (417) implies: % 116.97/16.20 | (418) addition(all_20_8, all_20_3) = all_242_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (333) with fresh symbol all_246_0 gives: % 116.97/16.20 | (419) addition(all_20_6, all_20_1) = all_246_0 & addition(all_20_8, % 116.97/16.20 | all_246_0) = all_144_0 & $i(all_246_0) & $i(all_144_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (419) implies: % 116.97/16.20 | (420) addition(all_20_6, all_20_1) = all_246_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (330) with fresh symbol all_248_0 gives: % 116.97/16.20 | (421) addition(all_20_3, all_122_0) = all_248_0 & addition(all_20_6, % 116.97/16.20 | all_248_0) = all_20_0 & $i(all_248_0) & $i(all_20_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (421) implies: % 116.97/16.20 | (422) addition(all_20_3, all_122_0) = all_248_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (329) with fresh symbol all_250_0 gives: % 116.97/16.20 | (423) addition(all_20_3, all_20_8) = all_250_0 & addition(all_20_6, % 116.97/16.20 | all_250_0) = all_56_0 & $i(all_250_0) & $i(all_56_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (423) implies: % 116.97/16.20 | (424) addition(all_20_3, all_20_8) = all_250_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (342) with fresh symbol all_252_0 gives: % 116.97/16.20 | (425) addition(all_38_0, all_252_0) = all_20_2 & addition(all_20_3, % 116.97/16.20 | all_20_10) = all_252_0 & $i(all_252_0) & $i(all_20_2) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (425) implies: % 116.97/16.20 | (426) addition(all_20_3, all_20_10) = all_252_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (332) with fresh symbol all_256_0 gives: % 116.97/16.20 | (427) addition(all_20_6, all_256_0) = all_144_0 & addition(all_20_8, % 116.97/16.20 | all_20_1) = all_256_0 & $i(all_256_0) & $i(all_144_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (427) implies: % 116.97/16.20 | (428) addition(all_20_8, all_20_1) = all_256_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (341) with fresh symbol all_260_0 gives: % 116.97/16.20 | (429) addition(all_56_0, all_260_0) = all_20_0 & addition(all_20_10, % 116.97/16.20 | all_20_1) = all_260_0 & $i(all_260_0) & $i(all_20_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (429) implies: % 116.97/16.20 | (430) addition(all_20_10, all_20_1) = all_260_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (340) with fresh symbol all_264_0 gives: % 116.97/16.20 | (431) addition(all_118_0, all_20_3) = all_264_0 & addition(all_20_7, % 116.97/16.20 | all_264_0) = all_20_0 & $i(all_264_0) & $i(all_20_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (431) implies: % 116.97/16.20 | (432) addition(all_118_0, all_20_3) = all_264_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (355) with fresh symbol all_268_0 gives: % 116.97/16.20 | (433) addition(all_20_6, all_36_0) = all_268_0 & addition(all_20_10, % 116.97/16.20 | all_268_0) = all_86_0 & $i(all_268_0) & $i(all_86_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (433) implies: % 116.97/16.20 | (434) addition(all_20_10, all_268_0) = all_86_0 % 116.97/16.20 | (435) addition(all_20_6, all_36_0) = all_268_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (336) with fresh symbol all_272_0 gives: % 116.97/16.20 | (436) addition(all_20_6, all_272_0) = all_50_0 & addition(all_20_8, % 116.97/16.20 | all_148_0) = all_272_0 & $i(all_272_0) & $i(all_50_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (436) implies: % 116.97/16.20 | (437) addition(all_20_8, all_148_0) = all_272_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (352) with fresh symbol all_274_0 gives: % 116.97/16.20 | (438) addition(all_20_6, all_274_0) = all_100_0 & addition(all_20_10, % 116.97/16.20 | all_20_3) = all_274_0 & $i(all_274_0) & $i(all_100_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (438) implies: % 116.97/16.20 | (439) addition(all_20_10, all_20_3) = all_274_0 % 116.97/16.20 | (440) addition(all_20_6, all_274_0) = all_100_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (337) with fresh symbol all_276_0 gives: % 116.97/16.20 | (441) addition(all_48_0, all_276_0) = all_20_0 & addition(all_20_8, % 116.97/16.20 | all_20_1) = all_276_0 & $i(all_276_0) & $i(all_20_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (441) implies: % 116.97/16.20 | (442) addition(all_20_8, all_20_1) = all_276_0 % 116.97/16.20 | (443) addition(all_48_0, all_276_0) = all_20_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (354) with fresh symbol all_282_0 gives: % 116.97/16.20 | (444) addition(all_20_6, all_282_0) = all_140_0 & addition(all_20_10, % 116.97/16.20 | all_20_1) = all_282_0 & $i(all_282_0) & $i(all_140_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (444) implies: % 116.97/16.20 | (445) addition(all_20_10, all_20_1) = all_282_0 % 116.97/16.20 | % 116.97/16.20 | DELTA: instantiating (353) with fresh symbol all_286_0 gives: % 116.97/16.20 | (446) addition(all_20_6, all_20_1) = all_286_0 & addition(all_20_10, % 116.97/16.20 | all_286_0) = all_140_0 & $i(all_286_0) & $i(all_140_0) % 116.97/16.20 | % 116.97/16.20 | ALPHA: (446) implies: % 116.97/16.20 | (447) addition(all_20_6, all_20_1) = all_286_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (280), (325) imply: % 116.97/16.20 | (448) multiplication(one, all_20_11) = all_34_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (266), (363) imply: % 116.97/16.20 | (449) multiplication(all_20_4, one) = all_20_4 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (265), (362) imply: % 116.97/16.20 | (450) multiplication(one, all_20_12) = all_20_12 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (162), (362), (363) imply: % 116.97/16.20 | (451) addition(all_20_4, all_20_12) = all_68_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (363), (393) imply: % 116.97/16.20 | (452) addition(all_20_4, all_20_10) = all_210_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (307), (363) imply: % 116.97/16.20 | (453) addition(all_20_4, all_20_10) = all_94_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (84), (363) imply: % 116.97/16.20 | (454) addition(all_20_1, all_20_3) = all_20_4 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (362), (391) imply: % 116.97/16.20 | (455) addition(all_20_1, all_20_12) = all_208_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (319), (362) imply: % 116.97/16.20 | (456) addition(all_20_1, all_20_12) = all_122_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (55), (363) imply: % 116.97/16.20 | (457) addition(all_20_3, all_20_1) = all_20_4 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (132), (325) imply: % 116.97/16.20 | (458) addition(all_20_4, all_20_12) = one % 116.97/16.20 | % 116.97/16.20 | REDUCE: (363), (435) imply: % 116.97/16.20 | (459) addition(all_20_6, all_20_4) = all_268_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (88), (363) imply: % 116.97/16.20 | (460) addition(all_20_6, all_20_4) = all_46_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (362), (381) imply: % 116.97/16.20 | (461) addition(all_20_12, all_20_1) = all_192_0 % 116.97/16.20 | % 116.97/16.20 | REDUCE: (229), (362) imply: % 116.97/16.20 | (462) addition(all_20_12, all_20_1) = all_122_0 % 116.97/16.20 | % 116.97/16.20 | GROUND_INST: instantiating (6) with all_122_0, all_192_0, all_20_1, all_20_12, % 116.97/16.20 | simplifying with (461), (462) gives: % 116.97/16.20 | (463) all_192_0 = all_122_0 % 116.97/16.20 | % 116.97/16.20 | GROUND_INST: instantiating (6) with all_124_0, all_274_0, all_20_3, all_20_10, % 116.97/16.20 | simplifying with (232), (439) gives: % 116.97/16.20 | (464) all_274_0 = all_124_0 % 116.97/16.20 | % 116.97/16.20 | GROUND_INST: instantiating (6) with all_148_0, all_228_0, all_20_1, all_20_10, % 116.97/16.20 | simplifying with (263), (405) gives: % 116.97/16.20 | (465) all_228_0 = all_148_0 % 116.97/16.20 | % 116.97/16.20 | GROUND_INST: instantiating (6) with all_228_0, all_260_0, all_20_1, all_20_10, % 116.97/16.20 | simplifying with (405), (430) gives: % 116.97/16.21 | (466) all_260_0 = all_228_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_260_0, all_282_0, all_20_1, all_20_10, % 116.97/16.21 | simplifying with (430), (445) gives: % 116.97/16.21 | (467) all_282_0 = all_260_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_222_0, all_282_0, all_20_1, all_20_10, % 116.97/16.21 | simplifying with (398), (445) gives: % 116.97/16.21 | (468) all_282_0 = all_222_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_110_0, all_242_0, all_20_3, all_20_8, % 116.97/16.21 | simplifying with (215), (418) gives: % 116.97/16.21 | (469) all_242_0 = all_110_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_230_0, all_256_0, all_20_1, all_20_8, % 116.97/16.21 | simplifying with (408), (428) gives: % 116.97/16.21 | (470) all_256_0 = all_230_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_184_0, all_256_0, all_20_1, all_20_8, % 116.97/16.21 | simplifying with (374), (428) gives: % 116.97/16.21 | (471) all_256_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_230_0, all_276_0, all_20_1, all_20_8, % 116.97/16.21 | simplifying with (408), (442) gives: % 116.97/16.21 | (472) all_276_0 = all_230_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_226_0, all_276_0, all_20_1, all_20_8, % 116.97/16.21 | simplifying with (403), (442) gives: % 116.97/16.21 | (473) all_276_0 = all_226_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_46_0, all_268_0, all_20_4, all_20_6, % 116.97/16.21 | simplifying with (459), (460) gives: % 116.97/16.21 | (474) all_268_0 = all_46_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_34_0, all_236_0, all_20_3, all_20_6, % 116.97/16.21 | simplifying with (51), (412) gives: % 116.97/16.21 | (475) all_236_0 = all_34_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_118_0, all_246_0, all_20_1, all_20_6, % 116.97/16.21 | simplifying with (224), (420) gives: % 116.97/16.21 | (476) all_246_0 = all_118_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_246_0, all_286_0, all_20_1, all_20_6, % 116.97/16.21 | simplifying with (420), (447) gives: % 116.97/16.21 | (477) all_286_0 = all_246_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_188_0, all_286_0, all_20_1, all_20_6, % 116.97/16.21 | simplifying with (377), (447) gives: % 116.97/16.21 | (478) all_286_0 = all_188_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with one, all_68_0, all_20_12, all_20_4, % 116.97/16.21 | simplifying with (451), (458) gives: % 116.97/16.21 | (479) all_68_0 = one % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_94_0, all_210_0, all_20_10, all_20_4, % 116.97/16.21 | simplifying with (452), (453) gives: % 116.97/16.21 | (480) all_210_0 = all_94_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_196_0, all_252_0, all_20_10, all_20_3, % 116.97/16.21 | simplifying with (386), (426) gives: % 116.97/16.21 | (481) all_252_0 = all_196_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_124_0, all_252_0, all_20_10, all_20_3, % 116.97/16.21 | simplifying with (303), (426) gives: % 116.97/16.21 | (482) all_252_0 = all_124_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_110_0, all_250_0, all_20_8, all_20_3, % 116.97/16.21 | simplifying with (312), (424) gives: % 116.97/16.21 | (483) all_250_0 = all_110_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_180_0, all_240_0, all_20_1, all_20_3, % 116.97/16.21 | simplifying with (370), (416) gives: % 116.97/16.21 | (484) all_240_0 = all_180_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_20_4, all_240_0, all_20_1, all_20_3, % 116.97/16.21 | simplifying with (416), (457) gives: % 116.97/16.21 | (485) all_240_0 = all_20_4 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_122_0, all_208_0, all_20_12, all_20_1, % 116.97/16.21 | simplifying with (455), (456) gives: % 116.97/16.21 | (486) all_208_0 = all_122_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_46_0, all_232_0, all_20_1, all_34_0, % 116.97/16.21 | simplifying with (293), (410) gives: % 116.97/16.21 | (487) all_232_0 = all_46_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_224_0, all_232_0, all_20_1, all_34_0, % 116.97/16.21 | simplifying with (401), (410) gives: % 116.97/16.21 | (488) all_232_0 = all_224_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_90_0, all_212_0, all_20_10, all_46_0, % 116.97/16.21 | simplifying with (309), (395) gives: % 116.97/16.21 | (489) all_212_0 = all_90_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_170_0, all_238_0, all_20_1, all_110_0, % 116.97/16.21 | simplifying with (365), (414) gives: % 116.97/16.21 | (490) all_238_0 = all_170_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_46_0, all_264_0, all_20_3, all_118_0, % 116.97/16.21 | simplifying with (327), (432) gives: % 116.97/16.21 | (491) all_264_0 = all_46_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_190_0, all_200_0, all_20_1, all_124_0, % 116.97/16.21 | simplifying with (379), (388) gives: % 116.97/16.21 | (492) all_200_0 = all_190_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (477), (478) imply: % 116.97/16.21 | (493) all_246_0 = all_188_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (493) implies: % 116.97/16.21 | (494) all_246_0 = all_188_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (467), (468) imply: % 116.97/16.21 | (495) all_260_0 = all_222_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (495) implies: % 116.97/16.21 | (496) all_260_0 = all_222_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (472), (473) imply: % 116.97/16.21 | (497) all_230_0 = all_226_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (497) implies: % 116.97/16.21 | (498) all_230_0 = all_226_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (466), (496) imply: % 116.97/16.21 | (499) all_228_0 = all_222_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (499) implies: % 116.97/16.21 | (500) all_228_0 = all_222_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (470), (471) imply: % 116.97/16.21 | (501) all_230_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (501) implies: % 116.97/16.21 | (502) all_230_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (481), (482) imply: % 116.97/16.21 | (503) all_196_0 = all_124_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (503) implies: % 116.97/16.21 | (504) all_196_0 = all_124_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (476), (494) imply: % 116.97/16.21 | (505) all_188_0 = all_118_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (484), (485) imply: % 116.97/16.21 | (506) all_180_0 = all_20_4 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (487), (488) imply: % 116.97/16.21 | (507) all_224_0 = all_46_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (507) implies: % 116.97/16.21 | (508) all_224_0 = all_46_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (498), (502) imply: % 116.97/16.21 | (509) all_226_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (509) implies: % 116.97/16.21 | (510) all_226_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (465), (500) imply: % 116.97/16.21 | (511) all_222_0 = all_148_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (473), (510) imply: % 116.97/16.21 | (512) all_276_0 = all_184_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (443), (512) imply: % 116.97/16.21 | (513) addition(all_48_0, all_184_0) = all_20_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (390), (479), (486) imply: % 116.97/16.21 | (514) addition(all_20_3, all_122_0) = one % 116.97/16.21 | % 116.97/16.21 | REDUCE: (382), (463) imply: % 116.97/16.21 | (515) addition(all_20_3, all_122_0) = all_142_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (440), (464) imply: % 116.97/16.21 | (516) addition(all_20_6, all_124_0) = all_100_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (385), (504) imply: % 116.97/16.21 | (517) addition(all_20_6, all_124_0) = all_48_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (406), (465) imply: % 116.97/16.21 | (518) addition(all_20_8, all_148_0) = all_122_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (434), (474) imply: % 116.97/16.21 | (519) addition(all_20_10, all_46_0) = all_86_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (400), (508) imply: % 116.97/16.21 | (520) addition(all_20_10, all_46_0) = all_106_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_90_0, all_106_0, all_46_0, all_20_10, % 116.97/16.21 | simplifying with (297), (520) gives: % 116.97/16.21 | (521) all_106_0 = all_90_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_86_0, all_106_0, all_46_0, all_20_10, % 116.97/16.21 | simplifying with (519), (520) gives: % 116.97/16.21 | (522) all_106_0 = all_86_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_272_0, all_122_0, all_148_0, all_20_8, % 116.97/16.21 | simplifying with (437), (518) gives: % 116.97/16.21 | (523) all_272_0 = all_122_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_178_0, all_48_0, all_124_0, all_20_6, % 116.97/16.21 | simplifying with (367), (517) gives: % 116.97/16.21 | (524) all_178_0 = all_48_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_178_0, all_100_0, all_124_0, all_20_6, % 116.97/16.21 | simplifying with (367), (516) gives: % 116.97/16.21 | (525) all_178_0 = all_100_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_248_0, one, all_122_0, all_20_3, % 116.97/16.21 | simplifying with (422), (514) gives: % 116.97/16.21 | (526) all_248_0 = one % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (6) with all_248_0, all_142_0, all_122_0, all_20_3, % 116.97/16.21 | simplifying with (422), (515) gives: % 116.97/16.21 | (527) all_248_0 = all_142_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (526), (527) imply: % 116.97/16.21 | (528) all_142_0 = one % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (524), (525) imply: % 116.97/16.21 | (529) all_100_0 = all_48_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (529) implies: % 116.97/16.21 | (530) all_100_0 = all_48_0 % 116.97/16.21 | % 116.97/16.21 | COMBINE_EQS: (521), (522) imply: % 116.97/16.21 | (531) all_90_0 = all_86_0 % 116.97/16.21 | % 116.97/16.21 | SIMP: (531) implies: % 116.97/16.21 | (532) all_90_0 = all_86_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (324), (528) imply: % 116.97/16.21 | (533) addition(one, all_20_6) = all_20_0 % 116.97/16.21 | % 116.97/16.21 | REDUCE: (256), (528) imply: % 116.97/16.21 | (534) addition(all_70_0, all_20_1) = one % 116.97/16.21 | % 116.97/16.21 | REDUCE: (309), (532) imply: % 116.97/16.21 | (535) addition(all_46_0, all_20_10) = all_86_0 % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_11, % 116.97/16.21 | all_20_9, one, all_20_0, simplifying with (13), (15), (17), % 116.97/16.21 | (267), (533) gives: % 116.97/16.21 | (536) ? [v0: $i] : (addition(all_20_9, v0) = all_20_0 & % 116.97/16.21 | addition(all_20_11, all_20_6) = v0 & $i(v0) & $i(all_20_0)) % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_9, % 116.97/16.21 | all_20_11, one, all_20_0, simplifying with (13), (15), (17), % 116.97/16.21 | (268), (533) gives: % 116.97/16.21 | (537) ? [v0: $i] : (addition(all_20_9, all_20_6) = v0 & % 116.97/16.21 | addition(all_20_11, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 116.97/16.21 | % 116.97/16.21 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_20_1, % 116.97/16.21 | all_184_0, simplifying with (16), (20), (374) gives: % 116.97/16.22 | (538) addition(all_20_1, all_20_8) = all_184_0 & $i(all_184_0) % 116.97/16.22 | % 116.97/16.22 | ALPHA: (538) implies: % 116.97/16.22 | (539) $i(all_184_0) % 116.97/16.22 | % 116.97/16.22 | GROUND_INST: instantiating (additive_commutativity) with all_20_8, all_148_0, % 116.97/16.22 | all_122_0, simplifying with (16), (305), (518) gives: % 116.97/16.22 | (540) addition(all_148_0, all_20_8) = all_122_0 & $i(all_122_0) % 116.97/16.22 | % 116.97/16.22 | GROUND_INST: instantiating (additive_commutativity) with all_20_3, all_122_0, % 116.97/16.22 | one, simplifying with (19), (318), (514) gives: % 116.97/16.22 | (541) addition(all_122_0, all_20_3) = one & $i(one) % 116.97/16.22 | % 116.97/16.22 | ALPHA: (541) implies: % 116.97/16.22 | (542) $i(one) % 116.97/16.22 | % 116.97/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_20_3, % 116.97/16.22 | all_20_1, all_20_4, all_94_0, simplifying with (14), (19), (20), % 116.97/16.22 | (453), (454) gives: % 116.97/16.22 | (543) ? [v0: $i] : (addition(all_20_1, v0) = all_94_0 & addition(all_20_3, % 116.97/16.22 | all_20_10) = v0 & $i(v0) & $i(all_94_0)) % 116.97/16.22 | % 116.97/16.22 | GROUND_INST: instantiating (additive_associativity) with all_184_0, all_124_0, % 116.97/16.22 | all_20_6, all_48_0, all_20_0, simplifying with (17), (302), % 116.97/16.22 | (513), (517), (539) gives: % 117.22/16.22 | (544) ? [v0: $i] : (addition(all_124_0, all_184_0) = v0 & % 117.22/16.22 | addition(all_20_6, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 117.22/16.22 | all_20_8, all_110_0, all_170_0, simplifying with (16), (19), % 117.22/16.22 | (20), (215), (365) gives: % 117.22/16.22 | (545) ? [v0: $i] : (addition(all_20_3, all_20_1) = v0 & addition(all_20_8, % 117.22/16.22 | v0) = all_170_0 & $i(v0) & $i(all_170_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 117.22/16.22 | all_20_3, all_110_0, all_170_0, simplifying with (16), (19), % 117.22/16.22 | (20), (312), (365) gives: % 117.22/16.22 | (546) ? [v0: $i] : (addition(all_20_3, v0) = all_170_0 & % 117.22/16.22 | addition(all_20_8, all_20_1) = v0 & $i(v0) & $i(all_170_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_10, all_20_3, % 117.22/16.22 | all_118_0, all_46_0, all_86_0, simplifying with (14), (19), % 117.22/16.22 | (321), (327), (535) gives: % 117.22/16.22 | (547) ? [v0: $i] : (addition(all_118_0, v0) = all_86_0 & % 117.22/16.22 | addition(all_20_3, all_20_10) = v0 & $i(v0) & $i(all_86_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_8, % 117.22/16.22 | all_124_0, all_70_0, one, simplifying with (16), (20), (302), % 117.22/16.22 | (314), (534) gives: % 117.22/16.22 | (548) ? [v0: $i] : (addition(all_124_0, v0) = one & addition(all_20_8, % 117.22/16.22 | all_20_1) = v0 & $i(v0) & $i(one)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_3, % 117.22/16.22 | all_20_10, all_124_0, all_182_0, simplifying with (14), (17), % 117.22/16.22 | (19), (232), (372) gives: % 117.22/16.22 | (549) ? [v0: $i] : (addition(all_20_3, all_20_6) = v0 & % 117.22/16.22 | addition(all_20_10, v0) = all_182_0 & $i(v0) & $i(all_182_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (additive_associativity) with all_20_1, all_20_3, % 117.22/16.22 | all_20_10, all_124_0, all_190_0, simplifying with (14), (19), % 117.22/16.22 | (20), (232), (379) gives: % 117.22/16.22 | (550) ? [v0: $i] : (addition(all_20_3, all_20_1) = v0 & % 117.22/16.22 | addition(all_20_10, v0) = all_190_0 & $i(v0) & $i(all_190_0)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (multiplicative_associativity) with one, all_20_12, % 117.22/16.22 | all_20_11, all_20_12, all_20_6, simplifying with (12), (13), % 117.22/16.22 | (25), (450), (542) gives: % 117.22/16.22 | (551) ? [v0: $i] : (multiplication(all_20_12, all_20_11) = v0 & % 117.22/16.22 | multiplication(one, v0) = all_20_6 & $i(v0) & $i(all_20_6)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (2) with all_20_11, all_34_0, simplifying with % 117.22/16.22 | (13), (448) gives: % 117.22/16.22 | (552) all_34_0 = all_20_11 % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, one, % 117.22/16.22 | all_20_9, all_20_4, all_20_1, simplifying with (15), (18), (29), % 117.22/16.22 | (449), (542) gives: % 117.22/16.22 | (553) ? [v0: $i] : (multiplication(all_20_4, v0) = all_20_1 & % 117.22/16.22 | multiplication(one, all_20_9) = v0 & $i(v0) & $i(all_20_1)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, one, % 117.22/16.22 | all_20_11, all_20_4, all_20_3, simplifying with (13), (18), (28), % 117.22/16.22 | (449), (542) gives: % 117.22/16.22 | (554) ? [v0: $i] : (multiplication(all_20_4, v0) = all_20_3 & % 117.22/16.22 | multiplication(one, all_20_11) = v0 & $i(v0) & $i(all_20_3)) % 117.22/16.22 | % 117.22/16.22 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, one, % 117.22/16.22 | one, all_20_4, all_20_4, simplifying with (18), (449), (542) % 117.22/16.22 | gives: % 117.22/16.22 | (555) ? [v0: $i] : (multiplication(all_20_4, v0) = all_20_4 & % 117.22/16.22 | multiplication(one, one) = v0 & $i(v0)) % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (555) with fresh symbol all_310_0 gives: % 117.22/16.22 | (556) multiplication(all_20_4, all_310_0) = all_20_4 & multiplication(one, % 117.22/16.22 | one) = all_310_0 & $i(all_310_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (556) implies: % 117.22/16.22 | (557) $i(all_310_0) % 117.22/16.22 | (558) multiplication(one, one) = all_310_0 % 117.22/16.22 | (559) multiplication(all_20_4, all_310_0) = all_20_4 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (546) with fresh symbol all_312_0 gives: % 117.22/16.22 | (560) addition(all_20_3, all_312_0) = all_170_0 & addition(all_20_8, % 117.22/16.22 | all_20_1) = all_312_0 & $i(all_312_0) & $i(all_170_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (560) implies: % 117.22/16.22 | (561) $i(all_312_0) % 117.22/16.22 | (562) addition(all_20_8, all_20_1) = all_312_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (545) with fresh symbol all_314_0 gives: % 117.22/16.22 | (563) addition(all_20_3, all_20_1) = all_314_0 & addition(all_20_8, % 117.22/16.22 | all_314_0) = all_170_0 & $i(all_314_0) & $i(all_170_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (563) implies: % 117.22/16.22 | (564) $i(all_314_0) % 117.22/16.22 | (565) addition(all_20_3, all_20_1) = all_314_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (537) with fresh symbol all_318_0 gives: % 117.22/16.22 | (566) addition(all_20_9, all_20_6) = all_318_0 & addition(all_20_11, % 117.22/16.22 | all_318_0) = all_20_0 & $i(all_318_0) & $i(all_20_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (566) implies: % 117.22/16.22 | (567) addition(all_20_11, all_318_0) = all_20_0 % 117.22/16.22 | (568) addition(all_20_9, all_20_6) = all_318_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (536) with fresh symbol all_322_0 gives: % 117.22/16.22 | (569) addition(all_20_9, all_322_0) = all_20_0 & addition(all_20_11, % 117.22/16.22 | all_20_6) = all_322_0 & $i(all_322_0) & $i(all_20_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (569) implies: % 117.22/16.22 | (570) addition(all_20_11, all_20_6) = all_322_0 % 117.22/16.22 | (571) addition(all_20_9, all_322_0) = all_20_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (551) with fresh symbol all_350_0 gives: % 117.22/16.22 | (572) multiplication(all_20_12, all_20_11) = all_350_0 & % 117.22/16.22 | multiplication(one, all_350_0) = all_20_6 & $i(all_350_0) & % 117.22/16.22 | $i(all_20_6) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (572) implies: % 117.22/16.22 | (573) $i(all_350_0) % 117.22/16.22 | (574) multiplication(one, all_350_0) = all_20_6 % 117.22/16.22 | (575) multiplication(all_20_12, all_20_11) = all_350_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (547) with fresh symbol all_354_0 gives: % 117.22/16.22 | (576) addition(all_118_0, all_354_0) = all_86_0 & addition(all_20_3, % 117.22/16.22 | all_20_10) = all_354_0 & $i(all_354_0) & $i(all_86_0) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (576) implies: % 117.22/16.22 | (577) $i(all_354_0) % 117.22/16.22 | (578) addition(all_20_3, all_20_10) = all_354_0 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (554) with fresh symbol all_396_0 gives: % 117.22/16.22 | (579) multiplication(all_20_4, all_396_0) = all_20_3 & multiplication(one, % 117.22/16.22 | all_20_11) = all_396_0 & $i(all_396_0) & $i(all_20_3) % 117.22/16.22 | % 117.22/16.22 | ALPHA: (579) implies: % 117.22/16.22 | (580) $i(all_396_0) % 117.22/16.22 | (581) multiplication(one, all_20_11) = all_396_0 % 117.22/16.22 | (582) multiplication(all_20_4, all_396_0) = all_20_3 % 117.22/16.22 | % 117.22/16.22 | DELTA: instantiating (553) with fresh symbol all_398_0 gives: % 117.22/16.23 | (583) multiplication(all_20_4, all_398_0) = all_20_1 & multiplication(one, % 117.22/16.23 | all_20_9) = all_398_0 & $i(all_398_0) & $i(all_20_1) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (583) implies: % 117.22/16.23 | (584) $i(all_398_0) % 117.22/16.23 | (585) multiplication(one, all_20_9) = all_398_0 % 117.22/16.23 | (586) multiplication(all_20_4, all_398_0) = all_20_1 % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (549) with fresh symbol all_412_0 gives: % 117.22/16.23 | (587) addition(all_20_3, all_20_6) = all_412_0 & addition(all_20_10, % 117.22/16.23 | all_412_0) = all_182_0 & $i(all_412_0) & $i(all_182_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (587) implies: % 117.22/16.23 | (588) addition(all_20_3, all_20_6) = all_412_0 % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (550) with fresh symbol all_414_0 gives: % 117.22/16.23 | (589) addition(all_20_3, all_20_1) = all_414_0 & addition(all_20_10, % 117.22/16.23 | all_414_0) = all_190_0 & $i(all_414_0) & $i(all_190_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (589) implies: % 117.22/16.23 | (590) addition(all_20_3, all_20_1) = all_414_0 % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (543) with fresh symbol all_424_0 gives: % 117.22/16.23 | (591) addition(all_20_1, all_424_0) = all_94_0 & addition(all_20_3, % 117.22/16.23 | all_20_10) = all_424_0 & $i(all_424_0) & $i(all_94_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (591) implies: % 117.22/16.23 | (592) addition(all_20_3, all_20_10) = all_424_0 % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (544) with fresh symbol all_430_0 gives: % 117.22/16.23 | (593) addition(all_124_0, all_184_0) = all_430_0 & addition(all_20_6, % 117.22/16.23 | all_430_0) = all_20_0 & $i(all_430_0) & $i(all_20_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (593) implies: % 117.22/16.23 | (594) addition(all_124_0, all_184_0) = all_430_0 % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (548) with fresh symbol all_478_0 gives: % 117.22/16.23 | (595) addition(all_124_0, all_478_0) = one & addition(all_20_8, all_20_1) = % 117.22/16.23 | all_478_0 & $i(all_478_0) & $i(one) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (595) implies: % 117.22/16.23 | (596) addition(all_20_8, all_20_1) = all_478_0 % 117.22/16.23 | (597) addition(all_124_0, all_478_0) = one % 117.22/16.23 | % 117.22/16.23 | REDUCE: (448), (552) imply: % 117.22/16.23 | (598) multiplication(one, all_20_11) = all_20_11 % 117.22/16.23 | % 117.22/16.23 | REDUCE: (77), (552) imply: % 117.22/16.23 | (599) addition(all_20_3, all_20_6) = all_20_11 % 117.22/16.23 | % 117.22/16.23 | REDUCE: (51), (552) imply: % 117.22/16.23 | (600) addition(all_20_6, all_20_3) = all_20_11 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_184_0, all_478_0, all_20_1, all_20_8, % 117.22/16.23 | simplifying with (374), (596) gives: % 117.22/16.23 | (601) all_478_0 = all_184_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_312_0, all_478_0, all_20_1, all_20_8, % 117.22/16.23 | simplifying with (562), (596) gives: % 117.22/16.23 | (602) all_478_0 = all_312_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_124_0, all_424_0, all_20_10, all_20_3, % 117.22/16.23 | simplifying with (303), (592) gives: % 117.22/16.23 | (603) all_424_0 = all_124_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_354_0, all_424_0, all_20_10, all_20_3, % 117.22/16.23 | simplifying with (578), (592) gives: % 117.22/16.23 | (604) all_424_0 = all_354_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_20_11, all_412_0, all_20_6, all_20_3, % 117.22/16.23 | simplifying with (588), (599) gives: % 117.22/16.23 | (605) all_412_0 = all_20_11 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_20_4, all_414_0, all_20_1, all_20_3, % 117.22/16.23 | simplifying with (457), (590) gives: % 117.22/16.23 | (606) all_414_0 = all_20_4 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_314_0, all_414_0, all_20_1, all_20_3, % 117.22/16.23 | simplifying with (565), (590) gives: % 117.22/16.23 | (607) all_414_0 = all_314_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (7) with all_20_11, all_396_0, all_20_11, one, % 117.22/16.23 | simplifying with (581), (598) gives: % 117.22/16.23 | (608) all_396_0 = all_20_11 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (7) with all_20_6, all_350_0, all_20_11, all_20_12, % 117.22/16.23 | simplifying with (25), (575) gives: % 117.22/16.23 | (609) all_350_0 = all_20_6 % 117.22/16.23 | % 117.22/16.23 | COMBINE_EQS: (601), (602) imply: % 117.22/16.23 | (610) all_312_0 = all_184_0 % 117.22/16.23 | % 117.22/16.23 | COMBINE_EQS: (603), (604) imply: % 117.22/16.23 | (611) all_354_0 = all_124_0 % 117.22/16.23 | % 117.22/16.23 | SIMP: (611) implies: % 117.22/16.23 | (612) all_354_0 = all_124_0 % 117.22/16.23 | % 117.22/16.23 | COMBINE_EQS: (606), (607) imply: % 117.22/16.23 | (613) all_314_0 = all_20_4 % 117.22/16.23 | % 117.22/16.23 | REDUCE: (574), (609) imply: % 117.22/16.23 | (614) multiplication(one, all_20_6) = all_20_6 % 117.22/16.23 | % 117.22/16.23 | REDUCE: (597), (601) imply: % 117.22/16.23 | (615) addition(all_124_0, all_184_0) = one % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (6) with all_430_0, one, all_184_0, all_124_0, % 117.22/16.23 | simplifying with (594), (615) gives: % 117.22/16.23 | (616) all_430_0 = one % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_commutativity) with all_20_11, all_20_6, % 117.22/16.23 | all_322_0, simplifying with (13), (17), (570) gives: % 117.22/16.23 | (617) addition(all_20_6, all_20_11) = all_322_0 & $i(all_322_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (617) implies: % 117.22/16.23 | (618) $i(all_322_0) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_commutativity) with all_20_9, all_20_6, % 117.22/16.23 | all_318_0, simplifying with (15), (17), (568) gives: % 117.22/16.23 | (619) addition(all_20_6, all_20_9) = all_318_0 & $i(all_318_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (619) implies: % 117.22/16.23 | (620) $i(all_318_0) % 117.22/16.23 | (621) addition(all_20_6, all_20_9) = all_318_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_commutativity) with all_20_9, all_322_0, % 117.22/16.23 | all_20_0, simplifying with (15), (571), (618) gives: % 117.22/16.23 | (622) addition(all_322_0, all_20_9) = all_20_0 & $i(all_20_0) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (622) implies: % 117.22/16.23 | (623) addition(all_322_0, all_20_9) = all_20_0 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_associativity) with all_318_0, all_20_3, % 117.22/16.23 | all_20_6, all_20_11, all_20_0, simplifying with (17), (19), % 117.22/16.23 | (567), (600), (620) gives: % 117.22/16.23 | (624) ? [v0: $i] : (addition(all_20_3, all_318_0) = v0 & % 117.22/16.23 | addition(all_20_6, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_associativity) with all_20_9, all_20_6, % 117.22/16.23 | all_20_3, all_20_11, one, simplifying with (15), (17), (19), % 117.22/16.23 | (268), (599) gives: % 117.22/16.23 | (625) ? [v0: $i] : (addition(all_20_3, v0) = one & addition(all_20_6, % 117.22/16.23 | all_20_9) = v0 & $i(v0) & $i(one)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_associativity) with all_20_6, all_20_6, % 117.22/16.23 | all_20_3, all_20_11, all_322_0, simplifying with (17), (19), % 117.22/16.23 | (570), (599) gives: % 117.22/16.23 | (626) ? [v0: $i] : (addition(all_20_3, v0) = all_322_0 & % 117.22/16.23 | addition(all_20_6, all_20_6) = v0 & $i(v0) & $i(all_322_0)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (additive_commutativity) with all_124_0, all_184_0, % 117.22/16.23 | one, simplifying with (302), (539), (615) gives: % 117.22/16.23 | (627) addition(all_184_0, all_124_0) = one & $i(one) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (1) with one, all_310_0, simplifying with (542), % 117.22/16.23 | (558) gives: % 117.22/16.23 | (628) all_310_0 = one % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (2) with all_20_9, all_398_0, simplifying with % 117.22/16.23 | (15), (585) gives: % 117.22/16.23 | (629) all_398_0 = all_20_9 % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, % 117.22/16.23 | all_310_0, all_20_9, all_20_4, all_20_1, simplifying with (15), % 117.22/16.23 | (18), (29), (557), (559) gives: % 117.22/16.23 | (630) ? [v0: $i] : (multiplication(all_310_0, all_20_9) = v0 & % 117.22/16.23 | multiplication(all_20_4, v0) = all_20_1 & $i(v0) & $i(all_20_1)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, % 117.22/16.23 | all_310_0, all_20_11, all_20_4, all_20_3, simplifying with (13), % 117.22/16.23 | (18), (28), (557), (559) gives: % 117.22/16.23 | (631) ? [v0: $i] : (multiplication(all_310_0, all_20_11) = v0 & % 117.22/16.23 | multiplication(all_20_4, v0) = all_20_3 & $i(v0) & $i(all_20_3)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, one, % 117.22/16.23 | all_398_0, all_20_4, all_20_1, simplifying with (18), (449), % 117.22/16.23 | (542), (584), (586) gives: % 117.22/16.23 | (632) ? [v0: $i] : (multiplication(all_20_4, v0) = all_20_1 & % 117.22/16.23 | multiplication(one, all_398_0) = v0 & $i(v0) & $i(all_20_1)) % 117.22/16.23 | % 117.22/16.23 | GROUND_INST: instantiating (multiplicative_associativity) with all_20_4, % 117.22/16.23 | all_310_0, all_398_0, all_20_4, all_20_1, simplifying with (18), % 117.22/16.23 | (557), (559), (584), (586) gives: % 117.22/16.23 | (633) ? [v0: $i] : (multiplication(all_310_0, all_398_0) = v0 & % 117.22/16.23 | multiplication(all_20_4, v0) = all_20_1 & $i(v0) & $i(all_20_1)) % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (625) with fresh symbol all_536_0 gives: % 117.22/16.23 | (634) addition(all_20_3, all_536_0) = one & addition(all_20_6, all_20_9) = % 117.22/16.23 | all_536_0 & $i(all_536_0) & $i(one) % 117.22/16.23 | % 117.22/16.23 | ALPHA: (634) implies: % 117.22/16.23 | (635) $i(all_536_0) % 117.22/16.23 | (636) addition(all_20_6, all_20_9) = all_536_0 % 117.22/16.23 | (637) addition(all_20_3, all_536_0) = one % 117.22/16.23 | % 117.22/16.23 | DELTA: instantiating (633) with fresh symbol all_542_0 gives: % 117.22/16.24 | (638) multiplication(all_310_0, all_398_0) = all_542_0 & % 117.22/16.24 | multiplication(all_20_4, all_542_0) = all_20_1 & $i(all_542_0) & % 117.22/16.24 | $i(all_20_1) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (638) implies: % 117.22/16.24 | (639) $i(all_542_0) % 117.22/16.24 | (640) multiplication(all_310_0, all_398_0) = all_542_0 % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (624) with fresh symbol all_544_0 gives: % 117.22/16.24 | (641) addition(all_20_3, all_318_0) = all_544_0 & addition(all_20_6, % 117.22/16.24 | all_544_0) = all_20_0 & $i(all_544_0) & $i(all_20_0) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (641) implies: % 117.22/16.24 | (642) addition(all_20_3, all_318_0) = all_544_0 % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (631) with fresh symbol all_546_0 gives: % 117.22/16.24 | (643) multiplication(all_310_0, all_20_11) = all_546_0 & % 117.22/16.24 | multiplication(all_20_4, all_546_0) = all_20_3 & $i(all_546_0) & % 117.22/16.24 | $i(all_20_3) % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (626) with fresh symbol all_552_0 gives: % 117.22/16.24 | (644) addition(all_20_3, all_552_0) = all_322_0 & addition(all_20_6, % 117.22/16.24 | all_20_6) = all_552_0 & $i(all_552_0) & $i(all_322_0) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (644) implies: % 117.22/16.24 | (645) $i(all_552_0) % 117.22/16.24 | (646) addition(all_20_6, all_20_6) = all_552_0 % 117.22/16.24 | (647) addition(all_20_3, all_552_0) = all_322_0 % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (632) with fresh symbol all_556_0 gives: % 117.22/16.24 | (648) multiplication(all_20_4, all_556_0) = all_20_1 & multiplication(one, % 117.22/16.24 | all_398_0) = all_556_0 & $i(all_556_0) & $i(all_20_1) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (648) implies: % 117.22/16.24 | (649) multiplication(one, all_398_0) = all_556_0 % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (630) with fresh symbol all_566_0 gives: % 117.22/16.24 | (650) multiplication(all_310_0, all_20_9) = all_566_0 & % 117.22/16.24 | multiplication(all_20_4, all_566_0) = all_20_1 & $i(all_566_0) & % 117.22/16.24 | $i(all_20_1) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (650) implies: % 117.22/16.24 | (651) multiplication(all_310_0, all_20_9) = all_566_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (628), (629), (640) imply: % 117.22/16.24 | (652) multiplication(one, all_20_9) = all_542_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (628), (651) imply: % 117.22/16.24 | (653) multiplication(one, all_20_9) = all_566_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (629), (649) imply: % 117.22/16.24 | (654) multiplication(one, all_20_9) = all_556_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (585), (629) imply: % 117.22/16.24 | (655) multiplication(one, all_20_9) = all_20_9 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (6) with all_318_0, all_536_0, all_20_9, all_20_6, % 117.22/16.24 | simplifying with (621), (636) gives: % 117.22/16.24 | (656) all_536_0 = all_318_0 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (7) with all_20_9, all_556_0, all_20_9, one, % 117.22/16.24 | simplifying with (654), (655) gives: % 117.22/16.24 | (657) all_556_0 = all_20_9 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (7) with all_556_0, all_566_0, all_20_9, one, % 117.22/16.24 | simplifying with (653), (654) gives: % 117.22/16.24 | (658) all_566_0 = all_556_0 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (7) with all_542_0, all_566_0, all_20_9, one, % 117.22/16.24 | simplifying with (652), (653) gives: % 117.22/16.24 | (659) all_566_0 = all_542_0 % 117.22/16.24 | % 117.22/16.24 | COMBINE_EQS: (658), (659) imply: % 117.22/16.24 | (660) all_556_0 = all_542_0 % 117.22/16.24 | % 117.22/16.24 | SIMP: (660) implies: % 117.22/16.24 | (661) all_556_0 = all_542_0 % 117.22/16.24 | % 117.22/16.24 | COMBINE_EQS: (657), (661) imply: % 117.22/16.24 | (662) all_542_0 = all_20_9 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (637), (656) imply: % 117.22/16.24 | (663) addition(all_20_3, all_318_0) = one % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (6) with all_544_0, one, all_318_0, all_20_3, % 117.22/16.24 | simplifying with (642), (663) gives: % 117.22/16.24 | (664) all_544_0 = one % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (additive_idempotence) with all_20_6, all_552_0, % 117.22/16.24 | simplifying with (17), (646) gives: % 117.22/16.24 | (665) all_552_0 = all_20_6 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (additive_commutativity) with all_20_3, all_318_0, % 117.22/16.24 | one, simplifying with (19), (620), (663) gives: % 117.22/16.24 | (666) addition(all_318_0, all_20_3) = one & $i(one) % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (additive_associativity) with all_20_9, all_552_0, % 117.22/16.24 | all_20_3, all_322_0, all_20_0, simplifying with (15), (19), % 117.22/16.24 | (623), (645), (647) gives: % 117.22/16.24 | (667) ? [v0: $i] : (addition(all_552_0, all_20_9) = v0 & % 117.22/16.24 | addition(all_20_3, v0) = all_20_0 & $i(v0) & $i(all_20_0)) % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (right_distributivity) with one, all_20_6, % 117.22/16.24 | all_20_9, all_20_6, all_20_9, all_318_0, simplifying with (15), % 117.22/16.24 | (17), (542), (614), (621), (655) gives: % 117.22/16.24 | (668) ? [v0: $i] : (multiplication(one, v0) = all_318_0 & % 117.22/16.24 | addition(all_20_6, all_20_9) = v0 & $i(v0) & $i(all_318_0)) % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (668) with fresh symbol all_680_0 gives: % 117.22/16.24 | (669) multiplication(one, all_680_0) = all_318_0 & addition(all_20_6, % 117.22/16.24 | all_20_9) = all_680_0 & $i(all_680_0) & $i(all_318_0) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (669) implies: % 117.22/16.24 | (670) addition(all_20_6, all_20_9) = all_680_0 % 117.22/16.24 | % 117.22/16.24 | DELTA: instantiating (667) with fresh symbol all_686_0 gives: % 117.22/16.24 | (671) addition(all_552_0, all_20_9) = all_686_0 & addition(all_20_3, % 117.22/16.24 | all_686_0) = all_20_0 & $i(all_686_0) & $i(all_20_0) % 117.22/16.24 | % 117.22/16.24 | ALPHA: (671) implies: % 117.22/16.24 | (672) addition(all_20_3, all_686_0) = all_20_0 % 117.22/16.24 | (673) addition(all_552_0, all_20_9) = all_686_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (665), (673) imply: % 117.22/16.24 | (674) addition(all_20_6, all_20_9) = all_686_0 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (6) with all_318_0, all_686_0, all_20_9, all_20_6, % 117.22/16.24 | simplifying with (621), (674) gives: % 117.22/16.24 | (675) all_686_0 = all_318_0 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (6) with all_680_0, all_686_0, all_20_9, all_20_6, % 117.22/16.24 | simplifying with (670), (674) gives: % 117.22/16.24 | (676) all_686_0 = all_680_0 % 117.22/16.24 | % 117.22/16.24 | COMBINE_EQS: (675), (676) imply: % 117.22/16.24 | (677) all_680_0 = all_318_0 % 117.22/16.24 | % 117.22/16.24 | REDUCE: (672), (675) imply: % 117.22/16.24 | (678) addition(all_20_3, all_318_0) = all_20_0 % 117.22/16.24 | % 117.22/16.24 | GROUND_INST: instantiating (6) with one, all_20_0, all_318_0, all_20_3, % 117.22/16.24 | simplifying with (663), (678) gives: % 117.22/16.24 | (679) all_20_0 = one % 117.22/16.24 | % 117.22/16.24 | REDUCE: (9), (679) imply: % 117.22/16.24 | (680) $false % 117.22/16.24 | % 117.22/16.24 | CLOSE: (680) is inconsistent. % 117.22/16.24 | % 117.22/16.24 End of proof % 117.22/16.24 % SZS output end Proof for theBenchmark % 117.22/16.24 % 117.22/16.24 15636ms %------------------------------------------------------------------------------