%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP320_1 : TPTP v9.2.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.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 : Wed Jun 3 08:26:20 AM UTC 2026 % Result : Theorem 2.43s 2.61s % Output : Proof 2.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP320_1 : TPTP v9.2.1. Released v8.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n013.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 04:59:30 EDT 2026 % 0.17/0.34 % CPUTime : % 0.42/0.66 %----Proving TF0_ARI % 2.43/2.61 --- Run --finite-model-find --decision=internal at 45... % 2.43/2.61 % SZS status Theorem % 2.43/2.61 % SZS output start Proof % 2.43/2.61 ( % 2.43/2.61 (declare-sort |tptp.'Nat_nat_bool_fun_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat_nat_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat_rows_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat_real_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat_int_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'A_a_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_rows_vec_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Cols_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Cols_cols_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_cols_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Int_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Int_cols_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_rows_bool_fun_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Cols$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat_bool_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_cols_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_bool_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Cols_a_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Int_bool_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'A_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'A_cols_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_bool_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_rows_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_set$'| 0) % 2.43/2.61 (declare-sort |tptp.'Int_rows_vec$'| 0) % 2.43/2.61 (declare-sort tptp.tlbool 0) % 2.43/2.61 (declare-sort |tptp.'Cols_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Nat$'| 0) % 2.43/2.61 (declare-sort |tptp.'A$'| 0) % 2.43/2.61 (declare-sort |tptp.'A_cols_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_a_cols_vec_fun$'| 0) % 2.43/2.61 (declare-sort |tptp.'Real_rows_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Int_rows_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Rows_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'A_rows_vec_rows_vec$'| 0) % 2.43/2.61 (declare-sort |tptp.'Cols_rows_vec_rows_vec$'| 0) % 2.43/2.61 (declare-const tptp.tlfalse tptp.tlbool) % 2.43/2.61 (declare-const |tptp.'uminus$a'| (-> |tptp.'Cols$'| |tptp.'Cols$'|)) % 2.43/2.61 (declare-const |tptp.'uminus$'| (-> |tptp.'Rows$'| |tptp.'Rows$'|)) % 2.43/2.61 (declare-const |tptp.'less_eq$'| |tptp.'Nat_nat_bool_fun_fun$'|) % 2.43/2.61 (declare-const |tptp.'from_nat$a'| (-> |tptp.'Nat$'| |tptp.'Cols$'|)) % 2.43/2.61 (declare-const |tptp.'powr$'| (-> Real Real Real)) % 2.43/2.61 (declare-const |tptp.'power$b'| (-> Real |tptp.'Nat_real_fun$'|)) % 2.43/2.61 (declare-const |tptp.'power$a'| (-> Int |tptp.'Nat_int_fun$'|)) % 2.43/2.61 (declare-const |tptp.'less_eq$a'| |tptp.'Rows_rows_bool_fun_fun$'|) % 2.43/2.61 (declare-const |tptp.'fun_app$k'| (-> |tptp.'Nat_nat_bool_fun_fun$'| |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$l'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 2.43/2.61 (declare-const |tptp.'of_nat$b'| |tptp.'Nat_nat_fun$'|) % 2.43/2.61 (declare-const |tptp.'from_nat$'| |tptp.'Nat_rows_fun$'|) % 2.43/2.61 (declare-const |tptp.'fun_app$i'| (-> |tptp.'Nat_real_fun$'| |tptp.'Nat$'| Real)) % 2.43/2.61 (declare-const |tptp.'of_nat$a'| |tptp.'Nat_real_fun$'|) % 2.43/2.61 (declare-const |tptp.'artanh$'| (-> Real Real)) % 2.43/2.61 (declare-const |tptp.'arsinh$'| (-> Real Real)) % 2.43/2.61 (declare-const |tptp.'axis$'| (-> |tptp.'Cols$'| |tptp.'A$'| |tptp.'A_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec$'| (-> |tptp.'A$'| |tptp.'A_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'to_nat$'| (-> |tptp.'Cols$'| |tptp.'Nat$'|)) % 2.43/2.61 (declare-const |tptp.'one$d'| |tptp.'Cols$'|) % 2.43/2.61 (declare-const |tptp.'one$c'| |tptp.'Rows$'|) % 2.43/2.61 (declare-const |tptp.'dbl_inc$'| (-> Real Real)) % 2.43/2.61 (declare-const |tptp.'one$e'| |tptp.'Nat$'|) % 2.43/2.61 (declare-const |tptp.'fun_app$h'| (-> |tptp.'Nat_int_fun$'| |tptp.'Nat$'| Int)) % 2.43/2.61 (declare-const |tptp.'map_matrix$'| (-> |tptp.'A_a_fun$'| |tptp.'A_cols_vec_rows_vec$'| |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$g'| (-> |tptp.'A_a_fun$'| |tptp.'A$'| |tptp.'A$'|)) % 2.43/2.61 (declare-const |tptp.'dbl_inc$c'| (-> |tptp.'Cols$'| |tptp.'Cols$'|)) % 2.43/2.61 (declare-const |tptp.'collect$'| (-> |tptp.'Real_bool_fun$'| |tptp.'Real_set$'|)) % 2.43/2.61 (declare-const tptp.tltrue tptp.tlbool) % 2.43/2.61 (declare-const |tptp.'one$b'| |tptp.'A_cols_vec_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'zero$j'| |tptp.'A_cols_vec_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'zero$i'| |tptp.'A_cols_vec$'|) % 2.43/2.61 (declare-const |tptp.'zero$k'| |tptp.'Nat$'|) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$j'| (-> |tptp.'Real_rows_vec_cols_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$t'| (-> |tptp.'Real_rows_vec_cols_vec$'| |tptp.'Cols$'| |tptp.'Real_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$j'| (-> |tptp.'Rows$'| |tptp.'Real_rows_vec_cols_vec$'| |tptp.'Real_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'zero$h'| |tptp.'Real_cols_vec$'|) % 2.43/2.61 (declare-const |tptp.'dbl_inc$b'| (-> |tptp.'Rows$'| |tptp.'Rows$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$i'| (-> |tptp.'Cols_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$r'| (-> |tptp.'Cols_cols_vec$'| |tptp.'Cols$'| |tptp.'Cols$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$s'| (-> |tptp.'Cols_cols_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Cols_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$h'| (-> |tptp.'Rows_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$p'| (-> |tptp.'Rows_cols_vec$'| |tptp.'Cols$'| |tptp.'Rows$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$j'| (-> |tptp.'Nat_rows_fun$'| |tptp.'Nat$'| |tptp.'Rows$'|)) % 2.43/2.61 (declare-const |tptp.'column$h'| (-> |tptp.'Cols$'| |tptp.'Rows_cols_vec_rows_vec$'| |tptp.'Rows_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$a'| (-> |tptp.'Rows$'| |tptp.'Real_rows_vec_rows_vec$'| |tptp.'Real_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'zero$d'| |tptp.'Real_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'fun_app$e'| (-> |tptp.'Cols_a_fun$'| |tptp.'Cols$'| |tptp.'A$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$d'| (-> |tptp.'Cols_rows_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'uu$'| (-> |tptp.'Real_set$'| |tptp.'Real_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$f'| (-> |tptp.'Rows_a_cols_vec_fun$'| |tptp.'Rows$'| |tptp.'A_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'nat$'| (-> Int |tptp.'Nat$'|)) % 2.43/2.61 (declare-const |tptp.'zero$c'| |tptp.'A$'|) % 2.43/2.61 (declare-const |tptp.'less_eq$b'| (-> |tptp.'Cols$'| |tptp.'Cols$'| Bool)) % 2.43/2.61 (declare-const |tptp.'column$'| (-> |tptp.'Cols$'| |tptp.'A_cols_vec_rows_vec$'| |tptp.'A_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'zero$a'| |tptp.'Cols$'|) % 2.43/2.61 (declare-const |tptp.'to_nat$a'| (-> |tptp.'Rows$'| |tptp.'Nat$'|)) % 2.43/2.61 (declare-const |tptp.'column$c'| (-> |tptp.'Rows$'| |tptp.'Rows_rows_vec_rows_vec$'| |tptp.'Rows_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'axis$a'| (-> |tptp.'Rows$'| |tptp.'A_cols_vec$'| |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$f'| (-> |tptp.'Cols$'| |tptp.'Real_cols_vec_rows_vec$'| |tptp.'Real_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'zero$b'| |tptp.'A_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'vec_nth$l'| (-> |tptp.'Real_cols_vec$'| |tptp.'Cols$'| Real)) % 2.43/2.61 (declare-const |tptp.'is_zero_row$'| (-> |tptp.'Rows$'| |tptp.'A_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'column$b'| (-> |tptp.'Rows$'| |tptp.'Int_rows_vec_rows_vec$'| |tptp.'Int_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$d'| (-> |tptp.'Int_rows_vec$'| |tptp.'Rows$'| Int)) % 2.43/2.61 (declare-const |tptp.'fun_app$b'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| Bool)) % 2.43/2.61 (declare-const |tptp.'dbl_inc$a'| (-> Int Int)) % 2.43/2.61 (declare-const |tptp.'vec_nth$h'| (-> |tptp.'Cols_rows_vec$'| |tptp.'Rows$'| |tptp.'Cols$'|)) % 2.43/2.61 (declare-const |tptp.'power$'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 2.43/2.61 (declare-const |tptp.'column$g'| (-> |tptp.'Cols$'| |tptp.'Int_cols_vec_rows_vec$'| |tptp.'Int_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'ncols$'| (-> |tptp.'A_cols_vec_rows_vec$'| |tptp.'Nat$'|)) % 2.43/2.61 (declare-const |tptp.'less$a'| |tptp.'Nat_nat_bool_fun_fun$'|) % 2.43/2.61 (declare-const |tptp.'uua$'| (-> Int |tptp.'Int_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'uub$'| (-> Real |tptp.'Real_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'one$'| |tptp.'A_cols_vec$'|) % 2.43/2.61 (declare-const |tptp.'fun_app$'| (-> |tptp.'Real_bool_fun$'| Real Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$q'| (-> |tptp.'Rows_cols_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Rows_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$a'| (-> |tptp.'Int_bool_fun$'| Int Bool)) % 2.43/2.61 (declare-const |tptp.'one$a'| |tptp.'A$'|) % 2.43/2.61 (declare-const |tptp.'member$'| (-> Real |tptp.'Real_set$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec$a'| (-> |tptp.'A_cols_vec$'| |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$c'| (-> |tptp.'Rows_bool_fun$'| |tptp.'Rows$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$'| (-> |tptp.'A_cols_vec$'| |tptp.'Cols_a_fun$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$'| (-> |tptp.'A_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'a$'| |tptp.'A_cols_vec_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$b'| (-> |tptp.'Int_rows_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'is_zero_row_upt_k$'| (-> |tptp.'Rows$'| |tptp.'Nat$'| |tptp.'A_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'zero$'| |tptp.'Rows$'|) % 2.43/2.61 (declare-const |tptp.'vec_nth$a'| (-> |tptp.'A_cols_vec_rows_vec$'| |tptp.'Rows_a_cols_vec_fun$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$c'| (-> |tptp.'Real_rows_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Real_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'i$'| |tptp.'Rows$'|) % 2.43/2.61 (declare-const |tptp.'vec_nth$b'| (-> |tptp.'Real_rows_vec$'| |tptp.'Rows$'| Real)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$a'| (-> |tptp.'Real_rows_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'ln$'| (-> Real Real)) % 2.43/2.61 (declare-const |tptp.'zero$e'| |tptp.'Int_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'of_nat$'| |tptp.'Nat_int_fun$'|) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$c'| (-> |tptp.'Rows_rows_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'less$'| |tptp.'Rows_rows_bool_fun_fun$'|) % 2.43/2.61 (declare-const |tptp.'vec_nth$e'| (-> |tptp.'Int_rows_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Int_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'fun_app$d'| (-> |tptp.'Rows_rows_bool_fun_fun$'| |tptp.'Rows$'| |tptp.'Rows_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'zero$f'| |tptp.'Rows_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'vec_nth$g'| (-> |tptp.'Rows_rows_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Rows_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$g'| (-> |tptp.'Int_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'arcosh$'| (-> Real Real)) % 2.43/2.61 (declare-const |tptp.'zero$g'| |tptp.'Cols_rows_vec$'|) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form_upt_k$'| (-> |tptp.'A_cols_vec_rows_vec$'| |tptp.'Nat_bool_fun$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$k'| (-> |tptp.'A_rows_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'A_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$d'| (-> |tptp.'Rows$'| |tptp.'Cols_rows_vec_rows_vec$'| |tptp.'Cols_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$e'| (-> |tptp.'Rows$'| |tptp.'A_rows_vec_rows_vec$'| |tptp.'A_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$j'| (-> |tptp.'A_rows_vec$'| |tptp.'Rows$'| |tptp.'A$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$f'| (-> |tptp.'Real_cols_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$f'| (-> |tptp.'Rows_rows_vec$'| |tptp.'Rows$'| |tptp.'Rows$'|)) % 2.43/2.61 (declare-const |tptp.'reduced_row_echelon_form$e'| (-> |tptp.'A_rows_vec_rows_vec$'| Bool)) % 2.43/2.61 (declare-const |tptp.'vec_nth$m'| (-> |tptp.'Real_cols_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Real_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'column$i'| (-> |tptp.'Cols$'| |tptp.'Cols_cols_vec_rows_vec$'| |tptp.'Cols_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$o'| (-> |tptp.'Int_cols_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Int_cols_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$i'| (-> |tptp.'Cols_rows_vec_rows_vec$'| |tptp.'Rows$'| |tptp.'Cols_rows_vec$'|)) % 2.43/2.61 (declare-const |tptp.'vec_nth$n'| (-> |tptp.'Int_cols_vec$'| |tptp.'Cols$'| Int)) % 2.43/2.61 (define @t1 () (@var "A__questionmark_v1" Real)) % 2.43/2.61 (define @t2 () (@var "A__questionmark_v0" Real)) % 2.43/2.61 (define @t3 () (< @t2 @t1)) % 2.43/2.61 (define @t4 () (@list @t2 @t1)) % 2.43/2.61 (define @t5 () (@var "A__questionmark_v1" Int)) % 2.43/2.61 (define @t6 () (@var "A__questionmark_v0" Int)) % 2.43/2.61 (define @t7 () (< @t6 @t5)) % 2.43/2.61 (define @t8 () (@list @t6 @t5)) % 2.43/2.61 (define @t9 () (@var "A__questionmark_v0" |tptp.'Real_set$'|)) % 2.43/2.61 (define @t10 () (|tptp.'member$'| @t1 @t9)) % 2.43/2.61 (define @t11 () (|tptp.'uu$'| @t9)) % 2.43/2.61 (define @t12 () (|tptp.'reduced_row_echelon_form$'| |tptp.'a$'|)) % 2.43/2.61 (define @t13 () (not @t12)) % 2.43/2.61 (define @t14 () (|tptp.'nat$'| 1)) % 2.43/2.61 (define @t15 () (|tptp.'is_zero_row_upt_k$'| |tptp.'i$'| @t14 |tptp.'a$'|)) % 2.43/2.61 (define @t16 () (|tptp.'is_zero_row_upt_k$'| |tptp.'zero$'| @t14 |tptp.'a$'|)) % 2.43/2.61 (define @t17 () (@var "A__questionmark_v1" |tptp.'Nat$'|)) % 2.43/2.61 (define @t18 () (@var "A__questionmark_v0" |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t19 () (|tptp.'reduced_row_echelon_form_upt_k$'| @t18)) % 2.43/2.61 (define @t20 () (|tptp.'fun_app$b'| @t19 @t17)) % 2.43/2.61 (define @t21 () (|tptp.'reduced_row_echelon_form$'| @t18)) % 2.43/2.61 (define @t22 () (@list @t18 @t17)) % 2.43/2.61 (define @t23 () (forall @t22 (=> @t21 @t20))) % 2.43/2.61 (define @t24 () (|tptp.'fun_app$d'| |tptp.'less$'| |tptp.'zero$'|)) % 2.43/2.61 (define @t25 () (|tptp.'fun_app$c'| @t24 |tptp.'i$'|)) % 2.43/2.61 (define @t26 () (@list @t18)) % 2.43/2.61 (define @t27 () (@var "A__questionmark_v2" |tptp.'Rows$'|)) % 2.43/2.61 (define @t28 () (|tptp.'is_zero_row$'| @t27 @t18)) % 2.43/2.61 (define @t29 () (@var "A__questionmark_v1" |tptp.'Rows$'|)) % 2.43/2.61 (define @t30 () (|tptp.'fun_app$d'| |tptp.'less$'| @t29)) % 2.43/2.61 (define @t31 () (|tptp.'fun_app$c'| @t30 @t27)) % 2.43/2.61 (define @t32 () (@list @t27)) % 2.43/2.61 (define @t33 () (|tptp.'is_zero_row$'| @t29 @t18)) % 2.43/2.61 (define @t34 () (@list @t29)) % 2.43/2.61 (define @t35 () (@list @t18 @t29)) % 2.43/2.61 (define @t36 () (|tptp.'vec_nth$a'| |tptp.'a$'|)) % 2.43/2.61 (define @t37 () (@var "A__questionmark_v0" |tptp.'Rows$'|)) % 2.43/2.61 (define @t38 () (@list @t37)) % 2.43/2.61 (define @t39 () (@var "A__questionmark_v1" |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t40 () (|tptp.'is_zero_row_upt_k$'| @t37 (|tptp.'ncols$'| @t39) @t39)) % 2.43/2.61 (define @t41 () (|tptp.'is_zero_row$'| @t37 @t39)) % 2.43/2.61 (define @t42 () (@list @t37 @t39)) % 2.43/2.61 (define @t43 () (@var "A__questionmark_v2" |tptp.'Cols$'|)) % 2.43/2.61 (define @t44 () (|tptp.'vec_nth$a'| @t39)) % 2.43/2.61 (define @t45 () (@list @t43)) % 2.43/2.61 (define @t46 () (forall @t45 (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| @t44 @t37)) @t43) |tptp.'zero$c'|))) % 2.43/2.61 (define @t47 () (@var "A__questionmark_v3" |tptp.'Rows$'|)) % 2.43/2.61 (define @t48 () (|tptp.'is_zero_row_upt_k$'| @t47 @t17 @t18)) % 2.43/2.61 (define @t49 () (not @t48)) % 2.43/2.61 (define @t50 () (|tptp.'fun_app$d'| |tptp.'less$'| @t27)) % 2.43/2.61 (define @t51 () (|tptp.'fun_app$c'| @t50 @t47)) % 2.43/2.61 (define @t52 () (and @t51 @t49)) % 2.43/2.61 (define @t53 () (@list @t47)) % 2.43/2.61 (define @t54 () (exists @t53 @t52)) % 2.43/2.61 (define @t55 () (not @t54)) % 2.43/2.61 (define @t56 () (|tptp.'is_zero_row_upt_k$'| @t27 @t17 @t18)) % 2.43/2.61 (define @t57 () (=> @t56 @t55)) % 2.43/2.61 (define @t58 () (forall @t32 @t57)) % 2.43/2.61 (define @t59 () (=> @t20 @t58)) % 2.43/2.61 (define @t60 () (forall @t22 @t59)) % 2.43/2.61 (define @t61 () (@var "A__questionmark_v2" |tptp.'Nat$'|)) % 2.43/2.61 (define @t62 () (@var "A__questionmark_v0" |tptp.'Nat$'|)) % 2.43/2.61 (define @t63 () (@var "A__questionmark_v0" |tptp.'Real_rows_vec_rows_vec$'|)) % 2.43/2.61 (define @t64 () (@var "A__questionmark_v0" |tptp.'Int_rows_vec_rows_vec$'|)) % 2.43/2.61 (define @t65 () (@var "A__questionmark_v0" |tptp.'Rows_rows_vec_rows_vec$'|)) % 2.43/2.61 (define @t66 () (@var "A__questionmark_v0" |tptp.'Cols_rows_vec_rows_vec$'|)) % 2.43/2.61 (define @t67 () (@var "A__questionmark_v0" |tptp.'A_rows_vec_rows_vec$'|)) % 2.43/2.61 (define @t68 () (@var "A__questionmark_v0" |tptp.'Real_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t69 () (@var "A__questionmark_v0" |tptp.'Int_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t70 () (@var "A__questionmark_v0" |tptp.'Rows_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t71 () (@var "A__questionmark_v0" |tptp.'Cols_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t72 () (@var "A__questionmark_v0" |tptp.'Real_rows_vec_cols_vec$'|)) % 2.43/2.61 (define @t73 () (@var "A__questionmark_v0" |tptp.'Cols$'|)) % 2.43/2.61 (define @t74 () (@list @t73)) % 2.43/2.61 (define @t75 () (|tptp.'nat$'| 0)) % 2.43/2.61 (define @t76 () (= @t2 0/1)) % 2.43/2.61 (define @t77 () (= 0/1 @t2)) % 2.43/2.61 (define @t78 () (@list @t2)) % 2.43/2.61 (define @t79 () (= @t6 0)) % 2.43/2.61 (define @t80 () (= 0 @t6)) % 2.43/2.61 (define @t81 () (@list @t6)) % 2.43/2.61 (define @t82 () (= @t37 |tptp.'zero$'|)) % 2.43/2.61 (define @t83 () (= |tptp.'zero$'| @t37)) % 2.43/2.61 (define @t84 () (= @t73 |tptp.'zero$a'|)) % 2.43/2.61 (define @t85 () (= |tptp.'zero$a'| @t73)) % 2.43/2.61 (define @t86 () (@var "A__questionmark_v0" |tptp.'A$'|)) % 2.43/2.61 (define @t87 () (< @t5 @t6)) % 2.43/2.61 (define @t88 () (= @t6 @t5)) % 2.43/2.61 (define @t89 () (< @t1 @t2)) % 2.43/2.61 (define @t90 () (= @t2 @t1)) % 2.43/2.61 (define @t91 () (= @t2 1/1)) % 2.43/2.61 (define @t92 () (@var "A__questionmark_v3" |tptp.'Cols$'|)) % 2.43/2.61 (define @t93 () (@var "A__questionmark_v2" |tptp.'A_cols_vec$'|)) % 2.43/2.61 (define @t94 () (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| @t93) @t92)) % 2.43/2.61 (define @t95 () (@var "A__questionmark_v0" tptp.tlbool)) % 2.43/2.61 (define @t96 () (= @t95 tptp.tltrue)) % 2.43/2.61 (define @t97 () (not @t96)) % 2.43/2.61 (define @t98 () (@var "A__questionmark_v1" |tptp.'A_cols_vec$'|)) % 2.43/2.61 (define @t99 () (|tptp.'vec_nth$'| @t98)) % 2.43/2.61 (define @t100 () (|tptp.'fun_app$e'| @t99 @t92)) % 2.43/2.61 (define @t101 () (@var "A__questionmark_v2" |tptp.'A_cols_vec_rows_vec$'|)) % 2.43/2.61 (define @t102 () (|tptp.'vec_nth$a'| @t101)) % 2.43/2.61 (define @t103 () (|tptp.'fun_app$f'| @t102 @t47)) % 2.43/2.61 (define @t104 () (|tptp.'fun_app$f'| @t44 @t47)) % 2.43/2.61 (define @t105 () (@var "A__questionmark_v0" |tptp.'A_cols_vec$'|)) % 2.43/2.61 (define @t106 () (|tptp.'vec_nth$'| @t105)) % 2.43/2.61 (define @t107 () (= @t105 @t98)) % 2.43/2.61 (define @t108 () (@list @t105 @t98)) % 2.43/2.61 (define @t109 () (|tptp.'fun_app$f'| @t44 @t27)) % 2.43/2.61 (define @t110 () (|tptp.'vec_nth$a'| @t18)) % 2.43/2.61 (define @t111 () (= @t18 @t39)) % 2.43/2.61 (define @t112 () (@list @t18 @t39)) % 2.43/2.61 (define @t113 () (@var "A__questionmark_v1" |tptp.'Real_bool_fun$'|)) % 2.43/2.61 (define @t114 () (@list @t9)) % 2.43/2.61 (define @t115 () (< 0 0)) % 2.43/2.61 (define @t116 () (@var "A__questionmark_v0" |tptp.'A_a_fun$'|)) % 2.43/2.61 (define @t117 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t62)) % 2.43/2.61 (define @t118 () (= @t117 0)) % 2.43/2.61 (define @t119 () (@list @t62)) % 2.43/2.61 (define @t120 () (@var "A__questionmark_v2" Real)) % 2.43/2.61 (define @t121 () (< 0/1 @t120)) % 2.43/2.61 (define @t122 () (@list @t120)) % 2.43/2.61 (define @t123 () (< 0/1 @t1)) % 2.43/2.61 (define @t124 () (< 0/1 @t2)) % 2.43/2.61 (define @t125 () (and @t124 @t123)) % 2.43/2.61 (define @t126 () (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| @t102 @t37))) % 2.43/2.61 (define @t127 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t17)) % 2.43/2.61 (define @t128 () (|tptp.'is_zero_row_upt_k$'| @t37 @t17 @t101)) % 2.43/2.61 (define @t129 () (@list @t37 @t17 @t101)) % 2.43/2.61 (define @t130 () (< 0 @t117)) % 2.43/2.61 (define @t131 () (not @t118)) % 2.43/2.61 (define @t132 () (< @t117 0)) % 2.43/2.61 (define @t133 () (@var "A__questionmark_v1" |tptp.'Cols$'|)) % 2.43/2.61 (define @t134 () (@var "A__questionmark_v1" |tptp.'A$'|)) % 2.43/2.61 (define @t135 () (=> @t118 false)) % 2.43/2.61 (define @t136 () (= @t127 0)) % 2.43/2.61 (define @t137 () (< @t117 @t127)) % 2.43/2.61 (define @t138 () (@list @t62 @t17)) % 2.43/2.61 (define @t139 () (@var "A__questionmark_v0" |tptp.'Nat_bool_fun$'|)) % 2.43/2.61 (define @t140 () (|tptp.'fun_app$b'| @t139 @t17)) % 2.43/2.61 (define @t141 () (@var "A__questionmark_v3" |tptp.'Nat$'|)) % 2.43/2.61 (define @t142 () (|tptp.'fun_app$b'| @t139 @t141)) % 2.43/2.61 (define @t143 () (not @t142)) % 2.43/2.61 (define @t144 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t61)) % 2.43/2.61 (define @t145 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t141)) % 2.43/2.61 (define @t146 () (< @t145 @t144)) % 2.43/2.61 (define @t147 () (@list @t141)) % 2.43/2.61 (define @t148 () (exists @t147 (and @t146 @t143))) % 2.43/2.61 (define @t149 () (|tptp.'fun_app$b'| @t139 @t61)) % 2.43/2.61 (define @t150 () (not @t149)) % 2.43/2.61 (define @t151 () (< 0 @t144)) % 2.43/2.61 (define @t152 () (@list @t61)) % 2.43/2.61 (define @t153 () (|tptp.'fun_app$b'| @t139 @t75)) % 2.43/2.61 (define @t154 () (@list @t139 @t17)) % 2.43/2.61 (define @t155 () (< @t127 @t117)) % 2.43/2.61 (define @t156 () (=> @t137 false)) % 2.43/2.61 (define @t157 () (= @t117 @t127)) % 2.43/2.61 (define @t158 () (not @t157)) % 2.43/2.61 (define @t159 () (< @t117 @t117)) % 2.43/2.61 (define @t160 () (= @t127 @t117)) % 2.43/2.61 (define @t161 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$a'| @t37))) % 2.43/2.61 (define @t162 () (|tptp.'fun_app$d'| |tptp.'less$'| @t37)) % 2.43/2.61 (define @t163 () (|tptp.'fun_app$c'| @t162 @t29)) % 2.43/2.61 (define @t164 () (@list @t37 @t29)) % 2.43/2.61 (define @t165 () (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t62)) % 2.43/2.61 (define @t166 () (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t17)) % 2.43/2.61 (define @t167 () (= 0 @t117)) % 2.43/2.61 (define @t168 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t75)) % 2.43/2.61 (define @t169 () (< @t165 @t166)) % 2.43/2.61 (define @t170 () (= @t117 1)) % 2.43/2.61 (define @t171 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t14)) % 2.43/2.61 (define @t172 () (< 1 @t117)) % 2.43/2.61 (define @t173 () (= @t6 @t127)) % 2.43/2.61 (define @t174 () (< 0 @t127)) % 2.43/2.61 (define @t175 () (@list @t17)) % 2.43/2.61 (define @t176 () (< 0 @t6)) % 2.43/2.61 (define @t177 () (forall @t175 (=> (and @t173 @t174) false))) % 2.43/2.61 (define @t178 () (or @t130 @t136)) % 2.43/2.61 (define @t179 () (|tptp.'fun_app$l'| |tptp.'of_nat$b'| @t62)) % 2.43/2.61 (define @t180 () (|tptp.'fun_app$l'| (|tptp.'power$'| @t179) @t17)) % 2.43/2.61 (define @t181 () (|tptp.'fun_app$k'| |tptp.'less$a'| |tptp.'zero$k'|)) % 2.43/2.61 (define @t182 () (|tptp.'fun_app$h'| (|tptp.'power$a'| @t117) @t17)) % 2.43/2.61 (define @t183 () (|tptp.'fun_app$i'| (|tptp.'power$b'| @t165) @t17)) % 2.43/2.61 (define @t184 () (|tptp.'powr$'| @t2 0/1)) % 2.43/2.61 (define @t185 () (not @t76)) % 2.43/2.61 (define @t186 () (+ @t127 1)) % 2.43/2.61 (define @t187 () (+ @t117 1)) % 2.43/2.61 (define @t188 () (= @t187 @t186)) % 2.43/2.61 (define @t189 () (+ 0 1)) % 2.43/2.61 (define @t190 () (|tptp.'power$'| @t62)) % 2.43/2.61 (define @t191 () (|tptp.'fun_app$l'| @t190 @t17)) % 2.43/2.61 (define @t192 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t191)) % 2.43/2.61 (define @t193 () (|tptp.'nat$'| @t189)) % 2.43/2.61 (define @t194 () (|tptp.'fun_app$l'| (|tptp.'power$'| @t17) @t61)) % 2.43/2.61 (define @t195 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t194)) % 2.43/2.61 (define @t196 () (= @t117 @t195)) % 2.43/2.61 (define @t197 () (|tptp.'fun_app$l'| (|tptp.'power$'| (|tptp.'fun_app$l'| |tptp.'of_nat$b'| @t17)) @t61)) % 2.43/2.61 (define @t198 () (@list @t62 @t17 @t61)) % 2.43/2.61 (define @t199 () (|tptp.'fun_app$h'| (|tptp.'power$a'| @t127) @t61)) % 2.43/2.61 (define @t200 () (|tptp.'fun_app$i'| (|tptp.'power$b'| @t166) @t61)) % 2.43/2.61 (define @t201 () (= @t192 @t144)) % 2.43/2.61 (define @t202 () (|tptp.'fun_app$l'| |tptp.'of_nat$b'| @t61)) % 2.43/2.61 (define @t203 () (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t61)) % 2.43/2.61 (define @t204 () (< @t187 @t186)) % 2.43/2.61 (define @t205 () (|tptp.'power$b'| @t2)) % 2.43/2.61 (define @t206 () (|tptp.'power$a'| @t6)) % 2.43/2.61 (define @t207 () (|tptp.'powr$'| @t2 @t1)) % 2.43/2.61 (define @t208 () (= @t127 @t144)) % 2.43/2.61 (define @t209 () (|tptp.'fun_app$l'| @t190 @t61)) % 2.43/2.61 (define @t210 () (|tptp.'fun_app$k'| |tptp.'less$a'| |tptp.'one$e'|)) % 2.43/2.61 (define @t211 () (|tptp.'fun_app$b'| @t210 @t62)) % 2.43/2.61 (define @t212 () (|tptp.'fun_app$h'| @t206 @t61)) % 2.43/2.61 (define @t213 () (|tptp.'fun_app$h'| @t206 @t17)) % 2.43/2.61 (define @t214 () (< 1 @t6)) % 2.43/2.61 (define @t215 () (@list @t6 @t17 @t61)) % 2.43/2.61 (define @t216 () (|tptp.'fun_app$i'| @t205 @t61)) % 2.43/2.61 (define @t217 () (|tptp.'fun_app$i'| @t205 @t17)) % 2.43/2.61 (define @t218 () (< 1/1 @t2)) % 2.43/2.61 (define @t219 () (@list @t2 @t17 @t61)) % 2.43/2.61 (define @t220 () (|tptp.'nat$'| @t187)) % 2.43/2.61 (define @t221 () (|tptp.'power$'| |tptp.'zero$k'|)) % 2.43/2.61 (define @t222 () (|tptp.'power$b'| 0/1)) % 2.43/2.61 (define @t223 () (|tptp.'power$a'| 0)) % 2.43/2.61 (define @t224 () (< @t127 @t144)) % 2.43/2.61 (define @t225 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t191) @t209)) % 2.43/2.61 (define @t226 () (< @t213 @t212)) % 2.43/2.61 (define @t227 () (< @t217 @t216)) % 2.43/2.61 (define @t228 () (= @t62 |tptp.'zero$k'|)) % 2.43/2.61 (define @t229 () (= @t191 |tptp.'zero$k'|)) % 2.43/2.61 (define @t230 () (= @t217 0/1)) % 2.43/2.61 (define @t231 () (@list @t2 @t17)) % 2.43/2.61 (define @t232 () (= @t213 0)) % 2.43/2.61 (define @t233 () (@list @t6 @t17)) % 2.43/2.61 (define @t234 () (< @t192 @t144)) % 2.43/2.61 (define @t235 () (< @t117 @t195)) % 2.43/2.61 (define @t236 () (< @t144 @t127)) % 2.43/2.61 (define @t237 () (|tptp.'fun_app$k'| |tptp.'less$a'| @t62)) % 2.43/2.61 (define @t238 () (|tptp.'fun_app$b'| @t181 @t62)) % 2.43/2.61 (define @t239 () (and @t238 (|tptp.'fun_app$b'| @t237 |tptp.'one$e'|))) % 2.43/2.61 (define @t240 () (and @t176 (< @t6 1))) % 2.43/2.61 (define @t241 () (< @t2 1/1)) % 2.43/2.61 (define @t242 () (and @t124 @t241)) % 2.43/2.61 (define @t243 () (|tptp.'nat$'| @t186)) % 2.43/2.61 (define @t244 () (exists @t175 @t140)) % 2.43/2.61 (define @t245 () (not @t153)) % 2.43/2.61 (define @t246 () (@list @t139)) % 2.43/2.61 (define @t247 () (|tptp.'fun_app$l'| @t190 @t243)) % 2.43/2.61 (define @t248 () (|tptp.'fun_app$h'| @t206 @t243)) % 2.43/2.61 (define @t249 () (|tptp.'fun_app$i'| @t205 @t243)) % 2.43/2.61 (define @t250 () (= 0 @t187)) % 2.43/2.61 (define @t251 () (= @t187 0)) % 2.43/2.61 (define @t252 () (= @t117 @t186)) % 2.43/2.61 (define @t253 () (=> @t252 false)) % 2.43/2.61 (define @t254 () (+ @t144 1)) % 2.43/2.61 (define @t255 () (|tptp.'nat$'| @t254)) % 2.43/2.61 (define @t256 () (|tptp.'fun_app$b'| @t139 @t255)) % 2.43/2.61 (define @t257 () (@var "A__questionmark_v0" |tptp.'Nat_nat_bool_fun_fun$'|)) % 2.43/2.61 (define @t258 () (@var "A__questionmark_v4" |tptp.'Nat$'|)) % 2.43/2.61 (define @t259 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t258)) % 2.43/2.61 (define @t260 () (+ @t145 1)) % 2.43/2.61 (define @t261 () (|tptp.'nat$'| @t260)) % 2.43/2.61 (define @t262 () (|tptp.'fun_app$k'| @t257 @t141)) % 2.43/2.61 (define @t263 () (@list @t141 @t258)) % 2.43/2.61 (define @t264 () (exists @t175 @t252)) % 2.43/2.61 (define @t265 () (< @t117 @t186)) % 2.43/2.61 (define @t266 () (not @t137)) % 2.43/2.61 (define @t267 () (@var "A__questionmark_v2" |tptp.'Nat_bool_fun$'|)) % 2.43/2.61 (define @t268 () (|tptp.'fun_app$b'| @t267 @t62)) % 2.43/2.61 (define @t269 () (|tptp.'fun_app$b'| @t267 @t141)) % 2.43/2.61 (define @t270 () (|tptp.'fun_app$b'| @t267 @t261)) % 2.43/2.61 (define @t271 () (< @t145 @t127)) % 2.43/2.61 (define @t272 () (@list @t62 @t17 @t267)) % 2.43/2.61 (define @t273 () (@var "A__questionmark_v2" |tptp.'Nat_nat_bool_fun_fun$'|)) % 2.43/2.61 (define @t274 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| @t273 @t62) @t17)) % 2.43/2.61 (define @t275 () (@var "A__questionmark_v5" |tptp.'Nat$'|)) % 2.43/2.61 (define @t276 () (|tptp.'fun_app$k'| @t273 @t141)) % 2.43/2.61 (define @t277 () (|tptp.'fun_app$b'| @t276 @t275)) % 2.43/2.61 (define @t278 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| @t273 @t258) @t275)) % 2.43/2.61 (define @t279 () (|tptp.'fun_app$b'| @t276 @t258)) % 2.43/2.61 (define @t280 () (< @t145 @t259)) % 2.43/2.61 (define @t281 () (@list @t141 @t258 @t275)) % 2.43/2.61 (define @t282 () (forall @t147 (|tptp.'fun_app$b'| @t276 @t261))) % 2.43/2.61 (define @t283 () (@list @t62 @t17 @t273)) % 2.43/2.61 (define @t284 () (< @t117 @t144)) % 2.43/2.61 (define @t285 () (= @t127 @t254)) % 2.43/2.61 (define @t286 () (< @t187 @t127)) % 2.43/2.61 (define @t287 () (@var "A__questionmark_v1" |tptp.'Nat_bool_fun$'|)) % 2.43/2.61 (define @t288 () (|tptp.'fun_app$b'| @t287 @t61)) % 2.43/2.61 (define @t289 () (< @t144 @t117)) % 2.43/2.61 (define @t290 () (|tptp.'fun_app$b'| @t287 @t62)) % 2.43/2.61 (define @t291 () (< @t144 @t187)) % 2.43/2.61 (define @t292 () (forall @t152 (=> @t291 @t288))) % 2.43/2.61 (define @t293 () (@list @t62 @t287)) % 2.43/2.61 (define @t294 () (< @t127 @t187)) % 2.43/2.61 (define @t295 () (or @t137 @t157)) % 2.43/2.61 (define @t296 () (exists @t152 (and @t291 @t288))) % 2.43/2.61 (define @t297 () (forall @t152 (=> (and @t284 @t285) false))) % 2.43/2.61 (define @t298 () (|tptp.'is_zero_row_upt_k$'| @t37 @t243 @t101)) % 2.43/2.61 (define @t299 () (|tptp.'fun_app$l'| @t221 @t62)) % 2.43/2.61 (define @t300 () (= @t299 |tptp.'zero$k'|)) % 2.43/2.61 (define @t301 () (|tptp.'fun_app$i'| @t222 @t62)) % 2.43/2.61 (define @t302 () (= @t301 0/1)) % 2.43/2.61 (define @t303 () (|tptp.'fun_app$h'| @t223 @t62)) % 2.43/2.61 (define @t304 () (= @t303 0)) % 2.43/2.61 (define @t305 () (|tptp.'power$'| @t61)) % 2.43/2.61 (define @t306 () (|tptp.'fun_app$l'| @t305 @t17)) % 2.43/2.61 (define @t307 () (|tptp.'fun_app$l'| @t305 @t62)) % 2.43/2.61 (define @t308 () (@var "A__questionmark_v2" Int)) % 2.43/2.61 (define @t309 () (|tptp.'power$a'| @t308)) % 2.43/2.61 (define @t310 () (|tptp.'fun_app$h'| @t309 @t17)) % 2.43/2.61 (define @t311 () (|tptp.'fun_app$h'| @t309 @t62)) % 2.43/2.61 (define @t312 () (@list @t62 @t17 @t308)) % 2.43/2.61 (define @t313 () (|tptp.'power$b'| @t120)) % 2.43/2.61 (define @t314 () (|tptp.'fun_app$i'| @t313 @t17)) % 2.43/2.61 (define @t315 () (|tptp.'fun_app$i'| @t313 @t62)) % 2.43/2.61 (define @t316 () (< 1/1 @t120)) % 2.43/2.61 (define @t317 () (@list @t62 @t17 @t120)) % 2.43/2.61 (define @t318 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t220)) % 2.43/2.61 (define @t319 () (@var "A__questionmark_v0" |tptp.'Nat_rows_fun$'|)) % 2.43/2.61 (define @t320 () (|tptp.'fun_app$j'| @t319 @t61)) % 2.43/2.61 (define @t321 () (|tptp.'fun_app$j'| @t319 @t17)) % 2.43/2.61 (define @t322 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t321) @t320)) % 2.43/2.61 (define @t323 () (|tptp.'fun_app$j'| @t319 @t261)) % 2.43/2.61 (define @t324 () (|tptp.'fun_app$j'| @t319 @t141)) % 2.43/2.61 (define @t325 () (forall @t147 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t324) @t323))) % 2.43/2.61 (define @t326 () (@list @t319 @t17 @t61)) % 2.43/2.61 (define @t327 () (@var "A__questionmark_v0" |tptp.'Nat_int_fun$'|)) % 2.43/2.61 (define @t328 () (|tptp.'fun_app$h'| @t327 @t61)) % 2.43/2.61 (define @t329 () (|tptp.'fun_app$h'| @t327 @t17)) % 2.43/2.61 (define @t330 () (< @t329 @t328)) % 2.43/2.61 (define @t331 () (|tptp.'fun_app$h'| @t327 @t261)) % 2.43/2.61 (define @t332 () (|tptp.'fun_app$h'| @t327 @t141)) % 2.43/2.61 (define @t333 () (forall @t147 (< @t332 @t331))) % 2.43/2.61 (define @t334 () (@list @t327 @t17 @t61)) % 2.43/2.61 (define @t335 () (@var "A__questionmark_v0" |tptp.'Nat_real_fun$'|)) % 2.43/2.61 (define @t336 () (|tptp.'fun_app$i'| @t335 @t61)) % 2.43/2.61 (define @t337 () (|tptp.'fun_app$i'| @t335 @t17)) % 2.43/2.61 (define @t338 () (< @t337 @t336)) % 2.43/2.61 (define @t339 () (|tptp.'fun_app$i'| @t335 @t261)) % 2.43/2.61 (define @t340 () (|tptp.'fun_app$i'| @t335 @t141)) % 2.43/2.61 (define @t341 () (forall @t147 (< @t340 @t339))) % 2.43/2.61 (define @t342 () (@list @t335 @t17 @t61)) % 2.43/2.61 (define @t343 () (|tptp.'fun_app$b'| @t287 @t255)) % 2.43/2.61 (define @t344 () (|tptp.'fun_app$b'| @t287 @t75)) % 2.43/2.61 (define @t345 () (|tptp.'from_nat$a'| @t17)) % 2.43/2.61 (define @t346 () (|tptp.'fun_app$j'| |tptp.'from_nat$'| @t75)) % 2.43/2.61 (define @t347 () (forall @t147 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t323) @t324))) % 2.43/2.61 (define @t348 () (= @t315 @t1)) % 2.43/2.61 (define @t349 () (and @t130 @t123)) % 2.43/2.61 (define @t350 () (@list @t62 @t1)) % 2.43/2.61 (define @t351 () (@var "A__questionmark_v3" Real)) % 2.43/2.61 (define @t352 () (@list @t351)) % 2.43/2.61 (define @t353 () (< @t1 @t120)) % 2.43/2.61 (define @t354 () (|tptp.'powr$'| @t2 @t120)) % 2.43/2.61 (define @t355 () (< @t207 @t354)) % 2.43/2.61 (define @t356 () (@list @t2 @t1 @t120)) % 2.43/2.61 (define @t357 () (|tptp.'ln$'| @t1)) % 2.43/2.61 (define @t358 () (|tptp.'ln$'| @t2)) % 2.43/2.61 (define @t359 () (< 0/1 @t358)) % 2.43/2.61 (define @t360 () (< @t358 0/1)) % 2.43/2.61 (define @t361 () (|tptp.'powr$'| @t1 @t2)) % 2.43/2.61 (define @t362 () (|tptp.'powr$'| @t120 @t2)) % 2.43/2.61 (define @t363 () (< @t2 0/1)) % 2.43/2.61 (define @t364 () (|tptp.'powr$'| @t120 @t1)) % 2.43/2.61 (define @t365 () (|tptp.'fun_app$i'| (|tptp.'power$b'| @t1) @t61)) % 2.43/2.61 (define @t366 () (= @t29 @t37)) % 2.43/2.61 (define @t367 () (|tptp.'fun_app$c'| @t30 @t37)) % 2.43/2.61 (define @t368 () (not @t163)) % 2.43/2.61 (define @t369 () (@var "A__questionmark_v0" |tptp.'Rows_rows_bool_fun_fun$'|)) % 2.43/2.61 (define @t370 () (@var "A__questionmark_v4" |tptp.'Rows$'|)) % 2.43/2.61 (define @t371 () (|tptp.'fun_app$d'| @t369 @t47)) % 2.43/2.61 (define @t372 () (|tptp.'fun_app$c'| @t371 @t370)) % 2.43/2.61 (define @t373 () (@list @t47 @t370)) % 2.43/2.61 (define @t374 () (|tptp.'fun_app$c'| @t50 @t29)) % 2.43/2.61 (define @t375 () (@list @t37 @t29 @t27)) % 2.43/2.61 (define @t376 () (|tptp.'fun_app$c'| @t50 @t37)) % 2.43/2.61 (define @t377 () (= @t37 @t29)) % 2.43/2.61 (define @t378 () (not @t367)) % 2.43/2.61 (define @t379 () (@var "A__questionmark_v0" |tptp.'Rows_bool_fun$'|)) % 2.43/2.61 (define @t380 () (|tptp.'fun_app$c'| @t379 @t27)) % 2.43/2.61 (define @t381 () (|tptp.'fun_app$c'| @t379 @t29)) % 2.43/2.61 (define @t382 () (=> @t367 false)) % 2.43/2.61 (define @t383 () (=> @t163 false)) % 2.43/2.61 (define @t384 () (@var "A__questionmark_v2" tptp.tlbool)) % 2.43/2.61 (define @t385 () (not @t366)) % 2.43/2.61 (define @t386 () (|tptp.'fun_app$c'| @t162 @t37)) % 2.43/2.61 (define @t387 () (not @t377)) % 2.43/2.61 (define @t388 () (|tptp.'nat$'| @t6)) % 2.43/2.61 (define @t389 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t388)) % 2.43/2.61 (define @t390 () (- @t127)) % 2.43/2.61 (define @t391 () (= @t6 @t390)) % 2.43/2.61 (define @t392 () (forall @t175 (=> (and @t391 @t174) false))) % 2.43/2.61 (define @t393 () (< @t6 0)) % 2.43/2.61 (define @t394 () (|tptp.'fun_app$k'| |tptp.'less_eq$'| |tptp.'zero$k'|)) % 2.43/2.61 (define @t395 () (|tptp.'fun_app$b'| @t394 @t62)) % 2.43/2.61 (define @t396 () (|tptp.'fun_app$h'| (|tptp.'power$a'| @t5) @t61)) % 2.43/2.61 (define @t397 () (<= 0 @t6)) % 2.43/2.61 (define @t398 () (@list @t6 @t5 @t61)) % 2.43/2.61 (define @t399 () (<= 0/1 @t2)) % 2.43/2.61 (define @t400 () (@list @t2 @t1 @t61)) % 2.43/2.61 (define @t401 () (- @t5)) % 2.43/2.61 (define @t402 () (- @t6)) % 2.43/2.61 (define @t403 () (<= 0 @t117)) % 2.43/2.61 (define @t404 () (<= @t117 @t127)) % 2.43/2.61 (define @t405 () (- @t1)) % 2.43/2.61 (define @t406 () (- @t2)) % 2.43/2.61 (define @t407 () (|tptp.'uminus$'| @t37)) % 2.43/2.61 (define @t408 () (|tptp.'uminus$a'| @t73)) % 2.43/2.61 (define @t409 () (<= @t165 @t166)) % 2.43/2.61 (define @t410 () (- @t117)) % 2.43/2.61 (define @t411 () (<= @t6 0)) % 2.43/2.61 (define @t412 () (<= @t2 0/1)) % 2.43/2.61 (define @t413 () (= @t389 0)) % 2.43/2.61 (define @t414 () (and @t118 @t136)) % 2.43/2.61 (define @t415 () (<= @t2 @t1)) % 2.43/2.61 (define @t416 () (= (|tptp.'powr$'| @t2 1/1) @t2)) % 2.43/2.61 (define @t417 () (<= @t1 @t120)) % 2.43/2.61 (define @t418 () (not @t397)) % 2.43/2.61 (define @t419 () (=> @t397 (= @t389 @t6))) % 2.43/2.61 (define @t420 () (- 1/1)) % 2.43/2.61 (define @t421 () (- 1)) % 2.43/2.61 (define @t422 () (<= @t127 @t144)) % 2.43/2.61 (define @t423 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t191) @t209)) % 2.43/2.61 (define @t424 () (<= @t213 @t212)) % 2.43/2.61 (define @t425 () (<= @t217 @t216)) % 2.43/2.61 (define @t426 () (<= @t117 0)) % 2.43/2.61 (define @t427 () (<= @t117 @t195)) % 2.43/2.61 (define @t428 () (<= @t192 @t144)) % 2.43/2.61 (define @t429 () (<= @t2 1/1)) % 2.43/2.61 (define @t430 () (<= 1/1 @t2)) % 2.43/2.61 (define @t431 () (<= 0/1 @t358)) % 2.43/2.61 (define @t432 () (|tptp.'nat$'| @t5)) % 2.43/2.61 (define @t433 () (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t432)) % 2.43/2.61 (define @t434 () (< @t389 @t433)) % 2.43/2.61 (define @t435 () (- @t318)) % 2.43/2.61 (define @t436 () (<= @t144 @t127)) % 2.43/2.61 (define @t437 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t62) @t17)) % 2.43/2.61 (define @t438 () (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t209) @t194)) % 2.43/2.61 (define @t439 () (<= @t6 @t5)) % 2.43/2.61 (define @t440 () (<= @t212 @t396)) % 2.43/2.61 (define @t441 () (<= 0 @t5)) % 2.43/2.61 (define @t442 () (<= @t216 @t365)) % 2.43/2.61 (define @t443 () (<= 0/1 @t1)) % 2.43/2.61 (define @t444 () (or @t163 @t366)) % 2.43/2.61 (define @t445 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$a'| @t37) @t29)) % 2.43/2.61 (define @t446 () (not @t445)) % 2.43/2.61 (define @t447 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$a'| @t29) @t37)) % 2.43/2.61 (define @t448 () (and @t445 @t385)) % 2.43/2.61 (define @t449 () (<= 1/1 @t120)) % 2.43/2.61 (define @t450 () (<= @t389 @t433)) % 2.43/2.61 (define @t451 () (|tptp.'fun_app$b'| @t139 @t432)) % 2.43/2.61 (define @t452 () (@list @t5)) % 2.43/2.61 (define @t453 () (= @t117 @t433)) % 2.43/2.61 (define @t454 () (@list @t62 @t5)) % 2.43/2.61 (define @t455 () (|tptp.'fun_app$k'| |tptp.'less_eq$'| |tptp.'one$e'|)) % 2.43/2.61 (define @t456 () (forall @t175 (=> @t391 false))) % 2.43/2.61 (define @t457 () (<= 0 0)) % 2.43/2.61 (define @t458 () (<= @t187 @t127)) % 2.43/2.61 (define @t459 () (<= @t117 @t186)) % 2.43/2.61 (define @t460 () (|tptp.'fun_app$b'| @t267 @t17)) % 2.43/2.61 (define @t461 () (<= @t117 @t145)) % 2.43/2.61 (define @t462 () (forall @t175 (=> @t173 false))) % 2.43/2.61 (define @t463 () (and @t404 @t158)) % 2.43/2.61 (define @t464 () (@var "A__questionmark_v0" |tptp.'Nat_nat_fun$'|)) % 2.43/2.61 (define @t465 () (<= 1 @t6)) % 2.43/2.61 (define @t466 () (@var "A__questionmark_v0" |tptp.'Int_bool_fun$'|)) % 2.43/2.61 (define @t467 () (= @t6 (- (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t243)))) % 2.43/2.61 (define @t468 () (and @t140 @t245)) % 2.43/2.61 (define @t469 () (<= @t145 @t144)) % 2.43/2.61 (define @t470 () (forall @t122 (=> (|tptp.'member$'| @t120 @t9) (<= @t120 @t1)))) % 2.43/2.61 (define @t471 () (@list @t1)) % 2.43/2.61 (define @t472 () (<= @t127 @t117)) % 2.43/2.61 (define @t473 () (@var "A__questionmark_v2" |tptp.'Nat_real_fun$'|)) % 2.43/2.61 (define @t474 () (|tptp.'fun_app$i'| @t473 @t62)) % 2.43/2.61 (define @t475 () (@var "A__questionmark_v1" |tptp.'Nat_real_fun$'|)) % 2.43/2.61 (define @t476 () (|tptp.'fun_app$i'| @t475 @t141)) % 2.43/2.61 (define @t477 () (|tptp.'fun_app$i'| @t473 @t141)) % 2.43/2.61 (define @t478 () (@var "B" tptp.tlbool)) % 2.43/2.61 (define @t479 () (@var "BOUND_VARIABLE_10431" |tptp.'Rows$'|)) % 2.43/2.61 (define @t480 () (|tptp.'is_zero_row_upt_k$'| @t479 @t17 @t18)) % 2.43/2.61 (define @t481 () (@var "BOUND_VARIABLE_10429" |tptp.'Rows$'|)) % 2.43/2.61 (define @t482 () (not (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t481) @t479))) % 2.43/2.61 (define @t483 () (not (|tptp.'is_zero_row_upt_k$'| @t481 @t17 @t18))) % 2.43/2.61 (define @t484 () (not @t20)) % 2.43/2.61 (define @t485 () (or @t483 @t482 @t480)) % 2.43/2.61 (define @t486 () (or @t484 @t485)) % 2.43/2.61 (define @t487 () (forall (@list @t18 @t17 @t481 @t479) @t486)) % 2.43/2.61 (define @t488 () (@list @t481 @t479)) % 2.43/2.61 (define @t489 () (forall @t488 @t486)) % 2.43/2.61 (define @t490 () (forall @t488 @t485)) % 2.43/2.61 (define @t491 () (@var "BOUND_VARIABLE_10413" |tptp.'Rows$'|)) % 2.43/2.61 (define @t492 () (or @t484 @t490)) % 2.43/2.61 (define @t493 () (|tptp.'is_zero_row_upt_k$'| @t491 @t17 @t18)) % 2.43/2.61 (define @t494 () (not (|tptp.'fun_app$c'| @t50 @t491))) % 2.43/2.61 (define @t495 () (not @t56)) % 2.43/2.61 (define @t496 () (or @t495 @t494 @t493)) % 2.43/2.61 (define @t497 () (@list @t27 @t491)) % 2.43/2.61 (define @t498 () (forall @t497 @t496)) % 2.43/2.61 (define @t499 () (or @t494 @t493)) % 2.43/2.61 (define @t500 () (or @t495 @t499)) % 2.43/2.61 (define @t501 () (forall @t497 @t500)) % 2.43/2.61 (define @t502 () (@list @t491)) % 2.43/2.61 (define @t503 () (forall @t502 @t500)) % 2.43/2.61 (define @t504 () (forall @t502 @t499)) % 2.43/2.61 (define @t505 () (or @t495 @t504)) % 2.43/2.61 (define @t506 () (not @t51)) % 2.43/2.61 (define @t507 () (forall @t53 (or @t506 @t48))) % 2.43/2.61 (define @t508 () (forall @t53 (not @t52))) % 2.43/2.61 (define @t509 () (not @t508)) % 2.43/2.61 (define @t510 () (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t346) |tptp.'i$'|)) % 2.43/2.61 (define @t511 () (not @t510)) % 2.43/2.61 (define @t512 () (|tptp.'is_zero_row_upt_k$'| @t346 @t14 |tptp.'a$'|)) % 2.43/2.62 (define @t513 () (not @t512)) % 2.43/2.62 (define @t514 () (|tptp.'fun_app$b'| (|tptp.'reduced_row_echelon_form_upt_k$'| |tptp.'a$'|) @t14)) % 2.43/2.62 (define @t515 () (not @t514)) % 2.43/2.62 (define @t516 () (or @t515 @t513 @t511 @t15)) % 2.43/2.62 (define @t517 () (or @t13 @t514)) % 2.43/2.62 (define @t518 () (not @t517)) % 2.43/2.62 (define @t519 () (forall @t22 (or (not @t21) @t20))) % 2.43/2.62 (assume @p1 (forall @t4 (= (|tptp.'fun_app$'| (|tptp.'uub$'| @t2) @t1) @t3))) % 2.43/2.62 (assume @p2 (forall @t8 (= (|tptp.'fun_app$a'| (|tptp.'uua$'| @t6) @t5) @t7))) % 2.43/2.62 (assume @p3 (forall (@list @t9 @t1) (= (|tptp.'fun_app$'| @t11 @t1) @t10))) % 2.43/2.62 (assume @p4 (not @t13)) % 2.43/2.62 (assume @p5 (not @t15)) % 2.43/2.62 (assume @p6 @t16) % 2.43/2.62 (assume @p7 @t12) % 2.43/2.62 (assume @p8 @t23) % 2.43/2.62 (assume @p9 @t25) % 2.43/2.62 (assume @p10 (not (= (|tptp.'column$'| |tptp.'zero$a'| |tptp.'a$'|) |tptp.'zero$b'|))) % 2.43/2.62 (assume @p11 (forall @t26 (= @t21 (|tptp.'fun_app$b'| @t19 (|tptp.'ncols$'| @t18))))) % 2.43/2.62 (assume @p12 (forall @t26 (=> @t21 (forall @t34 (=> @t33 (not (exists @t32 (and @t31 (not @t28))))))))) % 2.43/2.62 (assume @p13 (forall @t35 (=> (and @t21 @t33) (forall @t32 (=> @t31 @t28))))) % 2.43/2.62 (assume @p14 (not (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| @t36 |tptp.'i$'|)) |tptp.'zero$a'|) |tptp.'zero$c'|))) % 2.43/2.62 (assume @p15 (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| @t36 |tptp.'zero$'|)) |tptp.'zero$a'|) |tptp.'zero$c'|)) % 2.43/2.62 (assume @p16 (=> (forall @t38 (=> (and (not (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| @t36 @t37)) |tptp.'zero$a'|) |tptp.'zero$c'|)) (|tptp.'fun_app$c'| @t24 @t37)) false)) false)) % 2.43/2.62 (assume @p17 (forall @t42 (= @t41 @t40))) % 2.43/2.62 (assume @p18 (forall @t42 (= @t41 @t46))) % 2.43/2.62 (assume @p19 @t60) % 2.43/2.62 (assume @p20 (forall @t42 (= @t40 @t46))) % 2.43/2.62 (assume @p21 (forall (@list @t18 @t17 @t27 @t47) (=> (and @t20 @t56 @t51) @t48))) % 2.43/2.62 (assume @p22 (forall (@list @t37 @t39 @t61) (=> @t41 (|tptp.'is_zero_row_upt_k$'| @t37 @t61 @t39)))) % 2.43/2.62 (assume @p23 (forall (@list @t62 @t39) (=> (forall @t32 (|tptp.'is_zero_row_upt_k$'| @t27 @t62 @t39)) (|tptp.'fun_app$b'| (|tptp.'reduced_row_echelon_form_upt_k$'| @t39) @t62)))) % 2.43/2.62 (assume @p24 (forall (@list @t63) (=> (and (|tptp.'reduced_row_echelon_form$a'| @t63) (= (|tptp.'vec_nth$b'| (|tptp.'vec_nth$c'| @t63 |tptp.'zero$'|) |tptp.'zero$'|) 0/1)) (= (|tptp.'column$a'| |tptp.'zero$'| @t63) |tptp.'zero$d'|)))) % 2.43/2.62 (assume @p25 (forall (@list @t64) (=> (and (|tptp.'reduced_row_echelon_form$b'| @t64) (= (|tptp.'vec_nth$d'| (|tptp.'vec_nth$e'| @t64 |tptp.'zero$'|) |tptp.'zero$'|) 0)) (= (|tptp.'column$b'| |tptp.'zero$'| @t64) |tptp.'zero$e'|)))) % 2.43/2.62 (assume @p26 (forall (@list @t65) (=> (and (|tptp.'reduced_row_echelon_form$c'| @t65) (= (|tptp.'vec_nth$f'| (|tptp.'vec_nth$g'| @t65 |tptp.'zero$'|) |tptp.'zero$'|) |tptp.'zero$'|)) (= (|tptp.'column$c'| |tptp.'zero$'| @t65) |tptp.'zero$f'|)))) % 2.43/2.62 (assume @p27 (forall (@list @t66) (=> (and (|tptp.'reduced_row_echelon_form$d'| @t66) (= (|tptp.'vec_nth$h'| (|tptp.'vec_nth$i'| @t66 |tptp.'zero$'|) |tptp.'zero$'|) |tptp.'zero$a'|)) (= (|tptp.'column$d'| |tptp.'zero$'| @t66) |tptp.'zero$g'|)))) % 2.43/2.62 (assume @p28 (forall (@list @t67) (=> (and (|tptp.'reduced_row_echelon_form$e'| @t67) (= (|tptp.'vec_nth$j'| (|tptp.'vec_nth$k'| @t67 |tptp.'zero$'|) |tptp.'zero$'|) |tptp.'zero$c'|)) (= (|tptp.'column$e'| |tptp.'zero$'| @t67) |tptp.'zero$b'|)))) % 2.43/2.62 (assume @p29 (forall (@list @t68) (=> (and (|tptp.'reduced_row_echelon_form$f'| @t68) (= (|tptp.'vec_nth$l'| (|tptp.'vec_nth$m'| @t68 |tptp.'zero$'|) |tptp.'zero$a'|) 0/1)) (= (|tptp.'column$f'| |tptp.'zero$a'| @t68) |tptp.'zero$d'|)))) % 2.43/2.62 (assume @p30 (forall (@list @t69) (=> (and (|tptp.'reduced_row_echelon_form$g'| @t69) (= (|tptp.'vec_nth$n'| (|tptp.'vec_nth$o'| @t69 |tptp.'zero$'|) |tptp.'zero$a'|) 0)) (= (|tptp.'column$g'| |tptp.'zero$a'| @t69) |tptp.'zero$e'|)))) % 2.43/2.62 (assume @p31 (forall (@list @t70) (=> (and (|tptp.'reduced_row_echelon_form$h'| @t70) (= (|tptp.'vec_nth$p'| (|tptp.'vec_nth$q'| @t70 |tptp.'zero$'|) |tptp.'zero$a'|) |tptp.'zero$'|)) (= (|tptp.'column$h'| |tptp.'zero$a'| @t70) |tptp.'zero$f'|)))) % 2.43/2.62 (assume @p32 (forall (@list @t71) (=> (and (|tptp.'reduced_row_echelon_form$i'| @t71) (= (|tptp.'vec_nth$r'| (|tptp.'vec_nth$s'| @t71 |tptp.'zero$'|) |tptp.'zero$a'|) |tptp.'zero$a'|)) (= (|tptp.'column$i'| |tptp.'zero$a'| @t71) |tptp.'zero$g'|)))) % 2.43/2.62 (assume @p33 (forall (@list @t72) (=> (and (|tptp.'reduced_row_echelon_form$j'| @t72) (= (|tptp.'vec_nth$b'| (|tptp.'vec_nth$t'| @t72 |tptp.'zero$a'|) |tptp.'zero$'|) 0/1)) (= (|tptp.'column$j'| |tptp.'zero$'| @t72) |tptp.'zero$h'|)))) % 2.43/2.62 (assume @p34 (forall @t74 (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| |tptp.'zero$i'|) @t73) |tptp.'zero$c'|))) % 2.43/2.62 (assume @p35 (forall @t38 (= (|tptp.'fun_app$f'| (|tptp.'vec_nth$a'| |tptp.'zero$j'|) @t37) |tptp.'zero$i'|))) % 2.43/2.62 (assume @p36 (forall @t74 (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| |tptp.'one$'|) @t73) |tptp.'one$a'|))) % 2.43/2.62 (assume @p37 (forall @t38 (= (|tptp.'fun_app$f'| (|tptp.'vec_nth$a'| |tptp.'one$b'|) @t37) |tptp.'one$'|))) % 2.43/2.62 (assume @p38 (< 0 1)) % 2.43/2.62 (assume @p39 (< 0/1 1/1)) % 2.43/2.62 (assume @p40 (not (< 1 0))) % 2.43/2.62 (assume @p41 (not (< 1/1 0/1))) % 2.43/2.62 (assume @p42 (not (< 1 1))) % 2.43/2.62 (assume @p43 (not (< 1/1 1/1))) % 2.43/2.62 (assume @p44 (forall @t35 (|tptp.'is_zero_row_upt_k$'| @t29 @t75 @t18))) % 2.43/2.62 (assume @p45 (forall @t42 (|tptp.'is_zero_row_upt_k$'| @t37 @t75 @t39))) % 2.43/2.62 (assume @p46 (forall @t78 (= @t77 @t76))) % 2.43/2.62 (assume @p47 (forall @t81 (= @t80 @t79))) % 2.43/2.62 (assume @p48 (forall @t38 (= @t83 @t82))) % 2.43/2.62 (assume @p49 (forall @t74 (= @t85 @t84))) % 2.43/2.62 (assume @p50 (forall (@list @t86) (= (= |tptp.'zero$c'| @t86) (= @t86 |tptp.'zero$c'|)))) % 2.43/2.62 (assume @p51 (forall @t8 (=> (and (not @t88) (=> @t7 false) (=> @t87 false)) false))) % 2.43/2.62 (assume @p52 (forall @t4 (=> (and (not @t90) (=> @t3 false) (=> @t89 false)) false))) % 2.43/2.62 (assume @p53 (forall @t81 (= (= 1 @t6) (= @t6 1)))) % 2.43/2.62 (assume @p54 (forall @t78 (= (= 1/1 @t2) @t91))) % 2.43/2.62 (assume @p55 (forall (@list @t95 @t98 @t93 @t92) (and (=> @t96 (and (=> @t96 (= @t100 @t100)) (=> @t97 (= @t100 @t94)))) (=> @t97 (and (=> @t96 (= @t94 @t100)) (=> @t97 (= @t94 @t94))))))) % 2.43/2.62 (assume @p56 (forall (@list @t95 @t39 @t101 @t47) (and (=> @t96 (and (=> @t96 (= @t104 @t104)) (=> @t97 (= @t104 @t103)))) (=> @t97 (and (=> @t96 (= @t103 @t104)) (=> @t97 (= @t103 @t103))))))) % 2.43/2.62 (assume @p57 (forall @t108 (= @t107 (forall @t45 (= (|tptp.'fun_app$e'| @t106 @t43) (|tptp.'fun_app$e'| @t99 @t43)))))) % 2.43/2.62 (assume @p58 (forall @t112 (= @t111 (forall @t32 (= (|tptp.'fun_app$f'| @t110 @t27) @t109))))) % 2.43/2.62 (assume @p59 (forall @t108 (= (= @t106 @t99) @t107))) % 2.43/2.62 (assume @p60 (forall @t112 (= (= @t110 @t44) @t111))) % 2.43/2.62 (assume @p61 (forall (@list @t2 @t113) (= (|tptp.'member$'| @t2 (|tptp.'collect$'| @t113)) (|tptp.'fun_app$'| @t113 @t2)))) % 2.43/2.62 (assume @p62 (forall @t114 (= (|tptp.'collect$'| @t11) @t9))) % 2.43/2.62 (assume @p63 (not @t115)) % 2.43/2.62 (assume @p64 (not (< 0/1 0/1))) % 2.43/2.62 (assume @p65 (not (= 0/1 1/1))) % 2.43/2.62 (assume @p66 (not (= 0 1))) % 2.43/2.62 (assume @p67 (forall (@list @t116 @t39 @t27 @t92) (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'fun_app$f'| (|tptp.'vec_nth$a'| (|tptp.'map_matrix$'| @t116 @t39)) @t27)) @t92) (|tptp.'fun_app$g'| @t116 (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| @t109) @t92))))) % 2.43/2.62 (assume @p68 (forall @t119 (= (< @t117 1) @t118))) % 2.43/2.62 (assume @p69 (forall @t4 (=> @t125 (exists @t122 (and @t121 (< @t120 @t2) (< @t120 @t1)))))) % 2.43/2.62 (assume @p70 (= (|tptp.'dbl_inc$'| 0/1) 1/1)) % 2.43/2.62 (assume @p71 (= (|tptp.'dbl_inc$a'| 0) 1)) % 2.43/2.62 (assume @p72 (= (|tptp.'dbl_inc$b'| |tptp.'zero$'|) |tptp.'one$c'|)) % 2.43/2.62 (assume @p73 (= (|tptp.'dbl_inc$c'| |tptp.'zero$a'|) |tptp.'one$d'|)) % 2.43/2.62 (assume @p74 (forall @t129 (= @t128 (forall (@list @t92) (=> (< (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$'| @t92)) @t127) (= (|tptp.'fun_app$e'| @t126 @t92) |tptp.'zero$c'|)))))) % 2.43/2.62 (assume @p75 (= (|tptp.'arcosh$'| 1/1) 0/1)) % 2.43/2.62 (assume @p76 (= 1 1)) % 2.43/2.62 (assume @p77 (forall @t119 (= @t131 @t130))) % 2.43/2.62 (assume @p78 (forall @t119 (= @t132 false))) % 2.43/2.62 (assume @p79 (forall (@list @t86 @t133) (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'vec$'| @t86)) @t133) @t86))) % 2.43/2.62 (assume @p80 (forall (@list @t105 @t29) (= (|tptp.'fun_app$f'| (|tptp.'vec_nth$a'| (|tptp.'vec$a'| @t105)) @t29) @t105))) % 2.43/2.62 (assume @p81 (forall (@list @t73 @t134) (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| (|tptp.'axis$'| @t73 @t134)) @t73) @t134))) % 2.43/2.62 (assume @p82 (forall (@list @t37 @t98) (= (|tptp.'fun_app$f'| (|tptp.'vec_nth$a'| (|tptp.'axis$a'| @t37 @t98)) @t37) @t98))) % 2.43/2.62 (assume @p83 (forall @t119 (=> (and @t135 (=> @t131 false)) false))) % 2.43/2.62 (assume @p84 (= 0 0)) % 2.43/2.62 (assume @p85 (forall @t119 (not @t132))) % 2.43/2.62 (assume @p86 (forall @t119 (=> @t135 @t130))) % 2.43/2.62 (assume @p87 (forall @t119 (= (not @t130) @t118))) % 2.43/2.62 (assume @p88 (forall @t119 (=> @t132 false))) % 2.43/2.62 (assume @p89 (forall @t138 (=> @t137 (not @t136)))) % 2.43/2.62 (assume @p90 (forall @t154 (=> (and @t153 (forall @t152 (=> (and @t151 @t150) @t148))) @t140))) % 2.43/2.62 (assume @p91 (forall @t138 (=> (and @t158 @t156 (=> @t155 false)) false))) % 2.43/2.62 (assume @p92 (forall @t154 (=> (forall @t152 (=> @t150 @t148)) @t140))) % 2.43/2.62 (assume @p93 (forall @t154 (=> (forall @t152 (=> (forall @t147 (=> @t146 @t142)) @t149)) @t140))) % 2.43/2.62 (assume @p94 (forall @t119 (=> @t159 false))) % 2.43/2.62 (assume @p95 (forall @t138 (=> @t137 @t158))) % 2.43/2.62 (assume @p96 (forall @t138 (=> @t137 (not @t160)))) % 2.43/2.62 (assume @p97 (forall @t119 (not @t159))) % 2.43/2.62 (assume @p98 (forall @t138 (= @t158 (or @t137 @t155)))) % 2.43/2.62 (assume @p99 (= (|tptp.'arsinh$'| 0/1) 0/1)) % 2.43/2.62 (assume @p100 (= (|tptp.'artanh$'| 0/1) 0/1)) % 2.43/2.62 (assume @p101 (forall @t164 (=> @t163 (< @t161 (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$a'| @t29)))))) % 2.43/2.62 (assume @p102 (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$a'| |tptp.'zero$'|)) 0)) % 2.43/2.62 (assume @p103 (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$'| |tptp.'zero$a'|)) 0)) % 2.43/2.62 (assume @p104 (forall @t38 (= (= @t161 0) @t82))) % 2.43/2.62 (assume @p105 (forall @t74 (= (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'to_nat$'| @t73)) 0) @t84))) % 2.43/2.62 (assume @p106 (= (|tptp.'ln$'| 1/1) 0/1)) % 2.43/2.62 (assume @p107 (forall @t119 (= @t130 @t130))) % 2.43/2.62 (assume @p108 (forall @t119 (= (< 0/1 @t165) @t130))) % 2.43/2.62 (assume @p109 (forall @t138 (= @t157 @t157))) % 2.43/2.62 (assume @p110 (forall @t138 (= (= @t165 @t166) @t157))) % 2.43/2.62 (assume @p111 (forall @t119 (= @t118 @t118))) % 2.43/2.62 (assume @p112 (forall @t119 (= (= @t165 0/1) @t118))) % 2.43/2.62 (assume @p113 (forall @t119 (= @t167 @t167))) % 2.43/2.62 (assume @p114 (forall @t119 (= (= 0/1 @t165) @t167))) % 2.43/2.62 (assume @p115 (= @t168 0)) % 2.43/2.62 (assume @p116 (= (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t75) 0/1)) % 2.43/2.62 (assume @p117 (forall @t138 (= @t137 @t137))) % 2.43/2.62 (assume @p118 (forall @t138 (= @t169 @t137))) % 2.43/2.62 (assume @p119 (forall @t119 (= @t170 @t170))) % 2.43/2.62 (assume @p120 (forall @t119 (= (= @t165 1/1) @t170))) % 2.43/2.62 (assume @p121 (forall @t119 (= (= 1 @t117) @t170))) % 2.43/2.62 (assume @p122 (forall @t119 (= (= 1/1 @t165) @t170))) % 2.43/2.62 (assume @p123 (= @t171 1)) % 2.43/2.62 (assume @p124 (= (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t14) 1/1)) % 2.43/2.62 (assume @p125 (forall @t119 (not (< @t165 0/1)))) % 2.43/2.62 (assume @p126 (forall @t138 (=> @t137 @t137))) % 2.43/2.62 (assume @p127 (forall @t138 (=> @t169 @t137))) % 2.43/2.62 (assume @p128 (forall @t138 (=> @t137 @t169))) % 2.43/2.62 (assume @p129 (forall @t119 (=> @t172 @t172))) % 2.43/2.62 (assume @p130 (forall @t119 (=> (< 1/1 @t165) @t172))) % 2.43/2.62 (assume @p131 (forall @t81 (=> @t176 (exists @t175 (and @t174 @t173))))) % 2.43/2.62 (assume @p132 (forall @t81 (=> (and @t176 @t177) false))) % 2.43/2.62 (assume @p133 (forall @t78 (exists @t175 (< @t2 @t166)))) % 2.43/2.62 (assume @p134 (forall (@list @t37 @t17) (=> (|tptp.'fun_app$c'| @t162 (|tptp.'fun_app$j'| |tptp.'from_nat$'| @t17)) (< @t161 @t127)))) % 2.43/2.62 (assume @p135 (forall @t138 (= (|tptp.'fun_app$b'| @t181 @t180) @t178))) % 2.43/2.62 (assume @p136 (forall @t138 (= (< 0 @t182) @t178))) % 2.43/2.62 (assume @p137 (forall @t138 (= (< 0/1 @t183) @t178))) % 2.43/2.62 (assume @p138 (forall @t78 (and (=> @t76 (= @t184 0/1)) (=> @t185 (= @t184 1/1))))) % 2.43/2.62 (assume @p139 (forall @t138 (= @t188 @t157))) % 2.43/2.62 (assume @p140 (forall @t119 (= (|tptp.'fun_app$l'| (|tptp.'power$'| |tptp.'one$e'|) @t62) |tptp.'one$e'|))) % 2.43/2.62 (assume @p141 (forall @t119 (= (|tptp.'fun_app$i'| (|tptp.'power$b'| 1/1) @t62) 1/1))) % 2.43/2.62 (assume @p142 (forall @t119 (= (|tptp.'fun_app$h'| (|tptp.'power$a'| 1) @t62) 1))) % 2.43/2.62 (assume @p143 (forall @t138 (= (= @t192 @t189) (or @t136 (= @t117 @t189))))) % 2.43/2.62 (assume @p144 (forall @t119 (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| (|tptp.'power$'| @t193) @t62)) @t189))) % 2.43/2.62 (assume @p145 (forall @t138 (= (< 0 @t192) @t178))) % 2.43/2.62 (assume @p146 (forall @t198 (= (= @t179 @t197) @t196))) % 2.43/2.62 (assume @p147 (forall @t198 (= (= @t117 @t199) @t196))) % 2.43/2.62 (assume @p148 (forall @t198 (= (= @t165 @t200) @t196))) % 2.43/2.62 (assume @p149 (forall @t198 (= (= @t180 @t202) @t201))) % 2.43/2.62 (assume @p150 (forall @t198 (= (= @t182 @t144) @t201))) % 2.43/2.62 (assume @p151 (forall @t198 (= (= @t183 @t203) @t201))) % 2.43/2.62 (assume @p152 (forall @t138 (= (|tptp.'fun_app$l'| |tptp.'of_nat$b'| @t191) @t180))) % 2.43/2.62 (assume @p153 (forall @t138 (= @t192 @t182))) % 2.43/2.62 (assume @p154 (forall @t138 (= (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t191) @t183))) % 2.43/2.62 (assume @p155 (forall @t138 (= @t204 @t137))) % 2.43/2.62 (assume @p156 (forall @t138 (=> @t137 @t204))) % 2.43/2.62 (assume @p157 (forall @t119 (< @t117 @t187))) % 2.43/2.62 (assume @p158 (forall @t119 (= (|tptp.'fun_app$l'| @t190 @t14) @t62))) % 2.43/2.62 (assume @p159 (forall @t78 (= (|tptp.'fun_app$i'| @t205 @t14) @t2))) % 2.43/2.62 (assume @p160 (forall @t81 (= (|tptp.'fun_app$h'| @t206 @t14) @t6))) % 2.43/2.62 (assume @p161 (forall @t78 (= (|tptp.'powr$'| 0/1 @t2) 0/1))) % 2.43/2.62 (assume @p162 (forall @t4 (= (= @t207 0/1) @t76))) % 2.43/2.62 (assume @p163 (forall @t78 (= (|tptp.'powr$'| 1/1 @t2) 1/1))) % 2.43/2.62 (assume @p164 (forall @t198 (=> @t211 (= (= @t191 @t209) @t208)))) % 2.43/2.62 (assume @p165 (forall @t215 (=> @t214 (= (= @t213 @t212) @t208)))) % 2.43/2.62 (assume @p166 (forall @t219 (=> @t218 (= (= @t217 @t216) @t208)))) % 2.43/2.62 (assume @p167 (forall @t119 (= (|tptp.'fun_app$l'| @t221 @t220) |tptp.'zero$k'|))) % 2.43/2.62 (assume @p168 (forall @t119 (= (|tptp.'fun_app$i'| @t222 @t220) 0/1))) % 2.43/2.62 (assume @p169 (forall @t119 (= (|tptp.'fun_app$h'| @t223 @t220) 0))) % 2.43/2.62 (assume @p170 (forall @t119 (= (|tptp.'fun_app$l'| @t190 @t193) @t62))) % 2.43/2.62 (assume @p171 (forall @t78 (= (|tptp.'fun_app$i'| @t205 @t193) @t2))) % 2.43/2.62 (assume @p172 (forall @t81 (= (|tptp.'fun_app$h'| @t206 @t193) @t6))) % 2.43/2.62 (assume @p173 (forall @t119 (= (< @t117 @t189) @t118))) % 2.43/2.62 (assume @p174 (forall @t119 (< 0 @t187))) % 2.43/2.62 (assume @p175 (forall @t198 (=> @t211 (= @t225 @t224)))) % 2.43/2.62 (assume @p176 (forall @t215 (=> @t214 (= @t226 @t224)))) % 2.43/2.62 (assume @p177 (forall @t219 (=> @t218 (= @t227 @t224)))) % 2.43/2.62 (assume @p178 (forall @t138 (= @t229 (and @t228 @t174)))) % 2.43/2.62 (assume @p179 (forall @t231 (= @t230 (and @t76 @t174)))) % 2.43/2.62 (assume @p180 (forall @t233 (= @t232 (and @t79 @t174)))) % 2.43/2.62 (assume @p181 (forall @t198 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t180) @t202) @t234))) % 2.43/2.62 (assume @p182 (forall @t198 (= (< @t182 @t144) @t234))) % 2.43/2.62 (assume @p183 (forall @t198 (= (< @t183 @t203) @t234))) % 2.43/2.62 (assume @p184 (forall @t198 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t179) @t197) @t235))) % 2.43/2.62 (assume @p185 (forall @t198 (= (< @t117 @t199) @t235))) % 2.43/2.62 (assume @p186 (forall @t198 (= (< @t165 @t200) @t235))) % 2.43/2.62 (assume @p187 (forall @t198 (=> @t239 (= @t225 @t236)))) % 2.43/2.62 (assume @p188 (forall @t215 (=> @t240 (= @t226 @t236)))) % 2.43/2.62 (assume @p189 (forall @t219 (=> @t242 (= @t227 @t236)))) % 2.43/2.62 (assume @p190 (forall @t246 (=> (and @t245 @t244) (exists @t175 (and (not @t140) (|tptp.'fun_app$b'| @t139 @t243)))))) % 2.43/2.62 (assume @p191 (forall @t138 (=> @t211 (|tptp.'fun_app$b'| @t210 @t247)))) % 2.43/2.62 (assume @p192 (forall @t233 (=> @t214 (< 1 @t248)))) % 2.43/2.62 (assume @p193 (forall @t231 (=> @t218 (< 1/1 @t249)))) % 2.43/2.62 (assume @p194 (forall @t138 (=> (< @t189 @t117) (< @t127 @t192)))) % 2.43/2.62 (assume @p195 (forall @t138 (=> (not @t228) (not @t229)))) % 2.43/2.62 (assume @p196 (forall @t231 (=> @t185 (not @t230)))) % 2.43/2.62 (assume @p197 (forall @t233 (=> (not @t79) (not @t232)))) % 2.43/2.62 (assume @p198 (forall @t119 (not (= @t117 @t187)))) % 2.43/2.62 (assume @p199 (forall @t138 (=> @t188 @t157))) % 2.43/2.62 (assume @p200 (= @t115 false)) % 2.43/2.62 (assume @p201 (forall @t138 (=> @t239 (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t247) |tptp.'one$e'|)))) % 2.43/2.62 (assume @p202 (forall @t233 (=> @t240 (< @t248 1)))) % 2.43/2.62 (assume @p203 (forall @t231 (=> @t242 (< @t249 1/1)))) % 2.43/2.62 (assume @p204 (forall @t119 (not @t250))) % 2.43/2.62 (assume @p205 (forall @t119 (not @t251))) % 2.43/2.62 (assume @p206 (forall @t138 (=> @t252 @t131))) % 2.43/2.62 (assume @p207 (forall @t119 (=> (and @t135 (forall @t175 @t253)) false))) % 2.43/2.62 (assume @p208 (forall @t154 (=> (and @t153 (forall @t152 (=> @t149 @t256))) @t140))) % 2.43/2.62 (assume @p209 (forall (@list @t257 @t17 @t61) (=> (and (forall @t147 (|tptp.'fun_app$b'| @t262 @t75)) (forall @t147 (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| @t257 @t75) @t261)) (forall @t263 (=> (|tptp.'fun_app$b'| @t262 @t258) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| @t257 @t261) (|tptp.'nat$'| (+ @t259 1)))))) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| @t257 @t17) @t61)))) % 2.43/2.62 (assume @p210 (forall @t154 (=> (and @t140 (forall @t152 (=> @t256 @t149))) @t153))) % 2.43/2.62 (assume @p211 (forall @t119 (=> @t251 false))) % 2.43/2.62 (assume @p212 (forall @t119 (=> @t250 false))) % 2.43/2.62 (assume @p213 (forall @t119 (=> @t131 @t264))) % 2.43/2.62 (assume @p214 (forall @t138 (=> @t266 (= @t265 @t157)))) % 2.43/2.62 (assume @p215 (forall @t272 (=> (and @t137 (forall @t147 (=> (= @t127 @t260) @t269)) (forall @t147 (=> (and @t271 @t270) @t269))) @t268))) % 2.43/2.62 (assume @p216 (forall @t283 (=> (and @t137 @t282 (forall @t281 (=> (and @t280 (< @t259 (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t275)) @t279 @t278) @t277))) @t274))) % 2.43/2.62 (assume @p217 (forall @t198 (=> (and @t137 @t224) (< @t187 @t144)))) % 2.43/2.62 (assume @p218 (forall @t138 (=> @t204 @t137))) % 2.43/2.62 (assume @p219 (forall @t138 (=> (and @t266 @t265) @t160))) % 2.43/2.62 (assume @p220 (forall @t138 (= @t286 (exists @t152 (and @t285 @t284))))) % 2.43/2.62 (assume @p221 (forall @t293 (= @t292 (and @t290 (forall @t152 (=> @t289 @t288)))))) % 2.43/2.62 (assume @p222 (forall @t138 (= @t266 @t294))) % 2.43/2.62 (assume @p223 (forall @t138 (= @t265 @t295))) % 2.43/2.62 (assume @p224 (forall @t293 (= @t296 (or @t290 (exists @t152 (and @t289 @t288)))))) % 2.43/2.62 (assume @p225 (forall @t138 (=> @t137 @t265))) % 2.43/2.62 (assume @p226 (forall @t138 (=> (and @t265 @t156 (=> @t157 false)) false))) % 2.43/2.62 (assume @p227 (forall @t138 (=> (and @t137 (not (= @t187 @t127))) @t286))) % 2.43/2.62 (assume @p228 (forall @t138 (=> (and @t286 @t297) false))) % 2.43/2.62 (assume @p229 (forall @t138 (=> @t286 @t137))) % 2.43/2.62 (assume @p230 (forall @t138 (=> (and @t137 (=> (= @t127 @t187) false) @t297) false))) % 2.43/2.62 (assume @p231 (forall @t138 (=> @t238 (|tptp.'fun_app$b'| @t181 @t191)))) % 2.43/2.62 (assume @p232 (forall @t233 (=> @t176 (< 0 @t213)))) % 2.43/2.62 (assume @p233 (forall @t231 (=> @t124 (< 0/1 @t217)))) % 2.43/2.62 (assume @p234 (forall @t119 (= (|tptp.'fun_app$l'| @t190 @t75) |tptp.'one$e'|))) % 2.43/2.62 (assume @p235 (forall @t78 (= (|tptp.'fun_app$i'| @t205 @t75) 1/1))) % 2.43/2.62 (assume @p236 (forall @t81 (= (|tptp.'fun_app$h'| @t206 @t75) 1))) % 2.43/2.62 (assume @p237 (forall @t198 (=> (and @t130 (< @t192 (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t209))) @t224))) % 2.43/2.62 (assume @p238 (forall @t129 (=> @t298 @t128))) % 2.43/2.62 (assume @p239 (forall @t119 (and (=> @t118 (= @t299 |tptp.'one$e'|)) (=> @t131 @t300)))) % 2.43/2.62 (assume @p240 (forall @t119 (and (=> @t118 (= @t301 1/1)) (=> @t131 @t302)))) % 2.43/2.62 (assume @p241 (forall @t119 (and (=> @t118 (= @t303 1)) (=> @t131 @t304)))) % 2.43/2.62 (assume @p242 (forall @t198 (=> (and @t211 @t225) @t224))) % 2.43/2.62 (assume @p243 (forall @t215 (=> (and @t214 @t226) @t224))) % 2.43/2.62 (assume @p244 (forall @t219 (=> (and @t218 @t227) @t224))) % 2.43/2.62 (assume @p245 (forall @t198 (=> (and @t137 (|tptp.'fun_app$b'| @t210 @t61)) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t307) @t306)))) % 2.43/2.62 (assume @p246 (forall @t312 (=> (and @t137 (< 1 @t308)) (< @t311 @t310)))) % 2.43/2.62 (assume @p247 (forall @t317 (=> (and @t137 @t316) (< @t315 @t314)))) % 2.43/2.62 (assume @p248 (forall @t119 (=> @t130 @t300))) % 2.43/2.62 (assume @p249 (forall @t119 (=> @t130 @t302))) % 2.43/2.62 (assume @p250 (forall @t119 (=> @t130 @t304))) % 2.43/2.62 (assume @p251 (forall @t119 (not (= @t318 0)))) % 2.43/2.62 (assume @p252 (forall @t119 (not (= (|tptp.'fun_app$i'| |tptp.'of_nat$a'| @t220) 0/1)))) % 2.43/2.62 (assume @p253 (forall @t326 (=> (and @t325 @t224) @t322))) % 2.43/2.62 (assume @p254 (forall @t334 (=> (and @t333 @t224) @t330))) % 2.43/2.62 (assume @p255 (forall @t342 (=> (and @t341 @t224) @t338))) % 2.43/2.62 (assume @p256 (forall @t326 (=> @t325 (= @t322 @t224)))) % 2.43/2.62 (assume @p257 (forall @t334 (=> @t333 (= @t330 @t224)))) % 2.43/2.62 (assume @p258 (forall @t342 (=> @t341 (= @t338 @t224)))) % 2.43/2.62 (assume @p259 (forall @t293 (= @t296 (or @t344 (exists @t152 (and @t289 @t343)))))) % 2.43/2.62 (assume @p260 (forall @t119 (= @t130 @t264))) % 2.43/2.62 (assume @p261 (forall @t293 (= @t292 (and @t344 (forall @t152 (=> @t289 @t343)))))) % 2.43/2.62 (assume @p262 (forall @t119 (=> @t130 @t264))) % 2.43/2.62 (assume @p263 (forall @t138 (= @t265 (or @t118 (exists @t152 (and (= @t117 @t254) @t236)))))) % 2.43/2.62 (assume @p264 (= 1 @t189)) % 2.43/2.62 (assume @p265 (forall @t129 (=> (and @t128 (= (|tptp.'fun_app$e'| @t126 @t345) |tptp.'zero$c'|)) @t298))) % 2.43/2.62 (assume @p266 (forall @t129 (=> (and (not @t298) (forall @t53 (= (|tptp.'fun_app$e'| (|tptp.'vec_nth$'| @t103) @t345) |tptp.'zero$c'|))) (not @t128)))) % 2.43/2.62 (assume @p267 (= @t346 |tptp.'zero$'|)) % 2.43/2.62 (assume @p268 (= (|tptp.'from_nat$a'| @t75) |tptp.'zero$a'|)) % 2.43/2.62 (assume @p269 (forall @t198 (=> (and @t137 (|tptp.'fun_app$b'| @t181 @t61) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t61) |tptp.'one$e'|)) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t306) @t307)))) % 2.43/2.62 (assume @p270 (forall @t312 (=> (and @t137 (< 0 @t308) (< @t308 1)) (< @t310 @t311)))) % 2.43/2.62 (assume @p271 (forall @t317 (=> (and @t137 @t121 (< @t120 1/1)) (< @t314 @t315)))) % 2.43/2.62 (assume @p272 (forall @t138 (=> (and @t211 @t174) (|tptp.'fun_app$b'| @t210 @t191)))) % 2.43/2.62 (assume @p273 (forall @t233 (=> (and @t214 @t174) (< 1 @t213)))) % 2.43/2.62 (assume @p274 (forall @t231 (=> (and @t218 @t174) (< 1/1 @t217)))) % 2.43/2.62 (assume @p275 (forall @t293 (=> (and @t130 (|tptp.'fun_app$b'| @t287 @t14) (forall @t152 (=> (and @t151 @t288) @t343))) @t290))) % 2.43/2.62 (assume @p276 (forall @t326 (=> (and @t347 @t224) (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t320) @t321)))) % 2.43/2.62 (assume @p277 (forall @t326 (=> @t347 (= @t322 @t236)))) % 2.43/2.62 (assume @p278 (forall @t350 (=> @t349 (exists @t122 (and @t121 @t348))))) % 2.43/2.62 (assume @p279 (forall @t350 (=> @t349 (exists @t122 (and @t121 @t348 (forall @t352 (=> (and (< 0/1 @t351) (= (|tptp.'fun_app$i'| (|tptp.'power$b'| @t351) @t62) @t1)) (= @t351 @t120)))))))) % 2.43/2.62 (assume @p280 (forall @t356 (=> @t218 (= @t355 @t353)))) % 2.43/2.62 (assume @p281 (forall @t4 (=> @t125 (= (= @t358 @t357) @t90)))) % 2.43/2.62 (assume @p282 (forall @t78 (=> @t124 (= (= @t358 0/1) @t91)))) % 2.43/2.62 (assume @p283 (forall @t78 (=> @t124 (= @t359 @t218)))) % 2.43/2.62 (assume @p284 (forall @t78 (=> @t124 (= @t360 @t241)))) % 2.43/2.62 (assume @p285 (forall @t4 (=> @t125 (= (< @t358 @t357) @t3)))) % 2.43/2.62 (assume @p286 (forall @t4 (=> @t218 (= (= @t207 1/1) (= @t1 0/1))))) % 2.43/2.62 (assume @p287 (forall @t4 (= (< 0/1 @t207) @t185))) % 2.43/2.62 (assume @p288 (forall @t78 (=> @t218 @t359))) % 2.43/2.62 (assume @p289 (forall @t78 (=> @t124 (< @t358 @t2)))) % 2.43/2.62 (assume @p290 (forall @t78 (=> @t242 @t360))) % 2.43/2.62 (assume @p291 (forall @t231 (=> @t124 (= (|tptp.'powr$'| @t2 @t166) @t217)))) % 2.43/2.62 (assume @p292 (forall @t78 (=> (and @t359 @t124) @t218))) % 2.43/2.62 (assume @p293 (forall @t356 (=> (and @t363 @t123 @t353) (< @t362 @t361)))) % 2.43/2.62 (assume @p294 (forall @t356 (=> (and @t355 @t218) @t353))) % 2.43/2.62 (assume @p295 (forall @t356 (=> (and @t3 @t316) (< @t362 @t364)))) % 2.43/2.62 (assume @p296 (forall @t4 (not (< @t207 0/1)))) % 2.43/2.62 (assume @p297 (forall @t4 (=> (and @t218 @t123) (< 1/1 @t207)))) % 2.43/2.62 (assume @p298 (forall @t356 (=> (and @t124 (not @t91)) (= (= @t207 @t354) (= @t1 @t120))))) % 2.43/2.62 (assume @p299 (forall @t4 (=> (and @t124 (< @t1 1/1)) (exists @t152 (< @t365 @t2))))) % 2.43/2.62 (assume @p300 (forall @t4 (=> @t218 (exists @t152 (< @t1 @t216))))) % 2.43/2.62 (assume @p301 (forall @t164 (= @t368 (or @t367 @t366)))) % 2.43/2.62 (assume @p302 (forall (@list @t369 @t29 @t27) (=> (and (forall @t373 (=> (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less$'| @t370) @t47) @t372)) (forall @t53 (|tptp.'fun_app$c'| @t371 @t47)) (forall @t373 (=> (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t369 @t370) @t47) @t372))) (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| @t369 @t29) @t27)))) % 2.43/2.62 (assume @p303 (forall @t375 (=> (and @t163 (= @t37 @t27)) @t374))) % 2.43/2.62 (assume @p304 (forall @t375 (=> (and @t377 @t374) @t376))) % 2.43/2.62 (assume @p305 (forall @t164 (=> @t163 (= @t378 true)))) % 2.43/2.62 (assume @p306 (forall @t164 (=> @t163 (= @t377 false)))) % 2.43/2.62 (assume @p307 (forall (@list @t379) (= (exists @t34 @t381) (exists @t34 (and @t381 (forall @t32 (=> @t31 (not @t380)))))))) % 2.43/2.62 (assume @p308 (forall @t164 (=> @t163 (= @t366 false)))) % 2.43/2.62 (assume @p309 (forall @t164 (=> (and @t383 (=> @t366 false) @t382) false))) % 2.43/2.62 (assume @p310 (forall (@list @t37 @t29 @t384) (=> @t163 (= (=> @t367 (= @t384 tptp.tltrue)) true)))) % 2.43/2.62 (assume @p311 (forall @t164 (=> @t368 (= @t378 @t377)))) % 2.43/2.62 (assume @p312 (forall @t164 (=> @t163 @t378))) % 2.43/2.62 (assume @p313 (forall @t164 (=> @t163 @t385))) % 2.43/2.62 (assume @p314 (forall @t164 (or @t163 @t366 @t367))) % 2.43/2.62 (assume @p315 (forall @t38 (not @t386))) % 2.43/2.62 (assume @p316 (forall (@list @t379 @t29) (=> (forall @t32 (=> (forall @t53 (=> @t51 (|tptp.'fun_app$c'| @t379 @t47))) @t380)) @t381))) % 2.43/2.62 (assume @p317 (forall @t375 (=> (and @t163 @t376) @t374))) % 2.43/2.62 (assume @p318 (forall @t164 (=> (and @t163 @t367) false))) % 2.43/2.62 (assume @p319 (forall @t164 (= @t387 (or @t367 @t163)))) % 2.43/2.62 (assume @p320 (forall @t164 (=> (and @t387 @t382 @t383) false))) % 2.43/2.62 (assume @p321 (forall @t38 (= @t386 false))) % 2.43/2.62 (assume @p322 (forall @t81 (= (< @t6 @t6) false))) % 2.43/2.62 (assume @p323 (forall @t78 (= (< @t2 @t2) false))) % 2.43/2.62 (assume @p324 (forall @t231 (=> @t124 (exists @t122 (and @t121 (= (|tptp.'fun_app$i'| @t313 @t243) @t2)))))) % 2.43/2.62 (assume @p325 (forall (@list @t95 @t17 @t61) (and (=> @t96 (and (=> @t96 (= @t127 @t127)) (=> @t97 @t208))) (=> @t97 (and (=> @t96 (= @t144 @t127)) (=> @t97 (= @t144 @t144))))))) % 2.43/2.62 (assume @p326 (forall @t81 (= (< @t189 @t389) @t214))) % 2.43/2.62 (assume @p327 (forall @t81 (=> (and @t393 @t392) false))) % 2.43/2.62 (assume @p328 (forall @t198 (=> (and (|tptp.'fun_app$b'| @t237 @t17) @t395 @t151) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less$a'| @t209) @t194)))) % 2.43/2.62 (assume @p329 (forall @t398 (=> (and @t7 @t397 @t151) (< @t212 @t396)))) % 2.43/2.62 (assume @p330 (forall @t400 (=> (and @t3 @t399 @t151) (< @t216 @t365)))) % 2.43/2.62 (assume @p331 (forall @t8 (= (= @t402 @t401) @t88))) % 2.43/2.62 (assume @p332 (forall @t81 (= (- @t402) @t6))) % 2.43/2.62 (assume @p333 (forall @t119 @t403)) % 2.43/2.62 (assume @p334 (forall @t138 (= (<= @t187 @t186) @t404))) % 2.43/2.62 (assume @p335 (forall @t8 (= (<= @t402 @t401) (<= @t5 @t6)))) % 2.43/2.62 (assume @p336 (forall @t4 (= (<= @t406 @t405) (<= @t1 @t2)))) % 2.43/2.62 (assume @p337 (= 0/1 0/1)) % 2.43/2.62 (assume @p338 (= (|tptp.'uminus$'| |tptp.'zero$'|) |tptp.'zero$'|)) % 2.43/2.62 (assume @p339 (= (|tptp.'uminus$a'| |tptp.'zero$a'|) |tptp.'zero$a'|)) % 2.43/2.62 (assume @p340 (forall @t78 (= (= 0/1 @t406) @t77))) % 2.43/2.62 (assume @p341 (forall @t38 (= (= |tptp.'zero$'| @t407) @t83))) % 2.43/2.62 (assume @p342 (forall @t74 (= (= |tptp.'zero$a'| @t408) @t85))) % 2.43/2.62 (assume @p343 (forall @t81 (= (= 0 @t402) @t80))) % 2.43/2.62 (assume @p344 (forall @t78 (= (= @t406 0/1) @t76))) % 2.43/2.62 (assume @p345 (forall @t38 (= (= @t407 |tptp.'zero$'|) @t82))) % 2.43/2.62 (assume @p346 (forall @t74 (= (= @t408 |tptp.'zero$a'|) @t84))) % 2.43/2.62 (assume @p347 (forall @t81 (= (= @t402 0) @t79))) % 2.43/2.62 (assume @p348 (forall @t78 (= (= @t2 @t406) @t76))) % 2.43/2.62 (assume @p349 (forall @t81 (= (= @t6 @t402) @t79))) % 2.43/2.62 (assume @p350 (forall @t78 (= (= @t406 @t2) @t76))) % 2.43/2.62 (assume @p351 (forall @t81 (= (= @t402 @t6) @t79))) % 2.43/2.62 (assume @p352 (forall @t4 (= (< @t406 @t405) @t89))) % 2.43/2.62 (assume @p353 (forall @t8 (= (< @t402 @t401) @t87))) % 2.43/2.62 (assume @p354 (forall @t138 (= @t404 @t404))) % 2.43/2.62 (assume @p355 (forall @t138 (= @t409 @t404))) % 2.43/2.62 (assume @p356 (forall @t4 (= (<= @t207 0/1) @t76))) % 2.43/2.62 (assume @p357 (forall @t138 (<= @t410 @t127))) % 2.43/2.62 (assume @p358 (forall @t119 (= @t117 @t117))) % 2.43/2.62 (assume @p359 (forall @t81 (= (<= 0 @t402) @t411))) % 2.43/2.62 (assume @p360 (forall @t78 (= (<= 0/1 @t406) @t412))) % 2.43/2.62 (assume @p361 (forall @t81 (= (<= @t402 0) @t397))) % 2.43/2.62 (assume @p362 (forall @t78 (= (<= @t406 0/1) @t399))) % 2.43/2.62 (assume @p363 (forall @t81 (= (<= @t6 @t402) @t411))) % 2.43/2.62 (assume @p364 (forall @t78 (= (<= @t2 @t406) @t412))) % 2.43/2.62 (assume @p365 (forall @t81 (= (<= @t402 @t6) @t397))) % 2.43/2.62 (assume @p366 (forall @t78 (= (<= @t406 @t2) @t399))) % 2.43/2.62 (assume @p367 (forall @t78 (= (< @t2 @t406) @t363))) % 2.43/2.62 (assume @p368 (forall @t81 (= (< @t6 @t402) @t393))) % 2.43/2.62 (assume @p369 (forall @t78 (= (< @t406 @t2) @t124))) % 2.43/2.62 (assume @p370 (forall @t81 (= (< @t402 @t6) @t176))) % 2.43/2.62 (assume @p371 (forall @t78 (= (< 0/1 @t406) @t363))) % 2.43/2.62 (assume @p372 (forall @t81 (= (< 0 @t402) @t393))) % 2.43/2.62 (assume @p373 (forall @t78 (= (< @t406 0/1) @t124))) % 2.43/2.62 (assume @p374 (forall @t81 (= (< @t402 0) @t176))) % 2.43/2.62 (assume @p375 (forall @t81 (=> @t411 @t413))) % 2.43/2.62 (assume @p376 (forall @t81 (= @t413 @t411))) % 2.43/2.62 (assume @p377 (forall @t138 (= (= @t410 @t127) @t414))) % 2.43/2.62 (assume @p378 (forall @t4 (=> @t125 (= (<= @t358 @t357) @t415)))) % 2.43/2.62 (assume @p379 (forall @t78 (=> @t399 @t416))) % 2.43/2.62 (assume @p380 (forall @t78 (= @t416 @t399))) % 2.43/2.62 (assume @p381 (forall @t356 (=> @t218 (= (<= @t207 @t354) @t417)))) % 2.43/2.62 (assume @p382 (forall @t81 (and @t419 (=> @t418 @t413)))) % 2.43/2.62 (assume @p383 (= (|tptp.'dbl_inc$'| @t420) @t420)) % 2.43/2.62 (assume @p384 (= (|tptp.'dbl_inc$a'| @t421) @t421)) % 2.43/2.62 (assume @p385 (forall @t198 (=> @t211 (= @t423 @t422)))) % 2.43/2.62 (assume @p386 (forall @t215 (=> @t214 (= @t424 @t422)))) % 2.43/2.62 (assume @p387 (forall @t219 (=> @t218 (= @t425 @t422)))) % 2.43/2.62 (assume @p388 (forall @t119 (= @t426 @t118))) % 2.43/2.62 (assume @p389 (forall @t119 (= (<= @t165 0/1) @t118))) % 2.43/2.62 (assume @p390 (forall @t198 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t179) @t197) @t427))) % 2.43/2.62 (assume @p391 (forall @t198 (= (<= @t117 @t199) @t427))) % 2.43/2.62 (assume @p392 (forall @t198 (= (<= @t165 @t200) @t427))) % 2.43/2.62 (assume @p393 (forall @t198 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t180) @t202) @t428))) % 2.43/2.62 (assume @p394 (forall @t198 (= (<= @t182 @t144) @t428))) % 2.43/2.62 (assume @p395 (forall @t198 (= (<= @t183 @t203) @t428))) % 2.43/2.62 (assume @p396 (= @t171 @t189)) % 2.43/2.62 (assume @p397 (forall @t78 (=> @t124 (= (<= @t358 0/1) @t429)))) % 2.43/2.62 (assume @p398 (forall @t78 (=> @t124 (= @t431 @t430)))) % 2.43/2.62 (assume @p399 (forall @t8 (= @t434 (and (< 0 @t5) @t7)))) % 2.43/2.62 (assume @p400 (forall @t138 (< @t435 @t127))) % 2.43/2.62 (assume @p401 (forall @t119 (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'nat$'| @t410)) 0))) % 2.43/2.62 (assume @p402 (forall @t198 (=> @t239 (= @t423 @t436)))) % 2.43/2.62 (assume @p403 (forall @t215 (=> @t240 (= @t424 @t436)))) % 2.43/2.62 (assume @p404 (forall @t219 (=> @t242 (= @t425 @t436)))) % 2.43/2.62 (assume @p405 (forall @t198 (=> (and @t395 (|tptp.'fun_app$b'| @t394 @t17) @t151) (= @t438 @t437)))) % 2.43/2.62 (assume @p406 (forall @t398 (=> (and @t397 @t441 @t151) (= @t440 @t439)))) % 2.43/2.62 (assume @p407 (forall @t400 (=> (and @t399 @t443 @t151) (= @t442 @t415)))) % 2.43/2.62 (assume @p408 (forall @t81 (= (< 0 @t389) @t176))) % 2.43/2.62 (assume @p409 (forall @t233 (=> @t397 (= (<= @t127 @t389) (<= @t127 @t6))))) % 2.43/2.62 (assume @p410 (forall @t78 (=> @t430 @t431))) % 2.43/2.62 (assume @p411 (forall @t164 (=> @t445 @t444))) % 2.43/2.62 (assume @p412 (forall @t164 (=> @t446 @t367))) % 2.43/2.62 (assume @p413 (forall @t164 (= @t163 (and @t445 (not @t447))))) % 2.43/2.62 (assume @p414 (forall @t164 (or @t445 @t367))) % 2.43/2.62 (assume @p415 (forall @t375 (=> (and @t163 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$a'| @t27) @t37)) @t374))) % 2.43/2.62 (assume @p416 (forall @t375 (=> (and @t445 @t376) @t374))) % 2.43/2.62 (assume @p417 (forall @t164 (=> @t445 (= @t368 @t366)))) % 2.43/2.62 (assume @p418 (forall @t164 (=> @t368 (= @t445 @t366)))) % 2.43/2.62 (assume @p419 (forall @t164 (=> (and @t387 @t447) @t367))) % 2.43/2.62 (assume @p420 (forall @t164 (=> @t448 @t163))) % 2.43/2.62 (assume @p421 (forall @t164 (=> @t163 @t445))) % 2.43/2.62 (assume @p422 (forall @t164 (= @t368 @t447))) % 2.43/2.62 (assume @p423 (forall @t164 (= @t368 (or @t446 @t366)))) % 2.43/2.62 (assume @p424 (forall @t164 (= @t163 @t448))) % 2.43/2.62 (assume @p425 (forall @t164 (= @t445 @t444))) % 2.43/2.62 (assume @p426 (forall @t164 (= @t446 @t367))) % 2.43/2.62 (assume @p427 (forall @t164 (=> @t368 @t447))) % 2.43/2.62 (assume @p428 (forall @t164 (=> @t445 @t378))) % 2.43/2.62 (assume @p429 (forall @t8 (= (not @t439) @t87))) % 2.43/2.62 (assume @p430 (forall @t4 (= (not @t415) @t89))) % 2.43/2.62 (assume @p431 (forall @t4 (=> @t3 (< @t405 @t406)))) % 2.43/2.62 (assume @p432 (forall @t8 (=> @t7 (< @t401 @t402)))) % 2.43/2.62 (assume @p433 (forall @t4 (= @t415 (or @t3 @t90)))) % 2.43/2.62 (assume @p434 (forall @t4 (=> (and @t430 @t443) (<= 1/1 @t207)))) % 2.43/2.62 (assume @p435 (forall (@list @t2 @t1 @t120 @t351) (=> (and @t399 @t415 @t449 (<= @t120 @t351)) (<= @t362 (|tptp.'powr$'| @t351 @t1))))) % 2.43/2.62 (assume @p436 (forall @t4 (<= 0/1 @t207))) % 2.43/2.62 (assume @p437 (forall @t356 (=> (and @t399 @t443 @t417) (<= @t361 @t362)))) % 2.43/2.62 (assume @p438 (forall @t356 (=> (and @t415 @t449) (<= @t362 @t364)))) % 2.43/2.62 (assume @p439 (forall @t4 (=> (and @t399 @t443 (<= @t1 1/1)) (<= @t361 1/1)))) % 2.43/2.62 (assume @p440 (forall @t8 (=> (and @t397 @t441) (= (= @t389 @t433) @t88)))) % 2.43/2.62 (assume @p441 (forall @t8 (=> (or @t176 @t441) (= @t450 @t439)))) % 2.43/2.62 (assume @p442 (forall @t233 (=> @t397 (= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'nat$'| @t213)) (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| (|tptp.'power$'| @t388) @t17)))))) % 2.43/2.62 (assume @p443 (forall @t246 (= (forall @t175 @t140) (forall @t452 (=> @t441 @t451))))) % 2.43/2.62 (assume @p444 (forall @t246 (= @t244 (exists @t452 (and @t441 @t451))))) % 2.43/2.62 (assume @p445 (<= @t421 1)) % 2.43/2.62 (assume @p446 (<= @t420 1/1)) % 2.43/2.62 (assume @p447 (not (<= 1 @t421))) % 2.43/2.62 (assume @p448 (not (<= 1/1 @t420))) % 2.43/2.62 (assume @p449 (<= @t421 0)) % 2.43/2.62 (assume @p450 (<= @t420 0/1)) % 2.43/2.62 (assume @p451 (not (<= 0 @t421))) % 2.43/2.62 (assume @p452 (not (<= 0/1 @t420))) % 2.43/2.62 (assume @p453 (forall @t454 (= (= @t117 @t5) (and @t453 @t441)))) % 2.43/2.62 (assume @p454 (forall @t81 @t419)) % 2.43/2.62 (assume @p455 (forall @t198 (=> (and @t404 (|tptp.'fun_app$b'| @t455 @t61)) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t307) @t306)))) % 2.43/2.62 (assume @p456 (forall @t312 (=> (and @t404 (<= 1 @t308)) (<= @t311 @t310)))) % 2.43/2.62 (assume @p457 (forall @t317 (=> (and @t404 @t449) (<= @t315 @t314)))) % 2.43/2.62 (assume @p458 (forall @t138 (= (<= @t117 @t390) @t414))) % 2.43/2.62 (assume @p459 (forall @t81 (=> (and @t411 @t456) false))) % 2.43/2.62 (assume @p460 (forall @t119 (<= @t410 0))) % 2.43/2.62 (assume @p461 (forall @t4 (= (< @t406 @t1) (< @t405 @t2)))) % 2.43/2.62 (assume @p462 (forall @t8 (= (< @t402 @t5) (< @t401 @t6)))) % 2.43/2.62 (assume @p463 (forall @t4 (= (< @t2 @t405) (< @t1 @t406)))) % 2.43/2.62 (assume @p464 (forall @t8 (= (< @t6 @t401) (< @t5 @t402)))) % 2.43/2.62 (assume @p465 (not (= 1/1 @t420))) % 2.43/2.62 (assume @p466 (not (= 1 @t421))) % 2.43/2.62 (assume @p467 (forall @t38 (|tptp.'fun_app$c'| (|tptp.'fun_app$d'| |tptp.'less_eq$a'| |tptp.'zero$'|) @t37))) % 2.43/2.62 (assume @p468 (forall @t74 (|tptp.'less_eq$b'| |tptp.'zero$a'| @t73))) % 2.43/2.62 (assume @p469 @t457) % 2.43/2.62 (assume @p470 (<= 0/1 0/1)) % 2.43/2.62 (assume @p471 (<= 1 1)) % 2.43/2.62 (assume @p472 (<= 1/1 1/1)) % 2.43/2.62 (assume @p473 (forall @t119 (=> @t426 @t118))) % 2.43/2.62 (assume @p474 (forall @t119 (= @t403 true))) % 2.43/2.62 (assume @p475 (forall @t78 (exists @t175 (<= @t2 @t166)))) % 2.43/2.62 (assume @p476 (forall @t138 (=> @t458 @t404))) % 2.43/2.62 (assume @p477 (forall @t138 (=> (and @t459 (=> @t404 false) @t253) false))) % 2.43/2.62 (assume @p478 (forall @t138 (=> @t404 @t459))) % 2.43/2.62 (assume @p479 (forall @t138 (=> @t458 (exists @t152 @t285)))) % 2.43/2.62 (assume @p480 (forall @t138 (= @t459 (or @t404 @t252)))) % 2.43/2.62 (assume @p481 (forall @t119 (not (<= @t187 @t117)))) % 2.43/2.62 (assume @p482 (forall @t138 (= (not @t404) (<= @t186 @t117)))) % 2.43/2.62 (assume @p483 (forall @t154 (=> (forall @t152 (=> (forall @t147 (=> (<= @t260 @t144) @t142)) @t149)) @t140))) % 2.43/2.62 (assume @p484 (forall @t272 (=> (and @t404 @t268 (forall @t147 (=> (and @t461 @t269) @t270))) @t460))) % 2.43/2.62 (assume @p485 (forall @t283 (=> (and @t404 (forall @t147 (|tptp.'fun_app$b'| @t276 @t141)) (forall @t281 (=> (and @t279 @t278) @t277)) @t282) @t274))) % 2.43/2.62 (assume @p486 (forall @t81 (=> (and @t462 @t456) false))) % 2.43/2.62 (assume @p487 (forall @t138 (= @t137 @t463))) % 2.43/2.62 (assume @p488 (forall @t138 (=> @t137 @t404))) % 2.43/2.62 (assume @p489 (forall @t138 (= @t404 @t295))) % 2.43/2.62 (assume @p490 (forall @t138 (=> @t295 @t404))) % 2.43/2.62 (assume @p491 (forall @t138 (=> @t463 @t137))) % 2.43/2.62 (assume @p492 (forall (@list @t464 @t17 @t61) (=> (and (forall @t263 (=> @t280 (< (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| @t464 @t141)) (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| @t464 @t258))))) @t422) (<= (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| @t464 @t17)) (|tptp.'fun_app$h'| |tptp.'of_nat$'| (|tptp.'fun_app$l'| @t464 @t61)))))) % 2.43/2.62 (assume @p493 (= @t457 true)) % 2.43/2.62 (assume @p494 (forall @t8 (=> @t439 (<= @t401 @t402)))) % 2.43/2.62 (assume @p495 (forall @t4 (=> @t415 (<= @t405 @t406)))) % 2.43/2.62 (assume @p496 (forall @t8 (= (<= @t402 @t5) (<= @t401 @t6)))) % 2.43/2.62 (assume @p497 (forall @t4 (= (<= @t406 @t1) (<= @t405 @t2)))) % 2.43/2.62 (assume @p498 (forall @t8 (= (<= @t6 @t401) (<= @t5 @t402)))) % 2.43/2.62 (assume @p499 (forall @t4 (= (<= @t2 @t405) (<= @t1 @t406)))) % 2.43/2.62 (assume @p500 (forall @t8 (= (= @t402 @t5) (= @t401 @t6)))) % 2.43/2.62 (assume @p501 (forall @t8 (= (= @t6 @t401) (= @t5 @t402)))) % 2.43/2.62 (assume @p502 (forall @t334 (=> (and (forall @t147 (<= @t332 @t331)) @t422) (<= @t329 @t328)))) % 2.43/2.62 (assume @p503 (forall @t342 (=> (and (forall @t147 (<= @t340 @t339)) @t422) (<= @t337 @t336)))) % 2.43/2.62 (assume @p504 (forall @t334 (=> (and (forall @t147 (<= @t331 @t332)) @t422) (<= @t328 @t329)))) % 2.43/2.62 (assume @p505 (forall @t342 (=> (and (forall @t147 (<= @t339 @t340)) @t422) (<= @t336 @t337)))) % 2.43/2.62 (assume @p506 (forall @t356 (= (|tptp.'powr$'| @t207 @t120) (|tptp.'powr$'| @t354 @t1)))) % 2.43/2.62 (assume @p507 (forall @t8 (=> @t439 @t450))) % 2.43/2.62 (assume @p508 (forall @t233 (= (<= @t389 @t127) (<= @t6 @t127)))) % 2.43/2.62 (assume @p509 (forall @t138 (=> @t404 @t404))) % 2.43/2.62 (assume @p510 (forall @t138 (=> @t404 @t409))) % 2.43/2.62 (assume @p511 (forall @t233 (= (= @t389 @t127) (and (=> @t397 @t173) (=> @t418 @t136))))) % 2.43/2.62 (assume @p512 (forall @t454 (= @t453 (and (=> @t441 (= @t5 @t117)) (=> (not @t441) @t118))))) % 2.43/2.62 (assume @p513 (forall @t8 (=> @t397 (= @t434 @t7)))) % 2.43/2.62 (assume @p514 (forall @t198 (=> (and @t404 (|tptp.'fun_app$b'| @t394 @t61) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t61) |tptp.'one$e'|)) (|tptp.'fun_app$b'| (|tptp.'fun_app$k'| |tptp.'less_eq$'| @t306) @t307)))) % 2.43/2.62 (assume @p515 (forall @t312 (=> (and @t404 (<= 0 @t308) (<= @t308 1)) (<= @t310 @t311)))) % 2.43/2.62 (assume @p516 (forall @t317 (=> (and @t404 (<= 0/1 @t120) (<= @t120 1/1)) (<= @t314 @t315)))) % 2.43/2.62 (assume @p517 (forall @t198 (=> (and @t211 @t423) @t422))) % 2.43/2.62 (assume @p518 (forall @t215 (=> (and @t214 @t424) @t422))) % 2.43/2.62 (assume @p519 (forall @t219 (=> (and @t218 @t425) @t422))) % 2.43/2.62 (assume @p520 (forall @t119 (not (<= 0 @t435)))) % 2.43/2.62 (assume @p521 (forall @t233 (=> @t397 (= (< @t389 @t127) (< @t6 @t127))))) % 2.43/2.62 (assume @p522 (= 0 @t168)) % 2.43/2.62 (assume @p523 (not (= 0/1 @t420))) % 2.43/2.62 (assume @p524 (not (= 0 @t421))) % 2.43/2.62 (assume @p525 (= 1 @t171)) % 2.43/2.62 (assume @p526 (not (< 1/1 @t420))) % 2.43/2.62 (assume @p527 (not (< 1 @t421))) % 2.43/2.62 (assume @p528 (< @t420 1/1)) % 2.43/2.62 (assume @p529 (< @t421 1)) % 2.43/2.62 (assume @p530 (<= 0 1)) % 2.43/2.62 (assume @p531 (<= 0/1 1/1)) % 2.43/2.62 (assume @p532 (not (<= 1 0))) % 2.43/2.62 (assume @p533 (not (<= 1/1 0/1))) % 2.43/2.62 (assume @p534 (forall @t138 (=> @t395 (|tptp.'fun_app$b'| @t394 @t191)))) % 2.43/2.62 (assume @p535 (forall @t233 (=> @t397 (<= 0 @t213)))) % 2.43/2.62 (assume @p536 (forall @t231 (=> @t399 (<= 0/1 @t217)))) % 2.43/2.62 (assume @p537 (forall @t198 (=> (and @t437 @t395) @t438))) % 2.43/2.62 (assume @p538 (forall @t398 (=> (and @t439 @t397) @t440))) % 2.43/2.62 (assume @p539 (forall @t400 (=> (and @t415 @t399) @t442))) % 2.43/2.62 (assume @p540 (forall @t119 (<= 0/1 @t165))) % 2.43/2.62 (assume @p541 (forall @t138 (=> (|tptp.'fun_app$b'| @t455 @t62) (|tptp.'fun_app$b'| @t455 @t191)))) % 2.43/2.62 (assume @p542 (forall @t233 (=> @t465 (<= 1 @t213)))) % 2.43/2.62 (assume @p543 (forall @t231 (=> @t430 (<= 1/1 @t217)))) % 2.43/2.62 (assume @p544 (forall (@list @t466 @t5) (=> (and (forall @t152 (|tptp.'fun_app$a'| @t466 @t144)) (forall @t152 (|tptp.'fun_app$a'| @t466 (- (|tptp.'fun_app$h'| |tptp.'of_nat$'| @t255))))) (|tptp.'fun_app$a'| @t466 @t5)))) % 2.43/2.62 (assume @p545 (forall @t81 (=> (and @t462 (forall @t175 (=> @t467 false))) false))) % 2.43/2.62 (assume @p546 (forall @t356 (=> (and @t412 @t123 @t417) (<= @t362 @t361)))) % 2.43/2.62 (assume @p547 (forall @t356 (=> (and @t124 @t443 @t353) (< @t361 @t362)))) % 2.43/2.62 (assume @p548 (forall @t78 (=> (and @t431 @t124) @t430))) % 2.43/2.62 (assume @p549 (forall @t78 (=> @t124 (<= @t358 @t2)))) % 2.43/2.62 (assume @p550 (forall @t154 (=> @t468 (exists @t152 (and @t436 (forall @t147 (=> @t146 @t143)) @t149))))) % 2.43/2.62 (assume @p551 (forall @t138 (=> @t137 @t458))) % 2.43/2.62 (assume @p552 (forall @t138 (= @t458 @t137))) % 2.43/2.62 (assume @p553 (forall @t272 (=> (and @t404 @t268 (forall @t147 (=> (and @t461 @t271 @t269) @t270))) @t460))) % 2.43/2.62 (assume @p554 (forall @t272 (=> (and @t404 @t460 (forall @t147 (=> (and @t461 @t271 @t270) @t269))) @t268))) % 2.43/2.62 (assume @p555 (forall @t138 (=> @t458 @t137))) % 2.43/2.62 (assume @p556 (forall @t138 (=> @t404 (= @t294 @t160)))) % 2.43/2.62 (assume @p557 (forall @t138 (= @t265 @t404))) % 2.43/2.62 (assume @p558 (forall @t138 (= @t137 @t458))) % 2.43/2.62 (assume @p559 (forall @t138 (=> @t404 @t265))) % 2.43/2.62 (assume @p560 (forall @t138 (not (< @t117 @t390)))) % 2.43/2.62 (assume @p561 (forall @t81 (=> (and @t397 @t462) false))) % 2.43/2.62 (assume @p562 (forall @t81 (=> @t397 (exists @t175 @t173)))) % 2.43/2.62 (assume @p563 (forall @t8 (=> @t176 (= (< @t433 @t389) @t87)))) % 2.43/2.62 (assume @p564 (forall @t454 (= (< @t117 @t433) (< @t117 @t5)))) % 2.43/2.62 (assume @p565 (not (< 0/1 @t420))) % 2.43/2.62 (assume @p566 (not (< 0 @t421))) % 2.43/2.62 (assume @p567 (< @t421 0)) % 2.43/2.62 (assume @p568 (forall @t81 (=> (and @t462 (forall @t175 (=> (and @t174 @t391) false))) false))) % 2.43/2.62 (assume @p569 (forall @t154 (=> @t468 (exists @t152 (and @t236 (forall @t147 (=> @t469 @t143)) @t256))))) % 2.43/2.62 (assume @p570 (forall @t231 (=> @t399 (= (<= @t217 1/1) (or @t136 @t429))))) % 2.43/2.62 (assume @p571 (forall @t81 (= @t465 @t176))) % 2.43/2.62 (assume @p572 (forall @t138 (=> (<= @t189 @t117) (<= @t189 @t192)))) % 2.43/2.62 (assume @p573 (forall (@list @t139 @t5) (= @t451 (and (forall @t152 (=> (= @t5 @t144) @t149)) (=> (< @t5 0) @t153))))) % 2.43/2.62 (assume @p574 (forall @t81 (=> (and (=> @t79 false) @t177 @t392) false))) % 2.43/2.62 (assume @p575 (forall @t81 (=> @t393 (exists @t175 @t467)))) % 2.43/2.62 (assume @p576 (forall @t119 (< @t435 0))) % 2.43/2.62 (assume @p577 (forall @t119 (= (<= 1/1 @t165) (<= 1 @t117)))) % 2.43/2.62 (assume @p578 (forall (@list @t139 @t17 @t61) (=> (and @t140 (forall @t147 (=> @t142 @t469))) (exists @t147 (and @t142 (forall (@list @t258) (=> (|tptp.'fun_app$b'| @t139 @t258) (<= @t259 @t145)))))))) % 2.43/2.62 (assume @p579 (forall @t114 (=> (and (exists @t471 @t10) (exists @t471 @t470)) (exists @t471 (and @t470 (forall @t122 (=> (forall @t352 (=> (|tptp.'member$'| @t351 @t9) (<= @t351 @t120))) @t417))))))) % 2.43/2.62 (assume @p580 (forall @t138 (or @t404 @t472))) % 2.43/2.62 (assume @p581 (forall @t138 (=> (and @t404 @t472) @t157))) % 2.43/2.62 (assume @p582 (forall @t138 (=> @t157 @t404))) % 2.43/2.62 (assume @p583 (forall @t198 (=> (and @t404 @t422) (<= @t117 @t144)))) % 2.43/2.62 (assume @p584 (forall @t119 (<= @t117 @t117))) % 2.43/2.62 (assume @p585 (forall (@list @t62 @t475 @t473) (=> (and (forall @t147 (=> @t461 (< @t476 @t477))) (forall @t147 (=> @t461 (<= @t477 @t474)))) (forall @t147 (=> @t461 (< @t476 @t474)))))) % 2.43/2.62 (assume @p586 (forall @t119 (= (|tptp.'nat$'| @t117) @t62))) % 2.43/2.62 (assume @p587 (forall (@list @t478) (or (= @t478 tptp.tltrue) (= @t478 tptp.tlfalse)))) % 2.43/2.62 (assume @p588 (not (= tptp.tltrue tptp.tlfalse))) % 2.43/2.62 (assume @p589 true) % 2.43/2.62 (step @p590 :rule bool-impl-elim :args (@t21 @t20)) % 2.43/2.62 (step @p591 :rule cong :premises (@p590) :args (@t23)) % 2.43/2.62 (step @p592 :rule eq_resolve :premises (@p8 @p591)) % 2.43/2.62 (step @p593 :rule aci_norm :args ((= @t486 (or @t484 @t483 @t482 @t480)))) % 2.43/2.62 (step @p594 :rule cong :premises (@p593) :args (@t487)) % 2.43/2.62 (step @p595 :rule quant-merge-prenex :args ((= (forall @t22 @t489) @t487))) % 2.43/2.62 (step @p596 :rule alpha_equiv :args (@t490 (@list @t481 @t479) (@list @t27 @t491))) % 2.43/2.62 (step @p597 :rule refl :args (@t484)) % 2.43/2.62 (step @p598 :rule nary_cong :premises (@p597 @p596) :args (@t492)) % 2.43/2.62 (step @p599 :rule quant-miniscope-or :args ((= @t489 @t492))) % 2.43/2.62 (step @p600 :rule trans :premises (@p599 @p598)) % 2.43/2.62 (step @p601 :rule symm :premises (@p600)) % 2.43/2.62 (step @p602 :rule cong :premises (@p601) :args ((forall @t22 (or @t484 @t498)))) % 2.43/2.62 (step @p603 :rule trans :premises (@p602 @p595)) % 2.43/2.62 (step @p604 :rule trans :premises (@p603 @p594)) % 2.43/2.62 (step @p605 :rule bool-impl-elim :args (@t20 @t498)) % 2.43/2.62 (step @p606 :rule cong :premises (@p605) :args ((forall @t22 (=> @t20 @t498)))) % 2.43/2.62 (step @p607 :rule trans :premises (@p606 @p604)) % 2.43/2.62 (step @p608 :rule aci_norm :args ((= @t500 @t496))) % 2.43/2.62 (step @p609 :rule cong :premises (@p608) :args (@t501)) % 2.43/2.62 (step @p610 :rule quant-merge-prenex :args ((= (forall @t32 @t503) @t501))) % 2.43/2.62 (step @p611 :rule alpha_equiv :args (@t504 (@list @t491) (@list @t47))) % 2.43/2.62 (step @p612 :rule refl :args (@t495)) % 2.43/2.62 (step @p613 :rule nary_cong :premises (@p612 @p611) :args (@t505)) % 2.43/2.62 (step @p614 :rule quant-miniscope-or :args ((= @t503 @t505))) % 2.43/2.62 (step @p615 :rule trans :premises (@p614 @p613)) % 2.43/2.62 (step @p616 :rule symm :premises (@p615)) % 2.43/2.62 (step @p617 :rule cong :premises (@p616) :args ((forall @t32 (or @t495 @t507)))) % 2.43/2.62 (step @p618 :rule trans :premises (@p617 @p610)) % 2.43/2.62 (step @p619 :rule trans :premises (@p618 @p609)) % 2.43/2.62 (step @p620 :rule bool-impl-elim :args (@t56 @t507)) % 2.43/2.62 (step @p621 :rule cong :premises (@p620) :args ((forall @t32 (=> @t56 @t507)))) % 2.43/2.62 (step @p622 :rule trans :premises (@p621 @p619)) % 2.43/2.62 (step @p623 :rule bool-double-not-elim :args (@t507)) % 2.43/2.62 (step @p624 :rule bool-double-not-elim :args (@t48)) % 2.43/2.62 (step @p625 :rule refl :args (@t506)) % 2.43/2.62 (step @p626 :rule nary_cong :premises (@p625 @p624) :args ((or @t506 (not @t49)))) % 2.43/2.62 (step @p627 :rule bool-and-de-morgan :args (@t51 @t49 true)) % 2.43/2.62 (step @p628 :rule trans :premises (@p627 @p626)) % 2.43/2.62 (step @p629 :rule cong :premises (@p628) :args (@t508)) % 2.43/2.62 (step @p630 :rule cong :premises (@p629) :args (@t509)) % 2.43/2.62 (step @p631 :rule exists-elim :args ((= @t54 @t509))) % 2.43/2.62 (step @p632 :rule trans :premises (@p631 @p630)) % 2.43/2.62 (step @p633 :rule cong :premises (@p632) :args (@t55)) % 2.43/2.62 (step @p634 :rule trans :premises (@p633 @p623)) % 2.43/2.62 (step @p635 :rule refl :args (@t56)) % 2.43/2.62 (step @p636 :rule cong :premises (@p635 @p634) :args (@t57)) % 2.43/2.62 (step @p637 :rule cong :premises (@p636) :args (@t58)) % 2.43/2.62 (step @p638 :rule trans :premises (@p637 @p622)) % 2.43/2.62 (step @p639 :rule refl :args (@t20)) % 2.43/2.62 (step @p640 :rule cong :premises (@p639 @p638) :args (@t59)) % 2.43/2.62 (step @p641 :rule cong :premises (@p640) :args (@t60)) % 2.43/2.62 (step @p642 :rule trans :premises (@p641 @p607)) % 2.43/2.62 (step @p643 :rule eq_resolve :premises (@p19 @p642)) % 2.43/2.62 (step @p644 :rule instantiate :premises (@p643) :args ((@list |tptp.'a$'| @t14 @t346 |tptp.'i$'|))) % 2.43/2.62 (step @p645 :rule refl :args (|tptp.'i$'|)) % 2.43/2.62 (step @p646 :rule symm :premises (@p267)) % 2.43/2.62 (step @p647 :rule refl :args (|tptp.'less$'|)) % 2.43/2.62 (step @p648 :rule cong :premises (@p647 @p646) :args (@t24)) % 2.43/2.62 (step @p649 :rule cong :premises (@p648 @p645) :args (@t25)) % 2.43/2.62 (step @p650 :rule eq_resolve :premises (@p9 @p649)) % 2.43/2.62 (step @p651 :rule refl :args (|tptp.'a$'|)) % 2.43/2.62 (step @p652 :rule refl :args (@t14)) % 2.43/2.62 (step @p653 :rule cong :premises (@p646 @p652 @p651) :args (@t16)) % 2.43/2.62 (step @p654 :rule eq_resolve :premises (@p6 @p653)) % 2.43/2.62 (step @p655 :rule cnf_or_pos :args (@t516)) % 2.43/2.62 (step @p656 :rule reordering :premises (@p655) :args ((or @t15 @t513 @t511 @t515 (not @t516)))) % 2.43/2.62 (step @p657 :rule chain_m_resolution :premises (@p656 @p5 @p654 @p650 @p644) :args (@t515 (@list true false false false) (@list @t15 @t512 @t510 @t516))) % 2.43/2.62 (step @p658 :rule cnf_or_pos :args (@t517)) % 2.43/2.62 (step @p659 :rule reordering :premises (@p658) :args ((or @t13 @t514 @t518))) % 2.43/2.62 (step @p660 :rule chain_m_resolution :premises (@p659 @p7 @p657) :args (@t518 (@list false true) (@list @t12 @t514))) % 2.43/2.62 (assume-push @p667 @t519) % 2.43/2.62 (step @p662 :rule instantiate :premises (@p592) :args ((@list |tptp.'a$'| @t14))) % 2.43/2.62 (step-pop @p668 :rule scope :premises (@p662)) % 2.43/2.62 (step @p663 :rule process_scope :premises (@p668) :args (@t517)) % 2.43/2.62 (step @p665 :rule implies_elim :premises (@p663)) % 2.43/2.62 (step @p666 false :rule chain_m_resolution :premises (@p665 @p660 @p592) :args (false (@list true false) (@list @t517 @t519))) % 2.43/2.62 ) % 2.43/2.62 % SZS output end Proof % 2.43/2.62 % cvc5 exiting %------------------------------------------------------------------------------