%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP139^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.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:25:10 AM UTC 2026 % Result : Theorem 0.46s 0.96s % Output : Proof 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP139^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n003.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 04:15:29 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.61 %----Proving TH0 % 0.46/0.96 --- 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.46/0.96 % SZS status Theorem % 0.46/0.96 % SZS output start Proof % 0.46/0.96 ( % 0.46/0.96 (declare-sort tptp.produc270694976lle_tv 0) % 0.46/0.96 (declare-sort tptp.produc194167194tv_nat 0) % 0.46/0.96 (declare-sort tptp.set_Pr13445366lle_tv 0) % 0.46/0.96 (declare-sort tptp.set_Pr1725653840tv_nat 0) % 0.46/0.96 (declare-sort tptp.nat 0) % 0.46/0.96 (declare-sort tptp.paraco1605129243lle_tv 0) % 0.46/0.96 (declare-sort tptp.produc1647334210lle_tv 0) % 0.46/0.96 (declare-sort tptp.product_prod_nat_nat 0) % 0.46/0.96 (declare-sort tptp.set_Pr2014382200lle_tv 0) % 0.46/0.96 (declare-sort tptp.set_Pr1986765409at_nat 0) % 0.46/0.96 (declare-sort tptp.set_Pa1764573435lle_tv 0) % 0.46/0.96 (declare-sort tptp.set_nat 0) % 0.46/0.96 (declare-sort tptp.set_set_nat 0) % 0.46/0.96 (declare-sort tptp.set_se800614875lle_tv 0) % 0.46/0.96 (declare-const tptp.top_top_o Bool) % 0.46/0.96 (declare-const tptp.member1531318361lle_tv (-> tptp.produc1647334210lle_tv tptp.set_Pr2014382200lle_tv Bool)) % 0.46/0.96 (declare-const tptp.member737151281tv_nat (-> tptp.produc194167194tv_nat tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.96 (declare-const tptp.member813679063lle_tv (-> tptp.produc270694976lle_tv tptp.set_Pr13445366lle_tv Bool)) % 0.46/0.96 (declare-const tptp.member701585322at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.96 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.46/0.96 (declare-const tptp.member266900804lle_tv (-> tptp.paraco1605129243lle_tv tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.96 (declare-const tptp.top_to975729152tv_nat tptp.set_Pr1725653840tv_nat) % 0.46/0.96 (declare-const tptp.top_to1411004326lle_tv tptp.set_Pr13445366lle_tv) % 0.46/0.96 (declare-const tptp.top_to1555900337at_nat tptp.set_Pr1986765409at_nat) % 0.46/0.96 (declare-const tptp.ord_less_nat (-> tptp.nat tptp.nat Bool)) % 0.46/0.96 (declare-const tptp.ord_less_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 0.46/0.96 (declare-const tptp.ord_le727057319lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.96 (declare-const tptp.member_set_nat (-> tptp.set_nat tptp.set_set_nat Bool)) % 0.46/0.96 (declare-const tptp.member1875402276lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_se800614875lle_tv Bool)) % 0.46/0.96 (declare-const tptp.image_53754658tv_nat (-> (-> tptp.produc270694976lle_tv tptp.produc194167194tv_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (declare-const tptp.produc1975500101lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.produc386540311at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.image_1200372424lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc270694976lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (declare-const tptp.produc51277375tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc1647334210lle_tv tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.image_1892891680lle_tv (-> (-> tptp.produc1647334210lle_tv tptp.produc270694976lle_tv) tptp.set_Pr2014382200lle_tv tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (declare-const tptp.produc1095080935lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc1647334210lle_tv tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.image_228488944lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc1647334210lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pr2014382200lle_tv)) % 0.46/0.96 (declare-const tptp.produc1521089895lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.image_1796815776tv_nat (-> (-> tptp.produc1647334210lle_tv tptp.produc194167194tv_nat) tptp.set_Pr2014382200lle_tv tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (declare-const tptp.produc1500159719tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc1647334210lle_tv tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool)) % 0.46/0.96 (declare-const tptp.produc505105722at_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.produc2101297531lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.produc72207551lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on1954136462at_nat (-> (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat) tptp.set_Pr13445366lle_tv Bool)) % 0.46/0.96 (declare-const tptp.the_in857469900at_nat (-> tptp.set_Pr13445366lle_tv (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat) tptp.product_prod_nat_nat tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.produc1345917071lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on1971554740at_nat (-> (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat) tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.96 (declare-const tptp.the_in874888178at_nat (-> tptp.set_Pr1725653840tv_nat (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat) tptp.product_prod_nat_nat tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.image_1787705850at_nat (-> (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (declare-const tptp.image_1805124128at_nat (-> (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat) tptp.set_Pr1725653840tv_nat tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (declare-const tptp.the_in667485224tv_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat) tptp.produc194167194tv_nat tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.order_769474267at_nat (-> (-> tptp.nat tptp.nat) Bool)) % 0.46/0.96 (declare-const tptp.image_815163717at_nat (-> (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat) tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (declare-const tptp.image_1674248956lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on1764151786tv_nat (-> (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat) tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.96 (declare-const tptp.image_1597721174tv_nat (-> (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat) tptp.set_Pr1986765409at_nat tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (declare-const tptp.image_1104296520tv_nat (-> (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat) tptp.set_Pr1725653840tv_nat tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (declare-const tptp.the_in195660058tv_nat (-> tptp.set_Pr1725653840tv_nat (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.inj_on1612474245lle_tv (-> (-> tptp.produc194167194tv_nat tptp.paraco1605129243lle_tv) tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.96 (declare-const tptp.the_in1509933432tv_nat (-> tptp.set_Pa1764573435lle_tv (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.nat tptp.paraco1605129243lle_tv)) % 0.46/0.96 (declare-const tptp.produc1804670661lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.image_901203832at_nat (-> (-> tptp.produc1647334210lle_tv tptp.product_prod_nat_nat) tptp.set_Pr2014382200lle_tv tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (declare-const tptp.the_in427240730lle_tv (-> tptp.set_Pr2014382200lle_tv (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv) tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on394919723lle_tv (-> (-> tptp.produc270694976lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pr13445366lle_tv Bool)) % 0.46/0.96 (declare-const tptp.collec1111687558lle_tv (-> (-> tptp.paraco1605129243lle_tv Bool) tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.image_1221801032lle_tv (-> (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr2014382200lle_tv tptp.set_Pr2014382200lle_tv)) % 0.46/0.96 (declare-const tptp.collec924990229lle_tv (-> (-> tptp.produc270694976lle_tv Bool) tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (declare-const tptp.top_to1057771083lle_tv tptp.set_Pa1764573435lle_tv) % 0.46/0.96 (declare-const tptp.image_376325286tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv tptp.set_nat)) % 0.46/0.96 (declare-const tptp.f (-> tptp.nat tptp.nat)) % 0.46/0.96 (declare-const tptp.top_top_set_nat tptp.set_nat) % 0.46/0.96 (declare-const tptp.inj_on1179712058tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.96 (declare-const tptp.top_to1871154984lle_tv tptp.set_Pr2014382200lle_tv) % 0.46/0.96 (declare-const tptp.image_1397137548at_nat (-> (-> tptp.product_prod_nat_nat tptp.nat) tptp.set_Pr1986765409at_nat tptp.set_nat)) % 0.46/0.96 (declare-const tptp.the_in138087638lle_tv (-> tptp.set_nat (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.nat)) % 0.46/0.96 (declare-const tptp.inj_on520021963lle_tv (-> (-> tptp.product_prod_nat_nat tptp.paraco1605129243lle_tv) tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.96 (declare-const tptp.produc1608943133tv_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.paraco1147068288nge_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.96 (declare-const tptp.image_1093035615lle_tv (-> (-> tptp.product_prod_nat_nat tptp.paraco1605129243lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.paraco793048302_Indet (-> tptp.nat tptp.paraco1605129243lle_tv)) % 0.46/0.96 (declare-const tptp.image_1151963140lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_nat tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.the_in1388677748lle_tv (-> tptp.set_Pr13445366lle_tv (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 0.46/0.96 (declare-const tptp.image_988201162lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr2014382200lle_tv)) % 0.46/0.96 (declare-const tptp.the_in452116896lle_tv (-> tptp.set_Pa1764573435lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.96 (declare-const tptp.produc2040316391tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv)) % 0.46/0.96 (declare-const tptp.image_149830562lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (declare-const tptp.the_inv_into_nat_nat (-> tptp.set_nat (-> tptp.nat tptp.nat) tptp.nat tptp.nat)) % 0.46/0.96 (declare-const tptp.produc237097339lle_tv (-> (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.collec848462447tv_nat (-> (-> tptp.produc194167194tv_nat Bool) tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (declare-const tptp.plus_plus_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.46/0.96 (declare-const tptp.collec7649004at_nat (-> (-> tptp.product_prod_nat_nat Bool) tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (declare-const tptp.inj_on967082628lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc1647334210lle_tv) tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.96 (declare-const tptp.produc1408152463lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on1840679568lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv) tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.96 (declare-const tptp.produc1320959600at_nat (-> (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.image_335818702lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat)) % 0.46/0.96 (declare-const tptp.the_in2068894451at_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat) tptp.product_prod_nat_nat tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.image_1381266801at_nat (-> (-> tptp.produc194167194tv_nat tptp.nat) tptp.set_Pr1725653840tv_nat tptp.set_nat)) % 0.46/0.96 (declare-const tptp.produc42536895at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.inj_on808253149at_nat (-> (-> tptp.produc194167194tv_nat tptp.nat) tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.96 (declare-const tptp.the_in744013006lle_tv (-> tptp.set_Pr1986765409at_nat (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv) tptp.produc270694976lle_tv tptp.product_prod_nat_nat)) % 0.46/0.96 (declare-const tptp.image_2019567641lle_tv (-> (-> tptp.produc194167194tv_nat tptp.paraco1605129243lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.image_1509856791tv_nat (-> (-> tptp.produc270694976lle_tv tptp.nat) tptp.set_Pr13445366lle_tv tptp.set_nat)) % 0.46/0.96 (declare-const tptp.produc189459613tv_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.produc194167194tv_nat)) % 0.46/0.96 (declare-const tptp.inj_on936843139tv_nat (-> (-> tptp.produc270694976lle_tv tptp.nat) tptp.set_Pr13445366lle_tv Bool)) % 0.46/0.96 (declare-const tptp.image_802013119lle_tv (-> (-> tptp.produc270694976lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (declare-const tptp.inj_on642995232at_nat (-> (-> tptp.product_prod_nat_nat tptp.nat) tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.96 (define tptp.top_to1299250770e_tv_o () (lambda (@list (@var "X2" tptp.paraco1605129243lle_tv)) tptp.top_top_o)) % 0.46/0.96 (define tptp.top_top_nat_o () (lambda (@list (@var "X2" tptp.nat)) tptp.top_top_o)) % 0.46/0.96 (define tptp.inj_on2112487900lle_tv () (let ((_let_1 (@var "Y3" tptp.produc1647334210lle_tv))) (let ((_let_2 (@var "X2" tptp.produc1647334210lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))) (let ((_let_4 (@var "A2" tptp.set_Pr2014382200lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member1531318361lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member1531318361lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on552895452tv_nat () (let ((_let_1 (@var "Y3" tptp.produc194167194tv_nat))) (let ((_let_2 (@var "X2" tptp.produc194167194tv_nat))) (let ((_let_3 (@var "F2" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))) (let ((_let_4 (@var "A2" tptp.set_Pr1725653840tv_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member737151281tv_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member737151281tv_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on1745913142lle_tv () (let ((_let_1 (@var "Y3" tptp.produc270694976lle_tv))) (let ((_let_2 (@var "X2" tptp.produc270694976lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))) (let ((_let_4 (@var "A2" tptp.set_Pr13445366lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member813679063lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member813679063lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on26176689at_nat () (let ((_let_1 (@var "Y3" tptp.product_prod_nat_nat))) (let ((_let_2 (@var "X2" tptp.product_prod_nat_nat))) (let ((_let_3 (@var "F2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))) (let ((_let_4 (@var "A2" tptp.set_Pr1986765409at_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member701585322at_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member701585322at_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on1955349912lle_tv () (let ((_let_1 (@var "Y3" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on772319074lle_tv () (let ((_let_1 (@var "Y3" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "X2" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A2" tptp.set_Pa1764573435lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member266900804lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member266900804lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.inj_on_nat_nat () (let ((_let_1 (@var "Y3" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "F2" (-> tptp.nat tptp.nat)))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 0.46/0.96 (define tptp.top_to900819589_nat_o () (let ((_let_1 (@var "X2" tptp.produc194167194tv_nat))) (lambda (@list _let_1) (_ (_ tptp.member737151281tv_nat _let_1) tptp.top_to975729152tv_nat)))) % 0.46/0.96 (define tptp.top_to1889334367e_tv_o () (let ((_let_1 (@var "X2" tptp.produc270694976lle_tv))) (lambda (@list _let_1) (_ (_ tptp.member813679063lle_tv _let_1) tptp.top_to1411004326lle_tv)))) % 0.46/0.96 (define tptp.top_to632227436_nat_o () (let ((_let_1 (@var "X2" tptp.product_prod_nat_nat))) (lambda (@list _let_1) (_ (_ tptp.member701585322at_nat _let_1) tptp.top_to1555900337at_nat)))) % 0.46/0.96 (define tptp.strict2146030304at_nat () (let ((_let_1 (@var "S3" tptp.nat))) (let ((_let_2 (@var "F2" (-> tptp.nat tptp.nat)))) (let ((_let_3 (@var "R3" tptp.nat))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_nat _let_3) _let_4) (_ (_ tptp.member_nat _let_1) _let_4) (_ (_ tptp.ord_less_nat _let_3) _let_1)) (_ (_ tptp.ord_less_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict1310998166et_nat () (let ((_let_1 (@var "S3" tptp.nat))) (let ((_let_2 (@var "F2" (-> tptp.nat tptp.set_nat)))) (let ((_let_3 (@var "R3" tptp.nat))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_nat _let_3) _let_4) (_ (_ tptp.member_nat _let_1) _let_4) (_ (_ tptp.ord_less_nat _let_3) _let_1)) (_ (_ tptp.ord_less_set_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict1658340843lle_tv () (let ((_let_1 (@var "S3" tptp.nat))) (let ((_let_2 (@var "F2" (-> tptp.nat tptp.set_Pa1764573435lle_tv)))) (let ((_let_3 (@var "R3" tptp.nat))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_nat _let_3) _let_4) (_ (_ tptp.member_nat _let_1) _let_4) (_ (_ tptp.ord_less_nat _let_3) _let_1)) (_ (_ tptp.ord_le727057319lle_tv (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict1802283670at_nat () (let ((_let_1 (@var "S3" tptp.set_nat))) (let ((_let_2 (@var "F2" (-> tptp.set_nat tptp.nat)))) (let ((_let_3 (@var "R3" tptp.set_nat))) (let ((_let_4 (@var "A2" tptp.set_set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_set_nat _let_3) _let_4) (_ (_ tptp.member_set_nat _let_1) _let_4) (_ (_ tptp.ord_less_set_nat _let_3) _let_1)) (_ (_ tptp.ord_less_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict473775692et_nat () (let ((_let_1 (@var "S3" tptp.set_nat))) (let ((_let_2 (@var "F2" (-> tptp.set_nat tptp.set_nat)))) (let ((_let_3 (@var "R3" tptp.set_nat))) (let ((_let_4 (@var "A2" tptp.set_set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_set_nat _let_3) _let_4) (_ (_ tptp.member_set_nat _let_1) _let_4) (_ (_ tptp.ord_less_set_nat _let_3) _let_1)) (_ (_ tptp.ord_less_set_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict172559285lle_tv () (let ((_let_1 (@var "S3" tptp.set_nat))) (let ((_let_2 (@var "F2" (-> tptp.set_nat tptp.set_Pa1764573435lle_tv)))) (let ((_let_3 (@var "R3" tptp.set_nat))) (let ((_let_4 (@var "A2" tptp.set_set_nat))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member_set_nat _let_3) _let_4) (_ (_ tptp.member_set_nat _let_1) _let_4) (_ (_ tptp.ord_less_set_nat _let_3) _let_1)) (_ (_ tptp.ord_le727057319lle_tv (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict1125660301tv_nat () (let ((_let_1 (@var "S3" tptp.set_Pa1764573435lle_tv))) (let ((_let_2 (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.nat)))) (let ((_let_3 (@var "R3" tptp.set_Pa1764573435lle_tv))) (let ((_let_4 (@var "A2" tptp.set_se800614875lle_tv))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member1875402276lle_tv _let_3) _let_4) (_ (_ tptp.member1875402276lle_tv _let_1) _let_4) (_ (_ tptp.ord_le727057319lle_tv _let_3) _let_1)) (_ (_ tptp.ord_less_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict1455779395et_nat () (let ((_let_1 (@var "S3" tptp.set_Pa1764573435lle_tv))) (let ((_let_2 (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.set_nat)))) (let ((_let_3 (@var "R3" tptp.set_Pa1764573435lle_tv))) (let ((_let_4 (@var "A2" tptp.set_se800614875lle_tv))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member1875402276lle_tv _let_3) _let_4) (_ (_ tptp.member1875402276lle_tv _let_1) _let_4) (_ (_ tptp.ord_le727057319lle_tv _let_3) _let_1)) (_ (_ tptp.ord_less_set_nat (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.strict592849515lle_tv () (let ((_let_1 (@var "S3" tptp.set_Pa1764573435lle_tv))) (let ((_let_2 (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv)))) (let ((_let_3 (@var "R3" tptp.set_Pa1764573435lle_tv))) (let ((_let_4 (@var "A2" tptp.set_se800614875lle_tv))) (lambda (@list _let_2 _let_4) (forall (@list _let_3 _let_1) (=> (and (_ (_ tptp.member1875402276lle_tv _let_3) _let_4) (_ (_ tptp.member1875402276lle_tv _let_1) _let_4) (_ (_ tptp.ord_le727057319lle_tv _let_3) _let_1)) (_ (_ tptp.ord_le727057319lle_tv (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.46/0.96 (define tptp.ord_less_eq_set_nat () (let ((_let_1 (@var "B3" tptp.set_nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (_ tptp.member_nat _let_2))) (let ((_let_4 (@var "A2" tptp.set_nat))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.46/0.96 (define tptp.ord_le241064091lle_tv () (let ((_let_1 (@var "B3" tptp.set_Pa1764573435lle_tv))) (let ((_let_2 (@var "X2" tptp.paraco1605129243lle_tv))) (let ((_let_3 (_ tptp.member266900804lle_tv _let_2))) (let ((_let_4 (@var "A2" tptp.set_Pa1764573435lle_tv))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.46/0.96 (define @t1 () (@var "Tv2" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t2 () (@var "Tv1" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t3 () (= @t2 @t1)) % 0.46/0.96 (define @t4 () (_ tptp.paraco1147068288nge_tv tptp.f)) % 0.46/0.96 (define @t5 () (_ @t4 @t1)) % 0.46/0.96 (define @t6 () (_ @t4 @t2)) % 0.46/0.96 (define @t7 () (= @t6 @t5)) % 0.46/0.96 (define @t8 () (@list @t2 @t1)) % 0.46/0.96 (define @t9 () (forall @t8 (=> @t7 @t3))) % 0.46/0.96 (define @t10 () (@var "X" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t11 () (_ tptp.member737151281tv_nat @t10)) % 0.46/0.96 (define @t12 () (@var "X" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t13 () (_ tptp.member813679063lle_tv @t12)) % 0.46/0.96 (define @t14 () (@var "X" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t15 () (_ tptp.member701585322at_nat @t14)) % 0.46/0.96 (define @t16 () (@var "X" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t17 () (_ tptp.member266900804lle_tv @t16)) % 0.46/0.96 (define @t18 () (@list @t16)) % 0.46/0.96 (define @t19 () (@var "X" tptp.nat)) % 0.46/0.96 (define @t20 () (_ tptp.member_nat @t19)) % 0.46/0.96 (define @t21 () (@list @t19)) % 0.46/0.96 (define @t22 () (@var "Y" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t23 () (@var "X" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t24 () (= @t23 @t22)) % 0.46/0.96 (define @t25 () (@var "F" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.96 (define @t26 () (_ @t25 @t23)) % 0.46/0.96 (define @t27 () (= @t26 (_ @t25 @t22))) % 0.46/0.96 (define @t28 () (_ tptp.inj_on2112487900lle_tv @t25)) % 0.46/0.96 (define @t29 () (_ @t28 tptp.top_to1871154984lle_tv)) % 0.46/0.96 (define @t30 () (@list @t25 @t23 @t22)) % 0.46/0.96 (define @t31 () (@var "Y" tptp.nat)) % 0.46/0.96 (define @t32 () (= @t19 @t31)) % 0.46/0.96 (define @t33 () (@var "F" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.96 (define @t34 () (_ @t33 @t19)) % 0.46/0.96 (define @t35 () (= @t34 (_ @t33 @t31))) % 0.46/0.96 (define @t36 () (_ tptp.inj_on1955349912lle_tv @t33)) % 0.46/0.96 (define @t37 () (_ @t36 tptp.top_top_set_nat)) % 0.46/0.96 (define @t38 () (@list @t33 @t19 @t31)) % 0.46/0.96 (define @t39 () (@var "Y" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t40 () (= @t10 @t39)) % 0.46/0.96 (define @t41 () (@var "F" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.96 (define @t42 () (_ @t41 @t10)) % 0.46/0.96 (define @t43 () (= @t42 (_ @t41 @t39))) % 0.46/0.96 (define @t44 () (_ tptp.inj_on552895452tv_nat @t41)) % 0.46/0.96 (define @t45 () (_ @t44 tptp.top_to975729152tv_nat)) % 0.46/0.96 (define @t46 () (@list @t41 @t10 @t39)) % 0.46/0.96 (define @t47 () (@var "Y" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t48 () (= @t12 @t47)) % 0.46/0.96 (define @t49 () (@var "F" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.96 (define @t50 () (_ @t49 @t12)) % 0.46/0.96 (define @t51 () (= @t50 (_ @t49 @t47))) % 0.46/0.96 (define @t52 () (_ tptp.inj_on1745913142lle_tv @t49)) % 0.46/0.96 (define @t53 () (_ @t52 tptp.top_to1411004326lle_tv)) % 0.46/0.96 (define @t54 () (@list @t49 @t12 @t47)) % 0.46/0.96 (define @t55 () (@var "Y" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t56 () (= @t14 @t55)) % 0.46/0.96 (define @t57 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.96 (define @t58 () (_ @t57 @t14)) % 0.46/0.96 (define @t59 () (= @t58 (_ @t57 @t55))) % 0.46/0.96 (define @t60 () (_ tptp.inj_on26176689at_nat @t57)) % 0.46/0.96 (define @t61 () (_ @t60 tptp.top_to1555900337at_nat)) % 0.46/0.96 (define @t62 () (@list @t57 @t14 @t55)) % 0.46/0.96 (define @t63 () (@var "Y" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t64 () (= @t16 @t63)) % 0.46/0.96 (define @t65 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.96 (define @t66 () (_ @t65 @t16)) % 0.46/0.96 (define @t67 () (= @t66 (_ @t65 @t63))) % 0.46/0.96 (define @t68 () (_ tptp.inj_on772319074lle_tv @t65)) % 0.46/0.96 (define @t69 () (_ @t68 tptp.top_to1057771083lle_tv)) % 0.46/0.96 (define @t70 () (@list @t65 @t16 @t63)) % 0.46/0.96 (define @t71 () (@var "F" (-> tptp.nat tptp.nat))) % 0.46/0.96 (define @t72 () (_ @t71 @t19)) % 0.46/0.96 (define @t73 () (= @t72 (_ @t71 @t31))) % 0.46/0.96 (define @t74 () (_ tptp.inj_on_nat_nat @t71)) % 0.46/0.96 (define @t75 () (_ @t74 tptp.top_top_set_nat)) % 0.46/0.96 (define @t76 () (@list @t71 @t19 @t31)) % 0.46/0.96 (define @t77 () (@var "Y2" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t78 () (@var "X3" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t79 () (_ @t25 @t78)) % 0.46/0.96 (define @t80 () (=> (= @t79 (_ @t25 @t77)) (= @t78 @t77))) % 0.46/0.96 (define @t81 () (@list @t78 @t77)) % 0.46/0.96 (define @t82 () (@list @t25)) % 0.46/0.96 (define @t83 () (@var "Y2" tptp.nat)) % 0.46/0.96 (define @t84 () (@var "X3" tptp.nat)) % 0.46/0.96 (define @t85 () (= @t84 @t83)) % 0.46/0.96 (define @t86 () (_ @t33 @t84)) % 0.46/0.96 (define @t87 () (= @t86 (_ @t33 @t83))) % 0.46/0.96 (define @t88 () (=> @t87 @t85)) % 0.46/0.96 (define @t89 () (@list @t84 @t83)) % 0.46/0.96 (define @t90 () (@list @t33)) % 0.46/0.96 (define @t91 () (@var "Y2" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t92 () (@var "X3" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t93 () (_ @t41 @t92)) % 0.46/0.96 (define @t94 () (=> (= @t93 (_ @t41 @t91)) (= @t92 @t91))) % 0.46/0.96 (define @t95 () (@list @t92 @t91)) % 0.46/0.96 (define @t96 () (@list @t41)) % 0.46/0.96 (define @t97 () (@var "Y2" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t98 () (@var "X3" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t99 () (_ @t49 @t98)) % 0.46/0.96 (define @t100 () (=> (= @t99 (_ @t49 @t97)) (= @t98 @t97))) % 0.46/0.96 (define @t101 () (@list @t98 @t97)) % 0.46/0.96 (define @t102 () (@list @t49)) % 0.46/0.96 (define @t103 () (@var "Y2" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t104 () (@var "X3" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t105 () (_ @t57 @t104)) % 0.46/0.96 (define @t106 () (=> (= @t105 (_ @t57 @t103)) (= @t104 @t103))) % 0.46/0.96 (define @t107 () (@list @t104 @t103)) % 0.46/0.96 (define @t108 () (@list @t57)) % 0.46/0.96 (define @t109 () (@var "Y2" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t110 () (@var "X3" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t111 () (_ @t65 @t110)) % 0.46/0.96 (define @t112 () (=> (= @t111 (_ @t65 @t109)) (= @t110 @t109))) % 0.46/0.96 (define @t113 () (@list @t110 @t109)) % 0.46/0.96 (define @t114 () (@list @t65)) % 0.46/0.96 (define @t115 () (_ @t71 @t83)) % 0.46/0.96 (define @t116 () (_ @t71 @t84)) % 0.46/0.96 (define @t117 () (= @t116 @t115)) % 0.46/0.96 (define @t118 () (=> @t117 @t85)) % 0.46/0.96 (define @t119 () (@list @t71)) % 0.46/0.96 (define @t120 () (= @t27 @t24)) % 0.46/0.96 (define @t121 () (= @t35 @t32)) % 0.46/0.96 (define @t122 () (= @t43 @t40)) % 0.46/0.96 (define @t123 () (= @t51 @t48)) % 0.46/0.96 (define @t124 () (= @t59 @t56)) % 0.46/0.96 (define @t125 () (= @t67 @t64)) % 0.46/0.96 (define @t126 () (= @t73 @t32)) % 0.46/0.96 (define @t127 () (@var "Y3" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t128 () (@var "X2" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t129 () (= @t128 @t127)) % 0.46/0.96 (define @t130 () (@var "Y3" tptp.nat)) % 0.46/0.96 (define @t131 () (@var "X2" tptp.nat)) % 0.46/0.96 (define @t132 () (= @t131 @t130)) % 0.46/0.96 (define @t133 () (_ @t33 @t130)) % 0.46/0.96 (define @t134 () (_ @t33 @t131)) % 0.46/0.96 (define @t135 () (@list @t131 @t130)) % 0.46/0.96 (define @t136 () (@var "Y3" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t137 () (@var "X2" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t138 () (= @t137 @t136)) % 0.46/0.96 (define @t139 () (@var "Y3" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t140 () (@var "X2" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t141 () (= @t140 @t139)) % 0.46/0.96 (define @t142 () (@var "Y3" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t143 () (@var "X2" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t144 () (= @t143 @t142)) % 0.46/0.96 (define @t145 () (_ @t57 @t143)) % 0.46/0.96 (define @t146 () (@var "Y3" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t147 () (@var "X2" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t148 () (= @t147 @t146)) % 0.46/0.96 (define @t149 () (_ @t65 @t146)) % 0.46/0.96 (define @t150 () (_ @t65 @t147)) % 0.46/0.96 (define @t151 () (_ @t71 @t130)) % 0.46/0.96 (define @t152 () (_ @t71 @t131)) % 0.46/0.96 (define @t153 () (@var "A" tptp.set_Pr2014382200lle_tv)) % 0.46/0.96 (define @t154 () (_ (_ tptp.member1531318361lle_tv @t22) @t153)) % 0.46/0.96 (define @t155 () (_ (_ tptp.member1531318361lle_tv @t23) @t153)) % 0.46/0.96 (define @t156 () (_ @t28 @t153)) % 0.46/0.96 (define @t157 () (@list @t25 @t153 @t23 @t22)) % 0.46/0.96 (define @t158 () (@var "A" tptp.set_Pr1725653840tv_nat)) % 0.46/0.96 (define @t159 () (_ (_ tptp.member737151281tv_nat @t39) @t158)) % 0.46/0.96 (define @t160 () (_ @t11 @t158)) % 0.46/0.96 (define @t161 () (_ @t44 @t158)) % 0.46/0.96 (define @t162 () (@list @t41 @t158 @t10 @t39)) % 0.46/0.96 (define @t163 () (@var "A" tptp.set_Pr13445366lle_tv)) % 0.46/0.96 (define @t164 () (_ (_ tptp.member813679063lle_tv @t47) @t163)) % 0.46/0.96 (define @t165 () (_ @t13 @t163)) % 0.46/0.96 (define @t166 () (_ @t52 @t163)) % 0.46/0.96 (define @t167 () (@list @t49 @t163 @t12 @t47)) % 0.46/0.96 (define @t168 () (@var "A" tptp.set_Pr1986765409at_nat)) % 0.46/0.96 (define @t169 () (_ (_ tptp.member701585322at_nat @t55) @t168)) % 0.46/0.96 (define @t170 () (_ @t15 @t168)) % 0.46/0.96 (define @t171 () (_ @t60 @t168)) % 0.46/0.96 (define @t172 () (@list @t57 @t168 @t14 @t55)) % 0.46/0.96 (define @t173 () (@var "A" tptp.set_nat)) % 0.46/0.96 (define @t174 () (_ tptp.member_nat @t31)) % 0.46/0.96 (define @t175 () (_ @t174 @t173)) % 0.46/0.96 (define @t176 () (_ @t20 @t173)) % 0.46/0.96 (define @t177 () (=> @t176 (=> @t175 @t32))) % 0.46/0.96 (define @t178 () (_ @t36 @t173)) % 0.46/0.96 (define @t179 () (@list @t33 @t173 @t19 @t31)) % 0.46/0.96 (define @t180 () (@var "A" tptp.set_Pa1764573435lle_tv)) % 0.46/0.96 (define @t181 () (_ tptp.member266900804lle_tv @t63)) % 0.46/0.96 (define @t182 () (_ @t181 @t180)) % 0.46/0.96 (define @t183 () (_ @t17 @t180)) % 0.46/0.96 (define @t184 () (_ @t68 @t180)) % 0.46/0.96 (define @t185 () (@list @t65 @t180 @t16 @t63)) % 0.46/0.96 (define @t186 () (_ @t74 @t173)) % 0.46/0.96 (define @t187 () (@list @t71 @t173 @t19 @t31)) % 0.46/0.96 (define @t188 () (_ (_ tptp.member1531318361lle_tv @t78) @t153)) % 0.46/0.96 (define @t189 () (_ tptp.member737151281tv_nat @t92)) % 0.46/0.96 (define @t190 () (_ @t189 @t158)) % 0.46/0.96 (define @t191 () (_ tptp.member813679063lle_tv @t98)) % 0.46/0.96 (define @t192 () (_ @t191 @t163)) % 0.46/0.96 (define @t193 () (_ tptp.member701585322at_nat @t104)) % 0.46/0.96 (define @t194 () (_ @t193 @t168)) % 0.46/0.96 (define @t195 () (_ (_ tptp.member_nat @t83) @t173)) % 0.46/0.96 (define @t196 () (_ tptp.member_nat @t84)) % 0.46/0.96 (define @t197 () (_ @t196 @t173)) % 0.46/0.96 (define @t198 () (_ tptp.member266900804lle_tv @t110)) % 0.46/0.96 (define @t199 () (_ @t198 @t180)) % 0.46/0.96 (define @t200 () (@list @t173 @t71)) % 0.46/0.96 (define @t201 () (@var "G" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.96 (define @t202 () (@var "A3" tptp.produc1647334210lle_tv)) % 0.46/0.96 (define @t203 () (@var "G" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.96 (define @t204 () (@var "A3" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t205 () (@var "G" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.96 (define @t206 () (@var "A3" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t207 () (@var "G" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.96 (define @t208 () (@var "A3" tptp.product_prod_nat_nat)) % 0.46/0.96 (define @t209 () (@var "G" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.96 (define @t210 () (@var "A3" tptp.nat)) % 0.46/0.96 (define @t211 () (_ (_ tptp.member_nat @t210) @t173)) % 0.46/0.96 (define @t212 () (@list @t210)) % 0.46/0.96 (define @t213 () (@var "G" (-> tptp.nat tptp.nat))) % 0.46/0.96 (define @t214 () (_ tptp.inj_on_nat_nat @t213)) % 0.46/0.96 (define @t215 () (_ @t214 @t173)) % 0.46/0.96 (define @t216 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.96 (define @t217 () (_ tptp.inj_on772319074lle_tv @t216)) % 0.46/0.96 (define @t218 () (_ @t217 @t180)) % 0.46/0.96 (define @t219 () (@var "A3" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t220 () (= tptp.top_to1057771083lle_tv (_ tptp.collec1111687558lle_tv tptp.top_to1299250770e_tv_o))) % 0.46/0.96 (define @t221 () (@list @t92)) % 0.46/0.96 (define @t222 () (@list @t98)) % 0.46/0.96 (define @t223 () (@list @t104)) % 0.46/0.96 (define @t224 () (@list @t110)) % 0.46/0.96 (define @t225 () (@list @t84)) % 0.46/0.96 (define @t226 () (@list @t180)) % 0.46/0.96 (define @t227 () (@list @t173)) % 0.46/0.96 (define @t228 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.nat))) % 0.46/0.96 (define @t229 () (= (_ @t228 @t86) @t84)) % 0.46/0.96 (define @t230 () (_ @t213 @t116)) % 0.46/0.96 (define @t231 () (= @t230 @t84)) % 0.46/0.96 (define @t232 () (@list @t173 @t213 @t71)) % 0.46/0.96 (define @t233 () (_ @t216 @t111)) % 0.46/0.96 (define @t234 () (= @t233 @t110)) % 0.46/0.96 (define @t235 () (@list @t180 @t216 @t65)) % 0.46/0.96 (define @t236 () (not @t32)) % 0.46/0.96 (define @t237 () (_ tptp.member266900804lle_tv @t147)) % 0.46/0.96 (define @t238 () (@list @t147)) % 0.46/0.96 (define @t239 () (_ tptp.member_nat @t131)) % 0.46/0.96 (define @t240 () (@list @t131)) % 0.46/0.96 (define @t241 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.nat))) % 0.46/0.96 (define @t242 () (_ @t241 @t16)) % 0.46/0.96 (define @t243 () (_ tptp.inj_on1179712058tv_nat @t241)) % 0.46/0.96 (define @t244 () (_ @t243 tptp.top_to1057771083lle_tv)) % 0.46/0.96 (define @t245 () (@list @t241 @t16)) % 0.46/0.96 (define @t246 () (@list @t33 @t19)) % 0.46/0.96 (define @t247 () (@list @t65 @t16)) % 0.46/0.96 (define @t248 () (@list @t71 @t19)) % 0.46/0.96 (define @t249 () (_ (_ tptp.strict2146030304at_nat @t71) @t173)) % 0.46/0.96 (define @t250 () (@list @t71 @t173)) % 0.46/0.96 (define @t251 () (_ (_ tptp.ord_less_nat @t84) @t83)) % 0.46/0.96 (define @t252 () (not @t117)) % 0.46/0.96 (define @t253 () (@var "A4" tptp.nat)) % 0.46/0.96 (define @t254 () (_ tptp.inj_on_nat_nat (_ tptp.plus_plus_nat @t253))) % 0.46/0.96 (define @t255 () (@var "N" tptp.nat)) % 0.46/0.96 (define @t256 () (@var "A4" tptp.paraco1605129243lle_tv)) % 0.46/0.96 (define @t257 () (_ tptp.member266900804lle_tv @t256)) % 0.46/0.96 (define @t258 () (_ @t257 @t180)) % 0.46/0.96 (define @t259 () (_ tptp.image_376325286tv_nat @t241)) % 0.46/0.96 (define @t260 () (_ @t259 @t180)) % 0.46/0.96 (define @t261 () (= (_ (_ tptp.member_nat (_ @t241 @t256)) @t260) @t258)) % 0.46/0.96 (define @t262 () (_ tptp.image_335818702lle_tv @t65)) % 0.46/0.96 (define @t263 () (_ @t262 @t180)) % 0.46/0.96 (define @t264 () (= (_ (_ tptp.member266900804lle_tv (_ @t65 @t256)) @t263) @t258)) % 0.46/0.96 (define @t265 () (_ tptp.member_nat @t253)) % 0.46/0.96 (define @t266 () (_ @t265 @t173)) % 0.46/0.96 (define @t267 () (_ tptp.image_nat_nat @t71)) % 0.46/0.96 (define @t268 () (_ @t267 @t173)) % 0.46/0.96 (define @t269 () (= (_ (_ tptp.member_nat (_ @t71 @t253)) @t268) @t266)) % 0.46/0.96 (define @t270 () (_ tptp.image_1151963140lle_tv @t33)) % 0.46/0.96 (define @t271 () (_ @t270 @t173)) % 0.46/0.96 (define @t272 () (= (_ (_ tptp.member266900804lle_tv (_ @t33 @t253)) @t271) @t266)) % 0.46/0.96 (define @t273 () (@var "A4" tptp.produc194167194tv_nat)) % 0.46/0.96 (define @t274 () (_ (_ tptp.member737151281tv_nat @t273) @t158)) % 0.46/0.96 (define @t275 () (@var "F" (-> tptp.produc194167194tv_nat tptp.nat))) % 0.46/0.96 (define @t276 () (_ tptp.image_1381266801at_nat @t275)) % 0.46/0.96 (define @t277 () (_ (_ tptp.inj_on808253149at_nat @t275) tptp.top_to975729152tv_nat)) % 0.46/0.96 (define @t278 () (@var "F" (-> tptp.produc194167194tv_nat tptp.paraco1605129243lle_tv))) % 0.46/0.96 (define @t279 () (_ tptp.image_2019567641lle_tv @t278)) % 0.46/0.96 (define @t280 () (_ (_ tptp.inj_on1612474245lle_tv @t278) tptp.top_to975729152tv_nat)) % 0.46/0.96 (define @t281 () (@var "A4" tptp.produc270694976lle_tv)) % 0.46/0.96 (define @t282 () (_ (_ tptp.member813679063lle_tv @t281) @t163)) % 0.46/0.96 (define @t283 () (@var "F" (-> tptp.produc270694976lle_tv tptp.nat))) % 0.46/0.96 (define @t284 () (_ tptp.image_1509856791tv_nat @t283)) % 0.46/0.97 (define @t285 () (_ (_ tptp.inj_on936843139tv_nat @t283) tptp.top_to1411004326lle_tv)) % 0.46/0.97 (define @t286 () (@var "F" (-> tptp.produc270694976lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t287 () (_ tptp.image_802013119lle_tv @t286)) % 0.46/0.97 (define @t288 () (_ (_ tptp.inj_on394919723lle_tv @t286) tptp.top_to1411004326lle_tv)) % 0.46/0.97 (define @t289 () (@var "A4" tptp.product_prod_nat_nat)) % 0.46/0.97 (define @t290 () (_ (_ tptp.member701585322at_nat @t289) @t168)) % 0.46/0.97 (define @t291 () (@var "F" (-> tptp.product_prod_nat_nat tptp.nat))) % 0.46/0.97 (define @t292 () (_ tptp.image_1397137548at_nat @t291)) % 0.46/0.97 (define @t293 () (_ (_ tptp.inj_on642995232at_nat @t291) tptp.top_to1555900337at_nat)) % 0.46/0.97 (define @t294 () (@var "F" (-> tptp.product_prod_nat_nat tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t295 () (_ tptp.image_1093035615lle_tv @t294)) % 0.46/0.97 (define @t296 () (_ (_ tptp.inj_on520021963lle_tv @t294) tptp.top_to1555900337at_nat)) % 0.46/0.97 (define @t297 () (@var "B" tptp.set_Pr2014382200lle_tv)) % 0.46/0.97 (define @t298 () (_ tptp.image_1221801032lle_tv @t25)) % 0.46/0.97 (define @t299 () (_ @t298 @t153)) % 0.46/0.97 (define @t300 () (@var "B" tptp.set_nat)) % 0.46/0.97 (define @t301 () (= @t173 @t300)) % 0.46/0.97 (define @t302 () (@var "B" tptp.set_Pr1725653840tv_nat)) % 0.46/0.97 (define @t303 () (_ tptp.image_1104296520tv_nat @t41)) % 0.46/0.97 (define @t304 () (_ @t303 @t158)) % 0.46/0.97 (define @t305 () (@var "B" tptp.set_Pr13445366lle_tv)) % 0.46/0.97 (define @t306 () (_ tptp.image_149830562lle_tv @t49)) % 0.46/0.97 (define @t307 () (@var "B" tptp.set_Pr1986765409at_nat)) % 0.46/0.97 (define @t308 () (= @t168 @t307)) % 0.46/0.97 (define @t309 () (@var "F" (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat))) % 0.46/0.97 (define @t310 () (_ tptp.image_1597721174tv_nat @t309)) % 0.46/0.97 (define @t311 () (_ @t310 @t168)) % 0.46/0.97 (define @t312 () (_ tptp.inj_on1764151786tv_nat @t309)) % 0.46/0.97 (define @t313 () (@var "F" (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv))) % 0.46/0.97 (define @t314 () (_ tptp.image_1674248956lle_tv @t313)) % 0.46/0.97 (define @t315 () (_ @t314 @t168)) % 0.46/0.97 (define @t316 () (_ tptp.inj_on1840679568lle_tv @t313)) % 0.46/0.97 (define @t317 () (_ tptp.image_815163717at_nat @t57)) % 0.46/0.97 (define @t318 () (_ @t317 @t168)) % 0.46/0.97 (define @t319 () (@var "B" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t320 () (_ @t262 @t319)) % 0.46/0.97 (define @t321 () (= (= @t263 @t320) (= @t180 @t319))) % 0.46/0.97 (define @t322 () (@list @t65 @t180 @t319)) % 0.46/0.97 (define @t323 () (_ @t267 @t300)) % 0.46/0.97 (define @t324 () (= (= @t268 @t323) @t301)) % 0.46/0.97 (define @t325 () (@list @t71 @t173 @t300)) % 0.46/0.97 (define @t326 () (= @t146 @t147)) % 0.46/0.97 (define @t327 () (@var "B2" tptp.nat)) % 0.46/0.97 (define @t328 () (@list @t146)) % 0.46/0.97 (define @t329 () (_ @t241 @t147)) % 0.46/0.97 (define @t330 () (_ @t259 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t331 () (_ tptp.member_nat @t327)) % 0.46/0.97 (define @t332 () (_ @t331 @t330)) % 0.46/0.97 (define @t333 () (@var "B2" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t334 () (_ @t262 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t335 () (_ tptp.member266900804lle_tv @t333)) % 0.46/0.97 (define @t336 () (_ @t335 @t334)) % 0.46/0.97 (define @t337 () (= @t130 @t131)) % 0.46/0.97 (define @t338 () (@list @t130)) % 0.46/0.97 (define @t339 () (_ @t267 tptp.top_top_set_nat)) % 0.46/0.97 (define @t340 () (_ @t331 @t339)) % 0.46/0.97 (define @t341 () (_ @t270 tptp.top_top_set_nat)) % 0.46/0.97 (define @t342 () (_ @t335 @t341)) % 0.46/0.97 (define @t343 () (= @t136 @t137)) % 0.46/0.97 (define @t344 () (@list @t136)) % 0.46/0.97 (define @t345 () (@list @t137)) % 0.46/0.97 (define @t346 () (= @t139 @t140)) % 0.46/0.97 (define @t347 () (@list @t139)) % 0.46/0.97 (define @t348 () (@list @t140)) % 0.46/0.97 (define @t349 () (= @t142 @t143)) % 0.46/0.97 (define @t350 () (@list @t142)) % 0.46/0.97 (define @t351 () (@list @t143)) % 0.46/0.97 (define @t352 () (_ tptp.order_769474267at_nat @t71)) % 0.46/0.97 (define @t353 () (@var "B2" tptp.produc194167194tv_nat)) % 0.46/0.97 (define @t354 () (_ (_ tptp.member737151281tv_nat @t353) @t311)) % 0.46/0.97 (define @t355 () (_ @t309 @t14)) % 0.46/0.97 (define @t356 () (= @t353 @t355)) % 0.46/0.97 (define @t357 () (@var "B2" tptp.produc270694976lle_tv)) % 0.46/0.97 (define @t358 () (_ (_ tptp.member813679063lle_tv @t357) @t315)) % 0.46/0.97 (define @t359 () (_ @t313 @t14)) % 0.46/0.97 (define @t360 () (= @t357 @t359)) % 0.46/0.97 (define @t361 () (@var "B2" tptp.product_prod_nat_nat)) % 0.46/0.97 (define @t362 () (_ (_ tptp.member701585322at_nat @t361) @t318)) % 0.46/0.97 (define @t363 () (= @t361 @t58)) % 0.46/0.97 (define @t364 () (_ @t331 @t268)) % 0.46/0.97 (define @t365 () (= @t327 @t72)) % 0.46/0.97 (define @t366 () (_ @t335 @t271)) % 0.46/0.97 (define @t367 () (= @t333 @t34)) % 0.46/0.97 (define @t368 () (_ @t331 @t260)) % 0.46/0.97 (define @t369 () (= @t327 @t242)) % 0.46/0.97 (define @t370 () (_ @t335 @t263)) % 0.46/0.97 (define @t371 () (= @t333 @t66)) % 0.46/0.97 (define @t372 () (@var "Y22" tptp.nat)) % 0.46/0.97 (define @t373 () (@var "X22" tptp.nat)) % 0.46/0.97 (define @t374 () (forall @t18 (_ tptp.top_to1299250770e_tv_o @t16))) % 0.46/0.97 (define @t375 () (_ (_ tptp.the_in452116896lle_tv @t180) @t65)) % 0.46/0.97 (define @t376 () (@list @t65 @t180)) % 0.46/0.97 (define @t377 () (_ (_ tptp.the_inv_into_nat_nat @t173) @t71)) % 0.46/0.97 (define @t378 () (_ (_ tptp.the_in138087638lle_tv @t173) @t33)) % 0.46/0.97 (define @t379 () (_ (_ tptp.the_in1509933432tv_nat @t180) @t241)) % 0.46/0.97 (define @t380 () (_ @t243 @t180)) % 0.46/0.97 (define @t381 () (@var "F" (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat))) % 0.46/0.97 (define @t382 () (@var "F" (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat))) % 0.46/0.97 (define @t383 () (_ tptp.member_nat @t72)) % 0.46/0.97 (define @t384 () (_ tptp.member266900804lle_tv @t34)) % 0.46/0.97 (define @t385 () (_ tptp.member_nat @t242)) % 0.46/0.97 (define @t386 () (_ tptp.member266900804lle_tv @t66)) % 0.46/0.97 (define @t387 () (@var "Z" tptp.produc194167194tv_nat)) % 0.46/0.97 (define @t388 () (_ tptp.member701585322at_nat @t143)) % 0.46/0.97 (define @t389 () (_ @t388 @t168)) % 0.46/0.97 (define @t390 () (@var "Z" tptp.produc270694976lle_tv)) % 0.46/0.97 (define @t391 () (@var "Z" tptp.product_prod_nat_nat)) % 0.46/0.97 (define @t392 () (@var "Z" tptp.nat)) % 0.46/0.97 (define @t393 () (_ @t239 @t173)) % 0.46/0.97 (define @t394 () (@var "Z" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t395 () (_ @t309 @t104)) % 0.46/0.97 (define @t396 () (@var "P" (-> tptp.produc194167194tv_nat Bool))) % 0.46/0.97 (define @t397 () (@var "X4" tptp.produc194167194tv_nat)) % 0.46/0.97 (define @t398 () (@list @t309 @t168 @t396)) % 0.46/0.97 (define @t399 () (_ @t313 @t104)) % 0.46/0.97 (define @t400 () (@var "P" (-> tptp.produc270694976lle_tv Bool))) % 0.46/0.97 (define @t401 () (@var "X4" tptp.produc270694976lle_tv)) % 0.46/0.97 (define @t402 () (@list @t313 @t168 @t400)) % 0.46/0.97 (define @t403 () (@var "P" (-> tptp.product_prod_nat_nat Bool))) % 0.46/0.97 (define @t404 () (@var "X4" tptp.product_prod_nat_nat)) % 0.46/0.97 (define @t405 () (_ tptp.member701585322at_nat @t404)) % 0.46/0.97 (define @t406 () (@list @t404)) % 0.46/0.97 (define @t407 () (@list @t57 @t168 @t403)) % 0.46/0.97 (define @t408 () (@var "P" (-> tptp.paraco1605129243lle_tv Bool))) % 0.46/0.97 (define @t409 () (@var "X4" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t410 () (@list @t33 @t173 @t408)) % 0.46/0.97 (define @t411 () (@var "P" (-> tptp.nat Bool))) % 0.46/0.97 (define @t412 () (@var "X4" tptp.nat)) % 0.46/0.97 (define @t413 () (_ tptp.member_nat @t412)) % 0.46/0.97 (define @t414 () (@list @t412)) % 0.46/0.97 (define @t415 () (@list @t71 @t173 @t411)) % 0.46/0.97 (define @t416 () (@var "N2" tptp.set_Pr1986765409at_nat)) % 0.46/0.97 (define @t417 () (@var "G" (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat))) % 0.46/0.97 (define @t418 () (@var "M" tptp.set_Pr1986765409at_nat)) % 0.46/0.97 (define @t419 () (_ @t193 @t416)) % 0.46/0.97 (define @t420 () (= @t418 @t416)) % 0.46/0.97 (define @t421 () (@var "G" (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv))) % 0.46/0.97 (define @t422 () (@var "N2" tptp.set_nat)) % 0.46/0.97 (define @t423 () (_ tptp.image_1151963140lle_tv @t209)) % 0.46/0.97 (define @t424 () (@var "M" tptp.set_nat)) % 0.46/0.97 (define @t425 () (_ @t196 @t422)) % 0.46/0.97 (define @t426 () (= @t424 @t422)) % 0.46/0.97 (define @t427 () (_ tptp.image_nat_nat @t213)) % 0.46/0.97 (define @t428 () (_ @t213 @t84)) % 0.46/0.97 (define @t429 () (_ @t405 @t168)) % 0.46/0.97 (define @t430 () (_ @t413 @t173)) % 0.46/0.97 (define @t431 () (_ @t408 @t110)) % 0.46/0.97 (define @t432 () (_ @t411 @t84)) % 0.46/0.97 (define @t433 () (@var "S" tptp.nat)) % 0.46/0.97 (define @t434 () (@var "R" tptp.nat)) % 0.46/0.97 (define @t435 () (_ (_ tptp.ord_less_nat @t434) @t433)) % 0.46/0.97 (define @t436 () (_ (_ tptp.member_nat @t433) @t173)) % 0.46/0.97 (define @t437 () (_ (_ tptp.member_nat @t434) @t173)) % 0.46/0.97 (define @t438 () (@var "F" (-> tptp.nat tptp.set_nat))) % 0.46/0.97 (define @t439 () (_ (_ tptp.strict1310998166et_nat @t438) @t173)) % 0.46/0.97 (define @t440 () (@var "F" (-> tptp.nat tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t441 () (_ (_ tptp.strict1658340843lle_tv @t440) @t173)) % 0.46/0.97 (define @t442 () (@var "S" tptp.set_nat)) % 0.46/0.97 (define @t443 () (@var "F" (-> tptp.set_nat tptp.nat))) % 0.46/0.97 (define @t444 () (@var "R" tptp.set_nat)) % 0.46/0.97 (define @t445 () (_ (_ tptp.ord_less_set_nat @t444) @t442)) % 0.46/0.97 (define @t446 () (@var "A" tptp.set_set_nat)) % 0.46/0.97 (define @t447 () (_ (_ tptp.member_set_nat @t442) @t446)) % 0.46/0.97 (define @t448 () (_ (_ tptp.member_set_nat @t444) @t446)) % 0.46/0.97 (define @t449 () (_ (_ tptp.strict1802283670at_nat @t443) @t446)) % 0.46/0.97 (define @t450 () (@var "F" (-> tptp.set_nat tptp.set_nat))) % 0.46/0.97 (define @t451 () (_ (_ tptp.strict473775692et_nat @t450) @t446)) % 0.46/0.97 (define @t452 () (@var "F" (-> tptp.set_nat tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t453 () (_ (_ tptp.strict172559285lle_tv @t452) @t446)) % 0.46/0.97 (define @t454 () (@var "S" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t455 () (@var "F" (-> tptp.set_Pa1764573435lle_tv tptp.nat))) % 0.46/0.97 (define @t456 () (@var "R" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t457 () (_ (_ tptp.ord_le727057319lle_tv @t456) @t454)) % 0.46/0.97 (define @t458 () (@var "A" tptp.set_se800614875lle_tv)) % 0.46/0.97 (define @t459 () (_ (_ tptp.member1875402276lle_tv @t454) @t458)) % 0.46/0.97 (define @t460 () (_ (_ tptp.member1875402276lle_tv @t456) @t458)) % 0.46/0.97 (define @t461 () (_ (_ tptp.strict1125660301tv_nat @t455) @t458)) % 0.46/0.97 (define @t462 () (@var "F" (-> tptp.set_Pa1764573435lle_tv tptp.set_nat))) % 0.46/0.97 (define @t463 () (_ (_ tptp.strict1455779395et_nat @t462) @t458)) % 0.46/0.97 (define @t464 () (@var "F" (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t465 () (_ (_ tptp.strict592849515lle_tv @t464) @t458)) % 0.46/0.97 (define @t466 () (@var "S2" tptp.nat)) % 0.46/0.97 (define @t467 () (@var "R2" tptp.nat)) % 0.46/0.97 (define @t468 () (_ (_ tptp.ord_less_nat @t467) @t466)) % 0.46/0.97 (define @t469 () (_ (_ tptp.member_nat @t466) @t173)) % 0.46/0.97 (define @t470 () (_ (_ tptp.member_nat @t467) @t173)) % 0.46/0.97 (define @t471 () (@list @t467 @t466)) % 0.46/0.97 (define @t472 () (@var "S2" tptp.set_nat)) % 0.46/0.97 (define @t473 () (@var "R2" tptp.set_nat)) % 0.46/0.97 (define @t474 () (_ (_ tptp.ord_less_set_nat @t473) @t472)) % 0.46/0.97 (define @t475 () (_ (_ tptp.member_set_nat @t472) @t446)) % 0.46/0.97 (define @t476 () (_ (_ tptp.member_set_nat @t473) @t446)) % 0.46/0.97 (define @t477 () (@list @t473 @t472)) % 0.46/0.97 (define @t478 () (@var "S2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t479 () (@var "R2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t480 () (_ (_ tptp.ord_le727057319lle_tv @t479) @t478)) % 0.46/0.97 (define @t481 () (_ (_ tptp.member1875402276lle_tv @t478) @t458)) % 0.46/0.97 (define @t482 () (_ (_ tptp.member1875402276lle_tv @t479) @t458)) % 0.46/0.97 (define @t483 () (@list @t479 @t478)) % 0.46/0.97 (define @t484 () (@var "C" tptp.nat)) % 0.46/0.97 (define @t485 () (_ tptp.ord_less_nat @t253)) % 0.46/0.97 (define @t486 () (_ (_ tptp.ord_less_nat @t327) @t484)) % 0.46/0.97 (define @t487 () (@var "A4" tptp.set_nat)) % 0.46/0.97 (define @t488 () (_ tptp.ord_less_set_nat @t487)) % 0.46/0.97 (define @t489 () (@var "A4" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t490 () (_ tptp.ord_le727057319lle_tv @t489)) % 0.46/0.97 (define @t491 () (@var "C" tptp.set_nat)) % 0.46/0.97 (define @t492 () (@var "Y2" tptp.set_nat)) % 0.46/0.97 (define @t493 () (@var "X3" tptp.set_nat)) % 0.46/0.97 (define @t494 () (_ (_ tptp.ord_less_set_nat @t493) @t492)) % 0.46/0.97 (define @t495 () (@list @t493 @t492)) % 0.46/0.97 (define @t496 () (@var "B2" tptp.set_nat)) % 0.46/0.97 (define @t497 () (_ (_ tptp.ord_less_set_nat @t496) @t491)) % 0.46/0.97 (define @t498 () (@var "C" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t499 () (@var "Y2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t500 () (@var "X3" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t501 () (_ (_ tptp.ord_le727057319lle_tv @t500) @t499)) % 0.46/0.97 (define @t502 () (@list @t500 @t499)) % 0.46/0.97 (define @t503 () (@var "B2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t504 () (_ (_ tptp.ord_le727057319lle_tv @t503) @t498)) % 0.46/0.97 (define @t505 () (_ tptp.collect_nat @t411)) % 0.46/0.97 (define @t506 () (_ tptp.collec1111687558lle_tv @t408)) % 0.46/0.97 (define @t507 () (@var "Q" (-> tptp.nat Bool))) % 0.46/0.97 (define @t508 () (@var "Q" (-> tptp.paraco1605129243lle_tv Bool))) % 0.46/0.97 (define @t509 () (_ (_ tptp.ord_le727057319lle_tv @t180) @t319)) % 0.46/0.97 (define @t510 () (_ @t68 @t319)) % 0.46/0.97 (define @t511 () (@list @t65 @t319 @t180)) % 0.46/0.97 (define @t512 () (_ (_ tptp.ord_less_set_nat @t173) @t300)) % 0.46/0.97 (define @t513 () (_ @t74 @t300)) % 0.46/0.97 (define @t514 () (@list @t71 @t300 @t173)) % 0.46/0.97 (define @t515 () (_ @t377 @t31)) % 0.46/0.97 (define @t516 () (_ @t375 @t63)) % 0.46/0.97 (define @t517 () (forall @t225 @t231)) % 0.46/0.97 (define @t518 () (= @t339 tptp.top_top_set_nat)) % 0.46/0.97 (define @t519 () (= @t63 @t111)) % 0.46/0.97 (define @t520 () (= @t334 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t521 () (@list @t65 @t63)) % 0.46/0.97 (define @t522 () (_ @t241 @t110)) % 0.46/0.97 (define @t523 () (= @t31 @t522)) % 0.46/0.97 (define @t524 () (= @t330 tptp.top_top_set_nat)) % 0.46/0.97 (define @t525 () (@list @t241 @t31)) % 0.46/0.97 (define @t526 () (= @t63 @t86)) % 0.46/0.97 (define @t527 () (= @t341 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t528 () (@list @t33 @t63)) % 0.46/0.97 (define @t529 () (= @t31 @t116)) % 0.46/0.97 (define @t530 () (@list @t71 @t31)) % 0.46/0.97 (define @t531 () (= (_ (_ tptp.image_335818702lle_tv @t216) tptp.top_to1057771083lle_tv) tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t532 () (= (_ (_ tptp.image_376325286tv_nat @t228) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat)) % 0.46/0.97 (define @t533 () (= (_ @t423 tptp.top_top_set_nat) tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t534 () (= (_ @t427 tptp.top_top_set_nat) tptp.top_top_set_nat)) % 0.46/0.97 (define @t535 () (@var "Xa" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t536 () (@var "Xa" tptp.nat)) % 0.46/0.97 (define @t537 () (@list @t489)) % 0.46/0.97 (define @t538 () (@list @t487)) % 0.46/0.97 (define @t539 () (= @t489 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t540 () (= @t487 tptp.top_top_set_nat)) % 0.46/0.97 (define @t541 () (_ tptp.member_nat @t484)) % 0.46/0.97 (define @t542 () (=> (_ @t541 @t173) (_ @t541 @t300))) % 0.46/0.97 (define @t543 () (@list @t173 @t300 @t484)) % 0.46/0.97 (define @t544 () (@var "C" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t545 () (_ tptp.member266900804lle_tv @t544)) % 0.46/0.97 (define @t546 () (=> (_ @t545 @t180) (_ @t545 @t319))) % 0.46/0.97 (define @t547 () (@list @t180 @t319 @t544)) % 0.46/0.97 (define @t548 () (_ tptp.ord_less_eq_set_nat @t173)) % 0.46/0.97 (define @t549 () (_ @t548 @t300)) % 0.46/0.97 (define @t550 () (_ tptp.ord_le241064091lle_tv @t180)) % 0.46/0.97 (define @t551 () (_ @t550 @t319)) % 0.46/0.97 (define @t552 () (@var "F22" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t553 () (@var "F1" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t554 () (_ (_ tptp.inj_on772319074lle_tv @t552) tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t555 () (_ (_ tptp.inj_on772319074lle_tv @t553) tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t556 () (@var "F22" (-> tptp.nat tptp.nat))) % 0.46/0.97 (define @t557 () (_ (_ tptp.inj_on_nat_nat @t556) tptp.top_top_set_nat)) % 0.46/0.97 (define @t558 () (@var "F1" (-> tptp.nat tptp.nat))) % 0.46/0.97 (define @t559 () (_ (_ tptp.inj_on_nat_nat @t558) tptp.top_top_set_nat)) % 0.46/0.97 (define @t560 () (_ tptp.ord_less_eq_set_nat @t268)) % 0.46/0.97 (define @t561 () (_ tptp.ord_le241064091lle_tv @t263)) % 0.46/0.97 (define @t562 () (_ (_ tptp.ord_le241064091lle_tv tptp.top_to1057771083lle_tv) @t489)) % 0.46/0.97 (define @t563 () (_ (_ tptp.ord_less_eq_set_nat tptp.top_top_set_nat) @t487)) % 0.46/0.97 (define @t564 () (_ tptp.ord_le241064091lle_tv @t319)) % 0.46/0.97 (define @t565 () (_ tptp.ord_less_eq_set_nat @t300)) % 0.46/0.97 (define @t566 () (@var "B3" tptp.set_nat)) % 0.46/0.97 (define @t567 () (@var "T" tptp.nat)) % 0.46/0.97 (define @t568 () (_ tptp.member_nat @t567)) % 0.46/0.97 (define @t569 () (@var "A2" tptp.set_nat)) % 0.46/0.97 (define @t570 () (@list @t569 @t566)) % 0.46/0.97 (define @t571 () (@var "B3" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t572 () (@var "T" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t573 () (_ tptp.member266900804lle_tv @t572)) % 0.46/0.97 (define @t574 () (@var "A2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t575 () (@list @t574 @t571)) % 0.46/0.97 (define @t576 () (_ @t265 @t300)) % 0.46/0.97 (define @t577 () (_ @t257 @t319)) % 0.46/0.97 (define @t578 () (@var "C2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t579 () (@var "C2" tptp.set_nat)) % 0.46/0.97 (define @t580 () (@var "U" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t581 () (@var "S4" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t582 () (@var "T2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t583 () (@var "U" tptp.set_nat)) % 0.46/0.97 (define @t584 () (@var "S4" tptp.set_nat)) % 0.46/0.97 (define @t585 () (@var "T2" tptp.set_nat)) % 0.46/0.97 (define @t586 () (not (_ (_ tptp.inj_on772319074lle_tv @t4) tptp.top_to1057771083lle_tv))) % 0.46/0.97 (define @t587 () (lambda @t238 tptp.top_top_o)) % 0.46/0.97 (define @t588 () (lambda @t240 tptp.top_top_o)) % 0.46/0.97 (define @t589 () (@var "F2" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.97 (define @t590 () (@var "A2" tptp.set_Pr2014382200lle_tv)) % 0.46/0.97 (define @t591 () (lambda (@list @t589 @t590) (forall (@list @t128) (=> (_ (_ tptp.member1531318361lle_tv @t128) @t590) (forall (@list @t127) (=> (_ (_ tptp.member1531318361lle_tv @t127) @t590) (=> (= (_ @t589 @t128) (_ @t589 @t127)) @t129))))))) % 0.46/0.97 (define @t592 () (@var "F2" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.97 (define @t593 () (@var "A2" tptp.set_Pr1725653840tv_nat)) % 0.46/0.97 (define @t594 () (_ tptp.member737151281tv_nat @t137)) % 0.46/0.97 (define @t595 () (lambda (@list @t592 @t593) (forall @t345 (=> (_ @t594 @t593) (forall @t344 (=> (_ (_ tptp.member737151281tv_nat @t136) @t593) (=> (= (_ @t592 @t137) (_ @t592 @t136)) @t138))))))) % 0.46/0.97 (define @t596 () (@var "F2" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.97 (define @t597 () (@var "A2" tptp.set_Pr13445366lle_tv)) % 0.46/0.97 (define @t598 () (_ tptp.member813679063lle_tv @t140)) % 0.46/0.97 (define @t599 () (lambda (@list @t596 @t597) (forall @t348 (=> (_ @t598 @t597) (forall @t347 (=> (_ (_ tptp.member813679063lle_tv @t139) @t597) (=> (= (_ @t596 @t140) (_ @t596 @t139)) @t141))))))) % 0.46/0.97 (define @t600 () (@var "F2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.97 (define @t601 () (@var "A2" tptp.set_Pr1986765409at_nat)) % 0.46/0.97 (define @t602 () (lambda (@list @t600 @t601) (forall @t351 (=> (_ @t388 @t601) (forall @t350 (=> (_ (_ tptp.member701585322at_nat @t142) @t601) (=> (= (_ @t600 @t143) (_ @t600 @t142)) @t144))))))) % 0.46/0.97 (define @t603 () (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t604 () (_ (_ tptp.member_nat @t130) @t569)) % 0.46/0.97 (define @t605 () (_ @t239 @t569)) % 0.46/0.97 (define @t606 () (lambda (@list @t603 @t569) (forall @t240 (=> @t605 (forall @t338 (=> @t604 (=> (= (_ @t603 @t131) (_ @t603 @t130)) @t132))))))) % 0.46/0.97 (define @t607 () (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.97 (define @t608 () (_ @t607 @t146)) % 0.46/0.97 (define @t609 () (_ @t607 @t147)) % 0.46/0.97 (define @t610 () (= @t609 @t608)) % 0.46/0.97 (define @t611 () (=> @t610 @t148)) % 0.46/0.97 (define @t612 () (_ (_ tptp.member266900804lle_tv @t146) @t574)) % 0.46/0.97 (define @t613 () (forall @t328 (=> @t612 @t611))) % 0.46/0.97 (define @t614 () (_ @t237 @t574)) % 0.46/0.97 (define @t615 () (=> @t614 @t613)) % 0.46/0.97 (define @t616 () (forall @t238 @t615)) % 0.46/0.97 (define @t617 () (@list @t607 @t574)) % 0.46/0.97 (define @t618 () (lambda @t617 @t616)) % 0.46/0.97 (define @t619 () (@var "F2" (-> tptp.nat tptp.nat))) % 0.46/0.97 (define @t620 () (@list @t619 @t569)) % 0.46/0.97 (define @t621 () (lambda @t620 (forall @t240 (=> @t605 (forall @t338 (=> @t604 (=> (= (_ @t619 @t131) (_ @t619 @t130)) @t132))))))) % 0.46/0.97 (define @t622 () (lambda @t345 (_ @t594 tptp.top_to975729152tv_nat))) % 0.46/0.97 (define @t623 () (lambda @t348 (_ @t598 tptp.top_to1411004326lle_tv))) % 0.46/0.97 (define @t624 () (lambda @t351 (_ @t388 tptp.top_to1555900337at_nat))) % 0.46/0.97 (define @t625 () (@var "S3" tptp.nat)) % 0.46/0.97 (define @t626 () (@var "R3" tptp.nat)) % 0.46/0.97 (define @t627 () (and (_ (_ tptp.member_nat @t626) @t569) (_ (_ tptp.member_nat @t625) @t569) (_ (_ tptp.ord_less_nat @t626) @t625))) % 0.46/0.97 (define @t628 () (@list @t626 @t625)) % 0.46/0.97 (define @t629 () (lambda @t620 (forall @t628 (=> @t627 (_ (_ tptp.ord_less_nat (_ @t619 @t626)) (_ @t619 @t625)))))) % 0.46/0.97 (define @t630 () (@var "F2" (-> tptp.nat tptp.set_nat))) % 0.46/0.97 (define @t631 () (lambda (@list @t630 @t569) (forall @t628 (=> @t627 (_ (_ tptp.ord_less_set_nat (_ @t630 @t626)) (_ @t630 @t625)))))) % 0.46/0.97 (define @t632 () (@var "F2" (-> tptp.nat tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t633 () (lambda (@list @t632 @t569) (forall @t628 (=> @t627 (_ (_ tptp.ord_le727057319lle_tv (_ @t632 @t626)) (_ @t632 @t625)))))) % 0.46/0.97 (define @t634 () (@var "S3" tptp.set_nat)) % 0.46/0.97 (define @t635 () (@var "F2" (-> tptp.set_nat tptp.nat))) % 0.46/0.97 (define @t636 () (@var "R3" tptp.set_nat)) % 0.46/0.97 (define @t637 () (@var "A2" tptp.set_set_nat)) % 0.46/0.97 (define @t638 () (and (_ (_ tptp.member_set_nat @t636) @t637) (_ (_ tptp.member_set_nat @t634) @t637) (_ (_ tptp.ord_less_set_nat @t636) @t634))) % 0.46/0.97 (define @t639 () (@list @t636 @t634)) % 0.46/0.97 (define @t640 () (lambda (@list @t635 @t637) (forall @t639 (=> @t638 (_ (_ tptp.ord_less_nat (_ @t635 @t636)) (_ @t635 @t634)))))) % 0.46/0.97 (define @t641 () (@var "F2" (-> tptp.set_nat tptp.set_nat))) % 0.46/0.97 (define @t642 () (lambda (@list @t641 @t637) (forall @t639 (=> @t638 (_ (_ tptp.ord_less_set_nat (_ @t641 @t636)) (_ @t641 @t634)))))) % 0.46/0.97 (define @t643 () (@var "F2" (-> tptp.set_nat tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t644 () (lambda (@list @t643 @t637) (forall @t639 (=> @t638 (_ (_ tptp.ord_le727057319lle_tv (_ @t643 @t636)) (_ @t643 @t634)))))) % 0.46/0.97 (define @t645 () (@var "S3" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t646 () (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.nat))) % 0.46/0.97 (define @t647 () (@var "R3" tptp.set_Pa1764573435lle_tv)) % 0.46/0.97 (define @t648 () (@var "A2" tptp.set_se800614875lle_tv)) % 0.46/0.97 (define @t649 () (and (_ (_ tptp.member1875402276lle_tv @t647) @t648) (_ (_ tptp.member1875402276lle_tv @t645) @t648) (_ (_ tptp.ord_le727057319lle_tv @t647) @t645))) % 0.46/0.97 (define @t650 () (@list @t647 @t645)) % 0.46/0.97 (define @t651 () (lambda (@list @t646 @t648) (forall @t650 (=> @t649 (_ (_ tptp.ord_less_nat (_ @t646 @t647)) (_ @t646 @t645)))))) % 0.46/0.97 (define @t652 () (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.set_nat))) % 0.46/0.97 (define @t653 () (lambda (@list @t652 @t648) (forall @t650 (=> @t649 (_ (_ tptp.ord_less_set_nat (_ @t652 @t647)) (_ @t652 @t645)))))) % 0.46/0.97 (define @t654 () (@var "F2" (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv))) % 0.46/0.97 (define @t655 () (lambda (@list @t654 @t648) (forall @t650 (=> @t649 (_ (_ tptp.ord_le727057319lle_tv (_ @t654 @t647)) (_ @t654 @t645)))))) % 0.46/0.97 (define @t656 () (lambda @t570 (forall @t240 (=> @t605 (_ @t239 @t566))))) % 0.46/0.97 (define @t657 () (lambda @t575 (forall @t238 (=> @t614 (_ @t237 @t571))))) % 0.46/0.97 (define @t658 () (tptp.paraco1147068288nge_tv tptp.f @t1)) % 0.46/0.97 (define @t659 () (tptp.paraco1147068288nge_tv tptp.f @t2)) % 0.46/0.97 (define @t660 () (not @t7)) % 0.46/0.97 (define @t661 () (or @t660 @t3)) % 0.46/0.97 (define @t662 () (@var "BOUND_VARIABLE_8475" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t663 () (= @t147 @t662)) % 0.46/0.97 (define @t664 () (tptp.paraco1147068288nge_tv tptp.f @t662)) % 0.46/0.97 (define @t665 () (tptp.paraco1147068288nge_tv tptp.f @t147)) % 0.46/0.97 (define @t666 () (not (= @t665 @t664))) % 0.46/0.97 (define @t667 () (@var "BOUND_VARIABLE_20125" tptp.paraco1605129243lle_tv)) % 0.46/0.97 (define @t668 () (lambda (@list @t667) true)) % 0.46/0.97 (define @t669 () (tptp.collec1111687558lle_tv @t668)) % 0.46/0.97 (define @t670 () (_ tptp.collec1111687558lle_tv @t668)) % 0.46/0.97 (define @t671 () (tptp.member266900804lle_tv @t662 @t670)) % 0.46/0.97 (define @t672 () (not @t671)) % 0.46/0.97 (define @t673 () (tptp.member266900804lle_tv @t147 @t670)) % 0.46/0.97 (define @t674 () (not @t673)) % 0.46/0.97 (define @t675 () (or @t674 @t672 @t666 @t663)) % 0.46/0.97 (define @t676 () (@list @t147 @t662)) % 0.46/0.97 (define @t677 () (lambda @t238 true)) % 0.46/0.97 (define @t678 () (_ tptp.collec1111687558lle_tv @t677)) % 0.46/0.97 (define @t679 () (tptp.member266900804lle_tv @t662 @t678)) % 0.46/0.97 (define @t680 () (not @t679)) % 0.46/0.97 (define @t681 () (tptp.member266900804lle_tv @t147 @t678)) % 0.46/0.97 (define @t682 () (not @t681)) % 0.46/0.97 (define @t683 () (or @t682 @t680 @t666 @t663)) % 0.46/0.97 (define @t684 () (forall @t676 @t683)) % 0.46/0.97 (define @t685 () (_ @t587 @t16)) % 0.46/0.97 (define @t686 () (tptp.member266900804lle_tv @t662 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t687 () (not @t686)) % 0.46/0.97 (define @t688 () (tptp.member266900804lle_tv @t147 tptp.top_to1057771083lle_tv)) % 0.46/0.97 (define @t689 () (not @t688)) % 0.46/0.97 (define @t690 () (or @t689 @t687 @t666 @t663)) % 0.46/0.97 (define @t691 () (forall @t676 @t690)) % 0.46/0.97 (define @t692 () (not (tptp.member266900804lle_tv @t662 @t574))) % 0.46/0.97 (define @t693 () (tptp.member266900804lle_tv @t147 @t574)) % 0.46/0.97 (define @t694 () (not @t693)) % 0.46/0.97 (define @t695 () (@list @t574)) % 0.46/0.97 (define @t696 () (_ @t4 @t662)) % 0.46/0.97 (define @t697 () (_ @t4 @t147)) % 0.46/0.97 (define @t698 () (= @t697 @t696)) % 0.46/0.97 (define @t699 () (not @t698)) % 0.46/0.97 (define @t700 () (or @t694 @t692 @t699 @t663)) % 0.46/0.97 (define @t701 () (_ @t4 @t662)) % 0.46/0.97 (define @t702 () (_ @t4 @t147)) % 0.46/0.97 (define @t703 () (= @t702 @t701)) % 0.46/0.97 (define @t704 () (not @t703)) % 0.46/0.97 (define @t705 () (or @t694 @t692 @t704 @t663)) % 0.46/0.97 (define @t706 () (forall @t676 @t705)) % 0.46/0.97 (define @t707 () (lambda @t695 @t706)) % 0.46/0.97 (define @t708 () (_ @t607 @t147)) % 0.46/0.97 (define @t709 () (not (= @t708 (_ @t607 @t662)))) % 0.46/0.97 (define @t710 () (or @t694 @t692 @t709 @t663)) % 0.46/0.97 (define @t711 () (_ (lambda @t617 (forall @t676 @t710)) @t4)) % 0.46/0.97 (define @t712 () (or @t692 @t709 @t663)) % 0.46/0.97 (define @t713 () (or @t694 @t712)) % 0.46/0.97 (define @t714 () (forall @t676 @t713)) % 0.46/0.97 (define @t715 () (@list @t662)) % 0.46/0.97 (define @t716 () (forall @t715 @t713)) % 0.46/0.97 (define @t717 () (forall @t715 @t712)) % 0.46/0.97 (define @t718 () (or @t694 @t717)) % 0.46/0.97 (define @t719 () (_ @t607 @t146)) % 0.46/0.97 (define @t720 () (tptp.member266900804lle_tv @t146 @t574)) % 0.46/0.97 (define @t721 () (forall @t328 (or (not @t720) (not (= @t708 @t719)) @t148))) % 0.46/0.97 (define @t722 () (not @t614)) % 0.46/0.97 (define @t723 () (or @t722 @t721)) % 0.46/0.97 (define @t724 () (not @t610)) % 0.46/0.97 (define @t725 () (not @t612)) % 0.46/0.97 (define @t726 () (or @t725 @t724 @t148)) % 0.46/0.97 (define @t727 () (forall @t676 (or (not (tptp.member266900804lle_tv @t147 @t669)) (not (tptp.member266900804lle_tv @t662 @t669)) @t666 @t663))) % 0.46/0.97 (define @t728 () (@quantifiers_skolemize @t727 1)) % 0.46/0.97 (define @t729 () (@quantifiers_skolemize @t727 0)) % 0.46/0.97 (define @t730 () (= @t729 @t728)) % 0.46/0.97 (define @t731 () (= (tptp.paraco1147068288nge_tv tptp.f @t729) (tptp.paraco1147068288nge_tv tptp.f @t728))) % 0.46/0.97 (define @t732 () (not @t731)) % 0.46/0.97 (define @t733 () (@purify @t668)) % 0.46/0.97 (define @t734 () (tptp.collec1111687558lle_tv @t733)) % 0.46/0.97 (define @t735 () (or (not (tptp.member266900804lle_tv @t729 @t734)) (not (tptp.member266900804lle_tv @t728 @t734)) @t732 @t730)) % 0.46/0.97 (define @t736 () (not @t735)) % 0.46/0.97 (define @t737 () (not @t727)) % 0.46/0.97 (define @t738 () (tptp.member266900804lle_tv @t728 @t669)) % 0.46/0.97 (define @t739 () (not @t738)) % 0.46/0.97 (define @t740 () (tptp.member266900804lle_tv @t729 @t669)) % 0.46/0.97 (define @t741 () (not @t740)) % 0.46/0.97 (define @t742 () (or @t741 @t739 @t732 @t730)) % 0.46/0.97 (define @t743 () (not @t742)) % 0.46/0.97 (define @t744 () (@list true)) % 0.46/0.97 (define @t745 () (@list @t735)) % 0.46/0.97 (define @t746 () (or @t732 @t730)) % 0.46/0.97 (define @t747 () (not @t746)) % 0.46/0.97 (define @t748 () (forall @t8 (or (not (= @t659 @t658)) @t3))) % 0.46/0.97 (assume @p1 @t9) % 0.46/0.97 (assume @p2 (forall (@list @t10) (_ @t11 tptp.top_to975729152tv_nat))) % 0.46/0.97 (assume @p3 (forall (@list @t12) (_ @t13 tptp.top_to1411004326lle_tv))) % 0.46/0.97 (assume @p4 (forall (@list @t14) (_ @t15 tptp.top_to1555900337at_nat))) % 0.46/0.97 (assume @p5 (forall @t18 (_ @t17 tptp.top_to1057771083lle_tv))) % 0.46/0.97 (assume @p6 (forall @t21 (_ @t20 tptp.top_top_set_nat))) % 0.46/0.97 (assume @p7 (forall @t30 (=> @t29 (=> @t27 @t24)))) % 0.46/0.97 (assume @p8 (forall @t38 (=> @t37 (=> @t35 @t32)))) % 0.46/0.97 (assume @p9 (forall @t46 (=> @t45 (=> @t43 @t40)))) % 0.46/0.97 (assume @p10 (forall @t54 (=> @t53 (=> @t51 @t48)))) % 0.46/0.97 (assume @p11 (forall @t62 (=> @t61 (=> @t59 @t56)))) % 0.46/0.97 (assume @p12 (forall @t70 (=> @t69 (=> @t67 @t64)))) % 0.46/0.97 (assume @p13 (forall @t76 (=> @t75 (=> @t73 @t32)))) % 0.46/0.97 (assume @p14 (forall @t82 (=> (forall @t81 @t80) @t29))) % 0.46/0.97 (assume @p15 (forall @t90 (=> (forall @t89 @t88) @t37))) % 0.46/0.97 (assume @p16 (forall @t96 (=> (forall @t95 @t94) @t45))) % 0.46/0.97 (assume @p17 (forall @t102 (=> (forall @t101 @t100) @t53))) % 0.46/0.97 (assume @p18 (forall @t108 (=> (forall @t107 @t106) @t61))) % 0.46/0.97 (assume @p19 (forall @t114 (=> (forall @t113 @t112) @t69))) % 0.46/0.97 (assume @p20 (forall @t119 (=> (forall @t89 @t118) @t75))) % 0.46/0.97 (assume @p21 (forall @t30 (=> @t29 @t120))) % 0.46/0.97 (assume @p22 (forall @t38 (=> @t37 @t121))) % 0.46/0.97 (assume @p23 (forall @t46 (=> @t45 @t122))) % 0.46/0.97 (assume @p24 (forall @t54 (=> @t53 @t123))) % 0.46/0.97 (assume @p25 (forall @t62 (=> @t61 @t124))) % 0.46/0.97 (assume @p26 (forall @t70 (=> @t69 @t125))) % 0.46/0.97 (assume @p27 (forall @t76 (=> @t75 @t126))) % 0.46/0.97 (assume @p28 (forall @t82 (= @t29 (forall (@list @t128 @t127) (=> (= (_ @t25 @t128) (_ @t25 @t127)) @t129))))) % 0.46/0.97 (assume @p29 (forall @t90 (= @t37 (forall @t135 (=> (= @t134 @t133) @t132))))) % 0.46/0.97 (assume @p30 (forall @t96 (= @t45 (forall (@list @t137 @t136) (=> (= (_ @t41 @t137) (_ @t41 @t136)) @t138))))) % 0.46/0.97 (assume @p31 (forall @t102 (= @t53 (forall (@list @t140 @t139) (=> (= (_ @t49 @t140) (_ @t49 @t139)) @t141))))) % 0.46/0.97 (assume @p32 (forall @t108 (= @t61 (forall (@list @t143 @t142) (=> (= @t145 (_ @t57 @t142)) @t144))))) % 0.46/0.97 (assume @p33 (forall @t114 (= @t69 (forall (@list @t147 @t146) (=> (= @t150 @t149) @t148))))) % 0.46/0.97 (assume @p34 (forall @t119 (= @t75 (forall @t135 (=> (= @t152 @t151) @t132))))) % 0.46/0.97 (assume @p35 (forall @t157 (=> @t156 (=> @t27 (=> @t155 (=> @t154 @t24)))))) % 0.46/0.97 (assume @p36 (forall @t162 (=> @t161 (=> @t43 (=> @t160 (=> @t159 @t40)))))) % 0.46/0.97 (assume @p37 (forall @t167 (=> @t166 (=> @t51 (=> @t165 (=> @t164 @t48)))))) % 0.46/0.97 (assume @p38 (forall @t172 (=> @t171 (=> @t59 (=> @t170 (=> @t169 @t56)))))) % 0.46/0.97 (assume @p39 (forall @t179 (=> @t178 (=> @t35 @t177)))) % 0.46/0.97 (assume @p40 (forall @t185 (=> @t184 (=> @t67 (=> @t183 (=> @t182 @t64)))))) % 0.46/0.97 (assume @p41 (forall @t187 (=> @t186 (=> @t73 @t177)))) % 0.46/0.97 (assume @p42 (forall (@list @t153 @t25) (=> (forall @t81 (=> @t188 (=> (_ (_ tptp.member1531318361lle_tv @t77) @t153) @t80))) @t156))) % 0.46/0.97 (assume @p43 (forall (@list @t158 @t41) (=> (forall @t95 (=> @t190 (=> (_ (_ tptp.member737151281tv_nat @t91) @t158) @t94))) @t161))) % 0.46/0.97 (assume @p44 (forall (@list @t163 @t49) (=> (forall @t101 (=> @t192 (=> (_ (_ tptp.member813679063lle_tv @t97) @t163) @t100))) @t166))) % 0.46/0.97 (assume @p45 (forall (@list @t168 @t57) (=> (forall @t107 (=> @t194 (=> (_ (_ tptp.member701585322at_nat @t103) @t168) @t106))) @t171))) % 0.46/0.97 (assume @p46 (forall (@list @t173 @t33) (=> (forall @t89 (=> @t197 (=> @t195 @t88))) @t178))) % 0.46/0.97 (assume @p47 (forall (@list @t180 @t65) (=> (forall @t113 (=> @t199 (=> (_ (_ tptp.member266900804lle_tv @t109) @t180) @t112))) @t184))) % 0.46/0.97 (assume @p48 (forall @t200 (=> (forall @t89 (=> @t197 (=> @t195 @t118))) @t186))) % 0.46/0.97 (assume @p49 (forall (@list @t153 @t25 @t201) (=> (forall (@list @t202) (=> (_ (_ tptp.member1531318361lle_tv @t202) @t153) (= (_ @t25 @t202) (_ @t201 @t202)))) (= @t156 (_ (_ tptp.inj_on2112487900lle_tv @t201) @t153))))) % 0.46/0.97 (assume @p50 (forall (@list @t158 @t41 @t203) (=> (forall (@list @t204) (=> (_ (_ tptp.member737151281tv_nat @t204) @t158) (= (_ @t41 @t204) (_ @t203 @t204)))) (= @t161 (_ (_ tptp.inj_on552895452tv_nat @t203) @t158))))) % 0.46/0.97 (assume @p51 (forall (@list @t163 @t49 @t205) (=> (forall (@list @t206) (=> (_ (_ tptp.member813679063lle_tv @t206) @t163) (= (_ @t49 @t206) (_ @t205 @t206)))) (= @t166 (_ (_ tptp.inj_on1745913142lle_tv @t205) @t163))))) % 0.46/0.97 (assume @p52 (forall (@list @t168 @t57 @t207) (=> (forall (@list @t208) (=> (_ (_ tptp.member701585322at_nat @t208) @t168) (= (_ @t57 @t208) (_ @t207 @t208)))) (= @t171 (_ (_ tptp.inj_on26176689at_nat @t207) @t168))))) % 0.46/0.97 (assume @p53 (forall (@list @t173 @t33 @t209) (=> (forall @t212 (=> @t211 (= (_ @t33 @t210) (_ @t209 @t210)))) (= @t178 (_ (_ tptp.inj_on1955349912lle_tv @t209) @t173))))) % 0.46/0.97 (assume @p54 (forall (@list @t173 @t71 @t213) (=> (forall @t212 (=> @t211 (= (_ @t71 @t210) (_ @t213 @t210)))) (= @t186 @t215)))) % 0.46/0.97 (assume @p55 (forall (@list @t180 @t65 @t216) (=> (forall (@list @t219) (=> (_ (_ tptp.member266900804lle_tv @t219) @t180) (= (_ @t65 @t219) (_ @t216 @t219)))) (= @t184 @t218)))) % 0.46/0.97 (assume @p56 (forall @t157 (=> @t156 (=> @t155 (=> @t154 @t120))))) % 0.46/0.97 (assume @p57 (forall @t162 (=> @t161 (=> @t160 (=> @t159 @t122))))) % 0.46/0.97 (assume @p58 (forall @t167 (=> @t166 (=> @t165 (=> @t164 @t123))))) % 0.46/0.97 (assume @p59 (forall @t172 (=> @t171 (=> @t170 (=> @t169 @t124))))) % 0.46/0.97 (assume @p60 (forall @t179 (=> @t178 (=> @t176 (=> @t175 @t121))))) % 0.46/0.97 (assume @p61 (forall @t187 (=> @t186 (=> @t176 (=> @t175 @t126))))) % 0.46/0.97 (assume @p62 (forall @t185 (=> @t184 (=> @t183 (=> @t182 @t125))))) % 0.46/0.97 (assume @p63 (_ (_ tptp.inj_on_nat_nat tptp.f) tptp.top_top_set_nat)) % 0.46/0.97 (assume @p64 (= tptp.top_to975729152tv_nat (_ tptp.collec848462447tv_nat tptp.top_to900819589_nat_o))) % 0.46/0.97 (assume @p65 (= tptp.top_to1411004326lle_tv (_ tptp.collec924990229lle_tv tptp.top_to1889334367e_tv_o))) % 0.46/0.97 (assume @p66 (= tptp.top_to1555900337at_nat (_ tptp.collec7649004at_nat tptp.top_to632227436_nat_o))) % 0.46/0.97 (assume @p67 @t220) % 0.46/0.97 (assume @p68 (= tptp.top_top_set_nat (_ tptp.collect_nat tptp.top_top_nat_o))) % 0.46/0.97 (assume @p69 (exists @t221 (_ @t189 tptp.top_to975729152tv_nat))) % 0.46/0.97 (assume @p70 (exists @t222 (_ @t191 tptp.top_to1411004326lle_tv))) % 0.46/0.97 (assume @p71 (exists @t223 (_ @t193 tptp.top_to1555900337at_nat))) % 0.46/0.97 (assume @p72 (exists @t224 (_ @t198 tptp.top_to1057771083lle_tv))) % 0.46/0.97 (assume @p73 (exists @t225 (_ @t196 tptp.top_top_set_nat))) % 0.46/0.97 (assume @p74 (forall (@list @t158) (=> (forall @t221 @t190) (= tptp.top_to975729152tv_nat @t158)))) % 0.46/0.97 (assume @p75 (forall (@list @t163) (=> (forall @t222 @t192) (= tptp.top_to1411004326lle_tv @t163)))) % 0.46/0.97 (assume @p76 (forall (@list @t168) (=> (forall @t223 @t194) (= tptp.top_to1555900337at_nat @t168)))) % 0.46/0.97 (assume @p77 (forall @t226 (=> (forall @t224 @t199) (= tptp.top_to1057771083lle_tv @t180)))) % 0.46/0.97 (assume @p78 (forall @t227 (=> (forall @t225 @t197) (= tptp.top_top_set_nat @t173)))) % 0.46/0.97 (assume @p79 (forall (@list @t153 @t201 @t25) (=> (forall (@list @t78) (=> @t188 (= (_ @t201 @t79) @t78))) @t156))) % 0.46/0.97 (assume @p80 (forall (@list @t158 @t203 @t41) (=> (forall @t221 (=> @t190 (= (_ @t203 @t93) @t92))) @t161))) % 0.46/0.97 (assume @p81 (forall (@list @t163 @t205 @t49) (=> (forall @t222 (=> @t192 (= (_ @t205 @t99) @t98))) @t166))) % 0.46/0.97 (assume @p82 (forall (@list @t168 @t207 @t57) (=> (forall @t223 (=> @t194 (= (_ @t207 @t105) @t104))) @t171))) % 0.46/0.97 (assume @p83 (forall (@list @t173 @t228 @t33) (=> (forall @t225 (=> @t197 @t229)) @t178))) % 0.46/0.97 (assume @p84 (forall @t232 (=> (forall @t225 (=> @t197 @t231)) @t186))) % 0.46/0.97 (assume @p85 (forall @t235 (=> (forall @t224 (=> @t199 @t234)) @t184))) % 0.46/0.97 (assume @p86 (forall @t157 (=> @t156 (=> (not @t24) (=> @t155 (=> @t154 (not @t27))))))) % 0.46/0.97 (assume @p87 (forall @t162 (=> @t161 (=> (not @t40) (=> @t160 (=> @t159 (not @t43))))))) % 0.46/0.97 (assume @p88 (forall @t167 (=> @t166 (=> (not @t48) (=> @t165 (=> @t164 (not @t51))))))) % 0.46/0.97 (assume @p89 (forall @t172 (=> @t171 (=> (not @t56) (=> @t170 (=> @t169 (not @t59))))))) % 0.46/0.97 (assume @p90 (forall @t179 (=> @t178 (=> @t236 (=> @t176 (=> @t175 (not @t35))))))) % 0.46/0.97 (assume @p91 (forall @t187 (=> @t186 (=> @t236 (=> @t176 (=> @t175 (not @t73))))))) % 0.46/0.97 (assume @p92 (forall @t185 (=> @t184 (=> (not @t64) (=> @t183 (=> @t182 (not @t67))))))) % 0.46/0.97 (assume @p93 (= tptp.top_to1299250770e_tv_o (lambda @t238 (_ @t237 tptp.top_to1057771083lle_tv)))) % 0.46/0.97 (assume @p94 (= tptp.top_top_nat_o (lambda @t240 (_ @t239 tptp.top_top_set_nat)))) % 0.46/0.97 (assume @p95 (forall (@list @t25 @t23) (=> @t29 (= (_ (_ (_ tptp.the_in427240730lle_tv tptp.top_to1871154984lle_tv) @t25) @t26) @t23)))) % 0.46/0.97 (assume @p96 (forall @t245 (=> @t244 (= (_ (_ (_ tptp.the_in1509933432tv_nat tptp.top_to1057771083lle_tv) @t241) @t242) @t16)))) % 0.46/0.97 (assume @p97 (forall @t246 (=> @t37 (= (_ (_ (_ tptp.the_in138087638lle_tv tptp.top_top_set_nat) @t33) @t34) @t19)))) % 0.46/0.97 (assume @p98 (forall (@list @t41 @t10) (=> @t45 (= (_ (_ (_ tptp.the_in195660058tv_nat tptp.top_to975729152tv_nat) @t41) @t42) @t10)))) % 0.46/0.97 (assume @p99 (forall (@list @t49 @t12) (=> @t53 (= (_ (_ (_ tptp.the_in1388677748lle_tv tptp.top_to1411004326lle_tv) @t49) @t50) @t12)))) % 0.46/0.97 (assume @p100 (forall (@list @t57 @t14) (=> @t61 (= (_ (_ (_ tptp.the_in2068894451at_nat tptp.top_to1555900337at_nat) @t57) @t58) @t14)))) % 0.46/0.97 (assume @p101 (forall @t247 (=> @t69 (= (_ (_ (_ tptp.the_in452116896lle_tv tptp.top_to1057771083lle_tv) @t65) @t66) @t16)))) % 0.46/0.97 (assume @p102 (forall @t248 (=> @t75 (= (_ (_ (_ tptp.the_inv_into_nat_nat tptp.top_top_set_nat) @t71) @t72) @t19)))) % 0.46/0.97 (assume @p103 (forall @t250 (=> @t249 @t186))) % 0.46/0.97 (assume @p104 (forall @t90 (=> (forall @t89 (=> @t251 (not @t87))) @t37))) % 0.46/0.97 (assume @p105 (forall @t119 (=> (forall @t89 (=> @t251 @t252)) @t75))) % 0.46/0.97 (assume @p106 (forall (@list @t253) (_ @t254 tptp.top_top_set_nat))) % 0.46/0.97 (assume @p107 (forall (@list @t71 @t255) (= (_ (_ tptp.paraco1147068288nge_tv @t71) (_ tptp.paraco793048302_Indet @t255)) (_ tptp.paraco793048302_Indet (_ @t71 @t255))))) % 0.46/0.97 (assume @p108 (forall @t114 (= (_ (_ tptp.inj_on2112487900lle_tv (_ tptp.produc1408152463lle_tv @t65)) tptp.top_to1871154984lle_tv) @t69))) % 0.46/0.97 (assume @p109 (forall @t90 (= (_ (_ tptp.inj_on967082628lle_tv (_ tptp.produc1804670661lle_tv @t33)) tptp.top_to975729152tv_nat) @t37))) % 0.46/0.97 (assume @p110 (forall @t119 (= (_ (_ tptp.inj_on552895452tv_nat (_ tptp.produc237097339lle_tv @t71)) tptp.top_to975729152tv_nat) @t75))) % 0.46/0.97 (assume @p111 (forall @t114 (= (_ (_ tptp.inj_on1745913142lle_tv (_ tptp.produc2040316391tv_nat @t65)) tptp.top_to1411004326lle_tv) @t69))) % 0.46/0.97 (assume @p112 (forall @t90 (= (_ (_ tptp.inj_on1840679568lle_tv (_ tptp.produc1608943133tv_nat @t33)) tptp.top_to1555900337at_nat) @t37))) % 0.46/0.97 (assume @p113 (forall @t119 (= (_ (_ tptp.inj_on26176689at_nat (_ tptp.produc1320959600at_nat @t71)) tptp.top_to1555900337at_nat) @t75))) % 0.46/0.97 (assume @p114 (forall (@list @t241 @t256 @t180) (=> @t244 @t261))) % 0.46/0.97 (assume @p115 (forall (@list @t65 @t256 @t180) (=> @t69 @t264))) % 0.46/0.97 (assume @p116 (forall (@list @t71 @t253 @t173) (=> @t75 @t269))) % 0.46/0.97 (assume @p117 (forall (@list @t33 @t253 @t173) (=> @t37 @t272))) % 0.46/0.97 (assume @p118 (forall (@list @t275 @t273 @t158) (=> @t277 (= (_ (_ tptp.member_nat (_ @t275 @t273)) (_ @t276 @t158)) @t274)))) % 0.46/0.97 (assume @p119 (forall (@list @t278 @t273 @t158) (=> @t280 (= (_ (_ tptp.member266900804lle_tv (_ @t278 @t273)) (_ @t279 @t158)) @t274)))) % 0.46/0.97 (assume @p120 (forall (@list @t283 @t281 @t163) (=> @t285 (= (_ (_ tptp.member_nat (_ @t283 @t281)) (_ @t284 @t163)) @t282)))) % 0.46/0.97 (assume @p121 (forall (@list @t286 @t281 @t163) (=> @t288 (= (_ (_ tptp.member266900804lle_tv (_ @t286 @t281)) (_ @t287 @t163)) @t282)))) % 0.46/0.97 (assume @p122 (forall (@list @t291 @t289 @t168) (=> @t293 (= (_ (_ tptp.member_nat (_ @t291 @t289)) (_ @t292 @t168)) @t290)))) % 0.46/0.97 (assume @p123 (forall (@list @t294 @t289 @t168) (=> @t296 (= (_ (_ tptp.member266900804lle_tv (_ @t294 @t289)) (_ @t295 @t168)) @t290)))) % 0.46/0.97 (assume @p124 (forall (@list @t25 @t153 @t297) (=> @t29 (= (= @t299 (_ @t298 @t297)) (= @t153 @t297))))) % 0.46/0.97 (assume @p125 (forall (@list @t33 @t173 @t300) (=> @t37 (= (= @t271 (_ @t270 @t300)) @t301)))) % 0.46/0.97 (assume @p126 (forall (@list @t41 @t158 @t302) (=> @t45 (= (= @t304 (_ @t303 @t302)) (= @t158 @t302))))) % 0.46/0.97 (assume @p127 (forall (@list @t49 @t163 @t305) (=> @t53 (= (= (_ @t306 @t163) (_ @t306 @t305)) (= @t163 @t305))))) % 0.46/0.97 (assume @p128 (forall (@list @t309 @t168 @t307) (=> (_ @t312 tptp.top_to1555900337at_nat) (= (= @t311 (_ @t310 @t307)) @t308)))) % 0.46/0.97 (assume @p129 (forall (@list @t313 @t168 @t307) (=> (_ @t316 tptp.top_to1555900337at_nat) (= (= @t315 (_ @t314 @t307)) @t308)))) % 0.46/0.97 (assume @p130 (forall (@list @t57 @t168 @t307) (=> @t61 (= (= @t318 (_ @t317 @t307)) @t308)))) % 0.46/0.97 (assume @p131 (forall @t322 (=> @t69 @t321))) % 0.46/0.97 (assume @p132 (forall @t325 (=> @t75 @t324))) % 0.46/0.97 (assume @p133 (forall (@list @t241 @t327) (=> @t244 (= @t332 (exists @t238 (and (= @t327 @t329) (forall @t328 (=> (= @t327 (_ @t241 @t146)) @t326)))))))) % 0.46/0.97 (assume @p134 (forall (@list @t65 @t333) (=> @t69 (= @t336 (exists @t238 (and (= @t333 @t150) (forall @t328 (=> (= @t333 @t149) @t326)))))))) % 0.46/0.97 (assume @p135 (forall (@list @t71 @t327) (=> @t75 (= @t340 (exists @t240 (and (= @t327 @t152) (forall @t338 (=> (= @t327 @t151) @t337)))))))) % 0.46/0.97 (assume @p136 (forall (@list @t33 @t333) (=> @t37 (= @t342 (exists @t240 (and (= @t333 @t134) (forall @t338 (=> (= @t333 @t133) @t337)))))))) % 0.46/0.97 (assume @p137 (forall (@list @t275 @t327) (=> @t277 (= (_ @t331 (_ @t276 tptp.top_to975729152tv_nat)) (exists @t345 (and (= @t327 (_ @t275 @t137)) (forall @t344 (=> (= @t327 (_ @t275 @t136)) @t343)))))))) % 0.46/0.97 (assume @p138 (forall (@list @t278 @t333) (=> @t280 (= (_ @t335 (_ @t279 tptp.top_to975729152tv_nat)) (exists @t345 (and (= @t333 (_ @t278 @t137)) (forall @t344 (=> (= @t333 (_ @t278 @t136)) @t343)))))))) % 0.46/0.97 (assume @p139 (forall (@list @t283 @t327) (=> @t285 (= (_ @t331 (_ @t284 tptp.top_to1411004326lle_tv)) (exists @t348 (and (= @t327 (_ @t283 @t140)) (forall @t347 (=> (= @t327 (_ @t283 @t139)) @t346)))))))) % 0.46/0.97 (assume @p140 (forall (@list @t286 @t333) (=> @t288 (= (_ @t335 (_ @t287 tptp.top_to1411004326lle_tv)) (exists @t348 (and (= @t333 (_ @t286 @t140)) (forall @t347 (=> (= @t333 (_ @t286 @t139)) @t346)))))))) % 0.46/0.97 (assume @p141 (forall (@list @t291 @t327) (=> @t293 (= (_ @t331 (_ @t292 tptp.top_to1555900337at_nat)) (exists @t351 (and (= @t327 (_ @t291 @t143)) (forall @t350 (=> (= @t327 (_ @t291 @t142)) @t349)))))))) % 0.46/0.97 (assume @p142 (forall (@list @t294 @t333) (=> @t296 (= (_ @t335 (_ @t295 tptp.top_to1555900337at_nat)) (exists @t351 (and (= @t333 (_ @t294 @t143)) (forall @t350 (=> (= @t333 (_ @t294 @t142)) @t349)))))))) % 0.46/0.97 (assume @p143 (forall @t250 (=> @t352 @t186))) % 0.46/0.97 (assume @p144 (forall (@list @t353 @t309 @t14 @t168) (=> @t356 (=> @t170 @t354)))) % 0.46/0.97 (assume @p145 (forall (@list @t357 @t313 @t14 @t168) (=> @t360 (=> @t170 @t358)))) % 0.46/0.97 (assume @p146 (forall (@list @t361 @t57 @t14 @t168) (=> @t363 (=> @t170 @t362)))) % 0.46/0.97 (assume @p147 (forall (@list @t327 @t71 @t19 @t173) (=> @t365 (=> @t176 @t364)))) % 0.46/0.97 (assume @p148 (forall (@list @t333 @t33 @t19 @t173) (=> @t367 (=> @t176 @t366)))) % 0.46/0.97 (assume @p149 (forall (@list @t327 @t241 @t16 @t180) (=> @t369 (=> @t183 @t368)))) % 0.46/0.97 (assume @p150 (forall (@list @t333 @t65 @t16 @t180) (=> @t371 (=> @t183 @t370)))) % 0.46/0.97 (assume @p151 (forall (@list @t373 @t372) (= (= (_ tptp.paraco793048302_Indet @t373) (_ tptp.paraco793048302_Indet @t372)) (= @t373 @t372)))) % 0.46/0.97 (assume @p152 @t374) % 0.46/0.97 (assume @p153 (forall @t21 (_ tptp.top_top_nat_o @t19))) % 0.46/0.97 (assume @p154 (forall @t376 (=> @t184 (= (_ (_ tptp.image_335818702lle_tv @t375) @t263) @t180)))) % 0.46/0.97 (assume @p155 (forall @t250 (=> @t186 (= (_ (_ tptp.image_nat_nat @t377) @t268) @t173)))) % 0.46/0.97 (assume @p156 (forall (@list @t33 @t173) (=> @t178 (= (_ (_ tptp.image_376325286tv_nat @t378) @t271) @t173)))) % 0.46/0.97 (assume @p157 (forall (@list @t241 @t180) (=> @t380 (= (_ (_ tptp.image_1151963140lle_tv @t379) @t260) @t180)))) % 0.46/0.97 (assume @p158 (forall (@list @t309 @t168) (=> (_ @t312 @t168) (= (_ (_ tptp.image_1805124128at_nat (_ (_ tptp.the_in667485224tv_nat @t168) @t309)) @t311) @t168)))) % 0.46/0.97 (assume @p159 (forall (@list @t313 @t168) (=> (_ @t316 @t168) (= (_ (_ tptp.image_1787705850at_nat (_ (_ tptp.the_in744013006lle_tv @t168) @t313)) @t315) @t168)))) % 0.46/0.97 (assume @p160 (forall (@list @t381 @t158) (=> (_ (_ tptp.inj_on1971554740at_nat @t381) @t158) (= (_ (_ tptp.image_1597721174tv_nat (_ (_ tptp.the_in874888178at_nat @t158) @t381)) (_ (_ tptp.image_1805124128at_nat @t381) @t158)) @t158)))) % 0.46/0.97 (assume @p161 (forall (@list @t382 @t163) (=> (_ (_ tptp.inj_on1954136462at_nat @t382) @t163) (= (_ (_ tptp.image_1674248956lle_tv (_ (_ tptp.the_in857469900at_nat @t163) @t382)) (_ (_ tptp.image_1787705850at_nat @t382) @t163)) @t163)))) % 0.46/0.97 (assume @p162 (forall (@list @t25 @t153) (=> @t156 (= (_ (_ tptp.image_1221801032lle_tv (_ (_ tptp.the_in427240730lle_tv @t153) @t25)) @t299) @t153)))) % 0.46/0.97 (assume @p163 (forall (@list @t41 @t158) (=> @t161 (= (_ (_ tptp.image_1104296520tv_nat (_ (_ tptp.the_in195660058tv_nat @t158) @t41)) @t304) @t158)))) % 0.46/0.97 (assume @p164 (forall (@list @t14 @t168 @t309) (=> @t170 (_ (_ tptp.member737151281tv_nat @t355) @t311)))) % 0.46/0.97 (assume @p165 (forall (@list @t14 @t168 @t313) (=> @t170 (_ (_ tptp.member813679063lle_tv @t359) @t315)))) % 0.46/0.97 (assume @p166 (forall (@list @t14 @t168 @t57) (=> @t170 (_ (_ tptp.member701585322at_nat @t58) @t318)))) % 0.46/0.97 (assume @p167 (forall (@list @t19 @t173 @t71) (=> @t176 (_ @t383 @t268)))) % 0.46/0.97 (assume @p168 (forall (@list @t19 @t173 @t33) (=> @t176 (_ @t384 @t271)))) % 0.46/0.97 (assume @p169 (forall (@list @t16 @t180 @t241) (=> @t183 (_ @t385 @t260)))) % 0.46/0.97 (assume @p170 (forall (@list @t16 @t180 @t65) (=> @t183 (_ @t386 @t263)))) % 0.46/0.97 (assume @p171 (forall (@list @t387 @t309 @t168) (= (_ (_ tptp.member737151281tv_nat @t387) @t311) (exists @t351 (and @t389 (= @t387 (_ @t309 @t143))))))) % 0.46/0.97 (assume @p172 (forall (@list @t390 @t313 @t168) (= (_ (_ tptp.member813679063lle_tv @t390) @t315) (exists @t351 (and @t389 (= @t390 (_ @t313 @t143))))))) % 0.46/0.97 (assume @p173 (forall (@list @t391 @t57 @t168) (= (_ (_ tptp.member701585322at_nat @t391) @t318) (exists @t351 (and @t389 (= @t391 @t145)))))) % 0.46/0.97 (assume @p174 (forall (@list @t392 @t71 @t173) (= (_ (_ tptp.member_nat @t392) @t268) (exists @t240 (and @t393 (= @t392 @t152)))))) % 0.46/0.97 (assume @p175 (forall (@list @t394 @t33 @t173) (= (_ (_ tptp.member266900804lle_tv @t394) @t271) (exists @t240 (and @t393 (= @t394 @t134)))))) % 0.46/0.97 (assume @p176 (forall @t398 (=> (exists (@list @t397) (and (_ (_ tptp.member737151281tv_nat @t397) @t311) (_ @t396 @t397))) (exists @t223 (and @t194 (_ @t396 @t395)))))) % 0.46/0.97 (assume @p177 (forall @t402 (=> (exists (@list @t401) (and (_ (_ tptp.member813679063lle_tv @t401) @t315) (_ @t400 @t401))) (exists @t223 (and @t194 (_ @t400 @t399)))))) % 0.46/0.97 (assume @p178 (forall @t407 (=> (exists @t406 (and (_ @t405 @t318) (_ @t403 @t404))) (exists @t223 (and @t194 (_ @t403 @t105)))))) % 0.46/0.97 (assume @p179 (forall @t410 (=> (exists (@list @t409) (and (_ (_ tptp.member266900804lle_tv @t409) @t271) (_ @t408 @t409))) (exists @t225 (and @t197 (_ @t408 @t86)))))) % 0.46/0.97 (assume @p180 (forall @t415 (=> (exists @t414 (and (_ @t413 @t268) (_ @t411 @t412))) (exists @t225 (and @t197 (_ @t411 @t116)))))) % 0.46/0.97 (assume @p181 (forall (@list @t418 @t416 @t309 @t417) (=> @t420 (=> (forall @t223 (=> @t419 (= @t395 (_ @t417 @t104)))) (= (_ @t310 @t418) (_ (_ tptp.image_1597721174tv_nat @t417) @t416)))))) % 0.46/0.97 (assume @p182 (forall (@list @t418 @t416 @t313 @t421) (=> @t420 (=> (forall @t223 (=> @t419 (= @t399 (_ @t421 @t104)))) (= (_ @t314 @t418) (_ (_ tptp.image_1674248956lle_tv @t421) @t416)))))) % 0.46/0.97 (assume @p183 (forall (@list @t418 @t416 @t57 @t207) (=> @t420 (=> (forall @t223 (=> @t419 (= @t105 (_ @t207 @t104)))) (= (_ @t317 @t418) (_ (_ tptp.image_815163717at_nat @t207) @t416)))))) % 0.46/0.97 (assume @p184 (forall (@list @t424 @t422 @t33 @t209) (=> @t426 (=> (forall @t225 (=> @t425 (= @t86 (_ @t209 @t84)))) (= (_ @t270 @t424) (_ @t423 @t422)))))) % 0.46/0.97 (assume @p185 (forall (@list @t424 @t422 @t71 @t213) (=> @t426 (=> (forall @t225 (=> @t425 (= @t116 @t428))) (= (_ @t267 @t424) (_ @t427 @t422)))))) % 0.46/0.97 (assume @p186 (forall @t398 (=> (forall @t221 (=> (_ @t189 @t311) (_ @t396 @t92))) (forall @t406 (=> @t429 (_ @t396 (_ @t309 @t404))))))) % 0.46/0.97 (assume @p187 (forall @t402 (=> (forall @t222 (=> (_ @t191 @t315) (_ @t400 @t98))) (forall @t406 (=> @t429 (_ @t400 (_ @t313 @t404))))))) % 0.46/0.97 (assume @p188 (forall @t407 (=> (forall @t223 (=> (_ @t193 @t318) (_ @t403 @t104))) (forall @t406 (=> @t429 (_ @t403 (_ @t57 @t404))))))) % 0.46/0.97 (assume @p189 (forall @t410 (=> (forall @t224 (=> (_ @t198 @t271) @t431)) (forall @t414 (=> @t430 (_ @t408 (_ @t33 @t412))))))) % 0.46/0.97 (assume @p190 (forall @t415 (=> (forall @t225 (=> (_ @t196 @t268) @t432)) (forall @t414 (=> @t430 (_ @t411 (_ @t71 @t412))))))) % 0.46/0.97 (assume @p191 (forall (@list @t14 @t168 @t353 @t309) (=> @t170 (=> @t356 @t354)))) % 0.46/0.97 (assume @p192 (forall (@list @t14 @t168 @t357 @t313) (=> @t170 (=> @t360 @t358)))) % 0.46/0.97 (assume @p193 (forall (@list @t14 @t168 @t361 @t57) (=> @t170 (=> @t363 @t362)))) % 0.46/0.97 (assume @p194 (forall (@list @t19 @t173 @t327 @t71) (=> @t176 (=> @t365 @t364)))) % 0.46/0.97 (assume @p195 (forall (@list @t19 @t173 @t333 @t33) (=> @t176 (=> @t367 @t366)))) % 0.46/0.97 (assume @p196 (forall (@list @t16 @t180 @t327 @t241) (=> @t183 (=> @t369 @t368)))) % 0.46/0.97 (assume @p197 (forall (@list @t16 @t180 @t333 @t65) (=> @t183 (=> @t371 @t370)))) % 0.46/0.97 (assume @p198 (forall (@list @t71 @t173 @t434 @t433) (=> @t249 (=> @t437 (=> @t436 (=> @t435 (_ (_ tptp.ord_less_nat (_ @t71 @t434)) (_ @t71 @t433)))))))) % 0.46/0.97 (assume @p199 (forall (@list @t438 @t173 @t434 @t433) (=> @t439 (=> @t437 (=> @t436 (=> @t435 (_ (_ tptp.ord_less_set_nat (_ @t438 @t434)) (_ @t438 @t433)))))))) % 0.46/0.97 (assume @p200 (forall (@list @t440 @t173 @t434 @t433) (=> @t441 (=> @t437 (=> @t436 (=> @t435 (_ (_ tptp.ord_le727057319lle_tv (_ @t440 @t434)) (_ @t440 @t433)))))))) % 0.46/0.97 (assume @p201 (forall (@list @t443 @t446 @t444 @t442) (=> @t449 (=> @t448 (=> @t447 (=> @t445 (_ (_ tptp.ord_less_nat (_ @t443 @t444)) (_ @t443 @t442)))))))) % 0.46/0.97 (assume @p202 (forall (@list @t450 @t446 @t444 @t442) (=> @t451 (=> @t448 (=> @t447 (=> @t445 (_ (_ tptp.ord_less_set_nat (_ @t450 @t444)) (_ @t450 @t442)))))))) % 0.46/0.97 (assume @p203 (forall (@list @t452 @t446 @t444 @t442) (=> @t453 (=> @t448 (=> @t447 (=> @t445 (_ (_ tptp.ord_le727057319lle_tv (_ @t452 @t444)) (_ @t452 @t442)))))))) % 0.46/0.97 (assume @p204 (forall (@list @t455 @t458 @t456 @t454) (=> @t461 (=> @t460 (=> @t459 (=> @t457 (_ (_ tptp.ord_less_nat (_ @t455 @t456)) (_ @t455 @t454)))))))) % 0.46/0.97 (assume @p205 (forall (@list @t462 @t458 @t456 @t454) (=> @t463 (=> @t460 (=> @t459 (=> @t457 (_ (_ tptp.ord_less_set_nat (_ @t462 @t456)) (_ @t462 @t454)))))))) % 0.46/0.97 (assume @p206 (forall (@list @t464 @t458 @t456 @t454) (=> @t465 (=> @t460 (=> @t459 (=> @t457 (_ (_ tptp.ord_le727057319lle_tv (_ @t464 @t456)) (_ @t464 @t454)))))))) % 0.46/0.97 (assume @p207 (forall @t200 (=> (forall @t471 (=> @t470 (=> @t469 (=> @t468 (_ (_ tptp.ord_less_nat (_ @t71 @t467)) (_ @t71 @t466)))))) @t249))) % 0.46/0.97 (assume @p208 (forall (@list @t173 @t438) (=> (forall @t471 (=> @t470 (=> @t469 (=> @t468 (_ (_ tptp.ord_less_set_nat (_ @t438 @t467)) (_ @t438 @t466)))))) @t439))) % 0.46/0.97 (assume @p209 (forall (@list @t173 @t440) (=> (forall @t471 (=> @t470 (=> @t469 (=> @t468 (_ (_ tptp.ord_le727057319lle_tv (_ @t440 @t467)) (_ @t440 @t466)))))) @t441))) % 0.46/0.97 (assume @p210 (forall (@list @t446 @t443) (=> (forall @t477 (=> @t476 (=> @t475 (=> @t474 (_ (_ tptp.ord_less_nat (_ @t443 @t473)) (_ @t443 @t472)))))) @t449))) % 0.46/0.97 (assume @p211 (forall (@list @t446 @t450) (=> (forall @t477 (=> @t476 (=> @t475 (=> @t474 (_ (_ tptp.ord_less_set_nat (_ @t450 @t473)) (_ @t450 @t472)))))) @t451))) % 0.46/0.97 (assume @p212 (forall (@list @t446 @t452) (=> (forall @t477 (=> @t476 (=> @t475 (=> @t474 (_ (_ tptp.ord_le727057319lle_tv (_ @t452 @t473)) (_ @t452 @t472)))))) @t453))) % 0.46/0.97 (assume @p213 (forall (@list @t458 @t455) (=> (forall @t483 (=> @t482 (=> @t481 (=> @t480 (_ (_ tptp.ord_less_nat (_ @t455 @t479)) (_ @t455 @t478)))))) @t461))) % 0.46/0.97 (assume @p214 (forall (@list @t458 @t462) (=> (forall @t483 (=> @t482 (=> @t481 (=> @t480 (_ (_ tptp.ord_less_set_nat (_ @t462 @t479)) (_ @t462 @t478)))))) @t463))) % 0.46/0.97 (assume @p215 (forall (@list @t458 @t464) (=> (forall @t483 (=> @t482 (=> @t481 (=> @t480 (_ (_ tptp.ord_le727057319lle_tv (_ @t464 @t479)) (_ @t464 @t478)))))) @t465))) % 0.46/0.97 (assume @p216 (forall (@list @t253 @t71 @t327 @t484) (=> (= @t253 (_ @t71 @t327)) (=> @t486 (=> (forall @t89 (=> @t251 (_ (_ tptp.ord_less_nat @t116) @t115))) (_ @t485 (_ @t71 @t484))))))) % 0.46/0.97 (assume @p217 (forall (@list @t487 @t438 @t327 @t484) (=> (= @t487 (_ @t438 @t327)) (=> @t486 (=> (forall @t89 (=> @t251 (_ (_ tptp.ord_less_set_nat (_ @t438 @t84)) (_ @t438 @t83)))) (_ @t488 (_ @t438 @t484))))))) % 0.46/0.97 (assume @p218 (forall (@list @t489 @t440 @t327 @t484) (=> (= @t489 (_ @t440 @t327)) (=> @t486 (=> (forall @t89 (=> @t251 (_ (_ tptp.ord_le727057319lle_tv (_ @t440 @t84)) (_ @t440 @t83)))) (_ @t490 (_ @t440 @t484))))))) % 0.46/0.97 (assume @p219 (forall (@list @t253 @t443 @t496 @t491) (=> (= @t253 (_ @t443 @t496)) (=> @t497 (=> (forall @t495 (=> @t494 (_ (_ tptp.ord_less_nat (_ @t443 @t493)) (_ @t443 @t492)))) (_ @t485 (_ @t443 @t491))))))) % 0.46/0.97 (assume @p220 (forall (@list @t487 @t450 @t496 @t491) (=> (= @t487 (_ @t450 @t496)) (=> @t497 (=> (forall @t495 (=> @t494 (_ (_ tptp.ord_less_set_nat (_ @t450 @t493)) (_ @t450 @t492)))) (_ @t488 (_ @t450 @t491))))))) % 0.46/0.97 (assume @p221 (forall (@list @t489 @t452 @t496 @t491) (=> (= @t489 (_ @t452 @t496)) (=> @t497 (=> (forall @t495 (=> @t494 (_ (_ tptp.ord_le727057319lle_tv (_ @t452 @t493)) (_ @t452 @t492)))) (_ @t490 (_ @t452 @t491))))))) % 0.46/0.97 (assume @p222 (forall (@list @t253 @t455 @t503 @t498) (=> (= @t253 (_ @t455 @t503)) (=> @t504 (=> (forall @t502 (=> @t501 (_ (_ tptp.ord_less_nat (_ @t455 @t500)) (_ @t455 @t499)))) (_ @t485 (_ @t455 @t498))))))) % 0.46/0.97 (assume @p223 (forall (@list @t487 @t462 @t503 @t498) (=> (= @t487 (_ @t462 @t503)) (=> @t504 (=> (forall @t502 (=> @t501 (_ (_ tptp.ord_less_set_nat (_ @t462 @t500)) (_ @t462 @t499)))) (_ @t488 (_ @t462 @t498))))))) % 0.46/0.97 (assume @p224 (forall (@list @t489 @t464 @t503 @t498) (=> (= @t489 (_ @t464 @t503)) (=> @t504 (=> (forall @t502 (=> @t501 (_ (_ tptp.ord_le727057319lle_tv (_ @t464 @t500)) (_ @t464 @t499)))) (_ @t490 (_ @t464 @t498))))))) % 0.46/0.97 (assume @p225 (forall (@list @t253 @t411) (= (_ @t265 @t505) (_ @t411 @t253)))) % 0.46/0.97 (assume @p226 (forall (@list @t256 @t408) (= (_ @t257 @t506) (_ @t408 @t256)))) % 0.46/0.97 (assume @p227 (forall @t227 (= (_ tptp.collect_nat (lambda @t240 @t393)) @t173))) % 0.46/0.97 (assume @p228 (forall @t226 (= (_ tptp.collec1111687558lle_tv (lambda @t238 (_ @t237 @t180))) @t180))) % 0.46/0.97 (assume @p229 (forall (@list @t411 @t507) (=> (forall @t225 (= @t432 (_ @t507 @t84))) (= @t505 (_ tptp.collect_nat @t507))))) % 0.46/0.97 (assume @p230 (forall (@list @t408 @t508) (=> (forall @t224 (= @t431 (_ @t508 @t110))) (= @t506 (_ tptp.collec1111687558lle_tv @t508))))) % 0.46/0.97 (assume @p231 (forall @t511 (=> @t510 (=> @t509 (_ (_ tptp.ord_le727057319lle_tv @t263) @t320))))) % 0.46/0.97 (assume @p232 (forall @t514 (=> @t513 (=> @t512 (_ (_ tptp.ord_less_set_nat @t268) @t323))))) % 0.46/0.97 (assume @p233 (forall @t376 (=> @t184 (_ (_ tptp.inj_on772319074lle_tv @t375) @t263)))) % 0.46/0.97 (assume @p234 (forall @t250 (=> @t186 (_ (_ tptp.inj_on_nat_nat @t377) @t268)))) % 0.46/0.97 (assume @p235 (forall (@list @t71 @t173 @t31) (=> @t186 (=> (_ @t174 @t268) (= (_ @t71 @t515) @t31))))) % 0.46/0.97 (assume @p236 (forall (@list @t65 @t180 @t63) (=> @t184 (=> (_ @t181 @t263) (= (_ @t65 @t516) @t63))))) % 0.46/0.97 (assume @p237 (forall (@list @t71 @t213) (=> @t352 (=> @t518 (=> @t517 (_ tptp.order_769474267at_nat @t213)))))) % 0.46/0.97 (assume @p238 (forall @t521 (=> @t520 (exists @t224 @t519)))) % 0.46/0.97 (assume @p239 (forall @t525 (=> @t524 (exists @t224 @t523)))) % 0.46/0.97 (assume @p240 (forall @t528 (=> @t527 (exists @t225 @t526)))) % 0.46/0.97 (assume @p241 (forall @t530 (=> @t518 (exists @t225 @t529)))) % 0.46/0.97 (assume @p242 (forall @t521 (=> @t520 (not (forall @t224 (not @t519)))))) % 0.46/0.97 (assume @p243 (forall @t525 (=> @t524 (not (forall @t224 (not @t523)))))) % 0.46/0.97 (assume @p244 (forall @t528 (=> @t527 (not (forall @t225 (not @t526)))))) % 0.46/0.97 (assume @p245 (forall @t530 (=> @t518 (not (forall @t225 (not @t529)))))) % 0.46/0.97 (assume @p246 (forall (@list @t216 @t65) (=> (forall @t224 @t234) @t531))) % 0.46/0.97 (assume @p247 (forall (@list @t228 @t33) (=> (forall @t225 @t229) @t532))) % 0.46/0.97 (assume @p248 (forall (@list @t209 @t241) (=> (forall @t224 (= (_ @t209 @t522) @t110)) @t533))) % 0.46/0.97 (assume @p249 (forall (@list @t213 @t71) (=> @t517 @t534))) % 0.46/0.97 (assume @p250 (forall @t245 (_ @t385 @t330))) % 0.46/0.97 (assume @p251 (forall @t247 (_ @t386 @t334))) % 0.46/0.97 (assume @p252 (forall @t248 (_ @t383 @t339))) % 0.46/0.97 (assume @p253 (forall @t246 (_ @t384 @t341))) % 0.46/0.97 (assume @p254 (forall @t114 (= @t520 (forall @t328 (exists @t238 (= @t146 @t150)))))) % 0.46/0.97 (assume @p255 (forall (@list @t241) (= @t524 (forall @t338 (exists @t238 (= @t130 @t329)))))) % 0.46/0.97 (assume @p256 (forall @t90 (= @t527 (forall @t328 (exists @t240 (= @t146 @t134)))))) % 0.46/0.97 (assume @p257 (forall @t119 (= @t518 (forall @t338 (exists @t240 (= @t130 @t152)))))) % 0.46/0.97 (assume @p258 (forall (@list @t327 @t241 @t16) (=> @t369 @t332))) % 0.46/0.97 (assume @p259 (forall (@list @t333 @t65 @t16) (=> @t371 @t336))) % 0.46/0.97 (assume @p260 (forall (@list @t327 @t71 @t19) (=> @t365 @t340))) % 0.46/0.97 (assume @p261 (forall (@list @t333 @t33 @t19) (=> @t367 @t342))) % 0.46/0.97 (assume @p262 (forall @t235 (=> (forall @t224 (=> @t199 (forall (@list @t535) (=> (_ (_ tptp.member266900804lle_tv @t535) @t180) (= (= @t233 (_ @t216 (_ @t65 @t535))) (= (_ @t216 @t110) (_ @t216 @t535))))))) (=> @t184 (= (_ @t217 @t263) @t218))))) % 0.46/0.97 (assume @p263 (forall @t232 (=> (forall @t225 (=> @t197 (forall (@list @t536) (=> (_ (_ tptp.member_nat @t536) @t173) (= (= @t230 (_ @t213 (_ @t71 @t536))) (= @t428 (_ @t213 @t536))))))) (=> @t186 (= (_ @t214 @t268) @t215))))) % 0.46/0.97 (assume @p264 (forall @t537 (not (_ (_ tptp.ord_le727057319lle_tv tptp.top_to1057771083lle_tv) @t489)))) % 0.46/0.97 (assume @p265 (forall @t538 (not (_ (_ tptp.ord_less_set_nat tptp.top_top_set_nat) @t487)))) % 0.46/0.97 (assume @p266 (forall @t537 (= (not @t539) (_ @t490 tptp.top_to1057771083lle_tv)))) % 0.46/0.97 (assume @p267 (forall @t538 (= (not @t540) (_ @t488 tptp.top_top_set_nat)))) % 0.46/0.97 (assume @p268 (forall (@list @t253 @t173) (_ @t254 @t173))) % 0.46/0.97 (assume @p269 (forall (@list @t71 @t173 @t19) (=> @t186 (=> @t176 (= (_ @t377 @t72) @t19))))) % 0.46/0.97 (assume @p270 (forall (@list @t65 @t180 @t16) (=> @t184 (=> @t183 (= (_ @t375 @t66) @t16))))) % 0.46/0.97 (assume @p271 (forall @t187 (=> @t186 (=> (= @t72 @t31) (=> @t176 (= @t515 @t19)))))) % 0.46/0.97 (assume @p272 (forall @t185 (=> @t184 (=> (= @t66 @t63) (=> @t183 (= @t516 @t16)))))) % 0.46/0.97 (assume @p273 (forall @t543 (=> @t512 @t542))) % 0.46/0.97 (assume @p274 (forall @t547 (=> @t509 @t546))) % 0.46/0.97 (assume @p275 (forall (@list @t71 @t173 @t19 @t300) (=> @t186 (=> (_ @t20 @t268) (=> @t549 (_ (_ tptp.member_nat (_ @t377 @t19)) @t300)))))) % 0.46/0.97 (assume @p276 (forall (@list @t241 @t180 @t19 @t319) (=> @t380 (=> (_ @t20 @t260) (=> @t551 (_ (_ tptp.member266900804lle_tv (_ @t379 @t19)) @t319)))))) % 0.46/0.97 (assume @p277 (forall (@list @t33 @t173 @t16 @t300) (=> @t178 (=> (_ @t17 @t271) (=> @t549 (_ (_ tptp.member_nat (_ @t378 @t16)) @t300)))))) % 0.46/0.97 (assume @p278 (forall (@list @t65 @t180 @t16 @t319) (=> @t184 (=> (_ @t17 @t263) (=> @t551 (_ (_ tptp.member266900804lle_tv (_ @t375 @t16)) @t319)))))) % 0.46/0.97 (assume @p279 (forall (@list @t553 @t552) (=> @t555 (=> @t554 (_ (_ tptp.inj_on2112487900lle_tv (_ (_ tptp.produc1345917071lle_tv @t553) @t552)) tptp.top_to1871154984lle_tv))))) % 0.46/0.97 (assume @p280 (forall (@list @t553 @t556) (=> @t555 (=> @t557 (_ (_ tptp.inj_on552895452tv_nat (_ (_ tptp.produc42536895at_nat @t553) @t556)) tptp.top_to975729152tv_nat))))) % 0.46/0.97 (assume @p281 (forall (@list @t558 @t552) (=> @t559 (=> @t554 (_ (_ tptp.inj_on1745913142lle_tv (_ (_ tptp.produc2101297531lle_tv @t558) @t552)) tptp.top_to1411004326lle_tv))))) % 0.46/0.97 (assume @p282 (forall (@list @t558 @t556) (=> @t559 (=> @t557 (_ (_ tptp.inj_on26176689at_nat (_ (_ tptp.produc505105722at_nat @t558) @t556)) tptp.top_to1555900337at_nat))))) % 0.46/0.97 (assume @p283 (forall (@list @t173 @t300) (=> (forall @t225 (=> @t197 (_ @t196 @t300))) @t549))) % 0.46/0.97 (assume @p284 (forall (@list @t180 @t319) (=> (forall @t224 (=> @t199 (_ @t198 @t319))) @t551))) % 0.46/0.97 (assume @p285 (forall (@list @t173 @t71 @t300) (=> (forall @t225 (=> @t197 (_ (_ tptp.member_nat @t116) @t300))) (_ @t560 @t300)))) % 0.46/0.97 (assume @p286 (forall (@list @t173 @t33 @t319) (=> (forall @t225 (=> @t197 (_ (_ tptp.member266900804lle_tv @t86) @t319))) (_ (_ tptp.ord_le241064091lle_tv @t271) @t319)))) % 0.46/0.97 (assume @p287 (forall (@list @t180 @t241 @t300) (=> (forall @t224 (=> @t199 (_ (_ tptp.member_nat @t522) @t300))) (_ (_ tptp.ord_less_eq_set_nat @t260) @t300)))) % 0.46/0.97 (assume @p288 (forall (@list @t180 @t65 @t319) (=> (forall @t224 (=> @t199 (_ (_ tptp.member266900804lle_tv @t111) @t319))) (_ @t561 @t319)))) % 0.46/0.97 (assume @p289 (forall @t537 (=> @t562 @t539))) % 0.46/0.97 (assume @p290 (forall @t538 (=> @t563 @t540))) % 0.46/0.97 (assume @p291 (forall @t537 (= @t562 @t539))) % 0.46/0.97 (assume @p292 (forall @t538 (= @t563 @t540))) % 0.46/0.97 (assume @p293 (forall @t537 (_ (_ tptp.ord_le241064091lle_tv @t489) tptp.top_to1057771083lle_tv))) % 0.46/0.97 (assume @p294 (forall @t538 (_ (_ tptp.ord_less_eq_set_nat @t487) tptp.top_top_set_nat))) % 0.46/0.97 (assume @p295 (forall @t226 (_ @t550 tptp.top_to1057771083lle_tv))) % 0.46/0.97 (assume @p296 (forall @t227 (_ @t548 tptp.top_top_set_nat))) % 0.46/0.97 (assume @p297 (forall @t511 (=> @t510 (=> @t551 @t184)))) % 0.46/0.97 (assume @p298 (forall @t514 (=> @t513 (=> @t549 @t186)))) % 0.46/0.97 (assume @p299 (forall @t322 (=> @t184 (=> (_ @t564 @t180) @t510)))) % 0.46/0.97 (assume @p300 (forall @t325 (=> @t186 (=> (_ @t565 @t173) @t513)))) % 0.46/0.97 (assume @p301 (forall (@list @t173 @t300 @t19) (=> @t549 (=> @t176 (_ @t20 @t300))))) % 0.46/0.97 (assume @p302 (forall (@list @t180 @t319 @t16) (=> @t551 (=> @t183 (_ @t17 @t319))))) % 0.46/0.97 (assume @p303 (forall @t543 (=> @t549 @t542))) % 0.46/0.97 (assume @p304 (forall @t547 (=> @t551 @t546))) % 0.46/0.97 (assume @p305 (= tptp.ord_less_eq_set_nat (lambda @t570 (forall (@list @t567) (=> (_ @t568 @t569) (_ @t568 @t566)))))) % 0.46/0.97 (assume @p306 (= tptp.ord_le241064091lle_tv (lambda @t575 (forall (@list @t572) (=> (_ @t573 @t574) (_ @t573 @t571)))))) % 0.46/0.97 (assume @p307 (forall @t200 (=> (forall @t89 (=> @t251 (=> @t197 (=> @t195 @t252)))) (=> (forall @t89 (=> @t197 (=> @t195 (or (_ (_ tptp.ord_less_eq_nat @t84) @t83) (_ (_ tptp.ord_less_eq_nat @t83) @t84))))) @t186)))) % 0.46/0.97 (assume @p308 (forall (@list @t71 @t300 @t253 @t173) (=> @t513 (=> @t576 (=> @t549 @t269))))) % 0.46/0.97 (assume @p309 (forall (@list @t33 @t300 @t253 @t173) (=> (_ @t36 @t300) (=> @t576 (=> @t549 @t272))))) % 0.46/0.97 (assume @p310 (forall (@list @t241 @t319 @t256 @t180) (=> (_ @t243 @t319) (=> @t577 (=> @t551 @t261))))) % 0.46/0.97 (assume @p311 (forall (@list @t65 @t319 @t256 @t180) (=> @t510 (=> @t577 (=> @t551 @t264))))) % 0.46/0.97 (assume @p312 (forall (@list @t65 @t578 @t180 @t319) (=> (_ @t68 @t578) (=> (_ @t550 @t578) (=> (_ @t564 @t578) @t321))))) % 0.46/0.97 (assume @p313 (forall (@list @t71 @t579 @t173 @t300) (=> (_ @t74 @t579) (=> (_ @t548 @t579) (=> (_ @t565 @t579) @t324))))) % 0.46/0.97 (assume @p314 (forall @t322 (=> @t69 (= (_ @t561 @t320) @t551)))) % 0.46/0.97 (assume @p315 (forall @t325 (=> @t75 (= (_ @t560 @t323) @t549)))) % 0.46/0.97 (assume @p316 (forall (@list @t65 @t216) (=> @t520 (=> @t531 (= (_ (_ tptp.image_1221801032lle_tv (_ (_ tptp.produc1345917071lle_tv @t65) @t216)) tptp.top_to1871154984lle_tv) tptp.top_to1871154984lle_tv))))) % 0.46/0.97 (assume @p317 (forall (@list @t65 @t228) (=> @t520 (=> @t532 (= (_ (_ tptp.image_1796815776tv_nat (_ (_ tptp.produc1500159719tv_nat @t65) @t228)) tptp.top_to1871154984lle_tv) tptp.top_to975729152tv_nat))))) % 0.46/0.97 (assume @p318 (forall (@list @t65 @t209) (=> @t520 (=> @t533 (= (_ (_ tptp.image_228488944lle_tv (_ (_ tptp.produc1521089895lle_tv @t65) @t209)) tptp.top_to975729152tv_nat) tptp.top_to1871154984lle_tv))))) % 0.46/0.97 (assume @p319 (forall (@list @t65 @t213) (=> @t520 (=> @t534 (= (_ (_ tptp.image_1104296520tv_nat (_ (_ tptp.produc42536895at_nat @t65) @t213)) tptp.top_to975729152tv_nat) tptp.top_to975729152tv_nat))))) % 0.46/0.97 (assume @p320 (forall (@list @t241 @t216) (=> @t524 (=> @t531 (= (_ (_ tptp.image_1892891680lle_tv (_ (_ tptp.produc1095080935lle_tv @t241) @t216)) tptp.top_to1871154984lle_tv) tptp.top_to1411004326lle_tv))))) % 0.46/0.97 (assume @p321 (forall (@list @t241 @t228) (=> @t524 (=> @t532 (= (_ (_ tptp.image_901203832at_nat (_ (_ tptp.produc51277375tv_nat @t241) @t228)) tptp.top_to1871154984lle_tv) tptp.top_to1555900337at_nat))))) % 0.46/0.97 (assume @p322 (forall (@list @t241 @t209) (=> @t524 (=> @t533 (= (_ (_ tptp.image_1200372424lle_tv (_ (_ tptp.produc72207551lle_tv @t241) @t209)) tptp.top_to975729152tv_nat) tptp.top_to1411004326lle_tv))))) % 0.46/0.97 (assume @p323 (forall (@list @t241 @t213) (=> @t524 (=> @t534 (= (_ (_ tptp.image_1805124128at_nat (_ (_ tptp.produc386540311at_nat @t241) @t213)) tptp.top_to975729152tv_nat) tptp.top_to1555900337at_nat))))) % 0.46/0.97 (assume @p324 (forall (@list @t33 @t216) (=> @t527 (=> @t531 (= (_ (_ tptp.image_988201162lle_tv (_ (_ tptp.produc1975500101lle_tv @t33) @t216)) tptp.top_to1411004326lle_tv) tptp.top_to1871154984lle_tv))))) % 0.46/0.97 (assume @p325 (forall (@list @t33 @t228) (=> @t527 (=> @t532 (= (_ (_ tptp.image_53754658tv_nat (_ (_ tptp.produc189459613tv_nat @t33) @t228)) tptp.top_to1411004326lle_tv) tptp.top_to975729152tv_nat))))) % 0.46/0.97 (assume @p326 (forall (@list @t581 @t65 @t582) (= (_ (_ tptp.ord_le241064091lle_tv @t581) (_ @t262 @t582)) (exists (@list @t580) (and (_ (_ tptp.ord_le241064091lle_tv @t580) @t582) (_ @t68 @t580) (= @t581 (_ @t262 @t580))))))) % 0.46/0.97 (assume @p327 (forall (@list @t584 @t71 @t585) (= (_ (_ tptp.ord_less_eq_set_nat @t584) (_ @t267 @t585)) (exists (@list @t583) (and (_ (_ tptp.ord_less_eq_set_nat @t583) @t585) (_ @t74 @t583) (= @t584 (_ @t267 @t583))))))) % 0.46/0.97 (assume @p328 @t586) % 0.46/0.97 (assume @p329 true) % 0.46/0.97 (step @p330 (= tptp.top_to1299250770e_tv_o @t587) :rule refl :args (@t587)) % 0.46/0.97 (step @p331 (= tptp.top_top_nat_o @t588) :rule refl :args (@t588)) % 0.46/0.97 (step @p332 (= tptp.inj_on2112487900lle_tv @t591) :rule refl :args (@t591)) % 0.46/0.97 (step @p333 (= tptp.inj_on552895452tv_nat @t595) :rule refl :args (@t595)) % 0.46/0.97 (step @p334 (= tptp.inj_on1745913142lle_tv @t599) :rule refl :args (@t599)) % 0.46/0.97 (step @p335 (= tptp.inj_on26176689at_nat @t602) :rule refl :args (@t602)) % 0.46/0.97 (step @p336 (= tptp.inj_on1955349912lle_tv @t606) :rule refl :args (@t606)) % 0.46/0.97 (step @p337 (= tptp.inj_on772319074lle_tv @t618) :rule refl :args (@t618)) % 0.46/0.97 (step @p338 (= tptp.inj_on_nat_nat @t621) :rule refl :args (@t621)) % 0.46/0.97 (step @p339 (= tptp.top_to900819589_nat_o @t622) :rule refl :args (@t622)) % 0.46/0.97 (step @p340 (= tptp.top_to1889334367e_tv_o @t623) :rule refl :args (@t623)) % 0.46/0.97 (step @p341 (= tptp.top_to632227436_nat_o @t624) :rule refl :args (@t624)) % 0.46/0.97 (step @p342 (= tptp.strict2146030304at_nat @t629) :rule refl :args (@t629)) % 0.46/0.97 (step @p343 (= tptp.strict1310998166et_nat @t631) :rule refl :args (@t631)) % 0.46/0.97 (step @p344 (= tptp.strict1658340843lle_tv @t633) :rule refl :args (@t633)) % 0.46/0.97 (step @p345 (= tptp.strict1802283670at_nat @t640) :rule refl :args (@t640)) % 0.46/0.97 (step @p346 (= tptp.strict473775692et_nat @t642) :rule refl :args (@t642)) % 0.46/0.97 (step @p347 (= tptp.strict172559285lle_tv @t644) :rule refl :args (@t644)) % 0.46/0.97 (step @p348 (= tptp.strict1125660301tv_nat @t651) :rule refl :args (@t651)) % 0.46/0.97 (step @p349 (= tptp.strict1455779395et_nat @t653) :rule refl :args (@t653)) % 0.46/0.97 (step @p350 (= tptp.strict592849515lle_tv @t655) :rule refl :args (@t655)) % 0.46/0.97 (step @p351 (= tptp.ord_less_eq_set_nat @t656) :rule refl :args (@t656)) % 0.46/0.97 (step @p352 (= tptp.ord_le241064091lle_tv @t657) :rule refl :args (@t657)) % 0.46/0.97 (step @p353 :rule refl :args (@t3)) % 0.46/0.97 (step @p354 :rule refl :args (@t658)) % 0.46/0.97 (step @p355 :rule refl :args (@t5)) % 0.46/0.97 (step @p356 :rule cong :premises (@p355 @p354) :args ((= @t5 @t658))) % 0.46/0.97 (step @p357 :rule symm :premises (@p356)) % 0.46/0.97 (step @p358 :rule eq_resolve :premises (@p355 @p357)) % 0.46/0.97 (step @p359 :rule refl :args (@t659)) % 0.46/0.97 (step @p360 :rule refl :args (@t6)) % 0.46/0.97 (step @p361 :rule cong :premises (@p360 @p359) :args ((= @t6 @t659))) % 0.46/0.97 (step @p362 :rule symm :premises (@p361)) % 0.46/0.97 (step @p363 :rule eq_resolve :premises (@p360 @p362)) % 0.46/0.97 (step @p364 :rule cong :premises (@p363 @p358) :args (@t7)) % 0.46/0.97 (step @p365 :rule cong :premises (@p364) :args (@t660)) % 0.46/0.97 (step @p366 :rule nary_cong :premises (@p365 @p353) :args (@t661)) % 0.46/0.97 (step @p367 :rule cong :premises (@p366) :args ((forall @t8 @t661))) % 0.46/0.97 (step @p368 :rule bool-impl-elim :args (@t7 @t3)) % 0.46/0.97 (step @p369 :rule cong :premises (@p368) :args (@t9)) % 0.46/0.97 (step @p370 :rule trans :premises (@p369 @p367)) % 0.46/0.97 (step @p371 :rule eq_resolve :premises (@p1 @p370)) % 0.46/0.97 (step @p372 :rule refl :args (@t663)) % 0.46/0.97 (step @p373 :rule refl :args (@t666)) % 0.46/0.97 (step @p374 :rule refl :args (@t669)) % 0.46/0.97 (step @p375 :rule refl :args (@t668)) % 0.46/0.97 (step @p376 :rule cong :premises (@p375) :args (@t669)) % 0.46/0.97 (step @p377 :rule trans :premises (@p376 @p374)) % 0.46/0.97 (step @p378 :rule refl :args (tptp.collec1111687558lle_tv)) % 0.46/0.97 (step @p379 :rule ho_cong :premises (@p378 @p375)) % 0.46/0.97 (step @p380 :rule cong :premises (@p379 @p377) :args ((= @t670 @t669))) % 0.46/0.97 (step @p381 :rule symm :premises (@p380)) % 0.46/0.97 (step @p382 :rule refl :args ((_ tptp.collec1111687558lle_tv @t668))) % 0.46/0.97 (step @p383 :rule eq_resolve :premises (@p382 @p381)) % 0.46/0.97 (step @p384 :rule refl :args (@t662)) % 0.46/0.97 (step @p385 :rule cong :premises (@p384 @p383) :args (@t671)) % 0.46/0.97 (step @p386 :rule cong :premises (@p385) :args (@t672)) % 0.46/0.97 (step @p387 :rule refl :args (@t147)) % 0.46/0.97 (step @p388 :rule cong :premises (@p387 @p383) :args (@t673)) % 0.46/0.97 (step @p389 :rule cong :premises (@p388) :args (@t674)) % 0.46/0.97 (step @p390 :rule nary_cong :premises (@p389 @p386 @p373 @p372) :args (@t675)) % 0.46/0.97 (step @p391 :rule cong :premises (@p390) :args ((forall @t676 @t675))) % 0.46/0.97 (step @p392 :rule refl :args (@t663)) % 0.46/0.97 (step @p393 :rule refl :args (@t666)) % 0.46/0.97 (step @p394 :rule symm :premises (@p375)) % 0.46/0.97 (step @p395 :rule alpha_equiv :args (@t677 (@list @t147) (@list @t667))) % 0.46/0.97 (step @p396 :rule trans :premises (@p395 @p394)) % 0.46/0.97 (step @p397 :rule refl :args (tptp.collec1111687558lle_tv)) % 0.46/0.97 (step @p398 :rule ho_cong :premises (@p397 @p396)) % 0.46/0.97 (step @p399 :rule refl :args (@t662)) % 0.46/0.97 (step @p400 :rule cong :premises (@p399 @p398) :args (@t679)) % 0.46/0.97 (step @p401 :rule cong :premises (@p400) :args (@t680)) % 0.46/0.97 (step @p402 :rule refl :args (@t147)) % 0.46/0.97 (step @p403 :rule cong :premises (@p402 @p398) :args (@t681)) % 0.46/0.97 (step @p404 :rule cong :premises (@p403) :args (@t682)) % 0.46/0.97 (step @p405 :rule nary_cong :premises (@p404 @p401 @p393 @p392) :args (@t683)) % 0.46/0.97 (step @p406 :rule cong :premises (@p405) :args (@t684)) % 0.46/0.97 (step @p407 :rule trans :premises (@p406 @p391)) % 0.46/0.97 (step @p408 :rule cong :premises (@p407) :args ((not @t684))) % 0.46/0.97 (step @p409 :rule bool-eq-true :args (tptp.top_top_o)) % 0.46/0.97 (step @p410 :rule symm :premises (@p409)) % 0.46/0.97 (step @p411 :rule quant-unused-vars :args ((= (forall @t18 tptp.top_top_o) tptp.top_top_o))) % 0.46/0.97 (step @p412 :rule beta-reduce :args ((= @t685 tptp.top_top_o))) % 0.46/0.97 (step @p413 :rule cong :premises (@p412) :args ((forall @t18 @t685))) % 0.46/0.97 (step @p414 :rule trans :premises (@p413 @p411)) % 0.46/0.97 (step @p415 :rule refl :args (@t16)) % 0.46/0.97 (step @p416 :rule ho_cong :premises (@p330 @p415)) % 0.46/0.97 (step @p417 :rule cong :premises (@p416) :args (@t374)) % 0.46/0.97 (step @p418 :rule trans :premises (@p417 @p414)) % 0.46/0.97 (step @p419 :rule eq_resolve :premises (@p152 @p418)) % 0.46/0.97 (step @p420 :rule eq_resolve :premises (@p419 @p410)) % 0.46/0.97 (step @p421 :rule cong :premises (@p420) :args (@t587)) % 0.46/0.97 (step @p422 :rule ho_cong :premises (@p397 @p421)) % 0.46/0.97 (step @p423 :rule ho_cong :premises (@p397 @p330)) % 0.46/0.97 (step @p424 :rule refl :args (tptp.top_to1057771083lle_tv)) % 0.46/0.97 (step @p425 :rule cong :premises (@p424 @p423) :args (@t220)) % 0.46/0.97 (step @p426 :rule eq_resolve :premises (@p67 @p425)) % 0.46/0.97 (step @p427 :rule trans :premises (@p426 @p422)) % 0.46/0.97 (step @p428 :rule cong :premises (@p399 @p427) :args (@t686)) % 0.46/0.97 (step @p429 :rule cong :premises (@p428) :args (@t687)) % 0.46/0.97 (step @p430 :rule cong :premises (@p402 @p427) :args (@t688)) % 0.46/0.97 (step @p431 :rule cong :premises (@p430) :args (@t689)) % 0.46/0.97 (step @p432 :rule nary_cong :premises (@p431 @p429 @p393 @p392) :args (@t690)) % 0.46/0.97 (step @p433 :rule cong :premises (@p432) :args (@t691)) % 0.46/0.97 (step @p434 :rule cong :premises (@p433) :args ((not @t691))) % 0.46/0.97 (step @p435 :rule trans :premises (@p434 @p408)) % 0.46/0.97 (step @p436 :rule beta-reduce :args ((= (_ (lambda @t695 (forall @t676 (or @t694 @t692 @t666 @t663))) tptp.top_to1057771083lle_tv) @t691))) % 0.46/0.97 (step @p437 :rule refl :args (@t664)) % 0.46/0.97 (step @p438 :rule refl :args (@t696)) % 0.46/0.97 (step @p439 :rule cong :premises (@p438 @p437) :args ((= @t696 @t664))) % 0.46/0.97 (step @p440 :rule symm :premises (@p439)) % 0.46/0.97 (step @p441 :rule eq_resolve :premises (@p438 @p440)) % 0.46/0.97 (step @p442 :rule refl :args (@t665)) % 0.46/0.97 (step @p443 :rule refl :args (@t697)) % 0.46/0.97 (step @p444 :rule cong :premises (@p443 @p442) :args ((= @t697 @t665))) % 0.46/0.97 (step @p445 :rule symm :premises (@p444)) % 0.46/0.97 (step @p446 :rule eq_resolve :premises (@p443 @p445)) % 0.46/0.97 (step @p447 :rule cong :premises (@p446 @p441) :args (@t698)) % 0.46/0.97 (step @p448 :rule cong :premises (@p447) :args (@t699)) % 0.46/0.97 (step @p449 :rule refl :args (@t692)) % 0.46/0.97 (step @p450 :rule refl :args (@t694)) % 0.46/0.97 (step @p451 :rule nary_cong :premises (@p450 @p449 @p448 @p372) :args (@t700)) % 0.46/0.97 (step @p452 :rule cong :premises (@p451) :args ((forall @t676 @t700))) % 0.46/0.97 (step @p453 :rule refl :args (@t701)) % 0.46/0.97 (step @p454 :rule refl :args (@t702)) % 0.46/0.97 (step @p455 :rule cong :premises (@p454 @p453) :args (@t703)) % 0.46/0.97 (step @p456 :rule cong :premises (@p455) :args (@t704)) % 0.46/0.97 (step @p457 :rule refl :args (@t692)) % 0.46/0.97 (step @p458 :rule refl :args (@t694)) % 0.46/0.97 (step @p459 :rule nary_cong :premises (@p458 @p457 @p456 @p392) :args (@t705)) % 0.46/0.97 (step @p460 :rule cong :premises (@p459) :args (@t706)) % 0.46/0.97 (step @p461 :rule trans :premises (@p460 @p452)) % 0.46/0.97 (step @p462 :rule cong :premises (@p461) :args (@t707)) % 0.46/0.97 (step @p463 :rule beta-reduce :args ((= @t711 @t707))) % 0.46/0.97 (step @p464 :rule trans :premises (@p463 @p462)) % 0.46/0.97 (step @p465 :rule ho_cong :premises (@p464 @p424)) % 0.46/0.97 (step @p466 :rule trans :premises (@p465 @p436)) % 0.46/0.97 (step @p467 :rule cong :premises (@p466) :args ((not (_ @t711 tptp.top_to1057771083lle_tv)))) % 0.46/0.97 (step @p468 :rule refl :args (@t4)) % 0.46/0.97 (step @p469 :rule aci_norm :args ((= @t713 @t710))) % 0.46/0.97 (step @p470 :rule cong :premises (@p469) :args (@t714)) % 0.46/0.97 (step @p471 :rule quant-merge-prenex :args ((= (forall @t238 @t716) @t714))) % 0.46/0.97 (step @p472 :rule alpha_equiv :args (@t717 (@list @t662) (@list @t146))) % 0.46/0.97 (step @p473 :rule nary_cong :premises (@p450 @p472) :args (@t718)) % 0.46/0.97 (step @p474 :rule quant-miniscope-or :args ((= @t716 @t718))) % 0.46/0.97 (step @p475 :rule trans :premises (@p474 @p473)) % 0.46/0.97 (step @p476 :rule symm :premises (@p475)) % 0.46/0.97 (step @p477 :rule cong :premises (@p476) :args ((forall @t238 (or @t694 @t721)))) % 0.46/0.97 (step @p478 :rule trans :premises (@p477 @p471)) % 0.46/0.97 (step @p479 :rule trans :premises (@p478 @p470)) % 0.46/0.97 (step @p480 :rule refl :args (@t721)) % 0.46/0.97 (step @p481 :rule refl :args (@t693)) % 0.46/0.97 (step @p482 :rule refl :args (@t614)) % 0.46/0.97 (step @p483 :rule cong :premises (@p482 @p481) :args ((= @t614 @t693))) % 0.46/0.97 (step @p484 :rule symm :premises (@p483)) % 0.46/0.97 (step @p485 :rule eq_resolve :premises (@p482 @p484)) % 0.46/0.97 (step @p486 :rule cong :premises (@p485) :args (@t722)) % 0.46/0.97 (step @p487 :rule nary_cong :premises (@p486 @p480) :args (@t723)) % 0.46/0.97 (step @p488 :rule cong :premises (@p487) :args ((forall @t238 @t723))) % 0.46/0.97 (step @p489 :rule trans :premises (@p488 @p479)) % 0.46/0.97 (step @p490 :rule bool-impl-elim :args (@t614 @t721)) % 0.46/0.97 (step @p491 :rule cong :premises (@p490) :args ((forall @t238 (=> @t614 @t721)))) % 0.46/0.97 (step @p492 :rule trans :premises (@p491 @p489)) % 0.46/0.97 (step @p493 :rule refl :args (@t148)) % 0.46/0.97 (step @p494 :rule refl :args (@t719)) % 0.46/0.97 (step @p495 :rule refl :args (@t608)) % 0.46/0.97 (step @p496 :rule cong :premises (@p495 @p494) :args ((= @t608 @t719))) % 0.46/0.97 (step @p497 :rule symm :premises (@p496)) % 0.46/0.97 (step @p498 :rule eq_resolve :premises (@p495 @p497)) % 0.46/0.97 (step @p499 :rule refl :args (@t708)) % 0.46/0.97 (step @p500 :rule refl :args (@t609)) % 0.46/0.97 (step @p501 :rule cong :premises (@p500 @p499) :args ((= @t609 @t708))) % 0.46/0.97 (step @p502 :rule symm :premises (@p501)) % 0.46/0.97 (step @p503 :rule eq_resolve :premises (@p500 @p502)) % 0.46/0.97 (step @p504 :rule cong :premises (@p503 @p498) :args (@t610)) % 0.46/0.97 (step @p505 :rule cong :premises (@p504) :args (@t724)) % 0.46/0.97 (step @p506 :rule refl :args (@t720)) % 0.46/0.97 (step @p507 :rule refl :args (@t612)) % 0.46/0.97 (step @p508 :rule cong :premises (@p507 @p506) :args ((= @t612 @t720))) % 0.46/0.97 (step @p509 :rule symm :premises (@p508)) % 0.46/0.97 (step @p510 :rule eq_resolve :premises (@p507 @p509)) % 0.46/0.97 (step @p511 :rule cong :premises (@p510) :args (@t725)) % 0.46/0.97 (step @p512 :rule nary_cong :premises (@p511 @p505 @p493) :args (@t726)) % 0.46/0.97 (step @p513 :rule cong :premises (@p512) :args ((forall @t328 @t726))) % 0.46/0.97 (step @p514 :rule aci_norm :args ((= (or @t725 (or @t724 @t148)) @t726))) % 0.46/0.97 (step @p515 :rule bool-impl-elim :args (@t610 @t148)) % 0.46/0.97 (step @p516 :rule refl :args (@t725)) % 0.46/0.97 (step @p517 :rule nary_cong :premises (@p516 @p515) :args ((or @t725 @t611))) % 0.46/0.97 (step @p518 :rule trans :premises (@p517 @p514)) % 0.46/0.97 (step @p519 :rule bool-impl-elim :args (@t612 @t611)) % 0.46/0.97 (step @p520 :rule trans :premises (@p519 @p518)) % 0.46/0.97 (step @p521 :rule cong :premises (@p520) :args (@t613)) % 0.46/0.97 (step @p522 :rule trans :premises (@p521 @p513)) % 0.46/0.97 (step @p523 :rule refl :args (@t614)) % 0.46/0.97 (step @p524 :rule cong :premises (@p523 @p522) :args (@t615)) % 0.46/0.97 (step @p525 :rule cong :premises (@p524) :args (@t616)) % 0.46/0.97 (step @p526 :rule trans :premises (@p525 @p492)) % 0.46/0.97 (step @p527 :rule cong :premises (@p526) :args (@t618)) % 0.46/0.97 (step @p528 :rule trans :premises (@p337 @p527)) % 0.46/0.97 (step @p529 :rule ho_cong :premises (@p528 @p468)) % 0.46/0.97 (step @p530 :rule ho_cong :premises (@p529 @p424)) % 0.46/0.97 (step @p531 :rule cong :premises (@p530) :args (@t586)) % 0.46/0.97 (step @p532 :rule trans :premises (@p531 @p467)) % 0.46/0.97 (step @p533 :rule trans :premises (@p532 @p435)) % 0.46/0.97 (step @p534 :rule eq_resolve :premises (@p328 @p533)) % 0.46/0.97 (step @p535 :rule refl :args (@t736)) % 0.46/0.97 (step @p536 :rule bool-double-not-elim :args (@t727)) % 0.46/0.97 (step @p537 :rule nary_cong :premises (@p536 @p535) :args ((or (not @t737) @t736))) % 0.46/0.97 (step @p538 :rule refl :args (@t730)) % 0.46/0.97 (step @p539 :rule refl :args (@t732)) % 0.46/0.97 (step @p540 :rule eq-refl :args (@t668)) % 0.46/0.97 (step @p541 :rule refl :args (@t668)) % 0.46/0.97 (step @p542 :rule cong :premises (@p541 @p394) :args ((= @t668 @t668))) % 0.46/0.97 (step @p543 :rule trans :premises (@p542 @p540)) % 0.46/0.97 (step @p544 :rule skolem_intro :args (@t733)) % 0.46/0.97 (step @p545 :rule cong :premises (@p541 @p544) :args ((= @t668 @t733))) % 0.46/0.97 (step @p546 :rule trans :premises (@p545 @p543)) % 0.46/0.97 (step @p547 :rule true_elim :premises (@p546)) % 0.46/0.97 (step @p548 :rule cong :premises (@p547) :args (@t669)) % 0.46/0.97 (step @p549 :rule refl :args (@t728)) % 0.46/0.97 (step @p550 :rule cong :premises (@p549 @p548) :args (@t738)) % 0.46/0.97 (step @p551 :rule cong :premises (@p550) :args (@t739)) % 0.46/0.97 (step @p552 :rule refl :args (@t729)) % 0.46/0.97 (step @p553 :rule cong :premises (@p552 @p548) :args (@t740)) % 0.46/0.97 (step @p554 :rule cong :premises (@p553) :args (@t741)) % 0.46/0.97 (step @p555 :rule nary_cong :premises (@p554 @p551 @p539 @p538) :args (@t742)) % 0.46/0.97 (step @p556 :rule cong :premises (@p555) :args (@t743)) % 0.46/0.97 (step @p557 :rule refl :args (@t737)) % 0.46/0.97 (step @p558 :rule cong :premises (@p557 @p556) :args ((=> @t737 @t743))) % 0.46/0.97 (assume-push @p585 @t737) % 0.46/0.97 (step @p560 :rule skolemize :premises (@p534)) % 0.46/0.97 (step-pop @p586 :rule scope :premises (@p560)) % 0.46/0.97 (step @p561 :rule process_scope :premises (@p586) :args (@t743)) % 0.46/0.97 (step @p563 :rule eq_resolve :premises (@p561 @p558)) % 0.46/0.97 (step @p564 :rule implies_elim :premises (@p563)) % 0.46/0.97 (step @p565 :rule eq_resolve :premises (@p564 @p537)) % 0.46/0.97 (step @p566 :rule chain_m_resolution :premises (@p565 @p534) :args (@t736 @t744 (@list @t727))) % 0.46/0.97 (step @p567 :rule cnf_or_neg :args (@t735 3)) % 0.46/0.97 (step @p568 :rule chain_m_resolution :premises (@p567 @p566) :args ((not @t730) @t744 @t745)) % 0.46/0.97 (step @p569 :rule bool-double-not-elim :args (@t731)) % 0.46/0.97 (step @p570 :rule refl :args (@t735)) % 0.46/0.97 (step @p571 :rule nary_cong :premises (@p570 @p569) :args ((or @t735 (not @t732)))) % 0.46/0.97 (step @p572 :rule cnf_or_neg :args (@t735 2)) % 0.46/0.97 (step @p573 :rule eq_resolve :premises (@p572 @p571)) % 0.46/0.97 (step @p574 :rule reordering :premises (@p573) :args ((or @t731 @t735))) % 0.46/0.97 (step @p575 :rule chain_m_resolution :premises (@p574 @p566) :args (@t731 @t744 @t745)) % 0.46/0.97 (step @p576 :rule cnf_or_pos :args (@t746)) % 0.46/0.97 (step @p577 :rule reordering :premises (@p576) :args ((or @t732 @t730 @t747))) % 0.46/0.97 (step @p578 :rule chain_m_resolution :premises (@p577 @p575 @p568) :args (@t747 (@list false true) (@list @t731 @t730))) % 0.46/0.97 (assume-push @p587 @t748) % 0.46/0.97 (step @p580 :rule instantiate :premises (@p371) :args ((@list @t729 @t728))) % 0.46/0.97 (step-pop @p588 :rule scope :premises (@p580)) % 0.46/0.97 (step @p581 :rule process_scope :premises (@p588) :args (@t746)) % 0.46/0.97 (step @p583 :rule implies_elim :premises (@p581)) % 0.46/0.97 (step @p584 false :rule chain_m_resolution :premises (@p583 @p578 @p371) :args (false (@list true false) (@list @t746 @t748))) % 0.46/0.97 ) % 0.46/0.97 % SZS output end Proof % 0.46/0.97 % cvc5 exiting %------------------------------------------------------------------------------