%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP327_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 : n002.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 45.31s 7.70s % Output : Proof 80.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : ITP327_1 : TPTP v8.1.2. Released v8.0.0. % 0.14/0.15 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.37 % Computer : n002.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 300 % 0.15/0.37 % DateTime : Sun Aug 27 14:26:48 EDT 2023 % 0.15/0.37 % CPUTime : % 0.23/0.64 ________ _____ % 0.23/0.64 ___ __ \_________(_)________________________________ % 0.23/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.23/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.23/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.23/0.64 % 0.23/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.23/0.64 (2023-06-19) % 0.23/0.64 % 0.23/0.64 (c) Philipp Rümmer, 2009-2023 % 0.23/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.23/0.64 Amanda Stjerna. % 0.23/0.64 Free software under BSD-3-Clause. % 0.23/0.64 % 0.23/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.23/0.64 % 0.23/0.64 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.23/0.66 Running up to 7 provers in parallel. % 0.23/0.68 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.23/0.68 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.23/0.68 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.23/0.68 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.23/0.68 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.23/0.68 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.23/0.68 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 15.12/3.26 Prover 4: Preprocessing ... % 15.12/3.26 Prover 1: Preprocessing ... % 15.66/3.38 Prover 6: Preprocessing ... % 15.66/3.38 Prover 2: Preprocessing ... % 15.66/3.38 Prover 0: Preprocessing ... % 16.29/3.38 Prover 5: Preprocessing ... % 16.29/3.39 Prover 3: Preprocessing ... % 39.53/6.91 Prover 3: Warning: ignoring some quantifiers % 40.11/6.97 Prover 1: Warning: ignoring some quantifiers % 40.11/6.97 Prover 6: Proving ... % 40.11/7.01 Prover 3: Constructing countermodel ... % 41.06/7.11 Prover 1: Constructing countermodel ... % 45.31/7.70 Prover 3: proved (7016ms) % 45.31/7.70 % 45.31/7.70 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 45.31/7.70 % 45.31/7.70 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 45.31/7.71 Prover 6: stopped % 45.86/7.74 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 45.86/7.75 Prover 4: Warning: ignoring some quantifiers % 47.10/7.90 Prover 4: Constructing countermodel ... % 50.07/8.31 Prover 0: Proving ... % 50.07/8.31 Prover 0: stopped % 50.07/8.33 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 51.96/8.52 Prover 5: Proving ... % 51.96/8.52 Prover 5: stopped % 51.96/8.52 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 55.23/8.95 Prover 8: Preprocessing ... % 55.95/9.05 Prover 7: Preprocessing ... % 56.97/9.26 Prover 11: Preprocessing ... % 58.76/9.42 Prover 10: Preprocessing ... % 61.38/9.83 Prover 2: Proving ... % 61.38/9.83 Prover 2: stopped % 62.10/9.84 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 68.37/10.67 Prover 8: Warning: ignoring some quantifiers % 69.06/10.75 Prover 13: Preprocessing ... % 69.06/10.82 Prover 8: Constructing countermodel ... % 70.19/10.89 Prover 10: Warning: ignoring some quantifiers % 71.11/11.05 Prover 10: Constructing countermodel ... % 72.14/11.20 Prover 7: Warning: ignoring some quantifiers % 74.12/11.42 Prover 7: Constructing countermodel ... % 74.30/11.44 Prover 11: Warning: ignoring some quantifiers % 74.30/11.48 Prover 1: Found proof (size 16) % 74.30/11.48 Prover 1: proved (10812ms) % 74.30/11.48 Prover 8: stopped % 74.30/11.48 Prover 10: stopped % 74.30/11.48 Prover 4: stopped % 74.30/11.51 Prover 7: stopped % 75.26/11.60 Prover 11: Constructing countermodel ... % 75.26/11.61 Prover 11: stopped % 78.14/12.31 Prover 13: Warning: ignoring some quantifiers % 78.95/12.45 Prover 13: Constructing countermodel ... % 78.95/12.46 Prover 13: stopped % 78.95/12.46 % 78.95/12.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 78.95/12.46 % 78.95/12.47 % SZS output start Proof for theBenchmark % 79.23/12.52 Assumptions after simplification: % 79.23/12.52 --------------------------------- % 79.23/12.52 % 79.23/12.52 (axiom119) % 79.23/12.57 A_n_vec$(xa$) & A$(zero$) & N$(i$) & ? [v0: N_a_fun$] : (vec_nth$b(xa$) = v0 % 79.23/12.57 & fun_app$d(v0, i$) = zero$ & N_a_fun$(v0)) % 79.23/12.57 % 79.23/12.57 (axiom252) % 79.53/12.58 A_a_a_fun_fun$(times$e) & A$(zero$) & A$(one$) & ! [v0: A$] : ! [v1: A$] : % 79.53/12.58 ! [v2: A_a_fun$] : ! [v3: A$] : (v3 = v1 | ~ (fun_app$n(times$e, v0) = v2) | % 79.53/12.58 ~ (fun_app$m(v2, v1) = v3) | ~ A$(v1) | ~ A$(v0) | ( ~ (v1 = zero$) & ~ % 79.53/12.58 (v0 = one$))) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_a_fun$] : (v1 = % 79.53/12.58 zero$ | v0 = one$ | ~ (fun_app$n(times$e, v0) = v2) | ~ (fun_app$m(v2, v1) % 79.53/12.58 = v1) | ~ A$(v1) | ~ A$(v0)) % 79.53/12.58 % 79.53/12.58 (conjecture118) % 79.53/12.58 N_bool_fun$(uu$) & A_a_a_fun_fun$(times$e) & A_n_vec$(x$) & A_n_vec$(xa$) & % 79.53/12.58 A$(zero$) & N$(i$) & ? [v0: N_a_fun$] : ? [v1: N$] : ? [v2: A$] : ? [v3: % 79.53/12.58 A_a_fun$] : ? [v4: N_a_fun$] : ? [v5: A$] : ? [v6: A$] : ( ~ (v6 = zero$) % 79.53/12.58 & the$(uu$) = v1 & fun_app$n(times$e, v2) = v3 & fun_app$m(v3, v5) = v6 & % 79.53/12.58 vec_nth$b(x$) = v0 & vec_nth$b(xa$) = v4 & fun_app$d(v4, i$) = v5 & % 79.53/12.58 fun_app$d(v0, v1) = v2 & A_a_fun$(v3) & A$(v6) & A$(v5) & A$(v2) & % 79.53/12.58 N_a_fun$(v4) & N_a_fun$(v0) & N$(v1)) % 79.53/12.58 % 79.53/12.59 (function-axioms) % 79.83/12.71 ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: M$] : ! [v3: A$] : ! [v4: % 79.83/12.71 M$] : ! [v5: A_m_vec_m_vec$] : (v1 = v0 | ~ (uvy$(v5, v4, v3, v2) = v1) | % 79.83/12.71 ~ (uvy$(v5, v4, v3, v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! % 79.83/12.71 [v2: M$] : ! [v3: A$] : ! [v4: M$] : ! [v5: A_n_vec_m_vec$] : (v1 = v0 | ~ % 79.83/12.71 (uvz$(v5, v4, v3, v2) = v1) | ~ (uvz$(v5, v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! [v3: A$] : ! [v4: N$] : ! % 79.83/12.71 [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ (uwa$(v5, v4, v3, v2) = v1) | ~ % 79.83/12.71 (uwa$(v5, v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! % 79.83/12.71 [v2: M$] : ! [v3: A$] : ! [v4: M$] : ! [v5: A_m_vec_m_vec$] : (v1 = v0 | ~ % 79.83/12.71 (uvu$(v5, v4, v3, v2) = v1) | ~ (uvu$(v5, v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: M$] : ! [v3: A$] : ! [v4: N$] : ! % 79.83/12.71 [v5: A_n_vec_m_vec$] : (v1 = v0 | ~ (uvv$(v5, v4, v3, v2) = v1) | ~ % 79.83/12.71 (uvv$(v5, v4, v3, v2) = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! % 79.83/12.71 [v2: N$] : ! [v3: A$] : ! [v4: N$] : ! [v5: A_n_vec_n_vec$] : (v1 = v0 | ~ % 79.83/12.71 (uvw$(v5, v4, v3, v2) = v1) | ~ (uvw$(v5, v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: N$] : ! [v3: A$] : ! [v4: M$] : ! % 79.83/12.71 [v5: A_m_vec_n_vec$] : (v1 = v0 | ~ (uvx$(v5, v4, v3, v2) = v1) | ~ % 79.83/12.71 (uvx$(v5, v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! % 79.83/12.71 [v2: N$] : ! [v3: A$] : ! [v4: N$] : ! [v5: A_m_vec_n_vec$] : (v1 = v0 | ~ % 79.83/12.71 (uwb$(v5, v4, v3, v2) = v1) | ~ (uwb$(v5, v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: N$] : ! [v3: M$] : ! [v4: M$] : ! % 79.83/12.71 [v5: A_m_vec_n_vec$] : (v1 = v0 | ~ (uwv$(v5, v4, v3, v2) = v1) | ~ % 79.83/12.71 (uwv$(v5, v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! % 79.83/12.71 [v2: N$] : ! [v3: N$] : ! [v4: N$] : ! [v5: A_m_vec_n_vec$] : (v1 = v0 | ~ % 79.83/12.71 (uww$(v5, v4, v3, v2) = v1) | ~ (uww$(v5, v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: N$] : ! [v3: N$] : ! % 79.83/12.71 [v4: A_m_vec_n_vec$] : (v1 = v0 | ~ (interchange_rows$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (interchange_rows$(v4, v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 79.83/12.71 A_m_vec_n_vec$] : ! [v2: M$] : ! [v3: M$] : ! [v4: A_m_vec_n_vec$] : (v1 % 79.83/12.71 = v0 | ~ (interchange_columns$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (interchange_columns$(v4, v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 79.83/12.71 A_m_vec_n_vec$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_m_vec_n_vec$] : (v1 % 79.83/12.71 = v0 | ~ (mult_row$(v4, v3, v2) = v1) | ~ (mult_row$(v4, v3, v2) = v0)) & % 79.83/12.71 ! [v0: A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A$] : ! [v3: M$] : % 79.83/12.71 ! [v4: A_m_vec_n_vec$] : (v1 = v0 | ~ (mult_column$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (mult_column$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: % 79.83/12.71 N_a_m_vec_fun$] : ! [v2: N$] : ! [v3: N$] : ! [v4: A_m_vec_n_vec$] : (v1 % 79.83/12.71 = v0 | ~ (interchange_rows_row$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (interchange_rows_row$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! % 79.83/12.71 [v1: N_a_m_vec_fun$] : ! [v2: M$] : ! [v3: M$] : ! [v4: A_m_vec_n_vec$] : % 79.83/12.71 (v1 = v0 | ~ (interchange_columns_row$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (interchange_columns_row$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! % 79.83/12.71 [v1: N_a_m_vec_fun$] : ! [v2: A$] : ! [v3: M$] : ! [v4: A_m_vec_n_vec$] : % 79.83/12.71 (v1 = v0 | ~ (mult_column_row$c(v4, v3, v2) = v1) | ~ (mult_column_row$c(v4, % 79.83/12.71 v3, v2) = v0)) & ! [v0: M_a_m_vec_fun$] : ! [v1: M_a_m_vec_fun$] : ! % 79.83/12.71 [v2: A$] : ! [v3: M$] : ! [v4: A_m_vec_m_vec$] : (v1 = v0 | ~ % 79.83/12.71 (mult_column_row$b(v4, v3, v2) = v1) | ~ (mult_column_row$b(v4, v3, v2) = % 79.83/12.71 v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A$] : % 79.83/12.71 ! [v3: N$] : ! [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (mult_column_row$a(v4, % 79.83/12.71 v3, v2) = v1) | ~ (mult_column_row$a(v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 M_a_n_vec_fun$] : ! [v1: M_a_n_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! % 79.83/12.71 [v4: A_n_vec_m_vec$] : (v1 = v0 | ~ (mult_column_row$(v4, v3, v2) = v1) | ~ % 79.83/12.71 (mult_column_row$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: % 79.83/12.71 N_a_m_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_m_vec_n_vec$] : (v1 % 79.83/12.71 = v0 | ~ (mult_row_row$c(v4, v3, v2) = v1) | ~ (mult_row_row$c(v4, v3, v2) % 79.83/12.71 = v0)) & ! [v0: M_a_m_vec_fun$] : ! [v1: M_a_m_vec_fun$] : ! [v2: A$] : % 79.83/12.71 ! [v3: M$] : ! [v4: A_m_vec_m_vec$] : (v1 = v0 | ~ (mult_row_row$b(v4, v3, % 79.83/12.71 v2) = v1) | ~ (mult_row_row$b(v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! % 79.83/12.71 [v4: A_n_vec_n_vec$] : (v1 = v0 | ~ (mult_row_row$a(v4, v3, v2) = v1) | ~ % 79.83/12.71 (mult_row_row$a(v4, v3, v2) = v0)) & ! [v0: M_a_n_vec_fun$] : ! [v1: % 79.83/12.71 M_a_n_vec_fun$] : ! [v2: A$] : ! [v3: M$] : ! [v4: A_n_vec_m_vec$] : (v1 % 79.83/12.71 = v0 | ~ (mult_row_row$(v4, v3, v2) = v1) | ~ (mult_row_row$(v4, v3, v2) = % 79.83/12.71 v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 79.83/12.71 A_n_vec_a_n_vec_a_n_vec_fun_fun$] : ! [v3: A_n_vec_bool_fun$] : ! [v4: % 79.83/12.71 A_n_vec_bool_fun$] : (v1 = v0 | ~ (uxx$(v4, v3, v2) = v1) | ~ (uxx$(v4, % 79.83/12.71 v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! % 79.83/12.71 [v2: A$] : ! [v3: M$] : ! [v4: A_m_vec_n_vec$] : (v1 = v0 | ~ (uxg$(v4, v3, % 79.83/12.71 v2) = v1) | ~ (uxg$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! % 79.83/12.71 [v1: N_a_m_vec_fun$] : ! [v2: A$] : ! [v3: N$] : ! [v4: A_m_vec_n_vec$] : % 79.83/12.71 (v1 = v0 | ~ (uxh$(v4, v3, v2) = v1) | ~ (uxh$(v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: M$] : ! [v3: M$] : ! % 79.83/12.71 [v4: A_m_vec_n_vec$] : (v1 = v0 | ~ (uxi$(v4, v3, v2) = v1) | ~ (uxi$(v4, % 79.83/12.71 v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! % 79.83/12.71 [v2: N$] : ! [v3: N$] : ! [v4: A_m_vec_n_vec$] : (v1 = v0 | ~ (uym$(v4, v3, % 79.83/12.71 v2) = v1) | ~ (uym$(v4, v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : % 79.83/12.71 ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_a_fun$] : ! [v3: A_n_vec_a_fun$] % 79.83/12.71 : ! [v4: A_n_vec_set$] : (v1 = v0 | ~ (uyc$(v4, v3, v2) = v1) | ~ (uyc$(v4, % 79.83/12.71 v3, v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: N_bool_fun$] : ! [v2: % 79.83/12.71 N$] : ! [v3: N$] : ! [v4: tlbool] : (v1 = v0 | ~ (uuu$(v4, v3, v2) = v1) % 79.83/12.71 | ~ (uuu$(v4, v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: % 79.83/12.71 N_a_m_vec_fun$] : ! [v2: M$] : ! [v3: A_n_vec_m_vec$] : ! [v4: % 79.83/12.71 A_a_m_vec_fun$] : (v1 = v0 | ~ (uwc$(v4, v3, v2) = v1) | ~ (uwc$(v4, v3, % 79.83/12.71 v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: % 79.83/12.71 N$] : ! [v3: A_n_vec_n_vec$] : ! [v4: A_a_m_vec_fun$] : (v1 = v0 | ~ % 79.83/12.71 (uwe$(v4, v3, v2) = v1) | ~ (uwe$(v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : % 79.83/12.71 ! [v1: M_a_fun$] : ! [v2: M$] : ! [v3: A_m_vec_m_vec$] : ! [v4: A_a_fun$] : % 79.83/12.71 (v1 = v0 | ~ (uwg$(v4, v3, v2) = v1) | ~ (uwg$(v4, v3, v2) = v0)) & ! [v0: % 79.83/12.71 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: M$] : ! [v3: A_n_vec_m_vec$] : ! % 79.83/12.71 [v4: A_a_fun$] : (v1 = v0 | ~ (uwi$(v4, v3, v2) = v1) | ~ (uwi$(v4, v3, v2) % 79.83/12.71 = v0)) & ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: N$] : ! [v3: % 79.83/12.71 A_n_vec_n_vec$] : ! [v4: A_a_fun$] : (v1 = v0 | ~ (uwk$(v4, v3, v2) = v1) % 79.83/12.71 | ~ (uwk$(v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! % 79.83/12.71 [v2: N$] : ! [v3: A_m_vec_n_vec$] : ! [v4: A_a_fun$] : (v1 = v0 | ~ % 79.83/12.71 (uwm$(v4, v3, v2) = v1) | ~ (uwm$(v4, v3, v2) = v0)) & ! [v0: M_a_fun$] : % 79.83/12.71 ! [v1: M_a_fun$] : ! [v2: N$] : ! [v3: A_m_vec_m_vec_n_vec$] : ! [v4: % 79.83/12.71 A_m_vec_a_fun$] : (v1 = v0 | ~ (uwo$(v4, v3, v2) = v1) | ~ (uwo$(v4, v3, % 79.83/12.71 v2) = v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: N$] : ! % 79.83/12.71 [v3: A_n_vec_m_vec_n_vec$] : ! [v4: A_n_vec_a_fun$] : (v1 = v0 | ~ (uwq$(v4, % 79.83/12.71 v3, v2) = v1) | ~ (uwq$(v4, v3, v2) = v0)) & ! [v0: A_m_vec$] : ! % 79.83/12.71 [v1: A_m_vec$] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_a_m_vec_fun$] : (v1 = % 79.83/12.71 v0 | ~ (sum$a(v3, v2) = v1) | ~ (sum$a(v3, v2) = v0)) & ! [v0: A$] : ! % 79.83/12.71 [v1: A$] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ % 79.83/12.71 (sum$(v3, v2) = v1) | ~ (sum$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 79.83/12.71 ! [v1: MultipleValueBool] : ! [v2: A_set$] : ! [v3: A_set$] : (v1 = v0 | ~ % 79.83/12.71 (less_eq$c(v3, v2) = v1) | ~ (less_eq$c(v3, v2) = v0)) & ! [v0: % 79.83/12.71 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_m_vec_set$] : ! % 79.83/12.71 [v3: A_a_m_vec_a_m_vec_fun_fun$] : (v1 = v0 | ~ (dependent$b(v3, v2) = v1) | % 79.83/12.71 ~ (dependent$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.71 MultipleValueBool] : ! [v2: A_set$] : ! [v3: A_a_a_fun_fun$] : (v1 = v0 | % 79.83/12.71 ~ (dependent$a(v3, v2) = v1) | ~ (dependent$a(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_n_vec$] : ! % 79.83/12.71 [v3: A_m_vec$] : (v1 = v0 | ~ (vector_scalar_mult$b(v3, v2) = v1) | ~ % 79.83/12.71 (vector_scalar_mult$b(v3, v2) = v0)) & ! [v0: A_m_vec_a_m_vec_fun$] : ! % 79.83/12.71 [v1: A_m_vec_a_m_vec_fun$] : ! [v2: A$] : ! [v3: A_a_m_vec_a_m_vec_fun_fun$] % 79.83/12.71 : (v1 = v0 | ~ (fun_app$ah(v3, v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! % 79.83/12.71 [v0: A_n_vec_a_n_vec_fun$] : ! [v1: A_n_vec_a_n_vec_fun$] : ! [v2: A$] : ! % 79.83/12.71 [v3: A_a_n_vec_a_n_vec_fun_fun$] : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) | % 79.83/12.71 ~ (fun_app$ag(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.71 MultipleValueBool] : ! [v2: A_m_vec_n_vec$] : ! [v3: N$] : (v1 = v0 | ~ % 79.83/12.71 (is_zero_row$(v3, v2) = v1) | ~ (is_zero_row$(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] % 79.83/12.71 : ! [v3: A_n_vec_bool_fun$] : (v1 = v0 | ~ (minus$e(v3, v2) = v1) | ~ % 79.83/12.71 (minus$e(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.71 MultipleValueBool] : ! [v2: A_n_vec_bool_fun$] : ! [v3: A_n_vec_bool_fun$] % 79.83/12.71 : (v1 = v0 | ~ (less_eq$a(v3, v2) = v1) | ~ (less_eq$a(v3, v2) = v0)) & ! % 79.83/12.71 [v0: A_m_vec_set$] : ! [v1: A_m_vec_set$] : ! [v2: A_m_vec_set$] : ! [v3: % 79.83/12.71 A_m_vec$] : (v1 = v0 | ~ (insert$c(v3, v2) = v1) | ~ (insert$c(v3, v2) = % 79.83/12.71 v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: A_set$] : ! [v3: A$] : % 79.83/12.71 (v1 = v0 | ~ (insert$b(v3, v2) = v1) | ~ (insert$b(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_n_vec$] : ! % 79.83/12.71 [v3: A_m_vec_n_vec$] : (v1 = v0 | ~ (minus$d(v3, v2) = v1) | ~ (minus$d(v3, % 79.83/12.71 v2) = v0)) & ! [v0: A_n_vec_m_vec$] : ! [v1: A_n_vec_m_vec$] : ! [v2: % 79.83/12.71 A_n_vec_n_vec_m_vec$] : ! [v3: N$] : (v1 = v0 | ~ (column$g(v3, v2) = v1) % 79.83/12.71 | ~ (column$g(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 79.83/12.71 A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec_n_vec$] : ! [v3: N$] : (v1 = v0 | % 79.83/12.71 ~ (column$f(v3, v2) = v1) | ~ (column$f(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec_n_vec$] : ! [v1: A_m_vec_n_vec_n_vec$] : ! [v2: % 79.83/12.71 A_n_vec_n_vec$] : ! [v3: A_a_m_vec_fun$] : (v1 = v0 | ~ (map_matrix$k(v3, % 79.83/12.71 v2) = v1) | ~ (map_matrix$k(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec_m_vec$] : ! [v1: A_m_vec_n_vec_m_vec$] : ! [v2: % 79.83/12.71 A_n_vec_m_vec$] : ! [v3: A_a_m_vec_fun$] : (v1 = v0 | ~ (map_matrix$j(v3, % 79.83/12.71 v2) = v1) | ~ (map_matrix$j(v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : % 79.83/12.71 ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_m_vec_n_vec$] : ! [v3: M$] : (v1 = % 79.83/12.71 v0 | ~ (column$e(v3, v2) = v1) | ~ (column$e(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_n_vec_n_vec$] : % 79.83/12.71 ! [v3: N$] : (v1 = v0 | ~ (column$d(v3, v2) = v1) | ~ (column$d(v3, v2) = % 79.83/12.71 v0)) & ! [v0: A_n_vec_set_set$] : ! [v1: A_n_vec_set_set$] : ! [v2: % 79.83/12.71 A_n_vec_set_set$] : ! [v3: A_n_vec_set_set$] : (v1 = v0 | ~ (times$l(v3, % 79.83/12.71 v2) = v1) | ~ (times$l(v3, v2) = v0)) & ! [v0: A_set_set$] : ! [v1: % 79.83/12.71 A_set_set$] : ! [v2: A_set_set$] : ! [v3: A_set_set$] : (v1 = v0 | ~ % 79.83/12.71 (times$k(v3, v2) = v1) | ~ (times$k(v3, v2) = v0)) & ! [v0: % 79.83/12.71 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_set_set$] : ! % 79.83/12.71 [v3: A_set$] : (v1 = v0 | ~ (member$e(v3, v2) = v1) | ~ (member$e(v3, v2) = % 79.83/12.71 v0)) & ! [v0: A_m_vec_set$] : ! [v1: A_m_vec_set$] : ! [v2: % 79.83/12.71 A_m_vec_set$] : ! [v3: A_m_vec_set$] : (v1 = v0 | ~ (times$j(v3, v2) = v1) % 79.83/12.71 | ~ (times$j(v3, v2) = v0)) & ! [v0: A_m_vec_n_vec_set$] : ! [v1: % 79.83/12.71 A_m_vec_n_vec_set$] : ! [v2: A_m_vec_n_vec_set$] : ! [v3: % 79.83/12.71 A_m_vec_n_vec_set$] : (v1 = v0 | ~ (times$i(v3, v2) = v1) | ~ (times$i(v3, % 79.83/12.71 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 79.83/12.71 ! [v2: A_m_vec_n_vec_set$] : ! [v3: A_m_vec_n_vec$] : (v1 = v0 | ~ % 79.83/12.71 (member$d(v3, v2) = v1) | ~ (member$d(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_n_vec_m_vec_n_vec$] : % 79.83/12.71 ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ (map_matrix$i(v3, v2) = v1) | ~ % 79.83/12.71 (map_matrix$i(v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 79.83/12.71 A_m_vec_n_vec$] : ! [v2: A_m_vec_m_vec_n_vec$] : ! [v3: A_m_vec_a_fun$] : % 79.83/12.71 (v1 = v0 | ~ (map_matrix$h(v3, v2) = v1) | ~ (map_matrix$h(v3, v2) = v0)) & % 79.83/12.71 ! [v0: A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: % 79.83/12.71 A_n_vec_n_vec_n_vec$] : ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ % 79.83/12.71 (map_matrix$g(v3, v2) = v1) | ~ (map_matrix$g(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N$] : ! [v3: % 79.83/12.71 A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$k(v3, v2) = v1) | ~ % 79.83/12.71 (vec_nth$k(v3, v2) = v0)) & ! [v0: A_n_vec_n_vec$] : ! [v1: % 79.83/12.71 A_n_vec_n_vec$] : ! [v2: A_m_vec_n_vec_n_vec$] : ! [v3: A_m_vec_a_fun$] : % 79.83/12.71 (v1 = v0 | ~ (map_matrix$f(v3, v2) = v1) | ~ (map_matrix$f(v3, v2) = v0)) & % 79.83/12.71 ! [v0: A_n_vec_m_vec$] : ! [v1: A_n_vec_m_vec$] : ! [v2: % 79.83/12.71 A_n_vec_n_vec_m_vec$] : ! [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ % 79.83/12.71 (map_matrix$e(v3, v2) = v1) | ~ (map_matrix$e(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: M$] : ! [v3: % 79.83/12.71 A_n_vec_n_vec_m_vec$] : (v1 = v0 | ~ (vec_nth$j(v3, v2) = v1) | ~ % 79.83/12.71 (vec_nth$j(v3, v2) = v0)) & ! [v0: A_n_vec_m_vec$] : ! [v1: % 79.83/12.71 A_n_vec_m_vec$] : ! [v2: A_m_vec_n_vec_m_vec$] : ! [v3: A_m_vec_a_fun$] : % 79.83/12.71 (v1 = v0 | ~ (map_matrix$d(v3, v2) = v1) | ~ (map_matrix$d(v3, v2) = v0)) & % 79.83/12.71 ! [v0: A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: M$] : ! [v3: % 79.83/12.71 A_m_vec_n_vec_m_vec$] : (v1 = v0 | ~ (vec_nth$i(v3, v2) = v1) | ~ % 79.83/12.71 (vec_nth$i(v3, v2) = v0)) & ! [v0: A_m_vec_m_vec$] : ! [v1: % 79.83/12.71 A_m_vec_m_vec$] : ! [v2: A_m_vec_m_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | % 79.83/12.71 ~ (map_matrix$c(v3, v2) = v1) | ~ (map_matrix$c(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! % 79.83/12.71 [v3: A_a_fun$] : (v1 = v0 | ~ (map_matrix$b(v3, v2) = v1) | ~ % 79.83/12.71 (map_matrix$b(v3, v2) = v0)) & ! [v0: A_n_vec_m_vec$] : ! [v1: % 79.83/12.71 A_n_vec_m_vec$] : ! [v2: A_n_vec_m_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | % 79.83/12.71 ~ (map_matrix$a(v3, v2) = v1) | ~ (map_matrix$a(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_n_vec$] : ! % 79.83/12.71 [v3: A_a_fun$] : (v1 = v0 | ~ (map_matrix$(v3, v2) = v1) | ~ % 79.83/12.71 (map_matrix$(v3, v2) = v0)) & ! [v0: A_m_vec_bool_fun$] : ! [v1: % 79.83/12.71 A_m_vec_bool_fun$] : ! [v2: N$] : ! [v3: N_a_m_vec_bool_fun_fun$] : (v1 = % 79.83/12.71 v0 | ~ (fun_app$af(v3, v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: M$] : ! [v3: % 79.83/12.71 M_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ae(v3, v2) = v1) | ~ % 79.83/12.71 (fun_app$ae(v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : % 79.83/12.71 ! [v2: N$] : ! [v3: N_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = % 79.83/12.71 v1) | ~ (fun_app$ad(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 79.83/12.71 A_n_vec_bool_fun$] : ! [v2: N$] : ! [v3: N_a_n_vec_bool_fun_fun$] : (v1 = % 79.83/12.71 v0 | ~ (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: M$] : ! [v3: % 79.83/12.71 M_a_n_vec_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = v1) | ~ % 79.83/12.71 (fun_app$ab(v3, v2) = v0)) & ! [v0: A_m_vec_bool_fun$] : ! [v1: % 79.83/12.71 A_m_vec_bool_fun$] : ! [v2: M$] : ! [v3: M_a_m_vec_bool_fun_fun$] : (v1 = % 79.83/12.71 v0 | ~ (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: A_n_vec_n_vec$] : ! % 79.83/12.71 [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (times$h(v3, v2) = v1) | ~ (times$h(v3, % 79.83/12.71 v2) = v0)) & ! [v0: A_n_vec_m_vec$] : ! [v1: A_n_vec_m_vec$] : ! [v2: % 79.83/12.71 A_n_vec_m_vec$] : ! [v3: A_n_vec_m_vec$] : (v1 = v0 | ~ (times$g(v3, v2) = % 79.83/12.71 v1) | ~ (times$g(v3, v2) = v0)) & ! [v0: A_m_vec_m_vec$] : ! [v1: % 79.83/12.71 A_m_vec_m_vec$] : ! [v2: A_m_vec_m_vec$] : ! [v3: A_m_vec_m_vec$] : (v1 = % 79.83/12.71 v0 | ~ (times$f(v3, v2) = v1) | ~ (times$f(v3, v2) = v0)) & ! [v0: % 79.83/12.71 A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: A$] : ! [v3: A_a_m_vec_fun$] : (v1 % 79.83/12.71 = v0 | ~ (fun_app$z(v3, v2) = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A$] : ! [v1: A$] : ! [v2: A_m_vec$] : ! [v3: A_m_vec_a_fun$] : (v1 = v0 | % 79.83/12.72 ~ (fun_app$y(v3, v2) = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_m_vec$] : ! [v1: A_n_vec_m_vec$] : ! [v2: N$] : ! [v3: % 79.83/12.72 A_n_vec_m_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$h(v3, v2) = v1) | ~ % 79.83/12.72 (vec_nth$h(v3, v2) = v0)) & ! [v0: A_n_vec_a_n_vec_bool_fun_fun$] : ! [v1: % 79.83/12.72 A_n_vec_a_n_vec_bool_fun_fun$] : ! [v2: A_n_vec_a_n_vec_bool_fun_fun$] : ! % 79.83/12.72 [v3: A_n_vec_set$] : (v1 = v0 | ~ (uxt$(v3, v2) = v1) | ~ (uxt$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec_a_n_vec_bool_fun_fun$] : ! [v1: % 79.83/12.72 A_n_vec_a_n_vec_bool_fun_fun$] : ! [v2: A_n_vec$] : ! [v3: tlbool] : (v1 = % 79.83/12.72 v0 | ~ (uut$(v3, v2) = v1) | ~ (uut$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 79.83/12.72 A_n_vec_a_n_vec_bool_fun_fun$] : ! [v3: A_n_vec_bool_fun$] : (v1 = v0 | ~ % 79.83/12.72 (uxp$(v3, v2) = v1) | ~ (uxp$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : % 79.83/12.72 ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_a_n_vec_fun$] : ! [v3: % 79.83/12.72 A_n_vec_bool_fun$] : (v1 = v0 | ~ (uxy$(v3, v2) = v1) | ~ (uxy$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: M_a_m_vec_n_vec_fun$] : ! [v1: M_a_m_vec_n_vec_fun$] : ! % 79.83/12.72 [v2: A_n_vec_m_vec$] : ! [v3: A_a_m_vec_fun$] : (v1 = v0 | ~ (uwd$(v3, v2) = % 79.83/12.72 v1) | ~ (uwd$(v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 79.83/12.72 A_m_vec_n_vec$] : ! [v2: M$] : ! [v3: M_a_m_vec_n_vec_fun$] : (v1 = v0 | % 79.83/12.72 ~ (fun_app$x(v3, v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_m_vec_n_vec_fun$] : ! [v1: N_a_m_vec_n_vec_fun$] : ! [v2: % 79.83/12.72 A_n_vec_n_vec$] : ! [v3: A_a_m_vec_fun$] : (v1 = v0 | ~ (uwf$(v3, v2) = % 79.83/12.72 v1) | ~ (uwf$(v3, v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 79.83/12.72 A_m_vec_n_vec$] : ! [v2: N$] : ! [v3: N_a_m_vec_n_vec_fun$] : (v1 = v0 | % 79.83/12.72 ~ (fun_app$w(v3, v2) = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: % 79.83/12.72 M_a_m_vec_fun$] : ! [v1: M_a_m_vec_fun$] : ! [v2: A_m_vec_m_vec$] : ! % 79.83/12.72 [v3: A_a_fun$] : (v1 = v0 | ~ (uwh$(v3, v2) = v1) | ~ (uwh$(v3, v2) = v0)) & % 79.83/12.72 ! [v0: M_a_n_vec_fun$] : ! [v1: M_a_n_vec_fun$] : ! [v2: A_n_vec_m_vec$] : % 79.83/12.72 ! [v3: A_a_fun$] : (v1 = v0 | ~ (uwj$(v3, v2) = v1) | ~ (uwj$(v3, v2) = v0)) % 79.83/12.72 & ! [v0: N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] % 79.83/12.72 : ! [v3: A_a_fun$] : (v1 = v0 | ~ (uwl$(v3, v2) = v1) | ~ (uwl$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: % 79.83/12.72 A_m_vec_n_vec$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (uwn$(v3, v2) = v1) | ~ % 79.83/12.72 (uwn$(v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : % 79.83/12.72 ! [v2: A_m_vec_m_vec_n_vec$] : ! [v3: A_m_vec_a_fun$] : (v1 = v0 | ~ % 79.83/12.72 (uwp$(v3, v2) = v1) | ~ (uwp$(v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! % 79.83/12.72 [v1: N_a_m_vec_fun$] : ! [v2: A_n_vec_m_vec_n_vec$] : ! [v3: A_n_vec_a_fun$] % 79.83/12.72 : (v1 = v0 | ~ (uwr$(v3, v2) = v1) | ~ (uwr$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: A_m_vec$] : ! [v3: A$] : (v1 = v0 | % 79.83/12.72 ~ (uyf$(v3, v2) = v1) | ~ (uyf$(v3, v2) = v0)) & ! [v0: N_a_fun$] : ! % 79.83/12.72 [v1: N_a_fun$] : ! [v2: A_n_vec$] : ! [v3: A$] : (v1 = v0 | ~ (uyh$(v3, v2) % 79.83/12.72 = v1) | ~ (uyh$(v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: % 79.83/12.72 N_a_m_vec_fun$] : ! [v2: A_m_vec_n_vec$] : ! [v3: A_m_vec$] : (v1 = v0 | % 79.83/12.72 ~ (uyg$(v3, v2) = v1) | ~ (uyg$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] % 79.83/12.72 : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] : ! [v3: A_n_vec$] % 79.83/12.72 : (v1 = v0 | ~ (uxu$(v3, v2) = v1) | ~ (uxu$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] % 79.83/12.72 : ! [v3: A_n_vec_bool_fun$] : (v1 = v0 | ~ (uxn$(v3, v2) = v1) | ~ % 79.83/12.72 (uxn$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] : ! [v3: A_n_vec_bool_fun$] % 79.83/12.72 : (v1 = v0 | ~ (uxm$(v3, v2) = v1) | ~ (uxm$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: A_m_vec_m_vec$] : ! [v3: M$] : (v1 % 79.83/12.72 = v0 | ~ (uvo$(v3, v2) = v1) | ~ (uvo$(v3, v2) = v0)) & ! [v0: N_a_fun$] % 79.83/12.72 : ! [v1: N_a_fun$] : ! [v2: A_m_vec_n_vec$] : ! [v3: M$] : (v1 = v0 | ~ % 79.83/12.72 (uvq$(v3, v2) = v1) | ~ (uvq$(v3, v2) = v0)) & ! [v0: A_m_vec_m_vec$] : ! % 79.83/12.72 [v1: A_m_vec_m_vec$] : ! [v2: N$] : ! [v3: A_m_vec_m_vec_n_vec$] : (v1 = v0 % 79.83/12.72 | ~ (vec_nth$g(v3, v2) = v1) | ~ (vec_nth$g(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: A_m_vec_m_vec_n_vec$] : % 79.83/12.72 ! [v3: M$] : (v1 = v0 | ~ (uvm$(v3, v2) = v1) | ~ (uvm$(v3, v2) = v0)) & ! % 79.83/12.72 [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: A_n_vec_m_vec$] : ! [v3: N$] : % 79.83/12.72 (v1 = v0 | ~ (uvn$(v3, v2) = v1) | ~ (uvn$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec_n_vec$] : ! [v3: N$] : (v1 % 79.83/12.72 = v0 | ~ (uvp$(v3, v2) = v1) | ~ (uvp$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: N$] : ! [v3: % 79.83/12.72 A_m_vec_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$f(v3, v2) = v1) | ~ % 79.83/12.72 (vec_nth$f(v3, v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: % 79.83/12.72 N_a_m_vec_fun$] : ! [v2: A_m_vec_n_vec_n_vec$] : ! [v3: N$] : (v1 = v0 | % 79.83/12.72 ~ (uvl$(v3, v2) = v1) | ~ (uvl$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] % 79.83/12.72 : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_set$] : % 79.83/12.72 (v1 = v0 | ~ (uxw$(v3, v2) = v1) | ~ (uxw$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : ! % 79.83/12.72 [v3: A_n_vec_a_fun$] : (v1 = v0 | ~ (uyk$(v3, v2) = v1) | ~ (uyk$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 79.83/12.72 A_n_vec_set$] : ! [v3: A_n_vec_a_m_vec_fun$] : (v1 = v0 | ~ (uyl$(v3, v2) % 79.83/12.72 = v1) | ~ (uyl$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v2: A_n_vec_a_fun$] : ! [v3: A_n_vec_set$] : (v1 = % 79.83/12.72 v0 | ~ (uyb$(v3, v2) = v1) | ~ (uyb$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_a_fun$] : % 79.83/12.72 ! [v3: A_n_vec_set$] : (v1 = v0 | ~ (uyi$(v3, v2) = v1) | ~ (uyi$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: A_n_vec$] : ! [v3: % 79.83/12.72 A_n_vec_a_fun$] : (v1 = v0 | ~ (fun_app$v(v3, v2) = v1) | ~ (fun_app$v(v3, % 79.83/12.72 v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : % 79.83/12.72 ! [v2: A_n_vec_a_m_vec_fun$] : ! [v3: A_n_vec_set$] : (v1 = v0 | ~ (uyj$(v3, % 79.83/12.72 v2) = v1) | ~ (uyj$(v3, v2) = v0)) & ! [v0: A_m_vec$] : ! [v1: % 79.83/12.72 A_m_vec$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_a_m_vec_fun$] : (v1 = v0 | % 79.83/12.72 ~ (fun_app$u(v3, v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] % 79.83/12.72 : ! [v3: A_n_vec$] : (v1 = v0 | ~ (uya$(v3, v2) = v1) | ~ (uya$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v3: A_n_vec$] : (v1 = v0 | ~ (uxz$(v3, v2) = v1) | % 79.83/12.72 ~ (uxz$(v3, v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v2: A_n_vec_bool_fun$] : ! [v3: A_n_vec_set$] : % 79.83/12.72 (v1 = v0 | ~ (uxs$(v3, v2) = v1) | ~ (uxs$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : ! % 79.83/12.72 [v3: A_n_vec$] : (v1 = v0 | ~ (uxv$(v3, v2) = v1) | ~ (uxv$(v3, v2) = v0)) & % 79.83/12.72 ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: A_m_vec$] : ! [v3: A_m_vec$] % 79.83/12.72 : (v1 = v0 | ~ (uxk$(v3, v2) = v1) | ~ (uxk$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec$] : (v1 % 79.83/12.72 = v0 | ~ (uxj$(v3, v2) = v1) | ~ (uxj$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: A_m_vec_n_vec$] : ! % 79.83/12.72 [v3: A_m_vec_n_vec$] : (v1 = v0 | ~ (uxl$(v3, v2) = v1) | ~ (uxl$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: M_a_fun$] : ! [v1: M_a_fun$] : ! [v2: A_m_vec$] : ! [v3: % 79.83/12.72 A_m_vec$] : (v1 = v0 | ~ (uvh$(v3, v2) = v1) | ~ (uvh$(v3, v2) = v0)) & ! % 79.83/12.72 [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : ! [v3: A_n_vec$] : % 79.83/12.72 (v1 = v0 | ~ (uvg$(v3, v2) = v1) | ~ (uvg$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 M_a_m_vec_fun$] : ! [v1: M_a_m_vec_fun$] : ! [v2: A_m_vec_m_vec$] : ! % 79.83/12.72 [v3: A_m_vec_m_vec$] : (v1 = v0 | ~ (uvd$(v3, v2) = v1) | ~ (uvd$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: M$] : ! [v3: % 79.83/12.72 M_a_m_vec_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, % 79.83/12.72 v2) = v0)) & ! [v0: N_a_m_vec_fun$] : ! [v1: N_a_m_vec_fun$] : ! [v2: % 79.83/12.72 A_m_vec_n_vec$] : ! [v3: A_m_vec_n_vec$] : (v1 = v0 | ~ (uvi$(v3, v2) = % 79.83/12.72 v1) | ~ (uvi$(v3, v2) = v0)) & ! [v0: M_a_n_vec_fun$] : ! [v1: % 79.83/12.72 M_a_n_vec_fun$] : ! [v2: A_n_vec_m_vec$] : ! [v3: A_n_vec_m_vec$] : (v1 = % 79.83/12.72 v0 | ~ (uve$(v3, v2) = v1) | ~ (uve$(v3, v2) = v0)) & ! [v0: A_n_vec$] : % 79.83/12.72 ! [v1: A_n_vec$] : ! [v2: M$] : ! [v3: M_a_n_vec_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: % 79.83/12.72 N_a_n_vec_fun$] : ! [v1: N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : ! % 79.83/12.72 [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (uvf$(v3, v2) = v1) | ~ (uvf$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: N$] : ! [v3: % 79.83/12.72 N_a_n_vec_fun$] : (v1 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, % 79.83/12.72 v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: N_bool_fun$] : ! [v2: N$] : % 79.83/12.72 ! [v3: A_n_vec_n_vec$] : (v1 = v0 | ~ (uwy$(v3, v2) = v1) | ~ (uwy$(v3, v2) % 79.83/12.72 = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_n_vec$] : % 79.83/12.72 ! [v3: N$] : (v1 = v0 | ~ (column$c(v3, v2) = v1) | ~ (column$c(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_n_vec$] : % 79.83/12.72 ! [v3: N$] : (v1 = v0 | ~ (row$c(v3, v2) = v1) | ~ (row$c(v3, v2) = v0)) & % 79.83/12.72 ! [v0: N_bool_fun$] : ! [v1: N_bool_fun$] : ! [v2: M$] : ! [v3: % 79.83/12.72 A_n_vec_m_vec$] : (v1 = v0 | ~ (uxa$(v3, v2) = v1) | ~ (uxa$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: A_n_vec_m_vec$] : % 79.83/12.72 ! [v3: N$] : (v1 = v0 | ~ (column$b(v3, v2) = v1) | ~ (column$b(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_n_vec_m_vec$] : % 79.83/12.72 ! [v3: M$] : (v1 = v0 | ~ (row$b(v3, v2) = v1) | ~ (row$b(v3, v2) = v0)) & % 79.83/12.72 ! [v0: M_bool_fun$] : ! [v1: M_bool_fun$] : ! [v2: M$] : ! [v3: % 79.83/12.72 A_m_vec_m_vec$] : (v1 = v0 | ~ (uxc$(v3, v2) = v1) | ~ (uxc$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: A_m_vec_m_vec$] : % 79.83/12.72 ! [v3: M$] : (v1 = v0 | ~ (column$a(v3, v2) = v1) | ~ (column$a(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: A_m_vec_m_vec$] : % 79.83/12.72 ! [v3: M$] : (v1 = v0 | ~ (row$a(v3, v2) = v1) | ~ (row$a(v3, v2) = v0)) & % 79.83/12.72 ! [v0: M_bool_fun$] : ! [v1: M_bool_fun$] : ! [v2: N$] : ! [v3: % 79.83/12.72 A_m_vec_n_vec$] : (v1 = v0 | ~ (uxe$(v3, v2) = v1) | ~ (uxe$(v3, v2) = % 79.83/12.72 v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: % 79.83/12.72 A_n_vec$] : ! [v3: A_n_vec_a_n_vec_bool_fun_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$q(v3, v2) = v1) | ~ (fun_app$q(v3, v2) = v0)) & ! [v0: % 79.83/12.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A$] : ! [v3: % 79.83/12.72 A_bool_fun$] : (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, % 79.83/12.72 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 79.83/12.72 ! [v2: A_set$] : ! [v3: A$] : (v1 = v0 | ~ (member$c(v3, v2) = v1) | ~ % 79.83/12.72 (member$c(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_n_vec_set_set$] : ! [v3: A_n_vec_set$] : (v1 % 79.83/12.72 = v0 | ~ (member$b(v3, v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: % 79.83/12.72 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_m_vec$] : ! % 79.83/12.72 [v3: A_m_vec_bool_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 79.83/12.72 (fun_app$o(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_m_vec_set$] : ! [v3: A_m_vec$] : (v1 = v0 | % 79.83/12.72 ~ (member$a(v3, v2) = v1) | ~ (member$a(v3, v2) = v0)) & ! [v0: A_a_fun$] % 79.83/12.72 : ! [v1: A_a_fun$] : ! [v2: A$] : ! [v3: A_a_a_fun_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: A$] : ! % 79.83/12.72 [v1: A$] : ! [v2: A$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) % 79.83/12.72 = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : % 79.83/12.72 ! [v2: A_set$] : ! [v3: A_set_a_set_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) % 79.83/12.72 = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: A_m_vec$] : ! [v1: % 79.83/12.72 A_m_vec$] : ! [v2: A_m_vec$] : ! [v3: A_m_vec_a_m_vec_fun$] : (v1 = v0 | % 79.83/12.72 ~ (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_a_n_vec_fun$] : ! [v1: A_n_vec_a_n_vec_fun$] : ! [v2: A_n_vec$] : % 79.83/12.72 ! [v3: A_n_vec_a_n_vec_a_n_vec_fun_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = % 79.83/12.72 v1) | ~ (fun_app$j(v3, v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] % 79.83/12.72 : ! [v2: A_n_vec$] : ! [v3: A_n_vec_a_n_vec_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_m_vec_n_vec$] : ! [v1: A_m_vec_n_vec$] : ! [v2: A_m_vec_n_vec$] : ! % 79.83/12.72 [v3: A_m_vec_n_vec_a_m_vec_n_vec_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = % 79.83/12.72 v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_n_vec_set$] : ! [v3: A_n_vec_set_bool_fun$] % 79.83/12.72 : (v1 = v0 | ~ (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! % 79.83/12.72 [v0: N_set$] : ! [v1: N_set$] : ! [v2: N_set$] : ! [v3: N$] : (v1 = v0 | ~ % 79.83/12.72 (insert$a(v3, v2) = v1) | ~ (insert$a(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_set$] : ! [v3: % 79.83/12.72 A_n_vec_set_a_n_vec_set_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | ~ % 79.83/12.72 (fun_app$f(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_n_vec$] : ! [v3: A_n_vec_bool_fun$] : (v1 = % 79.83/12.72 v0 | ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: A_m_vec_n_vec$] : ! [v3: M$] : (v1 % 79.83/12.72 = v0 | ~ (column$(v3, v2) = v1) | ~ (column$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: A_m_vec_n_vec$] : ! [v3: N$] : (v1 % 79.83/12.72 = v0 | ~ (row$(v3, v2) = v1) | ~ (row$(v3, v2) = v0)) & ! [v0: A$] : ! % 79.83/12.72 [v1: A$] : ! [v2: N$] : ! [v3: N_a_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) % 79.83/12.72 = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 79.83/12.72 [v1: MultipleValueBool] : ! [v2: N$] : ! [v3: N_bool_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: A_m_vec$] % 79.83/12.72 : ! [v1: A_m_vec$] : ! [v2: N$] : ! [v3: N_a_m_vec_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: A$] : ! % 79.83/12.72 [v1: A$] : ! [v2: M$] : ! [v3: M_a_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) % 79.83/12.72 = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 79.83/12.72 [v1: MultipleValueBool] : ! [v2: M$] : ! [v3: M_bool_fun$] : (v1 = v0 | ~ % 79.83/12.72 (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: % 79.83/12.72 A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : ! [v2: % 79.83/12.72 A_n_vec_set$] : (v1 = v0 | ~ (less$b(v2) = v1) | ~ (less$b(v2) = v0)) & ! % 79.83/12.72 [v0: M_bool_fun$] : ! [v1: M_bool_fun$] : ! [v2: M$] : (v1 = v0 | ~ % 79.83/12.72 (less$a(v2) = v1) | ~ (less$a(v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: % 79.83/12.72 N_bool_fun$] : ! [v2: N$] : (v1 = v0 | ~ (less$(v2) = v1) | ~ (less$(v2) % 79.83/12.72 = v0)) & ! [v0: A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : % 79.83/12.72 ! [v2: A_a_n_vec_a_n_vec_fun_fun$] : (v1 = v0 | ~ (dependent$(v2) = v1) | ~ % 79.83/12.72 (dependent$(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: % 79.83/12.72 A_n_vec_set$] : (v1 = v0 | ~ (the_elem$a(v2) = v1) | ~ (the_elem$a(v2) = % 79.83/12.72 v0)) & ! [v0: N$] : ! [v1: N$] : ! [v2: N_set$] : (v1 = v0 | ~ % 79.83/12.72 (the_elem$(v2) = v1) | ~ (the_elem$(v2) = v0)) & ! [v0: A_n_vec_set$] : ! % 79.83/12.72 [v1: A_n_vec_set$] : ! [v2: A_n_vec_set_bool_fun$] : (v1 = v0 | ~ % 79.83/12.72 (least$b(v2) = v1) | ~ (least$b(v2) = v0)) & ! [v0: M_bool_fun$] : ! [v1: % 79.83/12.72 M_bool_fun$] : ! [v2: M$] : (v1 = v0 | ~ (less_eq$b(v2) = v1) | ~ % 79.83/12.72 (less_eq$b(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_n_vec_set_set$] : (v1 = v0 | ~ (finite$b(v2) % 79.83/12.72 = v1) | ~ (finite$b(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_set$] : (v1 = v0 | ~ (finite$a(v2) = v1) | % 79.83/12.72 ~ (finite$a(v2) = v0)) & ! [v0: A_n_vec_set_a_n_vec_set_fun$] : ! [v1: % 79.83/12.72 A_n_vec_set_a_n_vec_set_fun$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ % 79.83/12.72 (minus$b(v2) = v1) | ~ (minus$b(v2) = v0)) & ! [v0: A_n_vec_set$] : ! % 79.83/12.72 [v1: A_n_vec_set$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ (col_space$(v2) = % 79.83/12.72 v1) | ~ (col_space$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 79.83/12.72 MultipleValueBool] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ % 79.83/12.72 (reduced_row_echelon_form$e(v2) = v1) | ~ (reduced_row_echelon_form$e(v2) = % 79.83/12.72 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 79.83/12.72 A_m_vec_m_vec$] : (v1 = v0 | ~ (reduced_row_echelon_form$d(v2) = v1) | ~ % 79.83/12.72 (reduced_row_echelon_form$d(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 79.83/12.72 [v1: MultipleValueBool] : ! [v2: A_n_vec_m_vec$] : (v1 = v0 | ~ % 79.83/12.72 (reduced_row_echelon_form$c(v2) = v1) | ~ (reduced_row_echelon_form$c(v2) = % 79.83/12.72 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 79.83/12.72 A_n_vec_n_vec_m_vec$] : (v1 = v0 | ~ (reduced_row_echelon_form$b(v2) = v1) % 79.83/12.72 | ~ (reduced_row_echelon_form$b(v2) = v0)) & ! [v0: MultipleValueBool] : % 79.83/12.72 ! [v1: MultipleValueBool] : ! [v2: A_n_vec_n_vec_n_vec$] : (v1 = v0 | ~ % 80.24/12.72 (reduced_row_echelon_form$a(v2) = v1) | ~ (reduced_row_echelon_form$a(v2) = % 80.24/12.72 v0)) & ! [v0: A_m_vec_n_vec_n_vec$] : ! [v1: A_m_vec_n_vec_n_vec$] : ! % 80.24/12.72 [v2: N_a_m_vec_n_vec_fun$] : (v1 = v0 | ~ (vec_lambda$g(v2) = v1) | ~ % 80.24/12.72 (vec_lambda$g(v2) = v0)) & ! [v0: A_m_vec_n_vec_m_vec$] : ! [v1: % 80.24/12.72 A_m_vec_n_vec_m_vec$] : ! [v2: M_a_m_vec_n_vec_fun$] : (v1 = v0 | ~ % 80.24/12.72 (vec_lambda$f(v2) = v1) | ~ (vec_lambda$f(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_n_vec$] : ! [v1: A_n_vec_n_vec$] : ! [v2: N_a_n_vec_fun$] : (v1 = % 80.24/12.72 v0 | ~ (vec_lambda$e(v2) = v1) | ~ (vec_lambda$e(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_m_vec$] : ! [v1: A_n_vec_m_vec$] : ! [v2: M_a_n_vec_fun$] : (v1 = % 80.24/12.72 v0 | ~ (vec_lambda$d(v2) = v1) | ~ (vec_lambda$d(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_m_vec$] : ! [v1: A_m_vec_m_vec$] : ! [v2: M_a_m_vec_fun$] : (v1 = % 80.24/12.72 v0 | ~ (vec_lambda$c(v2) = v1) | ~ (vec_lambda$c(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_set$] : ! [v1: A_n_vec_set$] : ! [v2: A_n_vec_bool_fun$] : (v1 = % 80.24/12.72 v0 | ~ (collect$c(v2) = v1) | ~ (collect$c(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_set_set$] : ! [v1: A_n_vec_set_set$] : ! [v2: % 80.24/12.72 A_n_vec_set_bool_fun$] : (v1 = v0 | ~ (collect$b(v2) = v1) | ~ % 80.24/12.72 (collect$b(v2) = v0)) & ! [v0: A_m_vec_set$] : ! [v1: A_m_vec_set$] : ! % 80.24/12.72 [v2: A_m_vec_bool_fun$] : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ % 80.24/12.72 (collect$a(v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 80.24/12.72 A_bool_fun$] : (v1 = v0 | ~ (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & % 80.24/12.72 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 80.24/12.72 A_m_vec_n_vec$] : (v1 = v0 | ~ (reduced_row_echelon_form$(v2) = v1) | ~ % 80.24/12.72 (reduced_row_echelon_form$(v2) = v0)) & ! [v0: A_n_vec_set$] : ! [v1: % 80.24/12.72 A_n_vec_set$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ (columns$(v2) = v1) % 80.24/12.72 | ~ (columns$(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: A_n_vec$] : ! [v2: % 80.24/12.72 A_n_vec_bool_fun$] : (v1 = v0 | ~ (the$a(v2) = v1) | ~ (the$a(v2) = v0)) & % 80.24/12.72 ! [v0: N$] : ! [v1: N$] : ! [v2: N_bool_fun$] : (v1 = v0 | ~ (the$(v2) = % 80.24/12.72 v1) | ~ (the$(v2) = v0)) & ! [v0: A_m_vec_n_vec$] : ! [v1: % 80.24/12.72 A_m_vec_n_vec$] : ! [v2: N_a_m_vec_fun$] : (v1 = v0 | ~ (vec_lambda$b(v2) % 80.24/12.72 = v1) | ~ (vec_lambda$b(v2) = v0)) & ! [v0: A_n_vec$] : ! [v1: % 80.24/12.72 A_n_vec$] : ! [v2: N_a_fun$] : (v1 = v0 | ~ (vec_lambda$a(v2) = v1) | ~ % 80.24/12.72 (vec_lambda$a(v2) = v0)) & ! [v0: A_m_vec$] : ! [v1: A_m_vec$] : ! [v2: % 80.24/12.72 M_a_fun$] : (v1 = v0 | ~ (vec_lambda$(v2) = v1) | ~ (vec_lambda$(v2) = % 80.24/12.72 v0)) & ! [v0: A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : (v1 = v0 | ~ % 80.24/12.72 (minus$a(v2) = v1) | ~ (minus$a(v2) = v0)) & ! [v0: A_m_vec_a_m_vec_fun$] % 80.24/12.72 : ! [v1: A_m_vec_a_m_vec_fun$] : ! [v2: A_m_vec$] : (v1 = v0 | ~ % 80.24/12.72 (minus$(v2) = v1) | ~ (minus$(v2) = v0)) & ! [v0: M_a_m_vec_fun$] : ! % 80.24/12.72 [v1: M_a_m_vec_fun$] : ! [v2: A_m_vec_m_vec$] : (v1 = v0 | ~ (vec_nth$e(v2) % 80.24/12.72 = v1) | ~ (vec_nth$e(v2) = v0)) & ! [v0: M_a_n_vec_fun$] : ! [v1: % 80.24/12.72 M_a_n_vec_fun$] : ! [v2: A_n_vec_m_vec$] : (v1 = v0 | ~ (vec_nth$d(v2) = % 80.24/12.72 v1) | ~ (vec_nth$d(v2) = v0)) & ! [v0: N_a_n_vec_fun$] : ! [v1: % 80.24/12.72 N_a_n_vec_fun$] : ! [v2: A_n_vec_n_vec$] : (v1 = v0 | ~ (vec_nth$c(v2) = % 80.24/12.72 v1) | ~ (vec_nth$c(v2) = v0)) & ! [v0: A_n_vec_a_n_vec_bool_fun_fun$] : % 80.24/12.72 ! [v1: A_n_vec_a_n_vec_bool_fun_fun$] : ! [v2: A_n_vec_a_n_vec_bool_fun_fun$] % 80.24/12.72 : (v1 = v0 | ~ (uxq$(v2) = v1) | ~ (uxq$(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_bool_fun$] : ! [v1: A_m_vec_bool_fun$] : ! [v2: A_m_vec_n_vec$] : % 80.24/12.72 (v1 = v0 | ~ (uwx$(v2) = v1) | ~ (uwx$(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_n_vec$] : % 80.24/12.72 (v1 = v0 | ~ (uwz$(v2) = v1) | ~ (uwz$(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_bool_fun$] : ! [v1: A_m_vec_bool_fun$] : ! [v2: A_n_vec_m_vec$] : % 80.24/12.72 (v1 = v0 | ~ (uxb$(v2) = v1) | ~ (uxb$(v2) = v0)) & ! [v0: N$] : ! [v1: % 80.24/12.72 N$] : ! [v2: N_bool_fun$] : (v1 = v0 | ~ (least$a(v2) = v1) | ~ % 80.24/12.72 (least$a(v2) = v0)) & ! [v0: A_m_vec_bool_fun$] : ! [v1: % 80.24/12.72 A_m_vec_bool_fun$] : ! [v2: A_m_vec_m_vec$] : (v1 = v0 | ~ (uxd$(v2) = v1) % 80.24/12.72 | ~ (uxd$(v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: % 80.24/12.72 A_n_vec_bool_fun$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ (uxf$(v2) = v1) % 80.24/12.72 | ~ (uxf$(v2) = v0)) & ! [v0: N_bool_fun$] : ! [v1: N_bool_fun$] : ! % 80.24/12.72 [v2: N$] : (v1 = v0 | ~ (uui$(v2) = v1) | ~ (uui$(v2) = v0)) & ! [v0: % 80.24/12.72 N_bool_fun$] : ! [v1: N_bool_fun$] : ! [v2: N$] : (v1 = v0 | ~ (uug$(v2) % 80.24/12.72 = v1) | ~ (uug$(v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] % 80.24/12.72 : ! [v2: A_set$] : (v1 = v0 | ~ (uuj$(v2) = v1) | ~ (uuj$(v2) = v0)) & ! % 80.24/12.72 [v0: A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : ! [v2: % 80.24/12.72 A_n_vec_set_set$] : (v1 = v0 | ~ (uul$(v2) = v1) | ~ (uul$(v2) = v0)) & ! % 80.24/12.72 [v0: A_m_vec_bool_fun$] : ! [v1: A_m_vec_bool_fun$] : ! [v2: A_m_vec_set$] : % 80.24/12.72 (v1 = v0 | ~ (uuk$(v2) = v1) | ~ (uuk$(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : ! [v2: A_n_vec_set$] : % 80.24/12.72 (v1 = v0 | ~ (uum$(v2) = v1) | ~ (uum$(v2) = v0)) & ! [v0: % 80.24/12.72 A_n_vec_set_bool_fun$] : ! [v1: A_n_vec_set_bool_fun$] : ! [v2: A_n_vec$] % 80.24/12.72 : (v1 = v0 | ~ (member$(v2) = v1) | ~ (member$(v2) = v0)) & ! [v0: % 80.24/12.72 A_a_fun$] : ! [v1: A_a_fun$] : ! [v2: A$] : (v1 = v0 | ~ (uvc$(v2) = v1) % 80.24/12.72 | ~ (uvc$(v2) = v0)) & ! [v0: A_set_a_set_fun$] : ! [v1: % 80.24/12.72 A_set_a_set_fun$] : ! [v2: A_set$] : (v1 = v0 | ~ (uva$(v2) = v1) | ~ % 80.24/12.72 (uva$(v2) = v0)) & ! [v0: A_set_a_set_fun$] : ! [v1: A_set_a_set_fun$] : % 80.24/12.72 ! [v2: A_set$] : (v1 = v0 | ~ (times$d(v2) = v1) | ~ (times$d(v2) = v0)) & % 80.24/12.72 ! [v0: A_n_vec_set_a_n_vec_set_fun$] : ! [v1: A_n_vec_set_a_n_vec_set_fun$] : % 80.24/12.72 ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (uvb$(v2) = v1) | ~ (uvb$(v2) = v0)) & % 80.24/12.72 ! [v0: A_n_vec_set_a_n_vec_set_fun$] : ! [v1: A_n_vec_set_a_n_vec_set_fun$] : % 80.24/12.72 ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (times$c(v2) = v1) | ~ (times$c(v2) = % 80.24/12.72 v0)) & ! [v0: A_m_vec_a_m_vec_fun$] : ! [v1: A_m_vec_a_m_vec_fun$] : ! % 80.24/12.72 [v2: A_m_vec$] : (v1 = v0 | ~ (uuy$(v2) = v1) | ~ (uuy$(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_a_m_vec_fun$] : ! [v1: A_m_vec_a_m_vec_fun$] : ! [v2: A_m_vec$] : % 80.24/12.72 (v1 = v0 | ~ (times$b(v2) = v1) | ~ (times$b(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_n_vec_a_m_vec_n_vec_fun$] : ! [v1: % 80.24/12.72 A_m_vec_n_vec_a_m_vec_n_vec_fun$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ % 80.24/12.72 (uux$(v2) = v1) | ~ (uux$(v2) = v0)) & ! [v0: % 80.24/12.72 A_m_vec_n_vec_a_m_vec_n_vec_fun$] : ! [v1: % 80.24/12.72 A_m_vec_n_vec_a_m_vec_n_vec_fun$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ % 80.24/12.72 (times$(v2) = v1) | ~ (times$(v2) = v0)) & ! [v0: A_n_vec_set_bool_fun$] : % 80.24/12.72 ! [v1: A_n_vec_set_bool_fun$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ % 80.24/12.72 (uxo$(v2) = v1) | ~ (uxo$(v2) = v0)) & ! [v0: A_n_vec_set_bool_fun$] : ! % 80.24/12.72 [v1: A_n_vec_set_bool_fun$] : ! [v2: A_n_vec_set$] : (v1 = v0 | ~ % 80.24/12.72 (less_eq$(v2) = v1) | ~ (less_eq$(v2) = v0)) & ! [v0: N_bool_fun$] : ! % 80.24/12.72 [v1: N_bool_fun$] : ! [v2: N_set$] : (v1 = v0 | ~ (uyd$(v2) = v1) | ~ % 80.24/12.72 (uyd$(v2) = v0)) & ! [v0: A_n_vec_bool_fun$] : ! [v1: A_n_vec_bool_fun$] : % 80.24/12.72 ! [v2: A_n_vec_set$] : (v1 = v0 | ~ (uye$(v2) = v1) | ~ (uye$(v2) = v0)) & % 80.24/12.72 ! [v0: A_n_vec_set_a_n_vec_set_fun$] : ! [v1: A_n_vec_set_a_n_vec_set_fun$] : % 80.24/12.72 ! [v2: A_n_vec$] : (v1 = v0 | ~ (insert$(v2) = v1) | ~ (insert$(v2) = v0)) % 80.24/12.72 & ! [v0: M_bool_fun$] : ! [v1: M_bool_fun$] : ! [v2: N$] : (v1 = v0 | ~ % 80.24/12.72 (uvj$(v2) = v1) | ~ (uvj$(v2) = v0)) & ! [v0: M$] : ! [v1: M$] : ! [v2: % 80.24/12.72 M_bool_fun$] : (v1 = v0 | ~ (least$(v2) = v1) | ~ (least$(v2) = v0)) & ! % 80.24/12.72 [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | ~ % 80.24/12.72 (vec_nth$b(v2) = v1) | ~ (vec_nth$b(v2) = v0)) & ! [v0: N_a_m_vec_fun$] : % 80.24/12.72 ! [v1: N_a_m_vec_fun$] : ! [v2: A_m_vec_n_vec$] : (v1 = v0 | ~ % 80.24/12.72 (vec_nth$a(v2) = v1) | ~ (vec_nth$a(v2) = v0)) & ! [v0: M_a_fun$] : ! % 80.24/12.72 [v1: M_a_fun$] : ! [v2: A_m_vec$] : (v1 = v0 | ~ (vec_nth$(v2) = v1) | ~ % 80.24/12.72 (vec_nth$(v2) = v0)) % 80.24/12.72 % 80.24/12.72 Further assumptions not needed in the proof: % 80.24/12.72 -------------------------------------------- % 80.24/12.72 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 80.24/12.72 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 80.24/12.72 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom12, axiom120, % 80.24/12.72 axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, axiom128, % 80.24/12.72 axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, axiom135, % 80.24/12.72 axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, axiom142, % 80.24/12.72 axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, % 80.24/12.72 axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, % 80.24/12.72 axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, axiom164, % 80.24/12.72 axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, % 80.24/12.72 axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom179, % 80.24/12.72 axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, % 80.24/12.72 axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 80.24/12.72 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 80.24/12.72 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 80.24/12.72 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 80.24/12.72 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 80.24/12.72 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 80.24/12.72 axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, % 80.24/12.72 axiom237, axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, % 80.24/12.72 axiom244, axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, % 80.24/12.72 axiom251, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, % 80.24/12.72 axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, axiom266, % 80.24/12.72 axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, axiom273, % 80.24/12.72 axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, axiom280, % 80.24/12.72 axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, axiom288, % 80.24/12.72 axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, axiom294, axiom295, % 80.24/12.72 axiom296, axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, axiom301, % 80.24/12.72 axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, % 80.24/12.72 axiom31, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, % 80.24/12.72 axiom317, axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, axiom323, % 80.24/12.72 axiom324, axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, axiom330, % 80.24/12.72 axiom331, axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, % 80.24/12.72 axiom339, axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, axiom345, % 80.24/12.72 axiom346, axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, axiom352, % 80.24/12.72 axiom353, axiom354, axiom355, axiom356, axiom357, axiom358, axiom359, axiom36, % 80.24/12.72 axiom360, axiom361, axiom362, axiom363, axiom364, axiom365, axiom366, axiom367, % 80.24/12.72 axiom368, axiom369, axiom37, axiom370, axiom371, axiom372, axiom373, axiom374, % 80.24/12.72 axiom375, axiom376, axiom377, axiom378, axiom379, axiom38, axiom380, axiom381, % 80.24/12.72 axiom382, axiom383, axiom384, axiom385, axiom386, axiom387, axiom388, axiom389, % 80.24/12.72 axiom39, axiom390, axiom391, axiom392, axiom393, axiom394, axiom395, axiom396, % 80.24/12.72 axiom397, axiom398, axiom399, axiom4, axiom40, axiom400, axiom401, axiom402, % 80.24/12.72 axiom403, axiom404, axiom405, axiom406, axiom407, axiom408, axiom409, axiom41, % 80.24/12.72 axiom410, axiom411, axiom412, axiom413, axiom414, axiom415, axiom416, axiom417, % 80.24/12.72 axiom418, axiom419, axiom42, axiom420, axiom421, axiom422, axiom423, axiom424, % 80.24/12.72 axiom425, axiom426, axiom427, axiom428, axiom429, axiom43, axiom430, axiom431, % 80.24/12.72 axiom432, axiom433, axiom434, axiom435, axiom436, axiom437, axiom438, axiom439, % 80.24/12.72 axiom44, axiom440, axiom441, axiom442, axiom443, axiom444, axiom445, axiom446, % 80.24/12.72 axiom447, axiom448, axiom449, axiom45, axiom450, axiom451, axiom452, axiom453, % 80.24/12.72 axiom454, axiom455, axiom456, axiom457, axiom458, axiom459, axiom46, axiom460, % 80.24/12.72 axiom461, axiom462, axiom463, axiom464, axiom465, axiom466, axiom467, axiom468, % 80.24/12.72 axiom469, axiom47, axiom470, axiom471, axiom472, axiom473, axiom474, axiom475, % 80.24/12.72 axiom476, axiom477, axiom478, axiom479, axiom48, axiom480, axiom481, axiom482, % 80.24/12.72 axiom483, axiom484, axiom485, axiom486, axiom487, axiom488, axiom489, axiom49, % 80.24/12.72 axiom490, axiom491, axiom492, axiom493, axiom494, axiom495, axiom496, axiom497, % 80.24/12.72 axiom498, axiom499, axiom5, axiom50, axiom500, axiom501, axiom502, axiom503, % 80.24/12.72 axiom504, axiom505, axiom506, axiom507, axiom508, axiom509, axiom51, axiom510, % 80.24/12.72 axiom511, axiom512, axiom513, axiom514, axiom515, axiom516, axiom517, axiom518, % 80.24/12.72 axiom519, axiom52, axiom520, axiom521, axiom522, axiom523, axiom524, axiom525, % 80.24/12.72 axiom526, axiom527, axiom528, axiom529, axiom53, axiom530, axiom531, axiom532, % 80.24/12.72 axiom533, axiom534, axiom535, axiom536, axiom537, axiom538, axiom539, axiom54, % 80.24/12.72 axiom540, axiom541, axiom542, axiom543, axiom544, axiom545, axiom546, axiom547, % 80.24/12.72 axiom548, axiom549, axiom55, axiom550, axiom551, axiom552, axiom553, axiom554, % 80.24/12.72 axiom555, axiom556, axiom557, axiom558, axiom559, axiom56, axiom560, axiom561, % 80.24/12.72 axiom562, axiom563, axiom564, axiom565, axiom566, axiom567, axiom568, axiom569, % 80.24/12.72 axiom57, axiom570, axiom571, axiom572, axiom573, axiom574, axiom575, axiom576, % 80.24/12.72 axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, axiom582, axiom583, % 80.24/12.72 axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, axiom59, axiom590, % 80.24/12.72 axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, axiom597, axiom598, % 80.24/12.72 axiom599, axiom6, axiom60, axiom600, axiom601, axiom602, axiom603, axiom604, % 80.24/12.72 axiom605, axiom606, axiom607, axiom608, axiom609, axiom61, axiom610, axiom611, % 80.24/12.72 axiom612, axiom613, axiom614, axiom615, axiom616, axiom617, axiom618, axiom619, % 80.24/12.72 axiom62, axiom620, axiom621, axiom622, axiom623, axiom624, axiom625, axiom626, % 80.24/12.72 axiom627, axiom628, axiom629, axiom63, axiom630, axiom631, axiom632, axiom633, % 80.24/12.72 axiom634, axiom635, axiom636, axiom637, axiom638, axiom639, axiom64, axiom640, % 80.24/12.72 axiom641, axiom642, axiom643, axiom644, axiom645, axiom646, axiom647, axiom648, % 80.24/12.72 axiom649, axiom65, axiom650, axiom651, axiom652, axiom653, axiom654, axiom655, % 80.24/12.72 axiom656, axiom657, axiom658, axiom659, axiom66, axiom660, axiom661, axiom662, % 80.24/12.72 axiom663, axiom664, axiom665, axiom666, axiom667, axiom668, axiom669, axiom67, % 80.24/12.72 axiom670, axiom671, axiom672, axiom673, axiom674, axiom675, axiom676, axiom677, % 80.24/12.72 axiom678, axiom679, axiom68, axiom680, axiom681, axiom682, axiom683, axiom684, % 80.24/12.72 axiom685, axiom686, axiom687, axiom688, axiom689, axiom69, axiom690, axiom691, % 80.24/12.72 axiom692, axiom693, axiom694, axiom695, axiom696, axiom697, axiom698, axiom699, % 80.24/12.72 axiom7, axiom70, axiom700, axiom701, axiom702, axiom703, axiom704, axiom705, % 80.24/12.72 axiom706, axiom707, axiom708, axiom709, axiom71, axiom710, axiom711, axiom712, % 80.24/12.72 axiom713, axiom714, axiom715, axiom716, axiom717, axiom718, axiom719, axiom72, % 80.24/12.72 axiom720, axiom721, axiom722, axiom723, axiom724, axiom725, axiom726, axiom727, % 80.24/12.72 axiom728, axiom729, axiom73, axiom730, axiom731, axiom732, axiom733, axiom734, % 80.24/12.72 axiom735, axiom736, axiom737, axiom738, axiom739, axiom74, axiom740, axiom741, % 80.24/12.72 axiom742, axiom743, axiom744, axiom745, axiom746, axiom747, axiom748, axiom749, % 80.24/12.72 axiom75, axiom750, axiom751, axiom752, axiom76, axiom77, axiom78, axiom79, % 80.24/12.72 axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, axiom87, % 80.24/12.72 axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, % 80.24/12.72 axiom96, axiom97, axiom98, axiom99, formula_754, formula_755 % 80.24/12.72 % 80.24/12.72 Those formulas are unsatisfiable: % 80.24/12.72 --------------------------------- % 80.24/12.72 % 80.24/12.72 Begin of proof % 80.24/12.72 | % 80.24/12.72 | ALPHA: (axiom119) implies: % 80.24/12.73 | (1) ? [v0: N_a_fun$] : (vec_nth$b(xa$) = v0 & fun_app$d(v0, i$) = zero$ & % 80.24/12.73 | N_a_fun$(v0)) % 80.24/12.73 | % 80.24/12.73 | ALPHA: (axiom252) implies: % 80.24/12.73 | (2) ! [v0: A$] : ! [v1: A$] : ! [v2: A_a_fun$] : ! [v3: A$] : (v3 = v1 % 80.24/12.73 | | ~ (fun_app$n(times$e, v0) = v2) | ~ (fun_app$m(v2, v1) = v3) | ~ % 80.24/12.73 | A$(v1) | ~ A$(v0) | ( ~ (v1 = zero$) & ~ (v0 = one$))) % 80.24/12.73 | % 80.24/12.73 | ALPHA: (conjecture118) implies: % 80.24/12.73 | (3) ? [v0: N_a_fun$] : ? [v1: N$] : ? [v2: A$] : ? [v3: A_a_fun$] : ? % 80.24/12.73 | [v4: N_a_fun$] : ? [v5: A$] : ? [v6: A$] : ( ~ (v6 = zero$) & % 80.24/12.73 | the$(uu$) = v1 & fun_app$n(times$e, v2) = v3 & fun_app$m(v3, v5) = v6 % 80.24/12.73 | & vec_nth$b(x$) = v0 & vec_nth$b(xa$) = v4 & fun_app$d(v4, i$) = v5 & % 80.24/12.73 | fun_app$d(v0, v1) = v2 & A_a_fun$(v3) & A$(v6) & A$(v5) & A$(v2) & % 80.24/12.73 | N_a_fun$(v4) & N_a_fun$(v0) & N$(v1)) % 80.24/12.73 | % 80.24/12.73 | ALPHA: (function-axioms) implies: % 80.24/12.73 | (4) ! [v0: N_a_fun$] : ! [v1: N_a_fun$] : ! [v2: A_n_vec$] : (v1 = v0 | % 80.24/12.73 | ~ (vec_nth$b(v2) = v1) | ~ (vec_nth$b(v2) = v0)) % 80.24/12.73 | (5) ! [v0: A$] : ! [v1: A$] : ! [v2: N$] : ! [v3: N_a_fun$] : (v1 = v0 % 80.24/12.73 | | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) % 80.24/12.73 | % 80.24/12.73 | DELTA: instantiating (1) with fresh symbol all_746_0 gives: % 80.24/12.73 | (6) vec_nth$b(xa$) = all_746_0 & fun_app$d(all_746_0, i$) = zero$ & % 80.24/12.73 | N_a_fun$(all_746_0) % 80.24/12.73 | % 80.24/12.73 | ALPHA: (6) implies: % 80.24/12.73 | (7) fun_app$d(all_746_0, i$) = zero$ % 80.24/12.73 | (8) vec_nth$b(xa$) = all_746_0 % 80.24/12.73 | % 80.24/12.73 | DELTA: instantiating (3) with fresh symbols all_963_0, all_963_1, all_963_2, % 80.24/12.73 | all_963_3, all_963_4, all_963_5, all_963_6 gives: % 80.24/12.73 | (9) ~ (all_963_0 = zero$) & the$(uu$) = all_963_5 & fun_app$n(times$e, % 80.24/12.73 | all_963_4) = all_963_3 & fun_app$m(all_963_3, all_963_1) = all_963_0 % 80.24/12.73 | & vec_nth$b(x$) = all_963_6 & vec_nth$b(xa$) = all_963_2 & % 80.24/12.73 | fun_app$d(all_963_2, i$) = all_963_1 & fun_app$d(all_963_6, all_963_5) % 80.24/12.73 | = all_963_4 & A_a_fun$(all_963_3) & A$(all_963_0) & A$(all_963_1) & % 80.24/12.73 | A$(all_963_4) & N_a_fun$(all_963_2) & N_a_fun$(all_963_6) & % 80.24/12.73 | N$(all_963_5) % 80.24/12.73 | % 80.24/12.73 | ALPHA: (9) implies: % 80.24/12.73 | (10) ~ (all_963_0 = zero$) % 80.24/12.73 | (11) A$(all_963_4) % 80.24/12.73 | (12) A$(all_963_1) % 80.24/12.73 | (13) fun_app$d(all_963_2, i$) = all_963_1 % 80.24/12.73 | (14) vec_nth$b(xa$) = all_963_2 % 80.24/12.73 | (15) fun_app$m(all_963_3, all_963_1) = all_963_0 % 80.24/12.73 | (16) fun_app$n(times$e, all_963_4) = all_963_3 % 80.24/12.73 | % 80.24/12.73 | GROUND_INST: instantiating (4) with all_746_0, all_963_2, xa$, simplifying % 80.24/12.73 | with (8), (14) gives: % 80.24/12.74 | (17) all_963_2 = all_746_0 % 80.24/12.74 | % 80.24/12.74 | REDUCE: (13), (17) imply: % 80.24/12.74 | (18) fun_app$d(all_746_0, i$) = all_963_1 % 80.24/12.74 | % 80.24/12.74 | GROUND_INST: instantiating (5) with zero$, all_963_1, i$, all_746_0, % 80.24/12.74 | simplifying with (7), (18) gives: % 80.24/12.74 | (19) all_963_1 = zero$ % 80.24/12.74 | % 80.24/12.74 | REDUCE: (15), (19) imply: % 80.24/12.74 | (20) fun_app$m(all_963_3, zero$) = all_963_0 % 80.24/12.74 | % 80.24/12.74 | REDUCE: (12), (19) imply: % 80.24/12.74 | (21) A$(zero$) % 80.24/12.74 | % 80.24/12.74 | GROUND_INST: instantiating (2) with all_963_4, zero$, all_963_3, all_963_0, % 80.24/12.74 | simplifying with (11), (16), (20), (21) gives: % 80.24/12.74 | (22) all_963_0 = zero$ % 80.24/12.74 | % 80.24/12.74 | REDUCE: (10), (22) imply: % 80.24/12.74 | (23) $false % 80.24/12.74 | % 80.24/12.74 | CLOSE: (23) is inconsistent. % 80.24/12.74 | % 80.24/12.74 End of proof % 80.24/12.74 % SZS output end Proof for theBenchmark % 80.24/12.74 % 80.24/12.74 12094ms %------------------------------------------------------------------------------