%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ARI280_1 : TPTP v8.1.2. Released v5.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n019.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 : Wed Aug 30 17:47:33 EDT 2023 % Result : Theorem 22.11s 3.65s % Output : Proof 81.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ARI280_1 : TPTP v8.1.2. Released v5.0.0. % 0.13/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Aug 29 18:00:12 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.62 Running up to 7 provers in parallel. % 0.20/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.62/0.94 Prover 0: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 1: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 3: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 2: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 4: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 6: Warning: Problem contains rationals, using incomplete axiomatisation % 1.62/0.94 Prover 5: Warning: Problem contains rationals, using incomplete axiomatisation % 2.02/1.06 Prover 1: Preprocessing ... % 2.59/1.06 Prover 4: Preprocessing ... % 2.93/1.11 Prover 6: Preprocessing ... % 2.93/1.11 Prover 0: Preprocessing ... % 3.74/1.31 Prover 5: Preprocessing ... % 3.74/1.31 Prover 2: Preprocessing ... % 3.74/1.32 Prover 3: Preprocessing ... % 7.09/1.70 Prover 1: Constructing countermodel ... % 7.09/1.71 Prover 6: Constructing countermodel ... % 7.09/1.72 Prover 4: Constructing countermodel ... % 7.48/1.75 Prover 0: Proving ... % 10.54/2.17 Prover 6: gave up % 10.54/2.17 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 10.54/2.17 Prover 7: Warning: Problem contains rationals, using incomplete axiomatisation % 10.54/2.18 Prover 1: gave up % 10.54/2.19 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 10.54/2.19 Prover 8: Warning: Problem contains rationals, using incomplete axiomatisation % 10.54/2.20 Prover 8: Preprocessing ... % 11.39/2.28 Prover 8: Warning: ignoring some quantifiers % 11.39/2.28 Prover 8: Constructing countermodel ... % 11.39/2.28 Prover 7: Preprocessing ... % 12.90/2.51 Prover 8: gave up % 12.90/2.53 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 12.90/2.53 Prover 9: Warning: Problem contains rationals, using incomplete axiomatisation % 13.42/2.61 Prover 9: Preprocessing ... % 15.00/2.77 Prover 3: Constructing countermodel ... % 15.51/2.82 Prover 2: Proving ... % 16.62/3.02 Prover 5: Proving ... % 17.34/3.08 Prover 7: Warning: ignoring some quantifiers % 17.86/3.11 Prover 7: Constructing countermodel ... % 19.56/3.32 Prover 9: Constructing countermodel ... % 22.11/3.65 Prover 0: proved (3023ms) % 22.11/3.65 % 22.11/3.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.11/3.65 % 22.11/3.66 Prover 9: stopped % 22.11/3.66 Prover 2: stopped % 22.11/3.66 Prover 5: stopped % 22.11/3.66 Prover 3: stopped % 22.11/3.68 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 22.11/3.68 Prover 10: Warning: Problem contains rationals, using incomplete axiomatisation % 22.11/3.68 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 22.11/3.68 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 22.11/3.68 Prover 13: Warning: Problem contains rationals, using incomplete axiomatisation % 22.11/3.68 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 22.11/3.68 Prover 16: Warning: Problem contains rationals, using incomplete axiomatisation % 22.11/3.68 Prover 13: Preprocessing ... % 22.11/3.68 Prover 11: Warning: Problem contains rationals, using incomplete axiomatisation % 22.11/3.68 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 22.11/3.68 Prover 19: Warning: Problem contains rationals, using incomplete axiomatisation % 22.11/3.72 Prover 19: Preprocessing ... % 22.11/3.72 Prover 11: Preprocessing ... % 22.76/3.72 Prover 16: Preprocessing ... % 22.76/3.73 Prover 10: Preprocessing ... % 22.76/3.76 Prover 13: Warning: ignoring some quantifiers % 22.76/3.77 Prover 13: Constructing countermodel ... % 24.31/3.94 Prover 13: gave up % 27.56/4.36 Prover 10: Warning: ignoring some quantifiers % 27.72/4.37 Prover 10: Constructing countermodel ... % 27.72/4.43 Prover 16: Warning: ignoring some quantifiers % 27.72/4.44 Prover 16: Constructing countermodel ... % 28.21/4.54 Prover 11: Constructing countermodel ... % 36.33/5.48 Prover 19: Warning: ignoring some quantifiers % 36.33/5.51 Prover 19: Constructing countermodel ... % 64.11/9.05 Prover 19: stopped % 79.44/11.03 Prover 16: stopped % 79.77/11.09 Prover 4: Found proof (size 461) % 79.77/11.09 Prover 4: proved (10463ms) % 79.77/11.09 Prover 11: stopped % 79.77/11.10 Prover 7: stopped % 79.77/11.11 Prover 10: stopped % 79.77/11.11 % 79.77/11.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 79.77/11.11 % 80.55/11.20 % SZS output start Proof for theBenchmark % 80.55/11.20 Assumptions after simplification: % 80.55/11.20 --------------------------------- % 80.55/11.20 % 80.55/11.20 (rat_difference_problem_8) % 80.55/11.23 ? [v0: $rat] : ( ~ (v0 = rat_5/8) & rat_$difference(rat_5/2, v0) = rat_15/8) % 80.55/11.23 % 80.55/11.23 (input) % 80.83/11.27 ~ (rat_very_large = rat_very_small) & ~ (rat_very_large = rat_5/8) & ~ % 80.83/11.27 (rat_very_large = rat_15/8) & ~ (rat_very_large = rat_5/2) & ~ % 80.83/11.27 (rat_very_large = rat_0) & ~ (rat_very_small = rat_5/8) & ~ (rat_very_small % 80.83/11.27 = rat_15/8) & ~ (rat_very_small = rat_5/2) & ~ (rat_very_small = rat_0) & % 80.83/11.27 ~ (rat_5/8 = rat_15/8) & ~ (rat_5/8 = rat_5/2) & ~ (rat_5/8 = rat_0) & ~ % 80.83/11.27 (rat_15/8 = rat_5/2) & ~ (rat_15/8 = rat_0) & ~ (rat_5/2 = rat_0) & % 80.83/11.27 rat_$is_int(rat_5/8) = 1 & rat_$is_int(rat_15/8) = 1 & rat_$is_int(rat_5/2) = % 80.83/11.27 1 & rat_$is_int(rat_0) = 0 & rat_$is_rat(rat_5/8) = 0 & rat_$is_rat(rat_15/8) % 80.83/11.27 = 0 & rat_$is_rat(rat_5/2) = 0 & rat_$is_rat(rat_0) = 0 & rat_$floor(rat_5/8) % 80.83/11.27 = rat_0 & rat_$floor(rat_0) = rat_0 & rat_$ceiling(rat_0) = rat_0 & % 80.83/11.27 rat_$truncate(rat_5/8) = rat_0 & rat_$truncate(rat_0) = rat_0 & % 80.83/11.27 rat_$round(rat_0) = rat_0 & rat_$to_int(rat_5/8) = 0 & rat_$to_int(rat_15/8) = % 80.83/11.27 1 & rat_$to_int(rat_5/2) = 2 & rat_$to_int(rat_0) = 0 & rat_$to_rat(rat_5/8) = % 80.83/11.27 rat_5/8 & rat_$to_rat(rat_15/8) = rat_15/8 & rat_$to_rat(rat_5/2) = rat_5/2 & % 80.83/11.27 rat_$to_rat(rat_0) = rat_0 & rat_$to_real(rat_5/8) = real_5/8 & % 80.83/11.27 rat_$to_real(rat_15/8) = real_15/8 & rat_$to_real(rat_5/2) = real_5/2 & % 80.83/11.27 rat_$to_real(rat_0) = real_0 & int_$to_rat(0) = rat_0 & rat_$quotient(rat_0, % 80.83/11.27 rat_5/8) = rat_0 & rat_$quotient(rat_0, rat_15/8) = rat_0 & % 80.83/11.27 rat_$quotient(rat_0, rat_5/2) = rat_0 & rat_$product(rat_5/8, rat_0) = rat_0 & % 80.83/11.27 rat_$product(rat_15/8, rat_0) = rat_0 & rat_$product(rat_5/2, rat_0) = rat_0 & % 80.83/11.27 rat_$product(rat_0, rat_5/8) = rat_0 & rat_$product(rat_0, rat_15/8) = rat_0 & % 80.83/11.27 rat_$product(rat_0, rat_5/2) = rat_0 & rat_$product(rat_0, rat_0) = rat_0 & % 80.83/11.27 rat_$uminus(rat_0) = rat_0 & rat_$sum(rat_5/8, rat_15/8) = rat_5/2 & % 80.83/11.27 rat_$sum(rat_5/8, rat_0) = rat_5/8 & rat_$sum(rat_15/8, rat_5/8) = rat_5/2 & % 80.83/11.27 rat_$sum(rat_15/8, rat_0) = rat_15/8 & rat_$sum(rat_5/2, rat_0) = rat_5/2 & % 80.83/11.27 rat_$sum(rat_0, rat_5/8) = rat_5/8 & rat_$sum(rat_0, rat_15/8) = rat_15/8 & % 80.83/11.27 rat_$sum(rat_0, rat_5/2) = rat_5/2 & rat_$sum(rat_0, rat_0) = rat_0 & % 80.83/11.27 rat_$greatereq(rat_very_small, rat_very_large) = 1 & rat_$greatereq(rat_5/8, % 80.83/11.27 rat_5/8) = 0 & rat_$greatereq(rat_5/8, rat_15/8) = 1 & % 80.83/11.27 rat_$greatereq(rat_5/8, rat_5/2) = 1 & rat_$greatereq(rat_5/8, rat_0) = 0 & % 80.83/11.27 rat_$greatereq(rat_15/8, rat_5/8) = 0 & rat_$greatereq(rat_15/8, rat_15/8) = 0 % 80.83/11.27 & rat_$greatereq(rat_15/8, rat_5/2) = 1 & rat_$greatereq(rat_15/8, rat_0) = 0 % 80.83/11.27 & rat_$greatereq(rat_5/2, rat_5/8) = 0 & rat_$greatereq(rat_5/2, rat_15/8) = 0 % 80.83/11.27 & rat_$greatereq(rat_5/2, rat_5/2) = 0 & rat_$greatereq(rat_5/2, rat_0) = 0 & % 80.83/11.27 rat_$greatereq(rat_0, rat_5/8) = 1 & rat_$greatereq(rat_0, rat_15/8) = 1 & % 80.83/11.27 rat_$greatereq(rat_0, rat_5/2) = 1 & rat_$greatereq(rat_0, rat_0) = 0 & % 80.83/11.27 rat_$lesseq(rat_very_small, rat_very_large) = 0 & rat_$lesseq(rat_5/8, % 80.83/11.27 rat_5/8) = 0 & rat_$lesseq(rat_5/8, rat_15/8) = 0 & rat_$lesseq(rat_5/8, % 80.83/11.27 rat_5/2) = 0 & rat_$lesseq(rat_5/8, rat_0) = 1 & rat_$lesseq(rat_15/8, % 80.83/11.27 rat_5/8) = 1 & rat_$lesseq(rat_15/8, rat_15/8) = 0 & rat_$lesseq(rat_15/8, % 80.83/11.27 rat_5/2) = 0 & rat_$lesseq(rat_15/8, rat_0) = 1 & rat_$lesseq(rat_5/2, % 80.83/11.27 rat_5/8) = 1 & rat_$lesseq(rat_5/2, rat_15/8) = 1 & rat_$lesseq(rat_5/2, % 80.83/11.27 rat_5/2) = 0 & rat_$lesseq(rat_5/2, rat_0) = 1 & rat_$lesseq(rat_0, rat_5/8) % 80.83/11.27 = 0 & rat_$lesseq(rat_0, rat_15/8) = 0 & rat_$lesseq(rat_0, rat_5/2) = 0 & % 80.83/11.27 rat_$lesseq(rat_0, rat_0) = 0 & rat_$greater(rat_very_large, rat_5/8) = 0 & % 80.83/11.27 rat_$greater(rat_very_large, rat_15/8) = 0 & rat_$greater(rat_very_large, % 80.83/11.27 rat_5/2) = 0 & rat_$greater(rat_very_large, rat_0) = 0 & % 80.83/11.27 rat_$greater(rat_very_small, rat_very_large) = 1 & rat_$greater(rat_5/8, % 80.83/11.27 rat_very_small) = 0 & rat_$greater(rat_5/8, rat_5/8) = 1 & % 80.83/11.27 rat_$greater(rat_5/8, rat_15/8) = 1 & rat_$greater(rat_5/8, rat_5/2) = 1 & % 80.83/11.27 rat_$greater(rat_5/8, rat_0) = 0 & rat_$greater(rat_15/8, rat_very_small) = 0 % 80.83/11.27 & rat_$greater(rat_15/8, rat_5/8) = 0 & rat_$greater(rat_15/8, rat_15/8) = 1 & % 80.83/11.27 rat_$greater(rat_15/8, rat_5/2) = 1 & rat_$greater(rat_15/8, rat_0) = 0 & % 80.83/11.27 rat_$greater(rat_5/2, rat_very_small) = 0 & rat_$greater(rat_5/2, rat_5/8) = 0 % 80.83/11.27 & rat_$greater(rat_5/2, rat_15/8) = 0 & rat_$greater(rat_5/2, rat_5/2) = 1 & % 80.83/11.27 rat_$greater(rat_5/2, rat_0) = 0 & rat_$greater(rat_0, rat_very_small) = 0 & % 80.83/11.27 rat_$greater(rat_0, rat_5/8) = 1 & rat_$greater(rat_0, rat_15/8) = 1 & % 80.83/11.27 rat_$greater(rat_0, rat_5/2) = 1 & rat_$greater(rat_0, rat_0) = 1 & % 80.83/11.27 rat_$less(rat_very_small, rat_very_large) = 0 & rat_$less(rat_very_small, % 80.83/11.27 rat_5/8) = 0 & rat_$less(rat_very_small, rat_15/8) = 0 & % 80.83/11.27 rat_$less(rat_very_small, rat_5/2) = 0 & rat_$less(rat_very_small, rat_0) = 0 % 80.83/11.27 & rat_$less(rat_5/8, rat_very_large) = 0 & rat_$less(rat_5/8, rat_5/8) = 1 & % 80.83/11.27 rat_$less(rat_5/8, rat_15/8) = 0 & rat_$less(rat_5/8, rat_5/2) = 0 & % 80.83/11.27 rat_$less(rat_5/8, rat_0) = 1 & rat_$less(rat_15/8, rat_very_large) = 0 & % 80.83/11.27 rat_$less(rat_15/8, rat_5/8) = 1 & rat_$less(rat_15/8, rat_15/8) = 1 & % 80.83/11.27 rat_$less(rat_15/8, rat_5/2) = 0 & rat_$less(rat_15/8, rat_0) = 1 & % 80.83/11.27 rat_$less(rat_5/2, rat_very_large) = 0 & rat_$less(rat_5/2, rat_5/8) = 1 & % 80.83/11.27 rat_$less(rat_5/2, rat_15/8) = 1 & rat_$less(rat_5/2, rat_5/2) = 1 & % 80.83/11.27 rat_$less(rat_5/2, rat_0) = 1 & rat_$less(rat_0, rat_very_large) = 0 & % 80.83/11.27 rat_$less(rat_0, rat_5/8) = 0 & rat_$less(rat_0, rat_15/8) = 0 & % 80.83/11.27 rat_$less(rat_0, rat_5/2) = 0 & rat_$less(rat_0, rat_0) = 1 & % 80.83/11.27 rat_$difference(rat_5/8, rat_5/8) = rat_0 & rat_$difference(rat_5/8, rat_0) = % 80.83/11.27 rat_5/8 & rat_$difference(rat_15/8, rat_15/8) = rat_0 & % 80.83/11.27 rat_$difference(rat_15/8, rat_0) = rat_15/8 & rat_$difference(rat_5/2, % 80.83/11.27 rat_5/8) = rat_15/8 & rat_$difference(rat_5/2, rat_15/8) = rat_5/8 & % 80.83/11.27 rat_$difference(rat_5/2, rat_5/2) = rat_0 & rat_$difference(rat_5/2, rat_0) = % 80.83/11.27 rat_5/2 & rat_$difference(rat_0, rat_0) = rat_0 & ! [v0: $rat] : ! [v1: % 80.83/11.27 $rat] : ! [v2: $rat] : ! [v3: $rat] : ! [v4: $rat] : ( ~ (rat_$sum(v3, % 80.83/11.27 v0) = v4) | ~ (rat_$sum(v2, v1) = v3) | ? [v5: $rat] : (rat_$sum(v2, % 80.83/11.27 v5) = v4 & rat_$sum(v1, v0) = v5)) & ! [v0: $rat] : ! [v1: $rat] : ! % 80.83/11.27 [v2: $rat] : ! [v3: $rat] : ! [v4: $rat] : ( ~ (rat_$sum(v2, v3) = v4) | ~ % 80.83/11.27 (rat_$sum(v1, v0) = v3) | ? [v5: $rat] : (rat_$sum(v5, v0) = v4 & % 80.83/11.27 rat_$sum(v2, v1) = v5)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : % 80.83/11.27 ! [v3: int] : (v3 = 0 | ~ (rat_$lesseq(v2, v1) = 0) | ~ (rat_$lesseq(v2, v0) % 80.83/11.27 = v3) | ? [v4: int] : ( ~ (v4 = 0) & rat_$lesseq(v1, v0) = v4)) & ! [v0: % 80.83/11.27 $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: int] : (v3 = 0 | ~ % 80.83/11.27 (rat_$lesseq(v2, v1) = 0) | ~ (rat_$less(v2, v0) = v3) | ? [v4: int] : ( ~ % 80.83/11.27 (v4 = 0) & rat_$less(v1, v0) = v4)) & ! [v0: $rat] : ! [v1: $rat] : ! % 80.83/11.27 [v2: $rat] : ! [v3: int] : (v3 = 0 | ~ (rat_$lesseq(v2, v0) = v3) | ~ % 80.83/11.27 (rat_$lesseq(v1, v0) = 0) | ? [v4: int] : ( ~ (v4 = 0) & rat_$lesseq(v2, % 80.83/11.27 v1) = v4)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: % 80.83/11.27 int] : (v3 = 0 | ~ (rat_$lesseq(v1, v0) = 0) | ~ (rat_$less(v2, v0) = v3) % 80.83/11.27 | ? [v4: int] : ( ~ (v4 = 0) & rat_$less(v2, v1) = v4)) & ! [v0: $rat] : % 80.83/11.27 ! [v1: $rat] : ! [v2: $rat] : ! [v3: int] : (v3 = 0 | ~ (rat_$less(v2, v1) % 80.83/11.27 = 0) | ~ (rat_$less(v2, v0) = v3) | ? [v4: int] : ( ~ (v4 = 0) & % 80.83/11.27 rat_$lesseq(v1, v0) = v4)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] % 80.83/11.27 : ! [v3: int] : (v3 = 0 | ~ (rat_$less(v2, v0) = v3) | ~ (rat_$less(v1, v0) % 80.83/11.27 = 0) | ? [v4: int] : ( ~ (v4 = 0) & rat_$lesseq(v2, v1) = v4)) & ! [v0: % 80.83/11.27 $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : ( ~ (rat_$uminus(v0) % 80.83/11.27 = v2) | ~ (rat_$sum(v1, v2) = v3) | rat_$difference(v1, v0) = v3) & ! % 80.83/11.27 [v0: $rat] : ! [v1: $rat] : ! [v2: int] : (v2 = 0 | v1 = v0 | ~ % 80.83/11.27 (rat_$less(v1, v0) = v2) | ? [v3: int] : ( ~ (v3 = 0) & rat_$lesseq(v1, v0) % 80.83/11.27 = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: int] : (v2 = 0 | ~ % 80.83/11.27 (rat_$greatereq(v0, v1) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 80.83/11.27 rat_$lesseq(v1, v0) = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: int] % 80.83/11.27 : (v2 = 0 | ~ (rat_$lesseq(v1, v0) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 80.83/11.27 rat_$greatereq(v0, v1) = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: % 80.83/11.27 int] : (v2 = 0 | ~ (rat_$lesseq(v1, v0) = v2) | ? [v3: int] : ( ~ (v3 = 0) % 80.83/11.27 & rat_$less(v1, v0) = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: int] % 80.83/11.27 : (v2 = 0 | ~ (rat_$greater(v0, v1) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 80.83/11.27 rat_$less(v1, v0) = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: int] : % 80.83/11.27 (v2 = 0 | ~ (rat_$less(v1, v0) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 80.83/11.27 rat_$greater(v0, v1) = v3)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: % 80.83/11.27 $rat] : (v0 = rat_0 | ~ (rat_$product(v1, v0) = v2) | rat_$quotient(v2, v0) % 80.83/11.27 = v1) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ( ~ % 80.83/11.27 (rat_$product(v1, v0) = v2) | rat_$product(v0, v1) = v2) & ! [v0: $rat] : % 80.83/11.27 ! [v1: $rat] : ! [v2: $rat] : ( ~ (rat_$product(v0, v1) = v2) | % 80.83/11.27 rat_$product(v1, v0) = v2) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : % 80.83/11.27 ( ~ (rat_$sum(v1, v0) = v2) | rat_$sum(v0, v1) = v2) & ! [v0: $rat] : ! [v1: % 80.83/11.28 $rat] : ! [v2: $rat] : ( ~ (rat_$sum(v0, v1) = v2) | rat_$sum(v1, v0) = v2) % 80.83/11.28 & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ( ~ (rat_$lesseq(v2, v1) = % 80.83/11.28 0) | ~ (rat_$lesseq(v1, v0) = 0) | rat_$lesseq(v2, v0) = 0) & ! [v0: % 80.83/11.28 $rat] : ! [v1: $rat] : ! [v2: $rat] : ( ~ (rat_$lesseq(v2, v1) = 0) | ~ % 80.83/11.28 (rat_$less(v1, v0) = 0) | rat_$less(v2, v0) = 0) & ! [v0: $rat] : ! [v1: % 80.83/11.28 $rat] : ! [v2: $rat] : ( ~ (rat_$lesseq(v1, v0) = 0) | ~ (rat_$less(v2, % 80.83/11.28 v1) = 0) | rat_$less(v2, v0) = 0) & ! [v0: $rat] : ! [v1: $rat] : ! % 80.83/11.28 [v2: $rat] : ( ~ (rat_$difference(v1, v0) = v2) | ? [v3: $rat] : % 80.83/11.28 (rat_$uminus(v0) = v3 & rat_$sum(v1, v3) = v2)) & ! [v0: $rat] : ! [v1: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$sum(v0, rat_0) = v1)) & ! [v0: $rat] : ! [v1: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$lesseq(v1, v0) = 0) | rat_$less(v1, v0) = 0) & % 80.83/11.28 ! [v0: $rat] : ! [v1: int] : (v1 = 0 | ~ (rat_$lesseq(v0, v0) = v1)) & ! % 80.83/11.28 [v0: $rat] : ! [v1: $rat] : ( ~ (rat_$uminus(v0) = v1) | rat_$uminus(v1) = % 80.83/11.28 v0) & ! [v0: $rat] : ! [v1: $rat] : ( ~ (rat_$uminus(v0) = v1) | % 80.83/11.28 rat_$sum(v0, v1) = rat_0) & ! [v0: $rat] : ! [v1: $rat] : ( ~ % 80.83/11.28 (rat_$greatereq(v0, v1) = 0) | rat_$lesseq(v1, v0) = 0) & ! [v0: $rat] : ! % 80.83/11.28 [v1: $rat] : ( ~ (rat_$lesseq(v1, v0) = 0) | rat_$greatereq(v0, v1) = 0) & ! % 80.83/11.28 [v0: $rat] : ! [v1: $rat] : ( ~ (rat_$greater(v0, v1) = 0) | rat_$less(v1, % 80.83/11.28 v0) = 0) & ! [v0: $rat] : ! [v1: $rat] : ( ~ (rat_$less(v1, v0) = 0) | % 80.83/11.28 rat_$lesseq(v1, v0) = 0) & ! [v0: $rat] : ! [v1: $rat] : ( ~ % 80.83/11.28 (rat_$less(v1, v0) = 0) | rat_$greater(v0, v1) = 0) & ! [v0: $rat] : ! % 80.83/11.28 [v1: MultipleValueBool] : ( ~ (rat_$less(v0, v0) = v1) | rat_$lesseq(v0, v0) = % 80.83/11.28 0) & ! [v0: $rat] : (v0 = rat_0 | ~ (rat_$uminus(v0) = v0)) % 80.83/11.28 % 80.83/11.28 (function-axioms) % 80.83/11.28 ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : (v1 = v0 | ~ % 80.83/11.28 (rat_$quotient(v3, v2) = v1) | ~ (rat_$quotient(v3, v2) = v0)) & ! [v0: % 80.83/11.28 $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : (v1 = v0 | ~ % 80.83/11.28 (rat_$product(v3, v2) = v1) | ~ (rat_$product(v3, v2) = v0)) & ! [v0: % 80.83/11.28 $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : (v1 = v0 | ~ % 80.83/11.28 (rat_$sum(v3, v2) = v1) | ~ (rat_$sum(v3, v2) = v0)) & ! [v0: % 80.83/11.28 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $rat] : ! [v3: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$greatereq(v3, v2) = v1) | ~ (rat_$greatereq(v3, % 80.83/11.28 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 80.83/11.28 ! [v2: $rat] : ! [v3: $rat] : (v1 = v0 | ~ (rat_$lesseq(v3, v2) = v1) | ~ % 80.83/11.28 (rat_$lesseq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 80.83/11.28 MultipleValueBool] : ! [v2: $rat] : ! [v3: $rat] : (v1 = v0 | ~ % 80.83/11.28 (rat_$greater(v3, v2) = v1) | ~ (rat_$greater(v3, v2) = v0)) & ! [v0: % 80.83/11.28 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $rat] : ! [v3: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$less(v3, v2) = v1) | ~ (rat_$less(v3, v2) = % 80.83/11.28 v0)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : (v1 % 80.83/11.28 = v0 | ~ (rat_$difference(v3, v2) = v1) | ~ (rat_$difference(v3, v2) = % 80.83/11.28 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$is_int(v2) = v1) | ~ (rat_$is_int(v2) = v0)) & % 80.83/11.28 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $rat] : (v1 = % 80.83/11.28 v0 | ~ (rat_$is_rat(v2) = v1) | ~ (rat_$is_rat(v2) = v0)) & ! [v0: $rat] % 80.83/11.28 : ! [v1: $rat] : ! [v2: $rat] : (v1 = v0 | ~ (rat_$floor(v2) = v1) | ~ % 80.83/11.28 (rat_$floor(v2) = v0)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : (v1 % 80.83/11.28 = v0 | ~ (rat_$ceiling(v2) = v1) | ~ (rat_$ceiling(v2) = v0)) & ! [v0: % 80.83/11.28 $rat] : ! [v1: $rat] : ! [v2: $rat] : (v1 = v0 | ~ (rat_$truncate(v2) = % 80.83/11.28 v1) | ~ (rat_$truncate(v2) = v0)) & ! [v0: $rat] : ! [v1: $rat] : ! % 80.83/11.28 [v2: $rat] : (v1 = v0 | ~ (rat_$round(v2) = v1) | ~ (rat_$round(v2) = v0)) & % 80.83/11.28 ! [v0: int] : ! [v1: int] : ! [v2: $rat] : (v1 = v0 | ~ (rat_$to_int(v2) = % 80.83/11.28 v1) | ~ (rat_$to_int(v2) = v0)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: % 80.83/11.28 $rat] : (v1 = v0 | ~ (rat_$to_rat(v2) = v1) | ~ (rat_$to_rat(v2) = v0)) & % 80.83/11.28 ! [v0: $real] : ! [v1: $real] : ! [v2: $rat] : (v1 = v0 | ~ % 80.83/11.28 (rat_$to_real(v2) = v1) | ~ (rat_$to_real(v2) = v0)) & ! [v0: $rat] : ! % 80.83/11.28 [v1: $rat] : ! [v2: int] : (v1 = v0 | ~ (int_$to_rat(v2) = v1) | ~ % 80.83/11.28 (int_$to_rat(v2) = v0)) & ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : % 80.83/11.28 (v1 = v0 | ~ (rat_$uminus(v2) = v1) | ~ (rat_$uminus(v2) = v0)) % 80.83/11.28 % 80.83/11.28 Those formulas are unsatisfiable: % 80.83/11.28 --------------------------------- % 80.83/11.28 % 80.83/11.28 Begin of proof % 80.83/11.28 | % 80.83/11.28 | ALPHA: (function-axioms) implies: % 80.83/11.29 | (1) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : (v1 = v0 | ~ % 80.83/11.29 | (rat_$uminus(v2) = v1) | ~ (rat_$uminus(v2) = v0)) % 80.83/11.29 | (2) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : (v1 = % 80.83/11.29 | v0 | ~ (rat_$sum(v3, v2) = v1) | ~ (rat_$sum(v3, v2) = v0)) % 80.83/11.29 | % 80.83/11.29 | ALPHA: (input) implies: % 80.83/11.29 | (3) rat_$difference(rat_5/2, rat_5/2) = rat_0 % 80.83/11.29 | (4) rat_$difference(rat_5/2, rat_15/8) = rat_5/8 % 80.83/11.29 | (5) rat_$difference(rat_5/2, rat_5/8) = rat_15/8 % 80.83/11.29 | (6) rat_$difference(rat_15/8, rat_15/8) = rat_0 % 80.83/11.29 | (7) rat_$difference(rat_5/8, rat_5/8) = rat_0 % 80.83/11.29 | (8) rat_$less(rat_5/2, rat_5/8) = 1 % 80.83/11.29 | (9) rat_$less(rat_very_small, rat_5/8) = 0 % 80.83/11.29 | (10) rat_$sum(rat_0, rat_0) = rat_0 % 80.83/11.29 | (11) rat_$sum(rat_0, rat_5/2) = rat_5/2 % 80.83/11.29 | (12) rat_$sum(rat_0, rat_15/8) = rat_15/8 % 80.83/11.29 | (13) rat_$sum(rat_0, rat_5/8) = rat_5/8 % 80.83/11.29 | (14) rat_$sum(rat_5/2, rat_0) = rat_5/2 % 80.83/11.29 | (15) rat_$sum(rat_15/8, rat_0) = rat_15/8 % 80.83/11.29 | (16) rat_$sum(rat_15/8, rat_5/8) = rat_5/2 % 80.83/11.29 | (17) rat_$sum(rat_5/8, rat_0) = rat_5/8 % 80.83/11.29 | (18) rat_$sum(rat_5/8, rat_15/8) = rat_5/2 % 80.83/11.29 | (19) ! [v0: $rat] : ! [v1: $rat] : ( ~ (rat_$uminus(v0) = v1) | % 80.83/11.29 | rat_$uminus(v1) = v0) % 80.83/11.29 | (20) ! [v0: $rat] : ! [v1: $rat] : (v1 = v0 | ~ (rat_$sum(v0, rat_0) = % 80.83/11.29 | v1)) % 80.83/11.29 | (21) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ( ~ % 80.83/11.29 | (rat_$difference(v1, v0) = v2) | ? [v3: $rat] : (rat_$uminus(v0) = % 80.83/11.29 | v3 & rat_$sum(v1, v3) = v2)) % 80.83/11.29 | (22) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ( ~ (rat_$sum(v1, v0) % 80.83/11.29 | = v2) | rat_$sum(v0, v1) = v2) % 80.83/11.29 | (23) ! [v0: $rat] : ! [v1: $rat] : ! [v2: int] : (v2 = 0 | ~ % 80.83/11.29 | (rat_$lesseq(v1, v0) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 80.83/11.29 | rat_$greatereq(v0, v1) = v3)) % 80.83/11.29 | (24) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: int] : (v3 = 0 % 80.83/11.29 | | ~ (rat_$less(v2, v0) = v3) | ~ (rat_$less(v1, v0) = 0) | ? [v4: % 80.83/11.29 | int] : ( ~ (v4 = 0) & rat_$lesseq(v2, v1) = v4)) % 80.83/11.29 | (25) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : ! % 80.83/11.29 | [v4: $rat] : ( ~ (rat_$sum(v2, v3) = v4) | ~ (rat_$sum(v1, v0) = v3) % 80.83/11.29 | | ? [v5: $rat] : (rat_$sum(v5, v0) = v4 & rat_$sum(v2, v1) = v5)) % 80.83/11.30 | (26) ! [v0: $rat] : ! [v1: $rat] : ! [v2: $rat] : ! [v3: $rat] : ! % 80.83/11.30 | [v4: $rat] : ( ~ (rat_$sum(v3, v0) = v4) | ~ (rat_$sum(v2, v1) = v3) % 80.83/11.30 | | ? [v5: $rat] : (rat_$sum(v2, v5) = v4 & rat_$sum(v1, v0) = v5)) % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (rat_difference_problem_8) with fresh symbol all_5_0 % 80.83/11.30 | gives: % 80.83/11.30 | (27) ~ (all_5_0 = rat_5/8) & rat_$difference(rat_5/2, all_5_0) = rat_15/8 % 80.83/11.30 | % 80.83/11.30 | ALPHA: (27) implies: % 80.83/11.30 | (28) ~ (all_5_0 = rat_5/8) % 80.83/11.30 | (29) rat_$difference(rat_5/2, all_5_0) = rat_15/8 % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with rat_5/2, rat_5/2, rat_0, simplifying with % 80.83/11.30 | (3) gives: % 80.83/11.30 | (30) ? [v0: $rat] : (rat_$uminus(rat_5/2) = v0 & rat_$sum(rat_5/2, v0) = % 80.83/11.30 | rat_0) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with rat_15/8, rat_5/2, rat_5/8, simplifying % 80.83/11.30 | with (4) gives: % 80.83/11.30 | (31) ? [v0: $rat] : (rat_$uminus(rat_15/8) = v0 & rat_$sum(rat_5/2, v0) = % 80.83/11.30 | rat_5/8) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with rat_5/8, rat_5/2, rat_15/8, simplifying % 80.83/11.30 | with (5) gives: % 80.83/11.30 | (32) ? [v0: $rat] : (rat_$uminus(rat_5/8) = v0 & rat_$sum(rat_5/2, v0) = % 80.83/11.30 | rat_15/8) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with all_5_0, rat_5/2, rat_15/8, simplifying % 80.83/11.30 | with (29) gives: % 80.83/11.30 | (33) ? [v0: $rat] : (rat_$uminus(all_5_0) = v0 & rat_$sum(rat_5/2, v0) = % 80.83/11.30 | rat_15/8) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with rat_15/8, rat_15/8, rat_0, simplifying % 80.83/11.30 | with (6) gives: % 80.83/11.30 | (34) ? [v0: $rat] : (rat_$uminus(rat_15/8) = v0 & rat_$sum(rat_15/8, v0) = % 80.83/11.30 | rat_0) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (21) with rat_5/8, rat_5/8, rat_0, simplifying with % 80.83/11.30 | (7) gives: % 80.83/11.30 | (35) ? [v0: $rat] : (rat_$uminus(rat_5/8) = v0 & rat_$sum(rat_5/8, v0) = % 80.83/11.30 | rat_0) % 80.83/11.30 | % 80.83/11.30 | GROUND_INST: instantiating (24) with rat_5/8, rat_very_small, rat_5/2, 1, % 80.83/11.30 | simplifying with (8), (9) gives: % 80.83/11.30 | (36) ? [v0: int] : ( ~ (v0 = 0) & rat_$lesseq(rat_5/2, rat_very_small) = % 80.83/11.30 | v0) % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (33) with fresh symbol all_23_0 gives: % 80.83/11.30 | (37) rat_$uminus(all_5_0) = all_23_0 & rat_$sum(rat_5/2, all_23_0) = % 80.83/11.30 | rat_15/8 % 80.83/11.30 | % 80.83/11.30 | ALPHA: (37) implies: % 80.83/11.30 | (38) rat_$sum(rat_5/2, all_23_0) = rat_15/8 % 80.83/11.30 | (39) rat_$uminus(all_5_0) = all_23_0 % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (31) with fresh symbol all_25_0 gives: % 80.83/11.30 | (40) rat_$uminus(rat_15/8) = all_25_0 & rat_$sum(rat_5/2, all_25_0) = % 80.83/11.30 | rat_5/8 % 80.83/11.30 | % 80.83/11.30 | ALPHA: (40) implies: % 80.83/11.30 | (41) rat_$sum(rat_5/2, all_25_0) = rat_5/8 % 80.83/11.30 | (42) rat_$uminus(rat_15/8) = all_25_0 % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (30) with fresh symbol all_27_0 gives: % 80.83/11.30 | (43) rat_$uminus(rat_5/2) = all_27_0 & rat_$sum(rat_5/2, all_27_0) = rat_0 % 80.83/11.30 | % 80.83/11.30 | ALPHA: (43) implies: % 80.83/11.30 | (44) rat_$sum(rat_5/2, all_27_0) = rat_0 % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (35) with fresh symbol all_31_0 gives: % 80.83/11.30 | (45) rat_$uminus(rat_5/8) = all_31_0 & rat_$sum(rat_5/8, all_31_0) = rat_0 % 80.83/11.30 | % 80.83/11.30 | ALPHA: (45) implies: % 80.83/11.30 | (46) rat_$sum(rat_5/8, all_31_0) = rat_0 % 80.83/11.30 | (47) rat_$uminus(rat_5/8) = all_31_0 % 80.83/11.30 | % 80.83/11.30 | DELTA: instantiating (34) with fresh symbol all_33_0 gives: % 80.83/11.31 | (48) rat_$uminus(rat_15/8) = all_33_0 & rat_$sum(rat_15/8, all_33_0) = % 80.83/11.31 | rat_0 % 80.83/11.31 | % 80.83/11.31 | ALPHA: (48) implies: % 80.83/11.31 | (49) rat_$sum(rat_15/8, all_33_0) = rat_0 % 80.83/11.31 | (50) rat_$uminus(rat_15/8) = all_33_0 % 80.83/11.31 | % 80.83/11.31 | DELTA: instantiating (32) with fresh symbol all_35_0 gives: % 80.83/11.31 | (51) rat_$uminus(rat_5/8) = all_35_0 & rat_$sum(rat_5/2, all_35_0) = % 80.83/11.31 | rat_15/8 % 80.83/11.31 | % 80.83/11.31 | ALPHA: (51) implies: % 80.83/11.31 | (52) rat_$sum(rat_5/2, all_35_0) = rat_15/8 % 80.83/11.31 | (53) rat_$uminus(rat_5/8) = all_35_0 % 80.83/11.31 | % 80.83/11.31 | DELTA: instantiating (36) with fresh symbol all_41_0 gives: % 80.83/11.31 | (54) ~ (all_41_0 = 0) & rat_$lesseq(rat_5/2, rat_very_small) = all_41_0 % 80.83/11.31 | % 80.83/11.31 | ALPHA: (54) implies: % 80.83/11.31 | (55) ~ (all_41_0 = 0) % 80.83/11.31 | (56) rat_$lesseq(rat_5/2, rat_very_small) = all_41_0 % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (1) with all_25_0, all_33_0, rat_15/8, simplifying % 80.83/11.31 | with (42), (50) gives: % 80.83/11.31 | (57) all_33_0 = all_25_0 % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (1) with all_31_0, all_35_0, rat_5/8, simplifying % 80.83/11.31 | with (47), (53) gives: % 80.83/11.31 | (58) all_35_0 = all_31_0 % 80.83/11.31 | % 80.83/11.31 | REDUCE: (49), (57) imply: % 80.83/11.31 | (59) rat_$sum(rat_15/8, all_25_0) = rat_0 % 80.83/11.31 | % 80.83/11.31 | REDUCE: (52), (58) imply: % 80.83/11.31 | (60) rat_$sum(rat_5/2, all_31_0) = rat_15/8 % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (23) with rat_very_small, rat_5/2, all_41_0, % 80.83/11.31 | simplifying with (56) gives: % 80.83/11.31 | (61) all_41_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 80.83/11.31 | rat_$greatereq(rat_very_small, rat_5/2) = v0) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with all_23_0, rat_15/8, rat_5/8, rat_5/2, % 80.83/11.31 | rat_15/8, simplifying with (18), (38) gives: % 80.83/11.31 | (62) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = rat_15/8 & rat_$sum(rat_15/8, % 80.83/11.31 | all_23_0) = v0) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (25) with all_23_0, rat_5/2, rat_5/8, rat_15/8, % 80.83/11.31 | rat_5/2, simplifying with (18), (38) gives: % 80.83/11.31 | (63) ? [v0: $rat] : (rat_$sum(v0, all_23_0) = rat_5/2 & rat_$sum(rat_5/8, % 80.83/11.31 | rat_5/2) = v0) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with all_23_0, rat_5/8, rat_15/8, rat_5/2, % 80.83/11.31 | rat_15/8, simplifying with (16), (38) gives: % 80.83/11.31 | (64) ? [v0: $rat] : (rat_$sum(rat_5/8, all_23_0) = v0 & rat_$sum(rat_15/8, % 80.83/11.31 | v0) = rat_15/8) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with rat_0, all_23_0, rat_5/2, rat_15/8, % 80.83/11.31 | rat_15/8, simplifying with (15), (38) gives: % 80.83/11.31 | (65) ? [v0: $rat] : (rat_$sum(all_23_0, rat_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.31 | v0) = rat_15/8) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with all_23_0, rat_0, rat_5/2, rat_5/2, % 80.83/11.31 | rat_15/8, simplifying with (14), (38) gives: % 80.83/11.31 | (66) ? [v0: $rat] : (rat_$sum(rat_5/2, v0) = rat_15/8 & rat_$sum(rat_0, % 80.83/11.31 | all_23_0) = v0) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (22) with all_23_0, rat_5/2, rat_15/8, simplifying % 80.83/11.31 | with (38) gives: % 80.83/11.31 | (67) rat_$sum(all_23_0, rat_5/2) = rat_15/8 % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with rat_15/8, all_25_0, rat_5/2, rat_5/8, % 80.83/11.31 | rat_5/2, simplifying with (18), (41) gives: % 80.83/11.31 | (68) ? [v0: $rat] : (rat_$sum(all_25_0, rat_15/8) = v0 & rat_$sum(rat_5/2, % 80.83/11.31 | v0) = rat_5/2) % 80.83/11.31 | % 80.83/11.31 | GROUND_INST: instantiating (26) with rat_0, all_25_0, rat_5/2, rat_5/8, % 80.83/11.31 | rat_5/8, simplifying with (17), (41) gives: % 80.83/11.31 | (69) ? [v0: $rat] : (rat_$sum(all_25_0, rat_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.32 | v0) = rat_5/8) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with all_25_0, rat_5/8, rat_15/8, rat_5/2, % 80.83/11.32 | rat_5/8, simplifying with (16), (41) gives: % 80.83/11.32 | (70) ? [v0: $rat] : (rat_$sum(rat_5/8, all_25_0) = v0 & rat_$sum(rat_15/8, % 80.83/11.32 | v0) = rat_5/8) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (25) with all_25_0, rat_5/2, rat_15/8, rat_5/8, % 80.83/11.32 | rat_5/2, simplifying with (16), (41) gives: % 80.83/11.32 | (71) ? [v0: $rat] : (rat_$sum(v0, all_25_0) = rat_5/2 & rat_$sum(rat_15/8, % 80.83/11.32 | rat_5/2) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with all_25_0, rat_0, rat_5/2, rat_5/2, % 80.83/11.32 | rat_5/8, simplifying with (14), (41) gives: % 80.83/11.32 | (72) ? [v0: $rat] : (rat_$sum(rat_5/2, v0) = rat_5/8 & rat_$sum(rat_0, % 80.83/11.32 | all_25_0) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (22) with all_25_0, rat_5/2, rat_5/8, simplifying % 80.83/11.32 | with (41) gives: % 80.83/11.32 | (73) rat_$sum(all_25_0, rat_5/2) = rat_5/8 % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with all_27_0, rat_15/8, rat_5/8, rat_5/2, % 80.83/11.32 | rat_0, simplifying with (18), (44) gives: % 80.83/11.32 | (74) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = rat_0 & rat_$sum(rat_15/8, % 80.83/11.32 | all_27_0) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (25) with all_27_0, rat_5/2, rat_5/8, rat_0, % 80.83/11.32 | rat_5/8, simplifying with (17), (44) gives: % 80.83/11.32 | (75) ? [v0: $rat] : (rat_$sum(v0, all_27_0) = rat_5/8 & rat_$sum(rat_5/8, % 80.83/11.32 | rat_5/2) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with all_27_0, rat_5/8, rat_15/8, rat_5/2, % 80.83/11.32 | rat_0, simplifying with (16), (44) gives: % 80.83/11.32 | (76) ? [v0: $rat] : (rat_$sum(rat_5/8, all_27_0) = v0 & rat_$sum(rat_15/8, % 80.83/11.32 | v0) = rat_0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (25) with all_27_0, rat_5/2, rat_15/8, rat_0, % 80.83/11.32 | rat_15/8, simplifying with (15), (44) gives: % 80.83/11.32 | (77) ? [v0: $rat] : (rat_$sum(v0, all_27_0) = rat_15/8 & % 80.83/11.32 | rat_$sum(rat_15/8, rat_5/2) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with all_27_0, rat_0, rat_5/2, rat_5/2, rat_0, % 80.83/11.32 | simplifying with (14), (44) gives: % 80.83/11.32 | (78) ? [v0: $rat] : (rat_$sum(rat_5/2, v0) = rat_0 & rat_$sum(rat_0, % 80.83/11.32 | all_27_0) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (25) with all_27_0, rat_5/2, rat_5/2, rat_0, % 80.83/11.32 | rat_5/2, simplifying with (14), (44) gives: % 80.83/11.32 | (79) ? [v0: $rat] : (rat_$sum(v0, all_27_0) = rat_5/2 & rat_$sum(rat_5/2, % 80.83/11.32 | rat_5/2) = v0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with rat_5/8, all_27_0, rat_5/2, rat_0, % 80.83/11.32 | rat_5/8, simplifying with (13), (44) gives: % 80.83/11.32 | (80) ? [v0: $rat] : (rat_$sum(all_27_0, rat_5/8) = v0 & rat_$sum(rat_5/2, % 80.83/11.32 | v0) = rat_5/8) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with rat_15/8, all_27_0, rat_5/2, rat_0, % 80.83/11.32 | rat_15/8, simplifying with (12), (44) gives: % 80.83/11.32 | (81) ? [v0: $rat] : (rat_$sum(all_27_0, rat_15/8) = v0 & rat_$sum(rat_5/2, % 80.83/11.32 | v0) = rat_15/8) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with rat_5/2, all_27_0, rat_5/2, rat_0, % 80.83/11.32 | rat_5/2, simplifying with (11), (44) gives: % 80.83/11.32 | (82) ? [v0: $rat] : (rat_$sum(all_27_0, rat_5/2) = v0 & rat_$sum(rat_5/2, % 80.83/11.32 | v0) = rat_5/2) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (26) with rat_0, all_27_0, rat_5/2, rat_0, rat_0, % 80.83/11.32 | simplifying with (10), (44) gives: % 80.83/11.32 | (83) ? [v0: $rat] : (rat_$sum(all_27_0, rat_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.32 | v0) = rat_0) % 80.83/11.32 | % 80.83/11.32 | GROUND_INST: instantiating (22) with all_27_0, rat_5/2, rat_0, simplifying % 80.83/11.32 | with (44) gives: % 80.83/11.33 | (84) rat_$sum(all_27_0, rat_5/2) = rat_0 % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (25) with all_31_0, rat_5/2, rat_5/8, rat_15/8, % 80.83/11.33 | rat_5/2, simplifying with (18), (60) gives: % 80.83/11.33 | (85) ? [v0: $rat] : (rat_$sum(v0, all_31_0) = rat_5/2 & rat_$sum(rat_5/8, % 80.83/11.33 | rat_5/2) = v0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_5/8, all_31_0, rat_5/2, rat_15/8, % 80.83/11.33 | rat_5/2, simplifying with (16), (60) gives: % 80.83/11.33 | (86) ? [v0: $rat] : (rat_$sum(all_31_0, rat_5/8) = v0 & rat_$sum(rat_5/2, % 80.83/11.33 | v0) = rat_5/2) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_0, all_31_0, rat_5/2, rat_15/8, % 80.83/11.33 | rat_15/8, simplifying with (15), (60) gives: % 80.83/11.33 | (87) ? [v0: $rat] : (rat_$sum(all_31_0, rat_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.33 | v0) = rat_15/8) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with all_31_0, rat_0, rat_5/2, rat_5/2, % 80.83/11.33 | rat_15/8, simplifying with (14), (60) gives: % 80.83/11.33 | (88) ? [v0: $rat] : (rat_$sum(rat_5/2, v0) = rat_15/8 & rat_$sum(rat_0, % 80.83/11.33 | all_31_0) = v0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (22) with all_31_0, rat_5/2, rat_15/8, simplifying % 80.83/11.33 | with (60) gives: % 80.83/11.33 | (89) rat_$sum(all_31_0, rat_5/2) = rat_15/8 % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with all_25_0, rat_0, rat_15/8, rat_15/8, % 80.83/11.33 | rat_0, simplifying with (15), (59) gives: % 80.83/11.33 | (90) ? [v0: $rat] : (rat_$sum(rat_15/8, v0) = rat_0 & rat_$sum(rat_0, % 80.83/11.33 | all_25_0) = v0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (25) with all_25_0, rat_15/8, rat_15/8, rat_0, % 80.83/11.33 | rat_15/8, simplifying with (15), (59) gives: % 80.83/11.33 | (91) ? [v0: $rat] : (rat_$sum(v0, all_25_0) = rat_15/8 & % 80.83/11.33 | rat_$sum(rat_15/8, rat_15/8) = v0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (25) with all_25_0, rat_15/8, rat_5/2, rat_0, % 80.83/11.33 | rat_5/2, simplifying with (14), (59) gives: % 80.83/11.33 | (92) ? [v0: $rat] : (rat_$sum(v0, all_25_0) = rat_5/2 & rat_$sum(rat_5/2, % 80.83/11.33 | rat_15/8) = v0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_5/8, all_25_0, rat_15/8, rat_0, % 80.83/11.33 | rat_5/8, simplifying with (13), (59) gives: % 80.83/11.33 | (93) ? [v0: $rat] : (rat_$sum(all_25_0, rat_5/8) = v0 & rat_$sum(rat_15/8, % 80.83/11.33 | v0) = rat_5/8) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_15/8, all_25_0, rat_15/8, rat_0, % 80.83/11.33 | rat_15/8, simplifying with (12), (59) gives: % 80.83/11.33 | (94) ? [v0: $rat] : (rat_$sum(all_25_0, rat_15/8) = v0 & % 80.83/11.33 | rat_$sum(rat_15/8, v0) = rat_15/8) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_5/2, all_25_0, rat_15/8, rat_0, % 80.83/11.33 | rat_5/2, simplifying with (11), (59) gives: % 80.83/11.33 | (95) ? [v0: $rat] : (rat_$sum(all_25_0, rat_5/2) = v0 & rat_$sum(rat_15/8, % 80.83/11.33 | v0) = rat_5/2) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with rat_0, all_25_0, rat_15/8, rat_0, rat_0, % 80.83/11.33 | simplifying with (10), (59) gives: % 80.83/11.33 | (96) ? [v0: $rat] : (rat_$sum(all_25_0, rat_0) = v0 & rat_$sum(rat_15/8, % 80.83/11.33 | v0) = rat_0) % 80.83/11.33 | % 80.83/11.33 | GROUND_INST: instantiating (26) with all_25_0, all_31_0, rat_5/2, rat_15/8, % 80.83/11.33 | rat_0, simplifying with (59), (60) gives: % 80.83/11.33 | (97) ? [v0: $rat] : (rat_$sum(all_31_0, all_25_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.33 | v0) = rat_0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with all_25_0, all_23_0, rat_5/2, rat_15/8, % 80.83/11.34 | rat_0, simplifying with (38), (59) gives: % 80.83/11.34 | (98) ? [v0: $rat] : (rat_$sum(all_23_0, all_25_0) = v0 & rat_$sum(rat_5/2, % 80.83/11.34 | v0) = rat_0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (22) with all_25_0, rat_15/8, rat_0, simplifying % 80.83/11.34 | with (59) gives: % 80.83/11.34 | (99) rat_$sum(all_25_0, rat_15/8) = rat_0 % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with all_31_0, rat_0, rat_5/8, rat_5/8, rat_0, % 80.83/11.34 | simplifying with (17), (46) gives: % 80.83/11.34 | (100) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = rat_0 & rat_$sum(rat_0, % 80.83/11.34 | all_31_0) = v0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (25) with all_31_0, rat_5/8, rat_5/2, rat_0, % 80.83/11.34 | rat_5/2, simplifying with (14), (46) gives: % 80.83/11.34 | (101) ? [v0: $rat] : (rat_$sum(v0, all_31_0) = rat_5/2 & rat_$sum(rat_5/2, % 80.83/11.34 | rat_5/8) = v0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with rat_5/8, all_31_0, rat_5/8, rat_0, % 80.83/11.34 | rat_5/8, simplifying with (13), (46) gives: % 80.83/11.34 | (102) ? [v0: $rat] : (rat_$sum(all_31_0, rat_5/8) = v0 & rat_$sum(rat_5/8, % 80.83/11.34 | v0) = rat_5/8) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with rat_15/8, all_31_0, rat_5/8, rat_0, % 80.83/11.34 | rat_15/8, simplifying with (12), (46) gives: % 80.83/11.34 | (103) ? [v0: $rat] : (rat_$sum(all_31_0, rat_15/8) = v0 & % 80.83/11.34 | rat_$sum(rat_5/8, v0) = rat_15/8) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with rat_5/2, all_31_0, rat_5/8, rat_0, % 80.83/11.34 | rat_5/2, simplifying with (11), (46) gives: % 80.83/11.34 | (104) ? [v0: $rat] : (rat_$sum(all_31_0, rat_5/2) = v0 & rat_$sum(rat_5/8, % 80.83/11.34 | v0) = rat_5/2) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with rat_0, all_31_0, rat_5/8, rat_0, rat_0, % 80.83/11.34 | simplifying with (10), (46) gives: % 80.83/11.34 | (105) ? [v0: $rat] : (rat_$sum(all_31_0, rat_0) = v0 & rat_$sum(rat_5/8, % 80.83/11.34 | v0) = rat_0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (26) with all_31_0, all_25_0, rat_5/2, rat_5/8, % 80.83/11.34 | rat_0, simplifying with (41), (46) gives: % 80.83/11.34 | (106) ? [v0: $rat] : (rat_$sum(all_25_0, all_31_0) = v0 & % 80.83/11.34 | rat_$sum(rat_5/2, v0) = rat_0) % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (22) with all_31_0, rat_5/8, rat_0, simplifying % 80.83/11.34 | with (46) gives: % 80.83/11.34 | (107) rat_$sum(all_31_0, rat_5/8) = rat_0 % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (19) with rat_5/8, all_31_0, simplifying with (47) % 80.83/11.34 | gives: % 80.83/11.34 | (108) rat_$uminus(all_31_0) = rat_5/8 % 80.83/11.34 | % 80.83/11.34 | GROUND_INST: instantiating (19) with all_5_0, all_23_0, simplifying with (39) % 80.83/11.34 | gives: % 80.83/11.34 | (109) rat_$uminus(all_23_0) = all_5_0 % 80.83/11.34 | % 80.83/11.34 | DELTA: instantiating (83) with fresh symbol all_55_0 gives: % 80.83/11.34 | (110) rat_$sum(all_27_0, rat_0) = all_55_0 & rat_$sum(rat_5/2, all_55_0) = % 80.83/11.34 | rat_0 % 80.83/11.34 | % 80.83/11.35 | ALPHA: (110) implies: % 80.83/11.35 | (111) rat_$sum(rat_5/2, all_55_0) = rat_0 % 80.83/11.35 | (112) rat_$sum(all_27_0, rat_0) = all_55_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (98) with fresh symbol all_57_0 gives: % 80.83/11.35 | (113) rat_$sum(all_23_0, all_25_0) = all_57_0 & rat_$sum(rat_5/2, all_57_0) % 80.83/11.35 | = rat_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (113) implies: % 80.83/11.35 | (114) rat_$sum(rat_5/2, all_57_0) = rat_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (68) with fresh symbol all_59_0 gives: % 80.83/11.35 | (115) rat_$sum(all_25_0, rat_15/8) = all_59_0 & rat_$sum(rat_5/2, all_59_0) % 80.83/11.35 | = rat_5/2 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (115) implies: % 80.83/11.35 | (116) rat_$sum(rat_5/2, all_59_0) = rat_5/2 % 80.83/11.35 | (117) rat_$sum(all_25_0, rat_15/8) = all_59_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (106) with fresh symbol all_61_0 gives: % 80.83/11.35 | (118) rat_$sum(all_25_0, all_31_0) = all_61_0 & rat_$sum(rat_5/2, all_61_0) % 80.83/11.35 | = rat_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (118) implies: % 80.83/11.35 | (119) rat_$sum(rat_5/2, all_61_0) = rat_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (105) with fresh symbol all_63_0 gives: % 80.83/11.35 | (120) rat_$sum(all_31_0, rat_0) = all_63_0 & rat_$sum(rat_5/8, all_63_0) = % 80.83/11.35 | rat_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (120) implies: % 80.83/11.35 | (121) rat_$sum(all_31_0, rat_0) = all_63_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (102) with fresh symbol all_65_0 gives: % 80.83/11.35 | (122) rat_$sum(all_31_0, rat_5/8) = all_65_0 & rat_$sum(rat_5/8, all_65_0) % 80.83/11.35 | = rat_5/8 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (122) implies: % 80.83/11.35 | (123) rat_$sum(rat_5/8, all_65_0) = rat_5/8 % 80.83/11.35 | (124) rat_$sum(all_31_0, rat_5/8) = all_65_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (95) with fresh symbol all_69_0 gives: % 80.83/11.35 | (125) rat_$sum(all_25_0, rat_5/2) = all_69_0 & rat_$sum(rat_15/8, all_69_0) % 80.83/11.35 | = rat_5/2 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (125) implies: % 80.83/11.35 | (126) rat_$sum(rat_15/8, all_69_0) = rat_5/2 % 80.83/11.35 | (127) rat_$sum(all_25_0, rat_5/2) = all_69_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (94) with fresh symbol all_71_0 gives: % 80.83/11.35 | (128) rat_$sum(all_25_0, rat_15/8) = all_71_0 & rat_$sum(rat_15/8, % 80.83/11.35 | all_71_0) = rat_15/8 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (128) implies: % 80.83/11.35 | (129) rat_$sum(rat_15/8, all_71_0) = rat_15/8 % 80.83/11.35 | (130) rat_$sum(all_25_0, rat_15/8) = all_71_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (100) with fresh symbol all_73_0 gives: % 80.83/11.35 | (131) rat_$sum(rat_5/8, all_73_0) = rat_0 & rat_$sum(rat_0, all_31_0) = % 80.83/11.35 | all_73_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (131) implies: % 80.83/11.35 | (132) rat_$sum(rat_0, all_31_0) = all_73_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (101) with fresh symbol all_75_0 gives: % 80.83/11.35 | (133) rat_$sum(all_75_0, all_31_0) = rat_5/2 & rat_$sum(rat_5/2, rat_5/8) = % 80.83/11.35 | all_75_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (133) implies: % 80.83/11.35 | (134) rat_$sum(all_75_0, all_31_0) = rat_5/2 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (104) with fresh symbol all_77_0 gives: % 80.83/11.35 | (135) rat_$sum(all_31_0, rat_5/2) = all_77_0 & rat_$sum(rat_5/8, all_77_0) % 80.83/11.35 | = rat_5/2 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (135) implies: % 80.83/11.35 | (136) rat_$sum(rat_5/8, all_77_0) = rat_5/2 % 80.83/11.35 | (137) rat_$sum(all_31_0, rat_5/2) = all_77_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (103) with fresh symbol all_79_0 gives: % 80.83/11.35 | (138) rat_$sum(all_31_0, rat_15/8) = all_79_0 & rat_$sum(rat_5/8, all_79_0) % 80.83/11.35 | = rat_15/8 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (138) implies: % 80.83/11.35 | (139) rat_$sum(all_31_0, rat_15/8) = all_79_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (64) with fresh symbol all_83_0 gives: % 80.83/11.35 | (140) rat_$sum(rat_5/8, all_23_0) = all_83_0 & rat_$sum(rat_15/8, all_83_0) % 80.83/11.35 | = rat_15/8 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (140) implies: % 80.83/11.35 | (141) rat_$sum(rat_15/8, all_83_0) = rat_15/8 % 80.83/11.35 | (142) rat_$sum(rat_5/8, all_23_0) = all_83_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (63) with fresh symbol all_91_0 gives: % 80.83/11.35 | (143) rat_$sum(all_91_0, all_23_0) = rat_5/2 & rat_$sum(rat_5/8, rat_5/2) = % 80.83/11.35 | all_91_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (143) implies: % 80.83/11.35 | (144) rat_$sum(rat_5/8, rat_5/2) = all_91_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (62) with fresh symbol all_93_0 gives: % 80.83/11.35 | (145) rat_$sum(rat_5/8, all_93_0) = rat_15/8 & rat_$sum(rat_15/8, all_23_0) % 80.83/11.35 | = all_93_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (145) implies: % 80.83/11.35 | (146) rat_$sum(rat_15/8, all_23_0) = all_93_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (97) with fresh symbol all_95_0 gives: % 80.83/11.35 | (147) rat_$sum(all_31_0, all_25_0) = all_95_0 & rat_$sum(rat_5/2, all_95_0) % 80.83/11.35 | = rat_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (147) implies: % 80.83/11.35 | (148) rat_$sum(rat_5/2, all_95_0) = rat_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (96) with fresh symbol all_97_0 gives: % 80.83/11.35 | (149) rat_$sum(all_25_0, rat_0) = all_97_0 & rat_$sum(rat_15/8, all_97_0) = % 80.83/11.35 | rat_0 % 80.83/11.35 | % 80.83/11.35 | ALPHA: (149) implies: % 80.83/11.35 | (150) rat_$sum(rat_15/8, all_97_0) = rat_0 % 80.83/11.35 | (151) rat_$sum(all_25_0, rat_0) = all_97_0 % 80.83/11.35 | % 80.83/11.35 | DELTA: instantiating (93) with fresh symbol all_99_0 gives: % 80.83/11.35 | (152) rat_$sum(all_25_0, rat_5/8) = all_99_0 & rat_$sum(rat_15/8, all_99_0) % 80.83/11.35 | = rat_5/8 % 80.83/11.35 | % 80.83/11.36 | ALPHA: (152) implies: % 80.83/11.36 | (153) rat_$sum(rat_15/8, all_99_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (92) with fresh symbol all_101_0 gives: % 80.83/11.36 | (154) rat_$sum(all_101_0, all_25_0) = rat_5/2 & rat_$sum(rat_5/2, rat_15/8) % 80.83/11.36 | = all_101_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (154) implies: % 80.83/11.36 | (155) rat_$sum(rat_5/2, rat_15/8) = all_101_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (80) with fresh symbol all_103_0 gives: % 80.83/11.36 | (156) rat_$sum(all_27_0, rat_5/8) = all_103_0 & rat_$sum(rat_5/2, % 80.83/11.36 | all_103_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (156) implies: % 80.83/11.36 | (157) rat_$sum(all_27_0, rat_5/8) = all_103_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (78) with fresh symbol all_105_0 gives: % 80.83/11.36 | (158) rat_$sum(rat_5/2, all_105_0) = rat_0 & rat_$sum(rat_0, all_27_0) = % 80.83/11.36 | all_105_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (158) implies: % 80.83/11.36 | (159) rat_$sum(rat_0, all_27_0) = all_105_0 % 80.83/11.36 | (160) rat_$sum(rat_5/2, all_105_0) = rat_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (79) with fresh symbol all_107_0 gives: % 80.83/11.36 | (161) rat_$sum(all_107_0, all_27_0) = rat_5/2 & rat_$sum(rat_5/2, rat_5/2) % 80.83/11.36 | = all_107_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (161) implies: % 80.83/11.36 | (162) rat_$sum(rat_5/2, rat_5/2) = all_107_0 % 80.83/11.36 | (163) rat_$sum(all_107_0, all_27_0) = rat_5/2 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (76) with fresh symbol all_109_0 gives: % 80.83/11.36 | (164) rat_$sum(rat_5/8, all_27_0) = all_109_0 & rat_$sum(rat_15/8, % 80.83/11.36 | all_109_0) = rat_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (164) implies: % 80.83/11.36 | (165) rat_$sum(rat_15/8, all_109_0) = rat_0 % 80.83/11.36 | (166) rat_$sum(rat_5/8, all_27_0) = all_109_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (66) with fresh symbol all_111_0 gives: % 80.83/11.36 | (167) rat_$sum(rat_5/2, all_111_0) = rat_15/8 & rat_$sum(rat_0, all_23_0) = % 80.83/11.36 | all_111_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (167) implies: % 80.83/11.36 | (168) rat_$sum(rat_0, all_23_0) = all_111_0 % 80.83/11.36 | (169) rat_$sum(rat_5/2, all_111_0) = rat_15/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (75) with fresh symbol all_113_0 gives: % 80.83/11.36 | (170) rat_$sum(all_113_0, all_27_0) = rat_5/8 & rat_$sum(rat_5/8, rat_5/2) % 80.83/11.36 | = all_113_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (170) implies: % 80.83/11.36 | (171) rat_$sum(rat_5/8, rat_5/2) = all_113_0 % 80.83/11.36 | (172) rat_$sum(all_113_0, all_27_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (65) with fresh symbol all_125_0 gives: % 80.83/11.36 | (173) rat_$sum(all_23_0, rat_0) = all_125_0 & rat_$sum(rat_5/2, all_125_0) % 80.83/11.36 | = rat_15/8 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (173) implies: % 80.83/11.36 | (174) rat_$sum(rat_5/2, all_125_0) = rat_15/8 % 80.83/11.36 | (175) rat_$sum(all_23_0, rat_0) = all_125_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (77) with fresh symbol all_127_0 gives: % 80.83/11.36 | (176) rat_$sum(all_127_0, all_27_0) = rat_15/8 & rat_$sum(rat_15/8, % 80.83/11.36 | rat_5/2) = all_127_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (176) implies: % 80.83/11.36 | (177) rat_$sum(rat_15/8, rat_5/2) = all_127_0 % 80.83/11.36 | (178) rat_$sum(all_127_0, all_27_0) = rat_15/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (88) with fresh symbol all_129_0 gives: % 80.83/11.36 | (179) rat_$sum(rat_5/2, all_129_0) = rat_15/8 & rat_$sum(rat_0, all_31_0) = % 80.83/11.36 | all_129_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (179) implies: % 80.83/11.36 | (180) rat_$sum(rat_0, all_31_0) = all_129_0 % 80.83/11.36 | (181) rat_$sum(rat_5/2, all_129_0) = rat_15/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (74) with fresh symbol all_131_0 gives: % 80.83/11.36 | (182) rat_$sum(rat_5/8, all_131_0) = rat_0 & rat_$sum(rat_15/8, all_27_0) = % 80.83/11.36 | all_131_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (182) implies: % 80.83/11.36 | (183) rat_$sum(rat_15/8, all_27_0) = all_131_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (72) with fresh symbol all_133_0 gives: % 80.83/11.36 | (184) rat_$sum(rat_5/2, all_133_0) = rat_5/8 & rat_$sum(rat_0, all_25_0) = % 80.83/11.36 | all_133_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (184) implies: % 80.83/11.36 | (185) rat_$sum(rat_0, all_25_0) = all_133_0 % 80.83/11.36 | (186) rat_$sum(rat_5/2, all_133_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (70) with fresh symbol all_135_0 gives: % 80.83/11.36 | (187) rat_$sum(rat_5/8, all_25_0) = all_135_0 & rat_$sum(rat_15/8, % 80.83/11.36 | all_135_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (187) implies: % 80.83/11.36 | (188) rat_$sum(rat_15/8, all_135_0) = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (91) with fresh symbol all_137_0 gives: % 80.83/11.36 | (189) rat_$sum(all_137_0, all_25_0) = rat_15/8 & rat_$sum(rat_15/8, % 80.83/11.36 | rat_15/8) = all_137_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (189) implies: % 80.83/11.36 | (190) rat_$sum(rat_15/8, rat_15/8) = all_137_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (90) with fresh symbol all_139_0 gives: % 80.83/11.36 | (191) rat_$sum(rat_15/8, all_139_0) = rat_0 & rat_$sum(rat_0, all_25_0) = % 80.83/11.36 | all_139_0 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (191) implies: % 80.83/11.36 | (192) rat_$sum(rat_0, all_25_0) = all_139_0 % 80.83/11.36 | (193) rat_$sum(rat_15/8, all_139_0) = rat_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (82) with fresh symbol all_141_0 gives: % 80.83/11.36 | (194) rat_$sum(all_27_0, rat_5/2) = all_141_0 & rat_$sum(rat_5/2, % 80.83/11.36 | all_141_0) = rat_5/2 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (194) implies: % 80.83/11.36 | (195) rat_$sum(all_27_0, rat_5/2) = all_141_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (69) with fresh symbol all_143_0 gives: % 80.83/11.36 | (196) rat_$sum(all_25_0, rat_0) = all_143_0 & rat_$sum(rat_5/2, all_143_0) % 80.83/11.36 | = rat_5/8 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (196) implies: % 80.83/11.36 | (197) rat_$sum(all_25_0, rat_0) = all_143_0 % 80.83/11.36 | % 80.83/11.36 | DELTA: instantiating (81) with fresh symbol all_145_0 gives: % 80.83/11.36 | (198) rat_$sum(all_27_0, rat_15/8) = all_145_0 & rat_$sum(rat_5/2, % 80.83/11.36 | all_145_0) = rat_15/8 % 80.83/11.36 | % 80.83/11.36 | ALPHA: (198) implies: % 80.83/11.37 | (199) rat_$sum(rat_5/2, all_145_0) = rat_15/8 % 80.83/11.37 | (200) rat_$sum(all_27_0, rat_15/8) = all_145_0 % 80.83/11.37 | % 80.83/11.37 | DELTA: instantiating (71) with fresh symbol all_147_0 gives: % 80.83/11.37 | (201) rat_$sum(all_147_0, all_25_0) = rat_5/2 & rat_$sum(rat_15/8, rat_5/2) % 80.83/11.37 | = all_147_0 % 80.83/11.37 | % 80.83/11.37 | ALPHA: (201) implies: % 80.83/11.37 | (202) rat_$sum(rat_15/8, rat_5/2) = all_147_0 % 80.83/11.37 | % 80.83/11.37 | DELTA: instantiating (87) with fresh symbol all_149_0 gives: % 80.83/11.37 | (203) rat_$sum(all_31_0, rat_0) = all_149_0 & rat_$sum(rat_5/2, all_149_0) % 80.83/11.37 | = rat_15/8 % 80.83/11.37 | % 80.83/11.37 | ALPHA: (203) implies: % 80.83/11.37 | (204) rat_$sum(all_31_0, rat_0) = all_149_0 % 80.83/11.37 | % 80.83/11.37 | DELTA: instantiating (85) with fresh symbol all_151_0 gives: % 80.83/11.37 | (205) rat_$sum(all_151_0, all_31_0) = rat_5/2 & rat_$sum(rat_5/8, rat_5/2) % 80.83/11.37 | = all_151_0 % 80.83/11.37 | % 80.83/11.37 | ALPHA: (205) implies: % 80.83/11.37 | (206) rat_$sum(rat_5/8, rat_5/2) = all_151_0 % 80.83/11.37 | % 80.83/11.37 | DELTA: instantiating (86) with fresh symbol all_155_0 gives: % 80.83/11.37 | (207) rat_$sum(all_31_0, rat_5/8) = all_155_0 & rat_$sum(rat_5/2, % 80.83/11.37 | all_155_0) = rat_5/2 % 80.83/11.37 | % 80.83/11.37 | ALPHA: (207) implies: % 80.83/11.37 | (208) rat_$sum(all_31_0, rat_5/8) = all_155_0 % 80.83/11.37 | % 80.83/11.37 | BETA: splitting (61) gives: % 80.83/11.37 | % 80.83/11.37 | Case 1: % 80.83/11.37 | | % 80.83/11.37 | | (209) all_41_0 = 0 % 80.83/11.37 | | % 80.83/11.37 | | REDUCE: (55), (209) imply: % 80.83/11.37 | | (210) $false % 81.11/11.37 | | % 81.11/11.37 | | CLOSE: (210) is inconsistent. % 81.11/11.37 | | % 81.11/11.37 | Case 2: % 81.11/11.37 | | % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_133_0, all_139_0, all_25_0, rat_0, % 81.11/11.37 | | simplifying with (185), (192) gives: % 81.11/11.37 | | (211) all_139_0 = all_133_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_73_0, all_129_0, all_31_0, rat_0, % 81.11/11.37 | | simplifying with (132), (180) gives: % 81.11/11.37 | | (212) all_129_0 = all_73_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_127_0, all_147_0, rat_5/2, rat_15/8, % 81.11/11.37 | | simplifying with (177), (202) gives: % 81.11/11.37 | | (213) all_147_0 = all_127_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_113_0, all_151_0, rat_5/2, rat_5/8, % 81.11/11.37 | | simplifying with (171), (206) gives: % 81.11/11.37 | | (214) all_151_0 = all_113_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_91_0, all_151_0, rat_5/2, rat_5/8, % 81.11/11.37 | | simplifying with (144), (206) gives: % 81.11/11.37 | | (215) all_151_0 = all_91_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (20) with all_23_0, all_125_0, simplifying with % 81.11/11.37 | | (175) gives: % 81.11/11.37 | | (216) all_125_0 = all_23_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_97_0, all_143_0, rat_0, all_25_0, % 81.11/11.37 | | simplifying with (151), (197) gives: % 81.11/11.37 | | (217) all_143_0 = all_97_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (20) with all_25_0, all_143_0, simplifying with % 81.11/11.37 | | (197) gives: % 81.11/11.37 | | (218) all_143_0 = all_25_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with rat_5/8, all_69_0, rat_5/2, all_25_0, % 81.11/11.37 | | simplifying with (73), (127) gives: % 81.11/11.37 | | (219) all_69_0 = rat_5/8 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with all_59_0, all_71_0, rat_15/8, all_25_0, % 81.11/11.37 | | simplifying with (117), (130) gives: % 81.11/11.37 | | (220) all_71_0 = all_59_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (2) with rat_0, all_71_0, rat_15/8, all_25_0, % 81.11/11.37 | | simplifying with (99), (130) gives: % 81.11/11.37 | | (221) all_71_0 = rat_0 % 81.11/11.37 | | % 81.11/11.37 | | GROUND_INST: instantiating (20) with all_27_0, all_55_0, simplifying with % 81.11/11.37 | | (112) gives: % 81.11/11.37 | | (222) all_55_0 = all_27_0 % 81.11/11.37 | | % 81.11/11.38 | | GROUND_INST: instantiating (2) with rat_0, all_141_0, rat_5/2, all_27_0, % 81.11/11.38 | | simplifying with (84), (195) gives: % 81.11/11.38 | | (223) all_141_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (2) with all_63_0, all_149_0, rat_0, all_31_0, % 81.11/11.38 | | simplifying with (121), (204) gives: % 81.11/11.38 | | (224) all_149_0 = all_63_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (20) with all_31_0, all_149_0, simplifying with % 81.11/11.38 | | (204) gives: % 81.11/11.38 | | (225) all_149_0 = all_31_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (2) with rat_15/8, all_77_0, rat_5/2, all_31_0, % 81.11/11.38 | | simplifying with (89), (137) gives: % 81.11/11.38 | | (226) all_77_0 = rat_15/8 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (2) with all_65_0, all_155_0, rat_5/8, all_31_0, % 81.11/11.38 | | simplifying with (124), (208) gives: % 81.11/11.38 | | (227) all_155_0 = all_65_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (2) with rat_0, all_155_0, rat_5/8, all_31_0, % 81.11/11.38 | | simplifying with (107), (208) gives: % 81.11/11.38 | | (228) all_155_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | COMBINE_EQS: (227), (228) imply: % 81.11/11.38 | | (229) all_65_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | SIMP: (229) implies: % 81.11/11.38 | | (230) all_65_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | COMBINE_EQS: (214), (215) imply: % 81.11/11.38 | | (231) all_113_0 = all_91_0 % 81.11/11.38 | | % 81.11/11.38 | | COMBINE_EQS: (224), (225) imply: % 81.11/11.38 | | (232) all_63_0 = all_31_0 % 81.11/11.38 | | % 81.11/11.38 | | SIMP: (232) implies: % 81.11/11.38 | | (233) all_63_0 = all_31_0 % 81.11/11.38 | | % 81.11/11.38 | | COMBINE_EQS: (217), (218) imply: % 81.11/11.38 | | (234) all_97_0 = all_25_0 % 81.11/11.38 | | % 81.11/11.38 | | SIMP: (234) implies: % 81.11/11.38 | | (235) all_97_0 = all_25_0 % 81.11/11.38 | | % 81.11/11.38 | | COMBINE_EQS: (220), (221) imply: % 81.11/11.38 | | (236) all_59_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | SIMP: (236) implies: % 81.11/11.38 | | (237) all_59_0 = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (172), (231) imply: % 81.11/11.38 | | (238) rat_$sum(all_91_0, all_27_0) = rat_5/8 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (121), (233) imply: % 81.11/11.38 | | (239) rat_$sum(all_31_0, rat_0) = all_31_0 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (112), (222) imply: % 81.11/11.38 | | (240) rat_$sum(all_27_0, rat_0) = all_27_0 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (175), (216) imply: % 81.11/11.38 | | (241) rat_$sum(all_23_0, rat_0) = all_23_0 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (193), (211) imply: % 81.11/11.38 | | (242) rat_$sum(rat_15/8, all_133_0) = rat_0 % 81.11/11.38 | | % 81.11/11.38 | | REDUCE: (181), (212) imply: % 81.11/11.38 | | (243) rat_$sum(rat_5/2, all_73_0) = rat_15/8 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_23_0, rat_0, rat_0, rat_0, % 81.11/11.38 | | all_111_0, simplifying with (10), (168) gives: % 81.11/11.38 | | (244) ? [v0: $rat] : (rat_$sum(rat_0, v0) = all_111_0 & rat_$sum(rat_0, % 81.11/11.38 | | all_23_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_27_0, rat_0, rat_0, rat_0, % 81.11/11.38 | | all_105_0, simplifying with (10), (159) gives: % 81.11/11.38 | | (245) ? [v0: $rat] : (rat_$sum(rat_0, v0) = all_105_0 & rat_$sum(rat_0, % 81.11/11.38 | | all_27_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_105_0, rat_15/8, rat_5/8, rat_5/2, % 81.11/11.38 | | rat_0, simplifying with (18), (160) gives: % 81.11/11.38 | | (246) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = rat_0 & rat_$sum(rat_15/8, % 81.11/11.38 | | all_105_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_111_0, rat_0, rat_5/2, rat_5/2, % 81.11/11.38 | | rat_15/8, simplifying with (14), (169) gives: % 81.11/11.38 | | (247) ? [v0: $rat] : (rat_$sum(rat_5/2, v0) = rat_15/8 & rat_$sum(rat_0, % 81.11/11.38 | | all_111_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_23_0, rat_0, rat_15/8, rat_15/8, % 81.11/11.38 | | all_93_0, simplifying with (15), (146) gives: % 81.11/11.38 | | (248) ? [v0: $rat] : (rat_$sum(rat_15/8, v0) = all_93_0 & % 81.11/11.38 | | rat_$sum(rat_0, all_23_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_27_0, rat_0, rat_15/8, rat_15/8, % 81.11/11.38 | | all_131_0, simplifying with (15), (183) gives: % 81.11/11.38 | | (249) ? [v0: $rat] : (rat_$sum(rat_15/8, v0) = all_131_0 & % 81.11/11.38 | | rat_$sum(rat_0, all_27_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (22) with all_27_0, rat_15/8, all_131_0, % 81.11/11.38 | | simplifying with (183) gives: % 81.11/11.38 | | (250) rat_$sum(all_27_0, rat_15/8) = all_131_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_23_0, rat_0, rat_5/8, rat_5/8, % 81.11/11.38 | | all_83_0, simplifying with (17), (142) gives: % 81.11/11.38 | | (251) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = all_83_0 & rat_$sum(rat_0, % 81.11/11.38 | | all_23_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (26) with all_27_0, rat_0, rat_5/8, rat_5/8, % 81.11/11.38 | | all_109_0, simplifying with (17), (166) gives: % 81.11/11.38 | | (252) ? [v0: $rat] : (rat_$sum(rat_5/8, v0) = all_109_0 & % 81.11/11.38 | | rat_$sum(rat_0, all_27_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (25) with rat_0, all_23_0, rat_0, all_23_0, % 81.11/11.38 | | all_111_0, simplifying with (168), (241) gives: % 81.11/11.38 | | (253) ? [v0: $rat] : (rat_$sum(v0, rat_0) = all_111_0 & rat_$sum(rat_0, % 81.11/11.38 | | all_23_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (22) with rat_0, all_23_0, all_23_0, simplifying % 81.11/11.38 | | with (241) gives: % 81.11/11.38 | | (254) rat_$sum(rat_0, all_23_0) = all_23_0 % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (25) with rat_5/2, all_23_0, rat_0, rat_15/8, % 81.11/11.38 | | rat_15/8, simplifying with (12), (67) gives: % 81.11/11.38 | | (255) ? [v0: $rat] : (rat_$sum(v0, rat_5/2) = rat_15/8 & rat_$sum(rat_0, % 81.11/11.38 | | all_23_0) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (25) with all_25_0, rat_15/8, all_27_0, rat_0, % 81.11/11.38 | | all_27_0, simplifying with (59), (240) gives: % 81.11/11.38 | | (256) ? [v0: $rat] : (rat_$sum(v0, all_25_0) = all_27_0 & % 81.11/11.38 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (25) with all_27_0, rat_5/2, all_27_0, rat_0, % 81.11/11.38 | | all_27_0, simplifying with (44), (240) gives: % 81.11/11.38 | | (257) ? [v0: $rat] : (rat_$sum(v0, all_27_0) = all_27_0 & % 81.11/11.38 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.38 | | % 81.11/11.38 | | GROUND_INST: instantiating (25) with all_133_0, rat_15/8, all_27_0, rat_0, % 81.11/11.38 | | all_27_0, simplifying with (240), (242) gives: % 81.11/11.38 | | (258) ? [v0: $rat] : (rat_$sum(v0, all_133_0) = all_27_0 & % 81.11/11.38 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.38 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_109_0, rat_15/8, all_27_0, rat_0, % 81.11/11.39 | | all_27_0, simplifying with (165), (240) gives: % 81.11/11.39 | | (259) ? [v0: $rat] : (rat_$sum(v0, all_109_0) = all_27_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_105_0, rat_5/2, all_27_0, rat_0, % 81.11/11.39 | | all_27_0, simplifying with (160), (240) gives: % 81.11/11.39 | | (260) ? [v0: $rat] : (rat_$sum(v0, all_105_0) = all_27_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_61_0, rat_5/2, all_27_0, rat_0, % 81.11/11.39 | | all_27_0, simplifying with (119), (240) gives: % 81.11/11.39 | | (261) ? [v0: $rat] : (rat_$sum(v0, all_61_0) = all_27_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_57_0, rat_5/2, all_27_0, rat_0, % 81.11/11.39 | | all_27_0, simplifying with (114), (240) gives: % 81.11/11.39 | | (262) ? [v0: $rat] : (rat_$sum(v0, all_57_0) = all_27_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with rat_0, all_27_0, rat_0, all_27_0, % 81.11/11.39 | | all_105_0, simplifying with (159), (240) gives: % 81.11/11.39 | | (263) ? [v0: $rat] : (rat_$sum(v0, rat_0) = all_105_0 & rat_$sum(rat_0, % 81.11/11.39 | | all_27_0) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (22) with rat_0, all_27_0, all_27_0, simplifying % 81.11/11.39 | | with (240) gives: % 81.11/11.39 | | (264) rat_$sum(rat_0, all_27_0) = all_27_0 % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with rat_5/8, rat_15/8, all_27_0, rat_5/2, % 81.11/11.39 | | rat_0, simplifying with (16), (84) gives: % 81.11/11.39 | | (265) ? [v0: $rat] : (rat_$sum(v0, rat_5/8) = rat_0 & rat_$sum(all_27_0, % 81.11/11.39 | | rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with rat_5/2, all_27_0, rat_0, rat_0, rat_0, % 81.11/11.39 | | simplifying with (10), (84) gives: % 81.11/11.39 | | (266) ? [v0: $rat] : (rat_$sum(v0, rat_5/2) = rat_0 & rat_$sum(rat_0, % 81.11/11.39 | | all_27_0) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with rat_0, rat_15/8, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (15), (200) gives: % 81.11/11.39 | | (267) ? [v0: $rat] : (rat_$sum(v0, rat_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_23_0, rat_5/2, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (38), (200) gives: % 81.11/11.39 | | (268) ? [v0: $rat] : (rat_$sum(v0, all_23_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_83_0, rat_15/8, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (141), (200) gives: % 81.11/11.39 | | (269) ? [v0: $rat] : (rat_$sum(v0, all_83_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_145_0, rat_5/2, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (199), (200) gives: % 81.11/11.39 | | (270) ? [v0: $rat] : (rat_$sum(v0, all_145_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_111_0, rat_5/2, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (169), (200) gives: % 81.11/11.39 | | (271) ? [v0: $rat] : (rat_$sum(v0, all_111_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_73_0, rat_5/2, all_27_0, rat_15/8, % 81.11/11.39 | | all_145_0, simplifying with (200), (243) gives: % 81.11/11.39 | | (272) ? [v0: $rat] : (rat_$sum(v0, all_73_0) = all_145_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (22) with rat_15/8, all_27_0, all_145_0, % 81.11/11.39 | | simplifying with (200) gives: % 81.11/11.39 | | (273) rat_$sum(rat_15/8, all_27_0) = all_145_0 % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_135_0, rat_15/8, all_27_0, rat_5/8, % 81.11/11.39 | | all_103_0, simplifying with (157), (188) gives: % 81.11/11.39 | | (274) ? [v0: $rat] : (rat_$sum(v0, all_135_0) = all_103_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_99_0, rat_15/8, all_27_0, rat_5/8, % 81.11/11.39 | | all_103_0, simplifying with (153), (157) gives: % 81.11/11.39 | | (275) ? [v0: $rat] : (rat_$sum(v0, all_99_0) = all_103_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_133_0, rat_5/2, all_27_0, rat_5/8, % 81.11/11.39 | | all_103_0, simplifying with (157), (186) gives: % 81.11/11.39 | | (276) ? [v0: $rat] : (rat_$sum(v0, all_133_0) = all_103_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_27_0, rat_5/2, all_31_0, rat_0, % 81.11/11.39 | | all_31_0, simplifying with (44), (239) gives: % 81.11/11.39 | | (277) ? [v0: $rat] : (rat_$sum(v0, all_27_0) = all_31_0 & % 81.11/11.39 | | rat_$sum(all_31_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_95_0, rat_5/2, all_31_0, rat_0, % 81.11/11.39 | | all_31_0, simplifying with (148), (239) gives: % 81.11/11.39 | | (278) ? [v0: $rat] : (rat_$sum(v0, all_95_0) = all_31_0 & % 81.11/11.39 | | rat_$sum(all_31_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_57_0, rat_5/2, all_31_0, rat_0, % 81.11/11.39 | | all_31_0, simplifying with (114), (239) gives: % 81.11/11.39 | | (279) ? [v0: $rat] : (rat_$sum(v0, all_57_0) = all_31_0 & % 81.11/11.39 | | rat_$sum(all_31_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (25) with all_111_0, rat_5/2, all_31_0, rat_15/8, % 81.11/11.39 | | all_79_0, simplifying with (139), (169) gives: % 81.11/11.39 | | (280) ? [v0: $rat] : (rat_$sum(v0, all_111_0) = all_79_0 & % 81.11/11.39 | | rat_$sum(all_31_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_5/2, all_31_0, all_75_0, rat_5/2, % 81.11/11.39 | | all_107_0, simplifying with (134), (162) gives: % 81.11/11.39 | | (281) ? [v0: $rat] : (rat_$sum(all_75_0, v0) = all_107_0 & % 81.11/11.39 | | rat_$sum(all_31_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_15/8, all_27_0, all_91_0, rat_5/8, % 81.11/11.39 | | rat_5/2, simplifying with (18), (238) gives: % 81.11/11.39 | | (282) ? [v0: $rat] : (rat_$sum(all_91_0, v0) = rat_5/2 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_5/2, all_27_0, all_91_0, rat_5/8, % 81.11/11.39 | | all_91_0, simplifying with (144), (238) gives: % 81.11/11.39 | | (283) ? [v0: $rat] : (rat_$sum(all_91_0, v0) = all_91_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_15/8, all_27_0, all_107_0, rat_5/2, % 81.11/11.39 | | all_101_0, simplifying with (155), (163) gives: % 81.11/11.39 | | (284) ? [v0: $rat] : (rat_$sum(all_107_0, v0) = all_101_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_15/8, all_27_0, all_127_0, % 81.11/11.39 | | rat_15/8, all_137_0, simplifying with (178), (190) gives: % 81.11/11.39 | | (285) ? [v0: $rat] : (rat_$sum(all_127_0, v0) = all_137_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_15/8) = v0) % 81.11/11.39 | | % 81.11/11.39 | | GROUND_INST: instantiating (26) with rat_5/2, all_27_0, all_127_0, rat_15/8, % 81.11/11.39 | | all_127_0, simplifying with (177), (178) gives: % 81.11/11.39 | | (286) ? [v0: $rat] : (rat_$sum(all_127_0, v0) = all_127_0 & % 81.11/11.39 | | rat_$sum(all_27_0, rat_5/2) = v0) % 81.11/11.39 | | % 81.11/11.40 | | DELTA: instantiating (268) with fresh symbol all_256_0 gives: % 81.11/11.40 | | (287) rat_$sum(all_256_0, all_23_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_256_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (287) implies: % 81.11/11.40 | | (288) rat_$sum(all_27_0, rat_5/2) = all_256_0 % 81.11/11.40 | | (289) rat_$sum(all_256_0, all_23_0) = all_145_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (276) with fresh symbol all_296_0 gives: % 81.11/11.40 | | (290) rat_$sum(all_296_0, all_133_0) = all_103_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_296_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (290) implies: % 81.11/11.40 | | (291) rat_$sum(all_27_0, rat_5/2) = all_296_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (275) with fresh symbol all_298_0 gives: % 81.11/11.40 | | (292) rat_$sum(all_298_0, all_99_0) = all_103_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_298_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (292) implies: % 81.11/11.40 | | (293) rat_$sum(all_27_0, rat_15/8) = all_298_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (272) with fresh symbol all_304_0 gives: % 81.11/11.40 | | (294) rat_$sum(all_304_0, all_73_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_304_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (294) implies: % 81.11/11.40 | | (295) rat_$sum(all_27_0, rat_5/2) = all_304_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (271) with fresh symbol all_306_0 gives: % 81.11/11.40 | | (296) rat_$sum(all_306_0, all_111_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_306_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (296) implies: % 81.11/11.40 | | (297) rat_$sum(all_27_0, rat_5/2) = all_306_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (270) with fresh symbol all_308_0 gives: % 81.11/11.40 | | (298) rat_$sum(all_308_0, all_145_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_308_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (298) implies: % 81.11/11.40 | | (299) rat_$sum(all_27_0, rat_5/2) = all_308_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (269) with fresh symbol all_318_0 gives: % 81.11/11.40 | | (300) rat_$sum(all_318_0, all_83_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_318_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (300) implies: % 81.11/11.40 | | (301) rat_$sum(all_27_0, rat_15/8) = all_318_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (263) with fresh symbol all_340_0 gives: % 81.11/11.40 | | (302) rat_$sum(all_340_0, rat_0) = all_105_0 & rat_$sum(rat_0, all_27_0) % 81.11/11.40 | | = all_340_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (302) implies: % 81.11/11.40 | | (303) rat_$sum(rat_0, all_27_0) = all_340_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (262) with fresh symbol all_342_0 gives: % 81.11/11.40 | | (304) rat_$sum(all_342_0, all_57_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_342_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (304) implies: % 81.11/11.40 | | (305) rat_$sum(all_27_0, rat_5/2) = all_342_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (274) with fresh symbol all_352_0 gives: % 81.11/11.40 | | (306) rat_$sum(all_352_0, all_135_0) = all_103_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_352_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (306) implies: % 81.11/11.40 | | (307) rat_$sum(all_27_0, rat_15/8) = all_352_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (260) with fresh symbol all_364_0 gives: % 81.11/11.40 | | (308) rat_$sum(all_364_0, all_105_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_364_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (308) implies: % 81.11/11.40 | | (309) rat_$sum(all_27_0, rat_5/2) = all_364_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (259) with fresh symbol all_366_0 gives: % 81.11/11.40 | | (310) rat_$sum(all_366_0, all_109_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_366_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (310) implies: % 81.11/11.40 | | (311) rat_$sum(all_27_0, rat_15/8) = all_366_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (286) with fresh symbol all_484_0 gives: % 81.11/11.40 | | (312) rat_$sum(all_127_0, all_484_0) = all_127_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_484_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (312) implies: % 81.11/11.40 | | (313) rat_$sum(all_27_0, rat_5/2) = all_484_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (285) with fresh symbol all_490_0 gives: % 81.11/11.40 | | (314) rat_$sum(all_127_0, all_490_0) = all_137_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_490_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (314) implies: % 81.11/11.40 | | (315) rat_$sum(all_27_0, rat_15/8) = all_490_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (267) with fresh symbol all_504_0 gives: % 81.11/11.40 | | (316) rat_$sum(all_504_0, rat_0) = all_145_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_504_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (316) implies: % 81.11/11.40 | | (317) rat_$sum(all_27_0, rat_15/8) = all_504_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (283) with fresh symbol all_506_0 gives: % 81.11/11.40 | | (318) rat_$sum(all_91_0, all_506_0) = all_91_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_506_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (318) implies: % 81.11/11.40 | | (319) rat_$sum(all_27_0, rat_5/2) = all_506_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (261) with fresh symbol all_514_0 gives: % 81.11/11.40 | | (320) rat_$sum(all_514_0, all_61_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_514_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (320) implies: % 81.11/11.40 | | (321) rat_$sum(all_27_0, rat_5/2) = all_514_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (266) with fresh symbol all_518_0 gives: % 81.11/11.40 | | (322) rat_$sum(all_518_0, rat_5/2) = rat_0 & rat_$sum(rat_0, all_27_0) = % 81.11/11.40 | | all_518_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (322) implies: % 81.11/11.40 | | (323) rat_$sum(rat_0, all_27_0) = all_518_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (258) with fresh symbol all_546_0 gives: % 81.11/11.40 | | (324) rat_$sum(all_546_0, all_133_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_546_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (324) implies: % 81.11/11.40 | | (325) rat_$sum(all_27_0, rat_15/8) = all_546_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (280) with fresh symbol all_610_0 gives: % 81.11/11.40 | | (326) rat_$sum(all_610_0, all_111_0) = all_79_0 & rat_$sum(all_31_0, % 81.11/11.40 | | rat_5/2) = all_610_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (326) implies: % 81.11/11.40 | | (327) rat_$sum(all_31_0, rat_5/2) = all_610_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (257) with fresh symbol all_698_0 gives: % 81.11/11.40 | | (328) rat_$sum(all_698_0, all_27_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_5/2) = all_698_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (328) implies: % 81.11/11.40 | | (329) rat_$sum(all_27_0, rat_5/2) = all_698_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (256) with fresh symbol all_700_0 gives: % 81.11/11.40 | | (330) rat_$sum(all_700_0, all_25_0) = all_27_0 & rat_$sum(all_27_0, % 81.11/11.40 | | rat_15/8) = all_700_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (330) implies: % 81.11/11.40 | | (331) rat_$sum(all_27_0, rat_15/8) = all_700_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (265) with fresh symbol all_706_0 gives: % 81.11/11.40 | | (332) rat_$sum(all_706_0, rat_5/8) = rat_0 & rat_$sum(all_27_0, rat_15/8) % 81.11/11.40 | | = all_706_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (332) implies: % 81.11/11.40 | | (333) rat_$sum(all_27_0, rat_15/8) = all_706_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (279) with fresh symbol all_758_0 gives: % 81.11/11.40 | | (334) rat_$sum(all_758_0, all_57_0) = all_31_0 & rat_$sum(all_31_0, % 81.11/11.40 | | rat_5/2) = all_758_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (334) implies: % 81.11/11.40 | | (335) rat_$sum(all_31_0, rat_5/2) = all_758_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (277) with fresh symbol all_782_0 gives: % 81.11/11.40 | | (336) rat_$sum(all_782_0, all_27_0) = all_31_0 & rat_$sum(all_31_0, % 81.11/11.40 | | rat_5/2) = all_782_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (336) implies: % 81.11/11.40 | | (337) rat_$sum(all_31_0, rat_5/2) = all_782_0 % 81.11/11.40 | | (338) rat_$sum(all_782_0, all_27_0) = all_31_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (278) with fresh symbol all_934_0 gives: % 81.11/11.40 | | (339) rat_$sum(all_934_0, all_95_0) = all_31_0 & rat_$sum(all_31_0, % 81.11/11.40 | | rat_5/2) = all_934_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (339) implies: % 81.11/11.40 | | (340) rat_$sum(all_31_0, rat_5/2) = all_934_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (247) with fresh symbol all_948_0 gives: % 81.11/11.40 | | (341) rat_$sum(rat_5/2, all_948_0) = rat_15/8 & rat_$sum(rat_0, % 81.11/11.40 | | all_111_0) = all_948_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (341) implies: % 81.11/11.40 | | (342) rat_$sum(rat_0, all_111_0) = all_948_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (246) with fresh symbol all_960_0 gives: % 81.11/11.40 | | (343) rat_$sum(rat_5/8, all_960_0) = rat_0 & rat_$sum(rat_15/8, % 81.11/11.40 | | all_105_0) = all_960_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (343) implies: % 81.11/11.40 | | (344) rat_$sum(rat_15/8, all_105_0) = all_960_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (251) with fresh symbol all_1056_0 gives: % 81.11/11.40 | | (345) rat_$sum(rat_5/8, all_1056_0) = all_83_0 & rat_$sum(rat_0, % 81.11/11.40 | | all_23_0) = all_1056_0 % 81.11/11.40 | | % 81.11/11.40 | | ALPHA: (345) implies: % 81.11/11.40 | | (346) rat_$sum(rat_0, all_23_0) = all_1056_0 % 81.11/11.40 | | % 81.11/11.40 | | DELTA: instantiating (252) with fresh symbol all_1060_0 gives: % 81.11/11.41 | | (347) rat_$sum(rat_5/8, all_1060_0) = all_109_0 & rat_$sum(rat_0, % 81.11/11.41 | | all_27_0) = all_1060_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (347) implies: % 81.11/11.41 | | (348) rat_$sum(rat_0, all_27_0) = all_1060_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (281) with fresh symbol all_1108_0 gives: % 81.11/11.41 | | (349) rat_$sum(all_75_0, all_1108_0) = all_107_0 & rat_$sum(all_31_0, % 81.11/11.41 | | rat_5/2) = all_1108_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (349) implies: % 81.11/11.41 | | (350) rat_$sum(all_31_0, rat_5/2) = all_1108_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (284) with fresh symbol all_1130_0 gives: % 81.11/11.41 | | (351) rat_$sum(all_107_0, all_1130_0) = all_101_0 & rat_$sum(all_27_0, % 81.11/11.41 | | rat_15/8) = all_1130_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (351) implies: % 81.11/11.41 | | (352) rat_$sum(all_27_0, rat_15/8) = all_1130_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (253) with fresh symbol all_1316_0 gives: % 81.11/11.41 | | (353) rat_$sum(all_1316_0, rat_0) = all_111_0 & rat_$sum(rat_0, all_23_0) % 81.11/11.41 | | = all_1316_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (353) implies: % 81.11/11.41 | | (354) rat_$sum(rat_0, all_23_0) = all_1316_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (255) with fresh symbol all_1418_0 gives: % 81.11/11.41 | | (355) rat_$sum(all_1418_0, rat_5/2) = rat_15/8 & rat_$sum(rat_0, % 81.11/11.41 | | all_23_0) = all_1418_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (355) implies: % 81.11/11.41 | | (356) rat_$sum(rat_0, all_23_0) = all_1418_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (249) with fresh symbol all_1462_0 gives: % 81.11/11.41 | | (357) rat_$sum(rat_15/8, all_1462_0) = all_131_0 & rat_$sum(rat_0, % 81.11/11.41 | | all_27_0) = all_1462_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (357) implies: % 81.11/11.41 | | (358) rat_$sum(rat_0, all_27_0) = all_1462_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (244) with fresh symbol all_1508_0 gives: % 81.11/11.41 | | (359) rat_$sum(rat_0, all_1508_0) = all_111_0 & rat_$sum(rat_0, all_23_0) % 81.11/11.41 | | = all_1508_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (359) implies: % 81.11/11.41 | | (360) rat_$sum(rat_0, all_23_0) = all_1508_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (248) with fresh symbol all_1532_0 gives: % 81.11/11.41 | | (361) rat_$sum(rat_15/8, all_1532_0) = all_93_0 & rat_$sum(rat_0, % 81.11/11.41 | | all_23_0) = all_1532_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (361) implies: % 81.11/11.41 | | (362) rat_$sum(rat_0, all_23_0) = all_1532_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (245) with fresh symbol all_1560_0 gives: % 81.11/11.41 | | (363) rat_$sum(rat_0, all_1560_0) = all_105_0 & rat_$sum(rat_0, all_27_0) % 81.11/11.41 | | = all_1560_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (363) implies: % 81.11/11.41 | | (364) rat_$sum(rat_0, all_27_0) = all_1560_0 % 81.11/11.41 | | % 81.11/11.41 | | DELTA: instantiating (282) with fresh symbol all_1914_0 gives: % 81.11/11.41 | | (365) rat_$sum(all_91_0, all_1914_0) = rat_5/2 & rat_$sum(all_27_0, % 81.11/11.41 | | rat_15/8) = all_1914_0 % 81.11/11.41 | | % 81.11/11.41 | | ALPHA: (365) implies: % 81.11/11.41 | | (366) rat_$sum(all_27_0, rat_15/8) = all_1914_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_111_0, all_1418_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (168), (356) gives: % 81.11/11.41 | | (367) all_1418_0 = all_111_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1056_0, all_1418_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (346), (356) gives: % 81.11/11.41 | | (368) all_1418_0 = all_1056_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_23_0, all_1508_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (254), (360) gives: % 81.11/11.41 | | (369) all_1508_0 = all_23_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1508_0, all_1532_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (360), (362) gives: % 81.11/11.41 | | (370) all_1532_0 = all_1508_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1316_0, all_1532_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (354), (362) gives: % 81.11/11.41 | | (371) all_1532_0 = all_1316_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1056_0, all_1532_0, all_23_0, rat_0, % 81.11/11.41 | | simplifying with (346), (362) gives: % 81.11/11.41 | | (372) all_1532_0 = all_1056_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_105_0, all_518_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (159), (323) gives: % 81.11/11.41 | | (373) all_518_0 = all_105_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_518_0, all_1060_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (323), (348) gives: % 81.11/11.41 | | (374) all_1060_0 = all_518_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_27_0, all_1060_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (264), (348) gives: % 81.11/11.41 | | (375) all_1060_0 = all_27_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1060_0, all_1462_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (348), (358) gives: % 81.11/11.41 | | (376) all_1462_0 = all_1060_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_1462_0, all_1560_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (358), (364) gives: % 81.11/11.41 | | (377) all_1560_0 = all_1462_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_340_0, all_1560_0, all_27_0, rat_0, % 81.11/11.41 | | simplifying with (303), (364) gives: % 81.11/11.41 | | (378) all_1560_0 = all_340_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_306_0, all_308_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (297), (299) gives: % 81.11/11.41 | | (379) all_308_0 = all_306_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_304_0, all_308_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (295), (299) gives: % 81.11/11.41 | | (380) all_308_0 = all_304_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_296_0, all_308_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (291), (299) gives: % 81.11/11.41 | | (381) all_308_0 = all_296_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_306_0, all_364_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (297), (309) gives: % 81.11/11.41 | | (382) all_364_0 = all_306_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with rat_0, all_484_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (84), (313) gives: % 81.11/11.41 | | (383) all_484_0 = rat_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_364_0, all_484_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (309), (313) gives: % 81.11/11.41 | | (384) all_484_0 = all_364_0 % 81.11/11.41 | | % 81.11/11.41 | | GROUND_INST: instantiating (2) with all_506_0, all_514_0, rat_5/2, all_27_0, % 81.11/11.41 | | simplifying with (319), (321) gives: % 81.11/11.41 | | (385) all_514_0 = all_506_0 % 81.11/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_256_0, all_514_0, rat_5/2, all_27_0, % 81.59/11.41 | | simplifying with (288), (321) gives: % 81.59/11.41 | | (386) all_514_0 = all_256_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_506_0, all_698_0, rat_5/2, all_27_0, % 81.59/11.41 | | simplifying with (319), (329) gives: % 81.59/11.41 | | (387) all_698_0 = all_506_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_342_0, all_698_0, rat_5/2, all_27_0, % 81.59/11.41 | | simplifying with (305), (329) gives: % 81.59/11.41 | | (388) all_698_0 = all_342_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_296_0, all_698_0, rat_5/2, all_27_0, % 81.59/11.41 | | simplifying with (291), (329) gives: % 81.59/11.41 | | (389) all_698_0 = all_296_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_298_0, all_318_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (293), (301) gives: % 81.59/11.41 | | (390) all_318_0 = all_298_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_318_0, all_366_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (301), (311) gives: % 81.59/11.41 | | (391) all_366_0 = all_318_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_145_0, all_490_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (200), (315) gives: % 81.59/11.41 | | (392) all_490_0 = all_145_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_318_0, all_490_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (301), (315) gives: % 81.59/11.41 | | (393) all_490_0 = all_318_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_366_0, all_546_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (311), (325) gives: % 81.59/11.41 | | (394) all_546_0 = all_366_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_546_0, all_700_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (325), (331) gives: % 81.59/11.41 | | (395) all_700_0 = all_546_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_700_0, all_1130_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (331), (352) gives: % 81.59/11.41 | | (396) all_1130_0 = all_700_0 % 81.59/11.41 | | % 81.59/11.41 | | GROUND_INST: instantiating (2) with all_131_0, all_1130_0, rat_15/8, % 81.59/11.41 | | all_27_0, simplifying with (250), (352) gives: % 81.59/11.42 | | (397) all_1130_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_706_0, all_1914_0, rat_15/8, % 81.59/11.42 | | all_27_0, simplifying with (333), (366) gives: % 81.59/11.42 | | (398) all_1914_0 = all_706_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_504_0, all_1914_0, rat_15/8, % 81.59/11.42 | | all_27_0, simplifying with (317), (366) gives: % 81.59/11.42 | | (399) all_1914_0 = all_504_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_490_0, all_1914_0, rat_15/8, % 81.59/11.42 | | all_27_0, simplifying with (315), (366) gives: % 81.59/11.42 | | (400) all_1914_0 = all_490_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_352_0, all_1914_0, rat_15/8, % 81.59/11.42 | | all_27_0, simplifying with (307), (366) gives: % 81.59/11.42 | | (401) all_1914_0 = all_352_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with rat_15/8, all_758_0, rat_5/2, all_31_0, % 81.59/11.42 | | simplifying with (89), (335) gives: % 81.59/11.42 | | (402) all_758_0 = rat_15/8 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_758_0, all_782_0, rat_5/2, all_31_0, % 81.59/11.42 | | simplifying with (335), (337) gives: % 81.59/11.42 | | (403) all_782_0 = all_758_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_934_0, all_1108_0, rat_5/2, % 81.59/11.42 | | all_31_0, simplifying with (340), (350) gives: % 81.59/11.42 | | (404) all_1108_0 = all_934_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_782_0, all_1108_0, rat_5/2, % 81.59/11.42 | | all_31_0, simplifying with (337), (350) gives: % 81.59/11.42 | | (405) all_1108_0 = all_782_0 % 81.59/11.42 | | % 81.59/11.42 | | GROUND_INST: instantiating (2) with all_610_0, all_1108_0, rat_5/2, % 81.59/11.42 | | all_31_0, simplifying with (327), (350) gives: % 81.59/11.42 | | (406) all_1108_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (398), (400) imply: % 81.59/11.42 | | (407) all_706_0 = all_490_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (398), (399) imply: % 81.59/11.42 | | (408) all_706_0 = all_504_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (398), (401) imply: % 81.59/11.42 | | (409) all_706_0 = all_352_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (377), (378) imply: % 81.59/11.42 | | (410) all_1462_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (410) implies: % 81.59/11.42 | | (411) all_1462_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (370), (371) imply: % 81.59/11.42 | | (412) all_1508_0 = all_1316_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (412) implies: % 81.59/11.42 | | (413) all_1508_0 = all_1316_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (371), (372) imply: % 81.59/11.42 | | (414) all_1316_0 = all_1056_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (369), (413) imply: % 81.59/11.42 | | (415) all_1316_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (415) implies: % 81.59/11.42 | | (416) all_1316_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (376), (411) imply: % 81.59/11.42 | | (417) all_1060_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (417) implies: % 81.59/11.42 | | (418) all_1060_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (367), (368) imply: % 81.59/11.42 | | (419) all_1056_0 = all_111_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (419) implies: % 81.59/11.42 | | (420) all_1056_0 = all_111_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (414), (416) imply: % 81.59/11.42 | | (421) all_1056_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (421) implies: % 81.59/11.42 | | (422) all_1056_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (396), (397) imply: % 81.59/11.42 | | (423) all_700_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (423) implies: % 81.59/11.42 | | (424) all_700_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (404), (406) imply: % 81.59/11.42 | | (425) all_934_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (404), (405) imply: % 81.59/11.42 | | (426) all_934_0 = all_782_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (375), (418) imply: % 81.59/11.42 | | (427) all_340_0 = all_27_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (374), (418) imply: % 81.59/11.42 | | (428) all_518_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (428) implies: % 81.59/11.42 | | (429) all_518_0 = all_340_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (420), (422) imply: % 81.59/11.42 | | (430) all_111_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (430) implies: % 81.59/11.42 | | (431) all_111_0 = all_23_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (425), (426) imply: % 81.59/11.42 | | (432) all_782_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (432) implies: % 81.59/11.42 | | (433) all_782_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (403), (433) imply: % 81.59/11.42 | | (434) all_758_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (434) implies: % 81.59/11.42 | | (435) all_758_0 = all_610_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (402), (435) imply: % 81.59/11.42 | | (436) all_610_0 = rat_15/8 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (407), (408) imply: % 81.59/11.42 | | (437) all_504_0 = all_490_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (408), (409) imply: % 81.59/11.42 | | (438) all_504_0 = all_352_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (395), (424) imply: % 81.59/11.42 | | (439) all_546_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (439) implies: % 81.59/11.42 | | (440) all_546_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (388), (389) imply: % 81.59/11.42 | | (441) all_342_0 = all_296_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (387), (388) imply: % 81.59/11.42 | | (442) all_506_0 = all_342_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (442) implies: % 81.59/11.42 | | (443) all_506_0 = all_342_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (394), (440) imply: % 81.59/11.42 | | (444) all_366_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (444) implies: % 81.59/11.42 | | (445) all_366_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (373), (429) imply: % 81.59/11.42 | | (446) all_340_0 = all_105_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (446) implies: % 81.59/11.42 | | (447) all_340_0 = all_105_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (385), (386) imply: % 81.59/11.42 | | (448) all_506_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (448) implies: % 81.59/11.42 | | (449) all_506_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (443), (449) imply: % 81.59/11.42 | | (450) all_342_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (450) implies: % 81.59/11.42 | | (451) all_342_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (437), (438) imply: % 81.59/11.42 | | (452) all_490_0 = all_352_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (452) implies: % 81.59/11.42 | | (453) all_490_0 = all_352_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (392), (453) imply: % 81.59/11.42 | | (454) all_352_0 = all_145_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (393), (453) imply: % 81.59/11.42 | | (455) all_352_0 = all_318_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (383), (384) imply: % 81.59/11.42 | | (456) all_364_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (456) implies: % 81.59/11.42 | | (457) all_364_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (391), (445) imply: % 81.59/11.42 | | (458) all_318_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (458) implies: % 81.59/11.42 | | (459) all_318_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (382), (457) imply: % 81.59/11.42 | | (460) all_306_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (460) implies: % 81.59/11.42 | | (461) all_306_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (454), (455) imply: % 81.59/11.42 | | (462) all_318_0 = all_145_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (462) implies: % 81.59/11.42 | | (463) all_318_0 = all_145_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (441), (451) imply: % 81.59/11.42 | | (464) all_296_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (464) implies: % 81.59/11.42 | | (465) all_296_0 = all_256_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (427), (447) imply: % 81.59/11.42 | | (466) all_105_0 = all_27_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (390), (463) imply: % 81.59/11.42 | | (467) all_298_0 = all_145_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (390), (459) imply: % 81.59/11.42 | | (468) all_298_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (379), (380) imply: % 81.59/11.42 | | (469) all_306_0 = all_304_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (469) implies: % 81.59/11.42 | | (470) all_306_0 = all_304_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (380), (381) imply: % 81.59/11.42 | | (471) all_304_0 = all_296_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (461), (470) imply: % 81.59/11.42 | | (472) all_304_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (472) implies: % 81.59/11.42 | | (473) all_304_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (471), (473) imply: % 81.59/11.42 | | (474) all_296_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (474) implies: % 81.59/11.42 | | (475) all_296_0 = rat_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (467), (468) imply: % 81.59/11.42 | | (476) all_145_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | SIMP: (476) implies: % 81.59/11.42 | | (477) all_145_0 = all_131_0 % 81.59/11.42 | | % 81.59/11.42 | | COMBINE_EQS: (465), (475) imply: % 81.59/11.42 | | (478) all_256_0 = rat_0 % 81.59/11.42 | | % 81.59/11.43 | | COMBINE_EQS: (433), (436) imply: % 81.59/11.43 | | (479) all_782_0 = rat_15/8 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (338), (479) imply: % 81.59/11.43 | | (480) rat_$sum(rat_15/8, all_27_0) = all_31_0 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (289), (477), (478) imply: % 81.59/11.43 | | (481) rat_$sum(rat_0, all_23_0) = all_131_0 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (344), (466) imply: % 81.59/11.43 | | (482) rat_$sum(rat_15/8, all_27_0) = all_960_0 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (342), (431) imply: % 81.59/11.43 | | (483) rat_$sum(rat_0, all_23_0) = all_948_0 % 81.59/11.43 | | % 81.59/11.43 | | GROUND_INST: instantiating (2) with all_23_0, all_948_0, all_23_0, rat_0, % 81.59/11.43 | | simplifying with (254), (483) gives: % 81.59/11.43 | | (484) all_948_0 = all_23_0 % 81.59/11.43 | | % 81.59/11.43 | | GROUND_INST: instantiating (2) with all_131_0, all_948_0, all_23_0, rat_0, % 81.59/11.43 | | simplifying with (481), (483) gives: % 81.59/11.43 | | (485) all_948_0 = all_131_0 % 81.59/11.43 | | % 81.59/11.43 | | GROUND_INST: instantiating (2) with all_131_0, all_960_0, all_27_0, % 81.59/11.43 | | rat_15/8, simplifying with (183), (482) gives: % 81.59/11.43 | | (486) all_960_0 = all_131_0 % 81.59/11.43 | | % 81.59/11.43 | | GROUND_INST: instantiating (2) with all_31_0, all_960_0, all_27_0, rat_15/8, % 81.59/11.43 | | simplifying with (480), (482) gives: % 81.59/11.43 | | (487) all_960_0 = all_31_0 % 81.59/11.43 | | % 81.59/11.43 | | COMBINE_EQS: (486), (487) imply: % 81.59/11.43 | | (488) all_131_0 = all_31_0 % 81.59/11.43 | | % 81.59/11.43 | | COMBINE_EQS: (484), (485) imply: % 81.59/11.43 | | (489) all_131_0 = all_23_0 % 81.59/11.43 | | % 81.59/11.43 | | COMBINE_EQS: (488), (489) imply: % 81.59/11.43 | | (490) all_31_0 = all_23_0 % 81.59/11.43 | | % 81.59/11.43 | | SIMP: (490) implies: % 81.59/11.43 | | (491) all_31_0 = all_23_0 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (108), (491) imply: % 81.59/11.43 | | (492) rat_$uminus(all_23_0) = rat_5/8 % 81.59/11.43 | | % 81.59/11.43 | | GROUND_INST: instantiating (1) with all_5_0, rat_5/8, all_23_0, simplifying % 81.59/11.43 | | with (109), (492) gives: % 81.59/11.43 | | (493) all_5_0 = rat_5/8 % 81.59/11.43 | | % 81.59/11.43 | | REDUCE: (28), (493) imply: % 81.59/11.43 | | (494) $false % 81.59/11.43 | | % 81.59/11.43 | | CLOSE: (494) is inconsistent. % 81.59/11.43 | | % 81.59/11.43 | End of split % 81.59/11.43 | % 81.59/11.43 End of proof % 81.59/11.43 % SZS output end Proof for theBenchmark % 81.59/11.43 % 81.59/11.43 10825ms %------------------------------------------------------------------------------