%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP135^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n028.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:09 AM UTC 2026 % Result : Theorem 0.46s 0.92s % Output : Proof 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP135^1 : TPTP v9.2.1. Released v7.5.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.33 % Computer : n028.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue Jun 2 04:15:35 EDT 2026 % 0.15/0.34 % CPUTime : % 0.38/0.63 %----Proving TH0 % 0.46/0.92 --- 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.92 % SZS status Theorem % 0.46/0.92 % SZS output start Proof % 0.46/0.92 ( % 0.46/0.92 (declare-sort tptp.nat 0) % 0.46/0.92 (declare-sort tptp.list_char 0) % 0.46/0.92 (declare-sort tptp.paraco1605129243lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_Pr560526279lle_tv 0) % 0.46/0.92 (declare-sort tptp.produc931990033lle_tv 0) % 0.46/0.92 (declare-sort tptp.produc696645085lle_fm 0) % 0.46/0.92 (declare-sort tptp.paraco1604210848lle_fm 0) % 0.46/0.92 (declare-sort tptp.set_Pa1764573435lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_nat 0) % 0.46/0.92 (declare-sort tptp.set_Pr2014382200lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_Pr1986765409at_nat 0) % 0.46/0.92 (declare-sort tptp.produc194167194tv_nat 0) % 0.46/0.92 (declare-sort tptp.produc270694976lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_Pr1725653840tv_nat 0) % 0.46/0.92 (declare-sort tptp.set_Pr13445366lle_tv 0) % 0.46/0.92 (declare-sort tptp.product_prod_nat_nat 0) % 0.46/0.92 (declare-sort tptp.produc1647334210lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_Pr1723822845lle_tv 0) % 0.46/0.92 (declare-sort tptp.set_Pr2120184979lle_fm 0) % 0.46/0.92 (declare-sort tptp.produc596913417at_nat 0) % 0.46/0.92 (declare-sort tptp.set_Pr840833727at_nat 0) % 0.46/0.92 (declare-sort tptp.produc1443694919lle_tv 0) % 0.46/0.92 (declare-const tptp.paraco1147068288nge_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.paraco1344940915le_Det (-> Bool tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.paraco1325918602e_eval (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.top_top_o Bool) % 0.46/0.92 (declare-const tptp.member1531318361lle_tv (-> tptp.produc1647334210lle_tv tptp.set_Pr2014382200lle_tv Bool)) % 0.46/0.92 (declare-const tptp.member737151281tv_nat (-> tptp.produc194167194tv_nat tptp.set_Pr1725653840tv_nat Bool)) % 0.46/0.92 (declare-const tptp.member813679063lle_tv (-> tptp.produc270694976lle_tv tptp.set_Pr13445366lle_tv Bool)) % 0.46/0.92 (declare-const tptp.member701585322at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.92 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.46/0.92 (declare-const tptp.member266900804lle_tv (-> tptp.paraco1605129243lle_tv tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.92 (declare-const tptp.top_to975729152tv_nat tptp.set_Pr1725653840tv_nat) % 0.46/0.92 (declare-const tptp.top_to1411004326lle_tv tptp.set_Pr13445366lle_tv) % 0.46/0.92 (declare-const tptp.top_to1555900337at_nat tptp.set_Pr1986765409at_nat) % 0.46/0.92 (declare-const tptp.if_Par1134130401lle_tv (-> Bool tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.produc262413013lle_tv (-> tptp.produc1443694919lle_tv tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.produc381314067lle_tv (-> tptp.produc1443694919lle_tv tptp.list_char tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.produc1710735575lle_fm (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.produc696645085lle_fm)) % 0.46/0.92 (declare-const tptp.produc1589291287at_nat (-> tptp.produc596913417at_nat tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.produc500618325at_nat (-> tptp.produc596913417at_nat tptp.nat tptp.nat)) % 0.46/0.92 (declare-const tptp.produc1680557635lle_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.produc931990033lle_tv)) % 0.46/0.92 (declare-const tptp.ord_le1784136743lle_tv (-> tptp.set_Pr560526279lle_tv tptp.set_Pr560526279lle_tv Bool)) % 0.46/0.92 (declare-const tptp.ord_le1007985907lle_fm (-> tptp.set_Pr2120184979lle_fm tptp.set_Pr2120184979lle_fm Bool)) % 0.46/0.92 (declare-const tptp.produc1636169559lle_tv (-> tptp.produc931990033lle_tv tptp.nat tptp.nat)) % 0.46/0.92 (declare-const tptp.produc547496597lle_tv (-> tptp.produc931990033lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.produc29804011lle_fm (-> tptp.produc696645085lle_fm tptp.list_char tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.ord_le241064091lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.92 (declare-const tptp.inv_im1292588663lle_tv (-> tptp.set_Pr1986765409at_nat (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (declare-const tptp.total_on_nat (-> tptp.set_nat tptp.set_Pr1986765409at_nat Bool)) % 0.46/0.92 (declare-const tptp.inv_image_nat_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.nat tptp.nat) tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (declare-const tptp.produc72207551lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc270694976lle_tv)) % 0.46/0.92 (declare-const tptp.image_988201162lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (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.92 (declare-const tptp.image_53754658tv_nat (-> (-> tptp.produc270694976lle_tv tptp.produc194167194tv_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1725653840tv_nat)) % 0.46/0.92 (declare-const tptp.produc189459613tv_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.produc194167194tv_nat)) % 0.46/0.92 (declare-const tptp.inj_on1179712058tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv Bool)) % 0.46/0.92 (declare-const tptp.produc210389789lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc1647334210lle_tv)) % 0.46/0.92 (declare-const tptp.produc1250721397at_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.produc194167194tv_nat)) % 0.46/0.92 (declare-const tptp.image_149830562lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr13445366lle_tv)) % 0.46/0.92 (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.92 (declare-const tptp.produc313957681lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc270694976lle_tv)) % 0.46/0.92 (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.92 (declare-const tptp.image_376325286tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv tptp.set_nat)) % 0.46/0.92 (declare-const tptp.image_1151963140lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_nat tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (declare-const tptp.image_769496456lle_tv (-> (-> tptp.produc596913417at_nat tptp.produc931990033lle_tv) tptp.set_Pr840833727at_nat tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (declare-const tptp.image_326034184lle_fm (-> (-> tptp.produc1443694919lle_tv tptp.produc696645085lle_fm) tptp.set_Pr1723822845lle_tv tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (declare-const tptp.image_1724396928at_nat (-> (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat) tptp.set_Pr560526279lle_tv tptp.set_Pr840833727at_nat)) % 0.46/0.92 (declare-const tptp.image_924970994lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr1723822845lle_tv)) % 0.46/0.92 (declare-const tptp.produc225513635lle_tv (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat)) % 0.46/0.92 (declare-const tptp.produc1000205111lle_fm (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv)) % 0.46/0.92 (declare-const tptp.produc1633679363at_nat (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) tptp.produc596913417at_nat)) % 0.46/0.92 (declare-const tptp.produc1943344577lle_tv (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc1443694919lle_tv)) % 0.46/0.92 (declare-const tptp.image_1751508608lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv) tptp.set_Pr560526279lle_tv tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (declare-const tptp.image_1585092542lle_fm (-> (-> tptp.produc931990033lle_tv tptp.produc696645085lle_fm) tptp.set_Pr560526279lle_tv tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (declare-const tptp.image_1154804148lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc931990033lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (declare-const tptp.image_807538418lle_fm (-> (-> tptp.produc696645085lle_fm tptp.produc696645085lle_fm) tptp.set_Pr2120184979lle_fm tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (declare-const tptp.image_335818702lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat)) % 0.46/0.92 (declare-const tptp.produc532909085lle_tv (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc931990033lle_tv tptp.produc931990033lle_tv)) % 0.46/0.92 (declare-const tptp.produc951033137lle_fm (-> (-> (-> tptp.nat tptp.nat) tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1604210848lle_fm) tptp.produc931990033lle_tv tptp.produc696645085lle_fm)) % 0.46/0.92 (declare-const tptp.produc1566550641lle_tv (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.nat tptp.nat) (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv) tptp.produc696645085lle_fm tptp.produc931990033lle_tv)) % 0.46/0.92 (declare-const tptp.produc1900967599lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm) tptp.produc696645085lle_fm tptp.produc696645085lle_fm)) % 0.46/0.92 (declare-const tptp.image_1507992062lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc1647334210lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (declare-const tptp.produc752649287e_tv_o (-> (-> tptp.produc931990033lle_tv Bool) (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool)) % 0.46/0.92 (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.92 (declare-const tptp.produc275353523e_fm_o (-> (-> tptp.produc696645085lle_fm Bool) (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool)) % 0.46/0.92 (declare-const tptp.image_1200372424lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc270694976lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pr13445366lle_tv)) % 0.46/0.92 (declare-const tptp.member1569366824lle_tv (-> tptp.produc931990033lle_tv tptp.set_Pr560526279lle_tv Bool)) % 0.46/0.92 (declare-const tptp.member1474794996lle_fm (-> tptp.produc696645085lle_fm tptp.set_Pr2120184979lle_fm Bool)) % 0.46/0.92 (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.92 (declare-const tptp.paraco445776468le_Neg (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.collec1624074086lle_tv (-> (-> tptp.produc931990033lle_tv Bool) tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (declare-const tptp.member74361182lle_tv (-> tptp.produc1443694919lle_tv tptp.set_Pr1723822845lle_tv Bool)) % 0.46/0.92 (declare-const tptp.top_to378694061lle_tv tptp.set_Pr1723822845lle_tv) % 0.46/0.92 (declare-const tptp.total_1781621663lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pr2014382200lle_tv Bool)) % 0.46/0.92 (declare-const tptp.top_to730292591at_nat tptp.set_Pr840833727at_nat) % 0.46/0.92 (declare-const tptp.collec1288997470at_nat (-> (-> tptp.produc596913417at_nat Bool) tptp.set_Pr840833727at_nat)) % 0.46/0.92 (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 0.46/0.92 (declare-const tptp.p2 tptp.paraco1604210848lle_fm) % 0.46/0.92 (declare-const tptp.top_top_set_nat tptp.set_nat) % 0.46/0.92 (declare-const tptp.top_to775056195lle_fm tptp.set_Pr2120184979lle_fm) % 0.46/0.92 (declare-const tptp.i (-> tptp.list_char tptp.paraco1605129243lle_tv)) % 0.46/0.92 (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.92 (declare-const tptp.paraco793048302_Indet (-> tptp.nat tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.inv_im516950809tv_nat (-> tptp.set_Pr2014382200lle_tv (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (declare-const tptp.top_to1057771083lle_tv tptp.set_Pa1764573435lle_tv) % 0.46/0.92 (declare-const tptp.f (-> tptp.nat tptp.nat)) % 0.46/0.92 (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.92 (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.92 (declare-const tptp.produc1685803475tv_nat (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.product_prod_nat_nat)) % 0.46/0.92 (declare-const tptp.collec835549234lle_fm (-> (-> tptp.produc696645085lle_fm Bool) tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (declare-const tptp.paraco1389086619le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.paraco69239110le_Con (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.collec1111687558lle_tv (-> (-> tptp.paraco1605129243lle_tv Bool) tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (declare-const tptp.member1234290208at_nat (-> tptp.produc596913417at_nat tptp.set_Pr840833727at_nat Bool)) % 0.46/0.92 (declare-const tptp.inv_im719552961lle_tv (-> tptp.set_Pr2014382200lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (declare-const tptp.top_to449985143lle_tv tptp.set_Pr560526279lle_tv) % 0.46/0.92 (declare-const tptp.produc148705065lle_fm (-> tptp.produc696645085lle_fm tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.p1 tptp.paraco1604210848lle_fm) % 0.46/0.92 (declare-const tptp.paraco2051596139lle_tv (-> (-> Bool tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)) % 0.46/0.92 (declare-const tptp.paraco1480028776le_Pro (-> tptp.list_char tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.collec7649004at_nat (-> (-> tptp.product_prod_nat_nat Bool) tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (declare-const tptp.paraco1745535428le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) % 0.46/0.92 (declare-const tptp.collec1582599068lle_tv (-> (-> tptp.produc1443694919lle_tv Bool) tptp.set_Pr1723822845lle_tv)) % 0.46/0.92 (declare-const tptp.top_to1871154984lle_tv tptp.set_Pr2014382200lle_tv) % 0.46/0.92 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 0.46/0.92 (declare-const tptp.paraco367965286_Truth tptp.paraco1604210848lle_fm) % 0.46/0.92 (declare-const tptp.collec848462447tv_nat (-> (-> tptp.produc194167194tv_nat Bool) tptp.set_Pr1725653840tv_nat)) % 0.46/0.92 (declare-const tptp.paraco55203475lid_in (-> tptp.set_nat tptp.paraco1604210848lle_fm Bool)) % 0.46/0.92 (declare-const tptp.collec924990229lle_tv (-> (-> tptp.produc270694976lle_tv Bool) tptp.set_Pr13445366lle_tv)) % 0.46/0.92 (declare-const tptp.the_inv_into_nat_nat (-> tptp.set_nat (-> tptp.nat tptp.nat) tptp.nat tptp.nat)) % 0.46/0.92 (declare-const tptp.accp_P2085826120lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool) tptp.produc931990033lle_tv Bool)) % 0.46/0.92 (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.92 (declare-const tptp.produc42536895at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat)) % 0.46/0.92 (declare-const tptp.produc1942165868lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc696645085lle_fm tptp.produc696645085lle_fm)) % 0.46/0.92 (declare-const tptp.produc939316703lle_tv (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.produc931990033lle_tv tptp.produc931990033lle_tv)) % 0.46/0.92 (declare-const tptp.produc1807466521lle_tv (-> (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm) tptp.produc696645085lle_fm tptp.produc696645085lle_fm)) % 0.46/0.92 (declare-const tptp.produc109093078at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc931990033lle_tv tptp.produc931990033lle_tv)) % 0.46/0.92 (declare-const tptp.paraco1632582009tv_rel (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool)) % 0.46/0.92 (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.92 (declare-const tptp.produc2101297531lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv)) % 0.46/0.92 (define tptp.paraco761681009ge_int () (let ((_let_1 (@var "S" tptp.list_char))) (let ((_let_2 (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv)))) (let ((_let_3 (@var "F" (-> tptp.nat tptp.nat)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.paraco1147068288nge_tv _let_3) (_ _let_2 _let_1))))))) % 0.46/0.92 (define tptp.paraco327635598_valid () (let ((_let_1 (@var "P" tptp.paraco1604210848lle_fm))) (let ((_let_2 (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv)))) (lambda (@list _let_1) (forall (@list _let_2) (= (_ (_ tptp.paraco1325918602e_eval _let_2) _let_1) (_ tptp.paraco1344940915le_Det true))))))) % 0.46/0.92 (define tptp.top_to1299250770e_tv_o () (lambda (@list (@var "X2" tptp.paraco1605129243lle_tv)) tptp.top_top_o)) % 0.46/0.92 (define tptp.top_top_nat_o () (lambda (@list (@var "X2" tptp.nat)) tptp.top_top_o)) % 0.46/0.92 (define tptp.inj_on2112487900lle_tv () (let ((_let_1 (@var "Y4" tptp.produc1647334210lle_tv))) (let ((_let_2 (@var "X2" tptp.produc1647334210lle_tv))) (let ((_let_3 (@var "F" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on552895452tv_nat () (let ((_let_1 (@var "Y4" tptp.produc194167194tv_nat))) (let ((_let_2 (@var "X2" tptp.produc194167194tv_nat))) (let ((_let_3 (@var "F" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on1745913142lle_tv () (let ((_let_1 (@var "Y4" tptp.produc270694976lle_tv))) (let ((_let_2 (@var "X2" tptp.produc270694976lle_tv))) (let ((_let_3 (@var "F" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on26176689at_nat () (let ((_let_1 (@var "Y4" tptp.product_prod_nat_nat))) (let ((_let_2 (@var "X2" tptp.product_prod_nat_nat))) (let ((_let_3 (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on1955349912lle_tv () (let ((_let_1 (@var "Y4" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "F" (-> tptp.nat tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on_nat_nat () (let ((_let_1 (@var "Y4" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "F" (-> tptp.nat tptp.nat)))) (let ((_let_4 (@var "A4" 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.92 (define tptp.inj_on772319074lle_tv () (let ((_let_1 (@var "Y4" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "X2" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A4" 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.92 (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.92 (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.92 (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.92 (define tptp.produc234482697lle_tv () (let ((_let_1 (@var "F23" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "F12" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "Bool2" Bool))) (lambda (@list _let_2 _let_1 _let_3) (_ (_ (_ tptp.if_Par1134130401lle_tv _let_3) _let_2) _let_1)))))) % 0.46/0.92 (define tptp.produc1232814113lle_tv () (let ((_let_1 (@var "P" tptp.produc1443694919lle_tv))) (lambda (@list _let_1) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv _let_1)) (_ tptp.produc262413013lle_tv _let_1))))) % 0.46/0.92 (define tptp.produc178635363at_nat () (let ((_let_1 (@var "P" tptp.produc596913417at_nat))) (lambda (@list _let_1) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat _let_1)) (_ tptp.produc1589291287at_nat _let_1))))) % 0.46/0.92 (define @t1 () (_ tptp.paraco1344940915le_Det true)) % 0.46/0.92 (define @t2 () (_ tptp.paraco1325918602e_eval tptp.i)) % 0.46/0.92 (define @t3 () (_ @t2 tptp.p2)) % 0.46/0.92 (define @t4 () (_ tptp.paraco1147068288nge_tv tptp.f)) % 0.46/0.92 (define @t5 () (_ @t4 @t3)) % 0.46/0.92 (define @t6 () (_ tptp.paraco1325918602e_eval (_ (_ tptp.paraco761681009ge_int tptp.f) tptp.i))) % 0.46/0.92 (define @t7 () (_ @t6 tptp.p2)) % 0.46/0.92 (define @t8 () (= @t7 @t5)) % 0.46/0.92 (define @t9 () (@var "Y1" Bool)) % 0.46/0.92 (define @t10 () (@var "X1" Bool)) % 0.46/0.92 (define @t11 () (_ tptp.paraco1344940915le_Det @t10)) % 0.46/0.92 (define @t12 () (_ @t2 tptp.p1)) % 0.46/0.92 (define @t13 () (@var "B" Bool)) % 0.46/0.92 (define @t14 () (_ tptp.paraco1344940915le_Det @t13)) % 0.46/0.92 (define @t15 () (@var "F2" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t16 () (_ tptp.paraco1147068288nge_tv @t15)) % 0.46/0.92 (define @t17 () (@var "I2" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t18 () (_ tptp.paraco1325918602e_eval @t17)) % 0.46/0.92 (define @t19 () (_ tptp.paraco1344940915le_Det false)) % 0.46/0.92 (define @t20 () (@var "Q" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t21 () (@var "P2" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t22 () (_ @t18 (_ (_ tptp.paraco1389086619le_Eql @t21) @t20))) % 0.46/0.92 (define @t23 () (_ @t18 @t20)) % 0.46/0.92 (define @t24 () (_ @t18 @t21)) % 0.46/0.92 (define @t25 () (= @t24 @t23)) % 0.46/0.92 (define @t26 () (not @t25)) % 0.46/0.92 (define @t27 () (@list @t17 @t21 @t20)) % 0.46/0.92 (define @t28 () (_ (_ tptp.paraco69239110le_Con @t21) @t20)) % 0.46/0.92 (define @t29 () (_ @t18 @t28)) % 0.46/0.92 (define @t30 () (= @t23 @t1)) % 0.46/0.92 (define @t31 () (not @t30)) % 0.46/0.92 (define @t32 () (= @t29 @t24)) % 0.46/0.92 (define @t33 () (= @t24 @t1)) % 0.46/0.92 (define @t34 () (not @t33)) % 0.46/0.92 (define @t35 () (@var "F1" (-> Bool tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t36 () (@var "F22" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t37 () (_ (_ tptp.paraco2051596139lle_tv @t35) @t36)) % 0.46/0.92 (define @t38 () (_ @t18 (_ tptp.paraco445776468le_Neg @t21))) % 0.46/0.92 (define @t39 () (= @t24 @t19)) % 0.46/0.92 (define @t40 () (not @t39)) % 0.46/0.92 (define @t41 () (@list @t17 @t21)) % 0.46/0.92 (define @t42 () (@var "Y3" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t43 () (@var "X3" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t44 () (_ tptp.paraco445776468le_Neg @t43)) % 0.46/0.92 (define @t45 () (@var "Y42" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t46 () (@var "X42" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t47 () (@var "Y41" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t48 () (@var "X41" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t49 () (_ (_ tptp.paraco69239110le_Con @t48) @t46)) % 0.46/0.92 (define @t50 () (@var "Y62" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t51 () (@var "X62" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t52 () (@var "Y61" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t53 () (@var "X61" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t54 () (_ (_ tptp.paraco1745535428le_Eql @t53) @t51)) % 0.46/0.92 (define @t55 () (@var "Y52" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t56 () (@var "X52" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t57 () (@var "Y51" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t58 () (@var "X51" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t59 () (_ (_ tptp.paraco1389086619le_Eql @t58) @t56)) % 0.46/0.92 (define @t60 () (_ tptp.paraco327635598_valid @t21)) % 0.46/0.92 (define @t61 () (_ @t18 (_ (_ tptp.paraco1745535428le_Eql @t21) @t20))) % 0.46/0.92 (define @t62 () (= @t23 @t19)) % 0.46/0.92 (define @t63 () (@var "P" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t64 () (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t65 () (_ tptp.paraco1325918602e_eval @t64)) % 0.46/0.92 (define @t66 () (@var "X" tptp.produc596913417at_nat)) % 0.46/0.92 (define @t67 () (@var "X" tptp.produc1443694919lle_tv)) % 0.46/0.92 (define @t68 () (@var "X" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t69 () (@list @t68)) % 0.46/0.92 (define @t70 () (@var "X" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t71 () (@list @t70)) % 0.46/0.92 (define @t72 () (@var "X" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t73 () (_ tptp.member737151281tv_nat @t72)) % 0.46/0.92 (define @t74 () (@var "X" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t75 () (_ tptp.member813679063lle_tv @t74)) % 0.46/0.92 (define @t76 () (@var "X" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t77 () (_ tptp.member701585322at_nat @t76)) % 0.46/0.92 (define @t78 () (@var "X" tptp.nat)) % 0.46/0.92 (define @t79 () (_ tptp.member_nat @t78)) % 0.46/0.92 (define @t80 () (@var "X" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t81 () (_ tptp.member266900804lle_tv @t80)) % 0.46/0.92 (define @t82 () (@list @t80)) % 0.46/0.92 (define @t83 () (@var "Y" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t84 () (@var "X" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t85 () (= @t84 @t83)) % 0.46/0.92 (define @t86 () (@var "F2" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.92 (define @t87 () (= (_ @t86 @t84) (_ @t86 @t83))) % 0.46/0.92 (define @t88 () (_ tptp.inj_on2112487900lle_tv @t86)) % 0.46/0.92 (define @t89 () (_ @t88 tptp.top_to1871154984lle_tv)) % 0.46/0.92 (define @t90 () (@list @t86 @t84 @t83)) % 0.46/0.92 (define @t91 () (@var "Y" tptp.nat)) % 0.46/0.92 (define @t92 () (= @t78 @t91)) % 0.46/0.92 (define @t93 () (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t94 () (= (_ @t93 @t78) (_ @t93 @t91))) % 0.46/0.92 (define @t95 () (_ tptp.inj_on1955349912lle_tv @t93)) % 0.46/0.92 (define @t96 () (_ @t95 tptp.top_top_set_nat)) % 0.46/0.92 (define @t97 () (@list @t93 @t78 @t91)) % 0.46/0.92 (define @t98 () (@var "Y" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t99 () (= @t72 @t98)) % 0.46/0.92 (define @t100 () (@var "F2" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.92 (define @t101 () (= (_ @t100 @t72) (_ @t100 @t98))) % 0.46/0.92 (define @t102 () (_ tptp.inj_on552895452tv_nat @t100)) % 0.46/0.92 (define @t103 () (_ @t102 tptp.top_to975729152tv_nat)) % 0.46/0.92 (define @t104 () (@list @t100 @t72 @t98)) % 0.46/0.92 (define @t105 () (@var "Y" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t106 () (= @t74 @t105)) % 0.46/0.92 (define @t107 () (@var "F2" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.92 (define @t108 () (= (_ @t107 @t74) (_ @t107 @t105))) % 0.46/0.92 (define @t109 () (_ tptp.inj_on1745913142lle_tv @t107)) % 0.46/0.92 (define @t110 () (_ @t109 tptp.top_to1411004326lle_tv)) % 0.46/0.92 (define @t111 () (@list @t107 @t74 @t105)) % 0.46/0.92 (define @t112 () (@var "Y" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t113 () (= @t76 @t112)) % 0.46/0.92 (define @t114 () (@var "F2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.92 (define @t115 () (= (_ @t114 @t76) (_ @t114 @t112))) % 0.46/0.92 (define @t116 () (_ tptp.inj_on26176689at_nat @t114)) % 0.46/0.92 (define @t117 () (_ @t116 tptp.top_to1555900337at_nat)) % 0.46/0.92 (define @t118 () (@list @t114 @t76 @t112)) % 0.46/0.92 (define @t119 () (_ @t15 @t78)) % 0.46/0.92 (define @t120 () (= @t119 (_ @t15 @t91))) % 0.46/0.92 (define @t121 () (_ tptp.inj_on_nat_nat @t15)) % 0.46/0.92 (define @t122 () (_ @t121 tptp.top_top_set_nat)) % 0.46/0.92 (define @t123 () (@list @t15 @t78 @t91)) % 0.46/0.92 (define @t124 () (@var "Y" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t125 () (= @t80 @t124)) % 0.46/0.92 (define @t126 () (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t127 () (_ @t126 @t124)) % 0.46/0.92 (define @t128 () (_ @t126 @t80)) % 0.46/0.92 (define @t129 () (= @t128 @t127)) % 0.46/0.92 (define @t130 () (_ tptp.inj_on772319074lle_tv @t126)) % 0.46/0.92 (define @t131 () (_ @t130 tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t132 () (@list @t126 @t80 @t124)) % 0.46/0.92 (define @t133 () (@var "Y2" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t134 () (@var "X4" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t135 () (_ @t86 @t134)) % 0.46/0.92 (define @t136 () (=> (= @t135 (_ @t86 @t133)) (= @t134 @t133))) % 0.46/0.92 (define @t137 () (@list @t134 @t133)) % 0.46/0.92 (define @t138 () (@list @t86)) % 0.46/0.92 (define @t139 () (@var "Y2" tptp.nat)) % 0.46/0.92 (define @t140 () (@var "X4" tptp.nat)) % 0.46/0.92 (define @t141 () (= @t140 @t139)) % 0.46/0.92 (define @t142 () (_ @t93 @t140)) % 0.46/0.92 (define @t143 () (=> (= @t142 (_ @t93 @t139)) @t141)) % 0.46/0.92 (define @t144 () (@list @t140 @t139)) % 0.46/0.92 (define @t145 () (@list @t93)) % 0.46/0.92 (define @t146 () (@var "Y2" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t147 () (@var "X4" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t148 () (_ @t100 @t147)) % 0.46/0.92 (define @t149 () (=> (= @t148 (_ @t100 @t146)) (= @t147 @t146))) % 0.46/0.92 (define @t150 () (@list @t147 @t146)) % 0.46/0.92 (define @t151 () (@list @t100)) % 0.46/0.92 (define @t152 () (@var "Y2" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t153 () (@var "X4" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t154 () (_ @t107 @t153)) % 0.46/0.92 (define @t155 () (=> (= @t154 (_ @t107 @t152)) (= @t153 @t152))) % 0.46/0.92 (define @t156 () (@list @t153 @t152)) % 0.46/0.92 (define @t157 () (@list @t107)) % 0.46/0.92 (define @t158 () (@var "Y2" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t159 () (@var "X4" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t160 () (_ @t114 @t159)) % 0.46/0.92 (define @t161 () (=> (= @t160 (_ @t114 @t158)) (= @t159 @t158))) % 0.46/0.92 (define @t162 () (@list @t159 @t158)) % 0.46/0.92 (define @t163 () (@list @t114)) % 0.46/0.92 (define @t164 () (_ @t15 @t140)) % 0.46/0.92 (define @t165 () (=> (= @t164 (_ @t15 @t139)) @t141)) % 0.46/0.92 (define @t166 () (@list @t15)) % 0.46/0.92 (define @t167 () (@var "Y2" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t168 () (@var "X4" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t169 () (_ @t126 @t168)) % 0.46/0.92 (define @t170 () (=> (= @t169 (_ @t126 @t167)) (= @t168 @t167))) % 0.46/0.92 (define @t171 () (@list @t168 @t167)) % 0.46/0.92 (define @t172 () (@list @t126)) % 0.46/0.92 (define @t173 () (= @t87 @t85)) % 0.46/0.92 (define @t174 () (= @t94 @t92)) % 0.46/0.92 (define @t175 () (= @t101 @t99)) % 0.46/0.92 (define @t176 () (= @t108 @t106)) % 0.46/0.92 (define @t177 () (= @t115 @t113)) % 0.46/0.92 (define @t178 () (= @t120 @t92)) % 0.46/0.92 (define @t179 () (= @t129 @t125)) % 0.46/0.92 (define @t180 () (@var "Y4" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t181 () (@var "X2" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t182 () (= @t181 @t180)) % 0.46/0.92 (define @t183 () (@var "Y4" tptp.nat)) % 0.46/0.92 (define @t184 () (@var "X2" tptp.nat)) % 0.46/0.92 (define @t185 () (= @t184 @t183)) % 0.46/0.92 (define @t186 () (_ @t93 @t184)) % 0.46/0.92 (define @t187 () (@list @t184 @t183)) % 0.46/0.92 (define @t188 () (@var "Y4" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t189 () (@var "X2" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t190 () (= @t189 @t188)) % 0.46/0.92 (define @t191 () (@var "Y4" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t192 () (@var "X2" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t193 () (= @t192 @t191)) % 0.46/0.92 (define @t194 () (@var "Y4" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t195 () (@var "X2" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t196 () (= @t195 @t194)) % 0.46/0.92 (define @t197 () (_ @t15 @t183)) % 0.46/0.92 (define @t198 () (_ @t15 @t184)) % 0.46/0.92 (define @t199 () (@var "Y4" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t200 () (@var "X2" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t201 () (= @t200 @t199)) % 0.46/0.92 (define @t202 () (_ @t126 @t199)) % 0.46/0.92 (define @t203 () (_ @t126 @t200)) % 0.46/0.92 (define @t204 () (@var "Fm" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t205 () (@var "P3" (-> tptp.paraco1604210848lle_fm Bool))) % 0.46/0.92 (define @t206 () (@var "X22" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t207 () (@var "X1a" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t208 () (_ @t205 @t206)) % 0.46/0.92 (define @t209 () (_ @t205 @t207)) % 0.46/0.92 (define @t210 () (@list @t207 @t206)) % 0.46/0.92 (define @t211 () (@var "X4" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t212 () (_ @t205 tptp.paraco367965286_Truth)) % 0.46/0.92 (define @t213 () (@var "X4" tptp.list_char)) % 0.46/0.92 (define @t214 () (@var "X622" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t215 () (@var "X612" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t216 () (@var "Y" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t217 () (@var "X522" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t218 () (@var "X512" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t219 () (@var "X422" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t220 () (@var "X412" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t221 () (@var "X32" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t222 () (@var "X12" tptp.list_char)) % 0.46/0.92 (define @t223 () (@var "A" tptp.produc596913417at_nat)) % 0.46/0.92 (define @t224 () (@var "P3" (-> tptp.produc596913417at_nat Bool))) % 0.46/0.92 (define @t225 () (@var "A" tptp.produc1443694919lle_tv)) % 0.46/0.92 (define @t226 () (@var "P3" (-> tptp.produc1443694919lle_tv Bool))) % 0.46/0.92 (define @t227 () (@var "A" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t228 () (@var "P3" (-> tptp.produc696645085lle_fm Bool))) % 0.46/0.92 (define @t229 () (@var "A" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t230 () (@var "P3" (-> tptp.produc931990033lle_tv Bool))) % 0.46/0.92 (define @t231 () (@var "A" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t232 () (@var "P3" (-> tptp.paraco1605129243lle_tv Bool))) % 0.46/0.92 (define @t233 () (_ tptp.collec1111687558lle_tv @t232)) % 0.46/0.92 (define @t234 () (_ tptp.member266900804lle_tv @t231)) % 0.46/0.92 (define @t235 () (@var "A" tptp.nat)) % 0.46/0.92 (define @t236 () (@var "P3" (-> tptp.nat Bool))) % 0.46/0.92 (define @t237 () (_ tptp.collect_nat @t236)) % 0.46/0.92 (define @t238 () (_ tptp.member_nat @t235)) % 0.46/0.92 (define @t239 () (@var "A2" tptp.set_Pr840833727at_nat)) % 0.46/0.92 (define @t240 () (@var "X2" tptp.produc596913417at_nat)) % 0.46/0.92 (define @t241 () (@list @t239)) % 0.46/0.92 (define @t242 () (@var "A2" tptp.set_Pr1723822845lle_tv)) % 0.46/0.92 (define @t243 () (@var "X2" tptp.produc1443694919lle_tv)) % 0.46/0.92 (define @t244 () (@list @t242)) % 0.46/0.92 (define @t245 () (@var "A2" tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (define @t246 () (@var "X2" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t247 () (@list @t245)) % 0.46/0.92 (define @t248 () (@var "A2" tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (define @t249 () (@var "X2" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t250 () (@list @t248)) % 0.46/0.92 (define @t251 () (@var "A2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t252 () (_ tptp.member266900804lle_tv @t200)) % 0.46/0.92 (define @t253 () (@list @t200)) % 0.46/0.92 (define @t254 () (@list @t251)) % 0.46/0.92 (define @t255 () (@var "A2" tptp.set_nat)) % 0.46/0.92 (define @t256 () (_ tptp.member_nat @t184)) % 0.46/0.92 (define @t257 () (@list @t184)) % 0.46/0.92 (define @t258 () (@list @t255)) % 0.46/0.92 (define @t259 () (@var "Q2" (-> tptp.paraco1605129243lle_tv Bool))) % 0.46/0.92 (define @t260 () (@list @t168)) % 0.46/0.92 (define @t261 () (@var "Q2" (-> tptp.nat Bool))) % 0.46/0.92 (define @t262 () (@list @t140)) % 0.46/0.92 (define @t263 () (@var "Q3" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t264 () (@var "P4" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t265 () (_ (_ tptp.paraco1745535428le_Eql @t264) @t263)) % 0.46/0.92 (define @t266 () (@var "X" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t267 () (@list @t264 @t263)) % 0.46/0.92 (define @t268 () (_ (_ tptp.paraco1389086619le_Eql @t264) @t263)) % 0.46/0.92 (define @t269 () (_ (_ tptp.paraco69239110le_Con @t264) @t263)) % 0.46/0.92 (define @t270 () (_ tptp.paraco445776468le_Neg @t264)) % 0.46/0.92 (define @t271 () (@list @t264)) % 0.46/0.92 (define @t272 () (@var "S2" tptp.list_char)) % 0.46/0.92 (define @t273 () (_ tptp.paraco1480028776le_Pro @t272)) % 0.46/0.92 (define @t274 () (@list @t272)) % 0.46/0.92 (define @t275 () (@var "Y1" tptp.list_char)) % 0.46/0.92 (define @t276 () (@var "X1" tptp.list_char)) % 0.46/0.92 (define @t277 () (_ tptp.paraco1480028776le_Pro @t276)) % 0.46/0.92 (define @t278 () (@var "S3" tptp.list_char)) % 0.46/0.92 (define @t279 () (@var "X4" tptp.produc596913417at_nat)) % 0.46/0.92 (define @t280 () (_ tptp.member1234290208at_nat @t279)) % 0.46/0.92 (define @t281 () (@list @t279)) % 0.46/0.92 (define @t282 () (@var "X4" tptp.produc1443694919lle_tv)) % 0.46/0.92 (define @t283 () (_ tptp.member74361182lle_tv @t282)) % 0.46/0.92 (define @t284 () (@list @t282)) % 0.46/0.92 (define @t285 () (@var "X4" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t286 () (_ tptp.member1474794996lle_fm @t285)) % 0.46/0.92 (define @t287 () (@list @t285)) % 0.46/0.92 (define @t288 () (@var "X4" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t289 () (_ tptp.member1569366824lle_tv @t288)) % 0.46/0.92 (define @t290 () (@list @t288)) % 0.46/0.92 (define @t291 () (_ tptp.member737151281tv_nat @t147)) % 0.46/0.92 (define @t292 () (@list @t147)) % 0.46/0.92 (define @t293 () (_ tptp.member813679063lle_tv @t153)) % 0.46/0.92 (define @t294 () (@list @t153)) % 0.46/0.92 (define @t295 () (_ tptp.member701585322at_nat @t159)) % 0.46/0.92 (define @t296 () (@list @t159)) % 0.46/0.92 (define @t297 () (_ tptp.member_nat @t140)) % 0.46/0.92 (define @t298 () (_ tptp.member266900804lle_tv @t168)) % 0.46/0.92 (define @t299 () (@var "A2" tptp.set_Pr1725653840tv_nat)) % 0.46/0.92 (define @t300 () (_ @t291 @t299)) % 0.46/0.92 (define @t301 () (@var "A2" tptp.set_Pr13445366lle_tv)) % 0.46/0.92 (define @t302 () (_ @t293 @t301)) % 0.46/0.92 (define @t303 () (@var "A2" tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (define @t304 () (_ @t295 @t303)) % 0.46/0.92 (define @t305 () (_ @t297 @t255)) % 0.46/0.92 (define @t306 () (_ @t298 @t251)) % 0.46/0.92 (define @t307 () (@var "A2" tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (define @t308 () (_ @t88 @t307)) % 0.46/0.92 (define @t309 () (@var "G" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.92 (define @t310 () (_ (_ tptp.member1531318361lle_tv @t134) @t307)) % 0.46/0.92 (define @t311 () (_ @t102 @t299)) % 0.46/0.92 (define @t312 () (@var "G" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.92 (define @t313 () (_ @t109 @t301)) % 0.46/0.92 (define @t314 () (@var "G" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.92 (define @t315 () (_ @t116 @t303)) % 0.46/0.92 (define @t316 () (@var "G" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.92 (define @t317 () (_ @t95 @t255)) % 0.46/0.92 (define @t318 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.nat))) % 0.46/0.92 (define @t319 () (= (_ @t318 @t142) @t140)) % 0.46/0.92 (define @t320 () (_ @t121 @t255)) % 0.46/0.92 (define @t321 () (@var "G" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t322 () (_ @t321 @t164)) % 0.46/0.92 (define @t323 () (= @t322 @t140)) % 0.46/0.92 (define @t324 () (@list @t255 @t321 @t15)) % 0.46/0.92 (define @t325 () (_ @t130 @t251)) % 0.46/0.92 (define @t326 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t327 () (_ @t326 @t169)) % 0.46/0.92 (define @t328 () (= @t327 @t168)) % 0.46/0.92 (define @t329 () (@list @t251 @t326 @t126)) % 0.46/0.92 (define @t330 () (_ (_ tptp.member1531318361lle_tv @t83) @t307)) % 0.46/0.92 (define @t331 () (_ (_ tptp.member1531318361lle_tv @t84) @t307)) % 0.46/0.92 (define @t332 () (@list @t86 @t307 @t84 @t83)) % 0.46/0.92 (define @t333 () (_ (_ tptp.member737151281tv_nat @t98) @t299)) % 0.46/0.92 (define @t334 () (_ @t73 @t299)) % 0.46/0.92 (define @t335 () (@list @t100 @t299 @t72 @t98)) % 0.46/0.92 (define @t336 () (_ (_ tptp.member813679063lle_tv @t105) @t301)) % 0.46/0.92 (define @t337 () (_ @t75 @t301)) % 0.46/0.92 (define @t338 () (@list @t107 @t301 @t74 @t105)) % 0.46/0.92 (define @t339 () (_ (_ tptp.member701585322at_nat @t112) @t303)) % 0.46/0.92 (define @t340 () (_ @t77 @t303)) % 0.46/0.92 (define @t341 () (@list @t114 @t303 @t76 @t112)) % 0.46/0.92 (define @t342 () (_ tptp.member_nat @t91)) % 0.46/0.92 (define @t343 () (_ @t342 @t255)) % 0.46/0.92 (define @t344 () (_ @t79 @t255)) % 0.46/0.92 (define @t345 () (not @t92)) % 0.46/0.92 (define @t346 () (@list @t93 @t255 @t78 @t91)) % 0.46/0.92 (define @t347 () (@list @t15 @t255 @t78 @t91)) % 0.46/0.92 (define @t348 () (_ tptp.member266900804lle_tv @t124)) % 0.46/0.92 (define @t349 () (_ @t348 @t251)) % 0.46/0.92 (define @t350 () (_ @t81 @t251)) % 0.46/0.92 (define @t351 () (@list @t126 @t251 @t80 @t124)) % 0.46/0.92 (define @t352 () (@var "A3" tptp.produc1647334210lle_tv)) % 0.46/0.92 (define @t353 () (@var "A3" tptp.produc194167194tv_nat)) % 0.46/0.92 (define @t354 () (@var "A3" tptp.produc270694976lle_tv)) % 0.46/0.92 (define @t355 () (@var "A3" tptp.product_prod_nat_nat)) % 0.46/0.92 (define @t356 () (@var "G" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t357 () (@var "A3" tptp.nat)) % 0.46/0.92 (define @t358 () (_ (_ tptp.member_nat @t357) @t255)) % 0.46/0.92 (define @t359 () (@list @t357)) % 0.46/0.92 (define @t360 () (_ tptp.inj_on_nat_nat @t321)) % 0.46/0.92 (define @t361 () (_ @t360 @t255)) % 0.46/0.92 (define @t362 () (_ tptp.inj_on772319074lle_tv @t326)) % 0.46/0.92 (define @t363 () (_ @t362 @t251)) % 0.46/0.92 (define @t364 () (@var "A3" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t365 () (_ (_ tptp.member_nat @t139) @t255)) % 0.46/0.92 (define @t366 () (=> @t344 (=> @t343 @t92))) % 0.46/0.92 (define @t367 () (@var "A0" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t368 () (_ @t205 @t263)) % 0.46/0.92 (define @t369 () (_ @t205 @t264)) % 0.46/0.92 (define @t370 () (@var "I3" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t371 () (_ tptp.produc1710735575lle_fm @t370)) % 0.46/0.92 (define @t372 () (@list @t370 @t264 @t263)) % 0.46/0.92 (define @t373 () (@var "N" tptp.nat)) % 0.46/0.92 (define @t374 () (@var "X" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t375 () (= @t124 (_ tptp.paraco793048302_Indet (_ @t374 @t373)))) % 0.46/0.92 (define @t376 () (_ tptp.paraco793048302_Indet @t373)) % 0.46/0.92 (define @t377 () (@var "Xa" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t378 () (= @t377 @t376)) % 0.46/0.92 (define @t379 () (@list @t373)) % 0.46/0.92 (define @t380 () (@var "B2" Bool)) % 0.46/0.92 (define @t381 () (_ tptp.paraco1344940915le_Det @t380)) % 0.46/0.92 (define @t382 () (= @t124 @t381)) % 0.46/0.92 (define @t383 () (= @t377 @t381)) % 0.46/0.92 (define @t384 () (@list @t380)) % 0.46/0.92 (define @t385 () (= (_ (_ tptp.paraco1147068288nge_tv @t374) @t377) @t124)) % 0.46/0.92 (define @t386 () (@list @t374 @t377 @t124)) % 0.46/0.92 (define @t387 () (@var "U" tptp.set_nat)) % 0.46/0.92 (define @t388 () (_ tptp.paraco55203475lid_in @t387)) % 0.46/0.92 (define @t389 () (_ @t388 @t21)) % 0.46/0.92 (define @t390 () (@var "Y22" tptp.nat)) % 0.46/0.92 (define @t391 () (@var "X23" tptp.nat)) % 0.46/0.92 (define @t392 () (_ tptp.paraco793048302_Indet @t391)) % 0.46/0.92 (define @t393 () (@var "A0" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t394 () (@var "A1" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t395 () (@var "A0" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t396 () (@var "P3" (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool))) % 0.46/0.92 (define @t397 () (@var "F3" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t398 () (_ @t396 @t397)) % 0.46/0.92 (define @t399 () (@list @t397 @t373)) % 0.46/0.92 (define @t400 () (@list @t397 @t380)) % 0.46/0.92 (define @t401 () (@var "X22" tptp.nat)) % 0.46/0.92 (define @t402 () (@var "X12" Bool)) % 0.46/0.92 (define @t403 () (@var "Tv" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t404 () (@var "X4" Bool)) % 0.46/0.92 (define @t405 () (_ (_ tptp.the_inv_into_nat_nat @t255) @t15)) % 0.46/0.92 (define @t406 () (_ (_ tptp.the_in452116896lle_tv @t251) @t126)) % 0.46/0.92 (define @t407 () (_ @t405 @t91)) % 0.46/0.92 (define @t408 () (_ @t406 @t124)) % 0.46/0.92 (define @t409 () (@var "N2" tptp.nat)) % 0.46/0.92 (define @t410 () (@var "Y22" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t411 () (@var "X23" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t412 () (@var "Y1" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t413 () (@var "X1" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t414 () (_ (_ tptp.produc1710735575lle_fm @t413) @t411)) % 0.46/0.92 (define @t415 () (@var "Y22" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t416 () (@var "X23" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t417 () (@var "Y1" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t418 () (@var "X1" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t419 () (_ (_ tptp.produc1680557635lle_tv @t418) @t416)) % 0.46/0.92 (define @t420 () (@var "B3" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t421 () (@var "B" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t422 () (= @t421 @t420)) % 0.46/0.92 (define @t423 () (@var "A5" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t424 () (@var "A" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t425 () (= @t424 @t423)) % 0.46/0.92 (define @t426 () (_ (_ tptp.produc1710735575lle_fm @t424) @t421)) % 0.46/0.92 (define @t427 () (= @t426 (_ (_ tptp.produc1710735575lle_fm @t423) @t420))) % 0.46/0.92 (define @t428 () (@list @t424 @t421 @t423 @t420)) % 0.46/0.92 (define @t429 () (@var "B3" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t430 () (@var "B" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t431 () (= @t430 @t429)) % 0.46/0.92 (define @t432 () (@var "A5" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t433 () (@var "A" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t434 () (= @t433 @t432)) % 0.46/0.92 (define @t435 () (_ (_ tptp.produc1680557635lle_tv @t433) @t430)) % 0.46/0.92 (define @t436 () (= @t435 (_ (_ tptp.produc1680557635lle_tv @t432) @t429))) % 0.46/0.92 (define @t437 () (@list @t433 @t430 @t432 @t429)) % 0.46/0.92 (define @t438 () (@var "Y2" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t439 () (@var "X4" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t440 () (_ (_ tptp.produc1710735575lle_fm @t439) @t438)) % 0.46/0.92 (define @t441 () (@var "P2" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t442 () (@list @t439 @t438)) % 0.46/0.92 (define @t443 () (@var "X4" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t444 () (_ (_ tptp.produc1680557635lle_tv @t443) @t167)) % 0.46/0.92 (define @t445 () (@var "P2" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t446 () (@list @t443 @t167)) % 0.46/0.92 (define @t447 () (@var "F22" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t448 () (_ @t232 @t447)) % 0.46/0.92 (define @t449 () (@var "Bool" Bool)) % 0.46/0.92 (define @t450 () (not @t449)) % 0.46/0.92 (define @t451 () (@var "F1" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t452 () (_ @t232 @t451)) % 0.46/0.92 (define @t453 () (_ (_ tptp.produc234482697lle_tv @t451) @t447)) % 0.46/0.92 (define @t454 () (_ @t453 @t449)) % 0.46/0.92 (define @t455 () (_ @t232 @t454)) % 0.46/0.92 (define @t456 () (@list @t232 @t451 @t447 @t449)) % 0.46/0.92 (define @t457 () (@var "H" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t458 () (@list @t451 @t447)) % 0.46/0.92 (define @t459 () (_ tptp.produc1680557635lle_tv @t397)) % 0.46/0.92 (define @t460 () (@var "Prod" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t461 () (@var "B2" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t462 () (@var "A3" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t463 () (_ (_ tptp.produc1710735575lle_fm @t462) @t461)) % 0.46/0.92 (define @t464 () (@list @t462 @t461)) % 0.46/0.92 (define @t465 () (forall @t464 (_ @t228 @t463))) % 0.46/0.92 (define @t466 () (@var "Prod" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t467 () (@var "B2" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t468 () (@var "A3" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t469 () (_ (_ tptp.produc1680557635lle_tv @t468) @t467)) % 0.46/0.92 (define @t470 () (@list @t468 @t467)) % 0.46/0.92 (define @t471 () (forall @t470 (_ @t230 @t469))) % 0.46/0.92 (define @t472 () (@var "Y" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t473 () (@var "Y" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t474 () (@var "R2" tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (define @t475 () (@var "S4" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t476 () (@var "R" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t477 () (_ tptp.produc1710735575lle_fm @t476)) % 0.46/0.92 (define @t478 () (@var "S3" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t479 () (@var "R2" tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (define @t480 () (@var "S4" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t481 () (@var "R" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t482 () (_ tptp.produc1680557635lle_tv @t481)) % 0.46/0.92 (define @t483 () (@var "S3" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t484 () (@var "X" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t485 () (@var "F2" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t486 () (_ tptp.produc1710735575lle_fm @t484)) % 0.46/0.92 (define @t487 () (_ @t486 @t216)) % 0.46/0.92 (define @t488 () (@var "F2" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 0.46/0.92 (define @t489 () (_ tptp.produc1680557635lle_tv @t374)) % 0.46/0.92 (define @t490 () (_ @t489 @t124)) % 0.46/0.92 (define @t491 () (@var "F2" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))) % 0.46/0.92 (define @t492 () (_ tptp.accp_P2085826120lle_tv tptp.paraco1632582009tv_rel)) % 0.46/0.92 (define @t493 () (@var "F22" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t494 () (@var "F1" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t495 () (_ (_ tptp.inj_on_nat_nat @t493) tptp.top_top_set_nat)) % 0.46/0.92 (define @t496 () (_ (_ tptp.inj_on_nat_nat @t494) tptp.top_top_set_nat)) % 0.46/0.92 (define @t497 () (@var "F22" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t498 () (_ (_ tptp.inj_on772319074lle_tv @t497) tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t499 () (@var "F1" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t500 () (_ (_ tptp.inj_on772319074lle_tv @t499) tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t501 () (@var "F2" (-> tptp.produc696645085lle_fm Bool))) % 0.46/0.92 (define @t502 () (_ (_ (_ tptp.produc275353523e_fm_o @t501) @t424) @t421)) % 0.46/0.92 (define @t503 () (_ @t501 @t426)) % 0.46/0.92 (define @t504 () (@list @t501 @t424 @t421)) % 0.46/0.92 (define @t505 () (@var "F2" (-> tptp.produc931990033lle_tv Bool))) % 0.46/0.92 (define @t506 () (_ (_ (_ tptp.produc752649287e_tv_o @t505) @t433) @t430)) % 0.46/0.92 (define @t507 () (_ @t505 @t435)) % 0.46/0.92 (define @t508 () (@list @t505 @t433 @t430)) % 0.46/0.92 (define @t509 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))) % 0.46/0.92 (define @t510 () (_ (_ tptp.produc1710735575lle_fm (_ @t485 @t424)) (_ @t509 @t421))) % 0.46/0.92 (define @t511 () (_ (_ tptp.produc1900967599lle_fm @t485) @t509)) % 0.46/0.92 (define @t512 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t513 () (@var "F2" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.nat tptp.nat))) % 0.46/0.92 (define @t514 () (_ (_ tptp.produc1680557635lle_tv (_ @t513 @t424)) (_ @t512 @t421))) % 0.46/0.92 (define @t515 () (_ (_ tptp.produc1566550641lle_tv @t513) @t512)) % 0.46/0.92 (define @t516 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1604210848lle_fm))) % 0.46/0.92 (define @t517 () (@var "F2" (-> (-> tptp.nat tptp.nat) tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t518 () (_ (_ tptp.produc1710735575lle_fm (_ @t517 @t433)) (_ @t516 @t430))) % 0.46/0.92 (define @t519 () (_ (_ tptp.produc951033137lle_fm @t517) @t516)) % 0.46/0.92 (define @t520 () (_ (_ tptp.produc1680557635lle_tv (_ @t488 @t433)) (_ @t326 @t430))) % 0.46/0.92 (define @t521 () (_ (_ tptp.produc532909085lle_tv @t488) @t326)) % 0.46/0.92 (define @t522 () (_ tptp.image_nat_nat @t15)) % 0.46/0.92 (define @t523 () (_ @t522 @t255)) % 0.46/0.92 (define @t524 () (@list @t15 @t255)) % 0.46/0.92 (define @t525 () (_ tptp.image_335818702lle_tv @t126)) % 0.46/0.92 (define @t526 () (_ @t525 @t251)) % 0.46/0.92 (define @t527 () (@list @t126 @t251)) % 0.46/0.92 (define @t528 () (_ (_ tptp.image_807538418lle_fm @t511) @t474)) % 0.46/0.92 (define @t529 () (_ (_ tptp.member1474794996lle_fm @t426) @t474)) % 0.46/0.92 (define @t530 () (_ (_ tptp.image_1154804148lle_tv @t515) @t474)) % 0.46/0.92 (define @t531 () (_ (_ tptp.image_1585092542lle_fm @t519) @t479)) % 0.46/0.92 (define @t532 () (_ (_ tptp.member1569366824lle_tv @t435) @t479)) % 0.46/0.92 (define @t533 () (_ (_ tptp.image_1751508608lle_tv @t521) @t479)) % 0.46/0.92 (define @t534 () (@var "Y" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t535 () (_ (_ tptp.produc1710735575lle_fm @t534) @t266)) % 0.46/0.92 (define @t536 () (_ (_ tptp.produc1943344577lle_tv @t266) @t534)) % 0.46/0.92 (define @t537 () (@var "Y" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t538 () (_ (_ tptp.produc1680557635lle_tv @t537) @t80)) % 0.46/0.92 (define @t539 () (_ (_ tptp.produc1633679363at_nat @t80) @t537)) % 0.46/0.92 (define @t540 () (_ (_ tptp.produc1943344577lle_tv @t216) @t484)) % 0.46/0.92 (define @t541 () (_ (_ tptp.produc1633679363at_nat @t124) @t374)) % 0.46/0.92 (define @t542 () (@var "Xa2" tptp.nat)) % 0.46/0.92 (define @t543 () (@var "Xa2" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t544 () (= @t91 @t164)) % 0.46/0.92 (define @t545 () (_ @t522 tptp.top_top_set_nat)) % 0.46/0.92 (define @t546 () (= @t545 tptp.top_top_set_nat)) % 0.46/0.92 (define @t547 () (@list @t15 @t91)) % 0.46/0.92 (define @t548 () (= @t124 @t142)) % 0.46/0.92 (define @t549 () (= (_ (_ tptp.image_1151963140lle_tv @t93) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t550 () (@list @t93 @t124)) % 0.46/0.92 (define @t551 () (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.nat))) % 0.46/0.92 (define @t552 () (_ @t551 @t168)) % 0.46/0.92 (define @t553 () (= @t91 @t552)) % 0.46/0.92 (define @t554 () (= (_ (_ tptp.image_376325286tv_nat @t551) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat)) % 0.46/0.92 (define @t555 () (@list @t551 @t91)) % 0.46/0.92 (define @t556 () (= @t124 @t169)) % 0.46/0.92 (define @t557 () (_ @t525 tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t558 () (= @t557 tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t559 () (@list @t126 @t124)) % 0.46/0.92 (define @t560 () (= (_ (_ tptp.image_nat_nat @t321) tptp.top_top_set_nat) tptp.top_top_set_nat)) % 0.46/0.92 (define @t561 () (= (_ (_ tptp.image_1151963140lle_tv @t356) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t562 () (= (_ (_ tptp.image_376325286tv_nat @t318) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat)) % 0.46/0.92 (define @t563 () (= (_ (_ tptp.image_335818702lle_tv @t326) tptp.top_to1057771083lle_tv) tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t564 () (@list @t183)) % 0.46/0.92 (define @t565 () (@list @t199)) % 0.46/0.92 (define @t566 () (@var "B" tptp.nat)) % 0.46/0.92 (define @t567 () (@var "B4" tptp.set_nat)) % 0.46/0.92 (define @t568 () (_ @t522 @t567)) % 0.46/0.92 (define @t569 () (= (= @t523 @t568) (= @t255 @t567))) % 0.46/0.92 (define @t570 () (@list @t15 @t255 @t567)) % 0.46/0.92 (define @t571 () (@var "B4" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t572 () (_ @t525 @t571)) % 0.46/0.92 (define @t573 () (= (= @t526 @t572) (= @t251 @t571))) % 0.46/0.92 (define @t574 () (@list @t126 @t251 @t571)) % 0.46/0.92 (define @t575 () (= (_ (_ tptp.member_nat (_ @t15 @t235)) @t523) (_ @t238 @t255))) % 0.46/0.92 (define @t576 () (= (_ (_ tptp.member266900804lle_tv (_ @t126 @t231)) @t526) (_ @t234 @t251))) % 0.46/0.92 (define @t577 () (_ tptp.member1474794996lle_fm @t440)) % 0.46/0.92 (define @t578 () (not (_ @t577 @t474))) % 0.46/0.92 (define @t579 () (@var "C" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t580 () (_ tptp.member1474794996lle_fm @t579)) % 0.46/0.92 (define @t581 () (_ tptp.member1569366824lle_tv @t444)) % 0.46/0.92 (define @t582 () (not (_ @t581 @t479))) % 0.46/0.92 (define @t583 () (@var "C" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t584 () (_ tptp.member1569366824lle_tv @t583)) % 0.46/0.92 (define @t585 () (@var "R" tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (define @t586 () (_ tptp.total_on_nat tptp.top_top_set_nat)) % 0.46/0.92 (define @t587 () (_ @t586 @t585)) % 0.46/0.92 (define @t588 () (@var "R" tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (define @t589 () (_ tptp.total_1781621663lle_tv tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t590 () (_ @t589 @t588)) % 0.46/0.92 (define @t591 () (_ tptp.ord_less_eq_set_nat @t255)) % 0.46/0.92 (define @t592 () (_ @t591 @t567)) % 0.46/0.92 (define @t593 () (_ tptp.ord_le241064091lle_tv @t251)) % 0.46/0.92 (define @t594 () (_ @t593 @t571)) % 0.46/0.92 (define @t595 () (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t460)) (_ tptp.produc148705065lle_fm @t460))) % 0.46/0.92 (define @t596 () (@list @t460)) % 0.46/0.92 (define @t597 () (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t466)) (_ tptp.produc547496597lle_tv @t466))) % 0.46/0.92 (define @t598 () (@list @t466)) % 0.46/0.92 (define @t599 () (_ tptp.produc29804011lle_fm @t487)) % 0.46/0.92 (define @t600 () (_ tptp.produc1636169559lle_tv @t490)) % 0.46/0.92 (define @t601 () (@var "A" tptp.paraco1604210848lle_fm)) % 0.46/0.92 (define @t602 () (_ tptp.produc148705065lle_fm @t487)) % 0.46/0.92 (define @t603 () (_ tptp.produc547496597lle_tv @t490)) % 0.46/0.92 (define @t604 () (@list @t413 @t411)) % 0.46/0.92 (define @t605 () (@list @t418 @t416)) % 0.46/0.92 (define @t606 () (@var "T" tptp.produc696645085lle_fm)) % 0.46/0.92 (define @t607 () (@var "T" tptp.produc931990033lle_tv)) % 0.46/0.92 (define @t608 () (@var "S3" tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (define @t609 () (@var "R" tptp.set_Pr2120184979lle_fm)) % 0.46/0.92 (define @t610 () (@var "S3" tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (define @t611 () (@var "R" tptp.set_Pr560526279lle_tv)) % 0.46/0.92 (define @t612 () (@var "A" tptp.set_nat)) % 0.46/0.92 (define @t613 () (@list @t612)) % 0.46/0.92 (define @t614 () (@var "A" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t615 () (@list @t614)) % 0.46/0.92 (define @t616 () (= @t612 tptp.top_top_set_nat)) % 0.46/0.92 (define @t617 () (_ (_ tptp.ord_less_eq_set_nat tptp.top_top_set_nat) @t612)) % 0.46/0.92 (define @t618 () (= @t614 tptp.top_to1057771083lle_tv)) % 0.46/0.92 (define @t619 () (_ (_ tptp.ord_le241064091lle_tv tptp.top_to1057771083lle_tv) @t614)) % 0.46/0.92 (define @t620 () (_ @t121 @t567)) % 0.46/0.92 (define @t621 () (_ tptp.ord_less_eq_set_nat @t567)) % 0.46/0.92 (define @t622 () (_ @t130 @t571)) % 0.46/0.92 (define @t623 () (_ tptp.ord_le241064091lle_tv @t571)) % 0.46/0.92 (define @t624 () (@var "C2" tptp.set_nat)) % 0.46/0.92 (define @t625 () (@var "C2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t626 () (@var "P3" (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool))) % 0.46/0.92 (define @t627 () (@var "P3" (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) Bool))) % 0.46/0.92 (define @t628 () (@var "P2" (-> tptp.list_char tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t629 () (_ (_ tptp.produc1710735575lle_fm @t628) @t20)) % 0.46/0.92 (define @t630 () (@var "Q2" (-> tptp.paraco1604210848lle_fm Bool))) % 0.46/0.92 (define @t631 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool))) % 0.46/0.92 (define @t632 () (@var "Q" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t633 () (@var "P2" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t634 () (_ (_ tptp.produc1680557635lle_tv @t633) @t632)) % 0.46/0.92 (define @t635 () (@var "P3" (-> (-> tptp.nat tptp.nat) Bool))) % 0.46/0.92 (define @t636 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool))) % 0.46/0.92 (define @t637 () (@var "U2" tptp.set_nat)) % 0.46/0.92 (define @t638 () (@var "S5" tptp.set_nat)) % 0.46/0.92 (define @t639 () (@var "T2" tptp.set_nat)) % 0.46/0.92 (define @t640 () (@var "U2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t641 () (@var "S5" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t642 () (@var "T2" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t643 () (@var "P3" Bool)) % 0.46/0.92 (define @t644 () (@list @t80 @t124)) % 0.46/0.92 (define @t645 () (= @t7 @t1)) % 0.46/0.92 (define @t646 () (not @t645)) % 0.46/0.92 (define @t647 () (@var "S" tptp.list_char)) % 0.46/0.92 (define @t648 () (_ @t64 @t647)) % 0.46/0.92 (define @t649 () (@var "F" (-> tptp.nat tptp.nat))) % 0.46/0.92 (define @t650 () (lambda (@list @t649 @t64 @t647) (_ (_ tptp.paraco1147068288nge_tv @t649) @t648))) % 0.46/0.92 (define @t651 () (lambda (@list @t63) (forall (@list @t64) (= (_ @t65 @t63) @t1)))) % 0.46/0.92 (define @t652 () (lambda @t253 tptp.top_top_o)) % 0.46/0.92 (define @t653 () (lambda @t257 tptp.top_top_o)) % 0.46/0.92 (define @t654 () (@var "F" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))) % 0.46/0.92 (define @t655 () (@var "A4" tptp.set_Pr2014382200lle_tv)) % 0.46/0.92 (define @t656 () (lambda (@list @t654 @t655) (forall (@list @t181) (=> (_ (_ tptp.member1531318361lle_tv @t181) @t655) (forall (@list @t180) (=> (_ (_ tptp.member1531318361lle_tv @t180) @t655) (=> (= (_ @t654 @t181) (_ @t654 @t180)) @t182))))))) % 0.46/0.92 (define @t657 () (@var "F" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat))) % 0.46/0.92 (define @t658 () (@var "A4" tptp.set_Pr1725653840tv_nat)) % 0.46/0.92 (define @t659 () (_ tptp.member737151281tv_nat @t189)) % 0.46/0.92 (define @t660 () (@list @t189)) % 0.46/0.92 (define @t661 () (lambda (@list @t657 @t658) (forall @t660 (=> (_ @t659 @t658) (forall (@list @t188) (=> (_ (_ tptp.member737151281tv_nat @t188) @t658) (=> (= (_ @t657 @t189) (_ @t657 @t188)) @t190))))))) % 0.46/0.92 (define @t662 () (@var "F" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv))) % 0.46/0.92 (define @t663 () (@var "A4" tptp.set_Pr13445366lle_tv)) % 0.46/0.92 (define @t664 () (_ tptp.member813679063lle_tv @t192)) % 0.46/0.92 (define @t665 () (@list @t192)) % 0.46/0.92 (define @t666 () (lambda (@list @t662 @t663) (forall @t665 (=> (_ @t664 @t663) (forall (@list @t191) (=> (_ (_ tptp.member813679063lle_tv @t191) @t663) (=> (= (_ @t662 @t192) (_ @t662 @t191)) @t193))))))) % 0.46/0.92 (define @t667 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat))) % 0.46/0.92 (define @t668 () (@var "A4" tptp.set_Pr1986765409at_nat)) % 0.46/0.92 (define @t669 () (_ tptp.member701585322at_nat @t195)) % 0.46/0.92 (define @t670 () (@list @t195)) % 0.46/0.92 (define @t671 () (lambda (@list @t667 @t668) (forall @t670 (=> (_ @t669 @t668) (forall (@list @t194) (=> (_ (_ tptp.member701585322at_nat @t194) @t668) (=> (= (_ @t667 @t195) (_ @t667 @t194)) @t196))))))) % 0.46/0.92 (define @t672 () (@var "F" (-> tptp.nat tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t673 () (@var "A4" tptp.set_nat)) % 0.46/0.92 (define @t674 () (_ (_ tptp.member_nat @t183) @t673)) % 0.46/0.92 (define @t675 () (_ @t256 @t673)) % 0.46/0.92 (define @t676 () (lambda (@list @t672 @t673) (forall @t257 (=> @t675 (forall @t564 (=> @t674 (=> (= (_ @t672 @t184) (_ @t672 @t183)) @t185))))))) % 0.46/0.92 (define @t677 () (lambda (@list @t649 @t673) (forall @t257 (=> @t675 (forall @t564 (=> @t674 (=> (= (_ @t649 @t184) (_ @t649 @t183)) @t185))))))) % 0.46/0.92 (define @t678 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))) % 0.46/0.92 (define @t679 () (@var "A4" tptp.set_Pa1764573435lle_tv)) % 0.46/0.92 (define @t680 () (lambda (@list @t678 @t679) (forall @t253 (=> (_ @t252 @t679) (forall @t565 (=> (_ (_ tptp.member266900804lle_tv @t199) @t679) (=> (= (_ @t678 @t200) (_ @t678 @t199)) @t201))))))) % 0.46/0.92 (define @t681 () (lambda @t660 (_ @t659 tptp.top_to975729152tv_nat))) % 0.46/0.92 (define @t682 () (lambda @t665 (_ @t664 tptp.top_to1411004326lle_tv))) % 0.46/0.92 (define @t683 () (lambda @t670 (_ @t669 tptp.top_to1555900337at_nat))) % 0.46/0.92 (define @t684 () (@var "F23" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t685 () (@var "F12" tptp.paraco1605129243lle_tv)) % 0.46/0.92 (define @t686 () (@var "Bool2" Bool)) % 0.46/0.92 (define @t687 () (lambda (@list @t685 @t684 @t686) (_ (_ (_ tptp.if_Par1134130401lle_tv @t686) @t685) @t684))) % 0.46/0.92 (define @t688 () (@var "P" tptp.produc1443694919lle_tv)) % 0.46/0.92 (define @t689 () (lambda (@list @t688) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv @t688)) (_ tptp.produc262413013lle_tv @t688)))) % 0.46/0.92 (define @t690 () (@var "P" tptp.produc596913417at_nat)) % 0.46/0.92 (define @t691 () (lambda (@list @t690) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat @t690)) (_ tptp.produc1589291287at_nat @t690)))) % 0.46/0.92 (define @t692 () (tptp.paraco1325918602e_eval tptp.i tptp.p2)) % 0.46/0.92 (define @t693 () (tptp.paraco1147068288nge_tv tptp.f @t692)) % 0.46/0.92 (define @t694 () (@purify true)) % 0.46/0.92 (define @t695 () (tptp.paraco1344940915le_Det @t694)) % 0.46/0.92 (define @t696 () (_ tptp.paraco1344940915le_Det @t694)) % 0.46/0.92 (define @t697 () (lambda (@list @t647) (_ @t4 (_ tptp.i @t647)))) % 0.46/0.92 (define @t698 () (@purify @t697)) % 0.46/0.92 (define @t699 () (tptp.paraco1325918602e_eval @t698 tptp.p2)) % 0.46/0.92 (define @t700 () (_ (_ tptp.paraco1325918602e_eval @t698) tptp.p2)) % 0.46/0.92 (define @t701 () (_ (_ tptp.paraco1325918602e_eval @t697) tptp.p2)) % 0.46/0.92 (define @t702 () (lambda (@list @t64 @t647) (_ @t4 @t648))) % 0.46/0.92 (define @t703 () (_ @t650 tptp.f)) % 0.46/0.92 (define @t704 () (_ (_ tptp.paraco1325918602e_eval (_ @t703 tptp.i)) tptp.p2)) % 0.46/0.92 (define @t705 () (= @t1 @t701)) % 0.46/0.92 (define @t706 () (= @t704 @t1)) % 0.46/0.92 (define @t707 () (= @t695 @t693)) % 0.46/0.92 (define @t708 () (= @t693 @t699)) % 0.46/0.92 (define @t709 () (= @t695 @t699)) % 0.46/0.92 (define @t710 () (and @t707 @t708)) % 0.46/0.92 (assume @p1 (= @t3 @t1)) % 0.46/0.92 (assume @p2 (= @t5 @t1)) % 0.46/0.92 (assume @p3 @t8) % 0.46/0.92 (assume @p4 (forall (@list @t10 @t9) (= (= @t11 (_ tptp.paraco1344940915le_Det @t9)) (= @t10 @t9)))) % 0.46/0.92 (assume @p5 (not (= @t12 @t1))) % 0.46/0.92 (assume @p6 (not (= @t12 @t3))) % 0.46/0.92 (assume @p7 (= (_ @t6 tptp.p1) (_ @t4 @t12))) % 0.46/0.92 (assume @p8 (forall (@list @t15 @t13) (= (_ @t16 @t14) @t14))) % 0.46/0.92 (assume @p9 (= (_ @t2 (_ (_ tptp.paraco1745535428le_Eql tptp.p1) tptp.p2)) @t12)) % 0.46/0.92 (assume @p10 (forall (@list @t17) (= (_ @t18 tptp.paraco367965286_Truth) @t1))) % 0.46/0.92 (assume @p11 (forall @t27 (and (=> @t25 (= @t22 @t1)) (=> @t26 (= @t22 @t19))))) % 0.46/0.92 (assume @p12 (forall @t27 (= @t22 (_ tptp.paraco1344940915le_Det @t25)))) % 0.46/0.92 (assume @p13 (forall @t27 (and (=> @t25 @t32) (=> @t26 (and (=> @t33 (= @t29 @t23)) (=> @t34 (and (=> @t30 @t32) (=> @t31 (= @t29 @t19))))))))) % 0.46/0.92 (assume @p14 (forall (@list @t35 @t36 @t10) (= (_ @t37 @t11) (_ @t35 @t10)))) % 0.46/0.92 (assume @p15 (forall @t41 (and (=> @t39 (= @t38 @t1)) (=> @t40 (and (=> @t33 (= @t38 @t19)) (=> @t34 (= @t38 @t24))))))) % 0.46/0.92 (assume @p16 (_ (_ tptp.inj_on_nat_nat tptp.f) tptp.top_top_set_nat)) % 0.46/0.92 (assume @p17 (forall (@list @t43 @t42) (= (= @t44 (_ tptp.paraco445776468le_Neg @t42)) (= @t43 @t42)))) % 0.46/0.92 (assume @p18 (forall (@list @t48 @t46 @t47 @t45) (= (= @t49 (_ (_ tptp.paraco69239110le_Con @t47) @t45)) (and (= @t48 @t47) (= @t46 @t45))))) % 0.46/0.92 (assume @p19 (forall (@list @t53 @t51 @t52 @t50) (= (= @t54 (_ (_ tptp.paraco1745535428le_Eql @t52) @t50)) (and (= @t53 @t52) (= @t51 @t50))))) % 0.46/0.92 (assume @p20 (forall (@list @t58 @t56 @t57 @t55) (= (= @t59 (_ (_ tptp.paraco1389086619le_Eql @t57) @t55)) (and (= @t58 @t57) (= @t56 @t55))))) % 0.46/0.92 (assume @p21 (forall (@list @t58 @t56 @t53 @t51) (not (= @t59 @t54)))) % 0.46/0.92 (assume @p22 (forall (@list @t48 @t46 @t53 @t51) (not (= @t49 @t54)))) % 0.46/0.92 (assume @p23 (forall (@list @t48 @t46 @t58 @t56) (not (= @t49 @t59)))) % 0.46/0.92 (assume @p24 (forall (@list @t43 @t53 @t51) (not (= @t44 @t54)))) % 0.46/0.92 (assume @p25 (forall (@list @t43 @t58 @t56) (not (= @t44 @t59)))) % 0.46/0.92 (assume @p26 (forall (@list @t43 @t48 @t46) (not (= @t44 @t49)))) % 0.46/0.92 (assume @p27 (forall (@list @t53 @t51) (not (= tptp.paraco367965286_Truth @t54)))) % 0.46/0.92 (assume @p28 (forall (@list @t58 @t56) (not (= tptp.paraco367965286_Truth @t59)))) % 0.46/0.92 (assume @p29 (forall (@list @t48 @t46) (not (= tptp.paraco367965286_Truth @t49)))) % 0.46/0.92 (assume @p30 (forall (@list @t43) (not (= tptp.paraco367965286_Truth @t44)))) % 0.46/0.92 (assume @p31 (forall (@list @t21 @t20) (= (_ tptp.paraco327635598_valid @t28) (and @t60 (_ tptp.paraco327635598_valid @t20))))) % 0.46/0.92 (assume @p32 (forall @t27 (and (=> @t25 (= @t61 @t1)) (=> @t26 (and (=> @t33 (= @t61 @t23)) (=> @t34 (and (=> @t30 (= @t61 @t24)) (=> @t31 (and (=> @t39 (= @t61 (_ @t18 (_ tptp.paraco445776468le_Neg @t20)))) (=> @t40 (and (=> @t62 (= @t61 @t38)) (=> (not @t62) (= @t61 @t19))))))))))))) % 0.46/0.92 (assume @p33 (= tptp.paraco1325918602e_eval (lambda (@list @t64 @t63) (_ @t65 (_ tptp.paraco445776468le_Neg (_ tptp.paraco445776468le_Neg @t63)))))) % 0.46/0.92 (assume @p34 (forall (@list @t66) (_ (_ tptp.member1234290208at_nat @t66) tptp.top_to730292591at_nat))) % 0.46/0.92 (assume @p35 (forall (@list @t67) (_ (_ tptp.member74361182lle_tv @t67) tptp.top_to378694061lle_tv))) % 0.46/0.92 (assume @p36 (forall @t69 (_ (_ tptp.member1474794996lle_fm @t68) tptp.top_to775056195lle_fm))) % 0.46/0.92 (assume @p37 (forall @t71 (_ (_ tptp.member1569366824lle_tv @t70) tptp.top_to449985143lle_tv))) % 0.46/0.92 (assume @p38 (forall (@list @t72) (_ @t73 tptp.top_to975729152tv_nat))) % 0.46/0.92 (assume @p39 (forall (@list @t74) (_ @t75 tptp.top_to1411004326lle_tv))) % 0.46/0.92 (assume @p40 (forall (@list @t76) (_ @t77 tptp.top_to1555900337at_nat))) % 0.46/0.92 (assume @p41 (forall (@list @t78) (_ @t79 tptp.top_top_set_nat))) % 0.46/0.92 (assume @p42 (forall @t82 (_ @t81 tptp.top_to1057771083lle_tv))) % 0.46/0.92 (assume @p43 (forall @t90 (=> @t89 (=> @t87 @t85)))) % 0.46/0.92 (assume @p44 (forall @t97 (=> @t96 (=> @t94 @t92)))) % 0.46/0.92 (assume @p45 (forall @t104 (=> @t103 (=> @t101 @t99)))) % 0.46/0.92 (assume @p46 (forall @t111 (=> @t110 (=> @t108 @t106)))) % 0.46/0.92 (assume @p47 (forall @t118 (=> @t117 (=> @t115 @t113)))) % 0.46/0.92 (assume @p48 (forall @t123 (=> @t122 (=> @t120 @t92)))) % 0.46/0.92 (assume @p49 (forall @t132 (=> @t131 (=> @t129 @t125)))) % 0.46/0.92 (assume @p50 (forall @t138 (=> (forall @t137 @t136) @t89))) % 0.46/0.92 (assume @p51 (forall @t145 (=> (forall @t144 @t143) @t96))) % 0.46/0.92 (assume @p52 (forall @t151 (=> (forall @t150 @t149) @t103))) % 0.46/0.92 (assume @p53 (forall @t157 (=> (forall @t156 @t155) @t110))) % 0.46/0.92 (assume @p54 (forall @t163 (=> (forall @t162 @t161) @t117))) % 0.46/0.92 (assume @p55 (forall @t166 (=> (forall @t144 @t165) @t122))) % 0.46/0.92 (assume @p56 (forall @t172 (=> (forall @t171 @t170) @t131))) % 0.46/0.92 (assume @p57 (forall @t90 (=> @t89 @t173))) % 0.46/0.92 (assume @p58 (forall @t97 (=> @t96 @t174))) % 0.46/0.92 (assume @p59 (forall @t104 (=> @t103 @t175))) % 0.46/0.92 (assume @p60 (forall @t111 (=> @t110 @t176))) % 0.46/0.92 (assume @p61 (forall @t118 (=> @t117 @t177))) % 0.46/0.92 (assume @p62 (forall @t123 (=> @t122 @t178))) % 0.46/0.92 (assume @p63 (forall @t132 (=> @t131 @t179))) % 0.46/0.92 (assume @p64 (forall @t138 (= @t89 (forall (@list @t181 @t180) (=> (= (_ @t86 @t181) (_ @t86 @t180)) @t182))))) % 0.46/0.92 (assume @p65 (forall @t145 (= @t96 (forall @t187 (=> (= @t186 (_ @t93 @t183)) @t185))))) % 0.46/0.92 (assume @p66 (forall @t151 (= @t103 (forall (@list @t189 @t188) (=> (= (_ @t100 @t189) (_ @t100 @t188)) @t190))))) % 0.46/0.92 (assume @p67 (forall @t157 (= @t110 (forall (@list @t192 @t191) (=> (= (_ @t107 @t192) (_ @t107 @t191)) @t193))))) % 0.46/0.92 (assume @p68 (forall @t163 (= @t117 (forall (@list @t195 @t194) (=> (= (_ @t114 @t195) (_ @t114 @t194)) @t196))))) % 0.46/0.92 (assume @p69 (forall @t166 (= @t122 (forall @t187 (=> (= @t198 @t197) @t185))))) % 0.46/0.92 (assume @p70 (forall @t172 (= @t131 (forall (@list @t200 @t199) (=> (= @t203 @t202) @t201))))) % 0.46/0.92 (assume @p71 (forall (@list @t205 @t204) (=> (forall (@list @t213) (_ @t205 (_ tptp.paraco1480028776le_Pro @t213))) (=> @t212 (=> (forall (@list @t211) (=> (_ @t205 @t211) (_ @t205 (_ tptp.paraco445776468le_Neg @t211)))) (=> (forall @t210 (=> @t209 (=> @t208 (_ @t205 (_ (_ tptp.paraco69239110le_Con @t207) @t206))))) (=> (forall @t210 (=> @t209 (=> @t208 (_ @t205 (_ (_ tptp.paraco1389086619le_Eql @t207) @t206))))) (=> (forall @t210 (=> @t209 (=> @t208 (_ @t205 (_ (_ tptp.paraco1745535428le_Eql @t207) @t206))))) (_ @t205 @t204))))))))) % 0.46/0.92 (assume @p72 (forall (@list @t216) (=> (forall (@list @t222) (not (= @t216 (_ tptp.paraco1480028776le_Pro @t222)))) (=> (not (= @t216 tptp.paraco367965286_Truth)) (=> (forall (@list @t221) (not (= @t216 (_ tptp.paraco445776468le_Neg @t221)))) (=> (forall (@list @t220 @t219) (not (= @t216 (_ (_ tptp.paraco69239110le_Con @t220) @t219)))) (=> (forall (@list @t218 @t217) (not (= @t216 (_ (_ tptp.paraco1389086619le_Eql @t218) @t217)))) (not (forall (@list @t215 @t214) (not (= @t216 (_ (_ tptp.paraco1745535428le_Eql @t215) @t214)))))))))))) % 0.46/0.92 (assume @p73 (forall (@list @t223 @t224) (= (_ (_ tptp.member1234290208at_nat @t223) (_ tptp.collec1288997470at_nat @t224)) (_ @t224 @t223)))) % 0.46/0.92 (assume @p74 (forall (@list @t225 @t226) (= (_ (_ tptp.member74361182lle_tv @t225) (_ tptp.collec1582599068lle_tv @t226)) (_ @t226 @t225)))) % 0.46/0.92 (assume @p75 (forall (@list @t227 @t228) (= (_ (_ tptp.member1474794996lle_fm @t227) (_ tptp.collec835549234lle_fm @t228)) (_ @t228 @t227)))) % 0.46/0.92 (assume @p76 (forall (@list @t229 @t230) (= (_ (_ tptp.member1569366824lle_tv @t229) (_ tptp.collec1624074086lle_tv @t230)) (_ @t230 @t229)))) % 0.46/0.92 (assume @p77 (forall (@list @t231 @t232) (= (_ @t234 @t233) (_ @t232 @t231)))) % 0.46/0.92 (assume @p78 (forall (@list @t235 @t236) (= (_ @t238 @t237) (_ @t236 @t235)))) % 0.46/0.92 (assume @p79 (forall @t241 (= (_ tptp.collec1288997470at_nat (lambda (@list @t240) (_ (_ tptp.member1234290208at_nat @t240) @t239))) @t239))) % 0.46/0.92 (assume @p80 (forall @t244 (= (_ tptp.collec1582599068lle_tv (lambda (@list @t243) (_ (_ tptp.member74361182lle_tv @t243) @t242))) @t242))) % 0.46/0.92 (assume @p81 (forall @t247 (= (_ tptp.collec835549234lle_fm (lambda (@list @t246) (_ (_ tptp.member1474794996lle_fm @t246) @t245))) @t245))) % 0.46/0.92 (assume @p82 (forall @t250 (= (_ tptp.collec1624074086lle_tv (lambda (@list @t249) (_ (_ tptp.member1569366824lle_tv @t249) @t248))) @t248))) % 0.46/0.92 (assume @p83 (forall @t254 (= (_ tptp.collec1111687558lle_tv (lambda @t253 (_ @t252 @t251))) @t251))) % 0.46/0.92 (assume @p84 (forall @t258 (= (_ tptp.collect_nat (lambda @t257 (_ @t256 @t255))) @t255))) % 0.46/0.92 (assume @p85 (forall (@list @t232 @t259) (=> (forall @t260 (= (_ @t232 @t168) (_ @t259 @t168))) (= @t233 (_ tptp.collec1111687558lle_tv @t259))))) % 0.46/0.92 (assume @p86 (forall (@list @t236 @t261) (=> (forall @t262 (= (_ @t236 @t140) (_ @t261 @t140))) (= @t237 (_ tptp.collect_nat @t261))))) % 0.46/0.92 (assume @p87 (forall (@list @t266) (=> (not (= @t266 tptp.paraco367965286_Truth)) (=> (forall @t274 (not (= @t266 @t273))) (=> (forall @t271 (not (= @t266 @t270))) (=> (forall @t267 (not (= @t266 @t269))) (=> (forall @t267 (not (= @t266 @t268))) (not (forall @t267 (not (= @t266 @t265))))))))))) % 0.46/0.92 (assume @p88 (forall (@list @t276 @t275) (= (= @t277 (_ tptp.paraco1480028776le_Pro @t275)) (= @t276 @t275)))) % 0.46/0.92 (assume @p89 (= tptp.top_to975729152tv_nat (_ tptp.collec848462447tv_nat tptp.top_to900819589_nat_o))) % 0.46/0.92 (assume @p90 (= tptp.top_to1411004326lle_tv (_ tptp.collec924990229lle_tv tptp.top_to1889334367e_tv_o))) % 0.46/0.92 (assume @p91 (= tptp.top_to1555900337at_nat (_ tptp.collec7649004at_nat tptp.top_to632227436_nat_o))) % 0.46/0.92 (assume @p92 (= tptp.top_top_set_nat (_ tptp.collect_nat tptp.top_top_nat_o))) % 0.46/0.92 (assume @p93 (= tptp.top_to1057771083lle_tv (_ tptp.collec1111687558lle_tv tptp.top_to1299250770e_tv_o))) % 0.46/0.92 (assume @p94 (forall (@list @t17 @t278) (= (_ @t18 (_ tptp.paraco1480028776le_Pro @t278)) (_ @t17 @t278)))) % 0.46/0.92 (assume @p95 (forall (@list @t276 @t43) (not (= @t277 @t44)))) % 0.46/0.92 (assume @p96 (forall (@list @t276 @t48 @t46) (not (= @t277 @t49)))) % 0.46/0.92 (assume @p97 (forall (@list @t276 @t53 @t51) (not (= @t277 @t54)))) % 0.46/0.92 (assume @p98 (forall (@list @t276 @t58 @t56) (not (= @t277 @t59)))) % 0.46/0.92 (assume @p99 (forall (@list @t276) (not (= @t277 tptp.paraco367965286_Truth)))) % 0.46/0.92 (assume @p100 (forall @t166 (=> @t122 (_ (_ tptp.inj_on772319074lle_tv @t16) tptp.top_to1057771083lle_tv)))) % 0.46/0.92 (assume @p101 (exists @t281 (_ @t280 tptp.top_to730292591at_nat))) % 0.46/0.92 (assume @p102 (exists @t284 (_ @t283 tptp.top_to378694061lle_tv))) % 0.46/0.92 (assume @p103 (exists @t287 (_ @t286 tptp.top_to775056195lle_fm))) % 0.46/0.92 (assume @p104 (exists @t290 (_ @t289 tptp.top_to449985143lle_tv))) % 0.46/0.92 (assume @p105 (exists @t292 (_ @t291 tptp.top_to975729152tv_nat))) % 0.46/0.92 (assume @p106 (exists @t294 (_ @t293 tptp.top_to1411004326lle_tv))) % 0.46/0.92 (assume @p107 (exists @t296 (_ @t295 tptp.top_to1555900337at_nat))) % 0.46/0.92 (assume @p108 (exists @t262 (_ @t297 tptp.top_top_set_nat))) % 0.46/0.92 (assume @p109 (exists @t260 (_ @t298 tptp.top_to1057771083lle_tv))) % 0.46/0.92 (assume @p110 (forall @t241 (=> (forall @t281 (_ @t280 @t239)) (= tptp.top_to730292591at_nat @t239)))) % 0.46/0.92 (assume @p111 (forall @t244 (=> (forall @t284 (_ @t283 @t242)) (= tptp.top_to378694061lle_tv @t242)))) % 0.46/0.92 (assume @p112 (forall @t247 (=> (forall @t287 (_ @t286 @t245)) (= tptp.top_to775056195lle_fm @t245)))) % 0.46/0.92 (assume @p113 (forall @t250 (=> (forall @t290 (_ @t289 @t248)) (= tptp.top_to449985143lle_tv @t248)))) % 0.46/0.92 (assume @p114 (forall (@list @t299) (=> (forall @t292 @t300) (= tptp.top_to975729152tv_nat @t299)))) % 0.46/0.92 (assume @p115 (forall (@list @t301) (=> (forall @t294 @t302) (= tptp.top_to1411004326lle_tv @t301)))) % 0.46/0.92 (assume @p116 (forall (@list @t303) (=> (forall @t296 @t304) (= tptp.top_to1555900337at_nat @t303)))) % 0.46/0.92 (assume @p117 (forall @t258 (=> (forall @t262 @t305) (= tptp.top_top_set_nat @t255)))) % 0.46/0.92 (assume @p118 (forall @t254 (=> (forall @t260 @t306) (= tptp.top_to1057771083lle_tv @t251)))) % 0.46/0.92 (assume @p119 (forall (@list @t307 @t309 @t86) (=> (forall (@list @t134) (=> @t310 (= (_ @t309 @t135) @t134))) @t308))) % 0.46/0.92 (assume @p120 (forall (@list @t299 @t312 @t100) (=> (forall @t292 (=> @t300 (= (_ @t312 @t148) @t147))) @t311))) % 0.46/0.92 (assume @p121 (forall (@list @t301 @t314 @t107) (=> (forall @t294 (=> @t302 (= (_ @t314 @t154) @t153))) @t313))) % 0.46/0.92 (assume @p122 (forall (@list @t303 @t316 @t114) (=> (forall @t296 (=> @t304 (= (_ @t316 @t160) @t159))) @t315))) % 0.46/0.92 (assume @p123 (forall (@list @t255 @t318 @t93) (=> (forall @t262 (=> @t305 @t319)) @t317))) % 0.46/0.92 (assume @p124 (forall @t324 (=> (forall @t262 (=> @t305 @t323)) @t320))) % 0.46/0.92 (assume @p125 (forall @t329 (=> (forall @t260 (=> @t306 @t328)) @t325))) % 0.46/0.92 (assume @p126 (forall @t332 (=> @t308 (=> (not @t85) (=> @t331 (=> @t330 (not @t87))))))) % 0.46/0.92 (assume @p127 (forall @t335 (=> @t311 (=> (not @t99) (=> @t334 (=> @t333 (not @t101))))))) % 0.46/0.92 (assume @p128 (forall @t338 (=> @t313 (=> (not @t106) (=> @t337 (=> @t336 (not @t108))))))) % 0.46/0.92 (assume @p129 (forall @t341 (=> @t315 (=> (not @t113) (=> @t340 (=> @t339 (not @t115))))))) % 0.46/0.92 (assume @p130 (forall @t346 (=> @t317 (=> @t345 (=> @t344 (=> @t343 (not @t94))))))) % 0.46/0.92 (assume @p131 (forall @t347 (=> @t320 (=> @t345 (=> @t344 (=> @t343 (not @t120))))))) % 0.46/0.92 (assume @p132 (forall @t351 (=> @t325 (=> (not @t125) (=> @t350 (=> @t349 (not @t129))))))) % 0.46/0.92 (assume @p133 (forall @t332 (=> @t308 (=> @t331 (=> @t330 @t173))))) % 0.46/0.92 (assume @p134 (forall @t335 (=> @t311 (=> @t334 (=> @t333 @t175))))) % 0.46/0.92 (assume @p135 (forall @t338 (=> @t313 (=> @t337 (=> @t336 @t176))))) % 0.46/0.92 (assume @p136 (forall @t341 (=> @t315 (=> @t340 (=> @t339 @t177))))) % 0.46/0.92 (assume @p137 (forall @t346 (=> @t317 (=> @t344 (=> @t343 @t174))))) % 0.46/0.92 (assume @p138 (forall @t347 (=> @t320 (=> @t344 (=> @t343 @t178))))) % 0.46/0.92 (assume @p139 (forall @t351 (=> @t325 (=> @t350 (=> @t349 @t179))))) % 0.46/0.92 (assume @p140 (forall (@list @t307 @t86 @t309) (=> (forall (@list @t352) (=> (_ (_ tptp.member1531318361lle_tv @t352) @t307) (= (_ @t86 @t352) (_ @t309 @t352)))) (= @t308 (_ (_ tptp.inj_on2112487900lle_tv @t309) @t307))))) % 0.46/0.92 (assume @p141 (forall (@list @t299 @t100 @t312) (=> (forall (@list @t353) (=> (_ (_ tptp.member737151281tv_nat @t353) @t299) (= (_ @t100 @t353) (_ @t312 @t353)))) (= @t311 (_ (_ tptp.inj_on552895452tv_nat @t312) @t299))))) % 0.46/0.92 (assume @p142 (forall (@list @t301 @t107 @t314) (=> (forall (@list @t354) (=> (_ (_ tptp.member813679063lle_tv @t354) @t301) (= (_ @t107 @t354) (_ @t314 @t354)))) (= @t313 (_ (_ tptp.inj_on1745913142lle_tv @t314) @t301))))) % 0.46/0.92 (assume @p143 (forall (@list @t303 @t114 @t316) (=> (forall (@list @t355) (=> (_ (_ tptp.member701585322at_nat @t355) @t303) (= (_ @t114 @t355) (_ @t316 @t355)))) (= @t315 (_ (_ tptp.inj_on26176689at_nat @t316) @t303))))) % 0.46/0.92 (assume @p144 (forall (@list @t255 @t93 @t356) (=> (forall @t359 (=> @t358 (= (_ @t93 @t357) (_ @t356 @t357)))) (= @t317 (_ (_ tptp.inj_on1955349912lle_tv @t356) @t255))))) % 0.46/0.92 (assume @p145 (forall (@list @t255 @t15 @t321) (=> (forall @t359 (=> @t358 (= (_ @t15 @t357) (_ @t321 @t357)))) (= @t320 @t361)))) % 0.46/0.92 (assume @p146 (forall (@list @t251 @t126 @t326) (=> (forall (@list @t364) (=> (_ (_ tptp.member266900804lle_tv @t364) @t251) (= (_ @t126 @t364) (_ @t326 @t364)))) (= @t325 @t363)))) % 0.46/0.92 (assume @p147 (forall (@list @t307 @t86) (=> (forall @t137 (=> @t310 (=> (_ (_ tptp.member1531318361lle_tv @t133) @t307) @t136))) @t308))) % 0.46/0.92 (assume @p148 (forall (@list @t299 @t100) (=> (forall @t150 (=> @t300 (=> (_ (_ tptp.member737151281tv_nat @t146) @t299) @t149))) @t311))) % 0.46/0.92 (assume @p149 (forall (@list @t301 @t107) (=> (forall @t156 (=> @t302 (=> (_ (_ tptp.member813679063lle_tv @t152) @t301) @t155))) @t313))) % 0.46/0.92 (assume @p150 (forall (@list @t303 @t114) (=> (forall @t162 (=> @t304 (=> (_ (_ tptp.member701585322at_nat @t158) @t303) @t161))) @t315))) % 0.46/0.92 (assume @p151 (forall (@list @t255 @t93) (=> (forall @t144 (=> @t305 (=> @t365 @t143))) @t317))) % 0.46/0.92 (assume @p152 (forall (@list @t255 @t15) (=> (forall @t144 (=> @t305 (=> @t365 @t165))) @t320))) % 0.46/0.92 (assume @p153 (forall (@list @t251 @t126) (=> (forall @t171 (=> @t306 (=> (_ (_ tptp.member266900804lle_tv @t167) @t251) @t170))) @t325))) % 0.46/0.92 (assume @p154 (forall @t332 (=> @t308 (=> @t87 (=> @t331 (=> @t330 @t85)))))) % 0.46/0.92 (assume @p155 (forall @t335 (=> @t311 (=> @t101 (=> @t334 (=> @t333 @t99)))))) % 0.46/0.92 (assume @p156 (forall @t338 (=> @t313 (=> @t108 (=> @t337 (=> @t336 @t106)))))) % 0.46/0.92 (assume @p157 (forall @t341 (=> @t315 (=> @t115 (=> @t340 (=> @t339 @t113)))))) % 0.46/0.92 (assume @p158 (forall @t346 (=> @t317 (=> @t94 @t366)))) % 0.46/0.92 (assume @p159 (forall @t347 (=> @t320 (=> @t120 @t366)))) % 0.46/0.92 (assume @p160 (forall @t351 (=> @t325 (=> @t129 (=> @t350 (=> @t349 @t125)))))) % 0.46/0.92 (assume @p161 (forall (@list @t205 @t367) (=> @t212 (=> (forall @t274 (_ @t205 @t273)) (=> (forall @t271 (=> @t369 (_ @t205 @t270))) (=> (forall @t267 (=> @t369 (=> @t368 (_ @t205 @t269)))) (=> (forall @t267 (=> @t369 (=> @t368 (_ @t205 @t268)))) (=> (forall @t267 (=> @t369 (=> @t368 (_ @t205 @t265)))) (_ @t205 @t367))))))))) % 0.46/0.92 (assume @p162 (forall @t69 (=> (forall (@list @t370 @t272) (not (= @t68 (_ @t371 @t273)))) (=> (forall (@list @t370) (not (= @t68 (_ @t371 tptp.paraco367965286_Truth)))) (=> (forall (@list @t370 @t264) (not (= @t68 (_ @t371 @t270)))) (=> (forall @t372 (not (= @t68 (_ @t371 @t269)))) (=> (forall @t372 (not (= @t68 (_ @t371 @t268)))) (not (forall @t372 (not (= @t68 (_ @t371 @t265)))))))))))) % 0.46/0.92 (assume @p163 (= tptp.top_top_nat_o (lambda @t257 (_ @t256 tptp.top_top_set_nat)))) % 0.46/0.92 (assume @p164 (= tptp.top_to1299250770e_tv_o (lambda @t253 (_ @t252 tptp.top_to1057771083lle_tv)))) % 0.46/0.92 (assume @p165 (forall @t386 (=> @t385 (=> (forall @t384 (=> @t383 (not @t382))) (not (forall @t379 (=> @t378 (not @t375)))))))) % 0.46/0.92 (assume @p166 (forall (@list @t21 @t387) (=> @t60 @t389))) % 0.46/0.92 (assume @p167 (forall (@list @t387 @t21) (=> (not @t389) (not @t60)))) % 0.46/0.92 (assume @p168 (forall (@list @t15 @t78) (=> @t122 (= (_ (_ (_ tptp.the_inv_into_nat_nat tptp.top_top_set_nat) @t15) @t119) @t78)))) % 0.46/0.92 (assume @p169 (forall (@list @t126 @t80) (=> @t131 (= (_ (_ (_ tptp.the_in452116896lle_tv tptp.top_to1057771083lle_tv) @t126) @t128) @t80)))) % 0.46/0.92 (assume @p170 (forall (@list @t387 @t21 @t20) (= (_ @t388 @t28) (and @t389 (_ @t388 @t20))))) % 0.46/0.92 (assume @p171 (forall (@list @t391 @t390) (= (= @t392 (_ tptp.paraco793048302_Indet @t390)) (= @t391 @t390)))) % 0.46/0.92 (assume @p172 (forall (@list @t232 @t393) (=> (_ @t232 @t1) (=> (_ @t232 @t19) (=> (forall @t379 (_ @t232 @t376)) (_ @t232 @t393)))))) % 0.46/0.92 (assume @p173 (forall (@list @t396 @t395 @t394) (=> (forall @t400 (_ @t398 @t381)) (=> (forall @t399 (_ @t398 @t376)) (_ (_ @t396 @t395) @t394))))) % 0.46/0.92 (assume @p174 (forall @t82 (=> (not (= @t80 @t1)) (=> (not (= @t80 @t19)) (not (forall @t379 (not (= @t80 @t376)))))))) % 0.46/0.92 (assume @p175 (forall (@list @t124) (=> (forall (@list @t402) (not (= @t124 (_ tptp.paraco1344940915le_Det @t402)))) (not (forall (@list @t401) (not (= @t124 (_ tptp.paraco793048302_Indet @t401)))))))) % 0.46/0.92 (assume @p176 (forall (@list @t232 @t403) (=> (forall (@list @t404) (_ @t232 (_ tptp.paraco1344940915le_Det @t404))) (=> (forall @t262 (_ @t232 (_ tptp.paraco793048302_Indet @t140))) (_ @t232 @t403))))) % 0.46/0.92 (assume @p177 (forall (@list @t10 @t391) (not (= @t11 @t392)))) % 0.46/0.92 (assume @p178 (forall (@list @t15 @t255 @t78) (=> @t320 (=> @t344 (= (_ @t405 @t119) @t78))))) % 0.46/0.92 (assume @p179 (forall (@list @t126 @t251 @t80) (=> @t325 (=> @t350 (= (_ @t406 @t128) @t80))))) % 0.46/0.92 (assume @p180 (forall @t347 (=> @t320 (=> (= @t119 @t91) (=> @t344 (= @t407 @t78)))))) % 0.46/0.92 (assume @p181 (forall @t351 (=> @t325 (=> (= @t128 @t124) (=> @t350 (= @t408 @t80)))))) % 0.46/0.92 (assume @p182 (forall (@list @t35 @t36 @t391) (= (_ @t37 @t392) (_ @t36 @t391)))) % 0.46/0.92 (assume @p183 (forall (@list @t15 @t409) (= (_ @t16 (_ tptp.paraco793048302_Indet @t409)) (_ tptp.paraco793048302_Indet (_ @t15 @t409))))) % 0.46/0.92 (assume @p184 (forall (@list @t413 @t411 @t412 @t410) (= (= @t414 (_ (_ tptp.produc1710735575lle_fm @t412) @t410)) (and (= @t413 @t412) (= @t411 @t410))))) % 0.46/0.92 (assume @p185 (forall (@list @t418 @t416 @t417 @t415) (= (= @t419 (_ (_ tptp.produc1680557635lle_tv @t417) @t415)) (and (= @t418 @t417) (= @t416 @t415))))) % 0.46/0.92 (assume @p186 (forall @t428 (= @t427 (and @t425 @t422)))) % 0.46/0.92 (assume @p187 (forall @t437 (= @t436 (and @t434 @t431)))) % 0.46/0.92 (assume @p188 (forall @t41 (= @t38 (_ (_ (_ tptp.paraco2051596139lle_tv (_ (_ tptp.produc234482697lle_tv @t19) @t1)) tptp.paraco793048302_Indet) @t24)))) % 0.46/0.92 (assume @p189 (forall (@list @t441) (exists @t442 (= @t441 @t440)))) % 0.46/0.92 (assume @p190 (forall (@list @t445) (exists @t446 (= @t445 @t444)))) % 0.46/0.92 (assume @p191 (forall @t456 (= @t455 (not (or (and @t449 (not @t452)) (and @t450 (not @t448))))))) % 0.46/0.92 (assume @p192 (forall (@list @t457 @t451 @t447 @t449) (= (_ @t457 @t454) (_ (_ (_ tptp.produc234482697lle_tv (_ @t457 @t451)) (_ @t457 @t447)) @t449)))) % 0.46/0.92 (assume @p193 (forall @t456 (= @t455 (and (=> @t449 @t452) (=> @t450 @t448))))) % 0.46/0.92 (assume @p194 (forall @t458 (= (_ @t453 true) @t451))) % 0.46/0.92 (assume @p195 (forall @t458 (= (_ @t453 false) @t447))) % 0.46/0.92 (assume @p196 (forall @t71 (=> (forall @t400 (not (= @t70 (_ @t459 @t381)))) (not (forall @t399 (not (= @t70 (_ @t459 @t376)))))))) % 0.46/0.92 (assume @p197 (forall (@list @t228 @t460) (=> @t465 (_ @t228 @t460)))) % 0.46/0.92 (assume @p198 (forall (@list @t230 @t466) (=> @t471 (_ @t230 @t466)))) % 0.46/0.92 (assume @p199 (forall (@list @t472) (not (forall @t464 (not (= @t472 @t463)))))) % 0.46/0.92 (assume @p200 (forall (@list @t473) (not (forall @t470 (not (= @t473 @t469)))))) % 0.46/0.92 (assume @p201 (forall @t428 (=> @t427 (not (=> @t425 (not @t422)))))) % 0.46/0.92 (assume @p202 (forall @t437 (=> @t436 (not (=> @t434 (not @t431)))))) % 0.46/0.92 (assume @p203 (forall (@list @t228 @t441) (=> @t465 (_ @t228 @t441)))) % 0.46/0.92 (assume @p204 (forall (@list @t230 @t445) (=> @t471 (_ @t230 @t445)))) % 0.46/0.92 (assume @p205 (forall (@list @t476 @t478 @t474 @t475) (=> (_ (_ tptp.member1474794996lle_fm (_ @t477 @t478)) @t474) (=> (= @t475 @t478) (_ (_ tptp.member1474794996lle_fm (_ @t477 @t475)) @t474))))) % 0.46/0.92 (assume @p206 (forall (@list @t481 @t483 @t479 @t480) (=> (_ (_ tptp.member1569366824lle_tv (_ @t482 @t483)) @t479) (=> (= @t480 @t483) (_ (_ tptp.member1569366824lle_tv (_ @t482 @t480)) @t479))))) % 0.46/0.92 (assume @p207 (forall (@list @t485 @t484 @t216) (= (_ (_ tptp.produc1942165868lle_fm @t485) @t487) (_ (_ tptp.produc1710735575lle_fm (_ @t485 @t484)) @t216)))) % 0.46/0.92 (assume @p208 (forall (@list @t488 @t374 @t124) (= (_ (_ tptp.produc939316703lle_tv @t488) @t490) (_ (_ tptp.produc1680557635lle_tv (_ @t488 @t374)) @t124)))) % 0.46/0.92 (assume @p209 (forall (@list @t491 @t484 @t216) (= (_ (_ tptp.produc1807466521lle_tv @t491) @t487) (_ @t486 (_ @t491 @t216))))) % 0.46/0.92 (assume @p210 (forall (@list @t126 @t374 @t124) (= (_ (_ tptp.produc109093078at_nat @t126) @t490) (_ @t489 @t127)))) % 0.46/0.92 (assume @p211 (forall @t386 (=> @t385 (=> (_ @t492 (_ @t489 @t377)) (=> (forall @t384 (=> @t383 (=> @t382 (not (_ @t492 (_ @t489 @t381)))))) (not (forall @t379 (=> @t378 (=> @t375 (not (_ @t492 (_ @t489 @t376)))))))))))) % 0.46/0.92 (assume @p212 (forall (@list @t494 @t493) (=> @t496 (=> @t495 (_ (_ tptp.inj_on26176689at_nat (_ (_ tptp.produc505105722at_nat @t494) @t493)) tptp.top_to1555900337at_nat))))) % 0.46/0.92 (assume @p213 (forall (@list @t494 @t497) (=> @t496 (=> @t498 (_ (_ tptp.inj_on1745913142lle_tv (_ (_ tptp.produc2101297531lle_tv @t494) @t497)) tptp.top_to1411004326lle_tv))))) % 0.46/0.92 (assume @p214 (forall (@list @t499 @t493) (=> @t500 (=> @t495 (_ (_ tptp.inj_on552895452tv_nat (_ (_ tptp.produc42536895at_nat @t499) @t493)) tptp.top_to975729152tv_nat))))) % 0.46/0.92 (assume @p215 (forall (@list @t499 @t497) (=> @t500 (=> @t498 (_ (_ tptp.inj_on2112487900lle_tv (_ (_ tptp.produc1345917071lle_tv @t499) @t497)) tptp.top_to1871154984lle_tv))))) % 0.46/0.92 (assume @p216 (forall @t504 (=> @t503 @t502))) % 0.46/0.92 (assume @p217 (forall @t508 (=> @t507 @t506))) % 0.46/0.92 (assume @p218 (forall (@list @t485 @t509 @t424 @t421) (= (_ @t511 @t426) @t510))) % 0.46/0.92 (assume @p219 (forall (@list @t513 @t512 @t424 @t421) (= (_ @t515 @t426) @t514))) % 0.46/0.92 (assume @p220 (forall (@list @t517 @t516 @t433 @t430) (= (_ @t519 @t435) @t518))) % 0.46/0.92 (assume @p221 (forall (@list @t488 @t326 @t433 @t430) (= (_ @t521 @t435) @t520))) % 0.46/0.92 (assume @p222 (forall @t504 (=> @t502 @t503))) % 0.46/0.92 (assume @p223 (forall @t508 (=> @t506 @t507))) % 0.46/0.92 (assume @p224 (forall @t524 (=> @t320 (= (_ (_ tptp.image_nat_nat @t405) @t523) @t255)))) % 0.46/0.92 (assume @p225 (forall @t527 (=> @t325 (= (_ (_ tptp.image_335818702lle_tv @t406) @t526) @t251)))) % 0.46/0.92 (assume @p226 (forall (@list @t424 @t421 @t474 @t485 @t509) (=> @t529 (_ (_ tptp.member1474794996lle_fm @t510) @t528)))) % 0.46/0.92 (assume @p227 (forall (@list @t424 @t421 @t474 @t513 @t512) (=> @t529 (_ (_ tptp.member1569366824lle_tv @t514) @t530)))) % 0.46/0.92 (assume @p228 (forall (@list @t433 @t430 @t479 @t517 @t516) (=> @t532 (_ (_ tptp.member1474794996lle_fm @t518) @t531)))) % 0.46/0.92 (assume @p229 (forall (@list @t433 @t430 @t479 @t488 @t326) (=> @t532 (_ (_ tptp.member1569366824lle_tv @t520) @t533)))) % 0.46/0.92 (assume @p230 (forall (@list @t266 @t534) (= (_ tptp.produc1232814113lle_tv @t536) @t535))) % 0.46/0.92 (assume @p231 (forall (@list @t80 @t537) (= (_ tptp.produc178635363at_nat @t539) @t538))) % 0.46/0.92 (assume @p232 (forall (@list @t484 @t216) (= (_ tptp.produc1000205111lle_fm @t487) @t540))) % 0.46/0.92 (assume @p233 (forall (@list @t374 @t124) (= (_ tptp.produc225513635lle_tv @t490) @t541))) % 0.46/0.92 (assume @p234 (forall (@list @t216 @t484 @t245) (= (_ (_ tptp.member74361182lle_tv @t540) (_ (_ tptp.image_924970994lle_tv tptp.produc1000205111lle_fm) @t245)) (_ (_ tptp.member1474794996lle_fm @t487) @t245)))) % 0.46/0.92 (assume @p235 (forall (@list @t124 @t374 @t248) (= (_ (_ tptp.member1234290208at_nat @t541) (_ (_ tptp.image_1724396928at_nat tptp.produc225513635lle_tv) @t248)) (_ (_ tptp.member1569366824lle_tv @t490) @t248)))) % 0.46/0.92 (assume @p236 (forall (@list @t534 @t266 @t242) (= (_ (_ tptp.member1474794996lle_fm @t535) (_ (_ tptp.image_326034184lle_fm tptp.produc1232814113lle_tv) @t242)) (_ (_ tptp.member74361182lle_tv @t536) @t242)))) % 0.46/0.92 (assume @p237 (forall (@list @t537 @t80 @t239) (= (_ (_ tptp.member1569366824lle_tv @t538) (_ (_ tptp.image_769496456lle_tv tptp.produc178635363at_nat) @t239)) (_ (_ tptp.member1234290208at_nat @t539) @t239)))) % 0.46/0.92 (assume @p238 (forall @t324 (=> (forall @t262 (=> @t305 (forall (@list @t542) (=> (_ (_ tptp.member_nat @t542) @t255) (= (= @t322 (_ @t321 (_ @t15 @t542))) (= (_ @t321 @t140) (_ @t321 @t542))))))) (=> @t320 (= (_ @t360 @t523) @t361))))) % 0.46/0.92 (assume @p239 (forall @t329 (=> (forall @t260 (=> @t306 (forall (@list @t543) (=> (_ (_ tptp.member266900804lle_tv @t543) @t251) (= (= @t327 (_ @t326 (_ @t126 @t543))) (= (_ @t326 @t168) (_ @t326 @t543))))))) (=> @t325 (= (_ @t362 @t526) @t363))))) % 0.46/0.92 (assume @p240 (forall @t547 (=> @t546 (exists @t262 @t544)))) % 0.46/0.92 (assume @p241 (forall @t550 (=> @t549 (exists @t262 @t548)))) % 0.46/0.92 (assume @p242 (forall @t555 (=> @t554 (exists @t260 @t553)))) % 0.46/0.92 (assume @p243 (forall @t559 (=> @t558 (exists @t260 @t556)))) % 0.46/0.92 (assume @p244 (forall @t547 (=> @t546 (not (forall @t262 (not @t544)))))) % 0.46/0.92 (assume @p245 (forall @t550 (=> @t549 (not (forall @t262 (not @t548)))))) % 0.46/0.92 (assume @p246 (forall @t555 (=> @t554 (not (forall @t260 (not @t553)))))) % 0.46/0.92 (assume @p247 (forall @t559 (=> @t558 (not (forall @t260 (not @t556)))))) % 0.46/0.92 (assume @p248 (forall (@list @t321 @t15) (=> (forall @t262 @t323) @t560))) % 0.46/0.92 (assume @p249 (forall (@list @t356 @t551) (=> (forall @t260 (= (_ @t356 @t552) @t168)) @t561))) % 0.46/0.92 (assume @p250 (forall (@list @t318 @t93) (=> (forall @t262 @t319) @t562))) % 0.46/0.92 (assume @p251 (forall (@list @t326 @t126) (=> (forall @t260 @t328) @t563))) % 0.46/0.92 (assume @p252 (forall @t166 (= @t546 (forall @t564 (exists @t257 (= @t183 @t198)))))) % 0.46/0.92 (assume @p253 (forall @t145 (= @t549 (forall @t565 (exists @t257 (= @t199 @t186)))))) % 0.46/0.92 (assume @p254 (forall (@list @t551) (= @t554 (forall @t564 (exists @t253 (= @t183 (_ @t551 @t200))))))) % 0.46/0.92 (assume @p255 (forall @t172 (= @t558 (forall @t565 (exists @t253 (= @t199 @t203)))))) % 0.46/0.92 (assume @p256 (forall (@list @t15 @t321) (=> @t546 (=> @t560 (= (_ (_ tptp.image_815163717at_nat (_ (_ tptp.produc505105722at_nat @t15) @t321)) tptp.top_to1555900337at_nat) tptp.top_to1555900337at_nat))))) % 0.46/0.92 (assume @p257 (forall (@list @t15 @t356) (=> @t546 (=> @t561 (= (_ (_ tptp.image_1674248956lle_tv (_ (_ tptp.produc313957681lle_tv @t15) @t356)) tptp.top_to1555900337at_nat) tptp.top_to1411004326lle_tv))))) % 0.46/0.92 (assume @p258 (forall (@list @t15 @t318) (=> @t546 (=> @t562 (= (_ (_ tptp.image_1787705850at_nat (_ (_ tptp.produc1685803475tv_nat @t15) @t318)) tptp.top_to1411004326lle_tv) tptp.top_to1555900337at_nat))))) % 0.46/0.92 (assume @p259 (forall (@list @t15 @t326) (=> @t546 (=> @t563 (= (_ (_ tptp.image_149830562lle_tv (_ (_ tptp.produc2101297531lle_tv @t15) @t326)) tptp.top_to1411004326lle_tv) tptp.top_to1411004326lle_tv))))) % 0.46/0.92 (assume @p260 (forall (@list @t93 @t321) (=> @t549 (=> @t560 (= (_ (_ tptp.image_1597721174tv_nat (_ (_ tptp.produc1250721397at_nat @t93) @t321)) tptp.top_to1555900337at_nat) tptp.top_to975729152tv_nat))))) % 0.46/0.92 (assume @p261 (forall (@list @t93 @t356) (=> @t549 (=> @t561 (= (_ (_ tptp.image_1507992062lle_tv (_ (_ tptp.produc210389789lle_tv @t93) @t356)) tptp.top_to1555900337at_nat) tptp.top_to1871154984lle_tv))))) % 0.46/0.92 (assume @p262 (forall (@list @t93 @t318) (=> @t549 (=> @t562 (= (_ (_ tptp.image_53754658tv_nat (_ (_ tptp.produc189459613tv_nat @t93) @t318)) tptp.top_to1411004326lle_tv) tptp.top_to975729152tv_nat))))) % 0.46/0.92 (assume @p263 (forall (@list @t93 @t326) (=> @t549 (=> @t563 (= (_ (_ tptp.image_988201162lle_tv (_ (_ tptp.produc1975500101lle_tv @t93) @t326)) tptp.top_to1411004326lle_tv) tptp.top_to1871154984lle_tv))))) % 0.46/0.92 (assume @p264 (forall (@list @t551 @t321) (=> @t554 (=> @t560 (= (_ (_ tptp.image_1805124128at_nat (_ (_ tptp.produc386540311at_nat @t551) @t321)) tptp.top_to975729152tv_nat) tptp.top_to1555900337at_nat))))) % 0.46/0.92 (assume @p265 (forall (@list @t551 @t356) (=> @t554 (=> @t561 (= (_ (_ tptp.image_1200372424lle_tv (_ (_ tptp.produc72207551lle_tv @t551) @t356)) tptp.top_to975729152tv_nat) tptp.top_to1411004326lle_tv))))) % 0.46/0.92 (assume @p266 (forall (@list @t15 @t566) (=> @t122 (= (_ (_ tptp.member_nat @t566) @t545) (exists @t257 (and (= @t566 @t198) (forall @t564 (=> (= @t566 @t197) (= @t183 @t184))))))))) % 0.46/0.92 (assume @p267 (forall (@list @t126 @t430) (=> @t131 (= (_ (_ tptp.member266900804lle_tv @t430) @t557) (exists @t253 (and (= @t430 @t203) (forall @t565 (=> (= @t430 @t202) (= @t199 @t200))))))))) % 0.46/0.92 (assume @p268 (forall @t570 (=> @t122 @t569))) % 0.46/0.92 (assume @p269 (forall @t574 (=> @t131 @t573))) % 0.46/0.92 (assume @p270 (forall (@list @t15 @t235 @t255) (=> @t122 @t575))) % 0.46/0.92 (assume @p271 (forall (@list @t126 @t231 @t251) (=> @t131 @t576))) % 0.46/0.92 (assume @p272 (forall (@list @t579 @t485 @t509 @t474) (=> (_ @t580 @t528) (not (forall @t442 (=> (= @t579 (_ (_ tptp.produc1710735575lle_fm (_ @t485 @t439)) (_ @t509 @t438))) @t578)))))) % 0.46/0.92 (assume @p273 (forall (@list @t579 @t517 @t516 @t479) (=> (_ @t580 @t531) (not (forall @t446 (=> (= @t579 (_ (_ tptp.produc1710735575lle_fm (_ @t517 @t443)) (_ @t516 @t167))) @t582)))))) % 0.46/0.92 (assume @p274 (forall (@list @t583 @t513 @t512 @t474) (=> (_ @t584 @t530) (not (forall @t442 (=> (= @t583 (_ (_ tptp.produc1680557635lle_tv (_ @t513 @t439)) (_ @t512 @t438))) @t578)))))) % 0.46/0.92 (assume @p275 (forall (@list @t583 @t488 @t326 @t479) (=> (_ @t584 @t533) (not (forall @t446 (=> (= @t583 (_ (_ tptp.produc1680557635lle_tv (_ @t488 @t443)) (_ @t326 @t167))) @t582)))))) % 0.46/0.92 (assume @p276 (forall (@list @t15 @t255 @t91) (=> @t320 (=> (_ @t342 @t523) (= (_ @t15 @t407) @t91))))) % 0.46/0.92 (assume @p277 (forall (@list @t126 @t251 @t124) (=> @t325 (=> (_ @t348 @t526) (= (_ @t126 @t408) @t124))))) % 0.46/0.92 (assume @p278 (forall @t524 (=> @t320 (_ (_ tptp.inj_on_nat_nat @t405) @t523)))) % 0.46/0.92 (assume @p279 (forall @t527 (=> @t325 (_ (_ tptp.inj_on772319074lle_tv @t406) @t526)))) % 0.46/0.92 (assume @p280 (forall (@list @t15 @t585) (=> @t122 (=> @t587 (_ @t586 (_ (_ tptp.inv_image_nat_nat @t585) @t15)))))) % 0.46/0.92 (assume @p281 (forall (@list @t93 @t588) (=> @t96 (=> @t590 (_ @t586 (_ (_ tptp.inv_im516950809tv_nat @t588) @t93)))))) % 0.46/0.92 (assume @p282 (forall (@list @t551 @t585) (=> (_ (_ tptp.inj_on1179712058tv_nat @t551) tptp.top_to1057771083lle_tv) (=> @t587 (_ @t589 (_ (_ tptp.inv_im1292588663lle_tv @t585) @t551)))))) % 0.46/0.92 (assume @p283 (forall (@list @t126 @t588) (=> @t131 (=> @t590 (_ @t589 (_ (_ tptp.inv_im719552961lle_tv @t588) @t126)))))) % 0.46/0.92 (assume @p284 (forall (@list @t15 @t255 @t78 @t567) (=> @t320 (=> (_ @t79 @t523) (=> @t592 (_ (_ tptp.member_nat (_ @t405 @t78)) @t567)))))) % 0.46/0.92 (assume @p285 (forall (@list @t126 @t251 @t80 @t571) (=> @t325 (=> (_ @t81 @t526) (=> @t594 (_ (_ tptp.member266900804lle_tv (_ @t406 @t80)) @t571)))))) % 0.46/0.92 (assume @p286 (forall @t596 (= @t595 @t460))) % 0.46/0.92 (assume @p287 (forall @t598 (= @t597 @t466))) % 0.46/0.92 (assume @p288 (forall (@list @t484 @t216 @t424) (=> (= @t599 @t424) (= @t484 @t424)))) % 0.46/0.92 (assume @p289 (forall (@list @t374 @t124 @t433) (=> (= @t600 @t433) (= @t374 @t433)))) % 0.46/0.92 (assume @p290 (forall (@list @t484 @t216 @t601) (=> (= @t602 @t601) (= @t216 @t601)))) % 0.46/0.92 (assume @p291 (forall (@list @t374 @t124 @t231) (=> (= @t603 @t231) (= @t124 @t231)))) % 0.46/0.92 (assume @p292 (forall @t604 (= (_ tptp.produc29804011lle_fm @t414) @t413))) % 0.46/0.92 (assume @p293 (forall @t605 (= (_ tptp.produc1636169559lle_tv @t419) @t418))) % 0.46/0.92 (assume @p294 (forall @t604 (= (_ tptp.produc148705065lle_fm @t414) @t411))) % 0.46/0.92 (assume @p295 (forall @t605 (= (_ tptp.produc547496597lle_tv @t419) @t416))) % 0.46/0.92 (assume @p296 (forall @t596 (= @t460 @t595))) % 0.46/0.92 (assume @p297 (forall @t598 (= @t466 @t597))) % 0.46/0.92 (assume @p298 (forall (@list @t606) (= @t606 (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t606)) (_ tptp.produc148705065lle_fm @t606))))) % 0.46/0.92 (assume @p299 (forall (@list @t607) (= @t607 (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t607)) (_ tptp.produc547496597lle_tv @t607))))) % 0.46/0.92 (assume @p300 (forall (@list @t609 @t608) (=> (forall @t442 (=> (_ @t577 @t609) (_ @t577 @t608))) (_ (_ tptp.ord_le1007985907lle_fm @t609) @t608)))) % 0.46/0.92 (assume @p301 (forall (@list @t611 @t610) (=> (forall @t446 (=> (_ @t581 @t611) (_ @t581 @t610))) (_ (_ tptp.ord_le1784136743lle_tv @t611) @t610)))) % 0.46/0.92 (assume @p302 (forall @t613 (_ (_ tptp.ord_less_eq_set_nat @t612) tptp.top_top_set_nat))) % 0.46/0.92 (assume @p303 (forall @t615 (_ (_ tptp.ord_le241064091lle_tv @t614) tptp.top_to1057771083lle_tv))) % 0.46/0.92 (assume @p304 (forall @t613 (= @t617 @t616))) % 0.46/0.92 (assume @p305 (forall @t615 (= @t619 @t618))) % 0.46/0.92 (assume @p306 (forall @t613 (=> @t617 @t616))) % 0.46/0.92 (assume @p307 (forall @t615 (=> @t619 @t618))) % 0.46/0.92 (assume @p308 (forall @t258 (_ @t591 tptp.top_top_set_nat))) % 0.46/0.92 (assume @p309 (forall @t254 (_ @t593 tptp.top_to1057771083lle_tv))) % 0.46/0.92 (assume @p310 (forall @t570 (=> @t320 (=> (_ @t621 @t255) @t620)))) % 0.46/0.92 (assume @p311 (forall @t574 (=> @t325 (=> (_ @t623 @t251) @t622)))) % 0.46/0.92 (assume @p312 (forall (@list @t15 @t567 @t255) (=> @t620 (=> @t592 @t320)))) % 0.46/0.92 (assume @p313 (forall (@list @t126 @t571 @t251) (=> @t622 (=> @t594 @t325)))) % 0.46/0.92 (assume @p314 (forall (@list @t15 @t567 @t235 @t255) (=> @t620 (=> (_ @t238 @t567) (=> @t592 @t575))))) % 0.46/0.92 (assume @p315 (forall (@list @t126 @t571 @t231 @t251) (=> @t622 (=> (_ @t234 @t571) (=> @t594 @t576))))) % 0.46/0.92 (assume @p316 (forall (@list @t15 @t624 @t255 @t567) (=> (_ @t121 @t624) (=> (_ @t591 @t624) (=> (_ @t621 @t624) @t569))))) % 0.46/0.92 (assume @p317 (forall (@list @t126 @t625 @t251 @t571) (=> (_ @t130 @t625) (=> (_ @t593 @t625) (=> (_ @t623 @t625) @t573))))) % 0.46/0.92 (assume @p318 (forall @t570 (=> @t122 (= (_ (_ tptp.ord_less_eq_set_nat @t523) @t568) @t592)))) % 0.46/0.92 (assume @p319 (forall @t574 (=> @t131 (= (_ (_ tptp.ord_le241064091lle_tv @t526) @t572) @t594)))) % 0.46/0.92 (assume @p320 (forall (@list @t626 @t216 @t484) (=> (_ (_ @t626 @t216) @t484) (_ (_ @t626 @t602) @t599)))) % 0.46/0.92 (assume @p321 (forall (@list @t627 @t124 @t374) (=> (_ (_ @t627 @t124) @t374) (_ (_ @t627 @t603) @t600)))) % 0.46/0.92 (assume @p322 (forall (@list @t631 @t628 @t630 @t20) (=> (_ @t631 @t628) (=> (_ @t630 @t20) (and (_ @t631 (_ tptp.produc29804011lle_fm @t629)) (_ @t630 (_ tptp.produc148705065lle_fm @t629))))))) % 0.46/0.92 (assume @p323 (forall (@list @t635 @t633 @t259 @t632) (=> (_ @t635 @t633) (=> (_ @t259 @t632) (and (_ @t635 (_ tptp.produc1636169559lle_tv @t634)) (_ @t259 (_ tptp.produc547496597lle_tv @t634))))))) % 0.46/0.92 (assume @p324 (forall (@list @t636 @t484 @t216 @t227) (=> (_ (_ @t636 @t484) @t216) (=> (= @t227 @t487) (_ (_ @t636 (_ tptp.produc29804011lle_fm @t227)) (_ tptp.produc148705065lle_fm @t227)))))) % 0.46/0.92 (assume @p325 (forall (@list @t396 @t374 @t124 @t229) (=> (_ (_ @t396 @t374) @t124) (=> (= @t229 @t490) (_ (_ @t396 (_ tptp.produc1636169559lle_tv @t229)) (_ tptp.produc547496597lle_tv @t229)))))) % 0.46/0.92 (assume @p326 (forall (@list @t638 @t15 @t639) (= (_ (_ tptp.ord_less_eq_set_nat @t638) (_ @t522 @t639)) (exists (@list @t637) (and (_ (_ tptp.ord_less_eq_set_nat @t637) @t639) (_ @t121 @t637) (= @t638 (_ @t522 @t637))))))) % 0.46/0.92 (assume @p327 (forall (@list @t641 @t126 @t642) (= (_ (_ tptp.ord_le241064091lle_tv @t641) (_ @t525 @t642)) (exists (@list @t640) (and (_ (_ tptp.ord_le241064091lle_tv @t640) @t642) (_ @t130 @t640) (= @t641 (_ @t525 @t640))))))) % 0.46/0.92 (assume @p328 (forall (@list @t643) (or (= @t643 true) (= @t643 false)))) % 0.46/0.92 (assume @p329 (forall @t644 (= (_ (_ (_ tptp.if_Par1134130401lle_tv false) @t80) @t124) @t124))) % 0.46/0.92 (assume @p330 (forall @t644 (= (_ (_ (_ tptp.if_Par1134130401lle_tv true) @t80) @t124) @t80))) % 0.46/0.92 (assume @p331 @t646) % 0.46/0.92 (assume @p332 true) % 0.46/0.92 (step @p333 (= tptp.paraco761681009ge_int @t650) :rule refl :args (@t650)) % 0.46/0.92 (step @p334 (= tptp.paraco327635598_valid @t651) :rule refl :args (@t651)) % 0.46/0.92 (step @p335 (= tptp.top_to1299250770e_tv_o @t652) :rule refl :args (@t652)) % 0.46/0.92 (step @p336 (= tptp.top_top_nat_o @t653) :rule refl :args (@t653)) % 0.46/0.92 (step @p337 (= tptp.inj_on2112487900lle_tv @t656) :rule refl :args (@t656)) % 0.46/0.92 (step @p338 (= tptp.inj_on552895452tv_nat @t661) :rule refl :args (@t661)) % 0.46/0.92 (step @p339 (= tptp.inj_on1745913142lle_tv @t666) :rule refl :args (@t666)) % 0.46/0.92 (step @p340 (= tptp.inj_on26176689at_nat @t671) :rule refl :args (@t671)) % 0.46/0.92 (step @p341 (= tptp.inj_on1955349912lle_tv @t676) :rule refl :args (@t676)) % 0.46/0.92 (step @p342 (= tptp.inj_on_nat_nat @t677) :rule refl :args (@t677)) % 0.46/0.92 (step @p343 (= tptp.inj_on772319074lle_tv @t680) :rule refl :args (@t680)) % 0.46/0.92 (step @p344 (= tptp.top_to900819589_nat_o @t681) :rule refl :args (@t681)) % 0.46/0.92 (step @p345 (= tptp.top_to1889334367e_tv_o @t682) :rule refl :args (@t682)) % 0.46/0.92 (step @p346 (= tptp.top_to632227436_nat_o @t683) :rule refl :args (@t683)) % 0.46/0.92 (step @p347 (= tptp.produc234482697lle_tv @t687) :rule refl :args (@t687)) % 0.46/0.92 (step @p348 (= tptp.produc1232814113lle_tv @t689) :rule refl :args (@t689)) % 0.46/0.92 (step @p349 (= tptp.produc178635363at_nat @t691) :rule refl :args (@t691)) % 0.46/0.92 (step @p350 :rule refl :args ((tptp.paraco1147068288nge_tv tptp.f @t3))) % 0.46/0.92 (step @p351 :rule refl :args (@t692)) % 0.46/0.92 (step @p352 :rule refl :args (tptp.f)) % 0.46/0.92 (step @p353 :rule cong :premises (@p352 @p351) :args (@t693)) % 0.46/0.92 (step @p354 :rule trans :premises (@p353 @p350)) % 0.46/0.92 (step @p355 :rule refl :args (@t4)) % 0.46/0.92 (step @p356 :rule ho_cong :premises (@p355 @p351)) % 0.46/0.92 (step @p357 :rule cong :premises (@p356 @p354) :args ((= (_ @t4 @t692) @t693))) % 0.46/0.92 (step @p358 :rule symm :premises (@p357)) % 0.46/0.92 (step @p359 :rule refl :args (@t5)) % 0.46/0.92 (step @p360 :rule eq_resolve :premises (@p359 @p358)) % 0.46/0.92 (step @p361 :rule refl :args (@t3)) % 0.46/0.92 (step @p362 :rule cong :premises (@p361 @p351) :args ((= @t3 @t692))) % 0.46/0.92 (step @p363 :rule symm :premises (@p362)) % 0.46/0.92 (step @p364 :rule eq_resolve :premises (@p361 @p363)) % 0.46/0.92 (step @p365 :rule refl :args (@t4)) % 0.46/0.92 (step @p366 :rule ho_cong :premises (@p365 @p364)) % 0.46/0.92 (step @p367 :rule trans :premises (@p366 @p360)) % 0.46/0.92 (step @p368 :rule refl :args (@t695)) % 0.46/0.92 (step @p369 :rule refl :args (@t696)) % 0.46/0.92 (step @p370 :rule cong :premises (@p369 @p368) :args ((= @t696 @t695))) % 0.46/0.92 (step @p371 :rule symm :premises (@p370)) % 0.46/0.92 (step @p372 :rule eq_resolve :premises (@p369 @p371)) % 0.46/0.92 (step @p373 :rule skolem_intro :args (@t694)) % 0.46/0.92 (step @p374 :rule symm :premises (@p373)) % 0.46/0.92 (step @p375 :rule refl :args (tptp.paraco1344940915le_Det)) % 0.46/0.92 (step @p376 :rule ho_cong :premises (@p375 @p374)) % 0.46/0.92 (step @p377 :rule trans :premises (@p376 @p372)) % 0.46/0.92 (step @p378 :rule cong :premises (@p377 @p367) :args ((= @t1 @t5))) % 0.46/0.92 (step @p379 :rule eq-symm :args (@t5 @t1)) % 0.46/0.92 (step @p380 :rule trans :premises (@p379 @p378)) % 0.46/0.92 (step @p381 :rule eq_resolve :premises (@p2 @p380)) % 0.46/0.92 (step @p382 :rule refl :args (@t699)) % 0.46/0.92 (step @p383 :rule refl :args (@t700)) % 0.46/0.92 (step @p384 :rule cong :premises (@p383 @p382) :args ((= @t700 @t699))) % 0.46/0.92 (step @p385 :rule symm :premises (@p384)) % 0.46/0.92 (step @p386 :rule eq_resolve :premises (@p383 @p385)) % 0.46/0.92 (step @p387 :rule refl :args (tptp.p2)) % 0.46/0.92 (step @p388 :rule eq-refl :args (@t697)) % 0.46/0.92 (step @p389 :rule skolem_intro :args (@t698)) % 0.46/0.92 (step @p390 :rule refl :args (@t697)) % 0.46/0.92 (step @p391 :rule cong :premises (@p390 @p389) :args ((= @t697 @t698))) % 0.46/0.92 (step @p392 :rule trans :premises (@p391 @p388)) % 0.46/0.92 (step @p393 :rule true_elim :premises (@p392)) % 0.46/0.92 (step @p394 :rule refl :args (tptp.paraco1325918602e_eval)) % 0.46/0.92 (step @p395 :rule ho_cong :premises (@p394 @p393)) % 0.46/0.92 (step @p396 :rule ho_cong :premises (@p395 @p387)) % 0.46/0.92 (step @p397 :rule trans :premises (@p396 @p386)) % 0.46/0.92 (step @p398 :rule cong :premises (@p367 @p397) :args ((= @t5 @t701))) % 0.46/0.92 (step @p399 :rule eq-symm :args (@t701 @t5)) % 0.46/0.92 (step @p400 :rule refl :args (@t5)) % 0.46/0.92 (step @p401 :rule beta-reduce :args ((= (_ @t702 tptp.i) @t697))) % 0.46/0.92 (step @p402 :rule refl :args (tptp.i)) % 0.46/0.92 (step @p403 :rule beta-reduce :args ((= @t703 @t702))) % 0.46/0.92 (step @p404 :rule ho_cong :premises (@p403 @p402)) % 0.46/0.92 (step @p405 :rule trans :premises (@p404 @p401)) % 0.46/0.92 (step @p406 :rule ho_cong :premises (@p394 @p405)) % 0.46/0.92 (step @p407 :rule ho_cong :premises (@p406 @p387)) % 0.46/0.92 (step @p408 :rule cong :premises (@p407 @p400) :args ((= @t704 @t5))) % 0.46/0.92 (step @p409 :rule trans :premises (@p408 @p399)) % 0.46/0.92 (step @p410 :rule refl :args (tptp.f)) % 0.46/0.92 (step @p411 :rule ho_cong :premises (@p333 @p410)) % 0.46/0.92 (step @p412 :rule ho_cong :premises (@p411 @p402)) % 0.46/0.92 (step @p413 :rule ho_cong :premises (@p394 @p412)) % 0.46/0.92 (step @p414 :rule ho_cong :premises (@p413 @p387)) % 0.46/0.92 (step @p415 :rule cong :premises (@p414 @p400) :args (@t8)) % 0.46/0.92 (step @p416 :rule trans :premises (@p415 @p409)) % 0.46/0.92 (step @p417 :rule trans :premises (@p416 @p398)) % 0.46/0.92 (step @p418 :rule eq_resolve :premises (@p3 @p417)) % 0.46/0.92 (step @p419 :rule cong :premises (@p377 @p397) :args (@t705)) % 0.46/0.92 (step @p420 :rule cong :premises (@p419) :args ((not @t705))) % 0.46/0.92 (step @p421 :rule eq-symm :args (@t701 @t1)) % 0.46/0.92 (step @p422 :rule refl :args (@t1)) % 0.46/0.92 (step @p423 :rule cong :premises (@p407 @p422) :args (@t706)) % 0.46/0.92 (step @p424 :rule trans :premises (@p423 @p421)) % 0.46/0.92 (step @p425 :rule cong :premises (@p424) :args ((not @t706))) % 0.46/0.92 (step @p426 :rule cong :premises (@p414 @p422) :args (@t645)) % 0.46/0.92 (step @p427 :rule cong :premises (@p426) :args (@t646)) % 0.46/0.92 (step @p428 :rule trans :premises (@p427 @p425)) % 0.46/0.92 (step @p429 :rule trans :premises (@p428 @p420)) % 0.46/0.92 (step @p430 :rule eq_resolve :premises (@p331 @p429)) % 0.46/0.92 (assume-push @p442 @t707) % 0.46/0.92 (assume-push @p443 @t708) % 0.46/0.92 (step @p433 :rule trans :premises (@p381 @p418)) % 0.46/0.92 (step-pop @p444 :rule scope :premises (@p433)) % 0.46/0.92 (step-pop @p445 :rule scope :premises (@p444)) % 0.46/0.92 (step @p434 :rule process_scope :premises (@p445) :args (@t709)) % 0.46/0.92 (step @p437 :rule implies_elim :premises (@p434)) % 0.46/0.92 (step @p438 :rule cnf_and_neg :args (@t710)) % 0.46/0.92 (step @p439 :rule resolution :premises (@p438 @p437) :args (true @t710)) % 0.46/0.92 (step @p440 :rule reordering :premises (@p439) :args ((or @t709 (not @t707) (not @t708)))) % 0.46/0.92 (step @p441 false :rule chain_m_resolution :premises (@p440 @p430 @p418 @p381) :args (false (@list true false false) (@list @t709 @t708 @t707))) % 0.46/0.92 ) % 0.46/0.92 % SZS output end Proof % 0.46/0.92 % cvc5 exiting %------------------------------------------------------------------------------