%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ALG073+1 : TPTP v8.1.2. Released v2.7.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 16:36:12 EDT 2023 % Result : Theorem 7.78s 1.79s % Output : Proof 13.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG073+1 : TPTP v8.1.2. Released v2.7.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Aug 28 03:21:17 EDT 2023 % 0.12/0.34 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.60 ___ __ \_________(_)________________________________ % 0.20/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.60 (2023-06-19) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2023 % 0.20/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.60 Amanda Stjerna. % 0.20/0.60 Free software under BSD-3-Clause. % 0.20/0.60 % 0.20/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.60 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.61 Running up to 7 provers in parallel. % 0.20/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.00/1.02 Prover 4: Preprocessing ... % 2.00/1.02 Prover 1: Preprocessing ... % 2.59/1.06 Prover 3: Preprocessing ... % 2.59/1.06 Prover 2: Preprocessing ... % 2.59/1.06 Prover 5: Preprocessing ... % 2.59/1.06 Prover 0: Preprocessing ... % 2.59/1.06 Prover 6: Preprocessing ... % 4.11/1.34 Prover 1: Constructing countermodel ... % 4.11/1.34 Prover 3: Constructing countermodel ... % 4.11/1.34 Prover 6: Proving ... % 4.75/1.38 Prover 5: Constructing countermodel ... % 4.75/1.45 Prover 2: Proving ... % 5.18/1.49 Prover 4: Constructing countermodel ... % 5.18/1.51 Prover 3: gave up % 5.18/1.51 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 5.91/1.53 Prover 0: Proving ... % 5.91/1.53 Prover 1: gave up % 6.00/1.55 Prover 7: Preprocessing ... % 6.00/1.55 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 6.00/1.58 Prover 8: Preprocessing ... % 6.51/1.65 Prover 8: Warning: ignoring some quantifiers % 6.51/1.67 Prover 7: Constructing countermodel ... % 6.96/1.68 Prover 8: Constructing countermodel ... % 6.96/1.72 Prover 7: gave up % 6.96/1.73 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 6.96/1.75 Prover 9: Preprocessing ... % 7.78/1.79 Prover 5: proved (1172ms) % 7.78/1.79 % 7.78/1.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.78/1.79 % 7.78/1.80 Prover 2: stopped % 7.78/1.80 Prover 6: stopped % 7.78/1.82 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 7.78/1.82 Prover 0: stopped % 7.78/1.82 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 7.78/1.82 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.07/1.83 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 8.07/1.83 Prover 11: Preprocessing ... % 8.07/1.83 Prover 10: Preprocessing ... % 8.14/1.83 Prover 13: Preprocessing ... % 8.14/1.84 Prover 16: Preprocessing ... % 8.14/1.87 Prover 10: Constructing countermodel ... % 8.14/1.88 Prover 10: gave up % 8.14/1.89 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 8.14/1.89 Prover 16: Constructing countermodel ... % 8.14/1.90 Prover 9: Constructing countermodel ... % 8.68/1.91 Prover 9: stopped % 8.68/1.92 Prover 13: Constructing countermodel ... % 8.68/1.93 Prover 19: Preprocessing ... % 9.12/2.02 Prover 19: Warning: ignoring some quantifiers % 9.12/2.04 Prover 19: Constructing countermodel ... % 9.12/2.04 Prover 11: Constructing countermodel ... % 12.88/2.51 Prover 13: Found proof (size 277) % 12.88/2.51 Prover 13: proved (687ms) % 12.88/2.51 Prover 11: stopped % 12.88/2.51 Prover 16: stopped % 12.88/2.51 Prover 8: stopped % 12.88/2.51 Prover 4: stopped % 12.88/2.51 Prover 19: stopped % 12.88/2.51 % 12.88/2.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 12.88/2.51 % 13.42/2.61 % SZS output start Proof for theBenchmark % 13.42/2.61 Assumptions after simplification: % 13.42/2.61 --------------------------------- % 13.42/2.61 % 13.42/2.61 (ax1) % 13.42/2.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (op1(v0, v1) = v2) | ~ $i(v1) | % 13.42/2.64 ~ $i(v0) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) & ! [v0: $i] : ! % 13.42/2.64 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sorti1(v1) | ~ sorti1(v0) | ? [v2: % 13.42/2.64 $i] : (op1(v0, v1) = v2 & $i(v2) & sorti1(v2))) % 13.42/2.64 % 13.42/2.64 (ax2) % 13.42/2.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (op2(v0, v1) = v2) | ~ $i(v1) | % 13.42/2.64 ~ $i(v0) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) & ! [v0: $i] : ! % 13.42/2.64 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sorti2(v1) | ~ sorti2(v0) | ? [v2: % 13.42/2.64 $i] : (op2(v0, v1) = v2 & $i(v2) & sorti2(v2))) % 13.42/2.64 % 13.42/2.64 (ax3) % 13.42/2.64 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = v0) & op1(v1, v1) = v0 & % 13.42/2.64 op1(v0, v1) = v2 & op1(v0, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & sorti1(v1) % 13.42/2.64 & sorti1(v0)) % 13.42/2.64 % 13.42/2.64 (ax4) % 13.42/2.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (op2(v0, v1) = v2) | % 13.42/2.64 ~ (op2(v0, v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ sorti2(v1) | ~ sorti2(v0) % 13.42/2.64 | ? [v3: $i] : ( ~ (v3 = v0) & op2(v1, v1) = v3 & $i(v3))) & ! [v0: $i] : % 13.42/2.64 ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : (op2(v0, v0) = v1 & $i(v1) & ( ~ % 13.42/2.64 sorti2(v1) | ? [v2: $i] : ? [v3: $i] : (op2(v1, v1) = v2 & op2(v0, v1) % 13.42/2.64 = v3 & $i(v3) & $i(v2) & ( ~ (v2 = v0) | v3 = v0))))) % 13.42/2.64 % 13.42/2.64 (co1) % 13.42/2.65 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 13.42/2.65 (j(v2) = v3) | ~ (j(v0) = v1) | ~ (op1(v1, v3) = v4) | ~ $i(v2) | ~ % 13.42/2.65 $i(v0) | ~ sorti2(v2) | ~ sorti2(v0) | ? [v5: $i] : (j(v5) = v4 & op2(v0, % 13.42/2.65 v2) = v5 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 13.42/2.65 ! [v3: $i] : ! [v4: $i] : ( ~ (h(v2) = v3) | ~ (h(v0) = v1) | ~ (op2(v1, % 13.42/2.65 v3) = v4) | ~ $i(v2) | ~ $i(v0) | ~ sorti1(v2) | ~ sorti1(v0) | ? % 13.42/2.65 [v5: $i] : (h(v5) = v4 & op1(v0, v2) = v5 & $i(v5) & $i(v4))) & ! [v0: $i] % 13.42/2.65 : ! [v1: $i] : ( ~ (j(v0) = v1) | ~ $i(v0) | ~ sorti2(v0) | h(v1) = v0) & % 13.42/2.65 ! [v0: $i] : ! [v1: $i] : ( ~ (j(v0) = v1) | ~ $i(v0) | ~ sorti2(v0) | % 13.42/2.65 sorti1(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (h(v0) = v1) | ~ $i(v0) | ~ % 13.42/2.65 sorti1(v0) | j(v1) = v0) & ! [v0: $i] : ! [v1: $i] : ( ~ (h(v0) = v1) | ~ % 13.42/2.65 $i(v0) | ~ sorti1(v0) | sorti2(v1)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 13.42/2.65 sorti2(v0) | ? [v1: $i] : (j(v0) = v1 & h(v1) = v0 & $i(v1))) & ! [v0: $i] % 13.42/2.65 : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : (j(v0) = v1 & $i(v1) & % 13.42/2.65 sorti1(v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : % 13.42/2.65 (j(v0) = v1 & $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ sorti2(v2) | ? [v3: % 13.42/2.65 $i] : ? [v4: $i] : ? [v5: $i] : (j(v3) = v4 & j(v2) = v5 & op2(v0, % 13.42/2.65 v2) = v3 & op1(v1, v5) = v4 & $i(v5) & $i(v4) & $i(v3))))) & ! [v0: % 13.42/2.65 $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : (j(v1) = v0 & h(v0) = v1 & % 13.42/2.65 $i(v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : (h(v0) % 13.42/2.65 = v1 & $i(v1) & sorti2(v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | % 13.42/2.65 ? [v1: $i] : (h(v0) = v1 & $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ sorti1(v2) % 13.42/2.65 | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : (h(v3) = v4 & h(v2) = v5 & % 13.42/2.65 op2(v1, v5) = v4 & op1(v0, v2) = v3 & $i(v5) & $i(v4) & $i(v3))))) % 13.42/2.65 % 13.42/2.65 (function-axioms) % 13.42/2.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (op2(v3, % 13.42/2.66 v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 13.42/2.66 $i] : ! [v3: $i] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = % 13.42/2.66 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (j(v2) = % 13.42/2.66 v1) | ~ (j(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 13.42/2.66 v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 13.42/2.66 % 13.42/2.66 Those formulas are unsatisfiable: % 13.42/2.66 --------------------------------- % 13.42/2.66 % 13.42/2.66 Begin of proof % 13.42/2.66 | % 13.42/2.66 | ALPHA: (ax1) implies: % 13.42/2.66 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sorti1(v1) | ~ % 13.42/2.66 | sorti1(v0) | ? [v2: $i] : (op1(v0, v1) = v2 & $i(v2) & sorti1(v2))) % 13.42/2.66 | % 13.42/2.66 | ALPHA: (ax2) implies: % 13.42/2.66 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ sorti2(v1) | ~ % 13.42/2.66 | sorti2(v0) | ? [v2: $i] : (op2(v0, v1) = v2 & $i(v2) & sorti2(v2))) % 13.42/2.66 | % 13.42/2.66 | ALPHA: (ax4) implies: % 13.42/2.66 | (3) ! [v0: $i] : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : (op2(v0, v0) = % 13.42/2.66 | v1 & $i(v1) & ( ~ sorti2(v1) | ? [v2: $i] : ? [v3: $i] : (op2(v1, % 13.42/2.66 | v1) = v2 & op2(v0, v1) = v3 & $i(v3) & $i(v2) & ( ~ (v2 = v0) % 13.42/2.66 | | v3 = v0))))) % 13.42/2.66 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (op2(v0, v1) = % 13.42/2.66 | v2) | ~ (op2(v0, v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ sorti2(v1) % 13.42/2.66 | | ~ sorti2(v0) | ? [v3: $i] : ( ~ (v3 = v0) & op2(v1, v1) = v3 & % 13.42/2.66 | $i(v3))) % 13.42/2.66 | % 13.42/2.66 | ALPHA: (co1) implies: % 13.42/2.66 | (5) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : (h(v0) = v1 & % 13.42/2.66 | $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ sorti1(v2) | ? [v3: $i] : % 13.42/2.66 | ? [v4: $i] : ? [v5: $i] : (h(v3) = v4 & h(v2) = v5 & op2(v1, v5) % 13.42/2.66 | = v4 & op1(v0, v2) = v3 & $i(v5) & $i(v4) & $i(v3))))) % 13.42/2.66 | (6) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : (h(v0) = v1 & % 13.42/2.66 | $i(v1) & sorti2(v1))) % 13.42/2.66 | (7) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : (j(v1) = v0 & % 13.42/2.66 | h(v0) = v1 & $i(v1))) % 13.42/2.67 | (8) ! [v0: $i] : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : (j(v0) = v1 & % 13.42/2.67 | $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ sorti2(v2) | ? [v3: $i] : % 13.42/2.67 | ? [v4: $i] : ? [v5: $i] : (j(v3) = v4 & j(v2) = v5 & op2(v0, v2) % 13.42/2.67 | = v3 & op1(v1, v5) = v4 & $i(v5) & $i(v4) & $i(v3))))) % 13.42/2.67 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 13.42/2.67 | ~ (j(v2) = v3) | ~ (j(v0) = v1) | ~ (op1(v1, v3) = v4) | ~ $i(v2) % 13.42/2.67 | | ~ $i(v0) | ~ sorti2(v2) | ~ sorti2(v0) | ? [v5: $i] : (j(v5) = % 13.42/2.67 | v4 & op2(v0, v2) = v5 & $i(v5) & $i(v4))) % 13.42/2.67 | % 13.42/2.67 | ALPHA: (function-axioms) implies: % 13.42/2.67 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (h(v2) = v1) | % 13.42/2.67 | ~ (h(v2) = v0)) % 13.42/2.67 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (j(v2) = v1) | % 13.42/2.67 | ~ (j(v2) = v0)) % 13.42/2.67 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 13.42/2.67 | (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 13.42/2.67 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 13.42/2.67 | (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 13.42/2.67 | % 13.42/2.67 | DELTA: instantiating (ax3) with fresh symbols all_7_0, all_7_1, all_7_2 gives: % 13.42/2.67 | (14) ~ (all_7_0 = all_7_2) & op1(all_7_1, all_7_1) = all_7_2 & % 13.42/2.67 | op1(all_7_2, all_7_1) = all_7_0 & op1(all_7_2, all_7_2) = all_7_1 & % 13.42/2.67 | $i(all_7_0) & $i(all_7_1) & $i(all_7_2) & sorti1(all_7_1) & % 13.42/2.67 | sorti1(all_7_2) % 13.42/2.67 | % 13.42/2.67 | ALPHA: (14) implies: % 13.42/2.67 | (15) ~ (all_7_0 = all_7_2) % 13.42/2.67 | (16) sorti1(all_7_2) % 13.42/2.67 | (17) sorti1(all_7_1) % 13.42/2.67 | (18) $i(all_7_2) % 13.42/2.67 | (19) $i(all_7_1) % 13.42/2.68 | (20) op1(all_7_2, all_7_2) = all_7_1 % 13.42/2.68 | (21) op1(all_7_2, all_7_1) = all_7_0 % 13.42/2.68 | (22) op1(all_7_1, all_7_1) = all_7_2 % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (7) with all_7_2, simplifying with (16), (18) % 13.42/2.68 | gives: % 13.42/2.68 | (23) ? [v0: $i] : (j(v0) = all_7_2 & h(all_7_2) = v0 & $i(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (6) with all_7_2, simplifying with (16), (18) % 13.42/2.68 | gives: % 13.42/2.68 | (24) ? [v0: $i] : (h(all_7_2) = v0 & $i(v0) & sorti2(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (5) with all_7_2, simplifying with (16), (18) % 13.42/2.68 | gives: % 13.42/2.68 | (25) ? [v0: $i] : (h(all_7_2) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.68 | ~ sorti1(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (h(v2) = % 13.42/2.68 | v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_7_2, v1) = v2 & % 13.42/2.68 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (1) with all_7_2, all_7_1, simplifying with (16), % 13.42/2.68 | (17), (18), (19) gives: % 13.42/2.68 | (26) ? [v0: $i] : (op1(all_7_2, all_7_1) = v0 & $i(v0) & sorti1(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (1) with all_7_1, all_7_2, simplifying with (16), % 13.42/2.68 | (17), (18), (19) gives: % 13.42/2.68 | (27) ? [v0: $i] : (op1(all_7_1, all_7_2) = v0 & $i(v0) & sorti1(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (7) with all_7_1, simplifying with (17), (19) % 13.42/2.68 | gives: % 13.42/2.68 | (28) ? [v0: $i] : (j(v0) = all_7_1 & h(all_7_1) = v0 & $i(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (6) with all_7_1, simplifying with (17), (19) % 13.42/2.68 | gives: % 13.42/2.68 | (29) ? [v0: $i] : (h(all_7_1) = v0 & $i(v0) & sorti2(v0)) % 13.42/2.68 | % 13.42/2.68 | GROUND_INST: instantiating (5) with all_7_1, simplifying with (17), (19) % 13.42/2.68 | gives: % 13.42/2.68 | (30) ? [v0: $i] : (h(all_7_1) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.68 | ~ sorti1(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (h(v2) = % 13.42/2.68 | v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_7_1, v1) = v2 & % 13.42/2.68 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.68 | % 13.42/2.68 | DELTA: instantiating (29) with fresh symbol all_15_0 gives: % 13.42/2.68 | (31) h(all_7_1) = all_15_0 & $i(all_15_0) & sorti2(all_15_0) % 13.42/2.68 | % 13.42/2.68 | ALPHA: (31) implies: % 13.42/2.68 | (32) sorti2(all_15_0) % 13.42/2.68 | (33) h(all_7_1) = all_15_0 % 13.42/2.68 | % 13.42/2.68 | DELTA: instantiating (28) with fresh symbol all_17_0 gives: % 13.42/2.68 | (34) j(all_17_0) = all_7_1 & h(all_7_1) = all_17_0 & $i(all_17_0) % 13.42/2.68 | % 13.42/2.68 | ALPHA: (34) implies: % 13.42/2.68 | (35) h(all_7_1) = all_17_0 % 13.42/2.68 | (36) j(all_17_0) = all_7_1 % 13.42/2.68 | % 13.42/2.68 | DELTA: instantiating (27) with fresh symbol all_19_0 gives: % 13.42/2.68 | (37) op1(all_7_1, all_7_2) = all_19_0 & $i(all_19_0) & sorti1(all_19_0) % 13.42/2.68 | % 13.42/2.68 | ALPHA: (37) implies: % 13.42/2.68 | (38) sorti1(all_19_0) % 13.42/2.68 | (39) op1(all_7_1, all_7_2) = all_19_0 % 13.42/2.68 | % 13.42/2.68 | DELTA: instantiating (26) with fresh symbol all_21_0 gives: % 13.42/2.68 | (40) op1(all_7_2, all_7_1) = all_21_0 & $i(all_21_0) & sorti1(all_21_0) % 13.42/2.68 | % 13.42/2.68 | ALPHA: (40) implies: % 13.42/2.68 | (41) sorti1(all_21_0) % 13.42/2.68 | (42) $i(all_21_0) % 13.42/2.68 | (43) op1(all_7_2, all_7_1) = all_21_0 % 13.42/2.68 | % 13.42/2.68 | DELTA: instantiating (24) with fresh symbol all_23_0 gives: % 13.42/2.69 | (44) h(all_7_2) = all_23_0 & $i(all_23_0) & sorti2(all_23_0) % 13.42/2.69 | % 13.42/2.69 | ALPHA: (44) implies: % 13.42/2.69 | (45) sorti2(all_23_0) % 13.42/2.69 | (46) h(all_7_2) = all_23_0 % 13.42/2.69 | % 13.42/2.69 | DELTA: instantiating (23) with fresh symbol all_25_0 gives: % 13.42/2.69 | (47) j(all_25_0) = all_7_2 & h(all_7_2) = all_25_0 & $i(all_25_0) % 13.42/2.69 | % 13.42/2.69 | ALPHA: (47) implies: % 13.42/2.69 | (48) h(all_7_2) = all_25_0 % 13.42/2.69 | (49) j(all_25_0) = all_7_2 % 13.42/2.69 | % 13.42/2.69 | DELTA: instantiating (30) with fresh symbol all_27_0 gives: % 13.42/2.69 | (50) h(all_7_1) = all_27_0 & $i(all_27_0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 13.42/2.69 | sorti1(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (h(v1) = v2 & % 13.42/2.69 | h(v0) = v3 & op2(all_27_0, v3) = v2 & op1(all_7_1, v0) = v1 & % 13.42/2.69 | $i(v3) & $i(v2) & $i(v1))) % 13.42/2.69 | % 13.42/2.69 | ALPHA: (50) implies: % 13.42/2.69 | (51) h(all_7_1) = all_27_0 % 13.42/2.69 | (52) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] : % 13.42/2.69 | ? [v3: $i] : (h(v1) = v2 & h(v0) = v3 & op2(all_27_0, v3) = v2 & % 13.42/2.69 | op1(all_7_1, v0) = v1 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.69 | % 13.42/2.69 | GROUND_INST: instantiating (52) with all_7_2, simplifying with (16), (18) % 13.42/2.69 | gives: % 13.42/2.69 | (53) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_2) = % 13.42/2.69 | v2 & op2(all_27_0, v2) = v1 & op1(all_7_1, all_7_2) = v0 & $i(v2) & % 13.42/2.69 | $i(v1) & $i(v0)) % 13.42/2.69 | % 13.42/2.69 | GROUND_INST: instantiating (52) with all_7_1, simplifying with (17), (19) % 13.42/2.69 | gives: % 13.42/2.69 | (54) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_1) = % 13.42/2.69 | v2 & op2(all_27_0, v2) = v1 & op1(all_7_1, all_7_1) = v0 & $i(v2) & % 13.42/2.69 | $i(v1) & $i(v0)) % 13.42/2.69 | % 13.42/2.69 | DELTA: instantiating (25) with fresh symbol all_30_0 gives: % 13.42/2.69 | (55) h(all_7_2) = all_30_0 & $i(all_30_0) & ! [v0: $i] : ( ~ $i(v0) | ~ % 13.42/2.69 | sorti1(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (h(v1) = v2 & % 13.42/2.69 | h(v0) = v3 & op2(all_30_0, v3) = v2 & op1(all_7_2, v0) = v1 & % 13.42/2.69 | $i(v3) & $i(v2) & $i(v1))) % 13.42/2.69 | % 13.42/2.69 | ALPHA: (55) implies: % 13.42/2.69 | (56) h(all_7_2) = all_30_0 % 13.42/2.69 | (57) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] : % 13.42/2.69 | ? [v3: $i] : (h(v1) = v2 & h(v0) = v3 & op2(all_30_0, v3) = v2 & % 13.42/2.69 | op1(all_7_2, v0) = v1 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.69 | % 13.42/2.69 | GROUND_INST: instantiating (57) with all_7_2, simplifying with (16), (18) % 13.42/2.69 | gives: % 13.42/2.69 | (58) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_2) = % 13.42/2.69 | v2 & op2(all_30_0, v2) = v1 & op1(all_7_2, all_7_2) = v0 & $i(v2) & % 13.42/2.69 | $i(v1) & $i(v0)) % 13.42/2.69 | % 13.42/2.69 | GROUND_INST: instantiating (57) with all_7_1, simplifying with (17), (19) % 13.42/2.69 | gives: % 13.42/2.69 | (59) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_1) = % 13.42/2.69 | v2 & op2(all_30_0, v2) = v1 & op1(all_7_2, all_7_1) = v0 & $i(v2) & % 13.42/2.69 | $i(v1) & $i(v0)) % 13.42/2.69 | % 13.42/2.69 | DELTA: instantiating (54) with fresh symbols all_33_0, all_33_1, all_33_2 % 13.42/2.69 | gives: % 13.42/2.69 | (60) h(all_33_2) = all_33_1 & h(all_7_1) = all_33_0 & op2(all_27_0, % 13.42/2.69 | all_33_0) = all_33_1 & op1(all_7_1, all_7_1) = all_33_2 & % 13.42/2.69 | $i(all_33_0) & $i(all_33_1) & $i(all_33_2) % 13.42/2.69 | % 13.42/2.69 | ALPHA: (60) implies: % 13.42/2.69 | (61) $i(all_33_1) % 13.42/2.69 | (62) op1(all_7_1, all_7_1) = all_33_2 % 13.42/2.70 | (63) op2(all_27_0, all_33_0) = all_33_1 % 13.42/2.70 | (64) h(all_7_1) = all_33_0 % 13.42/2.70 | (65) h(all_33_2) = all_33_1 % 13.42/2.70 | % 13.42/2.70 | DELTA: instantiating (53) with fresh symbols all_35_0, all_35_1, all_35_2 % 13.42/2.70 | gives: % 13.42/2.70 | (66) h(all_35_2) = all_35_1 & h(all_7_2) = all_35_0 & op2(all_27_0, % 13.42/2.70 | all_35_0) = all_35_1 & op1(all_7_1, all_7_2) = all_35_2 & % 13.42/2.70 | $i(all_35_0) & $i(all_35_1) & $i(all_35_2) % 13.42/2.70 | % 13.42/2.70 | ALPHA: (66) implies: % 13.42/2.70 | (67) $i(all_35_2) % 13.42/2.70 | (68) op1(all_7_1, all_7_2) = all_35_2 % 13.42/2.70 | (69) op2(all_27_0, all_35_0) = all_35_1 % 13.42/2.70 | (70) h(all_7_2) = all_35_0 % 13.42/2.70 | (71) h(all_35_2) = all_35_1 % 13.42/2.70 | % 13.42/2.70 | DELTA: instantiating (59) with fresh symbols all_37_0, all_37_1, all_37_2 % 13.42/2.70 | gives: % 13.42/2.70 | (72) h(all_37_2) = all_37_1 & h(all_7_1) = all_37_0 & op2(all_30_0, % 13.42/2.70 | all_37_0) = all_37_1 & op1(all_7_2, all_7_1) = all_37_2 & % 13.42/2.70 | $i(all_37_0) & $i(all_37_1) & $i(all_37_2) % 13.42/2.70 | % 13.42/2.70 | ALPHA: (72) implies: % 13.42/2.70 | (73) op1(all_7_2, all_7_1) = all_37_2 % 13.42/2.70 | (74) op2(all_30_0, all_37_0) = all_37_1 % 13.42/2.70 | (75) h(all_7_1) = all_37_0 % 13.42/2.70 | (76) h(all_37_2) = all_37_1 % 13.42/2.70 | % 13.42/2.70 | DELTA: instantiating (58) with fresh symbols all_39_0, all_39_1, all_39_2 % 13.42/2.70 | gives: % 13.42/2.70 | (77) h(all_39_2) = all_39_1 & h(all_7_2) = all_39_0 & op2(all_30_0, % 13.42/2.70 | all_39_0) = all_39_1 & op1(all_7_2, all_7_2) = all_39_2 & % 13.42/2.70 | $i(all_39_0) & $i(all_39_1) & $i(all_39_2) % 13.42/2.70 | % 13.42/2.70 | ALPHA: (77) implies: % 13.42/2.70 | (78) $i(all_39_2) % 13.42/2.70 | (79) $i(all_39_1) % 13.42/2.70 | (80) op1(all_7_2, all_7_2) = all_39_2 % 13.42/2.70 | (81) op2(all_30_0, all_39_0) = all_39_1 % 13.42/2.70 | (82) h(all_7_2) = all_39_0 % 13.42/2.70 | (83) h(all_39_2) = all_39_1 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (12) with all_7_1, all_39_2, all_7_2, all_7_2, % 13.42/2.70 | simplifying with (20), (80) gives: % 13.42/2.70 | (84) all_39_2 = all_7_1 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (12) with all_7_0, all_37_2, all_7_1, all_7_2, % 13.42/2.70 | simplifying with (21), (73) gives: % 13.42/2.70 | (85) all_37_2 = all_7_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (12) with all_21_0, all_37_2, all_7_1, all_7_2, % 13.42/2.70 | simplifying with (43), (73) gives: % 13.42/2.70 | (86) all_37_2 = all_21_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (12) with all_19_0, all_35_2, all_7_2, all_7_1, % 13.42/2.70 | simplifying with (39), (68) gives: % 13.42/2.70 | (87) all_35_2 = all_19_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (12) with all_7_2, all_33_2, all_7_1, all_7_1, % 13.42/2.70 | simplifying with (22), (62) gives: % 13.42/2.70 | (88) all_33_2 = all_7_2 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_30_0, all_35_0, all_7_2, simplifying % 13.42/2.70 | with (56), (70) gives: % 13.42/2.70 | (89) all_35_0 = all_30_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_23_0, all_35_0, all_7_2, simplifying % 13.42/2.70 | with (46), (70) gives: % 13.42/2.70 | (90) all_35_0 = all_23_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_35_0, all_39_0, all_7_2, simplifying % 13.42/2.70 | with (70), (82) gives: % 13.42/2.70 | (91) all_39_0 = all_35_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_25_0, all_39_0, all_7_2, simplifying % 13.42/2.70 | with (48), (82) gives: % 13.42/2.70 | (92) all_39_0 = all_25_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_15_0, all_27_0, all_7_1, simplifying % 13.42/2.70 | with (33), (51) gives: % 13.42/2.70 | (93) all_27_0 = all_15_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_27_0, all_33_0, all_7_1, simplifying % 13.42/2.70 | with (51), (64) gives: % 13.42/2.70 | (94) all_33_0 = all_27_0 % 13.42/2.70 | % 13.42/2.70 | GROUND_INST: instantiating (10) with all_33_0, all_37_0, all_7_1, simplifying % 13.42/2.70 | with (64), (75) gives: % 13.42/2.71 | (95) all_37_0 = all_33_0 % 13.42/2.71 | % 13.42/2.71 | GROUND_INST: instantiating (10) with all_17_0, all_37_0, all_7_1, simplifying % 13.42/2.71 | with (35), (75) gives: % 13.42/2.71 | (96) all_37_0 = all_17_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (91), (92) imply: % 13.42/2.71 | (97) all_35_0 = all_25_0 % 13.42/2.71 | % 13.42/2.71 | SIMP: (97) implies: % 13.42/2.71 | (98) all_35_0 = all_25_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (95), (96) imply: % 13.42/2.71 | (99) all_33_0 = all_17_0 % 13.42/2.71 | % 13.42/2.71 | SIMP: (99) implies: % 13.42/2.71 | (100) all_33_0 = all_17_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (85), (86) imply: % 13.42/2.71 | (101) all_21_0 = all_7_0 % 13.42/2.71 | % 13.42/2.71 | SIMP: (101) implies: % 13.42/2.71 | (102) all_21_0 = all_7_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (89), (98) imply: % 13.42/2.71 | (103) all_30_0 = all_25_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (89), (90) imply: % 13.42/2.71 | (104) all_30_0 = all_23_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (94), (100) imply: % 13.42/2.71 | (105) all_27_0 = all_17_0 % 13.42/2.71 | % 13.42/2.71 | SIMP: (105) implies: % 13.42/2.71 | (106) all_27_0 = all_17_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (103), (104) imply: % 13.42/2.71 | (107) all_25_0 = all_23_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (93), (106) imply: % 13.42/2.71 | (108) all_17_0 = all_15_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (100), (108) imply: % 13.42/2.71 | (109) all_33_0 = all_15_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (96), (108) imply: % 13.42/2.71 | (110) all_37_0 = all_15_0 % 13.42/2.71 | % 13.42/2.71 | COMBINE_EQS: (92), (107) imply: % 13.42/2.71 | (111) all_39_0 = all_23_0 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (49), (107) imply: % 13.42/2.71 | (112) j(all_23_0) = all_7_2 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (36), (108) imply: % 13.42/2.71 | (113) j(all_15_0) = all_7_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (83), (84) imply: % 13.42/2.71 | (114) h(all_7_1) = all_39_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (76), (85) imply: % 13.42/2.71 | (115) h(all_7_0) = all_37_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (71), (87) imply: % 13.42/2.71 | (116) h(all_19_0) = all_35_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (65), (88) imply: % 13.42/2.71 | (117) h(all_7_2) = all_33_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (81), (104), (111) imply: % 13.42/2.71 | (118) op2(all_23_0, all_23_0) = all_39_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (74), (104), (110) imply: % 13.42/2.71 | (119) op2(all_23_0, all_15_0) = all_37_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (69), (90), (93) imply: % 13.42/2.71 | (120) op2(all_15_0, all_23_0) = all_35_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (63), (93), (109) imply: % 13.42/2.71 | (121) op2(all_15_0, all_15_0) = all_33_1 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (67), (87) imply: % 13.42/2.71 | (122) $i(all_19_0) % 13.42/2.71 | % 13.42/2.71 | REDUCE: (42), (102) imply: % 13.42/2.71 | (123) $i(all_7_0) % 13.42/2.71 | % 13.42/2.71 | REDUCE: (41), (102) imply: % 13.42/2.71 | (124) sorti1(all_7_0) % 13.42/2.71 | % 13.42/2.71 | GROUND_INST: instantiating (10) with all_23_0, all_33_1, all_7_2, simplifying % 13.42/2.71 | with (46), (117) gives: % 13.42/2.71 | (125) all_33_1 = all_23_0 % 13.42/2.71 | % 13.42/2.71 | GROUND_INST: instantiating (10) with all_15_0, all_39_1, all_7_1, simplifying % 13.42/2.71 | with (33), (114) gives: % 13.42/2.71 | (126) all_39_1 = all_15_0 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (118), (126) imply: % 13.42/2.71 | (127) op2(all_23_0, all_23_0) = all_15_0 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (121), (125) imply: % 13.42/2.71 | (128) op2(all_15_0, all_15_0) = all_23_0 % 13.42/2.71 | % 13.42/2.71 | REDUCE: (79), (126) imply: % 13.42/2.71 | (129) $i(all_15_0) % 13.42/2.71 | % 13.42/2.71 | REDUCE: (61), (125) imply: % 13.42/2.71 | (130) $i(all_23_0) % 13.42/2.71 | % 13.42/2.71 | GROUND_INST: instantiating (57) with all_7_0, simplifying with (123), (124) % 13.42/2.71 | gives: % 13.42/2.71 | (131) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_0) = % 13.42/2.71 | v2 & op2(all_30_0, v2) = v1 & op1(all_7_2, all_7_0) = v0 & $i(v2) & % 13.42/2.71 | $i(v1) & $i(v0)) % 13.42/2.71 | % 13.42/2.71 | GROUND_INST: instantiating (52) with all_7_0, simplifying with (123), (124) % 13.42/2.71 | gives: % 13.42/2.72 | (132) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_0) = % 13.42/2.72 | v2 & op2(all_27_0, v2) = v1 & op1(all_7_1, all_7_0) = v0 & $i(v2) & % 13.42/2.72 | $i(v1) & $i(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (7) with all_7_0, simplifying with (123), (124) % 13.42/2.72 | gives: % 13.42/2.72 | (133) ? [v0: $i] : (j(v0) = all_7_0 & h(all_7_0) = v0 & $i(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (6) with all_7_0, simplifying with (123), (124) % 13.42/2.72 | gives: % 13.42/2.72 | (134) ? [v0: $i] : (h(all_7_0) = v0 & $i(v0) & sorti2(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (5) with all_7_0, simplifying with (123), (124) % 13.42/2.72 | gives: % 13.42/2.72 | (135) ? [v0: $i] : (h(all_7_0) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.72 | ~ sorti1(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (h(v2) = % 13.42/2.72 | v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_7_0, v1) = v2 & % 13.42/2.72 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (57) with all_19_0, simplifying with (38), (122) % 13.42/2.72 | gives: % 13.42/2.72 | (136) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_19_0) = % 13.42/2.72 | v2 & op2(all_30_0, v2) = v1 & op1(all_7_2, all_19_0) = v0 & $i(v2) % 13.42/2.72 | & $i(v1) & $i(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (52) with all_19_0, simplifying with (38), (122) % 13.42/2.72 | gives: % 13.42/2.72 | (137) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_19_0) = % 13.42/2.72 | v2 & op2(all_27_0, v2) = v1 & op1(all_7_1, all_19_0) = v0 & $i(v2) % 13.42/2.72 | & $i(v1) & $i(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (5) with all_19_0, simplifying with (38), (122) % 13.42/2.72 | gives: % 13.42/2.72 | (138) ? [v0: $i] : (h(all_19_0) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.72 | ~ sorti1(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (h(v2) % 13.42/2.72 | = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_19_0, v1) = v2 & % 13.42/2.72 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (8) with all_15_0, simplifying with (32), (129) % 13.42/2.72 | gives: % 13.42/2.72 | (139) ? [v0: $i] : (j(all_15_0) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.72 | ~ sorti2(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (j(v2) % 13.42/2.72 | = v3 & j(v1) = v4 & op2(all_15_0, v1) = v2 & op1(v0, v4) = v3 & % 13.42/2.72 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (3) with all_15_0, simplifying with (32), (129) % 13.42/2.72 | gives: % 13.42/2.72 | (140) ? [v0: $i] : (op2(all_15_0, all_15_0) = v0 & $i(v0) & ( ~ sorti2(v0) % 13.42/2.72 | | ? [v1: $i] : ? [v2: $i] : (op2(v0, v0) = v1 & op2(all_15_0, % 13.42/2.72 | v0) = v2 & $i(v2) & $i(v1) & ( ~ (v1 = all_15_0) | v2 = % 13.42/2.72 | all_15_0)))) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (2) with all_23_0, all_15_0, simplifying with (32), % 13.42/2.72 | (45), (129), (130) gives: % 13.42/2.72 | (141) ? [v0: $i] : (op2(all_23_0, all_15_0) = v0 & $i(v0) & sorti2(v0)) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (8) with all_23_0, simplifying with (45), (130) % 13.42/2.72 | gives: % 13.42/2.72 | (142) ? [v0: $i] : (j(all_23_0) = v0 & $i(v0) & ! [v1: $i] : ( ~ $i(v1) | % 13.42/2.72 | ~ sorti2(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (j(v2) % 13.42/2.72 | = v3 & j(v1) = v4 & op2(all_23_0, v1) = v2 & op1(v0, v4) = v3 & % 13.42/2.72 | $i(v4) & $i(v3) & $i(v2)))) % 13.42/2.72 | % 13.42/2.72 | GROUND_INST: instantiating (3) with all_23_0, simplifying with (45), (130) % 13.42/2.72 | gives: % 13.42/2.72 | (143) ? [v0: $i] : (op2(all_23_0, all_23_0) = v0 & $i(v0) & ( ~ sorti2(v0) % 13.42/2.72 | | ? [v1: $i] : ? [v2: $i] : (op2(v0, v0) = v1 & op2(all_23_0, % 13.42/2.72 | v0) = v2 & $i(v2) & $i(v1) & ( ~ (v1 = all_23_0) | v2 = % 13.42/2.72 | all_23_0)))) % 13.42/2.72 | % 13.42/2.73 | GROUND_INST: instantiating (4) with all_15_0, all_23_0, all_35_1, simplifying % 13.42/2.73 | with (32), (45), (120), (128), (129), (130) gives: % 13.42/2.73 | (144) all_35_1 = all_15_0 | ? [v0: any] : ( ~ (v0 = all_15_0) & % 13.42/2.73 | op2(all_23_0, all_23_0) = v0 & $i(v0)) % 13.42/2.73 | % 13.42/2.73 | GROUND_INST: instantiating (4) with all_23_0, all_15_0, all_37_1, simplifying % 13.42/2.73 | with (32), (45), (119), (127), (129), (130) gives: % 13.42/2.73 | (145) all_37_1 = all_23_0 | ? [v0: any] : ( ~ (v0 = all_23_0) & % 13.42/2.73 | op2(all_15_0, all_15_0) = v0 & $i(v0)) % 13.42/2.73 | % 13.42/2.73 | GROUND_INST: instantiating (9) with all_23_0, all_7_2, all_15_0, all_7_1, % 13.42/2.73 | all_7_0, simplifying with (21), (32), (45), (112), (113), (129), % 13.42/2.73 | (130) gives: % 13.42/2.73 | (146) ? [v0: $i] : (j(v0) = all_7_0 & op2(all_23_0, all_15_0) = v0 & % 13.42/2.73 | $i(v0) & $i(all_7_0)) % 13.42/2.73 | % 13.42/2.73 | GROUND_INST: instantiating (9) with all_15_0, all_7_1, all_23_0, all_7_2, % 13.42/2.73 | all_19_0, simplifying with (32), (39), (45), (112), (113), (129), % 13.42/2.73 | (130) gives: % 13.42/2.73 | (147) ? [v0: $i] : (j(v0) = all_19_0 & op2(all_15_0, all_23_0) = v0 & % 13.42/2.73 | $i(v0) & $i(all_19_0)) % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (141) with fresh symbol all_61_0 gives: % 13.42/2.73 | (148) op2(all_23_0, all_15_0) = all_61_0 & $i(all_61_0) & sorti2(all_61_0) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (148) implies: % 13.42/2.73 | (149) op2(all_23_0, all_15_0) = all_61_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (134) with fresh symbol all_75_0 gives: % 13.42/2.73 | (150) h(all_7_0) = all_75_0 & $i(all_75_0) & sorti2(all_75_0) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (150) implies: % 13.42/2.73 | (151) h(all_7_0) = all_75_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (133) with fresh symbol all_79_0 gives: % 13.42/2.73 | (152) j(all_79_0) = all_7_0 & h(all_7_0) = all_79_0 & $i(all_79_0) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (152) implies: % 13.42/2.73 | (153) h(all_7_0) = all_79_0 % 13.42/2.73 | (154) j(all_79_0) = all_7_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (147) with fresh symbol all_91_0 gives: % 13.42/2.73 | (155) j(all_91_0) = all_19_0 & op2(all_15_0, all_23_0) = all_91_0 & % 13.42/2.73 | $i(all_91_0) & $i(all_19_0) % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (146) with fresh symbol all_93_0 gives: % 13.42/2.73 | (156) j(all_93_0) = all_7_0 & op2(all_23_0, all_15_0) = all_93_0 & % 13.42/2.73 | $i(all_93_0) & $i(all_7_0) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (156) implies: % 13.42/2.73 | (157) op2(all_23_0, all_15_0) = all_93_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (131) with fresh symbols all_95_0, all_95_1, all_95_2 % 13.42/2.73 | gives: % 13.42/2.73 | (158) h(all_95_2) = all_95_1 & h(all_7_0) = all_95_0 & op2(all_30_0, % 13.42/2.73 | all_95_0) = all_95_1 & op1(all_7_2, all_7_0) = all_95_2 & % 13.42/2.73 | $i(all_95_0) & $i(all_95_1) & $i(all_95_2) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (158) implies: % 13.42/2.73 | (159) h(all_7_0) = all_95_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (137) with fresh symbols all_97_0, all_97_1, all_97_2 % 13.42/2.73 | gives: % 13.42/2.73 | (160) h(all_97_2) = all_97_1 & h(all_19_0) = all_97_0 & op2(all_27_0, % 13.42/2.73 | all_97_0) = all_97_1 & op1(all_7_1, all_19_0) = all_97_2 & % 13.42/2.73 | $i(all_97_0) & $i(all_97_1) & $i(all_97_2) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (160) implies: % 13.42/2.73 | (161) op2(all_27_0, all_97_0) = all_97_1 % 13.42/2.73 | (162) h(all_19_0) = all_97_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (136) with fresh symbols all_99_0, all_99_1, all_99_2 % 13.42/2.73 | gives: % 13.42/2.73 | (163) h(all_99_2) = all_99_1 & h(all_19_0) = all_99_0 & op2(all_30_0, % 13.42/2.73 | all_99_0) = all_99_1 & op1(all_7_2, all_19_0) = all_99_2 & % 13.42/2.73 | $i(all_99_0) & $i(all_99_1) & $i(all_99_2) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (163) implies: % 13.42/2.73 | (164) h(all_19_0) = all_99_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (132) with fresh symbols all_101_0, all_101_1, all_101_2 % 13.42/2.73 | gives: % 13.42/2.73 | (165) h(all_101_2) = all_101_1 & h(all_7_0) = all_101_0 & op2(all_27_0, % 13.42/2.73 | all_101_0) = all_101_1 & op1(all_7_1, all_7_0) = all_101_2 & % 13.42/2.73 | $i(all_101_0) & $i(all_101_1) & $i(all_101_2) % 13.42/2.73 | % 13.42/2.73 | ALPHA: (165) implies: % 13.42/2.73 | (166) h(all_7_0) = all_101_0 % 13.42/2.73 | % 13.42/2.73 | DELTA: instantiating (143) with fresh symbol all_103_0 gives: % 13.42/2.73 | (167) op2(all_23_0, all_23_0) = all_103_0 & $i(all_103_0) & ( ~ % 13.42/2.74 | sorti2(all_103_0) | ? [v0: $i] : ? [v1: $i] : (op2(all_103_0, % 13.42/2.74 | all_103_0) = v0 & op2(all_23_0, all_103_0) = v1 & $i(v1) & % 13.42/2.74 | $i(v0) & ( ~ (v0 = all_23_0) | v1 = all_23_0))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (167) implies: % 13.42/2.74 | (168) op2(all_23_0, all_23_0) = all_103_0 % 13.42/2.74 | % 13.42/2.74 | DELTA: instantiating (140) with fresh symbol all_105_0 gives: % 13.42/2.74 | (169) op2(all_15_0, all_15_0) = all_105_0 & $i(all_105_0) & ( ~ % 13.42/2.74 | sorti2(all_105_0) | ? [v0: $i] : ? [v1: $i] : (op2(all_105_0, % 13.42/2.74 | all_105_0) = v0 & op2(all_15_0, all_105_0) = v1 & $i(v1) & % 13.42/2.74 | $i(v0) & ( ~ (v0 = all_15_0) | v1 = all_15_0))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (169) implies: % 13.42/2.74 | (170) op2(all_15_0, all_15_0) = all_105_0 % 13.42/2.74 | % 13.42/2.74 | DELTA: instantiating (142) with fresh symbol all_107_0 gives: % 13.42/2.74 | (171) j(all_23_0) = all_107_0 & $i(all_107_0) & ! [v0: $i] : ( ~ $i(v0) | % 13.42/2.74 | ~ sorti2(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (j(v1) = % 13.42/2.74 | v2 & j(v0) = v3 & op2(all_23_0, v0) = v1 & op1(all_107_0, v3) = % 13.42/2.74 | v2 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (171) implies: % 13.42/2.74 | (172) j(all_23_0) = all_107_0 % 13.42/2.74 | (173) ! [v0: $i] : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : ? [v2: $i] % 13.42/2.74 | : ? [v3: $i] : (j(v1) = v2 & j(v0) = v3 & op2(all_23_0, v0) = v1 & % 13.42/2.74 | op1(all_107_0, v3) = v2 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (173) with all_15_0, simplifying with (32), (129) % 13.42/2.74 | gives: % 13.42/2.74 | (174) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (j(v0) = v1 & j(all_15_0) = % 13.42/2.74 | v2 & op2(all_23_0, all_15_0) = v0 & op1(all_107_0, v2) = v1 & % 13.42/2.74 | $i(v2) & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (173) with all_23_0, simplifying with (45), (130) % 13.42/2.74 | gives: % 13.42/2.74 | (175) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (j(v0) = v1 & j(all_23_0) = % 13.42/2.74 | v2 & op2(all_23_0, all_23_0) = v0 & op1(all_107_0, v2) = v1 & % 13.42/2.74 | $i(v2) & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | DELTA: instantiating (139) with fresh symbol all_110_0 gives: % 13.42/2.74 | (176) j(all_15_0) = all_110_0 & $i(all_110_0) & ! [v0: $i] : ( ~ $i(v0) | % 13.42/2.74 | ~ sorti2(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (j(v1) = % 13.42/2.74 | v2 & j(v0) = v3 & op2(all_15_0, v0) = v1 & op1(all_110_0, v3) = % 13.42/2.74 | v2 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (176) implies: % 13.42/2.74 | (177) ! [v0: $i] : ( ~ $i(v0) | ~ sorti2(v0) | ? [v1: $i] : ? [v2: $i] % 13.42/2.74 | : ? [v3: $i] : (j(v1) = v2 & j(v0) = v3 & op2(all_15_0, v0) = v1 & % 13.42/2.74 | op1(all_110_0, v3) = v2 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (177) with all_15_0, simplifying with (32), (129) % 13.42/2.74 | gives: % 13.42/2.74 | (178) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (j(v0) = v1 & j(all_15_0) = % 13.42/2.74 | v2 & op2(all_15_0, all_15_0) = v0 & op1(all_110_0, v2) = v1 & % 13.42/2.74 | $i(v2) & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (177) with all_23_0, simplifying with (45), (130) % 13.42/2.74 | gives: % 13.42/2.74 | (179) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (j(v0) = v1 & j(all_23_0) = % 13.42/2.74 | v2 & op2(all_15_0, all_23_0) = v0 & op1(all_110_0, v2) = v1 & % 13.42/2.74 | $i(v2) & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | DELTA: instantiating (135) with fresh symbol all_113_0 gives: % 13.42/2.74 | (180) h(all_7_0) = all_113_0 & $i(all_113_0) & ! [v0: $i] : ( ~ $i(v0) | % 13.42/2.74 | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (h(v1) = % 13.42/2.74 | v2 & h(v0) = v3 & op2(all_113_0, v3) = v2 & op1(all_7_0, v0) = v1 % 13.42/2.74 | & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (180) implies: % 13.42/2.74 | (181) h(all_7_0) = all_113_0 % 13.42/2.74 | (182) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] % 13.42/2.74 | : ? [v3: $i] : (h(v1) = v2 & h(v0) = v3 & op2(all_113_0, v3) = v2 % 13.42/2.74 | & op1(all_7_0, v0) = v1 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (182) with all_7_0, simplifying with (123), (124) % 13.42/2.74 | gives: % 13.42/2.74 | (183) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_0) = % 13.42/2.74 | v2 & op2(all_113_0, v2) = v1 & op1(all_7_0, all_7_0) = v0 & $i(v2) % 13.42/2.74 | & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | GROUND_INST: instantiating (182) with all_19_0, simplifying with (38), (122) % 13.42/2.74 | gives: % 13.42/2.74 | (184) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_19_0) = % 13.42/2.74 | v2 & op2(all_113_0, v2) = v1 & op1(all_7_0, all_19_0) = v0 & $i(v2) % 13.42/2.74 | & $i(v1) & $i(v0)) % 13.42/2.74 | % 13.42/2.74 | DELTA: instantiating (138) with fresh symbol all_116_0 gives: % 13.42/2.74 | (185) h(all_19_0) = all_116_0 & $i(all_116_0) & ! [v0: $i] : ( ~ $i(v0) | % 13.42/2.74 | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (h(v1) = % 13.42/2.74 | v2 & h(v0) = v3 & op2(all_116_0, v3) = v2 & op1(all_19_0, v0) = % 13.42/2.74 | v1 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.74 | ALPHA: (185) implies: % 13.42/2.74 | (186) h(all_19_0) = all_116_0 % 13.42/2.74 | (187) ! [v0: $i] : ( ~ $i(v0) | ~ sorti1(v0) | ? [v1: $i] : ? [v2: $i] % 13.42/2.74 | : ? [v3: $i] : (h(v1) = v2 & h(v0) = v3 & op2(all_116_0, v3) = v2 % 13.42/2.74 | & op1(all_19_0, v0) = v1 & $i(v3) & $i(v2) & $i(v1))) % 13.42/2.74 | % 13.42/2.75 | GROUND_INST: instantiating (187) with all_7_1, simplifying with (17), (19) % 13.42/2.75 | gives: % 13.42/2.75 | (188) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_1) = % 13.42/2.75 | v2 & op2(all_116_0, v2) = v1 & op1(all_19_0, all_7_1) = v0 & $i(v2) % 13.42/2.75 | & $i(v1) & $i(v0)) % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (187) with all_7_0, simplifying with (123), (124) % 13.42/2.75 | gives: % 13.42/2.75 | (189) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_7_0) = % 13.42/2.75 | v2 & op2(all_116_0, v2) = v1 & op1(all_19_0, all_7_0) = v0 & $i(v2) % 13.42/2.75 | & $i(v1) & $i(v0)) % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (187) with all_19_0, simplifying with (38), (122) % 13.42/2.75 | gives: % 13.42/2.75 | (190) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (h(v0) = v1 & h(all_19_0) = % 13.42/2.75 | v2 & op2(all_116_0, v2) = v1 & op1(all_19_0, all_19_0) = v0 & % 13.42/2.75 | $i(v2) & $i(v1) & $i(v0)) % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (175) with fresh symbols all_119_0, all_119_1, all_119_2 % 13.42/2.75 | gives: % 13.42/2.75 | (191) j(all_119_2) = all_119_1 & j(all_23_0) = all_119_0 & op2(all_23_0, % 13.42/2.75 | all_23_0) = all_119_2 & op1(all_107_0, all_119_0) = all_119_1 & % 13.42/2.75 | $i(all_119_0) & $i(all_119_1) & $i(all_119_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (191) implies: % 13.42/2.75 | (192) op2(all_23_0, all_23_0) = all_119_2 % 13.42/2.75 | (193) j(all_23_0) = all_119_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (174) with fresh symbols all_121_0, all_121_1, all_121_2 % 13.42/2.75 | gives: % 13.42/2.75 | (194) j(all_121_2) = all_121_1 & j(all_15_0) = all_121_0 & op2(all_23_0, % 13.42/2.75 | all_15_0) = all_121_2 & op1(all_107_0, all_121_0) = all_121_1 & % 13.42/2.75 | $i(all_121_0) & $i(all_121_1) & $i(all_121_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (194) implies: % 13.42/2.75 | (195) op2(all_23_0, all_15_0) = all_121_2 % 13.42/2.75 | (196) j(all_121_2) = all_121_1 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (179) with fresh symbols all_123_0, all_123_1, all_123_2 % 13.42/2.75 | gives: % 13.42/2.75 | (197) j(all_123_2) = all_123_1 & j(all_23_0) = all_123_0 & op2(all_15_0, % 13.42/2.75 | all_23_0) = all_123_2 & op1(all_110_0, all_123_0) = all_123_1 & % 13.42/2.75 | $i(all_123_0) & $i(all_123_1) & $i(all_123_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (197) implies: % 13.42/2.75 | (198) j(all_23_0) = all_123_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (178) with fresh symbols all_125_0, all_125_1, all_125_2 % 13.42/2.75 | gives: % 13.42/2.75 | (199) j(all_125_2) = all_125_1 & j(all_15_0) = all_125_0 & op2(all_15_0, % 13.42/2.75 | all_15_0) = all_125_2 & op1(all_110_0, all_125_0) = all_125_1 & % 13.42/2.75 | $i(all_125_0) & $i(all_125_1) & $i(all_125_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (199) implies: % 13.42/2.75 | (200) op2(all_15_0, all_15_0) = all_125_2 % 13.42/2.75 | (201) j(all_125_2) = all_125_1 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (184) with fresh symbols all_127_0, all_127_1, all_127_2 % 13.42/2.75 | gives: % 13.42/2.75 | (202) h(all_127_2) = all_127_1 & h(all_19_0) = all_127_0 & op2(all_113_0, % 13.42/2.75 | all_127_0) = all_127_1 & op1(all_7_0, all_19_0) = all_127_2 & % 13.42/2.75 | $i(all_127_0) & $i(all_127_1) & $i(all_127_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (202) implies: % 13.42/2.75 | (203) h(all_19_0) = all_127_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (183) with fresh symbols all_129_0, all_129_1, all_129_2 % 13.42/2.75 | gives: % 13.42/2.75 | (204) h(all_129_2) = all_129_1 & h(all_7_0) = all_129_0 & op2(all_113_0, % 13.42/2.75 | all_129_0) = all_129_1 & op1(all_7_0, all_7_0) = all_129_2 & % 13.42/2.75 | $i(all_129_0) & $i(all_129_1) & $i(all_129_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (204) implies: % 13.42/2.75 | (205) h(all_7_0) = all_129_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (190) with fresh symbols all_135_0, all_135_1, all_135_2 % 13.42/2.75 | gives: % 13.42/2.75 | (206) h(all_135_2) = all_135_1 & h(all_19_0) = all_135_0 & op2(all_116_0, % 13.42/2.75 | all_135_0) = all_135_1 & op1(all_19_0, all_19_0) = all_135_2 & % 13.42/2.75 | $i(all_135_0) & $i(all_135_1) & $i(all_135_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (206) implies: % 13.42/2.75 | (207) op2(all_116_0, all_135_0) = all_135_1 % 13.42/2.75 | (208) h(all_19_0) = all_135_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (188) with fresh symbols all_137_0, all_137_1, all_137_2 % 13.42/2.75 | gives: % 13.42/2.75 | (209) h(all_137_2) = all_137_1 & h(all_7_1) = all_137_0 & op2(all_116_0, % 13.42/2.75 | all_137_0) = all_137_1 & op1(all_19_0, all_7_1) = all_137_2 & % 13.42/2.75 | $i(all_137_0) & $i(all_137_1) & $i(all_137_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (209) implies: % 13.42/2.75 | (210) op2(all_116_0, all_137_0) = all_137_1 % 13.42/2.75 | (211) h(all_7_1) = all_137_0 % 13.42/2.75 | % 13.42/2.75 | DELTA: instantiating (189) with fresh symbols all_141_0, all_141_1, all_141_2 % 13.42/2.75 | gives: % 13.42/2.75 | (212) h(all_141_2) = all_141_1 & h(all_7_0) = all_141_0 & op2(all_116_0, % 13.42/2.75 | all_141_0) = all_141_1 & op1(all_19_0, all_7_0) = all_141_2 & % 13.42/2.75 | $i(all_141_0) & $i(all_141_1) & $i(all_141_2) % 13.42/2.75 | % 13.42/2.75 | ALPHA: (212) implies: % 13.42/2.75 | (213) h(all_7_0) = all_141_0 % 13.42/2.75 | % 13.42/2.75 | REDUCE: (93), (161) imply: % 13.42/2.75 | (214) op2(all_15_0, all_97_0) = all_97_1 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_23_0, all_125_2, all_15_0, all_15_0, % 13.42/2.75 | simplifying with (128), (200) gives: % 13.42/2.75 | (215) all_125_2 = all_23_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_105_0, all_125_2, all_15_0, all_15_0, % 13.42/2.75 | simplifying with (170), (200) gives: % 13.42/2.75 | (216) all_125_2 = all_105_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_37_1, all_93_0, all_15_0, all_23_0, % 13.42/2.75 | simplifying with (119), (157) gives: % 13.42/2.75 | (217) all_93_0 = all_37_1 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_93_0, all_121_2, all_15_0, all_23_0, % 13.42/2.75 | simplifying with (157), (195) gives: % 13.42/2.75 | (218) all_121_2 = all_93_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_61_0, all_121_2, all_15_0, all_23_0, % 13.42/2.75 | simplifying with (149), (195) gives: % 13.42/2.75 | (219) all_121_2 = all_61_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_15_0, all_119_2, all_23_0, all_23_0, % 13.42/2.75 | simplifying with (127), (192) gives: % 13.42/2.75 | (220) all_119_2 = all_15_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (13) with all_103_0, all_119_2, all_23_0, all_23_0, % 13.42/2.75 | simplifying with (168), (192) gives: % 13.42/2.75 | (221) all_119_2 = all_103_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (10) with all_15_0, all_137_0, all_7_1, simplifying % 13.42/2.75 | with (33), (211) gives: % 13.42/2.75 | (222) all_137_0 = all_15_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (10) with all_37_1, all_79_0, all_7_0, simplifying % 13.42/2.75 | with (115), (153) gives: % 13.42/2.75 | (223) all_79_0 = all_37_1 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (10) with all_79_0, all_95_0, all_7_0, simplifying % 13.42/2.75 | with (153), (159) gives: % 13.42/2.75 | (224) all_95_0 = all_79_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (10) with all_95_0, all_101_0, all_7_0, simplifying % 13.42/2.75 | with (159), (166) gives: % 13.42/2.75 | (225) all_101_0 = all_95_0 % 13.42/2.75 | % 13.42/2.75 | GROUND_INST: instantiating (10) with all_101_0, all_113_0, all_7_0, % 13.42/2.75 | simplifying with (166), (181) gives: % 13.42/2.75 | (226) all_113_0 = all_101_0 % 13.42/2.75 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_113_0, all_129_0, all_7_0, % 13.42/2.76 | simplifying with (181), (205) gives: % 13.42/2.76 | (227) all_129_0 = all_113_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_129_0, all_141_0, all_7_0, % 13.42/2.76 | simplifying with (205), (213) gives: % 13.42/2.76 | (228) all_141_0 = all_129_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_75_0, all_141_0, all_7_0, simplifying % 13.42/2.76 | with (151), (213) gives: % 13.42/2.76 | (229) all_141_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_99_0, all_127_0, all_19_0, % 13.42/2.76 | simplifying with (164), (203) gives: % 13.42/2.76 | (230) all_127_0 = all_99_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_35_1, all_135_0, all_19_0, % 13.42/2.76 | simplifying with (116), (208) gives: % 13.42/2.76 | (231) all_135_0 = all_35_1 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_127_0, all_135_0, all_19_0, % 13.42/2.76 | simplifying with (203), (208) gives: % 13.42/2.76 | (232) all_135_0 = all_127_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_116_0, all_135_0, all_19_0, % 13.42/2.76 | simplifying with (186), (208) gives: % 13.42/2.76 | (233) all_135_0 = all_116_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (10) with all_97_0, all_135_0, all_19_0, % 13.42/2.76 | simplifying with (162), (208) gives: % 13.42/2.76 | (234) all_135_0 = all_97_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (11) with all_107_0, all_119_0, all_23_0, % 13.42/2.76 | simplifying with (172), (193) gives: % 13.42/2.76 | (235) all_119_0 = all_107_0 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (11) with all_7_2, all_123_0, all_23_0, simplifying % 13.42/2.76 | with (112), (198) gives: % 13.42/2.76 | (236) all_123_0 = all_7_2 % 13.42/2.76 | % 13.42/2.76 | GROUND_INST: instantiating (11) with all_119_0, all_123_0, all_23_0, % 13.42/2.76 | simplifying with (193), (198) gives: % 13.42/2.76 | (237) all_123_0 = all_119_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (228), (229) imply: % 13.42/2.76 | (238) all_129_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (238) implies: % 13.42/2.76 | (239) all_129_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (233), (234) imply: % 13.42/2.76 | (240) all_116_0 = all_97_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (232), (233) imply: % 13.42/2.76 | (241) all_127_0 = all_116_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (241) implies: % 13.42/2.76 | (242) all_127_0 = all_116_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (231), (233) imply: % 13.42/2.76 | (243) all_116_0 = all_35_1 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (227), (239) imply: % 13.42/2.76 | (244) all_113_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (244) implies: % 13.42/2.76 | (245) all_113_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (230), (242) imply: % 13.42/2.76 | (246) all_116_0 = all_99_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (246) implies: % 13.42/2.76 | (247) all_116_0 = all_99_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (215), (216) imply: % 13.42/2.76 | (248) all_105_0 = all_23_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (236), (237) imply: % 13.42/2.76 | (249) all_119_0 = all_7_2 % 13.42/2.76 | % 13.42/2.76 | SIMP: (249) implies: % 13.42/2.76 | (250) all_119_0 = all_7_2 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (218), (219) imply: % 13.42/2.76 | (251) all_93_0 = all_61_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (251) implies: % 13.42/2.76 | (252) all_93_0 = all_61_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (235), (250) imply: % 13.42/2.76 | (253) all_107_0 = all_7_2 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (220), (221) imply: % 13.42/2.76 | (254) all_103_0 = all_15_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (243), (247) imply: % 13.42/2.76 | (255) all_99_0 = all_35_1 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (240), (247) imply: % 13.42/2.76 | (256) all_99_0 = all_97_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (226), (245) imply: % 13.42/2.76 | (257) all_101_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (257) implies: % 13.42/2.76 | (258) all_101_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (225), (258) imply: % 13.42/2.76 | (259) all_95_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (259) implies: % 13.42/2.76 | (260) all_95_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (255), (256) imply: % 13.42/2.76 | (261) all_97_0 = all_35_1 % 13.42/2.76 | % 13.42/2.76 | SIMP: (261) implies: % 13.42/2.76 | (262) all_97_0 = all_35_1 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (224), (260) imply: % 13.42/2.76 | (263) all_79_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | SIMP: (263) implies: % 13.42/2.76 | (264) all_79_0 = all_75_0 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (217), (252) imply: % 13.42/2.76 | (265) all_61_0 = all_37_1 % 13.42/2.76 | % 13.42/2.76 | SIMP: (265) implies: % 13.42/2.76 | (266) all_61_0 = all_37_1 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (223), (264) imply: % 13.42/2.76 | (267) all_75_0 = all_37_1 % 13.42/2.76 | % 13.42/2.76 | COMBINE_EQS: (219), (266) imply: % 13.42/2.76 | (268) all_121_2 = all_37_1 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (201), (215) imply: % 13.42/2.76 | (269) j(all_23_0) = all_125_1 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (196), (268) imply: % 13.42/2.76 | (270) j(all_37_1) = all_121_1 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (154), (223) imply: % 13.42/2.76 | (271) j(all_37_1) = all_7_0 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (210), (222), (243) imply: % 13.42/2.76 | (272) op2(all_35_1, all_15_0) = all_137_1 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (207), (231), (243) imply: % 13.42/2.76 | (273) op2(all_35_1, all_35_1) = all_135_1 % 13.42/2.76 | % 13.42/2.76 | REDUCE: (214), (262) imply: % 13.42/2.76 | (274) op2(all_15_0, all_35_1) = all_97_1 % 13.42/2.76 | % 13.42/2.76 | BETA: splitting (144) gives: % 13.42/2.76 | % 13.42/2.76 | Case 1: % 13.42/2.76 | | % 13.42/2.76 | | (275) all_35_1 = all_15_0 % 13.42/2.76 | | % 13.42/2.76 | | REDUCE: (273), (275) imply: % 13.42/2.76 | | (276) op2(all_15_0, all_15_0) = all_135_1 % 13.42/2.76 | | % 13.42/2.76 | | REDUCE: (272), (275) imply: % 13.42/2.76 | | (277) op2(all_15_0, all_15_0) = all_137_1 % 13.42/2.76 | | % 13.42/2.76 | | REDUCE: (274), (275) imply: % 13.42/2.76 | | (278) op2(all_15_0, all_15_0) = all_97_1 % 13.42/2.76 | | % 13.42/2.76 | | BETA: splitting (145) gives: % 13.42/2.76 | | % 13.42/2.76 | | Case 1: % 13.42/2.76 | | | % 13.42/2.76 | | | (279) all_37_1 = all_23_0 % 13.42/2.76 | | | % 13.42/2.76 | | | REDUCE: (270), (279) imply: % 13.42/2.76 | | | (280) j(all_23_0) = all_121_1 % 13.42/2.76 | | | % 13.42/2.76 | | | REDUCE: (271), (279) imply: % 13.42/2.76 | | | (281) j(all_23_0) = all_7_0 % 13.42/2.76 | | | % 13.42/2.76 | | | GROUND_INST: instantiating (11) with all_7_2, all_125_1, all_23_0, % 13.42/2.76 | | | simplifying with (112), (269) gives: % 13.42/2.76 | | | (282) all_125_1 = all_7_2 % 13.42/2.76 | | | % 13.42/2.76 | | | GROUND_INST: instantiating (11) with all_121_1, all_125_1, all_23_0, % 13.42/2.76 | | | simplifying with (269), (280) gives: % 13.42/2.76 | | | (283) all_125_1 = all_121_1 % 13.42/2.76 | | | % 13.42/2.76 | | | GROUND_INST: instantiating (11) with all_7_0, all_125_1, all_23_0, % 13.42/2.76 | | | simplifying with (269), (281) gives: % 13.42/2.76 | | | (284) all_125_1 = all_7_0 % 13.42/2.76 | | | % 13.42/2.76 | | | COMBINE_EQS: (282), (283) imply: % 13.42/2.76 | | | (285) all_121_1 = all_7_2 % 13.42/2.76 | | | % 13.42/2.76 | | | COMBINE_EQS: (283), (284) imply: % 13.42/2.76 | | | (286) all_121_1 = all_7_0 % 13.42/2.76 | | | % 13.42/2.76 | | | COMBINE_EQS: (285), (286) imply: % 13.42/2.76 | | | (287) all_7_0 = all_7_2 % 13.42/2.76 | | | % 13.42/2.76 | | | REDUCE: (15), (287) imply: % 13.42/2.77 | | | (288) $false % 13.42/2.77 | | | % 13.42/2.77 | | | CLOSE: (288) is inconsistent. % 13.42/2.77 | | | % 13.42/2.77 | | Case 2: % 13.42/2.77 | | | % 13.42/2.77 | | | (289) ? [v0: any] : ( ~ (v0 = all_23_0) & op2(all_15_0, all_15_0) = v0 % 13.42/2.77 | | | & $i(v0)) % 13.42/2.77 | | | % 13.42/2.77 | | | DELTA: instantiating (289) with fresh symbol all_155_0 gives: % 13.42/2.77 | | | (290) ~ (all_155_0 = all_23_0) & op2(all_15_0, all_15_0) = all_155_0 & % 13.42/2.77 | | | $i(all_155_0) % 13.42/2.77 | | | % 13.42/2.77 | | | ALPHA: (290) implies: % 13.42/2.77 | | | (291) ~ (all_155_0 = all_23_0) % 13.42/2.77 | | | (292) op2(all_15_0, all_15_0) = all_155_0 % 13.88/2.77 | | | % 13.88/2.77 | | | GROUND_INST: instantiating (13) with all_23_0, all_135_1, all_15_0, % 13.88/2.77 | | | all_15_0, simplifying with (128), (276) gives: % 13.88/2.77 | | | (293) all_135_1 = all_23_0 % 13.88/2.77 | | | % 13.88/2.77 | | | GROUND_INST: instantiating (13) with all_135_1, all_137_1, all_15_0, % 13.88/2.77 | | | all_15_0, simplifying with (276), (277) gives: % 13.88/2.77 | | | (294) all_137_1 = all_135_1 % 13.88/2.77 | | | % 13.88/2.77 | | | GROUND_INST: instantiating (13) with all_137_1, all_155_0, all_15_0, % 13.88/2.77 | | | all_15_0, simplifying with (277), (292) gives: % 13.88/2.77 | | | (295) all_155_0 = all_137_1 % 13.88/2.77 | | | % 13.88/2.77 | | | GROUND_INST: instantiating (13) with all_97_1, all_155_0, all_15_0, % 13.88/2.77 | | | all_15_0, simplifying with (278), (292) gives: % 13.88/2.77 | | | (296) all_155_0 = all_97_1 % 13.88/2.77 | | | % 13.88/2.77 | | | COMBINE_EQS: (295), (296) imply: % 13.88/2.77 | | | (297) all_137_1 = all_97_1 % 13.88/2.77 | | | % 13.88/2.77 | | | SIMP: (297) implies: % 13.88/2.77 | | | (298) all_137_1 = all_97_1 % 13.88/2.77 | | | % 13.88/2.77 | | | COMBINE_EQS: (294), (298) imply: % 13.88/2.77 | | | (299) all_135_1 = all_97_1 % 13.88/2.77 | | | % 13.88/2.77 | | | SIMP: (299) implies: % 13.88/2.77 | | | (300) all_135_1 = all_97_1 % 13.88/2.77 | | | % 13.88/2.77 | | | COMBINE_EQS: (293), (300) imply: % 13.88/2.77 | | | (301) all_97_1 = all_23_0 % 13.88/2.77 | | | % 13.88/2.77 | | | COMBINE_EQS: (296), (301) imply: % 13.88/2.77 | | | (302) all_155_0 = all_23_0 % 13.88/2.77 | | | % 13.88/2.77 | | | REDUCE: (291), (302) imply: % 13.88/2.77 | | | (303) $false % 13.88/2.77 | | | % 13.88/2.77 | | | CLOSE: (303) is inconsistent. % 13.88/2.77 | | | % 13.88/2.77 | | End of split % 13.88/2.77 | | % 13.88/2.77 | Case 2: % 13.88/2.77 | | % 13.88/2.77 | | (304) ? [v0: any] : ( ~ (v0 = all_15_0) & op2(all_23_0, all_23_0) = v0 & % 13.88/2.77 | | $i(v0)) % 13.88/2.77 | | % 13.88/2.77 | | DELTA: instantiating (304) with fresh symbol all_151_0 gives: % 13.88/2.77 | | (305) ~ (all_151_0 = all_15_0) & op2(all_23_0, all_23_0) = all_151_0 & % 13.88/2.77 | | $i(all_151_0) % 13.88/2.77 | | % 13.88/2.77 | | ALPHA: (305) implies: % 13.88/2.77 | | (306) ~ (all_151_0 = all_15_0) % 13.88/2.77 | | (307) op2(all_23_0, all_23_0) = all_151_0 % 13.88/2.77 | | % 13.88/2.77 | | GROUND_INST: instantiating (13) with all_15_0, all_151_0, all_23_0, % 13.88/2.77 | | all_23_0, simplifying with (127), (307) gives: % 13.88/2.77 | | (308) all_151_0 = all_15_0 % 13.88/2.77 | | % 13.88/2.77 | | REDUCE: (306), (308) imply: % 13.88/2.77 | | (309) $false % 13.88/2.77 | | % 13.88/2.77 | | CLOSE: (309) is inconsistent. % 13.88/2.77 | | % 13.88/2.77 | End of split % 13.88/2.77 | % 13.88/2.77 End of proof % 13.88/2.77 % SZS output end Proof for theBenchmark % 13.88/2.77 % 13.88/2.77 2174ms %------------------------------------------------------------------------------