%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP378_1 : TPTP v9.2.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:26:26 AM UTC 2026 % Result : Theorem 203.66s 203.94s % Output : Proof 203.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP378_1 : TPTP v9.2.1. Released v8.1.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n013.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 05:04:15 EDT 2026 % 0.17/0.35 % CPUTime : % 0.44/0.73 %----Proving TF0_ARI % 203.66/203.94 --- Run --finite-model-find --decision=internal at 45... % 203.66/203.94 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 60... % 203.66/203.94 --- Run --no-e-matching --full-saturate-quant at 45... % 203.66/203.94 --- Run --cegqi-all --purify-triggers --full-saturate-quant at 45... % 203.66/203.94 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 203.66/203.94 % SZS status Theorem % 203.66/203.94 % SZS output start Proof % 203.66/203.94 ( % 203.66/203.94 (declare-sort |tptp.'Pratt_list_pratt_list_list_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_list$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_list_list$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_list_pratt_list_bool_fun_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Int_multiset_int_multiset_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_multiset_nat_multiset_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Int_multiset$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_int_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_list_bool_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_list$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_multiset$'| 0) % 203.66/203.94 (declare-sort tptp.tlbool 0) % 203.66/203.94 (declare-sort |tptp.'Pratt$'| 0) % 203.66/203.94 (declare-sort |tptp.'Int_int_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_set$'| 0) % 203.66/203.94 (declare-sort |tptp.'Pratt_bool_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_set$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_nat_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat$'| 0) % 203.66/203.94 (declare-sort |tptp.'Nat_bool_fun$'| 0) % 203.66/203.94 (declare-sort |tptp.'Int_set$'| 0) % 203.66/203.94 (declare-sort |tptp.'Int_bool_fun$'| 0) % 203.66/203.94 (declare-const tptp.tlfalse tptp.tlbool) % 203.66/203.94 (declare-const |tptp.'totient$'| (-> |tptp.'Nat$'| |tptp.'Nat$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$j'| (-> |tptp.'Pratt_list_pratt_list_list_fun$'| |tptp.'Pratt_list$'| |tptp.'Pratt_list_list$'|)) % 203.66/203.94 (declare-const |tptp.'n_lists$'| (-> |tptp.'Nat$'| |tptp.'Pratt_list_pratt_list_list_fun$'|)) % 203.66/203.94 (declare-const |tptp.'cons$b'| (-> |tptp.'Nat$'| |tptp.'Nat_list$'| |tptp.'Nat_list$'|)) % 203.66/203.94 (declare-const |tptp.'set$a'| (-> |tptp.'Nat_list$'| |tptp.'Nat_set$'|)) % 203.66/203.94 (declare-const |tptp.'nil$a'| |tptp.'Pratt_list_list$'|) % 203.66/203.94 (declare-const |tptp.'cons$a'| (-> |tptp.'Pratt_list$'| |tptp.'Pratt_list_list$'| |tptp.'Pratt_list_list$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$i'| (-> |tptp.'Pratt_list_pratt_list_bool_fun_fun$'| |tptp.'Pratt_list$'| |tptp.'Pratt_list_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'dvd$a'| (-> |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'dvd$'| (-> Int |tptp.'Int_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'accp$'| (-> |tptp.'Pratt_list_pratt_list_bool_fun_fun$'| |tptp.'Pratt_list_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'valid_cert_rel$'| |tptp.'Pratt_list_pratt_list_bool_fun_fun$'|) % 203.66/203.94 (declare-const tptp.tltrue tptp.tlbool) % 203.66/203.94 (declare-const |tptp.'valid_cert$'| |tptp.'Pratt_list_bool_fun$'|) % 203.66/203.94 (declare-const |tptp.'c$'| |tptp.'Pratt_list$'|) % 203.66/203.94 (declare-const |tptp.'prime_factorization$'| (-> |tptp.'Nat$'| |tptp.'Nat_multiset$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$a'| (-> |tptp.'Pratt_bool_fun$'| |tptp.'Pratt$'| Bool)) % 203.66/203.94 (declare-const |tptp.'power$'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 203.66/203.94 (declare-const |tptp.'divide$'| (-> Int |tptp.'Int_int_fun$'|)) % 203.66/203.94 (declare-const |tptp.'aa$'| |tptp.'Nat$'|) % 203.66/203.94 (declare-const |tptp.'minus$a'| (-> |tptp.'Nat_multiset$'| |tptp.'Nat_multiset_nat_multiset_fun$'|)) % 203.66/203.94 (declare-const |tptp.'nat$'| (-> Int |tptp.'Nat$'|)) % 203.66/203.94 (declare-const |tptp.'zero$a'| |tptp.'Int_multiset$'|) % 203.66/203.94 (declare-const |tptp.'set_mset$'| (-> |tptp.'Nat_multiset$'| |tptp.'Nat_set$'|)) % 203.66/203.94 (declare-const |tptp.'times$'| (-> Int Int Int)) % 203.66/203.94 (declare-const |tptp.'pa$'| |tptp.'Nat$'|) % 203.66/203.94 (declare-const |tptp.'uuc$'| (-> Int |tptp.'Int_int_fun$'|)) % 203.66/203.94 (declare-const |tptp.'one$'| |tptp.'Nat$'|) % 203.66/203.94 (declare-const |tptp.'ta$'| |tptp.'Pratt$'|) % 203.66/203.94 (declare-const |tptp.'triple$'| (-> |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Pratt$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$b'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| Bool)) % 203.66/203.94 (declare-const |tptp.'member$a'| (-> |tptp.'Nat$'| |tptp.'Nat_set$'| Bool)) % 203.66/203.94 (declare-const |tptp.'y$'| |tptp.'Pratt$'|) % 203.66/203.94 (declare-const |tptp.'collect$b'| (-> |tptp.'Pratt_bool_fun$'| |tptp.'Pratt_set$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$'| (-> |tptp.'Int_int_fun$'| Int Int)) % 203.66/203.94 (declare-const |tptp.'nil$'| |tptp.'Pratt_list$'|) % 203.66/203.94 (declare-const |tptp.'member$'| (-> |tptp.'Pratt$'| |tptp.'Pratt_set$'| Bool)) % 203.66/203.94 (declare-const |tptp.'xa$'| |tptp.'Nat$'|) % 203.66/203.94 (declare-const |tptp.'uub$'| (-> |tptp.'Pratt_set$'| |tptp.'Pratt_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'ys$'| |tptp.'Pratt_list$'|) % 203.66/203.94 (declare-const |tptp.'uua$'| (-> |tptp.'Nat_set$'| |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'member$b'| (-> Int |tptp.'Int_set$'| Bool)) % 203.66/203.94 (declare-const |tptp.'uu$'| (-> |tptp.'Int_set$'| |tptp.'Int_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'pratt_triple$'| (-> |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'cong$'| (-> |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'set$'| (-> |tptp.'Pratt_list$'| |tptp.'Pratt_set$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$c'| (-> |tptp.'Int_bool_fun$'| Int Bool)) % 203.66/203.94 (declare-const |tptp.'prime$'| (-> |tptp.'Nat$'| |tptp.'Pratt$'|)) % 203.66/203.94 (declare-const |tptp.'prime$a'| |tptp.'Nat_bool_fun$'|) % 203.66/203.94 (declare-const |tptp.'fun_app$d'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 203.66/203.94 (declare-const |tptp.'of_nat$'| (-> |tptp.'Nat$'| Int)) % 203.66/203.94 (declare-const |tptp.'minus$'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$e'| (-> |tptp.'Pratt_list_bool_fun$'| |tptp.'Pratt_list$'| Bool)) % 203.66/203.94 (declare-const |tptp.'less$'| (-> |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'zero$'| |tptp.'Nat$'|) % 203.66/203.94 (declare-const |tptp.'size_pratt$'| (-> |tptp.'Pratt$'| |tptp.'Nat$'|)) % 203.66/203.94 (declare-const |tptp.'power$a'| (-> Int |tptp.'Nat_int_fun$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$f'| (-> |tptp.'Nat_int_fun$'| |tptp.'Nat$'| Int)) % 203.66/203.94 (declare-const |tptp.'prime$b'| |tptp.'Int_bool_fun$'|) % 203.66/203.94 (declare-const |tptp.'prime_factorization$a'| (-> Int |tptp.'Int_multiset$'|)) % 203.66/203.94 (declare-const |tptp.'zero$b'| |tptp.'Nat_multiset$'|) % 203.66/203.94 (declare-const |tptp.'set_mset$a'| (-> |tptp.'Int_multiset$'| |tptp.'Int_set$'|)) % 203.66/203.94 (declare-const |tptp.'collect$'| (-> |tptp.'Int_bool_fun$'| |tptp.'Int_set$'|)) % 203.66/203.94 (declare-const |tptp.'collect$a'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat_set$'|)) % 203.66/203.94 (declare-const |tptp.'t$'| |tptp.'Pratt$'|) % 203.66/203.94 (declare-const |tptp.'divide$a'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 203.66/203.94 (declare-const |tptp.'cong$a'| (-> Int Int |tptp.'Int_bool_fun$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$g'| (-> |tptp.'Nat_multiset_nat_multiset_fun$'| |tptp.'Nat_multiset$'| |tptp.'Nat_multiset$'|)) % 203.66/203.94 (declare-const |tptp.'minus$b'| (-> |tptp.'Int_multiset$'| |tptp.'Int_multiset_int_multiset_fun$'|)) % 203.66/203.94 (declare-const |tptp.'fun_app$h'| (-> |tptp.'Int_multiset_int_multiset_fun$'| |tptp.'Int_multiset$'| |tptp.'Int_multiset$'|)) % 203.66/203.94 (declare-const |tptp.'cons$'| (-> |tptp.'Pratt$'| |tptp.'Pratt_list$'| |tptp.'Pratt_list$'|)) % 203.66/203.94 (declare-const |tptp.'times$a'| (-> |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 203.66/203.94 (define @t1 () (@var "A__questionmark_v1" Int)) % 203.66/203.94 (define @t2 () (@var "A__questionmark_v0" Int)) % 203.66/203.94 (define @t3 () (- @t2 @t1)) % 203.66/203.94 (define @t4 () (@list @t2 @t1)) % 203.66/203.94 (define @t5 () (@var "A__questionmark_v0" |tptp.'Pratt_set$'|)) % 203.66/203.94 (define @t6 () (@var "A__questionmark_v1" |tptp.'Pratt$'|)) % 203.66/203.94 (define @t7 () (|tptp.'uub$'| @t5)) % 203.66/203.94 (define @t8 () (@var "A__questionmark_v0" |tptp.'Nat_set$'|)) % 203.66/203.94 (define @t9 () (@var "A__questionmark_v1" |tptp.'Nat$'|)) % 203.66/203.94 (define @t10 () (|tptp.'uua$'| @t8)) % 203.66/203.94 (define @t11 () (@var "A__questionmark_v0" |tptp.'Int_set$'|)) % 203.66/203.94 (define @t12 () (|tptp.'uu$'| @t11)) % 203.66/203.94 (define @t13 () (|tptp.'of_nat$'| |tptp.'xa$'|)) % 203.66/203.94 (define @t14 () (|tptp.'nat$'| 1)) % 203.66/203.94 (define @t15 () (@var "A__questionmark_v0" |tptp.'Nat$'|)) % 203.66/203.94 (define @t16 () (|tptp.'of_nat$'| @t15)) % 203.66/203.94 (define @t17 () (|tptp.'of_nat$'| |tptp.'pa$'|)) % 203.66/203.94 (define @t18 () (- @t17 1)) % 203.66/203.94 (define @t19 () (|tptp.'divide$'| @t18)) % 203.66/203.94 (define @t20 () (|tptp.'fun_app$'| @t19 @t16)) % 203.66/203.94 (define @t21 () (|tptp.'nat$'| @t20)) % 203.66/203.94 (define @t22 () (|tptp.'power$'| |tptp.'aa$'|)) % 203.66/203.94 (define @t23 () (|tptp.'fun_app$d'| @t22 @t21)) % 203.66/203.94 (define @t24 () (|tptp.'cong$'| @t23 @t14)) % 203.66/203.94 (define @t25 () (|tptp.'fun_app$b'| @t24 |tptp.'pa$'|)) % 203.66/203.94 (define @t26 () (< @t17 1)) % 203.66/203.94 (define @t27 () (not @t26)) % 203.66/203.94 (define @t28 () (=> @t27 @t25)) % 203.66/203.94 (define @t29 () (|tptp.'divide$'| 0)) % 203.66/203.94 (define @t30 () (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t16))) % 203.66/203.94 (define @t31 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 @t30) @t14) |tptp.'pa$'|)) % 203.66/203.94 (define @t32 () (=> @t26 @t31)) % 203.66/203.94 (define @t33 () (and @t32 @t28)) % 203.66/203.94 (define @t34 () (not @t33)) % 203.66/203.94 (define @t35 () (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| |tptp.'xa$'|))) % 203.66/203.94 (define @t36 () (|tptp.'member$a'| @t15 @t35)) % 203.66/203.94 (define @t37 () (=> @t36 @t34)) % 203.66/203.94 (define @t38 () (@list @t15)) % 203.66/203.94 (define @t39 () (forall @t38 @t37)) % 203.66/203.94 (define @t40 () (and @t39 (< 0 @t13))) % 203.66/203.94 (define @t41 () (|tptp.'triple$'| |tptp.'pa$'| |tptp.'aa$'| |tptp.'xa$'|)) % 203.66/203.94 (define @t42 () (= |tptp.'ta$'| @t41)) % 203.66/203.94 (define @t43 () (=> @t42 @t40)) % 203.66/203.94 (define @t44 () (|tptp.'fun_app$b'| |tptp.'prime$a'| |tptp.'pa$'|)) % 203.66/203.94 (define @t45 () (|tptp.'prime$'| |tptp.'pa$'|)) % 203.66/203.94 (define @t46 () (= |tptp.'ta$'| @t45)) % 203.66/203.94 (define @t47 () (=> @t46 @t44)) % 203.66/203.94 (define @t48 () (and @t47 @t43)) % 203.66/203.94 (define @t49 () (not @t48)) % 203.66/203.94 (define @t50 () (@var "A__questionmark_v5" |tptp.'Nat$'|)) % 203.66/203.94 (define @t51 () (|tptp.'of_nat$'| @t50)) % 203.66/203.94 (define @t52 () (@var "A__questionmark_v2" |tptp.'Nat$'|)) % 203.66/203.94 (define @t53 () (|tptp.'of_nat$'| @t52)) % 203.66/203.94 (define @t54 () (@var "A__questionmark_v4" |tptp.'Nat$'|)) % 203.66/203.94 (define @t55 () (|tptp.'of_nat$'| @t54)) % 203.66/203.94 (define @t56 () (|tptp.'of_nat$'| @t9)) % 203.66/203.94 (define @t57 () (@var "A__questionmark_v3" |tptp.'Nat$'|)) % 203.66/203.94 (define @t58 () (|tptp.'of_nat$'| @t57)) % 203.66/203.94 (define @t59 () (|tptp.'triple$'| @t15 @t9 @t52)) % 203.66/203.94 (define @t60 () (= @t16 @t56)) % 203.66/203.94 (define @t61 () (|tptp.'prime$'| @t9)) % 203.66/203.94 (define @t62 () (|tptp.'prime$'| @t15)) % 203.66/203.94 (define @t63 () (@list @t15 @t9)) % 203.66/203.94 (define @t64 () (|tptp.'triple$'| @t9 @t52 @t57)) % 203.66/203.94 (define @t65 () (@list @t15 @t9 @t52 @t57)) % 203.66/203.94 (define @t66 () (@var "A__questionmark_v0" |tptp.'Pratt$'|)) % 203.66/203.94 (define @t67 () (= @t66 @t64)) % 203.66/203.94 (define @t68 () (@list @t9 @t52 @t57)) % 203.66/203.94 (define @t69 () (= @t66 @t61)) % 203.66/203.94 (define @t70 () (@list @t9)) % 203.66/203.94 (define @t71 () (= @t13 1)) % 203.66/203.94 (define @t72 () (= |tptp.'y$'| @t41)) % 203.66/203.94 (define @t73 () (< @t53 @t56)) % 203.66/203.94 (define @t74 () (|tptp.'power$'| @t15)) % 203.66/203.94 (define @t75 () (|tptp.'fun_app$d'| @t74 @t52)) % 203.66/203.94 (define @t76 () (|tptp.'fun_app$d'| @t74 @t9)) % 203.66/203.94 (define @t77 () (|tptp.'less$'| @t76)) % 203.66/203.94 (define @t78 () (|tptp.'fun_app$b'| @t77 @t75)) % 203.66/203.94 (define @t79 () (|tptp.'less$'| @t15)) % 203.66/203.94 (define @t80 () (|tptp.'less$'| |tptp.'zero$'|)) % 203.66/203.94 (define @t81 () (|tptp.'fun_app$b'| @t80 @t15)) % 203.66/203.94 (define @t82 () (and @t81 (|tptp.'fun_app$b'| @t79 |tptp.'one$'|))) % 203.66/203.94 (define @t83 () (@list @t15 @t9 @t52)) % 203.66/203.94 (define @t84 () (|tptp.'power$a'| @t2)) % 203.66/203.94 (define @t85 () (|tptp.'fun_app$f'| @t84 @t52)) % 203.66/203.94 (define @t86 () (|tptp.'fun_app$f'| @t84 @t9)) % 203.66/203.94 (define @t87 () (< @t86 @t85)) % 203.66/203.94 (define @t88 () (< 0 @t2)) % 203.66/203.94 (define @t89 () (and @t88 (< @t2 1))) % 203.66/203.94 (define @t90 () (@list @t2 @t9 @t52)) % 203.66/203.94 (define @t91 () (< @t56 @t16)) % 203.66/203.94 (define @t92 () (< 0 @t56)) % 203.66/203.94 (define @t93 () (- @t16 1)) % 203.66/203.94 (define @t94 () (|tptp.'divide$'| @t93)) % 203.66/203.94 (define @t95 () (|tptp.'power$'| @t9)) % 203.66/203.94 (define @t96 () (< @t16 1)) % 203.66/203.94 (define @t97 () (not @t96)) % 203.66/203.94 (define @t98 () (|tptp.'nat$'| @t93)) % 203.66/203.94 (define @t99 () (|tptp.'nat$'| 0)) % 203.66/203.94 (define @t100 () (@list @t52)) % 203.66/203.94 (define @t101 () (|tptp.'fun_app$d'| @t95 @t98)) % 203.66/203.94 (define @t102 () (=> @t97 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t101 @t14) @t15))) % 203.66/203.94 (define @t103 () (|tptp.'fun_app$d'| @t95 @t99)) % 203.66/203.94 (define @t104 () (=> @t96 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t103 @t14) @t15))) % 203.66/203.94 (define @t105 () (|tptp.'fun_app$b'| |tptp.'prime$a'| @t15)) % 203.66/203.94 (define @t106 () (= @t56 0)) % 203.66/203.94 (define @t107 () (|tptp.'fun_app$c'| |tptp.'prime$b'| @t2)) % 203.66/203.94 (define @t108 () (@list @t2 @t9)) % 203.66/203.94 (define @t109 () (= @t76 |tptp.'one$'|)) % 203.66/203.94 (define @t110 () (= @t86 1)) % 203.66/203.94 (define @t111 () (= @t15 |tptp.'zero$'|)) % 203.66/203.94 (define @t112 () (= @t76 |tptp.'zero$'|)) % 203.66/203.94 (define @t113 () (= @t2 0)) % 203.66/203.94 (define @t114 () (= @t86 0)) % 203.66/203.94 (define @t115 () (< @t56 @t53)) % 203.66/203.94 (define @t116 () (|tptp.'less$'| |tptp.'one$'|)) % 203.66/203.94 (define @t117 () (|tptp.'fun_app$b'| @t116 @t15)) % 203.66/203.94 (define @t118 () (< 1 @t2)) % 203.66/203.94 (define @t119 () (= |tptp.'y$'| @t45)) % 203.66/203.94 (define @t120 () (@list @t2)) % 203.66/203.94 (define @t121 () (= @t56 @t53)) % 203.66/203.94 (define @t122 () (= @t76 @t75)) % 203.66/203.94 (define @t123 () (= @t86 @t85)) % 203.66/203.94 (define @t124 () (< 0 @t16)) % 203.66/203.94 (define @t125 () (|tptp.'of_nat$'| @t76)) % 203.66/203.94 (define @t126 () (|tptp.'prime_factorization$a'| @t1)) % 203.66/203.94 (define @t127 () (|tptp.'set_mset$a'| @t126)) % 203.66/203.94 (define @t128 () (|tptp.'member$b'| @t2 @t127)) % 203.66/203.94 (define @t129 () (|tptp.'prime_factorization$'| @t9)) % 203.66/203.94 (define @t130 () (|tptp.'set_mset$'| @t129)) % 203.66/203.94 (define @t131 () (|tptp.'member$a'| @t15 @t130)) % 203.66/203.94 (define @t132 () (@var "A__questionmark_v1" |tptp.'Int_bool_fun$'|)) % 203.66/203.94 (define @t133 () (@list @t2 @t132)) % 203.66/203.94 (define @t134 () (@var "A__questionmark_v1" |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (define @t135 () (|tptp.'collect$a'| @t134)) % 203.66/203.94 (define @t136 () (@list @t15 @t134)) % 203.66/203.94 (define @t137 () (@var "A__questionmark_v1" |tptp.'Pratt_bool_fun$'|)) % 203.66/203.94 (define @t138 () (|tptp.'collect$b'| @t137)) % 203.66/203.94 (define @t139 () (@var "A__questionmark_v0" |tptp.'Pratt_bool_fun$'|)) % 203.66/203.94 (define @t140 () (@var "A__questionmark_v2" |tptp.'Pratt$'|)) % 203.66/203.94 (define @t141 () (@list @t140)) % 203.66/203.94 (define @t142 () (@var "A__questionmark_v0" |tptp.'Nat_bool_fun$'|)) % 203.66/203.94 (define @t143 () (|tptp.'fun_app$b'| @t134 @t52)) % 203.66/203.94 (define @t144 () (|tptp.'fun_app$b'| @t142 @t52)) % 203.66/203.94 (define @t145 () (not @t111)) % 203.66/203.94 (define @t146 () (not @t113)) % 203.66/203.94 (define @t147 () (|tptp.'fun_app$d'| @t74 @t99)) % 203.66/203.94 (define @t148 () (|tptp.'fun_app$f'| @t84 @t99)) % 203.66/203.94 (define @t149 () (= @t53 @t58)) % 203.66/203.94 (define @t150 () (= @t15 @t9)) % 203.66/203.94 (define @t151 () (= @t53 0)) % 203.66/203.94 (define @t152 () (and @t151 (= @t58 0))) % 203.66/203.94 (define @t153 () (|tptp.'fun_app$d'| @t95 @t57)) % 203.66/203.94 (define @t154 () (= @t75 @t153)) % 203.66/203.94 (define @t155 () (|tptp.'fun_app$b'| |tptp.'prime$a'| @t9)) % 203.66/203.94 (define @t156 () (= @t2 @t1)) % 203.66/203.94 (define @t157 () (|tptp.'power$a'| @t1)) % 203.66/203.94 (define @t158 () (|tptp.'fun_app$f'| @t157 @t57)) % 203.66/203.94 (define @t159 () (= @t85 @t158)) % 203.66/203.94 (define @t160 () (|tptp.'fun_app$c'| |tptp.'prime$b'| @t1)) % 203.66/203.94 (define @t161 () (@list @t2 @t1 @t52 @t57)) % 203.66/203.94 (define @t162 () (|tptp.'of_nat$'| @t75)) % 203.66/203.94 (define @t163 () (= @t56 1)) % 203.66/203.94 (define @t164 () (|tptp.'prime_factorization$a'| @t2)) % 203.66/203.94 (define @t165 () (|tptp.'set_mset$a'| @t164)) % 203.66/203.94 (define @t166 () (|tptp.'prime_factorization$'| @t15)) % 203.66/203.94 (define @t167 () (|tptp.'set_mset$'| @t166)) % 203.66/203.94 (define @t168 () (|tptp.'fun_app$b'| (|tptp.'cong$'| @t15 @t14) @t9)) % 203.66/203.94 (define @t169 () (|tptp.'fun_app$d'| (|tptp.'power$'| |tptp.'zero$'|) @t15)) % 203.66/203.94 (define @t170 () (= @t169 |tptp.'zero$'|)) % 203.66/203.94 (define @t171 () (= @t16 0)) % 203.66/203.94 (define @t172 () (not @t171)) % 203.66/203.94 (define @t173 () (|tptp.'fun_app$f'| (|tptp.'power$a'| 0) @t15)) % 203.66/203.94 (define @t174 () (= @t173 0)) % 203.66/203.94 (define @t175 () (|tptp.'power$'| @t52)) % 203.66/203.94 (define @t176 () (|tptp.'fun_app$d'| @t175 @t9)) % 203.66/203.94 (define @t177 () (|tptp.'fun_app$d'| @t175 @t15)) % 203.66/203.94 (define @t178 () (< @t16 @t56)) % 203.66/203.94 (define @t179 () (@var "A__questionmark_v2" Int)) % 203.66/203.94 (define @t180 () (|tptp.'power$a'| @t179)) % 203.66/203.94 (define @t181 () (|tptp.'fun_app$f'| @t180 @t9)) % 203.66/203.94 (define @t182 () (|tptp.'fun_app$f'| @t180 @t15)) % 203.66/203.94 (define @t183 () (@list @t15 @t9 @t179)) % 203.66/203.94 (define @t184 () (< 0 @t58)) % 203.66/203.94 (define @t185 () (< 0 @t53)) % 203.66/203.94 (define @t186 () (and @t105 @t155 @t154 @t185 @t184)) % 203.66/203.94 (define @t187 () (and @t107 @t160 @t159 @t185 @t184)) % 203.66/203.94 (define @t188 () (|tptp.'member$a'| @t9 @t167)) % 203.66/203.94 (define @t189 () (< 1 @t16)) % 203.66/203.94 (define @t190 () (|tptp.'fun_app$b'| @t80 @t52)) % 203.66/203.94 (define @t191 () (< 0 @t179)) % 203.66/203.94 (define @t192 () (|tptp.'divide$'| @t16)) % 203.66/203.94 (define @t193 () (|tptp.'fun_app$'| @t192 @t56)) % 203.66/203.94 (define @t194 () (= @t193 0)) % 203.66/203.94 (define @t195 () (- @t16 @t56)) % 203.66/203.94 (define @t196 () (not @t178)) % 203.66/203.94 (define @t197 () (< 0 0)) % 203.66/203.94 (define @t198 () (|tptp.'divide$a'| @t15)) % 203.66/203.94 (define @t199 () (|tptp.'divide$'| @t2)) % 203.66/203.94 (define @t200 () (< @t1 @t2)) % 203.66/203.94 (define @t201 () (@list @t57)) % 203.66/203.94 (define @t202 () (|tptp.'fun_app$b'| (|tptp.'pratt_triple$'| @t15 @t9) @t52)) % 203.66/203.94 (define @t203 () (|tptp.'fun_app$f'| @t157 @t15)) % 203.66/203.94 (define @t204 () (@list @t15 @t1)) % 203.66/203.94 (define @t205 () (|tptp.'fun_app$d'| @t95 @t15)) % 203.66/203.94 (define @t206 () (|tptp.'cong$a'| @t2 @t1)) % 203.66/203.94 (define @t207 () (|tptp.'cong$'| @t15 @t9)) % 203.66/203.94 (define @t208 () (< @t16 @t16)) % 203.66/203.94 (define @t209 () (not @t208)) % 203.66/203.94 (define @t210 () (= 0 0)) % 203.66/203.94 (define @t211 () (|tptp.'set$'| |tptp.'ys$'|)) % 203.66/203.94 (define @t212 () (|tptp.'member$'| |tptp.'ta$'| @t211)) % 203.66/203.94 (define @t213 () (@var "A__questionmark_v0" |tptp.'Nat_multiset$'|)) % 203.66/203.94 (define @t214 () (@list @t213)) % 203.66/203.94 (define @t215 () (@var "A__questionmark_v0" |tptp.'Int_multiset$'|)) % 203.66/203.94 (define @t216 () (@list @t215)) % 203.66/203.94 (define @t217 () (|tptp.'minus$'| @t15)) % 203.66/203.94 (define @t218 () (|tptp.'minus$a'| @t213)) % 203.66/203.94 (define @t219 () (|tptp.'minus$b'| @t215)) % 203.66/203.94 (define @t220 () (< @t16 0)) % 203.66/203.94 (define @t221 () (not @t124)) % 203.66/203.94 (define @t222 () (< @t2 @t1)) % 203.66/203.94 (define @t223 () (= @t2 1)) % 203.66/203.94 (define @t224 () (@var "A__questionmark_v3" Int)) % 203.66/203.94 (define @t225 () (= @t3 (- @t179 @t224))) % 203.66/203.94 (define @t226 () (@list @t2 @t1 @t179 @t224)) % 203.66/203.94 (define @t227 () (|tptp.'fun_app$d'| @t217 @t9)) % 203.66/203.94 (define @t228 () (@var "A__questionmark_v1" |tptp.'Nat_multiset$'|)) % 203.66/203.94 (define @t229 () (@var "A__questionmark_v2" |tptp.'Nat_multiset$'|)) % 203.66/203.94 (define @t230 () (@var "A__questionmark_v1" |tptp.'Int_multiset$'|)) % 203.66/203.94 (define @t231 () (@var "A__questionmark_v2" |tptp.'Int_multiset$'|)) % 203.66/203.94 (define @t232 () (- @t2 @t179)) % 203.66/203.94 (define @t233 () (@list @t2 @t1 @t179)) % 203.66/203.94 (define @t234 () (=> @t171 false)) % 203.66/203.94 (define @t235 () (not @t60)) % 203.66/203.94 (define @t236 () (= @t56 @t16)) % 203.66/203.94 (define @t237 () (|tptp.'fun_app$b'| @t142 @t9)) % 203.66/203.94 (define @t238 () (|tptp.'fun_app$b'| @t142 @t57)) % 203.66/203.94 (define @t239 () (< @t58 @t53)) % 203.66/203.94 (define @t240 () (@list @t142 @t9)) % 203.66/203.94 (define @t241 () (exists @t201 (and @t239 (not @t238)))) % 203.66/203.94 (define @t242 () (not @t144)) % 203.66/203.94 (define @t243 () (- @t16 @t53)) % 203.66/203.94 (define @t244 () (- @t243 @t56)) % 203.66/203.94 (define @t245 () (- @t195 @t53)) % 203.66/203.94 (define @t246 () (< @t16 @t53)) % 203.66/203.94 (define @t247 () (not @t246)) % 203.66/203.94 (define @t248 () (- 0 @t56)) % 203.66/203.94 (define @t249 () (and (=> @t246 @t92) (=> @t247 (< @t243 @t56)))) % 203.66/203.94 (define @t250 () (not @t249)) % 203.66/203.94 (define @t251 () (- 0 @t53)) % 203.66/203.94 (define @t252 () (and (=> @t178 @t185) (=> @t196 (< @t195 @t53)))) % 203.66/203.94 (define @t253 () (|tptp.'fun_app$c'| @t206 @t179)) % 203.66/203.94 (define @t254 () (|tptp.'fun_app$b'| (|tptp.'cong$'| @t9 @t15) @t52)) % 203.66/203.94 (define @t255 () (|tptp.'fun_app$b'| @t207 @t52)) % 203.66/203.94 (define @t256 () (- @t1 @t179)) % 203.66/203.94 (define @t257 () (- @t2 @t224)) % 203.66/203.94 (define @t258 () (< @t179 @t224)) % 203.66/203.94 (define @t259 () (- @t179 @t1)) % 203.66/203.94 (define @t260 () (not @t220)) % 203.66/203.94 (define @t261 () (not @t106)) % 203.66/203.94 (define @t262 () (= 0 @t16)) % 203.66/203.94 (define @t263 () (- @t56 @t16)) % 203.66/203.94 (define @t264 () (not @t91)) % 203.66/203.94 (define @t265 () (- @t53 @t16)) % 203.66/203.94 (define @t266 () (- @t53 @t56)) % 203.66/203.94 (define @t267 () (< @t53 @t16)) % 203.66/203.94 (define @t268 () (not @t267)) % 203.66/203.94 (define @t269 () (@var "A__questionmark_v4" Int)) % 203.66/203.94 (define @t270 () (and @t253 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t224 @t269) @t179))) % 203.66/203.94 (define @t271 () (@list @t2 @t1 @t179 @t224 @t269)) % 203.66/203.94 (define @t272 () (|tptp.'fun_app$d'| @t74 @t57)) % 203.66/203.94 (define @t273 () (and @t124 @t92)) % 203.66/203.94 (define @t274 () (= @t16 1)) % 203.66/203.94 (define @t275 () (|tptp.'divide$'| @t56)) % 203.66/203.94 (define @t276 () (|tptp.'fun_app$'| @t275 @t16)) % 203.66/203.94 (define @t277 () (- @t56 1)) % 203.66/203.94 (define @t278 () (|tptp.'divide$'| @t277)) % 203.66/203.94 (define @t279 () (|tptp.'fun_app$'| @t278 @t55)) % 203.66/203.94 (define @t280 () (|tptp.'nat$'| @t279)) % 203.66/203.94 (define @t281 () (|tptp.'fun_app$d'| @t175 @t280)) % 203.66/203.94 (define @t282 () (|tptp.'cong$'| @t281 @t14)) % 203.66/203.94 (define @t283 () (|tptp.'fun_app$b'| @t282 @t9)) % 203.66/203.94 (define @t284 () (< @t56 1)) % 203.66/203.94 (define @t285 () (not @t284)) % 203.66/203.94 (define @t286 () (=> @t285 @t283)) % 203.66/203.94 (define @t287 () (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t55))) % 203.66/203.94 (define @t288 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 @t287) @t14) @t9)) % 203.66/203.94 (define @t289 () (=> @t284 @t288)) % 203.66/203.94 (define @t290 () (and @t289 @t286)) % 203.66/203.94 (define @t291 () (not @t290)) % 203.66/203.94 (define @t292 () (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| @t57))) % 203.66/203.94 (define @t293 () (|tptp.'member$a'| @t54 @t292)) % 203.66/203.94 (define @t294 () (=> @t293 @t291)) % 203.66/203.94 (define @t295 () (@list @t54)) % 203.66/203.94 (define @t296 () (forall @t295 @t294)) % 203.66/203.94 (define @t297 () (and @t296 @t184)) % 203.66/203.94 (define @t298 () (=> @t67 @t297)) % 203.66/203.94 (define @t299 () (=> @t69 @t155)) % 203.66/203.94 (define @t300 () (and @t299 @t298)) % 203.66/203.94 (define @t301 () (|tptp.'member$'| @t66 @t211)) % 203.66/203.94 (define @t302 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| |tptp.'ys$'|)) % 203.66/203.94 (define @t303 () (and @t302 @t301)) % 203.66/203.94 (define @t304 () (=> @t303 @t300)) % 203.66/203.94 (define @t305 () (@list @t66 @t9 @t52 @t57)) % 203.66/203.94 (define @t306 () (forall @t305 @t304)) % 203.66/203.94 (define @t307 () (|tptp.'cons$'| |tptp.'y$'| |tptp.'ys$'|)) % 203.66/203.94 (define @t308 () (|tptp.'fun_app$d'| @t74 @t54)) % 203.66/203.94 (define @t309 () (|tptp.'of_nat$'| @t308)) % 203.66/203.94 (define @t310 () (|tptp.'of_nat$'| @t272)) % 203.66/203.94 (define @t311 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t307)) % 203.66/203.94 (define @t312 () (@var "A__questionmark_v1" |tptp.'Pratt_list$'|)) % 203.66/203.94 (define @t313 () (|tptp.'set$'| @t312)) % 203.66/203.94 (define @t314 () (@var "A__questionmark_v3" |tptp.'Pratt_list$'|)) % 203.66/203.94 (define @t315 () (|tptp.'set$'| @t314)) % 203.66/203.94 (define @t316 () (@list @t54 @t50)) % 203.66/203.95 (define @t317 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t314)) % 203.66/203.95 (define @t318 () (|tptp.'fun_app$'| @t278 @t51)) % 203.66/203.95 (define @t319 () (|tptp.'nat$'| @t318)) % 203.66/203.95 (define @t320 () (|tptp.'fun_app$d'| @t175 @t319)) % 203.66/203.95 (define @t321 () (|tptp.'cong$'| @t320 @t14)) % 203.66/203.95 (define @t322 () (|tptp.'fun_app$b'| @t321 @t9)) % 203.66/203.95 (define @t323 () (=> @t285 @t322)) % 203.66/203.95 (define @t324 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t51))) @t14) @t9)) % 203.66/203.95 (define @t325 () (=> @t284 @t324)) % 203.66/203.95 (define @t326 () (and @t325 @t323)) % 203.66/203.95 (define @t327 () (not @t326)) % 203.66/203.95 (define @t328 () (@var "A__questionmark_v4" |tptp.'Pratt_list$'|)) % 203.66/203.95 (define @t329 () (|tptp.'set$'| @t328)) % 203.66/203.95 (define @t330 () (@var "A__questionmark_v6" |tptp.'Nat$'|)) % 203.66/203.95 (define @t331 () (|tptp.'member$'| (|tptp.'triple$'| @t9 @t52 @t330) @t329)) % 203.66/203.95 (define @t332 () (|tptp.'member$'| (|tptp.'prime$'| @t50) @t329)) % 203.66/203.95 (define @t333 () (|tptp.'of_nat$'| @t330)) % 203.66/203.95 (define @t334 () (= @t58 (|tptp.'times$'| @t51 @t333))) % 203.66/203.95 (define @t335 () (and @t334 @t332 @t331 @t327)) % 203.66/203.95 (define @t336 () (@list @t50 @t330)) % 203.66/203.95 (define @t337 () (exists @t336 @t335)) % 203.66/203.95 (define @t338 () (= @t58 1)) % 203.66/203.95 (define @t339 () (or @t338 @t337)) % 203.66/203.95 (define @t340 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t328)) % 203.66/203.95 (define @t341 () (< 1 @t56)) % 203.66/203.95 (define @t342 () (not (and @t341 @t184 @t340 @t339))) % 203.66/203.95 (define @t343 () (|tptp.'cons$'| @t64 @t328)) % 203.66/203.95 (define @t344 () (@var "A__questionmark_v0" |tptp.'Pratt_list$'|)) % 203.66/203.95 (define @t345 () (= @t344 @t343)) % 203.66/203.95 (define @t346 () (@list @t9 @t52 @t57 @t328)) % 203.66/203.95 (define @t347 () (@var "A__questionmark_v2" |tptp.'Pratt_list$'|)) % 203.66/203.95 (define @t348 () (|tptp.'set$'| @t347)) % 203.66/203.95 (define @t349 () (|tptp.'nat$'| @t277)) % 203.66/203.95 (define @t350 () (|tptp.'triple$'| @t9 @t57 @t349)) % 203.66/203.95 (define @t351 () (|tptp.'member$'| @t350 @t348)) % 203.66/203.95 (define @t352 () (=> @t285 @t351)) % 203.66/203.95 (define @t353 () (|tptp.'member$'| (|tptp.'triple$'| @t9 @t57 @t99) @t348)) % 203.66/203.95 (define @t354 () (=> @t284 @t353)) % 203.66/203.95 (define @t355 () (|tptp.'power$'| @t57)) % 203.66/203.95 (define @t356 () (|tptp.'fun_app$d'| @t355 @t349)) % 203.66/203.95 (define @t357 () (|tptp.'cong$'| @t356 @t14)) % 203.66/203.95 (define @t358 () (|tptp.'fun_app$b'| @t357 @t9)) % 203.66/203.95 (define @t359 () (=> @t285 @t358)) % 203.66/203.95 (define @t360 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t355 @t99) @t14) @t9)) % 203.66/203.95 (define @t361 () (=> @t284 @t360)) % 203.66/203.95 (define @t362 () (and @t361 @t359 @t354 @t352)) % 203.66/203.95 (define @t363 () (exists @t201 @t362)) % 203.66/203.95 (define @t364 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t347)) % 203.66/203.95 (define @t365 () (not (and @t341 @t364 @t363))) % 203.66/203.95 (define @t366 () (|tptp.'cons$'| @t61 @t347)) % 203.66/203.95 (define @t367 () (= @t344 @t366)) % 203.66/203.95 (define @t368 () (@list @t9 @t347)) % 203.66/203.95 (define @t369 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t344)) % 203.66/203.95 (define @t370 () (not @t369)) % 203.66/203.95 (define @t371 () (@list @t344)) % 203.66/203.95 (define @t372 () (|tptp.'pratt_triple$'| @t9 @t52)) % 203.66/203.95 (define @t373 () (|tptp.'times$'| @t16 @t58)) % 203.66/203.95 (define @t374 () (< 0 @t55)) % 203.66/203.95 (define @t375 () (@list @t15 @t9 @t52 @t57 @t54)) % 203.66/203.95 (define @t376 () (|tptp.'times$a'| @t15)) % 203.66/203.95 (define @t377 () (= @t1 0)) % 203.66/203.95 (define @t378 () (or @t113 @t377)) % 203.66/203.95 (define @t379 () (|tptp.'times$'| @t2 @t1)) % 203.66/203.95 (define @t380 () (= @t379 0)) % 203.66/203.95 (define @t381 () (= @t9 |tptp.'zero$'|)) % 203.66/203.95 (define @t382 () (or @t111 @t381)) % 203.66/203.95 (define @t383 () (|tptp.'fun_app$d'| @t376 @t9)) % 203.66/203.95 (define @t384 () (= @t383 |tptp.'zero$'|)) % 203.66/203.95 (define @t385 () (= @t1 @t179)) % 203.66/203.95 (define @t386 () (|tptp.'times$'| @t2 @t179)) % 203.66/203.95 (define @t387 () (= @t379 @t386)) % 203.66/203.95 (define @t388 () (= @t9 @t52)) % 203.66/203.95 (define @t389 () (|tptp.'fun_app$d'| @t376 @t52)) % 203.66/203.95 (define @t390 () (= @t383 @t389)) % 203.66/203.95 (define @t391 () (= @t2 @t179)) % 203.66/203.95 (define @t392 () (|tptp.'times$'| @t179 @t1)) % 203.66/203.95 (define @t393 () (= @t15 @t52)) % 203.66/203.95 (define @t394 () (|tptp.'times$a'| @t52)) % 203.66/203.95 (define @t395 () (|tptp.'fun_app$d'| @t394 @t9)) % 203.66/203.95 (define @t396 () (|tptp.'times$'| @t16 @t56)) % 203.66/203.95 (define @t397 () (|tptp.'times$'| @t16 @t53)) % 203.66/203.95 (define @t398 () (= @t396 @t397)) % 203.66/203.95 (define @t399 () (|tptp.'times$'| @t53 @t56)) % 203.66/203.95 (define @t400 () (and @t274 @t163)) % 203.66/203.95 (define @t401 () (= @t1 1)) % 203.66/203.95 (define @t402 () (or @t113 @t401)) % 203.66/203.95 (define @t403 () (|tptp.'times$'| @t1 @t2)) % 203.66/203.95 (define @t404 () (|tptp.'divide$a'| @t383)) % 203.66/203.95 (define @t405 () (|tptp.'divide$'| @t379)) % 203.66/203.95 (define @t406 () (|tptp.'times$a'| @t9)) % 203.66/203.95 (define @t407 () (|tptp.'fun_app$d'| @t406 @t15)) % 203.66/203.95 (define @t408 () (|tptp.'divide$a'| @t407)) % 203.66/203.95 (define @t409 () (|tptp.'divide$'| @t403)) % 203.66/203.95 (define @t410 () (|tptp.'divide$a'| @t9)) % 203.66/203.95 (define @t411 () (|tptp.'fun_app$d'| @t410 @t52)) % 203.66/203.95 (define @t412 () (|tptp.'fun_app$d'| @t404 @t389)) % 203.66/203.95 (define @t413 () (=> @t145 (= @t412 @t411))) % 203.66/203.95 (define @t414 () (|tptp.'divide$'| @t1)) % 203.66/203.95 (define @t415 () (|tptp.'fun_app$'| @t414 @t179)) % 203.66/203.95 (define @t416 () (|tptp.'fun_app$'| @t405 @t386)) % 203.66/203.95 (define @t417 () (=> @t146 (= @t416 @t415))) % 203.66/203.95 (define @t418 () (|tptp.'fun_app$d'| @t394 @t15)) % 203.66/203.95 (define @t419 () (|tptp.'times$'| @t179 @t2)) % 203.66/203.95 (define @t420 () (|tptp.'times$'| @t56 @t16)) % 203.66/203.95 (define @t421 () (|tptp.'divide$'| @t396)) % 203.66/203.95 (define @t422 () (|tptp.'times$'| @t1 @t179)) % 203.66/203.95 (define @t423 () (|tptp.'times$'| @t2 @t422)) % 203.66/203.95 (define @t424 () (|tptp.'fun_app$d'| @t406 @t52)) % 203.66/203.95 (define @t425 () (|tptp.'fun_app$d'| @t376 @t424)) % 203.66/203.95 (define @t426 () (= @t379 @t403)) % 203.66/203.95 (define @t427 () (= @t383 @t407)) % 203.66/203.95 (define @t428 () (not @t377)) % 203.66/203.95 (define @t429 () (and @t146 @t428)) % 203.66/203.95 (define @t430 () (not @t380)) % 203.66/203.95 (define @t431 () (not @t381)) % 203.66/203.95 (define @t432 () (and @t145 @t431)) % 203.66/203.95 (define @t433 () (not @t384)) % 203.66/203.95 (define @t434 () (= @t387 @t385)) % 203.66/203.95 (define @t435 () (= @t390 @t388)) % 203.66/203.95 (define @t436 () (= (= @t403 @t419) @t385)) % 203.66/203.95 (define @t437 () (= (= @t407 @t418) @t388)) % 203.66/203.95 (define @t438 () (|tptp.'times$'| @t2 @t86)) % 203.66/203.95 (define @t439 () (|tptp.'fun_app$d'| @t376 @t76)) % 203.66/203.95 (define @t440 () (|tptp.'fun_app$f'| @t157 @t52)) % 203.66/203.95 (define @t441 () (|tptp.'times$'| @t85 @t440)) % 203.66/203.95 (define @t442 () (@list @t2 @t1 @t52)) % 203.66/203.95 (define @t443 () (|tptp.'fun_app$d'| @t95 @t52)) % 203.66/203.95 (define @t444 () (|tptp.'times$a'| @t75)) % 203.66/203.95 (define @t445 () (|tptp.'fun_app$d'| @t444 @t443)) % 203.66/203.95 (define @t446 () (|tptp.'times$'| @t1 @t85)) % 203.66/203.95 (define @t447 () (|tptp.'fun_app$d'| @t406 @t75)) % 203.66/203.95 (define @t448 () (|tptp.'times$'| @t56 @t53)) % 203.66/203.95 (define @t449 () (|tptp.'nat$'| @t448)) % 203.66/203.95 (define @t450 () (- @t397 @t448)) % 203.66/203.95 (define @t451 () (|tptp.'times$'| @t195 @t53)) % 203.66/203.95 (define @t452 () (< @t397 @t448)) % 203.66/203.95 (define @t453 () (not @t452)) % 203.66/203.95 (define @t454 () (|tptp.'times$'| 0 @t53)) % 203.66/203.95 (define @t455 () (- @t396 @t397)) % 203.66/203.95 (define @t456 () (- @t56 @t53)) % 203.66/203.95 (define @t457 () (|tptp.'times$'| @t16 @t456)) % 203.66/203.95 (define @t458 () (< @t396 @t397)) % 203.66/203.95 (define @t459 () (not @t458)) % 203.66/203.95 (define @t460 () (not @t115)) % 203.66/203.95 (define @t461 () (|tptp.'times$'| @t16 0)) % 203.66/203.95 (define @t462 () (|tptp.'times$'| @t2 @t224)) % 203.66/203.95 (define @t463 () (|tptp.'fun_app$d'| @t376 @t57)) % 203.66/203.95 (define @t464 () (|tptp.'times$'| @t179 @t224)) % 203.66/203.95 (define @t465 () (|tptp.'times$a'| @t57)) % 203.66/203.95 (define @t466 () (|tptp.'times$'| @t1 @t224)) % 203.66/203.95 (define @t467 () (|tptp.'fun_app$d'| @t406 @t57)) % 203.66/203.95 (define @t468 () (< 0 @t379)) % 203.66/203.95 (define @t469 () (< @t1 0)) % 203.66/203.95 (define @t470 () (< @t2 0)) % 203.66/203.95 (define @t471 () (and @t470 @t469)) % 203.66/203.95 (define @t472 () (< 0 @t1)) % 203.66/203.95 (define @t473 () (and @t470 @t472)) % 203.66/203.95 (define @t474 () (and @t88 @t469)) % 203.66/203.95 (define @t475 () (< @t379 0)) % 203.66/203.95 (define @t476 () (|tptp.'fun_app$b'| (|tptp.'less$'| @t383) |tptp.'zero$'|)) % 203.66/203.95 (define @t477 () (|tptp.'fun_app$b'| @t80 @t9)) % 203.66/203.95 (define @t478 () (and @t81 (|tptp.'fun_app$b'| (|tptp.'less$'| @t9) |tptp.'zero$'|))) % 203.66/203.95 (define @t479 () (|tptp.'fun_app$b'| @t80 @t383)) % 203.66/203.95 (define @t480 () (and @t88 @t472)) % 203.66/203.95 (define @t481 () (< @t179 @t1)) % 203.66/203.95 (define @t482 () (< @t379 @t386)) % 203.66/203.95 (define @t483 () (< @t1 @t179)) % 203.66/203.95 (define @t484 () (and @t222 (< @t179 0))) % 203.66/203.95 (define @t485 () (and (|tptp.'fun_app$b'| @t79 @t9) @t190)) % 203.66/203.95 (define @t486 () (and @t222 @t191)) % 203.66/203.95 (define @t487 () (< 1 @t1)) % 203.66/203.95 (define @t488 () (= @t379 1)) % 203.66/203.95 (define @t489 () (and @t178 @t185)) % 203.66/203.95 (define @t490 () (|tptp.'times$'| @t53 @t16)) % 203.66/203.95 (define @t491 () (|tptp.'cong$a'| @t379 0)) % 203.66/203.95 (define @t492 () (|tptp.'cong$'| @t383 |tptp.'zero$'|)) % 203.66/203.95 (define @t493 () (|tptp.'fun_app$'| @t192 @t53)) % 203.66/203.95 (define @t494 () (|tptp.'nat$'| @t396)) % 203.66/203.95 (define @t495 () (< 1 @t53)) % 203.66/203.95 (define @t496 () (not @t105)) % 203.66/203.95 (define @t497 () (|tptp.'fun_app$d'| @t74 @t349)) % 203.66/203.95 (define @t498 () (|tptp.'fun_app$'| @t421 @t397)) % 203.66/203.95 (define @t499 () (= @t498 (|tptp.'fun_app$'| @t275 @t53))) % 203.66/203.95 (define @t500 () (and @t345 @t341 @t184 @t340 @t339)) % 203.66/203.95 (define @t501 () (forall @t346 (=> @t500 false))) % 203.66/203.95 (define @t502 () (and @t367 @t341 @t364 @t363)) % 203.66/203.95 (define @t503 () (forall @t368 (=> @t502 false))) % 203.66/203.95 (define @t504 () (= @t344 |tptp.'nil$'|)) % 203.66/203.95 (define @t505 () (=> @t504 false)) % 203.66/203.95 (define @t506 () (and @t369 @t505 @t503 @t501)) % 203.66/203.95 (define @t507 () (forall @t371 (=> @t506 false))) % 203.66/203.95 (define @t508 () (- @t53 1)) % 203.66/203.95 (define @t509 () (< @t53 1)) % 203.66/203.95 (define @t510 () (not @t509)) % 203.66/203.95 (define @t511 () (@var "A__questionmark_v5" |tptp.'Pratt_list$'|)) % 203.66/203.95 (define @t512 () (|tptp.'set$'| @t511)) % 203.66/203.95 (define @t513 () (@var "A__questionmark_v7" |tptp.'Nat$'|)) % 203.66/203.95 (define @t514 () (@var "A__questionmark_v1" tptp.tlbool)) % 203.66/203.95 (define @t515 () (= @t514 tptp.tltrue)) % 203.66/203.95 (define @t516 () (= @t515 (and @t495 @t374 (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t511) (or (= @t55 1) (exists (@list @t330 @t513) (and (= @t55 (|tptp.'times$'| @t333 (|tptp.'of_nat$'| @t513))) (|tptp.'member$'| (|tptp.'prime$'| @t330) @t512) (|tptp.'member$'| (|tptp.'triple$'| @t52 @t57 @t513) @t512) (not (and (=> @t509 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t355 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t333))) @t14) @t52)) (=> @t510 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t355 (|tptp.'nat$'| (|tptp.'fun_app$'| (|tptp.'divide$'| @t508) @t333))) @t14) @t52)))))))))) % 203.66/203.95 (define @t517 () (|tptp.'cons$'| (|tptp.'triple$'| @t52 @t57 @t54) @t511)) % 203.66/203.95 (define @t518 () (= @t344 @t517)) % 203.66/203.95 (define @t519 () (@list @t52 @t57 @t54 @t511)) % 203.66/203.95 (define @t520 () (|tptp.'nat$'| @t508)) % 203.66/203.95 (define @t521 () (|tptp.'power$'| @t54)) % 203.66/203.95 (define @t522 () (= @t515 (and @t495 @t317 (exists @t295 (and (=> @t509 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t521 @t99) @t14) @t52)) (=> @t510 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t521 @t520) @t14) @t52)) (=> @t509 (|tptp.'member$'| (|tptp.'triple$'| @t52 @t54 @t99) @t315)) (=> @t510 (|tptp.'member$'| (|tptp.'triple$'| @t52 @t54 @t520) @t315))))))) % 203.66/203.95 (define @t523 () (|tptp.'cons$'| (|tptp.'prime$'| @t52) @t314)) % 203.66/203.95 (define @t524 () (= @t344 @t523)) % 203.66/203.95 (define @t525 () (@list @t52 @t314)) % 203.66/203.95 (define @t526 () (= @t369 @t515)) % 203.66/203.95 (define @t527 () (@list @t344 @t514)) % 203.66/203.95 (define @t528 () (|tptp.'cons$'| @t6 @t347)) % 203.66/203.95 (define @t529 () (= @t344 @t528)) % 203.66/203.95 (define @t530 () (@list @t6 @t347)) % 203.66/203.95 (define @t531 () (|tptp.'accp$'| |tptp.'valid_cert_rel$'|)) % 203.66/203.95 (define @t532 () (|tptp.'fun_app$e'| @t531 |tptp.'nil$'|)) % 203.66/203.95 (define @t533 () (|tptp.'fun_app$e'| @t531 @t344)) % 203.66/203.95 (define @t534 () (|tptp.'fun_app$e'| @t531 @t343)) % 203.66/203.95 (define @t535 () (|tptp.'fun_app$e'| @t531 @t366)) % 203.66/203.95 (define @t536 () (|tptp.'cons$'| @t140 @t314)) % 203.66/203.95 (define @t537 () (|tptp.'cons$'| @t66 @t312)) % 203.66/203.95 (define @t538 () (|tptp.'dvd$'| @t179)) % 203.66/203.95 (define @t539 () (|tptp.'fun_app$c'| @t538 @t2)) % 203.66/203.95 (define @t540 () (|tptp.'fun_app$c'| |tptp.'prime$b'| @t179)) % 203.66/203.95 (define @t541 () (|tptp.'fun_app$c'| @t132 @t179)) % 203.66/203.95 (define @t542 () (@list @t179)) % 203.66/203.95 (define @t543 () (|tptp.'dvd$a'| @t52)) % 203.66/203.95 (define @t544 () (|tptp.'fun_app$b'| @t543 @t15)) % 203.66/203.95 (define @t545 () (|tptp.'fun_app$b'| |tptp.'prime$a'| @t52)) % 203.66/203.95 (define @t546 () (@list @t52 @t57 @t54)) % 203.66/203.95 (define @t547 () (|tptp.'dvd$a'| @t15)) % 203.66/203.95 (define @t548 () (|tptp.'dvd$'| @t2)) % 203.66/203.95 (define @t549 () (|tptp.'dvd$a'| |tptp.'zero$'|)) % 203.66/203.95 (define @t550 () (|tptp.'fun_app$b'| @t549 @t15)) % 203.66/203.95 (define @t551 () (|tptp.'dvd$'| 0)) % 203.66/203.95 (define @t552 () (|tptp.'fun_app$c'| @t551 @t2)) % 203.66/203.95 (define @t553 () (|tptp.'dvd$a'| @t9)) % 203.66/203.95 (define @t554 () (|tptp.'fun_app$b'| @t553 @t52)) % 203.66/203.95 (define @t555 () (|tptp.'divide$a'| @t52)) % 203.66/203.95 (define @t556 () (|tptp.'fun_app$d'| @t555 @t15)) % 203.66/203.95 (define @t557 () (|tptp.'fun_app$d'| @t410 @t15)) % 203.66/203.95 (define @t558 () (|tptp.'dvd$a'| @t557)) % 203.66/203.95 (define @t559 () (|tptp.'fun_app$b'| @t547 @t52)) % 203.66/203.95 (define @t560 () (|tptp.'fun_app$b'| @t547 @t9)) % 203.66/203.95 (define @t561 () (and @t560 @t559)) % 203.66/203.95 (define @t562 () (|tptp.'dvd$'| @t1)) % 203.66/203.95 (define @t563 () (|tptp.'fun_app$c'| @t562 @t179)) % 203.66/203.95 (define @t564 () (|tptp.'divide$'| @t179)) % 203.66/203.95 (define @t565 () (|tptp.'fun_app$'| @t564 @t2)) % 203.66/203.95 (define @t566 () (|tptp.'fun_app$'| @t414 @t2)) % 203.66/203.95 (define @t567 () (|tptp.'dvd$'| @t566)) % 203.66/203.95 (define @t568 () (|tptp.'fun_app$c'| @t548 @t179)) % 203.66/203.95 (define @t569 () (|tptp.'fun_app$c'| @t548 @t1)) % 203.66/203.95 (define @t570 () (and @t569 @t568)) % 203.66/203.95 (define @t571 () (|tptp.'dvd$a'| @t494)) % 203.66/203.95 (define @t572 () (|tptp.'fun_app$b'| @t571 (|tptp.'nat$'| @t397))) % 203.66/203.95 (define @t573 () (|tptp.'dvd$'| @t379)) % 203.66/203.95 (define @t574 () (|tptp.'fun_app$c'| @t573 @t386)) % 203.66/203.95 (define @t575 () (|tptp.'dvd$a'| @t383)) % 203.66/203.95 (define @t576 () (|tptp.'dvd$'| @t403)) % 203.66/203.95 (define @t577 () (|tptp.'dvd$a'| @t407)) % 203.66/203.95 (define @t578 () (|tptp.'fun_app$c'| @t573 1)) % 203.66/203.95 (define @t579 () (|tptp.'fun_app$c'| @t562 1)) % 203.66/203.95 (define @t580 () (|tptp.'fun_app$c'| @t548 1)) % 203.66/203.95 (define @t581 () (and @t580 @t579)) % 203.66/203.95 (define @t582 () (|tptp.'fun_app$b'| @t575 |tptp.'one$'|)) % 203.66/203.95 (define @t583 () (|tptp.'fun_app$b'| @t553 |tptp.'one$'|)) % 203.66/203.95 (define @t584 () (|tptp.'fun_app$b'| @t547 |tptp.'one$'|)) % 203.66/203.95 (define @t585 () (and @t584 @t583)) % 203.66/203.95 (define @t586 () (|tptp.'times$a'| @t557)) % 203.66/203.95 (define @t587 () (= (|tptp.'fun_app$d'| @t586 @t15) @t9)) % 203.66/203.95 (define @t588 () (= (|tptp.'times$'| @t566 @t2) @t1)) % 203.66/203.95 (define @t589 () (|tptp.'divide$a'| |tptp.'one$'|)) % 203.66/203.95 (define @t590 () (|tptp.'fun_app$d'| @t589 @t15)) % 203.66/203.95 (define @t591 () (|tptp.'divide$'| 1)) % 203.66/203.95 (define @t592 () (|tptp.'fun_app$'| @t591 @t2)) % 203.66/203.95 (define @t593 () (|tptp.'fun_app$d'| @t198 @t9)) % 203.66/203.95 (define @t594 () (|tptp.'fun_app$'| @t199 @t1)) % 203.66/203.95 (define @t595 () (and @t560 @t554)) % 203.66/203.95 (define @t596 () (and @t569 @t563)) % 203.66/203.95 (define @t597 () (|tptp.'dvd$a'| @t57)) % 203.66/203.95 (define @t598 () (|tptp.'dvd$'| @t224)) % 203.66/203.95 (define @t599 () (|tptp.'fun_app$b'| @t543 @t9)) % 203.66/203.95 (define @t600 () (|tptp.'fun_app$b'| @t547 @t99)) % 203.66/203.95 (define @t601 () (= (= @t557 @t556) @t388)) % 203.66/203.95 (define @t602 () (= (= @t566 @t565) @t385)) % 203.66/203.95 (define @t603 () (|tptp.'fun_app$b'| @t553 @t15)) % 203.66/203.95 (define @t604 () (|tptp.'fun_app$d'| @t555 @t9)) % 203.66/203.95 (define @t605 () (|tptp.'fun_app$c'| @t562 @t2)) % 203.66/203.95 (define @t606 () (|tptp.'fun_app$'| @t564 @t1)) % 203.66/203.95 (define @t607 () (|tptp.'divide$a'| @t556)) % 203.66/203.95 (define @t608 () (|tptp.'divide$'| @t565)) % 203.66/203.95 (define @t609 () (|tptp.'fun_app$c'| @t548 @t256)) % 203.66/203.95 (define @t610 () (= @t1 @t386)) % 203.66/203.95 (define @t611 () (= @t9 @t389)) % 203.66/203.95 (define @t612 () (|tptp.'fun_app$c'| @t548 @t422)) % 203.66/203.95 (define @t613 () (|tptp.'fun_app$b'| @t547 @t424)) % 203.66/203.95 (define @t614 () (|tptp.'fun_app$c'| @t573 @t179)) % 203.66/203.95 (define @t615 () (|tptp.'fun_app$b'| @t575 @t52)) % 203.66/203.95 (define @t616 () (and @t569 (|tptp.'fun_app$c'| @t538 @t224))) % 203.66/203.95 (define @t617 () (and @t560 (|tptp.'fun_app$b'| @t543 @t57))) % 203.66/203.95 (define @t618 () (= (= @t557 |tptp.'zero$'|) @t381)) % 203.66/203.95 (define @t619 () (= (= @t566 0) @t377)) % 203.66/203.95 (define @t620 () (|tptp.'fun_app$c'| @t562 @t419)) % 203.66/203.95 (define @t621 () (|tptp.'fun_app$b'| @t553 @t418)) % 203.66/203.95 (define @t622 () (|tptp.'fun_app$d'| (|tptp.'divide$a'| @t424) @t15)) % 203.66/203.95 (define @t623 () (= (|tptp.'fun_app$d'| @t586 @t52) @t622)) % 203.66/203.95 (define @t624 () (|tptp.'fun_app$'| (|tptp.'divide$'| @t422) @t2)) % 203.66/203.95 (define @t625 () (= (|tptp.'times$'| @t566 @t179) @t624)) % 203.66/203.95 (define @t626 () (= (|tptp.'fun_app$d'| @t555 @t383) (|tptp.'fun_app$d'| @t607 @t9))) % 203.66/203.95 (define @t627 () (= (|tptp.'fun_app$'| @t564 @t379) (|tptp.'fun_app$'| @t608 @t1))) % 203.66/203.95 (define @t628 () (|tptp.'divide$a'| @t57)) % 203.66/203.95 (define @t629 () (|tptp.'divide$'| @t224)) % 203.66/203.95 (define @t630 () (|tptp.'fun_app$b'| @t558 @t52)) % 203.66/203.95 (define @t631 () (|tptp.'fun_app$c'| @t567 @t179)) % 203.66/203.95 (define @t632 () (not @t603)) % 203.66/203.95 (define @t633 () (or @t560 @t559)) % 203.66/203.95 (define @t634 () (or @t569 @t568)) % 203.66/203.95 (define @t635 () (and @t155 @t603)) % 203.66/203.95 (define @t636 () (= (= @t557 @t52) (= @t9 @t418))) % 203.66/203.95 (define @t637 () (and @t145 @t560)) % 203.66/203.95 (define @t638 () (= (= @t566 @t179) (= @t1 @t419))) % 203.66/203.95 (define @t639 () (and @t146 @t569)) % 203.66/203.95 (define @t640 () (|tptp.'fun_app$b'| @t553 @t57)) % 203.66/203.95 (define @t641 () (|tptp.'fun_app$c'| @t562 @t224)) % 203.66/203.95 (define @t642 () (not @t584)) % 203.66/203.95 (define @t643 () (@list @t1)) % 203.66/203.95 (define @t644 () (not @t580)) % 203.66/203.95 (define @t645 () (= @t53 @t55)) % 203.66/203.95 (define @t646 () (not (|tptp.'fun_app$b'| @t547 @t57))) % 203.66/203.95 (define @t647 () (not @t560)) % 203.66/203.95 (define @t648 () (= @t447 (|tptp.'fun_app$d'| @t465 @t308))) % 203.66/203.95 (define @t649 () (not (|tptp.'fun_app$c'| @t548 @t224))) % 203.66/203.95 (define @t650 () (not @t569)) % 203.66/203.95 (define @t651 () (= @t446 (|tptp.'times$'| @t224 (|tptp.'fun_app$f'| @t84 @t54)))) % 203.66/203.95 (define @t652 () (@list @t2 @t1 @t52 @t224 @t54)) % 203.66/203.95 (define @t653 () (= @t164 |tptp.'zero$a'|)) % 203.66/203.95 (define @t654 () (= @t166 |tptp.'zero$b'|)) % 203.66/203.95 (define @t655 () (@list @t66 @t312)) % 203.66/203.95 (define @t656 () (not @t504)) % 203.66/203.95 (define @t657 () (|tptp.'fun_app$d'| @t589 @t9)) % 203.66/203.95 (define @t658 () (and @t145 @t583)) % 203.66/203.95 (define @t659 () (|tptp.'fun_app$'| @t591 @t1)) % 203.66/203.95 (define @t660 () (and @t146 @t579)) % 203.66/203.95 (define @t661 () (|tptp.'fun_app$b'| @t543 |tptp.'one$'|)) % 203.66/203.95 (define @t662 () (|tptp.'fun_app$c'| @t538 1)) % 203.66/203.95 (define @t663 () (@list @t52 @t57)) % 203.66/203.95 (define @t664 () (@var "A__questionmark_v0" |tptp.'Int_bool_fun$'|)) % 203.66/203.95 (define @t665 () (< @t53 @t55)) % 203.66/203.95 (define @t666 () (and @t105 @t92)) % 203.66/203.95 (define @t667 () (@var "A__questionmark_v1" |tptp.'Pratt_list_bool_fun$'|)) % 203.66/203.95 (define @t668 () (@list @t140 @t314)) % 203.66/203.95 (define @t669 () (@var "A__questionmark_v0" |tptp.'Pratt_list_pratt_list_bool_fun_fun$'|)) % 203.66/203.95 (define @t670 () (@var "A__questionmark_v6" |tptp.'Pratt_list$'|)) % 203.66/203.95 (define @t671 () (@var "A__questionmark_v5" |tptp.'Pratt$'|)) % 203.66/203.95 (define @t672 () (@var "A__questionmark_v3" |tptp.'Pratt$'|)) % 203.66/203.95 (define @t673 () (|tptp.'cons$'| @t672 @t328)) % 203.66/203.95 (define @t674 () (|tptp.'fun_app$i'| @t669 @t673)) % 203.66/203.95 (define @t675 () (|tptp.'fun_app$i'| @t669 |tptp.'nil$'|)) % 203.66/203.95 (define @t676 () (@list @t672 @t328)) % 203.66/203.95 (define @t677 () (@var "A__questionmark_v3" |tptp.'Pratt_list_list$'|)) % 203.66/203.95 (define @t678 () (@var "A__questionmark_v0" |tptp.'Pratt_list_list$'|)) % 203.66/203.95 (define @t679 () (@var "A__questionmark_v1" |tptp.'Pratt_list_list$'|)) % 203.66/203.95 (define @t680 () (=> @t529 @t656)) % 203.66/203.95 (define @t681 () (@list @t344 @t6 @t347)) % 203.66/203.95 (define @t682 () (forall @t681 @t680)) % 203.66/203.95 (define @t683 () (@var "A__questionmark_v2" |tptp.'Nat_list$'|)) % 203.66/203.95 (define @t684 () (@var "A__questionmark_v3" |tptp.'Nat_list$'|)) % 203.66/203.95 (define @t685 () (@var "A__questionmark_v1" |tptp.'Nat_list$'|)) % 203.66/203.95 (define @t686 () (|tptp.'member$a'| @t15 (|tptp.'set$a'| @t685))) % 203.66/203.95 (define @t687 () (@list @t15 @t685)) % 203.66/203.95 (define @t688 () (|tptp.'member$'| @t66 @t313)) % 203.66/203.95 (define @t689 () (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t99) @t15)) % 203.66/203.95 (define @t690 () (and (= @t2 (|tptp.'times$'| @t224 @t269)) (|tptp.'fun_app$c'| @t598 @t1) (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t269) @t179))) % 203.66/203.95 (define @t691 () (@list @t224 @t269)) % 203.66/203.95 (define @t692 () (and (= @t15 (|tptp.'fun_app$d'| @t465 @t54)) (|tptp.'fun_app$b'| @t597 @t9) (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t54) @t52))) % 203.66/203.95 (define @t693 () (@list @t57 @t54)) % 203.66/203.95 (define @t694 () (|tptp.'times$'| @t16 @t55)) % 203.66/203.95 (define @t695 () (|tptp.'times$'| @t56 @t58)) % 203.66/203.95 (define @t696 () (< @t695 @t694)) % 203.66/203.95 (define @t697 () (= 0 @t53)) % 203.66/203.95 (define @t698 () (|tptp.'times$'| @t56 @t55)) % 203.66/203.95 (define @t699 () (< @t373 @t698)) % 203.66/203.95 (define @t700 () (|tptp.'fun_app$j'| (|tptp.'n_lists$'| @t15) |tptp.'nil$'|)) % 203.66/203.95 (define @t701 () (|tptp.'cons$a'| |tptp.'nil$'| |tptp.'nil$a'|)) % 203.66/203.95 (define @t702 () (|tptp.'of_nat$'| @t497)) % 203.66/203.95 (define @t703 () (|tptp.'of_nat$'| (|tptp.'totient$'| @t76))) % 203.66/203.95 (define @t704 () (|tptp.'of_nat$'| @t147)) % 203.66/203.95 (define @t705 () (|tptp.'totient$'| @t15)) % 203.66/203.95 (define @t706 () (|tptp.'of_nat$'| @t705)) % 203.66/203.95 (define @t707 () (= @t706 0)) % 203.66/203.95 (define @t708 () (=> @t97 (= @t706 @t93))) % 203.66/203.95 (define @t709 () (=> @t96 @t707)) % 203.66/203.95 (define @t710 () (|tptp.'totient$'| @t9)) % 203.66/203.95 (define @t711 () (|tptp.'of_nat$'| @t710)) % 203.66/203.95 (define @t712 () (|tptp.'of_nat$'| (|tptp.'totient$'| @t205))) % 203.66/203.95 (define @t713 () (|tptp.'of_nat$'| (|tptp.'nat$'| @t2))) % 203.66/203.95 (define @t714 () (<= 0 @t2)) % 203.66/203.95 (define @t715 () (@var "B" tptp.tlbool)) % 203.66/203.95 (define @t716 () (+ -1 @t56)) % 203.66/203.95 (define @t717 () (|tptp.'nat$'| @t716)) % 203.66/203.95 (define @t718 () (@var "BOUND_VARIABLE_13884" |tptp.'Nat$'|)) % 203.66/203.95 (define @t719 () (>= @t56 1)) % 203.66/203.95 (define @t720 () (and @t719 (not (|tptp.'member$'| (|tptp.'triple$'| @t9 @t718 @t717) @t348)))) % 203.66/203.95 (define @t721 () (not @t719)) % 203.66/203.95 (define @t722 () (and @t721 (not (|tptp.'member$'| (|tptp.'triple$'| @t9 @t718 @t99) @t348)))) % 203.66/203.95 (define @t723 () (|tptp.'power$'| @t718)) % 203.66/203.95 (define @t724 () (and @t719 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t723 @t717) @t14) @t9)))) % 203.66/203.95 (define @t725 () (and @t721 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t723 @t99) @t14) @t9)))) % 203.66/203.95 (define @t726 () (not @t364)) % 203.66/203.95 (define @t727 () (>= @t56 2)) % 203.66/203.95 (define @t728 () (not @t727)) % 203.66/203.95 (define @t729 () (@list @t9 @t347 @t718)) % 203.66/203.95 (define @t730 () (forall @t729 (or (not (= @t307 @t366)) @t728 @t726 @t725 @t724 @t722 @t720))) % 203.66/203.95 (define @t731 () (@quantifiers_skolemize @t730 1)) % 203.66/203.95 (define @t732 () (@quantifiers_skolemize @t730 0)) % 203.66/203.95 (define @t733 () (|tptp.'prime$'| @t732)) % 203.66/203.95 (define @t734 () (= @t307 (|tptp.'cons$'| @t733 @t731))) % 203.66/203.95 (define @t735 () (|tptp.'set$'| @t731)) % 203.66/203.95 (define @t736 () (|tptp.'of_nat$'| @t732)) % 203.66/203.95 (define @t737 () (|tptp.'nat$'| (+ -1 @t736))) % 203.66/203.95 (define @t738 () (@quantifiers_skolemize @t730 2)) % 203.66/203.95 (define @t739 () (>= @t736 1)) % 203.66/203.95 (define @t740 () (not @t739)) % 203.66/203.95 (define @t741 () (|tptp.'power$'| @t738)) % 203.66/203.95 (define @t742 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t731)) % 203.66/203.95 (define @t743 () (not @t742)) % 203.66/203.95 (define @t744 () (not @t734)) % 203.66/203.95 (define @t745 () (or @t744 (not (>= @t736 2)) @t743 (and @t740 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t741 @t99) @t14) @t732))) (and @t739 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t741 @t737) @t14) @t732))) (and @t740 (not (|tptp.'member$'| (|tptp.'triple$'| @t732 @t738 @t99) @t735))) (and @t739 (not (|tptp.'member$'| (|tptp.'triple$'| @t732 @t738 @t737) @t735))))) % 203.66/203.95 (define @t746 () (= |tptp.'ys$'| @t731)) % 203.66/203.95 (define @t747 () (and (= |tptp.'y$'| @t733) @t746)) % 203.66/203.95 (define @t748 () (= @t734 @t747)) % 203.66/203.95 (define @t749 () (not @t746)) % 203.66/203.95 (define @t750 () (not @t302)) % 203.66/203.95 (define @t751 () (not @t750)) % 203.66/203.95 (define @t752 () (= true false)) % 203.66/203.95 (define @t753 () (and @t750 @t746 @t742)) % 203.66/203.95 (define @t754 () (not @t745)) % 203.66/203.95 (define @t755 () (not @t730)) % 203.66/203.95 (define @t756 () (@var "BOUND_VARIABLE_13921" |tptp.'Nat$'|)) % 203.66/203.95 (define @t757 () (|tptp.'of_nat$'| @t756)) % 203.66/203.95 (define @t758 () (|tptp.'divide$'| @t716)) % 203.66/203.95 (define @t759 () (@var "BOUND_VARIABLE_13923" |tptp.'Nat$'|)) % 203.66/203.95 (define @t760 () (or (not (= @t58 (|tptp.'times$'| @t757 (|tptp.'of_nat$'| @t759)))) (not (|tptp.'member$'| (|tptp.'prime$'| @t756) @t329)) (not (|tptp.'member$'| (|tptp.'triple$'| @t9 @t52 @t759) @t329)) (and (or @t719 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t757))) @t14) @t9)) (or @t721 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t758 @t757))) @t14) @t9))))) % 203.66/203.95 (define @t761 () (not @t338)) % 203.66/203.95 (define @t762 () (and @t761 @t760)) % 203.66/203.95 (define @t763 () (not @t340)) % 203.66/203.95 (define @t764 () (>= @t58 1)) % 203.66/203.95 (define @t765 () (not @t764)) % 203.66/203.95 (define @t766 () (not @t345)) % 203.66/203.95 (define @t767 () (or @t766 @t728 @t765 @t763 @t762)) % 203.66/203.95 (define @t768 () (@list @t9 @t52 @t57 @t328 @t756 @t759)) % 203.66/203.95 (define @t769 () (forall @t768 @t767)) % 203.66/203.95 (define @t770 () (not @t769)) % 203.66/203.95 (define @t771 () (not @t367)) % 203.66/203.95 (define @t772 () (or @t771 @t728 @t726 @t725 @t724 @t722 @t720)) % 203.66/203.95 (define @t773 () (forall @t729 @t772)) % 203.66/203.95 (define @t774 () (not @t773)) % 203.66/203.95 (define @t775 () (= |tptp.'nil$'| @t344)) % 203.66/203.95 (define @t776 () (not @t775)) % 203.66/203.95 (define @t777 () (not @t776)) % 203.66/203.95 (define @t778 () (or @t370 @t777 @t774 @t770)) % 203.66/203.95 (define @t779 () (@list @t756 @t759)) % 203.66/203.95 (define @t780 () (forall @t779 @t767)) % 203.66/203.95 (define @t781 () (forall @t779 @t760)) % 203.66/203.95 (define @t782 () (forall @t779 @t761)) % 203.66/203.95 (define @t783 () (and @t782 @t781)) % 203.66/203.95 (define @t784 () (forall @t779 @t762)) % 203.66/203.95 (define @t785 () (or @t766 @t728 @t765 @t763 @t784)) % 203.66/203.95 (define @t786 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t758 @t51))) @t14) @t9)) % 203.66/203.95 (define @t787 () (not @t331)) % 203.66/203.95 (define @t788 () (not @t332)) % 203.66/203.95 (define @t789 () (not @t334)) % 203.66/203.95 (define @t790 () (forall @t336 (or @t789 @t788 @t787 (and (or @t719 @t324) (or @t721 @t786))))) % 203.66/203.95 (define @t791 () (not @t790)) % 203.66/203.95 (define @t792 () (or @t338 @t791)) % 203.66/203.95 (define @t793 () (not @t792)) % 203.66/203.95 (define @t794 () (or @t766 @t728 @t765 @t763 @t793)) % 203.66/203.95 (define @t795 () (and (=> @t721 @t324) (=> @t719 @t786))) % 203.66/203.95 (define @t796 () (not @t795)) % 203.66/203.95 (define @t797 () (not @t796)) % 203.66/203.95 (define @t798 () (or @t789 @t788 @t787 @t797)) % 203.66/203.95 (define @t799 () (and @t334 @t332 @t331 @t796)) % 203.66/203.95 (define @t800 () (forall @t336 (not @t799))) % 203.66/203.95 (define @t801 () (not @t800)) % 203.66/203.95 (define @t802 () (* -1 1)) % 203.66/203.95 (define @t803 () (+ @t56 @t802)) % 203.66/203.95 (define @t804 () (+ @t58 1)) % 203.66/203.95 (define @t805 () (>= 0 @t58)) % 203.66/203.95 (define @t806 () (+ @t56 1)) % 203.66/203.95 (define @t807 () (>= 1 @t56)) % 203.66/203.95 (define @t808 () (or @t725 @t724 @t722 @t720)) % 203.66/203.95 (define @t809 () (or @t771 @t728 @t726 @t808)) % 203.66/203.95 (define @t810 () (forall @t729 @t809)) % 203.66/203.95 (define @t811 () (@list @t718)) % 203.66/203.95 (define @t812 () (forall @t811 @t809)) % 203.66/203.95 (define @t813 () (forall @t811 @t808)) % 203.66/203.95 (define @t814 () (or @t771 @t728 @t726 @t813)) % 203.66/203.95 (define @t815 () (|tptp.'member$'| (|tptp.'triple$'| @t9 @t57 @t717) @t348)) % 203.66/203.95 (define @t816 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t355 @t717) @t14) @t9)) % 203.66/203.95 (define @t817 () (forall @t201 (or (and @t721 (not @t360)) (and @t719 (not @t816)) (and @t721 (not @t353)) (and @t719 (not @t815))))) % 203.66/203.95 (define @t818 () (not @t817)) % 203.66/203.95 (define @t819 () (not @t818)) % 203.66/203.95 (define @t820 () (or @t771 @t728 @t726 @t819)) % 203.66/203.95 (define @t821 () (=> @t719 @t815)) % 203.66/203.95 (define @t822 () (not @t821)) % 203.66/203.95 (define @t823 () (=> @t721 @t353)) % 203.66/203.95 (define @t824 () (not @t823)) % 203.66/203.95 (define @t825 () (=> @t719 @t816)) % 203.66/203.95 (define @t826 () (not @t825)) % 203.66/203.95 (define @t827 () (=> @t721 @t360)) % 203.66/203.95 (define @t828 () (not @t827)) % 203.66/203.95 (define @t829 () (or @t828 @t826 @t824 @t822)) % 203.66/203.95 (define @t830 () (and @t827 @t825 @t823 @t821)) % 203.66/203.95 (define @t831 () (forall @t201 (not @t830))) % 203.66/203.95 (define @t832 () (not @t831)) % 203.66/203.95 (define @t833 () (not (= |tptp.'nil$'| @t528))) % 203.66/203.95 (define @t834 () (not (= @t528 @t528))) % 203.66/203.95 (define @t835 () (or @t834 @t833)) % 203.66/203.95 (define @t836 () (not @t529)) % 203.66/203.95 (define @t837 () (or @t836 @t836 @t776)) % 203.66/203.95 (define @t838 () (or @t836 @t776)) % 203.66/203.95 (define @t839 () (forall @t371 @t838)) % 203.66/203.95 (define @t840 () (forall @t530 @t839)) % 203.66/203.95 (define @t841 () (forall (@list @t6 @t347 @t344) @t838)) % 203.66/203.95 (define @t842 () (forall @t768 (or (not (= @t307 @t343)) @t728 @t765 @t763 @t762))) % 203.66/203.95 (define @t843 () (not @t842)) % 203.66/203.95 (define @t844 () (= |tptp.'nil$'| @t307)) % 203.66/203.95 (define @t845 () (not @t311)) % 203.66/203.95 (define @t846 () (or @t845 @t844 @t755 @t843)) % 203.66/203.95 (define @t847 () (@quantifiers_skolemize @t842 0)) % 203.66/203.95 (define @t848 () (@quantifiers_skolemize @t842 4)) % 203.66/203.95 (define @t849 () (|tptp.'of_nat$'| @t848)) % 203.66/203.95 (define @t850 () (|tptp.'of_nat$'| @t847)) % 203.66/203.95 (define @t851 () (@quantifiers_skolemize @t842 1)) % 203.66/203.95 (define @t852 () (|tptp.'power$'| @t851)) % 203.66/203.95 (define @t853 () (>= @t850 1)) % 203.66/203.95 (define @t854 () (@quantifiers_skolemize @t842 3)) % 203.66/203.95 (define @t855 () (|tptp.'set$'| @t854)) % 203.66/203.95 (define @t856 () (@quantifiers_skolemize @t842 5)) % 203.66/203.95 (define @t857 () (@quantifiers_skolemize @t842 2)) % 203.66/203.95 (define @t858 () (|tptp.'of_nat$'| @t857)) % 203.66/203.95 (define @t859 () (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t854)) % 203.66/203.95 (define @t860 () (not @t859)) % 203.66/203.95 (define @t861 () (|tptp.'triple$'| @t847 @t851 @t857)) % 203.66/203.95 (define @t862 () (= @t307 (|tptp.'cons$'| @t861 @t854))) % 203.66/203.95 (define @t863 () (not @t862)) % 203.66/203.95 (define @t864 () (or @t863 (not (>= @t850 2)) (not (>= @t858 1)) @t860 (and (not (= @t858 1)) (or (not (= @t858 (|tptp.'times$'| @t849 (|tptp.'of_nat$'| @t856)))) (not (|tptp.'member$'| (|tptp.'prime$'| @t848) @t855)) (not (|tptp.'member$'| (|tptp.'triple$'| @t847 @t851 @t856) @t855)) (and (or @t853 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t852 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t849))) @t14) @t847)) (or (not @t853) (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t852 (|tptp.'nat$'| (|tptp.'fun_app$'| (|tptp.'divide$'| (+ -1 @t850)) @t849))) @t14) @t847))))))) % 203.66/203.95 (define @t865 () (not @t864)) % 203.66/203.95 (define @t866 () (= |tptp.'ys$'| @t854)) % 203.66/203.95 (define @t867 () (and (= |tptp.'y$'| @t861) @t866)) % 203.66/203.95 (define @t868 () (= @t862 @t867)) % 203.66/203.95 (define @t869 () (not @t866)) % 203.66/203.95 (define @t870 () (and @t750 @t866 @t859)) % 203.66/203.95 (define @t871 () (@var "BOUND_VARIABLE_12411" |tptp.'Nat$'|)) % 203.66/203.95 (define @t872 () (|tptp.'of_nat$'| @t871)) % 203.66/203.95 (define @t873 () (or (not (|tptp.'member$a'| @t871 @t292)) (and @t721 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t872))) @t14) @t9))) (and @t719 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t758 @t872))) @t14) @t9))))) % 203.66/203.95 (define @t874 () (and @t873 @t764)) % 203.66/203.95 (define @t875 () (= @t64 @t66)) % 203.66/203.95 (define @t876 () (not @t875)) % 203.66/203.95 (define @t877 () (or @t876 @t874)) % 203.66/203.95 (define @t878 () (= @t61 @t66)) % 203.66/203.95 (define @t879 () (or (not @t878) @t155)) % 203.66/203.95 (define @t880 () (and @t879 @t877)) % 203.66/203.95 (define @t881 () (not @t301)) % 203.66/203.95 (define @t882 () (or @t881 @t880)) % 203.66/203.95 (define @t883 () (forall (@list @t66 @t9 @t52 @t57 @t871) @t882)) % 203.66/203.95 (define @t884 () (@list @t871)) % 203.66/203.95 (define @t885 () (forall @t884 @t882)) % 203.66/203.95 (define @t886 () (forall @t884 @t764)) % 203.66/203.95 (define @t887 () (forall @t884 @t873)) % 203.66/203.95 (define @t888 () (and @t887 @t886)) % 203.66/203.95 (define @t889 () (forall @t884 @t874)) % 203.66/203.95 (define @t890 () (or @t876 @t889)) % 203.66/203.95 (define @t891 () (forall @t884 @t877)) % 203.66/203.95 (define @t892 () (forall @t884 @t879)) % 203.66/203.95 (define @t893 () (and @t892 @t891)) % 203.66/203.95 (define @t894 () (forall @t884 @t880)) % 203.66/203.95 (define @t895 () (or @t881 @t894)) % 203.66/203.95 (define @t896 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t758 @t55))) @t14) @t9)) % 203.66/203.95 (define @t897 () (and @t719 (not @t896))) % 203.66/203.95 (define @t898 () (and @t721 (not @t288))) % 203.66/203.95 (define @t899 () (not @t293)) % 203.66/203.95 (define @t900 () (or @t899 @t898 @t897)) % 203.66/203.95 (define @t901 () (and (forall @t295 @t900) @t764)) % 203.66/203.95 (define @t902 () (and @t879 (or @t876 @t901))) % 203.66/203.95 (define @t903 () (or @t881 @t902)) % 203.66/203.95 (define @t904 () (forall @t305 @t903)) % 203.66/203.95 (define @t905 () (or @t750 @t904)) % 203.66/203.95 (define @t906 () (or @t750 @t903)) % 203.66/203.95 (define @t907 () (or @t750 @t881 @t902)) % 203.66/203.95 (define @t908 () (and (=> @t878 @t155) (=> @t875 @t901))) % 203.66/203.95 (define @t909 () (=> @t719 @t896)) % 203.66/203.95 (define @t910 () (=> @t721 @t288)) % 203.66/203.95 (define @t911 () (not (and @t910 @t909))) % 203.66/203.95 (define @t912 () (@list false)) % 203.66/203.95 (define @t913 () (>= @t13 1)) % 203.66/203.95 (define @t914 () (@quantifiers_skolemize (forall @t70 (not (|tptp.'member$a'| @t9 @t35))) 0)) % 203.66/203.95 (define @t915 () (|tptp.'of_nat$'| @t914)) % 203.66/203.95 (define @t916 () (+ -1 @t17)) % 203.66/203.95 (define @t917 () (|tptp.'divide$'| @t916)) % 203.66/203.95 (define @t918 () (>= @t17 1)) % 203.66/203.95 (define @t919 () (not @t918)) % 203.66/203.95 (define @t920 () (and (or (not (|tptp.'member$a'| @t914 @t35)) (and @t919 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t915))) @t14) |tptp.'pa$'|))) (and @t918 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 (|tptp.'nat$'| (|tptp.'fun_app$'| @t917 @t915))) @t14) |tptp.'pa$'|)))) @t913)) % 203.66/203.95 (define @t921 () (not (= @t41 |tptp.'ta$'|))) % 203.66/203.95 (define @t922 () (or @t921 @t920)) % 203.66/203.95 (define @t923 () (not (= @t45 |tptp.'ta$'|))) % 203.66/203.95 (define @t924 () (or @t923 @t44)) % 203.66/203.95 (define @t925 () (and @t924 @t922)) % 203.66/203.95 (define @t926 () (not @t212)) % 203.66/203.95 (define @t927 () (or @t926 @t925)) % 203.66/203.95 (define @t928 () (not @t42)) % 203.66/203.95 (define @t929 () (or @t928 @t920)) % 203.66/203.95 (define @t930 () (not @t46)) % 203.66/203.95 (define @t931 () (or @t930 @t44)) % 203.66/203.95 (define @t932 () (and @t931 @t929)) % 203.66/203.95 (define @t933 () (or @t926 @t932)) % 203.66/203.95 (define @t934 () (@list @t883)) % 203.66/203.95 (define @t935 () (@list false false)) % 203.66/203.95 (define @t936 () (not @t932)) % 203.66/203.95 (define @t937 () (@list @t932)) % 203.66/203.95 (define @t938 () (+ @t13 1)) % 203.66/203.95 (define @t939 () (>= 0 @t13)) % 203.66/203.95 (define @t940 () (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 (|tptp.'nat$'| (|tptp.'fun_app$'| @t917 @t16))) @t14) |tptp.'pa$'|)) % 203.66/203.95 (define @t941 () (and @t918 (not @t940))) % 203.66/203.95 (define @t942 () (and @t919 (not @t31))) % 203.66/203.95 (define @t943 () (not @t36)) % 203.66/203.95 (define @t944 () (or @t943 @t942 @t941)) % 203.66/203.95 (define @t945 () (=> @t918 @t940)) % 203.66/203.95 (define @t946 () (=> @t919 @t31)) % 203.66/203.95 (define @t947 () (not (and @t946 @t945))) % 203.66/203.95 (define @t948 () (+ @t17 @t802)) % 203.66/203.95 (define @t949 () (forall @t38 @t944)) % 203.66/203.95 (define @t950 () (and @t949 @t913)) % 203.66/203.95 (define @t951 () (=> @t42 @t950)) % 203.66/203.95 (define @t952 () (= @t45 @t41)) % 203.66/203.95 (define @t953 () (not @t952)) % 203.66/203.95 (define @t954 () (and @t46 @t953)) % 203.66/203.95 (define @t955 () (@list true)) % 203.66/203.95 (define @t956 () (@list @t951)) % 203.66/203.95 (define @t957 () (not @t949)) % 203.66/203.95 (define @t958 () (@list false true)) % 203.66/203.95 (define @t959 () (@quantifiers_skolemize @t949 0)) % 203.66/203.95 (define @t960 () (|tptp.'of_nat$'| @t959)) % 203.66/203.95 (define @t961 () (or (not (|tptp.'member$a'| @t959 @t35)) (and @t919 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t960))) @t14) |tptp.'pa$'|))) (and @t918 (not (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t22 (|tptp.'nat$'| (|tptp.'fun_app$'| @t917 @t960))) @t14) |tptp.'pa$'|))))) % 203.66/203.95 (define @t962 () (not @t961)) % 203.66/203.95 (define @t963 () (and @t961 @t913)) % 203.66/203.95 (define @t964 () (not @t963)) % 203.66/203.95 (define @t965 () (or @t928 @t963)) % 203.66/203.95 (define @t966 () (not @t965)) % 203.66/203.95 (define @t967 () (or @t921 @t963)) % 203.66/203.95 (define @t968 () (and @t924 @t967)) % 203.66/203.95 (define @t969 () (or @t926 @t968)) % 203.66/203.95 (define @t970 () (and @t931 @t965)) % 203.66/203.95 (define @t971 () (or @t926 @t970)) % 203.66/203.95 (assume @p1 (forall @t4 (= (|tptp.'fun_app$'| (|tptp.'uuc$'| @t2) @t1) @t3))) % 203.66/203.95 (assume @p2 (forall (@list @t5 @t6) (= (|tptp.'fun_app$a'| @t7 @t6) (|tptp.'member$'| @t6 @t5)))) % 203.66/203.95 (assume @p3 (forall (@list @t8 @t9) (= (|tptp.'fun_app$b'| @t10 @t9) (|tptp.'member$a'| @t9 @t8)))) % 203.66/203.95 (assume @p4 (forall (@list @t11 @t1) (= (|tptp.'fun_app$c'| @t12 @t1) (|tptp.'member$b'| @t1 @t11)))) % 203.66/203.95 (assume @p5 @t49) % 203.66/203.95 (assume @p6 (forall (@list @t15 @t9 @t52 @t57 @t54 @t50) (= (= @t59 (|tptp.'triple$'| @t57 @t54 @t50)) (and (= @t16 @t58) (= @t56 @t55) (= @t53 @t51))))) % 203.66/203.95 (assume @p7 (forall @t63 (= (= @t62 @t61) @t60))) % 203.66/203.95 (assume @p8 (forall @t65 (not (= @t62 @t64)))) % 203.66/203.95 (assume @p9 (forall (@list @t66) (=> (and (forall @t70 (=> @t69 false)) (forall @t68 (=> @t67 false))) false))) % 203.66/203.95 (assume @p10 (=> (and @t72 @t71) @t40)) % 203.66/203.95 (assume @p11 (=> (and @t72 (not @t71)) @t40)) % 203.66/203.95 (assume @p12 (=> @t72 @t40)) % 203.66/203.95 (assume @p13 (|tptp.'fun_app$e'| |tptp.'valid_cert$'| |tptp.'c$'|)) % 203.66/203.95 (assume @p14 (forall @t83 (=> @t82 (= @t78 @t73)))) % 203.66/203.95 (assume @p15 (forall @t90 (=> @t89 (= @t87 @t73)))) % 203.66/203.95 (assume @p16 (forall @t38 (=> @t105 (exists @t70 (and @t104 @t102 (forall @t100 (=> (and (=> @t96 (|tptp.'member$a'| @t52 (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| @t99)))) (=> @t97 (|tptp.'member$a'| @t52 (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| @t98))))) (not (and (=> @t96 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t53))) @t14) @t15)) (=> @t97 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 (|tptp.'nat$'| (|tptp.'fun_app$'| @t94 @t53))) @t14) @t15)))))) @t92 @t91))))) % 203.66/203.95 (assume @p17 (forall @t63 (=> @t105 (= (= |tptp.'one$'| @t76) @t106)))) % 203.66/203.95 (assume @p18 (forall @t108 (=> @t107 (= (= 1 @t86) @t106)))) % 203.66/203.95 (assume @p19 (forall @t63 (=> @t105 (= @t109 @t106)))) % 203.66/203.95 (assume @p20 (forall @t108 (=> @t107 (= @t110 @t106)))) % 203.66/203.95 (assume @p21 (forall @t63 (= @t112 (and @t111 @t92)))) % 203.66/203.95 (assume @p22 (forall @t108 (= @t114 (and @t113 @t92)))) % 203.66/203.95 (assume @p23 (forall @t83 (=> @t117 (= @t78 @t115)))) % 203.66/203.95 (assume @p24 (forall @t90 (=> @t118 (= @t87 @t115)))) % 203.66/203.95 (assume @p25 (=> @t119 @t44)) % 203.66/203.95 (assume @p26 (=> @t119 (< 1 @t17))) % 203.66/203.95 (assume @p27 (forall @t38 (= (|tptp.'fun_app$d'| (|tptp.'power$'| |tptp.'one$'|) @t15) |tptp.'one$'|))) % 203.66/203.95 (assume @p28 (forall @t38 (= (|tptp.'fun_app$f'| (|tptp.'power$a'| 1) @t15) 1))) % 203.66/203.95 (assume @p29 (forall @t38 (= (|tptp.'fun_app$d'| @t74 @t14) @t15))) % 203.66/203.95 (assume @p30 (forall @t120 (= (|tptp.'fun_app$f'| @t84 @t14) @t2))) % 203.66/203.95 (assume @p31 (= (|tptp.'prime_factorization$a'| 0) |tptp.'zero$a'|)) % 203.66/203.95 (assume @p32 (= (|tptp.'prime_factorization$'| |tptp.'zero$'|) |tptp.'zero$b'|)) % 203.66/203.95 (assume @p33 (= (|tptp.'prime_factorization$a'| 1) |tptp.'zero$a'|)) % 203.66/203.95 (assume @p34 (= (|tptp.'prime_factorization$'| |tptp.'one$'|) |tptp.'zero$b'|)) % 203.66/203.95 (assume @p35 (forall @t83 (=> @t117 (= @t122 @t121)))) % 203.66/203.95 (assume @p36 (forall @t90 (=> @t118 (= @t123 @t121)))) % 203.66/203.95 (assume @p37 (forall @t63 (= (< 0 @t125) (or @t124 @t106)))) % 203.66/203.95 (assume @p38 (forall @t4 (=> @t128 @t107))) % 203.66/203.95 (assume @p39 (forall @t63 (=> @t131 @t105))) % 203.66/203.95 (assume @p40 (forall @t133 (= (|tptp.'member$b'| @t2 (|tptp.'collect$'| @t132)) (|tptp.'fun_app$c'| @t132 @t2)))) % 203.66/203.95 (assume @p41 (forall @t136 (= (|tptp.'member$a'| @t15 @t135) (|tptp.'fun_app$b'| @t134 @t15)))) % 203.66/203.95 (assume @p42 (forall (@list @t66 @t137) (= (|tptp.'member$'| @t66 @t138) (|tptp.'fun_app$a'| @t137 @t66)))) % 203.66/203.95 (assume @p43 (forall (@list @t11) (= (|tptp.'collect$'| @t12) @t11))) % 203.66/203.95 (assume @p44 (forall (@list @t8) (= (|tptp.'collect$a'| @t10) @t8))) % 203.66/203.95 (assume @p45 (forall (@list @t5) (= (|tptp.'collect$b'| @t7) @t5))) % 203.66/203.95 (assume @p46 (forall (@list @t139 @t137) (=> (forall @t141 (= (|tptp.'fun_app$a'| @t139 @t140) (|tptp.'fun_app$a'| @t137 @t140))) (= (|tptp.'collect$b'| @t139) @t138)))) % 203.66/203.95 (assume @p47 (forall (@list @t142 @t134) (=> (forall @t100 (= @t144 @t143)) (= (|tptp.'collect$a'| @t142) @t135)))) % 203.66/203.95 (assume @p48 (forall @t63 (=> @t145 (not @t112)))) % 203.66/203.95 (assume @p49 (forall @t108 (=> @t146 (not @t114)))) % 203.66/203.95 (assume @p50 (not (|tptp.'fun_app$b'| |tptp.'prime$a'| |tptp.'zero$'|))) % 203.66/203.95 (assume @p51 (not (|tptp.'fun_app$c'| |tptp.'prime$b'| 0))) % 203.66/203.95 (assume @p52 (not (|tptp.'fun_app$b'| |tptp.'prime$a'| |tptp.'one$'|))) % 203.66/203.95 (assume @p53 (not (|tptp.'fun_app$c'| |tptp.'prime$b'| 1))) % 203.66/203.95 (assume @p54 (forall @t83 (=> (and @t105 @t122) @t121))) % 203.66/203.95 (assume @p55 (forall @t90 (=> (and @t107 @t123) @t121))) % 203.66/203.95 (assume @p56 (forall @t63 (=> @t81 (|tptp.'fun_app$b'| @t80 @t76)))) % 203.66/203.95 (assume @p57 (forall @t108 (=> @t88 (< 0 @t86)))) % 203.66/203.95 (assume @p58 (forall @t38 (= @t147 |tptp.'one$'|))) % 203.66/203.95 (assume @p59 (forall @t120 (= @t148 1))) % 203.66/203.95 (assume @p60 (forall @t65 (=> (and @t105 @t155) (= @t154 (or @t152 (and @t150 @t149)))))) % 203.66/203.95 (assume @p61 (forall @t161 (=> (and @t107 @t160) (= @t159 (or @t152 (and @t156 @t149)))))) % 203.66/203.95 (assume @p62 (forall @t83 (=> (and @t124 (< @t125 @t162)) @t115))) % 203.66/203.95 (assume @p63 (forall @t63 (= (|tptp.'fun_app$b'| |tptp.'prime$a'| @t76) (and @t105 @t163)))) % 203.66/203.95 (assume @p64 (forall @t108 (= (|tptp.'fun_app$c'| |tptp.'prime$b'| @t86) (and @t107 @t163)))) % 203.66/203.95 (assume @p65 (forall @t120 (not (|tptp.'member$b'| 0 @t165)))) % 203.66/203.95 (assume @p66 (forall @t38 (not (|tptp.'member$a'| |tptp.'zero$'| @t167)))) % 203.66/203.95 (assume @p67 (forall @t83 (=> @t168 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t75 @t14) @t9)))) % 203.66/203.95 (assume @p68 (forall @t38 (and (=> @t171 (= @t169 |tptp.'one$'|)) (=> @t172 @t170)))) % 203.66/203.95 (assume @p69 (forall @t38 (and (=> @t171 (= @t173 1)) (=> @t172 @t174)))) % 203.66/203.95 (assume @p70 (forall @t83 (=> (and @t178 (|tptp.'fun_app$b'| @t116 @t52)) (|tptp.'fun_app$b'| (|tptp.'less$'| @t177) @t176)))) % 203.66/203.95 (assume @p71 (forall @t183 (=> (and @t178 (< 1 @t179)) (< @t182 @t181)))) % 203.66/203.95 (assume @p72 (forall @t83 (=> (and @t117 @t78) @t115))) % 203.66/203.95 (assume @p73 (forall @t90 (=> (and @t118 @t87) @t115))) % 203.66/203.95 (assume @p74 (forall @t38 (=> @t124 @t170))) % 203.66/203.95 (assume @p75 (forall @t38 (=> @t124 @t174))) % 203.66/203.95 (assume @p76 (forall @t65 (=> @t186 @t150))) % 203.66/203.95 (assume @p77 (forall @t161 (=> @t187 @t156))) % 203.66/203.95 (assume @p78 (forall @t65 (=> @t186 @t149))) % 203.66/203.95 (assume @p79 (forall @t161 (=> @t187 @t149))) % 203.66/203.95 (assume @p80 (forall @t38 (=> @t189 (exists @t70 @t188)))) % 203.66/203.95 (assume @p81 (forall @t83 (=> (and @t178 @t190 (|tptp.'fun_app$b'| (|tptp.'less$'| @t52) |tptp.'one$'|)) (|tptp.'fun_app$b'| (|tptp.'less$'| @t176) @t177)))) % 203.66/203.95 (assume @p82 (forall @t183 (=> (and @t178 @t191 (< @t179 1)) (< @t181 @t182)))) % 203.66/203.95 (assume @p83 (forall @t63 (=> (and @t117 @t92) (|tptp.'fun_app$b'| @t116 @t76)))) % 203.66/203.95 (assume @p84 (forall @t108 (=> (and @t118 @t92) (< 1 @t86)))) % 203.66/203.95 (assume @p85 (|tptp.'member$'| |tptp.'t$'| (|tptp.'set$'| |tptp.'c$'|))) % 203.66/203.95 (assume @p86 (forall @t63 (=> @t178 @t194))) % 203.66/203.95 (assume @p87 (forall @t38 (= @t96 @t171))) % 203.66/203.95 (assume @p88 (forall @t63 (= (and (=> @t178 @t197) (=> @t196 (< 0 @t195))) @t91))) % 203.66/203.95 (assume @p89 (forall @t38 (=> @t145 (= (|tptp.'fun_app$d'| @t198 @t15) |tptp.'one$'|)))) % 203.66/203.95 (assume @p90 (forall @t120 (=> @t146 (= (|tptp.'fun_app$'| @t199 @t2) 1)))) % 203.66/203.95 (assume @p91 (= (- 1 1) 0)) % 203.66/203.95 (assume @p92 (forall @t4 (= (< 0 @t3) @t200))) % 203.66/203.95 (assume @p93 (forall @t83 (= @t202 (and @t185 (forall @t201 (=> (|tptp.'member$a'| @t57 (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| @t52))) (not (and (=> @t96 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 (|tptp.'nat$'| (|tptp.'fun_app$'| @t29 @t58))) @t14) @t15)) (=> @t97 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 (|tptp.'nat$'| (|tptp.'fun_app$'| @t94 @t58))) @t14) @t15)))))))))) % 203.66/203.95 (assume @p94 (forall @t204 (=> @t124 (= (|tptp.'set_mset$a'| (|tptp.'prime_factorization$a'| @t203)) @t127)))) % 203.66/203.95 (assume @p95 (forall @t63 (=> @t124 (= (|tptp.'set_mset$'| (|tptp.'prime_factorization$'| @t205)) @t130)))) % 203.66/203.95 (assume @p96 (forall @t4 (= (|tptp.'fun_app$c'| @t206 0) @t156))) % 203.66/203.95 (assume @p97 (forall @t63 (= (|tptp.'fun_app$b'| @t207 |tptp.'zero$'|) @t150))) % 203.66/203.95 (assume @p98 (forall @t38 (and (=> @t208 @t210) (=> @t209 (= (- @t16 @t16) 0))))) % 203.66/203.95 (assume @p99 @t212) % 203.66/203.95 (assume @p100 (forall @t38 (= (not @t81) @t111))) % 203.66/203.95 (assume @p101 (forall @t120 (= (- @t2 @t2) 0))) % 203.66/203.95 (assume @p102 (forall @t120 (= (- @t2 0) @t2))) % 203.66/203.95 (assume @p103 (forall @t38 (= (|tptp.'fun_app$d'| (|tptp.'minus$'| |tptp.'zero$'|) @t15) |tptp.'zero$'|))) % 203.66/203.95 (assume @p104 (forall @t214 (= (|tptp.'fun_app$g'| (|tptp.'minus$a'| |tptp.'zero$b'|) @t213) |tptp.'zero$b'|))) % 203.66/203.95 (assume @p105 (forall @t216 (= (|tptp.'fun_app$h'| (|tptp.'minus$b'| |tptp.'zero$a'|) @t215) |tptp.'zero$a'|))) % 203.66/203.95 (assume @p106 (forall @t38 (= (|tptp.'fun_app$d'| @t217 |tptp.'zero$'|) @t15))) % 203.66/203.95 (assume @p107 (forall @t214 (= (|tptp.'fun_app$g'| @t218 |tptp.'zero$b'|) @t213))) % 203.66/203.95 (assume @p108 (forall @t216 (= (|tptp.'fun_app$h'| @t219 |tptp.'zero$a'|) @t215))) % 203.66/203.95 (assume @p109 (forall @t38 (= (|tptp.'fun_app$d'| @t217 @t15) |tptp.'zero$'|))) % 203.66/203.95 (assume @p110 (forall @t214 (= (|tptp.'fun_app$g'| @t218 @t213) |tptp.'zero$b'|))) % 203.66/203.95 (assume @p111 (forall @t216 (= (|tptp.'fun_app$h'| @t219 @t215) |tptp.'zero$a'|))) % 203.66/203.95 (assume @p112 (forall @t38 (= (|tptp.'fun_app$d'| (|tptp.'divide$a'| |tptp.'zero$'|) @t15) |tptp.'zero$'|))) % 203.66/203.95 (assume @p113 (forall @t120 (= (|tptp.'fun_app$'| @t29 @t2) 0))) % 203.66/203.95 (assume @p114 (forall @t38 (= (|tptp.'fun_app$d'| @t198 |tptp.'zero$'|) |tptp.'zero$'|))) % 203.66/203.95 (assume @p115 (forall @t120 (= (|tptp.'fun_app$'| @t199 0) 0))) % 203.66/203.95 (assume @p116 (forall @t38 (= (|tptp.'fun_app$d'| @t198 |tptp.'one$'|) @t15))) % 203.66/203.95 (assume @p117 (forall @t120 (= (|tptp.'fun_app$'| @t199 1) @t2))) % 203.66/203.95 (assume @p118 (forall @t38 (= @t172 @t124))) % 203.66/203.95 (assume @p119 (forall @t38 (= @t220 false))) % 203.66/203.95 (assume @p120 (forall @t38 (and (=> @t124 @t210) (=> @t221 (= (- 0 @t16) 0))))) % 203.66/203.95 (assume @p121 (forall @t38 (= (= |tptp.'zero$'| @t15) @t111))) % 203.66/203.95 (assume @p122 (forall @t214 (= (= |tptp.'zero$b'| @t213) (= @t213 |tptp.'zero$b'|)))) % 203.66/203.95 (assume @p123 (forall @t216 (= (= |tptp.'zero$a'| @t215) (= @t215 |tptp.'zero$a'|)))) % 203.66/203.95 (assume @p124 (forall @t120 (= (= 0 @t2) @t113))) % 203.66/203.95 (assume @p125 (forall @t4 (=> (and (not @t156) (=> @t222 false) (=> @t200 false)) false))) % 203.66/203.95 (assume @p126 (forall @t38 (= (= |tptp.'one$'| @t15) (= @t15 |tptp.'one$'|)))) % 203.66/203.95 (assume @p127 (forall @t120 (= (= 1 @t2) @t223))) % 203.66/203.95 (assume @p128 (forall @t226 (=> @t225 (= @t156 (= @t179 @t224))))) % 203.66/203.95 (assume @p129 (forall @t83 (= (|tptp.'fun_app$d'| (|tptp.'minus$'| @t227) @t52) (|tptp.'fun_app$d'| (|tptp.'minus$'| (|tptp.'fun_app$d'| @t217 @t52)) @t9)))) % 203.66/203.95 (assume @p130 (forall (@list @t213 @t228 @t229) (= (|tptp.'fun_app$g'| (|tptp.'minus$a'| (|tptp.'fun_app$g'| @t218 @t228)) @t229) (|tptp.'fun_app$g'| (|tptp.'minus$a'| (|tptp.'fun_app$g'| @t218 @t229)) @t228)))) % 203.66/203.95 (assume @p131 (forall (@list @t215 @t230 @t231) (= (|tptp.'fun_app$h'| (|tptp.'minus$b'| (|tptp.'fun_app$h'| @t219 @t230)) @t231) (|tptp.'fun_app$h'| (|tptp.'minus$b'| (|tptp.'fun_app$h'| @t219 @t231)) @t230)))) % 203.66/203.95 (assume @p132 (forall @t233 (= (- @t3 @t179) (- @t232 @t1)))) % 203.66/203.95 (assume @p133 (forall @t38 (=> (and @t234 (=> @t172 false)) false))) % 203.66/203.95 (assume @p134 (forall @t63 (= @t235 (or @t178 @t91)))) % 203.66/203.95 (assume @p135 (forall @t38 @t209)) % 203.66/203.95 (assume @p136 (forall @t63 (=> @t178 (not @t236)))) % 203.66/203.95 (assume @p137 (forall @t63 (=> @t178 @t235))) % 203.66/203.95 (assume @p138 (forall @t38 (=> @t208 false))) % 203.66/203.95 (assume @p139 (forall @t240 (=> (forall @t100 (=> (forall @t201 (=> @t239 @t238)) @t144)) @t237))) % 203.66/203.95 (assume @p140 (forall @t240 (=> (forall @t100 (=> @t242 @t241)) @t237))) % 203.66/203.95 (assume @p141 (forall @t63 (=> (and @t235 (=> @t178 false) (=> @t91 false)) false))) % 203.66/203.95 (assume @p142 (forall @t83 (and (=> @t252 (and (=> @t249 @t210) (=> @t250 (and (=> @t246 (= 0 @t248)) (=> @t247 (= 0 @t244)))))) (=> (not @t252) (and (=> @t178 (and (=> @t249 (= @t251 0)) (=> @t250 (and (=> @t246 (= @t251 @t248)) (=> @t247 (= @t251 @t244)))))) (=> @t196 (and (=> @t249 (= @t245 0)) (=> @t250 (and (=> @t246 (= @t245 @t248)) (=> @t247 (= @t245 @t244))))))))))) % 203.66/203.95 (assume @p143 (forall @t233 (=> @t253 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t1 @t2) @t179)))) % 203.66/203.95 (assume @p144 (forall @t83 (=> @t255 @t254))) % 203.66/203.95 (assume @p145 (forall @t4 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t2 @t2) @t1))) % 203.66/203.95 (assume @p146 (forall @t63 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t15 @t15) @t9))) % 203.66/203.95 (assume @p147 (forall @t65 (=> (and @t255 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t9 @t57) @t52)) (|tptp.'fun_app$b'| (|tptp.'cong$'| @t15 @t57) @t52)))) % 203.66/203.95 (assume @p148 (forall @t83 (= @t255 @t254))) % 203.66/203.95 (assume @p149 (forall @t83 (=> (and @t189 @t163) (|tptp.'fun_app$b'| (|tptp.'pratt_triple$'| @t15 @t52) @t9)))) % 203.66/203.95 (assume @p150 (not @t197)) % 203.66/203.95 (assume @p151 (not (= 0 1))) % 203.66/203.95 (assume @p152 (forall @t4 (= @t156 (= @t3 0)))) % 203.66/203.95 (assume @p153 (not (< 1 1))) % 203.66/203.95 (assume @p154 (forall @t226 (=> (and @t222 @t258) (< @t257 @t256)))) % 203.66/203.95 (assume @p155 (forall @t226 (=> @t225 (= @t222 @t258)))) % 203.66/203.95 (assume @p156 (forall @t233 (=> @t222 (< @t259 (- @t179 @t2))))) % 203.66/203.95 (assume @p157 (forall @t233 (=> @t222 (< @t232 @t256)))) % 203.66/203.95 (assume @p158 (forall @t38 @t260)) % 203.66/203.95 (assume @p159 (forall @t38 (=> @t234 @t124))) % 203.66/203.95 (assume @p160 (forall @t38 (= @t221 @t171))) % 203.66/203.95 (assume @p161 (forall @t38 (=> @t220 false))) % 203.66/203.95 (assume @p162 (forall @t63 (=> @t178 @t261))) % 203.66/203.95 (assume @p163 (forall @t240 (=> (and (|tptp.'fun_app$b'| @t142 @t99) (forall @t100 (=> (and @t185 @t242) @t241))) @t237))) % 203.66/203.95 (assume @p164 (forall @t38 (and (=> @t220 @t262) (=> @t260 (= (- @t16 0) @t16))))) % 203.66/203.95 (assume @p165 (forall @t63 (=> (and (=> @t178 @t210) (=> @t196 (= @t195 0)) (=> @t91 @t210) (=> @t264 (= @t263 0))) @t60))) % 203.66/203.95 (assume @p166 (forall @t83 (=> (and @t178 @t246) (and (=> @t73 (and (=> @t267 @t197) (=> @t268 (< 0 @t265)))) (=> (not @t73) (and (=> @t267 (< @t266 0)) (=> @t268 (< @t266 @t265)))))))) % 203.66/203.95 (assume @p167 (forall @t83 (=> @t178 @t249))) % 203.66/203.95 (assume @p168 (forall @t4 (|tptp.'fun_app$c'| @t206 1))) % 203.66/203.95 (assume @p169 (forall @t63 (|tptp.'fun_app$b'| @t207 |tptp.'one$'|))) % 203.66/203.95 (assume @p170 (forall @t271 (=> @t270 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t257 (- @t1 @t269)) @t179)))) % 203.66/203.95 (assume @p171 (forall (@list @t2 @t1 @t179 @t57) (=> @t253 (|tptp.'fun_app$c'| (|tptp.'cong$a'| (|tptp.'fun_app$f'| @t84 @t57) @t158) @t179)))) % 203.66/203.95 (assume @p172 (forall @t65 (=> @t255 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t272 @t153) @t52)))) % 203.66/203.95 (assume @p173 (forall @t83 (=> (and @t255 @t246 @t115) @t60))) % 203.66/203.95 (assume @p174 (< 0 1)) % 203.66/203.95 (assume @p175 (not (< 1 0))) % 203.66/203.95 (assume @p176 (forall @t4 (= @t222 (< @t3 0)))) % 203.66/203.95 (assume @p177 (forall @t233 (= (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t3 0) @t179) @t253))) % 203.66/203.95 (assume @p178 (forall @t63 (=> @t273 (and (=> @t91 @t92) (=> @t264 (< @t263 @t56)))))) % 203.66/203.95 (assume @p179 (forall @t63 (= @t194 (or @t178 @t106)))) % 203.66/203.95 (assume @p180 (forall @t38 (= (|tptp.'fun_app$b'| (|tptp.'cong$'| @t99 @t14) @t15) @t274))) % 203.66/203.95 (assume @p181 (forall @t65 (=> (and @t105 @t155 @t185 @t154) @t150))) % 203.66/203.95 (assume @p182 (forall @t161 (=> (and @t107 @t160 @t185 @t159) @t156))) % 203.66/203.95 (assume @p183 (forall @t63 (=> (and @t189 @t92) (< @t276 @t56)))) % 203.66/203.95 (assume @p184 (forall @t63 (=> @t124 (= (= @t193 @t16) @t163)))) % 203.66/203.95 (assume @p185 (forall @t83 (=> (and @t202 @t189 (=> @t96 @t151) (=> @t97 (= @t53 @t93)) @t104 @t102) @t105))) % 203.66/203.95 (assume @p186 @t306) % 203.66/203.95 (assume @p187 (forall @t63 (=> @t131 @t124))) % 203.66/203.95 (assume @p188 (|tptp.'member$'| |tptp.'ta$'| (|tptp.'set$'| @t307))) % 203.66/203.95 (assume @p189 (forall @t65 (=> (and @t105 @t261 (= (|tptp.'of_nat$'| @t176) @t310)) (exists @t295 (= @t53 @t309))))) % 203.66/203.95 (assume @p190 (forall @t38 (=> @t105 @t189))) % 203.66/203.95 (assume @p191 @t311) % 203.66/203.95 (assume @p192 (forall @t38 (exists @t70 (and @t155 @t178)))) % 203.66/203.95 (assume @p193 (forall (@list @t15 @t312) (= (|tptp.'fun_app$e'| |tptp.'valid_cert$'| (|tptp.'cons$'| @t62 @t312)) (and @t189 (|tptp.'fun_app$e'| |tptp.'valid_cert$'| @t312) (exists @t100 (and (=> @t96 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 @t99) @t14) @t15)) (=> @t97 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 @t98) @t14) @t15)) (=> @t96 (|tptp.'member$'| (|tptp.'triple$'| @t15 @t52 @t99) @t313)) (=> @t97 (|tptp.'member$'| (|tptp.'triple$'| @t15 @t52 @t98) @t313)))))))) % 203.66/203.95 (assume @p194 (forall @t38 (=> @t105 @t124))) % 203.66/203.95 (assume @p195 (forall (@list @t15 @t9 @t52 @t314) (= (|tptp.'fun_app$e'| |tptp.'valid_cert$'| (|tptp.'cons$'| @t59 @t314)) (and @t189 @t185 @t317 (or (= @t53 1) (exists @t316 (and (= @t53 (|tptp.'times$'| @t55 @t51)) (|tptp.'member$'| (|tptp.'prime$'| @t54) @t315) (|tptp.'member$'| (|tptp.'triple$'| @t15 @t9 @t50) @t315) (not (and (=> @t96 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 @t287) @t14) @t15)) (=> @t97 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t95 (|tptp.'nat$'| (|tptp.'fun_app$'| @t94 @t55))) @t14) @t15))))))))))) % 203.66/203.95 (assume @p196 (forall @t371 (=> (and @t370 (forall @t368 (=> (and @t367 @t365) false)) (forall @t346 (=> (and @t345 @t342) false))) false))) % 203.66/203.95 (assume @p197 (forall @t375 (=> (and @t105 (|tptp.'fun_app$b'| @t372 @t57) @t341 @t374 (= @t55 @t373) (not (and (=> @t284 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 @t30) @t14) @t9)) (=> @t285 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t175 (|tptp.'nat$'| (|tptp.'fun_app$'| @t278 @t16))) @t14) @t9))))) (|tptp.'fun_app$b'| @t372 @t54)))) % 203.66/203.95 (assume @p198 (forall @t38 (= (|tptp.'of_nat$'| (|tptp.'size_pratt$'| @t62)) 0))) % 203.66/203.95 (assume @p199 (forall @t83 (= (|tptp.'of_nat$'| (|tptp.'size_pratt$'| @t59)) 0))) % 203.66/203.95 (assume @p200 (forall @t120 (= (* 0 @t2) 0))) % 203.66/203.95 (assume @p201 (forall @t38 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| |tptp.'zero$'|) @t15) |tptp.'zero$'|))) % 203.66/203.95 (assume @p202 (forall @t120 (= (* @t2 0) 0))) % 203.66/203.95 (assume @p203 (forall @t38 (= (|tptp.'fun_app$d'| @t376 |tptp.'zero$'|) |tptp.'zero$'|))) % 203.66/203.95 (assume @p204 (forall @t4 (= @t380 @t378))) % 203.66/203.95 (assume @p205 (forall @t63 (= @t384 @t382))) % 203.66/203.95 (assume @p206 (forall @t233 (= @t387 (or @t113 @t385)))) % 203.66/203.95 (assume @p207 (forall @t83 (= @t390 (or @t111 @t388)))) % 203.66/203.95 (assume @p208 (forall @t233 (= (= @t379 @t392) (or @t377 @t391)))) % 203.66/203.95 (assume @p209 (forall @t83 (= (= @t383 @t395) (or @t381 @t393)))) % 203.66/203.95 (assume @p210 (forall @t120 (= (* @t2 1) @t2))) % 203.66/203.95 (assume @p211 (forall @t38 (= (|tptp.'fun_app$d'| @t376 |tptp.'one$'|) @t15))) % 203.66/203.95 (assume @p212 (forall @t120 (= (* 1 @t2) @t2))) % 203.66/203.95 (assume @p213 (forall @t38 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| |tptp.'one$'|) @t15) @t15))) % 203.66/203.95 (assume @p214 (forall @t63 (= (= @t396 0) (or @t171 @t106)))) % 203.66/203.95 (assume @p215 (forall @t38 (= (* @t16 0) 0))) % 203.66/203.95 (assume @p216 (forall @t83 (= @t398 (or @t121 @t171)))) % 203.66/203.95 (assume @p217 (forall @t83 (= (= @t396 @t399) (or (= @t16 @t53) @t106)))) % 203.66/203.95 (assume @p218 (forall @t63 (= (= 1 @t396) @t400))) % 203.66/203.95 (assume @p219 (forall @t63 (= (= @t396 1) @t400))) % 203.66/203.95 (assume @p220 (forall @t4 (= (= @t2 @t379) @t402))) % 203.66/203.95 (assume @p221 (forall @t4 (= (= @t379 @t2) @t402))) % 203.66/203.95 (assume @p222 (forall @t4 (= (= @t2 @t403) @t402))) % 203.66/203.95 (assume @p223 (forall @t4 (= (= @t379 @t1) (or @t377 @t223)))) % 203.66/203.95 (assume @p224 (forall @t63 (=> @t145 (= (|tptp.'fun_app$d'| @t404 @t15) @t9)))) % 203.66/203.95 (assume @p225 (forall @t4 (=> @t146 (= (|tptp.'fun_app$'| @t405 @t2) @t1)))) % 203.66/203.95 (assume @p226 (forall @t63 (=> @t145 (= (|tptp.'fun_app$d'| @t408 @t15) @t9)))) % 203.66/203.95 (assume @p227 (forall @t4 (=> @t146 (= (|tptp.'fun_app$'| @t409 @t2) @t1)))) % 203.66/203.95 (assume @p228 (forall @t83 @t413)) % 203.66/203.95 (assume @p229 (forall @t233 @t417)) % 203.66/203.95 (assume @p230 (forall @t83 (=> @t145 (= (|tptp.'fun_app$d'| @t408 @t418) @t411)))) % 203.66/203.95 (assume @p231 (forall @t233 (=> @t146 (= (|tptp.'fun_app$'| @t409 @t419) @t415)))) % 203.66/203.95 (assume @p232 (forall @t83 (and (=> @t111 (= @t412 |tptp.'zero$'|)) @t413))) % 203.66/203.95 (assume @p233 (forall @t233 (and (=> @t113 (= @t416 0)) @t417))) % 203.66/203.95 (assume @p234 (forall @t83 (= (< @t396 @t399) (and @t92 @t246)))) % 203.66/203.95 (assume @p235 (forall @t63 (= (< 0 @t396) @t273))) % 203.66/203.95 (assume @p236 (forall @t63 (=> @t124 (= (|tptp.'fun_app$'| (|tptp.'divide$'| @t420) @t16) @t56)))) % 203.66/203.95 (assume @p237 (forall @t63 (=> @t124 (= (|tptp.'fun_app$'| @t421 @t16) @t56)))) % 203.66/203.95 (assume @p238 (forall @t233 (= (|tptp.'times$'| @t379 @t179) @t423))) % 203.66/203.95 (assume @p239 (forall @t83 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| @t383) @t52) @t425))) % 203.66/203.95 (assume @p240 (forall @t4 @t426)) % 203.66/203.95 (assume @p241 (forall @t63 @t427)) % 203.66/203.95 (assume @p242 (forall @t233 (= @t423 (|tptp.'times$'| @t1 @t386)))) % 203.66/203.95 (assume @p243 (forall @t83 (= @t425 (|tptp.'fun_app$d'| @t406 @t389)))) % 203.66/203.95 (assume @p244 (forall @t4 (=> @t430 @t429))) % 203.66/203.95 (assume @p245 (forall @t63 (=> @t433 @t432))) % 203.66/203.95 (assume @p246 (forall @t4 (=> @t380 @t378))) % 203.66/203.95 (assume @p247 (forall @t63 (=> @t384 @t382))) % 203.66/203.95 (assume @p248 (forall @t4 (=> @t429 @t430))) % 203.66/203.95 (assume @p249 (forall @t63 (=> @t432 @t433))) % 203.66/203.95 (assume @p250 (forall @t233 (=> @t146 @t434))) % 203.66/203.95 (assume @p251 (forall @t83 (=> @t145 @t435))) % 203.66/203.95 (assume @p252 (forall @t233 (=> @t146 @t436))) % 203.66/203.95 (assume @p253 (forall @t83 (=> @t145 @t437))) % 203.66/203.95 (assume @p254 (forall @t233 (= (|tptp.'times$'| @t3 @t179) (- @t386 @t422)))) % 203.66/203.95 (assume @p255 (forall @t233 (= (|tptp.'times$'| @t2 @t256) (- @t379 @t386)))) % 203.66/203.95 (assume @p256 (forall @t83 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| @t227) @t52) (|tptp.'fun_app$d'| (|tptp.'minus$'| @t389) @t424)))) % 203.66/203.95 (assume @p257 (forall @t83 (= (|tptp.'fun_app$d'| @t376 (|tptp.'fun_app$d'| (|tptp.'minus$'| @t9) @t52)) (|tptp.'fun_app$d'| (|tptp.'minus$'| @t383) @t389)))) % 203.66/203.95 (assume @p258 (forall @t108 (= (|tptp.'times$'| @t86 @t2) @t438))) % 203.66/203.95 (assume @p259 (forall @t63 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| @t76) @t15) @t439))) % 203.66/203.95 (assume @p260 (forall @t442 (= (|tptp.'fun_app$f'| (|tptp.'power$a'| @t379) @t52) @t441))) % 203.66/203.95 (assume @p261 (forall @t83 (= (|tptp.'fun_app$d'| (|tptp.'power$'| @t383) @t52) @t445))) % 203.66/203.95 (assume @p262 (forall @t442 (=> @t426 (= (|tptp.'times$'| @t85 @t1) @t446)))) % 203.66/203.95 (assume @p263 (forall @t83 (=> @t427 (= (|tptp.'fun_app$d'| @t444 @t9) @t447)))) % 203.66/203.95 (assume @p264 (forall @t38 (= (* 0 @t16) 0))) % 203.66/203.95 (assume @p265 (forall @t83 (= (|tptp.'fun_app$d'| @t74 @t449) (|tptp.'fun_app$d'| (|tptp.'power$'| @t76) @t52)))) % 203.66/203.95 (assume @p266 (forall @t90 (= (|tptp.'fun_app$f'| @t84 @t449) (|tptp.'fun_app$f'| (|tptp.'power$a'| @t86) @t52)))) % 203.66/203.95 (assume @p267 (forall @t83 (and (=> @t178 (and (=> @t452 (= @t454 0)) (=> @t453 (= @t454 @t450)))) (=> @t196 (and (=> @t452 (= @t451 0)) (=> @t453 (= @t451 @t450))))))) % 203.66/203.95 (assume @p268 (forall @t83 (and (=> @t115 (and (=> @t458 (= @t461 0)) (=> @t459 (= @t461 @t455)))) (=> @t460 (and (=> @t458 (= @t457 0)) (=> @t459 (= @t457 @t455))))))) % 203.66/203.95 (assume @p269 (forall @t38 (= (* 1 @t16) @t16))) % 203.66/203.95 (assume @p270 (forall @t38 (= (* @t16 1) @t16))) % 203.66/203.95 (assume @p271 (forall @t271 (=> @t270 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t462 (|tptp.'times$'| @t1 @t269)) @t179)))) % 203.66/203.95 (assume @p272 (forall @t375 (=> (and @t255 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t57 @t54) @t52)) (|tptp.'fun_app$b'| (|tptp.'cong$'| @t463 (|tptp.'fun_app$d'| @t406 @t54)) @t52)))) % 203.66/203.95 (assume @p273 (forall @t226 (=> (|tptp.'fun_app$c'| @t206 @t464) @t253))) % 203.66/203.95 (assume @p274 (forall @t226 (=> @t253 (|tptp.'fun_app$c'| (|tptp.'cong$a'| (|tptp.'times$'| @t224 @t2) (|tptp.'times$'| @t224 @t1)) @t179)))) % 203.66/203.95 (assume @p275 (forall @t65 (=> @t255 (|tptp.'fun_app$b'| (|tptp.'cong$'| (|tptp.'fun_app$d'| @t465 @t15) (|tptp.'fun_app$d'| @t465 @t9)) @t52)))) % 203.66/203.95 (assume @p276 (forall @t226 (=> @t253 (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t462 @t466) @t179)))) % 203.66/203.95 (assume @p277 (forall @t65 (=> @t255 (|tptp.'fun_app$b'| (|tptp.'cong$'| @t463 @t467) @t52)))) % 203.66/203.95 (assume @p278 (forall @t83 (= (|tptp.'fun_app$'| @t192 @t448) (|tptp.'fun_app$'| (|tptp.'divide$'| @t193) @t53)))) % 203.66/203.95 (assume @p279 (forall @t65 (=> (|tptp.'fun_app$b'| @t207 (|tptp.'nat$'| (|tptp.'times$'| @t53 @t58))) @t255))) % 203.66/203.95 (assume @p280 (forall @t4 (=> @t471 @t468))) % 203.66/203.95 (assume @p281 (forall @t120 (not (< (|tptp.'times$'| @t2 @t2) 0)))) % 203.66/203.95 (assume @p282 (forall @t4 (= @t475 (or @t474 @t473)))) % 203.66/203.95 (assume @p283 (forall @t63 (=> (and (|tptp.'fun_app$b'| @t79 |tptp.'zero$'|) @t477) @t476))) % 203.66/203.95 (assume @p284 (forall @t4 (=> @t473 @t475))) % 203.66/203.95 (assume @p285 (forall @t63 (=> @t478 @t476))) % 203.66/203.95 (assume @p286 (forall @t4 (=> @t474 @t475))) % 203.66/203.95 (assume @p287 (forall @t63 (=> (and @t81 @t477) @t479))) % 203.66/203.95 (assume @p288 (forall @t4 (=> @t480 @t468))) % 203.66/203.95 (assume @p289 (forall @t63 (=> @t478 (|tptp.'fun_app$b'| (|tptp.'less$'| @t407) |tptp.'zero$'|)))) % 203.66/203.95 (assume @p290 (forall @t4 (=> @t474 (< @t403 0)))) % 203.66/203.95 (assume @p291 (forall @t4 (= @t468 (or @t480 @t471)))) % 203.66/203.95 (assume @p292 (forall @t63 (=> (and @t479 @t81) @t477))) % 203.66/203.95 (assume @p293 (forall @t4 (=> (and @t468 @t88) @t472))) % 203.66/203.95 (assume @p294 (forall @t63 (=> (and @t479 @t477) @t81))) % 203.66/203.95 (assume @p295 (forall @t4 (=> (and @t468 @t472) @t88))) % 203.66/203.95 (assume @p296 (forall @t233 (=> @t470 (= @t482 @t481)))) % 203.66/203.95 (assume @p297 (forall @t233 (=> @t88 (= @t482 @t483)))) % 203.66/203.95 (assume @p298 (forall @t233 (=> @t484 (< @t392 @t419)))) % 203.66/203.95 (assume @p299 (forall @t83 (=> @t485 (|tptp.'fun_app$b'| (|tptp.'less$'| @t418) @t395)))) % 203.66/203.95 (assume @p300 (forall @t233 (=> @t486 (< @t419 @t392)))) % 203.66/203.95 (assume @p301 (forall @t233 (= @t482 (or (and @t88 @t483) (and @t470 @t481))))) % 203.66/203.95 (assume @p302 (forall @t233 (=> @t484 (< @t422 @t386)))) % 203.66/203.95 (assume @p303 (forall @t83 (=> @t485 (|tptp.'fun_app$b'| (|tptp.'less$'| @t389) @t424)))) % 203.66/203.95 (assume @p304 (forall @t233 (=> @t486 (< @t386 @t422)))) % 203.66/203.95 (assume @p305 (forall @t233 (= (< @t379 @t392) (or (and @t472 (< @t2 @t179)) (and @t469 (< @t179 @t2)))))) % 203.66/203.95 (assume @p306 (forall @t63 (=> (and @t117 (|tptp.'fun_app$b'| @t116 @t9)) (|tptp.'fun_app$b'| @t116 @t383)))) % 203.66/203.95 (assume @p307 (forall @t4 (=> (and @t118 @t487) (< 1 @t379)))) % 203.66/203.95 (assume @p308 (forall @t442 (=> @t488 (= @t441 1)))) % 203.66/203.95 (assume @p309 (forall @t83 (=> (= @t383 |tptp.'one$'|) (= @t445 |tptp.'one$'|)))) % 203.66/203.95 (assume @p310 (forall @t83 (=> @t489 @t452))) % 203.66/203.95 (assume @p311 (forall @t83 (=> @t489 (< @t490 @t399)))) % 203.66/203.95 (assume @p312 (forall @t4 (|tptp.'fun_app$c'| @t491 @t2))) % 203.66/203.95 (assume @p313 (forall @t63 (|tptp.'fun_app$b'| @t492 @t15))) % 203.66/203.95 (assume @p314 (forall @t4 (|tptp.'fun_app$c'| @t491 @t1))) % 203.66/203.95 (assume @p315 (forall @t63 (|tptp.'fun_app$b'| @t492 @t9))) % 203.66/203.95 (assume @p316 (forall @t63 (=> (= @t16 @t396) (or @t163 @t171)))) % 203.66/203.95 (assume @p317 (forall @t83 (=> (< @t16 @t448) (< @t493 @t56)))) % 203.66/203.95 (assume @p318 (forall @t63 (=> (|tptp.'fun_app$b'| |tptp.'prime$a'| @t494) (or @t274 @t163)))) % 203.66/203.95 (assume @p319 (forall @t65 (=> (and @t105 (= @t448 @t310)) (exists @t316 (and (= @t56 @t309) (= @t53 (|tptp.'of_nat$'| (|tptp.'fun_app$d'| @t74 @t50)))))))) % 203.66/203.95 (assume @p320 (forall @t63 (=> @t117 (|tptp.'fun_app$b'| @t116 @t439)))) % 203.66/203.95 (assume @p321 (forall @t108 (=> @t118 (< 1 @t438)))) % 203.66/203.95 (assume @p322 (forall @t63 (=> @t117 (|tptp.'fun_app$b'| @t77 @t439)))) % 203.66/203.95 (assume @p323 (forall @t108 (=> @t118 (< @t86 @t438)))) % 203.66/203.95 (assume @p324 (forall @t83 (=> @t124 (= (< @t276 @t53) (< @t56 @t490))))) % 203.66/203.95 (assume @p325 (forall @t38 (=> (and @t189 @t496) (exists (@list @t9 @t52) (and (= @t56 @t397) @t189 @t178 @t495 @t73))))) % 203.66/203.95 (assume @p326 (forall @t63 (=> @t82 (|tptp.'fun_app$b'| (|tptp.'less$'| @t439) @t76)))) % 203.66/203.95 (assume @p327 (forall @t108 (=> @t89 (< @t438 @t86)))) % 203.66/203.95 (assume @p328 (forall @t108 (and (=> @t106 @t110) (=> @t261 (and (=> @t284 (= @t86 (|tptp.'times$'| @t2 @t148))) (=> @t285 (= @t86 (|tptp.'times$'| @t2 (|tptp.'fun_app$f'| @t84 @t349))))))))) % 203.66/203.95 (assume @p329 (forall @t63 (and (=> @t106 @t109) (=> @t261 (and (=> @t284 (= @t76 (|tptp.'fun_app$d'| @t376 @t147))) (=> @t285 (= @t76 (|tptp.'fun_app$d'| @t376 @t497)))))))) % 203.66/203.95 (assume @p330 (forall @t204 (=> @t124 (and (=> @t96 (= (|tptp.'times$'| (|tptp.'fun_app$f'| @t157 @t99) @t1) @t203)) (=> @t97 (= (|tptp.'times$'| (|tptp.'fun_app$f'| @t157 @t98) @t1) @t203)))))) % 203.66/203.95 (assume @p331 (forall @t63 (=> @t124 (and (=> @t96 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| @t103) @t9) @t205)) (=> @t97 (= (|tptp.'fun_app$d'| (|tptp.'times$a'| @t101) @t9) @t205)))))) % 203.66/203.95 (assume @p332 (forall @t83 (and (=> @t171 (= @t498 0)) (=> @t172 @t499)))) % 203.66/203.95 (assume @p333 (forall @t83 (= @t458 (and @t124 @t115)))) % 203.66/203.95 (assume @p334 @t507) % 203.66/203.95 (assume @p335 (forall @t527 (=> (and @t526 (=> (and @t504 @t515) false) (forall @t525 (=> (and @t524 @t522) false)) (forall @t519 (=> (and @t518 @t516) false))) false))) % 203.66/203.95 (assume @p336 (forall @t83 (=> @t124 @t499))) % 203.66/203.95 (assume @p337 (forall @t371 (=> (and @t505 (forall @t530 (=> @t529 false))) false))) % 203.66/203.95 (assume @p338 (= (|tptp.'fun_app$e'| |tptp.'valid_cert$'| |tptp.'nil$'|) true)) % 203.66/203.95 (assume @p339 (forall @t371 (=> (and @t505 (forall @t368 (=> @t367 false)) (forall @t346 (=> @t345 false))) false))) % 203.66/203.95 (assume @p340 (forall @t83 (= @t398 (or @t171 @t121)))) % 203.66/203.95 (assume @p341 (forall @t83 (=> @t124 (= @t458 @t115)))) % 203.66/203.95 (assume @p342 (forall @t83 (=> @t124 (= @t398 @t121)))) % 203.66/203.95 (assume @p343 (forall @t233 (=> @t88 (= (< @t403 @t419) @t483)))) % 203.66/203.95 (assume @p344 (forall @t527 (=> (and @t526 @t533 (=> (and @t504 @t515 @t532) false) (forall @t525 (=> (and @t524 @t522 (|tptp.'fun_app$e'| @t531 @t523)) false)) (forall @t519 (=> (and @t518 @t516 (|tptp.'fun_app$e'| @t531 @t517)) false))) false))) % 203.66/203.95 (assume @p345 (forall @t371 (=> (and @t369 @t533 (=> (and @t504 @t532) false) (forall @t368 (=> (and @t367 @t535 @t341 @t364 @t363) false)) (forall @t346 (=> (and @t345 @t534 @t341 @t184 @t340 @t339) false))) false))) % 203.66/203.95 (assume @p346 (forall @t371 (=> (and @t370 @t533 (forall @t368 (=> (and @t367 @t535 @t365) false)) (forall @t346 (=> (and @t345 @t534 @t342) false))) false))) % 203.66/203.95 (assume @p347 (forall (@list @t66 @t312 @t140 @t314) (= (= @t537 @t536) (and (= @t66 @t140) (= @t312 @t314))))) % 203.66/203.95 (assume @p348 (forall @t133 (=> (and @t146 (exists @t542 (and (|tptp.'member$b'| @t179 @t165) @t541)) (forall (@list @t179 @t57 @t269) (=> (and @t541 @t540 @t539 (not (|tptp.'fun_app$c'| @t538 @t269)) @t184 (= @t2 (|tptp.'times$'| (|tptp.'fun_app$f'| @t180 @t57) @t269))) false))) false))) % 203.66/203.95 (assume @p349 (forall @t136 (=> (and @t145 (exists @t100 (and (|tptp.'member$a'| @t52 @t167) @t143)) (forall @t546 (=> (and @t143 @t545 @t544 (not (|tptp.'fun_app$b'| @t543 @t54)) @t184 (= @t15 (|tptp.'fun_app$d'| (|tptp.'times$a'| (|tptp.'fun_app$d'| @t175 @t57)) @t54))) false))) false))) % 203.66/203.95 (assume @p350 (forall @t38 (= (|tptp.'fun_app$b'| @t547 @t14) @t274))) % 203.66/203.95 (assume @p351 (forall @t38 (|tptp.'fun_app$b'| @t547 |tptp.'zero$'|))) % 203.66/203.95 (assume @p352 (forall @t120 (|tptp.'fun_app$c'| @t548 0))) % 203.66/203.95 (assume @p353 (forall @t38 (= @t550 @t111))) % 203.66/203.95 (assume @p354 (forall @t120 (= @t552 @t113))) % 203.66/203.95 (assume @p355 (forall @t83 (=> @t561 (= (|tptp.'fun_app$b'| @t558 @t556) @t554)))) % 203.66/203.95 (assume @p356 (forall @t233 (=> @t570 (= (|tptp.'fun_app$c'| @t567 @t565) @t563)))) % 203.66/203.95 (assume @p357 (forall @t83 (= @t572 (or @t171 @t554)))) % 203.66/203.95 (assume @p358 (forall @t233 (= @t574 (or @t113 @t563)))) % 203.66/203.95 (assume @p359 (forall @t233 (= (|tptp.'fun_app$c'| @t573 @t392) (or @t377 @t568)))) % 203.66/203.95 (assume @p360 (forall @t233 (=> @t146 (= @t574 @t563)))) % 203.66/203.95 (assume @p361 (forall @t83 (=> @t145 (= (|tptp.'fun_app$b'| @t575 @t389) @t554)))) % 203.66/203.95 (assume @p362 (forall @t233 (=> @t146 (= (|tptp.'fun_app$c'| @t576 @t419) @t563)))) % 203.66/203.95 (assume @p363 (forall @t83 (=> @t145 (= (|tptp.'fun_app$b'| @t577 @t418) @t554)))) % 203.66/203.95 (assume @p364 (forall @t4 (=> @t581 @t578))) % 203.66/203.95 (assume @p365 (forall @t63 (=> @t585 @t582))) % 203.66/203.95 (assume @p366 (forall @t63 (=> @t560 @t587))) % 203.66/203.95 (assume @p367 (forall @t4 (=> @t569 @t588))) % 203.66/203.95 (assume @p368 (forall @t63 (=> @t560 (= (|tptp.'fun_app$d'| @t376 @t557) @t9)))) % 203.66/203.95 (assume @p369 (forall @t4 (=> @t569 (= (|tptp.'times$'| @t2 @t566) @t1)))) % 203.66/203.95 (assume @p370 (forall @t38 (=> @t584 (= (|tptp.'fun_app$d'| @t589 @t590) @t15)))) % 203.66/203.95 (assume @p371 (forall @t120 (=> @t580 (= (|tptp.'fun_app$'| @t591 @t592) @t2)))) % 203.66/203.95 (assume @p372 (forall @t38 (=> @t584 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t590) |tptp.'one$'|)))) % 203.66/203.95 (assume @p373 (forall @t120 (=> @t580 (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t592) 1)))) % 203.66/203.95 (assume @p374 (forall @t63 (=> @t585 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t593) |tptp.'one$'|)))) % 203.66/203.95 (assume @p375 (forall @t4 (=> @t581 (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t594) 1)))) % 203.66/203.95 (assume @p376 (forall @t233 (=> @t570 (= (|tptp.'fun_app$'| (|tptp.'divide$'| @t256) @t2) (- @t566 @t565))))) % 203.66/203.95 (assume @p377 (forall @t63 (=> @t584 @t587))) % 203.66/203.95 (assume @p378 (forall @t4 (=> @t580 @t588))) % 203.66/203.95 (assume @p379 (forall @t63 (=> @t584 (= (|tptp.'fun_app$d'| @t406 @t590) @t557)))) % 203.66/203.95 (assume @p380 (forall @t4 (=> @t580 (= (|tptp.'times$'| @t1 @t592) @t566)))) % 203.66/203.95 (assume @p381 (forall @t83 (=> @t595 @t559))) % 203.66/203.95 (assume @p382 (forall @t233 (=> @t596 @t568))) % 203.66/203.95 (assume @p383 (forall @t38 (|tptp.'fun_app$b'| @t547 @t15))) % 203.66/203.95 (assume @p384 (forall @t120 (|tptp.'fun_app$c'| @t548 @t2))) % 203.66/203.95 (assume @p385 (forall @t65 (=> (and @t255 (|tptp.'fun_app$b'| @t597 @t52)) (|tptp.'fun_app$b'| @t207 @t57)))) % 203.66/203.95 (assume @p386 (forall @t226 (=> (and @t253 (|tptp.'fun_app$c'| @t598 @t179)) (|tptp.'fun_app$c'| @t206 @t224)))) % 203.66/203.95 (assume @p387 (forall @t233 (=> @t253 (= @t539 (|tptp.'fun_app$c'| @t538 @t1))))) % 203.66/203.95 (assume @p388 (forall @t83 (=> @t255 (= @t544 @t599)))) % 203.66/203.95 (assume @p389 (forall @t63 (=> (and @t105 @t155 @t560) @t150))) % 203.66/203.95 (assume @p390 (forall @t4 (=> (and @t107 @t160 @t569) @t156))) % 203.66/203.95 (assume @p391 (forall @t83 (=> @t561 (and (=> @t115 @t600) (=> @t460 (|tptp.'fun_app$b'| @t547 (|tptp.'nat$'| @t456))))))) % 203.66/203.95 (assume @p392 (forall @t83 (=> @t560 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t75) @t443)))) % 203.66/203.95 (assume @p393 (forall @t442 (=> @t569 (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t85) @t440)))) % 203.66/203.95 (assume @p394 (forall @t83 (=> @t561 @t601))) % 203.66/203.95 (assume @p395 (forall @t233 (=> @t570 @t602))) % 203.66/203.95 (assume @p396 (forall @t83 (=> (and (= @t593 @t604) @t603 @t554) @t393))) % 203.66/203.95 (assume @p397 (forall @t233 (=> (and (= @t594 @t606) @t605 @t563) @t391))) % 203.66/203.95 (assume @p398 (forall @t83 (=> @t595 (= (|tptp.'fun_app$d'| @t607 @t557) @t604)))) % 203.66/203.95 (assume @p399 (forall @t233 (=> @t596 (= (|tptp.'fun_app$'| @t608 @t566) @t606)))) % 203.66/203.95 (assume @p400 (forall @t233 (=> @t570 @t609))) % 203.66/203.95 (assume @p401 (forall @t233 (= @t609 (|tptp.'fun_app$c'| @t548 @t259)))) % 203.66/203.95 (assume @p402 (forall @t38 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| |tptp.'one$'|) @t15))) % 203.66/203.95 (assume @p403 (forall @t120 (|tptp.'fun_app$c'| (|tptp.'dvd$'| 1) @t2))) % 203.66/203.95 (assume @p404 (forall @t63 (=> @t584 @t560))) % 203.66/203.95 (assume @p405 (forall @t4 (=> @t580 @t569))) % 203.66/203.95 (assume @p406 (forall @t63 (=> (and @t560 @t583) @t584))) % 203.66/203.95 (assume @p407 (forall @t4 (=> (and @t569 @t579) @t580))) % 203.66/203.95 (assume @p408 (forall @t4 (=> (and @t569 (forall @t542 (=> @t610 false))) false))) % 203.66/203.95 (assume @p409 (forall @t63 (=> (and @t560 (forall @t100 (=> @t611 false))) false))) % 203.66/203.95 (assume @p410 (forall @t233 (=> (= @t2 @t422) @t605))) % 203.66/203.95 (assume @p411 (forall @t83 (=> (= @t15 @t424) @t603))) % 203.66/203.95 (assume @p412 (forall @t4 (= @t569 (exists @t542 @t610)))) % 203.66/203.95 (assume @p413 (forall @t63 (= @t560 (exists @t100 @t611)))) % 203.66/203.95 (assume @p414 (forall @t233 (=> @t569 (|tptp.'fun_app$c'| @t548 @t392)))) % 203.66/203.95 (assume @p415 (forall @t83 (=> @t560 (|tptp.'fun_app$b'| @t547 @t395)))) % 203.66/203.95 (assume @p416 (forall @t233 (=> @t569 @t612))) % 203.66/203.95 (assume @p417 (forall @t83 (=> @t560 @t613))) % 203.66/203.95 (assume @p418 (forall @t233 (=> @t614 @t568))) % 203.66/203.95 (assume @p419 (forall @t83 (=> @t615 @t559))) % 203.66/203.95 (assume @p420 (forall @t4 (|tptp.'fun_app$c'| @t548 @t379))) % 203.66/203.95 (assume @p421 (forall @t63 (|tptp.'fun_app$b'| @t547 @t383))) % 203.66/203.95 (assume @p422 (forall @t226 (=> @t616 (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t386) @t466)))) % 203.66/203.95 (assume @p423 (forall @t65 (=> @t617 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t389) @t467)))) % 203.66/203.95 (assume @p424 (forall @t233 (=> @t614 @t563))) % 203.66/203.95 (assume @p425 (forall @t83 (=> @t615 @t554))) % 203.66/203.95 (assume @p426 (forall @t4 (|tptp.'fun_app$c'| @t548 @t403))) % 203.66/203.95 (assume @p427 (forall @t63 (|tptp.'fun_app$b'| @t547 @t407))) % 203.66/203.95 (assume @p428 (forall @t38 (=> @t550 @t111))) % 203.66/203.95 (assume @p429 (forall @t120 (=> @t552 @t113))) % 203.66/203.95 (assume @p430 (not (|tptp.'fun_app$b'| @t549 |tptp.'one$'|))) % 203.66/203.95 (assume @p431 (not (|tptp.'fun_app$c'| @t551 1))) % 203.66/203.95 (assume @p432 (forall @t63 (=> @t560 @t618))) % 203.66/203.95 (assume @p433 (forall @t4 (=> @t569 @t619))) % 203.66/203.95 (assume @p434 (forall @t4 (= @t578 @t581))) % 203.66/203.95 (assume @p435 (forall @t63 (= @t582 @t585))) % 203.66/203.95 (assume @p436 (forall @t233 (=> @t580 (= @t620 @t563)))) % 203.66/203.95 (assume @p437 (forall @t83 (=> @t584 (= @t621 @t554)))) % 203.66/203.95 (assume @p438 (forall @t233 (=> @t580 (= (|tptp.'fun_app$c'| @t576 @t179) @t563)))) % 203.66/203.95 (assume @p439 (forall @t83 (=> @t584 (= (|tptp.'fun_app$b'| @t577 @t52) @t554)))) % 203.66/203.95 (assume @p440 (forall @t233 (=> @t580 (= (|tptp.'fun_app$c'| @t562 @t386) @t563)))) % 203.66/203.95 (assume @p441 (forall @t83 (=> @t584 (= (|tptp.'fun_app$b'| @t553 @t389) @t554)))) % 203.66/203.95 (assume @p442 (forall @t233 (=> @t580 (= @t614 @t563)))) % 203.66/203.95 (assume @p443 (forall @t83 (=> @t584 (= @t615 @t554)))) % 203.66/203.95 (assume @p444 (forall @t233 (=> @t580 @t434))) % 203.66/203.95 (assume @p445 (forall @t83 (=> @t584 @t435))) % 203.66/203.95 (assume @p446 (forall @t233 (=> @t580 @t436))) % 203.66/203.95 (assume @p447 (forall @t83 (=> @t584 @t437))) % 203.66/203.95 (assume @p448 (forall @t83 (=> @t560 @t623))) % 203.66/203.95 (assume @p449 (forall @t233 (=> @t569 @t625))) % 203.66/203.95 (assume @p450 (forall @t83 (=> @t560 (= (|tptp.'fun_app$d'| @t394 @t557) (|tptp.'fun_app$d'| (|tptp.'divide$a'| @t395) @t15))))) % 203.66/203.95 (assume @p451 (forall @t233 (=> @t569 (= (|tptp.'times$'| @t179 @t566) (|tptp.'fun_app$'| (|tptp.'divide$'| @t392) @t2))))) % 203.66/203.95 (assume @p452 (forall @t83 (=> @t595 (= (|tptp.'fun_app$d'| @t555 @t557) (|tptp.'fun_app$d'| (|tptp.'times$a'| @t604) @t15))))) % 203.66/203.95 (assume @p453 (forall @t233 (=> @t596 (= (|tptp.'fun_app$'| @t564 @t566) (|tptp.'times$'| @t606 @t2))))) % 203.66/203.95 (assume @p454 (forall @t83 (=> @t615 @t626))) % 203.66/203.95 (assume @p455 (forall @t233 (=> @t614 @t627))) % 203.66/203.95 (assume @p456 (forall @t83 (=> @t615 (|tptp.'fun_app$b'| @t547 @t604)))) % 203.66/203.95 (assume @p457 (forall @t233 (=> @t614 (|tptp.'fun_app$c'| @t548 @t606)))) % 203.66/203.95 (assume @p458 (forall @t65 (=> @t617 (= (|tptp.'fun_app$d'| @t586 (|tptp.'fun_app$d'| @t628 @t52)) (|tptp.'fun_app$d'| (|tptp.'divide$a'| @t467) @t389))))) % 203.66/203.95 (assume @p459 (forall @t226 (=> @t616 (= (|tptp.'times$'| @t566 (|tptp.'fun_app$'| @t629 @t179)) (|tptp.'fun_app$'| (|tptp.'divide$'| @t466) @t386))))) % 203.66/203.95 (assume @p460 (forall @t83 (=> @t584 (= (|tptp.'fun_app$b'| @t553 @t556) @t554)))) % 203.66/203.95 (assume @p461 (forall @t233 (=> @t580 (= (|tptp.'fun_app$c'| @t562 @t565) @t563)))) % 203.66/203.95 (assume @p462 (forall @t83 (=> @t584 (= @t630 @t554)))) % 203.66/203.95 (assume @p463 (forall @t233 (=> @t580 (= @t631 @t563)))) % 203.66/203.95 (assume @p464 (forall @t83 (=> @t584 @t601))) % 203.66/203.95 (assume @p465 (forall @t233 (=> @t580 @t602))) % 203.66/203.95 (assume @p466 (forall @t83 (=> @t560 (= (|tptp.'fun_app$d'| (|tptp.'power$'| @t557) @t52) (|tptp.'fun_app$d'| (|tptp.'divide$a'| @t443) @t75))))) % 203.66/203.95 (assume @p467 (forall @t442 (=> @t569 (= (|tptp.'fun_app$f'| (|tptp.'power$a'| @t566) @t52) (|tptp.'fun_app$'| (|tptp.'divide$'| @t440) @t85))))) % 203.66/203.95 (assume @p468 (forall (@list @t2 @t9 @t179) (=> (and @t107 @t92) (= (|tptp.'fun_app$c'| @t548 @t181) @t568)))) % 203.66/203.95 (assume @p469 (forall @t63 (=> (and @t124 @t178) @t632))) % 203.66/203.95 (assume @p470 (forall @t4 (= (|tptp.'fun_app$c'| (|tptp.'cong$a'| @t2 0) @t1) @t605))) % 203.66/203.95 (assume @p471 (forall @t63 (= (|tptp.'fun_app$b'| (|tptp.'cong$'| @t15 |tptp.'zero$'|) @t9) @t603))) % 203.66/203.95 (assume @p472 (forall @t83 (=> @t105 (= @t613 @t633)))) % 203.66/203.95 (assume @p473 (forall @t233 (=> @t107 (= @t612 @t634)))) % 203.66/203.95 (assume @p474 (forall @t83 (=> (and @t105 @t613) @t633))) % 203.66/203.95 (assume @p475 (forall @t233 (=> (and @t107 @t612) @t634))) % 203.66/203.95 (assume @p476 (forall @t38 (=> @t584 @t496))) % 203.66/203.95 (assume @p477 (forall @t120 (=> @t580 (not @t107)))) % 203.66/203.95 (assume @p478 (forall @t233 (= @t253 (|tptp.'fun_app$c'| @t538 @t3)))) % 203.66/203.95 (assume @p479 (forall @t63 (= (and (=> @t91 @t600) (=> @t264 (|tptp.'fun_app$b'| @t547 (|tptp.'nat$'| @t263)))) (or @t91 @t560)))) % 203.66/203.95 (assume @p480 (forall @t83 (=> (and @t105 (|tptp.'fun_app$b'| @t547 @t443)) @t560))) % 203.66/203.95 (assume @p481 (forall @t442 (=> (and @t107 (|tptp.'fun_app$c'| @t548 @t440)) @t569))) % 203.66/203.95 (assume @p482 (forall @t4 (=> @t569 (= (|tptp.'prime_factorization$a'| @t566) (|tptp.'fun_app$h'| (|tptp.'minus$b'| @t126) @t164))))) % 203.66/203.95 (assume @p483 (forall @t63 (=> @t560 (= (|tptp.'prime_factorization$'| @t557) (|tptp.'fun_app$g'| (|tptp.'minus$a'| @t129) @t166))))) % 203.66/203.95 (assume @p484 (forall @t4 (=> @t128 @t569))) % 203.66/203.95 (assume @p485 (forall @t63 (=> @t131 @t560))) % 203.66/203.95 (assume @p486 (forall @t38 (=> (not @t274) (exists @t70 @t635)))) % 203.66/203.95 (assume @p487 (forall @t83 (=> @t105 (= (|tptp.'fun_app$b'| @t547 @t449) @t633)))) % 203.66/203.95 (assume @p488 (forall @t4 (=> (and @t580 (forall @t542 (=> (and @t146 @t610) false))) false))) % 203.66/203.95 (assume @p489 (forall @t63 (=> (and @t584 (forall @t100 (=> (and @t145 @t611) false))) false))) % 203.66/203.95 (assume @p490 (forall @t83 (=> @t637 @t636))) % 203.66/203.95 (assume @p491 (forall @t233 (=> @t639 @t638))) % 203.66/203.95 (assume @p492 (forall @t83 (=> @t637 (= @t630 @t621)))) % 203.66/203.95 (assume @p493 (forall @t233 (=> @t639 (= @t631 @t620)))) % 203.66/203.95 (assume @p494 (forall @t83 (=> @t637 (= (|tptp.'fun_app$b'| @t543 @t557) (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t418) @t9))))) % 203.66/203.95 (assume @p495 (forall @t233 (=> @t639 (= (|tptp.'fun_app$c'| @t538 @t566) (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t419) @t1))))) % 203.66/203.95 (assume @p496 (forall @t65 (=> (and @t145 @t431 @t559 @t640) (= (= @t556 (|tptp.'fun_app$d'| @t628 @t9)) (= @t395 @t463))))) % 203.66/203.95 (assume @p497 (forall @t226 (=> (and @t146 @t428 @t568 @t641) (= (= @t565 (|tptp.'fun_app$'| @t629 @t1)) (= @t392 @t462))))) % 203.66/203.95 (assume @p498 (forall @t63 (=> @t584 @t618))) % 203.66/203.95 (assume @p499 (forall @t4 (=> @t580 @t619))) % 203.66/203.95 (assume @p500 (forall @t83 (=> @t584 @t636))) % 203.66/203.95 (assume @p501 (forall @t233 (=> @t580 @t638))) % 203.66/203.95 (assume @p502 (forall @t83 (=> @t584 (= (= @t9 @t556) (= @t407 @t52))))) % 203.66/203.95 (assume @p503 (forall @t233 (=> @t580 (= (= @t1 @t565) (= @t403 @t179))))) % 203.66/203.95 (assume @p504 (forall @t83 (=> (and @t584 @t554) (= (|tptp.'fun_app$d'| @t555 @t407) (|tptp.'fun_app$d'| (|tptp.'divide$a'| @t604) @t15))))) % 203.66/203.95 (assume @p505 (forall @t233 (=> (and @t580 @t563) (= (|tptp.'fun_app$'| @t564 @t403) (|tptp.'fun_app$'| (|tptp.'divide$'| @t606) @t2))))) % 203.66/203.95 (assume @p506 (forall @t83 (=> @t584 @t623))) % 203.66/203.95 (assume @p507 (forall @t233 (=> @t580 @t625))) % 203.66/203.95 (assume @p508 (forall @t83 (=> @t584 (= (|tptp.'fun_app$d'| @t406 @t556) @t622)))) % 203.66/203.95 (assume @p509 (forall @t233 (=> @t580 (= (|tptp.'times$'| @t1 @t565) @t624)))) % 203.66/203.95 (assume @p510 (forall @t83 (=> @t585 @t626))) % 203.66/203.95 (assume @p511 (forall @t233 (=> @t581 @t627))) % 203.66/203.95 (assume @p512 (forall @t63 (= (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t76) |tptp.'one$'|) (or @t584 @t106)))) % 203.66/203.95 (assume @p513 (forall @t108 (= (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t86) 1) (or @t580 @t106)))) % 203.66/203.95 (assume @p514 (forall @t38 (=> (and @t145 @t642) (exists @t70 (and @t603 @t155))))) % 203.66/203.95 (assume @p515 (forall @t120 (=> (and @t146 @t644) (exists @t643 (and @t605 @t160))))) % 203.66/203.95 (assume @p516 (forall @t38 (=> (and @t145 @t642 (forall @t70 (=> @t635 false))) false))) % 203.66/203.95 (assume @p517 (forall @t120 (=> (and @t146 @t644 (forall @t643 (=> (and @t160 @t605) false))) false))) % 203.66/203.95 (assume @p518 (forall @t375 (=> (and @t105 @t648 @t647 @t646) @t645))) % 203.66/203.95 (assume @p519 (forall @t652 (=> (and @t107 @t651 @t650 @t649) @t645))) % 203.66/203.95 (assume @p520 (forall @t375 (=> (and @t105 @t648 @t647 @t646 (=> (and (= @t9 @t57) @t645) false)) false))) % 203.66/203.95 (assume @p521 (forall @t652 (=> (and @t107 @t651 @t650 @t649 (=> (and (= @t1 @t224) @t645) false)) false))) % 203.66/203.95 (assume @p522 (forall @t83 (=> @t124 (= @t572 @t554)))) % 203.66/203.95 (assume @p523 (forall @t83 (=> (and @t572 @t124) @t554))) % 203.66/203.95 (assume @p524 (forall @t120 (=> @t580 @t653))) % 203.66/203.95 (assume @p525 (forall @t38 (=> @t584 @t654))) % 203.66/203.95 (assume @p526 (forall @t63 (=> (and @t560 @t178) (< 1 @t276)))) % 203.66/203.95 (assume @p527 (forall @t63 (=> (and @t105 @t91 (not @t163)) @t632))) % 203.66/203.95 (assume @p528 (forall @t38 (= @t105 (and @t189 (forall @t70 (=> @t603 (or @t163 @t236))))))) % 203.66/203.95 (assume @p529 (forall @t63 (=> @t168 (and (=> @t96 (|tptp.'fun_app$b'| @t553 @t99)) (=> @t97 (|tptp.'fun_app$b'| @t553 @t98)))))) % 203.66/203.95 (assume @p530 (forall @t655 (not (= @t537 @t312)))) % 203.66/203.95 (assume @p531 (forall @t371 (=> (and @t505 (=> @t656 false)) false))) % 203.66/203.95 (assume @p532 (forall @t63 (=> @t658 (= (|tptp.'fun_app$d'| @t198 @t407) @t657)))) % 203.66/203.95 (assume @p533 (forall @t4 (=> @t660 (= (|tptp.'fun_app$'| @t199 @t403) @t659)))) % 203.66/203.95 (assume @p534 (forall @t63 (=> @t658 (= (|tptp.'fun_app$d'| @t198 @t383) @t657)))) % 203.66/203.95 (assume @p535 (forall @t4 (=> @t660 (= (|tptp.'fun_app$'| @t199 @t379) @t659)))) % 203.66/203.95 (assume @p536 (forall @t63 (=> (and @t584 (forall @t100 (=> (and @t145 (not (= @t52 |tptp.'zero$'|)) @t661 (= @t590 @t52) (= (|tptp.'fun_app$d'| @t589 @t52) @t15) (= @t389 |tptp.'one$'|) (= @t557 @t424)) false))) false))) % 203.66/203.95 (assume @p537 (forall @t4 (=> (and @t580 (forall @t542 (=> (and @t146 (not (= @t179 0)) @t662 (= @t592 @t179) (= (|tptp.'fun_app$'| @t591 @t179) @t2) (= @t386 1) (= @t566 @t422)) false))) false))) % 203.66/203.95 (assume @p538 (forall @t63 (=> (or @t124 (= @t9 |tptp.'one$'|)) (|tptp.'fun_app$b'| @t553 @t205)))) % 203.66/203.95 (assume @p539 (forall @t204 (=> (or @t124 @t401) (|tptp.'fun_app$c'| @t562 @t203)))) % 203.66/203.95 (assume @p540 (forall @t240 (=> (and (|tptp.'fun_app$b'| @t142 |tptp.'zero$'|) (forall @t100 (=> @t661 @t144)) (forall @t663 (=> (and @t545 @t238) (|tptp.'fun_app$b'| @t142 (|tptp.'fun_app$d'| @t394 @t57))))) @t237))) % 203.66/203.95 (assume @p541 (forall (@list @t664 @t1) (=> (and (|tptp.'fun_app$c'| @t664 0) (forall @t542 (=> @t662 (|tptp.'fun_app$c'| @t664 @t179))) (forall (@list @t179 @t224) (=> (and @t540 (|tptp.'fun_app$c'| @t664 @t224)) (|tptp.'fun_app$c'| @t664 @t464)))) (|tptp.'fun_app$c'| @t664 @t1)))) % 203.66/203.95 (assume @p542 (forall @t375 (=> (and @t105 @t648 @t665 @t647) false))) % 203.66/203.95 (assume @p543 (forall @t652 (=> (and @t107 @t651 @t665 @t650) false))) % 203.66/203.95 (assume @p544 (forall @t83 (=> @t666 (= (|tptp.'fun_app$b'| @t547 @t176) @t559)))) % 203.66/203.95 (assume @p545 (forall @t120 (= @t653 (or @t113 @t580)))) % 203.66/203.95 (assume @p546 (forall @t38 (= @t654 (or @t111 @t584)))) % 203.66/203.95 (assume @p547 (forall @t63 (=> @t124 (= (|tptp.'fun_app$b'| (|tptp.'dvd$a'| (|tptp.'nat$'| @t420)) @t15) @t163)))) % 203.66/203.95 (assume @p548 (forall @t63 (=> @t124 (= (|tptp.'fun_app$b'| @t571 @t15) @t163)))) % 203.66/203.95 (assume @p549 (forall @t4 (= @t128 (and @t428 @t569 @t107)))) % 203.66/203.95 (assume @p550 (forall @t63 (= @t131 (and @t431 @t560 @t105)))) % 203.66/203.95 (assume @p551 (forall @t4 (=> (and @t146 @t160 @t605) (|tptp.'member$b'| @t1 @t165)))) % 203.66/203.95 (assume @p552 (forall @t63 (=> (and @t145 @t155 @t603) @t188))) % 203.66/203.95 (assume @p553 (forall @t63 (=> @t666 (exists @t663 (and @t646 (= @t56 (|tptp.'times$'| @t58 @t162))))))) % 203.66/203.95 (assume @p554 (forall (@list @t344 @t667) (=> (and @t656 (forall @t141 (|tptp.'fun_app$e'| @t667 (|tptp.'cons$'| @t140 |tptp.'nil$'|))) (forall @t668 (=> (and (not (= @t314 |tptp.'nil$'|)) (|tptp.'fun_app$e'| @t667 @t314)) (|tptp.'fun_app$e'| @t667 @t536)))) (|tptp.'fun_app$e'| @t667 @t344)))) % 203.66/203.95 (assume @p555 (forall (@list @t669 @t312 @t347) (=> (and (|tptp.'fun_app$e'| @t675 |tptp.'nil$'|) (forall @t676 (|tptp.'fun_app$e'| @t674 |tptp.'nil$'|)) (forall @t676 (|tptp.'fun_app$e'| @t675 @t673)) (forall (@list @t672 @t328 @t671 @t670) (=> (|tptp.'fun_app$e'| (|tptp.'fun_app$i'| @t669 @t328) @t670) (|tptp.'fun_app$e'| @t674 (|tptp.'cons$'| @t671 @t670))))) (|tptp.'fun_app$e'| (|tptp.'fun_app$i'| @t669 @t312) @t347)))) % 203.66/203.95 (assume @p556 (forall @t371 (= @t656 (exists @t530 @t529)))) % 203.66/203.95 (assume @p557 (forall @t371 (=> (and @t505 (forall (@list @t6) (=> (= @t344 (|tptp.'cons$'| @t6 |tptp.'nil$'|)) false)) (forall (@list @t6 @t140 @t314) (=> (= @t344 (|tptp.'cons$'| @t6 @t536)) false))) false))) % 203.66/203.95 (assume @p558 (forall (@list @t678) (=> (and (=> (= @t678 |tptp.'nil$a'|) false) (forall (@list @t679) (=> (= @t678 (|tptp.'cons$a'| |tptp.'nil$'| @t679)) false)) (forall (@list @t6 @t347 @t677) (=> (= @t678 (|tptp.'cons$a'| @t528 @t677)) false))) false))) % 203.66/203.95 (assume @p559 @t682) % 203.66/203.95 (assume @p560 (forall @t655 (not (= |tptp.'nil$'| @t537)))) % 203.66/203.95 (assume @p561 (forall (@list @t15 @t9 @t683) (=> (|tptp.'member$a'| @t15 (|tptp.'set$a'| (|tptp.'cons$b'| @t9 @t683))) (or @t150 (|tptp.'member$a'| @t15 (|tptp.'set$a'| @t683)))))) % 203.66/203.95 (assume @p562 (forall (@list @t66 @t6 @t347) (=> (|tptp.'member$'| @t66 (|tptp.'set$'| @t528)) (or (= @t66 @t6) (|tptp.'member$'| @t66 @t348))))) % 203.66/203.95 (assume @p563 (forall @t687 (=> (and @t686 (forall (@list @t683) (=> (= @t685 (|tptp.'cons$b'| @t15 @t683)) false)) (forall (@list @t52 @t684) (=> (and (= @t685 (|tptp.'cons$b'| @t52 @t684)) (|tptp.'member$a'| @t15 (|tptp.'set$a'| @t684))) false))) false))) % 203.66/203.95 (assume @p564 (forall @t655 (=> (and @t688 (forall (@list @t347) (=> (= @t312 (|tptp.'cons$'| @t66 @t347)) false)) (forall @t668 (=> (and (= @t312 @t536) (|tptp.'member$'| @t66 @t315)) false))) false))) % 203.66/203.95 (assume @p565 (forall @t687 (|tptp.'member$a'| @t15 (|tptp.'set$a'| (|tptp.'cons$b'| @t15 @t685))))) % 203.66/203.95 (assume @p566 (forall @t655 (|tptp.'member$'| @t66 (|tptp.'set$'| @t537)))) % 203.66/203.95 (assume @p567 (forall (@list @t15 @t685 @t52) (=> @t686 (|tptp.'member$a'| @t15 (|tptp.'set$a'| (|tptp.'cons$b'| @t52 @t685)))))) % 203.66/203.95 (assume @p568 (forall (@list @t66 @t312 @t140) (=> @t688 (|tptp.'member$'| @t66 (|tptp.'set$'| (|tptp.'cons$'| @t140 @t312)))))) % 203.66/203.95 (assume @p569 (forall @t38 (=> (and @t145 @t642 (forall @t68 (=> (and @t155 @t603 (not @t640) @t185 (= @t15 (|tptp.'fun_app$d'| (|tptp.'times$a'| @t443) @t57))) false))) false))) % 203.66/203.95 (assume @p570 (forall @t120 (=> (and @t146 @t644 (forall (@list @t1 @t52 @t224) (=> (and @t160 @t605 (not @t641) @t185 (= @t2 (|tptp.'times$'| @t440 @t224))) false))) false))) % 203.66/203.95 (assume @p571 (forall @t83 (=> @t124 (= (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t205) @t177) @t554)))) % 203.66/203.95 (assume @p572 (forall (@list @t15 @t1 @t179) (=> @t124 (= (|tptp.'fun_app$c'| (|tptp.'dvd$'| @t203) @t182) @t563)))) % 203.66/203.95 (assume @p573 (forall @t63 (=> (and @t105 @t647) (and @t104 @t102)))) % 203.66/203.95 (assume @p574 (forall @t83 (=> (and @t124 @t603 @t544 (= @t193 @t493)) @t121))) % 203.66/203.95 (assume @p575 (forall @t63 (=> (and @t560 @t603) @t60))) % 203.66/203.95 (assume @p576 (forall @t4 (=> (and @t107 @t200 @t487) (not @t605)))) % 203.66/203.95 (assume @p577 (forall @t38 (=> @t689 @t171))) % 203.66/203.95 (assume @p578 (forall @t38 (= @t172 (and @t600 @t172)))) % 203.66/203.95 (assume @p579 (forall @t38 (= @t689 @t171))) % 203.66/203.95 (assume @p580 (forall @t38 (not (and @t689 (not @t262))))) % 203.66/203.95 (assume @p581 (forall @t38 @t600)) % 203.66/203.95 (assume @p582 (forall @t83 (=> (and @t560 @t559 (= @t276 (|tptp.'fun_app$'| (|tptp.'divide$'| @t53) @t16))) @t121))) % 203.66/203.95 (assume @p583 (forall @t233 (=> @t612 (exists @t691 @t690)))) % 203.66/203.95 (assume @p584 (forall @t83 (=> @t613 (exists @t693 @t692)))) % 203.66/203.95 (assume @p585 (forall @t233 (=> (and @t612 (forall @t691 (=> @t690 false))) false))) % 203.66/203.95 (assume @p586 (forall @t83 (=> (and @t613 (forall @t693 (=> @t692 false))) false))) % 203.66/203.95 (assume @p587 (forall @t63 (=> (and @t124 @t603) @t92))) % 203.66/203.95 (assume @p588 (forall @t63 (exists @t546 (and @t544 @t599 (or (and (=> @t699 @t697) (=> (not @t699) (= (- @t373 @t698) @t53))) (and (=> @t696 @t697) (=> (not @t696) (= (- @t695 @t694) @t53)))))))) % 203.66/203.95 (assume @p589 (forall @t38 (and (=> @t171 (= @t700 @t701)) (=> @t172 (= @t700 |tptp.'nil$a'|))))) % 203.66/203.95 (assume @p590 (forall @t371 (= (|tptp.'fun_app$j'| (|tptp.'n_lists$'| @t99) @t344) @t701))) % 203.66/203.95 (assume @p591 (forall @t4 (=> @t88 (= @t488 (and @t223 @t401))))) % 203.66/203.95 (assume @p592 (forall @t63 (=> @t666 (and (=> @t284 (and (=> @t96 (= @t703 (|tptp.'times$'| @t704 0))) (=> @t97 (= @t703 (|tptp.'times$'| @t704 @t93))))) (=> @t285 (and (=> @t96 (= @t703 (|tptp.'times$'| @t702 0))) (=> @t97 (= @t703 (|tptp.'times$'| @t702 @t93))))))))) % 203.66/203.95 (assume @p593 (forall @t38 (= @t707 @t171))) % 203.66/203.95 (assume @p594 (= (|tptp.'of_nat$'| (|tptp.'totient$'| @t99)) 0)) % 203.66/203.95 (assume @p595 (forall @t38 (= (< 0 @t706) @t124))) % 203.66/203.95 (assume @p596 (forall @t38 (=> @t189 (< @t706 @t16)))) % 203.66/203.95 (assume @p597 (forall @t38 (=> @t105 (and @t709 @t708)))) % 203.66/203.95 (assume @p598 (forall @t63 (=> @t560 (|tptp.'fun_app$b'| (|tptp.'dvd$a'| @t705) @t710)))) % 203.66/203.95 (assume @p599 (forall @t38 (=> (and @t709 @t708 @t124) @t105))) % 203.66/203.95 (assume @p600 (forall @t63 (=> @t124 (and (=> @t96 (= @t712 (|tptp.'times$'| (|tptp.'of_nat$'| @t103) @t711))) (=> @t97 (= @t712 (|tptp.'times$'| (|tptp.'of_nat$'| @t101) @t711))))))) % 203.66/203.95 (assume @p601 (forall @t233 (=> (and @t574 @t146) @t563))) % 203.66/203.95 (assume @p602 (forall @t38 (<= 0 @t16))) % 203.66/203.95 (assume @p603 (forall @t38 (= (|tptp.'nat$'| @t16) @t15))) % 203.66/203.95 (assume @p604 (forall @t120 (and (=> @t714 (= @t713 @t2)) (=> (not @t714) (= @t713 0))))) % 203.66/203.95 (assume @p605 (forall (@list @t715) (or (= @t715 tptp.tltrue) (= @t715 tptp.tlfalse)))) % 203.66/203.95 (assume @p606 (not (= tptp.tltrue tptp.tlfalse))) % 203.66/203.95 (assume @p607 true) % 203.66/203.95 (step @p608 :rule bool-double-not-elim :args (@t734)) % 203.66/203.95 (step @p609 :rule refl :args (@t745)) % 203.66/203.95 (step @p610 :rule nary_cong :premises (@p609 @p608) :args ((or @t745 (not @t744)))) % 203.66/203.95 (step @p611 :rule cnf_or_neg :args (@t745 0)) % 203.66/203.95 (step @p612 :rule eq_resolve :premises (@p611 @p610)) % 203.66/203.95 (step @p613 :rule reordering :premises (@p612) :args ((or @t734 @t745))) % 203.66/203.95 (step @p614 :rule bool-double-not-elim :args (@t742)) % 203.66/203.95 (step @p615 :rule nary_cong :premises (@p609 @p614) :args ((or @t745 (not @t743)))) % 203.66/203.95 (step @p616 :rule cnf_or_neg :args (@t745 2)) % 203.66/203.95 (step @p617 :rule eq_resolve :premises (@p616 @p615)) % 203.66/203.95 (step @p618 :rule reordering :premises (@p617) :args ((or @t742 @t745))) % 203.66/203.95 (step @p619 :rule instantiate :premises (@p347) :args ((@list |tptp.'y$'| |tptp.'ys$'| @t733 @t731))) % 203.66/203.95 (step @p620 :rule cnf_equiv_pos1 :args (@t748)) % 203.66/203.95 (step @p621 :rule reordering :premises (@p620) :args ((or @t744 @t747 (not @t748)))) % 203.66/203.95 (step @p622 :rule cnf_and_pos :args (@t747 1)) % 203.66/203.95 (step @p623 :rule reordering :premises (@p622) :args ((or @t746 (not @t747)))) % 203.66/203.95 (step @p624 :rule refl :args (@t749)) % 203.66/203.95 (step @p625 :rule refl :args (@t743)) % 203.66/203.95 (step @p626 :rule bool-double-not-elim :args (@t302)) % 203.66/203.95 (step @p627 :rule nary_cong :premises (@p626 @p625 @p624) :args ((or @t751 @t743 @t749))) % 203.66/203.95 (assume-push @p1230 @t750) % 203.66/203.95 (assume-push @p1231 @t746) % 203.66/203.95 (assume-push @p1232 @t742) % 203.66/203.95 (step @p631 :rule evaluate :args (@t752)) % 203.66/203.95 (step @p632 :rule false_intro :premises (@p1230)) % 203.66/203.95 (step @p633 :rule symm :premises (@p1231)) % 203.66/203.95 (step @p634 :rule refl :args (|tptp.'valid_cert$'|)) % 203.66/203.95 (step @p635 :rule cong :premises (@p634 @p633) :args (@t742)) % 203.66/203.95 (step @p636 :rule true_intro :premises (@p1232)) % 203.66/203.95 (step @p637 :rule symm :premises (@p636)) % 203.66/203.95 (step @p638 :rule trans :premises (@p637 @p635 @p632)) % 203.66/203.95 (step @p639 false :rule eq_resolve :premises (@p638 @p631)) % 203.66/203.95 (step-pop @p1233 :rule scope :premises (@p639)) % 203.66/203.95 (step-pop @p1234 :rule scope :premises (@p1233)) % 203.66/203.95 (step-pop @p1235 :rule scope :premises (@p1234)) % 203.66/203.95 (step @p640 :rule process_scope :premises (@p1235) :args (false)) % 203.66/203.95 (assume-push @p1236 @t750) % 203.66/203.95 (assume-push @p1237 @t742) % 203.66/203.95 (assume-push @p1238 @t746) % 203.66/203.95 (step @p647 :rule and_intro :premises (@p1236 @p1238 @p1237)) % 203.66/203.95 (step-pop @p1239 :rule scope :premises (@p647)) % 203.66/203.95 (step-pop @p1240 :rule scope :premises (@p1239)) % 203.66/203.95 (step-pop @p1241 :rule scope :premises (@p1240)) % 203.66/203.95 (step @p648 :rule process_scope :premises (@p1241) :args (@t753)) % 203.66/203.95 (step @p652 :rule implies_elim :premises (@p648)) % 203.66/203.95 (step @p653 :rule resolution :premises (@p652 @p640) :args (true @t753)) % 203.66/203.95 (step @p654 :rule not_and :premises (@p653)) % 203.66/203.95 (step @p655 :rule eq_resolve :premises (@p654 @p627)) % 203.66/203.95 (step @p656 :rule chain_m_resolution :premises (@p655 @p623 @p621 @p619 @p618 @p613) :args ((or @t302 @t745) (@list false false false false false) (@list @t746 @t747 @t748 @t742 @t734))) % 203.66/203.95 (step @p657 :rule refl :args (@t754)) % 203.66/203.95 (step @p658 :rule bool-double-not-elim :args (@t730)) % 203.66/203.95 (step @p659 :rule nary_cong :premises (@p658 @p657) :args ((or (not @t755) @t754))) % 203.66/203.95 (assume-push @p1242 @t755) % 203.66/203.95 (step @p661 :rule skolemize :premises (@p1242)) % 203.66/203.95 (step-pop @p1243 :rule scope :premises (@p661)) % 203.66/203.95 (step @p662 :rule process_scope :premises (@p1243) :args (@t754)) % 203.66/203.95 (step @p664 :rule implies_elim :premises (@p662)) % 203.66/203.95 (step @p665 :rule eq_resolve :premises (@p664 @p659)) % 203.66/203.95 (step @p666 :rule refl :args (@t770)) % 203.66/203.95 (step @p667 :rule refl :args (@t774)) % 203.66/203.95 (step @p668 :rule bool-double-not-elim :args (@t775)) % 203.66/203.95 (step @p669 :rule refl :args (@t370)) % 203.66/203.95 (step @p670 :rule nary_cong :premises (@p669 @p668 @p667 @p666) :args (@t778)) % 203.66/203.95 (step @p671 :rule aci_norm :args ((= (or @t370 (or @t777 (or @t774 @t770))) @t778))) % 203.66/203.95 (step @p672 :rule trans :premises (@p671 @p670)) % 203.66/203.95 (step @p673 :rule bool-and-de-morgan :args (@t773 @t769 true)) % 203.66/203.95 (step @p674 :rule refl :args (@t777)) % 203.66/203.95 (step @p675 :rule nary_cong :premises (@p674 @p673) :args ((or @t777 (not (and @t773 @t769))))) % 203.66/203.95 (step @p676 :rule bool-and-de-morgan :args (@t776 @t773 (and @t769))) % 203.66/203.95 (step @p677 :rule trans :premises (@p676 @p675)) % 203.66/203.95 (step @p678 :rule nary_cong :premises (@p669 @p677) :args ((or @t370 (not (and @t776 @t773 @t769))))) % 203.66/203.95 (step @p679 :rule bool-and-de-morgan :args (@t369 @t776 (and @t773 @t769))) % 203.66/203.95 (step @p680 :rule trans :premises (@p679 @p678)) % 203.66/203.95 (step @p681 :rule trans :premises (@p680 @p672)) % 203.66/203.95 (step @p682 :rule cong :premises (@p681) :args ((forall @t371 (not (and @t369 @t776 @t773 @t769))))) % 203.66/203.95 (step @p683 :rule quant-merge-prenex :args ((= (forall @t346 @t780) @t769))) % 203.66/203.95 (step @p684 :rule alpha_equiv :args (@t781 (@list @t756 @t759) (@list @t50 @t330))) % 203.66/203.95 (step @p685 :rule quant-unused-vars :args ((= @t782 @t761))) % 203.66/203.95 (step @p686 :rule nary_cong :premises (@p685 @p684) :args (@t783)) % 203.66/203.95 (step @p687 :rule quant-miniscope-and :args ((= @t784 @t783))) % 203.66/203.95 (step @p688 :rule trans :premises (@p687 @p686)) % 203.66/203.95 (step @p689 :rule refl :args (@t763)) % 203.66/203.95 (step @p690 :rule refl :args (@t765)) % 203.66/203.95 (step @p691 :rule refl :args (@t728)) % 203.66/203.95 (step @p692 :rule refl :args (@t766)) % 203.66/203.95 (step @p693 :rule nary_cong :premises (@p692 @p691 @p690 @p689 @p688) :args (@t785)) % 203.66/203.95 (step @p694 :rule quant-miniscope-or :args ((= @t780 @t785))) % 203.66/203.95 (step @p695 :rule trans :premises (@p694 @p693)) % 203.66/203.95 (step @p696 :rule symm :premises (@p695)) % 203.66/203.95 (step @p697 :rule cong :premises (@p696) :args ((forall @t346 (or @t766 @t728 @t765 @t763 (and @t761 @t790))))) % 203.66/203.95 (step @p698 :rule trans :premises (@p697 @p683)) % 203.66/203.95 (step @p699 :rule bool-double-not-elim :args (@t790)) % 203.66/203.95 (step @p700 :rule refl :args (@t761)) % 203.66/203.95 (step @p701 :rule nary_cong :premises (@p700 @p699) :args ((and @t761 (not @t791)))) % 203.66/203.95 (step @p702 :rule bool-or-de-morgan :args (@t338 @t791 false)) % 203.66/203.95 (step @p703 :rule trans :premises (@p702 @p701)) % 203.66/203.95 (step @p704 :rule nary_cong :premises (@p692 @p691 @p690 @p689 @p703) :args (@t794)) % 203.66/203.95 (step @p705 :rule aci_norm :args ((= (or @t766 (or @t728 (or @t765 (or @t763 @t793)))) @t794))) % 203.66/203.95 (step @p706 :rule bool-and-de-morgan :args (@t340 @t792 true)) % 203.66/203.95 (step @p707 :rule nary_cong :premises (@p690 @p706) :args ((or @t765 (not (and @t340 @t792))))) % 203.66/203.95 (step @p708 :rule bool-and-de-morgan :args (@t764 @t340 (and @t792))) % 203.66/203.95 (step @p709 :rule trans :premises (@p708 @p707)) % 203.66/203.95 (step @p710 :rule nary_cong :premises (@p691 @p709) :args ((or @t728 (not (and @t764 @t340 @t792))))) % 203.66/203.95 (step @p711 :rule bool-and-de-morgan :args (@t727 @t764 (and @t340 @t792))) % 203.66/203.95 (step @p712 :rule trans :premises (@p711 @p710)) % 203.66/203.95 (step @p713 :rule nary_cong :premises (@p692 @p712) :args ((or @t766 (not (and @t727 @t764 @t340 @t792))))) % 203.66/203.95 (step @p714 :rule bool-and-de-morgan :args (@t345 @t727 (and @t764 @t340 @t792))) % 203.66/203.95 (step @p715 :rule trans :premises (@p714 @p713)) % 203.66/203.95 (step @p716 :rule trans :premises (@p715 @p705)) % 203.66/203.95 (step @p717 :rule trans :premises (@p716 @p704)) % 203.66/203.95 (step @p718 :rule cong :premises (@p717) :args ((forall @t346 (not (and @t345 @t727 @t764 @t340 @t792))))) % 203.66/203.95 (step @p719 :rule trans :premises (@p718 @p698)) % 203.66/203.95 (step @p720 :rule bool-impl-elim :args (@t719 @t786)) % 203.66/203.95 (step @p721 :rule refl :args (@t324)) % 203.66/203.95 (step @p722 :rule bool-double-not-elim :args (@t719)) % 203.66/203.95 (step @p723 :rule nary_cong :premises (@p722 @p721) :args ((or (not @t721) @t324))) % 203.66/203.95 (step @p724 :rule bool-impl-elim :args (@t721 @t324)) % 203.66/203.95 (step @p725 :rule trans :premises (@p724 @p723)) % 203.66/203.95 (step @p726 :rule nary_cong :premises (@p725 @p720) :args (@t795)) % 203.66/203.95 (step @p727 :rule refl :args (@t787)) % 203.66/203.95 (step @p728 :rule refl :args (@t788)) % 203.66/203.95 (step @p729 :rule refl :args (@t789)) % 203.66/203.95 (step @p730 :rule nary_cong :premises (@p729 @p728 @p727 @p726) :args ((or @t789 @t788 @t787 @t795))) % 203.66/203.95 (step @p731 :rule bool-double-not-elim :args (@t795)) % 203.66/203.95 (step @p732 :rule nary_cong :premises (@p729 @p728 @p727 @p731) :args (@t798)) % 203.66/203.95 (step @p733 :rule aci_norm :args ((= (or @t789 (or @t788 (or @t787 @t797))) @t798))) % 203.66/203.95 (step @p734 :rule trans :premises (@p733 @p732)) % 203.66/203.95 (step @p735 :rule bool-and-de-morgan :args (@t331 @t796 true)) % 203.66/203.95 (step @p736 :rule nary_cong :premises (@p728 @p735) :args ((or @t788 (not (and @t331 @t796))))) % 203.66/203.95 (step @p737 :rule bool-and-de-morgan :args (@t332 @t331 (and @t796))) % 203.66/203.95 (step @p738 :rule trans :premises (@p737 @p736)) % 203.66/203.95 (step @p739 :rule nary_cong :premises (@p729 @p738) :args ((or @t789 (not (and @t332 @t331 @t796))))) % 203.66/203.95 (step @p740 :rule bool-and-de-morgan :args (@t334 @t332 (and @t331 @t796))) % 203.66/203.95 (step @p741 :rule trans :premises (@p740 @p739)) % 203.66/203.95 (step @p742 :rule trans :premises (@p741 @p734)) % 203.66/203.95 (step @p743 :rule trans :premises (@p742 @p730)) % 203.66/203.95 (step @p744 :rule cong :premises (@p743) :args (@t800)) % 203.66/203.95 (step @p745 :rule cong :premises (@p744) :args (@t801)) % 203.66/203.95 (step @p746 :rule exists-elim :args ((= (exists @t336 @t799) @t801))) % 203.66/203.95 (step @p747 :rule trans :premises (@p746 @p745)) % 203.66/203.95 (step @p748 :rule refl :args (@t9)) % 203.66/203.95 (step @p749 :rule refl :args (@t14)) % 203.66/203.95 (step @p750 :rule refl :args (@t51)) % 203.66/203.95 (step @p751 :rule arith_poly_norm :args ((= (+ @t56 -1) @t716))) % 203.66/203.95 (step @p752 :rule evaluate :args (@t802)) % 203.66/203.95 (step @p753 :rule refl :args (@t56)) % 203.66/203.95 (step @p754 :rule nary_cong :premises (@p753 @p752) :args (@t803)) % 203.66/203.95 (step @p755 :rule trans :premises (@p754 @p751)) % 203.66/203.95 (step @p756 :rule arith_poly_norm :args ((= @t277 @t803))) % 203.66/203.95 (step @p757 :rule trans :premises (@p756 @p755)) % 203.66/203.95 (step @p758 :rule cong :premises (@p757) :args (@t278)) % 203.66/203.95 (step @p759 :rule cong :premises (@p758 @p750) :args (@t318)) % 203.66/203.95 (step @p760 :rule cong :premises (@p759) :args (@t319)) % 203.66/203.95 (step @p761 :rule refl :args (@t175)) % 203.66/203.95 (step @p762 :rule cong :premises (@p761 @p760) :args (@t320)) % 203.66/203.95 (step @p763 :rule cong :premises (@p762 @p749) :args (@t321)) % 203.66/203.95 (step @p764 :rule cong :premises (@p763 @p748) :args (@t322)) % 203.66/203.95 (step @p765 :rule arith-elim-lt :args (@t56 1)) % 203.66/203.95 (step @p766 :rule cong :premises (@p765) :args (@t285)) % 203.66/203.95 (step @p767 :rule trans :premises (@p766 @p722)) % 203.66/203.95 (step @p768 :rule cong :premises (@p767 @p764) :args (@t323)) % 203.66/203.95 (step @p769 :rule refl :args (@t324)) % 203.66/203.95 (step @p770 :rule cong :premises (@p765 @p769) :args (@t325)) % 203.66/203.95 (step @p771 :rule nary_cong :premises (@p770 @p768) :args (@t326)) % 203.66/203.95 (step @p772 :rule cong :premises (@p771) :args (@t327)) % 203.66/203.95 (step @p773 :rule refl :args (@t331)) % 203.66/203.95 (step @p774 :rule refl :args (@t332)) % 203.66/203.95 (step @p775 :rule refl :args (@t334)) % 203.66/203.95 (step @p776 :rule nary_cong :premises (@p775 @p774 @p773 @p772) :args (@t335)) % 203.66/203.95 (step @p777 :rule cong :premises (@p776) :args (@t337)) % 203.66/203.95 (step @p778 :rule trans :premises (@p777 @p747)) % 203.66/203.95 (step @p779 :rule refl :args (@t338)) % 203.66/203.95 (step @p780 :rule nary_cong :premises (@p779 @p778) :args (@t339)) % 203.66/203.95 (step @p781 :rule refl :args (@t340)) % 203.66/203.95 (step @p782 :rule bool-double-not-elim :args (@t764)) % 203.66/203.95 (step @p783 :rule arith_poly_norm :args ((= (* -1 (- 1 @t804)) (* -1 (- 0 @t58))))) % 203.66/203.95 (step @p784 :rule arith_poly_norm_rel :premises (@p783) :args ((= (>= 1 @t804) @t805))) % 203.66/203.95 (step @p785 :rule arith-geq-tighten :args (@t58 1)) % 203.66/203.95 (step @p786 :rule trans :premises (@p785 @p784)) % 203.66/203.95 (step @p787 :rule symm :premises (@p786)) % 203.66/203.95 (step @p788 :rule cong :premises (@p787) :args ((not @t805))) % 203.66/203.95 (step @p789 :rule trans :premises (@p788 @p782)) % 203.66/203.95 (step @p790 :rule arith-elim-lt :args (0 @t58)) % 203.66/203.95 (step @p791 :rule trans :premises (@p790 @p789)) % 203.66/203.95 (step @p792 :rule bool-double-not-elim :args (@t727)) % 203.66/203.95 (step @p793 :rule arith_poly_norm :args ((= (* 1 (- 2 @t806)) (* 1 (- 1 @t56))))) % 203.66/203.95 (step @p794 :rule arith_poly_norm_rel :premises (@p793) :args ((= (>= 2 @t806) @t807))) % 203.66/203.95 (step @p795 :rule arith-geq-tighten :args (@t56 2)) % 203.66/203.95 (step @p796 :rule trans :premises (@p795 @p794)) % 203.66/203.95 (step @p797 :rule symm :premises (@p796)) % 203.66/203.95 (step @p798 :rule cong :premises (@p797) :args ((not @t807))) % 203.66/203.95 (step @p799 :rule trans :premises (@p798 @p792)) % 203.66/203.95 (step @p800 :rule arith-elim-lt :args (1 @t56)) % 203.66/203.95 (step @p801 :rule trans :premises (@p800 @p799)) % 203.66/203.95 (step @p802 :rule refl :args (@t345)) % 203.66/203.95 (step @p803 :rule nary_cong :premises (@p802 @p801 @p791 @p781 @p780) :args (@t500)) % 203.66/203.95 (step @p804 :rule cong :premises (@p803) :args ((not @t500))) % 203.66/203.95 (step @p805 :rule bool-impl-false1 :args (@t500)) % 203.66/203.95 (step @p806 :rule trans :premises (@p805 @p804)) % 203.66/203.95 (step @p807 :rule cong :premises (@p806) :args (@t501)) % 203.66/203.95 (step @p808 :rule trans :premises (@p807 @p719)) % 203.66/203.95 (step @p809 :rule aci_norm :args ((= @t809 @t772))) % 203.66/203.95 (step @p810 :rule cong :premises (@p809) :args (@t810)) % 203.66/203.95 (step @p811 :rule quant-merge-prenex :args ((= (forall @t368 @t812) @t810))) % 203.66/203.95 (step @p812 :rule alpha_equiv :args (@t813 (@list @t718) (@list @t57))) % 203.66/203.95 (step @p813 :rule refl :args (@t726)) % 203.66/203.95 (step @p814 :rule refl :args (@t771)) % 203.66/203.95 (step @p815 :rule nary_cong :premises (@p814 @p691 @p813 @p812) :args (@t814)) % 203.66/203.95 (step @p816 :rule quant-miniscope-or :args ((= @t812 @t814))) % 203.66/203.95 (step @p817 :rule trans :premises (@p816 @p815)) % 203.66/203.95 (step @p818 :rule symm :premises (@p817)) % 203.66/203.95 (step @p819 :rule cong :premises (@p818) :args ((forall @t368 (or @t771 @t728 @t726 @t817)))) % 203.66/203.95 (step @p820 :rule trans :premises (@p819 @p811)) % 203.66/203.95 (step @p821 :rule trans :premises (@p820 @p810)) % 203.66/203.95 (step @p822 :rule bool-double-not-elim :args (@t817)) % 203.66/203.95 (step @p823 :rule nary_cong :premises (@p814 @p691 @p813 @p822) :args (@t820)) % 203.66/203.95 (step @p824 :rule aci_norm :args ((= (or @t771 (or @t728 (or @t726 @t819))) @t820))) % 203.66/203.95 (step @p825 :rule trans :premises (@p824 @p823)) % 203.66/203.95 (step @p826 :rule bool-and-de-morgan :args (@t364 @t818 true)) % 203.66/203.95 (step @p827 :rule nary_cong :premises (@p691 @p826) :args ((or @t728 (not (and @t364 @t818))))) % 203.66/203.95 (step @p828 :rule bool-and-de-morgan :args (@t727 @t364 (and @t818))) % 203.66/203.95 (step @p829 :rule trans :premises (@p828 @p827)) % 203.66/203.95 (step @p830 :rule nary_cong :premises (@p814 @p829) :args ((or @t771 (not (and @t727 @t364 @t818))))) % 203.66/203.95 (step @p831 :rule bool-and-de-morgan :args (@t367 @t727 (and @t364 @t818))) % 203.66/203.95 (step @p832 :rule trans :premises (@p831 @p830)) % 203.66/203.95 (step @p833 :rule trans :premises (@p832 @p825)) % 203.66/203.95 (step @p834 :rule cong :premises (@p833) :args ((forall @t368 (not (and @t367 @t727 @t364 @t818))))) % 203.66/203.95 (step @p835 :rule trans :premises (@p834 @p821)) % 203.66/203.95 (step @p836 :rule bool-implies-de-morgan :args (@t719 @t815)) % 203.66/203.95 (step @p837 :rule bool-implies-de-morgan :args (@t721 @t353)) % 203.66/203.95 (step @p838 :rule bool-implies-de-morgan :args (@t719 @t816)) % 203.66/203.95 (step @p839 :rule bool-implies-de-morgan :args (@t721 @t360)) % 203.66/203.95 (step @p840 :rule nary_cong :premises (@p839 @p838 @p837 @p836) :args (@t829)) % 203.66/203.95 (step @p841 :rule aci_norm :args ((= (or @t828 (or @t826 (or @t824 @t822))) @t829))) % 203.66/203.95 (step @p842 :rule bool-and-de-morgan :args (@t823 @t821 true)) % 203.66/203.95 (step @p843 :rule refl :args (@t826)) % 203.66/203.95 (step @p844 :rule nary_cong :premises (@p843 @p842) :args ((or @t826 (not (and @t823 @t821))))) % 203.66/203.95 (step @p845 :rule bool-and-de-morgan :args (@t825 @t823 (and @t821))) % 203.66/203.95 (step @p846 :rule trans :premises (@p845 @p844)) % 203.66/203.95 (step @p847 :rule refl :args (@t828)) % 203.66/203.95 (step @p848 :rule nary_cong :premises (@p847 @p846) :args ((or @t828 (not (and @t825 @t823 @t821))))) % 203.66/203.95 (step @p849 :rule bool-and-de-morgan :args (@t827 @t825 (and @t823 @t821))) % 203.66/203.95 (step @p850 :rule trans :premises (@p849 @p848)) % 203.66/203.95 (step @p851 :rule trans :premises (@p850 @p841)) % 203.66/203.95 (step @p852 :rule trans :premises (@p851 @p840)) % 203.66/203.95 (step @p853 :rule cong :premises (@p852) :args (@t831)) % 203.66/203.95 (step @p854 :rule cong :premises (@p853) :args (@t832)) % 203.66/203.95 (step @p855 :rule exists-elim :args ((= (exists @t201 @t830) @t832))) % 203.66/203.95 (step @p856 :rule trans :premises (@p855 @p854)) % 203.66/203.95 (step @p857 :rule refl :args (@t348)) % 203.66/203.95 (step @p858 :rule cong :premises (@p757) :args (@t349)) % 203.66/203.95 (step @p859 :rule refl :args (@t57)) % 203.66/203.95 (step @p860 :rule cong :premises (@p748 @p859 @p858) :args (@t350)) % 203.66/203.95 (step @p861 :rule cong :premises (@p860 @p857) :args (@t351)) % 203.66/203.95 (step @p862 :rule cong :premises (@p767 @p861) :args (@t352)) % 203.66/203.95 (step @p863 :rule refl :args (@t353)) % 203.66/203.95 (step @p864 :rule cong :premises (@p765 @p863) :args (@t354)) % 203.66/203.95 (step @p865 :rule refl :args (@t355)) % 203.66/203.95 (step @p866 :rule cong :premises (@p865 @p858) :args (@t356)) % 203.66/203.95 (step @p867 :rule cong :premises (@p866 @p749) :args (@t357)) % 203.66/203.95 (step @p868 :rule cong :premises (@p867 @p748) :args (@t358)) % 203.66/203.95 (step @p869 :rule cong :premises (@p767 @p868) :args (@t359)) % 203.66/203.95 (step @p870 :rule refl :args (@t360)) % 203.66/203.95 (step @p871 :rule cong :premises (@p765 @p870) :args (@t361)) % 203.66/203.95 (step @p872 :rule nary_cong :premises (@p871 @p869 @p864 @p862) :args (@t362)) % 203.66/203.95 (step @p873 :rule cong :premises (@p872) :args (@t363)) % 203.66/203.95 (step @p874 :rule trans :premises (@p873 @p856)) % 203.66/203.95 (step @p875 :rule refl :args (@t364)) % 203.66/203.95 (step @p876 :rule refl :args (@t367)) % 203.66/203.95 (step @p877 :rule nary_cong :premises (@p876 @p801 @p875 @p874) :args (@t502)) % 203.66/203.95 (step @p878 :rule cong :premises (@p877) :args ((not @t502))) % 203.66/203.95 (step @p879 :rule bool-impl-false1 :args (@t502)) % 203.66/203.95 (step @p880 :rule trans :premises (@p879 @p878)) % 203.66/203.95 (step @p881 :rule cong :premises (@p880) :args (@t503)) % 203.66/203.95 (step @p882 :rule trans :premises (@p881 @p835)) % 203.66/203.95 (step @p883 :rule eq-symm :args (@t344 |tptp.'nil$'|)) % 203.66/203.95 (step @p884 :rule cong :premises (@p883) :args (@t656)) % 203.66/203.95 (step @p885 :rule bool-impl-false1 :args (@t504)) % 203.66/203.95 (step @p886 :rule trans :premises (@p885 @p884)) % 203.66/203.95 (step @p887 :rule refl :args (@t369)) % 203.66/203.95 (step @p888 :rule nary_cong :premises (@p887 @p886 @p882 @p808) :args (@t506)) % 203.66/203.95 (step @p889 :rule cong :premises (@p888) :args ((not @t506))) % 203.66/203.95 (step @p890 :rule bool-impl-false1 :args (@t506)) % 203.66/203.95 (step @p891 :rule trans :premises (@p890 @p889)) % 203.66/203.95 (step @p892 :rule cong :premises (@p891) :args (@t507)) % 203.66/203.95 (step @p893 :rule trans :premises (@p892 @p682)) % 203.66/203.95 (step @p894 :rule eq_resolve :premises (@p334 @p893)) % 203.66/203.95 (step @p895 :rule instantiate :premises (@p894) :args ((@list @t307))) % 203.66/203.95 (step @p896 :rule aci_norm :args ((= (or false @t833) @t833))) % 203.66/203.95 (step @p897 :rule refl :args (@t833)) % 203.66/203.95 (step @p898 :rule evaluate :args ((not true))) % 203.66/203.95 (step @p899 :rule eq-refl :args (@t528)) % 203.66/203.95 (step @p900 :rule cong :premises (@p899) :args (@t834)) % 203.66/203.95 (step @p901 :rule trans :premises (@p900 @p898)) % 203.66/203.95 (step @p902 :rule nary_cong :premises (@p901 @p897) :args (@t835)) % 203.66/203.95 (step @p903 :rule trans :premises (@p902 @p896)) % 203.66/203.95 (step @p904 :rule cong :premises (@p903) :args ((forall @t530 @t835))) % 203.66/203.95 (step @p905 :rule quant-var-elim-eq :args ((= (forall @t371 @t837) @t835))) % 203.66/203.95 (step @p906 :rule aci_norm :args ((= @t838 @t837))) % 203.66/203.95 (step @p907 :rule cong :premises (@p906) :args (@t839)) % 203.66/203.95 (step @p908 :rule trans :premises (@p907 @p905)) % 203.66/203.95 (step @p909 :rule cong :premises (@p908) :args (@t840)) % 203.66/203.95 (step @p910 :rule quant-merge-prenex :args ((= @t840 @t841))) % 203.66/203.95 (step @p911 :rule symm :premises (@p910)) % 203.66/203.95 (step @p912 :rule quant_var_reordering :args ((= (forall @t681 @t838) @t841))) % 203.66/203.95 (step @p913 :rule trans :premises (@p912 @p911 @p909)) % 203.66/203.95 (step @p914 :rule trans :premises (@p913 @p904)) % 203.66/203.95 (step @p915 :rule bool-impl-elim :args (@t529 @t776)) % 203.66/203.95 (step @p916 :rule cong :premises (@p915) :args ((forall @t681 (=> @t529 @t776)))) % 203.66/203.95 (step @p917 :rule trans :premises (@p916 @p914)) % 203.66/203.95 (step @p918 :rule refl :args (@t529)) % 203.66/203.95 (step @p919 :rule cong :premises (@p918 @p884) :args (@t680)) % 203.66/203.95 (step @p920 :rule cong :premises (@p919) :args (@t682)) % 203.66/203.95 (step @p921 :rule trans :premises (@p920 @p917)) % 203.66/203.95 (step @p922 :rule eq_resolve :premises (@p559 @p921)) % 203.66/203.95 (step @p923 :rule instantiate :premises (@p922) :args ((@list |tptp.'y$'| |tptp.'ys$'|))) % 203.66/203.95 (step @p924 :rule cnf_or_pos :args (@t846)) % 203.66/203.95 (step @p925 :rule reordering :premises (@p924) :args ((or @t845 @t844 @t755 @t843 (not @t846)))) % 203.66/203.95 (step @p926 :rule refl :args (@t865)) % 203.66/203.95 (step @p927 :rule bool-double-not-elim :args (@t842)) % 203.66/203.95 (step @p928 :rule nary_cong :premises (@p927 @p926) :args ((or (not @t843) @t865))) % 203.66/203.95 (assume-push @p1244 @t843) % 203.66/203.95 (step @p930 :rule skolemize :premises (@p1244)) % 203.66/203.95 (step-pop @p1245 :rule scope :premises (@p930)) % 203.66/203.95 (step @p931 :rule process_scope :premises (@p1245) :args (@t865)) % 203.66/203.95 (step @p933 :rule implies_elim :premises (@p931)) % 203.66/203.95 (step @p934 :rule eq_resolve :premises (@p933 @p928)) % 203.66/203.95 (step @p935 :rule bool-double-not-elim :args (@t862)) % 203.66/203.95 (step @p936 :rule refl :args (@t864)) % 203.66/203.95 (step @p937 :rule nary_cong :premises (@p936 @p935) :args ((or @t864 (not @t863)))) % 203.66/203.95 (step @p938 :rule cnf_or_neg :args (@t864 0)) % 203.66/203.95 (step @p939 :rule eq_resolve :premises (@p938 @p937)) % 203.66/203.95 (step @p940 :rule reordering :premises (@p939) :args ((or @t862 @t864))) % 203.66/203.95 (step @p941 :rule bool-double-not-elim :args (@t859)) % 203.66/203.95 (step @p942 :rule nary_cong :premises (@p936 @p941) :args ((or @t864 (not @t860)))) % 203.66/203.95 (step @p943 :rule cnf_or_neg :args (@t864 3)) % 203.66/203.95 (step @p944 :rule eq_resolve :premises (@p943 @p942)) % 203.66/203.95 (step @p945 :rule reordering :premises (@p944) :args ((or @t859 @t864))) % 203.66/203.95 (step @p946 :rule instantiate :premises (@p347) :args ((@list |tptp.'y$'| |tptp.'ys$'| @t861 @t854))) % 203.66/203.95 (step @p947 :rule cnf_equiv_pos1 :args (@t868)) % 203.66/203.95 (step @p948 :rule reordering :premises (@p947) :args ((or @t863 @t867 (not @t868)))) % 203.66/203.95 (step @p949 :rule cnf_and_pos :args (@t867 1)) % 203.66/203.95 (step @p950 :rule reordering :premises (@p949) :args ((or @t866 (not @t867)))) % 203.66/203.95 (step @p951 :rule refl :args (@t869)) % 203.66/203.95 (step @p952 :rule refl :args (@t860)) % 203.66/203.95 (step @p953 :rule nary_cong :premises (@p626 @p952 @p951) :args ((or @t751 @t860 @t869))) % 203.66/203.95 (assume-push @p1246 @t750) % 203.66/203.95 (assume-push @p1247 @t866) % 203.66/203.95 (assume-push @p1248 @t859) % 203.66/203.95 (step @p631 :rule evaluate :args (@t752)) % 203.66/203.95 (step @p957 :rule false_intro :premises (@p1246)) % 203.66/203.95 (step @p958 :rule symm :premises (@p1247)) % 203.66/203.95 (step @p634 :rule refl :args (|tptp.'valid_cert$'|)) % 203.66/203.95 (step @p959 :rule cong :premises (@p634 @p958) :args (@t859)) % 203.66/203.95 (step @p960 :rule true_intro :premises (@p1248)) % 203.66/203.95 (step @p961 :rule symm :premises (@p960)) % 203.66/203.95 (step @p962 :rule trans :premises (@p961 @p959 @p957)) % 203.66/203.95 (step @p963 false :rule eq_resolve :premises (@p962 @p631)) % 203.66/203.95 (step-pop @p1249 :rule scope :premises (@p963)) % 203.66/203.95 (step-pop @p1250 :rule scope :premises (@p1249)) % 203.66/203.95 (step-pop @p1251 :rule scope :premises (@p1250)) % 203.66/203.95 (step @p964 :rule process_scope :premises (@p1251) :args (false)) % 203.66/203.95 (assume-push @p1252 @t750) % 203.66/203.95 (assume-push @p1253 @t859) % 203.66/203.95 (assume-push @p1254 @t866) % 203.66/203.95 (step @p971 :rule and_intro :premises (@p1252 @p1254 @p1253)) % 203.66/203.95 (step-pop @p1255 :rule scope :premises (@p971)) % 203.66/203.95 (step-pop @p1256 :rule scope :premises (@p1255)) % 203.66/203.95 (step-pop @p1257 :rule scope :premises (@p1256)) % 203.66/203.95 (step @p972 :rule process_scope :premises (@p1257) :args (@t870)) % 203.66/203.95 (step @p976 :rule implies_elim :premises (@p972)) % 203.66/203.95 (step @p977 :rule resolution :premises (@p976 @p964) :args (true @t870)) % 203.66/203.95 (step @p978 :rule not_and :premises (@p977)) % 203.66/203.95 (step @p979 :rule eq_resolve :premises (@p978 @p953)) % 203.66/203.95 (step @p980 :rule chain_m_resolution :premises (@p979 @p950 @p948 @p946 @p945 @p940 @p934 @p925 @p923 @p895 @p191 @p665 @p656) :args (@t302 (@list false false false false false true true true false false false false) (@list @t866 @t867 @t868 @t859 @t862 @t864 @t842 @t844 @t846 @t311 @t730 @t745))) % 203.66/203.95 (step @p981 :rule quant-merge-prenex :args ((= (forall @t305 @t885) @t883))) % 203.66/203.95 (step @p982 :rule quant-unused-vars :args ((= @t886 @t764))) % 203.66/203.95 (step @p983 :rule alpha_equiv :args (@t887 (@list @t871) (@list @t54))) % 203.66/203.95 (step @p984 :rule nary_cong :premises (@p983 @p982) :args (@t888)) % 203.66/203.95 (step @p985 :rule quant-miniscope-and :args ((= @t889 @t888))) % 203.66/203.95 (step @p986 :rule trans :premises (@p985 @p984)) % 203.66/203.95 (step @p987 :rule refl :args (@t876)) % 203.66/203.95 (step @p988 :rule nary_cong :premises (@p987 @p986) :args (@t890)) % 203.66/203.95 (step @p989 :rule quant-miniscope-or :args ((= @t891 @t890))) % 203.66/203.95 (step @p990 :rule trans :premises (@p989 @p988)) % 203.66/203.95 (step @p991 :rule quant-unused-vars :args ((= @t892 @t879))) % 203.66/203.95 (step @p992 :rule nary_cong :premises (@p991 @p990) :args (@t893)) % 203.66/203.95 (step @p993 :rule quant-miniscope-and :args ((= @t894 @t893))) % 203.66/203.95 (step @p994 :rule trans :premises (@p993 @p992)) % 203.66/203.95 (step @p995 :rule refl :args (@t881)) % 203.66/203.95 (step @p996 :rule nary_cong :premises (@p995 @p994) :args (@t895)) % 203.66/203.95 (step @p997 :rule quant-miniscope-or :args ((= @t885 @t895))) % 203.66/203.95 (step @p998 :rule trans :premises (@p997 @p996)) % 203.66/203.95 (step @p999 :rule symm :premises (@p998)) % 203.66/203.95 (step @p1000 :rule cong :premises (@p999) :args (@t904)) % 203.66/203.95 (step @p1001 :rule trans :premises (@p1000 @p981)) % 203.66/203.95 (step @p1002 :rule refl :args (@t750)) % 203.66/203.95 (step @p1003 :rule nary_cong :premises (@p1002 @p1001) :args (@t905)) % 203.66/203.95 (step @p1004 :rule quant-miniscope-or :args ((= (forall @t305 @t906) @t905))) % 203.66/203.95 (step @p1005 :rule aci_norm :args ((= @t907 @t906))) % 203.66/203.95 (step @p1006 :rule cong :premises (@p1005) :args ((forall @t305 @t907))) % 203.66/203.95 (step @p1007 :rule trans :premises (@p1006 @p1004)) % 203.66/203.95 (step @p1008 :rule trans :premises (@p1007 @p1003)) % 203.66/203.95 (step @p1009 :rule aci_norm :args ((= (or (or @t750 @t881) @t902) @t907))) % 203.66/203.95 (step @p1010 :rule bool-impl-elim :args (@t875 @t901)) % 203.66/203.95 (step @p1011 :rule bool-impl-elim :args (@t878 @t155)) % 203.66/203.95 (step @p1012 :rule nary_cong :premises (@p1011 @p1010) :args (@t908)) % 203.66/203.95 (step @p1013 :rule bool-and-de-morgan :args (@t302 @t301 true)) % 203.66/203.95 (step @p1014 :rule nary_cong :premises (@p1013 @p1012) :args ((or (not @t303) @t908))) % 203.66/203.95 (step @p1015 :rule trans :premises (@p1014 @p1009)) % 203.66/203.95 (step @p1016 :rule bool-impl-elim :args (@t303 @t908)) % 203.66/203.95 (step @p1017 :rule trans :premises (@p1016 @p1015)) % 203.66/203.95 (step @p1018 :rule cong :premises (@p1017) :args ((forall @t305 (=> @t303 @t908)))) % 203.66/203.95 (step @p1019 :rule trans :premises (@p1018 @p1008)) % 203.66/203.95 (step @p1020 :rule aci_norm :args ((= (or @t899 (or @t898 @t897)) @t900))) % 203.66/203.95 (step @p1021 :rule bool-implies-de-morgan :args (@t719 @t896)) % 203.66/203.95 (step @p1022 :rule bool-implies-de-morgan :args (@t721 @t288)) % 203.66/203.95 (step @p1023 :rule nary_cong :premises (@p1022 @p1021) :args ((or (not @t910) (not @t909)))) % 203.66/203.95 (step @p1024 :rule bool-and-de-morgan :args (@t910 @t909 true)) % 203.66/203.95 (step @p1025 :rule trans :premises (@p1024 @p1023)) % 203.66/203.95 (step @p1026 :rule refl :args (@t899)) % 203.66/203.95 (step @p1027 :rule nary_cong :premises (@p1026 @p1025) :args ((or @t899 @t911))) % 203.66/203.95 (step @p1028 :rule trans :premises (@p1027 @p1020)) % 203.66/203.95 (step @p1029 :rule bool-impl-elim :args (@t293 @t911)) % 203.66/203.95 (step @p1030 :rule trans :premises (@p1029 @p1028)) % 203.66/203.95 (step @p1031 :rule cong :premises (@p1030) :args ((forall @t295 (=> @t293 @t911)))) % 203.66/203.95 (step @p1032 :rule refl :args (@t55)) % 203.66/203.95 (step @p1033 :rule cong :premises (@p758 @p1032) :args (@t279)) % 203.66/203.95 (step @p1034 :rule cong :premises (@p1033) :args (@t280)) % 203.66/203.95 (step @p1035 :rule cong :premises (@p761 @p1034) :args (@t281)) % 203.66/203.95 (step @p1036 :rule cong :premises (@p1035 @p749) :args (@t282)) % 203.66/203.95 (step @p1037 :rule cong :premises (@p1036 @p748) :args (@t283)) % 203.66/203.95 (step @p1038 :rule cong :premises (@p767 @p1037) :args (@t286)) % 203.66/203.95 (step @p1039 :rule refl :args (@t288)) % 203.66/203.95 (step @p1040 :rule cong :premises (@p765 @p1039) :args (@t289)) % 203.66/203.95 (step @p1041 :rule nary_cong :premises (@p1040 @p1038) :args (@t290)) % 203.66/203.95 (step @p1042 :rule cong :premises (@p1041) :args (@t291)) % 203.66/203.95 (step @p1043 :rule refl :args (@t293)) % 203.66/203.95 (step @p1044 :rule cong :premises (@p1043 @p1042) :args (@t294)) % 203.66/203.95 (step @p1045 :rule cong :premises (@p1044) :args (@t296)) % 203.66/203.95 (step @p1046 :rule trans :premises (@p1045 @p1031)) % 203.66/203.95 (step @p1047 :rule nary_cong :premises (@p1046 @p791) :args (@t297)) % 203.66/203.95 (step @p1048 :rule eq-symm :args (@t66 @t64)) % 203.66/203.95 (step @p1049 :rule cong :premises (@p1048 @p1047) :args (@t298)) % 203.66/203.95 (step @p1050 :rule refl :args (@t155)) % 203.66/203.95 (step @p1051 :rule eq-symm :args (@t66 @t61)) % 203.66/203.95 (step @p1052 :rule cong :premises (@p1051 @p1050) :args (@t299)) % 203.66/203.95 (step @p1053 :rule nary_cong :premises (@p1052 @p1049) :args (@t300)) % 203.66/203.95 (step @p1054 :rule refl :args (@t303)) % 203.66/203.95 (step @p1055 :rule cong :premises (@p1054 @p1053) :args (@t304)) % 203.66/203.95 (step @p1056 :rule cong :premises (@p1055) :args (@t306)) % 203.66/203.95 (step @p1057 :rule trans :premises (@p1056 @p1019)) % 203.66/203.95 (step @p1058 :rule eq_resolve :premises (@p186 @p1057)) % 203.66/203.95 (step @p1059 :rule chain_m_resolution :premises (@p1058 @p980) :args (@t883 @t912 (@list @t302))) % 203.66/203.95 (step @p1060 :rule refl :args (@t920)) % 203.66/203.95 (step @p1061 :rule eq-symm :args (@t41 |tptp.'ta$'|)) % 203.66/203.95 (step @p1062 :rule cong :premises (@p1061) :args (@t921)) % 203.66/203.95 (step @p1063 :rule nary_cong :premises (@p1062 @p1060) :args (@t922)) % 203.66/203.95 (step @p1064 :rule refl :args (@t44)) % 203.66/203.95 (step @p1065 :rule eq-symm :args (@t45 |tptp.'ta$'|)) % 203.66/203.95 (step @p1066 :rule cong :premises (@p1065) :args (@t923)) % 203.66/203.95 (step @p1067 :rule nary_cong :premises (@p1066 @p1064) :args (@t924)) % 203.66/203.95 (step @p1068 :rule nary_cong :premises (@p1067 @p1063) :args (@t925)) % 203.66/203.95 (step @p1069 :rule refl :args (@t926)) % 203.66/203.95 (step @p1070 :rule nary_cong :premises (@p1069 @p1068) :args (@t927)) % 203.66/203.95 (step @p1071 :rule refl :args (@t883)) % 203.66/203.95 (step @p1072 :rule cong :premises (@p1071 @p1070) :args ((=> @t883 @t927))) % 203.66/203.95 (assume-push @p1258 @t883) % 203.66/203.95 (step @p1074 :rule instantiate :premises (@p1258) :args ((@list |tptp.'ta$'| |tptp.'pa$'| |tptp.'aa$'| |tptp.'xa$'| @t914))) % 203.66/203.95 (step-pop @p1259 :rule scope :premises (@p1074)) % 203.66/203.95 (step @p1075 :rule process_scope :premises (@p1259) :args (@t927)) % 203.66/203.95 (step @p1077 :rule eq_resolve :premises (@p1075 @p1072)) % 203.66/203.95 (step @p1078 :rule implies_elim :premises (@p1077)) % 203.66/203.95 (step @p1079 :rule chain_m_resolution :premises (@p1078 @p1059) :args (@t933 @t912 @t934)) % 203.66/203.95 (step @p1080 :rule cnf_or_pos :args (@t933)) % 203.66/203.95 (step @p1081 :rule reordering :premises (@p1080) :args ((or @t926 @t932 (not @t933)))) % 203.66/203.95 (step @p1082 :rule chain_m_resolution :premises (@p1081 @p99 @p1079) :args (@t932 @t935 (@list @t212 @t933))) % 203.66/203.95 (step @p1083 :rule cnf_and_pos :args (@t932 0)) % 203.66/203.95 (step @p1084 :rule reordering :premises (@p1083) :args ((or @t931 @t936))) % 203.66/203.95 (step @p1085 :rule chain_m_resolution :premises (@p1084 @p1082) :args (@t931 @t912 @t937)) % 203.66/203.95 (step @p1086 :rule cnf_or_pos :args (@t931)) % 203.66/203.95 (step @p1087 :rule reordering :premises (@p1086) :args ((or @t44 @t930 (not @t931)))) % 203.66/203.95 (step @p1088 :rule cnf_implies_neg2 :args (@t47)) % 203.66/203.95 (step @p1089 :rule bool-double-not-elim :args (@t913)) % 203.66/203.95 (step @p1090 :rule arith_poly_norm :args ((= (* -1 (- 1 @t938)) (* -1 (- 0 @t13))))) % 203.66/203.95 (step @p1091 :rule arith_poly_norm_rel :premises (@p1090) :args ((= (>= 1 @t938) @t939))) % 203.66/203.95 (step @p1092 :rule arith-geq-tighten :args (@t13 1)) % 203.66/203.95 (step @p1093 :rule trans :premises (@p1092 @p1091)) % 203.66/203.95 (step @p1094 :rule symm :premises (@p1093)) % 203.66/203.95 (step @p1095 :rule cong :premises (@p1094) :args ((not @t939))) % 203.66/203.95 (step @p1096 :rule trans :premises (@p1095 @p1089)) % 203.66/203.95 (step @p1097 :rule arith-elim-lt :args (0 @t13)) % 203.66/203.95 (step @p1098 :rule trans :premises (@p1097 @p1096)) % 203.66/203.95 (step @p1099 :rule aci_norm :args ((= (or @t943 (or @t942 @t941)) @t944))) % 203.66/203.95 (step @p1100 :rule bool-implies-de-morgan :args (@t918 @t940)) % 203.66/203.95 (step @p1101 :rule bool-implies-de-morgan :args (@t919 @t31)) % 203.66/203.95 (step @p1102 :rule nary_cong :premises (@p1101 @p1100) :args ((or (not @t946) (not @t945)))) % 203.66/203.95 (step @p1103 :rule bool-and-de-morgan :args (@t946 @t945 true)) % 203.66/203.95 (step @p1104 :rule trans :premises (@p1103 @p1102)) % 203.66/203.95 (step @p1105 :rule refl :args (@t943)) % 203.66/203.95 (step @p1106 :rule nary_cong :premises (@p1105 @p1104) :args ((or @t943 @t947))) % 203.66/203.95 (step @p1107 :rule trans :premises (@p1106 @p1099)) % 203.66/203.95 (step @p1108 :rule bool-impl-elim :args (@t36 @t947)) % 203.66/203.95 (step @p1109 :rule trans :premises (@p1108 @p1107)) % 203.66/203.95 (step @p1110 :rule cong :premises (@p1109) :args ((forall @t38 (=> @t36 @t947)))) % 203.66/203.95 (step @p1111 :rule refl :args (|tptp.'pa$'|)) % 203.66/203.95 (step @p1112 :rule refl :args (@t16)) % 203.66/203.95 (step @p1113 :rule arith_poly_norm :args ((= (+ @t17 -1) @t916))) % 203.66/203.95 (step @p1114 :rule refl :args (@t17)) % 203.66/203.95 (step @p1115 :rule nary_cong :premises (@p1114 @p752) :args (@t948)) % 203.66/203.95 (step @p1116 :rule trans :premises (@p1115 @p1113)) % 203.66/203.95 (step @p1117 :rule arith_poly_norm :args ((= @t18 @t948))) % 203.66/203.95 (step @p1118 :rule trans :premises (@p1117 @p1116)) % 203.66/203.95 (step @p1119 :rule cong :premises (@p1118) :args (@t19)) % 203.66/203.95 (step @p1120 :rule cong :premises (@p1119 @p1112) :args (@t20)) % 203.66/203.95 (step @p1121 :rule cong :premises (@p1120) :args (@t21)) % 203.66/203.95 (step @p1122 :rule refl :args (@t22)) % 203.66/203.95 (step @p1123 :rule cong :premises (@p1122 @p1121) :args (@t23)) % 203.66/203.95 (step @p1124 :rule cong :premises (@p1123 @p749) :args (@t24)) % 203.66/203.95 (step @p1125 :rule cong :premises (@p1124 @p1111) :args (@t25)) % 203.66/203.95 (step @p1126 :rule bool-double-not-elim :args (@t918)) % 203.66/203.95 (step @p1127 :rule arith-elim-lt :args (@t17 1)) % 203.66/203.95 (step @p1128 :rule cong :premises (@p1127) :args (@t27)) % 203.66/203.95 (step @p1129 :rule trans :premises (@p1128 @p1126)) % 203.66/203.95 (step @p1130 :rule cong :premises (@p1129 @p1125) :args (@t28)) % 203.66/203.95 (step @p1131 :rule refl :args (@t31)) % 203.66/203.95 (step @p1132 :rule cong :premises (@p1127 @p1131) :args (@t32)) % 203.66/203.95 (step @p1133 :rule nary_cong :premises (@p1132 @p1130) :args (@t33)) % 203.66/203.95 (step @p1134 :rule cong :premises (@p1133) :args (@t34)) % 203.66/203.95 (step @p1135 :rule refl :args (@t36)) % 203.66/203.95 (step @p1136 :rule cong :premises (@p1135 @p1134) :args (@t37)) % 203.66/203.95 (step @p1137 :rule cong :premises (@p1136) :args (@t39)) % 203.66/203.95 (step @p1138 :rule trans :premises (@p1137 @p1110)) % 203.66/203.95 (step @p1139 :rule nary_cong :premises (@p1138 @p1098) :args (@t40)) % 203.66/203.95 (step @p1140 :rule refl :args (@t42)) % 203.66/203.95 (step @p1141 :rule cong :premises (@p1140 @p1139) :args (@t43)) % 203.66/203.95 (step @p1142 :rule refl :args (@t47)) % 203.66/203.95 (step @p1143 :rule nary_cong :premises (@p1142 @p1141) :args (@t48)) % 203.66/203.95 (step @p1144 :rule cong :premises (@p1143) :args (@t49)) % 203.66/203.95 (step @p1145 :rule eq_resolve :premises (@p5 @p1144)) % 203.66/203.95 (step @p1146 :rule not_and :premises (@p1145)) % 203.66/203.95 (step @p1147 :rule cnf_implies_neg1 :args (@t951)) % 203.66/203.95 (step @p1148 :rule reordering :premises (@p1147) :args ((or @t42 @t951))) % 203.66/203.95 (step @p1149 :rule instantiate :premises (@p8) :args ((@list |tptp.'pa$'| |tptp.'pa$'| |tptp.'aa$'| |tptp.'xa$'|))) % 203.66/203.95 (step @p1150 :rule refl :args (@t928)) % 203.66/203.95 (step @p1151 :rule bool-double-not-elim :args (@t952)) % 203.66/203.95 (step @p1152 :rule refl :args (@t930)) % 203.66/203.95 (step @p1153 :rule nary_cong :premises (@p1152 @p1151 @p1150) :args ((or @t930 (not @t953) @t928))) % 203.66/203.95 (assume-push @p1260 @t46) % 203.66/203.95 (assume-push @p1261 @t953) % 203.66/203.95 (assume-push @p1262 @t953) % 203.66/203.95 (assume-push @p1263 @t46) % 203.66/203.95 (step @p1158 :rule false_intro :premises (@p1149)) % 203.66/203.95 (step @p1159 :rule refl :args (@t41)) % 203.66/203.95 (step @p1160 :rule cong :premises (@p1260 @p1159) :args (@t42)) % 203.66/203.95 (step @p1161 :rule trans :premises (@p1160 @p1158)) % 203.66/203.95 (step @p1162 :rule false_elim :premises (@p1161)) % 203.66/203.95 (step-pop @p1264 :rule scope :premises (@p1162)) % 203.66/203.95 (step-pop @p1265 :rule scope :premises (@p1264)) % 203.66/203.95 (step @p1163 :rule process_scope :premises (@p1265) :args (@t928)) % 203.66/203.95 (step @p1166 :rule and_intro :premises (@p1149 @p1260)) % 203.66/203.95 (step @p1167 :rule modus_ponens :premises (@p1166 @p1163)) % 203.66/203.95 (step-pop @p1266 :rule scope :premises (@p1167)) % 203.66/203.95 (step-pop @p1267 :rule scope :premises (@p1266)) % 203.66/203.95 (step @p1168 :rule process_scope :premises (@p1267) :args (@t928)) % 203.66/203.95 (step @p1171 :rule implies_elim :premises (@p1168)) % 203.66/203.95 (step @p1172 :rule cnf_and_neg :args (@t954)) % 203.66/203.95 (step @p1173 :rule resolution :premises (@p1172 @p1171) :args (true @t954)) % 203.66/203.95 (step @p1174 :rule eq_resolve :premises (@p1173 @p1153)) % 203.66/203.95 (step @p1175 :rule reordering :premises (@p1174) :args ((or @t930 @t928 @t952))) % 203.66/203.95 (step @p1176 :rule chain_m_resolution :premises (@p1175 @p1149 @p1148 @p1146 @p1088 @p1087 @p1085) :args (@t930 (@list true false true false false false) (@list @t952 @t42 @t951 @t47 @t44 @t931))) % 203.66/203.95 (step @p1177 :rule cnf_implies_neg1 :args (@t47)) % 203.66/203.95 (step @p1178 :rule reordering :premises (@p1177) :args ((or @t46 @t47))) % 203.66/203.95 (step @p1179 :rule chain_m_resolution :premises (@p1178 @p1176) :args (@t47 @t955 (@list @t46))) % 203.66/203.95 (step @p1180 :rule chain_m_resolution :premises (@p1146 @p1179) :args ((not @t951) @t912 (@list @t47))) % 203.66/203.95 (step @p1181 :rule cnf_implies_neg2 :args (@t951)) % 203.66/203.95 (step @p1182 :rule chain_m_resolution :premises (@p1181 @p1180) :args ((not @t950) @t955 @t956)) % 203.66/203.95 (step @p1183 :rule cnf_and_pos :args (@t932 1)) % 203.66/203.95 (step @p1184 :rule reordering :premises (@p1183) :args ((or @t929 @t936))) % 203.66/203.95 (step @p1185 :rule chain_m_resolution :premises (@p1184 @p1082) :args (@t929 @t912 @t937)) % 203.66/203.95 (step @p1186 :rule chain_m_resolution :premises (@p1148 @p1180) :args (@t42 @t955 @t956)) % 203.66/203.95 (step @p1187 :rule cnf_or_pos :args (@t929)) % 203.66/203.95 (step @p1188 :rule reordering :premises (@p1187) :args ((or @t928 @t920 (not @t929)))) % 203.66/203.95 (step @p1189 :rule chain_m_resolution :premises (@p1188 @p1186 @p1185) :args (@t920 @t935 (@list @t42 @t929))) % 203.66/203.95 (step @p1190 :rule cnf_and_pos :args (@t920 1)) % 203.66/203.95 (step @p1191 :rule reordering :premises (@p1190) :args ((or @t913 (not @t920)))) % 203.66/203.95 (step @p1192 :rule chain_m_resolution :premises (@p1191 @p1189) :args (@t913 @t912 (@list @t920))) % 203.66/203.95 (step @p1193 :rule cnf_and_neg :args (@t950)) % 203.66/203.95 (step @p1194 :rule reordering :premises (@p1193) :args ((or (not @t913) @t950 @t957))) % 203.66/203.95 (step @p1195 :rule chain_m_resolution :premises (@p1194 @p1192 @p1182) :args (@t957 @t958 (@list @t913 @t950))) % 203.66/203.95 (step @p1196 :rule refl :args (@t962)) % 203.66/203.95 (step @p1197 :rule bool-double-not-elim :args (@t949)) % 203.66/203.95 (step @p1198 :rule nary_cong :premises (@p1197 @p1196) :args ((or (not @t957) @t962))) % 203.66/203.95 (assume-push @p1268 @t957) % 203.66/203.95 (step @p1200 :rule skolemize :premises (@p1268)) % 203.66/203.95 (step-pop @p1269 :rule scope :premises (@p1200)) % 203.66/203.95 (step @p1201 :rule process_scope :premises (@p1269) :args (@t962)) % 203.66/203.95 (step @p1203 :rule implies_elim :premises (@p1201)) % 203.66/203.95 (step @p1204 :rule eq_resolve :premises (@p1203 @p1198)) % 203.66/203.95 (step @p1205 :rule chain_m_resolution :premises (@p1204 @p1195) :args (@t962 @t955 (@list @t949))) % 203.66/203.95 (step @p1206 :rule cnf_and_pos :args (@t963 0)) % 203.66/203.95 (step @p1207 :rule reordering :premises (@p1206) :args ((or @t961 @t964))) % 203.66/203.96 (step @p1208 :rule chain_m_resolution :premises (@p1207 @p1205) :args (@t964 @t955 (@list @t961))) % 203.66/203.96 (step @p1209 :rule cnf_or_pos :args (@t965)) % 203.66/203.96 (step @p1210 :rule reordering :premises (@p1209) :args ((or @t928 @t963 @t966))) % 203.66/203.96 (step @p1211 :rule chain_m_resolution :premises (@p1210 @p1186 @p1208) :args (@t966 @t958 (@list @t42 @t963))) % 203.66/203.96 (step @p1212 :rule refl :args (@t963)) % 203.66/203.96 (step @p1213 :rule nary_cong :premises (@p1062 @p1212) :args (@t967)) % 203.66/203.96 (step @p1214 :rule nary_cong :premises (@p1067 @p1213) :args (@t968)) % 203.66/203.96 (step @p1215 :rule nary_cong :premises (@p1069 @p1214) :args (@t969)) % 203.66/203.96 (step @p1216 :rule cong :premises (@p1071 @p1215) :args ((=> @t883 @t969))) % 203.66/203.96 (assume-push @p1270 @t883) % 203.66/203.96 (step @p1218 :rule instantiate :premises (@p1270) :args ((@list |tptp.'ta$'| |tptp.'pa$'| |tptp.'aa$'| |tptp.'xa$'| @t959))) % 203.66/203.96 (step-pop @p1271 :rule scope :premises (@p1218)) % 203.66/203.96 (step @p1219 :rule process_scope :premises (@p1271) :args (@t969)) % 203.66/203.96 (step @p1221 :rule eq_resolve :premises (@p1219 @p1216)) % 203.66/203.96 (step @p1222 :rule implies_elim :premises (@p1221)) % 203.66/203.96 (step @p1223 :rule chain_m_resolution :premises (@p1222 @p1059) :args (@t971 @t912 @t934)) % 203.66/203.96 (step @p1224 :rule cnf_or_pos :args (@t971)) % 203.66/203.96 (step @p1225 :rule reordering :premises (@p1224) :args ((or @t926 @t970 (not @t971)))) % 203.66/203.96 (step @p1226 :rule chain_m_resolution :premises (@p1225 @p99 @p1223) :args (@t970 @t935 (@list @t212 @t971))) % 203.66/203.96 (step @p1227 :rule cnf_and_pos :args (@t970 1)) % 203.66/203.96 (step @p1228 :rule reordering :premises (@p1227) :args ((or @t965 (not @t970)))) % 203.66/203.96 (step @p1229 false :rule chain_m_resolution :premises (@p1228 @p1226 @p1211) :args (false @t958 (@list @t970 @t965))) % 203.66/203.96 ) % 203.66/203.96 % SZS output end Proof % 203.66/203.96 % cvc5 exiting %------------------------------------------------------------------------------