%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP049^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n009.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:24:54 AM UTC 2026 % Result : Theorem 0.47s 0.87s % Output : Proof 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP049^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n009.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 04:11:59 EDT 2026 % 0.16/0.34 % CPUTime : % 0.38/0.63 %----Proving TH0 % 0.47/0.87 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.47/0.87 % SZS status Theorem % 0.47/0.87 % SZS output start Proof % 0.47/0.87 ( % 0.47/0.87 (declare-sort tptp.set_nat 0) % 0.47/0.87 (declare-sort tptp.nat 0) % 0.47/0.87 (declare-sort tptp.set_Pr1490359111at_nat 0) % 0.47/0.87 (declare-sort tptp.set_Pr1986765409at_nat 0) % 0.47/0.87 (declare-sort tptp.set_Pr1746169692at_nat 0) % 0.47/0.87 (declare-sort tptp.product_prod_nat_nat 0) % 0.47/0.87 (declare-sort tptp.set_Pr1287749686at_nat 0) % 0.47/0.87 (declare-sort tptp.produc1695820582at_nat 0) % 0.47/0.87 (declare-sort tptp.produc842455143at_nat 0) % 0.47/0.87 (declare-sort tptp.produc1271302400at_nat 0) % 0.47/0.87 (declare-sort tptp.list_nat 0) % 0.47/0.87 (declare-sort tptp.set_set_nat 0) % 0.47/0.87 (declare-sort tptp.a 0) % 0.47/0.87 (declare-sort tptp.list_P559422087at_nat 0) % 0.47/0.87 (declare-sort tptp.set_se1612935105at_nat 0) % 0.47/0.87 (declare-const tptp.isShortestPath_a (-> (-> tptp.product_prod_nat_nat tptp.a) tptp.nat tptp.list_P559422087at_nat tptp.nat Bool)) % 0.47/0.87 (declare-const tptp.set_Pr2131844118at_nat (-> tptp.list_P559422087at_nat tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.member701585322at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat Bool)) % 0.47/0.87 (declare-const tptp.collec7649004at_nat (-> (-> tptp.product_prod_nat_nat Bool) tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.e_a (-> (-> tptp.product_prod_nat_nat tptp.a) tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.product_Pair_nat_nat (-> tptp.nat tptp.nat tptp.product_prod_nat_nat)) % 0.47/0.87 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.47/0.87 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 0.47/0.87 (declare-const tptp.transi1645084429cl_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.finite_finite_nat (-> tptp.set_nat Bool)) % 0.47/0.87 (declare-const tptp.transi1484096900at_nat (-> tptp.set_Pr1490359111at_nat tptp.set_Pr1490359111at_nat)) % 0.47/0.87 (declare-const tptp.finite277291581at_nat (-> tptp.set_Pr1746169692at_nat Bool)) % 0.47/0.87 (declare-const tptp.produc894163943at_nat (-> tptp.set_nat (-> tptp.nat tptp.set_Pr1986765409at_nat) tptp.set_Pr1746169692at_nat)) % 0.47/0.87 (declare-const tptp.finite2000257047at_nat (-> tptp.set_Pr1287749686at_nat Bool)) % 0.47/0.87 (declare-const tptp.produc2055342601at_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.product_prod_nat_nat tptp.set_nat) tptp.set_Pr1287749686at_nat)) % 0.47/0.87 (declare-const tptp.produc2056081288at_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat) tptp.set_Pr1490359111at_nat)) % 0.47/0.87 (declare-const tptp.isPath_a (-> (-> tptp.product_prod_nat_nat tptp.a) tptp.nat tptp.list_P559422087at_nat tptp.nat Bool)) % 0.47/0.87 (declare-const tptp.image_981520924at_nat (-> tptp.set_Pr1746169692at_nat tptp.set_nat tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.ord_le148299708at_nat (-> tptp.set_Pr1746169692at_nat tptp.set_Pr1746169692at_nat Bool)) % 0.47/0.87 (declare-const tptp.member868723479at_nat (-> tptp.produc1271302400at_nat tptp.set_Pr1287749686at_nat Bool)) % 0.47/0.87 (declare-const tptp.produc947540346at_nat (-> tptp.product_prod_nat_nat tptp.nat tptp.produc1271302400at_nat)) % 0.47/0.87 (declare-const tptp.ord_le1837363350at_nat (-> tptp.set_Pr1287749686at_nat tptp.set_Pr1287749686at_nat Bool)) % 0.47/0.87 (declare-const tptp.member2027625872at_nat (-> tptp.produc842455143at_nat tptp.set_Pr1490359111at_nat Bool)) % 0.47/0.87 (declare-const tptp.produc1168807639at_nat (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat tptp.produc842455143at_nat)) % 0.47/0.87 (declare-const tptp.image_2142699582at_nat (-> tptp.set_Pr1287749686at_nat tptp.set_Pr1986765409at_nat tptp.set_nat)) % 0.47/0.87 (declare-const tptp.isSimplePath_a (-> (-> tptp.product_prod_nat_nat tptp.a) tptp.nat tptp.list_P559422087at_nat tptp.nat Bool)) % 0.47/0.87 (declare-const tptp.finite1457549322at_nat (-> tptp.set_se1612935105at_nat Bool)) % 0.47/0.87 (declare-const tptp.collec1606769740at_nat (-> (-> tptp.set_Pr1986765409at_nat Bool) tptp.set_se1612935105at_nat)) % 0.47/0.87 (declare-const tptp.ord_less_eq_nat_o (-> (-> tptp.nat Bool) (-> tptp.nat Bool) Bool)) % 0.47/0.87 (declare-const tptp.member1293241661at_nat (-> tptp.produc1695820582at_nat tptp.set_Pr1746169692at_nat Bool)) % 0.47/0.87 (declare-const tptp.ord_le841296385at_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat Bool)) % 0.47/0.87 (declare-const tptp.t tptp.nat) % 0.47/0.87 (declare-const tptp.finite772653738at_nat (-> tptp.set_Pr1986765409at_nat Bool)) % 0.47/0.87 (declare-const tptp.c (-> tptp.product_prod_nat_nat tptp.a)) % 0.47/0.87 (declare-const tptp.image_1655366419at_nat (-> tptp.set_Pr1490359111at_nat tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.produc1933845336at_nat (-> tptp.nat tptp.product_prod_nat_nat tptp.produc1695820582at_nat)) % 0.47/0.87 (declare-const tptp.s tptp.nat) % 0.47/0.87 (declare-const tptp.range_nat_nat (-> tptp.set_Pr1986765409at_nat tptp.set_nat)) % 0.47/0.87 (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 0.47/0.87 (declare-const tptp.product_swap_nat_nat (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)) % 0.47/0.87 (declare-const tptp.adjacent_nodes_a (-> (-> tptp.product_prod_nat_nat tptp.a) tptp.nat tptp.set_nat)) % 0.47/0.87 (declare-const tptp.edmond1517640972ysis_a (-> (-> tptp.product_prod_nat_nat tptp.a) Bool)) % 0.47/0.87 (declare-const tptp.image_nat_nat (-> tptp.set_Pr1986765409at_nat tptp.set_nat tptp.set_nat)) % 0.47/0.87 (declare-const tptp.collect_set_nat (-> (-> tptp.set_nat Bool) tptp.set_set_nat)) % 0.47/0.87 (declare-const tptp.finite2012248349et_nat (-> tptp.set_set_nat Bool)) % 0.47/0.87 (declare-const tptp.ord_le1578155910_nat_o (-> (-> tptp.nat tptp.nat Bool) (-> tptp.nat tptp.nat Bool) Bool)) % 0.47/0.87 (declare-const tptp.member298845450at_nat (-> tptp.set_Pr1986765409at_nat tptp.set_se1612935105at_nat Bool)) % 0.47/0.87 (declare-const tptp.ord_le465611495at_nat (-> tptp.set_Pr1490359111at_nat tptp.set_Pr1490359111at_nat Bool)) % 0.47/0.87 (declare-const tptp.member_set_nat (-> tptp.set_nat tptp.set_set_nat Bool)) % 0.47/0.87 (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool)) % 0.47/0.87 (declare-const tptp.set_nat2 (-> tptp.list_nat tptp.set_nat)) % 0.47/0.87 (declare-const tptp.domain37934156at_nat (-> tptp.set_Pr1490359111at_nat tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (declare-const tptp.ord_le1039616028_nat_o (-> (-> tptp.product_prod_nat_nat Bool) (-> tptp.product_prod_nat_nat Bool) Bool)) % 0.47/0.87 (declare-const tptp.finite48957584at_nat (-> tptp.set_Pr1490359111at_nat Bool)) % 0.47/0.87 (declare-const tptp.produc45129834at_nat (-> tptp.set_nat (-> tptp.nat tptp.set_nat) tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define tptp.edmond475474835dges_a () (let ((_let_1 (@var "T" tptp.nat))) (let ((_let_2 (@var "P" tptp.list_P559422087at_nat))) (let ((_let_3 (@var "S2" tptp.nat))) (let ((_let_4 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_5 (@var "E" tptp.product_prod_nat_nat))) (lambda (@list _let_4 _let_3 _let_1) (_ tptp.collec7649004at_nat (lambda (@list _let_5) (exists (@list _let_2) (and (_ (_ tptp.member701585322at_nat _let_5) (_ tptp.set_Pr2131844118at_nat _let_2)) (_ (_ (_ (_ tptp.isShortestPath_a _let_4) _let_3) _let_2) _let_1)))))))))))) % 0.47/0.87 (define tptp.incoming_a () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (@var "V2" tptp.nat))) (let ((_let_3 (@var "U3" tptp.nat))) (let ((_let_4 (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2))) (let ((_let_5 (@var "Uu" tptp.product_prod_nat_nat))) (lambda (@list _let_1 _let_2) (_ tptp.collec7649004at_nat (lambda (@list _let_5) (exists (@list _let_3) (and (= _let_5 _let_4) (_ (_ tptp.member701585322at_nat _let_4) (_ tptp.e_a _let_1))))))))))))) % 0.47/0.87 (define tptp.incoming_a2 () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (@var "V2" tptp.nat))) (let ((_let_3 (@var "U3" tptp.nat))) (let ((_let_4 (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2))) (let ((_let_5 (@var "K2" tptp.set_nat))) (let ((_let_6 (@var "Uu" tptp.product_prod_nat_nat))) (lambda (@list _let_1 _let_5) (_ tptp.collec7649004at_nat (lambda (@list _let_6) (exists (@list _let_3 _let_2) (and (= _let_6 _let_4) (not (_ (_ tptp.member_nat _let_3) _let_5)) (_ (_ tptp.member_nat _let_2) _let_5) (_ (_ tptp.member701585322at_nat _let_4) (_ tptp.e_a _let_1)))))))))))))) % 0.47/0.87 (define tptp.outgoing_a2 () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (@var "U3" tptp.nat))) (let ((_let_3 (@var "V2" tptp.nat))) (let ((_let_4 (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2))) (let ((_let_5 (@var "K2" tptp.set_nat))) (let ((_let_6 (@var "Uu" tptp.product_prod_nat_nat))) (lambda (@list _let_1 _let_5) (_ tptp.collec7649004at_nat (lambda (@list _let_6) (exists (@list _let_2 _let_3) (and (= _let_6 _let_4) (not (_ (_ tptp.member_nat _let_2) _let_5)) (_ (_ tptp.member_nat _let_3) _let_5) (_ (_ tptp.member701585322at_nat _let_4) (_ tptp.e_a _let_1)))))))))))))) % 0.47/0.87 (define tptp.v_a () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (_ tptp.e_a _let_1))) (let ((_let_3 (@var "U3" tptp.nat))) (let ((_let_4 (@var "V2" tptp.nat))) (lambda (@list _let_1) (_ tptp.collect_nat (lambda (@list _let_3) (exists (@list _let_4) (or (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat _let_3) _let_4)) _let_2) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat _let_4) _let_3)) _let_2))))))))))) % 0.47/0.87 (define tptp.connected_a () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (@var "V2" tptp.nat))) (let ((_let_3 (@var "U3" tptp.nat))) (lambda (@list _let_1 _let_3 _let_2) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2)) (_ tptp.transi1645084429cl_nat (_ tptp.e_a _let_1)))))))) % 0.47/0.87 (define tptp.reachableNodes_a () (let ((_let_1 (@var "U3" tptp.nat))) (let ((_let_2 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (lambda (@list _let_2 _let_1) (_ tptp.collect_nat (_ (_ tptp.connected_a _let_2) _let_1)))))) % 0.47/0.87 (define tptp.domain_nat_nat () (let ((_let_1 (@var "R3" tptp.set_Pr1986765409at_nat))) (let ((_let_2 (@var "Y" tptp.nat))) (let ((_let_3 (@var "X" tptp.nat))) (lambda (@list _let_1) (_ tptp.collect_nat (lambda (@list _let_3) (exists (@list _let_2) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2)) _let_1))))))))) % 0.47/0.87 (define tptp.finite_Graph_a () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (lambda (@list _let_1) (_ tptp.finite_finite_nat (_ tptp.v_a _let_1))))) % 0.47/0.87 (define tptp.outgoing_a () (let ((_let_1 (@var "C2" (-> tptp.product_prod_nat_nat tptp.a)))) (let ((_let_2 (@var "U3" tptp.nat))) (let ((_let_3 (@var "V2" tptp.nat))) (let ((_let_4 (_ (_ tptp.product_Pair_nat_nat _let_3) _let_2))) (let ((_let_5 (@var "Uu" tptp.product_prod_nat_nat))) (lambda (@list _let_1 _let_3) (_ tptp.collec7649004at_nat (lambda (@list _let_5) (exists (@list _let_2) (and (= _let_5 _let_4) (_ (_ tptp.member701585322at_nat _let_4) (_ tptp.e_a _let_1))))))))))))) % 0.47/0.87 (define @t1 () (_ (_ (_ tptp.edmond475474835dges_a tptp.c) tptp.s) tptp.t)) % 0.47/0.87 (define @t2 () (_ tptp.finite772653738at_nat @t1)) % 0.47/0.87 (define @t3 () (_ tptp.e_a tptp.c)) % 0.47/0.87 (define @t4 () (_ tptp.finite772653738at_nat @t3)) % 0.47/0.87 (define @t5 () (=> @t4 @t2)) % 0.47/0.87 (define @t6 () (_ tptp.finite_Graph_a tptp.c)) % 0.47/0.87 (define @t7 () (@var "V" tptp.nat)) % 0.47/0.87 (define @t8 () (_ tptp.connected_a tptp.c)) % 0.47/0.87 (define @t9 () (_ @t8 @t7)) % 0.47/0.87 (define @t10 () (@list @t7)) % 0.47/0.87 (define @t11 () (@var "P" tptp.list_P559422087at_nat)) % 0.47/0.87 (define @t12 () (_ tptp.isShortestPath_a tptp.c)) % 0.47/0.87 (define @t13 () (_ tptp.set_Pr2131844118at_nat @t11)) % 0.47/0.87 (define @t14 () (@var "E" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t15 () (_ tptp.member701585322at_nat @t14)) % 0.47/0.87 (define @t16 () (_ @t15 @t13)) % 0.47/0.87 (define @t17 () (@list @t11)) % 0.47/0.87 (define @t18 () (@list @t14)) % 0.47/0.87 (define @t19 () (@var "R" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t20 () (_ tptp.range_nat_nat @t19)) % 0.47/0.87 (define @t21 () (_ tptp.finite772653738at_nat @t19)) % 0.47/0.87 (define @t22 () (@list @t19)) % 0.47/0.87 (define @t23 () (_ tptp.domain_nat_nat @t19)) % 0.47/0.87 (define @t24 () (_ tptp.v_a tptp.c)) % 0.47/0.87 (define @t25 () (_ tptp.finite_finite_nat @t24)) % 0.47/0.87 (define @t26 () (@var "U" tptp.nat)) % 0.47/0.87 (define @t27 () (_ tptp.member_nat @t26)) % 0.47/0.87 (define @t28 () (_ tptp.member_nat @t7)) % 0.47/0.87 (define @t29 () (_ @t8 @t26)) % 0.47/0.87 (define @t30 () (_ @t29 @t7)) % 0.47/0.87 (define @t31 () (@list @t26 @t7)) % 0.47/0.87 (define @t32 () (@var "P2" tptp.list_P559422087at_nat)) % 0.47/0.87 (define @t33 () (_ @t12 @t26)) % 0.47/0.87 (define @t34 () (@list @t32)) % 0.47/0.87 (define @t35 () (@var "X" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t36 () (@var "Q" (-> tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t37 () (_ @t36 @t35)) % 0.47/0.87 (define @t38 () (@var "P3" (-> tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t39 () (_ @t38 @t35)) % 0.47/0.87 (define @t40 () (@list @t35)) % 0.47/0.87 (define @t41 () (_ tptp.collec7649004at_nat @t36)) % 0.47/0.87 (define @t42 () (_ tptp.finite772653738at_nat @t41)) % 0.47/0.87 (define @t43 () (_ tptp.collec7649004at_nat @t38)) % 0.47/0.87 (define @t44 () (_ tptp.finite772653738at_nat @t43)) % 0.47/0.87 (define @t45 () (@list @t38 @t36)) % 0.47/0.87 (define @t46 () (@var "X" tptp.nat)) % 0.47/0.87 (define @t47 () (@var "Q" (-> tptp.nat Bool))) % 0.47/0.87 (define @t48 () (_ @t47 @t46)) % 0.47/0.87 (define @t49 () (@var "P3" (-> tptp.nat Bool))) % 0.47/0.87 (define @t50 () (_ @t49 @t46)) % 0.47/0.87 (define @t51 () (@list @t46)) % 0.47/0.87 (define @t52 () (_ tptp.collect_nat @t47)) % 0.47/0.87 (define @t53 () (_ tptp.finite_finite_nat @t52)) % 0.47/0.87 (define @t54 () (_ tptp.collect_nat @t49)) % 0.47/0.87 (define @t55 () (_ tptp.finite_finite_nat @t54)) % 0.47/0.87 (define @t56 () (@list @t49 @t47)) % 0.47/0.87 (define @t57 () (@var "Y" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t58 () (@var "Q" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t59 () (_ (_ @t58 @t35) @t57)) % 0.47/0.87 (define @t60 () (_ @t38 @t57)) % 0.47/0.87 (define @t61 () (@list @t57)) % 0.47/0.87 (define @t62 () (@var "Q" (-> tptp.nat tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t63 () (_ (_ @t62 @t46) @t57)) % 0.47/0.87 (define @t64 () (@var "Y" tptp.nat)) % 0.47/0.87 (define @t65 () (@var "Q" (-> tptp.product_prod_nat_nat tptp.nat Bool))) % 0.47/0.87 (define @t66 () (_ (_ @t65 @t35) @t64)) % 0.47/0.87 (define @t67 () (_ @t49 @t64)) % 0.47/0.87 (define @t68 () (@list @t64)) % 0.47/0.87 (define @t69 () (@var "Q" (-> tptp.nat tptp.nat Bool))) % 0.47/0.87 (define @t70 () (_ (_ @t69 @t46) @t64)) % 0.47/0.87 (define @t71 () (@var "A" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t72 () (@var "B" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t73 () (_ tptp.finite772653738at_nat @t71)) % 0.47/0.87 (define @t74 () (@list @t71)) % 0.47/0.87 (define @t75 () (@var "A" tptp.set_nat)) % 0.47/0.87 (define @t76 () (@var "B" tptp.set_nat)) % 0.47/0.87 (define @t77 () (_ tptp.finite_finite_nat @t75)) % 0.47/0.87 (define @t78 () (@list @t75)) % 0.47/0.87 (define @t79 () (@var "S" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t80 () (_ tptp.ord_le841296385at_nat @t19)) % 0.47/0.87 (define @t81 () (_ @t80 @t79)) % 0.47/0.87 (define @t82 () (@list @t19 @t79)) % 0.47/0.87 (define @t83 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t84 () (@var "Uu" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t85 () (@list @t84)) % 0.47/0.87 (define @t86 () (@var "F" (-> tptp.product_prod_nat_nat tptp.nat))) % 0.47/0.87 (define @t87 () (@var "Uu" tptp.nat)) % 0.47/0.87 (define @t88 () (@list @t87)) % 0.47/0.87 (define @t89 () (@var "F" (-> tptp.nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t90 () (@var "F" (-> tptp.nat tptp.nat))) % 0.47/0.87 (define @t91 () (_ @t36 @t57)) % 0.47/0.87 (define @t92 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t93 () (@list @t35 @t57)) % 0.47/0.87 (define @t94 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat tptp.nat))) % 0.47/0.87 (define @t95 () (_ @t47 @t64)) % 0.47/0.87 (define @t96 () (@var "F" (-> tptp.product_prod_nat_nat tptp.nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t97 () (@list @t35 @t64)) % 0.47/0.87 (define @t98 () (@var "F" (-> tptp.product_prod_nat_nat tptp.nat tptp.nat))) % 0.47/0.87 (define @t99 () (@var "F" (-> tptp.nat tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t100 () (@list @t46 @t57)) % 0.47/0.87 (define @t101 () (@var "F" (-> tptp.nat tptp.product_prod_nat_nat tptp.nat))) % 0.47/0.87 (define @t102 () (@var "F" (-> tptp.nat tptp.nat tptp.product_prod_nat_nat))) % 0.47/0.87 (define @t103 () (@list @t46 @t64)) % 0.47/0.87 (define @t104 () (@var "F" (-> tptp.nat tptp.nat tptp.nat))) % 0.47/0.87 (define @t105 () (@var "X_1" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t106 () (@var "X_1" tptp.nat)) % 0.47/0.87 (define @t107 () (@var "X2" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t108 () (@var "A2" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t109 () (@var "R2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t110 () (_ (_ tptp.member701585322at_nat @t108) @t71)) % 0.47/0.87 (define @t111 () (@list @t108)) % 0.47/0.87 (define @t112 () (@var "B2" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t113 () (_ tptp.member701585322at_nat @t107)) % 0.47/0.87 (define @t114 () (_ @t113 @t112)) % 0.47/0.87 (define @t115 () (@list @t107)) % 0.47/0.87 (define @t116 () (@var "Xa" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t117 () (_ (_ tptp.member701585322at_nat @t116) @t112)) % 0.47/0.87 (define @t118 () (@list @t116)) % 0.47/0.87 (define @t119 () (_ @t113 @t71)) % 0.47/0.87 (define @t120 () (_ tptp.finite772653738at_nat @t112)) % 0.47/0.87 (define @t121 () (not @t73)) % 0.47/0.87 (define @t122 () (@var "X2" tptp.nat)) % 0.47/0.87 (define @t123 () (@var "R2" (-> tptp.product_prod_nat_nat tptp.nat Bool))) % 0.47/0.87 (define @t124 () (@var "B2" tptp.set_nat)) % 0.47/0.87 (define @t125 () (_ tptp.member_nat @t122)) % 0.47/0.87 (define @t126 () (_ @t125 @t124)) % 0.47/0.87 (define @t127 () (@list @t122)) % 0.47/0.87 (define @t128 () (@var "Xa" tptp.nat)) % 0.47/0.87 (define @t129 () (_ tptp.member_nat @t128)) % 0.47/0.87 (define @t130 () (_ @t129 @t124)) % 0.47/0.87 (define @t131 () (@list @t128)) % 0.47/0.87 (define @t132 () (_ tptp.finite_finite_nat @t124)) % 0.47/0.87 (define @t133 () (@var "A2" tptp.nat)) % 0.47/0.87 (define @t134 () (@var "R2" (-> tptp.nat tptp.product_prod_nat_nat Bool))) % 0.47/0.87 (define @t135 () (_ (_ tptp.member_nat @t133) @t75)) % 0.47/0.87 (define @t136 () (@list @t133)) % 0.47/0.87 (define @t137 () (_ @t125 @t75)) % 0.47/0.87 (define @t138 () (not @t77)) % 0.47/0.87 (define @t139 () (@var "R2" (-> tptp.nat tptp.nat Bool))) % 0.47/0.87 (define @t140 () (@var "C" (-> tptp.product_prod_nat_nat tptp.a))) % 0.47/0.87 (define @t141 () (_ tptp.edmond1517640972ysis_a @t140)) % 0.47/0.87 (define @t142 () (_ tptp.finite_Graph_a @t140)) % 0.47/0.87 (define @t143 () (@list @t140)) % 0.47/0.87 (define @t144 () (@var "Xa" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t145 () (@var "X2" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t146 () (= @t145 @t144)) % 0.47/0.87 (define @t147 () (@var "A" tptp.set_se1612935105at_nat)) % 0.47/0.87 (define @t148 () (_ (_ tptp.member298845450at_nat @t144) @t147)) % 0.47/0.87 (define @t149 () (@list @t144)) % 0.47/0.87 (define @t150 () (@var "A3" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t151 () (_ tptp.ord_le841296385at_nat @t145)) % 0.47/0.87 (define @t152 () (_ (_ tptp.member298845450at_nat @t145) @t147)) % 0.47/0.87 (define @t153 () (@list @t145)) % 0.47/0.87 (define @t154 () (_ (_ tptp.member298845450at_nat @t150) @t147)) % 0.47/0.87 (define @t155 () (_ tptp.finite1457549322at_nat @t147)) % 0.47/0.87 (define @t156 () (@list @t147 @t150)) % 0.47/0.87 (define @t157 () (@var "Xa" tptp.set_nat)) % 0.47/0.87 (define @t158 () (@var "X2" tptp.set_nat)) % 0.47/0.87 (define @t159 () (= @t158 @t157)) % 0.47/0.87 (define @t160 () (@var "A" tptp.set_set_nat)) % 0.47/0.87 (define @t161 () (_ (_ tptp.member_set_nat @t157) @t160)) % 0.47/0.87 (define @t162 () (@list @t157)) % 0.47/0.87 (define @t163 () (@var "A3" tptp.set_nat)) % 0.47/0.87 (define @t164 () (_ tptp.ord_less_eq_set_nat @t158)) % 0.47/0.87 (define @t165 () (_ (_ tptp.member_set_nat @t158) @t160)) % 0.47/0.87 (define @t166 () (@list @t158)) % 0.47/0.87 (define @t167 () (_ (_ tptp.member_set_nat @t163) @t160)) % 0.47/0.87 (define @t168 () (_ tptp.finite2012248349et_nat @t160)) % 0.47/0.87 (define @t169 () (@list @t160 @t163)) % 0.47/0.87 (define @t170 () (= @t122 @t128)) % 0.47/0.87 (define @t171 () (_ @t129 @t75)) % 0.47/0.87 (define @t172 () (@var "A3" tptp.nat)) % 0.47/0.87 (define @t173 () (_ tptp.ord_less_eq_nat @t122)) % 0.47/0.87 (define @t174 () (_ tptp.member_nat @t172)) % 0.47/0.87 (define @t175 () (_ @t174 @t75)) % 0.47/0.87 (define @t176 () (@list @t75 @t172)) % 0.47/0.87 (define @t177 () (_ tptp.ord_le841296385at_nat @t150)) % 0.47/0.87 (define @t178 () (_ tptp.ord_less_eq_set_nat @t163)) % 0.47/0.87 (define @t179 () (_ tptp.ord_less_eq_nat @t172)) % 0.47/0.87 (define @t180 () (_ tptp.ord_le841296385at_nat @t71)) % 0.47/0.87 (define @t181 () (_ @t180 @t112)) % 0.47/0.87 (define @t182 () (_ tptp.ord_less_eq_set_nat @t75)) % 0.47/0.87 (define @t183 () (_ @t182 @t124)) % 0.47/0.87 (define @t184 () (@var "T2" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t185 () (@var "S3" tptp.set_Pr1986765409at_nat)) % 0.47/0.87 (define @t186 () (_ tptp.ord_le841296385at_nat @t185)) % 0.47/0.87 (define @t187 () (@var "T2" tptp.set_nat)) % 0.47/0.87 (define @t188 () (@var "S3" tptp.set_nat)) % 0.47/0.87 (define @t189 () (@list @t71 @t112)) % 0.47/0.87 (define @t190 () (@list @t75 @t124)) % 0.47/0.87 (define @t191 () (_ tptp.e_a @t140)) % 0.47/0.87 (define @t192 () (@var "T3" tptp.nat)) % 0.47/0.87 (define @t193 () (@var "S" tptp.nat)) % 0.47/0.87 (define @t194 () (@var "U2" tptp.set_nat)) % 0.47/0.87 (define @t195 () (_ tptp.incoming_a2 tptp.c)) % 0.47/0.87 (define @t196 () (_ @t195 @t194)) % 0.47/0.87 (define @t197 () (@list @t194)) % 0.47/0.87 (define @t198 () (_ tptp.outgoing_a2 tptp.c)) % 0.47/0.87 (define @t199 () (_ @t198 @t194)) % 0.47/0.87 (define @t200 () (_ tptp.reachableNodes_a tptp.c)) % 0.47/0.87 (define @t201 () (@list @t26)) % 0.47/0.87 (define @t202 () (@var "Xs" tptp.list_P559422087at_nat)) % 0.47/0.87 (define @t203 () (_ tptp.set_Pr2131844118at_nat @t202)) % 0.47/0.87 (define @t204 () (@var "Xs" tptp.list_nat)) % 0.47/0.87 (define @t205 () (_ tptp.set_nat2 @t204)) % 0.47/0.87 (define @t206 () (_ tptp.v_a @t140)) % 0.47/0.87 (define @t207 () (_ tptp.finite_finite_nat @t206)) % 0.47/0.87 (define @t208 () (_ tptp.finite772653738at_nat @t191)) % 0.47/0.87 (define @t209 () (@var "A3" tptp.product_prod_nat_nat)) % 0.47/0.87 (define @t210 () (_ tptp.member701585322at_nat @t209)) % 0.47/0.87 (define @t211 () (_ @t49 @t172)) % 0.47/0.87 (define @t212 () (_ tptp.member701585322at_nat @t35)) % 0.47/0.87 (define @t213 () (_ tptp.member_nat @t46)) % 0.47/0.88 (define @t214 () (_ @t213 @t75)) % 0.47/0.88 (define @t215 () (@var "P4" tptp.list_P559422087at_nat)) % 0.47/0.88 (define @t216 () (_ tptp.set_Pr2131844118at_nat @t215)) % 0.47/0.88 (define @t217 () (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t26) @t7))) % 0.47/0.88 (define @t218 () (_ @t217 @t216)) % 0.47/0.88 (define @t219 () (_ (_ (_ @t12 @t193) @t215) @t192)) % 0.47/0.88 (define @t220 () (@list @t193 @t215 @t192 @t26 @t7)) % 0.47/0.88 (define @t221 () (_ tptp.incoming_a tptp.c)) % 0.47/0.88 (define @t222 () (_ @t221 @t26)) % 0.47/0.88 (define @t223 () (_ @t200 @t193)) % 0.47/0.88 (define @t224 () (_ tptp.member_nat @t193)) % 0.47/0.88 (define @t225 () (@list @t193)) % 0.47/0.88 (define @t226 () (@var "W" tptp.nat)) % 0.47/0.88 (define @t227 () (_ tptp.product_Pair_nat_nat @t7)) % 0.47/0.88 (define @t228 () (_ tptp.member701585322at_nat (_ @t227 @t226))) % 0.47/0.88 (define @t229 () (@var "U3" tptp.nat)) % 0.47/0.88 (define @t230 () (@var "V2" tptp.nat)) % 0.47/0.88 (define @t231 () (_ (_ tptp.product_Pair_nat_nat @t230) @t229)) % 0.47/0.88 (define @t232 () (_ tptp.member701585322at_nat @t231)) % 0.47/0.88 (define @t233 () (_ @t232 @t3)) % 0.47/0.88 (define @t234 () (_ tptp.product_Pair_nat_nat @t229)) % 0.47/0.88 (define @t235 () (_ @t234 @t230)) % 0.47/0.88 (define @t236 () (_ tptp.member701585322at_nat @t235)) % 0.47/0.88 (define @t237 () (_ @t236 @t3)) % 0.47/0.88 (define @t238 () (@list @t230)) % 0.47/0.88 (define @t239 () (@list @t229)) % 0.47/0.88 (define @t240 () (_ @t234 @t7)) % 0.47/0.88 (define @t241 () (@var "K" tptp.set_nat)) % 0.47/0.88 (define @t242 () (_ tptp.member_nat @t230)) % 0.47/0.88 (define @t243 () (_ @t242 @t241)) % 0.47/0.88 (define @t244 () (_ tptp.member_nat @t229)) % 0.47/0.88 (define @t245 () (not (_ @t244 @t241))) % 0.47/0.88 (define @t246 () (= @t84 @t231)) % 0.47/0.88 (define @t247 () (@list @t229 @t230)) % 0.47/0.88 (define @t248 () (@list @t241)) % 0.47/0.88 (define @t249 () (= @t84 @t235)) % 0.47/0.88 (define @t250 () (@var "K" tptp.nat)) % 0.47/0.88 (define @t251 () (@var "N" tptp.nat)) % 0.47/0.88 (define @t252 () (_ (_ tptp.adjacent_nodes_a tptp.c) @t26)) % 0.47/0.88 (define @t253 () (_ (_ tptp.reachableNodes_a @t140) @t193)) % 0.47/0.88 (define @t254 () (@var "R2" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t255 () (_ tptp.product_Pair_nat_nat @t46)) % 0.47/0.88 (define @t256 () (_ tptp.member701585322at_nat (_ @t255 @t64))) % 0.47/0.88 (define @t257 () (lambda @t103 (_ @t256 @t185))) % 0.47/0.88 (define @t258 () (lambda @t103 (_ @t256 @t254))) % 0.47/0.88 (define @t259 () (@list @t254 @t185)) % 0.47/0.88 (define @t260 () (_ (_ tptp.ord_le841296385at_nat @t254) @t185)) % 0.47/0.88 (define @t261 () (@var "Y2" tptp.nat)) % 0.47/0.88 (define @t262 () (_ tptp.product_Pair_nat_nat @t122)) % 0.47/0.88 (define @t263 () (_ @t262 @t261)) % 0.47/0.88 (define @t264 () (_ tptp.member701585322at_nat @t263)) % 0.47/0.88 (define @t265 () (@list @t122 @t261)) % 0.47/0.88 (define @t266 () (@var "X3" tptp.nat)) % 0.47/0.88 (define @t267 () (_ @t49 @t266)) % 0.47/0.88 (define @t268 () (@var "A4" tptp.nat)) % 0.47/0.88 (define @t269 () (@var "B3" tptp.nat)) % 0.47/0.88 (define @t270 () (_ tptp.product_Pair_nat_nat @t268)) % 0.47/0.88 (define @t271 () (_ @t270 @t269)) % 0.47/0.88 (define @t272 () (_ tptp.member701585322at_nat @t271)) % 0.47/0.88 (define @t273 () (_ @t272 @t19)) % 0.47/0.88 (define @t274 () (@list @t268 @t269)) % 0.47/0.88 (define @t275 () (_ tptp.member_nat @t266)) % 0.47/0.88 (define @t276 () (@list @t266 @t19 @t49)) % 0.47/0.88 (define @t277 () (_ @t174 @t23)) % 0.47/0.88 (define @t278 () (@var "B4" tptp.nat)) % 0.47/0.88 (define @t279 () (_ tptp.product_Pair_nat_nat @t172)) % 0.47/0.88 (define @t280 () (_ @t279 @t278)) % 0.47/0.88 (define @t281 () (_ tptp.member701585322at_nat @t280)) % 0.47/0.88 (define @t282 () (_ @t281 @t19)) % 0.47/0.88 (define @t283 () (@list @t172 @t278 @t19)) % 0.47/0.88 (define @t284 () (@var "B5" tptp.nat)) % 0.47/0.88 (define @t285 () (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t133) @t284))) % 0.47/0.88 (define @t286 () (_ @t285 @t19)) % 0.47/0.88 (define @t287 () (@list @t133 @t284)) % 0.47/0.88 (define @t288 () (@list @t172 @t19)) % 0.47/0.88 (define @t289 () (@list @t269)) % 0.47/0.88 (define @t290 () (_ tptp.member_nat @t278)) % 0.47/0.88 (define @t291 () (_ @t290 @t20)) % 0.47/0.88 (define @t292 () (_ @t174 @t20)) % 0.47/0.88 (define @t293 () (@list @t268)) % 0.47/0.88 (define @t294 () (@var "R2" tptp.set_nat)) % 0.47/0.88 (define @t295 () (_ tptp.connected_a @t140)) % 0.47/0.88 (define @t296 () (_ @t295 @t26)) % 0.47/0.88 (define @t297 () (_ @t296 @t7)) % 0.47/0.88 (define @t298 () (_ (_ tptp.incoming_a @t140) @t26)) % 0.47/0.88 (define @t299 () (@list @t140 @t26)) % 0.47/0.88 (define @t300 () (_ tptp.isShortestPath_a @t140)) % 0.47/0.88 (define @t301 () (_ (_ (_ @t300 @t193) @t215) @t192)) % 0.47/0.88 (define @t302 () (@list @t140 @t193 @t215 @t192 @t26 @t7)) % 0.47/0.88 (define @t303 () (_ @t295 @t7)) % 0.47/0.88 (define @t304 () (_ (_ tptp.outgoing_a2 @t140) @t194)) % 0.47/0.88 (define @t305 () (@list @t140 @t194)) % 0.47/0.88 (define @t306 () (_ (_ tptp.incoming_a2 @t140) @t194)) % 0.47/0.88 (define @t307 () (@var "Xs2" tptp.list_P559422087at_nat)) % 0.47/0.88 (define @t308 () (@var "Xs2" tptp.list_nat)) % 0.47/0.88 (define @t309 () (@list @t140 @t26 @t7)) % 0.47/0.88 (define @t310 () (_ @t227 @t229)) % 0.47/0.88 (define @t311 () (_ tptp.outgoing_a tptp.c)) % 0.47/0.88 (define @t312 () (_ @t311 @t26)) % 0.47/0.88 (define @t313 () (_ @t217 (_ tptp.transi1645084429cl_nat @t3))) % 0.47/0.88 (define @t314 () (@var "U1" tptp.nat)) % 0.47/0.88 (define @t315 () (_ tptp.product_Pair_nat_nat @t314)) % 0.47/0.88 (define @t316 () (not (_ (_ tptp.member701585322at_nat (_ @t315 @t314)) @t216))) % 0.47/0.88 (define @t317 () (_ tptp.isSimplePath_a tptp.c)) % 0.47/0.88 (define @t318 () (_ (_ (_ @t317 @t26) @t215) @t7)) % 0.47/0.88 (define @t319 () (@var "V1" tptp.nat)) % 0.47/0.88 (define @t320 () (@var "U22" tptp.nat)) % 0.47/0.88 (define @t321 () (_ (_ tptp.member701585322at_nat (_ @t315 @t319)) @t216)) % 0.47/0.88 (define @t322 () (=> @t321 (=> (not (= @t314 @t320)) (not (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t320) @t319)) @t216))))) % 0.47/0.88 (define @t323 () (@var "V22" tptp.nat)) % 0.47/0.88 (define @t324 () (=> @t321 (=> (not (= @t319 @t323)) (not (_ (_ tptp.member701585322at_nat (_ @t315 @t323)) @t216))))) % 0.47/0.88 (define @t325 () (_ @t317 @t193)) % 0.47/0.88 (define @t326 () (_ (_ @t325 @t215) @t192)) % 0.47/0.88 (define @t327 () (@list @t193 @t215 @t192)) % 0.47/0.88 (define @t328 () (@var "R" tptp.set_Pr1490359111at_nat)) % 0.47/0.88 (define @t329 () (_ tptp.image_1655366419at_nat @t328)) % 0.47/0.88 (define @t330 () (_ @t329 @t71)) % 0.47/0.88 (define @t331 () (@var "B4" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t332 () (_ tptp.member701585322at_nat @t331)) % 0.47/0.88 (define @t333 () (_ @t332 @t330)) % 0.47/0.88 (define @t334 () (_ @t210 @t71)) % 0.47/0.88 (define @t335 () (_ tptp.member2027625872at_nat (_ (_ tptp.produc1168807639at_nat @t209) @t331))) % 0.47/0.88 (define @t336 () (_ @t335 @t328)) % 0.47/0.88 (define @t337 () (@list @t209 @t331 @t328 @t71)) % 0.47/0.88 (define @t338 () (@var "R" tptp.set_Pr1287749686at_nat)) % 0.47/0.88 (define @t339 () (_ (_ tptp.image_2142699582at_nat @t338) @t71)) % 0.47/0.88 (define @t340 () (_ @t290 @t339)) % 0.47/0.88 (define @t341 () (_ tptp.member868723479at_nat (_ (_ tptp.produc947540346at_nat @t209) @t278))) % 0.47/0.88 (define @t342 () (_ @t341 @t338)) % 0.47/0.88 (define @t343 () (@var "R" tptp.set_Pr1746169692at_nat)) % 0.47/0.88 (define @t344 () (_ (_ tptp.image_981520924at_nat @t343) @t75)) % 0.47/0.88 (define @t345 () (_ @t332 @t344)) % 0.47/0.88 (define @t346 () (_ tptp.member1293241661at_nat (_ (_ tptp.produc1933845336at_nat @t172) @t331))) % 0.47/0.88 (define @t347 () (_ @t346 @t343)) % 0.47/0.88 (define @t348 () (_ tptp.image_nat_nat @t19)) % 0.47/0.88 (define @t349 () (_ @t348 @t75)) % 0.47/0.88 (define @t350 () (_ @t290 @t349)) % 0.47/0.88 (define @t351 () (@list @t172 @t278 @t19 @t75)) % 0.47/0.88 (define @t352 () (@var "B2" (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t353 () (_ tptp.produc2056081288at_nat @t71)) % 0.47/0.88 (define @t354 () (_ @t353 @t352)) % 0.47/0.88 (define @t355 () (@var "A4" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t356 () (_ (_ tptp.member701585322at_nat @t355) @t71)) % 0.47/0.88 (define @t357 () (@list @t355)) % 0.47/0.88 (define @t358 () (@var "B2" (-> tptp.product_prod_nat_nat tptp.set_nat))) % 0.47/0.88 (define @t359 () (_ tptp.produc2055342601at_nat @t71)) % 0.47/0.88 (define @t360 () (_ @t359 @t358)) % 0.47/0.88 (define @t361 () (@var "B2" (-> tptp.nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t362 () (_ tptp.produc894163943at_nat @t75)) % 0.47/0.88 (define @t363 () (_ @t362 @t361)) % 0.47/0.88 (define @t364 () (_ (_ tptp.member_nat @t268) @t75)) % 0.47/0.88 (define @t365 () (@var "B2" (-> tptp.nat tptp.set_nat))) % 0.47/0.88 (define @t366 () (_ tptp.produc45129834at_nat @t75)) % 0.47/0.88 (define @t367 () (_ @t366 @t365)) % 0.47/0.88 (define @t368 () (@list @t278 @t19 @t75)) % 0.47/0.88 (define @t369 () (not @t119)) % 0.47/0.88 (define @t370 () (_ tptp.produc1168807639at_nat @t107)) % 0.47/0.88 (define @t371 () (not @t137)) % 0.47/0.88 (define @t372 () (_ tptp.produc1933845336at_nat @t122)) % 0.47/0.88 (define @t373 () (_ tptp.produc947540346at_nat @t107)) % 0.47/0.88 (define @t374 () (@var "C3" tptp.set_nat)) % 0.47/0.88 (define @t375 () (_ @t366 (lambda @t88 @t124))) % 0.47/0.88 (define @t376 () (_ tptp.isSimplePath_a @t140)) % 0.47/0.88 (define @t377 () (_ (_ (_ @t376 @t193) @t215) @t192)) % 0.47/0.88 (define @t378 () (@var "A5" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t379 () (@var "R4" tptp.set_Pr1490359111at_nat)) % 0.47/0.88 (define @t380 () (_ (_ tptp.ord_le841296385at_nat @t378) @t71)) % 0.47/0.88 (define @t381 () (@var "R4" tptp.set_Pr1287749686at_nat)) % 0.47/0.88 (define @t382 () (@var "A5" tptp.set_nat)) % 0.47/0.88 (define @t383 () (@var "R4" tptp.set_Pr1746169692at_nat)) % 0.47/0.88 (define @t384 () (_ (_ tptp.ord_less_eq_set_nat @t382) @t75)) % 0.47/0.88 (define @t385 () (@var "R4" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t386 () (_ tptp.finite772653738at_nat @t254)) % 0.47/0.88 (define @t387 () (@list @t254 @t75)) % 0.47/0.88 (define @t388 () (_ tptp.finite48957584at_nat (_ @t353 (lambda @t85 @t112)))) % 0.47/0.88 (define @t389 () (_ tptp.finite2000257047at_nat (_ @t359 (lambda @t85 @t124)))) % 0.47/0.88 (define @t390 () (@list @t71 @t124)) % 0.47/0.88 (define @t391 () (_ tptp.finite277291581at_nat (_ @t362 (lambda @t88 @t112)))) % 0.47/0.88 (define @t392 () (@list @t75 @t112)) % 0.47/0.88 (define @t393 () (_ tptp.finite772653738at_nat @t375)) % 0.47/0.88 (define @t394 () (_ (_ (_ @t376 @t26) @t215) @t7)) % 0.47/0.88 (define @t395 () (_ (_ tptp.adjacent_nodes_a @t140) @t26)) % 0.47/0.88 (define @t396 () (_ (_ tptp.outgoing_a @t140) @t26)) % 0.47/0.88 (define @t397 () (@var "E2" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t398 () (_ tptp.member701585322at_nat @t397)) % 0.47/0.88 (define @t399 () (_ @t398 @t216)) % 0.47/0.88 (define @t400 () (=> @t399 (not (_ (_ tptp.member701585322at_nat (_ tptp.product_swap_nat_nat @t397)) @t216)))) % 0.47/0.88 (define @t401 () (_ @t332 (_ @t352 @t209))) % 0.47/0.88 (define @t402 () (_ @t335 @t354)) % 0.47/0.88 (define @t403 () (@list @t209 @t331 @t71 @t352)) % 0.47/0.88 (define @t404 () (_ @t290 (_ @t358 @t209))) % 0.47/0.88 (define @t405 () (_ @t341 @t360)) % 0.47/0.88 (define @t406 () (@list @t209 @t278 @t71 @t358)) % 0.47/0.88 (define @t407 () (_ @t332 (_ @t361 @t172))) % 0.47/0.88 (define @t408 () (_ @t346 @t363)) % 0.47/0.88 (define @t409 () (@list @t172 @t331 @t75 @t361)) % 0.47/0.88 (define @t410 () (_ @t290 (_ @t365 @t172))) % 0.47/0.88 (define @t411 () (_ @t281 @t367)) % 0.47/0.88 (define @t412 () (@list @t172 @t278 @t75 @t365)) % 0.47/0.88 (define @t413 () (_ tptp.transi1484096900at_nat @t328)) % 0.47/0.88 (define @t414 () (= @t172 @t278)) % 0.47/0.88 (define @t415 () (_ tptp.transi1645084429cl_nat @t19)) % 0.47/0.88 (define @t416 () (_ @t281 @t415)) % 0.47/0.88 (define @t417 () (@var "B6" tptp.nat)) % 0.47/0.88 (define @t418 () (= @t278 @t417)) % 0.47/0.88 (define @t419 () (@var "A6" tptp.nat)) % 0.47/0.88 (define @t420 () (= @t172 @t419)) % 0.47/0.88 (define @t421 () (= @t280 (_ (_ tptp.product_Pair_nat_nat @t419) @t417))) % 0.47/0.88 (define @t422 () (@list @t172 @t278 @t419 @t417)) % 0.47/0.88 (define @t423 () (@var "Y22" tptp.nat)) % 0.47/0.88 (define @t424 () (@var "X22" tptp.nat)) % 0.47/0.88 (define @t425 () (@var "Y1" tptp.nat)) % 0.47/0.88 (define @t426 () (@var "X1" tptp.nat)) % 0.47/0.88 (define @t427 () (_ (_ tptp.product_Pair_nat_nat @t426) @t424)) % 0.47/0.88 (define @t428 () (@var "P4" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t429 () (_ tptp.member701585322at_nat @t428)) % 0.47/0.88 (define @t430 () (@list @t428)) % 0.47/0.88 (define @t431 () (@var "Y3" tptp.nat)) % 0.47/0.88 (define @t432 () (_ tptp.product_Pair_nat_nat @t431)) % 0.47/0.88 (define @t433 () (_ tptp.product_Pair_nat_nat @t266)) % 0.47/0.88 (define @t434 () (_ @t433 @t431)) % 0.47/0.88 (define @t435 () (@list @t266 @t431)) % 0.47/0.88 (define @t436 () (@var "Ay" tptp.nat)) % 0.47/0.88 (define @t437 () (@var "Ax" tptp.nat)) % 0.47/0.88 (define @t438 () (@var "P3" (-> tptp.nat tptp.nat Bool))) % 0.47/0.88 (define @t439 () (_ (_ @t438 @t437) @t436)) % 0.47/0.88 (define @t440 () (_ @t438 @t268)) % 0.47/0.88 (define @t441 () (_ @t440 @t269)) % 0.47/0.88 (define @t442 () (@var "Ba" tptp.nat)) % 0.47/0.88 (define @t443 () (@var "Aa" tptp.nat)) % 0.47/0.88 (define @t444 () (_ (_ @t438 @t443) @t442)) % 0.47/0.88 (define @t445 () (@var "By" tptp.nat)) % 0.47/0.88 (define @t446 () (@var "Bx" tptp.nat)) % 0.47/0.88 (define @t447 () (_ (_ tptp.product_Pair_nat_nat @t446) @t445)) % 0.47/0.88 (define @t448 () (_ (_ tptp.product_Pair_nat_nat @t443) @t442)) % 0.47/0.88 (define @t449 () (_ tptp.produc1168807639at_nat @t271)) % 0.47/0.88 (define @t450 () (_ (_ tptp.member2027625872at_nat (_ @t449 @t448)) @t328)) % 0.47/0.88 (define @t451 () (@list @t268 @t269 @t443 @t442)) % 0.47/0.88 (define @t452 () (_ (_ @t438 @t446) @t445)) % 0.47/0.88 (define @t453 () (_ tptp.produc1168807639at_nat (_ (_ tptp.product_Pair_nat_nat @t437) @t436))) % 0.47/0.88 (define @t454 () (_ (_ tptp.member2027625872at_nat (_ @t453 @t447)) @t413)) % 0.47/0.88 (define @t455 () (@list @t437 @t436 @t446 @t445 @t328 @t438)) % 0.47/0.88 (define @t456 () (@var "Zb" tptp.nat)) % 0.47/0.88 (define @t457 () (@var "Za" tptp.nat)) % 0.47/0.88 (define @t458 () (_ (_ tptp.product_Pair_nat_nat @t457) @t456)) % 0.47/0.88 (define @t459 () (@var "Xb" tptp.nat)) % 0.47/0.88 (define @t460 () (@var "Xa2" tptp.nat)) % 0.47/0.88 (define @t461 () (_ (_ tptp.product_Pair_nat_nat @t460) @t459)) % 0.47/0.88 (define @t462 () (_ tptp.produc1168807639at_nat @t461)) % 0.47/0.88 (define @t463 () (@var "Prod" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t464 () (forall @t274 (_ @t38 @t271))) % 0.47/0.88 (define @t465 () (@var "Y3" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t466 () (@var "D" (-> tptp.nat tptp.set_nat))) % 0.47/0.88 (define @t467 () (_ tptp.produc45129834at_nat @t124)) % 0.47/0.88 (define @t468 () (@var "C3" (-> tptp.nat tptp.set_nat))) % 0.47/0.88 (define @t469 () (_ @t466 @t122)) % 0.47/0.88 (define @t470 () (= @t75 @t124)) % 0.47/0.88 (define @t471 () (lambda @t88 @t374)) % 0.47/0.88 (define @t472 () (_ @t467 @t471)) % 0.47/0.88 (define @t473 () (_ @t366 @t471)) % 0.47/0.88 (define @t474 () (_ @t275 @t374)) % 0.47/0.88 (define @t475 () (@list @t266 @t374 @t75 @t124)) % 0.47/0.88 (define @t476 () (@var "Y2" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t477 () (@var "C" tptp.produc842455143at_nat)) % 0.47/0.88 (define @t478 () (_ @t352 @t107)) % 0.47/0.88 (define @t479 () (_ tptp.member701585322at_nat @t476)) % 0.47/0.88 (define @t480 () (@list @t476)) % 0.47/0.88 (define @t481 () (@var "C" tptp.produc1271302400at_nat)) % 0.47/0.88 (define @t482 () (_ @t358 @t107)) % 0.47/0.88 (define @t483 () (_ tptp.member_nat @t261)) % 0.47/0.88 (define @t484 () (@list @t261)) % 0.47/0.88 (define @t485 () (@var "C" tptp.produc1695820582at_nat)) % 0.47/0.88 (define @t486 () (_ @t361 @t122)) % 0.47/0.88 (define @t487 () (@var "C" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t488 () (_ @t365 @t122)) % 0.47/0.88 (define @t489 () (_ tptp.product_Pair_nat_nat @t261)) % 0.47/0.88 (define @t490 () (_ (_ tptp.member701585322at_nat (_ @t279 @t261)) @t415)) % 0.47/0.88 (define @t491 () (@var "A22" tptp.nat)) % 0.47/0.88 (define @t492 () (_ tptp.product_Pair_nat_nat @t269)) % 0.47/0.88 (define @t493 () (@var "A1" tptp.nat)) % 0.47/0.88 (define @t494 () (_ tptp.product_Pair_nat_nat @t493)) % 0.47/0.88 (define @t495 () (_ (_ tptp.member701585322at_nat (_ @t494 @t491)) @t415)) % 0.47/0.88 (define @t496 () (@list @t493 @t491 @t19)) % 0.47/0.88 (define @t497 () (@var "C2" tptp.nat)) % 0.47/0.88 (define @t498 () (= @t493 @t133)) % 0.47/0.88 (define @t499 () (@var "Z" tptp.nat)) % 0.47/0.88 (define @t500 () (_ (_ tptp.member701585322at_nat (_ @t433 @t499)) @t415)) % 0.47/0.88 (define @t501 () (_ tptp.member701585322at_nat @t434)) % 0.47/0.88 (define @t502 () (_ @t49 @t278)) % 0.47/0.88 (define @t503 () (@var "Z2" tptp.nat)) % 0.47/0.88 (define @t504 () (_ @t49 @t503)) % 0.47/0.88 (define @t505 () (_ @t49 @t261)) % 0.47/0.88 (define @t506 () (_ (_ tptp.member701585322at_nat (_ @t489 @t503)) @t19)) % 0.47/0.88 (define @t507 () (@list @t261 @t503)) % 0.47/0.88 (define @t508 () (@list @t172 @t278 @t19 @t49)) % 0.47/0.88 (define @t509 () (@var "C4" tptp.nat)) % 0.47/0.88 (define @t510 () (@var "C" tptp.nat)) % 0.47/0.88 (define @t511 () (_ (_ tptp.member701585322at_nat (_ @t279 @t510)) @t415)) % 0.47/0.88 (define @t512 () (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t278) @t510))) % 0.47/0.88 (define @t513 () (@list @t172 @t278 @t19 @t510)) % 0.47/0.88 (define @t514 () (_ tptp.transi1645084429cl_nat @t79)) % 0.47/0.88 (define @t515 () (_ (_ tptp.ord_le841296385at_nat @t415) @t514)) % 0.47/0.88 (define @t516 () (_ tptp.transi1645084429cl_nat @t254)) % 0.47/0.88 (define @t517 () (@var "D" (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t518 () (@var "C3" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t519 () (_ @t180 @t518)) % 0.47/0.88 (define @t520 () (@var "D" (-> tptp.product_prod_nat_nat tptp.set_nat))) % 0.47/0.88 (define @t521 () (@var "D" (-> tptp.nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t522 () (_ @t182 @t374)) % 0.47/0.88 (define @t523 () (@var "X4" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t524 () (@var "X4" tptp.set_nat)) % 0.47/0.88 (define @t525 () (@var "X3" tptp.product_prod_nat_nat)) % 0.47/0.88 (define @t526 () (@var "R2" tptp.set_Pr1490359111at_nat)) % 0.47/0.88 (define @t527 () (_ tptp.transi1484096900at_nat @t526)) % 0.47/0.88 (define @t528 () (_ tptp.member701585322at_nat @t525)) % 0.47/0.88 (define @t529 () (= @t266 @t431)) % 0.47/0.88 (define @t530 () (lambda @t85 @t518)) % 0.47/0.88 (define @t531 () (_ @t528 @t518)) % 0.47/0.88 (define @t532 () (lambda @t85 @t374)) % 0.47/0.88 (define @t533 () (lambda @t88 @t518)) % 0.47/0.88 (define @t534 () (not @t120)) % 0.47/0.88 (define @t535 () (not @t132)) % 0.47/0.88 (define @t536 () (@var "X3" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t537 () (_ tptp.ord_le841296385at_nat @t536)) % 0.47/0.88 (define @t538 () (@var "X3" tptp.set_nat)) % 0.47/0.88 (define @t539 () (_ tptp.ord_less_eq_set_nat @t538)) % 0.47/0.88 (define @t540 () (_ tptp.ord_less_eq_nat @t266)) % 0.47/0.88 (define @t541 () (@var "C" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t542 () (@var "F" (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t543 () (@var "Y2" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t544 () (_ @t151 @t543)) % 0.47/0.88 (define @t545 () (@list @t145 @t543)) % 0.47/0.88 (define @t546 () (forall @t545 (=> @t544 (_ (_ tptp.ord_le841296385at_nat (_ @t542 @t145)) (_ @t542 @t543))))) % 0.47/0.88 (define @t547 () (@var "B4" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t548 () (_ tptp.ord_le841296385at_nat @t547)) % 0.47/0.88 (define @t549 () (_ @t548 @t541)) % 0.47/0.88 (define @t550 () (=> @t549 (=> @t546 (_ @t177 (_ @t542 @t541))))) % 0.47/0.88 (define @t551 () (_ @t542 @t547)) % 0.47/0.88 (define @t552 () (@list @t150 @t542 @t547 @t541)) % 0.47/0.88 (define @t553 () (@var "C" tptp.set_nat)) % 0.47/0.88 (define @t554 () (@var "F" (-> tptp.set_nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t555 () (@var "Y2" tptp.set_nat)) % 0.47/0.88 (define @t556 () (_ @t164 @t555)) % 0.47/0.88 (define @t557 () (@list @t158 @t555)) % 0.47/0.88 (define @t558 () (forall @t557 (=> @t556 (_ (_ tptp.ord_le841296385at_nat (_ @t554 @t158)) (_ @t554 @t555))))) % 0.47/0.88 (define @t559 () (@var "B4" tptp.set_nat)) % 0.47/0.88 (define @t560 () (_ tptp.ord_less_eq_set_nat @t559)) % 0.47/0.88 (define @t561 () (_ @t560 @t553)) % 0.47/0.88 (define @t562 () (=> @t561 (=> @t558 (_ @t177 (_ @t554 @t553))))) % 0.47/0.88 (define @t563 () (_ @t554 @t559)) % 0.47/0.88 (define @t564 () (@list @t150 @t554 @t559 @t553)) % 0.47/0.88 (define @t565 () (@var "F" (-> tptp.nat tptp.set_Pr1986765409at_nat))) % 0.47/0.88 (define @t566 () (_ @t173 @t261)) % 0.47/0.88 (define @t567 () (forall @t265 (=> @t566 (_ (_ tptp.ord_le841296385at_nat (_ @t565 @t122)) (_ @t565 @t261))))) % 0.47/0.88 (define @t568 () (_ tptp.ord_less_eq_nat @t278)) % 0.47/0.88 (define @t569 () (_ @t568 @t510)) % 0.47/0.88 (define @t570 () (=> @t569 (=> @t567 (_ @t177 (_ @t565 @t510))))) % 0.47/0.88 (define @t571 () (_ @t565 @t278)) % 0.47/0.88 (define @t572 () (@list @t150 @t565 @t278 @t510)) % 0.47/0.88 (define @t573 () (@var "F" (-> tptp.set_Pr1986765409at_nat tptp.set_nat))) % 0.47/0.88 (define @t574 () (forall @t545 (=> @t544 (_ (_ tptp.ord_less_eq_set_nat (_ @t573 @t145)) (_ @t573 @t543))))) % 0.47/0.88 (define @t575 () (=> @t549 (=> @t574 (_ @t178 (_ @t573 @t541))))) % 0.47/0.88 (define @t576 () (_ @t573 @t547)) % 0.47/0.88 (define @t577 () (@list @t163 @t573 @t547 @t541)) % 0.47/0.88 (define @t578 () (@var "F" (-> tptp.set_nat tptp.set_nat))) % 0.47/0.88 (define @t579 () (forall @t557 (=> @t556 (_ (_ tptp.ord_less_eq_set_nat (_ @t578 @t158)) (_ @t578 @t555))))) % 0.47/0.88 (define @t580 () (=> @t561 (=> @t579 (_ @t178 (_ @t578 @t553))))) % 0.47/0.88 (define @t581 () (_ @t578 @t559)) % 0.47/0.88 (define @t582 () (@list @t163 @t578 @t559 @t553)) % 0.47/0.88 (define @t583 () (@var "F" (-> tptp.nat tptp.set_nat))) % 0.47/0.88 (define @t584 () (forall @t265 (=> @t566 (_ (_ tptp.ord_less_eq_set_nat (_ @t583 @t122)) (_ @t583 @t261))))) % 0.47/0.88 (define @t585 () (=> @t569 (=> @t584 (_ @t178 (_ @t583 @t510))))) % 0.47/0.88 (define @t586 () (_ @t583 @t278)) % 0.47/0.88 (define @t587 () (@list @t163 @t583 @t278 @t510)) % 0.47/0.88 (define @t588 () (@var "F" (-> tptp.set_Pr1986765409at_nat tptp.nat))) % 0.47/0.88 (define @t589 () (forall @t545 (=> @t544 (_ (_ tptp.ord_less_eq_nat (_ @t588 @t145)) (_ @t588 @t543))))) % 0.47/0.88 (define @t590 () (=> @t549 (=> @t589 (_ @t179 (_ @t588 @t541))))) % 0.47/0.88 (define @t591 () (_ @t588 @t547)) % 0.47/0.88 (define @t592 () (@list @t172 @t588 @t547 @t541)) % 0.47/0.88 (define @t593 () (@var "F" (-> tptp.set_nat tptp.nat))) % 0.47/0.88 (define @t594 () (forall @t557 (=> @t556 (_ (_ tptp.ord_less_eq_nat (_ @t593 @t158)) (_ @t593 @t555))))) % 0.47/0.88 (define @t595 () (=> @t561 (=> @t594 (_ @t179 (_ @t593 @t553))))) % 0.47/0.88 (define @t596 () (_ @t593 @t559)) % 0.47/0.88 (define @t597 () (@list @t172 @t593 @t559 @t553)) % 0.47/0.88 (define @t598 () (forall @t265 (=> @t566 (_ (_ tptp.ord_less_eq_nat (_ @t90 @t122)) (_ @t90 @t261))))) % 0.47/0.88 (define @t599 () (=> @t569 (=> @t598 (_ @t179 (_ @t90 @t510))))) % 0.47/0.88 (define @t600 () (_ @t90 @t278)) % 0.47/0.88 (define @t601 () (@list @t172 @t90 @t278 @t510)) % 0.47/0.88 (define @t602 () (=> @t546 (_ (_ tptp.ord_le841296385at_nat (_ @t542 @t150)) @t541))) % 0.47/0.88 (define @t603 () (_ @t177 @t547)) % 0.47/0.88 (define @t604 () (@list @t150 @t547 @t542 @t541)) % 0.47/0.88 (define @t605 () (=> @t574 (_ (_ tptp.ord_less_eq_set_nat (_ @t573 @t150)) @t553))) % 0.47/0.88 (define @t606 () (@list @t150 @t547 @t573 @t553)) % 0.47/0.88 (define @t607 () (=> @t589 (_ (_ tptp.ord_less_eq_nat (_ @t588 @t150)) @t510))) % 0.47/0.88 (define @t608 () (@list @t150 @t547 @t588 @t510)) % 0.47/0.88 (define @t609 () (=> @t558 (_ (_ tptp.ord_le841296385at_nat (_ @t554 @t163)) @t541))) % 0.47/0.88 (define @t610 () (_ @t178 @t559)) % 0.47/0.88 (define @t611 () (@list @t163 @t559 @t554 @t541)) % 0.47/0.88 (define @t612 () (=> @t579 (_ (_ tptp.ord_less_eq_set_nat (_ @t578 @t163)) @t553))) % 0.47/0.88 (define @t613 () (@list @t163 @t559 @t578 @t553)) % 0.47/0.88 (define @t614 () (=> @t594 (_ (_ tptp.ord_less_eq_nat (_ @t593 @t163)) @t510))) % 0.47/0.88 (define @t615 () (@list @t163 @t559 @t593 @t510)) % 0.47/0.88 (define @t616 () (=> @t567 (_ (_ tptp.ord_le841296385at_nat (_ @t565 @t172)) @t541))) % 0.47/0.88 (define @t617 () (_ @t179 @t278)) % 0.47/0.88 (define @t618 () (@list @t172 @t278 @t565 @t541)) % 0.47/0.88 (define @t619 () (=> @t584 (_ (_ tptp.ord_less_eq_set_nat (_ @t583 @t172)) @t553))) % 0.47/0.88 (define @t620 () (@list @t172 @t278 @t583 @t553)) % 0.47/0.88 (define @t621 () (=> @t598 (_ (_ tptp.ord_less_eq_nat (_ @t90 @t172)) @t510))) % 0.47/0.88 (define @t622 () (@list @t172 @t278 @t90 @t510)) % 0.47/0.88 (define @t623 () (@var "X" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t624 () (@var "Y" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t625 () (@var "Z3" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t626 () (@var "Y4" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t627 () (lambda (@list @t626 @t625) (= @t626 @t625))) % 0.47/0.88 (define @t628 () (@var "X" tptp.set_nat)) % 0.47/0.88 (define @t629 () (@var "Y" tptp.set_nat)) % 0.47/0.88 (define @t630 () (@var "Z3" tptp.set_nat)) % 0.47/0.88 (define @t631 () (@var "Y4" tptp.set_nat)) % 0.47/0.88 (define @t632 () (lambda (@list @t631 @t630) (= @t631 @t630))) % 0.47/0.88 (define @t633 () (@var "Z3" tptp.nat)) % 0.47/0.88 (define @t634 () (@var "Y4" tptp.nat)) % 0.47/0.88 (define @t635 () (lambda (@list @t634 @t633) (= @t634 @t633))) % 0.47/0.88 (define @t636 () (@var "Y3" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t637 () (= @t536 @t636)) % 0.47/0.88 (define @t638 () (_ tptp.ord_le841296385at_nat @t636)) % 0.47/0.88 (define @t639 () (_ @t638 @t536)) % 0.47/0.88 (define @t640 () (_ @t537 @t636)) % 0.47/0.88 (define @t641 () (@list @t536 @t636)) % 0.47/0.88 (define @t642 () (@var "Y3" tptp.set_nat)) % 0.47/0.88 (define @t643 () (= @t538 @t642)) % 0.47/0.88 (define @t644 () (_ tptp.ord_less_eq_set_nat @t642)) % 0.47/0.88 (define @t645 () (_ @t644 @t538)) % 0.47/0.88 (define @t646 () (_ @t539 @t642)) % 0.47/0.88 (define @t647 () (@list @t538 @t642)) % 0.47/0.88 (define @t648 () (_ tptp.ord_less_eq_nat @t431)) % 0.47/0.88 (define @t649 () (_ @t648 @t266)) % 0.47/0.88 (define @t650 () (_ @t540 @t431)) % 0.47/0.88 (define @t651 () (not @t650)) % 0.47/0.88 (define @t652 () (_ @t177 @t541)) % 0.47/0.88 (define @t653 () (=> @t549 @t652)) % 0.47/0.88 (define @t654 () (@list @t150 @t547 @t541)) % 0.47/0.88 (define @t655 () (_ @t178 @t553)) % 0.47/0.88 (define @t656 () (=> @t561 @t655)) % 0.47/0.88 (define @t657 () (@list @t163 @t559 @t553)) % 0.47/0.88 (define @t658 () (_ @t179 @t510)) % 0.47/0.88 (define @t659 () (=> @t569 @t658)) % 0.47/0.88 (define @t660 () (@list @t172 @t278 @t510)) % 0.47/0.88 (define @t661 () (_ tptp.ord_less_eq_nat @t499)) % 0.47/0.88 (define @t662 () (_ @t661 @t266)) % 0.47/0.88 (define @t663 () (_ @t648 @t499)) % 0.47/0.88 (define @t664 () (_ @t661 @t431)) % 0.47/0.88 (define @t665 () (_ @t540 @t499)) % 0.47/0.88 (define @t666 () (@list @t266 @t431 @t499)) % 0.47/0.88 (define @t667 () (@var "A2" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t668 () (@var "B5" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t669 () (@var "A2" tptp.set_nat)) % 0.47/0.88 (define @t670 () (@var "B5" tptp.set_nat)) % 0.47/0.88 (define @t671 () (= @t150 @t547)) % 0.47/0.88 (define @t672 () (= @t163 @t559)) % 0.47/0.88 (define @t673 () (@var "Z" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t674 () (@var "Z" tptp.set_nat)) % 0.47/0.88 (define @t675 () (_ tptp.isPath_a tptp.c)) % 0.47/0.88 (define @t676 () (_ @t675 @t26)) % 0.47/0.88 (define @t677 () (@var "P5" tptp.list_P559422087at_nat)) % 0.47/0.88 (define @t678 () (_ (_ @t676 @t215) @t7)) % 0.47/0.88 (define @t679 () (@list @t26 @t215 @t7)) % 0.47/0.88 (define @t680 () (@var "U23" tptp.nat)) % 0.47/0.88 (define @t681 () (@list @t26 @t215 @t7 @t314 @t319)) % 0.47/0.88 (define @t682 () (@var "V23" tptp.nat)) % 0.47/0.88 (define @t683 () (not @t2)) % 0.47/0.88 (define @t684 () (@var "T" tptp.nat)) % 0.47/0.88 (define @t685 () (@var "S2" tptp.nat)) % 0.47/0.88 (define @t686 () (@var "C2" (-> tptp.product_prod_nat_nat tptp.a))) % 0.47/0.88 (define @t687 () (_ (_ (_ (_ tptp.isShortestPath_a @t686) @t685) @t11) @t684)) % 0.47/0.88 (define @t688 () (and @t16 @t687)) % 0.47/0.88 (define @t689 () (exists @t17 @t688)) % 0.47/0.88 (define @t690 () (lambda @t18 @t689)) % 0.47/0.88 (define @t691 () (@list @t686 @t685 @t684)) % 0.47/0.88 (define @t692 () (lambda @t691 (_ tptp.collec7649004at_nat @t690))) % 0.47/0.88 (define @t693 () (_ tptp.e_a @t686)) % 0.47/0.88 (define @t694 () (_ @t236 @t693)) % 0.47/0.88 (define @t695 () (@list @t686 @t230)) % 0.47/0.88 (define @t696 () (lambda @t695 (_ tptp.collec7649004at_nat (lambda @t85 (exists @t239 (and @t249 @t694)))))) % 0.47/0.88 (define @t697 () (@var "K2" tptp.set_nat)) % 0.47/0.88 (define @t698 () (_ @t242 @t697)) % 0.47/0.88 (define @t699 () (not (_ @t244 @t697))) % 0.47/0.88 (define @t700 () (@list @t686 @t697)) % 0.47/0.88 (define @t701 () (lambda @t700 (_ tptp.collec7649004at_nat (lambda @t85 (exists @t247 (and @t249 @t699 @t698 @t694)))))) % 0.47/0.88 (define @t702 () (_ @t232 @t693)) % 0.47/0.88 (define @t703 () (lambda @t700 (_ tptp.collec7649004at_nat (lambda @t85 (exists @t247 (and @t246 @t699 @t698 @t702)))))) % 0.47/0.88 (define @t704 () (@list @t686)) % 0.47/0.88 (define @t705 () (lambda @t704 (_ tptp.collect_nat (lambda @t239 (exists @t238 (or @t694 @t702)))))) % 0.47/0.88 (define @t706 () (lambda (@list @t686 @t229) (_ tptp.collect_nat (_ (_ tptp.connected_a @t686) @t229)))) % 0.47/0.88 (define @t707 () (@var "R3" tptp.set_Pr1986765409at_nat)) % 0.47/0.88 (define @t708 () (lambda (@list @t707) (_ tptp.collect_nat (lambda @t51 (exists @t68 (_ @t256 @t707)))))) % 0.47/0.88 (define @t709 () (lambda @t704 (_ tptp.finite_finite_nat (_ tptp.v_a @t686)))) % 0.47/0.88 (define @t710 () (lambda @t695 (_ tptp.collec7649004at_nat (lambda @t85 (exists @t239 (and @t246 @t702)))))) % 0.47/0.88 (define @t711 () (lambda (@list @t686 @t229 @t230) (_ @t236 (_ tptp.transi1645084429cl_nat @t693)))) % 0.47/0.88 (define @t712 () (tptp.set_Pr2131844118at_nat @t11)) % 0.47/0.88 (define @t713 () (tptp.member701585322at_nat @t14 @t712)) % 0.47/0.88 (define @t714 () (not @t713)) % 0.47/0.88 (define @t715 () (lambda (@list @t684) (_ tptp.collec7649004at_nat (lambda @t18 (not (forall @t17 (or @t714 (not (tptp.isShortestPath_a tptp.c tptp.s @t11 @t684))))))))) % 0.47/0.88 (define @t716 () (lambda (@list @t685 @t684) (_ tptp.collec7649004at_nat (lambda @t18 (not (forall @t17 (or @t714 (not (tptp.isShortestPath_a tptp.c @t685 @t11 @t684))))))))) % 0.47/0.88 (define @t717 () (tptp.isShortestPath_a @t686 @t685 @t11 @t684)) % 0.47/0.88 (define @t718 () (_ (lambda @t691 (_ tptp.collec7649004at_nat (lambda @t18 (not (forall @t17 (or @t714 (not @t717))))))) tptp.c)) % 0.47/0.88 (define @t719 () (_ tptp.finite772653738at_nat (_ (_ @t718 tptp.s) tptp.t))) % 0.47/0.88 (define @t720 () (not @t687)) % 0.47/0.88 (define @t721 () (not @t16)) % 0.47/0.88 (define @t722 () (or @t721 @t720)) % 0.47/0.88 (define @t723 () (forall @t17 (not @t688))) % 0.47/0.88 (define @t724 () (not @t723)) % 0.47/0.88 (assume @p1 (_ tptp.edmond1517640972ysis_a tptp.c)) % 0.47/0.88 (assume @p2 @t5) % 0.47/0.88 (assume @p3 (= tptp.edmond475474835dges_a tptp.edmond475474835dges_a)) % 0.47/0.88 (assume @p4 @t4) % 0.47/0.88 (assume @p5 (_ (_ tptp.ord_le841296385at_nat @t1) @t3)) % 0.47/0.88 (assume @p6 @t6) % 0.47/0.88 (assume @p7 (=> @t4 @t6)) % 0.47/0.88 (assume @p8 (forall @t10 (_ @t9 @t7))) % 0.47/0.88 (assume @p9 (= @t1 (_ tptp.collec7649004at_nat (lambda @t18 (exists @t17 (and @t16 (_ (_ (_ @t12 tptp.s) @t11) tptp.t))))))) % 0.47/0.88 (assume @p10 (forall @t22 (=> @t21 (_ tptp.finite_finite_nat @t20)))) % 0.47/0.88 (assume @p11 (forall @t22 (=> @t21 (_ tptp.finite_finite_nat @t23)))) % 0.47/0.88 (assume @p12 (=> @t4 @t25)) % 0.47/0.88 (assume @p13 (forall @t31 (=> @t30 (= (_ @t28 @t24) (_ @t27 @t24))))) % 0.47/0.88 (assume @p14 (forall @t31 (=> @t30 (not (forall @t34 (not (_ (_ @t33 @t32) @t7))))))) % 0.47/0.88 (assume @p15 (forall @t45 (=> (or @t44 @t42) (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 (and @t39 @t37))))))) % 0.47/0.88 (assume @p16 (forall @t56 (=> (or @t55 @t53) (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 (and @t50 @t48))))))) % 0.47/0.88 (assume @p17 (forall @t45 (= (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 (or @t39 @t37)))) (and @t44 @t42)))) % 0.47/0.88 (assume @p18 (forall @t56 (= (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 (or @t50 @t48)))) (and @t55 @t53)))) % 0.47/0.88 (assume @p19 (forall (@list @t38 @t58) (=> @t44 (= (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 (exists @t61 (and @t60 @t59))))) (forall @t61 (=> @t60 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 @t59))))))))) % 0.47/0.88 (assume @p20 (forall (@list @t38 @t62) (=> @t44 (= (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 (exists @t61 (and @t60 @t63))))) (forall @t61 (=> @t60 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 @t63))))))))) % 0.47/0.88 (assume @p21 (forall (@list @t49 @t65) (=> @t55 (= (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 (exists @t68 (and @t67 @t66))))) (forall @t68 (=> @t67 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t40 @t66))))))))) % 0.47/0.88 (assume @p22 (forall (@list @t49 @t69) (=> @t55 (= (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 (exists @t68 (and @t67 @t70))))) (forall @t68 (=> @t67 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t51 @t70))))))))) % 0.47/0.88 (assume @p23 (forall @t74 (=> @t73 (_ tptp.finite1457549322at_nat (_ tptp.collec1606769740at_nat (lambda (@list @t72) (_ (_ tptp.ord_le841296385at_nat @t72) @t71))))))) % 0.47/0.88 (assume @p24 (forall @t78 (=> @t77 (_ tptp.finite2012248349et_nat (_ tptp.collect_set_nat (lambda (@list @t76) (_ (_ tptp.ord_less_eq_set_nat @t76) @t75))))))) % 0.47/0.88 (assume @p25 @t25) % 0.47/0.88 (assume @p26 (=> @t25 @t4)) % 0.47/0.88 (assume @p27 (forall @t82 (=> @t81 (_ (_ tptp.ord_less_eq_set_nat @t20) (_ tptp.range_nat_nat @t79))))) % 0.47/0.88 (assume @p28 (forall @t82 (=> @t81 (_ (_ tptp.ord_less_eq_set_nat @t23) (_ tptp.domain_nat_nat @t79))))) % 0.47/0.88 (assume @p29 (forall (@list @t38 @t83) (=> @t44 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t40 (and (= @t84 (_ @t83 @t35)) @t39)))))))) % 0.47/0.88 (assume @p30 (forall (@list @t38 @t86) (=> @t44 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t40 (and (= @t87 (_ @t86 @t35)) @t39)))))))) % 0.47/0.88 (assume @p31 (forall (@list @t49 @t89) (=> @t55 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t51 (and (= @t84 (_ @t89 @t46)) @t50)))))))) % 0.47/0.88 (assume @p32 (forall (@list @t49 @t90) (=> @t55 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t51 (and (= @t87 (_ @t90 @t46)) @t50)))))))) % 0.47/0.88 (assume @p33 (forall (@list @t38 @t36 @t92) (=> @t44 (=> @t42 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t93 (and (= @t84 (_ (_ @t92 @t35) @t57)) @t39 @t91))))))))) % 0.47/0.88 (assume @p34 (forall (@list @t38 @t36 @t94) (=> @t44 (=> @t42 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t93 (and (= @t87 (_ (_ @t94 @t35) @t57)) @t39 @t91))))))))) % 0.47/0.88 (assume @p35 (forall (@list @t38 @t47 @t96) (=> @t44 (=> @t53 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t97 (and (= @t84 (_ (_ @t96 @t35) @t64)) @t39 @t95))))))))) % 0.47/0.88 (assume @p36 (forall (@list @t38 @t47 @t98) (=> @t44 (=> @t53 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t97 (and (= @t87 (_ (_ @t98 @t35) @t64)) @t39 @t95))))))))) % 0.47/0.88 (assume @p37 (forall (@list @t49 @t36 @t99) (=> @t55 (=> @t42 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t100 (and (= @t84 (_ (_ @t99 @t46) @t57)) @t50 @t91))))))))) % 0.47/0.88 (assume @p38 (forall (@list @t49 @t36 @t101) (=> @t55 (=> @t42 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t100 (and (= @t87 (_ (_ @t101 @t46) @t57)) @t50 @t91))))))))) % 0.47/0.88 (assume @p39 (forall (@list @t49 @t47 @t102) (=> @t55 (=> @t53 (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t85 (exists @t103 (and (= @t84 (_ (_ @t102 @t46) @t64)) @t50 @t95))))))))) % 0.47/0.88 (assume @p40 (forall (@list @t49 @t47 @t104) (=> @t55 (=> @t53 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t88 (exists @t103 (and (= @t87 (_ (_ @t104 @t46) @t64)) @t50 @t95))))))))) % 0.47/0.88 (assume @p41 (forall (@list @t38) (=> (not @t44) (exists (@list @t105) (_ @t38 @t105))))) % 0.47/0.88 (assume @p42 (forall (@list @t49) (=> (not @t55) (exists (@list @t106) (_ @t49 @t106))))) % 0.47/0.88 (assume @p43 (forall (@list @t71 @t112 @t109) (=> @t121 (=> @t120 (=> (forall @t115 (=> @t119 (exists @t118 (and @t117 (_ (_ @t109 @t107) @t116))))) (exists @t115 (and @t114 (not (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t111 (and @t110 (_ (_ @t109 @t108) @t107))))))))))))) % 0.47/0.88 (assume @p44 (forall (@list @t71 @t124 @t123) (=> @t121 (=> @t132 (=> (forall @t115 (=> @t119 (exists @t131 (and @t130 (_ (_ @t123 @t107) @t128))))) (exists @t127 (and @t126 (not (_ tptp.finite772653738at_nat (_ tptp.collec7649004at_nat (lambda @t111 (and @t110 (_ (_ @t123 @t108) @t122))))))))))))) % 0.47/0.88 (assume @p45 (forall (@list @t75 @t112 @t134) (=> @t138 (=> @t120 (=> (forall @t127 (=> @t137 (exists @t118 (and @t117 (_ (_ @t134 @t122) @t116))))) (exists @t115 (and @t114 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t136 (and @t135 (_ (_ @t134 @t133) @t107))))))))))))) % 0.47/0.88 (assume @p46 (forall (@list @t75 @t124 @t139) (=> @t138 (=> @t132 (=> (forall @t127 (=> @t137 (exists @t131 (and @t130 (_ (_ @t139 @t122) @t128))))) (exists @t127 (and @t126 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t136 (and @t135 (_ (_ @t139 @t133) @t122))))))))))))) % 0.47/0.88 (assume @p47 (= tptp.edmond1517640972ysis_a tptp.finite_Graph_a)) % 0.47/0.88 (assume @p48 (forall @t143 (=> @t142 @t141))) % 0.47/0.88 (assume @p49 (forall @t143 (=> @t141 @t142))) % 0.47/0.88 (assume @p50 (forall @t156 (=> @t155 (=> @t154 (exists @t153 (and @t152 (_ @t151 @t150) (forall @t149 (=> @t148 (=> (_ (_ tptp.ord_le841296385at_nat @t144) @t145) @t146))))))))) % 0.47/0.88 (assume @p51 (forall @t169 (=> @t168 (=> @t167 (exists @t166 (and @t165 (_ @t164 @t163) (forall @t162 (=> @t161 (=> (_ (_ tptp.ord_less_eq_set_nat @t157) @t158) @t159))))))))) % 0.47/0.88 (assume @p52 (forall @t176 (=> @t77 (=> @t175 (exists @t127 (and @t137 (_ @t173 @t172) (forall @t131 (=> @t171 (=> (_ (_ tptp.ord_less_eq_nat @t128) @t122) @t170))))))))) % 0.47/0.88 (assume @p53 (forall @t156 (=> @t155 (=> @t154 (exists @t153 (and @t152 (_ @t177 @t145) (forall @t149 (=> @t148 (=> (_ @t151 @t144) @t146))))))))) % 0.47/0.88 (assume @p54 (forall @t169 (=> @t168 (=> @t167 (exists @t166 (and @t165 (_ @t178 @t158) (forall @t162 (=> @t161 (=> (_ @t164 @t157) @t159))))))))) % 0.47/0.88 (assume @p55 (forall @t176 (=> @t77 (=> @t175 (exists @t127 (and @t137 (_ @t179 @t122) (forall @t131 (=> @t171 (=> (_ @t173 @t128) @t170))))))))) % 0.47/0.88 (assume @p56 (forall (@list @t112 @t71) (=> @t120 (=> @t181 @t73)))) % 0.47/0.88 (assume @p57 (forall (@list @t124 @t75) (=> @t132 (=> @t183 @t77)))) % 0.47/0.88 (assume @p58 (forall (@list @t185 @t184) (=> (_ @t186 @t184) (=> (not (_ tptp.finite772653738at_nat @t185)) (not (_ tptp.finite772653738at_nat @t184)))))) % 0.47/0.88 (assume @p59 (forall (@list @t188 @t187) (=> (_ (_ tptp.ord_less_eq_set_nat @t188) @t187) (=> (not (_ tptp.finite_finite_nat @t188)) (not (_ tptp.finite_finite_nat @t187)))))) % 0.47/0.88 (assume @p60 (forall @t189 (=> @t181 (=> @t120 @t73)))) % 0.47/0.88 (assume @p61 (forall @t190 (=> @t183 (=> @t132 @t77)))) % 0.47/0.88 (assume @p62 (forall (@list @t140 @t193 @t192) (=> @t141 (_ (_ tptp.ord_le841296385at_nat (_ (_ (_ tptp.edmond475474835dges_a @t140) @t193) @t192)) @t191)))) % 0.47/0.88 (assume @p63 (forall @t197 (_ (_ tptp.ord_le841296385at_nat @t196) @t3))) % 0.47/0.88 (assume @p64 (forall @t197 (_ (_ tptp.ord_le841296385at_nat @t199) @t3))) % 0.47/0.88 (assume @p65 (forall @t201 (= (_ @t200 @t26) (_ tptp.collect_nat @t29)))) % 0.47/0.88 (assume @p66 (forall (@list @t202) (_ tptp.finite772653738at_nat @t203))) % 0.47/0.88 (assume @p67 (forall (@list @t204) (_ tptp.finite_finite_nat @t205))) % 0.47/0.88 (assume @p68 (forall @t143 (=> @t208 @t207))) % 0.47/0.88 (assume @p69 (forall @t143 (=> @t207 @t208))) % 0.47/0.88 (assume @p70 (forall (@list @t209 @t38) (= (_ @t210 @t43) (_ @t38 @t209)))) % 0.47/0.88 (assume @p71 (forall (@list @t172 @t49) (= (_ @t174 @t54) @t211))) % 0.47/0.88 (assume @p72 (forall @t74 (= (_ tptp.collec7649004at_nat (lambda @t40 (_ @t212 @t71))) @t71))) % 0.47/0.88 (assume @p73 (forall @t78 (= (_ tptp.collect_nat (lambda @t51 @t214)) @t75))) % 0.47/0.88 (assume @p74 (forall @t45 (=> (forall @t115 (= (_ @t38 @t107) (_ @t36 @t107))) (= @t43 @t41)))) % 0.47/0.88 (assume @p75 (forall @t56 (=> (forall @t127 (= (_ @t49 @t122) (_ @t47 @t122))) (= @t54 @t52)))) % 0.47/0.88 (assume @p76 (forall @t220 (=> @t219 (=> @t218 (_ (_ @t8 @t193) @t26))))) % 0.47/0.88 (assume @p77 (forall @t220 (=> @t219 (=> @t218 @t30)))) % 0.47/0.88 (assume @p78 (forall @t220 (=> @t219 (=> @t218 (_ @t9 @t192))))) % 0.47/0.88 (assume @p79 (forall @t201 (_ (_ tptp.ord_le841296385at_nat @t222) @t3))) % 0.47/0.88 (assume @p80 (forall @t225 (=> (_ @t224 @t24) (_ (_ tptp.ord_less_eq_set_nat @t223) @t24)))) % 0.47/0.88 (assume @p81 (forall (@list @t26 @t7 @t226) (=> @t30 (=> (_ @t228 @t3) (_ @t29 @t226))))) % 0.47/0.88 (assume @p82 (forall (@list @t26 @t193 @t7) (=> (_ @t27 @t223) (=> (_ @t217 @t3) (_ @t28 @t223))))) % 0.47/0.88 (assume @p83 (= @t24 (_ tptp.collect_nat (lambda @t239 (exists @t238 (or @t237 @t233)))))) % 0.47/0.88 (assume @p84 (forall @t10 (= (_ @t221 @t7) (_ tptp.collec7649004at_nat (lambda @t85 (exists @t239 (and (= @t84 @t240) (_ (_ tptp.member701585322at_nat @t240) @t3)))))))) % 0.47/0.88 (assume @p85 (forall @t248 (= (_ @t198 @t241) (_ tptp.collec7649004at_nat (lambda @t85 (exists @t247 (and @t246 @t245 @t243 @t233))))))) % 0.47/0.88 (assume @p86 (forall @t248 (= (_ @t195 @t241) (_ tptp.collec7649004at_nat (lambda @t85 (exists @t247 (and @t249 @t245 @t243 @t237))))))) % 0.47/0.88 (assume @p87 (forall (@list @t250) (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda (@list @t251) (_ (_ tptp.ord_less_eq_nat @t251) @t250)))))) % 0.47/0.88 (assume @p88 (forall @t201 (=> @t25 (_ tptp.finite772653738at_nat @t222)))) % 0.47/0.88 (assume @p89 (forall @t197 (=> @t25 (_ tptp.finite772653738at_nat @t199)))) % 0.47/0.88 (assume @p90 (forall @t197 (=> @t25 (_ tptp.finite772653738at_nat @t196)))) % 0.47/0.88 (assume @p91 (forall @t201 (_ (_ tptp.ord_less_eq_set_nat @t252) @t24))) % 0.47/0.88 (assume @p92 (forall (@list @t193 @t140) (=> (_ @t224 @t206) (_ (_ tptp.ord_less_eq_set_nat @t253) @t206)))) % 0.47/0.88 (assume @p93 (forall (@list @t26 @t140 @t193 @t7) (=> (_ @t27 @t253) (=> (_ @t217 @t191) (_ @t28 @t253))))) % 0.47/0.88 (assume @p94 (= tptp.reachableNodes_a tptp.reachableNodes_a)) % 0.47/0.88 (assume @p95 (= tptp.outgoing_a2 tptp.outgoing_a2)) % 0.47/0.88 (assume @p96 (= tptp.incoming_a2 tptp.incoming_a2)) % 0.47/0.88 (assume @p97 (= tptp.incoming_a tptp.incoming_a)) % 0.47/0.88 (assume @p98 (forall @t259 (= (= @t258 @t257) (= @t254 @t185)))) % 0.47/0.88 (assume @p99 (forall @t259 (= (_ (_ tptp.ord_le1578155910_nat_o @t258) @t257) @t260))) % 0.47/0.88 (assume @p100 (forall @t82 (=> (forall @t265 (=> (_ @t264 @t19) (_ @t264 @t79))) @t81))) % 0.47/0.88 (assume @p101 (forall @t276 (=> (_ @t275 @t23) (=> (forall @t274 (=> @t273 (_ @t49 @t268))) @t267)))) % 0.47/0.88 (assume @p102 (forall @t283 (=> @t282 @t277))) % 0.47/0.88 (assume @p103 (forall @t288 (= @t277 (exists @t287 (and (= @t172 @t133) @t286))))) % 0.47/0.88 (assume @p104 (forall @t288 (=> @t277 (not (forall @t289 (not (_ (_ tptp.member701585322at_nat (_ @t279 @t269)) @t19))))))) % 0.47/0.88 (assume @p105 (forall @t288 (= @t277 (exists @t68 (_ (_ tptp.member701585322at_nat (_ @t279 @t64)) @t19))))) % 0.47/0.88 (assume @p106 (forall @t276 (=> (_ @t275 @t20) (=> (forall @t274 (=> @t273 (_ @t49 @t269))) @t267)))) % 0.47/0.88 (assume @p107 (forall @t283 (=> @t282 @t291))) % 0.47/0.88 (assume @p108 (forall @t288 (= @t292 (exists @t287 (and (= @t172 @t284) @t286))))) % 0.47/0.88 (assume @p109 (forall @t288 (=> @t292 (not (forall @t293 (not (_ (_ tptp.member701585322at_nat (_ @t270 @t172)) @t19))))))) % 0.47/0.88 (assume @p110 (forall @t288 (= @t292 (exists @t68 (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t64) @t172)) @t19))))) % 0.47/0.88 (assume @p111 (forall (@list @t278 @t19) (=> @t291 (not (forall @t293 (not (_ (_ tptp.member701585322at_nat (_ @t270 @t278)) @t19))))))) % 0.47/0.88 (assume @p112 (forall @t259 (= (_ (_ tptp.ord_le1039616028_nat_o (lambda @t40 (_ @t212 @t254))) (lambda @t40 (_ @t212 @t185))) @t260))) % 0.47/0.88 (assume @p113 (forall (@list @t294 @t188) (= (_ (_ tptp.ord_less_eq_nat_o (lambda @t51 (_ @t213 @t294))) (lambda @t51 (_ @t213 @t188))) (_ (_ tptp.ord_less_eq_set_nat @t294) @t188)))) % 0.47/0.88 (assume @p114 (forall (@list @t140 @t26 @t7 @t226) (=> @t297 (=> (_ @t228 @t191) (_ @t296 @t226))))) % 0.47/0.88 (assume @p115 (forall @t299 (_ (_ tptp.ord_le841296385at_nat @t298) @t191))) % 0.47/0.88 (assume @p116 (forall @t302 (=> @t301 (=> @t218 (_ (_ @t295 @t193) @t26))))) % 0.47/0.88 (assume @p117 (forall @t302 (=> @t301 (=> @t218 @t297)))) % 0.47/0.88 (assume @p118 (forall @t302 (=> @t301 (=> @t218 (_ @t303 @t192))))) % 0.47/0.88 (assume @p119 (forall @t305 (_ (_ tptp.ord_le841296385at_nat @t304) @t191))) % 0.47/0.88 (assume @p120 (forall @t305 (_ (_ tptp.ord_le841296385at_nat @t306) @t191))) % 0.47/0.88 (assume @p121 (forall @t299 (=> @t207 (_ tptp.finite772653738at_nat @t298)))) % 0.47/0.88 (assume @p122 (= tptp.e_a tptp.e_a)) % 0.47/0.88 (assume @p123 (= tptp.v_a tptp.v_a)) % 0.47/0.88 (assume @p124 (forall (@list @t140 @t7) (_ @t303 @t7))) % 0.47/0.88 (assume @p125 (= tptp.connected_a tptp.connected_a)) % 0.47/0.88 (assume @p126 (forall @t305 (=> @t207 (_ tptp.finite772653738at_nat @t304)))) % 0.47/0.88 (assume @p127 (= tptp.isShortestPath_a tptp.isShortestPath_a)) % 0.47/0.88 (assume @p128 (forall @t305 (=> @t207 (_ tptp.finite772653738at_nat @t306)))) % 0.47/0.88 (assume @p129 (forall @t74 (=> @t73 (exists (@list @t307) (= (_ tptp.set_Pr2131844118at_nat @t307) @t71))))) % 0.47/0.88 (assume @p130 (forall @t78 (=> @t77 (exists (@list @t308) (= (_ tptp.set_nat2 @t308) @t75))))) % 0.47/0.88 (assume @p131 (forall (@list @t202 @t112) (= (_ (_ tptp.ord_le841296385at_nat @t203) @t112) (forall @t40 (=> (_ @t212 @t203) (_ @t212 @t112)))))) % 0.47/0.88 (assume @p132 (forall (@list @t204 @t124) (= (_ (_ tptp.ord_less_eq_set_nat @t205) @t124) (forall @t51 (=> (_ @t213 @t205) (_ @t213 @t124)))))) % 0.47/0.88 (assume @p133 (forall @t309 (=> @t297 (= (_ @t28 @t206) (_ @t27 @t206))))) % 0.47/0.88 (assume @p134 (forall @t309 (=> @t297 (not (forall @t34 (not (_ (_ (_ @t300 @t26) @t32) @t7))))))) % 0.47/0.88 (assume @p135 (forall @t143 (=> @t142 @t207))) % 0.47/0.88 (assume @p136 (forall @t143 (=> @t207 @t142))) % 0.47/0.88 (assume @p137 (forall @t143 (=> @t142 @t208))) % 0.47/0.88 (assume @p138 (forall @t143 (=> @t208 @t142))) % 0.47/0.88 (assume @p139 (forall @t10 (= (_ @t311 @t7) (_ tptp.collec7649004at_nat (lambda @t85 (exists @t239 (and (= @t84 @t310) (_ (_ tptp.member701585322at_nat @t310) @t3)))))))) % 0.47/0.88 (assume @p140 (forall @t201 (_ (_ tptp.ord_le841296385at_nat @t312) @t3))) % 0.47/0.88 (assume @p141 (_ (_ tptp.ord_le841296385at_nat @t3) (_ (_ tptp.produc45129834at_nat @t24) (lambda @t88 @t24)))) % 0.47/0.88 (assume @p142 (forall @t31 (= @t30 @t313))) % 0.47/0.88 (assume @p143 (forall (@list @t26 @t215 @t7 @t314) (=> @t318 @t316))) % 0.47/0.88 (assume @p144 (forall (@list @t26 @t215 @t7 @t314 @t319 @t320) (=> @t318 @t322))) % 0.47/0.88 (assume @p145 (forall (@list @t26 @t215 @t7 @t314 @t319 @t323) (=> @t318 @t324))) % 0.47/0.88 (assume @p146 (forall @t225 (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_nat_nat @t3) @t223)) @t223))) % 0.47/0.88 (assume @p147 (forall @t327 (=> @t219 @t326))) % 0.47/0.88 (assume @p148 (forall @t337 (=> @t336 (=> @t334 @t333)))) % 0.47/0.88 (assume @p149 (forall (@list @t209 @t278 @t338 @t71) (=> @t342 (=> @t334 @t340)))) % 0.47/0.88 (assume @p150 (forall (@list @t172 @t331 @t343 @t75) (=> @t347 (=> @t175 @t345)))) % 0.47/0.88 (assume @p151 (forall @t351 (=> @t282 (=> @t175 @t350)))) % 0.47/0.88 (assume @p152 (forall (@list @t71 @t352) (=> @t73 (=> (forall @t357 (=> @t356 (_ tptp.finite772653738at_nat (_ @t352 @t355)))) (_ tptp.finite48957584at_nat @t354))))) % 0.47/0.88 (assume @p153 (forall (@list @t71 @t358) (=> @t73 (=> (forall @t357 (=> @t356 (_ tptp.finite_finite_nat (_ @t358 @t355)))) (_ tptp.finite2000257047at_nat @t360))))) % 0.47/0.88 (assume @p154 (forall (@list @t75 @t361) (=> @t77 (=> (forall @t293 (=> @t364 (_ tptp.finite772653738at_nat (_ @t361 @t268)))) (_ tptp.finite277291581at_nat @t363))))) % 0.47/0.88 (assume @p155 (forall (@list @t75 @t365) (=> @t77 (=> (forall @t293 (=> @t364 (_ tptp.finite_finite_nat (_ @t365 @t268)))) (_ tptp.finite772653738at_nat @t367))))) % 0.47/0.88 (assume @p156 (forall @t201 (_ tptp.finite_finite_nat @t252))) % 0.47/0.88 (assume @p157 (forall @t201 (=> @t25 (_ tptp.finite772653738at_nat @t312)))) % 0.47/0.88 (assume @p158 (= tptp.adjacent_nodes_a tptp.adjacent_nodes_a)) % 0.47/0.88 (assume @p159 (= tptp.isSimplePath_a tptp.isSimplePath_a)) % 0.47/0.88 (assume @p160 (= tptp.outgoing_a tptp.outgoing_a)) % 0.47/0.88 (assume @p161 (forall (@list @t209 @t71 @t331 @t328) (=> @t334 (=> @t336 @t333)))) % 0.47/0.88 (assume @p162 (forall (@list @t209 @t71 @t278 @t338) (=> @t334 (=> @t342 @t340)))) % 0.47/0.88 (assume @p163 (forall (@list @t172 @t75 @t331 @t343) (=> @t175 (=> @t347 @t345)))) % 0.47/0.88 (assume @p164 (forall (@list @t172 @t75 @t278 @t19) (=> @t175 (=> @t282 @t350)))) % 0.47/0.88 (assume @p165 (forall @t368 (= @t350 (exists @t51 (and @t214 (_ (_ tptp.member701585322at_nat (_ @t255 @t278)) @t19)))))) % 0.47/0.88 (assume @p166 (forall (@list @t331 @t328 @t71) (=> @t333 (not (forall @t115 (=> (_ (_ tptp.member2027625872at_nat (_ @t370 @t331)) @t328) @t369)))))) % 0.47/0.88 (assume @p167 (forall (@list @t331 @t343 @t75) (=> @t345 (not (forall @t127 (=> (_ (_ tptp.member1293241661at_nat (_ @t372 @t331)) @t343) @t371)))))) % 0.47/0.88 (assume @p168 (forall (@list @t278 @t338 @t71) (=> @t340 (not (forall @t115 (=> (_ (_ tptp.member868723479at_nat (_ @t373 @t278)) @t338) @t369)))))) % 0.47/0.88 (assume @p169 (forall @t368 (=> @t350 (not (forall @t127 (=> (_ (_ tptp.member701585322at_nat (_ @t262 @t278)) @t19) @t371)))))) % 0.47/0.88 (assume @p170 (forall (@list @t19 @t75 @t124 @t374) (=> (_ @t80 @t375) (_ (_ tptp.ord_less_eq_set_nat (_ @t348 @t374)) @t124)))) % 0.47/0.88 (assume @p171 (forall (@list @t140 @t193 @t215 @t192) (=> @t301 @t377))) % 0.47/0.88 (assume @p172 (forall (@list @t379 @t328 @t378 @t71) (=> (_ (_ tptp.ord_le465611495at_nat @t379) @t328) (=> @t380 (_ (_ tptp.ord_le841296385at_nat (_ (_ tptp.image_1655366419at_nat @t379) @t378)) @t330))))) % 0.47/0.88 (assume @p173 (forall (@list @t381 @t338 @t378 @t71) (=> (_ (_ tptp.ord_le1837363350at_nat @t381) @t338) (=> @t380 (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_2142699582at_nat @t381) @t378)) @t339))))) % 0.47/0.88 (assume @p174 (forall (@list @t383 @t343 @t382 @t75) (=> (_ (_ tptp.ord_le148299708at_nat @t383) @t343) (=> @t384 (_ (_ tptp.ord_le841296385at_nat (_ (_ tptp.image_981520924at_nat @t383) @t382)) @t344))))) % 0.47/0.88 (assume @p175 (forall (@list @t385 @t19 @t382 @t75) (=> (_ (_ tptp.ord_le841296385at_nat @t385) @t19) (=> @t384 (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_nat_nat @t385) @t382)) @t349))))) % 0.47/0.88 (assume @p176 (forall @t387 (=> @t386 (_ tptp.finite_finite_nat (_ (_ tptp.image_nat_nat @t254) @t75))))) % 0.47/0.88 (assume @p177 (forall (@list @t140 @t193) (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_nat_nat @t191) @t253)) @t253))) % 0.47/0.88 (assume @p178 (forall @t189 (=> @t73 (=> @t120 @t388)))) % 0.47/0.88 (assume @p179 (forall @t390 (=> @t73 (=> @t132 @t389)))) % 0.47/0.88 (assume @p180 (forall @t392 (=> @t77 (=> @t120 @t391)))) % 0.47/0.88 (assume @p181 (forall @t190 (=> @t77 (=> @t132 @t393)))) % 0.47/0.88 (assume @p182 (forall (@list @t140 @t26 @t215 @t7 @t314 @t319 @t323) (=> @t394 @t324))) % 0.47/0.88 (assume @p183 (forall (@list @t140 @t26 @t215 @t7 @t314 @t319 @t320) (=> @t394 @t322))) % 0.47/0.88 (assume @p184 (forall (@list @t140 @t26 @t215 @t7 @t314) (=> @t394 @t316))) % 0.47/0.88 (assume @p185 (forall @t299 (_ (_ tptp.ord_less_eq_set_nat @t395) @t206))) % 0.47/0.88 (assume @p186 (forall @t299 (_ (_ tptp.ord_le841296385at_nat @t396) @t191))) % 0.47/0.88 (assume @p187 (forall @t143 (_ (_ tptp.ord_le841296385at_nat @t191) (_ (_ tptp.produc45129834at_nat @t206) (lambda @t88 @t206))))) % 0.47/0.88 (assume @p188 (forall @t299 (=> @t207 (_ tptp.finite772653738at_nat @t396)))) % 0.47/0.88 (assume @p189 (forall @t299 (=> @t142 (_ tptp.finite_finite_nat @t395)))) % 0.47/0.88 (assume @p190 (forall (@list @t193 @t215 @t192 @t397) (=> @t326 @t400))) % 0.47/0.88 (assume @p191 (forall @t403 (= @t402 (and @t334 @t401)))) % 0.47/0.88 (assume @p192 (forall @t406 (= @t405 (and @t334 @t404)))) % 0.47/0.88 (assume @p193 (forall @t409 (= @t408 (and @t175 @t407)))) % 0.47/0.88 (assume @p194 (forall @t412 (= @t411 (and @t175 @t410)))) % 0.47/0.88 (assume @p195 (forall (@list @t209 @t71 @t331 @t352) (=> @t334 (=> @t401 @t402)))) % 0.47/0.88 (assume @p196 (forall (@list @t209 @t71 @t278 @t358) (=> @t334 (=> @t404 @t405)))) % 0.47/0.88 (assume @p197 (forall (@list @t172 @t75 @t331 @t361) (=> @t175 (=> @t407 @t408)))) % 0.47/0.88 (assume @p198 (forall (@list @t172 @t75 @t278 @t365) (=> @t175 (=> @t410 @t411)))) % 0.47/0.88 (assume @p199 (forall @t337 (=> (_ @t335 @t413) (=> (_ (_ tptp.ord_le465611495at_nat @t328) (_ @t353 (lambda @t85 @t71))) (or (= @t209 @t331) @t334))))) % 0.47/0.88 (assume @p200 (forall @t351 (=> @t416 (=> (_ @t80 (_ @t366 (lambda @t88 @t75))) (or @t414 @t175))))) % 0.47/0.88 (assume @p201 (forall @t422 (= @t421 (and @t420 @t418)))) % 0.47/0.88 (assume @p202 (forall (@list @t426 @t424 @t425 @t423) (= (= @t427 (_ (_ tptp.product_Pair_nat_nat @t425) @t423)) (and (= @t426 @t425) (= @t424 @t423))))) % 0.47/0.88 (assume @p203 (forall (@list @t428 @t19) (=> (_ @t429 @t19) (_ @t429 @t415)))) % 0.47/0.88 (assume @p204 (forall @t22 (= (_ tptp.transi1645084429cl_nat @t415) @t415))) % 0.47/0.88 (assume @p205 (forall @t430 (= (_ tptp.product_swap_nat_nat (_ tptp.product_swap_nat_nat @t428)) @t428))) % 0.47/0.88 (assume @p206 (forall @t435 (= (_ tptp.product_swap_nat_nat @t434) (_ @t432 @t266)))) % 0.47/0.88 (assume @p207 (forall @t455 (=> @t454 (=> @t452 (=> (forall @t451 (=> @t450 (=> (_ (_ tptp.member2027625872at_nat (_ (_ tptp.produc1168807639at_nat @t448) @t447)) @t413) (=> @t444 @t441)))) @t439))))) % 0.47/0.88 (assume @p208 (forall (@list @t460 @t459 @t457 @t456 @t328) (=> (_ (_ tptp.member2027625872at_nat (_ @t462 @t458)) @t413) (=> (not (= @t461 @t458)) (not (forall @t274 (=> (_ (_ tptp.member2027625872at_nat (_ @t462 @t271)) @t328) (not (_ (_ tptp.member2027625872at_nat (_ @t449 @t458)) @t413))))))))) % 0.47/0.88 (assume @p209 (forall @t455 (=> @t454 (=> @t439 (=> (forall @t451 (=> (_ (_ tptp.member2027625872at_nat (_ @t453 @t271)) @t413) (=> @t450 (=> @t441 @t444)))) @t452))))) % 0.47/0.88 (assume @p210 (forall (@list @t38 @t463) (=> @t464 (_ @t38 @t463)))) % 0.47/0.88 (assume @p211 (forall (@list @t465) (not (forall @t274 (not (= @t465 @t271)))))) % 0.47/0.88 (assume @p212 (forall @t422 (=> @t421 (not (=> @t420 (not @t418)))))) % 0.47/0.88 (assume @p213 (forall (@list @t38 @t428) (=> @t464 (_ @t38 @t428)))) % 0.47/0.88 (assume @p214 (forall @t430 (exists @t265 (= @t428 @t263)))) % 0.47/0.88 (assume @p215 (forall (@list @t140 @t193 @t215 @t192 @t397) (=> @t377 @t400))) % 0.47/0.88 (assume @p216 (forall (@list @t75 @t124 @t468 @t466) (=> @t470 (=> (forall @t127 (=> @t126 (= (_ @t468 @t122) @t469))) (= (_ @t366 @t468) (_ @t467 @t466)))))) % 0.47/0.88 (assume @p217 (forall @t475 (=> @t474 (= (= @t473 @t472) @t470)))) % 0.47/0.88 (assume @p218 (forall (@list @t477 @t71 @t352) (=> (_ (_ tptp.member2027625872at_nat @t477) @t354) (not (forall @t115 (=> @t119 (forall @t480 (=> (_ @t479 @t478) (not (= @t477 (_ @t370 @t476))))))))))) % 0.47/0.88 (assume @p219 (forall (@list @t481 @t71 @t358) (=> (_ (_ tptp.member868723479at_nat @t481) @t360) (not (forall @t115 (=> @t119 (forall @t484 (=> (_ @t483 @t482) (not (= @t481 (_ @t373 @t261))))))))))) % 0.47/0.88 (assume @p220 (forall (@list @t485 @t75 @t361) (=> (_ (_ tptp.member1293241661at_nat @t485) @t363) (not (forall @t127 (=> @t137 (forall @t480 (=> (_ @t479 @t486) (not (= @t485 (_ @t372 @t476))))))))))) % 0.47/0.88 (assume @p221 (forall (@list @t487 @t75 @t365) (=> (_ (_ tptp.member701585322at_nat @t487) @t367) (not (forall @t127 (=> @t137 (forall @t484 (=> (_ @t483 @t488) (not (= @t487 @t263)))))))))) % 0.47/0.88 (assume @p222 (forall @t412 (=> @t411 @t175))) % 0.47/0.88 (assume @p223 (forall @t412 (=> @t411 @t410))) % 0.47/0.88 (assume @p224 (forall @t403 (=> @t402 (not (=> @t334 (not @t401)))))) % 0.47/0.88 (assume @p225 (forall @t406 (=> @t405 (not (=> @t334 (not @t404)))))) % 0.47/0.88 (assume @p226 (forall @t409 (=> @t408 (not (=> @t175 (not @t407)))))) % 0.47/0.88 (assume @p227 (forall @t412 (=> @t411 (not (=> @t175 (not @t410)))))) % 0.47/0.88 (assume @p228 (forall @t283 (=> @t416 (=> (not @t414) (not (forall @t484 (=> @t490 (not (_ (_ tptp.member701585322at_nat (_ @t489 @t278)) @t19))))))))) % 0.47/0.88 (assume @p229 (forall @t496 (=> @t495 (=> (not (= @t491 @t493)) (not (forall @t289 (=> (_ (_ tptp.member701585322at_nat (_ @t494 @t269)) @t415) (not (_ (_ tptp.member701585322at_nat (_ @t492 @t491)) @t19))))))))) % 0.47/0.88 (assume @p230 (forall @t496 (= @t495 (or (exists @t136 (and @t498 (= @t491 @t133))) (exists (@list @t133 @t284 @t497) (and @t498 (= @t491 @t497) (_ @t285 @t415) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t284) @t497)) @t19))))))) % 0.47/0.88 (assume @p231 (forall (@list @t266 @t431 @t19 @t499) (=> (_ @t501 @t415) (=> (_ (_ tptp.member701585322at_nat (_ @t432 @t499)) @t415) @t500)))) % 0.47/0.88 (assume @p232 (forall @t508 (=> @t416 (=> @t211 (=> (forall @t507 (=> @t490 (=> @t506 (=> @t505 @t504)))) @t502))))) % 0.47/0.88 (assume @p233 (forall (@list @t426 @t424 @t19 @t438) (=> (_ (_ tptp.member701585322at_nat @t427) @t415) (=> (forall @t293 (_ @t440 @t268)) (=> (forall (@list @t268 @t269 @t509) (=> (_ @t272 @t415) (=> @t441 (=> (_ (_ tptp.member701585322at_nat (_ @t492 @t509)) @t19) (_ @t440 @t509))))) (_ (_ @t438 @t426) @t424)))))) % 0.47/0.88 (assume @p234 (forall (@list @t266 @t499 @t19) (=> @t500 (=> (not (= @t266 @t499)) (not (forall @t484 (=> (_ (_ tptp.member701585322at_nat (_ @t433 @t261)) @t19) (not (_ (_ tptp.member701585322at_nat (_ @t489 @t499)) @t415))))))))) % 0.47/0.88 (assume @p235 (forall @t288 (_ (_ tptp.member701585322at_nat (_ @t279 @t172)) @t415))) % 0.47/0.88 (assume @p236 (forall @t508 (=> @t416 (=> @t502 (=> (forall @t507 (=> @t506 (=> (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t503) @t278)) @t415) (=> @t504 @t505)))) @t211))))) % 0.47/0.88 (assume @p237 (forall @t513 (=> @t416 (=> (_ @t512 @t19) @t511)))) % 0.47/0.88 (assume @p238 (forall @t513 (=> @t282 (=> (_ @t512 @t415) @t511)))) % 0.47/0.88 (assume @p239 (forall @t82 (=> @t81 @t515))) % 0.47/0.88 (assume @p240 (forall @t259 (=> @t260 (=> (_ @t186 @t516) (= (_ tptp.transi1645084429cl_nat @t185) @t516))))) % 0.47/0.88 (assume @p241 (forall @t82 (=> (_ @t80 @t514) @t515))) % 0.47/0.88 (assume @p242 (forall (@list @t71 @t518 @t352 @t517) (=> @t519 (=> (forall @t115 (=> @t119 (_ (_ tptp.ord_le841296385at_nat @t478) (_ @t517 @t107)))) (_ (_ tptp.ord_le465611495at_nat @t354) (_ (_ tptp.produc2056081288at_nat @t518) @t517)))))) % 0.47/0.88 (assume @p243 (forall (@list @t71 @t518 @t358 @t520) (=> @t519 (=> (forall @t115 (=> @t119 (_ (_ tptp.ord_less_eq_set_nat @t482) (_ @t520 @t107)))) (_ (_ tptp.ord_le1837363350at_nat @t360) (_ (_ tptp.produc2055342601at_nat @t518) @t520)))))) % 0.47/0.88 (assume @p244 (forall (@list @t75 @t374 @t361 @t521) (=> @t522 (=> (forall @t127 (=> @t137 (_ (_ tptp.ord_le841296385at_nat @t486) (_ @t521 @t122)))) (_ (_ tptp.ord_le148299708at_nat @t363) (_ (_ tptp.produc894163943at_nat @t374) @t521)))))) % 0.47/0.88 (assume @p245 (forall (@list @t75 @t374 @t365 @t466) (=> @t522 (=> (forall @t127 (=> @t137 (_ (_ tptp.ord_less_eq_set_nat @t488) @t469))) (_ (_ tptp.ord_le841296385at_nat @t367) (_ (_ tptp.produc45129834at_nat @t374) @t466)))))) % 0.47/0.88 (assume @p246 (forall (@list @t328 @t523) (=> (_ (_ tptp.ord_le841296385at_nat (_ @t329 @t523)) @t523) (= (_ (_ tptp.image_1655366419at_nat @t413) @t523) @t523)))) % 0.47/0.88 (assume @p247 (forall (@list @t19 @t524) (=> (_ (_ tptp.ord_less_eq_set_nat (_ @t348 @t524)) @t524) (= (_ (_ tptp.image_nat_nat @t415) @t524) @t524)))) % 0.47/0.88 (assume @p248 (forall (@list @t525 @t526 @t465) (=> (not (_ @t528 (_ tptp.domain37934156at_nat @t526))) (= (_ (_ tptp.member2027625872at_nat (_ (_ tptp.produc1168807639at_nat @t525) @t465)) @t527) (= @t525 @t465))))) % 0.47/0.88 (assume @p249 (forall (@list @t266 @t254 @t431) (=> (not (_ @t275 (_ tptp.domain_nat_nat @t254))) (= (_ @t501 @t516) @t529)))) % 0.47/0.88 (assume @p250 (forall (@list @t525 @t518 @t71 @t112) (=> @t531 (= (_ (_ tptp.ord_le465611495at_nat (_ @t353 @t530)) (_ (_ tptp.produc2056081288at_nat @t112) @t530)) @t181)))) % 0.47/0.88 (assume @p251 (forall (@list @t266 @t374 @t71 @t112) (=> @t474 (= (_ (_ tptp.ord_le1837363350at_nat (_ @t359 @t532)) (_ (_ tptp.produc2055342601at_nat @t112) @t532)) @t181)))) % 0.47/0.88 (assume @p252 (forall (@list @t525 @t518 @t75 @t124) (=> @t531 (= (_ (_ tptp.ord_le148299708at_nat (_ @t362 @t533)) (_ (_ tptp.produc894163943at_nat @t124) @t533)) @t183)))) % 0.47/0.88 (assume @p253 (forall @t475 (=> @t474 (= (_ (_ tptp.ord_le841296385at_nat @t473) @t472) @t183)))) % 0.47/0.88 (assume @p254 (forall (@list @t526 @t71) (=> (_ tptp.finite48957584at_nat @t526) (=> @t73 (_ tptp.finite772653738at_nat (_ (_ tptp.image_1655366419at_nat @t527) @t71)))))) % 0.47/0.88 (assume @p255 (forall @t387 (=> @t386 (=> @t77 (_ tptp.finite_finite_nat (_ (_ tptp.image_nat_nat @t516) @t75)))))) % 0.47/0.88 (assume @p256 (forall @t189 (=> @t121 (=> @t534 (not @t388))))) % 0.47/0.88 (assume @p257 (forall @t390 (=> @t121 (=> @t535 (not @t389))))) % 0.47/0.88 (assume @p258 (forall @t392 (=> @t138 (=> @t534 (not @t391))))) % 0.47/0.88 (assume @p259 (forall @t190 (=> @t138 (=> @t535 (not @t393))))) % 0.47/0.88 (assume @p260 (forall (@list @t536) (_ @t537 @t536))) % 0.47/0.88 (assume @p261 (forall (@list @t538) (_ @t539 @t538))) % 0.47/0.88 (assume @p262 (forall (@list @t266) (_ @t540 @t266))) % 0.47/0.88 (assume @p263 (forall @t552 (=> (_ @t177 @t551) @t550))) % 0.47/0.88 (assume @p264 (forall @t564 (=> (_ @t177 @t563) @t562))) % 0.47/0.88 (assume @p265 (forall @t572 (=> (_ @t177 @t571) @t570))) % 0.47/0.88 (assume @p266 (forall @t577 (=> (_ @t178 @t576) @t575))) % 0.47/0.88 (assume @p267 (forall @t582 (=> (_ @t178 @t581) @t580))) % 0.47/0.88 (assume @p268 (forall @t587 (=> (_ @t178 @t586) @t585))) % 0.47/0.88 (assume @p269 (forall @t592 (=> (_ @t179 @t591) @t590))) % 0.47/0.88 (assume @p270 (forall @t597 (=> (_ @t179 @t596) @t595))) % 0.47/0.88 (assume @p271 (forall @t601 (=> (_ @t179 @t600) @t599))) % 0.47/0.88 (assume @p272 (forall @t604 (=> @t603 (=> (_ (_ tptp.ord_le841296385at_nat @t551) @t541) @t602)))) % 0.47/0.88 (assume @p273 (forall @t606 (=> @t603 (=> (_ (_ tptp.ord_less_eq_set_nat @t576) @t553) @t605)))) % 0.47/0.88 (assume @p274 (forall @t608 (=> @t603 (=> (_ (_ tptp.ord_less_eq_nat @t591) @t510) @t607)))) % 0.47/0.88 (assume @p275 (forall @t611 (=> @t610 (=> (_ (_ tptp.ord_le841296385at_nat @t563) @t541) @t609)))) % 0.47/0.88 (assume @p276 (forall @t613 (=> @t610 (=> (_ (_ tptp.ord_less_eq_set_nat @t581) @t553) @t612)))) % 0.47/0.88 (assume @p277 (forall @t615 (=> @t610 (=> (_ (_ tptp.ord_less_eq_nat @t596) @t510) @t614)))) % 0.47/0.88 (assume @p278 (forall @t618 (=> @t617 (=> (_ (_ tptp.ord_le841296385at_nat @t571) @t541) @t616)))) % 0.47/0.88 (assume @p279 (forall @t620 (=> @t617 (=> (_ (_ tptp.ord_less_eq_set_nat @t586) @t553) @t619)))) % 0.47/0.88 (assume @p280 (forall @t622 (=> @t617 (=> (_ (_ tptp.ord_less_eq_nat @t600) @t510) @t621)))) % 0.47/0.88 (assume @p281 (forall @t552 (=> (= @t150 @t551) @t550))) % 0.47/0.88 (assume @p282 (forall @t577 (=> (= @t163 @t576) @t575))) % 0.47/0.88 (assume @p283 (forall @t592 (=> (= @t172 @t591) @t590))) % 0.47/0.88 (assume @p284 (forall @t564 (=> (= @t150 @t563) @t562))) % 0.47/0.88 (assume @p285 (forall @t582 (=> (= @t163 @t581) @t580))) % 0.47/0.88 (assume @p286 (forall @t597 (=> (= @t172 @t596) @t595))) % 0.47/0.88 (assume @p287 (forall @t572 (=> (= @t150 @t571) @t570))) % 0.47/0.88 (assume @p288 (forall @t587 (=> (= @t163 @t586) @t585))) % 0.47/0.88 (assume @p289 (forall @t601 (=> (= @t172 @t600) @t599))) % 0.47/0.88 (assume @p290 (forall @t604 (=> @t603 (=> (= @t551 @t541) @t602)))) % 0.47/0.88 (assume @p291 (forall @t606 (=> @t603 (=> (= @t576 @t553) @t605)))) % 0.47/0.88 (assume @p292 (forall @t608 (=> @t603 (=> (= @t591 @t510) @t607)))) % 0.47/0.88 (assume @p293 (forall @t611 (=> @t610 (=> (= @t563 @t541) @t609)))) % 0.47/0.88 (assume @p294 (forall @t613 (=> @t610 (=> (= @t581 @t553) @t612)))) % 0.47/0.88 (assume @p295 (forall @t615 (=> @t610 (=> (= @t596 @t510) @t614)))) % 0.47/0.88 (assume @p296 (forall @t618 (=> @t617 (=> (= @t571 @t541) @t616)))) % 0.47/0.88 (assume @p297 (forall @t620 (=> @t617 (=> (= @t586 @t553) @t619)))) % 0.47/0.88 (assume @p298 (forall @t622 (=> @t617 (=> (= @t600 @t510) @t621)))) % 0.47/0.88 (assume @p299 (= @t627 (lambda (@list @t623 @t624) (and (_ (_ tptp.ord_le841296385at_nat @t623) @t624) (_ (_ tptp.ord_le841296385at_nat @t624) @t623))))) % 0.47/0.88 (assume @p300 (= @t632 (lambda (@list @t628 @t629) (and (_ (_ tptp.ord_less_eq_set_nat @t628) @t629) (_ (_ tptp.ord_less_eq_set_nat @t629) @t628))))) % 0.47/0.88 (assume @p301 (= @t635 (lambda @t103 (and (_ (_ tptp.ord_less_eq_nat @t46) @t64) (_ (_ tptp.ord_less_eq_nat @t64) @t46))))) % 0.47/0.88 (assume @p302 (forall @t641 (=> @t640 (=> @t639 @t637)))) % 0.47/0.88 (assume @p303 (forall @t647 (=> @t646 (=> @t645 @t643)))) % 0.47/0.88 (assume @p304 (forall @t435 (=> @t650 (=> @t649 @t529)))) % 0.47/0.88 (assume @p305 (forall @t435 (or @t650 @t649))) % 0.47/0.88 (assume @p306 (forall @t641 (=> @t637 @t640))) % 0.47/0.88 (assume @p307 (forall @t647 (=> @t643 @t646))) % 0.47/0.88 (assume @p308 (forall @t435 (=> @t529 @t650))) % 0.47/0.88 (assume @p309 (forall @t435 (=> @t651 @t649))) % 0.47/0.88 (assume @p310 (forall @t654 (=> @t603 @t653))) % 0.47/0.88 (assume @p311 (forall @t657 (=> @t610 @t656))) % 0.47/0.88 (assume @p312 (forall @t660 (=> @t617 @t659))) % 0.47/0.88 (assume @p313 (forall @t666 (=> (=> @t650 (not @t663)) (=> (=> @t649 (not @t665)) (=> (=> @t665 (not @t664)) (=> (=> @t664 (not @t649)) (=> (=> @t663 (not @t662)) (not (=> @t662 @t651))))))))) % 0.47/0.88 (assume @p314 (forall (@list @t636 @t536) (=> @t639 (= @t640 @t637)))) % 0.47/0.88 (assume @p315 (forall (@list @t642 @t538) (=> @t645 (= @t646 @t643)))) % 0.47/0.88 (assume @p316 (forall (@list @t431 @t266) (=> @t649 (= @t650 @t529)))) % 0.47/0.88 (assume @p317 (= @t627 (lambda (@list @t667 @t668) (and (_ (_ tptp.ord_le841296385at_nat @t667) @t668) (_ (_ tptp.ord_le841296385at_nat @t668) @t667))))) % 0.47/0.88 (assume @p318 (= @t632 (lambda (@list @t669 @t670) (and (_ (_ tptp.ord_less_eq_set_nat @t669) @t670) (_ (_ tptp.ord_less_eq_set_nat @t670) @t669))))) % 0.47/0.88 (assume @p319 (= @t635 (lambda @t287 (and (_ (_ tptp.ord_less_eq_nat @t133) @t284) (_ (_ tptp.ord_less_eq_nat @t284) @t133))))) % 0.47/0.88 (assume @p320 (forall @t654 (=> @t671 @t653))) % 0.47/0.88 (assume @p321 (forall @t657 (=> @t672 @t656))) % 0.47/0.88 (assume @p322 (forall @t660 (=> @t414 @t659))) % 0.47/0.88 (assume @p323 (forall @t654 (=> @t603 (=> (= @t547 @t541) @t652)))) % 0.47/0.88 (assume @p324 (forall @t657 (=> @t610 (=> (= @t559 @t553) @t655)))) % 0.47/0.88 (assume @p325 (forall @t660 (=> @t617 (=> (= @t278 @t510) @t658)))) % 0.47/0.88 (assume @p326 (forall (@list @t150 @t547) (=> @t603 (=> (_ @t548 @t150) @t671)))) % 0.47/0.88 (assume @p327 (forall (@list @t163 @t559) (=> @t610 (=> (_ @t560 @t163) @t672)))) % 0.47/0.88 (assume @p328 (forall (@list @t172 @t278) (=> @t617 (=> (_ @t568 @t172) @t414)))) % 0.47/0.88 (assume @p329 (forall (@list @t536 @t636 @t673) (=> @t640 (=> (_ @t638 @t673) (_ @t537 @t673))))) % 0.47/0.88 (assume @p330 (forall (@list @t538 @t642 @t674) (=> @t646 (=> (_ @t644 @t674) (_ @t539 @t674))))) % 0.47/0.88 (assume @p331 (forall @t666 (=> @t650 (=> @t663 @t665)))) % 0.47/0.88 (assume @p332 (forall (@list @t150) (_ @t177 @t150))) % 0.47/0.88 (assume @p333 (forall (@list @t163) (_ @t178 @t163))) % 0.47/0.88 (assume @p334 (forall (@list @t172) (_ @t179 @t172))) % 0.47/0.88 (assume @p335 (forall (@list @t438 @t172 @t278) (=> (forall @t274 (=> (_ (_ tptp.ord_less_eq_nat @t268) @t269) @t441)) (=> (forall @t274 (=> (_ (_ @t438 @t269) @t268) @t441)) (_ (_ @t438 @t172) @t278))))) % 0.47/0.88 (assume @p336 (forall @t31 (=> @t313 (exists @t34 (_ (_ @t676 @t32) @t7))))) % 0.47/0.88 (assume @p337 (forall @t327 (=> (_ (_ (_ @t675 @t193) @t215) @t192) (exists (@list @t677) (_ (_ @t325 @t677) @t192))))) % 0.47/0.88 (assume @p338 (forall @t31 (= @t30 (exists @t17 (_ (_ @t676 @t11) @t7))))) % 0.47/0.88 (assume @p339 (forall @t679 (=> (_ (_ @t33 @t215) @t7) @t678))) % 0.47/0.88 (assume @p340 (forall @t681 (=> @t678 (=> @t321 (=> (not (= @t314 @t26)) (exists (@list @t680) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t680) @t314)) @t216))))))) % 0.47/0.88 (assume @p341 (forall @t681 (=> @t678 (=> @t321 (=> (not (= @t319 @t7)) (exists (@list @t682) (_ (_ tptp.member701585322at_nat (_ (_ tptp.product_Pair_nat_nat @t319) @t682)) @t216))))))) % 0.47/0.88 (assume @p342 (forall (@list @t26 @t215 @t7 @t397) (=> @t678 (=> @t399 (_ @t398 @t3))))) % 0.47/0.88 (assume @p343 (forall @t679 (=> @t678 @t313))) % 0.47/0.88 (assume @p344 @t683) % 0.47/0.88 (assume @p345 true) % 0.47/0.88 (step @p346 (= tptp.edmond475474835dges_a @t692) :rule refl :args (@t692)) % 0.47/0.88 (step @p347 (= tptp.incoming_a @t696) :rule refl :args (@t696)) % 0.47/0.88 (step @p348 (= tptp.incoming_a2 @t701) :rule refl :args (@t701)) % 0.47/0.88 (step @p349 (= tptp.outgoing_a2 @t703) :rule refl :args (@t703)) % 0.47/0.88 (step @p350 (= tptp.v_a @t705) :rule refl :args (@t705)) % 0.47/0.88 (step @p351 (= tptp.reachableNodes_a @t706) :rule refl :args (@t706)) % 0.47/0.88 (step @p352 (= tptp.domain_nat_nat @t708) :rule refl :args (@t708)) % 0.47/0.88 (step @p353 (= tptp.finite_Graph_a @t709) :rule refl :args (@t709)) % 0.47/0.88 (step @p354 (= tptp.outgoing_a @t710) :rule refl :args (@t710)) % 0.47/0.88 (step @p355 (= tptp.connected_a @t711) :rule refl :args (@t711)) % 0.47/0.88 (step @p356 :rule beta-reduce :args ((= (_ @t715 tptp.t) (_ tptp.collec7649004at_nat (lambda @t18 (not (forall @t17 (or @t714 (not (tptp.isShortestPath_a tptp.c tptp.s @t11 tptp.t)))))))))) % 0.47/0.88 (step @p357 :rule refl :args (tptp.t)) % 0.47/0.88 (step @p358 :rule beta-reduce :args ((= (_ @t716 tptp.s) @t715))) % 0.47/0.88 (step @p359 :rule refl :args (tptp.s)) % 0.47/0.88 (step @p360 :rule beta-reduce :args ((= @t718 @t716))) % 0.47/0.88 (step @p361 :rule ho_cong :premises (@p360 @p359)) % 0.47/0.88 (step @p362 :rule trans :premises (@p361 @p358)) % 0.47/0.88 (step @p363 :rule ho_cong :premises (@p362 @p357)) % 0.47/0.88 (step @p364 :rule trans :premises (@p363 @p356)) % 0.47/0.88 (step @p365 :rule refl :args (tptp.finite772653738at_nat)) % 0.47/0.88 (step @p366 :rule ho_cong :premises (@p365 @p364)) % 0.47/0.88 (step @p367 :rule cong :premises (@p366) :args ((not @t719))) % 0.47/0.88 (step @p368 :rule refl :args (tptp.c)) % 0.47/0.88 (step @p369 :rule refl :args (@t717)) % 0.47/0.88 (step @p370 :rule refl :args (@t687)) % 0.47/0.88 (step @p371 :rule cong :premises (@p370 @p369) :args ((= @t687 @t717))) % 0.47/0.88 (step @p372 :rule symm :premises (@p371)) % 0.47/0.88 (step @p373 :rule eq_resolve :premises (@p370 @p372)) % 0.47/0.88 (step @p374 :rule cong :premises (@p373) :args (@t720)) % 0.47/0.88 (step @p375 :rule refl :args ((tptp.member701585322at_nat @t14 @t13))) % 0.47/0.88 (step @p376 :rule refl :args (@t712)) % 0.47/0.88 (step @p377 :rule refl :args (@t14)) % 0.47/0.88 (step @p378 :rule cong :premises (@p377 @p376) :args (@t713)) % 0.47/0.88 (step @p379 :rule trans :premises (@p378 @p375)) % 0.47/0.88 (step @p380 :rule refl :args (@t15)) % 0.47/0.88 (step @p381 :rule ho_cong :premises (@p380 @p376)) % 0.47/0.88 (step @p382 :rule cong :premises (@p381 @p379) :args ((= (_ @t15 @t712) @t713))) % 0.47/0.88 (step @p383 :rule symm :premises (@p382)) % 0.47/0.88 (step @p384 :rule refl :args (@t16)) % 0.47/0.88 (step @p385 :rule eq_resolve :premises (@p384 @p383)) % 0.47/0.88 (step @p386 :rule refl :args (@t13)) % 0.47/0.88 (step @p387 :rule cong :premises (@p386 @p376) :args ((= @t13 @t712))) % 0.47/0.88 (step @p388 :rule symm :premises (@p387)) % 0.47/0.88 (step @p389 :rule eq_resolve :premises (@p386 @p388)) % 0.47/0.88 (step @p390 :rule ho_cong :premises (@p380 @p389)) % 0.47/0.88 (step @p391 :rule trans :premises (@p390 @p385)) % 0.47/0.88 (step @p392 :rule cong :premises (@p391) :args (@t721)) % 0.47/0.88 (step @p393 :rule nary_cong :premises (@p392 @p374) :args (@t722)) % 0.47/0.88 (step @p394 :rule cong :premises (@p393) :args ((forall @t17 @t722))) % 0.47/0.88 (step @p395 :rule bool-and-de-morgan :args (@t16 @t687 true)) % 0.47/0.88 (step @p396 :rule cong :premises (@p395) :args (@t723)) % 0.47/0.88 (step @p397 :rule trans :premises (@p396 @p394)) % 0.47/0.88 (step @p398 :rule cong :premises (@p397) :args (@t724)) % 0.47/0.88 (step @p399 :rule exists-elim :args ((= @t689 @t724))) % 0.47/0.88 (step @p400 :rule trans :premises (@p399 @p398)) % 0.47/0.88 (step @p401 :rule cong :premises (@p400) :args (@t690)) % 0.47/0.88 (step @p402 :rule refl :args (tptp.collec7649004at_nat)) % 0.47/0.88 (step @p403 :rule ho_cong :premises (@p402 @p401)) % 0.47/0.88 (step @p404 :rule cong :premises (@p403) :args (@t692)) % 0.47/0.88 (step @p405 :rule trans :premises (@p346 @p404)) % 0.47/0.88 (step @p406 :rule ho_cong :premises (@p405 @p368)) % 0.47/0.88 (step @p407 :rule ho_cong :premises (@p406 @p359)) % 0.47/0.88 (step @p408 :rule ho_cong :premises (@p407 @p357)) % 0.47/0.88 (step @p409 :rule ho_cong :premises (@p365 @p408)) % 0.47/0.88 (step @p410 :rule cong :premises (@p409) :args (@t683)) % 0.47/0.88 (step @p411 :rule trans :premises (@p410 @p367)) % 0.47/0.88 (step @p412 :rule eq_resolve :premises (@p344 @p411)) % 0.47/0.88 (step @p413 :rule refl :args (@t4)) % 0.47/0.88 (step @p414 :rule cong :premises (@p413 @p366) :args ((=> @t4 @t719))) % 0.47/0.88 (step @p415 :rule cong :premises (@p413 @p409) :args (@t5)) % 0.47/0.88 (step @p416 :rule trans :premises (@p415 @p414)) % 0.47/0.88 (step @p417 :rule eq_resolve :premises (@p2 @p416)) % 0.47/0.88 (step @p418 :rule implies_elim :premises (@p417)) % 0.47/0.88 (step @p419 :rule resolution :premises (@p418 @p4) :args (false @t4)) % 0.47/0.88 (step @p420 false :rule contra :premises (@p419 @p412)) % 0.47/0.88 ) % 0.47/0.88 % SZS output end Proof % 0.47/0.88 % cvc5 exiting %------------------------------------------------------------------------------