%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP073^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:24:58 AM UTC 2026 % Result : Theorem 0.47s 0.90s % Output : Proof 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP073^1 : TPTP v9.2.1. Released v7.5.0. % 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.34 % Computer : n001.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 04:14:05 EDT 2026 % 0.18/0.35 % CPUTime : % 0.39/0.61 %----Proving TH0 % 0.47/0.90 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.47/0.90 % SZS status Theorem % 0.47/0.90 % SZS output start Proof % 0.47/0.90 ( % 0.47/0.90 (declare-sort tptp.nat 0) % 0.47/0.90 (declare-sort tptp.set_nat 0) % 0.47/0.90 (declare-sort tptp.hF_Mirabelle_hf 0) % 0.47/0.90 (declare-sort tptp.set_HF_Mirabelle_hf 0) % 0.47/0.90 (declare-sort tptp.set_se933006839lle_hf 0) % 0.47/0.90 (declare-const tptp.hF_Mirabelle_hfset (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.member1367349282lle_hf (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.ord_less_nat (-> tptp.nat tptp.nat Bool)) % 0.47/0.90 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.47/0.90 (declare-const tptp.a tptp.hF_Mirabelle_hf) % 0.47/0.90 (declare-const tptp.b tptp.hF_Mirabelle_hf) % 0.47/0.90 (declare-const tptp.zero_zero_nat tptp.nat) % 0.47/0.90 (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat)) % 0.47/0.90 (declare-const tptp.zero_z189798548lle_hf tptp.hF_Mirabelle_hf) % 0.47/0.90 (declare-const tptp.image_246164834lle_hf (-> (-> tptp.nat tptp.hF_Mirabelle_hf) tptp.set_nat tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.inj_on1988990670lle_hf (-> (-> tptp.nat tptp.hF_Mirabelle_hf) tptp.set_nat Bool)) % 0.47/0.90 (declare-const tptp.image_131453538hf_nat (-> (-> tptp.hF_Mirabelle_hf tptp.nat) tptp.set_HF_Mirabelle_hf tptp.set_nat)) % 0.47/0.90 (declare-const tptp.inj_on_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat Bool)) % 0.47/0.90 (declare-const tptp.image_1743964010lle_hf (-> (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.inj_on755450110lle_hf (-> (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.collec1758573718lle_hf (-> (-> tptp.set_HF_Mirabelle_hf Bool) tptp.set_se933006839lle_hf)) % 0.47/0.90 (declare-const tptp.hF_Mirabelle_RepFun (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.order_1640852850lle_hf (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.hF_Mirabelle_HF (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.finite_card_nat (-> tptp.set_nat tptp.nat)) % 0.47/0.90 (declare-const tptp.collec2046588256lle_hf (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.ord_less_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 0.47/0.90 (declare-const tptp.hF_Mirabelle_Replace (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.member1490636632lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_se933006839lle_hf Bool)) % 0.47/0.90 (declare-const tptp.set_or1544565540an_nat (-> tptp.nat tptp.nat tptp.set_nat)) % 0.47/0.90 (declare-const tptp.hF_Mirabelle_HUnion (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.finite1450550360lle_hf (-> tptp.set_se933006839lle_hf Bool)) % 0.47/0.90 (declare-const tptp.image_899003828lle_hf (-> (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_se933006839lle_hf tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.hF_Mir818139703ollect (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.hF_Mir1248913145eplace (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf)) % 0.47/0.90 (declare-const tptp.finite586181922lle_hf (-> tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.ord_le432112161lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 0.47/0.90 (declare-const tptp.finite1213132899lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.nat)) % 0.47/0.90 (declare-const tptp.ord_le1344122901lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.inj_on1874279374hf_nat (-> (-> tptp.hF_Mirabelle_hf tptp.nat) tptp.set_HF_Mirabelle_hf Bool)) % 0.47/0.90 (declare-const tptp.ordering_nat (-> (-> tptp.nat tptp.nat Bool) (-> tptp.nat tptp.nat Bool) Bool)) % 0.47/0.90 (declare-const tptp.inj_on811196232lle_hf (-> (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_se933006839lle_hf Bool)) % 0.47/0.90 (declare-const tptp.orderi1737556723lle_hf (-> (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) Bool)) % 0.47/0.90 (declare-const tptp.order_Greatest_nat (-> (-> tptp.nat Bool) tptp.nat)) % 0.47/0.90 (declare-const tptp.finite90088345lle_hf (-> tptp.set_se933006839lle_hf tptp.nat)) % 0.47/0.90 (define tptp.hF_Mirabelle_hmem () (let ((_let_1 (@var "B2" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A2" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1367349282lle_hf _let_2) (_ tptp.hF_Mirabelle_hfset _let_1)))))) % 0.47/0.90 (define tptp.ord_le976219883lle_hf () (let ((_let_1 (@var "B3" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "X2" tptp.hF_Mirabelle_hf))) (let ((_let_3 (_ tptp.hF_Mirabelle_hmem _let_2))) (let ((_let_4 (@var "A3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.47/0.90 (define tptp.ord_le2017230260lle_hf () (let ((_let_1 (@var "Y6" (-> Bool tptp.hF_Mirabelle_hf)))) (let ((_let_2 (@var "X4" (-> Bool tptp.hF_Mirabelle_hf)))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le976219883lle_hf (_ _let_2 false)) (_ _let_1 false)) (_ (_ tptp.ord_le976219883lle_hf (_ _let_2 true)) (_ _let_1 true))))))) % 0.47/0.90 (define tptp.ord_less_eq_nat () (let ((_let_1 (@var "Y3" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (lambda (@list _let_2 _let_1) (or (_ (_ tptp.ord_less_nat _let_2) _let_1) (= _let_2 _let_1)))))) % 0.47/0.90 (define tptp.ord_less_eq_o_nat () (let ((_let_1 (@var "Y6" (-> Bool tptp.nat)))) (let ((_let_2 (@var "X4" (-> Bool tptp.nat)))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_nat (_ _let_2 false)) (_ _let_1 false)) (_ (_ tptp.ord_less_eq_nat (_ _let_2 true)) (_ _let_1 true))))))) % 0.47/0.90 (define tptp.ord_le1310584031lle_hf () (let ((_let_1 (@var "B3" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le976219883lle_hf _let_2) _let_1) (not (= _let_2 _let_1))))))) % 0.47/0.90 (define tptp.order_690706045lle_hf () (let ((_let_1 (@var "X2" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "F2" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)))) (let ((_let_3 (@var "Y3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2) (forall (@list _let_1 _let_3) (=> (_ (_ tptp.ord_le976219883lle_hf _let_1) _let_3) (_ (_ tptp.ord_le976219883lle_hf (_ _let_2 _let_3)) (_ _let_2 _let_1))))))))) % 0.47/0.90 (define tptp.order_557194383hf_nat () (let ((_let_1 (@var "X2" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "F2" (-> tptp.hF_Mirabelle_hf tptp.nat)))) (let ((_let_3 (@var "Y3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2) (forall (@list _let_1 _let_3) (=> (_ (_ tptp.ord_le976219883lle_hf _let_1) _let_3) (_ (_ tptp.ord_less_eq_nat (_ _let_2 _let_3)) (_ _let_2 _let_1))))))))) % 0.47/0.90 (define tptp.order_671905679lle_hf () (let ((_let_1 (@var "X2" tptp.nat))) (let ((_let_2 (@var "F2" (-> tptp.nat tptp.hF_Mirabelle_hf)))) (let ((_let_3 (@var "Y3" tptp.nat))) (lambda (@list _let_2) (forall (@list _let_1 _let_3) (=> (_ (_ tptp.ord_less_eq_nat _let_1) _let_3) (_ (_ tptp.ord_le976219883lle_hf (_ _let_2 _let_3)) (_ _let_2 _let_1))))))))) % 0.47/0.90 (define tptp.order_1631207636at_nat () (let ((_let_1 (@var "X2" tptp.nat))) (let ((_let_2 (@var "F2" (-> tptp.nat tptp.nat)))) (let ((_let_3 (@var "Y3" tptp.nat))) (lambda (@list _let_2) (forall (@list _let_1 _let_3) (=> (_ (_ tptp.ord_less_eq_nat _let_1) _let_3) (_ (_ tptp.ord_less_eq_nat (_ _let_2 _let_3)) (_ _let_2 _let_1))))))))) % 0.47/0.90 (define tptp.finite_finite_nat () (let ((_let_1 (@var "M" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "N3" tptp.set_nat))) (lambda (@list _let_3) (exists (@list _let_1) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_3) (_ (_ tptp.ord_less_eq_nat _let_2) _let_1))))))))) % 0.47/0.90 (define @t1 () (@var "B" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t2 () (@var "A" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t3 () (= @t2 @t1)) % 0.47/0.90 (define @t4 () (@var "X" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t5 () (_ tptp.hF_Mirabelle_hmem @t4)) % 0.47/0.90 (define @t6 () (@list @t4)) % 0.47/0.90 (define @t7 () (@list @t2 @t1)) % 0.47/0.90 (define @t8 () (@var "B2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t9 () (@var "X2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t10 () (_ tptp.hF_Mirabelle_hmem @t9)) % 0.47/0.90 (define @t11 () (@var "A2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t12 () (@list @t9)) % 0.47/0.90 (define @t13 () (@list @t11 @t8)) % 0.47/0.90 (define @t14 () (@var "Z" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t15 () (@var "Y" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t16 () (lambda (@list @t15 @t14) (= @t15 @t14))) % 0.47/0.90 (define @t17 () (@var "V3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t18 () (@var "U2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t19 () (@var "R" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t20 () (_ @t19 @t18)) % 0.47/0.90 (define @t21 () (@var "X3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t22 () (_ tptp.hF_Mirabelle_hmem @t18)) % 0.47/0.90 (define @t23 () (_ @t22 @t21)) % 0.47/0.90 (define @t24 () (@list @t18)) % 0.47/0.90 (define @t25 () (@var "Z2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t26 () (_ (_ tptp.hF_Mirabelle_hmem @t17) @t25)) % 0.47/0.90 (define @t27 () (@list @t17)) % 0.47/0.90 (define @t28 () (@list @t25)) % 0.47/0.90 (define @t29 () (@var "V" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t30 () (@var "V2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t31 () (@var "U" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t32 () (_ @t19 @t31)) % 0.47/0.90 (define @t33 () (=> (_ @t32 @t29) (=> (_ @t32 @t30) (= @t30 @t29)))) % 0.47/0.90 (define @t34 () (_ tptp.hF_Mirabelle_hmem @t31)) % 0.47/0.90 (define @t35 () (@list @t31 @t29 @t30)) % 0.47/0.90 (define @t36 () (@var "Y2" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t37 () (@var "U3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t38 () (_ tptp.hF_Mirabelle_hmem @t37)) % 0.47/0.90 (define @t39 () (_ @t38 @t21)) % 0.47/0.90 (define @t40 () (_ @t38 @t25)) % 0.47/0.90 (define @t41 () (@list @t37)) % 0.47/0.90 (define @t42 () (@list @t21 @t36)) % 0.47/0.90 (define @t43 () (@var "Y3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t44 () (_ tptp.hF_Mirabelle_hmem @t43)) % 0.47/0.90 (define @t45 () (@list @t43)) % 0.47/0.90 (define @t46 () (@list @t21)) % 0.47/0.90 (define @t47 () (@var "P" (-> tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t48 () (@var "F" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t49 () (_ @t48 @t18)) % 0.47/0.90 (define @t50 () (_ tptp.ord_le976219883lle_hf @t21)) % 0.47/0.90 (define @t51 () (@var "X3" tptp.nat)) % 0.47/0.90 (define @t52 () (_ tptp.ord_less_eq_nat @t51)) % 0.47/0.90 (define @t53 () (@list @t51)) % 0.47/0.90 (define @t54 () (@var "V4" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t55 () (_ @t20 @t54)) % 0.47/0.90 (define @t56 () (@var "A4" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t57 () (_ @t22 @t56)) % 0.47/0.90 (define @t58 () (_ tptp.hF_Mirabelle_hmem @t54)) % 0.47/0.90 (define @t59 () (_ tptp.hF_Mirabelle_hmem @t21)) % 0.47/0.90 (define @t60 () (_ @t47 @t21)) % 0.47/0.90 (define @t61 () (_ tptp.hF_Mirabelle_Replace @t56)) % 0.47/0.90 (define @t62 () (@var "C" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t63 () (_ @t48 @t62)) % 0.47/0.90 (define @t64 () (_ tptp.ord_le976219883lle_hf @t2)) % 0.47/0.90 (define @t65 () (@var "Y4" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t66 () (_ @t48 @t65)) % 0.47/0.90 (define @t67 () (_ @t48 @t4)) % 0.47/0.90 (define @t68 () (_ tptp.ord_le976219883lle_hf @t4)) % 0.47/0.90 (define @t69 () (_ @t68 @t65)) % 0.47/0.90 (define @t70 () (@list @t4 @t65)) % 0.47/0.90 (define @t71 () (forall @t70 (=> @t69 (_ (_ tptp.ord_le976219883lle_hf @t67) @t66)))) % 0.47/0.90 (define @t72 () (_ tptp.ord_le976219883lle_hf @t1)) % 0.47/0.90 (define @t73 () (_ @t72 @t62)) % 0.47/0.90 (define @t74 () (=> @t73 (=> @t71 (_ @t64 @t63)))) % 0.47/0.90 (define @t75 () (_ @t48 @t1)) % 0.47/0.90 (define @t76 () (_ @t64 @t75)) % 0.47/0.90 (define @t77 () (@list @t2 @t48 @t1 @t62)) % 0.47/0.90 (define @t78 () (@var "C" tptp.nat)) % 0.47/0.90 (define @t79 () (@var "F" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t80 () (_ @t79 @t78)) % 0.47/0.90 (define @t81 () (@var "Y4" tptp.nat)) % 0.47/0.90 (define @t82 () (_ @t79 @t81)) % 0.47/0.90 (define @t83 () (@var "X" tptp.nat)) % 0.47/0.90 (define @t84 () (_ @t79 @t83)) % 0.47/0.90 (define @t85 () (_ tptp.ord_less_eq_nat @t83)) % 0.47/0.90 (define @t86 () (_ @t85 @t81)) % 0.47/0.90 (define @t87 () (@list @t83 @t81)) % 0.47/0.90 (define @t88 () (forall @t87 (=> @t86 (_ (_ tptp.ord_le976219883lle_hf @t84) @t82)))) % 0.47/0.90 (define @t89 () (@var "B" tptp.nat)) % 0.47/0.90 (define @t90 () (_ tptp.ord_less_eq_nat @t89)) % 0.47/0.90 (define @t91 () (_ @t90 @t78)) % 0.47/0.90 (define @t92 () (=> @t91 (=> @t88 (_ @t64 @t80)))) % 0.47/0.90 (define @t93 () (_ @t79 @t89)) % 0.47/0.90 (define @t94 () (_ @t64 @t93)) % 0.47/0.90 (define @t95 () (@list @t2 @t79 @t89 @t78)) % 0.47/0.90 (define @t96 () (@var "F" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 0.47/0.90 (define @t97 () (_ @t96 @t62)) % 0.47/0.90 (define @t98 () (@var "A" tptp.nat)) % 0.47/0.90 (define @t99 () (_ tptp.ord_less_eq_nat @t98)) % 0.47/0.90 (define @t100 () (_ @t96 @t65)) % 0.47/0.90 (define @t101 () (_ @t96 @t4)) % 0.47/0.90 (define @t102 () (forall @t70 (=> @t69 (_ (_ tptp.ord_less_eq_nat @t101) @t100)))) % 0.47/0.90 (define @t103 () (=> @t73 (=> @t102 (_ @t99 @t97)))) % 0.47/0.90 (define @t104 () (_ @t96 @t1)) % 0.47/0.90 (define @t105 () (_ @t99 @t104)) % 0.47/0.90 (define @t106 () (@list @t98 @t96 @t1 @t62)) % 0.47/0.90 (define @t107 () (@var "F" (-> tptp.nat tptp.nat))) % 0.47/0.90 (define @t108 () (_ @t107 @t78)) % 0.47/0.90 (define @t109 () (_ @t107 @t81)) % 0.47/0.90 (define @t110 () (_ @t107 @t83)) % 0.47/0.90 (define @t111 () (forall @t87 (=> @t86 (_ (_ tptp.ord_less_eq_nat @t110) @t109)))) % 0.47/0.90 (define @t112 () (=> @t91 (=> @t111 (_ @t99 @t108)))) % 0.47/0.90 (define @t113 () (_ @t107 @t89)) % 0.47/0.90 (define @t114 () (_ @t99 @t113)) % 0.47/0.90 (define @t115 () (@list @t98 @t107 @t89 @t78)) % 0.47/0.90 (define @t116 () (_ @t48 @t2)) % 0.47/0.90 (define @t117 () (=> @t71 (_ (_ tptp.ord_le976219883lle_hf @t116) @t62))) % 0.47/0.90 (define @t118 () (_ (_ tptp.ord_le976219883lle_hf @t75) @t62)) % 0.47/0.90 (define @t119 () (_ @t64 @t1)) % 0.47/0.90 (define @t120 () (@list @t2 @t1 @t48 @t62)) % 0.47/0.90 (define @t121 () (_ @t96 @t2)) % 0.47/0.90 (define @t122 () (=> @t102 (_ (_ tptp.ord_less_eq_nat @t121) @t78))) % 0.47/0.90 (define @t123 () (_ (_ tptp.ord_less_eq_nat @t104) @t78)) % 0.47/0.90 (define @t124 () (@list @t2 @t1 @t96 @t78)) % 0.47/0.90 (define @t125 () (_ @t79 @t98)) % 0.47/0.90 (define @t126 () (=> @t88 (_ (_ tptp.ord_le976219883lle_hf @t125) @t62))) % 0.47/0.90 (define @t127 () (_ (_ tptp.ord_le976219883lle_hf @t93) @t62)) % 0.47/0.90 (define @t128 () (_ @t99 @t89)) % 0.47/0.90 (define @t129 () (@list @t98 @t89 @t79 @t62)) % 0.47/0.90 (define @t130 () (_ @t107 @t98)) % 0.47/0.90 (define @t131 () (=> @t111 (_ (_ tptp.ord_less_eq_nat @t130) @t78))) % 0.47/0.90 (define @t132 () (_ (_ tptp.ord_less_eq_nat @t113) @t78)) % 0.47/0.90 (define @t133 () (@list @t98 @t89 @t107 @t78)) % 0.47/0.90 (define @t134 () (_ @t90 @t98)) % 0.47/0.90 (define @t135 () (= @t98 @t89)) % 0.47/0.90 (define @t136 () (@list @t98 @t89)) % 0.47/0.90 (define @t137 () (@var "Q" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t138 () (@var "B4" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t139 () (@var "P" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t140 () (_ @t5 @t138)) % 0.47/0.90 (define @t141 () (= @t56 @t138)) % 0.47/0.90 (define @t142 () (_ @t72 @t2)) % 0.47/0.90 (define @t143 () (@list @t1 @t2)) % 0.47/0.90 (define @t144 () (@list @t89 @t98)) % 0.47/0.90 (define @t145 () (_ (_ tptp.ord_le976219883lle_hf @t11) @t8)) % 0.47/0.90 (define @t146 () (_ (_ tptp.ord_le976219883lle_hf @t8) @t11)) % 0.47/0.90 (define @t147 () (@var "B2" tptp.nat)) % 0.47/0.90 (define @t148 () (@var "A2" tptp.nat)) % 0.47/0.90 (define @t149 () (_ (_ tptp.ord_less_eq_nat @t148) @t147)) % 0.47/0.90 (define @t150 () (_ (_ tptp.ord_less_eq_nat @t147) @t148)) % 0.47/0.90 (define @t151 () (@list @t148 @t147)) % 0.47/0.90 (define @t152 () (@var "Z" tptp.nat)) % 0.47/0.90 (define @t153 () (@var "Y" tptp.nat)) % 0.47/0.90 (define @t154 () (lambda (@list @t153 @t152) (= @t153 @t152))) % 0.47/0.90 (define @t155 () (_ tptp.ord_le976219883lle_hf @t62)) % 0.47/0.90 (define @t156 () (_ @t155 @t1)) % 0.47/0.90 (define @t157 () (@list @t1 @t2 @t62)) % 0.47/0.90 (define @t158 () (_ tptp.ord_less_eq_nat @t78)) % 0.47/0.90 (define @t159 () (_ @t158 @t89)) % 0.47/0.90 (define @t160 () (@list @t89 @t98 @t78)) % 0.47/0.90 (define @t161 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 0.47/0.90 (define @t162 () (@var "B5" tptp.nat)) % 0.47/0.90 (define @t163 () (@var "A5" tptp.nat)) % 0.47/0.90 (define @t164 () (_ @t161 @t163)) % 0.47/0.90 (define @t165 () (_ @t164 @t162)) % 0.47/0.90 (define @t166 () (@list @t163 @t162)) % 0.47/0.90 (define @t167 () (=> (forall @t166 (=> (_ (_ @t161 @t162) @t163) @t165)) (_ (_ @t161 @t98) @t89))) % 0.47/0.90 (define @t168 () (@list @t161 @t98 @t89)) % 0.47/0.90 (define @t169 () (@list @t2)) % 0.47/0.90 (define @t170 () (@list @t98)) % 0.47/0.90 (define @t171 () (@var "Z3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t172 () (_ tptp.ord_le976219883lle_hf @t36)) % 0.47/0.90 (define @t173 () (_ @t172 @t171)) % 0.47/0.90 (define @t174 () (_ @t50 @t36)) % 0.47/0.90 (define @t175 () (@list @t21 @t36 @t171)) % 0.47/0.90 (define @t176 () (@var "Z3" tptp.nat)) % 0.47/0.90 (define @t177 () (_ @t52 @t176)) % 0.47/0.90 (define @t178 () (@var "Y2" tptp.nat)) % 0.47/0.90 (define @t179 () (_ tptp.ord_less_eq_nat @t178)) % 0.47/0.90 (define @t180 () (_ @t179 @t176)) % 0.47/0.90 (define @t181 () (_ @t52 @t178)) % 0.47/0.90 (define @t182 () (@list @t51 @t178 @t176)) % 0.47/0.90 (define @t183 () (_ @t64 @t62)) % 0.47/0.90 (define @t184 () (= @t1 @t62)) % 0.47/0.90 (define @t185 () (@list @t2 @t1 @t62)) % 0.47/0.90 (define @t186 () (_ @t99 @t78)) % 0.47/0.90 (define @t187 () (= @t89 @t78)) % 0.47/0.90 (define @t188 () (@list @t98 @t89 @t78)) % 0.47/0.90 (define @t189 () (=> @t73 @t183)) % 0.47/0.90 (define @t190 () (=> @t91 @t186)) % 0.47/0.90 (define @t191 () (= @t21 @t36)) % 0.47/0.90 (define @t192 () (= @t174 @t191)) % 0.47/0.90 (define @t193 () (_ @t172 @t21)) % 0.47/0.90 (define @t194 () (@list @t36 @t21)) % 0.47/0.90 (define @t195 () (= @t51 @t178)) % 0.47/0.90 (define @t196 () (= @t181 @t195)) % 0.47/0.90 (define @t197 () (_ @t179 @t51)) % 0.47/0.90 (define @t198 () (@list @t178 @t51)) % 0.47/0.90 (define @t199 () (not @t181)) % 0.47/0.90 (define @t200 () (_ tptp.ord_less_eq_nat @t176)) % 0.47/0.90 (define @t201 () (_ @t200 @t51)) % 0.47/0.90 (define @t202 () (not @t197)) % 0.47/0.90 (define @t203 () (_ @t200 @t178)) % 0.47/0.90 (define @t204 () (@list @t51 @t178)) % 0.47/0.90 (define @t205 () (_ (_ tptp.ord_le976219883lle_hf @t43) @t9)) % 0.47/0.90 (define @t206 () (_ (_ tptp.ord_le976219883lle_hf @t9) @t43)) % 0.47/0.90 (define @t207 () (@list @t9 @t43)) % 0.47/0.90 (define @t208 () (@var "X2" tptp.nat)) % 0.47/0.90 (define @t209 () (@var "Y3" tptp.nat)) % 0.47/0.90 (define @t210 () (_ (_ tptp.ord_less_eq_nat @t209) @t208)) % 0.47/0.90 (define @t211 () (_ tptp.ord_less_eq_nat @t208)) % 0.47/0.90 (define @t212 () (_ @t211 @t209)) % 0.47/0.90 (define @t213 () (@list @t208 @t209)) % 0.47/0.90 (define @t214 () (= @t75 @t62)) % 0.47/0.90 (define @t215 () (= @t104 @t78)) % 0.47/0.90 (define @t216 () (= @t93 @t62)) % 0.47/0.90 (define @t217 () (= @t113 @t78)) % 0.47/0.90 (define @t218 () (= @t2 @t75)) % 0.47/0.90 (define @t219 () (= @t98 @t104)) % 0.47/0.90 (define @t220 () (= @t2 @t93)) % 0.47/0.90 (define @t221 () (= @t98 @t113)) % 0.47/0.90 (define @t222 () (_ tptp.order_1640852850lle_hf @t47)) % 0.47/0.90 (define @t223 () (forall (@list @t65) (=> (_ @t47 @t65) (_ (_ tptp.ord_le976219883lle_hf @t65) @t21)))) % 0.47/0.90 (define @t224 () (@var "P" (-> tptp.nat Bool))) % 0.47/0.90 (define @t225 () (_ tptp.order_Greatest_nat @t224)) % 0.47/0.90 (define @t226 () (forall (@list @t81) (=> (_ @t224 @t81) (_ (_ tptp.ord_less_eq_nat @t81) @t51)))) % 0.47/0.90 (define @t227 () (_ @t224 @t51)) % 0.47/0.90 (define @t228 () (@var "Q" (-> tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t229 () (@var "Y5" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t230 () (@var "Q" (-> tptp.nat Bool))) % 0.47/0.90 (define @t231 () (_ @t230 @t83)) % 0.47/0.90 (define @t232 () (@var "Y5" tptp.nat)) % 0.47/0.90 (define @t233 () (_ @t224 @t232)) % 0.47/0.90 (define @t234 () (@list @t232)) % 0.47/0.90 (define @t235 () (_ @t224 @t83)) % 0.47/0.90 (define @t236 () (@list @t83)) % 0.47/0.90 (define @t237 () (_ tptp.member1367349282lle_hf @t2)) % 0.47/0.90 (define @t238 () (@var "A" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t239 () (@var "P" (-> tptp.set_HF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t240 () (_ tptp.collec1758573718lle_hf @t239)) % 0.47/0.90 (define @t241 () (@var "A4" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t242 () (_ tptp.member1367349282lle_hf @t9)) % 0.47/0.90 (define @t243 () (@list @t241)) % 0.47/0.90 (define @t244 () (@var "A4" tptp.set_se933006839lle_hf)) % 0.47/0.90 (define @t245 () (@var "X2" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t246 () (@var "Q" (-> tptp.set_HF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t247 () (@var "X" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t248 () (_ (_ tptp.hF_Mirabelle_RepFun @t56) @t48)) % 0.47/0.90 (define @t249 () (_ tptp.order_690706045lle_hf @t48)) % 0.47/0.90 (define @t250 () (@list @t48)) % 0.47/0.90 (define @t251 () (_ tptp.order_557194383hf_nat @t96)) % 0.47/0.90 (define @t252 () (_ tptp.order_671905679lle_hf @t79)) % 0.47/0.90 (define @t253 () (_ tptp.order_1631207636at_nat @t107)) % 0.47/0.90 (define @t254 () (_ tptp.ord_le1310584031lle_hf @t2)) % 0.47/0.90 (define @t255 () (_ tptp.ord_less_nat @t98)) % 0.47/0.90 (define @t256 () (_ @t254 @t63)) % 0.47/0.90 (define @t257 () (_ (_ tptp.ord_le1310584031lle_hf @t4) @t65)) % 0.47/0.90 (define @t258 () (forall @t70 (=> @t257 (_ (_ tptp.ord_le1310584031lle_hf @t67) @t66)))) % 0.47/0.90 (define @t259 () (_ tptp.ord_le1310584031lle_hf @t1)) % 0.47/0.90 (define @t260 () (_ @t259 @t62)) % 0.47/0.90 (define @t261 () (=> @t260 (=> @t258 @t256))) % 0.47/0.90 (define @t262 () (_ @t255 @t97)) % 0.47/0.90 (define @t263 () (forall @t70 (=> @t257 (_ (_ tptp.ord_less_nat @t101) @t100)))) % 0.47/0.90 (define @t264 () (=> @t260 (=> @t263 @t262))) % 0.47/0.90 (define @t265 () (_ @t254 @t80)) % 0.47/0.90 (define @t266 () (_ tptp.ord_less_nat @t83)) % 0.47/0.90 (define @t267 () (_ @t266 @t81)) % 0.47/0.90 (define @t268 () (forall @t87 (=> @t267 (_ (_ tptp.ord_le1310584031lle_hf @t84) @t82)))) % 0.47/0.90 (define @t269 () (_ tptp.ord_less_nat @t89)) % 0.47/0.90 (define @t270 () (_ @t269 @t78)) % 0.47/0.90 (define @t271 () (=> @t270 (=> @t268 @t265))) % 0.47/0.90 (define @t272 () (_ @t255 @t108)) % 0.47/0.90 (define @t273 () (forall @t87 (=> @t267 (_ (_ tptp.ord_less_nat @t110) @t109)))) % 0.47/0.90 (define @t274 () (=> @t270 (=> @t273 @t272))) % 0.47/0.90 (define @t275 () (_ (_ tptp.ord_le1310584031lle_hf @t116) @t62)) % 0.47/0.90 (define @t276 () (=> @t258 @t275)) % 0.47/0.90 (define @t277 () (_ @t254 @t1)) % 0.47/0.90 (define @t278 () (_ (_ tptp.ord_less_nat @t121) @t78)) % 0.47/0.90 (define @t279 () (=> @t263 @t278)) % 0.47/0.90 (define @t280 () (_ (_ tptp.ord_le1310584031lle_hf @t125) @t62)) % 0.47/0.90 (define @t281 () (=> @t268 @t280)) % 0.47/0.90 (define @t282 () (_ @t255 @t89)) % 0.47/0.90 (define @t283 () (_ (_ tptp.ord_less_nat @t130) @t78)) % 0.47/0.90 (define @t284 () (=> @t273 @t283)) % 0.47/0.90 (define @t285 () (_ @t254 @t75)) % 0.47/0.90 (define @t286 () (_ @t254 @t93)) % 0.47/0.90 (define @t287 () (_ @t255 @t104)) % 0.47/0.90 (define @t288 () (_ @t255 @t113)) % 0.47/0.90 (define @t289 () (_ (_ tptp.ord_le1310584031lle_hf @t75) @t62)) % 0.47/0.90 (define @t290 () (_ (_ tptp.ord_less_nat @t104) @t78)) % 0.47/0.90 (define @t291 () (_ (_ tptp.ord_le1310584031lle_hf @t93) @t62)) % 0.47/0.90 (define @t292 () (_ (_ tptp.ord_less_nat @t113) @t78)) % 0.47/0.90 (define @t293 () (@var "X_1" tptp.nat)) % 0.47/0.90 (define @t294 () (_ tptp.ord_less_nat @t51)) % 0.47/0.90 (define @t295 () (_ tptp.ord_less_nat @t178)) % 0.47/0.90 (define @t296 () (_ @t295 @t51)) % 0.47/0.90 (define @t297 () (_ @t294 @t178)) % 0.47/0.90 (define @t298 () (not @t297)) % 0.47/0.90 (define @t299 () (not @t195)) % 0.47/0.90 (define @t300 () (_ @t259 @t2)) % 0.47/0.90 (define @t301 () (_ @t269 @t98)) % 0.47/0.90 (define @t302 () (_ tptp.ord_le1310584031lle_hf @t21)) % 0.47/0.90 (define @t303 () (_ @t302 @t36)) % 0.47/0.90 (define @t304 () (_ tptp.ord_le1310584031lle_hf @t36)) % 0.47/0.90 (define @t305 () (_ @t304 @t21)) % 0.47/0.90 (define @t306 () (not @t296)) % 0.47/0.90 (define @t307 () (_ @t302 @t171)) % 0.47/0.90 (define @t308 () (=> (_ @t304 @t171) @t307)) % 0.47/0.90 (define @t309 () (_ @t294 @t176)) % 0.47/0.90 (define @t310 () (=> (_ @t295 @t176) @t309)) % 0.47/0.90 (define @t311 () (_ @t254 @t62)) % 0.47/0.90 (define @t312 () (=> @t260 @t311)) % 0.47/0.90 (define @t313 () (_ @t255 @t78)) % 0.47/0.90 (define @t314 () (=> @t270 @t313)) % 0.47/0.90 (define @t315 () (_ @t224 @t98)) % 0.47/0.90 (define @t316 () (= @t298 @t195)) % 0.47/0.90 (define @t317 () (@var "P" Bool)) % 0.47/0.90 (define @t318 () (@var "M" tptp.nat)) % 0.47/0.90 (define @t319 () (@var "P3" (-> tptp.nat Bool))) % 0.47/0.90 (define @t320 () (@var "N" tptp.nat)) % 0.47/0.90 (define @t321 () (@list @t318)) % 0.47/0.90 (define @t322 () (@var "X5" tptp.nat)) % 0.47/0.90 (define @t323 () (@var "P2" (-> tptp.nat Bool))) % 0.47/0.90 (define @t324 () (_ tptp.ord_le1310584031lle_hf @t62)) % 0.47/0.90 (define @t325 () (_ @t324 @t2)) % 0.47/0.90 (define @t326 () (=> (_ @t324 @t1) @t325)) % 0.47/0.90 (define @t327 () (_ tptp.ord_less_nat @t78)) % 0.47/0.90 (define @t328 () (_ @t327 @t98)) % 0.47/0.90 (define @t329 () (=> (_ @t327 @t89) @t328)) % 0.47/0.90 (define @t330 () (not @t3)) % 0.47/0.90 (define @t331 () (not @t135)) % 0.47/0.90 (define @t332 () (@var "B6" tptp.nat)) % 0.47/0.90 (define @t333 () (@var "A6" tptp.nat)) % 0.47/0.90 (define @t334 () (not @t303)) % 0.47/0.90 (define @t335 () (= @t9 @t43)) % 0.47/0.90 (define @t336 () (= @t208 @t209)) % 0.47/0.90 (define @t337 () (= @t11 @t8)) % 0.47/0.90 (define @t338 () (= @t148 @t147)) % 0.47/0.90 (define @t339 () (not @t337)) % 0.47/0.90 (define @t340 () (not @t338)) % 0.47/0.90 (define @t341 () (@list @t8 @t11)) % 0.47/0.90 (define @t342 () (@list @t147 @t148)) % 0.47/0.90 (define @t343 () (@var "G" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t344 () (@var "X6" tptp.nat)) % 0.47/0.90 (define @t345 () (@var "T" tptp.nat)) % 0.47/0.90 (define @t346 () (_ (_ tptp.ord_less_eq_nat @t345) @t344)) % 0.47/0.90 (define @t347 () (@var "Z2" tptp.nat)) % 0.47/0.90 (define @t348 () (_ tptp.ord_less_nat @t344)) % 0.47/0.90 (define @t349 () (_ @t348 @t347)) % 0.47/0.90 (define @t350 () (@list @t344)) % 0.47/0.90 (define @t351 () (@list @t347)) % 0.47/0.90 (define @t352 () (@list @t345)) % 0.47/0.90 (define @t353 () (_ (_ tptp.ord_less_eq_nat @t344) @t345)) % 0.47/0.90 (define @t354 () (_ (_ tptp.ord_less_nat @t347) @t344)) % 0.47/0.90 (define @t355 () (@var "C2" tptp.nat)) % 0.47/0.90 (define @t356 () (@var "D" tptp.nat)) % 0.47/0.90 (define @t357 () (_ @t99 @t83)) % 0.47/0.90 (define @t358 () (_ @t224 @t344)) % 0.47/0.90 (define @t359 () (_ tptp.hF_Mirabelle_hfset @t2)) % 0.47/0.90 (define @t360 () (_ (_ tptp.ord_less_nat @t345) @t344)) % 0.47/0.90 (define @t361 () (_ @t348 @t345)) % 0.47/0.90 (define @t362 () (not (= @t344 @t345))) % 0.47/0.90 (define @t363 () (@var "Q2" (-> tptp.nat Bool))) % 0.47/0.90 (define @t364 () (_ @t363 @t344)) % 0.47/0.90 (define @t365 () (@var "P4" (-> tptp.nat Bool))) % 0.47/0.90 (define @t366 () (_ @t365 @t344)) % 0.47/0.90 (define @t367 () (_ @t230 @t344)) % 0.47/0.90 (define @t368 () (= (or @t358 @t367) (or @t366 @t364))) % 0.47/0.90 (define @t369 () (= @t231 (_ @t363 @t83))) % 0.47/0.90 (define @t370 () (@var "Z4" tptp.nat)) % 0.47/0.90 (define @t371 () (_ @t266 @t370)) % 0.47/0.90 (define @t372 () (@list @t370)) % 0.47/0.90 (define @t373 () (exists @t372 (forall @t236 (=> @t371 @t369)))) % 0.47/0.90 (define @t374 () (= @t235 (_ @t365 @t83))) % 0.47/0.90 (define @t375 () (exists @t372 (forall @t236 (=> @t371 @t374)))) % 0.47/0.90 (define @t376 () (@list @t224 @t365 @t230 @t363)) % 0.47/0.90 (define @t377 () (= (and @t358 @t367) (and @t366 @t364))) % 0.47/0.90 (define @t378 () (_ (_ tptp.ord_less_nat @t370) @t83)) % 0.47/0.90 (define @t379 () (exists @t372 (forall @t236 (=> @t378 @t369)))) % 0.47/0.90 (define @t380 () (exists @t372 (forall @t236 (=> @t378 @t374)))) % 0.47/0.90 (define @t381 () (_ tptp.hF_Mirabelle_HF @t241)) % 0.47/0.90 (define @t382 () (_ tptp.finite586181922lle_hf @t241)) % 0.47/0.90 (define @t383 () (@var "Xa" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t384 () (= @t4 @t383)) % 0.47/0.90 (define @t385 () (_ (_ tptp.member1367349282lle_hf @t383) @t241)) % 0.47/0.90 (define @t386 () (@list @t383)) % 0.47/0.90 (define @t387 () (_ (_ tptp.member1367349282lle_hf @t4) @t241)) % 0.47/0.90 (define @t388 () (_ @t237 @t241)) % 0.47/0.90 (define @t389 () (@list @t241 @t2)) % 0.47/0.90 (define @t390 () (@var "Xa" tptp.nat)) % 0.47/0.90 (define @t391 () (= @t83 @t390)) % 0.47/0.90 (define @t392 () (@var "A4" tptp.set_nat)) % 0.47/0.90 (define @t393 () (_ (_ tptp.member_nat @t390) @t392)) % 0.47/0.90 (define @t394 () (@list @t390)) % 0.47/0.90 (define @t395 () (_ tptp.member_nat @t83)) % 0.47/0.90 (define @t396 () (_ @t395 @t392)) % 0.47/0.90 (define @t397 () (_ (_ tptp.member_nat @t98) @t392)) % 0.47/0.90 (define @t398 () (_ tptp.finite_finite_nat @t392)) % 0.47/0.90 (define @t399 () (@list @t392 @t98)) % 0.47/0.90 (define @t400 () (@var "B4" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t401 () (_ tptp.finite586181922lle_hf @t400)) % 0.47/0.90 (define @t402 () (_ tptp.ord_le432112161lle_hf @t241)) % 0.47/0.90 (define @t403 () (_ @t402 @t400)) % 0.47/0.90 (define @t404 () (@list @t241 @t400)) % 0.47/0.90 (define @t405 () (@var "B4" tptp.set_nat)) % 0.47/0.90 (define @t406 () (_ tptp.finite_finite_nat @t405)) % 0.47/0.90 (define @t407 () (=> @t406 @t398)) % 0.47/0.90 (define @t408 () (_ tptp.ord_less_eq_set_nat @t392)) % 0.47/0.90 (define @t409 () (_ @t408 @t405)) % 0.47/0.90 (define @t410 () (@list @t392 @t405)) % 0.47/0.90 (define @t411 () (@var "T2" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t412 () (@var "S" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t413 () (@var "T2" tptp.set_nat)) % 0.47/0.90 (define @t414 () (@var "S" tptp.set_nat)) % 0.47/0.90 (define @t415 () (@list @t400 @t241)) % 0.47/0.90 (define @t416 () (@list @t405 @t392)) % 0.47/0.90 (define @t417 () (@var "A7" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t418 () (@var "B7" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t419 () (@var "P" (-> tptp.set_nat Bool))) % 0.47/0.90 (define @t420 () (@var "A7" tptp.set_nat)) % 0.47/0.90 (define @t421 () (@var "B7" tptp.set_nat)) % 0.47/0.90 (define @t422 () (_ (_ tptp.ord_le1344122901lle_hf @t241) @t400)) % 0.47/0.90 (define @t423 () (_ tptp.finite1213132899lle_hf @t400)) % 0.47/0.90 (define @t424 () (_ tptp.finite1213132899lle_hf @t241)) % 0.47/0.90 (define @t425 () (_ (_ tptp.ord_less_nat @t424) @t423)) % 0.47/0.90 (define @t426 () (_ (_ tptp.ord_less_set_nat @t392) @t405)) % 0.47/0.90 (define @t427 () (_ tptp.finite_card_nat @t405)) % 0.47/0.90 (define @t428 () (_ tptp.finite_card_nat @t392)) % 0.47/0.90 (define @t429 () (_ (_ tptp.ord_less_nat @t428) @t427)) % 0.47/0.90 (define @t430 () (_ tptp.ord_less_eq_nat @t424)) % 0.47/0.90 (define @t431 () (_ @t430 @t423)) % 0.47/0.90 (define @t432 () (_ tptp.ord_less_eq_nat @t428)) % 0.47/0.90 (define @t433 () (_ @t432 @t427)) % 0.47/0.90 (define @t434 () (= @t241 @t400)) % 0.47/0.90 (define @t435 () (= @t392 @t405)) % 0.47/0.90 (define @t436 () (@var "B8" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t437 () (@var "N2" tptp.nat)) % 0.47/0.90 (define @t438 () (@var "B8" tptp.set_nat)) % 0.47/0.90 (define @t439 () (@var "C3" tptp.nat)) % 0.47/0.90 (define @t440 () (@var "F3" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t441 () (_ tptp.finite586181922lle_hf @t440)) % 0.47/0.90 (define @t442 () (@var "G2" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t443 () (@var "F3" tptp.set_nat)) % 0.47/0.90 (define @t444 () (_ tptp.finite_finite_nat @t443)) % 0.47/0.90 (define @t445 () (@var "G2" tptp.set_nat)) % 0.47/0.90 (define @t446 () (@var "T3" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t447 () (_ tptp.ord_less_eq_nat @t437)) % 0.47/0.90 (define @t448 () (@var "T3" tptp.set_nat)) % 0.47/0.90 (define @t449 () (@var "F" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t450 () (_ (_ tptp.inj_on811196232lle_hf @t449) @t244)) % 0.47/0.90 (define @t451 () (@var "Y4" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t452 () (_ (_ tptp.member1490636632lle_hf @t451) @t244)) % 0.47/0.90 (define @t453 () (_ (_ tptp.member1490636632lle_hf @t247) @t244)) % 0.47/0.90 (define @t454 () (@list @t247 @t451)) % 0.47/0.90 (define @t455 () (@var "A22" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t456 () (@var "A1" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t457 () (= @t456 @t455)) % 0.47/0.90 (define @t458 () (@var "B5" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t459 () (@var "R2" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.47/0.90 (define @t460 () (_ (_ tptp.member1367349282lle_hf @t455) @t241)) % 0.47/0.90 (define @t461 () (_ (_ tptp.member1367349282lle_hf @t456) @t241)) % 0.47/0.90 (define @t462 () (@var "B9" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t463 () (@var "A5" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t464 () (_ (_ tptp.member1367349282lle_hf @t463) @t241)) % 0.47/0.90 (define @t465 () (@list @t463)) % 0.47/0.90 (define @t466 () (_ @t430 @t427)) % 0.47/0.90 (define @t467 () (@var "R2" (-> tptp.hF_Mirabelle_hf tptp.nat Bool))) % 0.47/0.90 (define @t468 () (@var "B9" tptp.nat)) % 0.47/0.90 (define @t469 () (@var "N4" tptp.set_nat)) % 0.47/0.90 (define @t470 () (_ tptp.ord_less_nat @t208)) % 0.47/0.90 (define @t471 () (@var "N3" tptp.set_nat)) % 0.47/0.90 (define @t472 () (_ (_ tptp.member_nat @t208) @t471)) % 0.47/0.90 (define @t473 () (@list @t208)) % 0.47/0.90 (define @t474 () (@list @t471)) % 0.47/0.90 (define @t475 () (@var "F4" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t476 () (_ tptp.finite90088345lle_hf @t244)) % 0.47/0.90 (define @t477 () (_ (_ tptp.ord_less_eq_nat @t476) @t423)) % 0.47/0.90 (define @t478 () (_ tptp.finite1450550360lle_hf @t244)) % 0.47/0.90 (define @t479 () (@var "F4" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t480 () (@var "F4" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 0.47/0.90 (define @t481 () (@var "F4" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t482 () (@var "F4" (-> tptp.nat tptp.nat))) % 0.47/0.90 (define @t483 () (_ (_ tptp.image_899003828lle_hf @t449) @t244)) % 0.47/0.90 (define @t484 () (@var "H" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t485 () (@var "H" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 0.47/0.90 (define @t486 () (@var "H" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t487 () (@var "H" (-> tptp.nat tptp.nat))) % 0.47/0.90 (define @t488 () (@var "B3" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t489 () (_ tptp.image_1743964010lle_hf @t48)) % 0.47/0.90 (define @t490 () (_ @t239 (_ @t489 @t488))) % 0.47/0.90 (define @t491 () (_ tptp.ord_le432112161lle_hf @t488)) % 0.47/0.90 (define @t492 () (_ @t491 @t241)) % 0.47/0.90 (define @t493 () (_ tptp.finite586181922lle_hf @t488)) % 0.47/0.90 (define @t494 () (and @t493 @t492)) % 0.47/0.90 (define @t495 () (@list @t488)) % 0.47/0.90 (define @t496 () (_ @t239 @t488)) % 0.47/0.90 (define @t497 () (_ @t489 @t241)) % 0.47/0.90 (define @t498 () (_ @t491 @t497)) % 0.47/0.90 (define @t499 () (@list @t48 @t241 @t239)) % 0.47/0.90 (define @t500 () (@var "B3" tptp.set_nat)) % 0.47/0.90 (define @t501 () (_ tptp.image_246164834lle_hf @t79)) % 0.47/0.90 (define @t502 () (_ @t239 (_ @t501 @t500))) % 0.47/0.90 (define @t503 () (_ tptp.ord_less_eq_set_nat @t500)) % 0.47/0.90 (define @t504 () (_ @t503 @t392)) % 0.47/0.90 (define @t505 () (_ tptp.finite_finite_nat @t500)) % 0.47/0.90 (define @t506 () (and @t505 @t504)) % 0.47/0.90 (define @t507 () (@list @t500)) % 0.47/0.90 (define @t508 () (_ @t501 @t392)) % 0.47/0.90 (define @t509 () (_ @t491 @t508)) % 0.47/0.90 (define @t510 () (@list @t79 @t392 @t239)) % 0.47/0.90 (define @t511 () (_ tptp.image_131453538hf_nat @t96)) % 0.47/0.90 (define @t512 () (_ @t419 (_ @t511 @t488))) % 0.47/0.90 (define @t513 () (_ @t419 @t500)) % 0.47/0.90 (define @t514 () (_ @t511 @t241)) % 0.47/0.90 (define @t515 () (_ @t503 @t514)) % 0.47/0.90 (define @t516 () (@list @t96 @t241 @t419)) % 0.47/0.90 (define @t517 () (_ tptp.image_nat_nat @t107)) % 0.47/0.90 (define @t518 () (_ @t419 (_ @t517 @t500))) % 0.47/0.90 (define @t519 () (_ @t517 @t392)) % 0.47/0.90 (define @t520 () (_ @t503 @t519)) % 0.47/0.90 (define @t521 () (@list @t107 @t392 @t419)) % 0.47/0.90 (define @t522 () (@var "C4" tptp.set_HF_Mirabelle_hf)) % 0.47/0.90 (define @t523 () (_ tptp.finite586181922lle_hf @t522)) % 0.47/0.90 (define @t524 () (_ (_ tptp.ord_le432112161lle_hf @t522) @t241)) % 0.47/0.90 (define @t525 () (@list @t522)) % 0.47/0.90 (define @t526 () (_ tptp.ord_le432112161lle_hf @t400)) % 0.47/0.90 (define @t527 () (_ @t526 @t497)) % 0.47/0.90 (define @t528 () (@var "C4" tptp.set_nat)) % 0.47/0.90 (define @t529 () (_ tptp.finite_finite_nat @t528)) % 0.47/0.90 (define @t530 () (_ (_ tptp.ord_less_eq_set_nat @t528) @t392)) % 0.47/0.90 (define @t531 () (@list @t528)) % 0.47/0.90 (define @t532 () (_ @t526 @t508)) % 0.47/0.90 (define @t533 () (_ tptp.ord_less_eq_set_nat @t405)) % 0.47/0.90 (define @t534 () (_ @t533 @t514)) % 0.47/0.90 (define @t535 () (_ @t533 @t519)) % 0.47/0.90 (define @t536 () (_ tptp.finite586181922lle_hf @t483)) % 0.47/0.90 (define @t537 () (@list @t449 @t244)) % 0.47/0.90 (define @t538 () (_ tptp.finite586181922lle_hf @t497)) % 0.47/0.90 (define @t539 () (_ (_ tptp.inj_on755450110lle_hf @t48) @t241)) % 0.47/0.90 (define @t540 () (@list @t48 @t241)) % 0.47/0.90 (define @t541 () (_ tptp.finite586181922lle_hf @t508)) % 0.47/0.90 (define @t542 () (_ (_ tptp.inj_on1988990670lle_hf @t79) @t392)) % 0.47/0.90 (define @t543 () (@list @t79 @t392)) % 0.47/0.90 (define @t544 () (_ tptp.finite_finite_nat @t514)) % 0.47/0.90 (define @t545 () (_ (_ tptp.inj_on1874279374hf_nat @t96) @t241)) % 0.47/0.90 (define @t546 () (@list @t96 @t241)) % 0.47/0.90 (define @t547 () (_ tptp.finite_finite_nat @t519)) % 0.47/0.90 (define @t548 () (_ (_ tptp.inj_on_nat_nat @t107) @t392)) % 0.47/0.90 (define @t549 () (@list @t107 @t392)) % 0.47/0.90 (define @t550 () (@var "U4" tptp.nat)) % 0.47/0.90 (define @t551 () (@var "L" tptp.nat)) % 0.47/0.90 (define @t552 () (_ tptp.ord_less_nat tptp.zero_zero_nat)) % 0.47/0.90 (define @t553 () (= @t98 tptp.zero_zero_nat)) % 0.47/0.90 (define @t554 () (@list @t437)) % 0.47/0.90 (define @t555 () (_ @t552 @t437)) % 0.47/0.90 (define @t556 () (= @t437 tptp.zero_zero_nat)) % 0.47/0.90 (define @t557 () (not @t556)) % 0.47/0.90 (define @t558 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 0.47/0.90 (define @t559 () (_ @t99 tptp.zero_zero_nat)) % 0.47/0.90 (define @t560 () (@var "K" tptp.nat)) % 0.47/0.90 (define @t561 () (@var "I" tptp.nat)) % 0.47/0.90 (define @t562 () (_ @t224 tptp.zero_zero_nat)) % 0.47/0.90 (define @t563 () (_ @t224 @t437)) % 0.47/0.90 (define @t564 () (@list @t224 @t437)) % 0.47/0.90 (define @t565 () (@var "M2" tptp.nat)) % 0.47/0.90 (define @t566 () (@var "N5" tptp.nat)) % 0.47/0.90 (define @t567 () (@var "M3" tptp.nat)) % 0.47/0.90 (define @t568 () (@var "X6" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t569 () (_ tptp.hF_Mirabelle_hmem @t568)) % 0.47/0.90 (define @t570 () (=> (_ @t569 tptp.a) (_ @t569 tptp.b))) % 0.47/0.90 (define @t571 () (@list @t568)) % 0.47/0.90 (define @t572 () (forall @t571 @t570)) % 0.47/0.90 (define @t573 () (not (_ (_ tptp.ord_le976219883lle_hf tptp.a) tptp.b))) % 0.47/0.90 (define @t574 () (@var "B3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t575 () (_ @t10 @t574)) % 0.47/0.90 (define @t576 () (@var "A3" tptp.hF_Mirabelle_hf)) % 0.47/0.90 (define @t577 () (_ @t10 @t576)) % 0.47/0.90 (define @t578 () (forall @t12 (=> @t577 @t575))) % 0.47/0.90 (define @t579 () (@list @t576 @t574)) % 0.47/0.90 (define @t580 () (lambda @t579 @t578)) % 0.47/0.90 (define @t581 () (@var "Y6" (-> Bool tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t582 () (@var "X4" (-> Bool tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t583 () (lambda (@list @t582 @t581) (and (_ (_ tptp.ord_le976219883lle_hf (_ @t582 false)) (_ @t581 false)) (_ (_ tptp.ord_le976219883lle_hf (_ @t582 true)) (_ @t581 true))))) % 0.47/0.90 (define @t584 () (@var "Y6" (-> Bool tptp.nat))) % 0.47/0.90 (define @t585 () (@var "X4" (-> Bool tptp.nat))) % 0.47/0.90 (define @t586 () (lambda (@list @t585 @t584) (and (_ (_ tptp.ord_less_eq_nat (_ @t585 false)) (_ @t584 false)) (_ (_ tptp.ord_less_eq_nat (_ @t585 true)) (_ @t584 true))))) % 0.47/0.90 (define @t587 () (_ tptp.hF_Mirabelle_hfset @t8)) % 0.47/0.90 (define @t588 () (lambda @t13 (_ (_ tptp.member1367349282lle_hf @t11) @t587))) % 0.47/0.90 (define @t589 () (lambda @t579 (and (_ (_ tptp.ord_le976219883lle_hf @t576) @t574) (not (= @t576 @t574))))) % 0.47/0.90 (define @t590 () (@var "F2" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t591 () (lambda (@list @t590) (forall @t207 (=> @t206 (_ (_ tptp.ord_le976219883lle_hf (_ @t590 @t43)) (_ @t590 @t9)))))) % 0.47/0.90 (define @t592 () (@var "F2" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 0.47/0.90 (define @t593 () (lambda (@list @t592) (forall @t207 (=> @t206 (_ (_ tptp.ord_less_eq_nat (_ @t592 @t43)) (_ @t592 @t9)))))) % 0.47/0.90 (define @t594 () (@var "F2" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 0.47/0.90 (define @t595 () (lambda (@list @t594) (forall @t213 (=> @t212 (_ (_ tptp.ord_le976219883lle_hf (_ @t594 @t209)) (_ @t594 @t208)))))) % 0.47/0.90 (define @t596 () (@var "F2" (-> tptp.nat tptp.nat))) % 0.47/0.90 (define @t597 () (lambda (@list @t596) (forall @t213 (=> @t212 (_ (_ tptp.ord_less_eq_nat (_ @t596 @t209)) (_ @t596 @t208)))))) % 0.47/0.90 (define @t598 () (lambda @t213 (or (_ @t470 @t209) @t336))) % 0.47/0.90 (define @t599 () (lambda @t474 (exists @t321 (forall @t473 (=> @t472 (_ @t211 @t318)))))) % 0.47/0.90 (define @t600 () (_ tptp.hF_Mirabelle_hfset tptp.b)) % 0.47/0.90 (define @t601 () (tptp.hF_Mirabelle_hfset tptp.b)) % 0.47/0.90 (define @t602 () (tptp.member1367349282lle_hf @t568 @t601)) % 0.47/0.90 (define @t603 () (_ tptp.member1367349282lle_hf @t568)) % 0.47/0.90 (define @t604 () (_ @t603 @t600)) % 0.47/0.90 (define @t605 () (_ tptp.hF_Mirabelle_hfset tptp.a)) % 0.47/0.90 (define @t606 () (tptp.hF_Mirabelle_hfset tptp.a)) % 0.47/0.90 (define @t607 () (tptp.member1367349282lle_hf @t568 @t606)) % 0.47/0.90 (define @t608 () (_ @t603 @t605)) % 0.47/0.90 (define @t609 () (not @t608)) % 0.47/0.90 (define @t610 () (or @t609 @t604)) % 0.47/0.90 (define @t611 () (lambda (@list @t8) (_ @t603 @t587))) % 0.47/0.90 (define @t612 () (_ @t588 @t568)) % 0.47/0.90 (define @t613 () (=> (_ @t612 tptp.a) (_ @t612 tptp.b))) % 0.47/0.90 (define @t614 () (forall @t571 (or (not @t607) @t602))) % 0.47/0.90 (define @t615 () (not (tptp.member1367349282lle_hf @t9 @t606))) % 0.47/0.90 (define @t616 () (forall @t12 (or @t615 (tptp.member1367349282lle_hf @t9 @t601)))) % 0.47/0.90 (define @t617 () (@list false)) % 0.47/0.90 (define @t618 () (tptp.hF_Mirabelle_hfset @t574)) % 0.47/0.90 (define @t619 () (tptp.member1367349282lle_hf @t9 @t618)) % 0.47/0.90 (define @t620 () (lambda (@list @t574) (forall @t12 (or @t615 @t619)))) % 0.47/0.90 (define @t621 () (tptp.hF_Mirabelle_hfset @t576)) % 0.47/0.90 (define @t622 () (tptp.member1367349282lle_hf @t9 @t621)) % 0.47/0.90 (define @t623 () (_ tptp.hF_Mirabelle_hfset @t574)) % 0.47/0.90 (define @t624 () (_ @t242 @t623)) % 0.47/0.90 (define @t625 () (_ tptp.hF_Mirabelle_hfset @t576)) % 0.47/0.90 (define @t626 () (_ @t242 @t625)) % 0.47/0.90 (define @t627 () (not @t626)) % 0.47/0.90 (define @t628 () (or @t627 @t624)) % 0.47/0.90 (define @t629 () (_ @t588 @t9 @t574)) % 0.47/0.90 (define @t630 () (_ @t588 @t9 @t576)) % 0.47/0.90 (define @t631 () (not @t630)) % 0.47/0.90 (define @t632 () (or @t631 @t629)) % 0.47/0.90 (define @t633 () (forall @t12 @t632)) % 0.47/0.90 (define @t634 () (lambda @t579 @t633)) % 0.47/0.90 (define @t635 () (tptp.hF_Mirabelle_hmem @t9 @t576)) % 0.47/0.90 (define @t636 () (not @t635)) % 0.47/0.90 (define @t637 () (tptp.hF_Mirabelle_hmem @t9 @t574)) % 0.47/0.90 (define @t638 () (or @t636 @t637)) % 0.47/0.90 (define @t639 () (forall @t12 @t638)) % 0.47/0.90 (define @t640 () (not @t577)) % 0.47/0.90 (define @t641 () (or @t640 @t575)) % 0.47/0.90 (assume @p1 (forall @t7 (=> (forall @t6 (= (_ @t5 @t2) (_ @t5 @t1))) @t3))) % 0.47/0.90 (assume @p2 (= @t16 (lambda @t13 (forall @t12 (= (_ @t10 @t11) (_ @t10 @t8)))))) % 0.47/0.90 (assume @p3 (forall (@list @t21 @t19) (=> (forall @t35 (=> (_ @t34 @t21) @t33)) (exists @t28 (forall @t27 (= @t26 (exists @t24 (and @t23 (_ @t20 @t17))))))))) % 0.47/0.90 (assume @p4 (forall @t42 (exists @t28 (forall @t41 (= @t40 (or @t39 (_ @t38 @t36))))))) % 0.47/0.90 (assume @p5 (forall @t46 (exists @t28 (forall @t41 (= @t40 (exists @t45 (and (_ @t44 @t21) (_ @t38 @t43)))))))) % 0.47/0.90 (assume @p6 (forall (@list @t21 @t47) (exists @t28 (forall @t41 (= @t40 (and @t39 (_ @t47 @t37))))))) % 0.47/0.90 (assume @p7 (forall (@list @t21 @t48) (exists @t28 (forall @t27 (= @t26 (exists @t24 (and @t23 (= @t17 @t49)))))))) % 0.47/0.90 (assume @p8 (forall @t46 (_ @t50 @t21))) % 0.47/0.90 (assume @p9 (forall @t53 (_ @t52 @t51))) % 0.47/0.90 (assume @p10 (forall (@list @t56 @t19 @t54) (=> (forall @t35 (=> (_ @t34 @t56) @t33)) (= (_ @t58 (_ (_ tptp.hF_Mir1248913145eplace @t56) @t19)) (exists @t24 (and @t57 @t55)))))) % 0.47/0.90 (assume @p11 (forall (@list @t21 @t47 @t56) (= (_ @t59 (_ (_ tptp.hF_Mir818139703ollect @t47) @t56)) (and @t60 (_ @t59 @t56))))) % 0.47/0.90 (assume @p12 (forall (@list @t21 @t56) (= (_ @t59 (_ tptp.hF_Mirabelle_HUnion @t56)) (exists @t45 (and (_ @t44 @t56) (_ @t59 @t43)))))) % 0.47/0.90 (assume @p13 (forall (@list @t54 @t56 @t19) (= (_ @t58 (_ @t61 @t19)) (exists @t24 (and @t57 @t55 (forall @t45 (=> (_ @t20 @t43) (= @t43 @t54)))))))) % 0.47/0.90 (assume @p14 (forall @t77 (=> @t76 @t74))) % 0.47/0.90 (assume @p15 (forall @t95 (=> @t94 @t92))) % 0.47/0.90 (assume @p16 (forall @t106 (=> @t105 @t103))) % 0.47/0.90 (assume @p17 (forall @t115 (=> @t114 @t112))) % 0.47/0.90 (assume @p18 (forall @t120 (=> @t119 (=> @t118 @t117)))) % 0.47/0.90 (assume @p19 (forall @t124 (=> @t119 (=> @t123 @t122)))) % 0.47/0.90 (assume @p20 (forall @t129 (=> @t128 (=> @t127 @t126)))) % 0.47/0.90 (assume @p21 (forall @t133 (=> @t128 (=> @t132 @t131)))) % 0.47/0.90 (assume @p22 (forall @t136 (or @t135 (not @t128) (not @t134)))) % 0.47/0.90 (assume @p23 (forall (@list @t56 @t138 @t139 @t137) (=> @t141 (=> (forall @t70 (=> @t140 (= (_ (_ @t139 @t4) @t65) (_ (_ @t137 @t4) @t65)))) (= (_ @t61 @t139) (_ (_ tptp.hF_Mirabelle_Replace @t138) @t137)))))) % 0.47/0.90 (assume @p24 (forall @t143 (=> @t142 (=> @t119 @t3)))) % 0.47/0.90 (assume @p25 (forall @t144 (=> @t134 (=> @t128 @t135)))) % 0.47/0.90 (assume @p26 (= @t16 (lambda @t13 (and @t146 @t145)))) % 0.47/0.90 (assume @p27 (= @t154 (lambda @t151 (and @t150 @t149)))) % 0.47/0.90 (assume @p28 (forall @t157 (=> @t142 (=> @t156 (_ @t155 @t2))))) % 0.47/0.90 (assume @p29 (forall @t160 (=> @t134 (=> @t159 (_ @t158 @t98))))) % 0.47/0.90 (assume @p30 (forall @t168 (=> (forall @t166 (=> (_ (_ tptp.ord_less_eq_nat @t163) @t162) @t165)) @t167))) % 0.47/0.90 (assume @p31 (forall @t169 (_ @t64 @t2))) % 0.47/0.90 (assume @p32 (forall @t170 (_ @t99 @t98))) % 0.47/0.90 (assume @p33 (forall @t175 (=> @t174 (=> @t173 (_ @t50 @t171))))) % 0.47/0.90 (assume @p34 (forall @t182 (=> @t181 (=> @t180 @t177)))) % 0.47/0.90 (assume @p35 (forall @t7 (=> @t119 (=> @t142 @t3)))) % 0.47/0.90 (assume @p36 (forall @t136 (=> @t128 (=> @t134 @t135)))) % 0.47/0.90 (assume @p37 (forall @t185 (=> @t119 (=> @t184 @t183)))) % 0.47/0.90 (assume @p38 (forall @t188 (=> @t128 (=> @t187 @t186)))) % 0.47/0.90 (assume @p39 (forall @t185 (=> @t3 @t189))) % 0.47/0.90 (assume @p40 (forall @t188 (=> @t135 @t190))) % 0.47/0.90 (assume @p41 (= @t16 (lambda @t13 (and @t145 @t146)))) % 0.47/0.90 (assume @p42 (= @t154 (lambda @t151 (and @t149 @t150)))) % 0.47/0.90 (assume @p43 (forall @t194 (=> @t193 @t192))) % 0.47/0.90 (assume @p44 (forall @t198 (=> @t197 @t196))) % 0.47/0.90 (assume @p45 (forall @t182 (=> (=> @t181 (not @t180)) (=> (=> @t197 (not @t177)) (=> (=> @t177 (not @t203)) (=> (=> @t203 @t202) (=> (=> @t180 (not @t201)) (not (=> @t201 @t199))))))))) % 0.47/0.90 (assume @p46 (forall @t185 (=> @t119 @t189))) % 0.47/0.90 (assume @p47 (forall @t188 (=> @t128 @t190))) % 0.47/0.90 (assume @p48 (forall @t204 (=> @t199 @t197))) % 0.47/0.90 (assume @p49 (forall @t42 (=> @t191 @t174))) % 0.47/0.90 (assume @p50 (forall @t204 (=> @t195 @t181))) % 0.47/0.90 (assume @p51 (forall @t204 (or @t181 @t197))) % 0.47/0.90 (assume @p52 (forall @t42 (=> @t174 (=> @t193 @t191)))) % 0.47/0.90 (assume @p53 (forall @t204 (=> @t181 (=> @t197 @t195)))) % 0.47/0.90 (assume @p54 (= @t16 (lambda @t207 (and @t206 @t205)))) % 0.47/0.90 (assume @p55 (= @t154 (lambda @t213 (and @t212 @t210)))) % 0.47/0.90 (assume @p56 (forall @t120 (=> @t119 (=> @t214 @t117)))) % 0.47/0.90 (assume @p57 (forall @t124 (=> @t119 (=> @t215 @t122)))) % 0.47/0.90 (assume @p58 (forall @t129 (=> @t128 (=> @t216 @t126)))) % 0.47/0.90 (assume @p59 (forall @t133 (=> @t128 (=> @t217 @t131)))) % 0.47/0.90 (assume @p60 (forall @t77 (=> @t218 @t74))) % 0.47/0.90 (assume @p61 (forall @t106 (=> @t219 @t103))) % 0.47/0.90 (assume @p62 (forall @t95 (=> @t220 @t92))) % 0.47/0.90 (assume @p63 (forall @t115 (=> @t221 @t112))) % 0.47/0.90 (assume @p64 (forall (@list @t47 @t21) (=> @t60 (=> @t223 (= @t222 @t21))))) % 0.47/0.90 (assume @p65 (forall (@list @t224 @t51) (=> @t227 (=> @t226 (= @t225 @t51))))) % 0.47/0.90 (assume @p66 (forall (@list @t47 @t21 @t228) (=> @t60 (=> @t223 (=> (forall @t6 (=> (_ @t47 @t4) (=> (forall (@list @t229) (=> (_ @t47 @t229) (_ (_ tptp.ord_le976219883lle_hf @t229) @t4))) (_ @t228 @t4)))) (_ @t228 @t222)))))) % 0.47/0.90 (assume @p67 (forall (@list @t224 @t51 @t230) (=> @t227 (=> @t226 (=> (forall @t236 (=> @t235 (=> (forall @t234 (=> @t233 (_ (_ tptp.ord_less_eq_nat @t232) @t83))) @t231))) (_ @t230 @t225)))))) % 0.47/0.90 (assume @p68 (forall (@list @t2 @t47) (= (_ @t237 (_ tptp.collec2046588256lle_hf @t47)) (_ @t47 @t2)))) % 0.47/0.90 (assume @p69 (forall (@list @t238 @t239) (= (_ (_ tptp.member1490636632lle_hf @t238) @t240) (_ @t239 @t238)))) % 0.47/0.90 (assume @p70 (forall @t243 (= (_ tptp.collec2046588256lle_hf (lambda @t12 (_ @t242 @t241))) @t241))) % 0.47/0.90 (assume @p71 (forall (@list @t244) (= (_ tptp.collec1758573718lle_hf (lambda (@list @t245) (_ (_ tptp.member1490636632lle_hf @t245) @t244))) @t244))) % 0.47/0.90 (assume @p72 (forall (@list @t239 @t246) (=> (forall (@list @t247) (= (_ @t239 @t247) (_ @t246 @t247))) (= @t240 (_ tptp.collec1758573718lle_hf @t246))))) % 0.47/0.90 (assume @p73 (forall (@list @t54 @t56 @t48) (= (_ @t58 @t248) (exists @t24 (and @t57 (= @t54 @t49)))))) % 0.47/0.90 (assume @p74 (forall @t250 (=> (forall @t70 (=> @t69 (_ (_ tptp.ord_le976219883lle_hf @t66) @t67))) @t249))) % 0.47/0.90 (assume @p75 (forall (@list @t96) (=> (forall @t70 (=> @t69 (_ (_ tptp.ord_less_eq_nat @t100) @t101))) @t251))) % 0.47/0.90 (assume @p76 (forall (@list @t79) (=> (forall @t87 (=> @t86 (_ (_ tptp.ord_le976219883lle_hf @t82) @t84))) @t252))) % 0.47/0.90 (assume @p77 (forall (@list @t107) (=> (forall @t87 (=> @t86 (_ (_ tptp.ord_less_eq_nat @t109) @t110))) @t253))) % 0.47/0.90 (assume @p78 (forall (@list @t48 @t21 @t36) (=> @t249 (=> @t174 (_ (_ tptp.ord_le976219883lle_hf (_ @t48 @t36)) (_ @t48 @t21)))))) % 0.47/0.90 (assume @p79 (forall (@list @t96 @t21 @t36) (=> @t251 (=> @t174 (_ (_ tptp.ord_less_eq_nat (_ @t96 @t36)) (_ @t96 @t21)))))) % 0.47/0.90 (assume @p80 (forall (@list @t79 @t51 @t178) (=> @t252 (=> @t181 (_ (_ tptp.ord_le976219883lle_hf (_ @t79 @t178)) (_ @t79 @t51)))))) % 0.47/0.90 (assume @p81 (forall (@list @t107 @t51 @t178) (=> @t253 (=> @t181 (_ (_ tptp.ord_less_eq_nat (_ @t107 @t178)) (_ @t107 @t51)))))) % 0.47/0.90 (assume @p82 (forall @t169 (not (_ @t254 @t2)))) % 0.47/0.90 (assume @p83 (forall @t170 (not (_ @t255 @t98)))) % 0.47/0.90 (assume @p84 (forall @t77 (=> @t218 @t261))) % 0.47/0.90 (assume @p85 (forall @t106 (=> @t219 @t264))) % 0.47/0.90 (assume @p86 (forall @t95 (=> @t220 @t271))) % 0.47/0.90 (assume @p87 (forall @t115 (=> @t221 @t274))) % 0.47/0.90 (assume @p88 (forall @t120 (=> @t277 (=> @t214 @t276)))) % 0.47/0.90 (assume @p89 (forall @t124 (=> @t277 (=> @t215 @t279)))) % 0.47/0.90 (assume @p90 (forall @t129 (=> @t282 (=> @t216 @t281)))) % 0.47/0.90 (assume @p91 (forall @t133 (=> @t282 (=> @t217 @t284)))) % 0.47/0.90 (assume @p92 (forall @t77 (=> @t285 @t261))) % 0.47/0.90 (assume @p93 (forall @t95 (=> @t286 @t271))) % 0.47/0.90 (assume @p94 (forall @t106 (=> @t287 @t264))) % 0.47/0.90 (assume @p95 (forall @t115 (=> @t288 @t274))) % 0.47/0.90 (assume @p96 (forall @t120 (=> @t277 (=> @t289 @t276)))) % 0.47/0.90 (assume @p97 (forall @t124 (=> @t277 (=> @t290 @t279)))) % 0.47/0.90 (assume @p98 (forall @t129 (=> @t282 (=> @t291 @t281)))) % 0.47/0.90 (assume @p99 (forall @t133 (=> @t282 (=> @t292 @t284)))) % 0.47/0.90 (assume @p100 (forall @t53 (exists (@list @t293) (_ @t294 @t293)))) % 0.47/0.90 (assume @p101 (forall @t204 (=> @t299 (=> @t298 @t296)))) % 0.47/0.90 (assume @p102 (forall @t204 (= @t299 (or @t297 @t296)))) % 0.47/0.90 (assume @p103 (forall @t7 (=> @t277 (not @t300)))) % 0.47/0.90 (assume @p104 (forall @t136 (=> @t282 (not @t301)))) % 0.47/0.90 (assume @p105 (forall @t42 (=> @t303 (not @t191)))) % 0.47/0.90 (assume @p106 (forall @t204 (=> @t297 @t299))) % 0.47/0.90 (assume @p107 (forall @t42 (=> @t303 (not @t305)))) % 0.47/0.90 (assume @p108 (forall @t204 (=> @t297 @t306))) % 0.47/0.90 (assume @p109 (forall @t175 (=> @t303 @t308))) % 0.47/0.90 (assume @p110 (forall @t182 (=> @t297 @t310))) % 0.47/0.90 (assume @p111 (forall @t204 (or @t297 @t195 @t296))) % 0.47/0.90 (assume @p112 (forall @t46 (not (_ @t302 @t21)))) % 0.47/0.90 (assume @p113 (forall @t53 (not (_ @t294 @t51)))) % 0.47/0.90 (assume @p114 (forall @t185 (=> @t3 @t312))) % 0.47/0.90 (assume @p115 (forall @t188 (=> @t135 @t314))) % 0.47/0.90 (assume @p116 (forall @t185 (=> @t277 (=> @t184 @t311)))) % 0.47/0.90 (assume @p117 (forall @t188 (=> @t282 (=> @t187 @t313)))) % 0.47/0.90 (assume @p118 (forall @t143 (=> @t300 (not @t277)))) % 0.47/0.90 (assume @p119 (forall @t144 (=> @t301 (not @t282)))) % 0.47/0.90 (assume @p120 (forall (@list @t224 @t98) (=> (forall @t236 (=> (forall @t234 (=> (_ (_ tptp.ord_less_nat @t232) @t83) @t233)) @t235)) @t315))) % 0.47/0.90 (assume @p121 (forall @t198 (=> @t306 @t316))) % 0.47/0.90 (assume @p122 (forall @t42 (=> @t303 (not (= @t36 @t21))))) % 0.47/0.90 (assume @p123 (forall @t204 (=> @t297 (not (= @t178 @t51))))) % 0.47/0.90 (assume @p124 (forall (@list @t21 @t36 @t317) (=> @t303 (=> @t305 @t317)))) % 0.47/0.90 (assume @p125 (forall (@list @t51 @t178 @t317) (=> @t297 (=> @t296 @t317)))) % 0.47/0.90 (assume @p126 (forall @t204 (=> @t298 (=> @t299 @t296)))) % 0.47/0.90 (assume @p127 (forall @t185 (=> @t277 @t312))) % 0.47/0.90 (assume @p128 (forall @t188 (=> @t282 @t314))) % 0.47/0.90 (assume @p129 (= (lambda (@list @t323) (exists (@list @t322) (_ @t323 @t322))) (lambda (@list @t319) (exists (@list @t320) (and (_ @t319 @t320) (forall @t321 (=> (_ (_ tptp.ord_less_nat @t318) @t320) (not (_ @t319 @t318))))))))) % 0.47/0.90 (assume @p130 (forall @t168 (=> (forall @t166 (=> (_ (_ tptp.ord_less_nat @t163) @t162) @t165)) (=> (forall (@list @t163) (_ @t164 @t163)) @t167)))) % 0.47/0.90 (assume @p131 (forall @t157 (=> @t300 @t326))) % 0.47/0.90 (assume @p132 (forall @t160 (=> @t301 @t329))) % 0.47/0.90 (assume @p133 (forall @t204 (= @t298 (or @t296 @t195)))) % 0.47/0.90 (assume @p134 (forall @t7 (=> @t277 @t330))) % 0.47/0.90 (assume @p135 (forall @t136 (=> @t282 @t331))) % 0.47/0.90 (assume @p136 (forall @t143 (=> @t300 @t330))) % 0.47/0.90 (assume @p137 (forall @t144 (=> @t301 @t331))) % 0.47/0.90 (assume @p138 (forall (@list @t332 @t333) (= (not (_ (_ tptp.ord_less_eq_nat @t332) @t333)) (_ (_ tptp.ord_less_nat @t333) @t332)))) % 0.47/0.90 (assume @p139 (forall @t194 (=> @t193 @t334))) % 0.47/0.90 (assume @p140 (forall @t198 (=> @t197 @t298))) % 0.47/0.90 (assume @p141 (forall @t204 (=> @t298 @t197))) % 0.47/0.90 (assume @p142 (= tptp.ord_le976219883lle_hf (lambda @t207 (or (_ (_ tptp.ord_le1310584031lle_hf @t9) @t43) @t335)))) % 0.47/0.90 (assume @p143 (= tptp.ord_le1310584031lle_hf (lambda @t207 (and @t206 (not @t335))))) % 0.47/0.90 (assume @p144 (= tptp.ord_less_nat (lambda @t213 (and @t212 (not @t336))))) % 0.47/0.90 (assume @p145 (forall @t77 (=> @t76 @t261))) % 0.47/0.90 (assume @p146 (forall @t95 (=> @t94 @t271))) % 0.47/0.90 (assume @p147 (forall @t106 (=> @t105 @t264))) % 0.47/0.90 (assume @p148 (forall @t115 (=> @t114 @t274))) % 0.47/0.90 (assume @p149 (forall @t120 (=> @t119 (=> @t289 (=> @t71 @t275))))) % 0.47/0.90 (assume @p150 (forall @t124 (=> @t119 (=> @t290 (=> @t102 @t278))))) % 0.47/0.90 (assume @p151 (forall @t129 (=> @t128 (=> @t291 (=> @t88 @t280))))) % 0.47/0.90 (assume @p152 (forall @t133 (=> @t128 (=> @t292 (=> @t111 @t283))))) % 0.47/0.90 (assume @p153 (forall @t77 (=> @t285 (=> @t73 (=> @t71 @t256))))) % 0.47/0.90 (assume @p154 (forall @t106 (=> @t287 (=> @t73 (=> @t102 @t262))))) % 0.47/0.90 (assume @p155 (forall @t95 (=> @t286 (=> @t91 (=> @t88 @t265))))) % 0.47/0.90 (assume @p156 (forall @t115 (=> @t288 (=> @t91 (=> @t111 @t272))))) % 0.47/0.90 (assume @p157 (forall @t120 (=> @t277 (=> @t118 @t276)))) % 0.47/0.90 (assume @p158 (forall @t129 (=> @t282 (=> @t127 @t281)))) % 0.47/0.90 (assume @p159 (forall @t124 (=> @t277 (=> @t123 @t279)))) % 0.47/0.90 (assume @p160 (forall @t133 (=> @t282 (=> @t132 @t284)))) % 0.47/0.90 (assume @p161 (forall @t204 (= @t199 @t296))) % 0.47/0.90 (assume @p162 (forall @t204 (= @t298 @t197))) % 0.47/0.90 (assume @p163 (forall @t7 (=> @t119 (=> @t330 @t277)))) % 0.47/0.90 (assume @p164 (forall @t136 (=> @t128 (=> @t331 @t282)))) % 0.47/0.90 (assume @p165 (forall @t42 (=> @t334 @t192))) % 0.47/0.90 (assume @p166 (forall @t204 (=> @t298 @t196))) % 0.47/0.90 (assume @p167 (forall @t42 (=> @t174 (= @t334 @t191)))) % 0.47/0.90 (assume @p168 (forall @t204 (=> @t181 @t316))) % 0.47/0.90 (assume @p169 (forall @t42 (=> @t303 @t174))) % 0.47/0.90 (assume @p170 (forall @t204 (=> @t297 @t181))) % 0.47/0.90 (assume @p171 (forall @t175 (=> @t174 @t308))) % 0.47/0.90 (assume @p172 (forall @t182 (=> @t181 @t310))) % 0.47/0.90 (assume @p173 (forall @t175 (=> @t303 (=> @t173 @t307)))) % 0.47/0.90 (assume @p174 (forall @t182 (=> @t297 (=> @t180 @t309)))) % 0.47/0.90 (assume @p175 (forall @t204 (or @t181 @t296))) % 0.47/0.90 (assume @p176 (forall @t42 (=> @t174 (or @t303 @t191)))) % 0.47/0.90 (assume @p177 (forall @t204 (=> @t181 (or @t297 @t195)))) % 0.47/0.90 (assume @p178 (= tptp.ord_le1310584031lle_hf (lambda @t207 (and @t206 (not @t205))))) % 0.47/0.90 (assume @p179 (= tptp.ord_less_nat (lambda @t213 (and @t212 (not @t210))))) % 0.47/0.90 (assume @p180 (forall @t198 (=> @t202 @t297))) % 0.47/0.90 (assume @p181 (forall @t185 (=> @t119 @t312))) % 0.47/0.90 (assume @p182 (forall @t188 (=> @t128 @t314))) % 0.47/0.90 (assume @p183 (forall @t185 (=> @t277 (=> @t73 @t311)))) % 0.47/0.90 (assume @p184 (forall @t188 (=> @t282 (=> @t91 @t313)))) % 0.47/0.90 (assume @p185 (= tptp.ord_le976219883lle_hf (lambda @t13 (or (_ (_ tptp.ord_le1310584031lle_hf @t11) @t8) @t337)))) % 0.47/0.90 (assume @p186 (= tptp.ord_less_eq_nat (lambda @t151 (or (_ (_ tptp.ord_less_nat @t148) @t147) @t338)))) % 0.47/0.90 (assume @p187 (= tptp.ord_le1310584031lle_hf (lambda @t13 (and @t145 @t339)))) % 0.47/0.90 (assume @p188 (= tptp.ord_less_nat (lambda @t151 (and @t149 @t340)))) % 0.47/0.90 (assume @p189 (forall @t157 (=> @t142 @t326))) % 0.47/0.90 (assume @p190 (forall @t160 (=> @t134 @t329))) % 0.47/0.90 (assume @p191 (forall @t157 (=> @t300 (=> @t156 @t325)))) % 0.47/0.90 (assume @p192 (forall @t160 (=> @t301 (=> @t159 @t328)))) % 0.47/0.90 (assume @p193 (forall @t7 (=> @t277 @t119))) % 0.47/0.90 (assume @p194 (forall @t136 (=> @t282 @t128))) % 0.47/0.90 (assume @p195 (= tptp.ord_le976219883lle_hf (lambda @t341 (or (_ (_ tptp.ord_le1310584031lle_hf @t8) @t11) @t337)))) % 0.47/0.90 (assume @p196 (= tptp.ord_less_eq_nat (lambda @t342 (or (_ (_ tptp.ord_less_nat @t147) @t148) @t338)))) % 0.47/0.90 (assume @p197 (= tptp.ord_le1310584031lle_hf (lambda @t341 (and @t146 @t339)))) % 0.47/0.90 (assume @p198 (= tptp.ord_less_nat (lambda @t342 (and @t150 @t340)))) % 0.47/0.90 (assume @p199 (forall @t143 (=> @t300 @t142))) % 0.47/0.90 (assume @p200 (forall @t144 (=> @t301 @t134))) % 0.47/0.90 (assume @p201 (forall @t7 (=> @t330 (=> @t119 @t277)))) % 0.47/0.90 (assume @p202 (forall @t136 (=> @t331 (=> @t128 @t282)))) % 0.47/0.90 (assume @p203 (forall (@list @t56 @t138 @t48 @t343) (=> @t141 (=> (forall @t6 (=> @t140 (= @t67 (_ @t343 @t4)))) (= @t248 (_ (_ tptp.hF_Mirabelle_RepFun @t138) @t343)))))) % 0.47/0.90 (assume @p204 (forall @t352 (exists @t351 (forall @t350 (=> @t349 (not @t346)))))) % 0.47/0.90 (assume @p205 (forall @t352 (exists @t351 (forall @t350 (=> @t349 @t353))))) % 0.47/0.90 (assume @p206 (forall @t352 (exists @t351 (forall @t350 (=> @t354 @t346))))) % 0.47/0.90 (assume @p207 (forall @t352 (exists @t351 (forall @t350 (=> @t354 (not @t353)))))) % 0.47/0.90 (assume @p208 (forall (@list @t98 @t89 @t224) (=> @t282 (=> @t315 (=> (not (_ @t224 @t89)) (exists (@list @t355) (and (_ @t99 @t355) (_ (_ tptp.ord_less_eq_nat @t355) @t89) (forall @t350 (=> (and (_ @t99 @t344) (_ @t348 @t355)) @t358)) (forall (@list @t356) (=> (forall @t236 (=> (and @t357 (_ @t266 @t356)) @t235)) (_ (_ tptp.ord_less_eq_nat @t356) @t355)))))))))) % 0.47/0.90 (assume @p209 (forall @t169 (= (_ tptp.hF_Mirabelle_HF @t359) @t2))) % 0.47/0.90 (assume @p210 (forall @t352 (exists @t351 (forall @t350 (=> @t349 (not @t360)))))) % 0.47/0.90 (assume @p211 (forall @t352 (exists @t351 (forall @t350 (=> @t349 @t361))))) % 0.47/0.90 (assume @p212 (forall @t352 (exists @t351 (forall @t350 (=> @t349 @t362))))) % 0.47/0.90 (assume @p213 (forall @t376 (=> @t375 (=> @t373 (exists @t351 (forall @t350 (=> @t349 @t368))))))) % 0.47/0.90 (assume @p214 (forall @t376 (=> @t375 (=> @t373 (exists @t351 (forall @t350 (=> @t349 @t377))))))) % 0.47/0.90 (assume @p215 (forall @t352 (exists @t351 (forall @t350 (=> @t354 @t360))))) % 0.47/0.90 (assume @p216 (forall @t352 (exists @t351 (forall @t350 (=> @t354 (not @t361)))))) % 0.47/0.90 (assume @p217 (forall @t352 (exists @t351 (forall @t350 (=> @t354 @t362))))) % 0.47/0.90 (assume @p218 (forall @t376 (=> @t380 (=> @t379 (exists @t351 (forall @t350 (=> @t354 @t368))))))) % 0.47/0.90 (assume @p219 (forall @t376 (=> @t380 (=> @t379 (exists @t351 (forall @t350 (=> @t354 @t377))))))) % 0.47/0.90 (assume @p220 (forall @t243 (=> @t382 (= (_ tptp.hF_Mirabelle_hfset @t381) @t241)))) % 0.47/0.90 (assume @p221 (forall (@list @t21 @t241) (= (_ @t59 @t381) (and (_ (_ tptp.member1367349282lle_hf @t21) @t241) @t382)))) % 0.47/0.90 (assume @p222 (forall @t169 (_ tptp.finite586181922lle_hf @t359))) % 0.47/0.90 (assume @p223 (forall @t389 (=> @t382 (=> @t388 (exists @t6 (and @t387 (_ @t68 @t2) (forall @t386 (=> @t385 (=> (_ (_ tptp.ord_le976219883lle_hf @t383) @t4) @t384))))))))) % 0.47/0.90 (assume @p224 (forall @t399 (=> @t398 (=> @t397 (exists @t236 (and @t396 (_ @t85 @t98) (forall @t394 (=> @t393 (=> (_ (_ tptp.ord_less_eq_nat @t390) @t83) @t391))))))))) % 0.47/0.90 (assume @p225 (forall @t389 (=> @t382 (=> @t388 (exists @t6 (and @t387 (_ @t64 @t4) (forall @t386 (=> @t385 (=> (_ @t68 @t383) @t384))))))))) % 0.47/0.90 (assume @p226 (forall @t399 (=> @t398 (=> @t397 (exists @t236 (and @t396 @t357 (forall @t394 (=> @t393 (=> (_ @t85 @t390) @t391))))))))) % 0.47/0.90 (assume @p227 (forall @t404 (=> @t403 (=> @t401 @t382)))) % 0.47/0.90 (assume @p228 (forall @t410 (=> @t409 @t407))) % 0.47/0.90 (assume @p229 (forall (@list @t412 @t411) (=> (_ (_ tptp.ord_le432112161lle_hf @t412) @t411) (=> (not (_ tptp.finite586181922lle_hf @t412)) (not (_ tptp.finite586181922lle_hf @t411)))))) % 0.47/0.90 (assume @p230 (forall (@list @t414 @t413) (=> (_ (_ tptp.ord_less_eq_set_nat @t414) @t413) (=> (not (_ tptp.finite_finite_nat @t414)) (not (_ tptp.finite_finite_nat @t413)))))) % 0.47/0.90 (assume @p231 (forall @t415 (=> @t401 (=> @t403 @t382)))) % 0.47/0.90 (assume @p232 (forall @t416 (=> @t406 (=> @t409 @t398)))) % 0.47/0.90 (assume @p233 (forall (@list @t241 @t239) (=> @t382 (=> (forall (@list @t417) (=> (_ tptp.finite586181922lle_hf @t417) (=> (forall (@list @t418) (=> (_ (_ tptp.ord_le1344122901lle_hf @t418) @t417) (_ @t239 @t418))) (_ @t239 @t417)))) (_ @t239 @t241))))) % 0.47/0.90 (assume @p234 (forall (@list @t392 @t419) (=> @t398 (=> (forall (@list @t420) (=> (_ tptp.finite_finite_nat @t420) (=> (forall (@list @t421) (=> (_ (_ tptp.ord_less_set_nat @t421) @t420) (_ @t419 @t421))) (_ @t419 @t420)))) (_ @t419 @t392))))) % 0.47/0.90 (assume @p235 (forall @t415 (=> @t401 (=> @t403 (=> @t425 @t422))))) % 0.47/0.90 (assume @p236 (forall @t416 (=> @t406 (=> @t409 (=> @t429 @t426))))) % 0.47/0.90 (assume @p237 (_ (_ tptp.inj_on811196232lle_hf tptp.hF_Mirabelle_HF) (_ tptp.collec1758573718lle_hf tptp.finite586181922lle_hf))) % 0.47/0.90 (assume @p238 (_ (_ tptp.orderi1737556723lle_hf tptp.ord_le976219883lle_hf) tptp.ord_le1310584031lle_hf)) % 0.47/0.90 (assume @p239 (_ (_ tptp.ordering_nat tptp.ord_less_eq_nat) tptp.ord_less_nat)) % 0.47/0.90 (assume @p240 (forall @t415 (=> @t401 (=> @t403 @t431)))) % 0.47/0.90 (assume @p241 (forall @t416 (=> @t406 (=> @t409 @t433)))) % 0.47/0.90 (assume @p242 (forall @t415 (=> @t401 (=> @t403 (=> (_ (_ tptp.ord_less_eq_nat @t423) @t424) @t434))))) % 0.47/0.90 (assume @p243 (forall @t416 (=> @t406 (=> @t409 (=> (_ (_ tptp.ord_less_eq_nat @t427) @t428) @t435))))) % 0.47/0.90 (assume @p244 (forall @t415 (=> @t401 (=> @t403 (=> (= @t424 @t423) @t434))))) % 0.47/0.90 (assume @p245 (forall @t416 (=> @t406 (=> @t409 (=> (= @t428 @t427) @t435))))) % 0.47/0.90 (assume @p246 (forall (@list @t241 @t437) (=> (not @t382) (exists (@list @t436) (and (_ tptp.finite586181922lle_hf @t436) (= (_ tptp.finite1213132899lle_hf @t436) @t437) (_ (_ tptp.ord_le432112161lle_hf @t436) @t241)))))) % 0.47/0.90 (assume @p247 (forall (@list @t392 @t437) (=> (not @t398) (exists (@list @t438) (and (_ tptp.finite_finite_nat @t438) (= (_ tptp.finite_card_nat @t438) @t437) (_ (_ tptp.ord_less_eq_set_nat @t438) @t392)))))) % 0.47/0.90 (assume @p248 (forall (@list @t440 @t439) (=> (forall (@list @t442) (=> (_ (_ tptp.ord_le432112161lle_hf @t442) @t440) (=> (_ tptp.finite586181922lle_hf @t442) (_ (_ tptp.ord_less_eq_nat (_ tptp.finite1213132899lle_hf @t442)) @t439)))) (and @t441 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite1213132899lle_hf @t440)) @t439))))) % 0.47/0.90 (assume @p249 (forall (@list @t443 @t439) (=> (forall (@list @t445) (=> (_ (_ tptp.ord_less_eq_set_nat @t445) @t443) (=> (_ tptp.finite_finite_nat @t445) (_ (_ tptp.ord_less_eq_nat (_ tptp.finite_card_nat @t445)) @t439)))) (and @t444 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite_card_nat @t443)) @t439))))) % 0.47/0.90 (assume @p250 (forall @t415 (=> @t401 (=> @t422 @t425)))) % 0.47/0.90 (assume @p251 (forall @t416 (=> @t406 (=> @t426 @t429)))) % 0.47/0.90 (assume @p252 (forall (@list @t437 @t412) (=> (_ @t447 (_ tptp.finite1213132899lle_hf @t412)) (not (forall (@list @t446) (=> (_ (_ tptp.ord_le432112161lle_hf @t446) @t412) (=> (= (_ tptp.finite1213132899lle_hf @t446) @t437) (not (_ tptp.finite586181922lle_hf @t446))))))))) % 0.47/0.90 (assume @p253 (forall (@list @t437 @t414) (=> (_ @t447 (_ tptp.finite_card_nat @t414)) (not (forall (@list @t448) (=> (_ (_ tptp.ord_less_eq_set_nat @t448) @t414) (=> (= (_ tptp.finite_card_nat @t448) @t437) (not (_ tptp.finite_finite_nat @t448))))))))) % 0.47/0.90 (assume @p254 (forall (@list @t244 @t449) (=> (forall @t454 (=> (_ (_ tptp.ord_le1344122901lle_hf @t247) @t451) (=> @t453 (=> @t452 (not (= (_ @t449 @t247) (_ @t449 @t451))))))) (=> (forall @t454 (=> @t453 (=> @t452 (or (_ (_ tptp.ord_le432112161lle_hf @t247) @t451) (_ (_ tptp.ord_le432112161lle_hf @t451) @t247))))) @t450)))) % 0.47/0.90 (assume @p255 (forall (@list @t400 @t241 @t459) (=> @t401 (=> (forall @t465 (=> @t464 (exists (@list @t462) (and (_ (_ tptp.member1367349282lle_hf @t462) @t400) (_ (_ @t459 @t463) @t462))))) (=> (forall (@list @t456 @t455 @t458) (=> @t461 (=> @t460 (=> (_ (_ tptp.member1367349282lle_hf @t458) @t400) (=> (_ (_ @t459 @t456) @t458) (=> (_ (_ @t459 @t455) @t458) @t457)))))) @t431))))) % 0.47/0.90 (assume @p256 (forall (@list @t405 @t241 @t467) (=> @t406 (=> (forall @t465 (=> @t464 (exists (@list @t468) (and (_ (_ tptp.member_nat @t468) @t405) (_ (_ @t467 @t463) @t468))))) (=> (forall (@list @t456 @t455 @t162) (=> @t461 (=> @t460 (=> (_ (_ tptp.member_nat @t162) @t405) (=> (_ (_ @t467 @t456) @t162) (=> (_ (_ @t467 @t455) @t162) @t457)))))) @t466))))) % 0.47/0.90 (assume @p257 (forall (@list @t469 @t437) (=> (forall @t236 (=> (_ @t395 @t469) (_ @t266 @t437))) (_ tptp.finite_finite_nat @t469)))) % 0.47/0.90 (assume @p258 (= tptp.finite_finite_nat (lambda @t474 (exists @t321 (forall @t473 (=> @t472 (_ @t470 @t318))))))) % 0.47/0.90 (assume @p259 (forall (@list @t244 @t400) (=> @t478 (=> @t401 (=> @t477 (exists (@list @t475) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_899003828lle_hf @t475) @t244)) @t400) (_ (_ tptp.inj_on811196232lle_hf @t475) @t244)))))))) % 0.47/0.90 (assume @p260 (forall @t404 (=> @t382 (=> @t401 (=> @t431 (exists (@list @t479) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_1743964010lle_hf @t479) @t241)) @t400) (_ (_ tptp.inj_on755450110lle_hf @t479) @t241)))))))) % 0.47/0.90 (assume @p261 (forall (@list @t241 @t405) (=> @t382 (=> @t406 (=> @t466 (exists (@list @t480) (and (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_131453538hf_nat @t480) @t241)) @t405) (_ (_ tptp.inj_on1874279374hf_nat @t480) @t241)))))))) % 0.47/0.90 (assume @p262 (forall (@list @t392 @t400) (=> @t398 (=> @t401 (=> (_ @t432 @t423) (exists (@list @t481) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_246164834lle_hf @t481) @t392)) @t400) (_ (_ tptp.inj_on1988990670lle_hf @t481) @t392)))))))) % 0.47/0.90 (assume @p263 (forall @t410 (=> @t398 (=> @t406 (=> @t433 (exists (@list @t482) (and (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_nat_nat @t482) @t392)) @t405) (_ (_ tptp.inj_on_nat_nat @t482) @t392)))))))) % 0.47/0.90 (assume @p264 (forall (@list @t449 @t244 @t400) (=> @t450 (=> (_ (_ tptp.ord_le432112161lle_hf @t483) @t400) (=> @t401 @t477))))) % 0.47/0.90 (assume @p265 (forall (@list @t440 @t484) (=> @t441 (_ tptp.finite586181922lle_hf (_ (_ tptp.image_1743964010lle_hf @t484) @t440))))) % 0.47/0.90 (assume @p266 (forall (@list @t440 @t485) (=> @t441 (_ tptp.finite_finite_nat (_ (_ tptp.image_131453538hf_nat @t485) @t440))))) % 0.47/0.90 (assume @p267 (forall (@list @t443 @t486) (=> @t444 (_ tptp.finite586181922lle_hf (_ (_ tptp.image_246164834lle_hf @t486) @t443))))) % 0.47/0.90 (assume @p268 (forall (@list @t443 @t487) (=> @t444 (_ tptp.finite_finite_nat (_ (_ tptp.image_nat_nat @t487) @t443))))) % 0.47/0.90 (assume @p269 (forall @t499 (= (forall @t495 (=> (and @t493 @t498) @t496)) (forall @t495 (=> @t494 @t490))))) % 0.47/0.90 (assume @p270 (forall @t510 (= (forall @t495 (=> (and @t493 @t509) @t496)) (forall @t507 (=> @t506 @t502))))) % 0.47/0.90 (assume @p271 (forall @t516 (= (forall @t507 (=> (and @t505 @t515) @t513)) (forall @t495 (=> @t494 @t512))))) % 0.47/0.90 (assume @p272 (forall @t521 (= (forall @t507 (=> (and @t505 @t520) @t513)) (forall @t507 (=> @t506 @t518))))) % 0.47/0.90 (assume @p273 (forall @t499 (= (exists @t495 (and @t493 @t498 @t496)) (exists @t495 (and @t493 @t492 @t490))))) % 0.47/0.90 (assume @p274 (forall @t510 (= (exists @t495 (and @t493 @t509 @t496)) (exists @t507 (and @t505 @t504 @t502))))) % 0.47/0.90 (assume @p275 (forall @t516 (= (exists @t507 (and @t505 @t515 @t513)) (exists @t495 (and @t493 @t492 @t512))))) % 0.47/0.90 (assume @p276 (forall @t521 (= (exists @t507 (and @t505 @t520 @t513)) (exists @t507 (and @t505 @t504 @t518))))) % 0.47/0.90 (assume @p277 (forall (@list @t400 @t48 @t241) (=> @t401 (=> @t527 (exists @t525 (and @t524 @t523 (= @t400 (_ @t489 @t522)))))))) % 0.47/0.90 (assume @p278 (forall (@list @t400 @t79 @t392) (=> @t401 (=> @t532 (exists @t531 (and @t530 @t529 (= @t400 (_ @t501 @t528)))))))) % 0.47/0.90 (assume @p279 (forall (@list @t405 @t96 @t241) (=> @t406 (=> @t534 (exists @t525 (and @t524 @t523 (= @t405 (_ @t511 @t522)))))))) % 0.47/0.90 (assume @p280 (forall (@list @t405 @t107 @t392) (=> @t406 (=> @t535 (exists @t531 (and @t530 @t529 (= @t405 (_ @t517 @t528)))))))) % 0.47/0.90 (assume @p281 (forall (@list @t241 @t400 @t48) (=> @t382 (=> @t527 @t401)))) % 0.47/0.90 (assume @p282 (forall (@list @t241 @t405 @t96) (=> @t382 (=> @t534 @t406)))) % 0.47/0.90 (assume @p283 (forall (@list @t392 @t400 @t79) (=> @t398 (=> @t532 @t401)))) % 0.47/0.90 (assume @p284 (forall (@list @t392 @t405 @t107) (=> @t398 (=> @t535 @t406)))) % 0.47/0.90 (assume @p285 (forall @t537 (=> @t450 (= @t536 @t478)))) % 0.47/0.90 (assume @p286 (forall @t540 (=> @t539 (= @t538 @t382)))) % 0.47/0.90 (assume @p287 (forall @t543 (=> @t542 (= @t541 @t398)))) % 0.47/0.90 (assume @p288 (forall @t546 (=> @t545 (= @t544 @t382)))) % 0.47/0.90 (assume @p289 (forall @t549 (=> @t548 (= @t547 @t398)))) % 0.47/0.90 (assume @p290 (forall @t537 (=> @t536 (=> @t450 @t478)))) % 0.47/0.90 (assume @p291 (forall @t540 (=> @t538 (=> @t539 @t382)))) % 0.47/0.90 (assume @p292 (forall @t543 (=> @t541 (=> @t542 @t398)))) % 0.47/0.90 (assume @p293 (forall @t546 (=> @t544 (=> @t545 @t382)))) % 0.47/0.90 (assume @p294 (forall @t549 (=> @t547 (=> @t548 @t398)))) % 0.47/0.90 (assume @p295 (forall @t537 (=> @t450 (= (_ tptp.finite1213132899lle_hf @t483) @t476)))) % 0.47/0.90 (assume @p296 (forall (@list @t241 @t48) (=> @t382 (=> (_ @t402 @t497) @t539)))) % 0.47/0.90 (assume @p297 (forall (@list @t392 @t107) (=> @t398 (=> (_ @t408 @t519) @t548)))) % 0.47/0.90 (assume @p298 (forall (@list @t96 @t241 @t405) (=> @t545 (=> (_ (_ tptp.ord_less_eq_set_nat @t514) @t405) (=> @t406 @t382))))) % 0.47/0.90 (assume @p299 (forall (@list @t107 @t392 @t405) (=> @t548 (=> (_ (_ tptp.ord_less_eq_set_nat @t519) @t405) @t407)))) % 0.47/0.90 (assume @p300 (forall (@list @t551 @t550) (_ tptp.finite_finite_nat (_ (_ tptp.set_or1544565540an_nat @t551) @t550)))) % 0.47/0.90 (assume @p301 (forall @t170 (= (not @t553) (_ @t552 @t98)))) % 0.47/0.90 (assume @p302 (forall @t554 (not (_ (_ tptp.ord_less_nat @t437) tptp.zero_zero_nat)))) % 0.47/0.90 (assume @p303 (forall @t554 (= @t557 @t555))) % 0.47/0.90 (assume @p304 (forall @t554 (_ @t558 @t437))) % 0.47/0.90 (assume @p305 (forall @t170 (_ @t558 @t98))) % 0.47/0.90 (assume @p306 (forall @t554 (= (_ @t447 tptp.zero_zero_nat) @t556))) % 0.47/0.90 (assume @p307 (forall @t170 (= @t559 @t553))) % 0.47/0.90 (assume @p308 (forall @t170 (=> @t559 @t553))) % 0.47/0.90 (assume @p309 (forall @t564 (=> @t563 (=> (not @t562) (exists (@list @t560) (and (_ (_ tptp.ord_less_eq_nat @t560) @t437) (forall (@list @t561) (=> (_ (_ tptp.ord_less_nat @t561) @t560) (not (_ @t224 @t561)))) (_ @t224 @t560))))))) % 0.47/0.90 (assume @p310 (forall @t170 (not (_ @t255 tptp.zero_zero_nat)))) % 0.47/0.90 (assume @p311 (forall @t564 (=> @t562 (=> (forall (@list @t566) (=> (_ @t552 @t566) (=> (not (_ @t224 @t566)) (exists (@list @t565) (and (_ (_ tptp.ord_less_nat @t565) @t566) (not (_ @t224 @t565))))))) @t563)))) % 0.47/0.90 (assume @p312 (forall (@list @t567 @t437) (=> (_ (_ tptp.ord_less_nat @t567) @t437) @t557))) % 0.47/0.90 (assume @p313 (forall @t554 (= (not @t555) @t556))) % 0.47/0.90 (assume @p314 (forall @t554 (=> @t557 @t555))) % 0.47/0.90 (assume @p315 (forall @t250 (= (_ (_ tptp.hF_Mirabelle_RepFun tptp.zero_z189798548lle_hf) @t48) tptp.zero_z189798548lle_hf))) % 0.47/0.90 (assume @p316 (= (_ tptp.hF_Mirabelle_HUnion tptp.zero_z189798548lle_hf) tptp.zero_z189798548lle_hf)) % 0.47/0.90 (assume @p317 (forall (@list @t19) (= (_ (_ tptp.hF_Mirabelle_Replace tptp.zero_z189798548lle_hf) @t19) tptp.zero_z189798548lle_hf))) % 0.47/0.90 (assume @p318 @t572) % 0.47/0.90 (assume @p319 @t573) % 0.47/0.90 (assume @p320 true) % 0.47/0.90 (step @p321 (= tptp.ord_le976219883lle_hf @t580) :rule refl :args (@t580)) % 0.47/0.90 (step @p322 (= tptp.ord_le2017230260lle_hf @t583) :rule refl :args (@t583)) % 0.47/0.90 (step @p323 (= tptp.ord_less_eq_o_nat @t586) :rule refl :args (@t586)) % 0.47/0.90 (step @p324 (= tptp.hF_Mirabelle_hmem @t588) :rule refl :args (@t588)) % 0.47/0.90 (step @p325 (= tptp.ord_le1310584031lle_hf @t589) :rule refl :args (@t589)) % 0.47/0.90 (step @p326 (= tptp.order_690706045lle_hf @t591) :rule refl :args (@t591)) % 0.47/0.90 (step @p327 (= tptp.order_557194383hf_nat @t593) :rule refl :args (@t593)) % 0.47/0.90 (step @p328 (= tptp.order_671905679lle_hf @t595) :rule refl :args (@t595)) % 0.47/0.90 (step @p329 (= tptp.order_1631207636at_nat @t597) :rule refl :args (@t597)) % 0.47/0.90 (step @p330 (= tptp.ord_less_eq_nat @t598) :rule refl :args (@t598)) % 0.47/0.90 (step @p331 (= tptp.finite_finite_nat @t599) :rule refl :args (@t599)) % 0.47/0.90 (step @p332 :rule refl :args ((tptp.member1367349282lle_hf @t568 @t600))) % 0.47/0.90 (step @p333 :rule refl :args (@t601)) % 0.47/0.90 (step @p334 :rule refl :args (@t568)) % 0.47/0.90 (step @p335 :rule cong :premises (@p334 @p333) :args (@t602)) % 0.47/0.90 (step @p336 :rule trans :premises (@p335 @p332)) % 0.47/0.90 (step @p337 :rule refl :args (@t603)) % 0.47/0.90 (step @p338 :rule ho_cong :premises (@p337 @p333)) % 0.47/0.90 (step @p339 :rule cong :premises (@p338 @p336) :args ((= (_ @t603 @t601) @t602))) % 0.47/0.90 (step @p340 :rule symm :premises (@p339)) % 0.47/0.90 (step @p341 :rule refl :args (@t604)) % 0.47/0.90 (step @p342 :rule eq_resolve :premises (@p341 @p340)) % 0.47/0.90 (step @p343 :rule refl :args (@t600)) % 0.47/0.90 (step @p344 :rule cong :premises (@p343 @p333) :args ((= @t600 @t601))) % 0.47/0.90 (step @p345 :rule symm :premises (@p344)) % 0.47/0.90 (step @p346 :rule eq_resolve :premises (@p343 @p345)) % 0.47/0.90 (step @p347 :rule ho_cong :premises (@p337 @p346)) % 0.47/0.90 (step @p348 :rule trans :premises (@p347 @p342)) % 0.47/0.90 (step @p349 :rule refl :args ((tptp.member1367349282lle_hf @t568 @t605))) % 0.47/0.90 (step @p350 :rule refl :args (@t606)) % 0.47/0.90 (step @p351 :rule cong :premises (@p334 @p350) :args (@t607)) % 0.47/0.90 (step @p352 :rule trans :premises (@p351 @p349)) % 0.47/0.90 (step @p353 :rule ho_cong :premises (@p337 @p350)) % 0.47/0.90 (step @p354 :rule cong :premises (@p353 @p352) :args ((= (_ @t603 @t606) @t607))) % 0.47/0.90 (step @p355 :rule symm :premises (@p354)) % 0.47/0.90 (step @p356 :rule refl :args (@t608)) % 0.47/0.90 (step @p357 :rule eq_resolve :premises (@p356 @p355)) % 0.47/0.90 (step @p358 :rule refl :args (@t605)) % 0.47/0.90 (step @p359 :rule cong :premises (@p358 @p350) :args ((= @t605 @t606))) % 0.47/0.90 (step @p360 :rule symm :premises (@p359)) % 0.47/0.90 (step @p361 :rule eq_resolve :premises (@p358 @p360)) % 0.47/0.90 (step @p362 :rule ho_cong :premises (@p337 @p361)) % 0.47/0.90 (step @p363 :rule trans :premises (@p362 @p357)) % 0.47/0.90 (step @p364 :rule cong :premises (@p363) :args (@t609)) % 0.47/0.90 (step @p365 :rule nary_cong :premises (@p364 @p348) :args (@t610)) % 0.47/0.90 (step @p366 :rule cong :premises (@p365) :args ((forall @t571 @t610))) % 0.47/0.90 (step @p367 :rule bool-impl-elim :args (@t608 @t604)) % 0.47/0.90 (step @p368 :rule cong :premises (@p367) :args ((forall @t571 (=> @t608 @t604)))) % 0.47/0.90 (step @p369 :rule trans :premises (@p368 @p366)) % 0.47/0.90 (step @p370 :rule beta-reduce :args ((= (_ @t611 tptp.b) @t604))) % 0.47/0.90 (step @p371 :rule refl :args (tptp.b)) % 0.47/0.90 (step @p372 :rule beta-reduce :args ((= @t612 @t611))) % 0.47/0.90 (step @p373 :rule ho_cong :premises (@p372 @p371)) % 0.47/0.90 (step @p374 :rule trans :premises (@p373 @p370)) % 0.47/0.90 (step @p375 :rule beta-reduce :args ((= (_ @t611 tptp.a) @t608))) % 0.47/0.90 (step @p376 :rule refl :args (tptp.a)) % 0.47/0.90 (step @p377 :rule ho_cong :premises (@p372 @p376)) % 0.47/0.90 (step @p378 :rule trans :premises (@p377 @p375)) % 0.47/0.90 (step @p379 :rule cong :premises (@p378 @p374) :args (@t613)) % 0.47/0.90 (step @p380 :rule cong :premises (@p379) :args ((forall @t571 @t613))) % 0.47/0.90 (step @p381 :rule trans :premises (@p380 @p369)) % 0.47/0.90 (step @p382 :rule refl :args (@t568)) % 0.47/0.90 (step @p383 :rule ho_cong :premises (@p324 @p382)) % 0.47/0.90 (step @p384 :rule ho_cong :premises (@p383 @p371)) % 0.47/0.90 (step @p385 :rule ho_cong :premises (@p383 @p376)) % 0.47/0.90 (step @p386 :rule cong :premises (@p385 @p384) :args (@t570)) % 0.47/0.90 (step @p387 :rule cong :premises (@p386) :args (@t572)) % 0.47/0.90 (step @p388 :rule trans :premises (@p387 @p381)) % 0.47/0.90 (step @p389 :rule eq_resolve :premises (@p318 @p388)) % 0.47/0.90 (step @p390 :rule alpha_equiv :args (@t614 (@list @t568) (@list @t9))) % 0.47/0.90 (step @p391 :rule equiv_elim1 :premises (@p390)) % 0.47/0.90 (step @p392 :rule reordering :premises (@p391) :args ((or @t616 (not @t614)))) % 0.47/0.90 (step @p393 :rule chain_m_resolution :premises (@p392 @p389) :args (@t616 @t617 (@list @t614))) % 0.47/0.90 (step @p394 :rule beta-reduce :args ((= (_ @t620 tptp.b) @t616))) % 0.47/0.90 (step @p395 :rule beta-reduce :args ((= (_ (lambda @t579 (forall @t12 (or (not @t622) @t619))) tptp.a) @t620))) % 0.47/0.90 (step @p396 :rule refl :args ((tptp.member1367349282lle_hf @t9 @t623))) % 0.47/0.90 (step @p397 :rule refl :args (@t618)) % 0.47/0.90 (step @p398 :rule refl :args (@t9)) % 0.47/0.90 (step @p399 :rule cong :premises (@p398 @p397) :args (@t619)) % 0.47/0.90 (step @p400 :rule trans :premises (@p399 @p396)) % 0.47/0.90 (step @p401 :rule refl :args (@t242)) % 0.47/0.90 (step @p402 :rule ho_cong :premises (@p401 @p397)) % 0.47/0.90 (step @p403 :rule cong :premises (@p402 @p400) :args ((= (_ @t242 @t618) @t619))) % 0.47/0.90 (step @p404 :rule symm :premises (@p403)) % 0.47/0.90 (step @p405 :rule refl :args (@t624)) % 0.47/0.90 (step @p406 :rule eq_resolve :premises (@p405 @p404)) % 0.47/0.90 (step @p407 :rule refl :args (@t623)) % 0.47/0.90 (step @p408 :rule cong :premises (@p407 @p397) :args ((= @t623 @t618))) % 0.47/0.90 (step @p409 :rule symm :premises (@p408)) % 0.47/0.90 (step @p410 :rule eq_resolve :premises (@p407 @p409)) % 0.47/0.90 (step @p411 :rule ho_cong :premises (@p401 @p410)) % 0.47/0.90 (step @p412 :rule trans :premises (@p411 @p406)) % 0.47/0.90 (step @p413 :rule refl :args ((tptp.member1367349282lle_hf @t9 @t625))) % 0.47/0.90 (step @p414 :rule refl :args (@t621)) % 0.47/0.90 (step @p415 :rule cong :premises (@p398 @p414) :args (@t622)) % 0.47/0.90 (step @p416 :rule trans :premises (@p415 @p413)) % 0.47/0.90 (step @p417 :rule ho_cong :premises (@p401 @p414)) % 0.47/0.90 (step @p418 :rule cong :premises (@p417 @p416) :args ((= (_ @t242 @t621) @t622))) % 0.47/0.90 (step @p419 :rule symm :premises (@p418)) % 0.47/0.90 (step @p420 :rule refl :args (@t626)) % 0.47/0.90 (step @p421 :rule eq_resolve :premises (@p420 @p419)) % 0.47/0.90 (step @p422 :rule refl :args (@t625)) % 0.47/0.90 (step @p423 :rule cong :premises (@p422 @p414) :args ((= @t625 @t621))) % 0.47/0.90 (step @p424 :rule symm :premises (@p423)) % 0.47/0.90 (step @p425 :rule eq_resolve :premises (@p422 @p424)) % 0.47/0.90 (step @p426 :rule ho_cong :premises (@p401 @p425)) % 0.47/0.90 (step @p427 :rule trans :premises (@p426 @p421)) % 0.47/0.90 (step @p428 :rule cong :premises (@p427) :args (@t627)) % 0.47/0.90 (step @p429 :rule nary_cong :premises (@p428 @p412) :args (@t628)) % 0.47/0.90 (step @p430 :rule cong :premises (@p429) :args ((forall @t12 @t628))) % 0.47/0.90 (step @p431 :rule beta-reduce :args ((= @t629 @t624))) % 0.47/0.90 (step @p432 :rule beta-reduce :args ((= @t630 @t626))) % 0.47/0.90 (step @p433 :rule cong :premises (@p432) :args (@t631)) % 0.47/0.90 (step @p434 :rule nary_cong :premises (@p433 @p431) :args (@t632)) % 0.47/0.90 (step @p435 :rule cong :premises (@p434) :args (@t633)) % 0.47/0.90 (step @p436 :rule trans :premises (@p435 @p430)) % 0.47/0.90 (step @p437 :rule cong :premises (@p436) :args (@t634)) % 0.47/0.90 (step @p438 :rule ho_cong :premises (@p437 @p376)) % 0.47/0.90 (step @p439 :rule trans :premises (@p438 @p395)) % 0.47/0.90 (step @p440 :rule ho_cong :premises (@p439 @p371)) % 0.47/0.90 (step @p441 :rule trans :premises (@p440 @p394)) % 0.47/0.90 (step @p442 :rule cong :premises (@p441) :args ((not (_ (_ @t634 tptp.a) tptp.b)))) % 0.47/0.90 (step @p443 :rule refl :args (@t574)) % 0.47/0.90 (step @p444 :rule refl :args (@t9)) % 0.47/0.90 (step @p445 :rule ho_cong :premises (@p324 @p444 @p443)) % 0.47/0.90 (step @p446 :rule refl :args (@t576)) % 0.47/0.90 (step @p447 :rule ho_cong :premises (@p324 @p444 @p446)) % 0.47/0.90 (step @p448 :rule cong :premises (@p447) :args (@t636)) % 0.47/0.90 (step @p449 :rule nary_cong :premises (@p448 @p445) :args (@t638)) % 0.47/0.90 (step @p450 :rule cong :premises (@p449) :args (@t639)) % 0.47/0.90 (step @p451 :rule cong :premises (@p450) :args ((lambda @t579 @t639))) % 0.47/0.90 (step @p452 :rule refl :args (@t637)) % 0.47/0.90 (step @p453 :rule refl :args (@t575)) % 0.47/0.90 (step @p454 :rule cong :premises (@p453 @p452) :args ((= @t575 @t637))) % 0.47/0.90 (step @p455 :rule symm :premises (@p454)) % 0.47/0.90 (step @p456 :rule eq_resolve :premises (@p453 @p455)) % 0.47/0.90 (step @p457 :rule refl :args (@t635)) % 0.47/0.90 (step @p458 :rule refl :args (@t577)) % 0.47/0.90 (step @p459 :rule cong :premises (@p458 @p457) :args ((= @t577 @t635))) % 0.47/0.90 (step @p460 :rule symm :premises (@p459)) % 0.47/0.90 (step @p461 :rule eq_resolve :premises (@p458 @p460)) % 0.47/0.90 (step @p462 :rule cong :premises (@p461) :args (@t640)) % 0.47/0.90 (step @p463 :rule nary_cong :premises (@p462 @p456) :args (@t641)) % 0.47/0.90 (step @p464 :rule cong :premises (@p463) :args ((forall @t12 @t641))) % 0.47/0.90 (step @p465 :rule bool-impl-elim :args (@t577 @t575)) % 0.47/0.90 (step @p466 :rule cong :premises (@p465) :args (@t578)) % 0.47/0.90 (step @p467 :rule trans :premises (@p466 @p464)) % 0.47/0.90 (step @p468 :rule cong :premises (@p467) :args (@t580)) % 0.47/0.90 (step @p469 :rule trans :premises (@p321 @p468)) % 0.47/0.90 (step @p470 :rule trans :premises (@p469 @p451)) % 0.47/0.90 (step @p471 :rule ho_cong :premises (@p470 @p376)) % 0.47/0.90 (step @p472 :rule ho_cong :premises (@p471 @p371)) % 0.47/0.90 (step @p473 :rule cong :premises (@p472) :args (@t573)) % 0.47/0.90 (step @p474 :rule trans :premises (@p473 @p442)) % 0.47/0.90 (step @p475 :rule eq_resolve :premises (@p319 @p474)) % 0.47/0.90 (step @p476 false :rule chain_m_resolution :premises (@p475 @p393) :args (false @t617 (@list @t616))) % 0.47/0.90 ) % 0.47/0.90 % SZS output end Proof % 0.47/0.90 % cvc5 exiting %------------------------------------------------------------------------------