%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV122+1 : TPTP v8.1.2. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n026.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 22:55:00 EDT 2023 % Result : Theorem 30.88s 4.99s % Output : Proof 60.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWV122+1 : TPTP v8.1.2. Bugfixed v3.3.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.35 % Computer : n026.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Tue Aug 29 04:10:35 EDT 2023 % 0.15/0.35 % CPUTime : % 0.22/0.62 ________ _____ % 0.22/0.62 ___ __ \_________(_)________________________________ % 0.22/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.22/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.22/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.22/0.62 % 0.22/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.22/0.62 (2023-06-19) % 0.22/0.62 % 0.22/0.62 (c) Philipp Rümmer, 2009-2023 % 0.22/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.22/0.62 Amanda Stjerna. % 0.22/0.62 Free software under BSD-3-Clause. % 0.22/0.62 % 0.22/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.22/0.62 % 0.22/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.22/0.63 Running up to 7 provers in parallel. % 0.22/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.22/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.22/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.22/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.22/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.22/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.22/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.08/1.47 Prover 4: Preprocessing ... % 5.08/1.47 Prover 1: Preprocessing ... % 5.08/1.49 Prover 2: Preprocessing ... % 5.08/1.49 Prover 0: Preprocessing ... % 5.08/1.49 Prover 3: Preprocessing ... % 5.08/1.50 Prover 6: Preprocessing ... % 5.08/1.50 Prover 5: Preprocessing ... % 10.84/2.34 Prover 1: Warning: ignoring some quantifiers % 12.11/2.48 Prover 1: Constructing countermodel ... % 12.11/2.48 Prover 3: Warning: ignoring some quantifiers % 12.51/2.51 Prover 3: Constructing countermodel ... % 13.06/2.56 Prover 6: Proving ... % 13.19/2.58 Prover 4: Warning: ignoring some quantifiers % 13.70/2.71 Prover 4: Constructing countermodel ... % 13.70/2.72 Prover 5: Proving ... % 14.27/2.74 Prover 2: Proving ... % 14.69/2.79 Prover 0: Proving ... % 30.88/4.99 Prover 3: proved (4341ms) % 30.88/4.99 % 30.88/4.99 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.88/4.99 % 30.88/4.99 Prover 2: stopped % 30.88/4.99 Prover 5: stopped % 30.88/5.00 Prover 0: stopped % 30.88/5.00 Prover 6: stopped % 30.88/5.01 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 30.88/5.01 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 30.88/5.01 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 30.88/5.01 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 30.88/5.01 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 32.60/5.19 Prover 13: Preprocessing ... % 32.60/5.19 Prover 7: Preprocessing ... % 32.90/5.22 Prover 11: Preprocessing ... % 32.90/5.23 Prover 10: Preprocessing ... % 33.09/5.28 Prover 8: Preprocessing ... % 34.24/5.40 Prover 10: Warning: ignoring some quantifiers % 34.24/5.42 Prover 10: Constructing countermodel ... % 34.84/5.46 Prover 8: Warning: ignoring some quantifiers % 35.03/5.51 Prover 8: Constructing countermodel ... % 35.30/5.52 Prover 13: Warning: ignoring some quantifiers % 35.30/5.53 Prover 7: Warning: ignoring some quantifiers % 35.40/5.54 Prover 13: Constructing countermodel ... % 35.40/5.57 Prover 11: Warning: ignoring some quantifiers % 35.40/5.57 Prover 7: Constructing countermodel ... % 35.40/5.60 Prover 11: Constructing countermodel ... % 58.55/8.66 Prover 4: Found proof (size 409) % 58.55/8.66 Prover 4: proved (8008ms) % 58.55/8.66 Prover 13: stopped % 58.55/8.66 Prover 7: stopped % 58.55/8.66 Prover 11: stopped % 58.55/8.66 Prover 10: stopped % 58.55/8.66 Prover 8: stopped % 58.55/8.66 Prover 1: stopped % 58.55/8.66 % 58.55/8.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 58.55/8.66 % 59.81/8.77 % SZS output start Proof for theBenchmark % 59.81/8.77 Assumptions after simplification: % 59.81/8.77 --------------------------------- % 59.81/8.77 % 59.81/8.77 (gt_3_0) % 59.96/8.80 gt(n3, n0) = 0 & $i(n3) & $i(n0) % 59.96/8.80 % 59.96/8.80 (gt_3_1) % 59.96/8.80 gt(n3, n1) = 0 & $i(n3) & $i(n1) % 59.96/8.80 % 59.96/8.80 (gt_3_2) % 59.96/8.80 gt(n3, n2) = 0 & $i(n3) & $i(n2) % 59.96/8.80 % 59.96/8.80 (gt_3_tptp_minus_1) % 59.96/8.80 gt(n3, tptp_minus_1) = 0 & $i(n3) & $i(tptp_minus_1) % 59.96/8.80 % 59.96/8.80 (gt_6_0) % 59.96/8.80 gt(n6, n0) = 0 & $i(n6) & $i(n0) % 59.96/8.80 % 59.96/8.80 (gt_6_1) % 59.96/8.80 gt(n6, n1) = 0 & $i(n6) & $i(n1) % 59.96/8.80 % 59.96/8.80 (gt_6_2) % 59.96/8.80 gt(n6, n2) = 0 & $i(n6) & $i(n2) % 59.96/8.80 % 59.96/8.80 (gt_6_3) % 59.96/8.80 gt(n6, n3) = 0 & $i(n6) & $i(n3) % 59.96/8.80 % 59.96/8.80 (gt_6_4) % 59.96/8.80 gt(n6, n4) = 0 & $i(n6) & $i(n4) % 59.96/8.80 % 59.96/8.80 (gt_6_5) % 59.96/8.81 gt(n6, n5) = 0 & $i(n6) & $i(n5) % 59.96/8.81 % 59.96/8.81 (gt_6_tptp_minus_1) % 59.96/8.81 gt(n6, tptp_minus_1) = 0 & $i(n6) & $i(tptp_minus_1) % 59.96/8.81 % 59.96/8.81 (leq_gt_pred) % 59.96/8.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 59.96/8.81 (pred(v1) = v2) | ~ (leq(v0, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 59.96/8.81 int] : ( ~ (v4 = 0) & gt(v1, v0) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 59.96/8.81 [v2: int] : (v2 = 0 | ~ (gt(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 59.96/8.81 $i] : ? [v4: int] : ( ~ (v4 = 0) & pred(v1) = v3 & leq(v0, v3) = v4 & % 59.96/8.81 $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (pred(v1) = v2) | % 59.96/8.81 ~ (leq(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0) | gt(v1, v0) = 0) & ! [v0: $i] % 59.96/8.81 : ! [v1: $i] : ( ~ (gt(v1, v0) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : % 59.96/8.81 (pred(v1) = v2 & leq(v0, v2) = 0 & $i(v2))) % 59.96/8.81 % 59.96/8.81 (pred_minus_1) % 59.96/8.81 $i(n1) & ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 59.96/8.81 (pred(v0) = v1 & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (pred(v0) = v1) % 59.96/8.81 | ~ $i(v0) | (minus(v0, n1) = v1 & $i(v1))) % 59.96/8.81 % 59.96/8.81 (pred_succ) % 59.96/8.81 ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) | ~ $i(v0) | pred(v1) = v0) % 59.96/8.81 % 59.96/8.81 (quaternion_ds1_symm_0015) % 59.96/8.83 $i(pminus_ds1_filter) & $i(r_ds1_filter) & $i(q_ds1_filter) & $i(n6) & $i(n3) % 59.96/8.83 & $i(n1) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? % 59.96/8.83 [v4: int] : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: $i] : ? [v9: % 59.96/8.83 $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: int] : ? [v13: int] : ? [v14: % 59.96/8.83 int] : ? [v15: int] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: % 59.96/8.83 $i] : ? [v20: int] : ? [v21: int] : ? [v22: int] : ? [v23: int] : ? % 59.96/8.83 [v24: $i] : ? [v25: $i] : (minus(n6, n1) = v0 & minus(n3, n1) = v1 & $i(v19) % 59.96/8.83 & $i(v18) & $i(v11) & $i(v10) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v26: % 59.96/8.83 $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(pminus_ds1_filter, v27, % 59.96/8.83 v26) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: any] % 59.96/8.83 : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 59.96/8.83 (a_select3(pminus_ds1_filter, v26, v27) = v33 & leq(v27, v0) = v32 & % 59.96/8.83 leq(v26, v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) & % 59.96/8.83 ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = % 59.96/8.83 v28))) & ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ % 59.96/8.83 (a_select3(pminus_ds1_filter, v26, v27) = v28) | ~ $i(v27) | ~ $i(v26) | % 59.96/8.83 ? [v29: any] : ? [v30: any] : ? [v31: any] : ? [v32: any] : ? [v33: % 59.96/8.83 $i] : (a_select3(pminus_ds1_filter, v27, v26) = v33 & leq(v27, v0) = v32 % 59.96/8.83 & leq(v26, v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) % 59.96/8.83 & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = % 59.96/8.83 v28))) & ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ % 59.96/8.83 (a_select3(r_ds1_filter, v27, v26) = v28) | ~ $i(v27) | ~ $i(v26) | ? % 59.96/8.83 [v29: any] : ? [v30: any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] % 59.96/8.83 : (a_select3(r_ds1_filter, v26, v27) = v33 & leq(v27, v1) = v32 & leq(v26, % 59.96/8.83 v1) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ % 59.96/8.83 (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) % 59.96/8.83 & ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(r_ds1_filter, % 59.96/8.83 v26, v27) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: % 59.96/8.83 any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 59.96/8.83 (a_select3(r_ds1_filter, v27, v26) = v33 & leq(v27, v1) = v32 & leq(v26, % 59.96/8.83 v1) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ % 59.96/8.83 (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) % 59.96/8.83 & ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(q_ds1_filter, % 59.96/8.83 v27, v26) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: % 59.96/8.83 any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 59.96/8.83 (a_select3(q_ds1_filter, v26, v27) = v33 & leq(v27, v0) = v32 & leq(v26, % 59.96/8.83 v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ % 59.96/8.83 (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) % 59.96/8.83 & ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(q_ds1_filter, % 59.96/8.83 v26, v27) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: % 59.96/8.83 any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 59.96/8.83 (a_select3(q_ds1_filter, v27, v26) = v33 & leq(v27, v0) = v32 & leq(v26, % 59.96/8.83 v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ % 59.96/8.83 (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) % 59.96/8.83 & ((v23 = 0 & v22 = 0 & v21 = 0 & v20 = 0 & ~ (v25 = v24) & % 59.96/8.83 a_select3(q_ds1_filter, v19, v18) = v25 & a_select3(q_ds1_filter, v18, % 59.96/8.83 v19) = v24 & leq(v19, v0) = 0 & leq(v18, v0) = 0 & leq(n0, v19) = 0 & % 59.96/8.83 leq(n0, v18) = 0 & $i(v25) & $i(v24)) | (v15 = 0 & v14 = 0 & v13 = 0 & % 59.96/8.83 v12 = 0 & ~ (v17 = v16) & a_select3(r_ds1_filter, v11, v10) = v17 & % 59.96/8.83 a_select3(r_ds1_filter, v10, v11) = v16 & leq(v11, v1) = 0 & leq(v10, % 59.96/8.83 v1) = 0 & leq(n0, v11) = 0 & leq(n0, v10) = 0 & $i(v17) & $i(v16)) | % 59.96/8.83 (v7 = 0 & v6 = 0 & v5 = 0 & v4 = 0 & ~ (v9 = v8) & % 59.96/8.83 a_select3(pminus_ds1_filter, v3, v2) = v9 & a_select3(pminus_ds1_filter, % 59.96/8.83 v2, v3) = v8 & leq(v3, v0) = 0 & leq(v2, v0) = 0 & leq(n0, v3) = 0 & % 59.96/8.83 leq(n0, v2) = 0 & $i(v9) & $i(v8)))) % 59.96/8.83 % 59.96/8.83 (succ_plus_1_l) % 59.96/8.83 $i(n1) & ! [v0: $i] : ! [v1: $i] : ( ~ (plus(n1, v0) = v1) | ~ $i(v0) | % 59.96/8.83 (succ(v0) = v1 & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) % 59.96/8.83 | ~ $i(v0) | (plus(n1, v0) = v1 & $i(v1))) % 59.96/8.83 % 59.96/8.83 (succ_plus_1_r) % 59.96/8.83 $i(n1) & ! [v0: $i] : ! [v1: $i] : ( ~ (plus(v0, n1) = v1) | ~ $i(v0) | % 59.96/8.83 (succ(v0) = v1 & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) % 59.96/8.83 | ~ $i(v0) | (plus(v0, n1) = v1 & $i(v1))) % 59.96/8.83 % 59.96/8.83 (successor_1) % 59.96/8.83 succ(n0) = n1 & $i(n1) & $i(n0) % 59.96/8.83 % 59.96/8.83 (successor_2) % 59.96/8.83 $i(n2) & $i(n0) & ? [v0: $i] : (succ(v0) = n2 & succ(n0) = v0 & $i(v0)) % 59.96/8.83 % 59.96/8.83 (successor_3) % 59.96/8.83 $i(n3) & $i(n0) & ? [v0: $i] : ? [v1: $i] : (succ(v1) = n3 & succ(v0) = v1 & % 59.96/8.83 succ(n0) = v0 & $i(v1) & $i(v0)) % 59.96/8.83 % 59.96/8.83 (successor_4) % 60.14/8.83 $i(n4) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (succ(v2) = n4 & % 60.14/8.83 succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 & $i(v2) & $i(v1) & $i(v0)) % 60.14/8.83 % 60.14/8.83 (successor_5) % 60.14/8.83 $i(n5) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 60.14/8.83 (succ(v3) = n5 & succ(v2) = v3 & succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 % 60.14/8.83 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.14/8.83 % 60.14/8.83 (successor_6) % 60.15/8.83 $i(n6) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? % 60.15/8.83 [v4: $i] : (succ(v4) = n6 & succ(v3) = v4 & succ(v2) = v3 & succ(v1) = v2 & % 60.15/8.83 succ(v0) = v1 & succ(n0) = v0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.15/8.83 % 60.15/8.83 (function-axioms) % 60.15/8.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 60.15/8.84 $i] : (v1 = v0 | ~ (tptp_update3(v5, v4, v3, v2) = v1) | ~ % 60.15/8.84 (tptp_update3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 60.15/8.84 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_update2(v4, v3, v2) = % 60.15/8.84 v1) | ~ (tptp_update2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 60.15/8.84 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sum(v4, v3, v2) = v1) | % 60.15/8.84 ~ (sum(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 60.15/8.84 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_const_array2(v4, v3, v2) = v1) | % 60.15/8.84 ~ (tptp_const_array2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 60.15/8.84 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (a_select3(v4, v3, v2) = % 60.15/8.84 v1) | ~ (a_select3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 60.15/8.84 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (minus(v3, v2) = v1) | ~ (minus(v3, % 60.15/8.84 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 60.15/8.84 = v0 | ~ (plus(v3, v2) = v1) | ~ (plus(v3, v2) = v0)) & ! [v0: $i] : ! % 60.15/8.84 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_mmul(v3, v2) = v1) % 60.15/8.84 | ~ (tptp_mmul(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 60.15/8.84 ! [v3: $i] : (v1 = v0 | ~ (tptp_msub(v3, v2) = v1) | ~ (tptp_msub(v3, v2) = % 60.15/8.84 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 60.15/8.84 ~ (tptp_madd(v3, v2) = v1) | ~ (tptp_madd(v3, v2) = v0)) & ! [v0: $i] : ! % 60.15/8.84 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (dim(v3, v2) = v1) | ~ % 60.15/8.84 (dim(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 60.15/8.84 : (v1 = v0 | ~ (tptp_const_array1(v3, v2) = v1) | ~ (tptp_const_array1(v3, % 60.15/8.84 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 60.15/8.84 = v0 | ~ (a_select2(v3, v2) = v1) | ~ (a_select2(v3, v2) = v0)) & ! [v0: % 60.15/8.84 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 60.15/8.84 (uniform_int_rnd(v3, v2) = v1) | ~ (uniform_int_rnd(v3, v2) = v0)) & ! % 60.15/8.84 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 60.15/8.84 $i] : (v1 = v0 | ~ (geq(v3, v2) = v1) | ~ (geq(v3, v2) = v0)) & ! [v0: % 60.15/8.84 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 60.15/8.84 : (v1 = v0 | ~ (lt(v3, v2) = v1) | ~ (lt(v3, v2) = v0)) & ! [v0: % 60.15/8.84 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 60.15/8.84 : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) & ! [v0: % 60.15/8.84 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 60.15/8.84 : (v1 = v0 | ~ (gt(v3, v2) = v1) | ~ (gt(v3, v2) = v0)) & ! [v0: $i] : ! % 60.15/8.84 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (inv(v2) = v1) | ~ (inv(v2) = v0)) & % 60.15/8.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (trans(v2) = v1) | ~ % 60.15/8.84 (trans(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 60.15/8.84 (succ(v2) = v1) | ~ (succ(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 60.15/8.84 $i] : (v1 = v0 | ~ (pred(v2) = v1) | ~ (pred(v2) = v0)) % 60.15/8.84 % 60.15/8.84 Further assumptions not needed in the proof: % 60.15/8.84 -------------------------------------------- % 60.15/8.84 const_array1_select, const_array2_select, defuse, finite_domain_0, % 60.15/8.84 finite_domain_1, finite_domain_2, finite_domain_3, finite_domain_4, % 60.15/8.84 finite_domain_5, finite_domain_6, gt_0_tptp_minus_1, gt_1_0, gt_1_tptp_minus_1, % 60.15/8.84 gt_2_0, gt_2_1, gt_2_tptp_minus_1, gt_4_0, gt_4_1, gt_4_2, gt_4_3, % 60.15/8.84 gt_4_tptp_minus_1, gt_5_0, gt_5_1, gt_5_2, gt_5_3, gt_5_4, gt_5_tptp_minus_1, % 60.15/8.84 gt_succ, irreflexivity_gt, leq_geq, leq_gt1, leq_gt2, leq_minus, leq_succ, % 60.15/8.84 leq_succ_gt, leq_succ_gt_equiv, leq_succ_succ, lt_gt, matrix_symm_aba1, % 60.15/8.84 matrix_symm_aba2, matrix_symm_add, matrix_symm_inv, matrix_symm_joseph_update, % 60.15/8.84 matrix_symm_sub, matrix_symm_trans, matrix_symm_update_diagonal, % 60.15/8.84 reflexivity_leq, sel2_update_1, sel2_update_2, sel2_update_3, sel3_update_1, % 60.15/8.84 sel3_update_2, sel3_update_3, succ_plus_2_l, succ_plus_2_r, succ_plus_3_l, % 60.15/8.84 succ_plus_3_r, succ_plus_4_l, succ_plus_4_r, succ_plus_5_l, succ_plus_5_r, % 60.15/8.84 succ_pred, succ_tptp_minus_1, sum_plus_base, sum_plus_base_float, totality, % 60.15/8.84 transitivity_gt, transitivity_leq, ttrue, uniform_int_rand_ranges_hi, % 60.15/8.84 uniform_int_rand_ranges_lo % 60.15/8.84 % 60.15/8.84 Those formulas are unsatisfiable: % 60.15/8.84 --------------------------------- % 60.15/8.84 % 60.15/8.84 Begin of proof % 60.15/8.85 | % 60.15/8.85 | ALPHA: (leq_gt_pred) implies: % 60.15/8.85 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (gt(v1, v0) = 0) | ~ $i(v1) | ~ % 60.15/8.85 | $i(v0) | ? [v2: $i] : (pred(v1) = v2 & leq(v0, v2) = 0 & $i(v2))) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (succ_plus_1_r) implies: % 60.15/8.85 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) | ~ $i(v0) | (plus(v0, % 60.15/8.85 | n1) = v1 & $i(v1))) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (succ_plus_1_l) implies: % 60.15/8.85 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) | ~ $i(v0) | (plus(n1, % 60.15/8.85 | v0) = v1 & $i(v1))) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (pred_minus_1) implies: % 60.15/8.85 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 60.15/8.85 | (pred(v0) = v1 & $i(v1))) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_4) implies: % 60.15/8.85 | (5) gt(n6, n4) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_5) implies: % 60.15/8.85 | (6) gt(n6, n5) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_tptp_minus_1) implies: % 60.15/8.85 | (7) gt(n6, tptp_minus_1) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_3_tptp_minus_1) implies: % 60.15/8.85 | (8) $i(tptp_minus_1) % 60.15/8.85 | (9) gt(n3, tptp_minus_1) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_0) implies: % 60.15/8.85 | (10) gt(n6, n0) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_3_0) implies: % 60.15/8.85 | (11) gt(n3, n0) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_1) implies: % 60.15/8.85 | (12) gt(n6, n1) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_3_1) implies: % 60.15/8.85 | (13) gt(n3, n1) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_2) implies: % 60.15/8.85 | (14) gt(n6, n2) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_3_2) implies: % 60.15/8.85 | (15) gt(n3, n2) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (gt_6_3) implies: % 60.15/8.85 | (16) gt(n6, n3) = 0 % 60.15/8.85 | % 60.15/8.85 | ALPHA: (successor_4) implies: % 60.15/8.85 | (17) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (succ(v2) = n4 & succ(v1) = % 60.15/8.85 | v2 & succ(v0) = v1 & succ(n0) = v0 & $i(v2) & $i(v1) & $i(v0)) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (successor_5) implies: % 60.15/8.85 | (18) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (succ(v3) = n5 % 60.15/8.85 | & succ(v2) = v3 & succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 & % 60.15/8.85 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (successor_6) implies: % 60.15/8.85 | (19) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 60.15/8.85 | (succ(v4) = n6 & succ(v3) = v4 & succ(v2) = v3 & succ(v1) = v2 & % 60.15/8.85 | succ(v0) = v1 & succ(n0) = v0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 60.15/8.85 | $i(v0)) % 60.15/8.85 | % 60.15/8.85 | ALPHA: (successor_1) implies: % 60.15/8.86 | (20) succ(n0) = n1 % 60.15/8.86 | % 60.15/8.86 | ALPHA: (successor_2) implies: % 60.15/8.86 | (21) ? [v0: $i] : (succ(v0) = n2 & succ(n0) = v0 & $i(v0)) % 60.15/8.86 | % 60.15/8.86 | ALPHA: (successor_3) implies: % 60.15/8.86 | (22) ? [v0: $i] : ? [v1: $i] : (succ(v1) = n3 & succ(v0) = v1 & succ(n0) % 60.15/8.86 | = v0 & $i(v1) & $i(v0)) % 60.15/8.86 | % 60.15/8.86 | ALPHA: (quaternion_ds1_symm_0015) implies: % 60.15/8.86 | (23) $i(n0) % 60.15/8.86 | (24) $i(n6) % 60.15/8.87 | (25) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : % 60.15/8.87 | ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: $i] : ? [v9: $i] % 60.15/8.87 | : ? [v10: $i] : ? [v11: $i] : ? [v12: int] : ? [v13: int] : ? % 60.15/8.87 | [v14: int] : ? [v15: int] : ? [v16: $i] : ? [v17: $i] : ? [v18: % 60.15/8.87 | $i] : ? [v19: $i] : ? [v20: int] : ? [v21: int] : ? [v22: int] : % 60.15/8.87 | ? [v23: int] : ? [v24: $i] : ? [v25: $i] : (minus(n6, n1) = v0 & % 60.15/8.87 | minus(n3, n1) = v1 & $i(v19) & $i(v18) & $i(v11) & $i(v10) & $i(v3) % 60.15/8.87 | & $i(v2) & $i(v1) & $i(v0) & ! [v26: $i] : ! [v27: $i] : ! [v28: % 60.15/8.87 | $i] : ( ~ (a_select3(pminus_ds1_filter, v27, v26) = v28) | ~ % 60.15/8.87 | $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: any] : ? [v31: % 60.15/8.87 | any] : ? [v32: any] : ? [v33: $i] : % 60.15/8.87 | (a_select3(pminus_ds1_filter, v26, v27) = v33 & leq(v27, v0) = v32 % 60.15/8.87 | & leq(v26, v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & % 60.15/8.87 | $i(v33) & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 % 60.15/8.87 | = 0) | v33 = v28))) & ! [v26: $i] : ! [v27: $i] : ! [v28: % 60.15/8.87 | $i] : ( ~ (a_select3(pminus_ds1_filter, v26, v27) = v28) | ~ % 60.15/8.87 | $i(v27) | ~ $i(v26) | ? [v29: any] : ? [v30: any] : ? [v31: % 60.15/8.87 | any] : ? [v32: any] : ? [v33: $i] : % 60.15/8.87 | (a_select3(pminus_ds1_filter, v27, v26) = v33 & leq(v27, v0) = v32 % 60.15/8.87 | & leq(v26, v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & % 60.15/8.87 | $i(v33) & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 % 60.15/8.87 | = 0) | v33 = v28))) & ! [v26: $i] : ! [v27: $i] : ! [v28: % 60.15/8.87 | $i] : ( ~ (a_select3(r_ds1_filter, v27, v26) = v28) | ~ $i(v27) | % 60.15/8.87 | ~ $i(v26) | ? [v29: any] : ? [v30: any] : ? [v31: any] : ? % 60.15/8.87 | [v32: any] : ? [v33: $i] : (a_select3(r_ds1_filter, v26, v27) = % 60.15/8.87 | v33 & leq(v27, v1) = v32 & leq(v26, v1) = v31 & leq(n0, v27) = % 60.15/8.87 | v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ (v32 = 0) | ~ (v31 = % 60.15/8.87 | 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) & ! [v26: % 60.15/8.87 | $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(r_ds1_filter, % 60.15/8.87 | v26, v27) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : % 60.15/8.87 | ? [v30: any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 60.15/8.87 | (a_select3(r_ds1_filter, v27, v26) = v33 & leq(v27, v1) = v32 & % 60.15/8.87 | leq(v26, v1) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & % 60.15/8.87 | $i(v33) & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 % 60.15/8.87 | = 0) | v33 = v28))) & ! [v26: $i] : ! [v27: $i] : ! [v28: % 60.15/8.87 | $i] : ( ~ (a_select3(q_ds1_filter, v27, v26) = v28) | ~ $i(v27) | % 60.15/8.87 | ~ $i(v26) | ? [v29: any] : ? [v30: any] : ? [v31: any] : ? % 60.15/8.87 | [v32: any] : ? [v33: $i] : (a_select3(q_ds1_filter, v26, v27) = % 60.15/8.87 | v33 & leq(v27, v0) = v32 & leq(v26, v0) = v31 & leq(n0, v27) = % 60.15/8.87 | v30 & leq(n0, v26) = v29 & $i(v33) & ( ~ (v32 = 0) | ~ (v31 = % 60.15/8.87 | 0) | ~ (v30 = 0) | ~ (v29 = 0) | v33 = v28))) & ! [v26: % 60.15/8.87 | $i] : ! [v27: $i] : ! [v28: $i] : ( ~ (a_select3(q_ds1_filter, % 60.15/8.87 | v26, v27) = v28) | ~ $i(v27) | ~ $i(v26) | ? [v29: any] : % 60.15/8.87 | ? [v30: any] : ? [v31: any] : ? [v32: any] : ? [v33: $i] : % 60.15/8.87 | (a_select3(q_ds1_filter, v27, v26) = v33 & leq(v27, v0) = v32 & % 60.15/8.87 | leq(v26, v0) = v31 & leq(n0, v27) = v30 & leq(n0, v26) = v29 & % 60.15/8.87 | $i(v33) & ( ~ (v32 = 0) | ~ (v31 = 0) | ~ (v30 = 0) | ~ (v29 % 60.15/8.87 | = 0) | v33 = v28))) & ((v23 = 0 & v22 = 0 & v21 = 0 & v20 = % 60.15/8.87 | 0 & ~ (v25 = v24) & a_select3(q_ds1_filter, v19, v18) = v25 & % 60.15/8.87 | a_select3(q_ds1_filter, v18, v19) = v24 & leq(v19, v0) = 0 & % 60.15/8.87 | leq(v18, v0) = 0 & leq(n0, v19) = 0 & leq(n0, v18) = 0 & $i(v25) % 60.15/8.87 | & $i(v24)) | (v15 = 0 & v14 = 0 & v13 = 0 & v12 = 0 & ~ (v17 = % 60.15/8.87 | v16) & a_select3(r_ds1_filter, v11, v10) = v17 & % 60.15/8.87 | a_select3(r_ds1_filter, v10, v11) = v16 & leq(v11, v1) = 0 & % 60.15/8.87 | leq(v10, v1) = 0 & leq(n0, v11) = 0 & leq(n0, v10) = 0 & $i(v17) % 60.15/8.87 | & $i(v16)) | (v7 = 0 & v6 = 0 & v5 = 0 & v4 = 0 & ~ (v9 = v8) & % 60.15/8.87 | a_select3(pminus_ds1_filter, v3, v2) = v9 & % 60.15/8.87 | a_select3(pminus_ds1_filter, v2, v3) = v8 & leq(v3, v0) = 0 & % 60.15/8.87 | leq(v2, v0) = 0 & leq(n0, v3) = 0 & leq(n0, v2) = 0 & $i(v9) & % 60.15/8.87 | $i(v8)))) % 60.15/8.87 | % 60.15/8.87 | ALPHA: (function-axioms) implies: % 60.15/8.87 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (pred(v2) = % 60.15/8.87 | v1) | ~ (pred(v2) = v0)) % 60.15/8.87 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (succ(v2) = % 60.15/8.87 | v1) | ~ (succ(v2) = v0)) % 60.15/8.87 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 60.15/8.87 | : ! [v3: $i] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = % 60.15/8.87 | v0)) % 60.15/8.87 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 60.15/8.87 | (v1 = v0 | ~ (a_select3(v4, v3, v2) = v1) | ~ (a_select3(v4, v3, v2) % 60.15/8.87 | = v0)) % 60.15/8.87 | % 60.15/8.87 | DELTA: instantiating (21) with fresh symbol all_50_0 gives: % 60.15/8.87 | (30) succ(all_50_0) = n2 & succ(n0) = all_50_0 & $i(all_50_0) % 60.15/8.87 | % 60.15/8.87 | ALPHA: (30) implies: % 60.15/8.87 | (31) $i(all_50_0) % 60.15/8.87 | (32) succ(n0) = all_50_0 % 60.15/8.87 | (33) succ(all_50_0) = n2 % 60.15/8.87 | % 60.15/8.87 | DELTA: instantiating (22) with fresh symbols all_52_0, all_52_1 gives: % 60.15/8.87 | (34) succ(all_52_0) = n3 & succ(all_52_1) = all_52_0 & succ(n0) = all_52_1 % 60.15/8.87 | & $i(all_52_0) & $i(all_52_1) % 60.15/8.87 | % 60.15/8.87 | ALPHA: (34) implies: % 60.15/8.87 | (35) $i(all_52_0) % 60.15/8.87 | (36) succ(n0) = all_52_1 % 60.15/8.87 | (37) succ(all_52_1) = all_52_0 % 60.15/8.87 | (38) succ(all_52_0) = n3 % 60.15/8.87 | % 60.15/8.87 | DELTA: instantiating (17) with fresh symbols all_54_0, all_54_1, all_54_2 % 60.15/8.87 | gives: % 60.15/8.87 | (39) succ(all_54_0) = n4 & succ(all_54_1) = all_54_0 & succ(all_54_2) = % 60.15/8.87 | all_54_1 & succ(n0) = all_54_2 & $i(all_54_0) & $i(all_54_1) & % 60.15/8.87 | $i(all_54_2) % 60.15/8.87 | % 60.15/8.87 | ALPHA: (39) implies: % 60.15/8.87 | (40) $i(all_54_0) % 60.15/8.87 | (41) succ(n0) = all_54_2 % 60.15/8.87 | (42) succ(all_54_2) = all_54_1 % 60.15/8.87 | (43) succ(all_54_1) = all_54_0 % 60.15/8.87 | (44) succ(all_54_0) = n4 % 60.15/8.87 | % 60.15/8.87 | DELTA: instantiating (18) with fresh symbols all_56_0, all_56_1, all_56_2, % 60.15/8.87 | all_56_3 gives: % 60.15/8.87 | (45) succ(all_56_0) = n5 & succ(all_56_1) = all_56_0 & succ(all_56_2) = % 60.15/8.87 | all_56_1 & succ(all_56_3) = all_56_2 & succ(n0) = all_56_3 & % 60.15/8.87 | $i(all_56_0) & $i(all_56_1) & $i(all_56_2) & $i(all_56_3) % 60.15/8.87 | % 60.15/8.87 | ALPHA: (45) implies: % 60.15/8.87 | (46) $i(all_56_0) % 60.15/8.87 | (47) succ(n0) = all_56_3 % 60.15/8.87 | (48) succ(all_56_3) = all_56_2 % 60.15/8.87 | (49) succ(all_56_2) = all_56_1 % 60.15/8.87 | (50) succ(all_56_1) = all_56_0 % 60.15/8.87 | (51) succ(all_56_0) = n5 % 60.15/8.87 | % 60.15/8.87 | DELTA: instantiating (19) with fresh symbols all_58_0, all_58_1, all_58_2, % 60.15/8.87 | all_58_3, all_58_4 gives: % 60.15/8.88 | (52) succ(all_58_0) = n6 & succ(all_58_1) = all_58_0 & succ(all_58_2) = % 60.15/8.88 | all_58_1 & succ(all_58_3) = all_58_2 & succ(all_58_4) = all_58_3 & % 60.15/8.88 | succ(n0) = all_58_4 & $i(all_58_0) & $i(all_58_1) & $i(all_58_2) & % 60.15/8.88 | $i(all_58_3) & $i(all_58_4) % 60.15/8.88 | % 60.15/8.88 | ALPHA: (52) implies: % 60.15/8.88 | (53) $i(all_58_0) % 60.15/8.88 | (54) succ(n0) = all_58_4 % 60.15/8.88 | (55) succ(all_58_4) = all_58_3 % 60.15/8.88 | (56) succ(all_58_3) = all_58_2 % 60.15/8.88 | (57) succ(all_58_2) = all_58_1 % 60.15/8.88 | (58) succ(all_58_1) = all_58_0 % 60.15/8.88 | (59) succ(all_58_0) = n6 % 60.15/8.88 | % 60.15/8.88 | DELTA: instantiating (25) with fresh symbols all_96_0, all_96_1, all_96_2, % 60.15/8.88 | all_96_3, all_96_4, all_96_5, all_96_6, all_96_7, all_96_8, all_96_9, % 60.15/8.88 | all_96_10, all_96_11, all_96_12, all_96_13, all_96_14, all_96_15, % 60.15/8.88 | all_96_16, all_96_17, all_96_18, all_96_19, all_96_20, all_96_21, % 60.15/8.88 | all_96_22, all_96_23, all_96_24, all_96_25 gives: % 60.15/8.88 | (60) minus(n6, n1) = all_96_25 & minus(n3, n1) = all_96_24 & $i(all_96_6) & % 60.15/8.88 | $i(all_96_7) & $i(all_96_14) & $i(all_96_15) & $i(all_96_22) & % 60.15/8.88 | $i(all_96_23) & $i(all_96_24) & $i(all_96_25) & ! [v0: $i] : ! [v1: % 60.15/8.88 | $i] : ! [v2: $i] : ( ~ (a_select3(pminus_ds1_filter, v1, v0) = v2) % 60.15/8.88 | | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 60.15/8.88 | : ? [v6: any] : ? [v7: $i] : (a_select3(pminus_ds1_filter, v0, v1) % 60.15/8.88 | = v7 & leq(v1, all_96_25) = v6 & leq(v0, all_96_25) = v5 & leq(n0, % 60.15/8.88 | v1) = v4 & leq(n0, v0) = v3 & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = % 60.15/8.88 | 0) | ~ (v4 = 0) | ~ (v3 = 0) | v7 = v2))) & ! [v0: $i] : ! % 60.15/8.88 | [v1: $i] : ! [v2: $i] : ( ~ (a_select3(pminus_ds1_filter, v0, v1) = % 60.15/8.88 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? % 60.15/8.88 | [v5: any] : ? [v6: any] : ? [v7: $i] : % 60.15/8.88 | (a_select3(pminus_ds1_filter, v1, v0) = v7 & leq(v1, all_96_25) = v6 % 60.15/8.88 | & leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.88 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.88 | v7 = v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.88 | (a_select3(r_ds1_filter, v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 60.15/8.88 | [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] % 60.15/8.88 | : (a_select3(r_ds1_filter, v0, v1) = v7 & leq(v1, all_96_24) = v6 & % 60.15/8.88 | leq(v0, all_96_24) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.88 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.88 | v7 = v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.88 | (a_select3(r_ds1_filter, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 60.15/8.88 | [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] % 60.15/8.88 | : (a_select3(r_ds1_filter, v1, v0) = v7 & leq(v1, all_96_24) = v6 & % 60.15/8.88 | leq(v0, all_96_24) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.88 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.88 | v7 = v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.88 | (a_select3(q_ds1_filter, v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 60.15/8.88 | [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] % 60.15/8.88 | : (a_select3(q_ds1_filter, v0, v1) = v7 & leq(v1, all_96_25) = v6 & % 60.15/8.88 | leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.88 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.88 | v7 = v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.88 | (a_select3(q_ds1_filter, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 60.15/8.88 | [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] % 60.15/8.88 | : (a_select3(q_ds1_filter, v1, v0) = v7 & leq(v1, all_96_25) = v6 & % 60.15/8.88 | leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.88 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.88 | v7 = v2))) & ((all_96_2 = 0 & all_96_3 = 0 & all_96_4 = 0 & % 60.15/8.88 | all_96_5 = 0 & ~ (all_96_0 = all_96_1) & a_select3(q_ds1_filter, % 60.15/8.88 | all_96_6, all_96_7) = all_96_0 & a_select3(q_ds1_filter, % 60.15/8.88 | all_96_7, all_96_6) = all_96_1 & leq(all_96_6, all_96_25) = 0 & % 60.15/8.88 | leq(all_96_7, all_96_25) = 0 & leq(n0, all_96_6) = 0 & leq(n0, % 60.15/8.88 | all_96_7) = 0 & $i(all_96_0) & $i(all_96_1)) | (all_96_10 = 0 & % 60.15/8.88 | all_96_11 = 0 & all_96_12 = 0 & all_96_13 = 0 & ~ (all_96_8 = % 60.15/8.88 | all_96_9) & a_select3(r_ds1_filter, all_96_14, all_96_15) = % 60.15/8.88 | all_96_8 & a_select3(r_ds1_filter, all_96_15, all_96_14) = % 60.15/8.88 | all_96_9 & leq(all_96_14, all_96_24) = 0 & leq(all_96_15, % 60.15/8.88 | all_96_24) = 0 & leq(n0, all_96_14) = 0 & leq(n0, all_96_15) = 0 % 60.15/8.88 | & $i(all_96_8) & $i(all_96_9)) | (all_96_18 = 0 & all_96_19 = 0 & % 60.15/8.88 | all_96_20 = 0 & all_96_21 = 0 & ~ (all_96_16 = all_96_17) & % 60.15/8.88 | a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_96_16 & % 60.15/8.88 | a_select3(pminus_ds1_filter, all_96_23, all_96_22) = all_96_17 & % 60.15/8.88 | leq(all_96_22, all_96_25) = 0 & leq(all_96_23, all_96_25) = 0 & % 60.15/8.88 | leq(n0, all_96_22) = 0 & leq(n0, all_96_23) = 0 & $i(all_96_16) & % 60.15/8.88 | $i(all_96_17))) % 60.15/8.88 | % 60.15/8.88 | ALPHA: (60) implies: % 60.15/8.88 | (61) $i(all_96_23) % 60.15/8.88 | (62) $i(all_96_22) % 60.15/8.88 | (63) $i(all_96_15) % 60.15/8.88 | (64) $i(all_96_14) % 60.15/8.88 | (65) $i(all_96_7) % 60.15/8.88 | (66) $i(all_96_6) % 60.15/8.89 | (67) minus(n3, n1) = all_96_24 % 60.15/8.89 | (68) minus(n6, n1) = all_96_25 % 60.15/8.89 | (69) (all_96_2 = 0 & all_96_3 = 0 & all_96_4 = 0 & all_96_5 = 0 & ~ % 60.15/8.89 | (all_96_0 = all_96_1) & a_select3(q_ds1_filter, all_96_6, all_96_7) % 60.15/8.89 | = all_96_0 & a_select3(q_ds1_filter, all_96_7, all_96_6) = all_96_1 % 60.15/8.89 | & leq(all_96_6, all_96_25) = 0 & leq(all_96_7, all_96_25) = 0 & % 60.15/8.89 | leq(n0, all_96_6) = 0 & leq(n0, all_96_7) = 0 & $i(all_96_0) & % 60.15/8.89 | $i(all_96_1)) | (all_96_10 = 0 & all_96_11 = 0 & all_96_12 = 0 & % 60.15/8.89 | all_96_13 = 0 & ~ (all_96_8 = all_96_9) & a_select3(r_ds1_filter, % 60.15/8.89 | all_96_14, all_96_15) = all_96_8 & a_select3(r_ds1_filter, % 60.15/8.89 | all_96_15, all_96_14) = all_96_9 & leq(all_96_14, all_96_24) = 0 & % 60.15/8.89 | leq(all_96_15, all_96_24) = 0 & leq(n0, all_96_14) = 0 & leq(n0, % 60.15/8.89 | all_96_15) = 0 & $i(all_96_8) & $i(all_96_9)) | (all_96_18 = 0 & % 60.15/8.89 | all_96_19 = 0 & all_96_20 = 0 & all_96_21 = 0 & ~ (all_96_16 = % 60.15/8.89 | all_96_17) & a_select3(pminus_ds1_filter, all_96_22, all_96_23) = % 60.15/8.89 | all_96_16 & a_select3(pminus_ds1_filter, all_96_23, all_96_22) = % 60.15/8.89 | all_96_17 & leq(all_96_22, all_96_25) = 0 & leq(all_96_23, % 60.15/8.89 | all_96_25) = 0 & leq(n0, all_96_22) = 0 & leq(n0, all_96_23) = 0 & % 60.15/8.89 | $i(all_96_16) & $i(all_96_17)) % 60.15/8.89 | (70) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a_select3(q_ds1_filter, % 60.15/8.89 | v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 60.15/8.89 | any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 60.15/8.89 | (a_select3(q_ds1_filter, v1, v0) = v7 & leq(v1, all_96_25) = v6 & % 60.15/8.89 | leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.89 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.89 | v7 = v2))) % 60.15/8.89 | (71) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a_select3(q_ds1_filter, % 60.15/8.89 | v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 60.15/8.89 | any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 60.15/8.89 | (a_select3(q_ds1_filter, v0, v1) = v7 & leq(v1, all_96_25) = v6 & % 60.15/8.89 | leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.89 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.89 | v7 = v2))) % 60.15/8.89 | (72) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a_select3(r_ds1_filter, % 60.15/8.89 | v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 60.15/8.89 | any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 60.15/8.89 | (a_select3(r_ds1_filter, v1, v0) = v7 & leq(v1, all_96_24) = v6 & % 60.15/8.89 | leq(v0, all_96_24) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.89 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.89 | v7 = v2))) % 60.15/8.89 | (73) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a_select3(r_ds1_filter, % 60.15/8.89 | v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 60.15/8.89 | any] : ? [v5: any] : ? [v6: any] : ? [v7: $i] : % 60.15/8.89 | (a_select3(r_ds1_filter, v0, v1) = v7 & leq(v1, all_96_24) = v6 & % 60.15/8.89 | leq(v0, all_96_24) = v5 & leq(n0, v1) = v4 & leq(n0, v0) = v3 & % 60.15/8.89 | $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | % 60.15/8.89 | v7 = v2))) % 60.15/8.89 | (74) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.89 | (a_select3(pminus_ds1_filter, v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 60.15/8.89 | | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? % 60.15/8.89 | [v7: $i] : (a_select3(pminus_ds1_filter, v1, v0) = v7 & leq(v1, % 60.15/8.89 | all_96_25) = v6 & leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & % 60.15/8.89 | leq(n0, v0) = v3 & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = % 60.15/8.89 | 0) | ~ (v3 = 0) | v7 = v2))) % 60.15/8.89 | (75) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 60.15/8.89 | (a_select3(pminus_ds1_filter, v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) % 60.15/8.89 | | ? [v3: any] : ? [v4: any] : ? [v5: any] : ? [v6: any] : ? % 60.15/8.89 | [v7: $i] : (a_select3(pminus_ds1_filter, v0, v1) = v7 & leq(v1, % 60.15/8.89 | all_96_25) = v6 & leq(v0, all_96_25) = v5 & leq(n0, v1) = v4 & % 60.15/8.89 | leq(n0, v0) = v3 & $i(v7) & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = % 60.15/8.89 | 0) | ~ (v3 = 0) | v7 = v2))) % 60.15/8.89 | % 60.15/8.89 | GROUND_INST: instantiating (27) with all_54_2, all_56_3, n0, simplifying with % 60.15/8.89 | (41), (47) gives: % 60.15/8.89 | (76) all_56_3 = all_54_2 % 60.15/8.89 | % 60.15/8.89 | GROUND_INST: instantiating (27) with all_52_1, all_56_3, n0, simplifying with % 60.15/8.89 | (36), (47) gives: % 60.15/8.89 | (77) all_56_3 = all_52_1 % 60.15/8.89 | % 60.15/8.89 | GROUND_INST: instantiating (27) with all_50_0, all_56_3, n0, simplifying with % 60.15/8.89 | (32), (47) gives: % 60.15/8.89 | (78) all_56_3 = all_50_0 % 60.15/8.89 | % 60.15/8.89 | GROUND_INST: instantiating (27) with all_54_2, all_58_4, n0, simplifying with % 60.15/8.89 | (41), (54) gives: % 60.15/8.89 | (79) all_58_4 = all_54_2 % 60.15/8.89 | % 60.15/8.89 | GROUND_INST: instantiating (27) with n1, all_58_4, n0, simplifying with (20), % 60.15/8.89 | (54) gives: % 60.15/8.89 | (80) all_58_4 = n1 % 60.15/8.89 | % 60.15/8.90 | COMBINE_EQS: (79), (80) imply: % 60.15/8.90 | (81) all_54_2 = n1 % 60.15/8.90 | % 60.15/8.90 | SIMP: (81) implies: % 60.15/8.90 | (82) all_54_2 = n1 % 60.15/8.90 | % 60.15/8.90 | COMBINE_EQS: (76), (77) imply: % 60.15/8.90 | (83) all_54_2 = all_52_1 % 60.15/8.90 | % 60.15/8.90 | SIMP: (83) implies: % 60.15/8.90 | (84) all_54_2 = all_52_1 % 60.15/8.90 | % 60.15/8.90 | COMBINE_EQS: (77), (78) imply: % 60.15/8.90 | (85) all_52_1 = all_50_0 % 60.15/8.90 | % 60.15/8.90 | COMBINE_EQS: (82), (84) imply: % 60.15/8.90 | (86) all_52_1 = n1 % 60.15/8.90 | % 60.15/8.90 | SIMP: (86) implies: % 60.15/8.90 | (87) all_52_1 = n1 % 60.15/8.90 | % 60.15/8.90 | COMBINE_EQS: (85), (87) imply: % 60.15/8.90 | (88) all_50_0 = n1 % 60.15/8.90 | % 60.15/8.90 | COMBINE_EQS: (77), (87) imply: % 60.15/8.90 | (89) all_56_3 = n1 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (55), (80) imply: % 60.15/8.90 | (90) succ(n1) = all_58_3 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (48), (89) imply: % 60.15/8.90 | (91) succ(n1) = all_56_2 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (42), (82) imply: % 60.15/8.90 | (92) succ(n1) = all_54_1 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (37), (87) imply: % 60.15/8.90 | (93) succ(n1) = all_52_0 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (33), (88) imply: % 60.15/8.90 | (94) succ(n1) = n2 % 60.15/8.90 | % 60.15/8.90 | REDUCE: (31), (88) imply: % 60.15/8.90 | (95) $i(n1) % 60.15/8.90 | % 60.15/8.90 | GROUND_INST: instantiating (27) with all_54_1, all_56_2, n1, simplifying with % 60.15/8.90 | (91), (92) gives: % 60.15/8.90 | (96) all_56_2 = all_54_1 % 60.15/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with all_52_0, all_56_2, n1, simplifying with % 60.47/8.90 | (91), (93) gives: % 60.47/8.90 | (97) all_56_2 = all_52_0 % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with all_56_2, all_58_3, n1, simplifying with % 60.47/8.90 | (90), (91) gives: % 60.47/8.90 | (98) all_58_3 = all_56_2 % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with n2, all_58_3, n1, simplifying with (90), % 60.47/8.90 | (94) gives: % 60.47/8.90 | (99) all_58_3 = n2 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (98), (99) imply: % 60.47/8.90 | (100) all_56_2 = n2 % 60.47/8.90 | % 60.47/8.90 | SIMP: (100) implies: % 60.47/8.90 | (101) all_56_2 = n2 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (96), (97) imply: % 60.47/8.90 | (102) all_54_1 = all_52_0 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (96), (101) imply: % 60.47/8.90 | (103) all_54_1 = n2 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (102), (103) imply: % 60.47/8.90 | (104) all_52_0 = n2 % 60.47/8.90 | % 60.47/8.90 | SIMP: (104) implies: % 60.47/8.90 | (105) all_52_0 = n2 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (56), (99) imply: % 60.47/8.90 | (106) succ(n2) = all_58_2 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (49), (101) imply: % 60.47/8.90 | (107) succ(n2) = all_56_1 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (43), (103) imply: % 60.47/8.90 | (108) succ(n2) = all_54_0 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (38), (105) imply: % 60.47/8.90 | (109) succ(n2) = n3 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (35), (105) imply: % 60.47/8.90 | (110) $i(n2) % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with all_54_0, all_56_1, n2, simplifying with % 60.47/8.90 | (107), (108) gives: % 60.47/8.90 | (111) all_56_1 = all_54_0 % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with all_56_1, all_58_2, n2, simplifying with % 60.47/8.90 | (106), (107) gives: % 60.47/8.90 | (112) all_58_2 = all_56_1 % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with n3, all_58_2, n2, simplifying with (106), % 60.47/8.90 | (109) gives: % 60.47/8.90 | (113) all_58_2 = n3 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (112), (113) imply: % 60.47/8.90 | (114) all_56_1 = n3 % 60.47/8.90 | % 60.47/8.90 | SIMP: (114) implies: % 60.47/8.90 | (115) all_56_1 = n3 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (111), (115) imply: % 60.47/8.90 | (116) all_54_0 = n3 % 60.47/8.90 | % 60.47/8.90 | SIMP: (116) implies: % 60.47/8.90 | (117) all_54_0 = n3 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (57), (113) imply: % 60.47/8.90 | (118) succ(n3) = all_58_1 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (50), (115) imply: % 60.47/8.90 | (119) succ(n3) = all_56_0 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (44), (117) imply: % 60.47/8.90 | (120) succ(n3) = n4 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (40), (117) imply: % 60.47/8.90 | (121) $i(n3) % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with all_56_0, all_58_1, n3, simplifying with % 60.47/8.90 | (118), (119) gives: % 60.47/8.90 | (122) all_58_1 = all_56_0 % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with n4, all_58_1, n3, simplifying with (118), % 60.47/8.90 | (120) gives: % 60.47/8.90 | (123) all_58_1 = n4 % 60.47/8.90 | % 60.47/8.90 | COMBINE_EQS: (122), (123) imply: % 60.47/8.90 | (124) all_56_0 = n4 % 60.47/8.90 | % 60.47/8.90 | SIMP: (124) implies: % 60.47/8.90 | (125) all_56_0 = n4 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (58), (123) imply: % 60.47/8.90 | (126) succ(n4) = all_58_0 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (51), (125) imply: % 60.47/8.90 | (127) succ(n4) = n5 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (46), (125) imply: % 60.47/8.90 | (128) $i(n4) % 60.47/8.90 | % 60.47/8.90 | GROUND_INST: instantiating (27) with n5, all_58_0, n4, simplifying with (126), % 60.47/8.90 | (127) gives: % 60.47/8.90 | (129) all_58_0 = n5 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (59), (129) imply: % 60.47/8.90 | (130) succ(n5) = n6 % 60.47/8.90 | % 60.47/8.90 | REDUCE: (53), (129) imply: % 60.47/8.90 | (131) $i(n5) % 60.47/8.90 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n0, n3, simplifying with (11), (23), (121) % 60.47/8.91 | gives: % 60.47/8.91 | (132) ? [v0: $i] : (pred(n3) = v0 & leq(n0, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with tptp_minus_1, n3, simplifying with (8), % 60.47/8.91 | (9), (121) gives: % 60.47/8.91 | (133) ? [v0: $i] : (pred(n3) = v0 & leq(tptp_minus_1, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n1, n3, simplifying with (13), (95), (121) % 60.47/8.91 | gives: % 60.47/8.91 | (134) ? [v0: $i] : (pred(n3) = v0 & leq(n1, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n2, n3, simplifying with (15), (110), % 60.47/8.91 | (121) gives: % 60.47/8.91 | (135) ? [v0: $i] : (pred(n3) = v0 & leq(n2, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n0, n6, simplifying with (10), (23), (24) % 60.47/8.91 | gives: % 60.47/8.91 | (136) ? [v0: $i] : (pred(n6) = v0 & leq(n0, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with tptp_minus_1, n6, simplifying with (7), % 60.47/8.91 | (8), (24) gives: % 60.47/8.91 | (137) ? [v0: $i] : (pred(n6) = v0 & leq(tptp_minus_1, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n1, n6, simplifying with (12), (24), (95) % 60.47/8.91 | gives: % 60.47/8.91 | (138) ? [v0: $i] : (pred(n6) = v0 & leq(n1, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n2, n6, simplifying with (14), (24), (110) % 60.47/8.91 | gives: % 60.47/8.91 | (139) ? [v0: $i] : (pred(n6) = v0 & leq(n2, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n3, n6, simplifying with (16), (24), (121) % 60.47/8.91 | gives: % 60.47/8.91 | (140) ? [v0: $i] : (pred(n6) = v0 & leq(n3, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n4, n6, simplifying with (5), (24), (128) % 60.47/8.91 | gives: % 60.47/8.91 | (141) ? [v0: $i] : (pred(n6) = v0 & leq(n4, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (1) with n5, n6, simplifying with (6), (24), (131) % 60.47/8.91 | gives: % 60.47/8.91 | (142) ? [v0: $i] : (pred(n6) = v0 & leq(n5, v0) = 0 & $i(v0)) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (3) with n0, n1, simplifying with (20), (23) gives: % 60.47/8.91 | (143) plus(n1, n0) = n1 & $i(n1) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (2) with n1, n2, simplifying with (94), (95) gives: % 60.47/8.91 | (144) plus(n1, n1) = n2 & $i(n2) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (pred_succ) with n2, n3, simplifying with (109), % 60.47/8.91 | (110) gives: % 60.47/8.91 | (145) pred(n3) = n2 % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (3) with n2, n3, simplifying with (109), (110) % 60.47/8.91 | gives: % 60.47/8.91 | (146) plus(n1, n2) = n3 & $i(n3) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (3) with n3, n4, simplifying with (120), (121) % 60.47/8.91 | gives: % 60.47/8.91 | (147) plus(n1, n3) = n4 & $i(n4) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (3) with n4, n5, simplifying with (127), (128) % 60.47/8.91 | gives: % 60.47/8.91 | (148) plus(n1, n4) = n5 & $i(n5) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (pred_succ) with n5, n6, simplifying with (130), % 60.47/8.91 | (131) gives: % 60.47/8.91 | (149) pred(n6) = n5 % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (3) with n5, n6, simplifying with (130), (131) % 60.47/8.91 | gives: % 60.47/8.91 | (150) plus(n1, n5) = n6 & $i(n6) % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (4) with n3, all_96_24, simplifying with (67), % 60.47/8.91 | (121) gives: % 60.47/8.91 | (151) pred(n3) = all_96_24 & $i(all_96_24) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (151) implies: % 60.47/8.91 | (152) pred(n3) = all_96_24 % 60.47/8.91 | % 60.47/8.91 | GROUND_INST: instantiating (4) with n6, all_96_25, simplifying with (24), (68) % 60.47/8.91 | gives: % 60.47/8.91 | (153) pred(n6) = all_96_25 & $i(all_96_25) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (153) implies: % 60.47/8.91 | (154) pred(n6) = all_96_25 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (133) with fresh symbol all_133_0 gives: % 60.47/8.91 | (155) pred(n3) = all_133_0 & leq(tptp_minus_1, all_133_0) = 0 & % 60.47/8.91 | $i(all_133_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (155) implies: % 60.47/8.91 | (156) pred(n3) = all_133_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (141) with fresh symbol all_145_0 gives: % 60.47/8.91 | (157) pred(n6) = all_145_0 & leq(n4, all_145_0) = 0 & $i(all_145_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (157) implies: % 60.47/8.91 | (158) pred(n6) = all_145_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (137) with fresh symbol all_155_0 gives: % 60.47/8.91 | (159) pred(n6) = all_155_0 & leq(tptp_minus_1, all_155_0) = 0 & % 60.47/8.91 | $i(all_155_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (159) implies: % 60.47/8.91 | (160) pred(n6) = all_155_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (135) with fresh symbol all_167_0 gives: % 60.47/8.91 | (161) pred(n3) = all_167_0 & leq(n2, all_167_0) = 0 & $i(all_167_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (161) implies: % 60.47/8.91 | (162) pred(n3) = all_167_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (134) with fresh symbol all_169_0 gives: % 60.47/8.91 | (163) pred(n3) = all_169_0 & leq(n1, all_169_0) = 0 & $i(all_169_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (163) implies: % 60.47/8.91 | (164) pred(n3) = all_169_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (138) with fresh symbol all_177_0 gives: % 60.47/8.91 | (165) pred(n6) = all_177_0 & leq(n1, all_177_0) = 0 & $i(all_177_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (165) implies: % 60.47/8.91 | (166) pred(n6) = all_177_0 % 60.47/8.91 | % 60.47/8.91 | DELTA: instantiating (136) with fresh symbol all_179_0 gives: % 60.47/8.91 | (167) pred(n6) = all_179_0 & leq(n0, all_179_0) = 0 & $i(all_179_0) % 60.47/8.91 | % 60.47/8.91 | ALPHA: (167) implies: % 60.47/8.92 | (168) pred(n6) = all_179_0 % 60.47/8.92 | % 60.47/8.92 | DELTA: instantiating (140) with fresh symbol all_183_0 gives: % 60.47/8.92 | (169) pred(n6) = all_183_0 & leq(n3, all_183_0) = 0 & $i(all_183_0) % 60.47/8.92 | % 60.47/8.92 | ALPHA: (169) implies: % 60.47/8.92 | (170) pred(n6) = all_183_0 % 60.47/8.92 | % 60.47/8.92 | DELTA: instantiating (139) with fresh symbol all_185_0 gives: % 60.47/8.92 | (171) pred(n6) = all_185_0 & leq(n2, all_185_0) = 0 & $i(all_185_0) % 60.47/8.92 | % 60.47/8.92 | ALPHA: (171) implies: % 60.47/8.92 | (172) pred(n6) = all_185_0 % 60.47/8.92 | % 60.47/8.92 | DELTA: instantiating (142) with fresh symbol all_187_0 gives: % 60.47/8.92 | (173) pred(n6) = all_187_0 & leq(n5, all_187_0) = 0 & $i(all_187_0) % 60.47/8.92 | % 60.47/8.92 | ALPHA: (173) implies: % 60.47/8.92 | (174) pred(n6) = all_187_0 % 60.47/8.92 | % 60.47/8.92 | DELTA: instantiating (132) with fresh symbol all_193_0 gives: % 60.47/8.92 | (175) pred(n3) = all_193_0 & leq(n0, all_193_0) = 0 & $i(all_193_0) % 60.47/8.92 | % 60.47/8.92 | ALPHA: (175) implies: % 60.47/8.92 | (176) pred(n3) = all_193_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_96_24, all_133_0, n3, simplifying % 60.47/8.92 | with (152), (156) gives: % 60.47/8.92 | (177) all_133_0 = all_96_24 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_133_0, all_167_0, n3, simplifying % 60.47/8.92 | with (156), (162) gives: % 60.47/8.92 | (178) all_167_0 = all_133_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_167_0, all_169_0, n3, simplifying % 60.47/8.92 | with (162), (164) gives: % 60.47/8.92 | (179) all_169_0 = all_167_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_169_0, all_193_0, n3, simplifying % 60.47/8.92 | with (164), (176) gives: % 60.47/8.92 | (180) all_193_0 = all_169_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with n2, all_193_0, n3, simplifying with % 60.47/8.92 | (145), (176) gives: % 60.47/8.92 | (181) all_193_0 = n2 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_145_0, all_155_0, n6, simplifying % 60.47/8.92 | with (158), (160) gives: % 60.47/8.92 | (182) all_155_0 = all_145_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_155_0, all_177_0, n6, simplifying % 60.47/8.92 | with (160), (166) gives: % 60.47/8.92 | (183) all_177_0 = all_155_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_96_25, all_183_0, n6, simplifying % 60.47/8.92 | with (154), (170) gives: % 60.47/8.92 | (184) all_183_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_183_0, all_185_0, n6, simplifying % 60.47/8.92 | with (170), (172) gives: % 60.47/8.92 | (185) all_185_0 = all_183_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_179_0, all_185_0, n6, simplifying % 60.47/8.92 | with (168), (172) gives: % 60.47/8.92 | (186) all_185_0 = all_179_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_177_0, all_185_0, n6, simplifying % 60.47/8.92 | with (166), (172) gives: % 60.47/8.92 | (187) all_185_0 = all_177_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with all_145_0, all_187_0, n6, simplifying % 60.47/8.92 | with (158), (174) gives: % 60.47/8.92 | (188) all_187_0 = all_145_0 % 60.47/8.92 | % 60.47/8.92 | GROUND_INST: instantiating (26) with n5, all_187_0, n6, simplifying with % 60.47/8.92 | (149), (174) gives: % 60.47/8.92 | (189) all_187_0 = n5 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (180), (181) imply: % 60.47/8.92 | (190) all_169_0 = n2 % 60.47/8.92 | % 60.47/8.92 | SIMP: (190) implies: % 60.47/8.92 | (191) all_169_0 = n2 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (188), (189) imply: % 60.47/8.92 | (192) all_145_0 = n5 % 60.47/8.92 | % 60.47/8.92 | SIMP: (192) implies: % 60.47/8.92 | (193) all_145_0 = n5 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (185), (186) imply: % 60.47/8.92 | (194) all_183_0 = all_179_0 % 60.47/8.92 | % 60.47/8.92 | SIMP: (194) implies: % 60.47/8.92 | (195) all_183_0 = all_179_0 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (186), (187) imply: % 60.47/8.92 | (196) all_179_0 = all_177_0 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (184), (195) imply: % 60.47/8.92 | (197) all_179_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | SIMP: (197) implies: % 60.47/8.92 | (198) all_179_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (196), (198) imply: % 60.47/8.92 | (199) all_177_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | SIMP: (199) implies: % 60.47/8.92 | (200) all_177_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (183), (200) imply: % 60.47/8.92 | (201) all_155_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | SIMP: (201) implies: % 60.47/8.92 | (202) all_155_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (179), (191) imply: % 60.47/8.92 | (203) all_167_0 = n2 % 60.47/8.92 | % 60.47/8.92 | SIMP: (203) implies: % 60.47/8.92 | (204) all_167_0 = n2 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (178), (204) imply: % 60.47/8.92 | (205) all_133_0 = n2 % 60.47/8.92 | % 60.47/8.92 | SIMP: (205) implies: % 60.47/8.92 | (206) all_133_0 = n2 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (182), (202) imply: % 60.47/8.92 | (207) all_145_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | SIMP: (207) implies: % 60.47/8.92 | (208) all_145_0 = all_96_25 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (193), (208) imply: % 60.47/8.92 | (209) all_96_25 = n5 % 60.47/8.92 | % 60.47/8.92 | COMBINE_EQS: (177), (206) imply: % 60.47/8.92 | (210) all_96_24 = n2 % 60.47/8.92 | % 60.47/8.92 | SIMP: (210) implies: % 60.47/8.92 | (211) all_96_24 = n2 % 60.47/8.92 | % 60.47/8.92 | BETA: splitting (69) gives: % 60.47/8.92 | % 60.47/8.92 | Case 1: % 60.47/8.92 | | % 60.47/8.92 | | (212) all_96_2 = 0 & all_96_3 = 0 & all_96_4 = 0 & all_96_5 = 0 & ~ % 60.47/8.92 | | (all_96_0 = all_96_1) & a_select3(q_ds1_filter, all_96_6, all_96_7) % 60.47/8.92 | | = all_96_0 & a_select3(q_ds1_filter, all_96_7, all_96_6) = all_96_1 % 60.47/8.92 | | & leq(all_96_6, all_96_25) = 0 & leq(all_96_7, all_96_25) = 0 & % 60.47/8.92 | | leq(n0, all_96_6) = 0 & leq(n0, all_96_7) = 0 & $i(all_96_0) & % 60.47/8.92 | | $i(all_96_1) % 60.47/8.92 | | % 60.47/8.92 | | ALPHA: (212) implies: % 60.47/8.92 | | (213) ~ (all_96_0 = all_96_1) % 60.47/8.92 | | (214) leq(n0, all_96_7) = 0 % 60.47/8.92 | | (215) leq(n0, all_96_6) = 0 % 60.47/8.92 | | (216) leq(all_96_7, all_96_25) = 0 % 60.47/8.92 | | (217) leq(all_96_6, all_96_25) = 0 % 60.47/8.92 | | (218) a_select3(q_ds1_filter, all_96_7, all_96_6) = all_96_1 % 60.47/8.92 | | (219) a_select3(q_ds1_filter, all_96_6, all_96_7) = all_96_0 % 60.47/8.92 | | % 60.47/8.92 | | REDUCE: (209), (217) imply: % 60.47/8.92 | | (220) leq(all_96_6, n5) = 0 % 60.47/8.92 | | % 60.47/8.92 | | REDUCE: (209), (216) imply: % 60.47/8.92 | | (221) leq(all_96_7, n5) = 0 % 60.47/8.92 | | % 60.47/8.92 | | GROUND_INST: instantiating (71) with all_96_6, all_96_7, all_96_1, % 60.47/8.92 | | simplifying with (65), (66), (218) gives: % 60.47/8.93 | | (222) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 60.47/8.93 | | $i] : (a_select3(q_ds1_filter, all_96_6, all_96_7) = v4 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = v2 & leq(all_96_7, all_96_25) = v3 & % 60.47/8.93 | | leq(n0, all_96_6) = v0 & leq(n0, all_96_7) = v1 & $i(v4) & ( ~ % 60.47/8.93 | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.93 | | all_96_1)) % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (70) with all_96_7, all_96_6, all_96_1, % 60.47/8.93 | | simplifying with (65), (66), (218) gives: % 60.47/8.93 | | (223) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 60.47/8.93 | | $i] : (a_select3(q_ds1_filter, all_96_6, all_96_7) = v4 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = v3 & leq(all_96_7, all_96_25) = v2 & % 60.47/8.93 | | leq(n0, all_96_6) = v1 & leq(n0, all_96_7) = v0 & $i(v4) & ( ~ % 60.47/8.93 | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.93 | | all_96_1)) % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (71) with all_96_7, all_96_6, all_96_0, % 60.47/8.93 | | simplifying with (65), (66), (219) gives: % 60.47/8.93 | | (224) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 60.47/8.93 | | $i] : (a_select3(q_ds1_filter, all_96_7, all_96_6) = v4 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = v3 & leq(all_96_7, all_96_25) = v2 & % 60.47/8.93 | | leq(n0, all_96_6) = v1 & leq(n0, all_96_7) = v0 & $i(v4) & ( ~ % 60.47/8.93 | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.93 | | all_96_0)) % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (70) with all_96_6, all_96_7, all_96_0, % 60.47/8.93 | | simplifying with (65), (66), (219) gives: % 60.47/8.93 | | (225) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? [v4: % 60.47/8.93 | | $i] : (a_select3(q_ds1_filter, all_96_7, all_96_6) = v4 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = v2 & leq(all_96_7, all_96_25) = v3 & % 60.47/8.93 | | leq(n0, all_96_6) = v0 & leq(n0, all_96_7) = v1 & $i(v4) & ( ~ % 60.47/8.93 | | (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.93 | | all_96_0)) % 60.47/8.93 | | % 60.47/8.93 | | DELTA: instantiating (225) with fresh symbols all_591_0, all_591_1, % 60.47/8.93 | | all_591_2, all_591_3, all_591_4 gives: % 60.47/8.93 | | (226) a_select3(q_ds1_filter, all_96_7, all_96_6) = all_591_0 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = all_591_2 & leq(all_96_7, all_96_25) = % 60.47/8.93 | | all_591_1 & leq(n0, all_96_6) = all_591_4 & leq(n0, all_96_7) = % 60.47/8.93 | | all_591_3 & $i(all_591_0) & ( ~ (all_591_1 = 0) | ~ (all_591_2 = % 60.47/8.93 | | 0) | ~ (all_591_3 = 0) | ~ (all_591_4 = 0) | all_591_0 = % 60.47/8.93 | | all_96_0) % 60.47/8.93 | | % 60.47/8.93 | | ALPHA: (226) implies: % 60.47/8.93 | | (227) leq(n0, all_96_6) = all_591_4 % 60.47/8.93 | | (228) leq(all_96_7, all_96_25) = all_591_1 % 60.47/8.93 | | % 60.47/8.93 | | DELTA: instantiating (224) with fresh symbols all_593_0, all_593_1, % 60.47/8.93 | | all_593_2, all_593_3, all_593_4 gives: % 60.47/8.93 | | (229) a_select3(q_ds1_filter, all_96_7, all_96_6) = all_593_0 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = all_593_1 & leq(all_96_7, all_96_25) = % 60.47/8.93 | | all_593_2 & leq(n0, all_96_6) = all_593_3 & leq(n0, all_96_7) = % 60.47/8.93 | | all_593_4 & $i(all_593_0) & ( ~ (all_593_1 = 0) | ~ (all_593_2 = % 60.47/8.93 | | 0) | ~ (all_593_3 = 0) | ~ (all_593_4 = 0) | all_593_0 = % 60.47/8.93 | | all_96_0) % 60.47/8.93 | | % 60.47/8.93 | | ALPHA: (229) implies: % 60.47/8.93 | | (230) leq(n0, all_96_6) = all_593_3 % 60.47/8.93 | | (231) leq(all_96_7, all_96_25) = all_593_2 % 60.47/8.93 | | % 60.47/8.93 | | DELTA: instantiating (223) with fresh symbols all_595_0, all_595_1, % 60.47/8.93 | | all_595_2, all_595_3, all_595_4 gives: % 60.47/8.93 | | (232) a_select3(q_ds1_filter, all_96_6, all_96_7) = all_595_0 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = all_595_1 & leq(all_96_7, all_96_25) = % 60.47/8.93 | | all_595_2 & leq(n0, all_96_6) = all_595_3 & leq(n0, all_96_7) = % 60.47/8.93 | | all_595_4 & $i(all_595_0) & ( ~ (all_595_1 = 0) | ~ (all_595_2 = % 60.47/8.93 | | 0) | ~ (all_595_3 = 0) | ~ (all_595_4 = 0) | all_595_0 = % 60.47/8.93 | | all_96_1) % 60.47/8.93 | | % 60.47/8.93 | | ALPHA: (232) implies: % 60.47/8.93 | | (233) leq(n0, all_96_7) = all_595_4 % 60.47/8.93 | | (234) leq(n0, all_96_6) = all_595_3 % 60.47/8.93 | | (235) leq(all_96_7, all_96_25) = all_595_2 % 60.47/8.93 | | (236) leq(all_96_6, all_96_25) = all_595_1 % 60.47/8.93 | | (237) a_select3(q_ds1_filter, all_96_6, all_96_7) = all_595_0 % 60.47/8.93 | | % 60.47/8.93 | | DELTA: instantiating (222) with fresh symbols all_597_0, all_597_1, % 60.47/8.93 | | all_597_2, all_597_3, all_597_4 gives: % 60.47/8.93 | | (238) a_select3(q_ds1_filter, all_96_6, all_96_7) = all_597_0 & % 60.47/8.93 | | leq(all_96_6, all_96_25) = all_597_2 & leq(all_96_7, all_96_25) = % 60.47/8.93 | | all_597_1 & leq(n0, all_96_6) = all_597_4 & leq(n0, all_96_7) = % 60.47/8.93 | | all_597_3 & $i(all_597_0) & ( ~ (all_597_1 = 0) | ~ (all_597_2 = % 60.47/8.93 | | 0) | ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | all_597_0 = % 60.47/8.93 | | all_96_1) % 60.47/8.93 | | % 60.47/8.93 | | ALPHA: (238) implies: % 60.47/8.93 | | (239) leq(n0, all_96_7) = all_597_3 % 60.47/8.93 | | (240) leq(n0, all_96_6) = all_597_4 % 60.47/8.93 | | (241) leq(all_96_7, all_96_25) = all_597_1 % 60.47/8.93 | | (242) leq(all_96_6, all_96_25) = all_597_2 % 60.47/8.93 | | (243) a_select3(q_ds1_filter, all_96_6, all_96_7) = all_597_0 % 60.47/8.93 | | (244) ~ (all_597_1 = 0) | ~ (all_597_2 = 0) | ~ (all_597_3 = 0) | ~ % 60.47/8.93 | | (all_597_4 = 0) | all_597_0 = all_96_1 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (242) imply: % 60.47/8.93 | | (245) leq(all_96_6, n5) = all_597_2 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (236) imply: % 60.47/8.93 | | (246) leq(all_96_6, n5) = all_595_1 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (241) imply: % 60.47/8.93 | | (247) leq(all_96_7, n5) = all_597_1 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (235) imply: % 60.47/8.93 | | (248) leq(all_96_7, n5) = all_595_2 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (231) imply: % 60.47/8.93 | | (249) leq(all_96_7, n5) = all_593_2 % 60.47/8.93 | | % 60.47/8.93 | | REDUCE: (209), (228) imply: % 60.47/8.93 | | (250) leq(all_96_7, n5) = all_591_1 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with 0, all_597_3, all_96_7, n0, simplifying % 60.47/8.93 | | with (214), (239) gives: % 60.47/8.93 | | (251) all_597_3 = 0 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with all_595_4, all_597_3, all_96_7, n0, % 60.47/8.93 | | simplifying with (233), (239) gives: % 60.47/8.93 | | (252) all_597_3 = all_595_4 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with 0, all_593_3, all_96_6, n0, simplifying % 60.47/8.93 | | with (215), (230) gives: % 60.47/8.93 | | (253) all_593_3 = 0 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with all_595_3, all_597_4, all_96_6, n0, % 60.47/8.93 | | simplifying with (234), (240) gives: % 60.47/8.93 | | (254) all_597_4 = all_595_3 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with all_593_3, all_597_4, all_96_6, n0, % 60.47/8.93 | | simplifying with (230), (240) gives: % 60.47/8.93 | | (255) all_597_4 = all_593_3 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with all_591_4, all_597_4, all_96_6, n0, % 60.47/8.93 | | simplifying with (227), (240) gives: % 60.47/8.93 | | (256) all_597_4 = all_591_4 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with 0, all_593_2, n5, all_96_7, simplifying % 60.47/8.93 | | with (221), (249) gives: % 60.47/8.93 | | (257) all_593_2 = 0 % 60.47/8.93 | | % 60.47/8.93 | | GROUND_INST: instantiating (28) with all_595_2, all_597_1, n5, all_96_7, % 60.47/8.93 | | simplifying with (247), (248) gives: % 60.47/8.93 | | (258) all_597_1 = all_595_2 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (28) with all_593_2, all_597_1, n5, all_96_7, % 60.47/8.94 | | simplifying with (247), (249) gives: % 60.47/8.94 | | (259) all_597_1 = all_593_2 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (28) with all_591_1, all_597_1, n5, all_96_7, % 60.47/8.94 | | simplifying with (247), (250) gives: % 60.47/8.94 | | (260) all_597_1 = all_591_1 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (28) with 0, all_597_2, n5, all_96_6, simplifying % 60.47/8.94 | | with (220), (245) gives: % 60.47/8.94 | | (261) all_597_2 = 0 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (28) with all_595_1, all_597_2, n5, all_96_6, % 60.47/8.94 | | simplifying with (245), (246) gives: % 60.47/8.94 | | (262) all_597_2 = all_595_1 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (29) with all_96_0, all_597_0, all_96_7, % 60.47/8.94 | | all_96_6, q_ds1_filter, simplifying with (219), (243) gives: % 60.47/8.94 | | (263) all_597_0 = all_96_0 % 60.47/8.94 | | % 60.47/8.94 | | GROUND_INST: instantiating (29) with all_595_0, all_597_0, all_96_7, % 60.47/8.94 | | all_96_6, q_ds1_filter, simplifying with (237), (243) gives: % 60.47/8.94 | | (264) all_597_0 = all_595_0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (263), (264) imply: % 60.47/8.94 | | (265) all_595_0 = all_96_0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (258), (260) imply: % 60.47/8.94 | | (266) all_595_2 = all_591_1 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (258), (259) imply: % 60.47/8.94 | | (267) all_595_2 = all_593_2 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (261), (262) imply: % 60.47/8.94 | | (268) all_595_1 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (251), (252) imply: % 60.47/8.94 | | (269) all_595_4 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (254), (255) imply: % 60.47/8.94 | | (270) all_595_3 = all_593_3 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (254), (256) imply: % 60.47/8.94 | | (271) all_595_3 = all_591_4 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (266), (267) imply: % 60.47/8.94 | | (272) all_593_2 = all_591_1 % 60.47/8.94 | | % 60.47/8.94 | | SIMP: (272) implies: % 60.47/8.94 | | (273) all_593_2 = all_591_1 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (270), (271) imply: % 60.47/8.94 | | (274) all_593_3 = all_591_4 % 60.47/8.94 | | % 60.47/8.94 | | SIMP: (274) implies: % 60.47/8.94 | | (275) all_593_3 = all_591_4 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (257), (273) imply: % 60.47/8.94 | | (276) all_591_1 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (253), (275) imply: % 60.47/8.94 | | (277) all_591_4 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (271), (277) imply: % 60.47/8.94 | | (278) all_595_3 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (266), (276) imply: % 60.47/8.94 | | (279) all_595_2 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (254), (278) imply: % 60.47/8.94 | | (280) all_597_4 = 0 % 60.47/8.94 | | % 60.47/8.94 | | COMBINE_EQS: (258), (279) imply: % 60.47/8.94 | | (281) all_597_1 = 0 % 60.47/8.94 | | % 60.47/8.94 | | BETA: splitting (244) gives: % 60.47/8.94 | | % 60.47/8.94 | | Case 1: % 60.47/8.94 | | | % 60.47/8.94 | | | (282) ~ (all_597_1 = 0) % 60.47/8.94 | | | % 60.47/8.94 | | | REDUCE: (281), (282) imply: % 60.47/8.94 | | | (283) $false % 60.47/8.94 | | | % 60.47/8.94 | | | CLOSE: (283) is inconsistent. % 60.47/8.94 | | | % 60.47/8.94 | | Case 2: % 60.47/8.94 | | | % 60.47/8.94 | | | (284) ~ (all_597_2 = 0) | ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | % 60.47/8.94 | | | all_597_0 = all_96_1 % 60.47/8.94 | | | % 60.47/8.94 | | | BETA: splitting (284) gives: % 60.47/8.94 | | | % 60.47/8.94 | | | Case 1: % 60.47/8.94 | | | | % 60.47/8.94 | | | | (285) ~ (all_597_2 = 0) % 60.47/8.94 | | | | % 60.47/8.94 | | | | REDUCE: (261), (285) imply: % 60.47/8.94 | | | | (286) $false % 60.47/8.94 | | | | % 60.47/8.94 | | | | CLOSE: (286) is inconsistent. % 60.47/8.94 | | | | % 60.47/8.94 | | | Case 2: % 60.47/8.94 | | | | % 60.47/8.94 | | | | (287) ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | all_597_0 = all_96_1 % 60.47/8.94 | | | | % 60.47/8.94 | | | | BETA: splitting (287) gives: % 60.47/8.94 | | | | % 60.47/8.94 | | | | Case 1: % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | (288) ~ (all_597_3 = 0) % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | REDUCE: (251), (288) imply: % 60.47/8.94 | | | | | (289) $false % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | CLOSE: (289) is inconsistent. % 60.47/8.94 | | | | | % 60.47/8.94 | | | | Case 2: % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | (290) ~ (all_597_4 = 0) | all_597_0 = all_96_1 % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | BETA: splitting (290) gives: % 60.47/8.94 | | | | | % 60.47/8.94 | | | | | Case 1: % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | (291) ~ (all_597_4 = 0) % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | REDUCE: (280), (291) imply: % 60.47/8.94 | | | | | | (292) $false % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | CLOSE: (292) is inconsistent. % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | Case 2: % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | (293) all_597_0 = all_96_1 % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | COMBINE_EQS: (263), (293) imply: % 60.47/8.94 | | | | | | (294) all_96_0 = all_96_1 % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | REDUCE: (213), (294) imply: % 60.47/8.94 | | | | | | (295) $false % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | | CLOSE: (295) is inconsistent. % 60.47/8.94 | | | | | | % 60.47/8.94 | | | | | End of split % 60.47/8.94 | | | | | % 60.47/8.94 | | | | End of split % 60.47/8.94 | | | | % 60.47/8.94 | | | End of split % 60.47/8.94 | | | % 60.47/8.94 | | End of split % 60.47/8.94 | | % 60.47/8.94 | Case 2: % 60.47/8.94 | | % 60.47/8.94 | | (296) (all_96_10 = 0 & all_96_11 = 0 & all_96_12 = 0 & all_96_13 = 0 & ~ % 60.47/8.94 | | (all_96_8 = all_96_9) & a_select3(r_ds1_filter, all_96_14, % 60.47/8.94 | | all_96_15) = all_96_8 & a_select3(r_ds1_filter, all_96_15, % 60.47/8.94 | | all_96_14) = all_96_9 & leq(all_96_14, all_96_24) = 0 & % 60.47/8.94 | | leq(all_96_15, all_96_24) = 0 & leq(n0, all_96_14) = 0 & leq(n0, % 60.47/8.94 | | all_96_15) = 0 & $i(all_96_8) & $i(all_96_9)) | (all_96_18 = 0 % 60.47/8.94 | | & all_96_19 = 0 & all_96_20 = 0 & all_96_21 = 0 & ~ (all_96_16 = % 60.47/8.94 | | all_96_17) & a_select3(pminus_ds1_filter, all_96_22, all_96_23) % 60.47/8.94 | | = all_96_16 & a_select3(pminus_ds1_filter, all_96_23, all_96_22) % 60.47/8.94 | | = all_96_17 & leq(all_96_22, all_96_25) = 0 & leq(all_96_23, % 60.47/8.94 | | all_96_25) = 0 & leq(n0, all_96_22) = 0 & leq(n0, all_96_23) = % 60.47/8.94 | | 0 & $i(all_96_16) & $i(all_96_17)) % 60.47/8.94 | | % 60.47/8.94 | | BETA: splitting (296) gives: % 60.47/8.94 | | % 60.47/8.94 | | Case 1: % 60.47/8.94 | | | % 60.47/8.94 | | | (297) all_96_10 = 0 & all_96_11 = 0 & all_96_12 = 0 & all_96_13 = 0 & % 60.47/8.94 | | | ~ (all_96_8 = all_96_9) & a_select3(r_ds1_filter, all_96_14, % 60.47/8.94 | | | all_96_15) = all_96_8 & a_select3(r_ds1_filter, all_96_15, % 60.47/8.94 | | | all_96_14) = all_96_9 & leq(all_96_14, all_96_24) = 0 & % 60.47/8.94 | | | leq(all_96_15, all_96_24) = 0 & leq(n0, all_96_14) = 0 & leq(n0, % 60.47/8.94 | | | all_96_15) = 0 & $i(all_96_8) & $i(all_96_9) % 60.47/8.94 | | | % 60.47/8.94 | | | ALPHA: (297) implies: % 60.47/8.94 | | | (298) ~ (all_96_8 = all_96_9) % 60.47/8.94 | | | (299) leq(n0, all_96_15) = 0 % 60.47/8.94 | | | (300) leq(n0, all_96_14) = 0 % 60.47/8.94 | | | (301) leq(all_96_15, all_96_24) = 0 % 60.47/8.94 | | | (302) leq(all_96_14, all_96_24) = 0 % 60.47/8.94 | | | (303) a_select3(r_ds1_filter, all_96_15, all_96_14) = all_96_9 % 60.47/8.94 | | | (304) a_select3(r_ds1_filter, all_96_14, all_96_15) = all_96_8 % 60.47/8.94 | | | % 60.47/8.94 | | | REDUCE: (211), (302) imply: % 60.47/8.94 | | | (305) leq(all_96_14, n2) = 0 % 60.47/8.94 | | | % 60.47/8.94 | | | REDUCE: (211), (301) imply: % 60.47/8.94 | | | (306) leq(all_96_15, n2) = 0 % 60.47/8.94 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (73) with all_96_14, all_96_15, all_96_9, % 60.47/8.95 | | | simplifying with (63), (64), (303) gives: % 60.47/8.95 | | | (307) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.47/8.95 | | | [v4: $i] : (a_select3(r_ds1_filter, all_96_14, all_96_15) = v4 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = v2 & leq(all_96_15, all_96_24) = v3 % 60.47/8.95 | | | & leq(n0, all_96_14) = v0 & leq(n0, all_96_15) = v1 & $i(v4) & % 60.47/8.95 | | | ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.95 | | | all_96_9)) % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (72) with all_96_15, all_96_14, all_96_9, % 60.47/8.95 | | | simplifying with (63), (64), (303) gives: % 60.47/8.95 | | | (308) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.47/8.95 | | | [v4: $i] : (a_select3(r_ds1_filter, all_96_14, all_96_15) = v4 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = v3 & leq(all_96_15, all_96_24) = v2 % 60.47/8.95 | | | & leq(n0, all_96_14) = v1 & leq(n0, all_96_15) = v0 & $i(v4) & % 60.47/8.95 | | | ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.95 | | | all_96_9)) % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (73) with all_96_15, all_96_14, all_96_8, % 60.47/8.95 | | | simplifying with (63), (64), (304) gives: % 60.47/8.95 | | | (309) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.47/8.95 | | | [v4: $i] : (a_select3(r_ds1_filter, all_96_15, all_96_14) = v4 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = v3 & leq(all_96_15, all_96_24) = v2 % 60.47/8.95 | | | & leq(n0, all_96_14) = v1 & leq(n0, all_96_15) = v0 & $i(v4) & % 60.47/8.95 | | | ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.95 | | | all_96_8)) % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (72) with all_96_14, all_96_15, all_96_8, % 60.47/8.95 | | | simplifying with (63), (64), (304) gives: % 60.47/8.95 | | | (310) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.47/8.95 | | | [v4: $i] : (a_select3(r_ds1_filter, all_96_15, all_96_14) = v4 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = v2 & leq(all_96_15, all_96_24) = v3 % 60.47/8.95 | | | & leq(n0, all_96_14) = v0 & leq(n0, all_96_15) = v1 & $i(v4) & % 60.47/8.95 | | | ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) | v4 = % 60.47/8.95 | | | all_96_8)) % 60.47/8.95 | | | % 60.47/8.95 | | | DELTA: instantiating (310) with fresh symbols all_591_0, all_591_1, % 60.47/8.95 | | | all_591_2, all_591_3, all_591_4 gives: % 60.47/8.95 | | | (311) a_select3(r_ds1_filter, all_96_15, all_96_14) = all_591_0 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = all_591_2 & leq(all_96_15, all_96_24) % 60.47/8.95 | | | = all_591_1 & leq(n0, all_96_14) = all_591_4 & leq(n0, all_96_15) % 60.47/8.95 | | | = all_591_3 & $i(all_591_0) & ( ~ (all_591_1 = 0) | ~ (all_591_2 % 60.47/8.95 | | | = 0) | ~ (all_591_3 = 0) | ~ (all_591_4 = 0) | all_591_0 = % 60.47/8.95 | | | all_96_8) % 60.47/8.95 | | | % 60.47/8.95 | | | ALPHA: (311) implies: % 60.47/8.95 | | | (312) leq(n0, all_96_15) = all_591_3 % 60.47/8.95 | | | (313) leq(n0, all_96_14) = all_591_4 % 60.47/8.95 | | | (314) leq(all_96_15, all_96_24) = all_591_1 % 60.47/8.95 | | | (315) leq(all_96_14, all_96_24) = all_591_2 % 60.47/8.95 | | | (316) a_select3(r_ds1_filter, all_96_15, all_96_14) = all_591_0 % 60.47/8.95 | | | (317) ~ (all_591_1 = 0) | ~ (all_591_2 = 0) | ~ (all_591_3 = 0) | ~ % 60.47/8.95 | | | (all_591_4 = 0) | all_591_0 = all_96_8 % 60.47/8.95 | | | % 60.47/8.95 | | | DELTA: instantiating (309) with fresh symbols all_593_0, all_593_1, % 60.47/8.95 | | | all_593_2, all_593_3, all_593_4 gives: % 60.47/8.95 | | | (318) a_select3(r_ds1_filter, all_96_15, all_96_14) = all_593_0 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = all_593_1 & leq(all_96_15, all_96_24) % 60.47/8.95 | | | = all_593_2 & leq(n0, all_96_14) = all_593_3 & leq(n0, all_96_15) % 60.47/8.95 | | | = all_593_4 & $i(all_593_0) & ( ~ (all_593_1 = 0) | ~ (all_593_2 % 60.47/8.95 | | | = 0) | ~ (all_593_3 = 0) | ~ (all_593_4 = 0) | all_593_0 = % 60.47/8.95 | | | all_96_8) % 60.47/8.95 | | | % 60.47/8.95 | | | ALPHA: (318) implies: % 60.47/8.95 | | | (319) leq(n0, all_96_15) = all_593_4 % 60.47/8.95 | | | (320) leq(n0, all_96_14) = all_593_3 % 60.47/8.95 | | | (321) leq(all_96_15, all_96_24) = all_593_2 % 60.47/8.95 | | | (322) leq(all_96_14, all_96_24) = all_593_1 % 60.47/8.95 | | | (323) a_select3(r_ds1_filter, all_96_15, all_96_14) = all_593_0 % 60.47/8.95 | | | % 60.47/8.95 | | | DELTA: instantiating (308) with fresh symbols all_595_0, all_595_1, % 60.47/8.95 | | | all_595_2, all_595_3, all_595_4 gives: % 60.47/8.95 | | | (324) a_select3(r_ds1_filter, all_96_14, all_96_15) = all_595_0 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = all_595_1 & leq(all_96_15, all_96_24) % 60.47/8.95 | | | = all_595_2 & leq(n0, all_96_14) = all_595_3 & leq(n0, all_96_15) % 60.47/8.95 | | | = all_595_4 & $i(all_595_0) & ( ~ (all_595_1 = 0) | ~ (all_595_2 % 60.47/8.95 | | | = 0) | ~ (all_595_3 = 0) | ~ (all_595_4 = 0) | all_595_0 = % 60.47/8.95 | | | all_96_9) % 60.47/8.95 | | | % 60.47/8.95 | | | ALPHA: (324) implies: % 60.47/8.95 | | | (325) leq(n0, all_96_15) = all_595_4 % 60.47/8.95 | | | (326) leq(n0, all_96_14) = all_595_3 % 60.47/8.95 | | | (327) leq(all_96_15, all_96_24) = all_595_2 % 60.47/8.95 | | | (328) leq(all_96_14, all_96_24) = all_595_1 % 60.47/8.95 | | | % 60.47/8.95 | | | DELTA: instantiating (307) with fresh symbols all_597_0, all_597_1, % 60.47/8.95 | | | all_597_2, all_597_3, all_597_4 gives: % 60.47/8.95 | | | (329) a_select3(r_ds1_filter, all_96_14, all_96_15) = all_597_0 & % 60.47/8.95 | | | leq(all_96_14, all_96_24) = all_597_2 & leq(all_96_15, all_96_24) % 60.47/8.95 | | | = all_597_1 & leq(n0, all_96_14) = all_597_4 & leq(n0, all_96_15) % 60.47/8.95 | | | = all_597_3 & $i(all_597_0) & ( ~ (all_597_1 = 0) | ~ (all_597_2 % 60.47/8.95 | | | = 0) | ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | all_597_0 = % 60.47/8.95 | | | all_96_9) % 60.47/8.95 | | | % 60.47/8.95 | | | ALPHA: (329) implies: % 60.47/8.95 | | | (330) leq(n0, all_96_15) = all_597_3 % 60.47/8.95 | | | (331) leq(n0, all_96_14) = all_597_4 % 60.47/8.95 | | | (332) leq(all_96_15, all_96_24) = all_597_1 % 60.47/8.95 | | | (333) leq(all_96_14, all_96_24) = all_597_2 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (333) imply: % 60.47/8.95 | | | (334) leq(all_96_14, n2) = all_597_2 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (328) imply: % 60.47/8.95 | | | (335) leq(all_96_14, n2) = all_595_1 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (322) imply: % 60.47/8.95 | | | (336) leq(all_96_14, n2) = all_593_1 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (315) imply: % 60.47/8.95 | | | (337) leq(all_96_14, n2) = all_591_2 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (332) imply: % 60.47/8.95 | | | (338) leq(all_96_15, n2) = all_597_1 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (327) imply: % 60.47/8.95 | | | (339) leq(all_96_15, n2) = all_595_2 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (321) imply: % 60.47/8.95 | | | (340) leq(all_96_15, n2) = all_593_2 % 60.47/8.95 | | | % 60.47/8.95 | | | REDUCE: (211), (314) imply: % 60.47/8.95 | | | (341) leq(all_96_15, n2) = all_591_1 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_591_3, all_593_4, all_96_15, n0, % 60.47/8.95 | | | simplifying with (312), (319) gives: % 60.47/8.95 | | | (342) all_593_4 = all_591_3 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with 0, all_597_3, all_96_15, n0, % 60.47/8.95 | | | simplifying with (299), (330) gives: % 60.47/8.95 | | | (343) all_597_3 = 0 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_595_4, all_597_3, all_96_15, n0, % 60.47/8.95 | | | simplifying with (325), (330) gives: % 60.47/8.95 | | | (344) all_597_3 = all_595_4 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_593_4, all_597_3, all_96_15, n0, % 60.47/8.95 | | | simplifying with (319), (330) gives: % 60.47/8.95 | | | (345) all_597_3 = all_593_4 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with 0, all_593_3, all_96_14, n0, % 60.47/8.95 | | | simplifying with (300), (320) gives: % 60.47/8.95 | | | (346) all_593_3 = 0 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_595_3, all_597_4, all_96_14, n0, % 60.47/8.95 | | | simplifying with (326), (331) gives: % 60.47/8.95 | | | (347) all_597_4 = all_595_3 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_593_3, all_597_4, all_96_14, n0, % 60.47/8.95 | | | simplifying with (320), (331) gives: % 60.47/8.95 | | | (348) all_597_4 = all_593_3 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with all_591_4, all_597_4, all_96_14, n0, % 60.47/8.95 | | | simplifying with (313), (331) gives: % 60.47/8.95 | | | (349) all_597_4 = all_591_4 % 60.47/8.95 | | | % 60.47/8.95 | | | GROUND_INST: instantiating (28) with 0, all_593_2, n2, all_96_15, % 60.47/8.95 | | | simplifying with (306), (340) gives: % 60.47/8.95 | | | (350) all_593_2 = 0 % 60.47/8.95 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_595_2, all_597_1, n2, all_96_15, % 60.47/8.96 | | | simplifying with (338), (339) gives: % 60.47/8.96 | | | (351) all_597_1 = all_595_2 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_593_2, all_597_1, n2, all_96_15, % 60.47/8.96 | | | simplifying with (338), (340) gives: % 60.47/8.96 | | | (352) all_597_1 = all_593_2 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_591_1, all_597_1, n2, all_96_15, % 60.47/8.96 | | | simplifying with (338), (341) gives: % 60.47/8.96 | | | (353) all_597_1 = all_591_1 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_591_2, all_593_1, n2, all_96_14, % 60.47/8.96 | | | simplifying with (336), (337) gives: % 60.47/8.96 | | | (354) all_593_1 = all_591_2 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with 0, all_597_2, n2, all_96_14, % 60.47/8.96 | | | simplifying with (305), (334) gives: % 60.47/8.96 | | | (355) all_597_2 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_595_1, all_597_2, n2, all_96_14, % 60.47/8.96 | | | simplifying with (334), (335) gives: % 60.47/8.96 | | | (356) all_597_2 = all_595_1 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (28) with all_593_1, all_597_2, n2, all_96_14, % 60.47/8.96 | | | simplifying with (334), (336) gives: % 60.47/8.96 | | | (357) all_597_2 = all_593_1 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (29) with all_96_9, all_593_0, all_96_14, % 60.47/8.96 | | | all_96_15, r_ds1_filter, simplifying with (303), (323) gives: % 60.47/8.96 | | | (358) all_593_0 = all_96_9 % 60.47/8.96 | | | % 60.47/8.96 | | | GROUND_INST: instantiating (29) with all_591_0, all_593_0, all_96_14, % 60.47/8.96 | | | all_96_15, r_ds1_filter, simplifying with (316), (323) gives: % 60.47/8.96 | | | (359) all_593_0 = all_591_0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (351), (353) imply: % 60.47/8.96 | | | (360) all_595_2 = all_591_1 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (351), (352) imply: % 60.47/8.96 | | | (361) all_595_2 = all_593_2 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (355), (356) imply: % 60.47/8.96 | | | (362) all_595_1 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (356), (357) imply: % 60.47/8.96 | | | (363) all_595_1 = all_593_1 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (343), (344) imply: % 60.47/8.96 | | | (364) all_595_4 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (344), (345) imply: % 60.47/8.96 | | | (365) all_595_4 = all_593_4 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (347), (348) imply: % 60.47/8.96 | | | (366) all_595_3 = all_593_3 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (347), (349) imply: % 60.47/8.96 | | | (367) all_595_3 = all_591_4 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (362), (363) imply: % 60.47/8.96 | | | (368) all_593_1 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (368) implies: % 60.47/8.96 | | | (369) all_593_1 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (360), (361) imply: % 60.47/8.96 | | | (370) all_593_2 = all_591_1 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (370) implies: % 60.47/8.96 | | | (371) all_593_2 = all_591_1 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (366), (367) imply: % 60.47/8.96 | | | (372) all_593_3 = all_591_4 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (372) implies: % 60.47/8.96 | | | (373) all_593_3 = all_591_4 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (364), (365) imply: % 60.47/8.96 | | | (374) all_593_4 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (374) implies: % 60.47/8.96 | | | (375) all_593_4 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (358), (359) imply: % 60.47/8.96 | | | (376) all_591_0 = all_96_9 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (354), (369) imply: % 60.47/8.96 | | | (377) all_591_2 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (377) implies: % 60.47/8.96 | | | (378) all_591_2 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (350), (371) imply: % 60.47/8.96 | | | (379) all_591_1 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (346), (373) imply: % 60.47/8.96 | | | (380) all_591_4 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | COMBINE_EQS: (342), (375) imply: % 60.47/8.96 | | | (381) all_591_3 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | SIMP: (381) implies: % 60.47/8.96 | | | (382) all_591_3 = 0 % 60.47/8.96 | | | % 60.47/8.96 | | | BETA: splitting (317) gives: % 60.47/8.96 | | | % 60.47/8.96 | | | Case 1: % 60.47/8.96 | | | | % 60.47/8.96 | | | | (383) ~ (all_591_1 = 0) % 60.47/8.96 | | | | % 60.47/8.96 | | | | REDUCE: (379), (383) imply: % 60.47/8.96 | | | | (384) $false % 60.47/8.96 | | | | % 60.47/8.96 | | | | CLOSE: (384) is inconsistent. % 60.47/8.96 | | | | % 60.47/8.96 | | | Case 2: % 60.47/8.96 | | | | % 60.47/8.96 | | | | (385) ~ (all_591_2 = 0) | ~ (all_591_3 = 0) | ~ (all_591_4 = 0) | % 60.47/8.96 | | | | all_591_0 = all_96_8 % 60.47/8.96 | | | | % 60.47/8.96 | | | | BETA: splitting (385) gives: % 60.47/8.96 | | | | % 60.47/8.96 | | | | Case 1: % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | (386) ~ (all_591_2 = 0) % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | REDUCE: (378), (386) imply: % 60.47/8.96 | | | | | (387) $false % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | CLOSE: (387) is inconsistent. % 60.47/8.96 | | | | | % 60.47/8.96 | | | | Case 2: % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | (388) ~ (all_591_3 = 0) | ~ (all_591_4 = 0) | all_591_0 = % 60.47/8.96 | | | | | all_96_8 % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | BETA: splitting (388) gives: % 60.47/8.96 | | | | | % 60.47/8.96 | | | | | Case 1: % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | (389) ~ (all_591_3 = 0) % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | REDUCE: (382), (389) imply: % 60.47/8.96 | | | | | | (390) $false % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | CLOSE: (390) is inconsistent. % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | Case 2: % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | (391) ~ (all_591_4 = 0) | all_591_0 = all_96_8 % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | BETA: splitting (391) gives: % 60.47/8.96 | | | | | | % 60.47/8.96 | | | | | | Case 1: % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | (392) ~ (all_591_4 = 0) % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | REDUCE: (380), (392) imply: % 60.47/8.96 | | | | | | | (393) $false % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | CLOSE: (393) is inconsistent. % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | Case 2: % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | (394) all_591_0 = all_96_8 % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | COMBINE_EQS: (376), (394) imply: % 60.47/8.96 | | | | | | | (395) all_96_8 = all_96_9 % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | SIMP: (395) implies: % 60.47/8.96 | | | | | | | (396) all_96_8 = all_96_9 % 60.47/8.96 | | | | | | | % 60.47/8.96 | | | | | | | REDUCE: (298), (396) imply: % 60.76/8.96 | | | | | | | (397) $false % 60.76/8.96 | | | | | | | % 60.76/8.96 | | | | | | | CLOSE: (397) is inconsistent. % 60.76/8.96 | | | | | | | % 60.76/8.96 | | | | | | End of split % 60.76/8.96 | | | | | | % 60.76/8.96 | | | | | End of split % 60.76/8.96 | | | | | % 60.76/8.96 | | | | End of split % 60.76/8.96 | | | | % 60.76/8.96 | | | End of split % 60.76/8.96 | | | % 60.76/8.96 | | Case 2: % 60.76/8.96 | | | % 60.76/8.96 | | | (398) all_96_18 = 0 & all_96_19 = 0 & all_96_20 = 0 & all_96_21 = 0 & % 60.76/8.96 | | | ~ (all_96_16 = all_96_17) & a_select3(pminus_ds1_filter, % 60.76/8.96 | | | all_96_22, all_96_23) = all_96_16 & % 60.76/8.96 | | | a_select3(pminus_ds1_filter, all_96_23, all_96_22) = all_96_17 & % 60.76/8.96 | | | leq(all_96_22, all_96_25) = 0 & leq(all_96_23, all_96_25) = 0 & % 60.76/8.96 | | | leq(n0, all_96_22) = 0 & leq(n0, all_96_23) = 0 & $i(all_96_16) & % 60.76/8.96 | | | $i(all_96_17) % 60.76/8.96 | | | % 60.76/8.96 | | | ALPHA: (398) implies: % 60.76/8.96 | | | (399) ~ (all_96_16 = all_96_17) % 60.76/8.96 | | | (400) leq(n0, all_96_23) = 0 % 60.76/8.96 | | | (401) leq(n0, all_96_22) = 0 % 60.76/8.96 | | | (402) leq(all_96_23, all_96_25) = 0 % 60.76/8.96 | | | (403) leq(all_96_22, all_96_25) = 0 % 60.76/8.96 | | | (404) a_select3(pminus_ds1_filter, all_96_23, all_96_22) = all_96_17 % 60.76/8.96 | | | (405) a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_96_16 % 60.76/8.96 | | | % 60.76/8.96 | | | REDUCE: (209), (403) imply: % 60.76/8.96 | | | (406) leq(all_96_22, n5) = 0 % 60.76/8.96 | | | % 60.76/8.96 | | | REDUCE: (209), (402) imply: % 60.76/8.96 | | | (407) leq(all_96_23, n5) = 0 % 60.76/8.96 | | | % 60.76/8.96 | | | GROUND_INST: instantiating (75) with all_96_22, all_96_23, all_96_17, % 60.76/8.96 | | | simplifying with (61), (62), (404) gives: % 60.76/8.96 | | | (408) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.76/8.96 | | | [v4: $i] : (a_select3(pminus_ds1_filter, all_96_22, all_96_23) = % 60.76/8.96 | | | v4 & leq(all_96_22, all_96_25) = v2 & leq(all_96_23, all_96_25) % 60.76/8.96 | | | = v3 & leq(n0, all_96_22) = v0 & leq(n0, all_96_23) = v1 & % 60.76/8.96 | | | $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 60.76/8.96 | | | | v4 = all_96_17)) % 60.76/8.96 | | | % 60.76/8.97 | | | GROUND_INST: instantiating (74) with all_96_23, all_96_22, all_96_17, % 60.76/8.97 | | | simplifying with (61), (62), (404) gives: % 60.76/8.97 | | | (409) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.76/8.97 | | | [v4: $i] : (a_select3(pminus_ds1_filter, all_96_22, all_96_23) = % 60.76/8.97 | | | v4 & leq(all_96_22, all_96_25) = v3 & leq(all_96_23, all_96_25) % 60.76/8.97 | | | = v2 & leq(n0, all_96_22) = v1 & leq(n0, all_96_23) = v0 & % 60.76/8.97 | | | $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 60.76/8.97 | | | | v4 = all_96_17)) % 60.76/8.97 | | | % 60.76/8.97 | | | GROUND_INST: instantiating (75) with all_96_23, all_96_22, all_96_16, % 60.76/8.97 | | | simplifying with (61), (62), (405) gives: % 60.76/8.97 | | | (410) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.76/8.97 | | | [v4: $i] : (a_select3(pminus_ds1_filter, all_96_23, all_96_22) = % 60.76/8.97 | | | v4 & leq(all_96_22, all_96_25) = v3 & leq(all_96_23, all_96_25) % 60.76/8.97 | | | = v2 & leq(n0, all_96_22) = v1 & leq(n0, all_96_23) = v0 & % 60.76/8.97 | | | $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 60.76/8.97 | | | | v4 = all_96_16)) % 60.76/8.97 | | | % 60.76/8.97 | | | GROUND_INST: instantiating (74) with all_96_22, all_96_23, all_96_16, % 60.76/8.97 | | | simplifying with (61), (62), (405) gives: % 60.76/8.97 | | | (411) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : ? % 60.76/8.97 | | | [v4: $i] : (a_select3(pminus_ds1_filter, all_96_23, all_96_22) = % 60.76/8.97 | | | v4 & leq(all_96_22, all_96_25) = v2 & leq(all_96_23, all_96_25) % 60.76/8.97 | | | = v3 & leq(n0, all_96_22) = v0 & leq(n0, all_96_23) = v1 & % 60.76/8.97 | | | $i(v4) & ( ~ (v3 = 0) | ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0) % 60.76/8.97 | | | | v4 = all_96_16)) % 60.76/8.97 | | | % 60.76/8.97 | | | DELTA: instantiating (411) with fresh symbols all_591_0, all_591_1, % 60.76/8.97 | | | all_591_2, all_591_3, all_591_4 gives: % 60.76/8.97 | | | (412) a_select3(pminus_ds1_filter, all_96_23, all_96_22) = all_591_0 & % 60.76/8.97 | | | leq(all_96_22, all_96_25) = all_591_2 & leq(all_96_23, all_96_25) % 60.76/8.97 | | | = all_591_1 & leq(n0, all_96_22) = all_591_4 & leq(n0, all_96_23) % 60.76/8.97 | | | = all_591_3 & $i(all_591_0) & ( ~ (all_591_1 = 0) | ~ (all_591_2 % 60.76/8.97 | | | = 0) | ~ (all_591_3 = 0) | ~ (all_591_4 = 0) | all_591_0 = % 60.76/8.97 | | | all_96_16) % 60.76/8.97 | | | % 60.76/8.97 | | | ALPHA: (412) implies: % 60.76/8.97 | | | (413) leq(n0, all_96_22) = all_591_4 % 60.76/8.97 | | | (414) leq(all_96_23, all_96_25) = all_591_1 % 60.76/8.97 | | | % 60.76/8.97 | | | DELTA: instantiating (410) with fresh symbols all_593_0, all_593_1, % 60.76/8.97 | | | all_593_2, all_593_3, all_593_4 gives: % 60.76/8.98 | | | (415) a_select3(pminus_ds1_filter, all_96_23, all_96_22) = all_593_0 & % 60.76/8.98 | | | leq(all_96_22, all_96_25) = all_593_1 & leq(all_96_23, all_96_25) % 60.76/8.98 | | | = all_593_2 & leq(n0, all_96_22) = all_593_3 & leq(n0, all_96_23) % 60.76/8.98 | | | = all_593_4 & $i(all_593_0) & ( ~ (all_593_1 = 0) | ~ (all_593_2 % 60.76/8.98 | | | = 0) | ~ (all_593_3 = 0) | ~ (all_593_4 = 0) | all_593_0 = % 60.76/8.98 | | | all_96_16) % 60.76/8.98 | | | % 60.76/8.98 | | | ALPHA: (415) implies: % 60.76/8.98 | | | (416) leq(n0, all_96_22) = all_593_3 % 60.76/8.98 | | | (417) leq(all_96_23, all_96_25) = all_593_2 % 60.76/8.98 | | | % 60.76/8.98 | | | DELTA: instantiating (409) with fresh symbols all_595_0, all_595_1, % 60.76/8.98 | | | all_595_2, all_595_3, all_595_4 gives: % 60.76/8.98 | | | (418) a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_595_0 & % 60.76/8.98 | | | leq(all_96_22, all_96_25) = all_595_1 & leq(all_96_23, all_96_25) % 60.76/8.98 | | | = all_595_2 & leq(n0, all_96_22) = all_595_3 & leq(n0, all_96_23) % 60.76/8.98 | | | = all_595_4 & $i(all_595_0) & ( ~ (all_595_1 = 0) | ~ (all_595_2 % 60.76/8.98 | | | = 0) | ~ (all_595_3 = 0) | ~ (all_595_4 = 0) | all_595_0 = % 60.76/8.98 | | | all_96_17) % 60.76/8.98 | | | % 60.76/8.98 | | | ALPHA: (418) implies: % 60.76/8.98 | | | (419) leq(n0, all_96_23) = all_595_4 % 60.76/8.98 | | | (420) leq(n0, all_96_22) = all_595_3 % 60.76/8.98 | | | (421) leq(all_96_23, all_96_25) = all_595_2 % 60.76/8.98 | | | (422) leq(all_96_22, all_96_25) = all_595_1 % 60.76/8.98 | | | (423) a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_595_0 % 60.76/8.98 | | | % 60.76/8.98 | | | DELTA: instantiating (408) with fresh symbols all_597_0, all_597_1, % 60.76/8.98 | | | all_597_2, all_597_3, all_597_4 gives: % 60.76/8.98 | | | (424) a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_597_0 & % 60.76/8.98 | | | leq(all_96_22, all_96_25) = all_597_2 & leq(all_96_23, all_96_25) % 60.76/8.98 | | | = all_597_1 & leq(n0, all_96_22) = all_597_4 & leq(n0, all_96_23) % 60.76/8.98 | | | = all_597_3 & $i(all_597_0) & ( ~ (all_597_1 = 0) | ~ (all_597_2 % 60.76/8.98 | | | = 0) | ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | all_597_0 = % 60.76/8.98 | | | all_96_17) % 60.76/8.98 | | | % 60.76/8.98 | | | ALPHA: (424) implies: % 60.76/8.98 | | | (425) leq(n0, all_96_23) = all_597_3 % 60.76/8.98 | | | (426) leq(n0, all_96_22) = all_597_4 % 60.76/8.98 | | | (427) leq(all_96_23, all_96_25) = all_597_1 % 60.76/8.98 | | | (428) leq(all_96_22, all_96_25) = all_597_2 % 60.76/8.98 | | | (429) a_select3(pminus_ds1_filter, all_96_22, all_96_23) = all_597_0 % 60.76/8.98 | | | (430) ~ (all_597_1 = 0) | ~ (all_597_2 = 0) | ~ (all_597_3 = 0) | ~ % 60.76/8.98 | | | (all_597_4 = 0) | all_597_0 = all_96_17 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (428) imply: % 60.76/8.98 | | | (431) leq(all_96_22, n5) = all_597_2 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (422) imply: % 60.76/8.98 | | | (432) leq(all_96_22, n5) = all_595_1 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (427) imply: % 60.76/8.98 | | | (433) leq(all_96_23, n5) = all_597_1 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (421) imply: % 60.76/8.98 | | | (434) leq(all_96_23, n5) = all_595_2 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (417) imply: % 60.76/8.98 | | | (435) leq(all_96_23, n5) = all_593_2 % 60.76/8.98 | | | % 60.76/8.98 | | | REDUCE: (209), (414) imply: % 60.76/8.98 | | | (436) leq(all_96_23, n5) = all_591_1 % 60.76/8.98 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with 0, all_597_3, all_96_23, n0, % 60.76/8.99 | | | simplifying with (400), (425) gives: % 60.76/8.99 | | | (437) all_597_3 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_595_4, all_597_3, all_96_23, n0, % 60.76/8.99 | | | simplifying with (419), (425) gives: % 60.76/8.99 | | | (438) all_597_3 = all_595_4 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with 0, all_593_3, all_96_22, n0, % 60.76/8.99 | | | simplifying with (401), (416) gives: % 60.76/8.99 | | | (439) all_593_3 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_595_3, all_597_4, all_96_22, n0, % 60.76/8.99 | | | simplifying with (420), (426) gives: % 60.76/8.99 | | | (440) all_597_4 = all_595_3 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_593_3, all_597_4, all_96_22, n0, % 60.76/8.99 | | | simplifying with (416), (426) gives: % 60.76/8.99 | | | (441) all_597_4 = all_593_3 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_591_4, all_597_4, all_96_22, n0, % 60.76/8.99 | | | simplifying with (413), (426) gives: % 60.76/8.99 | | | (442) all_597_4 = all_591_4 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with 0, all_593_2, n5, all_96_23, % 60.76/8.99 | | | simplifying with (407), (435) gives: % 60.76/8.99 | | | (443) all_593_2 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_595_2, all_597_1, n5, all_96_23, % 60.76/8.99 | | | simplifying with (433), (434) gives: % 60.76/8.99 | | | (444) all_597_1 = all_595_2 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_593_2, all_597_1, n5, all_96_23, % 60.76/8.99 | | | simplifying with (433), (435) gives: % 60.76/8.99 | | | (445) all_597_1 = all_593_2 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_591_1, all_597_1, n5, all_96_23, % 60.76/8.99 | | | simplifying with (433), (436) gives: % 60.76/8.99 | | | (446) all_597_1 = all_591_1 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with 0, all_597_2, n5, all_96_22, % 60.76/8.99 | | | simplifying with (406), (431) gives: % 60.76/8.99 | | | (447) all_597_2 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (28) with all_595_1, all_597_2, n5, all_96_22, % 60.76/8.99 | | | simplifying with (431), (432) gives: % 60.76/8.99 | | | (448) all_597_2 = all_595_1 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (29) with all_96_16, all_597_0, all_96_23, % 60.76/8.99 | | | all_96_22, pminus_ds1_filter, simplifying with (405), (429) % 60.76/8.99 | | | gives: % 60.76/8.99 | | | (449) all_597_0 = all_96_16 % 60.76/8.99 | | | % 60.76/8.99 | | | GROUND_INST: instantiating (29) with all_595_0, all_597_0, all_96_23, % 60.76/8.99 | | | all_96_22, pminus_ds1_filter, simplifying with (423), (429) % 60.76/8.99 | | | gives: % 60.76/8.99 | | | (450) all_597_0 = all_595_0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (449), (450) imply: % 60.76/8.99 | | | (451) all_595_0 = all_96_16 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (444), (446) imply: % 60.76/8.99 | | | (452) all_595_2 = all_591_1 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (444), (445) imply: % 60.76/8.99 | | | (453) all_595_2 = all_593_2 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (447), (448) imply: % 60.76/8.99 | | | (454) all_595_1 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (437), (438) imply: % 60.76/8.99 | | | (455) all_595_4 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (440), (441) imply: % 60.76/8.99 | | | (456) all_595_3 = all_593_3 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (440), (442) imply: % 60.76/8.99 | | | (457) all_595_3 = all_591_4 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (452), (453) imply: % 60.76/8.99 | | | (458) all_593_2 = all_591_1 % 60.76/8.99 | | | % 60.76/8.99 | | | SIMP: (458) implies: % 60.76/8.99 | | | (459) all_593_2 = all_591_1 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (456), (457) imply: % 60.76/8.99 | | | (460) all_593_3 = all_591_4 % 60.76/8.99 | | | % 60.76/8.99 | | | SIMP: (460) implies: % 60.76/8.99 | | | (461) all_593_3 = all_591_4 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (443), (459) imply: % 60.76/8.99 | | | (462) all_591_1 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (439), (461) imply: % 60.76/8.99 | | | (463) all_591_4 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (457), (463) imply: % 60.76/8.99 | | | (464) all_595_3 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (452), (462) imply: % 60.76/8.99 | | | (465) all_595_2 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (440), (464) imply: % 60.76/8.99 | | | (466) all_597_4 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | COMBINE_EQS: (444), (465) imply: % 60.76/8.99 | | | (467) all_597_1 = 0 % 60.76/8.99 | | | % 60.76/8.99 | | | BETA: splitting (430) gives: % 60.76/8.99 | | | % 60.76/8.99 | | | Case 1: % 60.76/8.99 | | | | % 60.76/8.99 | | | | (468) ~ (all_597_1 = 0) % 60.76/8.99 | | | | % 60.76/8.99 | | | | REDUCE: (467), (468) imply: % 60.76/8.99 | | | | (469) $false % 60.76/8.99 | | | | % 60.76/8.99 | | | | CLOSE: (469) is inconsistent. % 60.76/8.99 | | | | % 60.76/8.99 | | | Case 2: % 60.76/8.99 | | | | % 60.76/8.99 | | | | (470) ~ (all_597_2 = 0) | ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | % 60.76/8.99 | | | | all_597_0 = all_96_17 % 60.76/8.99 | | | | % 60.76/8.99 | | | | BETA: splitting (470) gives: % 60.76/8.99 | | | | % 60.76/8.99 | | | | Case 1: % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | (471) ~ (all_597_2 = 0) % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | REDUCE: (447), (471) imply: % 60.76/8.99 | | | | | (472) $false % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | CLOSE: (472) is inconsistent. % 60.76/8.99 | | | | | % 60.76/8.99 | | | | Case 2: % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | (473) ~ (all_597_3 = 0) | ~ (all_597_4 = 0) | all_597_0 = % 60.76/8.99 | | | | | all_96_17 % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | BETA: splitting (473) gives: % 60.76/8.99 | | | | | % 60.76/8.99 | | | | | Case 1: % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | (474) ~ (all_597_3 = 0) % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | REDUCE: (437), (474) imply: % 60.76/8.99 | | | | | | (475) $false % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | CLOSE: (475) is inconsistent. % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | Case 2: % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | (476) ~ (all_597_4 = 0) | all_597_0 = all_96_17 % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | BETA: splitting (476) gives: % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | | Case 1: % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | (477) ~ (all_597_4 = 0) % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | REDUCE: (466), (477) imply: % 60.76/8.99 | | | | | | | (478) $false % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | CLOSE: (478) is inconsistent. % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | Case 2: % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | (479) all_597_0 = all_96_17 % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | COMBINE_EQS: (449), (479) imply: % 60.76/8.99 | | | | | | | (480) all_96_16 = all_96_17 % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | REDUCE: (399), (480) imply: % 60.76/8.99 | | | | | | | (481) $false % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | | CLOSE: (481) is inconsistent. % 60.76/8.99 | | | | | | | % 60.76/8.99 | | | | | | End of split % 60.76/8.99 | | | | | | % 60.76/8.99 | | | | | End of split % 60.76/8.99 | | | | | % 60.76/8.99 | | | | End of split % 60.76/8.99 | | | | % 60.76/8.99 | | | End of split % 60.76/8.99 | | | % 60.76/8.99 | | End of split % 60.76/8.99 | | % 60.76/8.99 | End of split % 60.76/8.99 | % 60.76/8.99 End of proof % 60.76/8.99 % SZS output end Proof for theBenchmark % 60.76/8.99 % 60.76/8.99 8373ms %------------------------------------------------------------------------------