%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KRS102+1 : TPTP v8.1.2. Released v3.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 05:51:15 EDT 2023 % Result : Unsatisfiable 12.46s 2.42s % Output : Proof 16.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS102+1 : TPTP v8.1.2. Released v3.1.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n004.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Mon Aug 28 02:12:07 EDT 2023 % 0.13/0.33 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.32/1.16 Prover 1: Preprocessing ... % 3.32/1.16 Prover 4: Preprocessing ... % 3.32/1.19 Prover 5: Preprocessing ... % 3.32/1.19 Prover 6: Preprocessing ... % 3.32/1.19 Prover 0: Preprocessing ... % 3.65/1.20 Prover 2: Preprocessing ... % 3.65/1.21 Prover 3: Preprocessing ... % 6.25/1.58 Prover 6: Constructing countermodel ... % 6.25/1.59 Prover 2: Proving ... % 6.25/1.59 Prover 3: Constructing countermodel ... % 6.25/1.60 Prover 5: Proving ... % 6.43/1.60 Prover 0: Proving ... % 6.43/1.62 Prover 4: Constructing countermodel ... % 6.60/1.63 Prover 1: Constructing countermodel ... % 7.88/1.86 Prover 3: gave up % 7.88/1.86 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.78/1.94 Prover 7: Preprocessing ... % 8.78/2.03 Prover 6: gave up % 8.78/2.03 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.78/2.08 Prover 7: Warning: ignoring some quantifiers % 8.78/2.09 Prover 7: Constructing countermodel ... % 8.78/2.09 Prover 1: gave up % 8.78/2.10 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 8.78/2.11 Prover 8: Preprocessing ... % 9.93/2.13 Prover 4: gave up % 9.93/2.13 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 9.93/2.18 Prover 10: Preprocessing ... % 10.72/2.20 Prover 9: Preprocessing ... % 10.72/2.23 Prover 8: Warning: ignoring some quantifiers % 10.72/2.24 Prover 8: Constructing countermodel ... % 11.52/2.31 Prover 9: Constructing countermodel ... % 11.70/2.32 Prover 10: Warning: ignoring some quantifiers % 11.70/2.33 Prover 10: Constructing countermodel ... % 12.46/2.42 Prover 9: gave up % 12.46/2.42 Prover 2: proved (1796ms) % 12.46/2.42 % 12.46/2.42 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.46/2.42 % 12.46/2.42 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 12.46/2.42 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 12.46/2.42 Prover 5: stopped % 12.46/2.43 Prover 0: stopped % 12.46/2.44 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 12.46/2.44 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 12.46/2.44 Prover 8: gave up % 12.46/2.46 Prover 11: Preprocessing ... % 12.46/2.49 Prover 13: Preprocessing ... % 13.02/2.50 Prover 19: Preprocessing ... % 13.02/2.50 Prover 16: Preprocessing ... % 13.02/2.54 Prover 13: Warning: ignoring some quantifiers % 13.02/2.55 Prover 13: Constructing countermodel ... % 13.02/2.57 Prover 16: Warning: ignoring some quantifiers % 13.61/2.58 Prover 16: Constructing countermodel ... % 13.79/2.61 Prover 11: Constructing countermodel ... % 13.79/2.65 Prover 19: Warning: ignoring some quantifiers % 13.79/2.66 Prover 19: Constructing countermodel ... % 14.34/2.76 Prover 11: gave up % 15.87/2.89 Prover 7: Found proof (size 3478) % 15.87/2.89 Prover 7: proved (1035ms) % 15.87/2.89 Prover 19: stopped % 15.87/2.89 Prover 16: stopped % 15.87/2.90 Prover 10: Found proof (size 3006) % 15.87/2.90 Prover 10: proved (766ms) % 15.87/2.90 Prover 13: stopped % 15.87/2.90 % 15.87/2.90 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.87/2.90 % 15.87/2.93 % SZS output start Proof for theBenchmark % 15.87/2.93 Assumptions after simplification: % 15.87/2.93 --------------------------------- % 15.87/2.93 % 15.87/2.93 (axiom_10) % 15.87/2.94 $i(iplus6) & $i(iminus6) & cTorF(iplus6) & cTorF(iminus6) & ! [v0: $i] : (v0 % 15.87/2.94 = iplus6 | v0 = iminus6 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.94 % 15.87/2.94 (axiom_11) % 15.87/2.94 $i(iplus9) & $i(iminus9) & cTorF(iplus9) & cTorF(iminus9) & ! [v0: $i] : (v0 % 15.87/2.94 = iplus9 | v0 = iminus9 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.94 % 15.87/2.94 (axiom_15) % 15.87/2.94 $i(iplus8) & $i(iT) & $i(iminus3) & $i(iplus7) & (iplus8 = iT | iT = iminus3 | % 15.87/2.94 iT = iplus7) % 15.87/2.94 % 15.87/2.94 (axiom_17) % 15.87/2.94 $i(iplus9) & $i(iminus6) & $i(iT) & $i(iplus1) & (iplus9 = iT | iminus6 = iT | % 15.87/2.94 iT = iplus1) % 15.87/2.94 % 15.87/2.94 (axiom_18) % 15.87/2.94 $i(iminus9) & $i(iT) & $i(iplus3) & $i(iplus4) & (iminus9 = iT | iT = iplus3 | % 15.87/2.94 iT = iplus4) % 15.87/2.94 % 15.87/2.94 (axiom_19) % 15.87/2.94 $i(iminus9) & $i(iminus6) & $i(iT) & $i(iplus1) & (iminus9 = iT | iminus6 = iT % 15.87/2.94 | iT = iplus1) % 15.87/2.94 % 15.87/2.94 (axiom_2) % 15.87/2.94 $i(iminus1) & $i(iplus1) & cTorF(iminus1) & cTorF(iplus1) & ! [v0: $i] : (v0 % 15.87/2.94 = iminus1 | v0 = iplus1 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.94 % 15.87/2.94 (axiom_22) % 15.87/2.94 $i(iplus6) & $i(iT) & $i(iplus3) & $i(iplus4) & (iplus6 = iT | iT = iplus3 | % 15.87/2.94 iT = iplus4) % 15.87/2.94 % 15.87/2.94 (axiom_24) % 15.87/2.94 $i(iminus8) & $i(iT) & $i(iplus3) & $i(iminus2) & (iminus8 = iT | iT = iplus3 % 15.87/2.94 | iT = iminus2) % 15.87/2.94 % 15.87/2.94 (axiom_26) % 15.87/2.94 $i(iminus9) & $i(iT) & $i(iplus3) & $i(iminus2) & (iminus9 = iT | iT = iplus3 % 15.87/2.94 | iT = iminus2) % 15.87/2.94 % 15.87/2.94 (axiom_27) % 15.87/2.95 $i(iplus6) & $i(iT) & $i(iminus7) & $i(iminus2) & (iplus6 = iT | iT = iminus7 % 15.87/2.95 | iT = iminus2) % 15.87/2.95 % 15.87/2.95 (axiom_3) % 15.87/2.95 $i(iplus4) & $i(iminus4) & cTorF(iplus4) & cTorF(iminus4) & ! [v0: $i] : (v0 % 15.87/2.95 = iplus4 | v0 = iminus4 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.95 % 15.87/2.95 (axiom_31) % 15.87/2.95 $i(iplus8) & $i(iT) & $i(iplus2) & $i(iminus4) & (iplus8 = iT | iT = iplus2 | % 15.87/2.95 iT = iminus4) % 15.87/2.95 % 15.87/2.95 (axiom_34) % 15.87/2.95 $i(iplus8) & $i(iT) & $i(iminus5) & $i(iplus7) & (iplus8 = iT | iT = iminus5 | % 15.87/2.95 iT = iplus7) % 15.87/2.95 % 15.87/2.95 (axiom_36) % 15.87/2.95 $i(iT) & $i(iminus3) & $i(iminus7) & $i(iminus4) & (iT = iminus3 | iT = % 15.87/2.95 iminus7 | iT = iminus4) % 15.87/2.95 % 15.87/2.95 (axiom_38) % 15.87/2.95 $i(iT) & $i(iminus3) & $i(iminus2) & $i(iplus1) & (iT = iminus3 | iT = iminus2 % 15.87/2.95 | iT = iplus1) % 15.87/2.95 % 15.87/2.95 (axiom_39) % 15.87/2.95 $i(iplus6) & $i(iT) & $i(iplus3) & $i(iminus4) & (iplus6 = iT | iT = iplus3 | % 15.87/2.95 iT = iminus4) % 15.87/2.95 % 15.87/2.95 (axiom_4) % 15.87/2.95 $i(iminus2) & $i(iplus2) & cTorF(iminus2) & cTorF(iplus2) & ! [v0: $i] : (v0 % 15.87/2.95 = iminus2 | v0 = iplus2 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.95 % 15.87/2.95 (axiom_40) % 15.87/2.95 $i(iminus9) & $i(iminus8) & $i(iT) & $i(iminus4) & (iminus9 = iT | iminus8 = % 15.87/2.95 iT | iT = iminus4) % 15.87/2.95 % 15.87/2.95 (axiom_41) % 15.87/2.95 $i(iT) & $i(iplus3) & $i(iplus4) & $i(iplus1) & (iT = iplus3 | iT = iplus4 | % 15.87/2.95 iT = iplus1) % 15.87/2.95 % 15.87/2.95 (axiom_42) % 15.87/2.95 $i(iplus8) & $i(iT) & $i(iminus3) & $i(iplus2) & (iplus8 = iT | iT = iminus3 | % 15.87/2.95 iT = iplus2) % 15.87/2.95 % 15.87/2.95 (axiom_43) % 15.87/2.95 $i(iplus9) & $i(iminus8) & $i(iT) & $i(iplus3) & (iplus9 = iT | iminus8 = iT | % 15.87/2.95 iT = iplus3) % 15.87/2.95 % 15.87/2.95 (axiom_44) % 15.87/2.96 $i(iplus8) & $i(iT) & $i(iplus3) & $i(iminus7) & (iplus8 = iT | iT = iplus3 | % 15.87/2.96 iT = iminus7) % 15.87/2.96 % 15.87/2.96 (axiom_45) % 15.87/2.96 $i(iminus8) & $i(iT) & $i(iminus3) & $i(iminus5) & (iminus8 = iT | iT = % 15.87/2.96 iminus3 | iT = iminus5) % 15.87/2.96 % 15.87/2.96 (axiom_46) % 15.87/2.96 $i(iplus9) & $i(iT) & $i(iplus3) & $i(iplus4) & (iplus9 = iT | iT = iplus3 | % 15.87/2.96 iT = iplus4) % 15.87/2.96 % 15.87/2.96 (axiom_49) % 15.87/2.96 $i(iminus8) & $i(iT) & $i(iminus3) & $i(iplus5) & (iminus8 = iT | iT = iminus3 % 15.87/2.96 | iT = iplus5) % 15.87/2.96 % 15.87/2.96 (axiom_5) % 15.87/2.96 $i(iminus7) & $i(iplus7) & cTorF(iminus7) & cTorF(iplus7) & ! [v0: $i] : (v0 % 15.87/2.96 = iminus7 | v0 = iplus7 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.96 % 15.87/2.96 (axiom_56) % 15.87/2.96 $i(iminus6) & $i(iT) & $i(iminus2) & $i(iplus4) & (iminus6 = iT | iT = iminus2 % 15.87/2.96 | iT = iplus4) % 15.87/2.96 % 15.87/2.96 (axiom_58) % 15.87/2.96 $i(iplus9) & $i(iT) & $i(iplus7) & $i(iminus4) & (iplus9 = iT | iT = iplus7 | % 15.87/2.96 iT = iminus4) % 15.87/2.96 % 15.87/2.96 (axiom_6) % 15.87/2.96 $i(iminus5) & $i(iplus5) & cTorF(iminus5) & cTorF(iplus5) & ! [v0: $i] : (v0 % 15.87/2.96 = iminus5 | v0 = iplus5 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.96 % 15.87/2.96 (axiom_7) % 15.87/2.96 $i(iminus3) & $i(iplus3) & cTorF(iminus3) & cTorF(iplus3) & ! [v0: $i] : (v0 % 15.87/2.96 = iminus3 | v0 = iplus3 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.96 % 15.87/2.96 (axiom_77) % 15.87/2.96 ~ (iF = iT) & $i(iF) & $i(iT) % 15.87/2.96 % 15.87/2.96 (axiom_8) % 15.87/2.96 $i(iF) & $i(iT) & cTorF(iF) & cTorF(iT) & ! [v0: $i] : (v0 = iF | v0 = iT | % 15.87/2.96 ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.96 % 15.87/2.96 (axiom_9) % 15.87/2.96 $i(iminus8) & $i(iplus8) & cTorF(iminus8) & cTorF(iplus8) & ! [v0: $i] : (v0 % 15.87/2.96 = iminus8 | v0 = iplus8 | ~ $i(v0) | ~ cTorF(v0)) % 15.87/2.96 % 15.87/2.96 Further assumptions not needed in the proof: % 15.87/2.96 -------------------------------------------- % 15.87/2.96 axiom_0, axiom_1, axiom_12, axiom_13, axiom_14, axiom_16, axiom_20, axiom_21, % 15.87/2.96 axiom_23, axiom_25, axiom_28, axiom_29, axiom_30, axiom_32, axiom_33, axiom_35, % 15.87/2.96 axiom_37, axiom_47, axiom_48, axiom_50, axiom_51, axiom_52, axiom_53, axiom_54, % 15.87/2.96 axiom_55, axiom_57, axiom_59, axiom_60, axiom_61, axiom_62, axiom_63, axiom_64, % 15.87/2.96 axiom_65, axiom_66, axiom_67, axiom_68, axiom_69, axiom_70, axiom_71, axiom_72, % 15.87/2.96 axiom_73, axiom_74, axiom_75, axiom_76, cTorF_substitution_1, % 15.87/2.96 cowlNothing_substitution_1, cowlThing_substitution_1, % 15.87/2.96 xsd_integer_substitution_1, xsd_string_substitution_1 % 15.87/2.96 % 15.87/2.96 Those formulas are unsatisfiable: % 15.87/2.96 --------------------------------- % 15.87/2.96 % 15.87/2.96 Begin of proof % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_77) implies: % 15.87/2.97 | (1) ~ (iF = iT) % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_58) implies: % 15.87/2.97 | (2) iplus9 = iT | iT = iplus7 | iT = iminus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_56) implies: % 15.87/2.97 | (3) iminus6 = iT | iT = iminus2 | iT = iplus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_49) implies: % 15.87/2.97 | (4) iminus8 = iT | iT = iminus3 | iT = iplus5 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_46) implies: % 15.87/2.97 | (5) iplus9 = iT | iT = iplus3 | iT = iplus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_45) implies: % 15.87/2.97 | (6) iminus8 = iT | iT = iminus3 | iT = iminus5 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_44) implies: % 15.87/2.97 | (7) iplus8 = iT | iT = iplus3 | iT = iminus7 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_43) implies: % 15.87/2.97 | (8) iplus9 = iT | iminus8 = iT | iT = iplus3 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_42) implies: % 15.87/2.97 | (9) iplus8 = iT | iT = iminus3 | iT = iplus2 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_41) implies: % 15.87/2.97 | (10) iT = iplus3 | iT = iplus4 | iT = iplus1 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_40) implies: % 15.87/2.97 | (11) iminus9 = iT | iminus8 = iT | iT = iminus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_39) implies: % 15.87/2.97 | (12) iplus6 = iT | iT = iplus3 | iT = iminus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_38) implies: % 15.87/2.97 | (13) iT = iminus3 | iT = iminus2 | iT = iplus1 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_36) implies: % 15.87/2.97 | (14) iT = iminus3 | iT = iminus7 | iT = iminus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_34) implies: % 15.87/2.97 | (15) iplus8 = iT | iT = iminus5 | iT = iplus7 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_31) implies: % 15.87/2.97 | (16) iplus8 = iT | iT = iplus2 | iT = iminus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_27) implies: % 15.87/2.97 | (17) iplus6 = iT | iT = iminus7 | iT = iminus2 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_26) implies: % 15.87/2.97 | (18) iminus9 = iT | iT = iplus3 | iT = iminus2 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_24) implies: % 15.87/2.97 | (19) iminus8 = iT | iT = iplus3 | iT = iminus2 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_22) implies: % 15.87/2.97 | (20) iplus6 = iT | iT = iplus3 | iT = iplus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_19) implies: % 15.87/2.97 | (21) iminus9 = iT | iminus6 = iT | iT = iplus1 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_18) implies: % 15.87/2.97 | (22) iminus9 = iT | iT = iplus3 | iT = iplus4 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_17) implies: % 15.87/2.97 | (23) iplus9 = iT | iminus6 = iT | iT = iplus1 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_15) implies: % 15.87/2.97 | (24) iplus8 = iT | iT = iminus3 | iT = iplus7 % 15.87/2.97 | % 15.87/2.97 | ALPHA: (axiom_11) implies: % 16.34/2.97 | (25) cTorF(iplus9) % 16.34/2.97 | (26) $i(iplus9) % 16.34/2.97 | (27) ! [v0: $i] : (v0 = iplus9 | v0 = iminus9 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.97 | % 16.34/2.97 | ALPHA: (axiom_10) implies: % 16.34/2.97 | (28) cTorF(iminus6) % 16.34/2.97 | (29) $i(iminus6) % 16.34/2.97 | (30) ! [v0: $i] : (v0 = iplus6 | v0 = iminus6 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.97 | % 16.34/2.97 | ALPHA: (axiom_9) implies: % 16.34/2.98 | (31) cTorF(iplus8) % 16.34/2.98 | (32) cTorF(iminus8) % 16.34/2.98 | (33) $i(iplus8) % 16.34/2.98 | (34) $i(iminus8) % 16.34/2.98 | (35) ! [v0: $i] : (v0 = iminus8 | v0 = iplus8 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_8) implies: % 16.34/2.98 | (36) cTorF(iT) % 16.34/2.98 | (37) cTorF(iF) % 16.34/2.98 | (38) $i(iT) % 16.34/2.98 | (39) $i(iF) % 16.34/2.98 | (40) ! [v0: $i] : (v0 = iF | v0 = iT | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_7) implies: % 16.34/2.98 | (41) cTorF(iplus3) % 16.34/2.98 | (42) cTorF(iminus3) % 16.34/2.98 | (43) $i(iplus3) % 16.34/2.98 | (44) $i(iminus3) % 16.34/2.98 | (45) ! [v0: $i] : (v0 = iminus3 | v0 = iplus3 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_6) implies: % 16.34/2.98 | (46) cTorF(iplus5) % 16.34/2.98 | (47) $i(iplus5) % 16.34/2.98 | (48) ! [v0: $i] : (v0 = iminus5 | v0 = iplus5 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_5) implies: % 16.34/2.98 | (49) ! [v0: $i] : (v0 = iminus7 | v0 = iplus7 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_4) implies: % 16.34/2.98 | (50) cTorF(iminus2) % 16.34/2.98 | (51) $i(iminus2) % 16.34/2.98 | (52) ! [v0: $i] : (v0 = iminus2 | v0 = iplus2 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_3) implies: % 16.34/2.98 | (53) ! [v0: $i] : (v0 = iplus4 | v0 = iminus4 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | ALPHA: (axiom_2) implies: % 16.34/2.98 | (54) cTorF(iminus1) % 16.34/2.98 | (55) $i(iminus1) % 16.34/2.98 | (56) ! [v0: $i] : (v0 = iminus1 | v0 = iplus1 | ~ $i(v0) | ~ cTorF(v0)) % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (30) with iminus1, simplifying with (54), (55) % 16.34/2.98 | gives: % 16.34/2.98 | (57) iplus6 = iminus1 | iminus6 = iminus1 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (49) with iminus1, simplifying with (54), (55) % 16.34/2.98 | gives: % 16.34/2.98 | (58) iminus7 = iminus1 | iplus7 = iminus1 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (56) with iminus2, simplifying with (50), (51) % 16.34/2.98 | gives: % 16.34/2.98 | (59) iminus2 = iminus1 | iminus2 = iplus1 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (52) with iplus5, simplifying with (46), (47) % 16.34/2.98 | gives: % 16.34/2.98 | (60) iplus5 = iminus2 | iplus5 = iplus2 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (40) with iplus3, simplifying with (41), (43) % 16.34/2.98 | gives: % 16.34/2.98 | (61) iF = iplus3 | iT = iplus3 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (49) with iplus3, simplifying with (41), (43) % 16.34/2.98 | gives: % 16.34/2.98 | (62) iplus3 = iminus7 | iplus3 = iplus7 % 16.34/2.98 | % 16.34/2.98 | GROUND_INST: instantiating (35) with iminus3, simplifying with (42), (44) % 16.34/2.98 | gives: % 16.34/2.99 | (63) iminus8 = iminus3 | iplus8 = iminus3 % 16.34/2.99 | % 16.34/2.99 | GROUND_INST: instantiating (53) with iminus3, simplifying with (42), (44) % 16.34/2.99 | gives: % 16.34/2.99 | (64) iminus3 = iplus4 | iminus3 = iminus4 % 16.34/2.99 | % 16.34/2.99 | GROUND_INST: instantiating (45) with iT, simplifying with (36), (38) gives: % 16.34/2.99 | (65) iT = iminus3 | iT = iplus3 % 16.34/2.99 | % 16.34/2.99 | GROUND_INST: instantiating (27) with iF, simplifying with (37), (39) gives: % 16.34/2.99 | (66) iplus9 = iF | iminus9 = iF % 16.34/2.99 | % 16.34/2.99 | GROUND_INST: instantiating (30) with iF, simplifying with (37), (39) gives: % 16.34/2.99 | (67) iplus6 = iF | iminus6 = iF % 16.34/2.99 | % 16.34/2.99 | GROUND_INST: instantiating (35) with iF, simplifying with (37), (39) gives: % 16.34/2.99 | (68) iminus8 = iF | iplus8 = iF % 16.34/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (45) with iF, simplifying with (37), (39) gives: % 16.41/2.99 | (69) iF = iminus3 | iF = iplus3 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (53) with iF, simplifying with (37), (39) gives: % 16.41/2.99 | (70) iF = iplus4 | iF = iminus4 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (56) with iF, simplifying with (37), (39) gives: % 16.41/2.99 | (71) iF = iminus1 | iF = iplus1 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (40) with iplus8, simplifying with (31), (33) % 16.41/2.99 | gives: % 16.41/2.99 | (72) iplus8 = iF | iplus8 = iT % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (48) with iplus8, simplifying with (31), (33) % 16.41/2.99 | gives: % 16.41/2.99 | (73) iplus8 = iminus5 | iplus8 = iplus5 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (52) with iplus8, simplifying with (31), (33) % 16.41/2.99 | gives: % 16.41/2.99 | (74) iplus8 = iminus2 | iplus8 = iplus2 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (53) with iplus8, simplifying with (31), (33) % 16.41/2.99 | gives: % 16.41/2.99 | (75) iplus8 = iplus4 | iplus8 = iminus4 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (48) with iminus8, simplifying with (32), (34) % 16.41/2.99 | gives: % 16.41/2.99 | (76) iminus8 = iminus5 | iminus8 = iplus5 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (53) with iminus6, simplifying with (28), (29) % 16.41/2.99 | gives: % 16.41/2.99 | (77) iminus6 = iplus4 | iminus6 = iminus4 % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (40) with iplus9, simplifying with (25), (26) % 16.41/2.99 | gives: % 16.41/2.99 | (78) iplus9 = iF | iplus9 = iT % 16.41/2.99 | % 16.41/2.99 | GROUND_INST: instantiating (56) with iplus9, simplifying with (25), (26) % 16.41/2.99 | gives: % 16.41/2.99 | (79) iplus9 = iminus1 | iplus9 = iplus1 % 16.41/2.99 | % 16.41/2.99 | BETA: splitting (10) gives: % 16.41/2.99 | % 16.41/2.99 | Case 1: % 16.41/2.99 | | % 16.41/2.99 | | (80) iT = iplus3 % 16.41/2.99 | | % 16.41/2.99 | | REDUCE: (1), (80) imply: % 16.41/2.99 | | (81) ~ (iF = iplus3) % 16.41/2.99 | | % 16.41/2.99 | | BETA: splitting (69) gives: % 16.41/2.99 | | % 16.41/2.99 | | Case 1: % 16.41/2.99 | | | % 16.41/2.99 | | | (82) iF = iplus3 % 16.41/2.99 | | | % 16.41/2.99 | | | REDUCE: (81), (82) imply: % 16.41/2.99 | | | (83) $false % 16.41/2.99 | | | % 16.41/2.99 | | | CLOSE: (83) is inconsistent. % 16.41/2.99 | | | % 16.41/2.99 | | Case 2: % 16.41/2.99 | | | % 16.41/2.99 | | | (84) iF = iminus3 % 16.41/2.99 | | | % 16.41/2.99 | | | REDUCE: (81), (84) imply: % 16.41/2.99 | | | (85) ~ (iminus3 = iplus3) % 16.41/2.99 | | | % 16.41/3.00 | | | REF_CLOSE: (3), (4), (6), (9), (13), (14), (17), (24), (57), (58), (59), % 16.41/3.00 | | | (64), (68), (72), (74), (76), (80), (84), (85) are inconsistent % 16.41/3.00 | | | by sub-proof #11. % 16.41/3.00 | | | % 16.41/3.00 | | End of split % 16.41/3.00 | | % 16.41/3.00 | Case 2: % 16.41/3.00 | | % 16.41/3.00 | | (86) ~ (iT = iplus3) % 16.41/3.00 | | % 16.41/3.00 | | BETA: splitting (61) gives: % 16.41/3.00 | | % 16.41/3.00 | | Case 1: % 16.41/3.00 | | | % 16.41/3.00 | | | (87) iT = iplus3 % 16.41/3.00 | | | % 16.41/3.00 | | | REDUCE: (86), (87) imply: % 16.41/3.00 | | | (88) $false % 16.41/3.00 | | | % 16.41/3.00 | | | CLOSE: (88) is inconsistent. % 16.41/3.00 | | | % 16.41/3.00 | | Case 2: % 16.41/3.00 | | | % 16.41/3.00 | | | (89) iF = iplus3 % 16.41/3.00 | | | % 16.41/3.00 | | | REDUCE: (1), (89) imply: % 16.41/3.00 | | | (90) ~ (iT = iplus3) % 16.41/3.00 | | | % 16.41/3.00 | | | BETA: splitting (65) gives: % 16.41/3.00 | | | % 16.41/3.00 | | | Case 1: % 16.41/3.00 | | | | % 16.41/3.00 | | | | (91) iT = iminus3 % 16.41/3.00 | | | | % 16.41/3.00 | | | | REDUCE: (86), (91) imply: % 16.41/3.00 | | | | (92) ~ (iminus3 = iplus3) % 16.41/3.00 | | | | % 16.41/3.00 | | | | BETA: splitting (12) gives: % 16.41/3.00 | | | | % 16.41/3.00 | | | | Case 1: % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | (93) iplus6 = iT % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | COMBINE_EQS: (91), (93) imply: % 16.41/3.00 | | | | | (94) iplus6 = iminus3 % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | REF_CLOSE: (2), (3), (4), (5), (6), (7), (8), (9), (11), (13), (14), % 16.41/3.00 | | | | | (15), (16), (17), (18), (19), (21), (22), (23), (24), (57), % 16.41/3.00 | | | | | (58), (59), (60), (62), (63), (64), (66), (67), (68), (70), % 16.41/3.00 | | | | | (71), (72), (73), (74), (75), (76), (77), (78), (79), (89), % 16.41/3.00 | | | | | (91), (92), (94) are inconsistent by sub-proof #1. % 16.41/3.00 | | | | | % 16.41/3.00 | | | | Case 2: % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | (95) iT = iplus3 | iT = iminus4 % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | BETA: splitting (20) gives: % 16.41/3.00 | | | | | % 16.41/3.00 | | | | | Case 1: % 16.41/3.00 | | | | | | % 16.41/3.00 | | | | | | (96) iplus6 = iT % 16.41/3.00 | | | | | | % 16.41/3.00 | | | | | | COMBINE_EQS: (91), (96) imply: % 16.41/3.00 | | | | | | (97) iplus6 = iminus3 % 16.41/3.00 | | | | | | % 16.53/3.01 | | | | | | REF_CLOSE: (2), (3), (4), (5), (6), (7), (8), (9), (11), (13), (14), % 16.53/3.01 | | | | | | (15), (16), (17), (18), (19), (21), (22), (23), (24), % 16.53/3.01 | | | | | | (57), (58), (59), (60), (62), (63), (64), (66), (67), % 16.53/3.01 | | | | | | (68), (70), (71), (72), (73), (74), (75), (76), (77), % 16.53/3.01 | | | | | | (78), (79), (89), (91), (92), (97) are inconsistent by % 16.53/3.01 | | | | | | sub-proof #1. % 16.53/3.01 | | | | | | % 16.53/3.01 | | | | | Case 2: % 16.53/3.01 | | | | | | % 16.53/3.01 | | | | | | (98) iT = iplus3 | iT = iplus4 % 16.53/3.01 | | | | | | % 16.53/3.01 | | | | | | BETA: splitting (95) gives: % 16.53/3.01 | | | | | | % 16.53/3.01 | | | | | | Case 1: % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | (99) iT = iplus3 % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | REF_CLOSE: (91), (92), (99) are inconsistent by sub-proof #15. % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | Case 2: % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | (100) iT = iminus4 % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | COMBINE_EQS: (91), (100) imply: % 16.53/3.01 | | | | | | | (101) iminus3 = iminus4 % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | SIMP: (101) implies: % 16.53/3.01 | | | | | | | (102) iminus3 = iminus4 % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | REDUCE: (92), (102) imply: % 16.53/3.01 | | | | | | | (103) ~ (iplus3 = iminus4) % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | SIMP: (103) implies: % 16.53/3.01 | | | | | | | (104) ~ (iplus3 = iminus4) % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | BETA: splitting (70) gives: % 16.53/3.01 | | | | | | | % 16.53/3.01 | | | | | | | Case 1: % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | (105) iF = iminus4 % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | COMBINE_EQS: (89), (105) imply: % 16.53/3.01 | | | | | | | | (106) iplus3 = iminus4 % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | REDUCE: (104), (106) imply: % 16.53/3.01 | | | | | | | | (107) $false % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | CLOSE: (107) is inconsistent. % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | Case 2: % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | (108) iF = iplus4 % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | COMBINE_EQS: (89), (108) imply: % 16.53/3.01 | | | | | | | | (109) iplus3 = iplus4 % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | BETA: splitting (98) gives: % 16.53/3.01 | | | | | | | | % 16.53/3.01 | | | | | | | | Case 1: % 16.53/3.01 | | | | | | | | | % 16.53/3.01 | | | | | | | | | (110) iT = iplus3 % 16.53/3.01 | | | | | | | | | % 16.53/3.01 | | | | | | | | | COMBINE_EQS: (100), (110) imply: % 16.53/3.01 | | | | | | | | | (111) iplus3 = iminus4 % 16.53/3.01 | | | | | | | | | % 16.53/3.01 | | | | | | | | | COMBINE_EQS: (109), (111) imply: % 16.53/3.01 | | | | | | | | | (112) iplus4 = iminus4 % 16.53/3.01 | | | | | | | | | % 16.53/3.02 | | | | | | | | | SIMP: (112) implies: % 16.53/3.02 | | | | | | | | | (113) iplus4 = iminus4 % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | | REF_CLOSE: (70), (89), (104), (113) are inconsistent by % 16.53/3.02 | | | | | | | | | sub-proof #3. % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | Case 2: % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | | (114) iT = iplus4 % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | | COMBINE_EQS: (100), (114) imply: % 16.53/3.02 | | | | | | | | | (115) iplus4 = iminus4 % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | | REF_CLOSE: (70), (89), (104), (115) are inconsistent by % 16.53/3.02 | | | | | | | | | sub-proof #3. % 16.53/3.02 | | | | | | | | | % 16.53/3.02 | | | | | | | | End of split % 16.53/3.02 | | | | | | | | % 16.53/3.02 | | | | | | | End of split % 16.53/3.02 | | | | | | | % 16.53/3.02 | | | | | | End of split % 16.53/3.02 | | | | | | % 16.53/3.02 | | | | | End of split % 16.53/3.02 | | | | | % 16.53/3.02 | | | | End of split % 16.53/3.02 | | | | % 16.53/3.02 | | | Case 2: % 16.53/3.02 | | | | % 16.53/3.02 | | | | (116) iT = iplus3 % 16.53/3.02 | | | | % 16.53/3.02 | | | | REDUCE: (86), (116) imply: % 16.53/3.02 | | | | (117) $false % 16.53/3.02 | | | | % 16.53/3.02 | | | | CLOSE: (117) is inconsistent. % 16.53/3.02 | | | | % 16.53/3.02 | | | End of split % 16.53/3.02 | | | % 16.53/3.02 | | End of split % 16.53/3.02 | | % 16.53/3.02 | End of split % 16.53/3.02 | % 16.53/3.02 End of proof % 16.53/3.02 % 16.53/3.02 Sub-proof #1 shows that the following formulas are inconsistent: % 16.53/3.02 ---------------------------------------------------------------- % 16.53/3.02 (1) iminus6 = iT | iT = iminus2 | iT = iplus4 % 16.53/3.02 (2) iminus8 = iT | iT = iminus3 | iT = iplus5 % 16.53/3.02 (3) iminus8 = iT | iT = iminus3 | iT = iminus5 % 16.53/3.02 (4) iminus2 = iminus1 | iminus2 = iplus1 % 16.53/3.02 (5) iF = iplus3 % 16.53/3.02 (6) iplus8 = iplus4 | iplus8 = iminus4 % 16.53/3.02 (7) iplus6 = iminus3 % 16.53/3.02 (8) iT = iminus3 % 16.53/3.02 (9) iplus9 = iT | iminus8 = iT | iT = iplus3 % 16.53/3.02 (10) iF = iplus4 | iF = iminus4 % 16.53/3.02 (11) iplus9 = iT | iT = iplus7 | iT = iminus4 % 16.58/3.02 (12) iplus8 = iminus5 | iplus8 = iplus5 % 16.58/3.02 (13) iT = iminus3 | iT = iminus7 | iT = iminus4 % 16.58/3.02 (14) iplus9 = iF | iplus9 = iT % 16.58/3.02 (15) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.02 (16) iplus5 = iminus2 | iplus5 = iplus2 % 16.58/3.02 (17) iminus9 = iT | iminus8 = iT | iT = iminus4 % 16.58/3.02 (18) iplus6 = iF | iminus6 = iF % 16.58/3.02 (19) iminus7 = iminus1 | iplus7 = iminus1 % 16.58/3.02 (20) iminus6 = iplus4 | iminus6 = iminus4 % 16.58/3.02 (21) iminus9 = iT | iminus6 = iT | iT = iplus1 % 16.58/3.02 (22) iF = iminus1 | iF = iplus1 % 16.58/3.02 (23) iplus8 = iT | iT = iplus2 | iT = iminus4 % 16.58/3.02 (24) iplus9 = iminus1 | iplus9 = iplus1 % 16.58/3.02 (25) iminus9 = iT | iT = iplus3 | iT = iplus4 % 16.58/3.02 (26) iminus8 = iT | iT = iplus3 | iT = iminus2 % 16.58/3.02 (27) iplus9 = iT | iminus6 = iT | iT = iplus1 % 16.58/3.02 (28) iplus8 = iT | iT = iminus3 | iT = iplus2 % 16.58/3.02 (29) iminus9 = iT | iT = iplus3 | iT = iminus2 % 16.58/3.02 (30) iplus8 = iminus2 | iplus8 = iplus2 % 16.58/3.02 (31) iminus8 = iF | iplus8 = iF % 16.58/3.02 (32) iplus8 = iF | iplus8 = iT % 16.58/3.02 (33) iplus6 = iT | iT = iminus7 | iT = iminus2 % 16.58/3.02 (34) iplus8 = iT | iT = iplus3 | iT = iminus7 % 16.58/3.02 (35) iplus8 = iT | iT = iminus5 | iT = iplus7 % 16.58/3.02 (36) iplus3 = iminus7 | iplus3 = iplus7 % 16.58/3.02 (37) iplus9 = iF | iminus9 = iF % 16.58/3.02 (38) iminus8 = iminus3 | iplus8 = iminus3 % 16.58/3.02 (39) iT = iminus3 | iT = iminus2 | iT = iplus1 % 16.58/3.02 (40) iplus9 = iT | iT = iplus3 | iT = iplus4 % 16.58/3.02 (41) ~ (iminus3 = iplus3) % 16.58/3.02 (42) iminus8 = iminus5 | iminus8 = iplus5 % 16.58/3.02 (43) iminus3 = iplus4 | iminus3 = iminus4 % 16.58/3.02 (44) iplus8 = iT | iT = iminus3 | iT = iplus7 % 16.58/3.02 % 16.58/3.02 Begin of proof % 16.58/3.02 | % 16.58/3.02 | BETA: splitting (18) gives: % 16.58/3.02 | % 16.58/3.02 | Case 1: % 16.58/3.02 | | % 16.58/3.02 | | (45) iplus6 = iF % 16.58/3.02 | | % 16.58/3.02 | | COMBINE_EQS: (7), (45) imply: % 16.58/3.02 | | (46) iF = iminus3 % 16.58/3.02 | | % 16.58/3.02 | | SIMP: (46) implies: % 16.58/3.02 | | (47) iF = iminus3 % 16.58/3.02 | | % 16.58/3.02 | | REF_CLOSE: (1), (2), (3), (4), (5), (8), (13), (15), (19), (28), (30), (31), % 16.58/3.02 | | (32), (33), (39), (41), (42), (43), (44), (47) are inconsistent % 16.58/3.02 | | by sub-proof #10. % 16.58/3.02 | | % 16.58/3.02 | Case 2: % 16.58/3.02 | | % 16.58/3.02 | | (48) iminus6 = iF % 16.58/3.02 | | (49) ~ (iplus6 = iF) % 16.58/3.02 | | % 16.58/3.02 | | COMBINE_EQS: (5), (48) imply: % 16.58/3.02 | | (50) iminus6 = iplus3 % 16.58/3.02 | | % 16.58/3.02 | | BETA: splitting (26) gives: % 16.58/3.02 | | % 16.58/3.02 | | Case 1: % 16.58/3.02 | | | % 16.58/3.02 | | | (51) iminus8 = iT % 16.58/3.02 | | | % 16.58/3.02 | | | COMBINE_EQS: (8), (51) imply: % 16.58/3.02 | | | (52) iminus8 = iminus3 % 16.58/3.02 | | | % 16.58/3.02 | | | BETA: splitting (31) gives: % 16.58/3.02 | | | % 16.58/3.02 | | | Case 1: % 16.58/3.02 | | | | % 16.58/3.02 | | | | (53) iminus8 = iF % 16.58/3.02 | | | | % 16.58/3.02 | | | | COMBINE_EQS: (52), (53) imply: % 16.58/3.02 | | | | (54) iF = iminus3 % 16.58/3.02 | | | | % 16.58/3.02 | | | | COMBINE_EQS: (5), (54) imply: % 16.58/3.02 | | | | (55) iminus3 = iplus3 % 16.58/3.02 | | | | % 16.58/3.02 | | | | SIMP: (55) implies: % 16.58/3.02 | | | | (56) iminus3 = iplus3 % 16.58/3.02 | | | | % 16.58/3.02 | | | | COMBINE_EQS: (8), (56) imply: % 16.58/3.02 | | | | (57) iT = iplus3 % 16.58/3.03 | | | | % 16.58/3.03 | | | | REF_CLOSE: (2), (3), (41), (42), (52), (57) are inconsistent by % 16.58/3.03 | | | | sub-proof #14. % 16.58/3.03 | | | | % 16.58/3.03 | | | Case 2: % 16.58/3.03 | | | | % 16.58/3.03 | | | | (58) iplus8 = iF % 16.58/3.03 | | | | (59) ~ (iminus8 = iF) % 16.58/3.03 | | | | % 16.58/3.03 | | | | COMBINE_EQS: (5), (58) imply: % 16.58/3.03 | | | | (60) iplus8 = iplus3 % 16.58/3.03 | | | | % 16.58/3.03 | | | | BETA: splitting (34) gives: % 16.58/3.03 | | | | % 16.58/3.03 | | | | Case 1: % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | (61) iplus8 = iT % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | COMBINE_EQS: (60), (61) imply: % 16.58/3.03 | | | | | (62) iT = iplus3 % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | REF_CLOSE: (2), (3), (41), (42), (52), (62) are inconsistent by % 16.58/3.03 | | | | | sub-proof #14. % 16.58/3.03 | | | | | % 16.58/3.03 | | | | Case 2: % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | (63) ~ (iplus8 = iT) % 16.58/3.03 | | | | | (64) iT = iplus3 | iT = iminus7 % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | REDUCE: (8), (60), (63) imply: % 16.58/3.03 | | | | | (65) ~ (iminus3 = iplus3) % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | BETA: splitting (64) gives: % 16.58/3.03 | | | | | % 16.58/3.03 | | | | | Case 1: % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | (66) iT = iplus3 % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | REF_CLOSE: (2), (3), (41), (42), (52), (66) are inconsistent by % 16.58/3.03 | | | | | | sub-proof #14. % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | Case 2: % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | (67) iT = iminus7 % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | COMBINE_EQS: (8), (67) imply: % 16.58/3.03 | | | | | | (68) iminus3 = iminus7 % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | COMBINE_EQS: (7), (68) imply: % 16.58/3.03 | | | | | | (69) iplus6 = iminus7 % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | REDUCE: (41), (68) imply: % 16.58/3.03 | | | | | | (70) ~ (iplus3 = iminus7) % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | SIMP: (70) implies: % 16.58/3.03 | | | | | | (71) ~ (iplus3 = iminus7) % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | BETA: splitting (36) gives: % 16.58/3.03 | | | | | | % 16.58/3.03 | | | | | | Case 1: % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | (72) iplus3 = iminus7 % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | REDUCE: (71), (72) imply: % 16.58/3.03 | | | | | | | (73) $false % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | CLOSE: (73) is inconsistent. % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | Case 2: % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | (74) iplus3 = iplus7 % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | COMBINE_EQS: (5), (74) imply: % 16.58/3.03 | | | | | | | (75) iF = iplus7 % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | COMBINE_EQS: (60), (74) imply: % 16.58/3.03 | | | | | | | (76) iplus8 = iplus7 % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | COMBINE_EQS: (50), (74) imply: % 16.58/3.03 | | | | | | | (77) iminus6 = iplus7 % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | REDUCE: (71), (74) imply: % 16.58/3.03 | | | | | | | (78) ~ (iminus7 = iplus7) % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | SIMP: (78) implies: % 16.58/3.03 | | | | | | | (79) ~ (iminus7 = iplus7) % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | BETA: splitting (35) gives: % 16.58/3.03 | | | | | | | % 16.58/3.03 | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | (80) iplus8 = iT % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | COMBINE_EQS: (76), (80) imply: % 16.58/3.03 | | | | | | | | (81) iT = iplus7 % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | REF_CLOSE: (67), (79), (81) are inconsistent by sub-proof #9. % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | (82) iT = iminus5 | iT = iplus7 % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | BETA: splitting (82) gives: % 16.58/3.03 | | | | | | | | % 16.58/3.03 | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | % 16.58/3.03 | | | | | | | | | (83) iT = iminus5 % 16.58/3.03 | | | | | | | | | % 16.58/3.03 | | | | | | | | | COMBINE_EQS: (67), (83) imply: % 16.58/3.03 | | | | | | | | | (84) iminus5 = iminus7 % 16.58/3.03 | | | | | | | | | % 16.58/3.03 | | | | | | | | | BETA: splitting (12) gives: % 16.58/3.03 | | | | | | | | | % 16.58/3.03 | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | (85) iplus8 = iminus5 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | COMBINE_EQS: (76), (85) imply: % 16.58/3.03 | | | | | | | | | | (86) iminus5 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | SIMP: (86) implies: % 16.58/3.03 | | | | | | | | | | (87) iminus5 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | COMBINE_EQS: (84), (87) imply: % 16.58/3.03 | | | | | | | | | | (88) iminus7 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | SIMP: (88) implies: % 16.58/3.03 | | | | | | | | | | (89) iminus7 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | REDUCE: (79), (89) imply: % 16.58/3.03 | | | | | | | | | | (90) $false % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | CLOSE: (90) is inconsistent. % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | (91) iplus8 = iplus5 % 16.58/3.03 | | | | | | | | | | (92) ~ (iplus8 = iminus5) % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | COMBINE_EQS: (76), (91) imply: % 16.58/3.03 | | | | | | | | | | (93) iplus5 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | SIMP: (93) implies: % 16.58/3.03 | | | | | | | | | | (94) iplus5 = iplus7 % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | BETA: splitting (25) gives: % 16.58/3.03 | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | (95) iminus9 = iT % 16.58/3.03 | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | COMBINE_EQS: (67), (95) imply: % 16.58/3.03 | | | | | | | | | | | (96) iminus9 = iminus7 % 16.58/3.03 | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | BETA: splitting (37) gives: % 16.58/3.03 | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | (97) iplus9 = iF % 16.58/3.03 | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | COMBINE_EQS: (75), (97) imply: % 16.58/3.03 | | | | | | | | | | | | (98) iplus9 = iplus7 % 16.58/3.03 | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | BETA: splitting (27) gives: % 16.58/3.03 | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | (99) iplus9 = iT % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | COMBINE_EQS: (98), (99) imply: % 16.58/3.03 | | | | | | | | | | | | | (100) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | SIMP: (100) implies: % 16.58/3.03 | | | | | | | | | | | | | (101) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | COMBINE_EQS: (67), (101) imply: % 16.58/3.03 | | | | | | | | | | | | | (102) iminus7 = iplus7 % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | REDUCE: (79), (102) imply: % 16.58/3.03 | | | | | | | | | | | | | (103) $false % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | CLOSE: (103) is inconsistent. % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | (104) ~ (iplus9 = iT) % 16.58/3.03 | | | | | | | | | | | | | (105) iminus6 = iT | iT = iplus1 % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | BETA: splitting (105) gives: % 16.58/3.03 | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | (106) iminus6 = iT % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | COMBINE_EQS: (77), (106) imply: % 16.58/3.03 | | | | | | | | | | | | | | (107) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | SIMP: (107) implies: % 16.58/3.03 | | | | | | | | | | | | | | (108) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | REF_CLOSE: (67), (79), (108) are inconsistent by sub-proof % 16.58/3.03 | | | | | | | | | | | | | | #9. % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | (109) iT = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | COMBINE_EQS: (67), (109) imply: % 16.58/3.03 | | | | | | | | | | | | | | (110) iminus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | SIMP: (110) implies: % 16.58/3.03 | | | | | | | | | | | | | | (111) iminus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | COMBINE_EQS: (69), (111) imply: % 16.58/3.03 | | | | | | | | | | | | | | (112) iplus6 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | REDUCE: (79), (111) imply: % 16.58/3.03 | | | | | | | | | | | | | | (113) ~ (iplus7 = iplus1) % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | SIMP: (113) implies: % 16.58/3.03 | | | | | | | | | | | | | | (114) ~ (iplus7 = iplus1) % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | BETA: splitting (40) gives: % 16.58/3.03 | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | (115) iplus9 = iT % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | COMBINE_EQS: (98), (115) imply: % 16.58/3.03 | | | | | | | | | | | | | | | (116) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | SIMP: (116) implies: % 16.58/3.03 | | | | | | | | | | | | | | | (117) iT = iplus7 % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | COMBINE_EQS: (109), (117) imply: % 16.58/3.03 | | | | | | | | | | | | | | | (118) iplus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | SIMP: (118) implies: % 16.58/3.03 | | | | | | | | | | | | | | | (119) iplus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | REDUCE: (114), (119) imply: % 16.58/3.03 | | | | | | | | | | | | | | | (120) $false % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | CLOSE: (120) is inconsistent. % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | (121) iT = iplus3 | iT = iplus4 % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | BETA: splitting (22) gives: % 16.58/3.03 | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | Case 1: % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | (122) iF = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (75), (122) imply: % 16.58/3.03 | | | | | | | | | | | | | | | | (123) iplus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | SIMP: (123) implies: % 16.58/3.03 | | | | | | | | | | | | | | | | (124) iplus7 = iplus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | REDUCE: (114), (124) imply: % 16.58/3.03 | | | | | | | | | | | | | | | | (125) $false % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | CLOSE: (125) is inconsistent. % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | Case 2: % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | (126) iF = iminus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (75), (126) imply: % 16.58/3.03 | | | | | | | | | | | | | | | | (127) iplus7 = iminus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.03 | | | | | | | | | | | | | | | | SIMP: (127) implies: % 16.58/3.03 | | | | | | | | | | | | | | | | (128) iplus7 = iminus1 % 16.58/3.03 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (74), (128) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (129) iplus3 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (77), (128) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (130) iminus6 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (98), (128) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (131) iplus9 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | REDUCE: (114), (128) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (132) ~ (iminus1 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | BETA: splitting (11) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | (133) iplus9 = iT % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | COMBINE_EQS: (131), (133) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | (134) iT = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | SIMP: (134) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | (135) iT = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | COMBINE_EQS: (109), (135) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | (136) iminus1 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (112), (130), (132), (136) are inconsistent % 16.58/3.04 | | | | | | | | | | | | | | | | | by sub-proof #8. % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | (137) iT = iplus7 | iT = iminus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | BETA: splitting (121) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | (138) iT = iplus3 % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | REF_CLOSE: (2), (3), (41), (42), (52), (138) are inconsistent % 16.58/3.04 | | | | | | | | | | | | | | | | | | by sub-proof #14. % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | (139) iT = iplus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | | (140) ~ (iT = iplus3) % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (109), (139) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | (141) iplus4 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | REDUCE: (109), (129), (140) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | (142) ~ (iminus1 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | BETA: splitting (20) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (143) iminus6 = iminus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (130), (143) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (144) iminus4 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | SIMP: (144) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (145) iminus4 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | BETA: splitting (137) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | (146) iT = iplus7 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (109), (146) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | (147) iplus7 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | SIMP: (147) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | (148) iplus7 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (128), (148) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | (149) iminus1 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (112), (130), (132), (149) are inconsistent % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | by sub-proof #8. % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | (150) iT = iminus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (109), (112), (130), (132), (145), (150) are % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | inconsistent by sub-proof #7. % 16.58/3.04 | | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (151) iminus6 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (130), (151) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (152) iplus4 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | SIMP: (152) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (153) iplus4 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (112), (130), (132), (141), (153) are % 16.58/3.04 | | | | | | | | | | | | | | | | | | | inconsistent by sub-proof #6. % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | (154) iminus9 = iF % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | COMBINE_EQS: (96), (154) imply: % 16.58/3.04 | | | | | | | | | | | | (155) iF = iminus7 % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | SIMP: (155) implies: % 16.58/3.04 | | | | | | | | | | | | (156) iF = iminus7 % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | COMBINE_EQS: (75), (156) imply: % 16.58/3.04 | | | | | | | | | | | | (157) iminus7 = iplus7 % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | REDUCE: (79), (157) imply: % 16.58/3.04 | | | | | | | | | | | | (158) $false % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | CLOSE: (158) is inconsistent. % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | End of split % 16.58/3.04 | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | (159) ~ (iminus9 = iT) % 16.58/3.04 | | | | | | | | | | | (160) iT = iplus3 | iT = iplus4 % 16.58/3.04 | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | REDUCE: (67), (159) imply: % 16.58/3.04 | | | | | | | | | | | (161) ~ (iminus9 = iminus7) % 16.58/3.04 | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | BETA: splitting (21) gives: % 16.58/3.04 | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | (162) iminus9 = iT % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | COMBINE_EQS: (67), (162) imply: % 16.58/3.04 | | | | | | | | | | | | (163) iminus9 = iminus7 % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | REDUCE: (161), (163) imply: % 16.58/3.04 | | | | | | | | | | | | (164) $false % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | CLOSE: (164) is inconsistent. % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | (165) iminus6 = iT | iT = iplus1 % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | BETA: splitting (160) gives: % 16.58/3.04 | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | (166) iT = iplus3 % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | REF_CLOSE: (2), (3), (41), (42), (52), (166) are inconsistent % 16.58/3.04 | | | | | | | | | | | | | by sub-proof #14. % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | (167) iT = iplus4 % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | COMBINE_EQS: (67), (167) imply: % 16.58/3.04 | | | | | | | | | | | | | (168) iminus7 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | SIMP: (168) implies: % 16.58/3.04 | | | | | | | | | | | | | (169) iminus7 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | COMBINE_EQS: (69), (169) imply: % 16.58/3.04 | | | | | | | | | | | | | (170) iplus6 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | REDUCE: (161), (169) imply: % 16.58/3.04 | | | | | | | | | | | | | (171) ~ (iminus9 = iplus4) % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | REDUCE: (79), (169) imply: % 16.58/3.04 | | | | | | | | | | | | | (172) ~ (iplus7 = iplus4) % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | SIMP: (172) implies: % 16.58/3.04 | | | | | | | | | | | | | (173) ~ (iplus7 = iplus4) % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | BETA: splitting (165) gives: % 16.58/3.04 | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | (174) iminus6 = iT % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | COMBINE_EQS: (77), (174) imply: % 16.58/3.04 | | | | | | | | | | | | | | (175) iT = iplus7 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | SIMP: (175) implies: % 16.58/3.04 | | | | | | | | | | | | | | (176) iT = iplus7 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | COMBINE_EQS: (167), (176) imply: % 16.58/3.04 | | | | | | | | | | | | | | (177) iplus7 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | SIMP: (177) implies: % 16.58/3.04 | | | | | | | | | | | | | | (178) iplus7 = iplus4 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | REDUCE: (173), (178) imply: % 16.58/3.04 | | | | | | | | | | | | | | (179) $false % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | CLOSE: (179) is inconsistent. % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | (180) iT = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | COMBINE_EQS: (167), (180) imply: % 16.58/3.04 | | | | | | | | | | | | | | (181) iplus4 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | SIMP: (181) implies: % 16.58/3.04 | | | | | | | | | | | | | | (182) iplus4 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | COMBINE_EQS: (170), (182) imply: % 16.58/3.04 | | | | | | | | | | | | | | (183) iplus6 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | REDUCE: (171), (182) imply: % 16.58/3.04 | | | | | | | | | | | | | | (184) ~ (iminus9 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | REDUCE: (173), (182) imply: % 16.58/3.04 | | | | | | | | | | | | | | (185) ~ (iplus7 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | BETA: splitting (29) gives: % 16.58/3.04 | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | (186) iminus9 = iT % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | COMBINE_EQS: (180), (186) imply: % 16.58/3.04 | | | | | | | | | | | | | | | (187) iminus9 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | REDUCE: (184), (187) imply: % 16.58/3.04 | | | | | | | | | | | | | | | (188) $false % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | CLOSE: (188) is inconsistent. % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | (189) iT = iplus3 | iT = iminus2 % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | BETA: splitting (22) gives: % 16.58/3.04 | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | (190) iF = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (75), (190) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (191) iplus7 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | REDUCE: (185), (191) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (192) $false % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | CLOSE: (192) is inconsistent. % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | (193) iF = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (75), (193) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (194) iplus7 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (94), (194) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (195) iplus5 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (74), (194) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (196) iplus3 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (76), (194) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (197) iplus8 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | COMBINE_EQS: (77), (194) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | (198) iminus6 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | BETA: splitting (189) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | (199) iT = iplus3 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | REF_CLOSE: (2), (3), (41), (42), (52), (199) are inconsistent % 16.58/3.04 | | | | | | | | | | | | | | | | | by sub-proof #14. % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | Case 2: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | (200) iT = iminus2 % 16.58/3.04 | | | | | | | | | | | | | | | | | (201) ~ (iT = iplus3) % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | COMBINE_EQS: (180), (200) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | (202) iminus2 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | SIMP: (202) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | (203) iminus2 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | REDUCE: (180), (196), (201) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | (204) ~ (iminus1 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | SIMP: (204) implies: % 16.58/3.04 | | | | | | | | | | | | | | | | | (205) ~ (iminus1 = iplus1) % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | BETA: splitting (6) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | (206) iplus8 = iminus4 % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (197), (206) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | (207) iminus4 = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | BETA: splitting (23) gives: % 16.58/3.04 | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (208) iplus8 = iT % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (197), (208) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (209) iT = iminus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (180), (209) imply: % 16.58/3.04 | | | | | | | | | | | | | | | | | | | (210) iminus1 = iplus1 % 16.58/3.04 | | | | | | | | | | | | | | | | | | | % 16.58/3.04 | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (183), (198), (205), (210) are inconsistent % 16.58/3.05 | | | | | | | | | | | | | | | | | | | by sub-proof #8. % 16.58/3.05 | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | (211) iT = iplus2 | iT = iminus4 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | BETA: splitting (16) gives: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (212) iplus5 = iminus2 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (195), (212) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (213) iminus2 = iminus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (203), (213) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (214) iminus1 = iplus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (183), (198), (205), (214) are inconsistent % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | by sub-proof #8. % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (215) iplus5 = iplus2 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (216) ~ (iplus5 = iminus2) % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (195), (215) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | (217) iplus2 = iminus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | BETA: splitting (211) gives: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | Case 1: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | (218) iT = iplus2 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (180), (218) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | (219) iplus2 = iplus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | SIMP: (219) implies: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | (220) iplus2 = iplus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (217), (220) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | (221) iminus1 = iplus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (183), (198), (205), (221) are inconsistent % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | by sub-proof #8. % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | (222) iT = iminus4 % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (180), (183), (198), (205), (207), (222) are % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | inconsistent by sub-proof #7. % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | (223) iplus8 = iplus4 % 16.58/3.05 | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (197), (223) imply: % 16.58/3.05 | | | | | | | | | | | | | | | | | | (224) iplus4 = iminus1 % 16.58/3.05 | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | | REF_CLOSE: (15), (182), (183), (198), (205), (224) are % 16.58/3.05 | | | | | | | | | | | | | | | | | | inconsistent by sub-proof #6. % 16.58/3.05 | | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | (225) iT = iplus7 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | COMBINE_EQS: (67), (225) imply: % 16.58/3.05 | | | | | | | | | (226) iminus7 = iplus7 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | SIMP: (226) implies: % 16.58/3.05 | | | | | | | | | (227) iminus7 = iplus7 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | REDUCE: (79), (227) imply: % 16.58/3.05 | | | | | | | | | (228) $false % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | CLOSE: (228) is inconsistent. % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | End of split % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | End of split % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | End of split % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | End of split % 16.58/3.05 | | | | | % 16.58/3.05 | | | | End of split % 16.58/3.05 | | | | % 16.58/3.05 | | | End of split % 16.58/3.05 | | | % 16.58/3.05 | | Case 2: % 16.58/3.05 | | | % 16.58/3.05 | | | (229) ~ (iminus8 = iT) % 16.58/3.05 | | | % 16.58/3.05 | | | REDUCE: (8), (229) imply: % 16.58/3.05 | | | (230) ~ (iminus8 = iminus3) % 16.58/3.05 | | | % 16.58/3.05 | | | BETA: splitting (38) gives: % 16.58/3.05 | | | % 16.58/3.05 | | | Case 1: % 16.58/3.05 | | | | % 16.58/3.05 | | | | (231) iminus8 = iminus3 % 16.58/3.05 | | | | % 16.58/3.05 | | | | REDUCE: (230), (231) imply: % 16.58/3.05 | | | | (232) $false % 16.58/3.05 | | | | % 16.58/3.05 | | | | CLOSE: (232) is inconsistent. % 16.58/3.05 | | | | % 16.58/3.05 | | | Case 2: % 16.58/3.05 | | | | % 16.58/3.05 | | | | (233) iplus8 = iminus3 % 16.58/3.05 | | | | % 16.58/3.05 | | | | BETA: splitting (9) gives: % 16.58/3.05 | | | | % 16.58/3.05 | | | | Case 1: % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | (234) iplus9 = iT % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | COMBINE_EQS: (8), (234) imply: % 16.58/3.05 | | | | | (235) iplus9 = iminus3 % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | REF_CLOSE: (1), (2), (3), (4), (5), (8), (10), (13), (15), (17), (19), % 16.58/3.05 | | | | | (25), (28), (30), (31), (32), (33), (37), (39), (41), (42), % 16.58/3.05 | | | | | (43), (44), (230), (233), (235) are inconsistent by % 16.58/3.05 | | | | | sub-proof #2. % 16.58/3.05 | | | | | % 16.58/3.05 | | | | Case 2: % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | (236) ~ (iplus9 = iT) % 16.58/3.05 | | | | | (237) iminus8 = iT | iT = iplus3 % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | REDUCE: (8), (236) imply: % 16.58/3.05 | | | | | (238) ~ (iplus9 = iminus3) % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | BETA: splitting (14) gives: % 16.58/3.05 | | | | | % 16.58/3.05 | | | | | Case 1: % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | (239) iplus9 = iT % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | COMBINE_EQS: (8), (239) imply: % 16.58/3.05 | | | | | | (240) iplus9 = iminus3 % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | REF_CLOSE: (1), (2), (3), (4), (5), (8), (10), (13), (15), (17), % 16.58/3.05 | | | | | | (19), (25), (28), (30), (31), (32), (33), (37), (39), % 16.58/3.05 | | | | | | (41), (42), (43), (44), (230), (233), (240) are % 16.58/3.05 | | | | | | inconsistent by sub-proof #2. % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | Case 2: % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | (241) iplus9 = iF % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | COMBINE_EQS: (5), (241) imply: % 16.58/3.05 | | | | | | (242) iplus9 = iplus3 % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | REDUCE: (238), (242) imply: % 16.58/3.05 | | | | | | (243) ~ (iminus3 = iplus3) % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | BETA: splitting (27) gives: % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | | Case 1: % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | (244) iplus9 = iT % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | COMBINE_EQS: (242), (244) imply: % 16.58/3.05 | | | | | | | (245) iT = iplus3 % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | SIMP: (245) implies: % 16.58/3.05 | | | | | | | (246) iT = iplus3 % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | COMBINE_EQS: (8), (246) imply: % 16.58/3.05 | | | | | | | (247) iminus3 = iplus3 % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | REDUCE: (41), (247) imply: % 16.58/3.05 | | | | | | | (248) $false % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | CLOSE: (248) is inconsistent. % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | Case 2: % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | (249) iminus6 = iT | iT = iplus1 % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | BETA: splitting (249) gives: % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | | Case 1: % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | (250) iminus6 = iT % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | COMBINE_EQS: (50), (250) imply: % 16.58/3.05 | | | | | | | | (251) iT = iplus3 % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | REF_CLOSE: (8), (41), (251) are inconsistent by sub-proof #5. % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | (252) iT = iplus1 % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | COMBINE_EQS: (8), (252) imply: % 16.58/3.05 | | | | | | | | (253) iminus3 = iplus1 % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | SIMP: (253) implies: % 16.58/3.05 | | | | | | | | (254) iminus3 = iplus1 % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | COMBINE_EQS: (7), (254) imply: % 16.58/3.05 | | | | | | | | (255) iplus6 = iplus1 % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | REDUCE: (230), (254) imply: % 16.58/3.05 | | | | | | | | (256) ~ (iminus8 = iplus1) % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | REDUCE: (41), (254) imply: % 16.58/3.05 | | | | | | | | (257) ~ (iplus3 = iplus1) % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | SIMP: (257) implies: % 16.58/3.05 | | | | | | | | (258) ~ (iplus3 = iplus1) % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | BETA: splitting (24) gives: % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | | Case 1: % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | (259) iplus9 = iminus1 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | COMBINE_EQS: (242), (259) imply: % 16.58/3.05 | | | | | | | | | (260) iplus3 = iminus1 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | COMBINE_EQS: (50), (260) imply: % 16.58/3.05 | | | | | | | | | (261) iminus6 = iminus1 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | REDUCE: (258), (260) imply: % 16.58/3.05 | | | | | | | | | (262) ~ (iminus1 = iplus1) % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | BETA: splitting (237) gives: % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | Case 1: % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | (263) iminus8 = iT % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | COMBINE_EQS: (252), (263) imply: % 16.58/3.05 | | | | | | | | | | (264) iminus8 = iplus1 % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | REDUCE: (256), (264) imply: % 16.58/3.05 | | | | | | | | | | (265) $false % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | CLOSE: (265) is inconsistent. % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | (266) iT = iplus3 % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | COMBINE_EQS: (252), (266) imply: % 16.58/3.05 | | | | | | | | | | (267) iplus3 = iplus1 % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | COMBINE_EQS: (260), (267) imply: % 16.58/3.05 | | | | | | | | | | (268) iminus1 = iplus1 % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | COMBINE_EQS: (261), (268) imply: % 16.58/3.05 | | | | | | | | | | (269) iminus6 = iplus1 % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | | REF_CLOSE: (15), (255), (262), (269) are inconsistent by % 16.58/3.05 | | | | | | | | | | sub-proof #13. % 16.58/3.05 | | | | | | | | | | % 16.58/3.05 | | | | | | | | | End of split % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | Case 2: % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | (270) iplus9 = iplus1 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | COMBINE_EQS: (242), (270) imply: % 16.58/3.05 | | | | | | | | | (271) iplus3 = iplus1 % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | REDUCE: (258), (271) imply: % 16.58/3.05 | | | | | | | | | (272) $false % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | | CLOSE: (272) is inconsistent. % 16.58/3.05 | | | | | | | | | % 16.58/3.05 | | | | | | | | End of split % 16.58/3.05 | | | | | | | | % 16.58/3.05 | | | | | | | End of split % 16.58/3.05 | | | | | | | % 16.58/3.05 | | | | | | End of split % 16.58/3.05 | | | | | | % 16.58/3.05 | | | | | End of split % 16.58/3.05 | | | | | % 16.58/3.05 | | | | End of split % 16.58/3.05 | | | | % 16.58/3.05 | | | End of split % 16.58/3.05 | | | % 16.58/3.05 | | End of split % 16.58/3.05 | | % 16.58/3.05 | End of split % 16.58/3.05 | % 16.58/3.05 End of proof % 16.58/3.05 % 16.58/3.05 Sub-proof #2 shows that the following formulas are inconsistent: % 16.58/3.05 ---------------------------------------------------------------- % 16.58/3.05 (1) iminus6 = iT | iT = iminus2 | iT = iplus4 % 16.58/3.05 (2) iminus8 = iT | iT = iminus3 | iT = iplus5 % 16.58/3.05 (3) iminus8 = iT | iT = iminus3 | iT = iminus5 % 16.58/3.05 (4) iminus2 = iminus1 | iminus2 = iplus1 % 16.58/3.05 (5) iF = iplus3 % 16.58/3.05 (6) iT = iminus3 % 16.58/3.05 (7) iplus8 = iminus3 % 16.58/3.05 (8) iF = iplus4 | iF = iminus4 % 16.58/3.05 (9) iT = iminus3 | iT = iminus7 | iT = iminus4 % 16.58/3.05 (10) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.05 (11) iminus9 = iT | iminus8 = iT | iT = iminus4 % 16.58/3.05 (12) iminus7 = iminus1 | iplus7 = iminus1 % 16.58/3.05 (13) iplus9 = iminus3 % 16.58/3.05 (14) iminus9 = iT | iT = iplus3 | iT = iplus4 % 16.58/3.05 (15) iplus8 = iT | iT = iminus3 | iT = iplus2 % 16.58/3.05 (16) iplus8 = iminus2 | iplus8 = iplus2 % 16.58/3.05 (17) iminus8 = iF | iplus8 = iF % 16.58/3.05 (18) iplus8 = iF | iplus8 = iT % 16.58/3.05 (19) iplus6 = iT | iT = iminus7 | iT = iminus2 % 16.58/3.05 (20) iplus9 = iF | iminus9 = iF % 16.58/3.05 (21) ~ (iminus8 = iminus3) % 16.58/3.05 (22) iT = iminus3 | iT = iminus2 | iT = iplus1 % 16.58/3.05 (23) ~ (iminus3 = iplus3) % 16.58/3.05 (24) iminus8 = iminus5 | iminus8 = iplus5 % 16.58/3.05 (25) iminus3 = iplus4 | iminus3 = iminus4 % 16.58/3.05 (26) iplus8 = iT | iT = iminus3 | iT = iplus7 % 16.58/3.05 % 16.58/3.05 Begin of proof % 16.58/3.05 | % 16.58/3.05 | BETA: splitting (17) gives: % 16.58/3.05 | % 16.58/3.05 | Case 1: % 16.58/3.05 | | % 16.58/3.05 | | (27) iminus8 = iF % 16.58/3.05 | | % 16.58/3.05 | | COMBINE_EQS: (5), (27) imply: % 16.58/3.05 | | (28) iminus8 = iplus3 % 16.58/3.05 | | % 16.58/3.05 | | REDUCE: (21), (28) imply: % 16.58/3.05 | | (29) ~ (iminus3 = iplus3) % 16.58/3.05 | | % 16.58/3.05 | | BETA: splitting (20) gives: % 16.58/3.05 | | % 16.58/3.05 | | Case 1: % 16.58/3.05 | | | % 16.58/3.05 | | | (30) iplus9 = iF % 16.58/3.05 | | | % 16.58/3.05 | | | COMBINE_EQS: (13), (30) imply: % 16.58/3.06 | | | (31) iF = iminus3 % 16.58/3.06 | | | % 16.58/3.06 | | | SIMP: (31) implies: % 16.58/3.06 | | | (32) iF = iminus3 % 16.58/3.06 | | | % 16.58/3.06 | | | REF_CLOSE: (1), (2), (3), (4), (5), (6), (9), (10), (12), (15), (16), % 16.58/3.06 | | | (17), (18), (19), (22), (23), (24), (25), (26), (32) are % 16.58/3.06 | | | inconsistent by sub-proof #10. % 16.58/3.06 | | | % 16.58/3.06 | | Case 2: % 16.58/3.06 | | | % 16.58/3.06 | | | (33) iminus9 = iF % 16.58/3.06 | | | (34) ~ (iplus9 = iF) % 16.58/3.06 | | | % 16.58/3.06 | | | COMBINE_EQS: (5), (33) imply: % 16.58/3.06 | | | (35) iminus9 = iplus3 % 16.58/3.06 | | | % 16.58/3.06 | | | BETA: splitting (14) gives: % 16.58/3.06 | | | % 16.58/3.06 | | | Case 1: % 16.58/3.06 | | | | % 16.58/3.06 | | | | (36) iminus9 = iT % 16.58/3.06 | | | | % 16.58/3.06 | | | | COMBINE_EQS: (35), (36) imply: % 16.58/3.06 | | | | (37) iT = iplus3 % 16.58/3.06 | | | | % 16.58/3.06 | | | | SIMP: (37) implies: % 16.58/3.06 | | | | (38) iT = iplus3 % 16.58/3.06 | | | | % 16.58/3.06 | | | | REF_CLOSE: (6), (23), (38) are inconsistent by sub-proof #5. % 16.58/3.06 | | | | % 16.58/3.06 | | | Case 2: % 16.58/3.06 | | | | % 16.58/3.06 | | | | (39) ~ (iminus9 = iT) % 16.58/3.06 | | | | (40) iT = iplus3 | iT = iplus4 % 16.58/3.06 | | | | % 16.58/3.06 | | | | BETA: splitting (40) gives: % 16.58/3.06 | | | | % 16.58/3.06 | | | | Case 1: % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | (41) iT = iplus3 % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | COMBINE_EQS: (6), (41) imply: % 16.58/3.06 | | | | | (42) iminus3 = iplus3 % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | REDUCE: (23), (42) imply: % 16.58/3.06 | | | | | (43) $false % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | CLOSE: (43) is inconsistent. % 16.58/3.06 | | | | | % 16.58/3.06 | | | | Case 2: % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | (44) iT = iplus4 % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | COMBINE_EQS: (6), (44) imply: % 16.58/3.06 | | | | | (45) iminus3 = iplus4 % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | REDUCE: (23), (45) imply: % 16.58/3.06 | | | | | (46) ~ (iplus3 = iplus4) % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | SIMP: (46) implies: % 16.58/3.06 | | | | | (47) ~ (iplus3 = iplus4) % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | BETA: splitting (11) gives: % 16.58/3.06 | | | | | % 16.58/3.06 | | | | | Case 1: % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | (48) iminus9 = iT % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | COMBINE_EQS: (35), (48) imply: % 16.58/3.06 | | | | | | (49) iT = iplus3 % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | SIMP: (49) implies: % 16.58/3.06 | | | | | | (50) iT = iplus3 % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | REF_CLOSE: (44), (47), (50) are inconsistent by sub-proof #4. % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | Case 2: % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | (51) iminus8 = iT | iT = iminus4 % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | BETA: splitting (51) gives: % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | | Case 1: % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | (52) iminus8 = iT % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | COMBINE_EQS: (28), (52) imply: % 16.58/3.06 | | | | | | | (53) iT = iplus3 % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | REF_CLOSE: (44), (47), (53) are inconsistent by sub-proof #4. % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | Case 2: % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | (54) iT = iminus4 % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | COMBINE_EQS: (44), (54) imply: % 16.58/3.06 | | | | | | | (55) iplus4 = iminus4 % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | SIMP: (55) implies: % 16.58/3.06 | | | | | | | (56) iplus4 = iminus4 % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | REDUCE: (47), (56) imply: % 16.58/3.06 | | | | | | | (57) ~ (iplus3 = iminus4) % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | | REF_CLOSE: (5), (8), (56), (57) are inconsistent by sub-proof #3. % 16.58/3.06 | | | | | | | % 16.58/3.06 | | | | | | End of split % 16.58/3.06 | | | | | | % 16.58/3.06 | | | | | End of split % 16.58/3.06 | | | | | % 16.58/3.06 | | | | End of split % 16.58/3.06 | | | | % 16.58/3.06 | | | End of split % 16.58/3.06 | | | % 16.58/3.06 | | End of split % 16.58/3.06 | | % 16.58/3.06 | Case 2: % 16.58/3.06 | | % 16.58/3.06 | | (58) iplus8 = iF % 16.58/3.06 | | % 16.58/3.06 | | COMBINE_EQS: (7), (58) imply: % 16.58/3.06 | | (59) iF = iminus3 % 16.58/3.06 | | % 16.58/3.06 | | REF_CLOSE: (1), (2), (3), (4), (5), (6), (9), (10), (12), (15), (16), (17), % 16.58/3.06 | | (18), (19), (22), (23), (24), (25), (26), (59) are inconsistent % 16.58/3.06 | | by sub-proof #10. % 16.58/3.06 | | % 16.58/3.06 | End of split % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #3 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iF = iplus4 | iF = iminus4 % 16.58/3.06 (2) iF = iplus3 % 16.58/3.06 (3) ~ (iplus3 = iminus4) % 16.58/3.06 (4) iplus4 = iminus4 % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | BETA: splitting (1) gives: % 16.58/3.06 | % 16.58/3.06 | Case 1: % 16.58/3.06 | | % 16.58/3.06 | | (5) iF = iminus4 % 16.58/3.06 | | % 16.58/3.06 | | COMBINE_EQS: (2), (5) imply: % 16.58/3.06 | | (6) iplus3 = iminus4 % 16.58/3.06 | | % 16.58/3.06 | | SIMP: (6) implies: % 16.58/3.06 | | (7) iplus3 = iminus4 % 16.58/3.06 | | % 16.58/3.06 | | REDUCE: (3), (7) imply: % 16.58/3.06 | | (8) $false % 16.58/3.06 | | % 16.58/3.06 | | CLOSE: (8) is inconsistent. % 16.58/3.06 | | % 16.58/3.06 | Case 2: % 16.58/3.06 | | % 16.58/3.06 | | (9) iF = iplus4 % 16.58/3.06 | | % 16.58/3.06 | | COMBINE_EQS: (2), (9) imply: % 16.58/3.06 | | (10) iplus3 = iplus4 % 16.58/3.06 | | % 16.58/3.06 | | SIMP: (10) implies: % 16.58/3.06 | | (11) iplus3 = iplus4 % 16.58/3.06 | | % 16.58/3.06 | | COMBINE_EQS: (4), (11) imply: % 16.58/3.06 | | (12) iplus3 = iminus4 % 16.58/3.06 | | % 16.58/3.06 | | REDUCE: (3), (12) imply: % 16.58/3.06 | | (13) $false % 16.58/3.06 | | % 16.58/3.06 | | CLOSE: (13) is inconsistent. % 16.58/3.06 | | % 16.58/3.06 | End of split % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #4 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iT = iplus3 % 16.58/3.06 (2) iT = iplus4 % 16.58/3.06 (3) ~ (iplus3 = iplus4) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (1), (2) imply: % 16.58/3.06 | (4) iplus3 = iplus4 % 16.58/3.06 | % 16.58/3.06 | SIMP: (4) implies: % 16.58/3.06 | (5) iplus3 = iplus4 % 16.58/3.06 | % 16.58/3.06 | REDUCE: (3), (5) imply: % 16.58/3.06 | (6) $false % 16.58/3.06 | % 16.58/3.06 | CLOSE: (6) is inconsistent. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #5 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iT = iminus3 % 16.58/3.06 (2) iT = iplus3 % 16.58/3.06 (3) ~ (iminus3 = iplus3) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (1), (2) imply: % 16.58/3.06 | (4) iminus3 = iplus3 % 16.58/3.06 | % 16.58/3.06 | SIMP: (4) implies: % 16.58/3.06 | (5) iminus3 = iplus3 % 16.58/3.06 | % 16.58/3.06 | REDUCE: (3), (5) imply: % 16.58/3.06 | (6) $false % 16.58/3.06 | % 16.58/3.06 | CLOSE: (6) is inconsistent. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #6 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iplus4 = iplus1 % 16.58/3.06 (2) iplus6 = iplus1 % 16.58/3.06 (3) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.06 (4) iplus4 = iminus1 % 16.58/3.06 (5) iminus6 = iminus1 % 16.58/3.06 (6) ~ (iminus1 = iplus1) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (1), (4) imply: % 16.58/3.06 | (7) iminus1 = iplus1 % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (5), (7) imply: % 16.58/3.06 | (8) iminus6 = iplus1 % 16.58/3.06 | % 16.58/3.06 | REF_CLOSE: (2), (3), (6), (8) are inconsistent by sub-proof #13. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #7 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iplus6 = iplus1 % 16.58/3.06 (2) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.06 (3) iT = iplus1 % 16.58/3.06 (4) iT = iminus4 % 16.58/3.06 (5) iminus6 = iminus1 % 16.58/3.06 (6) iminus4 = iminus1 % 16.58/3.06 (7) ~ (iminus1 = iplus1) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (3), (4) imply: % 16.58/3.06 | (8) iminus4 = iplus1 % 16.58/3.06 | % 16.58/3.06 | SIMP: (8) implies: % 16.58/3.06 | (9) iminus4 = iplus1 % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (6), (9) imply: % 16.58/3.06 | (10) iminus1 = iplus1 % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (5), (10) imply: % 16.58/3.06 | (11) iminus6 = iplus1 % 16.58/3.06 | % 16.58/3.06 | REF_CLOSE: (1), (2), (7), (11) are inconsistent by sub-proof #13. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #8 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iplus6 = iplus1 % 16.58/3.06 (2) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.06 (3) iminus1 = iplus1 % 16.58/3.06 (4) iminus6 = iminus1 % 16.58/3.06 (5) ~ (iminus1 = iplus1) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | SIMP: (3) implies: % 16.58/3.06 | (6) iminus1 = iplus1 % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (4), (6) imply: % 16.58/3.06 | (7) iminus6 = iplus1 % 16.58/3.06 | % 16.58/3.06 | REF_CLOSE: (1), (2), (5), (7) are inconsistent by sub-proof #13. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #9 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iT = iminus7 % 16.58/3.06 (2) iT = iplus7 % 16.58/3.06 (3) ~ (iminus7 = iplus7) % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (1), (2) imply: % 16.58/3.06 | (4) iminus7 = iplus7 % 16.58/3.06 | % 16.58/3.06 | SIMP: (4) implies: % 16.58/3.06 | (5) iminus7 = iplus7 % 16.58/3.06 | % 16.58/3.06 | REDUCE: (3), (5) imply: % 16.58/3.06 | (6) $false % 16.58/3.06 | % 16.58/3.06 | CLOSE: (6) is inconsistent. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #10 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iminus6 = iT | iT = iminus2 | iT = iplus4 % 16.58/3.06 (2) iminus8 = iT | iT = iminus3 | iT = iplus5 % 16.58/3.06 (3) iminus8 = iT | iT = iminus3 | iT = iminus5 % 16.58/3.06 (4) iminus2 = iminus1 | iminus2 = iplus1 % 16.58/3.06 (5) iF = iplus3 % 16.58/3.06 (6) iT = iminus3 % 16.58/3.06 (7) iT = iminus3 | iT = iminus7 | iT = iminus4 % 16.58/3.06 (8) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.06 (9) iF = iminus3 % 16.58/3.06 (10) iminus7 = iminus1 | iplus7 = iminus1 % 16.58/3.06 (11) iplus8 = iT | iT = iminus3 | iT = iplus2 % 16.58/3.06 (12) iplus8 = iminus2 | iplus8 = iplus2 % 16.58/3.06 (13) iminus8 = iF | iplus8 = iF % 16.58/3.06 (14) iplus8 = iF | iplus8 = iT % 16.58/3.06 (15) iplus6 = iT | iT = iminus7 | iT = iminus2 % 16.58/3.06 (16) iT = iminus3 | iT = iminus2 | iT = iplus1 % 16.58/3.06 (17) ~ (iminus3 = iplus3) % 16.58/3.06 (18) iminus8 = iminus5 | iminus8 = iplus5 % 16.58/3.06 (19) iminus3 = iplus4 | iminus3 = iminus4 % 16.58/3.06 (20) iplus8 = iT | iT = iminus3 | iT = iplus7 % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (5), (9) imply: % 16.58/3.06 | (21) iminus3 = iplus3 % 16.58/3.06 | % 16.58/3.06 | SIMP: (21) implies: % 16.58/3.06 | (22) iminus3 = iplus3 % 16.58/3.06 | % 16.58/3.06 | COMBINE_EQS: (6), (22) imply: % 16.58/3.06 | (23) iT = iplus3 % 16.58/3.06 | % 16.58/3.06 | REF_CLOSE: (1), (2), (3), (4), (7), (8), (9), (10), (11), (12), (13), (14), % 16.58/3.06 | (15), (16), (17), (18), (19), (20), (23) are inconsistent by % 16.58/3.06 | sub-proof #11. % 16.58/3.06 | % 16.58/3.06 End of proof % 16.58/3.06 % 16.58/3.06 Sub-proof #11 shows that the following formulas are inconsistent: % 16.58/3.06 ---------------------------------------------------------------- % 16.58/3.06 (1) iminus6 = iT | iT = iminus2 | iT = iplus4 % 16.58/3.06 (2) iminus8 = iT | iT = iminus3 | iT = iplus5 % 16.58/3.06 (3) iminus8 = iT | iT = iminus3 | iT = iminus5 % 16.58/3.06 (4) iminus2 = iminus1 | iminus2 = iplus1 % 16.58/3.06 (5) iT = iminus3 | iT = iminus7 | iT = iminus4 % 16.58/3.06 (6) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.06 (7) iF = iminus3 % 16.58/3.06 (8) iminus7 = iminus1 | iplus7 = iminus1 % 16.58/3.06 (9) iplus8 = iT | iT = iminus3 | iT = iplus2 % 16.58/3.06 (10) iplus8 = iminus2 | iplus8 = iplus2 % 16.58/3.06 (11) iminus8 = iF | iplus8 = iF % 16.58/3.06 (12) iplus8 = iF | iplus8 = iT % 16.58/3.06 (13) iplus6 = iT | iT = iminus7 | iT = iminus2 % 16.58/3.06 (14) iT = iplus3 % 16.58/3.06 (15) iT = iminus3 | iT = iminus2 | iT = iplus1 % 16.58/3.06 (16) ~ (iminus3 = iplus3) % 16.58/3.06 (17) iminus8 = iminus5 | iminus8 = iplus5 % 16.58/3.06 (18) iminus3 = iplus4 | iminus3 = iminus4 % 16.58/3.06 (19) iplus8 = iT | iT = iminus3 | iT = iplus7 % 16.58/3.06 % 16.58/3.06 Begin of proof % 16.58/3.06 | % 16.58/3.06 | BETA: splitting (15) gives: % 16.58/3.06 | % 16.58/3.06 | Case 1: % 16.58/3.06 | | % 16.58/3.06 | | (20) iT = iminus3 % 16.58/3.06 | | % 16.58/3.06 | | COMBINE_EQS: (14), (20) imply: % 16.58/3.06 | | (21) iminus3 = iplus3 % 16.58/3.06 | | % 16.58/3.06 | | REDUCE: (16), (21) imply: % 16.58/3.06 | | (22) $false % 16.58/3.06 | | % 16.58/3.06 | | CLOSE: (22) is inconsistent. % 16.58/3.06 | | % 16.58/3.06 | Case 2: % 16.58/3.06 | | % 16.58/3.06 | | (23) ~ (iT = iminus3) % 16.58/3.07 | | (24) iT = iminus2 | iT = iplus1 % 16.58/3.07 | | % 16.58/3.07 | | REDUCE: (14), (23) imply: % 16.58/3.07 | | (25) ~ (iminus3 = iplus3) % 16.58/3.07 | | % 16.58/3.07 | | BETA: splitting (9) gives: % 16.58/3.07 | | % 16.58/3.07 | | Case 1: % 16.58/3.07 | | | % 16.58/3.07 | | | (26) iplus8 = iT % 16.58/3.07 | | | % 16.58/3.07 | | | COMBINE_EQS: (14), (26) imply: % 16.58/3.07 | | | (27) iplus8 = iplus3 % 16.58/3.07 | | | % 16.58/3.07 | | | BETA: splitting (11) gives: % 16.58/3.07 | | | % 16.58/3.07 | | | Case 1: % 16.58/3.07 | | | | % 16.58/3.07 | | | | (28) iminus8 = iF % 16.58/3.07 | | | | % 16.58/3.07 | | | | COMBINE_EQS: (7), (28) imply: % 16.58/3.07 | | | | (29) iminus8 = iminus3 % 16.58/3.07 | | | | % 16.58/3.07 | | | | REF_CLOSE: (2), (3), (14), (16), (17), (29) are inconsistent by % 16.58/3.07 | | | | sub-proof #14. % 16.58/3.07 | | | | % 16.58/3.07 | | | Case 2: % 16.58/3.07 | | | | % 16.58/3.07 | | | | (30) iplus8 = iF % 16.58/3.07 | | | | % 16.58/3.07 | | | | COMBINE_EQS: (27), (30) imply: % 16.58/3.07 | | | | (31) iF = iplus3 % 16.58/3.07 | | | | % 16.58/3.07 | | | | SIMP: (31) implies: % 16.58/3.07 | | | | (32) iF = iplus3 % 16.58/3.07 | | | | % 16.58/3.07 | | | | COMBINE_EQS: (7), (32) imply: % 16.58/3.07 | | | | (33) iminus3 = iplus3 % 16.58/3.07 | | | | % 16.58/3.07 | | | | REDUCE: (16), (33) imply: % 16.58/3.07 | | | | (34) $false % 16.58/3.07 | | | | % 16.58/3.07 | | | | CLOSE: (34) is inconsistent. % 16.58/3.07 | | | | % 16.58/3.07 | | | End of split % 16.58/3.07 | | | % 16.58/3.07 | | Case 2: % 16.58/3.07 | | | % 16.58/3.07 | | | (35) ~ (iplus8 = iT) % 16.58/3.07 | | | (36) iT = iminus3 | iT = iplus2 % 16.58/3.07 | | | % 16.58/3.07 | | | REDUCE: (14), (35) imply: % 16.58/3.07 | | | (37) ~ (iplus8 = iplus3) % 16.58/3.07 | | | % 16.58/3.07 | | | BETA: splitting (19) gives: % 16.58/3.07 | | | % 16.58/3.07 | | | Case 1: % 16.58/3.07 | | | | % 16.58/3.07 | | | | (38) iplus8 = iT % 16.58/3.07 | | | | % 16.58/3.07 | | | | COMBINE_EQS: (14), (38) imply: % 16.58/3.07 | | | | (39) iplus8 = iplus3 % 16.58/3.07 | | | | % 16.58/3.07 | | | | REDUCE: (37), (39) imply: % 16.58/3.07 | | | | (40) $false % 16.58/3.07 | | | | % 16.58/3.07 | | | | CLOSE: (40) is inconsistent. % 16.58/3.07 | | | | % 16.58/3.07 | | | Case 2: % 16.58/3.07 | | | | % 16.58/3.07 | | | | (41) iT = iminus3 | iT = iplus7 % 16.58/3.07 | | | | % 16.58/3.07 | | | | BETA: splitting (12) gives: % 16.58/3.07 | | | | % 16.58/3.07 | | | | Case 1: % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | (42) iplus8 = iT % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | COMBINE_EQS: (14), (42) imply: % 16.58/3.07 | | | | | (43) iplus8 = iplus3 % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | REDUCE: (37), (43) imply: % 16.58/3.07 | | | | | (44) $false % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | CLOSE: (44) is inconsistent. % 16.58/3.07 | | | | | % 16.58/3.07 | | | | Case 2: % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | (45) iplus8 = iF % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | COMBINE_EQS: (7), (45) imply: % 16.58/3.07 | | | | | (46) iplus8 = iminus3 % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | BETA: splitting (36) gives: % 16.58/3.07 | | | | | % 16.58/3.07 | | | | | Case 1: % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | (47) iT = iminus3 % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | REF_CLOSE: (14), (16), (47) are inconsistent by sub-proof #15. % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | Case 2: % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | (48) iT = iplus2 % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | COMBINE_EQS: (14), (48) imply: % 16.58/3.07 | | | | | | (49) iplus3 = iplus2 % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | REDUCE: (16), (49) imply: % 16.58/3.07 | | | | | | (50) ~ (iminus3 = iplus2) % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | BETA: splitting (10) gives: % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | | Case 1: % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | (51) iplus8 = iminus2 % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | COMBINE_EQS: (46), (51) imply: % 16.58/3.07 | | | | | | | (52) iminus3 = iminus2 % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | REDUCE: (50), (52) imply: % 16.58/3.07 | | | | | | | (53) ~ (iminus2 = iplus2) % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | BETA: splitting (24) gives: % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | (54) iT = iminus2 % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | COMBINE_EQS: (48), (54) imply: % 16.58/3.07 | | | | | | | | (55) iminus2 = iplus2 % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | REDUCE: (53), (55) imply: % 16.58/3.07 | | | | | | | | (56) $false % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | CLOSE: (56) is inconsistent. % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | (57) iT = iplus1 % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | COMBINE_EQS: (48), (57) imply: % 16.58/3.07 | | | | | | | | (58) iplus2 = iplus1 % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | SIMP: (58) implies: % 16.58/3.07 | | | | | | | | (59) iplus2 = iplus1 % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | REDUCE: (53), (59) imply: % 16.58/3.07 | | | | | | | | (60) ~ (iminus2 = iplus1) % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | BETA: splitting (4) gives: % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | (61) iminus2 = iplus1 % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | REDUCE: (60), (61) imply: % 16.58/3.07 | | | | | | | | | (62) $false % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | CLOSE: (62) is inconsistent. % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | (63) iminus2 = iminus1 % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | COMBINE_EQS: (52), (63) imply: % 16.58/3.07 | | | | | | | | | (64) iminus3 = iminus1 % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | REDUCE: (60), (63) imply: % 16.58/3.07 | | | | | | | | | (65) ~ (iminus1 = iplus1) % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | BETA: splitting (41) gives: % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | (66) iT = iminus3 % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | COMBINE_EQS: (57), (66) imply: % 16.58/3.07 | | | | | | | | | | (67) iminus3 = iplus1 % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | COMBINE_EQS: (64), (67) imply: % 16.58/3.07 | | | | | | | | | | (68) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | REDUCE: (65), (68) imply: % 16.58/3.07 | | | | | | | | | | (69) $false % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | CLOSE: (69) is inconsistent. % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | (70) iT = iplus7 % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | COMBINE_EQS: (57), (70) imply: % 16.58/3.07 | | | | | | | | | | (71) iplus7 = iplus1 % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | REDUCE: (23), (57), (64) imply: % 16.58/3.07 | | | | | | | | | | (72) ~ (iminus1 = iplus1) % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | BETA: splitting (8) gives: % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | (73) iminus7 = iminus1 % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | BETA: splitting (5) gives: % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | (74) iT = iminus3 % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | COMBINE_EQS: (57), (74) imply: % 16.58/3.07 | | | | | | | | | | | | (75) iminus3 = iplus1 % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | SIMP: (75) implies: % 16.58/3.07 | | | | | | | | | | | | (76) iminus3 = iplus1 % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | COMBINE_EQS: (64), (76) imply: % 16.58/3.07 | | | | | | | | | | | | (77) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | REDUCE: (65), (77) imply: % 16.58/3.07 | | | | | | | | | | | | (78) $false % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | CLOSE: (78) is inconsistent. % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | (79) iT = iminus7 | iT = iminus4 % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | BETA: splitting (79) gives: % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | (80) iT = iminus7 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | COMBINE_EQS: (57), (80) imply: % 16.58/3.07 | | | | | | | | | | | | | (81) iminus7 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | SIMP: (81) implies: % 16.58/3.07 | | | | | | | | | | | | | (82) iminus7 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | COMBINE_EQS: (73), (82) imply: % 16.58/3.07 | | | | | | | | | | | | | (83) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | REDUCE: (65), (83) imply: % 16.58/3.07 | | | | | | | | | | | | | (84) $false % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | CLOSE: (84) is inconsistent. % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | (85) iT = iminus4 % 16.58/3.07 | | | | | | | | | | | | | (86) ~ (iT = iminus7) % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | COMBINE_EQS: (57), (85) imply: % 16.58/3.07 | | | | | | | | | | | | | (87) iminus4 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | SIMP: (87) implies: % 16.58/3.07 | | | | | | | | | | | | | (88) iminus4 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | BETA: splitting (18) gives: % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | (89) iminus3 = iminus4 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | COMBINE_EQS: (64), (89) imply: % 16.58/3.07 | | | | | | | | | | | | | | (90) iminus4 = iminus1 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | SIMP: (90) implies: % 16.58/3.07 | | | | | | | | | | | | | | (91) iminus4 = iminus1 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | COMBINE_EQS: (88), (91) imply: % 16.58/3.07 | | | | | | | | | | | | | | (92) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | REDUCE: (65), (92) imply: % 16.58/3.07 | | | | | | | | | | | | | | (93) $false % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | CLOSE: (93) is inconsistent. % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | (94) iminus3 = iplus4 % 16.58/3.07 | | | | | | | | | | | | | | (95) ~ (iminus3 = iminus4) % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | COMBINE_EQS: (64), (94) imply: % 16.58/3.07 | | | | | | | | | | | | | | (96) iplus4 = iminus1 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | SIMP: (96) implies: % 16.58/3.07 | | | | | | | | | | | | | | (97) iplus4 = iminus1 % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | BETA: splitting (13) gives: % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | (98) iplus6 = iT % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | COMBINE_EQS: (57), (98) imply: % 16.58/3.07 | | | | | | | | | | | | | | | (99) iplus6 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | BETA: splitting (1) gives: % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | (100) iminus6 = iT % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | COMBINE_EQS: (57), (100) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | (101) iminus6 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | REF_CLOSE: (6), (65), (99), (101) are inconsistent by % 16.58/3.07 | | | | | | | | | | | | | | | | sub-proof #13. % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | (102) iT = iminus2 | iT = iplus4 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | BETA: splitting (102) gives: % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | (103) iT = iminus2 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | REF_CLOSE: (57), (63), (65), (103) are inconsistent by % 16.58/3.07 | | | | | | | | | | | | | | | | | sub-proof #12. % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | (104) iT = iplus4 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | COMBINE_EQS: (57), (104) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | | (105) iplus4 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | SIMP: (105) implies: % 16.58/3.07 | | | | | | | | | | | | | | | | | (106) iplus4 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | COMBINE_EQS: (97), (106) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | | (107) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | SIMP: (107) implies: % 16.58/3.07 | | | | | | | | | | | | | | | | | (108) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | REDUCE: (65), (108) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | | (109) $false % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | | CLOSE: (109) is inconsistent. % 16.58/3.07 | | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | (110) iT = iminus7 | iT = iminus2 % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | BETA: splitting (110) gives: % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | Case 1: % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | (111) iT = iminus7 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | COMBINE_EQS: (57), (111) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | (112) iminus7 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | SIMP: (112) implies: % 16.58/3.07 | | | | | | | | | | | | | | | | (113) iminus7 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | COMBINE_EQS: (73), (113) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | (114) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | SIMP: (114) implies: % 16.58/3.07 | | | | | | | | | | | | | | | | (115) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | REDUCE: (65), (115) imply: % 16.58/3.07 | | | | | | | | | | | | | | | | (116) $false % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | CLOSE: (116) is inconsistent. % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | (117) iT = iminus2 % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | | REF_CLOSE: (57), (63), (65), (117) are inconsistent by % 16.58/3.07 | | | | | | | | | | | | | | | | sub-proof #12. % 16.58/3.07 | | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | Case 2: % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | (118) iplus7 = iminus1 % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | COMBINE_EQS: (71), (118) imply: % 16.58/3.07 | | | | | | | | | | | (119) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | SIMP: (119) implies: % 16.58/3.07 | | | | | | | | | | | (120) iminus1 = iplus1 % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | REDUCE: (65), (120) imply: % 16.58/3.07 | | | | | | | | | | | (121) $false % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | | CLOSE: (121) is inconsistent. % 16.58/3.07 | | | | | | | | | | | % 16.58/3.07 | | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | | % 16.58/3.07 | | | | | | | | | End of split % 16.58/3.07 | | | | | | | | | % 16.58/3.07 | | | | | | | | End of split % 16.58/3.07 | | | | | | | | % 16.58/3.07 | | | | | | | End of split % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | Case 2: % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | (122) iplus8 = iplus2 % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | COMBINE_EQS: (46), (122) imply: % 16.58/3.07 | | | | | | | (123) iminus3 = iplus2 % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | REDUCE: (50), (123) imply: % 16.58/3.07 | | | | | | | (124) $false % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | | CLOSE: (124) is inconsistent. % 16.58/3.07 | | | | | | | % 16.58/3.07 | | | | | | End of split % 16.58/3.07 | | | | | | % 16.58/3.07 | | | | | End of split % 16.58/3.07 | | | | | % 16.58/3.07 | | | | End of split % 16.58/3.07 | | | | % 16.58/3.07 | | | End of split % 16.58/3.07 | | | % 16.58/3.07 | | End of split % 16.58/3.07 | | % 16.58/3.07 | End of split % 16.58/3.07 | % 16.58/3.07 End of proof % 16.58/3.07 % 16.58/3.07 Sub-proof #12 shows that the following formulas are inconsistent: % 16.58/3.07 ---------------------------------------------------------------- % 16.58/3.07 (1) iT = iminus2 % 16.58/3.07 (2) iT = iplus1 % 16.58/3.07 (3) iminus2 = iminus1 % 16.58/3.07 (4) ~ (iminus1 = iplus1) % 16.58/3.07 % 16.58/3.07 Begin of proof % 16.58/3.07 | % 16.58/3.07 | COMBINE_EQS: (1), (2) imply: % 16.58/3.07 | (5) iminus2 = iplus1 % 16.58/3.07 | % 16.58/3.07 | SIMP: (5) implies: % 16.58/3.07 | (6) iminus2 = iplus1 % 16.58/3.07 | % 16.58/3.07 | COMBINE_EQS: (3), (6) imply: % 16.58/3.07 | (7) iminus1 = iplus1 % 16.58/3.07 | % 16.58/3.07 | SIMP: (7) implies: % 16.58/3.07 | (8) iminus1 = iplus1 % 16.58/3.07 | % 16.58/3.07 | REDUCE: (4), (8) imply: % 16.58/3.07 | (9) $false % 16.58/3.07 | % 16.58/3.07 | CLOSE: (9) is inconsistent. % 16.58/3.07 | % 16.58/3.07 End of proof % 16.58/3.07 % 16.58/3.07 Sub-proof #13 shows that the following formulas are inconsistent: % 16.58/3.07 ---------------------------------------------------------------- % 16.58/3.07 (1) iplus6 = iminus1 | iminus6 = iminus1 % 16.58/3.07 (2) iplus6 = iplus1 % 16.58/3.07 (3) ~ (iminus1 = iplus1) % 16.58/3.07 (4) iminus6 = iplus1 % 16.58/3.07 % 16.58/3.07 Begin of proof % 16.58/3.07 | % 16.58/3.07 | BETA: splitting (1) gives: % 16.58/3.07 | % 16.58/3.07 | Case 1: % 16.58/3.07 | | % 16.58/3.07 | | (5) iplus6 = iminus1 % 16.58/3.07 | | % 16.58/3.07 | | COMBINE_EQS: (2), (5) imply: % 16.58/3.07 | | (6) iminus1 = iplus1 % 16.58/3.07 | | % 16.58/3.07 | | SIMP: (6) implies: % 16.58/3.07 | | (7) iminus1 = iplus1 % 16.58/3.07 | | % 16.58/3.07 | | REDUCE: (3), (7) imply: % 16.58/3.07 | | (8) $false % 16.58/3.07 | | % 16.58/3.07 | | CLOSE: (8) is inconsistent. % 16.58/3.07 | | % 16.58/3.07 | Case 2: % 16.58/3.07 | | % 16.58/3.07 | | (9) iminus6 = iminus1 % 16.58/3.07 | | % 16.58/3.07 | | COMBINE_EQS: (4), (9) imply: % 16.58/3.07 | | (10) iminus1 = iplus1 % 16.58/3.07 | | % 16.58/3.07 | | SIMP: (10) implies: % 16.58/3.07 | | (11) iminus1 = iplus1 % 16.58/3.07 | | % 16.58/3.07 | | REDUCE: (3), (11) imply: % 16.58/3.07 | | (12) $false % 16.58/3.07 | | % 16.58/3.07 | | CLOSE: (12) is inconsistent. % 16.58/3.07 | | % 16.58/3.07 | End of split % 16.58/3.07 | % 16.58/3.07 End of proof % 16.58/3.07 % 16.58/3.07 Sub-proof #14 shows that the following formulas are inconsistent: % 16.58/3.07 ---------------------------------------------------------------- % 16.58/3.07 (1) iminus8 = iT | iT = iminus3 | iT = iplus5 % 16.58/3.07 (2) iminus8 = iT | iT = iminus3 | iT = iminus5 % 16.58/3.07 (3) iT = iplus3 % 16.58/3.07 (4) iminus8 = iminus3 % 16.58/3.07 (5) ~ (iminus3 = iplus3) % 16.58/3.07 (6) iminus8 = iminus5 | iminus8 = iplus5 % 16.58/3.07 % 16.58/3.07 Begin of proof % 16.58/3.07 | % 16.58/3.07 | BETA: splitting (1) gives: % 16.58/3.07 | % 16.58/3.07 | Case 1: % 16.58/3.07 | | % 16.58/3.07 | | (7) iminus8 = iT % 16.58/3.07 | | % 16.58/3.07 | | COMBINE_EQS: (4), (7) imply: % 16.58/3.07 | | (8) iT = iminus3 % 16.58/3.07 | | % 16.58/3.07 | | SIMP: (8) implies: % 16.58/3.07 | | (9) iT = iminus3 % 16.58/3.07 | | % 16.58/3.07 | | COMBINE_EQS: (3), (9) imply: % 16.58/3.07 | | (10) iminus3 = iplus3 % 16.58/3.07 | | % 16.58/3.07 | | REDUCE: (5), (10) imply: % 16.58/3.07 | | (11) $false % 16.58/3.07 | | % 16.58/3.07 | | CLOSE: (11) is inconsistent. % 16.58/3.07 | | % 16.58/3.07 | Case 2: % 16.58/3.07 | | % 16.58/3.07 | | (12) ~ (iminus8 = iT) % 16.58/3.07 | | (13) iT = iminus3 | iT = iplus5 % 16.58/3.07 | | % 16.58/3.07 | | BETA: splitting (13) gives: % 16.58/3.07 | | % 16.58/3.07 | | Case 1: % 16.58/3.07 | | | % 16.58/3.07 | | | (14) iT = iminus3 % 16.58/3.07 | | | % 16.58/3.07 | | | REF_CLOSE: (3), (5), (14) are inconsistent by sub-proof #15. % 16.58/3.07 | | | % 16.58/3.08 | | Case 2: % 16.58/3.08 | | | % 16.58/3.08 | | | (15) iT = iplus5 % 16.58/3.08 | | | % 16.58/3.08 | | | COMBINE_EQS: (3), (15) imply: % 16.58/3.08 | | | (16) iplus3 = iplus5 % 16.58/3.08 | | | % 16.58/3.08 | | | REDUCE: (5), (16) imply: % 16.58/3.08 | | | (17) ~ (iminus3 = iplus5) % 16.58/3.08 | | | % 16.58/3.08 | | | BETA: splitting (6) gives: % 16.58/3.08 | | | % 16.58/3.08 | | | Case 1: % 16.58/3.08 | | | | % 16.58/3.08 | | | | (18) iminus8 = iminus5 % 16.58/3.08 | | | | % 16.58/3.08 | | | | COMBINE_EQS: (4), (18) imply: % 16.58/3.08 | | | | (19) iminus3 = iminus5 % 16.58/3.08 | | | | % 16.58/3.08 | | | | REDUCE: (17), (19) imply: % 16.58/3.08 | | | | (20) ~ (iminus5 = iplus5) % 16.58/3.08 | | | | % 16.58/3.08 | | | | BETA: splitting (2) gives: % 16.58/3.08 | | | | % 16.58/3.08 | | | | Case 1: % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | (21) iminus8 = iT % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | COMBINE_EQS: (18), (21) imply: % 16.58/3.08 | | | | | (22) iT = iminus5 % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | SIMP: (22) implies: % 16.58/3.08 | | | | | (23) iT = iminus5 % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | COMBINE_EQS: (15), (23) imply: % 16.58/3.08 | | | | | (24) iminus5 = iplus5 % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | SIMP: (24) implies: % 16.58/3.08 | | | | | (25) iminus5 = iplus5 % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | REDUCE: (20), (25) imply: % 16.58/3.08 | | | | | (26) $false % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | CLOSE: (26) is inconsistent. % 16.58/3.08 | | | | | % 16.58/3.08 | | | | Case 2: % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | (27) iT = iminus3 | iT = iminus5 % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | BETA: splitting (27) gives: % 16.58/3.08 | | | | | % 16.58/3.08 | | | | | Case 1: % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | (28) iT = iminus3 % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | COMBINE_EQS: (15), (28) imply: % 16.58/3.08 | | | | | | (29) iminus3 = iplus5 % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | COMBINE_EQS: (19), (29) imply: % 16.58/3.08 | | | | | | (30) iminus5 = iplus5 % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | REDUCE: (20), (30) imply: % 16.58/3.08 | | | | | | (31) $false % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | CLOSE: (31) is inconsistent. % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | Case 2: % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | (32) iT = iminus5 % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | COMBINE_EQS: (15), (32) imply: % 16.58/3.08 | | | | | | (33) iminus5 = iplus5 % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | REDUCE: (20), (33) imply: % 16.58/3.08 | | | | | | (34) $false % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | | CLOSE: (34) is inconsistent. % 16.58/3.08 | | | | | | % 16.58/3.08 | | | | | End of split % 16.58/3.08 | | | | | % 16.58/3.08 | | | | End of split % 16.58/3.08 | | | | % 16.58/3.08 | | | Case 2: % 16.58/3.08 | | | | % 16.58/3.08 | | | | (35) iminus8 = iplus5 % 16.58/3.08 | | | | % 16.58/3.08 | | | | COMBINE_EQS: (4), (35) imply: % 16.58/3.08 | | | | (36) iminus3 = iplus5 % 16.58/3.08 | | | | % 16.58/3.08 | | | | REDUCE: (17), (36) imply: % 16.58/3.08 | | | | (37) $false % 16.58/3.08 | | | | % 16.58/3.08 | | | | CLOSE: (37) is inconsistent. % 16.58/3.08 | | | | % 16.58/3.08 | | | End of split % 16.58/3.08 | | | % 16.58/3.08 | | End of split % 16.58/3.08 | | % 16.58/3.08 | End of split % 16.58/3.08 | % 16.58/3.08 End of proof % 16.58/3.08 % 16.58/3.08 Sub-proof #15 shows that the following formulas are inconsistent: % 16.58/3.08 ---------------------------------------------------------------- % 16.58/3.08 (1) iT = iminus3 % 16.58/3.08 (2) iT = iplus3 % 16.58/3.08 (3) ~ (iminus3 = iplus3) % 16.58/3.08 % 16.58/3.08 Begin of proof % 16.58/3.08 | % 16.58/3.08 | COMBINE_EQS: (1), (2) imply: % 16.58/3.08 | (4) iminus3 = iplus3 % 16.58/3.08 | % 16.58/3.08 | SIMP: (4) implies: % 16.58/3.08 | (5) iminus3 = iplus3 % 16.58/3.08 | % 16.58/3.08 | REDUCE: (3), (5) imply: % 16.58/3.08 | (6) $false % 16.58/3.08 | % 16.58/3.08 | CLOSE: (6) is inconsistent. % 16.58/3.08 | % 16.58/3.08 End of proof % 16.58/3.08 % SZS output end Proof for theBenchmark % 16.58/3.08 % 16.58/3.08 2473ms %------------------------------------------------------------------------------