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