%------------------------------------------------------------------------------ % 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 : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:11:47 EDT 2023 % Result : Theorem 43.82s 6.59s % Output : Proof 65.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.36 % Computer : n004.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Sun Aug 27 14:12:07 EDT 2023 % 0.13/0.36 % CPUTime : % 0.21/0.61 ________ _____ % 0.21/0.61 ___ __ \_________(_)________________________________ % 0.21/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.61 % 0.21/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.61 (2023-06-19) % 0.21/0.61 % 0.21/0.61 (c) Philipp Rümmer, 2009-2023 % 0.21/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.61 Amanda Stjerna. % 0.21/0.61 Free software under BSD-3-Clause. % 0.21/0.61 % 0.21/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.61 % 0.21/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.62 Running up to 7 provers in parallel. % 0.21/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.97/1.08 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.08 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.08 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.09 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.10 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.10 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 2.97/1.11 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 14.32/2.65 Prover 4: Preprocessing ... % 14.32/2.67 Prover 2: Preprocessing ... % 14.32/2.67 Prover 6: Preprocessing ... % 14.32/2.68 Prover 5: Preprocessing ... % 14.32/2.69 Prover 1: Preprocessing ... % 14.32/2.69 Prover 3: Preprocessing ... % 14.32/2.77 Prover 0: Preprocessing ... % 33.42/5.18 Prover 1: Warning: ignoring some quantifiers % 34.30/5.29 Prover 6: Proving ... % 34.30/5.29 Prover 3: Warning: ignoring some quantifiers % 34.30/5.39 Prover 3: Constructing countermodel ... % 35.03/5.43 Prover 1: Constructing countermodel ... % 39.41/6.06 Prover 5: Proving ... % 40.78/6.16 Prover 4: Warning: ignoring some quantifiers % 42.60/6.45 Prover 4: Constructing countermodel ... % 43.56/6.53 Prover 0: Proving ... % 43.82/6.58 Prover 6: proved (5936ms) % 43.82/6.58 % 43.82/6.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 43.82/6.59 % 43.82/6.60 Prover 3: stopped % 43.82/6.60 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 43.82/6.60 Prover 5: stopped % 43.82/6.60 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 43.82/6.60 Prover 0: stopped % 43.82/6.61 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 43.82/6.61 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 43.82/6.62 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 43.82/6.63 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 43.82/6.63 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 43.82/6.63 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 45.54/6.83 Prover 2: Proving ... % 45.54/6.83 Prover 2: stopped % 45.54/6.83 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 45.54/6.85 Prover 13: Warning: Problem contains reals, using incomplete axiomatisation % 52.23/7.67 Prover 8: Preprocessing ... % 52.23/7.67 Prover 11: Preprocessing ... % 52.23/7.67 Prover 7: Preprocessing ... % 52.68/7.74 Prover 13: Preprocessing ... % 52.92/7.75 Prover 10: Preprocessing ... % 59.71/8.71 Prover 1: Found proof (size 31) % 59.71/8.71 Prover 1: proved (8077ms) % 59.71/8.71 Prover 4: stopped % 59.71/8.72 Prover 8: Warning: ignoring some quantifiers % 60.50/8.82 Prover 8: Constructing countermodel ... % 60.50/8.83 Prover 8: stopped % 61.26/8.86 Prover 10: Warning: ignoring some quantifiers % 61.88/8.96 Prover 10: Constructing countermodel ... % 61.88/8.97 Prover 10: stopped % 61.88/9.02 Prover 7: Warning: ignoring some quantifiers % 62.77/9.12 Prover 7: Constructing countermodel ... % 62.77/9.13 Prover 7: stopped % 63.57/9.34 Prover 13: Warning: ignoring some quantifiers % 63.57/9.38 Prover 11: Warning: ignoring some quantifiers % 64.31/9.46 Prover 13: Constructing countermodel ... % 64.31/9.46 Prover 13: stopped % 64.80/9.48 Prover 11: Constructing countermodel ... % 64.80/9.49 Prover 11: stopped % 64.80/9.49 % 64.80/9.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 64.80/9.49 % 64.80/9.50 % SZS output start Proof for theBenchmark % 64.80/9.52 Assumptions after simplification: % 64.80/9.52 --------------------------------- % 64.80/9.52 % 64.80/9.52 (axiom3) % 64.80/9.54 A_cols_vec_rows_vec$(a$) & Rows$(i$) & ? [v0: A_rows_vec_rows_vec$] : ? [v1: % 64.80/9.54 A_rows_vec$] : ? [v2: A_cols_vec$] : ? [v3: Rows_a_rows_vec_fun$] : ? % 64.80/9.54 [v4: A_rows_vec$] : (p_Gauss_Jordan$(a$) = v0 & row$(i$, v0) = v1 & % 64.80/9.54 vec_nth$(v0) = v3 & fun_app$d(v3, i$) = v4 & vector_matrix_mult$(v4, a$) = % 64.80/9.54 v2 & vector_matrix_mult$(v1, a$) = v2 & A_rows_vec_rows_vec$(v0) & % 64.80/9.54 A_cols_vec$(v2) & Rows_a_rows_vec_fun$(v3) & A_rows_vec$(v4) & % 64.80/9.54 A_rows_vec$(v1)) % 64.80/9.54 % 64.80/9.54 (axiom7) % 64.80/9.54 ! [v0: A_rows_vec_rows_vec$] : ! [v1: Rows$] : ! [v2: A_cols_vec_rows_vec$] % 64.80/9.54 : ! [v3: A_cols_vec_rows_vec$] : ! [v4: Rows_a_cols_vec_fun$] : ! [v5: % 64.80/9.54 A_cols_vec$] : ( ~ (matrix_matrix_mult$(v0, v2) = v3) | ~ (vec_nth$a(v3) = % 64.80/9.54 v4) | ~ (fun_app$e(v4, v1) = v5) | ~ A_rows_vec_rows_vec$(v0) | ~ % 64.80/9.54 A_cols_vec_rows_vec$(v2) | ~ Rows$(v1) | ? [v6: Rows_a_rows_vec_fun$] : ? % 64.80/9.54 [v7: A_rows_vec$] : (vec_nth$(v0) = v6 & fun_app$d(v6, v1) = v7 & % 64.80/9.54 vector_matrix_mult$(v7, v2) = v5 & A_cols_vec$(v5) & % 64.80/9.54 Rows_a_rows_vec_fun$(v6) & A_rows_vec$(v7))) % 64.80/9.54 % 64.80/9.54 (conjecture2) % 64.80/9.54 A_cols_vec_rows_vec$(a$) & Rows$(i$) & ? [v0: A_rows_vec_rows_vec$] : ? [v1: % 64.80/9.54 Rows_a_rows_vec_fun$] : ? [v2: A_rows_vec$] : ? [v3: A_cols_vec$] : ? % 64.80/9.54 [v4: A_cols_vec_rows_vec$] : ? [v5: Rows_a_cols_vec_fun$] : ? [v6: % 64.80/9.54 A_cols_vec$] : ( ~ (v6 = v3) & matrix_matrix_mult$(v0, a$) = v4 & % 64.80/9.54 vec_nth$a(v4) = v5 & fun_app$e(v5, i$) = v6 & p_Gauss_Jordan$(a$) = v0 & % 64.80/9.54 vec_nth$(v0) = v1 & fun_app$d(v1, i$) = v2 & vector_matrix_mult$(v2, a$) = % 64.80/9.54 v3 & A_rows_vec_rows_vec$(v0) & A_cols_vec$(v6) & A_cols_vec$(v3) & % 64.80/9.54 A_cols_vec_rows_vec$(v4) & Rows_a_rows_vec_fun$(v1) & A_rows_vec$(v2) & % 64.80/9.54 Rows_a_cols_vec_fun$(v5)) % 64.80/9.54 % 64.80/9.54 (function-axioms) % 65.18/9.58 ! [v0: A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! [v2: Cols$] % 65.18/9.58 : ! [v3: Rows$] : ! [v4: A_cols_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (gauss_Jordan_in_ij$a(v4, v3, v2) = v1) | ~ (gauss_Jordan_in_ij$a(v4, v3, % 65.18/9.58 v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: Rows$] : ! [v4: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (gauss_Jordan_in_ij$(v4, v3, v2) = v1) % 65.18/9.58 | ~ (gauss_Jordan_in_ij$(v4, v3, v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] % 65.18/9.58 : ! [v1: A_cols_vec_rows_vec$] : ! [v2: Cols$] : ! [v3: Cols$] : ! [v4: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (interchange_columns$a(v4, v3, v2) = % 65.18/9.58 v1) | ~ (interchange_columns$a(v4, v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: Rows$] : ! [v4: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (interchange_columns$(v4, v3, v2) = v1) | ~ (interchange_columns$(v4, v3, % 65.18/9.58 v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: Rows$] : ! [v4: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (interchange_rows$a(v4, v3, v2) = v1) % 65.18/9.58 | ~ (interchange_rows$a(v4, v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] % 65.18/9.58 : ! [v1: A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: Rows$] : ! [v4: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (interchange_rows$(v4, v3, v2) = v1) | % 65.18/9.58 ~ (interchange_rows$(v4, v3, v2) = v0)) & ! [v0: Rows_a_cols_vec_fun$] : % 65.18/9.58 ! [v1: Rows_a_cols_vec_fun$] : ! [v2: Cols$] : ! [v3: Cols$] : ! [v4: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (interchange_columns_row$a(v4, v3, v2) % 65.18/9.58 = v1) | ~ (interchange_columns_row$a(v4, v3, v2) = v0)) & ! [v0: % 65.18/9.58 Rows_a_rows_vec_fun$] : ! [v1: Rows_a_rows_vec_fun$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: Rows$] : ! [v4: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (interchange_columns_row$(v4, v3, v2) = v1) | ~ % 65.18/9.58 (interchange_columns_row$(v4, v3, v2) = v0)) & ! [v0: Rows_a_cols_vec_fun$] % 65.18/9.58 : ! [v1: Rows_a_cols_vec_fun$] : ! [v2: Rows$] : ! [v3: Rows$] : ! [v4: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (interchange_rows_row$a(v4, v3, v2) = % 65.18/9.58 v1) | ~ (interchange_rows_row$a(v4, v3, v2) = v0)) & ! [v0: % 65.18/9.58 Rows_a_rows_vec_fun$] : ! [v1: Rows_a_rows_vec_fun$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: Rows$] : ! [v4: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (interchange_rows_row$(v4, v3, v2) = v1) | ~ (interchange_rows_row$(v4, v3, % 65.18/9.58 v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: % 65.18/9.58 $real] : (v1 = v0 | ~ (real_$quotient(v3, v2) = v1) | ~ % 65.18/9.58 (real_$quotient(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 65.18/9.58 $real] : ! [v3: $real] : (v1 = v0 | ~ (real_$difference(v3, v2) = v1) | ~ % 65.18/9.58 (real_$difference(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 65.18/9.58 $real] : ! [v3: $real] : (v1 = v0 | ~ (real_$sum(v3, v2) = v1) | ~ % 65.18/9.58 (real_$sum(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 65.18/9.58 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 65.18/9.58 (real_$greatereq(v3, v2) = v1) | ~ (real_$greatereq(v3, v2) = v0)) & ! % 65.18/9.58 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! % 65.18/9.58 [v3: $real] : (v1 = v0 | ~ (real_$greater(v3, v2) = v1) | ~ % 65.18/9.58 (real_$greater(v3, v2) = v0)) & ! [v0: A_cols_vec$] : ! [v1: A_cols_vec$] % 65.18/9.58 : ! [v2: A_cols_vec$] : ! [v3: A_cols_vec$] : (v1 = v0 | ~ (times$e(v3, v2) % 65.18/9.58 = v1) | ~ (times$e(v3, v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_cols_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (times$d(v3, v2) = v1) | ~ % 65.18/9.58 (times$d(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! % 65.18/9.58 [v2: A_rows_vec$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ (times$c(v3, v2) = % 65.18/9.58 v1) | ~ (times$c(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (times$b(v3, v2) = v1) | ~ % 65.18/9.58 (times$b(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : % 65.18/9.58 ! [v3: $real] : (v1 = v0 | ~ (real_$product(v3, v2) = v1) | ~ % 65.18/9.58 (real_$product(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] % 65.18/9.58 : ! [v2: A_cols_vec_rows_vec$] : ! [v3: Cols$] : (v1 = v0 | ~ (column$a(v3, % 65.18/9.58 v2) = v1) | ~ (column$a(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] % 65.18/9.58 : ! [v2: Nat$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$u(v3, v2) = % 65.18/9.58 v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 65.18/9.58 MultipleValueBool] : ! [v2: Rows$] : ! [v3: Rows$] : (v1 = v0 | ~ % 65.18/9.58 (less$(v3, v2) = v1) | ~ (less$(v3, v2) = v0)) & ! [v0: $real] : ! [v1: % 65.18/9.58 $real] : ! [v2: Nat$] : ! [v3: Nat_real_fun$] : (v1 = v0 | ~ % 65.18/9.58 (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec$] : ! [v1: A_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! % 65.18/9.58 [v3: Rows$] : (v1 = v0 | ~ (column$(v3, v2) = v1) | ~ (column$(v3, v2) = % 65.18/9.58 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 65.18/9.58 Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$s(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$s(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] % 65.18/9.58 : ! [v3: Real_real_fun$] : (v1 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$r(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: int] : % 65.18/9.58 ! [v3: Int_real_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$q(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: $real] : % 65.18/9.58 ! [v3: Real_int_fun$] : (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$p(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 65.18/9.58 [v3: Int_int_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$o(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 65.18/9.58 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 65.18/9.58 (real_$lesseq(v3, v2) = v1) | ~ (real_$lesseq(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: A_cols_vec$] : (v1 = v0 | ~ (mat_row$a(v3, v2) = v1) | ~ (mat_row$a(v3, % 65.18/9.58 v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: A_rows_vec$] : (v1 = v0 | % 65.18/9.58 ~ (mat_row$(v3, v2) = v1) | ~ (mat_row$(v3, v2) = v0)) & ! [v0: % 65.18/9.58 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Rows$] : ! [v3: % 65.18/9.58 Rows$] : (v1 = v0 | ~ (less_eq$(v3, v2) = v1) | ~ (less_eq$(v3, v2) = v0)) % 65.18/9.58 & ! [v0: A_rows_vec_cols_vec$] : ! [v1: A_rows_vec_cols_vec$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v3: A_rows_vec_cols_vec$] : (v1 = v0 | ~ % 65.18/9.58 (matrix_matrix_mult$d(v3, v2) = v1) | ~ (matrix_matrix_mult$d(v3, v2) = % 65.18/9.58 v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! % 65.18/9.58 [v2: A_cols_vec$] : ! [v3: Rows$] : (v1 = v0 | ~ (axis$a(v3, v2) = v1) | ~ % 65.18/9.58 (axis$a(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec$] : ! [v3: Rows$] : (v1 = v0 | % 65.18/9.58 ~ (axis$(v3, v2) = v1) | ~ (axis$(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: A_cols_vec_rows_vec$] : (v1 = v0 | ~ (columnvector_row$a(v3, v2) = v1) | % 65.18/9.58 ~ (columnvector_row$a(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: A_rows_vec_rows_vec$] : % 65.18/9.58 (v1 = v0 | ~ (columnvector_row$(v3, v2) = v1) | ~ (columnvector_row$(v3, v2) % 65.18/9.58 = v0)) & ! [v0: A_cols_vec$] : ! [v1: A_cols_vec$] : ! [v2: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v3: Rows$] : (v1 = v0 | ~ (row$a(v3, v2) = v1) % 65.18/9.58 | ~ (row$a(v3, v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: % 65.18/9.58 A_cols_vec_rows_vec_rows_vec$] : (v1 = v0 | ~ (transpose_row$c(v3, v2) = % 65.18/9.58 v1) | ~ (transpose_row$c(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : % 65.18/9.58 ! [v1: A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: % 65.18/9.58 A_rows_vec_rows_vec_rows_vec$] : (v1 = v0 | ~ (transpose_row$b(v3, v2) = % 65.18/9.58 v1) | ~ (transpose_row$b(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec$] : ! [v2: Cols$] : ! [v3: A_cols_vec_rows_vec$] : (v1 = v0 | % 65.18/9.58 ~ (transpose_row$a(v3, v2) = v1) | ~ (transpose_row$a(v3, v2) = v0)) & ! % 65.18/9.58 [v0: Rows_a_cols_vec_fun$] : ! [v1: Rows_a_cols_vec_fun$] : ! [v2: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v3: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (mat_mult_row$(v3, v2) = v1) | ~ (mat_mult_row$(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec_bool_fun$] : ! [v1: A_cols_vec_bool_fun$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: Rows_a_cols_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | % 65.18/9.58 ~ (fun_app$n(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 65.18/9.58 MultipleValueBool] : ! [v2: A_cols_vec$] : ! [v3: A_cols_vec_bool_fun$] : % 65.18/9.58 (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! % 65.18/9.58 [v0: A_rows_vec_bool_fun$] : ! [v1: A_rows_vec_bool_fun$] : ! [v2: Rows$] : % 65.18/9.58 ! [v3: Rows_a_rows_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) % 65.18/9.58 | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 65.18/9.58 MultipleValueBool] : ! [v2: A_rows_vec$] : ! [v3: A_rows_vec_bool_fun$] : % 65.18/9.58 (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! % 65.18/9.58 [v0: A_cols_vec_rows_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec_rows_vec$] : % 65.18/9.58 ! [v2: A_rows_vec_rows_vec$] : ! [v3: A_a_cols_vec_fun$] : (v1 = v0 | ~ % 65.18/9.58 (map_matrix$e(v3, v2) = v1) | ~ (map_matrix$e(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec$] : ! [v1: A_cols_vec$] : ! [v2: A$] : ! [v3: % 65.18/9.58 A_a_cols_vec_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$j(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_a_rows_vec_fun$] : (v1 = v0 | ~ (map_matrix$d(v3, v2) = v1) | ~ % 65.18/9.58 (map_matrix$d(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : % 65.18/9.58 ! [v2: A$] : ! [v3: A_a_rows_vec_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = % 65.18/9.58 v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_cols_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec$] : ! [v3: A_a_fun$] % 65.18/9.58 : (v1 = v0 | ~ (map_matrix$c(v3, v2) = v1) | ~ (map_matrix$c(v3, v2) = v0)) % 65.18/9.58 & ! [v0: A$] : ! [v1: A$] : ! [v2: Cols$] : ! [v3: A_cols_vec$] : (v1 = v0 % 65.18/9.58 | ~ (vec_nth$e(v3, v2) = v1) | ~ (vec_nth$e(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! [v2: Rows$] : ! % 65.18/9.58 [v3: A_cols_vec_rows_vec_rows_vec$] : (v1 = v0 | ~ (vec_nth$d(v3, v2) = v1) | % 65.18/9.58 ~ (vec_nth$d(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: % 65.18/9.58 A_cols_vec$] : ! [v3: A_cols_vec_a_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) % 65.18/9.58 = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_rows_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_cols_vec_a_fun$] : (v1 = v0 | ~ (map_matrix$b(v3, v2) = v1) | ~ % 65.18/9.58 (map_matrix$b(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: Rows$] : ! [v3: % 65.18/9.58 A_rows_vec_rows_vec_rows_vec$] : (v1 = v0 | ~ (vec_nth$c(v3, v2) = v1) | ~ % 65.18/9.58 (vec_nth$c(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_rows_vec$] % 65.18/9.58 : ! [v3: A_rows_vec_a_fun$] : (v1 = v0 | ~ (fun_app$g(v3, v2) = v1) | ~ % 65.18/9.58 (fun_app$g(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec_rows_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_rows_vec_a_fun$] : (v1 = v0 | ~ (map_matrix$a(v3, v2) = v1) | ~ % 65.18/9.58 (map_matrix$a(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: A_a_fun$] : % 65.18/9.58 (v1 = v0 | ~ (map_matrix$(v3, v2) = v1) | ~ (map_matrix$(v3, v2) = v0)) & ! % 65.18/9.58 [v0: A$] : ! [v1: A$] : ! [v2: Rows$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (vec_nth$b(v3, v2) = v1) | ~ (vec_nth$b(v3, v2) = v0)) & ! [v0: A$] : ! % 65.18/9.58 [v1: A$] : ! [v2: A$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) % 65.18/9.58 = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_cols_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$(v3, v2) = v1) | % 65.18/9.58 ~ (matrix_matrix_mult$(v3, v2) = v0)) & ! [v0: A_cols_vec$] : ! [v1: % 65.18/9.58 A_cols_vec$] : ! [v2: A_cols_vec_cols_vec$] : ! [v3: A_cols_vec$] : (v1 = % 65.18/9.58 v0 | ~ (vector_matrix_mult$c(v3, v2) = v1) | ~ (vector_matrix_mult$c(v3, % 65.18/9.58 v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: A_cols_vec_cols_vec$] : ! [v3: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$c(v3, v2) = v1) | % 65.18/9.58 ~ (matrix_matrix_mult$c(v3, v2) = v0)) & ! [v0: A_cols_vec$] : ! [v1: % 65.18/9.58 A_cols_vec$] : ! [v2: Rows$] : ! [v3: Rows_a_cols_vec_fun$] : (v1 = v0 | % 65.18/9.58 ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec$] : ! [v1: A_rows_vec$] : ! [v2: A_rows_vec_cols_vec$] : ! % 65.18/9.58 [v3: A_cols_vec$] : (v1 = v0 | ~ (vector_matrix_mult$b(v3, v2) = v1) | ~ % 65.18/9.58 (vector_matrix_mult$b(v3, v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! % 65.18/9.58 [v1: A_rows_vec_rows_vec$] : ! [v2: A_rows_vec_cols_vec$] : ! [v3: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$b(v3, v2) = v1) | % 65.18/9.58 ~ (matrix_matrix_mult$b(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: A_rows_vec$] : (v1 = % 65.18/9.58 v0 | ~ (vector_matrix_mult$a(v3, v2) = v1) | ~ (vector_matrix_mult$a(v3, % 65.18/9.58 v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (matrix_matrix_mult$a(v3, v2) = v1) | % 65.18/9.58 ~ (matrix_matrix_mult$a(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec$] : ! [v2: A_rows_vec_rows_vec$] : ! [v3: Rows$] : (v1 = v0 | % 65.18/9.58 ~ (row$(v3, v2) = v1) | ~ (row$(v3, v2) = v0)) & ! [v0: A_rows_vec$] : ! % 65.18/9.58 [v1: A_rows_vec$] : ! [v2: Rows$] : ! [v3: Rows_a_rows_vec_fun$] : (v1 = v0 % 65.18/9.58 | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec$] : ! [v1: A_cols_vec$] : ! [v2: A_cols_vec_rows_vec$] : ! % 65.18/9.58 [v3: A_rows_vec$] : (v1 = v0 | ~ (vector_matrix_mult$(v3, v2) = v1) | ~ % 65.18/9.58 (vector_matrix_mult$(v3, v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: % 65.18/9.58 Int_bool_fun$] : ! [v2: int] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | % 65.18/9.58 ~ (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: % 65.18/9.58 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 65.18/9.58 Int_bool_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, % 65.18/9.58 v2) = v0)) & ! [v0: Real_bool_fun$] : ! [v1: Real_bool_fun$] : ! [v2: % 65.18/9.58 $real] : ! [v3: Real_real_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) % 65.18/9.58 = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 65.18/9.58 [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: Real_bool_fun$] : (v1 = v0 % 65.18/9.58 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: % 65.18/9.58 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 65.18/9.58 $real] : (v1 = v0 | ~ (real_$less(v3, v2) = v1) | ~ (real_$less(v3, v2) = % 65.18/9.58 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 65.18/9.58 $real] : (v1 = v0 | ~ (real_$is_int(v2) = v1) | ~ (real_$is_int(v2) = v0)) % 65.18/9.58 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : % 65.18/9.58 (v1 = v0 | ~ (real_$is_rat(v2) = v1) | ~ (real_$is_rat(v2) = v0)) & ! [v0: % 65.18/9.58 $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$floor(v2) = % 65.18/9.58 v1) | ~ (real_$floor(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 65.18/9.58 [v2: $real] : (v1 = v0 | ~ (real_$ceiling(v2) = v1) | ~ (real_$ceiling(v2) = % 65.18/9.58 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 65.18/9.58 (real_$truncate(v2) = v1) | ~ (real_$truncate(v2) = v0)) & ! [v0: $real] : % 65.18/9.58 ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$round(v2) = v1) | ~ % 65.18/9.58 (real_$round(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: $real] : (v1 % 65.18/9.58 = v0 | ~ (real_$to_int(v2) = v1) | ~ (real_$to_int(v2) = v0)) & ! [v0: % 65.18/9.58 $rat] : ! [v1: $rat] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_rat(v2) = % 65.18/9.58 v1) | ~ (real_$to_rat(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! % 65.18/9.58 [v2: $real] : (v1 = v0 | ~ (real_$to_real(v2) = v1) | ~ (real_$to_real(v2) = % 65.18/9.58 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: int] : (v1 = v0 | ~ % 65.18/9.58 (int_$to_real(v2) = v1) | ~ (int_$to_real(v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: A$] : (v1 = % 65.18/9.58 v0 | ~ (mat$(v2) = v1) | ~ (mat$(v2) = v0)) & ! [v0: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v1: A_cols_vec_rows_vec$] : ! [v2: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (uminus$b(v2) = v1) | ~ (uminus$b(v2) % 65.18/9.58 = v0)) & ! [v0: A_cols_vec$] : ! [v1: A_cols_vec$] : ! [v2: % 65.18/9.58 A_cols_vec$] : (v1 = v0 | ~ (uminus$c(v2) = v1) | ~ (uminus$c(v2) = v0)) & % 65.18/9.58 ! [v0: A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (uminus$(v2) = v1) | ~ (uminus$(v2) = % 65.18/9.58 v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! [v2: A_rows_vec$] % 65.18/9.58 : (v1 = v0 | ~ (uminus$a(v2) = v1) | ~ (uminus$a(v2) = v0)) & ! [v0: $real] % 65.18/9.58 : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$uminus(v2) = v1) | ~ % 65.18/9.58 (real_$uminus(v2) = v0)) & ! [v0: Int_int_fun$] : ! [v1: Int_int_fun$] : % 65.18/9.58 ! [v2: int] : (v1 = v0 | ~ (times$a(v2) = v1) | ~ (times$a(v2) = v0)) & ! % 65.18/9.58 [v0: Real_real_fun$] : ! [v1: Real_real_fun$] : ! [v2: $real] : (v1 = v0 | % 65.18/9.58 ~ (times$(v2) = v1) | ~ (times$(v2) = v0)) & ! [v0: MultipleValueBool] : % 65.18/9.58 ! [v1: MultipleValueBool] : ! [v2: A_cols_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (reduced_row_echelon_form$a(v2) = v1) | ~ (reduced_row_echelon_form$a(v2) = % 65.18/9.58 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (reduced_row_echelon_form$(v2) = v1) | % 65.18/9.58 ~ (reduced_row_echelon_form$(v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : % 65.18/9.58 ! [v1: A_cols_vec_rows_vec$] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$d(v2) = % 65.18/9.58 v1) | ~ (of_nat$d(v2) = v0)) & ! [v0: A_cols_vec$] : ! [v1: % 65.18/9.58 A_cols_vec$] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$e(v2) = v1) | ~ % 65.18/9.58 (of_nat$e(v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$b(v2) = v1) | % 65.18/9.58 ~ (of_nat$b(v2) = v0)) & ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! % 65.18/9.58 [v2: Nat$] : (v1 = v0 | ~ (of_nat$c(v2) = v1) | ~ (of_nat$c(v2) = v0)) & ! % 65.18/9.58 [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : (v1 = v0 | ~ (nat$(v2) = v1) | ~ % 65.18/9.58 (nat$(v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (gauss_Jordan$a(v2) = v1) | ~ (gauss_Jordan$a(v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (gauss_Jordan$(v2) = v1) | ~ % 65.18/9.58 (gauss_Jordan$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (rank$b(v2) = v1) | ~ (rank$b(v2) = % 65.18/9.58 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: A_rows_vec_cols_vec$] : (v1 % 65.18/9.58 = v0 | ~ (rank$a(v2) = v1) | ~ (rank$a(v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec_cols_vec$] : ! [v1: A_rows_vec_cols_vec$] : ! [v2: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (transpose$b(v2) = v1) | ~ % 65.18/9.58 (transpose$b(v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: A_cols_vec$] : (v1 = v0 | ~ (vec$a(v2) = % 65.18/9.58 v1) | ~ (vec$a(v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_rows_vec$] : (v1 = v0 | ~ (vec$(v2) = v1) % 65.18/9.58 | ~ (vec$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Rows$] : (v1 % 65.18/9.58 = v0 | ~ (to_nat$(v2) = v1) | ~ (to_nat$(v2) = v0)) & ! [v0: Nat$] : ! % 65.18/9.58 [v1: Nat$] : ! [v2: A_cols_vec_rows_vec$] : (v1 = v0 | ~ (rank$(v2) = v1) | % 65.18/9.58 ~ (rank$(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : (v1 = v0 % 65.18/9.58 | ~ (of_nat$(v2) = v1) | ~ (of_nat$(v2) = v0)) & ! [v0: % 65.18/9.58 Rows_a_cols_vec_fun$] : ! [v1: Rows_a_cols_vec_fun$] : ! [v2: % 65.18/9.58 A_rows_vec_cols_vec$] : (v1 = v0 | ~ (transpose_row$d(v2) = v1) | ~ % 65.18/9.58 (transpose_row$d(v2) = v0)) & ! [v0: A_cols_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_cols_vec_rows_vec$] : ! [v2: A_rows_vec_cols_vec$] : (v1 = v0 | ~ % 65.18/9.58 (transpose$a(v2) = v1) | ~ (transpose$a(v2) = v0)) & ! [v0: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (transpose$(v2) = v1) | ~ % 65.18/9.58 (transpose$(v2) = v0)) & ! [v0: Rows_a_rows_vec_fun$] : ! [v1: % 65.18/9.58 Rows_a_rows_vec_fun$] : ! [v2: A_rows_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (transpose_row$(v2) = v1) | ~ (transpose_row$(v2) = v0)) & ! [v0: % 65.18/9.58 Rows_a_cols_vec_fun$] : ! [v1: Rows_a_cols_vec_fun$] : ! [v2: % 65.18/9.58 A_cols_vec_rows_vec$] : (v1 = v0 | ~ (vec_nth$a(v2) = v1) | ~ % 65.18/9.58 (vec_nth$a(v2) = v0)) & ! [v0: A_rows_vec_rows_vec$] : ! [v1: % 65.18/9.58 A_rows_vec_rows_vec$] : ! [v2: A_cols_vec_rows_vec$] : (v1 = v0 | ~ % 65.18/9.58 (p_Gauss_Jordan$(v2) = v1) | ~ (p_Gauss_Jordan$(v2) = v0)) & ! [v0: % 65.18/9.58 Rows_a_rows_vec_fun$] : ! [v1: Rows_a_rows_vec_fun$] : ! [v2: % 65.18/9.58 A_rows_vec_rows_vec$] : (v1 = v0 | ~ (vec_nth$(v2) = v1) | ~ (vec_nth$(v2) % 65.18/9.58 = v0)) % 65.18/9.58 % 65.18/9.58 Further assumptions not needed in the proof: % 65.18/9.58 -------------------------------------------- % 65.18/9.59 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 65.18/9.59 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 65.18/9.59 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 65.18/9.59 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 65.18/9.59 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 65.18/9.59 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 65.18/9.59 axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, % 65.18/9.59 axiom149, axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 65.18/9.59 axiom156, axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, % 65.18/9.59 axiom163, axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, % 65.18/9.59 axiom170, axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, % 65.18/9.59 axiom178, axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, % 65.18/9.59 axiom185, axiom186, axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, % 65.18/9.59 axiom192, axiom193, axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, % 65.18/9.59 axiom20, axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, % 65.18/9.59 axiom207, axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, % 65.18/9.59 axiom214, axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, % 65.18/9.59 axiom221, axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, % 65.18/9.59 axiom229, axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, % 65.18/9.59 axiom236, axiom237, axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, % 65.18/9.59 axiom243, axiom244, axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, % 65.18/9.59 axiom250, axiom251, axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, % 65.18/9.59 axiom258, axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, % 65.18/9.59 axiom265, axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, % 65.18/9.59 axiom272, axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, % 65.18/9.59 axiom28, axiom280, axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, % 65.18/9.59 axiom287, axiom288, axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, % 65.18/9.59 axiom294, axiom295, axiom296, axiom297, axiom298, axiom299, axiom30, axiom300, % 65.18/9.59 axiom301, axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, % 65.18/9.59 axiom309, axiom31, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, % 65.18/9.59 axiom316, axiom317, axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, % 65.18/9.59 axiom323, axiom324, axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, % 65.18/9.59 axiom330, axiom331, axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, % 65.18/9.59 axiom338, axiom339, axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, % 65.18/9.59 axiom345, axiom346, axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, % 65.18/9.59 axiom352, axiom353, axiom354, axiom355, axiom356, axiom357, axiom358, axiom359, % 65.18/9.59 axiom36, axiom360, axiom361, axiom362, axiom363, axiom364, axiom365, axiom366, % 65.18/9.59 axiom367, axiom368, axiom369, axiom37, axiom370, axiom371, axiom372, axiom373, % 65.18/9.59 axiom374, axiom375, axiom376, axiom377, axiom378, axiom379, axiom38, axiom380, % 65.18/9.59 axiom381, axiom382, axiom383, axiom384, axiom385, axiom386, axiom387, axiom388, % 65.18/9.59 axiom389, axiom39, axiom390, axiom391, axiom392, axiom393, axiom394, axiom395, % 65.18/9.59 axiom396, axiom397, axiom398, axiom399, axiom4, axiom40, axiom400, axiom401, % 65.18/9.59 axiom402, axiom403, axiom404, axiom405, axiom406, axiom407, axiom408, axiom409, % 65.18/9.59 axiom41, axiom410, axiom411, axiom412, axiom413, axiom414, axiom415, axiom416, % 65.18/9.59 axiom417, axiom418, axiom419, axiom42, axiom420, axiom421, axiom422, axiom423, % 65.18/9.59 axiom424, axiom425, axiom426, axiom427, axiom428, axiom429, axiom43, axiom430, % 65.18/9.59 axiom431, axiom432, axiom433, axiom434, axiom435, axiom436, axiom437, axiom438, % 65.18/9.59 axiom439, axiom44, axiom440, axiom441, axiom442, axiom443, axiom444, axiom445, % 65.18/9.59 axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, axiom451, axiom452, % 65.18/9.59 axiom453, axiom454, axiom455, axiom456, axiom457, axiom458, axiom459, axiom46, % 65.18/9.59 axiom460, axiom461, axiom462, axiom463, axiom464, axiom465, axiom466, axiom467, % 65.18/9.59 axiom468, axiom469, axiom47, axiom470, axiom471, axiom472, axiom473, axiom474, % 65.18/9.59 axiom475, axiom476, axiom477, axiom478, axiom479, axiom48, axiom480, axiom481, % 65.18/9.59 axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, axiom488, axiom489, % 65.18/9.59 axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, axiom495, axiom496, % 65.18/9.59 axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, axiom501, axiom502, % 65.18/9.59 axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, axiom509, axiom51, % 65.18/9.59 axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, axiom516, axiom517, % 65.18/9.59 axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, axiom523, axiom524, % 65.18/9.59 axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, axiom530, axiom531, % 65.18/9.59 axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, axiom538, axiom539, % 65.18/9.59 axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, axiom545, axiom546, % 65.18/9.59 axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, axiom552, axiom553, % 65.18/9.59 axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, axiom56, axiom560, % 65.18/9.59 axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, axiom567, axiom568, % 65.18/9.59 axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, axiom574, axiom575, % 65.18/9.59 axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, axiom582, % 65.18/9.59 axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, axiom59, % 65.18/9.59 axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, axiom597, % 65.18/9.59 axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, axiom602, axiom603, % 65.18/9.59 axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, axiom61, axiom610, % 65.18/9.59 axiom611, axiom612, axiom613, axiom614, axiom62, axiom63, axiom64, axiom65, % 65.18/9.59 axiom66, axiom67, axiom68, axiom69, axiom70, axiom71, axiom72, axiom73, axiom74, % 65.18/9.59 axiom75, axiom76, axiom77, axiom78, axiom79, axiom8, axiom80, axiom81, axiom82, % 65.18/9.59 axiom83, axiom84, axiom85, axiom86, axiom87, axiom88, axiom89, axiom9, axiom90, % 65.18/9.59 axiom91, axiom92, axiom93, axiom94, axiom95, axiom96, axiom97, axiom98, axiom99, % 65.18/9.59 formula_616, formula_617 % 65.18/9.59 % 65.18/9.59 Those formulas are unsatisfiable: % 65.18/9.59 --------------------------------- % 65.18/9.59 % 65.18/9.59 Begin of proof % 65.18/9.59 | % 65.18/9.59 | ALPHA: (axiom3) implies: % 65.18/9.59 | (1) ? [v0: A_rows_vec_rows_vec$] : ? [v1: A_rows_vec$] : ? [v2: % 65.18/9.59 | A_cols_vec$] : ? [v3: Rows_a_rows_vec_fun$] : ? [v4: A_rows_vec$] : % 65.18/9.59 | (p_Gauss_Jordan$(a$) = v0 & row$(i$, v0) = v1 & vec_nth$(v0) = v3 & % 65.18/9.59 | fun_app$d(v3, i$) = v4 & vector_matrix_mult$(v4, a$) = v2 & % 65.18/9.59 | vector_matrix_mult$(v1, a$) = v2 & A_rows_vec_rows_vec$(v0) & % 65.18/9.59 | A_cols_vec$(v2) & Rows_a_rows_vec_fun$(v3) & A_rows_vec$(v4) & % 65.18/9.59 | A_rows_vec$(v1)) % 65.18/9.59 | % 65.18/9.59 | ALPHA: (conjecture2) implies: % 65.18/9.59 | (2) Rows$(i$) % 65.18/9.59 | (3) A_cols_vec_rows_vec$(a$) % 65.18/9.59 | (4) ? [v0: A_rows_vec_rows_vec$] : ? [v1: Rows_a_rows_vec_fun$] : ? [v2: % 65.18/9.59 | A_rows_vec$] : ? [v3: A_cols_vec$] : ? [v4: A_cols_vec_rows_vec$] : % 65.18/9.59 | ? [v5: Rows_a_cols_vec_fun$] : ? [v6: A_cols_vec$] : ( ~ (v6 = v3) & % 65.18/9.59 | matrix_matrix_mult$(v0, a$) = v4 & vec_nth$a(v4) = v5 & fun_app$e(v5, % 65.18/9.59 | i$) = v6 & p_Gauss_Jordan$(a$) = v0 & vec_nth$(v0) = v1 & % 65.18/9.59 | fun_app$d(v1, i$) = v2 & vector_matrix_mult$(v2, a$) = v3 & % 65.18/9.59 | A_rows_vec_rows_vec$(v0) & A_cols_vec$(v6) & A_cols_vec$(v3) & % 65.18/9.59 | A_cols_vec_rows_vec$(v4) & Rows_a_rows_vec_fun$(v1) & A_rows_vec$(v2) % 65.18/9.59 | & Rows_a_cols_vec_fun$(v5)) % 65.18/9.59 | % 65.18/9.59 | ALPHA: (function-axioms) implies: % 65.18/9.59 | (5) ! [v0: Rows_a_rows_vec_fun$] : ! [v1: Rows_a_rows_vec_fun$] : ! [v2: % 65.18/9.59 | A_rows_vec_rows_vec$] : (v1 = v0 | ~ (vec_nth$(v2) = v1) | ~ % 65.18/9.59 | (vec_nth$(v2) = v0)) % 65.18/9.59 | (6) ! [v0: A_rows_vec_rows_vec$] : ! [v1: A_rows_vec_rows_vec$] : ! [v2: % 65.18/9.59 | A_cols_vec_rows_vec$] : (v1 = v0 | ~ (p_Gauss_Jordan$(v2) = v1) | ~ % 65.18/9.59 | (p_Gauss_Jordan$(v2) = v0)) % 65.18/9.59 | (7) ! [v0: A_cols_vec$] : ! [v1: A_cols_vec$] : ! [v2: % 65.18/9.59 | A_cols_vec_rows_vec$] : ! [v3: A_rows_vec$] : (v1 = v0 | ~ % 65.18/9.59 | (vector_matrix_mult$(v3, v2) = v1) | ~ (vector_matrix_mult$(v3, v2) % 65.18/9.59 | = v0)) % 65.18/9.59 | (8) ! [v0: A_rows_vec$] : ! [v1: A_rows_vec$] : ! [v2: Rows$] : ! [v3: % 65.18/9.59 | Rows_a_rows_vec_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 65.18/9.59 | (fun_app$d(v3, v2) = v0)) % 65.18/9.59 | % 65.18/9.60 | DELTA: instantiating (1) with fresh symbols all_530_0, all_530_1, all_530_2, % 65.18/9.60 | all_530_3, all_530_4 gives: % 65.18/9.60 | (9) p_Gauss_Jordan$(a$) = all_530_4 & row$(i$, all_530_4) = all_530_3 & % 65.18/9.60 | vec_nth$(all_530_4) = all_530_1 & fun_app$d(all_530_1, i$) = all_530_0 % 65.18/9.60 | & vector_matrix_mult$(all_530_0, a$) = all_530_2 & % 65.18/9.60 | vector_matrix_mult$(all_530_3, a$) = all_530_2 & % 65.18/9.60 | A_rows_vec_rows_vec$(all_530_4) & A_cols_vec$(all_530_2) & % 65.18/9.60 | Rows_a_rows_vec_fun$(all_530_1) & A_rows_vec$(all_530_0) & % 65.18/9.60 | A_rows_vec$(all_530_3) % 65.18/9.60 | % 65.18/9.60 | ALPHA: (9) implies: % 65.18/9.60 | (10) vector_matrix_mult$(all_530_0, a$) = all_530_2 % 65.18/9.60 | (11) fun_app$d(all_530_1, i$) = all_530_0 % 65.18/9.60 | (12) vec_nth$(all_530_4) = all_530_1 % 65.18/9.60 | (13) p_Gauss_Jordan$(a$) = all_530_4 % 65.18/9.60 | % 65.18/9.60 | DELTA: instantiating (4) with fresh symbols all_536_0, all_536_1, all_536_2, % 65.18/9.60 | all_536_3, all_536_4, all_536_5, all_536_6 gives: % 65.18/9.60 | (14) ~ (all_536_0 = all_536_3) & matrix_matrix_mult$(all_536_6, a$) = % 65.18/9.60 | all_536_2 & vec_nth$a(all_536_2) = all_536_1 & fun_app$e(all_536_1, % 65.18/9.60 | i$) = all_536_0 & p_Gauss_Jordan$(a$) = all_536_6 & % 65.18/9.60 | vec_nth$(all_536_6) = all_536_5 & fun_app$d(all_536_5, i$) = all_536_4 % 65.18/9.60 | & vector_matrix_mult$(all_536_4, a$) = all_536_3 & % 65.18/9.60 | A_rows_vec_rows_vec$(all_536_6) & A_cols_vec$(all_536_0) & % 65.18/9.60 | A_cols_vec$(all_536_3) & A_cols_vec_rows_vec$(all_536_2) & % 65.18/9.60 | Rows_a_rows_vec_fun$(all_536_5) & A_rows_vec$(all_536_4) & % 65.18/9.60 | Rows_a_cols_vec_fun$(all_536_1) % 65.18/9.60 | % 65.18/9.60 | ALPHA: (14) implies: % 65.18/9.60 | (15) ~ (all_536_0 = all_536_3) % 65.18/9.60 | (16) A_rows_vec_rows_vec$(all_536_6) % 65.18/9.60 | (17) vector_matrix_mult$(all_536_4, a$) = all_536_3 % 65.18/9.60 | (18) fun_app$d(all_536_5, i$) = all_536_4 % 65.18/9.60 | (19) vec_nth$(all_536_6) = all_536_5 % 65.18/9.60 | (20) p_Gauss_Jordan$(a$) = all_536_6 % 65.18/9.60 | (21) fun_app$e(all_536_1, i$) = all_536_0 % 65.18/9.60 | (22) vec_nth$a(all_536_2) = all_536_1 % 65.18/9.60 | (23) matrix_matrix_mult$(all_536_6, a$) = all_536_2 % 65.18/9.60 | % 65.18/9.60 | GROUND_INST: instantiating (6) with all_530_4, all_536_6, a$, simplifying with % 65.18/9.60 | (13), (20) gives: % 65.18/9.60 | (24) all_536_6 = all_530_4 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (23), (24) imply: % 65.18/9.60 | (25) matrix_matrix_mult$(all_530_4, a$) = all_536_2 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (19), (24) imply: % 65.18/9.60 | (26) vec_nth$(all_530_4) = all_536_5 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (16), (24) imply: % 65.18/9.60 | (27) A_rows_vec_rows_vec$(all_530_4) % 65.18/9.60 | % 65.18/9.60 | GROUND_INST: instantiating (5) with all_530_1, all_536_5, all_530_4, % 65.18/9.60 | simplifying with (12), (26) gives: % 65.18/9.60 | (28) all_536_5 = all_530_1 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (18), (28) imply: % 65.18/9.60 | (29) fun_app$d(all_530_1, i$) = all_536_4 % 65.18/9.60 | % 65.18/9.60 | GROUND_INST: instantiating (8) with all_530_0, all_536_4, i$, all_530_1, % 65.18/9.60 | simplifying with (11), (29) gives: % 65.18/9.60 | (30) all_536_4 = all_530_0 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (17), (30) imply: % 65.18/9.60 | (31) vector_matrix_mult$(all_530_0, a$) = all_536_3 % 65.18/9.60 | % 65.18/9.60 | GROUND_INST: instantiating (7) with all_530_2, all_536_3, a$, all_530_0, % 65.18/9.60 | simplifying with (10), (31) gives: % 65.18/9.60 | (32) all_536_3 = all_530_2 % 65.18/9.60 | % 65.18/9.60 | REDUCE: (15), (32) imply: % 65.18/9.60 | (33) ~ (all_536_0 = all_530_2) % 65.18/9.60 | % 65.18/9.60 | GROUND_INST: instantiating (axiom7) with all_530_4, i$, a$, all_536_2, % 65.18/9.60 | all_536_1, all_536_0, simplifying with (2), (3), (21), (22), % 65.18/9.60 | (25), (27) gives: % 65.18/9.61 | (34) ? [v0: Rows_a_rows_vec_fun$] : ? [v1: A_rows_vec$] : % 65.18/9.61 | (vec_nth$(all_530_4) = v0 & fun_app$d(v0, i$) = v1 & % 65.18/9.61 | vector_matrix_mult$(v1, a$) = all_536_0 & A_cols_vec$(all_536_0) & % 65.18/9.61 | Rows_a_rows_vec_fun$(v0) & A_rows_vec$(v1)) % 65.18/9.61 | % 65.18/9.61 | DELTA: instantiating (34) with fresh symbols all_750_0, all_750_1 gives: % 65.18/9.61 | (35) vec_nth$(all_530_4) = all_750_1 & fun_app$d(all_750_1, i$) = all_750_0 % 65.18/9.61 | & vector_matrix_mult$(all_750_0, a$) = all_536_0 & % 65.18/9.61 | A_cols_vec$(all_536_0) & Rows_a_rows_vec_fun$(all_750_1) & % 65.18/9.61 | A_rows_vec$(all_750_0) % 65.18/9.61 | % 65.18/9.61 | ALPHA: (35) implies: % 65.18/9.61 | (36) vector_matrix_mult$(all_750_0, a$) = all_536_0 % 65.18/9.61 | (37) fun_app$d(all_750_1, i$) = all_750_0 % 65.18/9.61 | (38) vec_nth$(all_530_4) = all_750_1 % 65.18/9.61 | % 65.18/9.61 | GROUND_INST: instantiating (5) with all_530_1, all_750_1, all_530_4, % 65.18/9.61 | simplifying with (12), (38) gives: % 65.18/9.61 | (39) all_750_1 = all_530_1 % 65.18/9.61 | % 65.18/9.61 | REDUCE: (37), (39) imply: % 65.18/9.61 | (40) fun_app$d(all_530_1, i$) = all_750_0 % 65.18/9.61 | % 65.18/9.61 | GROUND_INST: instantiating (8) with all_530_0, all_750_0, i$, all_530_1, % 65.18/9.61 | simplifying with (11), (40) gives: % 65.18/9.61 | (41) all_750_0 = all_530_0 % 65.18/9.61 | % 65.18/9.61 | REDUCE: (36), (41) imply: % 65.18/9.61 | (42) vector_matrix_mult$(all_530_0, a$) = all_536_0 % 65.18/9.61 | % 65.18/9.61 | GROUND_INST: instantiating (7) with all_530_2, all_536_0, a$, all_530_0, % 65.18/9.61 | simplifying with (10), (42) gives: % 65.18/9.61 | (43) all_536_0 = all_530_2 % 65.18/9.61 | % 65.18/9.61 | REDUCE: (33), (43) imply: % 65.18/9.61 | (44) $false % 65.18/9.61 | % 65.18/9.61 | CLOSE: (44) is inconsistent. % 65.18/9.61 | % 65.18/9.61 End of proof % 65.18/9.61 % SZS output end Proof for theBenchmark % 65.18/9.61 % 65.18/9.61 8997ms %------------------------------------------------------------------------------