%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:11:47 EDT 2023 % Result : Theorem 44.06s 6.55s % Output : Proof 59.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.04/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.36 % Computer : n023.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Sun Aug 27 16:57:11 EDT 2023 % 0.14/0.36 % CPUTime : % 0.52/0.63 ________ _____ % 0.52/0.63 ___ __ \_________(_)________________________________ % 0.52/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.52/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.52/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.52/0.63 % 0.52/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.52/0.63 (2023-06-19) % 0.52/0.63 % 0.52/0.63 (c) Philipp Rümmer, 2009-2023 % 0.52/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.52/0.63 Amanda Stjerna. % 0.52/0.63 Free software under BSD-3-Clause. % 0.52/0.63 % 0.52/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.52/0.63 % 0.52/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.68/0.64 Running up to 7 provers in parallel. % 0.68/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.68/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.68/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.68/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.68/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.68/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.68/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 14.81/2.72 Prover 6: Preprocessing ... % 14.81/2.72 Prover 4: Preprocessing ... % 14.81/2.73 Prover 1: Preprocessing ... % 15.12/2.79 Prover 5: Preprocessing ... % 15.12/2.79 Prover 3: Preprocessing ... % 15.12/2.80 Prover 0: Preprocessing ... % 15.12/2.81 Prover 2: Preprocessing ... % 33.09/5.08 Prover 3: Warning: ignoring some quantifiers % 33.28/5.12 Prover 1: Warning: ignoring some quantifiers % 34.21/5.23 Prover 3: Constructing countermodel ... % 34.21/5.24 Prover 6: Proving ... % 34.21/5.26 Prover 1: Constructing countermodel ... % 35.55/5.42 Prover 4: Warning: ignoring some quantifiers % 37.62/5.67 Prover 4: Constructing countermodel ... % 38.84/5.83 Prover 0: Proving ... % 39.42/5.95 Prover 5: Proving ... % 44.06/6.55 Prover 3: proved (5899ms) % 44.06/6.55 % 44.06/6.55 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 44.06/6.55 % 44.06/6.55 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 44.06/6.55 Prover 6: stopped % 44.45/6.57 Prover 0: stopped % 44.45/6.57 Prover 5: stopped % 44.45/6.57 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 44.45/6.57 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 44.45/6.58 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 44.45/6.60 Prover 2: Proving ... % 44.45/6.60 Prover 2: stopped % 44.45/6.60 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 52.52/7.63 Prover 10: Preprocessing ... % 52.78/7.65 Prover 13: Preprocessing ... % 53.37/7.74 Prover 7: Preprocessing ... % 53.37/7.75 Prover 11: Preprocessing ... % 53.86/7.80 Prover 8: Preprocessing ... % 55.64/8.07 Prover 1: Found proof (size 75) % 55.64/8.07 Prover 1: proved (7420ms) % 55.64/8.07 Prover 10: stopped % 55.64/8.07 Prover 4: stopped % 55.64/8.08 Prover 7: stopped % 56.14/8.09 Prover 11: stopped % 56.14/8.12 Prover 13: stopped % 57.46/8.46 Prover 8: Warning: ignoring some quantifiers % 57.99/8.53 Prover 8: Constructing countermodel ... % 57.99/8.54 Prover 8: stopped % 57.99/8.54 % 57.99/8.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.99/8.54 % 57.99/8.57 % SZS output start Proof for theBenchmark % 57.99/8.61 Assumptions after simplification: % 57.99/8.61 --------------------------------- % 57.99/8.61 % 57.99/8.61 (axiom10) % 58.39/8.63 Nat$(i$) & A_b_vec_c_vec$(a$) & ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : % 58.39/8.63 ($lesseq(v1, v2) & nrows$(a$) = v0 & of_nat$(v0) = v1 & of_nat$(i$) = v2 & % 58.39/8.63 Nat$(v0)) % 58.39/8.63 % 58.39/8.63 (axiom11) % 58.39/8.63 Nat$(k$) & A_b_vec_c_vec$(a$) & ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : % 58.39/8.63 ($lesseq(1, $difference(v1, v2)) & ncols$(a$) = v0 & of_nat$(v0) = v1 & % 58.39/8.63 of_nat$(k$) = v2 & Nat$(v0)) % 58.39/8.63 % 58.39/8.63 (axiom271) % 58.39/8.64 ! [v0: Nat$] : ! [v1: A_b_vec_c_vec$] : ! [v2: Nat_a_b_vec_c_vec_prod$] : ( % 58.39/8.64 ~ (pair$a(v0, v1) = v2) | ~ Nat$(v0) | ~ A_b_vec_c_vec$(v1) | snd$(v2) = % 58.39/8.64 v1) % 58.39/8.64 % 58.39/8.64 (axiom273) % 58.39/8.64 ! [v0: Nat$] : ! [v1: A_iarray_iarray$] : ! [v2: Nat_a_iarray_iarray_prod$] % 58.39/8.64 : ( ~ (pair$d(v0, v1) = v2) | ~ Nat$(v0) | ~ A_iarray_iarray$(v1) | % 58.39/8.64 snd$c(v2) = v1) % 58.39/8.64 % 58.39/8.64 (axiom275) % 58.39/8.64 ! [v0: A$] : ! [v1: Nat_a_b_vec_c_vec_prod$] : ! [v2: % 58.39/8.64 A_nat_a_b_vec_c_vec_prod_prod$] : ( ~ (pair$(v0, v1) = v2) | ~ % 58.39/8.64 Nat_a_b_vec_c_vec_prod$(v1) | ~ A$(v0) | snd$a(v2) = v1) % 58.39/8.64 % 58.39/8.64 (axiom276) % 58.39/8.64 ! [v0: A$] : ! [v1: Nat_a_iarray_iarray_prod$] : ! [v2: % 58.39/8.64 A_nat_a_iarray_iarray_prod_prod$] : ( ~ (pair$c(v0, v1) = v2) | ~ A$(v0) | % 58.39/8.64 ~ Nat_a_iarray_iarray_prod$(v1) | snd$d(v2) = v1) % 58.39/8.64 % 58.39/8.64 (axiom507) % 58.39/8.64 ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : ! [v3: int] : ( ~ ($lesseq(1, % 58.39/8.64 $difference(v2, v3))) | ~ (of_nat$(v1) = v2) | ~ (of_nat$(v0) = v3) | % 58.39/8.64 ~ Nat$(v1) | ~ Nat$(v0) | ? [v4: Nat$] : (of_nat$(v4) = $difference(v2, % 58.39/8.64 v3) & Nat$(v4))) % 58.39/8.64 % 58.39/8.64 (axiom571) % 58.39/8.65 ! [v0: A_b_vec_c_vec$] : ! [v1: Nat$] : ( ~ (nrows$(v0) = v1) | ~ % 58.39/8.65 A_b_vec_c_vec$(v0) | ? [v2: int] : ? [v3: A_iarray_iarray$] : ? [v4: % 58.39/8.65 Nat$] : (matrix_to_iarray$(v0) = v3 & nrows_iarray$(v3) = v4 & of_nat$(v4) % 58.39/8.65 = v2 & of_nat$(v1) = v2 & Nat$(v4) & A_iarray_iarray$(v3))) % 58.39/8.65 % 58.39/8.65 (axiom9) % 58.39/8.65 Nat$(i$) & A_b_vec_c_vec$(a$) & ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : % 58.39/8.65 ($lesseq(v2, v1) & nrows$(a$) = v0 & of_nat$(v0) = v1 & of_nat$(i$) = v2 & % 58.39/8.65 Nat$(v0)) % 58.39/8.65 % 58.39/8.65 (conjecture8) % 58.39/8.66 Nat_a_iarray_prod_bool_fun$(vector_all_zero_from_index$) & A$(n$) & A$(zero$a) % 58.39/8.66 & Nat$(k$) & Nat$(i$) & A_b_vec_c_vec$(a$) & ? [v0: C$] : ? [v1: % 58.39/8.66 C_a_b_vec_fun$] : ? [v2: B$] : ? [v3: int] : ? [v4: Nat$] : ? [v5: int] % 58.39/8.66 : ? [v6: A_iarray_iarray$] : ? [v7: A_iarray$] : ? [v8: Nat_a_iarray_prod$] % 58.39/8.66 : ? [v9: any] : ? [v10: Nat$] : ? [v11: int] : ? [v12: % 58.39/8.66 Nat_a_b_vec_c_vec_prod$] : ? [v13: A_nat_a_b_vec_c_vec_prod_prod$] : ? % 58.39/8.66 [v14: Nat_a_b_vec_c_vec_prod$] : ? [v15: A_b_vec_c_vec$] : ? [v16: % 58.39/8.66 A_iarray_iarray$] : ? [v17: Nat_a_iarray_iarray_prod$] : ? [v18: % 58.39/8.66 A_nat_a_iarray_iarray_prod_prod$] : ? [v19: Nat_a_iarray_iarray_prod$] : ? % 58.39/8.66 [v20: A_iarray_iarray$] : ? [v21: A_a_iarray_iarray_prod$] : ? [v22: A$] : % 58.39/8.66 ? [v23: A_a_fun$] : ? [v24: A$] : ? [v25: Nat$] : ? [v26: A_iarray_iarray$] % 58.39/8.66 : ? [v27: Nat_a_iarray_iarray_prod$] : ? [v28: % 58.39/8.66 A_nat_a_iarray_iarray_prod_prod$] : ? [v29: Nat_a_iarray_iarray_prod$] : ? % 58.39/8.66 [v30: A_iarray_iarray$] : ? [v31: A_a_b_vec_c_vec_prod$] : ? [v32: A$] : ? % 58.39/8.66 [v33: A_a_fun$] : ? [v34: A$] : ? [v35: A_b_vec_c_vec$] : ? [v36: % 58.39/8.66 Nat_a_b_vec_c_vec_prod$] : ? [v37: A_nat_a_b_vec_c_vec_prod_prod$] : ? % 58.39/8.66 [v38: Nat_a_b_vec_c_vec_prod$] : ? [v39: A_b_vec_c_vec$] : ? [v40: % 58.39/8.66 A_iarray_iarray$] : (matrix_to_iarray$(v39) = v40 & matrix_to_iarray$(v15) = % 58.39/8.66 v16 & matrix_to_iarray$(a$) = v6 & gauss_Jordan_in_ij_det_P$(a$, v0, v2) = % 58.39/8.66 v31 & vec_nth$a(a$) = v1 & from_nat$a(k$) = v2 & from_nat$(i$) = v0 & % 58.39/8.66 gauss_Jordan_in_ij_det_P_iarrays$(v6, i$, k$) = v21 & nat$($sum(v3, 1)) = % 58.39/8.66 v25 & column_iarray$(k$, v6) = v7 & nrows_iarray$(v6) = v10 & % 58.39/8.66 fun_app$e(vector_all_zero_from_index$, v8) = v9 & times$(v32) = v33 & % 58.39/8.66 times$(v22) = v23 & fst$a(v21) = v22 & snd$e(v21) = v26 & snd$d(v28) = v29 & % 58.39/8.66 snd$d(v18) = v19 & pair$c(v24, v27) = v28 & pair$c(n$, v17) = v18 & % 58.39/8.66 snd$a(v37) = v38 & snd$a(v13) = v14 & pair$(v34, v36) = v37 & pair$(n$, v12) % 58.39/8.66 = v13 & fst$(v31) = v32 & snd$b(v31) = v35 & snd$c(v29) = v30 & snd$c(v19) = % 58.39/8.66 v20 & pair$d(v25, v26) = v27 & pair$d(i$, v6) = v17 & pair$b(i$, v7) = v8 & % 58.39/8.66 snd$(v38) = v39 & snd$(v14) = v15 & pair$a(v25, v35) = v36 & pair$a(i$, a$) % 58.39/8.66 = v12 & nrows$(a$) = v4 & of_nat$(v10) = v11 & of_nat$(v4) = v5 & % 58.39/8.66 of_nat$(i$) = v3 & fun_app$b(v33, n$) = v34 & fun_app$b(v23, n$) = v24 & % 58.39/8.66 Nat_a_iarray_prod$(v8) & A_iarray$(v7) & A_a_fun$(v33) & A_a_fun$(v23) & % 58.39/8.66 Nat_a_b_vec_c_vec_prod$(v38) & Nat_a_b_vec_c_vec_prod$(v36) & % 58.39/8.66 Nat_a_b_vec_c_vec_prod$(v14) & Nat_a_b_vec_c_vec_prod$(v12) & A$(v34) & % 58.39/8.66 A$(v32) & A$(v24) & A$(v22) & Nat_a_iarray_iarray_prod$(v29) & % 58.39/8.66 Nat_a_iarray_iarray_prod$(v27) & Nat_a_iarray_iarray_prod$(v19) & % 58.39/8.66 Nat_a_iarray_iarray_prod$(v17) & A_a_b_vec_c_vec_prod$(v31) & Nat$(v25) & % 58.39/8.66 Nat$(v10) & Nat$(v4) & C$(v0) & C_a_b_vec_fun$(v1) & A_b_vec_c_vec$(v39) & % 58.39/8.66 A_b_vec_c_vec$(v35) & A_b_vec_c_vec$(v15) & B$(v2) & % 58.39/8.66 A_a_iarray_iarray_prod$(v21) & A_iarray_iarray$(v40) & A_iarray_iarray$(v30) % 58.39/8.66 & A_iarray_iarray$(v26) & A_iarray_iarray$(v20) & A_iarray_iarray$(v16) & % 58.39/8.66 A_iarray_iarray$(v6) & A_nat_a_iarray_iarray_prod_prod$(v28) & % 58.39/8.66 A_nat_a_iarray_iarray_prod_prod$(v18) & A_nat_a_b_vec_c_vec_prod_prod$(v37) % 58.39/8.66 & A_nat_a_b_vec_c_vec_prod_prod$(v13) & (( ~ (v5 = v3) & ? [v41: C$] : ? % 58.39/8.66 [v42: A_b_vec$] : ? [v43: B_a_fun$] : ? [v44: A$] : ( ~ (v44 = zero$a) % 58.39/8.66 & fun_app$d(v1, v41) = v42 & vec_nth$(v42) = v43 & fun_app$c(v43, v2) % 58.39/8.66 = v44 & less_eq$(v0, v41) = 0 & A$(v44) & B_a_fun$(v43) & % 58.39/8.66 A_b_vec$(v42) & C$(v41)) & (( ~ (v40 = v30) & ~ (v11 = v3) & ~ (v9 = % 58.39/8.66 0)) | ( ~ (v40 = v20) & (v11 = v3 | v9 = 0)))) | ((v5 = v3 | ! % 58.39/8.66 [v41: C$] : ( ~ (less_eq$(v0, v41) = 0) | ~ C$(v41) | ? [v42: % 58.39/8.66 A_b_vec$] : ? [v43: B_a_fun$] : (fun_app$d(v1, v41) = v42 & % 58.39/8.66 vec_nth$(v42) = v43 & fun_app$c(v43, v2) = zero$a & B_a_fun$(v43) % 58.39/8.66 & A_b_vec$(v42)))) & (( ~ (v30 = v16) & ~ (v11 = v3) & ~ (v9 = % 58.39/8.66 0)) | ( ~ (v20 = v16) & (v11 = v3 | v9 = 0)))))) % 58.39/8.66 % 58.39/8.66 (function-axioms) % 58.77/8.71 ! [v0: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.71 A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! [v2: B$] : ! [v3: C$] : ! [v4: % 58.77/8.71 Nat$] : ! [v5: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ % 58.77/8.71 (row_add_iterate_PA$(v5, v4, v3, v2) = v1) | ~ (row_add_iterate_PA$(v5, v4, % 58.77/8.71 v3, v2) = v0)) & ! [v0: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.71 A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! [v2: B$] : ! [v3: C$] : ! [v4: % 58.77/8.71 A_c_vec_c_vec_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_PA$c(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij_PA$c(v4, % 58.77/8.71 v3, v2) = v0)) & ! [v0: A_b_vec_b_vec_a_b_vec_b_vec_prod$] : ! [v1: % 58.77/8.71 A_b_vec_b_vec_a_b_vec_b_vec_prod$] : ! [v2: B$] : ! [v3: B$] : ! [v4: % 58.77/8.71 A_b_vec_b_vec_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_PA$b(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij_PA$b(v4, % 58.77/8.71 v3, v2) = v0)) & ! [v0: A_b_vec_b_vec_a_c_vec_b_vec_prod$] : ! [v1: % 58.77/8.71 A_b_vec_b_vec_a_c_vec_b_vec_prod$] : ! [v2: C$] : ! [v3: B$] : ! [v4: % 58.77/8.71 A_b_vec_b_vec_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_PA$a(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij_PA$a(v4, % 58.77/8.71 v3, v2) = v0)) & ! [v0: A_c_vec_c_vec_a_c_vec_c_vec_prod$] : ! [v1: % 58.77/8.71 A_c_vec_c_vec_a_c_vec_c_vec_prod$] : ! [v2: C$] : ! [v3: C$] : ! [v4: % 58.77/8.71 A_c_vec_c_vec_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_PA$(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij_PA$(v4, % 58.77/8.71 v3, v2) = v0)) & ! [v0: A_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.71 A_a_b_vec_c_vec_prod$] : ! [v2: B$] : ! [v3: C$] : ! [v4: A_b_vec_c_vec$] % 58.77/8.71 : (v1 = v0 | ~ (gauss_Jordan_in_ij_det_P$(v4, v3, v2) = v1) | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$(v4, v3, v2) = v0)) & ! [v0: % 58.77/8.71 A_a_b_vec_b_vec_prod$] : ! [v1: A_a_b_vec_b_vec_prod$] : ! [v2: B$] : ! % 58.77/8.71 [v3: B$] : ! [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$c(v4, v3, v2) = v1) | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$c(v4, v3, v2) = v0)) & ! [v0: % 58.77/8.71 A_a_c_vec_b_vec_prod$] : ! [v1: A_a_c_vec_b_vec_prod$] : ! [v2: C$] : ! % 58.77/8.71 [v3: B$] : ! [v4: A_c_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$b(v4, v3, v2) = v1) | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$b(v4, v3, v2) = v0)) & ! [v0: % 58.77/8.71 A_a_c_vec_c_vec_prod$] : ! [v1: A_a_c_vec_c_vec_prod$] : ! [v2: C$] : ! % 58.77/8.71 [v3: C$] : ! [v4: A_c_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$a(v4, v3, v2) = v1) | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P$a(v4, v3, v2) = v0)) & ! [v0: % 58.77/8.71 A_a_iarray_iarray_prod$] : ! [v1: A_a_iarray_iarray_prod$] : ! [v2: Nat$] % 58.77/8.71 : ! [v3: Nat$] : ! [v4: A_iarray_iarray$] : (v1 = v0 | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P_iarrays$(v4, v3, v2) = v1) | ~ % 58.77/8.71 (gauss_Jordan_in_ij_det_P_iarrays$(v4, v3, v2) = v0)) & ! [v0: % 58.77/8.71 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Int_set$] : ! % 58.77/8.71 [v3: Int_set$] : (v1 = v0 | ~ (less_eq$d(v3, v2) = v1) | ~ (less_eq$d(v3, % 58.77/8.71 v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: A_set$] : ! % 58.77/8.71 [v3: A_set$] : (v1 = v0 | ~ (plus$q(v3, v2) = v1) | ~ (plus$q(v3, v2) = v0)) % 58.77/8.71 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_set$] : % 58.77/8.71 ! [v3: A_set$] : (v1 = v0 | ~ (less_eq$c(v3, v2) = v1) | ~ (less_eq$c(v3, % 58.77/8.71 v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_set$] : % 58.77/8.71 ! [v3: Nat_set$] : (v1 = v0 | ~ (times$g(v3, v2) = v1) | ~ (times$g(v3, v2) % 58.77/8.71 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 58.77/8.71 Nat_set$] : ! [v3: Nat$] : (v1 = v0 | ~ (member$b(v3, v2) = v1) | ~ % 58.77/8.72 (member$b(v3, v2) = v0)) & ! [v0: Int_set$] : ! [v1: Int_set$] : ! [v2: % 58.77/8.72 Int_set$] : ! [v3: Int_set$] : (v1 = v0 | ~ (times$f(v3, v2) = v1) | ~ % 58.77/8.72 (times$f(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 58.77/8.72 A_set$] : ! [v3: A_set$] : (v1 = v0 | ~ (times$e(v3, v2) = v1) | ~ % 58.77/8.72 (times$e(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_set$] : ! [v3: A$] : (v1 = v0 | ~ % 58.77/8.72 (member$a(v3, v2) = v1) | ~ (member$a(v3, v2) = v0)) & ! [v0: Int_set$] : % 58.77/8.72 ! [v1: Int_set$] : ! [v2: Int_set$] : ! [v3: Int_set$] : (v1 = v0 | ~ % 58.77/8.72 (plus$p(v3, v2) = v1) | ~ (plus$p(v3, v2) = v0)) & ! [v0: % 58.77/8.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Int_set$] : ! % 58.77/8.72 [v3: int] : (v1 = v0 | ~ (member$(v3, v2) = v1) | ~ (member$(v3, v2) = v0)) % 58.77/8.72 & ! [v0: A_iarray_iarray_bool_fun$] : ! [v1: A_iarray_iarray_bool_fun$] : ! % 58.77/8.72 [v2: A$] : ! [v3: A_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ % 58.77/8.72 (fun_app$x(v3, v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_iarray_iarray_prod_bool_fun$] : ! [v1: % 58.77/8.72 Nat_a_iarray_iarray_prod_bool_fun$] : ! [v2: A$] : ! [v3: % 58.77/8.72 A_nat_a_iarray_iarray_prod_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$w(v3, v2) % 58.77/8.72 = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_b_vec_c_vec_prod_bool_fun$] : ! [v1: % 58.77/8.72 Nat_a_b_vec_c_vec_prod_bool_fun$] : ! [v2: A$] : ! [v3: % 58.77/8.72 A_nat_a_b_vec_c_vec_prod_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$v(v3, v2) = % 58.77/8.72 v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: A_b_vec_c_vec_bool_fun$] : ! % 58.77/8.72 [v1: A_b_vec_c_vec_bool_fun$] : ! [v2: A$] : ! [v3: % 58.77/8.72 A_a_b_vec_c_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$u(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$u(v3, v2) = v0)) & ! [v0: A_iarray_iarray_bool_fun$] : ! [v1: % 58.77/8.72 A_iarray_iarray_bool_fun$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 Nat_a_iarray_iarray_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) = v1) % 58.77/8.72 | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_iarray_iarray$] : ! [v3: % 58.77/8.72 A_iarray_iarray_bool_fun$] : (v1 = v0 | ~ (fun_app$s(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$s(v3, v2) = v0)) & ! [v0: A_iarray_bool_fun$] : ! [v1: % 58.77/8.72 A_iarray_bool_fun$] : ! [v2: Nat$] : ! [v3: Nat_a_iarray_bool_fun_fun$] : % 58.77/8.72 (v1 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! % 58.77/8.72 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_iarray$] : ! % 58.77/8.72 [v3: A_iarray_bool_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$q(v3, v2) = v0)) & ! [v0: A_b_vec_c_vec_bool_fun$] : ! [v1: % 58.77/8.72 A_b_vec_c_vec_bool_fun$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 Nat_a_b_vec_c_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | % 58.77/8.72 ~ (fun_app$p(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_b_vec_c_vec$] : ! [v3: % 58.77/8.72 A_b_vec_c_vec_bool_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$o(v3, v2) = v0)) & ! [v0: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! % 58.77/8.72 [v1: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : ! [v2: A_b_vec_c_vec$] : ! [v3: % 58.77/8.72 A_c_vec_c_vec$] : (v1 = v0 | ~ (pair$x(v3, v2) = v1) | ~ (pair$x(v3, v2) = % 58.77/8.72 v0)) & ! [v0: A_b_vec_b_vec_a_b_vec_b_vec_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_a_b_vec_b_vec_prod$] : ! [v2: A_b_vec_b_vec$] : ! [v3: % 58.77/8.72 A_b_vec_b_vec$] : (v1 = v0 | ~ (pair$w(v3, v2) = v1) | ~ (pair$w(v3, v2) = % 58.77/8.72 v0)) & ! [v0: A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_b_vec_prod$] : ! [v3: A_b_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.72 (pair$v(v3, v2) = v1) | ~ (pair$v(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$c(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$c(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec_b_vec_a_c_vec_b_vec_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_a_c_vec_b_vec_prod$] : ! [v2: A_c_vec_b_vec$] : ! [v3: % 58.77/8.72 A_b_vec_b_vec$] : (v1 = v0 | ~ (pair$u(v3, v2) = v1) | ~ (pair$u(v3, v2) = % 58.77/8.72 v0)) & ! [v0: A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : ! [v2: % 58.77/8.72 Nat_a_c_vec_b_vec_prod$] : ! [v3: A_b_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.72 (pair$t(v3, v2) = v1) | ~ (pair$t(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$b(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$b(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_c_vec_c_vec_a_c_vec_c_vec_prod$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec_a_c_vec_c_vec_prod$] : ! [v2: A_c_vec_c_vec$] : ! [v3: % 58.77/8.72 A_c_vec_c_vec$] : (v1 = v0 | ~ (pair$s(v3, v2) = v1) | ~ (pair$s(v3, v2) = % 58.77/8.72 v0)) & ! [v0: A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : ! [v2: % 58.77/8.72 Nat_a_c_vec_c_vec_prod$] : ! [v3: A_c_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.72 (pair$r(v3, v2) = v1) | ~ (pair$r(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$a(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$a(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : ! [v3: A_c_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.72 (pair$q(v3, v2) = v1) | ~ (pair$q(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_PA$(v3, v2) = v1) | ~ (gauss_Jordan_column_k_PA$(v3, % 58.77/8.72 v2) = v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! [v2: % 58.77/8.72 C$] : ! [v3: A_b_vec_c_vec_c_vec$] : (v1 = v0 | ~ (vec_nth$f(v3, v2) = v1) % 58.77/8.72 | ~ (vec_nth$f(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: B$] : ! [v3: B$] : (v1 = v0 | ~ (less$b(v3, % 58.77/8.72 v2) = v1) | ~ (less$b(v3, v2) = v0)) & ! [v0: A_b_vec_bool_fun$] : ! % 58.77/8.72 [v1: A_b_vec_bool_fun$] : ! [v2: C$] : ! [v3: C_a_b_vec_bool_fun_fun$] : (v1 % 58.77/8.72 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: % 58.77/8.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_b_vec$] : ! % 58.77/8.72 [v3: A_b_vec_bool_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$m(v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! % 58.77/8.72 [v2: B$] : ! [v3: B_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) % 58.77/8.72 | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A$] : ! [v3: A_bool_fun$] : (v1 = v0 | ~ % 58.77/8.72 (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! [v2: A_b_vec_c_vec$] : ! % 58.77/8.72 [v3: A_a_fun$] : (v1 = v0 | ~ (map_matrix$(v3, v2) = v1) | ~ % 58.77/8.72 (map_matrix$(v3, v2) = v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: % 58.77/8.72 A_b_vec_c_vec$] : ! [v2: A_b_vec_c_vec$] : ! [v3: A_b_vec_c_vec$] : (v1 = % 58.77/8.72 v0 | ~ (times$d(v3, v2) = v1) | ~ (times$d(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: A_b_vec$] : ! [v3: A_b_vec$] : (v1 % 58.77/8.72 = v0 | ~ (times$c(v3, v2) = v1) | ~ (times$c(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: A_b_vec$] : ! [v3: A_b_vec$] : (v1 % 58.77/8.72 = v0 | ~ (plus$o(v3, v2) = v1) | ~ (plus$o(v3, v2) = v0)) & ! [v0: % 58.77/8.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: C$] : ! [v3: C$] % 58.77/8.72 : (v1 = v0 | ~ (less$a(v3, v2) = v1) | ~ (less$a(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Int_a_prod$] : ! [v1: Int_a_prod$] : ! [v2: A$] : ! [v3: int] : (v1 = v0 % 58.77/8.72 | ~ (pair$p(v3, v2) = v1) | ~ (pair$p(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_int_prod$] : ! [v1: A_int_prod$] : ! [v2: int] : ! [v3: A$] : (v1 = v0 % 58.77/8.72 | ~ (pair$o(v3, v2) = v1) | ~ (pair$o(v3, v2) = v0)) & ! [v0: A_a_prod$] % 58.77/8.72 : ! [v1: A_a_prod$] : ! [v2: A$] : ! [v3: A$] : (v1 = v0 | ~ (pair$n(v3, % 58.77/8.72 v2) = v1) | ~ (pair$n(v3, v2) = v0)) & ! [v0: Int_int_prod$] : ! [v1: % 58.77/8.72 Int_int_prod$] : ! [v2: Int_int_prod$] : ! [v3: Int_int_prod$] : (v1 = v0 % 58.77/8.72 | ~ (plus$n(v3, v2) = v1) | ~ (plus$n(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Int_int_prod$] : ! [v1: Int_int_prod$] : ! [v2: int] : ! [v3: int] : (v1 % 58.77/8.72 = v0 | ~ (pair$m(v3, v2) = v1) | ~ (pair$m(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_iarray$] : ! [v1: A_iarray$] : ! [v2: A_iarray$] : ! [v3: A_iarray$] : % 58.77/8.72 (v1 = v0 | ~ (plus$m(v3, v2) = v1) | ~ (plus$m(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_iarray_prod$] : ! [v1: Nat_a_iarray_prod$] : ! [v2: % 58.77/8.72 Nat_a_iarray_prod$] : ! [v3: Nat_a_iarray_prod$] : (v1 = v0 | ~ % 58.77/8.72 (plus$l(v3, v2) = v1) | ~ (plus$l(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v2: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v3: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : (v1 = v0 | ~ (plus$k(v3, v2) = v1) | ~ % 58.77/8.72 (plus$k(v3, v2) = v0)) & ! [v0: Nat_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : ! [v2: Nat_a_b_vec_c_vec_prod$] : ! [v3: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (plus$j(v3, v2) = v1) | ~ % 58.77/8.72 (plus$j(v3, v2) = v0)) & ! [v0: A_nat_a_b_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_b_vec_c_vec_prod_prod$] : ! [v2: A_nat_a_b_vec_c_vec_prod_prod$] : % 58.77/8.72 ! [v3: A_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (plus$i(v3, v2) = v1) | % 58.77/8.72 ~ (plus$i(v3, v2) = v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: % 58.77/8.72 A_b_vec_c_vec$] : ! [v2: A_b_vec_c_vec$] : ! [v3: A_b_vec_c_vec$] : (v1 = % 58.77/8.72 v0 | ~ (plus$h(v3, v2) = v1) | ~ (plus$h(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: A_iarray_iarray$] : % 58.77/8.72 ! [v3: A_iarray_iarray$] : (v1 = v0 | ~ (plus$g(v3, v2) = v1) | ~ % 58.77/8.72 (plus$g(v3, v2) = v0)) & ! [v0: Nat_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.72 Nat_a_iarray_iarray_prod$] : ! [v2: Nat_a_iarray_iarray_prod$] : ! [v3: % 58.77/8.72 Nat_a_iarray_iarray_prod$] : (v1 = v0 | ~ (plus$f(v3, v2) = v1) | ~ % 58.77/8.72 (plus$f(v3, v2) = v0)) & ! [v0: A_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.72 A_a_iarray_iarray_prod$] : ! [v2: A_a_iarray_iarray_prod$] : ! [v3: % 58.77/8.72 A_a_iarray_iarray_prod$] : (v1 = v0 | ~ (plus$e(v3, v2) = v1) | ~ % 58.77/8.72 (plus$e(v3, v2) = v0)) & ! [v0: A_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.72 A_a_b_vec_c_vec_prod$] : ! [v2: A_a_b_vec_c_vec_prod$] : ! [v3: % 58.77/8.72 A_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (plus$d(v3, v2) = v1) | ~ % 58.77/8.72 (plus$d(v3, v2) = v0)) & ! [v0: B$] : ! [v1: B$] : ! [v2: B$] : ! [v3: % 58.77/8.72 B$] : (v1 = v0 | ~ (plus$c(v3, v2) = v1) | ~ (plus$c(v3, v2) = v0)) & ! % 58.77/8.72 [v0: C$] : ! [v1: C$] : ! [v2: C$] : ! [v3: C$] : (v1 = v0 | ~ (plus$b(v3, % 58.77/8.72 v2) = v1) | ~ (plus$b(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_b_vec_c_vec_prod_prod$] : ! [v1: A_nat_a_b_vec_c_vec_prod_prod$] : % 58.77/8.72 ! [v2: Nat$] : ! [v3: A_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$c(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$c(v3, v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: % 58.77/8.72 A_b_vec$] : ! [v2: C$] : ! [v3: C_a_b_vec_fun$] : (v1 = v0 | ~ % 58.77/8.72 (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_b_vec_b_vec_prod$] : ! [v1: Nat_a_b_vec_b_vec_prod$] : ! [v2: % 58.77/8.72 A_b_vec_b_vec$] : ! [v3: Nat$] : (v1 = v0 | ~ (pair$l(v3, v2) = v1) | ~ % 58.77/8.72 (pair$l(v3, v2) = v0)) & ! [v0: A_nat_a_b_vec_b_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_b_vec_b_vec_prod_prod$] : ! [v2: Nat_a_b_vec_b_vec_prod$] : ! [v3: % 58.77/8.72 A$] : (v1 = v0 | ~ (pair$k(v3, v2) = v1) | ~ (pair$k(v3, v2) = v0)) & ! % 58.77/8.72 [v0: A_nat_a_b_vec_b_vec_prod_prod$] : ! [v1: A_nat_a_b_vec_b_vec_prod_prod$] % 58.77/8.72 : ! [v2: Nat$] : ! [v3: A_nat_a_b_vec_b_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$b(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$b(v3, v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: % 58.77/8.72 A_b_vec$] : ! [v2: B$] : ! [v3: A_b_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.72 (vec_nth$e(v3, v2) = v1) | ~ (vec_nth$e(v3, v2) = v0)) & ! [v0: A$] : ! % 58.77/8.72 [v1: A$] : ! [v2: B$] : ! [v3: B_a_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) % 58.77/8.72 = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: Nat_a_c_vec_b_vec_prod$] : % 58.77/8.72 ! [v1: Nat_a_c_vec_b_vec_prod$] : ! [v2: A_c_vec_b_vec$] : ! [v3: Nat$] : % 58.77/8.72 (v1 = v0 | ~ (pair$j(v3, v2) = v1) | ~ (pair$j(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_c_vec_b_vec_prod_prod$] : ! [v1: A_nat_a_c_vec_b_vec_prod_prod$] : % 58.77/8.72 ! [v2: Nat_a_c_vec_b_vec_prod$] : ! [v3: A$] : (v1 = v0 | ~ (pair$i(v3, v2) % 58.77/8.72 = v1) | ~ (pair$i(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_c_vec_b_vec_prod_prod$] : ! [v1: A_nat_a_c_vec_b_vec_prod_prod$] : % 58.77/8.72 ! [v2: Nat$] : ! [v3: A_nat_a_c_vec_b_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$a(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 58.77/8.72 ! [v1: MultipleValueBool] : ! [v2: B$] : ! [v3: B$] : (v1 = v0 | ~ % 58.77/8.72 (less_eq$b(v3, v2) = v1) | ~ (less_eq$b(v3, v2) = v0)) & ! [v0: A_c_vec$] % 58.77/8.72 : ! [v1: A_c_vec$] : ! [v2: B$] : ! [v3: A_c_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.72 (vec_nth$d(v3, v2) = v1) | ~ (vec_nth$d(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_c_vec_c_vec_prod$] : ! [v1: Nat_a_c_vec_c_vec_prod$] : ! [v2: % 58.77/8.72 A_c_vec_c_vec$] : ! [v3: Nat$] : (v1 = v0 | ~ (pair$h(v3, v2) = v1) | ~ % 58.77/8.72 (pair$h(v3, v2) = v0)) & ! [v0: A_nat_a_c_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_c_vec_c_vec_prod_prod$] : ! [v2: Nat_a_c_vec_c_vec_prod$] : ! [v3: % 58.77/8.72 A$] : (v1 = v0 | ~ (pair$g(v3, v2) = v1) | ~ (pair$g(v3, v2) = v0)) & ! % 58.77/8.72 [v0: A_nat_a_c_vec_c_vec_prod_prod$] : ! [v1: A_nat_a_c_vec_c_vec_prod_prod$] % 58.77/8.72 : ! [v2: Nat$] : ! [v3: A_nat_a_c_vec_c_vec_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 58.77/8.72 ! [v1: MultipleValueBool] : ! [v2: C$] : ! [v3: C$] : (v1 = v0 | ~ % 58.77/8.72 (less_eq$(v3, v2) = v1) | ~ (less_eq$(v3, v2) = v0)) & ! [v0: A_c_vec$] : % 58.77/8.72 ! [v1: A_c_vec$] : ! [v2: C$] : ! [v3: A_c_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.72 (vec_nth$c(v3, v2) = v1) | ~ (vec_nth$c(v3, v2) = v0)) & ! [v0: A$] : ! % 58.77/8.72 [v1: A$] : ! [v2: C$] : ! [v3: A_c_vec$] : (v1 = v0 | ~ (vec_nth$b(v3, v2) % 58.77/8.72 = v1) | ~ (vec_nth$b(v3, v2) = v0)) & ! [v0: A_iarray$] : ! [v1: % 58.77/8.72 A_iarray$] : ! [v2: A_iarray_iarray$] : ! [v3: Nat$] : (v1 = v0 | ~ % 58.77/8.72 (column_iarray$(v3, v2) = v1) | ~ (column_iarray$(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : (v1 = v0 | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P_iarrays$(v3, v2) = v1) | ~ % 58.77/8.72 (gauss_Jordan_column_k_det_P_iarrays$(v3, v2) = v0)) & ! [v0: % 58.77/8.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, % 58.77/8.72 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 58.77/8.72 ! [v2: Nat_a_iarray_iarray_prod$] : ! [v3: % 58.77/8.72 Nat_a_iarray_iarray_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = v1) % 58.77/8.72 | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_nat_a_iarray_iarray_prod_prod$] : ! [v3: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$h(v3, % 58.77/8.72 v2) = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 58.77/8.72 ! [v1: MultipleValueBool] : ! [v2: Nat_a_iarray_prod$] : ! [v3: % 58.77/8.72 Nat_a_iarray_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) | ~ % 58.77/8.72 (fun_app$e(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: Nat_a_b_vec_c_vec_prod$] : ! [v3: % 58.77/8.72 Nat_a_b_vec_c_vec_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$g(v3, v2) = v1) | % 58.77/8.72 ~ (fun_app$g(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_nat_a_b_vec_c_vec_prod_prod$] : ! [v3: % 58.77/8.72 A_nat_a_b_vec_c_vec_prod_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) % 58.77/8.72 = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 58.77/8.72 [v2: int] : ! [v3: int] : (v1 = v0 | ~ (times$a(v3, v2) = v1) | ~ % 58.77/8.72 (times$a(v3, v2) = v0)) & ! [v0: A_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.72 A_a_iarray_iarray_prod$] : ! [v2: A_iarray_iarray$] : ! [v3: A$] : (v1 = % 58.77/8.72 v0 | ~ (pair$f(v3, v2) = v1) | ~ (pair$f(v3, v2) = v0)) & ! [v0: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : ! [v2: Nat_a_iarray_iarray_prod$] : ! % 58.77/8.72 [v3: A$] : (v1 = v0 | ~ (pair$c(v3, v2) = v1) | ~ (pair$c(v3, v2) = v0)) & % 58.77/8.72 ! [v0: A_nat_a_b_vec_c_vec_prod_prod$] : ! [v1: % 58.77/8.72 A_nat_a_b_vec_c_vec_prod_prod$] : ! [v2: Nat_a_b_vec_c_vec_prod$] : ! [v3: % 58.77/8.72 A$] : (v1 = v0 | ~ (pair$(v3, v2) = v1) | ~ (pair$(v3, v2) = v0)) & ! % 58.77/8.72 [v0: A_a_b_vec_c_vec_prod$] : ! [v1: A_a_b_vec_c_vec_prod$] : ! [v2: % 58.77/8.72 A_b_vec_c_vec$] : ! [v3: A$] : (v1 = v0 | ~ (pair$e(v3, v2) = v1) | ~ % 58.77/8.72 (pair$e(v3, v2) = v0)) & ! [v0: Nat_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.72 Nat_a_iarray_iarray_prod$] : ! [v2: A_iarray_iarray$] : ! [v3: Nat$] : (v1 % 58.77/8.72 = v0 | ~ (pair$d(v3, v2) = v1) | ~ (pair$d(v3, v2) = v0)) & ! [v0: % 58.77/8.72 Nat_a_iarray_prod$] : ! [v1: Nat_a_iarray_prod$] : ! [v2: A_iarray$] : ! % 58.77/8.72 [v3: Nat$] : (v1 = v0 | ~ (pair$b(v3, v2) = v1) | ~ (pair$b(v3, v2) = v0)) & % 58.77/8.72 ! [v0: Nat_a_b_vec_c_vec_prod$] : ! [v1: Nat_a_b_vec_c_vec_prod$] : ! [v2: % 58.77/8.72 A_b_vec_c_vec$] : ! [v3: Nat$] : (v1 = v0 | ~ (pair$a(v3, v2) = v1) | ~ % 58.77/8.72 (pair$a(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A$] : ! [v3: % 58.77/8.72 A_a_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = % 58.77/8.72 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat$] : ! [v3: % 58.77/8.72 Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, % 58.77/8.72 v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: % 58.77/8.72 Int_int_fun$] : (v1 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) % 58.77/8.72 = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: % 58.77/8.72 A_b_vec_c_vec_c_vec$] : (v1 = v0 | ~ (upper_triangular_upt_k$a(v2) = v1) | % 58.77/8.72 ~ (upper_triangular_upt_k$a(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 58.77/8.72 Nat_bool_fun$] : ! [v2: A_b_vec_b_vec$] : (v1 = v0 | ~ % 58.77/8.72 (upper_triangular_upt_k$(v2) = v1) | ~ (upper_triangular_upt_k$(v2) = v0)) % 58.77/8.72 & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: C$] : (v1 = v0 | ~ (to_nat$(v2) = % 58.77/8.72 v1) | ~ (to_nat$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: B$] % 58.77/8.72 : (v1 = v0 | ~ (to_nat$a(v2) = v1) | ~ (to_nat$a(v2) = v0)) & ! [v0: % 58.77/8.72 A_c_vec_c_vec$] : ! [v1: A_c_vec_c_vec$] : ! [v2: % 58.77/8.72 A_c_vec_c_vec_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (fst$x(v2) = v1) | ~ % 58.77/8.72 (fst$x(v2) = v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! % 58.77/8.72 [v2: A_c_vec_c_vec_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$x(v2) = v1) | ~ % 58.77/8.72 (snd$x(v2) = v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: A_c_vec_c_vec$] : ! % 58.77/8.72 [v2: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (fst$w(v2) = % 58.77/8.72 v1) | ~ (fst$w(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec$] : ! [v2: A_b_vec_b_vec_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (fst$v(v2) = v1) | ~ (fst$v(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec$] : ! [v2: A_b_vec_b_vec_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (snd$w(v2) = v1) | ~ (snd$w(v2) = v0)) & ! [v0: Nat_a_b_vec_b_vec_prod$] : % 58.77/8.72 ! [v1: Nat_a_b_vec_b_vec_prod$] : ! [v2: % 58.77/8.72 A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (snd$v(v2) = v1) % 58.77/8.72 | ~ (snd$v(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : % 58.77/8.72 ! [v2: A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (fst$u(v2) % 58.77/8.72 = v1) | ~ (fst$u(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 58.77/8.72 A_b_vec_b_vec$] : ! [v2: A_b_vec_b_vec_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (fst$t(v2) = v1) | ~ (fst$t(v2) = v0)) & ! [v0: A_c_vec_b_vec$] : ! [v1: % 58.77/8.72 A_c_vec_b_vec$] : ! [v2: A_b_vec_b_vec_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (snd$u(v2) = v1) | ~ (snd$u(v2) = v0)) & ! [v0: Nat_a_c_vec_b_vec_prod$] : % 58.77/8.72 ! [v1: Nat_a_c_vec_b_vec_prod$] : ! [v2: % 58.77/8.72 A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (snd$t(v2) = v1) % 58.77/8.72 | ~ (snd$t(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : % 58.77/8.72 ! [v2: A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (fst$s(v2) % 58.77/8.72 = v1) | ~ (fst$s(v2) = v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec$] : ! [v2: A_c_vec_c_vec_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (fst$r(v2) = v1) | ~ (fst$r(v2) = v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: % 58.77/8.72 A_c_vec_c_vec$] : ! [v2: A_c_vec_c_vec_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (snd$s(v2) = v1) | ~ (snd$s(v2) = v0)) & ! [v0: Nat_a_c_vec_c_vec_prod$] : % 58.77/8.72 ! [v1: Nat_a_c_vec_c_vec_prod$] : ! [v2: % 58.77/8.72 A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (snd$r(v2) = v1) % 58.77/8.72 | ~ (snd$r(v2) = v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: A_c_vec_c_vec$] : % 58.77/8.72 ! [v2: A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (fst$q(v2) % 58.77/8.72 = v1) | ~ (fst$q(v2) = v0)) & ! [v0: Nat_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : ! [v2: % 58.77/8.72 A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (snd$q(v2) = v1) % 58.77/8.72 | ~ (snd$q(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 58.77/8.72 MultipleValueBool] : ! [v2: A_b_vec_c_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.72 (upper_triangular$a(v2) = v1) | ~ (upper_triangular$a(v2) = v0)) & ! [v0: % 58.77/8.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_b_vec_b_vec$] : % 58.77/8.72 (v1 = v0 | ~ (upper_triangular$(v2) = v1) | ~ (upper_triangular$(v2) = v0)) % 58.77/8.72 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 58.77/8.72 Int_int_prod$] : (v1 = v0 | ~ (divides_aux$(v2) = v1) | ~ % 58.77/8.72 (divides_aux$(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 58.77/8.72 Int_int_prod$] : (v1 = v0 | ~ (fst$p(v2) = v1) | ~ (fst$p(v2) = v0)) & ! % 58.77/8.72 [v0: int] : ! [v1: int] : ! [v2: Int_int_prod$] : (v1 = v0 | ~ (snd$p(v2) = % 58.77/8.72 v1) | ~ (snd$p(v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: % 58.77/8.72 A_iarray_iarray$] : ! [v2: A_b_vec_c_vec$] : (v1 = v0 | ~ % 58.77/8.72 (matrix_to_iarray$(v2) = v1) | ~ (matrix_to_iarray$(v2) = v0)) & ! [v0: % 58.77/8.72 C_a_b_vec_fun$] : ! [v1: C_a_b_vec_fun$] : ! [v2: A_b_vec_c_vec$] : (v1 = % 58.77/8.72 v0 | ~ (vec_nth$a(v2) = v1) | ~ (vec_nth$a(v2) = v0)) & ! [v0: A$] : ! % 58.77/8.72 [v1: A$] : ! [v2: A_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ (fst$o(v2) = v1) | % 58.77/8.72 ~ (fst$o(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! % 58.77/8.72 [v2: A_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ (snd$o(v2) = v1) | ~ (snd$o(v2) = % 58.77/8.72 v0)) & ! [v0: Nat_a_b_vec_b_vec_prod$] : ! [v1: Nat_a_b_vec_b_vec_prod$] % 58.77/8.72 : ! [v2: A_nat_a_b_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (snd$m(v2) = v1) | % 58.77/8.72 ~ (snd$m(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ (fst$m(v2) = v1) | ~ (fst$m(v2) = % 58.77/8.72 v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_b_vec_prod$] : (v1 = v0 | ~ (snd$n(v2) = v1) | ~ (snd$n(v2) = % 58.77/8.72 v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_nat_a_b_vec_b_vec_prod_prod$] % 58.77/8.72 : (v1 = v0 | ~ (fst$n(v2) = v1) | ~ (fst$n(v2) = v0)) & ! [v0: Nat$] : ! % 58.77/8.72 [v1: Nat$] : ! [v2: A_b_vec_b_vec$] : (v1 = v0 | ~ (nrows$c(v2) = v1) | ~ % 58.77/8.72 (nrows$c(v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: % 58.77/8.72 A_b_vec$] : (v1 = v0 | ~ (vec_nth$(v2) = v1) | ~ (vec_nth$(v2) = v0)) & ! % 58.77/8.72 [v0: A$] : ! [v1: A$] : ! [v2: A_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ % 58.77/8.72 (fst$l(v2) = v1) | ~ (fst$l(v2) = v0)) & ! [v0: A_c_vec_b_vec$] : ! [v1: % 58.77/8.72 A_c_vec_b_vec$] : ! [v2: A_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ (snd$l(v2) % 58.77/8.72 = v1) | ~ (snd$l(v2) = v0)) & ! [v0: Nat_a_c_vec_b_vec_prod$] : ! [v1: % 58.77/8.72 Nat_a_c_vec_b_vec_prod$] : ! [v2: A_nat_a_c_vec_b_vec_prod_prod$] : (v1 = % 58.77/8.72 v0 | ~ (snd$j(v2) = v1) | ~ (snd$j(v2) = v0)) & ! [v0: Nat$] : ! [v1: % 58.77/8.72 Nat$] : ! [v2: Nat_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ (fst$j(v2) = v1) | % 58.77/8.72 ~ (fst$j(v2) = v0)) & ! [v0: A_c_vec_b_vec$] : ! [v1: A_c_vec_b_vec$] : ! % 58.77/8.72 [v2: Nat_a_c_vec_b_vec_prod$] : (v1 = v0 | ~ (snd$k(v2) = v1) | ~ (snd$k(v2) % 58.77/8.72 = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 58.77/8.72 A_nat_a_c_vec_b_vec_prod_prod$] : (v1 = v0 | ~ (fst$k(v2) = v1) | ~ % 58.77/8.72 (fst$k(v2) = v0)) & ! [v0: B$] : ! [v1: B$] : ! [v2: Nat$] : (v1 = v0 | % 58.77/8.72 ~ (from_nat$a(v2) = v1) | ~ (from_nat$a(v2) = v0)) & ! [v0: Nat$] : ! % 58.77/8.72 [v1: Nat$] : ! [v2: A_c_vec_b_vec$] : (v1 = v0 | ~ (nrows$b(v2) = v1) | ~ % 58.77/8.72 (nrows$b(v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 58.77/8.72 A_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ (fst$i(v2) = v1) | ~ (fst$i(v2) = % 58.77/8.72 v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: A_c_vec_c_vec$] : ! [v2: % 58.77/8.72 A_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$i(v2) = v1) | ~ (snd$i(v2) = % 58.77/8.72 v0)) & ! [v0: Nat_a_c_vec_c_vec_prod$] : ! [v1: Nat_a_c_vec_c_vec_prod$] % 58.77/8.72 : ! [v2: A_nat_a_c_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (snd$g(v2) = v1) | % 58.77/8.72 ~ (snd$g(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 58.77/8.72 Nat_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ (fst$g(v2) = v1) | ~ (fst$g(v2) = % 58.77/8.72 v0)) & ! [v0: A_c_vec_c_vec$] : ! [v1: A_c_vec_c_vec$] : ! [v2: % 58.77/8.72 Nat_a_c_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$h(v2) = v1) | ~ (snd$h(v2) = % 58.77/8.72 v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_nat_a_c_vec_c_vec_prod_prod$] % 58.77/8.72 : (v1 = v0 | ~ (fst$h(v2) = v1) | ~ (fst$h(v2) = v0)) & ! [v0: C$] : ! % 58.77/8.72 [v1: C$] : ! [v2: Nat$] : (v1 = v0 | ~ (from_nat$(v2) = v1) | ~ % 58.77/8.72 (from_nat$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 58.77/8.72 A_c_vec_c_vec$] : (v1 = v0 | ~ (nrows$a(v2) = v1) | ~ (nrows$a(v2) = v0)) % 58.77/8.72 & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : (v1 = v0 | ~ (nat$(v2) = v1) % 58.77/8.72 | ~ (nat$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 58.77/8.72 A_iarray_iarray$] : (v1 = v0 | ~ (nrows_iarray$(v2) = v1) | ~ % 58.77/8.72 (nrows_iarray$(v2) = v0)) & ! [v0: Nat_nat_fun$] : ! [v1: Nat_nat_fun$] : % 58.77/8.72 ! [v2: Nat$] : (v1 = v0 | ~ (plus$a(v2) = v1) | ~ (plus$a(v2) = v0)) & ! % 58.77/8.72 [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ % 58.77/8.72 (less_eq$a(v2) = v1) | ~ (less_eq$a(v2) = v0)) & ! [v0: Nat_bool_fun$] : % 58.77/8.72 ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ (less$(v2) = v1) | ~ % 58.77/8.72 (less$(v2) = v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : % 58.77/8.72 (v1 = v0 | ~ (plus$(v2) = v1) | ~ (plus$(v2) = v0)) & ! [v0: Nat_nat_fun$] % 58.77/8.72 : ! [v1: Nat_nat_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ (times$b(v2) = v1) | % 58.77/8.72 ~ (times$b(v2) = v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] % 58.77/8.72 : (v1 = v0 | ~ (times$(v2) = v1) | ~ (times$(v2) = v0)) & ! [v0: A$] : ! % 58.77/8.72 [v1: A$] : ! [v2: A_a_iarray_iarray_prod$] : (v1 = v0 | ~ (fst$a(v2) = v1) | % 58.77/8.72 ~ (fst$a(v2) = v0)) & ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] % 58.77/8.72 : ! [v2: A_a_iarray_iarray_prod$] : (v1 = v0 | ~ (snd$e(v2) = v1) | ~ % 58.77/8.72 (snd$e(v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 58.77/8.72 A_nat_a_iarray_iarray_prod_prod$] : (v1 = v0 | ~ (fst$f(v2) = v1) | ~ % 58.77/8.72 (fst$f(v2) = v0)) & ! [v0: Nat_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.72 Nat_a_iarray_iarray_prod$] : ! [v2: A_nat_a_iarray_iarray_prod_prod$] : (v1 % 58.77/8.72 = v0 | ~ (snd$d(v2) = v1) | ~ (snd$d(v2) = v0)) & ! [v0: A$] : ! [v1: % 58.77/8.72 A$] : ! [v2: A_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (fst$e(v2) = % 58.77/8.72 v1) | ~ (fst$e(v2) = v0)) & ! [v0: Nat_a_b_vec_c_vec_prod$] : ! [v1: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : ! [v2: A_nat_a_b_vec_c_vec_prod_prod$] : (v1 = % 58.77/8.72 v0 | ~ (snd$a(v2) = v1) | ~ (snd$a(v2) = v0)) & ! [v0: A$] : ! [v1: A$] % 58.77/8.72 : ! [v2: A_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (fst$(v2) = v1) | ~ % 58.77/8.72 (fst$(v2) = v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! % 58.77/8.72 [v2: A_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$b(v2) = v1) | ~ (snd$b(v2) = % 58.77/8.72 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_a_iarray_iarray_prod$] % 58.77/8.72 : (v1 = v0 | ~ (fst$d(v2) = v1) | ~ (fst$d(v2) = v0)) & ! [v0: % 58.77/8.72 A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 58.77/8.72 Nat_a_iarray_iarray_prod$] : (v1 = v0 | ~ (snd$c(v2) = v1) | ~ (snd$c(v2) % 58.77/8.72 = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_a_iarray_prod$] : (v1 % 58.77/8.72 = v0 | ~ (fst$c(v2) = v1) | ~ (fst$c(v2) = v0)) & ! [v0: A_iarray$] : ! % 58.77/8.72 [v1: A_iarray$] : ! [v2: Nat_a_iarray_prod$] : (v1 = v0 | ~ (snd$f(v2) = v1) % 58.77/8.72 | ~ (snd$f(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (fst$b(v2) = v1) | ~ (fst$b(v2) = % 58.77/8.72 v0)) & ! [v0: A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! [v2: % 58.77/8.72 Nat_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$(v2) = v1) | ~ (snd$(v2) = % 58.77/8.72 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_b_vec_c_vec$] : (v1 = v0 % 58.77/8.72 | ~ (ncols$(v2) = v1) | ~ (ncols$(v2) = v0)) & ! [v0: Nat$] : ! [v1: % 58.77/8.72 Nat$] : ! [v2: A_b_vec_c_vec$] : (v1 = v0 | ~ (nrows$(v2) = v1) | ~ % 58.77/8.72 (nrows$(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : (v1 = v0 % 58.77/8.72 | ~ (of_nat$(v2) = v1) | ~ (of_nat$(v2) = v0)) % 58.77/8.72 % 58.77/8.72 Further assumptions not needed in the proof: % 58.77/8.72 -------------------------------------------- % 58.77/8.73 axiom0, axiom1, axiom100, axiom101, axiom102, axiom103, axiom104, axiom105, % 58.77/8.73 axiom106, axiom107, axiom108, axiom109, axiom110, axiom111, axiom112, axiom113, % 58.77/8.73 axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, axiom12, axiom120, % 58.77/8.73 axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, axiom128, % 58.77/8.73 axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, axiom135, % 58.77/8.73 axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, axiom142, % 58.77/8.73 axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, % 58.77/8.73 axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, % 58.77/8.73 axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, axiom164, % 58.77/8.73 axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, % 58.77/8.73 axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom179, % 58.77/8.73 axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, % 58.77/8.73 axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 58.77/8.73 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 58.77/8.73 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 58.77/8.73 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 58.77/8.73 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 58.77/8.73 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 58.77/8.73 axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, % 58.77/8.73 axiom237, axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, % 58.77/8.73 axiom244, axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, % 58.77/8.73 axiom251, axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, % 58.77/8.73 axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, % 58.77/8.73 axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, axiom272, axiom274, % 58.77/8.73 axiom277, axiom278, axiom279, axiom28, axiom280, axiom281, axiom282, axiom283, % 58.77/8.73 axiom284, axiom285, axiom286, axiom287, axiom288, axiom289, axiom29, axiom290, % 58.77/8.73 axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, axiom297, axiom298, % 58.77/8.73 axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, axiom303, axiom304, % 58.77/8.73 axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, axiom310, axiom311, % 58.77/8.73 axiom312, axiom313, axiom314, axiom315, axiom316, axiom317, axiom318, axiom319, % 58.77/8.73 axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, axiom325, axiom326, % 58.77/8.73 axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, axiom332, axiom333, % 58.77/8.73 axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, axiom340, % 58.77/8.73 axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, axiom348, % 58.77/8.73 axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, % 58.77/8.73 axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, axiom362, % 58.77/8.73 axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, % 58.77/8.73 axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, % 58.77/8.73 axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, % 58.77/8.73 axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, axiom391, % 58.77/8.73 axiom392, axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, % 58.77/8.73 axiom4, axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, % 58.77/8.73 axiom406, axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, % 58.77/8.73 axiom413, axiom414, axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, % 58.77/8.73 axiom420, axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, % 58.77/8.73 axiom428, axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, % 58.77/8.73 axiom435, axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, % 58.77/8.73 axiom442, axiom443, axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, % 58.77/8.73 axiom45, axiom450, axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, % 58.77/8.73 axiom457, axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, % 58.77/8.73 axiom464, axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, % 58.77/8.73 axiom471, axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, % 58.77/8.73 axiom479, axiom48, axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, % 58.77/8.73 axiom486, axiom487, axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, % 58.77/8.73 axiom493, axiom494, axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, % 58.77/8.73 axiom50, axiom500, axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, % 58.77/8.73 axiom508, axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, axiom514, % 58.77/8.73 axiom515, axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, axiom521, % 58.77/8.73 axiom522, axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, axiom529, % 58.77/8.73 axiom53, axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, % 58.77/8.73 axiom537, axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, % 58.77/8.73 axiom544, axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, % 58.77/8.73 axiom551, axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, % 58.77/8.73 axiom559, axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, % 58.77/8.73 axiom566, axiom567, axiom568, axiom569, axiom57, axiom570, axiom572, axiom573, % 58.77/8.73 axiom574, axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, % 58.77/8.73 axiom581, axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, % 58.77/8.73 axiom589, axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, % 58.77/8.73 axiom596, axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, % 58.77/8.73 axiom602, axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, % 58.77/8.73 axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, % 58.77/8.73 axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, % 58.77/8.73 axiom624, axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, % 58.77/8.73 axiom631, axiom632, axiom64, axiom65, axiom66, axiom67, axiom68, axiom69, % 58.77/8.73 axiom7, axiom70, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, % 58.77/8.73 axiom78, axiom79, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, % 58.77/8.73 axiom87, axiom88, axiom89, axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, % 58.77/8.73 axiom96, axiom97, axiom98, axiom99, formula_634, formula_635 % 58.77/8.73 % 58.77/8.73 Those formulas are unsatisfiable: % 58.77/8.73 --------------------------------- % 58.77/8.73 % 58.77/8.73 Begin of proof % 58.77/8.73 | % 58.77/8.73 | ALPHA: (axiom9) implies: % 58.77/8.73 | (1) ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : ($lesseq(v2, v1) & % 58.77/8.73 | nrows$(a$) = v0 & of_nat$(v0) = v1 & of_nat$(i$) = v2 & Nat$(v0)) % 58.77/8.73 | % 58.77/8.73 | ALPHA: (axiom10) implies: % 58.77/8.73 | (2) ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : ($lesseq(v1, v2) & % 58.77/8.73 | nrows$(a$) = v0 & of_nat$(v0) = v1 & of_nat$(i$) = v2 & Nat$(v0)) % 58.77/8.73 | % 58.77/8.73 | ALPHA: (axiom11) implies: % 58.77/8.73 | (3) ? [v0: Nat$] : ? [v1: int] : ? [v2: int] : ($lesseq(1, % 58.77/8.73 | $difference(v1, v2)) & ncols$(a$) = v0 & of_nat$(v0) = v1 & % 58.77/8.73 | of_nat$(k$) = v2 & Nat$(v0)) % 58.77/8.73 | % 58.77/8.73 | ALPHA: (conjecture8) implies: % 58.77/8.73 | (4) A_b_vec_c_vec$(a$) % 58.77/8.73 | (5) Nat$(i$) % 58.77/8.74 | (6) Nat$(k$) % 58.77/8.74 | (7) A$(n$) % 58.77/8.74 | (8) ? [v0: C$] : ? [v1: C_a_b_vec_fun$] : ? [v2: B$] : ? [v3: int] : ? % 58.77/8.74 | [v4: Nat$] : ? [v5: int] : ? [v6: A_iarray_iarray$] : ? [v7: % 58.77/8.74 | A_iarray$] : ? [v8: Nat_a_iarray_prod$] : ? [v9: any] : ? [v10: % 58.77/8.74 | Nat$] : ? [v11: int] : ? [v12: Nat_a_b_vec_c_vec_prod$] : ? [v13: % 58.77/8.74 | A_nat_a_b_vec_c_vec_prod_prod$] : ? [v14: Nat_a_b_vec_c_vec_prod$] : % 58.77/8.74 | ? [v15: A_b_vec_c_vec$] : ? [v16: A_iarray_iarray$] : ? [v17: % 58.77/8.74 | Nat_a_iarray_iarray_prod$] : ? [v18: % 58.77/8.74 | A_nat_a_iarray_iarray_prod_prod$] : ? [v19: % 58.77/8.74 | Nat_a_iarray_iarray_prod$] : ? [v20: A_iarray_iarray$] : ? [v21: % 58.77/8.74 | A_a_iarray_iarray_prod$] : ? [v22: A$] : ? [v23: A_a_fun$] : ? % 58.77/8.74 | [v24: A$] : ? [v25: Nat$] : ? [v26: A_iarray_iarray$] : ? [v27: % 58.77/8.74 | Nat_a_iarray_iarray_prod$] : ? [v28: % 58.77/8.74 | A_nat_a_iarray_iarray_prod_prod$] : ? [v29: % 58.77/8.74 | Nat_a_iarray_iarray_prod$] : ? [v30: A_iarray_iarray$] : ? [v31: % 58.77/8.74 | A_a_b_vec_c_vec_prod$] : ? [v32: A$] : ? [v33: A_a_fun$] : ? [v34: % 58.77/8.74 | A$] : ? [v35: A_b_vec_c_vec$] : ? [v36: Nat_a_b_vec_c_vec_prod$] : % 58.77/8.74 | ? [v37: A_nat_a_b_vec_c_vec_prod_prod$] : ? [v38: % 58.77/8.74 | Nat_a_b_vec_c_vec_prod$] : ? [v39: A_b_vec_c_vec$] : ? [v40: % 58.77/8.74 | A_iarray_iarray$] : (matrix_to_iarray$(v39) = v40 & % 58.77/8.74 | matrix_to_iarray$(v15) = v16 & matrix_to_iarray$(a$) = v6 & % 58.77/8.74 | gauss_Jordan_in_ij_det_P$(a$, v0, v2) = v31 & vec_nth$a(a$) = v1 & % 58.77/8.74 | from_nat$a(k$) = v2 & from_nat$(i$) = v0 & % 58.77/8.74 | gauss_Jordan_in_ij_det_P_iarrays$(v6, i$, k$) = v21 & nat$($sum(v3, % 58.77/8.74 | 1)) = v25 & column_iarray$(k$, v6) = v7 & nrows_iarray$(v6) = v10 % 58.77/8.74 | & fun_app$e(vector_all_zero_from_index$, v8) = v9 & times$(v32) = v33 % 58.77/8.74 | & times$(v22) = v23 & fst$a(v21) = v22 & snd$e(v21) = v26 & % 58.77/8.74 | snd$d(v28) = v29 & snd$d(v18) = v19 & pair$c(v24, v27) = v28 & % 58.77/8.74 | pair$c(n$, v17) = v18 & snd$a(v37) = v38 & snd$a(v13) = v14 & % 58.77/8.74 | pair$(v34, v36) = v37 & pair$(n$, v12) = v13 & fst$(v31) = v32 & % 58.77/8.74 | snd$b(v31) = v35 & snd$c(v29) = v30 & snd$c(v19) = v20 & pair$d(v25, % 58.77/8.74 | v26) = v27 & pair$d(i$, v6) = v17 & pair$b(i$, v7) = v8 & snd$(v38) % 58.77/8.74 | = v39 & snd$(v14) = v15 & pair$a(v25, v35) = v36 & pair$a(i$, a$) = % 58.77/8.74 | v12 & nrows$(a$) = v4 & of_nat$(v10) = v11 & of_nat$(v4) = v5 & % 58.77/8.74 | of_nat$(i$) = v3 & fun_app$b(v33, n$) = v34 & fun_app$b(v23, n$) = % 58.77/8.74 | v24 & Nat_a_iarray_prod$(v8) & A_iarray$(v7) & A_a_fun$(v33) & % 58.77/8.74 | A_a_fun$(v23) & Nat_a_b_vec_c_vec_prod$(v38) & % 58.77/8.74 | Nat_a_b_vec_c_vec_prod$(v36) & Nat_a_b_vec_c_vec_prod$(v14) & % 58.77/8.74 | Nat_a_b_vec_c_vec_prod$(v12) & A$(v34) & A$(v32) & A$(v24) & A$(v22) % 58.77/8.74 | & Nat_a_iarray_iarray_prod$(v29) & Nat_a_iarray_iarray_prod$(v27) & % 58.77/8.74 | Nat_a_iarray_iarray_prod$(v19) & Nat_a_iarray_iarray_prod$(v17) & % 58.77/8.74 | A_a_b_vec_c_vec_prod$(v31) & Nat$(v25) & Nat$(v10) & Nat$(v4) & % 58.77/8.74 | C$(v0) & C_a_b_vec_fun$(v1) & A_b_vec_c_vec$(v39) & % 58.77/8.74 | A_b_vec_c_vec$(v35) & A_b_vec_c_vec$(v15) & B$(v2) & % 58.77/8.74 | A_a_iarray_iarray_prod$(v21) & A_iarray_iarray$(v40) & % 58.77/8.74 | A_iarray_iarray$(v30) & A_iarray_iarray$(v26) & A_iarray_iarray$(v20) % 58.77/8.74 | & A_iarray_iarray$(v16) & A_iarray_iarray$(v6) & % 58.77/8.74 | A_nat_a_iarray_iarray_prod_prod$(v28) & % 58.77/8.74 | A_nat_a_iarray_iarray_prod_prod$(v18) & % 58.77/8.74 | A_nat_a_b_vec_c_vec_prod_prod$(v37) & % 58.77/8.74 | A_nat_a_b_vec_c_vec_prod_prod$(v13) & (( ~ (v5 = v3) & ? [v41: C$] : % 58.77/8.74 | ? [v42: A_b_vec$] : ? [v43: B_a_fun$] : ? [v44: A$] : ( ~ (v44 % 58.77/8.74 | = zero$a) & fun_app$d(v1, v41) = v42 & vec_nth$(v42) = v43 & % 58.77/8.74 | fun_app$c(v43, v2) = v44 & less_eq$(v0, v41) = 0 & A$(v44) & % 58.77/8.74 | B_a_fun$(v43) & A_b_vec$(v42) & C$(v41)) & (( ~ (v40 = v30) & % 58.77/8.74 | ~ (v11 = v3) & ~ (v9 = 0)) | ( ~ (v40 = v20) & (v11 = v3 | % 58.77/8.74 | v9 = 0)))) | ((v5 = v3 | ! [v41: C$] : ( ~ (less_eq$(v0, % 58.77/8.74 | v41) = 0) | ~ C$(v41) | ? [v42: A_b_vec$] : ? [v43: % 58.77/8.74 | B_a_fun$] : (fun_app$d(v1, v41) = v42 & vec_nth$(v42) = v43 % 58.77/8.74 | & fun_app$c(v43, v2) = zero$a & B_a_fun$(v43) & % 58.77/8.74 | A_b_vec$(v42)))) & (( ~ (v30 = v16) & ~ (v11 = v3) & ~ % 58.77/8.74 | (v9 = 0)) | ( ~ (v20 = v16) & (v11 = v3 | v9 = 0)))))) % 58.77/8.74 | % 58.77/8.74 | ALPHA: (function-axioms) implies: % 58.77/8.74 | (9) ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : (v1 = v0 | ~ % 58.77/8.74 | (of_nat$(v2) = v1) | ~ (of_nat$(v2) = v0)) % 58.77/8.74 | (10) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_b_vec_c_vec$] : (v1 = v0 | % 58.77/8.74 | ~ (nrows$(v2) = v1) | ~ (nrows$(v2) = v0)) % 58.77/8.74 | (11) ! [v0: A_b_vec_c_vec$] : ! [v1: A_b_vec_c_vec$] : ! [v2: % 58.77/8.74 | Nat_a_b_vec_c_vec_prod$] : (v1 = v0 | ~ (snd$(v2) = v1) | ~ % 58.77/8.74 | (snd$(v2) = v0)) % 58.77/8.74 | (12) ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 58.77/8.74 | Nat_a_iarray_iarray_prod$] : (v1 = v0 | ~ (snd$c(v2) = v1) | ~ % 58.77/8.74 | (snd$c(v2) = v0)) % 58.77/8.75 | (13) ! [v0: Nat_a_b_vec_c_vec_prod$] : ! [v1: Nat_a_b_vec_c_vec_prod$] : % 58.77/8.75 | ! [v2: A_nat_a_b_vec_c_vec_prod_prod$] : (v1 = v0 | ~ (snd$a(v2) = % 58.77/8.75 | v1) | ~ (snd$a(v2) = v0)) % 58.77/8.75 | (14) ! [v0: Nat_a_iarray_iarray_prod$] : ! [v1: % 58.77/8.75 | Nat_a_iarray_iarray_prod$] : ! [v2: % 58.77/8.75 | A_nat_a_iarray_iarray_prod_prod$] : (v1 = v0 | ~ (snd$d(v2) = v1) | % 58.77/8.75 | ~ (snd$d(v2) = v0)) % 58.77/8.75 | (15) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_iarray_iarray$] : (v1 = v0 | % 58.77/8.75 | ~ (nrows_iarray$(v2) = v1) | ~ (nrows_iarray$(v2) = v0)) % 58.77/8.75 | (16) ! [v0: A_iarray_iarray$] : ! [v1: A_iarray_iarray$] : ! [v2: % 58.77/8.75 | A_b_vec_c_vec$] : (v1 = v0 | ~ (matrix_to_iarray$(v2) = v1) | ~ % 58.77/8.75 | (matrix_to_iarray$(v2) = v0)) % 58.77/8.75 | % 58.77/8.75 | DELTA: instantiating (3) with fresh symbols all_559_0, all_559_1, all_559_2 % 58.77/8.75 | gives: % 58.77/8.75 | (17) $lesseq(1, $difference(all_559_1, all_559_0)) & ncols$(a$) = all_559_2 % 58.77/8.75 | & of_nat$(all_559_2) = all_559_1 & of_nat$(k$) = all_559_0 & % 58.77/8.75 | Nat$(all_559_2) % 58.77/8.75 | % 58.77/8.75 | ALPHA: (17) implies: % 58.77/8.75 | (18) $lesseq(1, $difference(all_559_1, all_559_0)) % 58.77/8.75 | (19) Nat$(all_559_2) % 58.77/8.75 | (20) of_nat$(k$) = all_559_0 % 58.77/8.75 | (21) of_nat$(all_559_2) = all_559_1 % 58.77/8.75 | % 58.77/8.75 | DELTA: instantiating (2) with fresh symbols all_562_0, all_562_1, all_562_2 % 58.77/8.75 | gives: % 58.77/8.75 | (22) $lesseq(all_562_1, all_562_0) & nrows$(a$) = all_562_2 & % 58.77/8.75 | of_nat$(all_562_2) = all_562_1 & of_nat$(i$) = all_562_0 & % 58.77/8.75 | Nat$(all_562_2) % 58.77/8.75 | % 58.77/8.75 | ALPHA: (22) implies: % 58.77/8.75 | (23) $lesseq(all_562_1, all_562_0) % 58.77/8.75 | (24) of_nat$(i$) = all_562_0 % 58.77/8.75 | (25) of_nat$(all_562_2) = all_562_1 % 58.77/8.75 | (26) nrows$(a$) = all_562_2 % 58.77/8.75 | % 58.77/8.75 | DELTA: instantiating (1) with fresh symbols all_589_0, all_589_1, all_589_2 % 58.77/8.75 | gives: % 58.77/8.75 | (27) $lesseq(all_589_0, all_589_1) & nrows$(a$) = all_589_2 & % 58.77/8.75 | of_nat$(all_589_2) = all_589_1 & of_nat$(i$) = all_589_0 & % 58.77/8.75 | Nat$(all_589_2) % 58.77/8.75 | % 58.77/8.75 | ALPHA: (27) implies: % 58.77/8.75 | (28) $lesseq(all_589_0, all_589_1) % 58.77/8.75 | (29) of_nat$(i$) = all_589_0 % 58.77/8.75 | (30) of_nat$(all_589_2) = all_589_1 % 58.77/8.75 | (31) nrows$(a$) = all_589_2 % 58.77/8.75 | % 58.77/8.75 | DELTA: instantiating (8) with fresh symbols all_754_0, all_754_1, all_754_2, % 58.77/8.75 | all_754_3, all_754_4, all_754_5, all_754_6, all_754_7, all_754_8, % 58.77/8.75 | all_754_9, all_754_10, all_754_11, all_754_12, all_754_13, all_754_14, % 58.77/8.75 | all_754_15, all_754_16, all_754_17, all_754_18, all_754_19, all_754_20, % 58.77/8.75 | all_754_21, all_754_22, all_754_23, all_754_24, all_754_25, all_754_26, % 58.77/8.75 | all_754_27, all_754_28, all_754_29, all_754_30, all_754_31, all_754_32, % 58.77/8.75 | all_754_33, all_754_34, all_754_35, all_754_36, all_754_37, all_754_38, % 58.77/8.75 | all_754_39, all_754_40 gives: % 58.77/8.76 | (32) matrix_to_iarray$(all_754_1) = all_754_0 & % 58.77/8.76 | matrix_to_iarray$(all_754_25) = all_754_24 & matrix_to_iarray$(a$) = % 58.77/8.76 | all_754_34 & gauss_Jordan_in_ij_det_P$(a$, all_754_40, all_754_38) = % 58.77/8.76 | all_754_9 & vec_nth$a(a$) = all_754_39 & from_nat$a(k$) = all_754_38 & % 58.77/8.76 | from_nat$(i$) = all_754_40 & % 58.77/8.76 | gauss_Jordan_in_ij_det_P_iarrays$(all_754_34, i$, k$) = all_754_19 & % 58.77/8.76 | nat$($sum(all_754_37, 1)) = all_754_15 & column_iarray$(k$, % 58.77/8.76 | all_754_34) = all_754_33 & nrows_iarray$(all_754_34) = all_754_30 & % 58.77/8.76 | fun_app$e(vector_all_zero_from_index$, all_754_32) = all_754_31 & % 58.77/8.76 | times$(all_754_8) = all_754_7 & times$(all_754_18) = all_754_17 & % 58.77/8.76 | fst$a(all_754_19) = all_754_18 & snd$e(all_754_19) = all_754_14 & % 58.77/8.76 | snd$d(all_754_12) = all_754_11 & snd$d(all_754_22) = all_754_21 & % 58.77/8.76 | pair$c(all_754_16, all_754_13) = all_754_12 & pair$c(n$, all_754_23) = % 58.77/8.76 | all_754_22 & snd$a(all_754_3) = all_754_2 & snd$a(all_754_27) = % 58.77/8.76 | all_754_26 & pair$(all_754_6, all_754_4) = all_754_3 & pair$(n$, % 58.77/8.76 | all_754_28) = all_754_27 & fst$(all_754_9) = all_754_8 & % 58.77/8.76 | snd$b(all_754_9) = all_754_5 & snd$c(all_754_11) = all_754_10 & % 58.77/8.76 | snd$c(all_754_21) = all_754_20 & pair$d(all_754_15, all_754_14) = % 58.77/8.76 | all_754_13 & pair$d(i$, all_754_34) = all_754_23 & pair$b(i$, % 58.77/8.76 | all_754_33) = all_754_32 & snd$(all_754_2) = all_754_1 & % 58.77/8.76 | snd$(all_754_26) = all_754_25 & pair$a(all_754_15, all_754_5) = % 58.77/8.76 | all_754_4 & pair$a(i$, a$) = all_754_28 & nrows$(a$) = all_754_36 & % 58.77/8.76 | of_nat$(all_754_30) = all_754_29 & of_nat$(all_754_36) = all_754_35 & % 58.77/8.76 | of_nat$(i$) = all_754_37 & fun_app$b(all_754_7, n$) = all_754_6 & % 58.77/8.76 | fun_app$b(all_754_17, n$) = all_754_16 & % 58.77/8.76 | Nat_a_iarray_prod$(all_754_32) & A_iarray$(all_754_33) & % 58.77/8.76 | A_a_fun$(all_754_7) & A_a_fun$(all_754_17) & % 58.77/8.76 | Nat_a_b_vec_c_vec_prod$(all_754_2) & % 58.77/8.76 | Nat_a_b_vec_c_vec_prod$(all_754_4) & % 58.77/8.76 | Nat_a_b_vec_c_vec_prod$(all_754_26) & % 58.77/8.76 | Nat_a_b_vec_c_vec_prod$(all_754_28) & A$(all_754_6) & A$(all_754_8) & % 58.77/8.76 | A$(all_754_16) & A$(all_754_18) & % 58.77/8.76 | Nat_a_iarray_iarray_prod$(all_754_11) & % 58.77/8.76 | Nat_a_iarray_iarray_prod$(all_754_13) & % 58.77/8.76 | Nat_a_iarray_iarray_prod$(all_754_21) & % 58.77/8.76 | Nat_a_iarray_iarray_prod$(all_754_23) & % 58.77/8.76 | A_a_b_vec_c_vec_prod$(all_754_9) & Nat$(all_754_15) & Nat$(all_754_30) % 58.77/8.76 | & Nat$(all_754_36) & C$(all_754_40) & C_a_b_vec_fun$(all_754_39) & % 58.77/8.76 | A_b_vec_c_vec$(all_754_1) & A_b_vec_c_vec$(all_754_5) & % 58.77/8.76 | A_b_vec_c_vec$(all_754_25) & B$(all_754_38) & % 58.77/8.76 | A_a_iarray_iarray_prod$(all_754_19) & A_iarray_iarray$(all_754_0) & % 58.77/8.76 | A_iarray_iarray$(all_754_10) & A_iarray_iarray$(all_754_14) & % 58.77/8.76 | A_iarray_iarray$(all_754_20) & A_iarray_iarray$(all_754_24) & % 58.77/8.76 | A_iarray_iarray$(all_754_34) & % 58.77/8.76 | A_nat_a_iarray_iarray_prod_prod$(all_754_12) & % 58.77/8.76 | A_nat_a_iarray_iarray_prod_prod$(all_754_22) & % 58.77/8.76 | A_nat_a_b_vec_c_vec_prod_prod$(all_754_3) & % 58.77/8.76 | A_nat_a_b_vec_c_vec_prod_prod$(all_754_27) & (( ~ (all_754_35 = % 58.77/8.76 | all_754_37) & ? [v0: C$] : ? [v1: A_b_vec$] : ? [v2: % 58.77/8.76 | B_a_fun$] : ? [v3: A$] : ( ~ (v3 = zero$a) & % 58.77/8.76 | fun_app$d(all_754_39, v0) = v1 & vec_nth$(v1) = v2 & % 58.77/8.76 | fun_app$c(v2, all_754_38) = v3 & less_eq$(all_754_40, v0) = 0 & % 58.77/8.76 | A$(v3) & B_a_fun$(v2) & A_b_vec$(v1) & C$(v0)) & (( ~ (all_754_0 % 58.77/8.76 | = all_754_10) & ~ (all_754_29 = all_754_37) & ~ % 58.77/8.76 | (all_754_31 = 0)) | ( ~ (all_754_0 = all_754_20) & (all_754_29 % 58.77/8.76 | = all_754_37 | all_754_31 = 0)))) | ((all_754_35 = % 58.77/8.76 | all_754_37 | ! [v0: C$] : ( ~ (less_eq$(all_754_40, v0) = 0) | % 58.77/8.76 | ~ C$(v0) | ? [v1: A_b_vec$] : ? [v2: B_a_fun$] : % 58.77/8.76 | (fun_app$d(all_754_39, v0) = v1 & vec_nth$(v1) = v2 & % 58.77/8.76 | fun_app$c(v2, all_754_38) = zero$a & B_a_fun$(v2) & % 58.77/8.76 | A_b_vec$(v1)))) & (( ~ (all_754_10 = all_754_24) & ~ % 58.77/8.76 | (all_754_29 = all_754_37) & ~ (all_754_31 = 0)) | ( ~ % 58.77/8.76 | (all_754_20 = all_754_24) & (all_754_29 = all_754_37 | % 58.77/8.76 | all_754_31 = 0))))) % 58.77/8.76 | % 58.77/8.76 | ALPHA: (32) implies: % 58.77/8.76 | (33) A_iarray_iarray$(all_754_34) % 58.77/8.76 | (34) Nat_a_iarray_iarray_prod$(all_754_23) % 58.77/8.76 | (35) Nat_a_b_vec_c_vec_prod$(all_754_28) % 58.77/8.76 | (36) of_nat$(i$) = all_754_37 % 58.77/8.76 | (37) of_nat$(all_754_36) = all_754_35 % 58.77/8.76 | (38) of_nat$(all_754_30) = all_754_29 % 58.77/8.76 | (39) nrows$(a$) = all_754_36 % 58.77/8.76 | (40) pair$a(i$, a$) = all_754_28 % 58.77/8.76 | (41) snd$(all_754_26) = all_754_25 % 58.77/8.76 | (42) pair$d(i$, all_754_34) = all_754_23 % 58.77/8.76 | (43) snd$c(all_754_21) = all_754_20 % 58.77/8.76 | (44) pair$(n$, all_754_28) = all_754_27 % 58.77/8.76 | (45) snd$a(all_754_27) = all_754_26 % 58.77/8.76 | (46) pair$c(n$, all_754_23) = all_754_22 % 58.77/8.76 | (47) snd$d(all_754_22) = all_754_21 % 58.77/8.76 | (48) nrows_iarray$(all_754_34) = all_754_30 % 58.77/8.76 | (49) matrix_to_iarray$(a$) = all_754_34 % 58.77/8.76 | (50) matrix_to_iarray$(all_754_25) = all_754_24 % 58.77/8.76 | (51) ( ~ (all_754_35 = all_754_37) & ? [v0: C$] : ? [v1: A_b_vec$] : ? % 58.77/8.76 | [v2: B_a_fun$] : ? [v3: A$] : ( ~ (v3 = zero$a) & % 58.77/8.76 | fun_app$d(all_754_39, v0) = v1 & vec_nth$(v1) = v2 & fun_app$c(v2, % 58.77/8.76 | all_754_38) = v3 & less_eq$(all_754_40, v0) = 0 & A$(v3) & % 58.77/8.76 | B_a_fun$(v2) & A_b_vec$(v1) & C$(v0)) & (( ~ (all_754_0 = % 58.77/8.76 | all_754_10) & ~ (all_754_29 = all_754_37) & ~ (all_754_31 = % 58.77/8.76 | 0)) | ( ~ (all_754_0 = all_754_20) & (all_754_29 = all_754_37 % 58.77/8.76 | | all_754_31 = 0)))) | ((all_754_35 = all_754_37 | ! [v0: C$] % 58.77/8.76 | : ( ~ (less_eq$(all_754_40, v0) = 0) | ~ C$(v0) | ? [v1: % 58.77/8.76 | A_b_vec$] : ? [v2: B_a_fun$] : (fun_app$d(all_754_39, v0) = % 58.77/8.76 | v1 & vec_nth$(v1) = v2 & fun_app$c(v2, all_754_38) = zero$a & % 58.77/8.76 | B_a_fun$(v2) & A_b_vec$(v1)))) & (( ~ (all_754_10 = % 58.77/8.76 | all_754_24) & ~ (all_754_29 = all_754_37) & ~ (all_754_31 = % 58.77/8.76 | 0)) | ( ~ (all_754_20 = all_754_24) & (all_754_29 = all_754_37 % 58.77/8.76 | | all_754_31 = 0)))) % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (9) with all_589_0, all_754_37, i$, simplifying % 58.77/8.76 | with (29), (36) gives: % 58.77/8.76 | (52) all_754_37 = all_589_0 % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (9) with all_562_0, all_754_37, i$, simplifying % 58.77/8.76 | with (24), (36) gives: % 58.77/8.76 | (53) all_754_37 = all_562_0 % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (10) with all_589_2, all_754_36, a$, simplifying % 58.77/8.76 | with (31), (39) gives: % 58.77/8.76 | (54) all_754_36 = all_589_2 % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (10) with all_562_2, all_754_36, a$, simplifying % 58.77/8.76 | with (26), (39) gives: % 58.77/8.76 | (55) all_754_36 = all_562_2 % 58.77/8.76 | % 58.77/8.76 | COMBINE_EQS: (54), (55) imply: % 58.77/8.76 | (56) all_589_2 = all_562_2 % 58.77/8.76 | % 58.77/8.76 | SIMP: (56) implies: % 58.77/8.76 | (57) all_589_2 = all_562_2 % 58.77/8.76 | % 58.77/8.76 | COMBINE_EQS: (52), (53) imply: % 58.77/8.76 | (58) all_589_0 = all_562_0 % 58.77/8.76 | % 58.77/8.76 | SIMP: (58) implies: % 58.77/8.76 | (59) all_589_0 = all_562_0 % 58.77/8.76 | % 58.77/8.76 | REDUCE: (28), (59) imply: % 58.77/8.76 | (60) $lesseq(all_562_0, all_589_1) % 58.77/8.76 | % 58.77/8.76 | REDUCE: (37), (55) imply: % 58.77/8.76 | (61) of_nat$(all_562_2) = all_754_35 % 58.77/8.76 | % 58.77/8.76 | REDUCE: (30), (57) imply: % 58.77/8.76 | (62) of_nat$(all_562_2) = all_589_1 % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (9) with all_562_1, all_754_35, all_562_2, % 58.77/8.76 | simplifying with (25), (61) gives: % 58.77/8.76 | (63) all_754_35 = all_562_1 % 58.77/8.76 | % 58.77/8.76 | GROUND_INST: instantiating (9) with all_589_1, all_754_35, all_562_2, % 58.77/8.76 | simplifying with (61), (62) gives: % 58.77/8.76 | (64) all_754_35 = all_589_1 % 58.77/8.76 | % 58.77/8.76 | COMBINE_EQS: (63), (64) imply: % 58.77/8.76 | (65) all_589_1 = all_562_1 % 58.77/8.76 | % 58.77/8.76 | REDUCE: (60), (65) imply: % 58.77/8.76 | (66) $lesseq(all_562_0, all_562_1) % 58.77/8.76 | % 58.77/8.76 | ANTI_SYMM: (23), (66) imply: % 58.77/8.76 | (67) all_562_0 = all_562_1 % 58.77/8.76 | % 58.77/8.76 | COMBINE_EQS: (53), (67) imply: % 58.77/8.76 | (68) all_754_37 = all_562_1 % 58.77/8.76 | % 58.77/8.77 | GROUND_INST: instantiating (axiom507) with k$, all_559_2, all_559_1, % 58.77/8.77 | all_559_0, simplifying with (6), (19), (20), (21) gives: % 58.77/8.77 | (69) ~ ($lesseq(1, $difference(all_559_1, all_559_0))) | ? [v0: Nat$] : % 58.77/8.77 | (of_nat$(v0) = $difference(all_559_1, all_559_0) & Nat$(v0)) % 58.77/8.77 | % 58.77/8.77 | GROUND_INST: instantiating (axiom571) with a$, all_562_2, simplifying with % 58.77/8.77 | (4), (26) gives: % 58.77/8.77 | (70) ? [v0: int] : ? [v1: A_iarray_iarray$] : ? [v2: Nat$] : % 58.77/8.77 | (matrix_to_iarray$(a$) = v1 & nrows_iarray$(v1) = v2 & of_nat$(v2) = % 58.77/8.77 | v0 & of_nat$(all_562_2) = v0 & Nat$(v2) & A_iarray_iarray$(v1)) % 58.77/8.77 | % 58.77/8.77 | GROUND_INST: instantiating (axiom271) with i$, a$, all_754_28, simplifying % 58.77/8.77 | with (4), (5), (40) gives: % 58.77/8.77 | (71) snd$(all_754_28) = a$ % 58.77/8.77 | % 58.77/8.77 | GROUND_INST: instantiating (axiom273) with i$, all_754_34, all_754_23, % 58.77/8.77 | simplifying with (5), (33), (42) gives: % 58.77/8.77 | (72) snd$c(all_754_23) = all_754_34 % 58.77/8.77 | % 58.77/8.77 | GROUND_INST: instantiating (axiom275) with n$, all_754_28, all_754_27, % 58.77/8.77 | simplifying with (7), (35), (44) gives: % 58.77/8.77 | (73) snd$a(all_754_27) = all_754_28 % 58.77/8.77 | % 58.77/8.77 | GROUND_INST: instantiating (axiom276) with n$, all_754_23, all_754_22, % 58.77/8.77 | simplifying with (7), (34), (46) gives: % 58.77/8.77 | (74) snd$d(all_754_22) = all_754_23 % 58.77/8.77 | % 58.77/8.77 | DELTA: instantiating (70) with fresh symbols all_781_0, all_781_1, all_781_2 % 58.77/8.77 | gives: % 58.77/8.77 | (75) matrix_to_iarray$(a$) = all_781_1 & nrows_iarray$(all_781_1) = % 58.77/8.77 | all_781_0 & of_nat$(all_781_0) = all_781_2 & of_nat$(all_562_2) = % 58.77/8.77 | all_781_2 & Nat$(all_781_0) & A_iarray_iarray$(all_781_1) % 58.77/8.77 | % 58.77/8.77 | ALPHA: (75) implies: % 58.77/8.77 | (76) of_nat$(all_562_2) = all_781_2 % 58.77/8.77 | (77) of_nat$(all_781_0) = all_781_2 % 58.77/8.77 | (78) nrows_iarray$(all_781_1) = all_781_0 % 58.77/8.77 | (79) matrix_to_iarray$(a$) = all_781_1 % 58.77/8.77 | % 58.77/8.77 | BETA: splitting (69) gives: % 58.77/8.77 | % 58.77/8.77 | Case 1: % 58.77/8.77 | | % 58.77/8.77 | | (80) $lesseq(all_559_1, all_559_0) % 58.77/8.77 | | % 58.77/8.77 | | COMBINE_INEQS: (18), (80) imply: % 58.77/8.77 | | (81) $false % 58.77/8.77 | | % 58.77/8.77 | | CLOSE: (81) is inconsistent. % 58.77/8.77 | | % 58.77/8.77 | Case 2: % 58.77/8.77 | | % 58.77/8.77 | | % 58.77/8.77 | | GROUND_INST: instantiating (9) with all_562_1, all_781_2, all_562_2, % 58.77/8.77 | | simplifying with (25), (76) gives: % 58.77/8.77 | | (82) all_781_2 = all_562_1 % 58.77/8.77 | | % 58.77/8.77 | | GROUND_INST: instantiating (13) with all_754_26, all_754_28, all_754_27, % 58.77/8.77 | | simplifying with (45), (73) gives: % 58.77/8.77 | | (83) all_754_26 = all_754_28 % 58.77/8.77 | | % 58.77/8.77 | | GROUND_INST: instantiating (14) with all_754_21, all_754_23, all_754_22, % 58.77/8.77 | | simplifying with (47), (74) gives: % 58.77/8.77 | | (84) all_754_21 = all_754_23 % 58.77/8.77 | | % 58.77/8.77 | | GROUND_INST: instantiating (16) with all_754_34, all_781_1, a$, simplifying % 58.77/8.77 | | with (49), (79) gives: % 58.77/8.77 | | (85) all_781_1 = all_754_34 % 58.77/8.77 | | % 58.77/8.77 | | REDUCE: (78), (85) imply: % 59.15/8.77 | | (86) nrows_iarray$(all_754_34) = all_781_0 % 59.15/8.77 | | % 59.15/8.77 | | REDUCE: (43), (84) imply: % 59.15/8.77 | | (87) snd$c(all_754_23) = all_754_20 % 59.15/8.77 | | % 59.15/8.77 | | REDUCE: (41), (83) imply: % 59.15/8.77 | | (88) snd$(all_754_28) = all_754_25 % 59.15/8.77 | | % 59.15/8.77 | | REDUCE: (77), (82) imply: % 59.15/8.77 | | (89) of_nat$(all_781_0) = all_562_1 % 59.15/8.77 | | % 59.15/8.77 | | GROUND_INST: instantiating (11) with a$, all_754_25, all_754_28, simplifying % 59.15/8.77 | | with (71), (88) gives: % 59.15/8.77 | | (90) all_754_25 = a$ % 59.15/8.77 | | % 59.15/8.77 | | GROUND_INST: instantiating (12) with all_754_34, all_754_20, all_754_23, % 59.15/8.77 | | simplifying with (72), (87) gives: % 59.15/8.77 | | (91) all_754_20 = all_754_34 % 59.15/8.77 | | % 59.15/8.77 | | GROUND_INST: instantiating (15) with all_754_30, all_781_0, all_754_34, % 59.15/8.77 | | simplifying with (48), (86) gives: % 59.15/8.77 | | (92) all_781_0 = all_754_30 % 59.15/8.77 | | % 59.15/8.77 | | REDUCE: (50), (90) imply: % 59.15/8.77 | | (93) matrix_to_iarray$(a$) = all_754_24 % 59.15/8.77 | | % 59.15/8.77 | | REDUCE: (89), (92) imply: % 59.15/8.77 | | (94) of_nat$(all_754_30) = all_562_1 % 59.15/8.77 | | % 59.15/8.77 | | GROUND_INST: instantiating (9) with all_754_29, all_562_1, all_754_30, % 59.15/8.77 | | simplifying with (38), (94) gives: % 59.15/8.77 | | (95) all_754_29 = all_562_1 % 59.15/8.77 | | % 59.15/8.77 | | GROUND_INST: instantiating (16) with all_754_34, all_754_24, a$, simplifying % 59.15/8.77 | | with (49), (93) gives: % 59.15/8.77 | | (96) all_754_24 = all_754_34 % 59.15/8.77 | | % 59.15/8.77 | | BETA: splitting (51) gives: % 59.15/8.77 | | % 59.15/8.77 | | Case 1: % 59.15/8.77 | | | % 59.15/8.78 | | | (97) ~ (all_754_35 = all_754_37) & ? [v0: C$] : ? [v1: A_b_vec$] : % 59.15/8.78 | | | ? [v2: B_a_fun$] : ? [v3: A$] : ( ~ (v3 = zero$a) & % 59.15/8.78 | | | fun_app$d(all_754_39, v0) = v1 & vec_nth$(v1) = v2 & % 59.15/8.78 | | | fun_app$c(v2, all_754_38) = v3 & less_eq$(all_754_40, v0) = 0 & % 59.15/8.78 | | | A$(v3) & B_a_fun$(v2) & A_b_vec$(v1) & C$(v0)) & (( ~ (all_754_0 % 59.15/8.78 | | | = all_754_10) & ~ (all_754_29 = all_754_37) & ~ % 59.15/8.78 | | | (all_754_31 = 0)) | ( ~ (all_754_0 = all_754_20) & (all_754_29 % 59.15/8.78 | | | = all_754_37 | all_754_31 = 0))) % 59.15/8.78 | | | % 59.15/8.78 | | | ALPHA: (97) implies: % 59.15/8.78 | | | (98) ~ (all_754_35 = all_754_37) % 59.15/8.78 | | | % 59.15/8.78 | | | REDUCE: (63), (68), (98) imply: % 59.15/8.78 | | | (99) $false % 59.15/8.78 | | | % 59.15/8.78 | | | CLOSE: (99) is inconsistent. % 59.15/8.78 | | | % 59.15/8.78 | | Case 2: % 59.15/8.78 | | | % 59.17/8.78 | | | (100) (all_754_35 = all_754_37 | ! [v0: C$] : ( ~ % 59.17/8.78 | | | (less_eq$(all_754_40, v0) = 0) | ~ C$(v0) | ? [v1: % 59.17/8.78 | | | A_b_vec$] : ? [v2: B_a_fun$] : (fun_app$d(all_754_39, v0) % 59.17/8.78 | | | = v1 & vec_nth$(v1) = v2 & fun_app$c(v2, all_754_38) = % 59.17/8.78 | | | zero$a & B_a_fun$(v2) & A_b_vec$(v1)))) & (( ~ (all_754_10 % 59.17/8.78 | | | = all_754_24) & ~ (all_754_29 = all_754_37) & ~ % 59.17/8.78 | | | (all_754_31 = 0)) | ( ~ (all_754_20 = all_754_24) & % 59.17/8.78 | | | (all_754_29 = all_754_37 | all_754_31 = 0))) % 59.17/8.78 | | | % 59.17/8.78 | | | ALPHA: (100) implies: % 59.17/8.78 | | | (101) ( ~ (all_754_10 = all_754_24) & ~ (all_754_29 = all_754_37) & ~ % 59.17/8.78 | | | (all_754_31 = 0)) | ( ~ (all_754_20 = all_754_24) & (all_754_29 % 59.17/8.78 | | | = all_754_37 | all_754_31 = 0)) % 59.17/8.78 | | | % 59.17/8.78 | | | BETA: splitting (101) gives: % 59.17/8.78 | | | % 59.17/8.78 | | | Case 1: % 59.17/8.78 | | | | % 59.17/8.78 | | | | (102) ~ (all_754_10 = all_754_24) & ~ (all_754_29 = all_754_37) & % 59.17/8.78 | | | | ~ (all_754_31 = 0) % 59.17/8.78 | | | | % 59.17/8.78 | | | | ALPHA: (102) implies: % 59.17/8.78 | | | | (103) ~ (all_754_29 = all_754_37) % 59.17/8.78 | | | | % 59.17/8.78 | | | | REDUCE: (68), (95), (103) imply: % 59.17/8.78 | | | | (104) $false % 59.17/8.78 | | | | % 59.17/8.78 | | | | CLOSE: (104) is inconsistent. % 59.17/8.78 | | | | % 59.17/8.78 | | | Case 2: % 59.17/8.78 | | | | % 59.17/8.78 | | | | (105) ~ (all_754_20 = all_754_24) & (all_754_29 = all_754_37 | % 59.17/8.78 | | | | all_754_31 = 0) % 59.17/8.78 | | | | % 59.17/8.78 | | | | ALPHA: (105) implies: % 59.17/8.78 | | | | (106) ~ (all_754_20 = all_754_24) % 59.17/8.78 | | | | % 59.17/8.78 | | | | REDUCE: (91), (96), (106) imply: % 59.17/8.78 | | | | (107) $false % 59.17/8.78 | | | | % 59.17/8.78 | | | | CLOSE: (107) is inconsistent. % 59.17/8.78 | | | | % 59.17/8.78 | | | End of split % 59.17/8.78 | | | % 59.17/8.78 | | End of split % 59.17/8.78 | | % 59.17/8.78 | End of split % 59.17/8.78 | % 59.17/8.78 End of proof % 59.17/8.78 % SZS output end Proof for theBenchmark % 59.17/8.78 % 59.17/8.78 8148ms %------------------------------------------------------------------------------