%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP366_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 : n011.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:25 AM UTC 2026 % Result : Theorem 0.47s 0.87s % Output : Proof 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP366_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.16/0.34 % Computer : n011.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 05:03:35 EDT 2026 % 0.16/0.34 % CPUTime : % 0.38/0.64 %----Proving TF0_ARI % 0.47/0.87 --- Run --finite-model-find --decision=internal at 45... % 0.47/0.87 % SZS status Theorem % 0.47/0.87 % SZS output start Proof % 0.47/0.87 ( % 0.47/0.87 (declare-sort |tptp.'Nat_num_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Num$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_nat_bool_fun_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_set_list$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln_bool_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_int_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln_a_ltln_bool_fun_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln_a_set_a_ltln_fun_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln_a_ltln_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_set_a_ltln_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_set$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_nat_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Bool_nat_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Num_bool_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln_set$'| 0) % 0.47/0.87 (declare-sort |tptp.'Int_bool_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Int_int_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'A_ltln$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_a_set_fun_bool_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_a_set_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat_a_set_fun_set$'| 0) % 0.47/0.87 (declare-sort |tptp.'Nat$'| 0) % 0.47/0.87 (declare-sort tptp.tlbool 0) % 0.47/0.87 (declare-sort |tptp.'Nat_bool_fun$'| 0) % 0.47/0.87 (declare-sort |tptp.'Bool_bool_fun$'| 0) % 0.47/0.87 (declare-const |tptp.'plus$'| (-> |tptp.'Num$'| |tptp.'Num$'| |tptp.'Num$'|)) % 0.47/0.87 (declare-const |tptp.'bit1$'| (-> |tptp.'Num$'| |tptp.'Num$'|)) % 0.47/0.87 (declare-const |tptp.'bit0$'| (-> |tptp.'Num$'| |tptp.'Num$'|)) % 0.47/0.87 (declare-const |tptp.'sub$'| (-> |tptp.'Num$'| |tptp.'Num$'| Int)) % 0.47/0.87 (declare-const |tptp.'num_of_nat$'| |tptp.'Nat_num_fun$'|) % 0.47/0.87 (declare-const tptp.tlfalse tptp.tlbool) % 0.47/0.87 (declare-const tptp.def_9 (-> tptp.tlbool |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const tptp.def_10 (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const tptp.def_8 (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'pred$'| |tptp.'Nat_nat_fun$'|) % 0.47/0.87 (declare-const tptp.tltrue tptp.tlbool) % 0.47/0.87 (declare-const tptp.def_5 (-> tptp.tlbool |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const tptp.def_6 (-> |tptp.'Bool_bool_fun$'| tptp.tlbool tptp.tlbool)) % 0.47/0.87 (declare-const tptp.def_4 (-> tptp.tlbool |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'case_nat$a'| (-> tptp.tlbool |tptp.'Nat_bool_fun$'| |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'conc$'| (-> |tptp.'A_set_list$'| |tptp.'Nat_a_set_fun$'| |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (declare-const |tptp.'case_nat$'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'| |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (declare-const |tptp.'one$'| |tptp.'Num$'|) % 0.47/0.87 (declare-const |tptp.'inc$'| (-> |tptp.'Num$'| |tptp.'Num$'|)) % 0.47/0.87 (declare-const |tptp.'numeral$'| (-> |tptp.'Num$'| Int)) % 0.47/0.87 (declare-const |tptp.'nu_stable$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'mu_stable$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'g_F$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun$'| |tptp.'A_ltln_set$'|)) % 0.47/0.87 (declare-const |tptp.'f_G$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun$'| |tptp.'A_ltln_set$'|)) % 0.47/0.87 (declare-const |tptp.'g$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun$'| |tptp.'A_ltln_set$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$k'| (-> |tptp.'Nat_int_fun$'| |tptp.'Nat$'| Int)) % 0.47/0.87 (declare-const |tptp.'x$'| |tptp.'A_ltln_set$'|) % 0.47/0.87 (declare-const |tptp.'next_ltln$'| |tptp.'A_ltln_a_ltln_fun$'|) % 0.47/0.87 (declare-const |tptp.'semantics_ltln$'| (-> |tptp.'Nat_a_set_fun$'| |tptp.'A_ltln$'| Bool)) % 0.47/0.87 (declare-const |tptp.'uuj$'| |tptp.'Nat_bool_fun$'|) % 0.47/0.87 (declare-const |tptp.'w$'| |tptp.'Nat_a_set_fun$'|) % 0.47/0.87 (declare-const |tptp.'uue$'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat_nat_fun$'| |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (declare-const tptp.def_1 (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'phi$'| |tptp.'A_ltln$'|) % 0.47/0.87 (declare-const |tptp.'uuf$'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat_nat_fun$'| |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$h'| (-> |tptp.'A_ltln_a_set_a_ltln_fun_fun$'| |tptp.'A_ltln$'| |tptp.'A_set_a_ltln_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$e'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 0.47/0.87 (declare-const |tptp.'sgn$'| (-> Int Int)) % 0.47/0.87 (declare-const |tptp.'uug$'| (-> |tptp.'Bool_nat_fun$'| |tptp.'Nat_bool_fun$'| |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$f'| (-> |tptp.'Bool_nat_fun$'| tptp.tlbool |tptp.'Nat$'|)) % 0.47/0.87 (declare-const tptp.def_2 (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'gF_advice$'| (-> |tptp.'A_ltln$'| |tptp.'A_ltln_set$'| |tptp.'A_ltln$'|)) % 0.47/0.87 (declare-const |tptp.'uub$'| (-> Int |tptp.'Int_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'uuc$'| (-> Int |tptp.'Int_int_fun$'|)) % 0.47/0.87 (declare-const |tptp.'subsequence$'| (-> |tptp.'Nat_a_set_fun$'| |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'A_set_list$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$'| (-> |tptp.'Int_bool_fun$'| Int Bool)) % 0.47/0.87 (declare-const |tptp.'uu$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'nat$'| (-> Int |tptp.'Nat$'|)) % 0.47/0.87 (declare-const |tptp.'uud$'| |tptp.'Nat_nat_fun$'|) % 0.47/0.87 (declare-const |tptp.'fun_app$a'| (-> |tptp.'Int_int_fun$'| Int Int)) % 0.47/0.87 (declare-const |tptp.'fun_app$b'| (-> |tptp.'Nat_a_set_fun_bool_fun$'| |tptp.'Nat_a_set_fun$'| Bool)) % 0.47/0.87 (declare-const |tptp.'uuh$'| (-> |tptp.'Bool_bool_fun$'| |tptp.'Nat_bool_fun$'| |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$o'| (-> |tptp.'Num_bool_fun$'| |tptp.'Num$'| Bool)) % 0.47/0.87 (declare-const |tptp.'member$'| (-> |tptp.'Nat_a_set_fun$'| |tptp.'Nat_a_set_fun_set$'| Bool)) % 0.47/0.87 (declare-const |tptp.'fun_app$c'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| Bool)) % 0.47/0.87 (declare-const |tptp.'fun_app$j'| (-> |tptp.'Nat_a_set_fun$'| |tptp.'Nat$'| |tptp.'A_set$'|)) % 0.47/0.87 (declare-const |tptp.'uua$'| (-> |tptp.'Nat_a_set_fun_set$'| |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$i'| (-> |tptp.'A_ltln_a_ltln_fun$'| |tptp.'A_ltln$'| |tptp.'A_ltln$'|)) % 0.47/0.87 (declare-const |tptp.'uui$'| |tptp.'Nat_bool_fun$'|) % 0.47/0.87 (declare-const |tptp.'fun_app$d'| (-> |tptp.'Bool_bool_fun$'| tptp.tlbool Bool)) % 0.47/0.87 (declare-const tptp.def_7 (-> tptp.tlbool |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'af_letter$'| |tptp.'A_ltln_a_set_a_ltln_fun_fun$'|) % 0.47/0.87 (declare-const |tptp.'dbl_inc$'| (-> Int Int)) % 0.47/0.87 (declare-const |tptp.'fun_app$g'| (-> |tptp.'A_set_a_ltln_fun$'| |tptp.'A_set$'| |tptp.'A_ltln$'|)) % 0.47/0.87 (declare-const |tptp.'gF_advice_congruent$'| (-> |tptp.'A_ltln_a_ltln_bool_fun_fun$'| |tptp.'A_ltln_a_ltln_fun$'| Bool)) % 0.47/0.87 (declare-const |tptp.'suffix$'| (-> |tptp.'Nat$'| |tptp.'Nat_a_set_fun$'| |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (declare-const |tptp.'unf$'| |tptp.'A_ltln_a_ltln_fun$'|) % 0.47/0.87 (declare-const |tptp.'collect$'| (-> |tptp.'Nat_a_set_fun_bool_fun$'| |tptp.'Nat_a_set_fun_set$'|)) % 0.47/0.87 (declare-const |tptp.'language_ltln$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun_set$'|)) % 0.47/0.87 (declare-const |tptp.'of_nat$'| |tptp.'Nat_int_fun$'|) % 0.47/0.87 (declare-const |tptp.'build$'| (-> |tptp.'A_set$'| |tptp.'Nat_a_set_fun$'| |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$m'| (-> |tptp.'A_ltln_a_ltln_bool_fun_fun$'| |tptp.'A_ltln$'| |tptp.'A_ltln_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$l'| (-> |tptp.'A_ltln_bool_fun$'| |tptp.'A_ltln$'| Bool)) % 0.47/0.87 (declare-const |tptp.'af_congruent_axioms$'| (-> |tptp.'A_ltln_a_ltln_bool_fun_fun$'| Bool)) % 0.47/0.87 (declare-const |tptp.'gF_advice_congruent_axioms$'| (-> |tptp.'A_ltln_a_ltln_bool_fun_fun$'| |tptp.'A_ltln_a_ltln_fun$'| Bool)) % 0.47/0.87 (declare-const |tptp.'fG_advice$'| (-> |tptp.'A_ltln$'| |tptp.'A_ltln_set$'| |tptp.'A_ltln$'|)) % 0.47/0.87 (declare-const |tptp.'dbl_dec$'| (-> Int Int)) % 0.47/0.87 (declare-const |tptp.'dbl$'| (-> Int Int)) % 0.47/0.87 (declare-const |tptp.'foldl$'| (-> |tptp.'A_ltln_a_set_a_ltln_fun_fun$'| |tptp.'A_ltln$'| |tptp.'A_set_list$'| |tptp.'A_ltln$'|)) % 0.47/0.87 (declare-const tptp.def_3 (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| tptp.tlbool)) % 0.47/0.87 (declare-const |tptp.'idx_sequence$'| (-> |tptp.'Nat_nat_fun$'| Bool)) % 0.47/0.87 (declare-const |tptp.'fun_app$n'| (-> |tptp.'Nat_nat_bool_fun_fun$'| |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'fun_app$p'| (-> |tptp.'Nat_num_fun$'| |tptp.'Nat$'| |tptp.'Num$'|)) % 0.47/0.87 (declare-const |tptp.'less$'| (-> |tptp.'Num$'| |tptp.'Num_bool_fun$'|)) % 0.47/0.87 (declare-const |tptp.'id$'| |tptp.'A_ltln_a_ltln_fun$'|) % 0.47/0.87 (declare-const |tptp.'f$'| (-> |tptp.'A_ltln$'| |tptp.'Nat_a_set_fun$'| |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t1 () (@var "A__questionmark_v1" Int)) % 0.47/0.87 (define @t2 () (@var "A__questionmark_v0" Int)) % 0.47/0.87 (define @t3 () (< @t2 @t1)) % 0.47/0.87 (define @t4 () (@list @t2 @t1)) % 0.47/0.87 (define @t5 () (- @t2 @t1)) % 0.47/0.87 (define @t6 () (@var "A__questionmark_v0" |tptp.'A_ltln$'|)) % 0.47/0.87 (define @t7 () (@var "A__questionmark_v1" |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (define @t8 () (|tptp.'uu$'| @t6)) % 0.47/0.87 (define @t9 () (@list @t6 @t7)) % 0.47/0.87 (define @t10 () (@var "A__questionmark_v0" |tptp.'Nat_a_set_fun_set$'|)) % 0.47/0.87 (define @t11 () (|tptp.'uua$'| @t10)) % 0.47/0.87 (define @t12 () (@var "A__questionmark_v2" |tptp.'Nat$'|)) % 0.47/0.87 (define @t13 () (@var "A__questionmark_v1" |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (define @t14 () (tptp.def_1 @t13 @t12)) % 0.47/0.87 (define @t15 () (@var "A__questionmark_v0" |tptp.'Bool_bool_fun$'|)) % 0.47/0.87 (define @t16 () (tptp.def_2 @t13 @t12)) % 0.47/0.87 (define @t17 () (@var "A__questionmark_v0" |tptp.'Bool_nat_fun$'|)) % 0.47/0.87 (define @t18 () (@var "A__questionmark_v1" |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (define @t19 () (|tptp.'fun_app$e'| @t18 @t12)) % 0.47/0.87 (define @t20 () (@var "A__questionmark_v0" |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (define @t21 () (@var "A__questionmark_v0" |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (define @t22 () (@var "A__questionmark_v0" |tptp.'Nat$'|)) % 0.47/0.87 (define @t23 () (@list @t22)) % 0.47/0.87 (define @t24 () (|tptp.'nat$'| 0)) % 0.47/0.87 (define @t25 () (|tptp.'fun_app$j'| |tptp.'w$'| @t24)) % 0.47/0.87 (define @t26 () (|tptp.'fun_app$i'| |tptp.'next_ltln$'| |tptp.'phi$'|)) % 0.47/0.87 (define @t27 () (|tptp.'nat$'| 1)) % 0.47/0.87 (define @t28 () (|tptp.'suffix$'| @t27 |tptp.'w$'|)) % 0.47/0.87 (define @t29 () (@var "A__questionmark_v0" |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (define @t30 () (@list @t29)) % 0.47/0.87 (define @t31 () (@var "A__questionmark_v1" |tptp.'A_ltln$'|)) % 0.47/0.87 (define @t32 () (|tptp.'suffix$'| @t27 @t29)) % 0.47/0.87 (define @t33 () (|tptp.'fun_app$i'| |tptp.'next_ltln$'| @t31)) % 0.47/0.87 (define @t34 () (@list @t29 @t31)) % 0.47/0.87 (define @t35 () (@var "A__questionmark_v2" |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t36 () (|tptp.'fun_app$i'| |tptp.'unf$'| @t31)) % 0.47/0.87 (define @t37 () (|tptp.'semantics_ltln$'| @t29 (|tptp.'gF_advice$'| @t31 @t35))) % 0.47/0.87 (define @t38 () (@list @t29 @t31 @t35)) % 0.47/0.87 (define @t39 () (|tptp.'fun_app$i'| |tptp.'next_ltln$'| @t6)) % 0.47/0.87 (define @t40 () (@var "A__questionmark_v1" |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t41 () (@list @t6 @t40)) % 0.47/0.87 (define @t42 () (@var "A__questionmark_v1" |tptp.'A_set$'|)) % 0.47/0.87 (define @t43 () (|tptp.'fun_app$g'| (|tptp.'fun_app$h'| |tptp.'af_letter$'| @t39) @t42)) % 0.47/0.87 (define @t44 () (forall (@list @t6 @t42) (= @t43 @t6))) % 0.47/0.87 (define @t45 () (|tptp.'fun_app$i'| |tptp.'unf$'| @t39)) % 0.47/0.87 (define @t46 () (@list @t6)) % 0.47/0.87 (define @t47 () (forall @t46 (= @t45 @t39))) % 0.47/0.87 (define @t48 () (|tptp.'semantics_ltln$'| @t29 @t31)) % 0.47/0.87 (define @t49 () (= @t2 0)) % 0.47/0.87 (define @t50 () (= 0 @t2)) % 0.47/0.87 (define @t51 () (@list @t2)) % 0.47/0.87 (define @t52 () (|tptp.'fun_app$j'| @t29 @t24)) % 0.47/0.87 (define @t53 () (@var "A__questionmark_v3" |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t54 () (@var "A__questionmark_v0" |tptp.'A_set$'|)) % 0.47/0.87 (define @t55 () (@var "A__questionmark_v2" |tptp.'A_ltln$'|)) % 0.47/0.87 (define @t56 () (|tptp.'fun_app$h'| |tptp.'af_letter$'| @t55)) % 0.47/0.87 (define @t57 () (|tptp.'fun_app$g'| @t56 @t54)) % 0.47/0.87 (define @t58 () (|tptp.'gF_advice$'| @t55 @t53)) % 0.47/0.87 (define @t59 () (|tptp.'build$'| @t54 @t7)) % 0.47/0.87 (define @t60 () (@var "A__questionmark_v4" |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t61 () (@var "A__questionmark_v3" |tptp.'A_ltln$'|)) % 0.47/0.87 (define @t62 () (@var "A__questionmark_v1" |tptp.'A_ltln_a_ltln_fun$'|)) % 0.47/0.87 (define @t63 () (|tptp.'fun_app$i'| @t62 @t61)) % 0.47/0.87 (define @t64 () (|tptp.'gF_advice$'| @t63 @t60)) % 0.47/0.87 (define @t65 () (@var "A__questionmark_v2" |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (define @t66 () (|tptp.'semantics_ltln$'| @t65 @t64)) % 0.47/0.87 (define @t67 () (|tptp.'semantics_ltln$'| @t65 (|tptp.'gF_advice$'| @t61 @t60))) % 0.47/0.87 (define @t68 () (@var "A__questionmark_v0" |tptp.'A_ltln_a_ltln_bool_fun_fun$'|)) % 0.47/0.87 (define @t69 () (|tptp.'gF_advice_congruent$'| @t68 @t62)) % 0.47/0.87 (define @t70 () (@list @t68 @t62 @t65 @t61 @t60)) % 0.47/0.87 (define @t71 () (= 0 0)) % 0.47/0.87 (define @t72 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t22)) % 0.47/0.87 (define @t73 () (= @t72 0)) % 0.47/0.87 (define @t74 () (not @t73)) % 0.47/0.87 (define @t75 () (=> @t73 false)) % 0.47/0.87 (define @t76 () (@var "A__questionmark_v3" |tptp.'A_set$'|)) % 0.47/0.87 (define @t77 () (|tptp.'fun_app$h'| |tptp.'af_letter$'| @t31)) % 0.47/0.87 (define @t78 () (forall (@list @t31 @t55 @t76) (=> (|tptp.'fun_app$l'| (|tptp.'fun_app$m'| @t68 @t31) @t55) (|tptp.'fun_app$l'| (|tptp.'fun_app$m'| @t68 (|tptp.'fun_app$g'| @t77 @t76)) (|tptp.'fun_app$g'| @t56 @t76))))) % 0.47/0.87 (define @t79 () (|tptp.'af_congruent_axioms$'| @t68)) % 0.47/0.87 (define @t80 () (@list @t68)) % 0.47/0.87 (define @t81 () (@var "A__questionmark_v3" |tptp.'Nat_a_set_fun$'|)) % 0.47/0.87 (define @t82 () (@var "A__questionmark_v2" |tptp.'A_set$'|)) % 0.47/0.87 (define @t83 () (|tptp.'fun_app$i'| @t62 @t55)) % 0.47/0.87 (define @t84 () (|tptp.'fun_app$m'| @t68 @t55)) % 0.47/0.87 (define @t85 () (|tptp.'fun_app$l'| @t84 @t83)) % 0.47/0.87 (define @t86 () (|tptp.'fun_app$l'| (|tptp.'fun_app$m'| @t68 (|tptp.'gF_advice$'| @t83 @t60)) @t64)) % 0.47/0.87 (define @t87 () (|tptp.'fun_app$l'| @t84 @t61)) % 0.47/0.87 (define @t88 () (+ 0 1)) % 0.47/0.87 (define @t89 () (|tptp.'gF_advice_congruent_axioms$'| @t68 @t62)) % 0.47/0.87 (define @t90 () (@list @t68 @t62)) % 0.47/0.87 (define @t91 () (|tptp.'fG_advice$'| @t31 @t53)) % 0.47/0.87 (define @t92 () (+ @t72 1)) % 0.47/0.87 (define @t93 () (|tptp.'nat$'| @t92)) % 0.47/0.87 (define @t94 () (@var "A__questionmark_v1" |tptp.'Nat$'|)) % 0.47/0.87 (define @t95 () (|tptp.'suffix$'| @t94 @t29)) % 0.47/0.87 (define @t96 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t94)) % 0.47/0.87 (define @t97 () (+ @t96 1)) % 0.47/0.87 (define @t98 () (|tptp.'nat$'| @t97)) % 0.47/0.87 (define @t99 () (@list @t29 @t94)) % 0.47/0.87 (define @t100 () (- 1)) % 0.47/0.87 (define @t101 () (@var "A__questionmark_v5" |tptp.'Nat$'|)) % 0.47/0.87 (define @t102 () (exists (@list @t101) (|tptp.'semantics_ltln$'| (|tptp.'suffix$'| @t101 @t65) (|tptp.'gF_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t61 (|tptp.'subsequence$'| @t65 @t24 @t101)) @t60)))) % 0.47/0.87 (define @t103 () (< @t72 1)) % 0.47/0.87 (define @t104 () (= @t72 @t96)) % 0.47/0.87 (define @t105 () (= @t92 @t97)) % 0.47/0.87 (define @t106 () (@list @t22 @t94)) % 0.47/0.87 (define @t107 () (@var "A__questionmark_v1" |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (define @t108 () (|tptp.'collect$'| @t107)) % 0.47/0.87 (define @t109 () (@var "A__questionmark_v0" |tptp.'Nat_a_set_fun_bool_fun$'|)) % 0.47/0.87 (define @t110 () (= @t2 @t1)) % 0.47/0.87 (define @t111 () (- @t1)) % 0.47/0.87 (define @t112 () (- @t2)) % 0.47/0.87 (define @t113 () (= @t112 @t111)) % 0.47/0.87 (define @t114 () (< @t1 @t2)) % 0.47/0.87 (define @t115 () (< @t72 0)) % 0.47/0.87 (define @t116 () (< 0 @t72)) % 0.47/0.87 (define @t117 () (< @t72 @t96)) % 0.47/0.87 (define @t118 () (< @t92 @t97)) % 0.47/0.87 (define @t119 () (< @t2 0)) % 0.47/0.87 (define @t120 () (< 0 @t2)) % 0.47/0.87 (define @t121 () (< 0 @t92)) % 0.47/0.87 (define @t122 () (< @t72 @t88)) % 0.47/0.87 (define @t123 () (< @t72 @t97)) % 0.47/0.87 (define @t124 () (not @t117)) % 0.47/0.87 (define @t125 () (@var "A__questionmark_v2" |tptp.'Nat_bool_fun$'|)) % 0.47/0.87 (define @t126 () (@var "A__questionmark_v3" |tptp.'Nat$'|)) % 0.47/0.87 (define @t127 () (|tptp.'fun_app$c'| @t125 @t126)) % 0.47/0.87 (define @t128 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t126)) % 0.47/0.87 (define @t129 () (+ @t128 1)) % 0.47/0.87 (define @t130 () (|tptp.'nat$'| @t129)) % 0.47/0.87 (define @t131 () (@list @t126)) % 0.47/0.87 (define @t132 () (< @t96 @t72)) % 0.47/0.87 (define @t133 () (=> @t117 false)) % 0.47/0.87 (define @t134 () (not @t104)) % 0.47/0.87 (define @t135 () (|tptp.'fun_app$c'| @t20 @t94)) % 0.47/0.87 (define @t136 () (|tptp.'fun_app$c'| @t20 @t126)) % 0.47/0.87 (define @t137 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t12)) % 0.47/0.87 (define @t138 () (< @t128 @t137)) % 0.47/0.87 (define @t139 () (exists @t131 (and @t138 (not @t136)))) % 0.47/0.87 (define @t140 () (|tptp.'fun_app$c'| @t20 @t12)) % 0.47/0.87 (define @t141 () (not @t140)) % 0.47/0.87 (define @t142 () (@list @t12)) % 0.47/0.87 (define @t143 () (@list @t20 @t94)) % 0.47/0.87 (define @t144 () (< @t72 @t72)) % 0.47/0.87 (define @t145 () (@var "A__questionmark_v2" |tptp.'Nat_nat_bool_fun_fun$'|)) % 0.47/0.87 (define @t146 () (|tptp.'fun_app$n'| @t145 @t126)) % 0.47/0.87 (define @t147 () (@var "A__questionmark_v4" |tptp.'Nat$'|)) % 0.47/0.87 (define @t148 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t147)) % 0.47/0.87 (define @t149 () (< @t96 @t137)) % 0.47/0.87 (define @t150 () (@list @t22 @t94 @t12)) % 0.47/0.87 (define @t151 () (= @t96 @t72)) % 0.47/0.87 (define @t152 () (not @t144)) % 0.47/0.87 (define @t153 () (< @t72 @t137)) % 0.47/0.87 (define @t154 () (+ @t137 1)) % 0.47/0.87 (define @t155 () (= @t96 @t154)) % 0.47/0.87 (define @t156 () (< @t92 @t96)) % 0.47/0.87 (define @t157 () (|tptp.'fun_app$c'| @t13 @t12)) % 0.47/0.87 (define @t158 () (< @t137 @t72)) % 0.47/0.87 (define @t159 () (|tptp.'fun_app$c'| @t13 @t22)) % 0.47/0.87 (define @t160 () (< @t137 @t92)) % 0.47/0.87 (define @t161 () (forall @t142 (=> @t160 @t157))) % 0.47/0.87 (define @t162 () (@list @t22 @t13)) % 0.47/0.87 (define @t163 () (< @t96 @t92)) % 0.47/0.87 (define @t164 () (exists @t142 (and @t160 @t157))) % 0.47/0.87 (define @t165 () (forall @t142 (=> (and @t153 @t155) false))) % 0.47/0.87 (define @t166 () (@var "A__questionmark_v0" |tptp.'Nat_num_fun$'|)) % 0.47/0.87 (define @t167 () (|tptp.'fun_app$o'| (|tptp.'less$'| (|tptp.'fun_app$p'| @t166 @t94)) (|tptp.'fun_app$p'| @t166 @t12))) % 0.47/0.87 (define @t168 () (forall @t131 (|tptp.'fun_app$o'| (|tptp.'less$'| (|tptp.'fun_app$p'| @t166 @t126)) (|tptp.'fun_app$p'| @t166 @t130)))) % 0.47/0.87 (define @t169 () (@list @t166 @t94 @t12)) % 0.47/0.87 (define @t170 () (@var "A__questionmark_v0" |tptp.'Nat_int_fun$'|)) % 0.47/0.87 (define @t171 () (< (|tptp.'fun_app$k'| @t170 @t94) (|tptp.'fun_app$k'| @t170 @t12))) % 0.47/0.87 (define @t172 () (forall @t131 (< (|tptp.'fun_app$k'| @t170 @t126) (|tptp.'fun_app$k'| @t170 @t130)))) % 0.47/0.87 (define @t173 () (@list @t170 @t94 @t12)) % 0.47/0.87 (define @t174 () (= @t112 @t1)) % 0.47/0.87 (define @t175 () (= @t1 @t112)) % 0.47/0.87 (define @t176 () (= @t2 @t111)) % 0.47/0.87 (define @t177 () (< @t137 @t96)) % 0.47/0.87 (define @t178 () (= @t72 @t97)) % 0.47/0.87 (define @t179 () (@list @t94)) % 0.47/0.87 (define @t180 () (exists @t179 @t178)) % 0.47/0.87 (define @t181 () (|tptp.'nat$'| @t154)) % 0.47/0.87 (define @t182 () (|tptp.'fun_app$c'| @t13 @t181)) % 0.47/0.87 (define @t183 () (|tptp.'fun_app$c'| @t13 @t24)) % 0.47/0.87 (define @t184 () (< 0 @t137)) % 0.47/0.87 (define @t185 () (< 0 0)) % 0.47/0.87 (define @t186 () (|tptp.'suffix$'| @t22 @t7)) % 0.47/0.87 (define @t187 () (= 0 @t92)) % 0.47/0.87 (define @t188 () (= @t92 0)) % 0.47/0.87 (define @t189 () (|tptp.'fun_app$c'| @t20 @t24)) % 0.47/0.87 (define @t190 () (|tptp.'fun_app$c'| @t20 @t181)) % 0.47/0.87 (define @t191 () (@var "A__questionmark_v0" |tptp.'Nat_nat_bool_fun_fun$'|)) % 0.47/0.87 (define @t192 () (|tptp.'fun_app$n'| @t191 @t126)) % 0.47/0.87 (define @t193 () (= @t96 0)) % 0.47/0.87 (define @t194 () (not @t115)) % 0.47/0.87 (define @t195 () (not @t116)) % 0.47/0.87 (define @t196 () (@list @t65 @t61 @t60)) % 0.47/0.87 (define @t197 () (and (forall (@list @t55) @t85) (forall @t196 (=> @t67 @t66)) (forall @t196 (=> @t66 @t102)) (forall (@list @t55 @t61 @t60) (=> @t87 @t86)))) % 0.47/0.87 (define @t198 () (|tptp.'subsequence$'| @t29 @t24 @t147)) % 0.47/0.87 (define @t199 () (|tptp.'suffix$'| @t147 @t29)) % 0.47/0.87 (define @t200 () (|tptp.'semantics_ltln$'| @t199 (|tptp.'gF_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t61 @t198) @t35))) % 0.47/0.87 (define @t201 () (|tptp.'semantics_ltln$'| @t199 (|tptp.'gF_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t31 @t198) @t35))) % 0.47/0.87 (define @t202 () (@list @t147)) % 0.47/0.87 (define @t203 () (|tptp.'semantics_ltln$'| (|tptp.'suffix$'| @t126 @t29) (|tptp.'gF_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t31 (|tptp.'subsequence$'| @t29 @t24 @t126)) @t35))) % 0.47/0.87 (define @t204 () (|tptp.'fun_app$i'| |tptp.'id$'| @t31)) % 0.47/0.87 (define @t205 () (|tptp.'semantics_ltln$'| @t29 (|tptp.'gF_advice$'| @t204 @t35))) % 0.47/0.87 (define @t206 () (@var "A__questionmark_v0" |tptp.'Num$'|)) % 0.47/0.87 (define @t207 () (|tptp.'less$'| @t206)) % 0.47/0.87 (define @t208 () (@list @t206)) % 0.47/0.87 (define @t209 () (|tptp.'fun_app$e'| @t21 @t94)) % 0.47/0.87 (define @t210 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t209)) % 0.47/0.87 (define @t211 () (|tptp.'idx_sequence$'| @t21)) % 0.47/0.87 (define @t212 () (|tptp.'sgn$'| @t2)) % 0.47/0.87 (define @t213 () (= @t212 @t100)) % 0.47/0.87 (define @t214 () (|tptp.'suffix$'| @t12 @t7)) % 0.47/0.87 (define @t215 () (|tptp.'foldl$'| |tptp.'af_letter$'| @t6 (|tptp.'subsequence$'| @t7 @t24 @t12))) % 0.47/0.87 (define @t216 () (@list @t6 @t7 @t12)) % 0.47/0.87 (define @t217 () (- @t212)) % 0.47/0.87 (define @t218 () (= @t212 1)) % 0.47/0.87 (define @t219 () (=> @t120 @t218)) % 0.47/0.87 (define @t220 () (@var "A__questionmark_v0" |tptp.'A_ltln_set$'|)) % 0.47/0.87 (define @t221 () (|tptp.'semantics_ltln$'| @t65 @t31)) % 0.47/0.87 (define @t222 () (@list @t220 @t31 @t65)) % 0.47/0.87 (define @t223 () (= @t212 0)) % 0.47/0.87 (define @t224 () (|tptp.'sgn$'| @t1)) % 0.47/0.87 (define @t225 () (= @t212 @t224)) % 0.47/0.87 (define @t226 () (@var "A__questionmark_v0" |tptp.'A_ltln_a_ltln_fun$'|)) % 0.47/0.87 (define @t227 () (|tptp.'suffix$'| @t94 @t65)) % 0.47/0.87 (define @t228 () (@list @t6 @t94 @t65)) % 0.47/0.87 (define @t229 () (|tptp.'f$'| @t6 @t7)) % 0.47/0.87 (define @t230 () (|tptp.'g$'| @t6 @t7)) % 0.47/0.87 (define @t231 () (|tptp.'f_G$'| @t6 @t7)) % 0.47/0.87 (define @t232 () (|tptp.'g_F$'| @t6 @t7)) % 0.47/0.87 (define @t233 () (|tptp.'mu_stable$'| @t6)) % 0.47/0.87 (define @t234 () (|tptp.'fun_app$b'| @t233 @t7)) % 0.47/0.87 (define @t235 () (|tptp.'nu_stable$'| @t6)) % 0.47/0.87 (define @t236 () (|tptp.'fun_app$b'| @t235 @t7)) % 0.47/0.87 (define @t237 () (- @t72 1)) % 0.47/0.87 (define @t238 () (+ @t237 1)) % 0.47/0.87 (define @t239 () (not @t103)) % 0.47/0.87 (define @t240 () (= @t88 @t72)) % 0.47/0.87 (define @t241 () (|tptp.'numeral$'| @t206)) % 0.47/0.87 (define @t242 () (- @t241)) % 0.47/0.87 (define @t243 () (|tptp.'dbl_inc$'| @t241)) % 0.47/0.87 (define @t244 () (@var "A__questionmark_v1" |tptp.'Num$'|)) % 0.47/0.87 (define @t245 () (= @t206 @t244)) % 0.47/0.87 (define @t246 () (|tptp.'numeral$'| @t244)) % 0.47/0.87 (define @t247 () (@list @t206 @t244)) % 0.47/0.87 (define @t248 () (|tptp.'fun_app$o'| @t207 @t244)) % 0.47/0.87 (define @t249 () (- @t246)) % 0.47/0.87 (define @t250 () (- @t1 @t2)) % 0.47/0.87 (define @t251 () (- @t72 @t96)) % 0.47/0.87 (define @t252 () (- @t251 @t137)) % 0.47/0.87 (define @t253 () (- @t92 @t96)) % 0.47/0.87 (define @t254 () (- @t253 @t154)) % 0.47/0.87 (define @t255 () (- 0 @t137)) % 0.47/0.87 (define @t256 () (and (=> @t117 @t184) (=> @t124 (< @t251 @t137)))) % 0.47/0.87 (define @t257 () (not @t256)) % 0.47/0.87 (define @t258 () (not @t156)) % 0.47/0.87 (define @t259 () (- 0 @t154)) % 0.47/0.87 (define @t260 () (and (=> @t156 (< 0 @t154)) (=> @t258 (< @t253 @t154)))) % 0.47/0.87 (define @t261 () (- @t92 @t97)) % 0.47/0.87 (define @t262 () (=> @t117 @t71)) % 0.47/0.87 (define @t263 () (|tptp.'fun_app$o'| (|tptp.'less$'| @t244) @t206)) % 0.47/0.87 (define @t264 () (< @t92 1)) % 0.47/0.87 (define @t265 () (= 0 @t72)) % 0.47/0.87 (define @t266 () (|tptp.'dbl$'| @t241)) % 0.47/0.87 (define @t267 () (@var "A__questionmark_v2" Int)) % 0.47/0.87 (define @t268 () (- @t1 @t267)) % 0.47/0.87 (define @t269 () (@var "A__questionmark_v3" Int)) % 0.47/0.87 (define @t270 () (- @t2 @t269)) % 0.47/0.87 (define @t271 () (< @t267 @t269)) % 0.47/0.87 (define @t272 () (and @t3 @t271)) % 0.47/0.87 (define @t273 () (@list @t2 @t1 @t267 @t269)) % 0.47/0.87 (define @t274 () (- @t267 @t269)) % 0.47/0.87 (define @t275 () (= @t5 @t274)) % 0.47/0.87 (define @t276 () (- @t267 @t1)) % 0.47/0.87 (define @t277 () (@list @t2 @t1 @t267)) % 0.47/0.87 (define @t278 () (- @t2 @t267)) % 0.47/0.87 (define @t279 () (- @t96 @t72)) % 0.47/0.87 (define @t280 () (not @t132)) % 0.47/0.87 (define @t281 () (- @t96 @t137)) % 0.47/0.87 (define @t282 () (not @t149)) % 0.47/0.87 (define @t283 () (- @t137 @t72)) % 0.47/0.87 (define @t284 () (- @t137 @t96)) % 0.47/0.87 (define @t285 () (not @t158)) % 0.47/0.87 (define @t286 () (- @t72 @t137)) % 0.47/0.87 (define @t287 () (not @t153)) % 0.47/0.87 (define @t288 () (< 0 @t96)) % 0.47/0.87 (define @t289 () (and (=> @t153 @t288) (=> @t287 (< @t286 @t96)))) % 0.47/0.87 (define @t290 () (- @t286 @t96)) % 0.47/0.87 (define @t291 () (- 0 @t96)) % 0.47/0.87 (define @t292 () (not @t289)) % 0.47/0.87 (define @t293 () (= @t252 0)) % 0.47/0.87 (define @t294 () (= @t255 0)) % 0.47/0.87 (define @t295 () (= 0 @t291)) % 0.47/0.87 (define @t296 () (- @t278 @t1)) % 0.47/0.87 (define @t297 () (- @t5 @t267)) % 0.47/0.87 (define @t298 () (= @t267 @t269)) % 0.47/0.87 (define @t299 () (and @t116 @t288)) % 0.47/0.87 (define @t300 () (+ (- @t96 @t92) 1)) % 0.47/0.87 (define @t301 () (- @t237 @t96)) % 0.47/0.87 (define @t302 () (- @t72 @t97)) % 0.47/0.87 (define @t303 () (and (=> @t103 @t288) (=> @t239 (< @t237 @t96)))) % 0.47/0.87 (define @t304 () (not @t303)) % 0.47/0.87 (define @t305 () (not @t123)) % 0.47/0.87 (define @t306 () (|tptp.'subsequence$'| @t7 @t22 @t12)) % 0.47/0.87 (define @t307 () (@list @t22 @t7 @t12)) % 0.47/0.87 (define @t308 () (- @t96 @t237)) % 0.47/0.87 (define @t309 () (- @t97 @t72)) % 0.47/0.87 (define @t310 () (- @t96 0)) % 0.47/0.87 (define @t311 () (and (=> @t103 (< @t96 0)) (=> @t239 (< @t96 @t237)))) % 0.47/0.87 (define @t312 () (not @t311)) % 0.47/0.87 (define @t313 () (< @t97 @t72)) % 0.47/0.87 (define @t314 () (= @t72 @t88)) % 0.47/0.87 (define @t315 () (|tptp.'inc$'| @t206)) % 0.47/0.87 (define @t316 () (|tptp.'numeral$'| @t315)) % 0.47/0.87 (define @t317 () (- @t316)) % 0.47/0.87 (define @t318 () (= @t206 |tptp.'one$'|)) % 0.47/0.87 (define @t319 () (|tptp.'case_nat$'| @t24 |tptp.'uud$'|)) % 0.47/0.87 (define @t320 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t319 (|tptp.'nat$'| @t251)))) % 0.47/0.87 (define @t321 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t319 @t24))) % 0.47/0.87 (define @t322 () (@var "A__questionmark_v2" |tptp.'A_set_list$'|)) % 0.47/0.87 (define @t323 () (@var "A__questionmark_v0" |tptp.'A_set_list$'|)) % 0.47/0.87 (define @t324 () (|tptp.'conc$'| @t323 @t7)) % 0.47/0.87 (define @t325 () (@var "A__questionmark_v0" |tptp.'Num_bool_fun$'|)) % 0.47/0.87 (define @t326 () (@var "A__questionmark_v2" |tptp.'Num$'|)) % 0.47/0.87 (define @t327 () (@var "A__questionmark_v2" |tptp.'Nat_nat_fun$'|)) % 0.47/0.87 (define @t328 () (|tptp.'fun_app$e'| (|tptp.'case_nat$'| @t94 @t327) @t126)) % 0.47/0.87 (define @t329 () (tptp.def_3 @t20 @t94)) % 0.47/0.87 (define @t330 () (|tptp.'fun_app$c'| @t20 @t328)) % 0.47/0.87 (define @t331 () (@list @t20 @t94 @t327 @t126)) % 0.47/0.87 (define @t332 () (@var "A__questionmark_v1" tptp.tlbool)) % 0.47/0.87 (define @t333 () (tptp.def_4 @t332 @t125 @t126)) % 0.47/0.87 (define @t334 () (tptp.def_6 @t15 @t332)) % 0.47/0.87 (define @t335 () (tptp.def_5 @t332 @t125 @t126)) % 0.47/0.87 (define @t336 () (@list @t15 @t332 @t125 @t126)) % 0.47/0.87 (define @t337 () (|tptp.'case_nat$'| @t22 @t18)) % 0.47/0.87 (define @t338 () (@var "A__questionmark_v0" tptp.tlbool)) % 0.47/0.87 (define @t339 () (= @t338 tptp.tltrue)) % 0.47/0.87 (define @t340 () (|tptp.'case_nat$a'| @t338 @t13)) % 0.47/0.87 (define @t341 () (@list @t22 @t18 @t12)) % 0.47/0.87 (define @t342 () (@list @t338 @t13 @t12)) % 0.47/0.87 (define @t343 () (|tptp.'foldl$'| |tptp.'af_letter$'| @t55 @t323)) % 0.47/0.87 (define @t344 () (|tptp.'nat$'| (- @t137 1))) % 0.47/0.87 (define @t345 () (|tptp.'fun_app$e'| @t337 @t12)) % 0.47/0.87 (define @t346 () (< @t137 1)) % 0.47/0.87 (define @t347 () (not @t346)) % 0.47/0.87 (define @t348 () (= @t137 0)) % 0.47/0.87 (define @t349 () (not @t348)) % 0.47/0.87 (define @t350 () (|tptp.'fun_app$e'| |tptp.'pred$'| @t126)) % 0.47/0.87 (define @t351 () (|tptp.'fun_app$c'| @t20 (|tptp.'fun_app$e'| @t327 @t350))) % 0.47/0.87 (define @t352 () (= @t128 (+ (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t350) 1))) % 0.47/0.87 (define @t353 () (= @t128 0)) % 0.47/0.87 (define @t354 () (tptp.def_8 @t125 @t126)) % 0.47/0.87 (define @t355 () (|tptp.'fun_app$d'| @t15 @t332)) % 0.47/0.87 (define @t356 () (tptp.def_7 @t332 @t125 @t126)) % 0.47/0.87 (define @t357 () (tptp.def_10 @t125 @t126)) % 0.47/0.87 (define @t358 () (tptp.def_9 @t332 @t125 @t126)) % 0.47/0.87 (define @t359 () (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| @t93)) % 0.47/0.87 (define @t360 () (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| @t22)) % 0.47/0.87 (define @t361 () (|tptp.'sub$'| |tptp.'one$'| @t206)) % 0.47/0.87 (define @t362 () (|tptp.'sub$'| @t206 |tptp.'one$'|)) % 0.47/0.87 (define @t363 () (|tptp.'sub$'| @t206 @t244)) % 0.47/0.87 (define @t364 () (- @t241 @t246)) % 0.47/0.87 (define @t365 () (|tptp.'sub$'| @t244 @t206)) % 0.47/0.87 (define @t366 () (- 2)) % 0.47/0.87 (define @t367 () (= @t2 @t267)) % 0.47/0.87 (define @t368 () (+ @t267 @t1)) % 0.47/0.87 (define @t369 () (+ @t2 @t1)) % 0.47/0.87 (define @t370 () (= @t369 @t368)) % 0.47/0.87 (define @t371 () (= @t1 @t267)) % 0.47/0.87 (define @t372 () (+ @t2 @t267)) % 0.47/0.87 (define @t373 () (= @t369 @t372)) % 0.47/0.87 (define @t374 () (|tptp.'bit0$'| @t244)) % 0.47/0.87 (define @t375 () (|tptp.'bit0$'| @t206)) % 0.47/0.87 (define @t376 () (+ @t72 @t96)) % 0.47/0.87 (define @t377 () (+ @t376 1)) % 0.47/0.87 (define @t378 () (+ @t72 @t97)) % 0.47/0.87 (define @t379 () (+ @t72 @t137)) % 0.47/0.87 (define @t380 () (< @t376 @t379)) % 0.47/0.87 (define @t381 () (|tptp.'bit1$'| @t244)) % 0.47/0.87 (define @t382 () (|tptp.'bit1$'| @t206)) % 0.47/0.87 (define @t383 () (+ @t96 @t137)) % 0.47/0.87 (define @t384 () (- @t72 @t383)) % 0.47/0.87 (define @t385 () (< @t72 @t383)) % 0.47/0.87 (define @t386 () (not @t385)) % 0.47/0.87 (define @t387 () (|tptp.'nat$'| @t379)) % 0.47/0.87 (define @t388 () (+ @t96 @t72)) % 0.47/0.87 (define @t389 () (+ @t2 @t2)) % 0.47/0.87 (define @t390 () (= @t1 0)) % 0.47/0.87 (define @t391 () (+ @t1 @t2)) % 0.47/0.87 (define @t392 () (< @t1 @t267)) % 0.47/0.87 (define @t393 () (< @t369 @t372)) % 0.47/0.87 (define @t394 () (< @t2 @t267)) % 0.47/0.87 (define @t395 () (< @t369 @t368)) % 0.47/0.87 (define @t396 () (|tptp.'plus$'| @t206 @t244)) % 0.47/0.87 (define @t397 () (|tptp.'numeral$'| @t396)) % 0.47/0.87 (define @t398 () (+ @t241 @t246)) % 0.47/0.87 (define @t399 () (+ @t112 @t1)) % 0.47/0.87 (define @t400 () (- @t369)) % 0.47/0.87 (define @t401 () (+ @t72 @t128)) % 0.47/0.87 (define @t402 () (< @t1 0)) % 0.47/0.87 (define @t403 () (< 0 @t1)) % 0.47/0.87 (define @t404 () (|tptp.'plus$'| @t206 |tptp.'one$'|)) % 0.47/0.87 (define @t405 () (|tptp.'numeral$'| @t404)) % 0.47/0.87 (define @t406 () (+ @t241 1)) % 0.47/0.87 (define @t407 () (|tptp.'numeral$'| @t375)) % 0.47/0.87 (define @t408 () (|tptp.'numeral$'| @t382)) % 0.47/0.87 (define @t409 () (|tptp.'dbl$'| @t363)) % 0.47/0.87 (define @t410 () (|tptp.'plus$'| |tptp.'one$'| @t206)) % 0.47/0.87 (define @t411 () (|tptp.'numeral$'| @t410)) % 0.47/0.87 (define @t412 () (+ 1 @t241)) % 0.47/0.87 (define @t413 () (+ @t92 1)) % 0.47/0.87 (define @t414 () (+ @t1 @t267)) % 0.47/0.87 (define @t415 () (- @t2 @t414)) % 0.47/0.87 (define @t416 () (- @t372 @t1)) % 0.47/0.87 (define @t417 () (= @t2 @t414)) % 0.47/0.87 (define @t418 () (< @t137 @t128)) % 0.47/0.87 (define @t419 () (+ @t137 @t96)) % 0.47/0.87 (define @t420 () (@list @t22 @t94 @t12 @t126)) % 0.47/0.87 (define @t421 () (< @t376 @t96)) % 0.47/0.87 (define @t422 () (not @t421)) % 0.47/0.87 (define @t423 () (< @t376 @t72)) % 0.47/0.87 (define @t424 () (not @t423)) % 0.47/0.87 (define @t425 () (@list @t244)) % 0.47/0.87 (define @t426 () (+ @t1 @t269)) % 0.47/0.87 (define @t427 () (< @t372 @t426)) % 0.47/0.87 (define @t428 () (- @t376 @t379)) % 0.47/0.87 (define @t429 () (- @t376 @t419)) % 0.47/0.87 (define @t430 () (< @t376 @t419)) % 0.47/0.87 (define @t431 () (+ @t2 @t414)) % 0.47/0.87 (define @t432 () (+ @t92 @t96)) % 0.47/0.87 (define @t433 () (+ @t241 @t241)) % 0.47/0.87 (define @t434 () (< @t369 0)) % 0.47/0.87 (define @t435 () (+ @t2 1)) % 0.47/0.87 (define @t436 () (= @t369 0)) % 0.47/0.87 (define @t437 () (or (and @t314 @t193) (and @t73 (= @t96 @t88)))) % 0.47/0.87 (define @t438 () (= @t96 (+ @t379 1))) % 0.47/0.87 (define @t439 () (exists @t142 @t438)) % 0.47/0.87 (define @t440 () (< @t72 @t376)) % 0.47/0.87 (define @t441 () (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'nat$'| @t2))) % 0.47/0.87 (define @t442 () (<= 0 @t2)) % 0.47/0.87 (define @t443 () (@list @t13 @t12)) % 0.47/0.87 (define @t444 () (|tptp.'fun_app$c'| (|tptp.'case_nat$a'| @t332 @t125) @t126)) % 0.47/0.87 (define @t445 () (@list @t332 @t125 @t126)) % 0.47/0.87 (define @t446 () (|tptp.'fun_app$c'| @t125 @t350)) % 0.47/0.87 (define @t447 () (@list @t125 @t126)) % 0.47/0.87 (define @t448 () (@var "B" tptp.tlbool)) % 0.47/0.87 (define @t449 () (|tptp.'gF_advice$'| |tptp.'phi$'| |tptp.'x$'|)) % 0.47/0.87 (define @t450 () (|tptp.'semantics_ltln$'| @t28 @t449)) % 0.47/0.87 (define @t451 () (|tptp.'semantics_ltln$'| |tptp.'w$'| (|tptp.'fun_app$i'| |tptp.'next_ltln$'| @t449))) % 0.47/0.87 (define @t452 () (= @t451 @t450)) % 0.47/0.87 (assume @p1 (forall @t4 (= (|tptp.'fun_app$'| (|tptp.'uub$'| @t2) @t1) @t3))) % 0.47/0.87 (assume @p2 (forall @t4 (= (|tptp.'fun_app$a'| (|tptp.'uuc$'| @t2) @t1) @t5))) % 0.47/0.87 (assume @p3 (forall @t9 (= (|tptp.'fun_app$b'| @t8 @t7) (|tptp.'semantics_ltln$'| @t7 @t6)))) % 0.47/0.87 (assume @p4 (forall (@list @t10 @t7) (= (|tptp.'fun_app$b'| @t11 @t7) (|tptp.'member$'| @t7 @t10)))) % 0.47/0.87 (assume @p5 (forall (@list @t15 @t13 @t12) (= (|tptp.'fun_app$c'| (|tptp.'uuh$'| @t15 @t13) @t12) (|tptp.'fun_app$d'| @t15 @t14)))) % 0.47/0.87 (assume @p6 (forall (@list @t17 @t13 @t12) (= (|tptp.'fun_app$e'| (|tptp.'uug$'| @t17 @t13) @t12) (|tptp.'fun_app$f'| @t17 @t16)))) % 0.47/0.87 (assume @p7 (forall (@list @t20 @t18 @t12) (= (|tptp.'fun_app$c'| (|tptp.'uuf$'| @t20 @t18) @t12) (|tptp.'fun_app$c'| @t20 @t19)))) % 0.47/0.87 (assume @p8 (forall (@list @t21 @t18 @t12) (= (|tptp.'fun_app$e'| (|tptp.'uue$'| @t21 @t18) @t12) (|tptp.'fun_app$e'| @t21 @t19)))) % 0.47/0.87 (assume @p9 (forall @t23 (= (|tptp.'fun_app$e'| |tptp.'uud$'| @t22) @t22))) % 0.47/0.87 (assume @p10 (forall @t23 (= (|tptp.'fun_app$c'| |tptp.'uui$'| @t22) false))) % 0.47/0.87 (assume @p11 (forall @t23 (= (|tptp.'fun_app$c'| |tptp.'uuj$'| @t22) true))) % 0.47/0.87 (assume @p12 (not (|tptp.'semantics_ltln$'| @t28 (|tptp.'gF_advice$'| (|tptp.'fun_app$g'| (|tptp.'fun_app$h'| |tptp.'af_letter$'| @t26) @t25) |tptp.'x$'|)))) % 0.47/0.87 (assume @p13 (|tptp.'semantics_ltln$'| |tptp.'w$'| (|tptp.'gF_advice$'| (|tptp.'fun_app$i'| |tptp.'unf$'| @t26) |tptp.'x$'|))) % 0.47/0.87 (assume @p14 (=> (|tptp.'semantics_ltln$'| |tptp.'w$'| (|tptp.'gF_advice$'| (|tptp.'fun_app$i'| |tptp.'unf$'| |tptp.'phi$'|) |tptp.'x$'|)) (|tptp.'semantics_ltln$'| @t28 (|tptp.'gF_advice$'| (|tptp.'fun_app$g'| (|tptp.'fun_app$h'| |tptp.'af_letter$'| |tptp.'phi$'|) @t25) |tptp.'x$'|)))) % 0.47/0.87 (assume @p15 (forall @t30 (= (|tptp.'suffix$'| @t24 @t29) @t29))) % 0.47/0.87 (assume @p16 (forall @t34 (= (|tptp.'semantics_ltln$'| @t29 @t33) (|tptp.'semantics_ltln$'| @t32 @t31)))) % 0.47/0.87 (assume @p17 (forall @t38 (=> @t37 (|tptp.'semantics_ltln$'| @t29 (|tptp.'gF_advice$'| @t36 @t35))))) % 0.47/0.87 (assume @p18 (forall (@list @t6 @t31) (= (= @t39 @t33) (= @t6 @t31)))) % 0.47/0.87 (assume @p19 (forall @t41 (= (|tptp.'gF_advice$'| @t39 @t40) (|tptp.'fun_app$i'| |tptp.'next_ltln$'| (|tptp.'gF_advice$'| @t6 @t40))))) % 0.47/0.87 (assume @p20 @t44) % 0.47/0.87 (assume @p21 (not (= 0 1))) % 0.47/0.87 (assume @p22 @t47) % 0.47/0.87 (assume @p23 (forall @t34 (= (|tptp.'semantics_ltln$'| @t29 @t36) @t48))) % 0.47/0.87 (assume @p24 (forall @t51 (= @t50 @t49))) % 0.47/0.87 (assume @p25 (forall @t51 (= (= 1 @t2) (= @t2 1)))) % 0.47/0.87 (assume @p26 (forall @t46 (= (|tptp.'language_ltln$'| @t6) (|tptp.'collect$'| @t8)))) % 0.47/0.87 (assume @p27 (forall @t30 (= @t29 (|tptp.'build$'| @t52 @t32)))) % 0.47/0.87 (assume @p28 (forall (@list @t54 @t7 @t55 @t53) (=> (|tptp.'semantics_ltln$'| @t59 @t58) (|tptp.'semantics_ltln$'| @t7 (|tptp.'gF_advice$'| @t57 @t53))))) % 0.47/0.87 (assume @p29 (forall @t70 (=> (and @t69 @t67) @t66))) % 0.47/0.87 (assume @p30 (= 1 1)) % 0.47/0.87 (assume @p31 (forall (@list @t54 @t7 @t55) (= (|tptp.'semantics_ltln$'| @t59 @t55) (|tptp.'semantics_ltln$'| @t7 @t57)))) % 0.47/0.87 (assume @p32 @t71) % 0.47/0.87 (assume @p33 (forall @t23 (=> (and @t75 (=> @t74 false)) false))) % 0.47/0.87 (assume @p34 (forall @t80 (= @t79 @t78))) % 0.47/0.87 (assume @p35 (forall @t80 (=> @t78 @t79))) % 0.47/0.87 (assume @p36 (= (|tptp.'dbl_inc$'| 0) 1)) % 0.47/0.87 (assume @p37 (forall (@list @t54 @t7 @t82 @t81) (= (= @t59 (|tptp.'build$'| @t82 @t81)) (and (= @t54 @t82) (= @t7 @t81))))) % 0.47/0.87 (assume @p38 (forall (@list @t68 @t62 @t55) (=> @t69 @t85))) % 0.47/0.87 (assume @p39 (forall (@list @t54 @t7) (= (|tptp.'fun_app$j'| @t59 @t24) @t54))) % 0.47/0.87 (assume @p40 (forall (@list @t68 @t62 @t65 @t61) (=> @t69 (= (|tptp.'semantics_ltln$'| @t65 @t63) (|tptp.'semantics_ltln$'| @t65 @t61))))) % 0.47/0.87 (assume @p41 (forall (@list @t68 @t62 @t55 @t61 @t60) (=> (and @t69 @t87) @t86))) % 0.47/0.87 (assume @p42 (forall @t30 (= (|tptp.'build$'| @t52 (|tptp.'suffix$'| (|tptp.'nat$'| @t88) @t29)) @t29))) % 0.47/0.87 (assume @p43 (forall @t90 (=> @t69 @t89))) % 0.47/0.87 (assume @p44 (forall (@list @t29 @t31 @t82 @t53) (=> (|tptp.'semantics_ltln$'| @t29 (|tptp.'fG_advice$'| (|tptp.'fun_app$g'| @t77 @t82) @t53)) (|tptp.'semantics_ltln$'| (|tptp.'build$'| @t82 @t29) @t91)))) % 0.47/0.87 (assume @p45 (= (|tptp.'dbl_dec$'| 1) 1)) % 0.47/0.87 (assume @p46 (= (|tptp.'dbl$'| 0) 0)) % 0.47/0.87 (assume @p47 (forall (@list @t22 @t42 @t65) (= (|tptp.'suffix$'| @t93 (|tptp.'build$'| @t42 @t65)) (|tptp.'suffix$'| @t22 @t65)))) % 0.47/0.87 (assume @p48 (forall @t99 (= (|tptp.'build$'| (|tptp.'fun_app$j'| @t29 @t94) (|tptp.'suffix$'| @t98 @t29)) @t95))) % 0.47/0.87 (assume @p49 (= (|tptp.'dbl_inc$'| @t100) @t100)) % 0.47/0.87 (assume @p50 (forall @t70 (=> (and @t69 @t66) @t102))) % 0.47/0.87 (assume @p51 (forall @t23 (= @t103 @t73))) % 0.47/0.87 (assume @p52 (forall @t106 (= @t105 @t104))) % 0.47/0.87 (assume @p53 (forall (@list @t29 @t107) (= (|tptp.'member$'| @t29 @t108) (|tptp.'fun_app$b'| @t107 @t29)))) % 0.47/0.87 (assume @p54 (forall (@list @t10) (= (|tptp.'collect$'| @t11) @t10))) % 0.47/0.87 (assume @p55 (forall (@list @t109 @t107) (=> (forall (@list @t65) (= (|tptp.'fun_app$b'| @t109 @t65) (|tptp.'fun_app$b'| @t107 @t65))) (= (|tptp.'collect$'| @t109) @t108)))) % 0.47/0.87 (assume @p56 (forall @t4 (= @t113 @t110))) % 0.47/0.87 (assume @p57 (forall @t51 (= (- @t112) @t2))) % 0.47/0.87 (assume @p58 (forall @t51 (= (= @t112 @t2) @t49))) % 0.47/0.87 (assume @p59 (forall @t51 (= (= @t2 @t112) @t49))) % 0.47/0.87 (assume @p60 (forall @t51 (= (= @t112 0) @t49))) % 0.47/0.87 (assume @p61 (forall @t51 (= (= 0 @t112) @t50))) % 0.47/0.87 (assume @p62 (forall @t4 (= (< @t112 @t111) @t114))) % 0.47/0.87 (assume @p63 (forall @t23 (= @t115 false))) % 0.47/0.87 (assume @p64 (forall @t23 (= @t74 @t116))) % 0.47/0.87 (assume @p65 (forall @t106 (= @t118 @t117))) % 0.47/0.87 (assume @p66 (forall @t106 (=> @t117 @t118))) % 0.47/0.87 (assume @p67 (forall @t23 (< @t72 @t92))) % 0.47/0.87 (assume @p68 (forall @t51 (= (< @t2 @t112) @t119))) % 0.47/0.87 (assume @p69 (forall @t51 (= (< @t112 @t2) @t120))) % 0.47/0.87 (assume @p70 (forall @t51 (= (< 0 @t112) @t119))) % 0.47/0.87 (assume @p71 (forall @t51 (= (< @t112 0) @t120))) % 0.47/0.87 (assume @p72 (forall @t23 @t121)) % 0.47/0.87 (assume @p73 (forall @t23 (= @t122 @t73))) % 0.47/0.87 (assume @p74 (= (|tptp.'dbl_dec$'| 0) @t100)) % 0.47/0.87 (assume @p75 (forall @t106 (=> @t124 (= @t123 @t104)))) % 0.47/0.87 (assume @p76 (forall (@list @t22 @t94 @t125) (=> (and @t117 (forall @t131 (=> (= @t96 @t129) @t127)) (forall @t131 (=> (and (< @t128 @t96) (|tptp.'fun_app$c'| @t125 @t130)) @t127))) (|tptp.'fun_app$c'| @t125 @t22)))) % 0.47/0.87 (assume @p77 (forall @t106 (=> (and @t134 @t133 (=> @t132 false)) false))) % 0.47/0.87 (assume @p78 (forall @t143 (=> (forall @t142 (=> @t141 @t139)) @t135))) % 0.47/0.87 (assume @p79 (forall @t143 (=> (forall @t142 (=> (forall @t131 (=> @t138 @t136)) @t140)) @t135))) % 0.47/0.87 (assume @p80 (forall @t23 (=> @t144 false))) % 0.47/0.87 (assume @p81 (forall (@list @t22 @t94 @t145) (=> (and @t117 (forall @t131 (|tptp.'fun_app$c'| @t146 @t130)) (forall (@list @t126 @t147 @t101) (=> (and (< @t128 @t148) (< @t148 (|tptp.'fun_app$k'| |tptp.'of_nat$'| @t101)) (|tptp.'fun_app$c'| @t146 @t147) (|tptp.'fun_app$c'| (|tptp.'fun_app$n'| @t145 @t147) @t101)) (|tptp.'fun_app$c'| @t146 @t101)))) (|tptp.'fun_app$c'| (|tptp.'fun_app$n'| @t145 @t22) @t94)))) % 0.47/0.87 (assume @p82 (forall @t150 (=> (and @t117 @t149) (< @t92 @t137)))) % 0.47/0.87 (assume @p83 (forall @t106 (=> @t117 @t134))) % 0.47/0.87 (assume @p84 (forall @t106 (=> @t117 (not @t151)))) % 0.47/0.87 (assume @p85 (forall @t23 @t152)) % 0.47/0.87 (assume @p86 (forall @t106 (=> @t118 @t117))) % 0.47/0.87 (assume @p87 (forall @t106 (=> (and @t124 @t123) @t151))) % 0.47/0.87 (assume @p88 (forall @t106 (= @t156 (exists @t142 (and @t155 @t153))))) % 0.47/0.87 (assume @p89 (forall @t162 (= @t161 (and @t159 (forall @t142 (=> @t158 @t157)))))) % 0.47/0.87 (assume @p90 (forall @t106 (= @t124 @t163))) % 0.47/0.87 (assume @p91 (forall @t106 (= @t134 (or @t117 @t132)))) % 0.47/0.87 (assume @p92 (forall @t23 (not (= @t72 @t92)))) % 0.47/0.87 (assume @p93 (forall @t106 (= @t123 (or @t117 @t104)))) % 0.47/0.87 (assume @p94 (forall @t162 (= @t164 (or @t159 (exists @t142 (and @t158 @t157)))))) % 0.47/0.87 (assume @p95 (forall @t106 (=> @t105 @t104))) % 0.47/0.87 (assume @p96 (forall @t106 (=> @t117 @t123))) % 0.47/0.87 (assume @p97 (forall @t106 (=> (and @t123 @t133 (=> @t104 false)) false))) % 0.47/0.87 (assume @p98 (forall @t106 (=> (and @t117 (not (= @t92 @t96))) @t156))) % 0.47/0.87 (assume @p99 (forall @t106 (=> (and @t156 @t165) false))) % 0.47/0.87 (assume @p100 (forall @t106 (=> @t156 @t117))) % 0.47/0.87 (assume @p101 (forall @t106 (=> (and @t117 (=> (= @t96 @t92) false) @t165) false))) % 0.47/0.87 (assume @p102 (forall @t169 (=> @t168 (= @t167 @t149)))) % 0.47/0.87 (assume @p103 (forall @t173 (=> @t172 (= @t171 @t149)))) % 0.47/0.87 (assume @p104 (forall @t169 (=> (and @t168 @t149) @t167))) % 0.47/0.87 (assume @p105 (forall @t173 (=> (and @t172 @t149) @t171))) % 0.47/0.87 (assume @p106 (forall @t4 (=> (and (not @t110) (=> @t3 false) (=> @t114 false)) false))) % 0.47/0.87 (assume @p107 (forall @t4 (= (< @t112 @t1) (< @t111 @t2)))) % 0.47/0.87 (assume @p108 (forall @t4 (= (< @t2 @t111) (< @t1 @t112)))) % 0.47/0.87 (assume @p109 (forall @t4 (= @t174 (= @t111 @t2)))) % 0.47/0.87 (assume @p110 (forall @t4 (= @t176 @t175))) % 0.47/0.87 (assume @p111 (< @t100 1)) % 0.47/0.87 (assume @p112 (not (< 1 @t100))) % 0.47/0.87 (assume @p113 (forall @t106 (= @t123 (or @t73 (exists @t142 (and (= @t72 @t154) @t177)))))) % 0.47/0.87 (assume @p114 (forall @t23 (=> @t116 @t180))) % 0.47/0.87 (assume @p115 (forall @t162 (= @t161 (and @t183 (forall @t142 (=> @t158 @t182)))))) % 0.47/0.87 (assume @p116 (forall @t23 (= @t116 @t180))) % 0.47/0.87 (assume @p117 (forall @t162 (= @t164 (or @t183 (exists @t142 (and @t158 @t182)))))) % 0.47/0.87 (assume @p118 (< @t100 0)) % 0.47/0.87 (assume @p119 (not (< 0 @t100))) % 0.47/0.87 (assume @p120 (forall @t162 (=> (and @t116 (|tptp.'fun_app$c'| @t13 @t27) (forall @t142 (=> (and @t184 @t157) @t182))) @t159))) % 0.47/0.87 (assume @p121 (forall @t41 (= (|tptp.'fG_advice$'| @t39 @t40) (|tptp.'fun_app$i'| |tptp.'next_ltln$'| (|tptp.'fG_advice$'| @t6 @t40))))) % 0.47/0.87 (assume @p122 (not (= 1 @t100))) % 0.47/0.87 (assume @p123 (not @t185)) % 0.47/0.87 (assume @p124 (forall (@list @t22 @t7 @t55 @t53) (=> (|tptp.'semantics_ltln$'| @t186 (|tptp.'fG_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t55 (|tptp.'subsequence$'| @t7 @t24 @t22)) @t53)) (|tptp.'semantics_ltln$'| @t7 (|tptp.'fG_advice$'| @t55 @t53))))) % 0.47/0.87 (assume @p125 (not (< 1 1))) % 0.47/0.87 (assume @p126 (forall @t23 (=> @t74 @t180))) % 0.47/0.87 (assume @p127 (forall @t23 (not @t187))) % 0.47/0.87 (assume @p128 (forall @t23 (=> @t187 false))) % 0.47/0.87 (assume @p129 (forall @t23 (=> @t188 false))) % 0.47/0.87 (assume @p130 (forall @t143 (=> (and @t135 (forall @t142 (=> @t190 @t140))) @t189))) % 0.47/0.87 (assume @p131 (forall (@list @t191 @t94 @t12) (=> (and (forall @t131 (|tptp.'fun_app$c'| @t192 @t24)) (forall @t131 (|tptp.'fun_app$c'| (|tptp.'fun_app$n'| @t191 @t24) @t130)) (forall (@list @t126 @t147) (=> (|tptp.'fun_app$c'| @t192 @t147) (|tptp.'fun_app$c'| (|tptp.'fun_app$n'| @t191 @t130) (|tptp.'nat$'| (+ @t148 1)))))) (|tptp.'fun_app$c'| (|tptp.'fun_app$n'| @t191 @t94) @t12)))) % 0.47/0.87 (assume @p132 (forall @t143 (=> (and @t189 (forall @t142 (=> @t140 @t190))) @t135))) % 0.47/0.87 (assume @p133 (forall @t23 (=> (and @t75 (forall @t179 (=> @t178 false))) false))) % 0.47/0.87 (assume @p134 (forall @t106 (=> @t178 @t74))) % 0.47/0.87 (assume @p135 (forall @t23 (not @t188))) % 0.47/0.87 (assume @p136 (forall @t143 (=> (and @t189 (forall @t142 (=> (and @t184 @t141) @t139))) @t135))) % 0.47/0.87 (assume @p137 (forall @t106 (=> @t117 (not @t193)))) % 0.47/0.87 (assume @p138 (forall @t23 (=> @t115 false))) % 0.47/0.87 (assume @p139 (forall @t23 @t194)) % 0.47/0.87 (assume @p140 (forall @t23 (= @t195 @t73))) % 0.47/0.87 (assume @p141 (forall @t23 (=> @t75 @t116))) % 0.47/0.87 (assume @p142 (forall (@list @t54 @t7 @t12) (= (|tptp.'fun_app$j'| @t59 @t181) (|tptp.'fun_app$j'| @t7 @t12)))) % 0.47/0.87 (assume @p143 (forall @t90 (= @t89 @t197))) % 0.47/0.87 (assume @p144 (forall @t90 (=> @t197 @t89))) % 0.47/0.87 (assume @p145 (not (= 0 @t100))) % 0.47/0.87 (assume @p146 (not (< 1 0))) % 0.47/0.87 (assume @p147 (< 0 1)) % 0.47/0.87 (assume @p148 (= 1 @t88)) % 0.47/0.87 (assume @p149 (forall (@list @t29 @t31 @t35 @t61) (=> (and (exists @t202 @t201) (exists @t202 @t200)) (exists @t202 (and @t201 @t200))))) % 0.47/0.87 (assume @p150 (forall (@list @t29 @t31 @t35 @t126) (=> @t37 @t203))) % 0.47/0.87 (assume @p151 (forall @t38 (=> @t205 (exists @t131 @t203)))) % 0.47/0.87 (assume @p152 (forall @t4 (=> @t3 (< @t111 @t112)))) % 0.47/0.87 (assume @p153 (forall @t34 (= (|tptp.'semantics_ltln$'| @t29 @t204) @t48))) % 0.47/0.87 (assume @p154 (forall @t38 (=> @t37 @t205))) % 0.47/0.87 (assume @p155 (forall @t208 (= (|tptp.'fun_app$o'| @t207 @t206) false))) % 0.47/0.87 (assume @p156 (forall @t51 (= (< @t2 @t2) false))) % 0.47/0.87 (assume @p157 (forall @t4 (=> @t110 @t113))) % 0.47/0.87 (assume @p158 (forall @t46 (= (|tptp.'fun_app$i'| |tptp.'id$'| @t6) @t6))) % 0.47/0.87 (assume @p159 (forall (@list @t21) (= @t211 (and (= (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t21 @t24)) 0) (forall @t179 (< @t210 (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t21 @t98)))))))) % 0.47/0.87 (assume @p160 (forall @t51 (=> @t119 @t213))) % 0.47/0.87 (assume @p161 (forall @t216 (= (|tptp.'f$'| @t215 @t214) (|tptp.'f$'| @t6 @t214)))) % 0.47/0.87 (assume @p162 (forall @t216 (= (|tptp.'g$'| @t215 @t214) (|tptp.'g$'| @t6 @t214)))) % 0.47/0.87 (assume @p163 (forall @t216 (= (|tptp.'f_G$'| @t215 @t214) (|tptp.'f_G$'| @t6 @t214)))) % 0.47/0.87 (assume @p164 (forall @t51 (= (|tptp.'sgn$'| @t212) @t212))) % 0.47/0.87 (assume @p165 (= (|tptp.'sgn$'| 0) 0)) % 0.47/0.87 (assume @p166 (= (|tptp.'sgn$'| 1) 1)) % 0.47/0.87 (assume @p167 (forall @t51 (= (|tptp.'sgn$'| @t112) @t217))) % 0.47/0.87 (assume @p168 (forall @t51 (= (< @t212 0) @t119))) % 0.47/0.87 (assume @p169 (forall @t51 (= (< 0 @t212) @t120))) % 0.47/0.87 (assume @p170 (forall @t51 @t219)) % 0.47/0.87 (assume @p171 (forall @t222 (=> (and (= @t220 (|tptp.'f_G$'| @t31 @t65)) (= @t220 (|tptp.'g$'| @t31 @t65))) (= @t221 (|tptp.'semantics_ltln$'| @t65 (|tptp.'fG_advice$'| @t31 @t220)))))) % 0.47/0.87 (assume @p172 (forall (@list @t21 @t94 @t12) (=> (and @t211 (= @t210 (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t21 @t12)))) (= @t96 @t137)))) % 0.47/0.87 (assume @p173 (forall @t51 (= @t223 @t49))) % 0.47/0.87 (assume @p174 (forall @t4 (=> (and (not @t225) (not (= @t224 0)) (not @t223)) (= @t224 @t217)))) % 0.47/0.87 (assume @p175 (= (|tptp.'sgn$'| @t100) @t100)) % 0.47/0.87 (assume @p176 (forall @t51 (= @t218 @t120))) % 0.47/0.87 (assume @p177 (forall (@list @t226) (= (forall (@list @t31) (= (|tptp.'fun_app$i'| @t226 @t31) @t31)) (= @t226 |tptp.'id$'|)))) % 0.47/0.87 (assume @p178 (forall @t51 (= @t213 @t119))) % 0.47/0.87 (assume @p179 (forall @t51 (and (=> @t49 @t223) (=> (not @t49) (and @t219 (=> (not @t120) @t213)))))) % 0.47/0.87 (assume @p180 (forall @t228 (= (|tptp.'f_G$'| @t6 @t227) (|tptp.'f_G$'| @t6 @t65)))) % 0.47/0.87 (assume @p181 (forall @t9 (= (|tptp.'f$'| @t39 @t7) @t229))) % 0.47/0.87 (assume @p182 (forall @t9 (= (|tptp.'g$'| @t39 @t7) @t230))) % 0.47/0.87 (assume @p183 (forall @t9 (= (|tptp.'f_G$'| @t39 @t7) @t231))) % 0.47/0.87 (assume @p184 (forall @t216 (= (|tptp.'g_F$'| @t215 @t214) (|tptp.'g_F$'| @t6 @t214)))) % 0.47/0.87 (assume @p185 (forall @t228 (= (|tptp.'g_F$'| @t6 @t227) (|tptp.'g_F$'| @t6 @t65)))) % 0.47/0.87 (assume @p186 (forall @t9 (= (|tptp.'g_F$'| @t39 @t7) @t232))) % 0.47/0.87 (assume @p187 (forall @t222 (=> (and (= @t220 (|tptp.'f$'| @t31 @t65)) (= @t220 (|tptp.'g_F$'| @t31 @t65))) (= @t221 (|tptp.'semantics_ltln$'| @t65 (|tptp.'gF_advice$'| @t31 @t220)))))) % 0.47/0.87 (assume @p188 (forall @t9 (= @t234 (= @t232 @t229)))) % 0.47/0.87 (assume @p189 (forall @t9 (= @t236 (= @t231 @t230)))) % 0.47/0.87 (assume @p190 (forall @t23 (=> @t116 (and (=> @t103 @t240) (=> @t239 (= @t238 @t72)))))) % 0.47/0.87 (assume @p191 (forall @t208 (= (|tptp.'dbl_inc$'| @t242) (- (|tptp.'dbl_dec$'| @t241))))) % 0.47/0.87 (assume @p192 (forall @t208 (= (|tptp.'dbl_dec$'| @t242) (- @t243)))) % 0.47/0.87 (assume @p193 (forall @t247 (= (= @t241 @t246) @t245))) % 0.47/0.87 (assume @p194 (forall @t247 (= (< @t241 @t246) @t248))) % 0.47/0.87 (assume @p195 (forall @t51 (= (- @t2 @t2) 0))) % 0.47/0.87 (assume @p196 (forall @t51 (= (- @t2 0) @t2))) % 0.47/0.87 (assume @p197 (forall @t247 (= (= @t242 @t249) @t245))) % 0.47/0.87 (assume @p198 (forall @t4 (= (- @t5) @t250))) % 0.47/0.87 (assume @p199 (forall @t23 (and (=> @t144 @t71) (=> @t152 (= (- @t72 @t72) 0))))) % 0.47/0.87 (assume @p200 (forall @t23 (and (=> @t116 @t71) (=> @t195 (= (- 0 @t72) 0))))) % 0.47/0.87 (assume @p201 (forall @t150 (and (=> @t260 (and (=> @t256 @t71) (=> @t257 (and (=> @t117 (= 0 @t255)) (=> @t124 (= 0 @t252)))))) (=> (not @t260) (and (=> @t156 (and (=> @t256 (= @t259 0)) (=> @t257 (and (=> @t117 (= @t259 @t255)) (=> @t124 (= @t259 @t252)))))) (=> @t258 (and (=> @t256 (= @t254 0)) (=> @t257 (and (=> @t117 (= @t254 @t255)) (=> @t124 (= @t254 @t252))))))))))) % 0.47/0.87 (assume @p202 (forall @t106 (and (=> @t118 (and @t262 (=> @t124 (= 0 @t251)))) (=> (not @t118) (and (=> @t117 (= @t261 0)) (=> @t124 (= @t261 @t251))))))) % 0.47/0.87 (assume @p203 (forall @t4 (= (< 0 @t5) @t114))) % 0.47/0.87 (assume @p204 (= (- 1 1) 0)) % 0.47/0.87 (assume @p205 (forall @t247 (= (< @t242 @t249) @t263))) % 0.47/0.87 (assume @p206 (forall @t51 (= (- 0 @t2) @t112))) % 0.47/0.87 (assume @p207 (forall @t106 (= (and (=> @t117 @t185) (=> @t124 (< 0 @t251))) @t132))) % 0.47/0.87 (assume @p208 (forall @t23 (and (=> @t264 @t265) (=> (not @t264) (= (- @t92 1) @t72))))) % 0.47/0.87 (assume @p209 (forall @t208 (= (|tptp.'dbl$'| @t242) (- @t266)))) % 0.47/0.87 (assume @p210 (= (- @t100 @t100) 0)) % 0.47/0.87 (assume @p211 (forall @t23 (=> @t116 (and (=> @t122 @t240) (=> (not @t122) (= (+ (- @t72 @t88) 1) @t72)))))) % 0.47/0.87 (assume @p212 (forall @t4 (= @t110 (= @t5 0)))) % 0.47/0.87 (assume @p213 (forall @t273 (=> @t272 (< @t270 @t268)))) % 0.47/0.87 (assume @p214 (forall @t273 (=> @t275 (= @t3 @t271)))) % 0.47/0.87 (assume @p215 (forall @t277 (=> @t3 (< @t276 (- @t267 @t2))))) % 0.47/0.87 (assume @p216 (forall @t277 (=> @t3 (< @t278 @t268)))) % 0.47/0.87 (assume @p217 (forall @t4 (= (- @t112 @t1) (- @t111 @t2)))) % 0.47/0.87 (assume @p218 (forall @t208 (not (= 0 @t241)))) % 0.47/0.87 (assume @p219 (forall @t23 (and (=> @t115 @t265) (=> @t194 (= (- @t72 0) @t72))))) % 0.47/0.87 (assume @p220 (forall @t106 (=> (and @t262 (=> @t124 (= @t251 0)) (=> @t132 @t71) (=> @t280 (= @t279 0))) @t104))) % 0.47/0.87 (assume @p221 (forall (@list @t20 @t94 @t12) (=> (and @t135 (forall @t131 (=> (|tptp.'fun_app$c'| @t20 @t130) @t136))) (and (=> @t149 @t189) (=> @t282 (|tptp.'fun_app$c'| @t20 (|tptp.'nat$'| @t281))))))) % 0.47/0.87 (assume @p222 (forall @t150 (=> (and @t117 @t153) (and (=> @t177 (and (=> @t158 @t185) (=> @t285 (< 0 @t283)))) (=> (not @t177) (and (=> @t158 (< @t284 0)) (=> @t285 (< @t284 @t283)))))))) % 0.47/0.87 (assume @p223 (forall @t150 (=> @t117 @t289))) % 0.47/0.87 (assume @p224 (forall @t247 (not (= @t242 @t246)))) % 0.47/0.87 (assume @p225 (forall @t247 (not (= @t241 @t249)))) % 0.47/0.87 (assume @p226 (forall @t150 (and (=> @t256 (and (=> @t289 @t71) (=> @t292 (and (=> @t153 @t295) (=> @t287 (= 0 @t290)))))) (=> @t257 (and (=> @t117 (and (=> @t289 @t294) (=> @t292 (and (=> @t153 (= @t255 @t291)) (=> @t287 (= @t255 @t290)))))) (=> @t124 (and (=> @t289 @t293) (=> @t292 (and (=> @t153 (= @t252 @t291)) (=> @t287 (= @t252 @t290))))))))))) % 0.47/0.87 (assume @p227 (forall @t277 (= @t297 @t296))) % 0.47/0.87 (assume @p228 (forall @t273 (=> @t275 (= @t110 @t298)))) % 0.47/0.87 (assume @p229 (forall @t4 (= @t3 (< @t5 0)))) % 0.47/0.87 (assume @p230 (forall @t208 (not (< @t241 0)))) % 0.47/0.87 (assume @p231 (forall @t208 (< 0 @t241))) % 0.47/0.87 (assume @p232 (forall @t208 (not (< @t241 1)))) % 0.47/0.87 (assume @p233 (forall @t208 (not (= 0 @t242)))) % 0.47/0.87 (assume @p234 (forall @t247 (not (< @t241 @t249)))) % 0.47/0.87 (assume @p235 (forall @t247 (< @t242 @t246))) % 0.47/0.87 (assume @p236 (forall @t106 (=> @t299 (and (=> @t132 @t288) (=> @t280 (< @t279 @t96)))))) % 0.47/0.87 (assume @p237 (forall @t106 (and (=> @t117 @t121) (=> @t124 (< @t251 @t92))))) % 0.47/0.87 (assume @p238 (forall @t106 (=> @t117 (and (=> @t163 (and (=> @t132 (= @t88 0)) (=> @t280 (= @t88 @t279)))) (=> (not @t163) (and (=> @t132 (= @t300 0)) (=> @t280 (= @t300 @t279)))))))) % 0.47/0.87 (assume @p239 (forall @t208 (not (= 1 @t242)))) % 0.47/0.87 (assume @p240 (forall @t208 (not (= @t241 @t100)))) % 0.47/0.87 (assume @p241 (forall @t106 (and (=> @t123 (and (=> @t303 @t71) (=> @t304 (and (=> @t103 @t295) (=> @t239 (= 0 @t301)))))) (=> @t305 (and (=> @t303 (= @t302 0)) (=> @t304 (and (=> @t103 (= @t302 @t291)) (=> @t239 (= @t302 @t301))))))))) % 0.47/0.87 (assume @p242 (forall @t216 (=> @t236 (|tptp.'fun_app$b'| @t235 @t214)))) % 0.47/0.87 (assume @p243 (forall @t216 (=> @t234 (|tptp.'fun_app$b'| @t233 @t214)))) % 0.47/0.87 (assume @p244 (forall @t208 (< @t242 0))) % 0.47/0.87 (assume @p245 (forall @t208 (not (< 0 @t242)))) % 0.47/0.87 (assume @p246 (forall @t208 (< @t242 1))) % 0.47/0.87 (assume @p247 (forall @t208 (< @t100 @t241))) % 0.47/0.87 (assume @p248 (forall @t208 (not (< @t241 @t100)))) % 0.47/0.87 (assume @p249 (forall @t208 (not (< 1 @t242)))) % 0.47/0.87 (assume @p250 (forall @t208 (not (< @t100 @t242)))) % 0.47/0.87 (assume @p251 (forall @t106 (=> @t116 (and (=> @t123 @t116) (=> @t305 (< @t302 @t72)))))) % 0.47/0.87 (assume @p252 (forall @t307 (and (=> @t158 (= (|tptp.'subsequence$'| @t186 @t24 @t24) @t306)) (=> @t285 (= (|tptp.'subsequence$'| @t186 @t24 (|tptp.'nat$'| @t283)) @t306))))) % 0.47/0.87 (assume @p253 (forall @t106 (=> @t116 (and (=> @t313 (and (=> @t311 @t71) (=> @t312 (and (=> @t103 (= 0 @t310)) (=> @t239 (= 0 @t308)))))) (=> (not @t313) (and (=> @t311 (= @t309 0)) (=> @t312 (and (=> @t103 (= @t309 @t310)) (=> @t239 (= @t309 @t308)))))))))) % 0.47/0.87 (assume @p254 (forall @t23 (=> @t116 (and (=> @t103 @t314) (=> @t239 (= @t72 @t238)))))) % 0.47/0.87 (assume @p255 (forall @t208 (= (- @t100 @t241) @t317))) % 0.47/0.87 (assume @p256 (forall @t208 (= (- @t241 @t100) @t316))) % 0.47/0.87 (assume @p257 (forall @t208 (= (< @t242 @t100) (not @t318)))) % 0.47/0.87 (assume @p258 (forall @t106 (and (=> @t123 (and (=> @t117 (= 0 @t321)) (=> @t124 (= 0 @t320)))) (=> @t305 (and (=> @t117 (= @t302 @t321)) (=> @t124 (= @t302 @t320))))))) % 0.47/0.87 (assume @p259 (forall (@list @t29 @t31 @t322 @t53) (=> (|tptp.'semantics_ltln$'| @t29 (|tptp.'fG_advice$'| (|tptp.'foldl$'| |tptp.'af_letter$'| @t31 @t322) @t53)) (|tptp.'semantics_ltln$'| (|tptp.'conc$'| @t322 @t29) @t91)))) % 0.47/0.87 (assume @p260 (forall (@list @t323 @t7 @t65) (= (= @t324 (|tptp.'conc$'| @t323 @t65)) (= @t7 @t65)))) % 0.47/0.87 (assume @p261 (forall @t208 (= (= 1 @t241) (= |tptp.'one$'| @t206)))) % 0.47/0.87 (assume @p262 (forall @t208 (= (= @t241 1) @t318))) % 0.47/0.87 (assume @p263 (forall @t208 (= (= @t100 @t242) @t318))) % 0.47/0.87 (assume @p264 (forall @t208 (= (= @t242 @t100) @t318))) % 0.47/0.87 (assume @p265 (forall @t208 (= (< 1 @t241) (|tptp.'fun_app$o'| (|tptp.'less$'| |tptp.'one$'|) @t206)))) % 0.47/0.87 (assume @p266 (forall (@list @t325 @t244) (=> (and (|tptp.'fun_app$o'| @t325 |tptp.'one$'|) (forall (@list @t326) (=> (|tptp.'fun_app$o'| @t325 @t326) (|tptp.'fun_app$o'| @t325 (|tptp.'inc$'| @t326))))) (|tptp.'fun_app$o'| @t325 @t244)))) % 0.47/0.87 (assume @p267 (forall (@list @t21 @t94 @t327 @t126) (= (|tptp.'fun_app$e'| @t21 @t328) (|tptp.'fun_app$e'| (|tptp.'case_nat$'| @t209 (|tptp.'uue$'| @t21 @t327)) @t126)))) % 0.47/0.87 (assume @p268 (forall @t331 (= @t330 (|tptp.'fun_app$c'| (|tptp.'case_nat$a'| @t329 (|tptp.'uuf$'| @t20 @t327)) @t126)))) % 0.47/0.87 (assume @p269 (forall (@list @t17 @t332 @t125 @t126) (= (|tptp.'fun_app$f'| @t17 @t333) (|tptp.'fun_app$e'| (|tptp.'case_nat$'| (|tptp.'fun_app$f'| @t17 @t332) (|tptp.'uug$'| @t17 @t125)) @t126)))) % 0.47/0.87 (assume @p270 (forall @t336 (= (|tptp.'fun_app$d'| @t15 @t335) (|tptp.'fun_app$c'| (|tptp.'case_nat$a'| @t334 (|tptp.'uuh$'| @t15 @t125)) @t126)))) % 0.47/0.87 (assume @p271 (forall (@list @t22 @t18) (= (|tptp.'fun_app$e'| @t337 @t24) @t22))) % 0.47/0.87 (assume @p272 (forall (@list @t338 @t13) (= (|tptp.'fun_app$c'| @t340 @t24) @t339))) % 0.47/0.87 (assume @p273 (forall @t341 (= (|tptp.'fun_app$e'| @t337 @t181) @t19))) % 0.47/0.87 (assume @p274 (forall @t342 (= (|tptp.'fun_app$c'| @t340 @t181) @t157))) % 0.47/0.87 (assume @p275 (= @t100 @t100)) % 0.47/0.87 (assume @p276 (forall (@list @t323 @t7 @t55) (= (|tptp.'semantics_ltln$'| @t324 @t55) (|tptp.'semantics_ltln$'| @t7 @t343)))) % 0.47/0.87 (assume @p277 (forall @t99 (= @t29 (|tptp.'conc$'| (|tptp.'subsequence$'| @t29 @t24 @t94) @t95)))) % 0.47/0.87 (assume @p278 (forall (@list @t323 @t7 @t55 @t53) (=> (|tptp.'semantics_ltln$'| @t324 @t58) (|tptp.'semantics_ltln$'| @t7 (|tptp.'gF_advice$'| @t343 @t53))))) % 0.47/0.87 (assume @p279 (forall @t341 (and (=> @t348 (= @t345 @t22)) (=> @t349 (and (=> @t346 (= @t345 (|tptp.'fun_app$e'| @t18 @t24))) (=> @t347 (= @t345 (|tptp.'fun_app$e'| @t18 @t344)))))))) % 0.47/0.87 (assume @p280 (forall @t342 (= (|tptp.'fun_app$c'| @t340 @t12) (and (=> @t348 @t339) (=> @t349 (and (=> @t346 @t183) (=> @t347 (|tptp.'fun_app$c'| @t13 @t344)))))))) % 0.47/0.87 (assume @p281 (forall @t331 (= @t330 (not (or (and @t353 (not @t135)) (and @t352 (not @t351))))))) % 0.47/0.87 (assume @p282 (forall @t336 (= (|tptp.'fun_app$d'| @t15 @t356) (not (or (and @t353 (not @t355)) (and @t352 (not (|tptp.'fun_app$d'| @t15 @t354)))))))) % 0.47/0.87 (assume @p283 (forall @t331 (= @t330 (and (=> @t353 @t135) (=> @t352 @t351))))) % 0.47/0.87 (assume @p284 (forall @t336 (= (|tptp.'fun_app$d'| @t15 @t358) (and (=> @t353 @t355) (=> @t352 (|tptp.'fun_app$d'| @t15 @t357)))))) % 0.47/0.87 (assume @p285 (forall @t23 (= (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| |tptp.'pred$'| @t22)) (|tptp.'fun_app$k'| |tptp.'of_nat$'| (|tptp.'fun_app$e'| @t319 @t22))))) % 0.47/0.87 (assume @p286 (forall @t23 (= @t73 (|tptp.'fun_app$c'| (|tptp.'case_nat$a'| tptp.tltrue |tptp.'uui$'|) @t22)))) % 0.47/0.87 (assume @p287 (forall @t23 (= @t74 (|tptp.'fun_app$c'| (|tptp.'case_nat$a'| tptp.tlfalse |tptp.'uuj$'|) @t22)))) % 0.47/0.87 (assume @p288 (forall @t23 (and (=> @t116 (= @t359 (|tptp.'inc$'| @t360))) (=> @t195 (= @t359 |tptp.'one$'|))))) % 0.47/0.87 (assume @p289 (forall @t208 (= (- @t242 @t100) @t361))) % 0.47/0.87 (assume @p290 (forall @t208 (= (- @t100 @t242) @t362))) % 0.47/0.87 (assume @p291 (forall @t208 (= (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| (|tptp.'nat$'| @t241)) @t206))) % 0.47/0.87 (assume @p292 (= (|tptp.'sub$'| |tptp.'one$'| |tptp.'one$'|) 0)) % 0.47/0.87 (assume @p293 (forall @t247 (= @t364 @t363))) % 0.47/0.87 (assume @p294 (forall @t247 (= (- @t242 @t249) @t365))) % 0.47/0.87 (assume @p295 (forall @t208 (= (- 1 @t241) @t361))) % 0.47/0.87 (assume @p296 (forall @t208 (= (- @t241 1) @t362))) % 0.47/0.87 (assume @p297 (forall @t208 (= (- (- @t362) 1) @t242))) % 0.47/0.87 (assume @p298 (forall @t247 (= @t363 @t364))) % 0.47/0.87 (assume @p299 (= (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| @t24) |tptp.'one$'|)) % 0.47/0.87 (assume @p300 (forall @t247 (= (< 0 @t363) @t263))) % 0.47/0.87 (assume @p301 (forall @t247 (= (< @t363 0) @t248))) % 0.47/0.87 (assume @p302 (forall @t208 (= (|tptp.'sub$'| @t315 |tptp.'one$'|) @t241))) % 0.47/0.87 (assume @p303 (forall @t23 (=> @t116 (= (|tptp.'numeral$'| @t360) @t72)))) % 0.47/0.87 (assume @p304 (= (|tptp.'dbl$'| @t100) @t366)) % 0.47/0.87 (assume @p305 (= (|tptp.'dbl_dec$'| @t100) (- 3))) % 0.47/0.87 (assume @p306 (forall @t208 (= (+ @t100 @t241) @t362))) % 0.47/0.87 (assume @p307 (forall @t277 (= @t370 @t367))) % 0.47/0.87 (assume @p308 (forall @t277 (= @t373 @t371))) % 0.47/0.87 (assume @p309 (forall @t247 (= (= @t375 @t374) @t245))) % 0.47/0.87 (assume @p310 (forall @t106 (= (= @t376 0) (and @t73 @t193)))) % 0.47/0.87 (assume @p311 (forall @t23 (= (+ @t72 0) @t72))) % 0.47/0.87 (assume @p312 (forall @t106 (= @t378 @t377))) % 0.47/0.87 (assume @p313 (forall @t150 (= @t380 @t149))) % 0.47/0.87 (assume @p314 (forall @t247 (= (= @t382 @t381) @t245))) % 0.47/0.87 (assume @p315 (forall @t150 (and (=> @t256 (and (=> @t385 @t71) (=> @t386 (= 0 @t384)))) (=> @t257 (and (=> @t117 (and (=> @t385 @t294) (=> @t386 (= @t255 @t384)))) (=> @t124 (and (=> @t385 @t293) (=> @t386 (= @t252 @t384))))))))) % 0.47/0.87 (assume @p316 (forall @t307 (= (|tptp.'fun_app$j'| @t186 @t12) (|tptp.'fun_app$j'| @t7 @t387)))) % 0.47/0.87 (assume @p317 (forall (@list @t22 @t94 @t65) (= (|tptp.'suffix$'| @t22 @t227) (|tptp.'suffix$'| (|tptp.'nat$'| @t388) @t65)))) % 0.47/0.87 (assume @p318 (forall @t51 (= (+ @t2 0) @t2))) % 0.47/0.87 (assume @p319 (forall @t51 (= (= 0 @t389) @t49))) % 0.47/0.87 (assume @p320 (forall @t4 (= (= @t369 @t1) @t49))) % 0.47/0.87 (assume @p321 (forall @t4 (= (= @t369 @t2) @t390))) % 0.47/0.87 (assume @p322 (forall @t4 (= (= @t2 @t391) @t390))) % 0.47/0.87 (assume @p323 (forall @t4 (= (= @t2 @t369) @t390))) % 0.47/0.87 (assume @p324 (forall @t51 (= (+ 0 @t2) @t2))) % 0.47/0.87 (assume @p325 (forall @t277 (= @t393 @t392))) % 0.47/0.87 (assume @p326 (forall @t277 (= @t395 @t394))) % 0.47/0.87 (assume @p327 (forall (@list @t206 @t244 @t267) (= (+ @t241 (+ @t246 @t267)) (+ @t397 @t267)))) % 0.47/0.87 (assume @p328 (forall @t247 (= @t398 @t397))) % 0.47/0.87 (assume @p329 (forall @t4 (= (- @t369 @t1) @t2))) % 0.47/0.87 (assume @p330 (forall @t4 (= (+ @t5 @t1) @t2))) % 0.47/0.87 (assume @p331 (forall @t277 (= (- @t369 @t372) @t268))) % 0.47/0.87 (assume @p332 (forall @t4 (= (- @t369 @t2) @t1))) % 0.47/0.87 (assume @p333 (forall @t277 (= (- @t369 @t368) @t278))) % 0.47/0.87 (assume @p334 (forall @t4 (= (+ @t2 @t399) @t1))) % 0.47/0.87 (assume @p335 (forall @t4 (= (+ @t112 @t369) @t1))) % 0.47/0.87 (assume @p336 (forall @t4 (= @t400 (+ @t112 @t111)))) % 0.47/0.87 (assume @p337 (forall @t106 (= (< 0 @t376) (or @t116 @t288)))) % 0.47/0.87 (assume @p338 (forall (@list @t22 @t7 @t12 @t126) (= (|tptp.'subsequence$'| @t186 @t12 @t126) (|tptp.'subsequence$'| @t7 @t387 (|tptp.'nat$'| @t401))))) % 0.47/0.87 (assume @p339 (forall @t4 (= (< @t369 @t2) @t402))) % 0.47/0.87 (assume @p340 (forall @t4 (= (< @t369 @t1) @t119))) % 0.47/0.87 (assume @p341 (forall @t4 (= (< @t2 @t369) @t403))) % 0.47/0.87 (assume @p342 (forall @t4 (= (< @t2 @t391) @t403))) % 0.47/0.87 (assume @p343 (forall @t51 (= (< @t389 0) @t119))) % 0.47/0.87 (assume @p344 (forall @t51 (= (< 0 @t389) @t120))) % 0.47/0.87 (assume @p345 (forall @t51 (= (+ @t2 @t112) 0))) % 0.47/0.87 (assume @p346 (forall @t51 (= (+ @t112 @t2) 0))) % 0.47/0.87 (assume @p347 (forall @t247 (= (+ @t242 @t249) (- @t398)))) % 0.47/0.87 (assume @p348 (forall @t247 (= (- @t241 @t249) @t397))) % 0.47/0.87 (assume @p349 (forall @t247 (= (- @t242 @t246) (- @t397)))) % 0.47/0.87 (assume @p350 (forall @t4 (= (- @t2 @t111) @t369))) % 0.47/0.87 (assume @p351 (forall @t4 (= @t399 @t250))) % 0.47/0.87 (assume @p352 (forall @t208 (= @t406 @t405))) % 0.47/0.87 (assume @p353 (forall @t208 (= @t266 @t407))) % 0.47/0.87 (assume @p354 (forall @t208 (= @t243 @t408))) % 0.47/0.87 (assume @p355 (forall @t247 (= (|tptp.'sub$'| @t375 @t374) @t409))) % 0.47/0.87 (assume @p356 (forall @t247 (= (|tptp.'sub$'| @t382 @t381) @t409))) % 0.47/0.87 (assume @p357 (= (+ 1 @t100) 0)) % 0.47/0.87 (assume @p358 (= (+ @t100 1) 0)) % 0.47/0.87 (assume @p359 (forall @t208 (= @t412 @t411))) % 0.47/0.87 (assume @p360 (forall @t23 (= (+ @t72 2) @t413))) % 0.47/0.87 (assume @p361 (forall @t23 (= (+ 2 @t72) @t413))) % 0.47/0.87 (assume @p362 (forall @t247 (= (+ @t241 @t249) @t363))) % 0.47/0.87 (assume @p363 (forall @t247 (= (+ @t242 @t246) @t365))) % 0.47/0.87 (assume @p364 (forall @t247 (= (|tptp.'sub$'| @t375 @t381) (|tptp.'dbl_dec$'| @t363)))) % 0.47/0.87 (assume @p365 (forall @t247 (= (|tptp.'sub$'| @t382 @t374) (|tptp.'dbl_inc$'| @t363)))) % 0.47/0.87 (assume @p366 (= (+ 1 1) 2)) % 0.47/0.87 (assume @p367 (forall @t208 (= (- @t242 1) (- @t405)))) % 0.47/0.87 (assume @p368 (forall @t208 (= (- 1 @t242) @t411))) % 0.47/0.87 (assume @p369 (forall @t208 (= (|tptp.'sub$'| @t382 |tptp.'one$'|) @t407))) % 0.47/0.87 (assume @p370 (forall @t208 (= (+ @t100 @t242) @t317))) % 0.47/0.87 (assume @p371 (forall @t208 (= (+ @t242 @t100) @t317))) % 0.47/0.87 (assume @p372 (= (|tptp.'dbl$'| 1) 2)) % 0.47/0.87 (assume @p373 (= (|tptp.'dbl_inc$'| 1) 3)) % 0.47/0.87 (assume @p374 (= (+ @t100 @t100) @t366)) % 0.47/0.87 (assume @p375 (= (- 1 @t100) 2)) % 0.47/0.87 (assume @p376 (= (- @t100 1) @t366)) % 0.47/0.87 (assume @p377 (forall @t208 (= (+ 1 @t242) @t361))) % 0.47/0.87 (assume @p378 (forall @t208 (= (+ @t242 1) @t361))) % 0.47/0.87 (assume @p379 (forall @t208 (= (+ @t241 @t100) @t362))) % 0.47/0.87 (assume @p380 (forall @t208 (= (|tptp.'sub$'| |tptp.'one$'| @t382) (- @t407)))) % 0.47/0.87 (assume @p381 (forall @t106 (=> @t299 (= (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| (|tptp.'nat$'| @t376)) (|tptp.'plus$'| @t360 (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| @t94)))))) % 0.47/0.87 (assume @p382 (forall @t23 (=> @t116 (= (|tptp.'fun_app$p'| |tptp.'num_of_nat$'| (|tptp.'nat$'| (+ @t72 @t72))) (|tptp.'bit0$'| @t360))))) % 0.47/0.87 (assume @p383 (forall @t277 (= @t297 @t415))) % 0.47/0.87 (assume @p384 (forall @t277 (=> (= @t369 @t267) (= @t2 @t276)))) % 0.47/0.87 (assume @p385 (forall @t277 (= @t415 @t296))) % 0.47/0.87 (assume @p386 (forall @t277 (= (+ @t5 @t267) @t416))) % 0.47/0.87 (assume @p387 (forall @t277 (= (- @t2 @t268) @t416))) % 0.47/0.87 (assume @p388 (forall @t277 (= (+ @t2 @t268) (- @t369 @t267)))) % 0.47/0.87 (assume @p389 (forall @t277 (= (= @t2 @t268) (= @t372 @t1)))) % 0.47/0.87 (assume @p390 (forall @t277 (= (= @t5 @t267) (= @t2 @t368)))) % 0.47/0.87 (assume @p391 (forall @t273 (=> @t417 (= @t270 (+ @t1 @t274))))) % 0.47/0.87 (assume @p392 (forall @t420 (=> (and @t117 (= @t419 @t401)) @t418))) % 0.47/0.87 (assume @p393 (forall @t150 (=> @t117 (< @t72 @t419)))) % 0.47/0.87 (assume @p394 (forall @t150 (=> @t117 @t385))) % 0.47/0.87 (assume @p395 (forall @t150 (=> @t117 (< @t379 @t383)))) % 0.47/0.87 (assume @p396 (forall @t106 @t422)) % 0.47/0.87 (assume @p397 (forall @t106 @t424)) % 0.47/0.87 (assume @p398 (forall @t420 (=> (and @t117 @t418) (< @t379 (+ @t96 @t128))))) % 0.47/0.87 (assume @p399 (forall @t150 (=> (< @t376 @t137) @t153))) % 0.47/0.87 (assume @p400 (forall @t208 (= (|tptp.'inc$'| @t382) (|tptp.'bit0$'| @t315)))) % 0.47/0.87 (assume @p401 (forall @t208 (= (|tptp.'inc$'| @t375) @t382))) % 0.47/0.87 (assume @p402 (forall @t208 (=> (and (=> @t318 false) (forall @t425 (=> (= @t206 @t374) false)) (forall @t425 (=> (= @t206 @t381) false))) false))) % 0.47/0.87 (assume @p403 (forall @t247 (= (|tptp.'plus$'| @t206 (|tptp.'inc$'| @t244)) (|tptp.'inc$'| @t396)))) % 0.47/0.87 (assume @p404 (forall @t208 (= @t410 @t404))) % 0.47/0.87 (assume @p405 (forall @t208 (not (= |tptp.'one$'| @t382)))) % 0.47/0.87 (assume @p406 (forall @t208 (not (= |tptp.'one$'| @t375)))) % 0.47/0.87 (assume @p407 (forall @t277 (=> @t395 @t394))) % 0.47/0.87 (assume @p408 (forall @t277 (=> @t393 @t392))) % 0.47/0.87 (assume @p409 (forall @t277 (=> @t3 (< @t372 @t414)))) % 0.47/0.87 (assume @p410 (forall @t277 (=> @t3 (< (+ @t267 @t2) @t368)))) % 0.47/0.87 (assume @p411 (forall @t273 (=> @t272 @t427))) % 0.47/0.87 (assume @p412 (forall @t273 (=> (and @t3 @t298) @t427))) % 0.47/0.87 (assume @p413 (forall @t273 (=> (and @t110 @t271) @t427))) % 0.47/0.87 (assume @p414 (forall @t150 (and (=> @t380 (and (=> @t149 @t71) (=> @t282 (= 0 @t281)))) (=> (not @t380) (and (=> @t149 (= @t428 0)) (=> @t282 (= @t428 @t281))))))) % 0.47/0.87 (assume @p415 (forall @t150 (and (=> @t430 (and (=> @t153 @t71) (=> @t287 (= 0 @t286)))) (=> (not @t430) (and (=> @t153 (= @t429 0)) (=> @t287 (= @t429 @t286))))))) % 0.47/0.87 (assume @p416 (forall @t106 (and (=> @t423 (= 0 @t96)) (=> @t424 (= (- @t376 @t72) @t96))))) % 0.47/0.87 (assume @p417 (forall @t106 (and (=> @t421 @t265) (=> @t422 (= (- @t376 @t96) @t72))))) % 0.47/0.87 (assume @p418 (forall @t4 (=> @t225 (= (|tptp.'sgn$'| @t391) @t224)))) % 0.47/0.87 (assume @p419 (forall @t51 (= (|tptp.'dbl$'| @t2) @t389))) % 0.47/0.87 (assume @p420 (forall @t277 (=> @t417 (= @t112 (+ @t111 (- @t267)))))) % 0.47/0.87 (assume @p421 (forall @t4 (= @t400 (+ @t111 @t112)))) % 0.47/0.87 (assume @p422 (forall @t247 (not (= @t375 @t381)))) % 0.47/0.87 (assume @p423 (forall @t277 (= (+ @t369 @t267) @t431))) % 0.47/0.87 (assume @p424 (forall @t277 (=> @t370 @t367))) % 0.47/0.87 (assume @p425 (forall @t277 (=> @t373 @t371))) % 0.47/0.87 (assume @p426 (forall @t277 (= @t431 (+ @t1 @t372)))) % 0.47/0.87 (assume @p427 (forall @t4 (= @t369 @t391))) % 0.47/0.87 (assume @p428 (forall @t273 (=> @t417 (= (+ @t269 @t2) (+ @t1 (+ @t269 @t267)))))) % 0.47/0.87 (assume @p429 (forall @t273 (=> @t417 (= (+ @t2 @t269) (+ @t1 (+ @t267 @t269)))))) % 0.47/0.87 (assume @p430 (forall @t273 (=> (and @t110 @t298) (= @t372 @t426)))) % 0.47/0.87 (assume @p431 (forall @t150 (=> (= @t72 @t383) (= @t92 (+ @t96 @t154))))) % 0.47/0.87 (assume @p432 (forall @t106 (= @t432 @t377))) % 0.47/0.87 (assume @p433 (forall @t106 (= @t432 @t378))) % 0.47/0.87 (assume @p434 (forall @t23 (= (+ 0 @t72) @t72))) % 0.47/0.87 (assume @p435 (forall @t106 (=> (= @t376 @t72) @t193))) % 0.47/0.87 (assume @p436 (forall @t208 (= @t408 (+ @t433 1)))) % 0.47/0.87 (assume @p437 (forall @t208 (= @t407 @t433))) % 0.47/0.87 (assume @p438 (forall @t208 (= @t408 (+ @t407 1)))) % 0.47/0.87 (assume @p439 (forall (@list @t206 @t94) (= (+ (+ @t241 @t96) 1) (+ @t405 @t96)))) % 0.47/0.87 (assume @p440 (forall @t23 (= (+ @t413 1) (+ 3 @t72)))) % 0.47/0.87 (assume @p441 (forall @t4 (=> @t434 (or @t119 @t402)))) % 0.47/0.87 (assume @p442 (forall @t4 (=> (and @t119 @t402) @t434))) % 0.47/0.87 (assume @p443 (forall @t4 (=> (and @t120 @t403) (< 0 @t369)))) % 0.47/0.87 (assume @p444 (forall @t277 (=> (and @t120 @t392) (< @t1 @t372)))) % 0.47/0.87 (assume @p445 (forall @t51 (< @t2 @t435))) % 0.47/0.87 (assume @p446 (forall @t4 (=> @t3 (< @t435 (+ @t1 1))))) % 0.47/0.87 (assume @p447 (forall @t4 (=> (not @t3) (= (+ @t1 @t5) @t2)))) % 0.47/0.87 (assume @p448 (forall @t277 (= (< @t2 @t268) (< @t372 @t1)))) % 0.47/0.87 (assume @p449 (forall @t277 (= (< @t5 @t267) (< @t2 @t368)))) % 0.47/0.87 (assume @p450 (forall @t4 (= @t436 @t175))) % 0.47/0.87 (assume @p451 (forall @t4 (=> @t436 @t174))) % 0.47/0.87 (assume @p452 (forall @t4 (= @t176 @t436))) % 0.47/0.87 (assume @p453 (forall @t4 (= @t174 @t436))) % 0.47/0.87 (assume @p454 (forall @t208 (= @t412 @t406))) % 0.47/0.87 (assume @p455 (forall @t4 (= @t5 (+ @t2 @t111)))) % 0.47/0.87 (assume @p456 (forall @t273 (=> @t417 (= (- @t269 @t2) (+ @t111 (- @t269 @t267)))))) % 0.47/0.87 (assume @p457 (forall @t106 (= (= @t88 @t376) @t437))) % 0.47/0.87 (assume @p458 (forall @t106 (= (= @t376 @t88) @t437))) % 0.47/0.87 (assume @p459 (forall @t106 (=> @t117 (exists @t142 (and @t184 (= @t379 @t96)))))) % 0.47/0.87 (assume @p460 (forall @t106 (=> @t117 @t439))) % 0.47/0.87 (assume @p461 (forall @t106 (= @t117 @t439))) % 0.47/0.87 (assume @p462 (forall @t106 (< @t72 (+ @t388 1)))) % 0.47/0.87 (assume @p463 (forall @t106 (< @t72 @t377))) % 0.47/0.87 (assume @p464 (forall @t106 (=> (and @t117 (forall @t142 (=> @t438 false))) false))) % 0.47/0.87 (assume @p465 (forall @t106 (and (=> @t440 @t71) (=> (not @t440) (= (- @t72 @t376) 0))))) % 0.47/0.87 (assume @p466 (forall @t106 (=> @t124 (and (=> @t117 (= (+ @t96 0) @t72)) (=> @t124 (= (+ @t96 @t251) @t72)))))) % 0.47/0.87 (assume @p467 (forall @t23 (<= 0 @t72))) % 0.47/0.87 (assume @p468 (forall @t23 (= (|tptp.'nat$'| @t72) @t22))) % 0.47/0.87 (assume @p469 (forall @t51 (and (=> @t442 (= @t441 @t2)) (=> (not @t442) (= @t441 0))))) % 0.47/0.87 (assume @p470 (forall @t443 (= (= @t14 tptp.tltrue) @t157))) % 0.47/0.87 (assume @p471 (forall @t443 (= (= @t16 tptp.tltrue) @t157))) % 0.47/0.87 (assume @p472 (forall @t143 (= (= @t329 tptp.tltrue) @t135))) % 0.47/0.87 (assume @p473 (forall @t445 (= (= @t333 tptp.tltrue) @t444))) % 0.47/0.87 (assume @p474 (forall @t445 (= (= @t335 tptp.tltrue) @t444))) % 0.47/0.87 (assume @p475 (forall (@list @t15 @t332) (= (= @t334 tptp.tltrue) @t355))) % 0.47/0.87 (assume @p476 (forall @t445 (= (= @t356 tptp.tltrue) @t444))) % 0.47/0.87 (assume @p477 (forall @t447 (= (= @t354 tptp.tltrue) @t446))) % 0.47/0.87 (assume @p478 (forall @t445 (= (= @t358 tptp.tltrue) @t444))) % 0.47/0.87 (assume @p479 (forall @t447 (= (= @t357 tptp.tltrue) @t446))) % 0.47/0.87 (assume @p480 (forall (@list @t448) (or (= @t448 tptp.tltrue) (= @t448 tptp.tlfalse)))) % 0.47/0.87 (assume @p481 (not (= tptp.tltrue tptp.tlfalse))) % 0.47/0.87 (assume @p482 true) % 0.47/0.87 (step @p483 :rule instantiate :premises (@p16) :args ((@list |tptp.'w$'| @t449))) % 0.47/0.87 (step @p484 :rule false_intro :premises (@p12)) % 0.47/0.87 (step @p485 :rule refl :args (|tptp.'x$'|)) % 0.47/0.87 (step @p486 :rule eq-symm :args (@t43 @t6)) % 0.47/0.87 (step @p487 :rule cong :premises (@p486) :args (@t44)) % 0.47/0.87 (step @p488 :rule eq_resolve :premises (@p20 @p487)) % 0.47/0.87 (step @p489 :rule instantiate :premises (@p488) :args ((@list |tptp.'phi$'| @t25))) % 0.47/0.87 (step @p490 :rule cong :premises (@p489 @p485) :args (@t449)) % 0.47/0.87 (step @p491 :rule refl :args (@t28)) % 0.47/0.87 (step @p492 :rule cong :premises (@p491 @p490) :args (@t450)) % 0.47/0.87 (step @p493 :rule trans :premises (@p492 @p484)) % 0.47/0.87 (step @p494 :rule false_elim :premises (@p493)) % 0.47/0.87 (step @p495 :rule true_intro :premises (@p13)) % 0.47/0.87 (step @p496 :rule eq-symm :args (@t45 @t39)) % 0.47/0.87 (step @p497 :rule cong :premises (@p496) :args (@t47)) % 0.47/0.87 (step @p498 :rule eq_resolve :premises (@p22 @p497)) % 0.47/0.87 (step @p499 :rule instantiate :premises (@p498) :args ((@list |tptp.'phi$'|))) % 0.47/0.87 (step @p500 :rule cong :premises (@p499 @p485) :args ((|tptp.'gF_advice$'| @t26 |tptp.'x$'|))) % 0.47/0.87 (step @p501 :rule instantiate :premises (@p19) :args ((@list |tptp.'phi$'| |tptp.'x$'|))) % 0.47/0.87 (step @p502 :rule symm :premises (@p501)) % 0.47/0.87 (step @p503 :rule trans :premises (@p502 @p500)) % 0.47/0.87 (step @p504 :rule refl :args (|tptp.'w$'|)) % 0.47/0.87 (step @p505 :rule cong :premises (@p504 @p503) :args (@t451)) % 0.47/0.87 (step @p506 :rule trans :premises (@p505 @p495)) % 0.47/0.87 (step @p507 :rule true_elim :premises (@p506)) % 0.47/0.87 (step @p508 :rule cnf_equiv_pos1 :args (@t452)) % 0.47/0.87 (step @p509 :rule reordering :premises (@p508) :args ((or @t450 (not @t451) (not @t452)))) % 0.47/0.87 (step @p510 false :rule chain_m_resolution :premises (@p509 @p507 @p494 @p483) :args (false (@list false true false) (@list @t451 @t450 @t452))) % 0.47/0.87 ) % 0.47/0.87 % SZS output end Proof % 0.47/0.87 % cvc5 exiting %------------------------------------------------------------------------------