%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP325_1 : TPTP v8.1.2. Released v8.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n025.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:45 EDT 2023 % Result : Theorem 32.01s 5.03s % Output : Proof 46.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP325_1 : TPTP v8.1.2. Released v8.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.36 % Computer : n025.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 15:12:38 EDT 2023 % 0.14/0.36 % CPUTime : % 0.21/0.62 ________ _____ % 0.21/0.62 ___ __ \_________(_)________________________________ % 0.21/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.62 % 0.21/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.62 (2023-06-19) % 0.21/0.62 % 0.21/0.62 (c) Philipp Rümmer, 2009-2023 % 0.21/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.62 Amanda Stjerna. % 0.21/0.62 Free software under BSD-3-Clause. % 0.21/0.62 % 0.21/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.62 % 0.21/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.63 Running up to 7 provers in parallel. % 0.21/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.21/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 12.33/2.47 Prover 4: Preprocessing ... % 12.33/2.48 Prover 1: Preprocessing ... % 13.03/2.50 Prover 5: Preprocessing ... % 13.03/2.50 Prover 3: Preprocessing ... % 13.03/2.50 Prover 0: Preprocessing ... % 13.03/2.50 Prover 6: Preprocessing ... % 13.03/2.50 Prover 2: Preprocessing ... % 29.70/4.73 Prover 3: Warning: ignoring some quantifiers % 29.70/4.74 Prover 1: Warning: ignoring some quantifiers % 30.39/4.80 Prover 3: Constructing countermodel ... % 30.98/4.88 Prover 1: Constructing countermodel ... % 30.98/4.89 Prover 6: Proving ... % 32.01/5.03 Prover 3: proved (4386ms) % 32.01/5.03 % 32.01/5.03 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.01/5.03 % 32.01/5.05 Prover 6: stopped % 32.01/5.07 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 32.01/5.07 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 35.57/5.46 Prover 4: Warning: ignoring some quantifiers % 36.50/5.62 Prover 5: Proving ... % 36.50/5.63 Prover 5: stopped % 36.50/5.63 Prover 0: Proving ... % 36.50/5.63 Prover 0: stopped % 36.50/5.64 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 36.50/5.64 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 37.29/5.69 Prover 4: Constructing countermodel ... % 37.29/5.75 Prover 7: Preprocessing ... % 38.23/5.86 Prover 8: Preprocessing ... % 41.83/6.27 Prover 1: Found proof (size 41) % 41.83/6.27 Prover 1: proved (5638ms) % 41.83/6.27 Prover 4: stopped % 41.83/6.28 Prover 7: stopped % 42.21/6.42 Prover 11: Preprocessing ... % 42.21/6.46 Prover 10: Preprocessing ... % 42.85/6.47 Prover 2: Proving ... % 42.85/6.47 Prover 2: stopped % 44.67/6.74 Prover 10: stopped % 44.93/6.82 Prover 11: stopped % 45.36/6.87 Prover 8: Warning: ignoring some quantifiers % 45.56/6.94 Prover 8: Constructing countermodel ... % 45.79/6.95 Prover 8: stopped % 45.79/6.95 % 45.79/6.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 45.79/6.95 % 45.85/6.96 % SZS output start Proof for theBenchmark % 45.85/7.00 Assumptions after simplification: % 45.85/7.00 --------------------------------- % 45.85/7.00 % 45.85/7.00 (axiom105) % 45.85/7.04 A$(one$) & N$(i$) & B$(j$) & A_b_vec_n_vec$(interchange_A$) & % 45.85/7.04 A_b_vec_n_vec$(a$a) & ? [v0: A_a_b_vec_n_vec_fun$] : ? [v1: A_a_fun$] : ? % 45.85/7.04 [v2: N_a_b_vec_fun$] : ? [v3: A_b_vec$] : ? [v4: B_a_fun$] : ? [v5: A$] : % 45.85/7.04 ? [v6: A$] : (divide$(one$) = v1 & mult_row$(interchange_A$, i$) = v0 & % 45.85/7.04 fun_app$n(v0, v6) = a$a & fun_app$m(v1, v5) = v6 & vec_nth$a(interchange_A$) % 45.85/7.04 = v2 & fun_app$b(v2, i$) = v3 & vec_nth$(v3) = v4 & fun_app$a(v4, j$) = v5 & % 45.85/7.04 A_a_fun$(v1) & A$(v6) & A$(v5) & N_a_b_vec_fun$(v2) & B_a_fun$(v4) & % 45.85/7.04 A_b_vec$(v3) & A_a_b_vec_n_vec_fun$(v0)) % 45.85/7.04 % 45.85/7.05 (axiom240) % 45.85/7.06 N_bool_fun$(uu$) & N_n_bool_fun_fun$(less_eq$) & A$(zero$) & A$(one$) & N$(i$) % 45.85/7.06 & B$(j$) & A_b_vec_n_vec$(a$) & ? [v0: N$] : ? [v1: N_a_b_vec_fun$] : ? % 45.85/7.06 [v2: N_bool_fun$] : ? [v3: N_a_b_vec_n_vec_fun$] : ? [v4: A_a_fun$] : ? % 45.85/7.06 [v5: A_b_vec_n_vec$] : (gauss_Jordan_in_ij$(a$, i$, j$) = v5 & divide$(one$) = % 45.85/7.06 v4 & interchange_rows$(a$, i$) = v3 & least$(uu$) = v0 & vec_nth$a(a$) = v1 % 45.85/7.06 & fun_app$c(less_eq$, i$) = v2 & N_a_b_vec_n_vec_fun$(v3) & N_bool_fun$(v2) % 45.85/7.06 & A_a_fun$(v4) & N_a_b_vec_fun$(v1) & N$(v0) & A_b_vec_n_vec$(v5) & ! [v6: % 45.85/7.06 A_b_vec_n_vec$] : ! [v7: A_b_vec_n_vec$] : ! [v8: N_a_b_vec_fun$] : ( ~ % 45.85/7.06 (uua$(v6, v7) = v8) | ~ (fun_app$d(v3, v0) = v6) | ~ A_b_vec_n_vec$(v7) % 45.85/7.06 | ~ A_b_vec_n_vec$(v6) | thesis$ | ? [v9: A_b_vec$] : ? [v10: B_a_fun$] % 45.85/7.06 : ? [v11: A$] : ? [v12: any] : ? [v13: A_a_b_vec_n_vec_fun$] : ? [v14: % 45.85/7.06 N_a_b_vec_fun$] : ? [v15: A_b_vec$] : ? [v16: B_a_fun$] : ? [v17: A$] % 45.85/7.06 : ? [v18: A$] : ? [v19: A_b_vec_n_vec$] : ? [v20: A_b_vec_n_vec$] : % 45.85/7.06 (mult_row$(v6, i$) = v13 & fun_app$n(v13, v18) = v19 & fun_app$m(v4, v17) % 45.85/7.06 = v18 & vec_lambda$a(v8) = v20 & vec_nth$a(v6) = v14 & fun_app$(v2, v0) % 45.85/7.06 = v12 & fun_app$b(v14, i$) = v15 & fun_app$b(v1, v0) = v9 & % 45.85/7.06 vec_nth$(v15) = v16 & vec_nth$(v9) = v10 & fun_app$a(v16, j$) = v17 & % 45.85/7.06 fun_app$a(v10, j$) = v11 & A$(v18) & A$(v17) & A$(v11) & % 45.85/7.06 N_a_b_vec_fun$(v14) & B_a_fun$(v16) & B_a_fun$(v10) & A_b_vec$(v15) & % 45.85/7.06 A_b_vec$(v9) & A_a_b_vec_n_vec_fun$(v13) & A_b_vec_n_vec$(v20) & % 45.85/7.06 A_b_vec_n_vec$(v19) & ( ~ (v20 = v5) | ~ (v19 = v7) | ~ (v12 = 0) | % 45.85/7.06 v11 = zero$)))) % 45.85/7.06 % 45.85/7.06 (axiom44) % 45.85/7.07 A_a_fun$(uminus$c) & A$(one$) & ? [v0: A_a_fun$] : (divide$(one$) = v0 & % 45.85/7.07 A_a_fun$(v0) & ! [v1: A_b_vec_n_vec$] : ! [v2: N$] : ! [v3: B$] : ! [v4: % 45.85/7.07 N$] : ! [v5: N_a_b_vec_n_vec_fun$] : ! [v6: N_bool_fun$] : ! [v7: N$] : % 45.85/7.07 ! [v8: A_b_vec_n_vec$] : ! [v9: A_a_b_vec_n_vec_fun$] : ! [v10: % 45.85/7.07 N_a_b_vec_fun$] : ! [v11: A_b_vec$] : ! [v12: B_a_fun$] : ! [v13: A$] : % 45.85/7.07 ! [v14: A$] : ! [v15: A_b_vec_n_vec$] : ! [v16: A_a_b_vec_n_vec_fun$] : % 45.85/7.07 ! [v17: A_b_vec$] : ! [v18: B_a_fun$] : ! [v19: A$] : ! [v20: A$] : ! % 45.85/7.07 [v21: A_b_vec_n_vec$] : ! [v22: N_a_b_vec_fun$] : ! [v23: A_b_vec$] : (v4 % 45.85/7.07 = v2 | ~ (interchange_rows$(v1, v2) = v5) | ~ (uwf$(v1, v2, v3) = v6) | % 45.85/7.07 ~ (least$(v6) = v7) | ~ (mult_row$(v8, v2) = v9) | ~ (row_add$(v15, v4, % 45.85/7.07 v2) = v16) | ~ (fun_app$n(v16, v20) = v21) | ~ (fun_app$n(v9, v14) = % 45.85/7.07 v15) | ~ (fun_app$m(v0, v13) = v14) | ~ (fun_app$m(uminus$c, v19) = % 45.85/7.07 v20) | ~ (fun_app$d(v5, v7) = v8) | ~ (vec_nth$a(v21) = v22) | ~ % 45.85/7.07 (vec_nth$a(v8) = v10) | ~ (fun_app$b(v22, v4) = v23) | ~ (fun_app$b(v10, % 45.85/7.07 v4) = v17) | ~ (fun_app$b(v10, v2) = v11) | ~ (vec_nth$(v17) = v18) % 45.85/7.07 | ~ (vec_nth$(v11) = v12) | ~ (fun_app$a(v18, v3) = v19) | ~ % 45.85/7.07 (fun_app$a(v12, v3) = v13) | ~ N$(v4) | ~ N$(v2) | ~ B$(v3) | ~ % 45.85/7.07 A_b_vec_n_vec$(v1) | ? [v24: N_a_b_vec_fun$] : (uwg$(v1, v2, v3) = v24 & % 45.85/7.07 fun_app$b(v24, v4) = v23 & N_a_b_vec_fun$(v24) & A_b_vec$(v23))) & ! % 45.85/7.07 [v1: A_b_vec_n_vec$] : ! [v2: N$] : ! [v3: B$] : ! [v4: % 45.85/7.07 N_a_b_vec_n_vec_fun$] : ! [v5: N_bool_fun$] : ! [v6: N$] : ! [v7: % 45.85/7.07 A_b_vec_n_vec$] : ! [v8: A_a_b_vec_n_vec_fun$] : ! [v9: N_a_b_vec_fun$] % 45.85/7.07 : ! [v10: A_b_vec$] : ! [v11: B_a_fun$] : ! [v12: A$] : ! [v13: A$] : ! % 45.85/7.07 [v14: A_b_vec_n_vec$] : ! [v15: N_a_b_vec_fun$] : ! [v16: A_b_vec$] : ( ~ % 45.85/7.07 (interchange_rows$(v1, v2) = v4) | ~ (uwf$(v1, v2, v3) = v5) | ~ % 45.85/7.07 (least$(v5) = v6) | ~ (mult_row$(v7, v2) = v8) | ~ (fun_app$n(v8, v13) = % 45.85/7.07 v14) | ~ (fun_app$m(v0, v12) = v13) | ~ (fun_app$d(v4, v6) = v7) | ~ % 45.85/7.07 (vec_nth$a(v14) = v15) | ~ (vec_nth$a(v7) = v9) | ~ (fun_app$b(v15, v2) % 45.85/7.07 = v16) | ~ (fun_app$b(v9, v2) = v10) | ~ (vec_nth$(v10) = v11) | ~ % 45.85/7.07 (fun_app$a(v11, v3) = v12) | ~ N$(v2) | ~ B$(v3) | ~ A_b_vec_n_vec$(v1) % 45.85/7.07 | ? [v17: N_a_b_vec_fun$] : (uwg$(v1, v2, v3) = v17 & fun_app$b(v17, v2) % 45.85/7.07 = v16 & N_a_b_vec_fun$(v17) & A_b_vec$(v16)))) % 45.85/7.07 % 45.85/7.07 (axiom45) % 45.85/7.08 A_a_fun$(uminus$c) & A$(one$) & ? [v0: A_a_fun$] : (divide$(one$) = v0 & % 45.85/7.08 A_a_fun$(v0) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 45.85/7.08 N$] : ! [v5: N_a_n_vec_n_vec_fun$] : ! [v6: N_n_bool_fun_fun$] : ! [v7: % 45.85/7.08 N_bool_fun$] : ! [v8: N$] : ! [v9: A_n_vec_n_vec$] : ! [v10: % 45.85/7.08 N_a_n_vec_fun$] : ! [v11: A_n_vec$] : ! [v12: N_a_fun$] : ! [v13: A$] : % 45.85/7.08 ! [v14: A$] : ! [v15: A_n_vec_n_vec$] : ! [v16: A_n_vec$] : ! [v17: % 45.85/7.08 N_a_fun$] : ! [v18: A$] : ! [v19: A$] : ! [v20: A_n_vec_n_vec$] : ! % 45.85/7.08 [v21: N_a_n_vec_fun$] : ! [v22: A_n_vec$] : (v4 = v2 | ~ (row_add$a(v15, % 45.85/7.08 v4, v2, v19) = v20) | ~ (interchange_rows$a(v1, v2) = v5) | ~ % 45.85/7.08 (uwd$(v1, v2) = v6) | ~ (mult_row$a(v9, v2, v14) = v15) | ~ (least$(v7) % 45.85/7.08 = v8) | ~ (vec_nth$e(v16) = v17) | ~ (vec_nth$e(v11) = v12) | ~ % 45.85/7.08 (fun_app$l(v17, v3) = v18) | ~ (fun_app$l(v12, v3) = v13) | ~ % 45.85/7.08 (fun_app$m(v0, v13) = v14) | ~ (fun_app$m(uminus$c, v18) = v19) | ~ % 45.85/7.08 (vec_nth$c(v20) = v21) | ~ (vec_nth$c(v9) = v10) | ~ (fun_app$h(v5, v8) % 45.85/7.08 = v9) | ~ (fun_app$f(v21, v4) = v22) | ~ (fun_app$f(v10, v4) = v16) | % 45.85/7.08 ~ (fun_app$f(v10, v2) = v11) | ~ (fun_app$c(v6, v3) = v7) | ~ N$(v4) | % 45.85/7.08 ~ N$(v3) | ~ N$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v23: N_a_n_vec_fun$] : % 45.85/7.08 (uwe$(v1, v2, v3) = v23 & fun_app$f(v23, v4) = v22 & A_n_vec$(v22) & % 45.85/7.08 N_a_n_vec_fun$(v23))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.08 N$] : ! [v4: N_a_n_vec_n_vec_fun$] : ! [v5: N_n_bool_fun_fun$] : ! [v6: % 45.85/7.08 N_bool_fun$] : ! [v7: N$] : ! [v8: A_n_vec_n_vec$] : ! [v9: % 45.85/7.08 N_a_n_vec_fun$] : ! [v10: A_n_vec$] : ! [v11: N_a_fun$] : ! [v12: A$] : % 45.85/7.08 ! [v13: A$] : ! [v14: A_n_vec_n_vec$] : ! [v15: N_a_n_vec_fun$] : ! % 45.85/7.08 [v16: A_n_vec$] : ( ~ (interchange_rows$a(v1, v2) = v4) | ~ (uwd$(v1, v2) = % 45.85/7.08 v5) | ~ (mult_row$a(v8, v2, v13) = v14) | ~ (least$(v6) = v7) | ~ % 45.85/7.08 (vec_nth$e(v10) = v11) | ~ (fun_app$l(v11, v3) = v12) | ~ (fun_app$m(v0, % 45.85/7.08 v12) = v13) | ~ (vec_nth$c(v14) = v15) | ~ (vec_nth$c(v8) = v9) | ~ % 45.85/7.08 (fun_app$h(v4, v7) = v8) | ~ (fun_app$f(v15, v2) = v16) | ~ % 45.85/7.08 (fun_app$f(v9, v2) = v10) | ~ (fun_app$c(v5, v3) = v6) | ~ N$(v3) | ~ % 45.85/7.08 N$(v2) | ~ A_n_vec_n_vec$(v1) | ? [v17: N_a_n_vec_fun$] : (uwe$(v1, v2, % 45.85/7.08 v3) = v17 & fun_app$f(v17, v2) = v16 & A_n_vec$(v16) & % 45.85/7.08 N_a_n_vec_fun$(v17)))) % 45.85/7.08 % 45.85/7.08 (conjecture104) % 45.85/7.08 A$(one$) & N$(i$) & B$(j$) & A_b_vec_n_vec$(interchange_A$) & % 45.85/7.08 A_b_vec_n_vec$(a$a) & ? [v0: A_a_b_vec_n_vec_fun$] : ? [v1: A_a_fun$] : ? % 45.85/7.08 [v2: N_a_b_vec_fun$] : ? [v3: A_b_vec$] : ? [v4: B_a_fun$] : ? [v5: A$] : % 45.85/7.08 ? [v6: A$] : ? [v7: A_b_vec_n_vec$] : ( ~ (v7 = a$a) & divide$(one$) = v1 & % 45.85/7.08 mult_row$(interchange_A$, i$) = v0 & fun_app$n(v0, v6) = v7 & fun_app$m(v1, % 45.85/7.08 v5) = v6 & vec_nth$a(interchange_A$) = v2 & fun_app$b(v2, i$) = v3 & % 45.85/7.08 vec_nth$(v3) = v4 & fun_app$a(v4, j$) = v5 & A_a_fun$(v1) & A$(v6) & A$(v5) % 45.85/7.08 & N_a_b_vec_fun$(v2) & B_a_fun$(v4) & A_b_vec$(v3) & % 45.85/7.08 A_a_b_vec_n_vec_fun$(v0) & A_b_vec_n_vec$(v7)) % 45.85/7.08 % 45.85/7.08 (function-axioms) % 45.85/7.13 ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: A$] : ! [v3: N$] % 45.85/7.13 : ! [v4: N$] : ! [v5: A_b_vec_n_vec$] : (v1 = v0 | ~ (row_add_row$b(v5, v4, % 45.85/7.13 v3, v2) = v1) | ~ (row_add_row$b(v5, v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! % 45.85/7.13 [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (row_add_row$a(v5, v4, v3, % 45.85/7.13 v2) = v1) | ~ (row_add_row$a(v5, v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec$] : % 45.85/7.13 ! [v3: N$] : ! [v4: N$] : ! [v5: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (row_add_row$(v5, v4, v3, v2) = v1) | ~ (row_add_row$(v5, v4, v3, v2) = % 45.85/7.13 v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : ! % 45.85/7.13 [v2: A_b_vec$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_b_vec_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (row_add$b(v5, v4, v3, v2) = v1) | ~ (row_add$b(v5, v4, v3, v2) % 45.85/7.13 = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! [v3: N$] % 45.85/7.13 : ! [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (uuh$(v5, v4, v3, v2) % 45.85/7.13 = v1) | ~ (uuh$(v5, v4, v3, v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: % 45.85/7.13 B_a_fun$] : ! [v2: B$] : ! [v3: B$] : ! [v4: B$] : ! [v5: % 45.85/7.13 A_b_vec_b_vec$] : (v1 = v0 | ~ (uuj$(v5, v4, v3, v2) = v1) | ~ (uuj$(v5, % 45.85/7.13 v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : % 45.85/7.13 ! [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_b_vec_n_vec_n_vec$] : (v1 % 45.85/7.13 = v0 | ~ (uul$(v5, v4, v3, v2) = v1) | ~ (uul$(v5, v4, v3, v2) = v0)) & ! % 45.85/7.13 [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: N$] : ! [v3: B$] : ! [v4: B$] : % 45.85/7.13 ! [v5: A_b_vec_n_vec$] : (v1 = v0 | ~ (uun$(v5, v4, v3, v2) = v1) | ~ % 45.85/7.13 (uun$(v5, v4, v3, v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! % 45.85/7.13 [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (uup$(v5, v4, v3, v2) = v1) | ~ (uup$(v5, v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: B$] : ! [v3: B$] : ! [v4: B$] : ! % 45.85/7.13 [v5: A_b_vec_b_vec$] : (v1 = v0 | ~ (uur$(v5, v4, v3, v2) = v1) | ~ % 45.85/7.13 (uur$(v5, v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.13 N_a_b_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uut$(v5, v4, v3, v2) = v1) | ~ % 45.85/7.13 (uut$(v5, v4, v3, v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! % 45.85/7.13 [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (uuv$(v5, v4, v3, v2) = v1) | ~ (uuv$(v5, v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! [v3: A$] : ! [v4: N$] : ! % 45.85/7.13 [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (uxb$(v5, v4, v3, v2) = v1) | ~ % 45.85/7.13 (uxb$(v5, v4, v3, v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! % 45.85/7.13 [v2: B$] : ! [v3: A$] : ! [v4: B$] : ! [v5: A_b_vec_b_vec$] : (v1 = v0 | ~ % 45.85/7.13 (uxd$(v5, v4, v3, v2) = v1) | ~ (uxd$(v5, v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: N$] : ! [v3: A_b_vec$] % 45.85/7.13 : ! [v4: N$] : ! [v5: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uxf$(v5, v4, % 45.85/7.13 v3, v2) = v1) | ~ (uxf$(v5, v4, v3, v2) = v0)) & ! [v0: B_a_fun$] : ! % 45.85/7.13 [v1: B_a_fun$] : ! [v2: N$] : ! [v3: A$] : ! [v4: N$] : ! [v5: % 45.85/7.13 A_b_vec_n_vec$] : (v1 = v0 | ~ (uxh$(v5, v4, v3, v2) = v1) | ~ (uxh$(v5, % 45.85/7.13 v4, v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : % 45.85/7.13 ! [v2: A$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | % 45.85/7.13 ~ (row_add$a(v5, v4, v3, v2) = v1) | ~ (row_add$a(v5, v4, v3, v2) = v0)) & % 45.85/7.13 ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! [v2: A$] : ! [v3: B$] % 45.85/7.13 : ! [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ (mult_row$c(v4, v3, v2) = v1) | ~ % 45.85/7.13 (mult_row$c(v4, v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 % 45.85/7.13 = v0 | ~ (gauss_Jordan_in_ij$a(v4, v3, v2) = v1) | ~ % 45.85/7.13 (gauss_Jordan_in_ij$a(v4, v3, v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 45.85/7.13 A_b_vec_b_vec$] : ! [v2: B$] : ! [v3: B$] : ! [v4: A_b_vec_b_vec$] : (v1 % 45.85/7.13 = v0 | ~ (interchange_rows$c(v4, v3, v2) = v1) | ~ (interchange_rows$c(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! % 45.85/7.13 [v2: B$] : ! [v3: B$] : ! [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ % 45.85/7.13 (interchange_columns$c(v4, v3, v2) = v1) | ~ (interchange_columns$c(v4, v3, % 45.85/7.13 v2) = v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: % 45.85/7.13 B$] : ! [v3: B$] : ! [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (interchange_columns$b(v4, v3, v2) = v1) | ~ (interchange_columns$b(v4, v3, % 45.85/7.13 v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (interchange_columns$a(v4, v3, v2) = % 45.85/7.13 v1) | ~ (interchange_columns$a(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! % 45.85/7.13 [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (interchange_columns$(v4, v3, v2) = v1) | % 45.85/7.13 ~ (interchange_columns$(v4, v3, v2) = v0)) & ! [v0: A_b_vec_n_vec$] : ! % 45.85/7.13 [v1: A_b_vec_n_vec$] : ! [v2: B$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (gauss_Jordan_in_ij$(v4, v3, v2) = v1) | ~ % 45.85/7.13 (gauss_Jordan_in_ij$(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.13 N_a_b_vec_fun$] : ! [v2: B$] : ! [v3: B$] : ! [v4: A_b_vec_n_vec$] : (v1 % 45.85/7.13 = v0 | ~ (interchange_columns_row$b(v4, v3, v2) = v1) | ~ % 45.85/7.13 (interchange_columns_row$b(v4, v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.13 [v1: N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (interchange_columns_row$a(v4, v3, v2) = v1) | ~ % 45.85/7.13 (interchange_columns_row$a(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! % 45.85/7.13 [v3: N$] : ! [v4: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (interchange_columns_row$(v4, v3, v2) = v1) | ~ % 45.85/7.13 (interchange_columns_row$(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! % 45.85/7.13 [v1: N_a_b_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (interchange_rows_row$b(v4, v3, v2) = v1) | ~ % 45.85/7.13 (interchange_rows_row$b(v4, v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.13 [v1: N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (interchange_rows_row$a(v4, v3, v2) = v1) | ~ % 45.85/7.13 (interchange_rows_row$a(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : % 45.85/7.13 ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (interchange_rows_row$(v4, v3, v2) = % 45.85/7.13 v1) | ~ (interchange_rows_row$(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! % 45.85/7.13 [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ (mult_row_row$b(v4, v3, v2) = v1) | ~ % 45.85/7.13 (mult_row_row$b(v4, v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: % 45.85/7.13 N_a_n_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 % 45.85/7.13 = v0 | ~ (mult_row_row$a(v4, v3, v2) = v1) | ~ (mult_row_row$a(v4, v3, v2) % 45.85/7.13 = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : % 45.85/7.13 ! [v2: A_b_vec$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (mult_row_row$(v4, v3, v2) = v1) | ~ (mult_row_row$(v4, v3, v2) = v0)) & ! % 45.85/7.13 [v0: A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : ! [v2: A_b_vec$] % 45.85/7.13 : ! [v3: N$] : ! [v4: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (mult_row$b(v4, % 45.85/7.13 v3, v2) = v1) | ~ (mult_row$b(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! % 45.85/7.13 [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (uui$(v4, v3, v2) = v1) | ~ (uui$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! % 45.85/7.13 [v2: B$] : ! [v3: B$] : ! [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ (uuk$(v4, v3, % 45.85/7.13 v2) = v1) | ~ (uuk$(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] % 45.85/7.13 : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uum$(v4, v3, v2) = v1) | ~ (uum$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! % 45.85/7.13 [v2: B$] : ! [v3: B$] : ! [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ (uuo$(v4, v3, % 45.85/7.13 v2) = v1) | ~ (uuo$(v4, v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.13 [v1: N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (uuq$(v4, v3, v2) = v1) | ~ (uuq$(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: B$] : ! [v3: B$] : ! % 45.85/7.13 [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ (uus$(v4, v3, v2) = v1) | ~ (uus$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.13 N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uuu$(v4, v3, v2) = v1) | ~ (uuu$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! % 45.85/7.13 [v2: N$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ (uuw$(v4, v3, % 45.85/7.13 v2) = v1) | ~ (uuw$(v4, v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.13 [v1: N_a_n_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (uxc$(v4, v3, v2) = v1) | ~ (uxc$(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: A$] : ! [v3: B$] : ! % 45.85/7.13 [v4: A_b_vec_b_vec$] : (v1 = v0 | ~ (uxe$(v4, v3, v2) = v1) | ~ (uxe$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.13 N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec$] : ! [v3: N$] : ! [v4: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uxg$(v4, v3, v2) = v1) | ~ (uxg$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! % 45.85/7.13 [v2: A$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ (uxi$(v4, v3, % 45.85/7.13 v2) = v1) | ~ (uxi$(v4, v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! % 45.85/7.13 [v1: A_n_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (mult_row$a(v4, v3, v2) = v1) | ~ (mult_row$a(v4, v3, v2) = % 45.85/7.13 v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: N$] : % 45.85/7.13 ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (uwe$(v4, v3, v2) = v1) | % 45.85/7.13 ~ (uwe$(v4, v3, v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: N_bool_fun$] : % 45.85/7.13 ! [v2: B$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : (v1 = v0 | ~ (uwf$(v4, % 45.85/7.13 v3, v2) = v1) | ~ (uwf$(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : % 45.85/7.13 ! [v1: N_a_b_vec_fun$] : ! [v2: B$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (uwg$(v4, v3, v2) = v1) | ~ (uwg$(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: N$] : ! [v3: A_b_vec_n_vec$] : ! % 45.85/7.13 [v4: A_a_fun$] : (v1 = v0 | ~ (uux$(v4, v3, v2) = v1) | ~ (uux$(v4, v3, v2) % 45.85/7.13 = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: N$] : % 45.85/7.13 ! [v3: A_n_vec_n_vec$] : ! [v4: A_a_b_vec_fun$] : (v1 = v0 | ~ (uuz$(v4, % 45.85/7.13 v3, v2) = v1) | ~ (uuz$(v4, v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : % 45.85/7.13 ! [v1: N_a_b_vec_fun$] : ! [v2: N$] : ! [v3: A_b_vec_n_vec_n_vec$] : ! [v4: % 45.85/7.13 A_b_vec_a_b_vec_fun$] : (v1 = v0 | ~ (uvb$(v4, v3, v2) = v1) | ~ (uvb$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : % 45.85/7.13 ! [v3: A_n_vec_n_vec$] : ! [v4: A_a_fun$] : (v1 = v0 | ~ (uvd$(v4, v3, v2) = % 45.85/7.13 v1) | ~ (uvd$(v4, v3, v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] % 45.85/7.13 : ! [v2: B$] : ! [v3: A_b_vec_b_vec$] : ! [v4: A_a_fun$] : (v1 = v0 | ~ % 45.85/7.13 (uvf$(v4, v3, v2) = v1) | ~ (uvf$(v4, v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: % 45.85/7.13 A_n_vec_n_vec$] : ! [v4: A_a_n_vec_fun$] : (v1 = v0 | ~ (uvh$(v4, v3, v2) % 45.85/7.13 = v1) | ~ (uvh$(v4, v3, v2) = v0)) & ! [v0: B_a_b_vec_fun$] : ! [v1: % 45.85/7.13 B_a_b_vec_fun$] : ! [v2: N$] : ! [v3: A_b_vec_n_vec$] : ! [v4: % 45.85/7.13 A_a_b_vec_fun$] : (v1 = v0 | ~ (uvj$(v4, v3, v2) = v1) | ~ (uvj$(v4, v3, % 45.85/7.13 v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! % 45.85/7.13 [v3: A_b_vec_n_vec_n_vec$] : ! [v4: A_b_vec_a_fun$] : (v1 = v0 | ~ (uvl$(v4, % 45.85/7.13 v3, v2) = v1) | ~ (uvl$(v4, v3, v2) = v0)) & ! [v0: N_a_fun$] : ! % 45.85/7.13 [v1: N_a_fun$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec_n_vec$] : ! [v4: % 45.85/7.13 A_n_vec_a_fun$] : (v1 = v0 | ~ (uvn$(v4, v3, v2) = v1) | ~ (uvn$(v4, v3, % 45.85/7.13 v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.13 N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : ! [v4: % 45.85/7.13 A_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (uvp$(v4, v3, v2) = v1) | ~ (uvp$(v4, % 45.85/7.13 v3, v2) = v0)) & ! [v0: A_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.13 A_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_b_vec_n_vec$] % 45.85/7.13 : (v1 = v0 | ~ (row_add$(v4, v3, v2) = v1) | ~ (row_add$(v4, v3, v2) = v0)) % 45.85/7.13 & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! [v2: A_b_vec_b_vec$] % 45.85/7.13 : ! [v3: A_b_vec_b_vec$] : (v1 = v0 | ~ (times$f(v3, v2) = v1) | ~ % 45.85/7.13 (times$f(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] % 45.85/7.13 : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.13 (times$e(v3, v2) = v1) | ~ (times$e(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_b_vec_b_vec_n_vec$] : ! [v1: A_b_vec_b_vec_n_vec$] : ! [v2: % 45.85/7.13 A_b_vec_n_vec$] : ! [v3: A_a_b_vec_fun$] : (v1 = v0 | ~ (map_matrix$k(v3, % 45.85/7.13 v2) = v1) | ~ (map_matrix$k(v3, v2) = v0)) & ! [v0: A_b_vec_b_vec$] : % 45.85/7.13 ! [v1: A_b_vec_b_vec$] : ! [v2: A_b_vec_b_vec$] : ! [v3: A_a_fun$] : (v1 = % 45.85/7.13 v0 | ~ (map_matrix$j(v3, v2) = v1) | ~ (map_matrix$j(v3, v2) = v0)) & ! % 45.85/7.13 [v0: N$] : ! [v1: N$] : ! [v2: N$] : ! [v3: N_n_fun$] : (v1 = v0 | ~ % 45.85/7.13 (fun_app$ag(v3, v2) = v1) | ~ (fun_app$ag(v3, v2) = v0)) & ! [v0: % 45.85/7.13 N_a_b_vec_n_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_n_vec_fun$] : ! [v2: % 45.85/7.13 N$] : ! [v3: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (interchange_rows$b(v3, % 45.85/7.13 v2) = v1) | ~ (interchange_rows$b(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_b_vec_bool_fun$] : ! [v1: A_b_vec_bool_fun$] : ! [v2: N$] : ! [v3: % 45.85/7.13 N_a_b_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$af(v3, v2) = v1) | ~ % 45.85/7.13 (fun_app$af(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 45.85/7.13 MultipleValueBool] : ! [v2: A_b_vec$] : ! [v3: A_b_vec_bool_fun$] : (v1 = % 45.85/7.13 v0 | ~ (fun_app$ae(v3, v2) = v1) | ~ (fun_app$ae(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: B$] : ! [v3: % 45.85/7.13 B_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ % 45.85/7.13 (fun_app$ad(v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : % 45.85/7.13 ! [v2: N$] : ! [v3: N_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ac(v3, v2) = % 45.85/7.13 v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 45.85/7.13 MultipleValueBool] : ! [v2: A$] : ! [v3: A_bool_fun$] : (v1 = v0 | ~ % 45.85/7.13 (fun_app$ab(v3, v2) = v1) | ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: N$] : ! [v3: % 45.85/7.13 N_a_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$aa(v3, v2) = v1) | ~ % 45.85/7.13 (fun_app$aa(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 45.85/7.13 MultipleValueBool] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_bool_fun$] : (v1 = % 45.85/7.13 v0 | ~ (fun_app$z(v3, v2) = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_b_vec_n_vec_bool_fun$] : ! [v1: A_b_vec_n_vec_bool_fun$] : ! [v2: N$] : % 45.85/7.13 ! [v3: N_a_b_vec_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$y(v3, v2) = v1) % 45.85/7.13 | ~ (fun_app$y(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 45.85/7.13 MultipleValueBool] : ! [v2: A_b_vec_n_vec$] : ! [v3: % 45.85/7.13 A_b_vec_n_vec_bool_fun$] : (v1 = v0 | ~ (fun_app$x(v3, v2) = v1) | ~ % 45.85/7.13 (fun_app$x(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 45.85/7.13 A_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (map_matrix$i(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$i(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_n_vec_n_vec$] : ! [v2: A_b_vec_n_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.13 A_b_vec_n_vec_a_fun$] : (v1 = v0 | ~ (map_matrix$h(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$h(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v2: N$] : ! [v3: A_b_vec_n_vec_n_vec_n_vec$] : % 45.85/7.13 (v1 = v0 | ~ (vec_nth$g(v3, v2) = v1) | ~ (vec_nth$g(v3, v2) = v0)) & ! % 45.85/7.13 [v0: A$] : ! [v1: A$] : ! [v2: A_b_vec_n_vec$] : ! [v3: % 45.85/7.13 A_b_vec_n_vec_a_fun$] : (v1 = v0 | ~ (fun_app$w(v3, v2) = v1) | ~ % 45.85/7.13 (fun_app$w(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.13 A_n_vec_a_b_vec_fun$] : (v1 = v0 | ~ (map_matrix$g(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$g(v3, v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! % 45.85/7.13 [v2: A_n_vec$] : ! [v3: A_n_vec_a_b_vec_fun$] : (v1 = v0 | ~ (fun_app$v(v3, % 45.85/7.13 v2) = v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] % 45.85/7.13 : ! [v1: A_b_vec_n_vec_n_vec$] : ! [v2: A_b_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.13 A_b_vec_a_b_vec_fun$] : (v1 = v0 | ~ (map_matrix$f(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$f(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_n_vec_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_a_n_vec_fun$] : % 45.85/7.13 (v1 = v0 | ~ (map_matrix$e(v3, v2) = v1) | ~ (map_matrix$e(v3, v2) = v0)) & % 45.85/7.13 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 45.85/7.13 A_n_vec_n_vec_n_vec$] : ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ % 45.85/7.13 (map_matrix$d(v3, v2) = v1) | ~ (map_matrix$d(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_b_vec_n_vec_n_vec$] : % 45.85/7.13 ! [v3: A_b_vec_a_fun$] : (v1 = v0 | ~ (map_matrix$c(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$c(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_a_b_vec_fun$] : % 45.85/7.13 (v1 = v0 | ~ (map_matrix$b(v3, v2) = v1) | ~ (map_matrix$b(v3, v2) = v0)) & % 45.85/7.13 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : % 45.85/7.13 ! [v3: A_a_fun$] : (v1 = v0 | ~ (map_matrix$a(v3, v2) = v1) | ~ % 45.85/7.13 (map_matrix$a(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: % 45.85/7.13 A_b_vec_n_vec$] : ! [v2: A_b_vec_n_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | % 45.85/7.13 ~ (map_matrix$(v3, v2) = v1) | ~ (map_matrix$(v3, v2) = v0)) & ! [v0: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : ! [v2: % 45.85/7.13 A_b_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.13 A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$u(v3, % 45.85/7.13 v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: % 45.85/7.13 A_b_vec$] : ! [v2: A$] : ! [v3: A_a_b_vec_fun$] : (v1 = v0 | ~ % 45.85/7.14 (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: A_n_vec$] % 45.85/7.14 : ! [v1: A_n_vec$] : ! [v2: A$] : ! [v3: A_a_n_vec_fun$] : (v1 = v0 | ~ % 45.85/7.14 (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: A$] : ! % 45.85/7.14 [v1: A$] : ! [v2: A_b_vec$] : ! [v3: A_b_vec_a_fun$] : (v1 = v0 | ~ % 45.85/7.14 (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: % 45.85/7.14 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.14 A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$f(v3, v2) = v1) | ~ % 45.85/7.14 (vec_nth$f(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_n_vec$] : % 45.85/7.14 ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 45.85/7.14 (fun_app$q(v3, v2) = v0)) & ! [v0: N_a_n_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_n_vec_n_vec_fun$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | % 45.85/7.14 ~ (interchange_rows$a(v3, v2) = v1) | ~ (interchange_rows$a(v3, v2) = v0)) % 45.85/7.14 & ! [v0: N_n_bool_fun_fun$] : ! [v1: N_n_bool_fun_fun$] : ! [v2: N$] : ! % 45.85/7.14 [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (uwd$(v3, v2) = v1) | ~ (uwd$(v3, v2) = % 45.85/7.14 v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! % 45.85/7.14 [v2: N$] : ! [v3: A_b_vec_n_vec$] : (v1 = v0 | ~ (interchange_rows$(v3, v2) % 45.85/7.14 = v1) | ~ (interchange_rows$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 A_a_b_vec_n_vec_fun$] : ! [v1: A_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! % 45.85/7.14 [v3: A_b_vec_n_vec$] : (v1 = v0 | ~ (mult_row$(v3, v2) = v1) | ~ % 45.85/7.14 (mult_row$(v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_fun$] : ! [v2: A_b_vec_n_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | % 45.85/7.14 ~ (uuy$(v3, v2) = v1) | ~ (uuy$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: % 45.85/7.14 A_n_vec_n_vec$] : ! [v3: A_a_b_vec_fun$] : (v1 = v0 | ~ (uva$(v3, v2) = % 45.85/7.14 v1) | ~ (uva$(v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.14 A_b_vec_a_b_vec_fun$] : (v1 = v0 | ~ (uvc$(v3, v2) = v1) | ~ (uvc$(v3, v2) % 45.85/7.14 = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: % 45.85/7.14 A_n_vec_n_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (uve$(v3, v2) = v1) | ~ % 45.85/7.14 (uve$(v3, v2) = v0)) & ! [v0: B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : % 45.85/7.14 ! [v2: A_b_vec_b_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (uvg$(v3, v2) = v1) % 45.85/7.14 | ~ (uvg$(v3, v2) = v0)) & ! [v0: N_a_n_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_n_vec_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_a_n_vec_fun$] : % 45.85/7.14 (v1 = v0 | ~ (uvi$(v3, v2) = v1) | ~ (uvi$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 N_a_b_vec_b_vec_fun$] : ! [v1: N_a_b_vec_b_vec_fun$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec$] : ! [v3: A_a_b_vec_fun$] : (v1 = v0 | ~ (uvk$(v3, v2) = % 45.85/7.14 v1) | ~ (uvk$(v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_n_vec_fun$] : ! [v2: A_b_vec_n_vec_n_vec$] : ! [v3: A_b_vec_a_fun$] : % 45.85/7.14 (v1 = v0 | ~ (uvm$(v3, v2) = v1) | ~ (uvm$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec_n_vec$] : % 45.85/7.14 ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ (uvo$(v3, v2) = v1) | ~ (uvo$(v3, v2) % 45.85/7.14 = v0)) & ! [v0: N_a_b_vec_n_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_n_vec_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : ! [v3: % 45.85/7.14 A_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (uvq$(v3, v2) = v1) | ~ (uvq$(v3, v2) % 45.85/7.14 = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: A_b_vec$] : ! % 45.85/7.14 [v3: A_b_vec$] : (v1 = v0 | ~ (uxn$(v3, v2) = v1) | ~ (uxn$(v3, v2) = v0)) & % 45.85/7.14 ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec$] % 45.85/7.14 : (v1 = v0 | ~ (uxl$(v3, v2) = v1) | ~ (uxl$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: A_b_vec_b_vec$] : ! % 45.85/7.14 [v3: A_b_vec_b_vec$] : (v1 = v0 | ~ (uxk$(v3, v2) = v1) | ~ (uxk$(v3, v2) = % 45.85/7.14 v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec$] : ! [v3: A_b_vec_n_vec$] : (v1 = v0 | ~ (uxo$(v3, v2) = % 45.85/7.14 v1) | ~ (uxo$(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! % 45.85/7.14 [v2: A_n_vec$] : ! [v3: A_n_vec_a_n_vec_fun$] : (v1 = v0 | ~ (fun_app$p(v3, % 45.85/7.14 v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.14 [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : ! [v3: A_n_vec_n_vec$] : (v1 % 45.85/7.14 = v0 | ~ (uxj$(v3, v2) = v1) | ~ (uxj$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: A_b_vec_n_vec$] : ! % 45.85/7.14 [v3: A_b_vec_n_vec_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = % 45.85/7.14 v1) | ~ (fun_app$o(v3, v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! % 45.85/7.14 [v1: N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec_n_vec$] : ! [v3: % 45.85/7.14 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uxm$(v3, v2) = v1) | ~ (uxm$(v3, v2) % 45.85/7.14 = v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: A$] : % 45.85/7.14 ! [v3: A_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ % 45.85/7.14 (fun_app$n(v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_fun$] : ! [v2: A_b_vec_n_vec$] : ! [v3: A_b_vec_n_vec$] : (v1 = % 45.85/7.14 v0 | ~ (uua$(v3, v2) = v1) | ~ (uua$(v3, v2) = v0)) & ! [v0: A$] : ! % 45.85/7.14 [v1: A$] : ! [v2: N$] : ! [v3: N_a_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) % 45.85/7.14 = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 45.85/7.14 A$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) | ~ % 45.85/7.14 (fun_app$m(v3, v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: % 45.85/7.14 A_b_vec$] : ! [v3: A_b_vec_a_b_vec_fun$] : (v1 = v0 | ~ (fun_app$k(v3, v2) % 45.85/7.14 = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! % 45.85/7.14 [v1: A_b_vec_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N_a_b_vec_n_vec_n_vec_fun$] % 45.85/7.14 : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! % 45.85/7.14 [v0: N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: N$] : ! % 45.85/7.14 [v3: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uwl$(v3, v2) = v1) | ~ (uwl$(v3, % 45.85/7.14 v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: B$] : ! % 45.85/7.14 [v3: B_a_n_vec_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = v1) | ~ % 45.85/7.14 (fun_app$i(v3, v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: % 45.85/7.14 B$] : ! [v3: A_b_vec$] : (v1 = v0 | ~ (uwn$(v3, v2) = v1) | ~ (uwn$(v3, % 45.85/7.14 v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 45.85/7.14 N$] : ! [v3: N_a_n_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) % 45.85/7.14 | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_n_vec_fun$] : ! [v2: N$] : ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (uwp$(v3, v2) = v1) | ~ (uwp$(v3, v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! % 45.85/7.14 [v1: A_b_vec_b_vec$] : ! [v2: N$] : ! [v3: N_a_b_vec_b_vec_fun$] : (v1 = v0 % 45.85/7.14 | ~ (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 45.85/7.14 B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: N$] : ! [v3: % 45.85/7.14 A_b_vec_n_vec$] : (v1 = v0 | ~ (uwr$(v3, v2) = v1) | ~ (uwr$(v3, v2) = % 45.85/7.14 v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.14 N_a_n_vec_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | ~ (fun_app$f(v3, % 45.85/7.14 v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! % 45.85/7.14 [v3: A_n_vec$] : (v1 = v0 | ~ (uwt$(v3, v2) = v1) | ~ (uwt$(v3, v2) = v0)) & % 45.85/7.14 ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: B$] : ! [v3: B_a_b_vec_fun$] % 45.85/7.14 : (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! % 45.85/7.14 [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: B$] : ! [v3: A_b_vec$] : (v1 = % 45.85/7.14 v0 | ~ (uwv$(v3, v2) = v1) | ~ (uwv$(v3, v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.14 N_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 45.85/7.14 (fun_app$d(v3, v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_fun$] : ! [v2: N$] : ! [v3: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (uwx$(v3, v2) = v1) | ~ (uwx$(v3, v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: % 45.85/7.14 B_a_fun$] : ! [v2: N$] : ! [v3: A_n_vec$] : (v1 = v0 | ~ (uwz$(v3, v2) = % 45.85/7.14 v1) | ~ (uwz$(v3, v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: % 45.85/7.14 N_bool_fun$] : ! [v2: N$] : ! [v3: N_n_bool_fun_fun$] : (v1 = v0 | ~ % 45.85/7.14 (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: % 45.85/7.14 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: N$] : ! [v3: % 45.85/7.14 N_bool_fun$] : (v1 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) % 45.85/7.14 = v0)) & ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.14 N_a_b_vec_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, % 45.85/7.14 v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: B$] : ! [v3: B_a_fun$] % 45.85/7.14 : (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! % 45.85/7.14 [v0: A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (times$d(v2) = v1) | ~ (times$d(v2) = % 45.85/7.14 v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: % 45.85/7.14 A_n_vec$] : (v1 = v0 | ~ (columnvector$g(v2) = v1) | ~ (columnvector$g(v2) % 45.85/7.14 = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : % 45.85/7.14 ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ (columnvector$f(v2) = v1) | ~ % 45.85/7.14 (columnvector$f(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 45.85/7.14 A_b_vec_b_vec$] : ! [v2: A_b_vec$] : (v1 = v0 | ~ (columnvector$e(v2) = % 45.85/7.14 v1) | ~ (columnvector$e(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 45.85/7.14 A_n_vec_n_vec$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (columnvector$d(v2) = % 45.85/7.14 v1) | ~ (columnvector$d(v2) = v0)) & ! [v0: A_b_vec_b_vec_n_vec$] : ! % 45.85/7.14 [v1: A_b_vec_b_vec_n_vec$] : ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (columnvector$c(v2) = v1) | ~ (columnvector$c(v2) = v0)) & ! [v0: % 45.85/7.14 A_n_vec_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec_n_vec$] : ! [v2: % 45.85/7.14 A_n_vec_n_vec$] : (v1 = v0 | ~ (columnvector$b(v2) = v1) | ~ % 45.85/7.14 (columnvector$b(v2) = v0)) & ! [v0: A_n_vec_b_vec$] : ! [v1: % 45.85/7.14 A_n_vec_b_vec$] : ! [v2: A_b_vec$] : (v1 = v0 | ~ (columnvector$a(v2) = % 45.85/7.14 v1) | ~ (columnvector$a(v2) = v0)) & ! [v0: A_n_vec_b_vec$] : ! [v1: % 45.85/7.14 A_n_vec_b_vec$] : ! [v2: B_a_n_vec_fun$] : (v1 = v0 | ~ (vec_lambda$i(v2) % 45.85/7.14 = v1) | ~ (vec_lambda$i(v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec_n_vec$] % 45.85/7.14 : ! [v1: A_b_vec_n_vec_n_vec_n_vec$] : ! [v2: A_b_vec_n_vec_n_vec$] : (v1 = % 45.85/7.14 v0 | ~ (columnvector$(v2) = v1) | ~ (columnvector$(v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: A_b_vec$] : (v1 = v0 | % 45.85/7.14 ~ (rowvector$c(v2) = v1) | ~ (rowvector$c(v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec$] : (v1 = v0 | ~ (rowvector$b(v2) = v1) | ~ (rowvector$b(v2) % 45.85/7.14 = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] : ! [v2: % 45.85/7.14 A_b_vec$] : (v1 = v0 | ~ (rowvector$a(v2) = v1) | ~ (rowvector$a(v2) = % 45.85/7.14 v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 45.85/7.14 A_n_vec$] : (v1 = v0 | ~ (rowvector$(v2) = v1) | ~ (rowvector$(v2) = v0)) % 45.85/7.14 & ! [v0: A_b_vec_n_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec_n_vec$] : % 45.85/7.14 ! [v2: N_a_b_vec_n_vec_n_vec_fun$] : (v1 = v0 | ~ (vec_lambda$h(v2) = v1) | % 45.85/7.14 ~ (vec_lambda$h(v2) = v0)) & ! [v0: A_b_vec_b_vec_n_vec$] : ! [v1: % 45.85/7.14 A_b_vec_b_vec_n_vec$] : ! [v2: N_a_b_vec_b_vec_fun$] : (v1 = v0 | ~ % 45.85/7.14 (vec_lambda$g(v2) = v1) | ~ (vec_lambda$g(v2) = v0)) & ! [v0: % 45.85/7.14 A_n_vec_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec_n_vec$] : ! [v2: % 45.85/7.14 N_a_n_vec_n_vec_fun$] : (v1 = v0 | ~ (vec_lambda$f(v2) = v1) | ~ % 45.85/7.14 (vec_lambda$f(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: A_b_vec_b_vec$] % 45.85/7.14 : ! [v2: A_b_vec_b_vec$] : (v1 = v0 | ~ (uminus$f(v2) = v1) | ~ % 45.85/7.14 (uminus$f(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : % 45.85/7.14 ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (uminus$e(v2) = v1) | ~ (uminus$e(v2) % 45.85/7.14 = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! [v1: A_b_vec_n_vec_n_vec$] : % 45.85/7.14 ! [v2: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uminus$d(v2) = v1) | ~ % 45.85/7.14 (uminus$d(v2) = v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : % 45.85/7.14 (v1 = v0 | ~ (divide$(v2) = v1) | ~ (divide$(v2) = v0)) & ! [v0: N$] : ! % 45.85/7.14 [v1: N$] : ! [v2: N_bool_fun$] : (v1 = v0 | ~ (least$(v2) = v1) | ~ % 45.85/7.14 (least$(v2) = v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : % 45.85/7.14 (v1 = v0 | ~ (times$c(v2) = v1) | ~ (times$c(v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_a_b_vec_fun$] : ! [v1: A_b_vec_a_b_vec_fun$] : ! [v2: A_b_vec$] : % 45.85/7.14 (v1 = v0 | ~ (times$b(v2) = v1) | ~ (times$b(v2) = v0)) & ! [v0: % 45.85/7.14 A_n_vec_a_n_vec_fun$] : ! [v1: A_n_vec_a_n_vec_fun$] : ! [v2: A_n_vec$] : % 45.85/7.14 (v1 = v0 | ~ (times$a(v2) = v1) | ~ (times$a(v2) = v0)) & ! [v0: % 45.85/7.14 A_b_vec_n_vec_a_b_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 A_b_vec_n_vec_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (times$(v2) = v1) | ~ (times$(v2) = v0)) & ! [v0: B_a_b_vec_fun$] : ! % 45.85/7.14 [v1: B_a_b_vec_fun$] : ! [v2: A_b_vec$] : (v1 = v0 | ~ (uwi$(v2) = v1) | ~ % 45.85/7.14 (uwi$(v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! % 45.85/7.14 [v2: A_b_vec$] : (v1 = v0 | ~ (uwk$(v2) = v1) | ~ (uwk$(v2) = v0)) & ! [v0: % 45.85/7.14 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | % 45.85/7.14 ~ (uwh$(v2) = v1) | ~ (uwh$(v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : ! % 45.85/7.14 [v1: N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ (uwj$(v2) % 45.85/7.14 = v1) | ~ (uwj$(v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! % 45.85/7.14 [v2: A_b_vec$] : (v1 = v0 | ~ (uuf$(v2) = v1) | ~ (uuf$(v2) = v0)) & ! [v0: % 45.85/7.14 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (uud$(v2) % 45.85/7.14 = v1) | ~ (uud$(v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! % 45.85/7.14 [v2: A_n_vec$] : (v1 = v0 | ~ (vec_nth$e(v2) = v1) | ~ (vec_nth$e(v2) = v0)) % 45.85/7.14 & ! [v0: B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: A_b_vec_b_vec$] % 45.85/7.14 : (v1 = v0 | ~ (uuc$(v2) = v1) | ~ (uuc$(v2) = v0)) & ! [v0: % 45.85/7.14 B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: A_b_vec_b_vec$] : (v1 = % 45.85/7.14 v0 | ~ (vec_nth$d(v2) = v1) | ~ (vec_nth$d(v2) = v0)) & ! [v0: % 45.85/7.14 N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = % 45.85/7.14 v0 | ~ (uug$(v2) = v1) | ~ (uug$(v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! % 45.85/7.14 [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (uub$(v2) = v1) % 45.85/7.14 | ~ (uub$(v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : % 45.85/7.14 ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$c(v2) = v1) | ~ % 45.85/7.14 (vec_nth$c(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: % 45.85/7.14 A_n_vec$] : (v1 = v0 | ~ (uminus$a(v2) = v1) | ~ (uminus$a(v2) = v0)) & ! % 45.85/7.14 [v0: N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (uue$(v2) = v1) | ~ (uue$(v2) = v0)) % 45.85/7.14 & ! [v0: N_a_b_vec_n_vec_fun$] : ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: % 45.85/7.14 A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$b(v2) = v1) | ~ % 45.85/7.14 (vec_nth$b(v2) = v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : % 45.85/7.14 ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ (uminus$(v2) = v1) | ~ (uminus$(v2) = % 45.85/7.14 v0)) & ! [v0: N_a_b_vec_n_vec_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_n_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (uwm$(v2) = v1) | ~ (uwm$(v2) = v0)) & ! [v0: A_b_vec_n_vec_n_vec$] : ! % 45.85/7.14 [v1: A_b_vec_n_vec_n_vec$] : ! [v2: N_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ % 45.85/7.14 (vec_lambda$e(v2) = v1) | ~ (vec_lambda$e(v2) = v0)) & ! [v0: % 45.85/7.14 B_a_n_vec_fun$] : ! [v1: B_a_n_vec_fun$] : ! [v2: A_b_vec$] : (v1 = v0 | % 45.85/7.14 ~ (uwo$(v2) = v1) | ~ (uwo$(v2) = v0)) & ! [v0: N_a_n_vec_n_vec_fun$] : ! % 45.85/7.14 [v1: N_a_n_vec_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (uwq$(v2) % 45.85/7.14 = v1) | ~ (uwq$(v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 45.85/7.14 A_n_vec_n_vec$] : ! [v2: N_a_n_vec_fun$] : (v1 = v0 | ~ (vec_lambda$d(v2) % 45.85/7.14 = v1) | ~ (vec_lambda$d(v2) = v0)) & ! [v0: N_a_b_vec_b_vec_fun$] : ! % 45.85/7.14 [v1: N_a_b_vec_b_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ (uws$(v2) % 45.85/7.14 = v1) | ~ (uws$(v2) = v0)) & ! [v0: A_b_vec_b_vec$] : ! [v1: % 45.85/7.14 A_b_vec_b_vec$] : ! [v2: B_a_b_vec_fun$] : (v1 = v0 | ~ (vec_lambda$c(v2) % 45.85/7.14 = v1) | ~ (vec_lambda$c(v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: % 45.85/7.14 N_a_n_vec_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (uwu$(v2) = v1) | ~ % 45.85/7.14 (uwu$(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: N_a_fun$] % 45.85/7.14 : (v1 = v0 | ~ (vec_lambda$b(v2) = v1) | ~ (vec_lambda$b(v2) = v0)) & ! % 45.85/7.14 [v0: B_a_b_vec_fun$] : ! [v1: B_a_b_vec_fun$] : ! [v2: A_b_vec$] : (v1 = v0 % 45.85/7.14 | ~ (uww$(v2) = v1) | ~ (uww$(v2) = v0)) & ! [v0: N_a_b_vec_n_vec_fun$] : % 45.85/7.14 ! [v1: N_a_b_vec_n_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = v0 | ~ % 45.85/7.14 (uwy$(v2) = v1) | ~ (uwy$(v2) = v0)) & ! [v0: A_b_vec_n_vec$] : ! [v1: % 45.85/7.14 A_b_vec_n_vec$] : ! [v2: N_a_b_vec_fun$] : (v1 = v0 | ~ (vec_lambda$a(v2) % 45.85/7.14 = v1) | ~ (vec_lambda$a(v2) = v0)) & ! [v0: N_a_b_vec_fun$] : ! [v1: % 45.85/7.14 N_a_b_vec_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ (uxa$(v2) = v1) | ~ % 45.85/7.14 (uxa$(v2) = v0)) & ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: B_a_fun$] % 45.85/7.14 : (v1 = v0 | ~ (vec_lambda$(v2) = v1) | ~ (vec_lambda$(v2) = v0)) & ! [v0: % 45.85/7.14 N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: A_b_vec_n_vec$] : (v1 = % 45.85/7.14 v0 | ~ (vec_nth$a(v2) = v1) | ~ (vec_nth$a(v2) = v0)) & ! [v0: B_a_fun$] % 45.85/7.14 : ! [v1: B_a_fun$] : ! [v2: A_b_vec$] : (v1 = v0 | ~ (vec_nth$(v2) = v1) | % 45.85/7.14 ~ (vec_nth$(v2) = v0)) % 45.85/7.14 % 45.85/7.14 Further assumptions not needed in the proof: % 45.85/7.14 -------------------------------------------- % 45.85/7.14 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom106, % 45.85/7.14 axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, axiom112, axiom113, % 45.85/7.14 axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, axiom12, axiom120, % 45.85/7.14 axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, axiom128, % 45.85/7.14 axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, axiom135, % 45.85/7.14 axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, axiom142, % 45.85/7.14 axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, % 45.85/7.14 axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, % 45.85/7.14 axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, axiom164, % 45.85/7.14 axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, % 45.85/7.14 axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom179, % 45.85/7.14 axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, % 45.85/7.14 axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 45.85/7.14 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 45.85/7.14 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 45.85/7.14 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 45.85/7.14 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 45.85/7.14 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 45.85/7.14 axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, % 45.85/7.14 axiom237, axiom238, axiom239, axiom24, axiom241, axiom242, axiom243, axiom244, % 45.85/7.14 axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, axiom251, % 45.85/7.14 axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, % 45.85/7.14 axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, axiom266, % 45.85/7.14 axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, axiom273, % 45.85/7.14 axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, axiom280, % 45.85/7.14 axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, % 45.85/7.14 axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, % 45.85/7.14 axiom296, axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, % 45.85/7.14 axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, % 45.85/7.14 axiom31, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, % 45.85/7.14 axiom317, axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, % 45.85/7.14 axiom324, axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, % 45.85/7.14 axiom331, axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, % 45.85/7.14 axiom339, axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, % 45.85/7.14 axiom346, axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, % 45.85/7.14 axiom353, axiom354, axiom355, axiom356, axiom357, axiom358, axiom359, axiom36, % 45.85/7.14 axiom360, axiom361, axiom362, axiom363, axiom364, axiom365, axiom366, axiom367, % 45.85/7.14 axiom368, axiom369, axiom37, axiom370, axiom371, axiom372, axiom373, axiom374, % 45.85/7.14 axiom375, axiom376, axiom377, axiom378, axiom379, axiom38, axiom380, axiom381, % 45.85/7.14 axiom382, axiom383, axiom384, axiom385, axiom386, axiom387, axiom388, axiom389, % 45.85/7.14 axiom39, axiom390, axiom391, axiom392, axiom393, axiom394, axiom395, axiom396, % 45.85/7.14 axiom397, axiom398, axiom399, axiom4, axiom40, axiom400, axiom401, axiom402, % 45.85/7.14 axiom403, axiom404, axiom405, axiom406, axiom407, axiom408, axiom409, axiom41, % 45.85/7.14 axiom410, axiom411, axiom412, axiom413, axiom414, axiom415, axiom416, axiom417, % 45.85/7.14 axiom418, axiom419, axiom42, axiom420, axiom421, axiom422, axiom423, axiom424, % 45.85/7.14 axiom425, axiom426, axiom427, axiom428, axiom429, axiom43, axiom430, axiom431, % 45.85/7.14 axiom432, axiom433, axiom434, axiom435, axiom436, axiom437, axiom438, axiom439, % 45.85/7.14 axiom440, axiom441, axiom442, axiom443, axiom444, axiom445, axiom446, axiom447, % 45.85/7.14 axiom448, axiom449, axiom450, axiom451, axiom452, axiom453, axiom454, axiom455, % 45.85/7.14 axiom456, axiom457, axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, % 45.85/7.14 axiom463, axiom464, axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, % 45.85/7.14 axiom470, axiom471, axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, % 45.85/7.14 axiom478, axiom479, axiom48, axiom480, axiom481, axiom482, axiom483, axiom484, % 45.85/7.14 axiom485, axiom486, axiom487, axiom488, axiom489, axiom49, axiom490, axiom491, % 45.85/7.14 axiom492, axiom493, axiom494, axiom495, axiom496, axiom497, axiom498, axiom499, % 45.85/7.14 axiom5, axiom50, axiom500, axiom501, axiom51, axiom52, axiom53, axiom54, % 45.85/7.14 axiom55, axiom56, axiom57, axiom58, axiom59, axiom6, axiom60, axiom61, axiom62, % 45.85/7.14 axiom63, axiom64, axiom65, axiom66, axiom67, axiom68, axiom69, axiom7, axiom70, % 45.85/7.14 axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, axiom78, axiom79, % 45.85/7.14 axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, axiom87, % 45.85/7.14 axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, % 45.85/7.14 axiom96, axiom97, axiom98, axiom99, formula_503, formula_504 % 45.85/7.14 % 45.85/7.14 Those formulas are unsatisfiable: % 45.85/7.14 --------------------------------- % 45.85/7.14 % 45.85/7.14 Begin of proof % 45.85/7.14 | % 45.85/7.14 | ALPHA: (axiom44) implies: % 45.85/7.15 | (1) ? [v0: A_a_fun$] : (divide$(one$) = v0 & A_a_fun$(v0) & ! [v1: % 45.85/7.15 | A_b_vec_n_vec$] : ! [v2: N$] : ! [v3: B$] : ! [v4: N$] : ! [v5: % 45.85/7.15 | N_a_b_vec_n_vec_fun$] : ! [v6: N_bool_fun$] : ! [v7: N$] : ! % 45.85/7.15 | [v8: A_b_vec_n_vec$] : ! [v9: A_a_b_vec_n_vec_fun$] : ! [v10: % 45.85/7.15 | N_a_b_vec_fun$] : ! [v11: A_b_vec$] : ! [v12: B_a_fun$] : ! % 45.85/7.15 | [v13: A$] : ! [v14: A$] : ! [v15: A_b_vec_n_vec$] : ! [v16: % 45.85/7.15 | A_a_b_vec_n_vec_fun$] : ! [v17: A_b_vec$] : ! [v18: B_a_fun$] : % 45.85/7.15 | ! [v19: A$] : ! [v20: A$] : ! [v21: A_b_vec_n_vec$] : ! [v22: % 45.85/7.15 | N_a_b_vec_fun$] : ! [v23: A_b_vec$] : (v4 = v2 | ~ % 45.85/7.15 | (interchange_rows$(v1, v2) = v5) | ~ (uwf$(v1, v2, v3) = v6) | ~ % 45.85/7.15 | (least$(v6) = v7) | ~ (mult_row$(v8, v2) = v9) | ~ (row_add$(v15, % 45.85/7.15 | v4, v2) = v16) | ~ (fun_app$n(v16, v20) = v21) | ~ % 45.85/7.15 | (fun_app$n(v9, v14) = v15) | ~ (fun_app$m(v0, v13) = v14) | ~ % 45.85/7.15 | (fun_app$m(uminus$c, v19) = v20) | ~ (fun_app$d(v5, v7) = v8) | ~ % 45.85/7.15 | (vec_nth$a(v21) = v22) | ~ (vec_nth$a(v8) = v10) | ~ % 45.85/7.15 | (fun_app$b(v22, v4) = v23) | ~ (fun_app$b(v10, v4) = v17) | ~ % 45.85/7.15 | (fun_app$b(v10, v2) = v11) | ~ (vec_nth$(v17) = v18) | ~ % 45.85/7.15 | (vec_nth$(v11) = v12) | ~ (fun_app$a(v18, v3) = v19) | ~ % 45.85/7.15 | (fun_app$a(v12, v3) = v13) | ~ N$(v4) | ~ N$(v2) | ~ B$(v3) | ~ % 45.85/7.15 | A_b_vec_n_vec$(v1) | ? [v24: N_a_b_vec_fun$] : (uwg$(v1, v2, v3) = % 45.85/7.15 | v24 & fun_app$b(v24, v4) = v23 & N_a_b_vec_fun$(v24) & % 45.85/7.15 | A_b_vec$(v23))) & ! [v1: A_b_vec_n_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.15 | B$] : ! [v4: N_a_b_vec_n_vec_fun$] : ! [v5: N_bool_fun$] : ! % 45.85/7.15 | [v6: N$] : ! [v7: A_b_vec_n_vec$] : ! [v8: A_a_b_vec_n_vec_fun$] : % 45.85/7.15 | ! [v9: N_a_b_vec_fun$] : ! [v10: A_b_vec$] : ! [v11: B_a_fun$] : ! % 45.85/7.15 | [v12: A$] : ! [v13: A$] : ! [v14: A_b_vec_n_vec$] : ! [v15: % 45.85/7.15 | N_a_b_vec_fun$] : ! [v16: A_b_vec$] : ( ~ (interchange_rows$(v1, % 45.85/7.15 | v2) = v4) | ~ (uwf$(v1, v2, v3) = v5) | ~ (least$(v5) = v6) | % 45.85/7.15 | ~ (mult_row$(v7, v2) = v8) | ~ (fun_app$n(v8, v13) = v14) | ~ % 45.85/7.15 | (fun_app$m(v0, v12) = v13) | ~ (fun_app$d(v4, v6) = v7) | ~ % 45.85/7.15 | (vec_nth$a(v14) = v15) | ~ (vec_nth$a(v7) = v9) | ~ % 45.85/7.15 | (fun_app$b(v15, v2) = v16) | ~ (fun_app$b(v9, v2) = v10) | ~ % 45.85/7.15 | (vec_nth$(v10) = v11) | ~ (fun_app$a(v11, v3) = v12) | ~ N$(v2) | % 45.85/7.15 | ~ B$(v3) | ~ A_b_vec_n_vec$(v1) | ? [v17: N_a_b_vec_fun$] : % 45.85/7.15 | (uwg$(v1, v2, v3) = v17 & fun_app$b(v17, v2) = v16 & % 45.85/7.15 | N_a_b_vec_fun$(v17) & A_b_vec$(v16)))) % 45.85/7.15 | % 45.85/7.15 | ALPHA: (axiom45) implies: % 45.85/7.15 | (2) ? [v0: A_a_fun$] : (divide$(one$) = v0 & A_a_fun$(v0) & ! [v1: % 45.85/7.15 | A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: % 45.85/7.15 | N_a_n_vec_n_vec_fun$] : ! [v6: N_n_bool_fun_fun$] : ! [v7: % 45.85/7.15 | N_bool_fun$] : ! [v8: N$] : ! [v9: A_n_vec_n_vec$] : ! [v10: % 45.85/7.15 | N_a_n_vec_fun$] : ! [v11: A_n_vec$] : ! [v12: N_a_fun$] : ! % 45.85/7.15 | [v13: A$] : ! [v14: A$] : ! [v15: A_n_vec_n_vec$] : ! [v16: % 45.85/7.15 | A_n_vec$] : ! [v17: N_a_fun$] : ! [v18: A$] : ! [v19: A$] : ! % 45.85/7.15 | [v20: A_n_vec_n_vec$] : ! [v21: N_a_n_vec_fun$] : ! [v22: A_n_vec$] % 45.85/7.15 | : (v4 = v2 | ~ (row_add$a(v15, v4, v2, v19) = v20) | ~ % 45.85/7.15 | (interchange_rows$a(v1, v2) = v5) | ~ (uwd$(v1, v2) = v6) | ~ % 45.85/7.15 | (mult_row$a(v9, v2, v14) = v15) | ~ (least$(v7) = v8) | ~ % 45.85/7.15 | (vec_nth$e(v16) = v17) | ~ (vec_nth$e(v11) = v12) | ~ % 45.85/7.15 | (fun_app$l(v17, v3) = v18) | ~ (fun_app$l(v12, v3) = v13) | ~ % 45.85/7.15 | (fun_app$m(v0, v13) = v14) | ~ (fun_app$m(uminus$c, v18) = v19) | % 45.85/7.15 | ~ (vec_nth$c(v20) = v21) | ~ (vec_nth$c(v9) = v10) | ~ % 45.85/7.15 | (fun_app$h(v5, v8) = v9) | ~ (fun_app$f(v21, v4) = v22) | ~ % 45.85/7.15 | (fun_app$f(v10, v4) = v16) | ~ (fun_app$f(v10, v2) = v11) | ~ % 45.85/7.15 | (fun_app$c(v6, v3) = v7) | ~ N$(v4) | ~ N$(v3) | ~ N$(v2) | ~ % 45.85/7.15 | A_n_vec_n_vec$(v1) | ? [v23: N_a_n_vec_fun$] : (uwe$(v1, v2, v3) = % 45.85/7.15 | v23 & fun_app$f(v23, v4) = v22 & A_n_vec$(v22) & % 45.85/7.15 | N_a_n_vec_fun$(v23))) & ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : % 45.85/7.15 | ! [v3: N$] : ! [v4: N_a_n_vec_n_vec_fun$] : ! [v5: % 45.85/7.15 | N_n_bool_fun_fun$] : ! [v6: N_bool_fun$] : ! [v7: N$] : ! [v8: % 45.85/7.15 | A_n_vec_n_vec$] : ! [v9: N_a_n_vec_fun$] : ! [v10: A_n_vec$] : ! % 45.85/7.15 | [v11: N_a_fun$] : ! [v12: A$] : ! [v13: A$] : ! [v14: % 45.85/7.15 | A_n_vec_n_vec$] : ! [v15: N_a_n_vec_fun$] : ! [v16: A_n_vec$] : ( % 45.85/7.15 | ~ (interchange_rows$a(v1, v2) = v4) | ~ (uwd$(v1, v2) = v5) | ~ % 45.85/7.15 | (mult_row$a(v8, v2, v13) = v14) | ~ (least$(v6) = v7) | ~ % 45.85/7.15 | (vec_nth$e(v10) = v11) | ~ (fun_app$l(v11, v3) = v12) | ~ % 45.85/7.15 | (fun_app$m(v0, v12) = v13) | ~ (vec_nth$c(v14) = v15) | ~ % 45.85/7.15 | (vec_nth$c(v8) = v9) | ~ (fun_app$h(v4, v7) = v8) | ~ % 45.85/7.15 | (fun_app$f(v15, v2) = v16) | ~ (fun_app$f(v9, v2) = v10) | ~ % 45.85/7.15 | (fun_app$c(v5, v3) = v6) | ~ N$(v3) | ~ N$(v2) | ~ % 45.85/7.15 | A_n_vec_n_vec$(v1) | ? [v17: N_a_n_vec_fun$] : (uwe$(v1, v2, v3) = % 45.85/7.15 | v17 & fun_app$f(v17, v2) = v16 & A_n_vec$(v16) & % 45.85/7.15 | N_a_n_vec_fun$(v17)))) % 45.85/7.15 | % 45.85/7.15 | ALPHA: (axiom105) implies: % 45.85/7.15 | (3) ? [v0: A_a_b_vec_n_vec_fun$] : ? [v1: A_a_fun$] : ? [v2: % 45.85/7.15 | N_a_b_vec_fun$] : ? [v3: A_b_vec$] : ? [v4: B_a_fun$] : ? [v5: A$] % 45.85/7.15 | : ? [v6: A$] : (divide$(one$) = v1 & mult_row$(interchange_A$, i$) = % 45.85/7.15 | v0 & fun_app$n(v0, v6) = a$a & fun_app$m(v1, v5) = v6 & % 45.85/7.15 | vec_nth$a(interchange_A$) = v2 & fun_app$b(v2, i$) = v3 & % 45.85/7.15 | vec_nth$(v3) = v4 & fun_app$a(v4, j$) = v5 & A_a_fun$(v1) & A$(v6) & % 45.85/7.15 | A$(v5) & N_a_b_vec_fun$(v2) & B_a_fun$(v4) & A_b_vec$(v3) & % 45.85/7.15 | A_a_b_vec_n_vec_fun$(v0)) % 45.85/7.15 | % 45.85/7.15 | ALPHA: (axiom240) implies: % 45.85/7.15 | (4) ? [v0: N$] : ? [v1: N_a_b_vec_fun$] : ? [v2: N_bool_fun$] : ? [v3: % 45.85/7.15 | N_a_b_vec_n_vec_fun$] : ? [v4: A_a_fun$] : ? [v5: A_b_vec_n_vec$] : % 45.85/7.15 | (gauss_Jordan_in_ij$(a$, i$, j$) = v5 & divide$(one$) = v4 & % 45.85/7.15 | interchange_rows$(a$, i$) = v3 & least$(uu$) = v0 & vec_nth$a(a$) = % 45.85/7.15 | v1 & fun_app$c(less_eq$, i$) = v2 & N_a_b_vec_n_vec_fun$(v3) & % 45.85/7.15 | N_bool_fun$(v2) & A_a_fun$(v4) & N_a_b_vec_fun$(v1) & N$(v0) & % 45.85/7.15 | A_b_vec_n_vec$(v5) & ! [v6: A_b_vec_n_vec$] : ! [v7: % 45.85/7.15 | A_b_vec_n_vec$] : ! [v8: N_a_b_vec_fun$] : ( ~ (uua$(v6, v7) = v8) % 45.85/7.15 | | ~ (fun_app$d(v3, v0) = v6) | ~ A_b_vec_n_vec$(v7) | ~ % 45.85/7.15 | A_b_vec_n_vec$(v6) | thesis$ | ? [v9: A_b_vec$] : ? [v10: % 45.85/7.15 | B_a_fun$] : ? [v11: A$] : ? [v12: any] : ? [v13: % 45.85/7.15 | A_a_b_vec_n_vec_fun$] : ? [v14: N_a_b_vec_fun$] : ? [v15: % 45.85/7.15 | A_b_vec$] : ? [v16: B_a_fun$] : ? [v17: A$] : ? [v18: A$] : ? % 45.85/7.15 | [v19: A_b_vec_n_vec$] : ? [v20: A_b_vec_n_vec$] : (mult_row$(v6, % 45.85/7.15 | i$) = v13 & fun_app$n(v13, v18) = v19 & fun_app$m(v4, v17) = % 45.85/7.15 | v18 & vec_lambda$a(v8) = v20 & vec_nth$a(v6) = v14 & fun_app$(v2, % 45.85/7.15 | v0) = v12 & fun_app$b(v14, i$) = v15 & fun_app$b(v1, v0) = v9 & % 45.85/7.15 | vec_nth$(v15) = v16 & vec_nth$(v9) = v10 & fun_app$a(v16, j$) = % 45.85/7.15 | v17 & fun_app$a(v10, j$) = v11 & A$(v18) & A$(v17) & A$(v11) & % 45.85/7.15 | N_a_b_vec_fun$(v14) & B_a_fun$(v16) & B_a_fun$(v10) & % 45.85/7.15 | A_b_vec$(v15) & A_b_vec$(v9) & A_a_b_vec_n_vec_fun$(v13) & % 45.85/7.15 | A_b_vec_n_vec$(v20) & A_b_vec_n_vec$(v19) & ( ~ (v20 = v5) | ~ % 45.85/7.15 | (v19 = v7) | ~ (v12 = 0) | v11 = zero$)))) % 45.85/7.15 | % 45.85/7.15 | ALPHA: (conjecture104) implies: % 45.85/7.15 | (5) ? [v0: A_a_b_vec_n_vec_fun$] : ? [v1: A_a_fun$] : ? [v2: % 45.85/7.15 | N_a_b_vec_fun$] : ? [v3: A_b_vec$] : ? [v4: B_a_fun$] : ? [v5: A$] % 45.85/7.15 | : ? [v6: A$] : ? [v7: A_b_vec_n_vec$] : ( ~ (v7 = a$a) & % 45.85/7.15 | divide$(one$) = v1 & mult_row$(interchange_A$, i$) = v0 & % 45.85/7.15 | fun_app$n(v0, v6) = v7 & fun_app$m(v1, v5) = v6 & % 45.85/7.15 | vec_nth$a(interchange_A$) = v2 & fun_app$b(v2, i$) = v3 & % 45.85/7.15 | vec_nth$(v3) = v4 & fun_app$a(v4, j$) = v5 & A_a_fun$(v1) & A$(v6) & % 45.85/7.15 | A$(v5) & N_a_b_vec_fun$(v2) & B_a_fun$(v4) & A_b_vec$(v3) & % 45.85/7.15 | A_a_b_vec_n_vec_fun$(v0) & A_b_vec_n_vec$(v7)) % 45.85/7.15 | % 45.85/7.15 | ALPHA: (function-axioms) implies: % 45.85/7.16 | (6) ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: A_b_vec$] : (v1 = v0 | % 45.85/7.16 | ~ (vec_nth$(v2) = v1) | ~ (vec_nth$(v2) = v0)) % 45.85/7.16 | (7) ! [v0: N_a_b_vec_fun$] : ! [v1: N_a_b_vec_fun$] : ! [v2: % 45.85/7.16 | A_b_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$a(v2) = v1) | ~ % 45.85/7.16 | (vec_nth$a(v2) = v0)) % 45.85/7.16 | (8) ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : (v1 = v0 | ~ % 45.85/7.16 | (divide$(v2) = v1) | ~ (divide$(v2) = v0)) % 45.85/7.16 | (9) ! [v0: A$] : ! [v1: A$] : ! [v2: B$] : ! [v3: B_a_fun$] : (v1 = v0 % 45.85/7.16 | | ~ (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) % 45.85/7.16 | (10) ! [v0: A_b_vec$] : ! [v1: A_b_vec$] : ! [v2: N$] : ! [v3: % 45.85/7.16 | N_a_b_vec_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ % 45.85/7.16 | (fun_app$b(v3, v2) = v0)) % 45.85/7.16 | (11) ! [v0: A$] : ! [v1: A$] : ! [v2: A$] : ! [v3: A_a_fun$] : (v1 = v0 % 45.85/7.16 | | ~ (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) % 45.85/7.16 | (12) ! [v0: A_b_vec_n_vec$] : ! [v1: A_b_vec_n_vec$] : ! [v2: A$] : ! % 45.85/7.16 | [v3: A_a_b_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | % 45.85/7.16 | ~ (fun_app$n(v3, v2) = v0)) % 45.85/7.16 | (13) ! [v0: A_a_b_vec_n_vec_fun$] : ! [v1: A_a_b_vec_n_vec_fun$] : ! % 45.85/7.16 | [v2: N$] : ! [v3: A_b_vec_n_vec$] : (v1 = v0 | ~ (mult_row$(v3, v2) % 45.85/7.16 | = v1) | ~ (mult_row$(v3, v2) = v0)) % 45.85/7.16 | % 45.85/7.16 | DELTA: instantiating (3) with fresh symbols all_611_0, all_611_1, all_611_2, % 45.85/7.16 | all_611_3, all_611_4, all_611_5, all_611_6 gives: % 45.85/7.16 | (14) divide$(one$) = all_611_5 & mult_row$(interchange_A$, i$) = all_611_6 % 45.85/7.16 | & fun_app$n(all_611_6, all_611_0) = a$a & fun_app$m(all_611_5, % 45.85/7.16 | all_611_1) = all_611_0 & vec_nth$a(interchange_A$) = all_611_4 & % 45.85/7.16 | fun_app$b(all_611_4, i$) = all_611_3 & vec_nth$(all_611_3) = all_611_2 % 45.85/7.16 | & fun_app$a(all_611_2, j$) = all_611_1 & A_a_fun$(all_611_5) & % 45.85/7.16 | A$(all_611_0) & A$(all_611_1) & N_a_b_vec_fun$(all_611_4) & % 45.85/7.16 | B_a_fun$(all_611_2) & A_b_vec$(all_611_3) & % 45.85/7.16 | A_a_b_vec_n_vec_fun$(all_611_6) % 45.85/7.16 | % 45.85/7.16 | ALPHA: (14) implies: % 45.85/7.16 | (15) fun_app$a(all_611_2, j$) = all_611_1 % 45.85/7.16 | (16) vec_nth$(all_611_3) = all_611_2 % 45.85/7.16 | (17) fun_app$b(all_611_4, i$) = all_611_3 % 45.85/7.16 | (18) vec_nth$a(interchange_A$) = all_611_4 % 45.85/7.16 | (19) fun_app$m(all_611_5, all_611_1) = all_611_0 % 45.85/7.16 | (20) fun_app$n(all_611_6, all_611_0) = a$a % 45.85/7.16 | (21) mult_row$(interchange_A$, i$) = all_611_6 % 45.85/7.16 | (22) divide$(one$) = all_611_5 % 45.85/7.16 | % 45.85/7.16 | DELTA: instantiating (5) with fresh symbols all_613_0, all_613_1, all_613_2, % 45.85/7.16 | all_613_3, all_613_4, all_613_5, all_613_6, all_613_7 gives: % 45.85/7.16 | (23) ~ (all_613_0 = a$a) & divide$(one$) = all_613_6 & % 45.85/7.16 | mult_row$(interchange_A$, i$) = all_613_7 & fun_app$n(all_613_7, % 45.85/7.16 | all_613_1) = all_613_0 & fun_app$m(all_613_6, all_613_2) = all_613_1 % 45.85/7.16 | & vec_nth$a(interchange_A$) = all_613_5 & fun_app$b(all_613_5, i$) = % 45.85/7.16 | all_613_4 & vec_nth$(all_613_4) = all_613_3 & fun_app$a(all_613_3, j$) % 45.85/7.16 | = all_613_2 & A_a_fun$(all_613_6) & A$(all_613_1) & A$(all_613_2) & % 45.85/7.16 | N_a_b_vec_fun$(all_613_5) & B_a_fun$(all_613_3) & A_b_vec$(all_613_4) % 45.85/7.16 | & A_a_b_vec_n_vec_fun$(all_613_7) & A_b_vec_n_vec$(all_613_0) % 45.85/7.16 | % 45.85/7.16 | ALPHA: (23) implies: % 45.85/7.16 | (24) ~ (all_613_0 = a$a) % 45.85/7.16 | (25) fun_app$a(all_613_3, j$) = all_613_2 % 45.85/7.16 | (26) vec_nth$(all_613_4) = all_613_3 % 45.85/7.16 | (27) fun_app$b(all_613_5, i$) = all_613_4 % 45.85/7.16 | (28) vec_nth$a(interchange_A$) = all_613_5 % 45.85/7.16 | (29) fun_app$m(all_613_6, all_613_2) = all_613_1 % 45.85/7.16 | (30) fun_app$n(all_613_7, all_613_1) = all_613_0 % 45.85/7.16 | (31) mult_row$(interchange_A$, i$) = all_613_7 % 45.85/7.16 | (32) divide$(one$) = all_613_6 % 45.85/7.16 | % 45.85/7.16 | DELTA: instantiating (4) with fresh symbols all_618_0, all_618_1, all_618_2, % 45.85/7.16 | all_618_3, all_618_4, all_618_5 gives: % 45.85/7.17 | (33) gauss_Jordan_in_ij$(a$, i$, j$) = all_618_0 & divide$(one$) = % 45.85/7.17 | all_618_1 & interchange_rows$(a$, i$) = all_618_2 & least$(uu$) = % 45.85/7.17 | all_618_5 & vec_nth$a(a$) = all_618_4 & fun_app$c(less_eq$, i$) = % 45.85/7.17 | all_618_3 & N_a_b_vec_n_vec_fun$(all_618_2) & N_bool_fun$(all_618_3) & % 45.85/7.17 | A_a_fun$(all_618_1) & N_a_b_vec_fun$(all_618_4) & N$(all_618_5) & % 45.85/7.17 | A_b_vec_n_vec$(all_618_0) & ! [v0: A_b_vec_n_vec$] : ! [v1: % 45.85/7.17 | A_b_vec_n_vec$] : ! [v2: N_a_b_vec_fun$] : ( ~ (uua$(v0, v1) = v2) % 45.85/7.17 | | ~ (fun_app$d(all_618_2, all_618_5) = v0) | ~ A_b_vec_n_vec$(v1) % 45.85/7.17 | | ~ A_b_vec_n_vec$(v0) | thesis$ | ? [v3: A_b_vec$] : ? [v4: % 45.85/7.17 | B_a_fun$] : ? [v5: A$] : ? [v6: any] : ? [v7: % 45.85/7.17 | A_a_b_vec_n_vec_fun$] : ? [v8: N_a_b_vec_fun$] : ? [v9: % 45.85/7.17 | A_b_vec$] : ? [v10: B_a_fun$] : ? [v11: A$] : ? [v12: A$] : ? % 45.85/7.17 | [v13: A_b_vec_n_vec$] : ? [v14: A_b_vec_n_vec$] : (mult_row$(v0, % 45.85/7.17 | i$) = v7 & fun_app$n(v7, v12) = v13 & fun_app$m(all_618_1, v11) % 45.85/7.17 | = v12 & vec_lambda$a(v2) = v14 & vec_nth$a(v0) = v8 & % 45.85/7.17 | fun_app$(all_618_3, all_618_5) = v6 & fun_app$b(v8, i$) = v9 & % 45.85/7.17 | fun_app$b(all_618_4, all_618_5) = v3 & vec_nth$(v9) = v10 & % 46.59/7.17 | vec_nth$(v3) = v4 & fun_app$a(v10, j$) = v11 & fun_app$a(v4, j$) = % 46.59/7.17 | v5 & A$(v12) & A$(v11) & A$(v5) & N_a_b_vec_fun$(v8) & % 46.59/7.17 | B_a_fun$(v10) & B_a_fun$(v4) & A_b_vec$(v9) & A_b_vec$(v3) & % 46.59/7.17 | A_a_b_vec_n_vec_fun$(v7) & A_b_vec_n_vec$(v14) & % 46.59/7.17 | A_b_vec_n_vec$(v13) & ( ~ (v14 = all_618_0) | ~ (v13 = v1) | ~ % 46.59/7.17 | (v6 = 0) | v5 = zero$))) % 46.59/7.17 | % 46.59/7.17 | ALPHA: (33) implies: % 46.59/7.17 | (34) divide$(one$) = all_618_1 % 46.59/7.17 | % 46.59/7.17 | DELTA: instantiating (2) with fresh symbol all_621_0 gives: % 46.59/7.17 | (35) divide$(one$) = all_621_0 & A_a_fun$(all_621_0) & ! [v0: % 46.59/7.17 | A_n_vec_n_vec$] : ! [v1: N$] : ! [v2: N$] : ! [v3: N$] : ! [v4: % 46.59/7.17 | N_a_n_vec_n_vec_fun$] : ! [v5: N_n_bool_fun_fun$] : ! [v6: % 46.59/7.17 | N_bool_fun$] : ! [v7: N$] : ! [v8: A_n_vec_n_vec$] : ! [v9: % 46.59/7.17 | N_a_n_vec_fun$] : ! [v10: A_n_vec$] : ! [v11: N_a_fun$] : ! [v12: % 46.59/7.17 | A$] : ! [v13: A$] : ! [v14: A_n_vec_n_vec$] : ! [v15: A_n_vec$] : % 46.59/7.17 | ! [v16: N_a_fun$] : ! [v17: A$] : ! [v18: A$] : ! [v19: % 46.59/7.17 | A_n_vec_n_vec$] : ! [v20: N_a_n_vec_fun$] : ! [v21: A_n_vec$] : % 46.59/7.17 | (v3 = v1 | ~ (row_add$a(v14, v3, v1, v18) = v19) | ~ % 46.59/7.17 | (interchange_rows$a(v0, v1) = v4) | ~ (uwd$(v0, v1) = v5) | ~ % 46.59/7.17 | (mult_row$a(v8, v1, v13) = v14) | ~ (least$(v6) = v7) | ~ % 46.59/7.17 | (vec_nth$e(v15) = v16) | ~ (vec_nth$e(v10) = v11) | ~ % 46.59/7.17 | (fun_app$l(v16, v2) = v17) | ~ (fun_app$l(v11, v2) = v12) | ~ % 46.59/7.17 | (fun_app$m(all_621_0, v12) = v13) | ~ (fun_app$m(uminus$c, v17) = % 46.59/7.17 | v18) | ~ (vec_nth$c(v19) = v20) | ~ (vec_nth$c(v8) = v9) | ~ % 46.59/7.17 | (fun_app$h(v4, v7) = v8) | ~ (fun_app$f(v20, v3) = v21) | ~ % 46.59/7.17 | (fun_app$f(v9, v3) = v15) | ~ (fun_app$f(v9, v1) = v10) | ~ % 46.59/7.17 | (fun_app$c(v5, v2) = v6) | ~ N$(v3) | ~ N$(v2) | ~ N$(v1) | ~ % 46.59/7.17 | A_n_vec_n_vec$(v0) | ? [v22: N_a_n_vec_fun$] : (uwe$(v0, v1, v2) = % 46.59/7.17 | v22 & fun_app$f(v22, v3) = v21 & A_n_vec$(v21) & % 46.59/7.17 | N_a_n_vec_fun$(v22))) & ! [v0: A_n_vec_n_vec$] : ! [v1: N$] : ! % 46.59/7.17 | [v2: N$] : ! [v3: N_a_n_vec_n_vec_fun$] : ! [v4: N_n_bool_fun_fun$] % 46.59/7.17 | : ! [v5: N_bool_fun$] : ! [v6: N$] : ! [v7: A_n_vec_n_vec$] : ! % 46.59/7.17 | [v8: N_a_n_vec_fun$] : ! [v9: A_n_vec$] : ! [v10: N_a_fun$] : ! % 46.59/7.17 | [v11: A$] : ! [v12: A$] : ! [v13: A_n_vec_n_vec$] : ! [v14: % 46.59/7.17 | N_a_n_vec_fun$] : ! [v15: A_n_vec$] : ( ~ (interchange_rows$a(v0, % 46.59/7.17 | v1) = v3) | ~ (uwd$(v0, v1) = v4) | ~ (mult_row$a(v7, v1, v12) % 46.59/7.17 | = v13) | ~ (least$(v5) = v6) | ~ (vec_nth$e(v9) = v10) | ~ % 46.59/7.17 | (fun_app$l(v10, v2) = v11) | ~ (fun_app$m(all_621_0, v11) = v12) | % 46.59/7.17 | ~ (vec_nth$c(v13) = v14) | ~ (vec_nth$c(v7) = v8) | ~ % 46.59/7.17 | (fun_app$h(v3, v6) = v7) | ~ (fun_app$f(v14, v1) = v15) | ~ % 46.59/7.17 | (fun_app$f(v8, v1) = v9) | ~ (fun_app$c(v4, v2) = v5) | ~ N$(v2) | % 46.59/7.17 | ~ N$(v1) | ~ A_n_vec_n_vec$(v0) | ? [v16: N_a_n_vec_fun$] : % 46.59/7.17 | (uwe$(v0, v1, v2) = v16 & fun_app$f(v16, v1) = v15 & A_n_vec$(v15) & % 46.59/7.17 | N_a_n_vec_fun$(v16))) % 46.59/7.17 | % 46.59/7.17 | ALPHA: (35) implies: % 46.59/7.17 | (36) divide$(one$) = all_621_0 % 46.59/7.17 | % 46.59/7.17 | DELTA: instantiating (1) with fresh symbol all_624_0 gives: % 46.59/7.17 | (37) divide$(one$) = all_624_0 & A_a_fun$(all_624_0) & ! [v0: % 46.59/7.17 | A_b_vec_n_vec$] : ! [v1: N$] : ! [v2: B$] : ! [v3: N$] : ! [v4: % 46.59/7.17 | N_a_b_vec_n_vec_fun$] : ! [v5: N_bool_fun$] : ! [v6: N$] : ! [v7: % 46.59/7.17 | A_b_vec_n_vec$] : ! [v8: A_a_b_vec_n_vec_fun$] : ! [v9: % 46.59/7.17 | N_a_b_vec_fun$] : ! [v10: A_b_vec$] : ! [v11: B_a_fun$] : ! [v12: % 46.59/7.17 | A$] : ! [v13: A$] : ! [v14: A_b_vec_n_vec$] : ! [v15: % 46.59/7.17 | A_a_b_vec_n_vec_fun$] : ! [v16: A_b_vec$] : ! [v17: B_a_fun$] : ! % 46.59/7.17 | [v18: A$] : ! [v19: A$] : ! [v20: A_b_vec_n_vec$] : ! [v21: % 46.59/7.17 | N_a_b_vec_fun$] : ! [v22: A_b_vec$] : (v3 = v1 | ~ % 46.59/7.17 | (interchange_rows$(v0, v1) = v4) | ~ (uwf$(v0, v1, v2) = v5) | ~ % 46.59/7.17 | (least$(v5) = v6) | ~ (mult_row$(v7, v1) = v8) | ~ (row_add$(v14, % 46.59/7.17 | v3, v1) = v15) | ~ (fun_app$n(v15, v19) = v20) | ~ % 46.59/7.17 | (fun_app$n(v8, v13) = v14) | ~ (fun_app$m(all_624_0, v12) = v13) | % 46.59/7.17 | ~ (fun_app$m(uminus$c, v18) = v19) | ~ (fun_app$d(v4, v6) = v7) | % 46.59/7.17 | ~ (vec_nth$a(v20) = v21) | ~ (vec_nth$a(v7) = v9) | ~ % 46.59/7.17 | (fun_app$b(v21, v3) = v22) | ~ (fun_app$b(v9, v3) = v16) | ~ % 46.59/7.17 | (fun_app$b(v9, v1) = v10) | ~ (vec_nth$(v16) = v17) | ~ % 46.59/7.17 | (vec_nth$(v10) = v11) | ~ (fun_app$a(v17, v2) = v18) | ~ % 46.59/7.17 | (fun_app$a(v11, v2) = v12) | ~ N$(v3) | ~ N$(v1) | ~ B$(v2) | ~ % 46.59/7.17 | A_b_vec_n_vec$(v0) | ? [v23: N_a_b_vec_fun$] : (uwg$(v0, v1, v2) = % 46.59/7.17 | v23 & fun_app$b(v23, v3) = v22 & N_a_b_vec_fun$(v23) & % 46.59/7.17 | A_b_vec$(v22))) & ! [v0: A_b_vec_n_vec$] : ! [v1: N$] : ! [v2: % 46.59/7.17 | B$] : ! [v3: N_a_b_vec_n_vec_fun$] : ! [v4: N_bool_fun$] : ! [v5: % 46.59/7.17 | N$] : ! [v6: A_b_vec_n_vec$] : ! [v7: A_a_b_vec_n_vec_fun$] : ! % 46.59/7.17 | [v8: N_a_b_vec_fun$] : ! [v9: A_b_vec$] : ! [v10: B_a_fun$] : ! % 46.59/7.17 | [v11: A$] : ! [v12: A$] : ! [v13: A_b_vec_n_vec$] : ! [v14: % 46.59/7.17 | N_a_b_vec_fun$] : ! [v15: A_b_vec$] : ( ~ (interchange_rows$(v0, % 46.59/7.17 | v1) = v3) | ~ (uwf$(v0, v1, v2) = v4) | ~ (least$(v4) = v5) | % 46.59/7.17 | ~ (mult_row$(v6, v1) = v7) | ~ (fun_app$n(v7, v12) = v13) | ~ % 46.59/7.17 | (fun_app$m(all_624_0, v11) = v12) | ~ (fun_app$d(v3, v5) = v6) | ~ % 46.59/7.17 | (vec_nth$a(v13) = v14) | ~ (vec_nth$a(v6) = v8) | ~ % 46.59/7.17 | (fun_app$b(v14, v1) = v15) | ~ (fun_app$b(v8, v1) = v9) | ~ % 46.59/7.17 | (vec_nth$(v9) = v10) | ~ (fun_app$a(v10, v2) = v11) | ~ N$(v1) | % 46.59/7.17 | ~ B$(v2) | ~ A_b_vec_n_vec$(v0) | ? [v16: N_a_b_vec_fun$] : % 46.59/7.17 | (uwg$(v0, v1, v2) = v16 & fun_app$b(v16, v1) = v15 & % 46.59/7.17 | N_a_b_vec_fun$(v16) & A_b_vec$(v15))) % 46.59/7.17 | % 46.59/7.17 | ALPHA: (37) implies: % 46.59/7.17 | (38) divide$(one$) = all_624_0 % 46.59/7.17 | % 46.59/7.17 | GROUND_INST: instantiating (7) with all_611_4, all_613_5, interchange_A$, % 46.59/7.17 | simplifying with (18), (28) gives: % 46.59/7.17 | (39) all_613_5 = all_611_4 % 46.59/7.17 | % 46.59/7.17 | GROUND_INST: instantiating (13) with all_611_6, all_613_7, i$, interchange_A$, % 46.59/7.17 | simplifying with (21), (31) gives: % 46.59/7.17 | (40) all_613_7 = all_611_6 % 46.59/7.17 | % 46.59/7.17 | GROUND_INST: instantiating (8) with all_613_6, all_618_1, one$, simplifying % 46.59/7.17 | with (32), (34) gives: % 46.59/7.18 | (41) all_618_1 = all_613_6 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (8) with all_618_1, all_621_0, one$, simplifying % 46.59/7.18 | with (34), (36) gives: % 46.59/7.18 | (42) all_621_0 = all_618_1 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (8) with all_621_0, all_624_0, one$, simplifying % 46.59/7.18 | with (36), (38) gives: % 46.59/7.18 | (43) all_624_0 = all_621_0 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (8) with all_611_5, all_624_0, one$, simplifying % 46.59/7.18 | with (22), (38) gives: % 46.59/7.18 | (44) all_624_0 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | COMBINE_EQS: (43), (44) imply: % 46.59/7.18 | (45) all_621_0 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | SIMP: (45) implies: % 46.59/7.18 | (46) all_621_0 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | COMBINE_EQS: (42), (46) imply: % 46.59/7.18 | (47) all_618_1 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | SIMP: (47) implies: % 46.59/7.18 | (48) all_618_1 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | COMBINE_EQS: (41), (48) imply: % 46.59/7.18 | (49) all_613_6 = all_611_5 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (30), (40) imply: % 46.59/7.18 | (50) fun_app$n(all_611_6, all_613_1) = all_613_0 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (29), (49) imply: % 46.59/7.18 | (51) fun_app$m(all_611_5, all_613_2) = all_613_1 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (27), (39) imply: % 46.59/7.18 | (52) fun_app$b(all_611_4, i$) = all_613_4 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (10) with all_611_3, all_613_4, i$, all_611_4, % 46.59/7.18 | simplifying with (17), (52) gives: % 46.59/7.18 | (53) all_613_4 = all_611_3 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (26), (53) imply: % 46.59/7.18 | (54) vec_nth$(all_611_3) = all_613_3 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (6) with all_611_2, all_613_3, all_611_3, % 46.59/7.18 | simplifying with (16), (54) gives: % 46.59/7.18 | (55) all_613_3 = all_611_2 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (25), (55) imply: % 46.59/7.18 | (56) fun_app$a(all_611_2, j$) = all_613_2 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (9) with all_611_1, all_613_2, j$, all_611_2, % 46.59/7.18 | simplifying with (15), (56) gives: % 46.59/7.18 | (57) all_613_2 = all_611_1 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (51), (57) imply: % 46.59/7.18 | (58) fun_app$m(all_611_5, all_611_1) = all_613_1 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (11) with all_611_0, all_613_1, all_611_1, % 46.59/7.18 | all_611_5, simplifying with (19), (58) gives: % 46.59/7.18 | (59) all_613_1 = all_611_0 % 46.59/7.18 | % 46.59/7.18 | REDUCE: (50), (59) imply: % 46.59/7.18 | (60) fun_app$n(all_611_6, all_611_0) = all_613_0 % 46.59/7.18 | % 46.59/7.18 | GROUND_INST: instantiating (12) with a$a, all_613_0, all_611_0, all_611_6, % 46.59/7.18 | simplifying with (20), (60) gives: % 46.59/7.18 | (61) all_613_0 = a$a % 46.59/7.18 | % 46.59/7.18 | REDUCE: (24), (61) imply: % 46.59/7.18 | (62) $false % 46.59/7.18 | % 46.59/7.18 | CLOSE: (62) is inconsistent. % 46.59/7.18 | % 46.59/7.18 End of proof % 46.59/7.18 % SZS output end Proof for theBenchmark % 46.59/7.18 % 46.59/7.18 6563ms %------------------------------------------------------------------------------