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