%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP204^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:25:22 AM UTC 2026 % Result : Theorem 0.45s 0.94s % Output : Proof 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : ITP204^1 : TPTP v9.2.1. Released v7.5.0. % 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n028.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 04:19:05 EDT 2026 % 0.17/0.35 % CPUTime : % 0.37/0.63 %----Proving TH0 % 0.45/0.94 --- 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.45/0.94 % SZS status Theorem % 0.45/0.94 % SZS output start Proof % 0.45/0.94 ( % 0.45/0.94 (declare-sort tptp.option_game 0) % 0.45/0.94 (declare-sort tptp.option_fml 0) % 0.45/0.94 (declare-sort tptp.produc1739631244on_fml 0) % 0.45/0.94 (declare-sort tptp.char 0) % 0.45/0.94 (declare-sort tptp.trm 0) % 0.45/0.94 (declare-sort tptp.option_trm 0) % 0.45/0.94 (declare-sort tptp.fml 0) % 0.45/0.94 (declare-sort tptp.game 0) % 0.45/0.94 (declare-sort tptp.produc62062515n_game 0) % 0.45/0.94 (declare-sort tptp.set_variable 0) % 0.45/0.94 (declare-sort tptp.variable 0) % 0.45/0.94 (declare-sort tptp.produc799602994n_game 0) % 0.45/0.94 (declare-sort tptp.produc1418842292n_game 0) % 0.45/0.94 (declare-const tptp.produc1499310791on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.option_fml) tptp.produc1418842292n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc692578258on_trm (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.option_trm) tptp.produc62062515n_game tptp.option_trm)) % 0.45/0.94 (declare-const tptp.produc154833544on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.option_fml) tptp.produc62062515n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc885547027on_trm (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_trm) tptp.produc799602994n_game tptp.option_trm)) % 0.45/0.94 (declare-const tptp.produc347802313on_fml (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_fml) tptp.produc799602994n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.the_game (-> tptp.option_game tptp.game)) % 0.45/0.94 (declare-const tptp.none_game tptp.option_game) % 0.45/0.94 (declare-const tptp.the_trm (-> tptp.option_trm tptp.trm)) % 0.45/0.94 (declare-const tptp.none_trm tptp.option_trm) % 0.45/0.94 (declare-const tptp.the_fml (-> tptp.option_fml tptp.fml)) % 0.45/0.94 (declare-const tptp.none_fml tptp.option_fml) % 0.45/0.94 (declare-const tptp.if_option_fml (-> Bool tptp.option_fml tptp.option_fml tptp.option_fml)) % 0.45/0.94 (declare-const tptp.if_option_trm (-> Bool tptp.option_trm tptp.option_trm tptp.option_trm)) % 0.45/0.94 (declare-const tptp.inf_inf_o (-> Bool Bool Bool)) % 0.45/0.94 (declare-const tptp.member_variable (-> tptp.variable tptp.set_variable Bool)) % 0.45/0.94 (declare-const tptp.collect_variable (-> (-> tptp.variable Bool) tptp.set_variable)) % 0.45/0.94 (declare-const tptp.ord_le1407353162able_o (-> (-> tptp.variable Bool) (-> tptp.variable Bool) Bool)) % 0.45/0.94 (declare-const tptp.bot_bot_set_variable tptp.set_variable) % 0.45/0.94 (declare-const tptp.some_trm (-> tptp.trm tptp.option_trm)) % 0.45/0.94 (declare-const tptp.produc866613687on_trm (-> (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.char tptp.option_trm) tptp.produc1418842292n_game tptp.char tptp.option_trm)) % 0.45/0.94 (declare-const tptp.static_FVT (-> tptp.trm tptp.set_variable)) % 0.45/0.94 (declare-const tptp.const (-> tptp.char tptp.trm)) % 0.45/0.94 (declare-const tptp.produc2124676926on_fml (-> tptp.option_game tptp.option_fml tptp.produc1739631244on_fml)) % 0.45/0.94 (declare-const tptp.func (-> tptp.char tptp.trm tptp.trm)) % 0.45/0.94 (declare-const tptp.produc724717725on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.option_fml) tptp.produc1418842292n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc1903410526on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.option_fml) tptp.produc62062515n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc2129367017on_trm (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_trm) tptp.produc799602994n_game tptp.option_trm)) % 0.45/0.94 (declare-const tptp.produc1214549391on_trm (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_trm)) % 0.45/0.94 (declare-const tptp.uSubst516392818stappt (-> tptp.produc1418842292n_game tptp.set_variable tptp.trm tptp.option_trm)) % 0.45/0.94 (declare-const tptp.va tptp.set_variable) % 0.45/0.94 (declare-const tptp.produc1591622303on_fml (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_fml) tptp.produc799602994n_game tptp.option_fml)) % 0.45/0.94 (declare-const tptp.uSubst516392804stappf (-> tptp.produc1418842292n_game tptp.set_variable tptp.fml tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc377919108on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_fml) tptp.produc62062515n_game tptp.char tptp.option_fml)) % 0.45/0.94 (declare-const tptp.sigma tptp.produc1418842292n_game) % 0.45/0.94 (declare-const tptp.ua tptp.set_variable) % 0.45/0.94 (declare-const tptp.pred (-> tptp.char tptp.trm tptp.fml)) % 0.45/0.94 (declare-const tptp.uSubst1408967625substt (-> tptp.trm tptp.produc1418842292n_game)) % 0.45/0.94 (declare-const tptp.p tptp.char) % 0.45/0.94 (declare-const tptp.produc2141841102on_trm (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.char tptp.option_trm)) % 0.45/0.94 (declare-const tptp.theta tptp.trm) % 0.45/0.94 (declare-const tptp.vv (-> tptp.set_variable tptp.set_variable tptp.variable)) % 0.45/0.94 (declare-const tptp.vva (-> tptp.set_variable tptp.set_variable tptp.variable)) % 0.45/0.94 (declare-const tptp.some_fml (-> tptp.fml tptp.option_fml)) % 0.45/0.94 (declare-const tptp.geq (-> tptp.trm tptp.trm tptp.fml)) % 0.45/0.94 (declare-const tptp.produc293671592on_trm (-> (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.option_trm) tptp.produc62062515n_game tptp.option_trm)) % 0.45/0.94 (declare-const tptp.some_game (-> tptp.game tptp.option_game)) % 0.45/0.94 (declare-const tptp.static_FVF (-> tptp.fml tptp.set_variable)) % 0.45/0.94 (declare-const tptp.produc1598111045on_fml (-> (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_fml) tptp.produc799602994n_game tptp.char tptp.option_fml)) % 0.45/0.94 (declare-const tptp.uSubst152838031e_Geqo (-> tptp.option_trm tptp.option_trm tptp.option_fml)) % 0.45/0.94 (declare-const tptp.produc1278328899on_fml (-> (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.char tptp.option_fml) tptp.produc1418842292n_game tptp.char tptp.option_fml)) % 0.45/0.94 (define tptp.produc1250175341on_fml () (let ((_let_1 (@var "X" tptp.produc1418842292n_game))) (let ((_let_2 (@var "Y" tptp.char))) (let ((_let_3 (@var "R" tptp.produc62062515n_game))) (let ((_let_4 (@var "L" (-> tptp.char tptp.option_trm)))) (let ((_let_5 (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.char tptp.option_fml)))) (lambda (@list _let_5 _let_1 _let_2) (_ (_ tptp.produc1499310791on_fml (lambda (@list _let_4 _let_3) (_ (_ (_ _let_5 _let_4) _let_3) _let_2))) _let_1)))))))) % 0.45/0.94 (define tptp.produc1231571704on_trm () (let ((_let_1 (@var "X" tptp.produc62062515n_game))) (let ((_let_2 (@var "Y" tptp.char))) (let ((_let_3 (@var "R" tptp.produc799602994n_game))) (let ((_let_4 (@var "L" (-> tptp.char tptp.option_trm)))) (let ((_let_5 (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_trm)))) (lambda (@list _let_5 _let_1 _let_2) (_ (_ tptp.produc692578258on_trm (lambda (@list _let_4 _let_3) (_ (_ (_ _let_5 _let_4) _let_3) _let_2))) _let_1)))))))) % 0.45/0.94 (define tptp.produc1615133358on_fml () (let ((_let_1 (@var "X" tptp.produc62062515n_game))) (let ((_let_2 (@var "Y" tptp.char))) (let ((_let_3 (@var "R" tptp.produc799602994n_game))) (let ((_let_4 (@var "L" (-> tptp.char tptp.option_trm)))) (let ((_let_5 (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_fml)))) (lambda (@list _let_5 _let_1 _let_2) (_ (_ tptp.produc154833544on_fml (lambda (@list _let_4 _let_3) (_ (_ (_ _let_5 _let_4) _let_3) _let_2))) _let_1)))))))) % 0.45/0.94 (define tptp.produc1036610745on_trm () (let ((_let_1 (@var "X" tptp.produc799602994n_game))) (let ((_let_2 (@var "Y" tptp.char))) (let ((_let_3 (@var "R" (-> tptp.char tptp.option_game)))) (let ((_let_4 (@var "L" (-> tptp.char tptp.option_fml)))) (let ((_let_5 (@var "F" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_trm)))) (lambda (@list _let_5 _let_1 _let_2) (_ (_ tptp.produc885547027on_trm (lambda (@list _let_4 _let_3) (_ (_ (_ _let_5 _let_4) _let_3) _let_2))) _let_1)))))))) % 0.45/0.94 (define tptp.produc1420172399on_fml () (let ((_let_1 (@var "X" tptp.produc799602994n_game))) (let ((_let_2 (@var "Y" tptp.char))) (let ((_let_3 (@var "R" (-> tptp.char tptp.option_game)))) (let ((_let_4 (@var "L" (-> tptp.char tptp.option_fml)))) (let ((_let_5 (@var "F" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_fml)))) (lambda (@list _let_5 _let_1 _let_2) (_ (_ tptp.produc347802313on_fml (lambda (@list _let_4 _let_3) (_ (_ (_ _let_5 _let_4) _let_3) _let_2))) _let_1)))))))) % 0.45/0.94 (define tptp.case_option_o_game () (let ((_let_1 (@var "Option2" tptp.option_game))) (let ((_let_2 (@var "F23" (-> tptp.game Bool)))) (let ((_let_3 (= _let_1 tptp.none_game))) (let ((_let_4 (@var "F12" Bool))) (lambda (@list _let_4 _let_2 _let_1) (and (=> _let_3 _let_4) (=> (not _let_3) (_ _let_2 (_ tptp.the_game _let_1)))))))))) % 0.45/0.94 (define tptp.case_option_o_trm () (let ((_let_1 (@var "Option2" tptp.option_trm))) (let ((_let_2 (@var "F23" (-> tptp.trm Bool)))) (let ((_let_3 (= _let_1 tptp.none_trm))) (let ((_let_4 (@var "F12" Bool))) (lambda (@list _let_4 _let_2 _let_1) (and (=> _let_3 _let_4) (=> (not _let_3) (_ _let_2 (_ tptp.the_trm _let_1)))))))))) % 0.45/0.94 (define tptp.case_option_o_fml () (let ((_let_1 (@var "Option2" tptp.option_fml))) (let ((_let_2 (@var "F23" (-> tptp.fml Bool)))) (let ((_let_3 (= _let_1 tptp.none_fml))) (let ((_let_4 (@var "F12" Bool))) (lambda (@list _let_4 _let_2 _let_1) (and (=> _let_3 _let_4) (=> (not _let_3) (_ _let_2 (_ tptp.the_fml _let_1)))))))))) % 0.45/0.94 (define tptp.case_o209804997ml_fml () (let ((_let_1 (@var "Option2" tptp.option_fml))) (let ((_let_2 (@var "F23" (-> tptp.fml tptp.option_fml)))) (let ((_let_3 (@var "F12" tptp.option_fml))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.if_option_fml (= _let_1 tptp.none_fml)) _let_3) (_ _let_2 (_ tptp.the_fml _let_1)))))))) % 0.45/0.94 (define tptp.case_o325794063ml_trm () (let ((_let_1 (@var "Option2" tptp.option_trm))) (let ((_let_2 (@var "F23" (-> tptp.trm tptp.option_fml)))) (let ((_let_3 (@var "F12" tptp.option_fml))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.if_option_fml (= _let_1 tptp.none_trm)) _let_3) (_ _let_2 (_ tptp.the_trm _let_1)))))))) % 0.45/0.94 (define tptp.case_o487727941rm_trm () (let ((_let_1 (@var "Option2" tptp.option_trm))) (let ((_let_2 (@var "F23" (-> tptp.trm tptp.option_trm)))) (let ((_let_3 (@var "F12" tptp.option_trm))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ tptp.if_option_trm (= _let_1 tptp.none_trm)) _let_3) (_ _let_2 (_ tptp.the_trm _let_1)))))))) % 0.45/0.94 (define tptp.inf_inf_variable_o () (let ((_let_1 (@var "X" tptp.variable))) (let ((_let_2 (@var "G" (-> tptp.variable Bool)))) (let ((_let_3 (@var "F" (-> tptp.variable Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.inf_inf_o (_ _let_3 _let_1)) (_ _let_2 _let_1))))))) % 0.45/0.94 (define tptp.inf_inf_set_variable () (let ((_let_1 (@var "B4" tptp.set_variable))) (let ((_let_2 (@var "X" tptp.variable))) (let ((_let_3 (_ tptp.member_variable _let_2))) (let ((_let_4 (@list _let_2))) (let ((_let_5 (@var "A4" tptp.set_variable))) (lambda (@list _let_5 _let_1) (_ tptp.collect_variable (_ (_ tptp.inf_inf_variable_o (lambda _let_4 (_ _let_3 _let_5))) (lambda _let_4 (_ _let_3 _let_1))))))))))) % 0.45/0.94 (define tptp.ord_le282106107riable () (let ((_let_1 (@var "B4" tptp.set_variable))) (let ((_let_2 (@var "X" tptp.variable))) (let ((_let_3 (_ tptp.member_variable _let_2))) (let ((_let_4 (@list _let_2))) (let ((_let_5 (@var "A4" tptp.set_variable))) (lambda (@list _let_5 _let_1) (_ (_ tptp.ord_le1407353162able_o (lambda _let_4 (_ _let_3 _let_5))) (lambda _let_4 (_ _let_3 _let_1)))))))))) % 0.45/0.94 (define tptp.bot_bot_variable_o () (let ((_let_1 (@var "X" tptp.variable))) (lambda (@list _let_1) (_ (_ tptp.member_variable _let_1) tptp.bot_bot_set_variable)))) % 0.45/0.94 (define tptp.is_empty_variable () (let ((_let_1 (@var "A4" tptp.set_variable))) (lambda (@list _let_1) (= _let_1 tptp.bot_bot_set_variable)))) % 0.45/0.94 (define tptp.uSubst1559070963pconst () (let ((_let_1 (@var "F" tptp.char))) (let ((_let_2 (@var "Sigma2" tptp.produc1418842292n_game))) (let ((_let_3 (@var "__flatten_var_1" tptp.char))) (let ((_let_4 (@var "__flatten_var_0" tptp.produc62062515n_game))) (let ((_let_5 (@var "__flatten_var_0" tptp.produc799602994n_game))) (let ((_let_6 (@var "__flatten_var_0" tptp.char))) (let ((_let_7 (@var "F0" (-> tptp.char tptp.option_trm)))) (let ((_let_8 (@var "R" tptp.trm))) (let ((_let_9 (@var "U2" tptp.set_variable))) (lambda (@list _let_2 _let_9 _let_1) (_ (_ (_ tptp.case_o487727941rm_trm (_ tptp.some_trm (_ tptp.const _let_1))) (lambda (@list _let_8) (_ (_ (_ tptp.if_option_trm (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVT _let_8)) _let_9) tptp.bot_bot_set_variable)) (_ tptp.some_trm _let_8)) tptp.none_trm))) (_ (_ (_ tptp.produc866613687on_trm (lambda (@list _let_7 _let_4 _let_3) (_ (_ (_ tptp.produc1231571704on_trm (lambda (@list (@var "Uu" (-> tptp.char tptp.option_trm)) _let_5 _let_3) (_ (_ (_ tptp.produc1036610745on_trm (lambda (@list (@var "Uv" (-> tptp.char tptp.option_fml)) (@var "Uw" (-> tptp.char tptp.option_game)) _let_6) (_ _let_7 _let_6))) _let_5) _let_3))) _let_4) _let_3))) _let_2) _let_1))))))))))))) % 0.45/0.94 (define @t1 () (@var "V3" tptp.variable)) % 0.45/0.94 (define @t2 () (@var "X1" tptp.set_variable)) % 0.45/0.94 (define @t3 () (@var "X0" tptp.set_variable)) % 0.45/0.94 (define @t4 () (_ (_ tptp.vv @t3) @t2)) % 0.45/0.94 (define @t5 () (_ (_ tptp.member_variable @t1) @t3)) % 0.45/0.94 (define @t6 () (@list @t1)) % 0.45/0.94 (define @t7 () (@var "V2" tptp.variable)) % 0.45/0.94 (define @t8 () (_ tptp.pred tptp.p)) % 0.45/0.94 (define @t9 () (_ @t8 tptp.theta)) % 0.45/0.94 (define @t10 () (_ tptp.uSubst516392804stappf tptp.sigma)) % 0.45/0.94 (define @t11 () (_ @t10 tptp.ua)) % 0.45/0.94 (define @t12 () (_ @t11 @t9)) % 0.45/0.94 (define @t13 () (not (= @t12 tptp.none_fml))) % 0.45/0.94 (define @t14 () (@var "__flatten_var_1" tptp.char)) % 0.45/0.94 (define @t15 () (@var "__flatten_var_0" tptp.produc62062515n_game)) % 0.45/0.94 (define @t16 () (@var "__flatten_var_0" tptp.produc799602994n_game)) % 0.45/0.94 (define @t17 () (@var "__flatten_var_0" tptp.char)) % 0.45/0.94 (define @t18 () (@var "P" (-> tptp.char tptp.option_fml))) % 0.45/0.94 (define @t19 () (@var "Uw" (-> tptp.char tptp.option_game))) % 0.45/0.94 (define @t20 () (lambda (@list @t18 @t19 @t17) (_ @t18 @t17))) % 0.45/0.94 (define @t21 () (@list (@var "Uv" (-> tptp.char tptp.option_trm)) @t16 @t14)) % 0.45/0.94 (define @t22 () (lambda @t21 (_ (_ (_ tptp.produc1420172399on_fml @t20) @t16) @t14))) % 0.45/0.94 (define @t23 () (@var "Uu" (-> tptp.char tptp.option_trm))) % 0.45/0.94 (define @t24 () (@list @t23 @t15 @t14)) % 0.45/0.94 (define @t25 () (lambda @t24 (_ (_ (_ tptp.produc1615133358on_fml @t22) @t15) @t14))) % 0.45/0.94 (define @t26 () (_ tptp.produc1250175341on_fml @t25)) % 0.45/0.94 (define @t27 () (_ (_ @t26 tptp.sigma) tptp.p)) % 0.45/0.94 (define @t28 () (_ tptp.the_fml @t27)) % 0.45/0.94 (define @t29 () (_ tptp.uSubst516392818stappt tptp.sigma)) % 0.45/0.94 (define @t30 () (_ (_ @t29 tptp.va) tptp.theta)) % 0.45/0.94 (define @t31 () (_ tptp.the_trm @t30)) % 0.45/0.94 (define @t32 () (_ tptp.uSubst1408967625substt @t31)) % 0.45/0.94 (define @t33 () (_ tptp.uSubst516392804stappf @t32)) % 0.45/0.94 (define @t34 () (_ @t33 tptp.bot_bot_set_variable)) % 0.45/0.94 (define @t35 () (_ @t34 @t28)) % 0.45/0.94 (define @t36 () (= @t35 tptp.none_fml)) % 0.45/0.94 (define @t37 () (_ tptp.static_FVF @t28)) % 0.45/0.94 (define @t38 () (= (_ (_ tptp.inf_inf_set_variable @t37) tptp.va) tptp.bot_bot_set_variable)) % 0.45/0.94 (define @t39 () (=> @t38 @t36)) % 0.45/0.94 (define @t40 () (not @t39)) % 0.45/0.94 (define @t41 () (= @t27 tptp.none_fml)) % 0.45/0.94 (define @t42 () (_ @t10 tptp.va)) % 0.45/0.94 (define @t43 () (_ @t42 @t9)) % 0.45/0.94 (define @t44 () (= tptp.none_fml @t43)) % 0.45/0.94 (define @t45 () (not @t38)) % 0.45/0.94 (define @t46 () (=> @t45 @t44)) % 0.45/0.94 (define @t47 () (= @t35 @t43)) % 0.45/0.94 (define @t48 () (=> @t38 @t47)) % 0.45/0.94 (define @t49 () (and @t48 @t46)) % 0.45/0.94 (define @t50 () (not @t49)) % 0.45/0.94 (define @t51 () (=> @t50 @t41)) % 0.45/0.94 (define @t52 () (@var "Phi" tptp.fml)) % 0.45/0.94 (define @t53 () (@var "V" tptp.set_variable)) % 0.45/0.94 (define @t54 () (@var "Sigma" tptp.produc1418842292n_game)) % 0.45/0.94 (define @t55 () (_ tptp.uSubst516392804stappf @t54)) % 0.45/0.94 (define @t56 () (_ (_ @t55 @t53) @t52)) % 0.45/0.94 (define @t57 () (@var "U" tptp.set_variable)) % 0.45/0.94 (define @t58 () (_ @t55 @t57)) % 0.45/0.94 (define @t59 () (_ @t58 @t52)) % 0.45/0.94 (define @t60 () (= @t12 @t43)) % 0.45/0.94 (define @t61 () (=> @t41 @t60)) % 0.45/0.94 (define @t62 () (_ (_ tptp.vva tptp.va) @t37)) % 0.45/0.94 (define @t63 () (_ (_ tptp.vv tptp.va) @t37)) % 0.45/0.94 (define @t64 () (= @t63 @t62)) % 0.45/0.94 (define @t65 () (_ (_ tptp.member_variable @t62) tptp.va)) % 0.45/0.94 (define @t66 () (_ (_ tptp.member_variable @t63) @t37)) % 0.45/0.94 (define @t67 () (@var "Y12" tptp.trm)) % 0.45/0.94 (define @t68 () (@var "X12" tptp.trm)) % 0.45/0.94 (define @t69 () (@var "Y11" tptp.char)) % 0.45/0.94 (define @t70 () (@var "X11" tptp.char)) % 0.45/0.94 (define @t71 () (_ (_ tptp.pred @t70) @t68)) % 0.45/0.94 (define @t72 () (_ (_ @t29 tptp.ua) tptp.theta)) % 0.45/0.94 (define @t73 () (@var "V4" tptp.variable)) % 0.45/0.94 (define @t74 () (_ tptp.member_variable @t73)) % 0.45/0.94 (define @t75 () (@list @t73)) % 0.45/0.94 (define @t76 () (@var "Va" tptp.variable)) % 0.45/0.94 (define @t77 () (not (= @t73 @t76))) % 0.45/0.94 (define @t78 () (_ tptp.member_variable @t76)) % 0.45/0.94 (define @t79 () (@list @t76)) % 0.45/0.94 (define @t80 () (@var "Prod" tptp.produc799602994n_game)) % 0.45/0.94 (define @t81 () (@var "X2" (-> tptp.char tptp.option_game))) % 0.45/0.94 (define @t82 () (@var "X13" (-> tptp.char tptp.option_fml))) % 0.45/0.94 (define @t83 () (@var "F2" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_fml))) % 0.45/0.94 (define @t84 () (_ (_ @t83 @t82) @t81)) % 0.45/0.94 (define @t85 () (@var "H" (-> tptp.option_fml tptp.option_fml))) % 0.45/0.94 (define @t86 () (@list @t82 @t81)) % 0.45/0.94 (define @t87 () (_ (_ tptp.produc347802313on_fml @t83) @t80)) % 0.45/0.94 (define @t88 () (@var "H" (-> tptp.option_fml tptp.option_trm))) % 0.45/0.94 (define @t89 () (@var "F2" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.option_trm))) % 0.45/0.94 (define @t90 () (_ (_ @t89 @t82) @t81)) % 0.45/0.94 (define @t91 () (@var "H" (-> tptp.option_trm tptp.option_fml))) % 0.45/0.94 (define @t92 () (_ (_ tptp.produc885547027on_trm @t89) @t80)) % 0.45/0.94 (define @t93 () (@var "H" (-> tptp.option_trm tptp.option_trm))) % 0.45/0.94 (define @t94 () (@var "F2" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_trm))) % 0.45/0.94 (define @t95 () (_ (_ @t94 @t82) @t81)) % 0.45/0.94 (define @t96 () (@var "H" (-> (-> tptp.char tptp.option_trm) tptp.option_fml))) % 0.45/0.94 (define @t97 () (_ (_ tptp.produc1036610745on_trm @t94) @t80)) % 0.45/0.94 (define @t98 () (@var "H" (-> (-> tptp.char tptp.option_trm) tptp.option_trm))) % 0.45/0.94 (define @t99 () (@var "F2" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_fml))) % 0.45/0.94 (define @t100 () (_ (_ @t99 @t82) @t81)) % 0.45/0.94 (define @t101 () (@var "H" (-> (-> tptp.char tptp.option_fml) tptp.option_fml))) % 0.45/0.94 (define @t102 () (_ (_ tptp.produc1420172399on_fml @t99) @t80)) % 0.45/0.94 (define @t103 () (@var "H" (-> (-> tptp.char tptp.option_fml) tptp.option_trm))) % 0.45/0.94 (define @t104 () (@var "H" (-> tptp.option_fml tptp.char tptp.option_trm))) % 0.45/0.94 (define @t105 () (@list @t82 @t81 @t17)) % 0.45/0.94 (define @t106 () (@var "H" (-> tptp.option_fml tptp.char tptp.option_fml))) % 0.45/0.94 (define @t107 () (@var "Theta" tptp.trm)) % 0.45/0.94 (define @t108 () (@var "P2" tptp.char)) % 0.45/0.94 (define @t109 () (_ tptp.pred @t108)) % 0.45/0.94 (define @t110 () (_ @t58 (_ @t109 @t107))) % 0.45/0.94 (define @t111 () (= @t110 tptp.none_fml)) % 0.45/0.94 (define @t112 () (@var "R2" tptp.fml)) % 0.45/0.94 (define @t113 () (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVF @t112)) @t57) tptp.bot_bot_set_variable)) % 0.45/0.94 (define @t114 () (_ (_ @t26 @t54) @t108)) % 0.45/0.94 (define @t115 () (= @t114 (_ tptp.some_fml @t112))) % 0.45/0.94 (define @t116 () (@var "Za" tptp.option_fml)) % 0.45/0.94 (define @t117 () (@var "F3" (-> tptp.fml tptp.option_fml))) % 0.45/0.94 (define @t118 () (@var "Z" tptp.option_fml)) % 0.45/0.94 (define @t119 () (_ (_ (_ tptp.case_o209804997ml_fml @t118) @t117) @t116)) % 0.45/0.94 (define @t120 () (= @t116 tptp.none_fml)) % 0.45/0.94 (define @t121 () (@var "V5" tptp.set_variable)) % 0.45/0.94 (define @t122 () (@var "Va2" tptp.set_variable)) % 0.45/0.94 (define @t123 () (_ (_ tptp.vva @t122) @t121)) % 0.45/0.94 (define @t124 () (_ (_ tptp.vv @t122) @t121)) % 0.45/0.94 (define @t125 () (_ (_ tptp.member_variable @t124) @t121)) % 0.45/0.94 (define @t126 () (= (_ (_ tptp.inf_inf_set_variable @t121) @t122) tptp.bot_bot_set_variable)) % 0.45/0.94 (define @t127 () (or (not @t126) (forall @t75 (or (not (_ @t74 @t121)) (forall @t79 (or (not (_ @t78 @t122)) @t77)))))) % 0.45/0.94 (define @t128 () (@list @t121 @t122)) % 0.45/0.94 (define @t129 () (@var "Vva" (-> tptp.set_variable tptp.set_variable tptp.variable))) % 0.45/0.94 (define @t130 () (_ (_ @t129 @t122) @t121)) % 0.45/0.94 (define @t131 () (@var "Y2" tptp.fml)) % 0.45/0.94 (define @t132 () (@var "X22" tptp.fml)) % 0.45/0.94 (define @t133 () (_ tptp.some_fml @t132)) % 0.45/0.94 (define @t134 () (@var "Y2" tptp.trm)) % 0.45/0.94 (define @t135 () (@var "X22" tptp.trm)) % 0.45/0.94 (define @t136 () (_ tptp.some_trm @t135)) % 0.45/0.94 (define @t137 () (@var "Y2" tptp.game)) % 0.45/0.94 (define @t138 () (@var "X22" tptp.game)) % 0.45/0.94 (define @t139 () (_ tptp.some_game @t138)) % 0.45/0.94 (define @t140 () (@var "X3" tptp.option_fml)) % 0.45/0.94 (define @t141 () (= @t140 tptp.none_fml)) % 0.45/0.94 (define @t142 () (@var "Y" tptp.fml)) % 0.45/0.94 (define @t143 () (= @t140 (_ tptp.some_fml @t142))) % 0.45/0.94 (define @t144 () (@list @t142)) % 0.45/0.94 (define @t145 () (@list @t140)) % 0.45/0.94 (define @t146 () (@var "X3" tptp.option_trm)) % 0.45/0.94 (define @t147 () (= @t146 tptp.none_trm)) % 0.45/0.94 (define @t148 () (@var "Y" tptp.trm)) % 0.45/0.94 (define @t149 () (= @t146 (_ tptp.some_trm @t148))) % 0.45/0.94 (define @t150 () (@list @t148)) % 0.45/0.94 (define @t151 () (@list @t146)) % 0.45/0.94 (define @t152 () (@var "X3" tptp.option_game)) % 0.45/0.94 (define @t153 () (= @t152 tptp.none_game)) % 0.45/0.94 (define @t154 () (@var "Y" tptp.game)) % 0.45/0.94 (define @t155 () (= @t152 (_ tptp.some_game @t154))) % 0.45/0.94 (define @t156 () (@list @t154)) % 0.45/0.94 (define @t157 () (@list @t152)) % 0.45/0.94 (define @t158 () (@var "Option" tptp.option_fml)) % 0.45/0.94 (define @t159 () (_ tptp.the_fml @t158)) % 0.45/0.94 (define @t160 () (_ tptp.some_fml @t159)) % 0.45/0.94 (define @t161 () (= @t158 tptp.none_fml)) % 0.45/0.94 (define @t162 () (not @t161)) % 0.45/0.94 (define @t163 () (@list @t158)) % 0.45/0.94 (define @t164 () (@var "Option" tptp.option_trm)) % 0.45/0.94 (define @t165 () (_ tptp.the_trm @t164)) % 0.45/0.94 (define @t166 () (_ tptp.some_trm @t165)) % 0.45/0.94 (define @t167 () (= @t164 tptp.none_trm)) % 0.45/0.94 (define @t168 () (not @t167)) % 0.45/0.94 (define @t169 () (@list @t164)) % 0.45/0.94 (define @t170 () (@var "Option" tptp.option_game)) % 0.45/0.94 (define @t171 () (_ tptp.the_game @t170)) % 0.45/0.94 (define @t172 () (_ tptp.some_game @t171)) % 0.45/0.95 (define @t173 () (= @t170 tptp.none_game)) % 0.45/0.95 (define @t174 () (not @t173)) % 0.45/0.95 (define @t175 () (@list @t170)) % 0.45/0.95 (define @t176 () (@var "F22" (-> tptp.game Bool))) % 0.45/0.95 (define @t177 () (@var "F1" Bool)) % 0.45/0.95 (define @t178 () (_ (_ tptp.case_option_o_game @t177) @t176)) % 0.45/0.95 (define @t179 () (@var "F22" (-> tptp.trm Bool))) % 0.45/0.95 (define @t180 () (_ (_ tptp.case_option_o_trm @t177) @t179)) % 0.45/0.95 (define @t181 () (@var "F22" (-> tptp.fml Bool))) % 0.45/0.95 (define @t182 () (_ (_ tptp.case_option_o_fml @t177) @t181)) % 0.45/0.95 (define @t183 () (@var "F22" (-> tptp.fml tptp.option_fml))) % 0.45/0.95 (define @t184 () (@var "F1" tptp.option_fml)) % 0.45/0.95 (define @t185 () (_ (_ tptp.case_o209804997ml_fml @t184) @t183)) % 0.45/0.95 (define @t186 () (@var "F22" (-> tptp.trm tptp.option_fml))) % 0.45/0.95 (define @t187 () (_ (_ tptp.case_o325794063ml_trm @t184) @t186)) % 0.45/0.95 (define @t188 () (@var "F22" (-> tptp.trm tptp.option_trm))) % 0.45/0.95 (define @t189 () (@var "F1" tptp.option_trm)) % 0.45/0.95 (define @t190 () (_ (_ tptp.case_o487727941rm_trm @t189) @t188)) % 0.45/0.95 (define @t191 () (@list @t132)) % 0.45/0.95 (define @t192 () (@list @t135)) % 0.45/0.95 (define @t193 () (@list @t138)) % 0.45/0.95 (define @t194 () (@var "P3" (-> Bool Bool))) % 0.45/0.95 (define @t195 () (_ @t194 (_ @t176 @t171))) % 0.45/0.95 (define @t196 () (= @t170 @t172)) % 0.45/0.95 (define @t197 () (_ @t194 @t177)) % 0.45/0.95 (define @t198 () (_ @t178 @t170)) % 0.45/0.95 (define @t199 () (_ @t194 @t198)) % 0.45/0.95 (define @t200 () (@list @t194 @t177 @t176 @t170)) % 0.45/0.95 (define @t201 () (_ @t194 (_ @t179 @t165))) % 0.45/0.95 (define @t202 () (= @t164 @t166)) % 0.45/0.95 (define @t203 () (_ @t180 @t164)) % 0.45/0.95 (define @t204 () (_ @t194 @t203)) % 0.45/0.95 (define @t205 () (@list @t194 @t177 @t179 @t164)) % 0.45/0.95 (define @t206 () (_ @t194 (_ @t181 @t159))) % 0.45/0.95 (define @t207 () (= @t158 @t160)) % 0.45/0.95 (define @t208 () (_ @t182 @t158)) % 0.45/0.95 (define @t209 () (_ @t194 @t208)) % 0.45/0.95 (define @t210 () (@list @t194 @t177 @t181 @t158)) % 0.45/0.95 (define @t211 () (@var "P3" (-> tptp.option_fml Bool))) % 0.45/0.95 (define @t212 () (_ @t211 (_ @t183 @t159))) % 0.45/0.95 (define @t213 () (_ @t211 @t184)) % 0.45/0.95 (define @t214 () (_ @t185 @t158)) % 0.45/0.95 (define @t215 () (_ @t211 @t214)) % 0.45/0.95 (define @t216 () (@list @t211 @t184 @t183 @t158)) % 0.45/0.95 (define @t217 () (_ @t211 (_ @t186 @t165))) % 0.45/0.95 (define @t218 () (_ @t187 @t164)) % 0.45/0.95 (define @t219 () (_ @t211 @t218)) % 0.45/0.95 (define @t220 () (@list @t211 @t184 @t186 @t164)) % 0.45/0.95 (define @t221 () (@var "P3" (-> tptp.option_trm Bool))) % 0.45/0.95 (define @t222 () (_ @t221 (_ @t188 @t165))) % 0.45/0.95 (define @t223 () (_ @t221 @t189)) % 0.45/0.95 (define @t224 () (_ @t190 @t164)) % 0.45/0.95 (define @t225 () (_ @t221 @t224)) % 0.45/0.95 (define @t226 () (@list @t221 @t189 @t188 @t164)) % 0.45/0.95 (define @t227 () (@var "X" tptp.fml)) % 0.45/0.95 (define @t228 () (_ @t183 @t227)) % 0.45/0.95 (define @t229 () (@list @t227)) % 0.45/0.95 (define @t230 () (_ @t85 @t184)) % 0.45/0.95 (define @t231 () (@var "X" tptp.trm)) % 0.45/0.95 (define @t232 () (_ @t186 @t231)) % 0.45/0.95 (define @t233 () (@list @t231)) % 0.45/0.95 (define @t234 () (_ @t188 @t231)) % 0.45/0.95 (define @t235 () (@var "X" tptp.game)) % 0.45/0.95 (define @t236 () (@var "H" (-> Bool Bool))) % 0.45/0.95 (define @t237 () (@list @t235)) % 0.45/0.95 (define @t238 () (_ @t236 @t177)) % 0.45/0.95 (define @t239 () (@var "H" (-> tptp.option_fml Bool))) % 0.45/0.95 (define @t240 () (_ @t239 @t184)) % 0.45/0.95 (define @t241 () (not @t197)) % 0.45/0.95 (define @t242 () (not @t213)) % 0.45/0.95 (define @t243 () (_ tptp.uSubst516392818stappt @t54)) % 0.45/0.95 (define @t244 () (_ (_ @t243 @t53) @t107)) % 0.45/0.95 (define @t245 () (_ @t243 @t57)) % 0.45/0.95 (define @t246 () (_ @t245 @t107)) % 0.45/0.95 (define @t247 () (= @t246 @t244)) % 0.45/0.95 (define @t248 () (not (= @t246 tptp.none_trm))) % 0.45/0.95 (define @t249 () (@var "Y3" tptp.option_fml)) % 0.45/0.95 (define @t250 () (@var "P3" (-> tptp.option_fml tptp.option_fml Bool))) % 0.45/0.95 (define @t251 () (_ (_ @t250 @t140) @t249)) % 0.45/0.95 (define @t252 () (@var "B" tptp.fml)) % 0.45/0.95 (define @t253 () (= @t249 (_ tptp.some_fml @t252))) % 0.45/0.95 (define @t254 () (@var "A" tptp.fml)) % 0.45/0.95 (define @t255 () (= @t140 (_ tptp.some_fml @t254))) % 0.45/0.95 (define @t256 () (= @t249 tptp.none_fml)) % 0.45/0.95 (define @t257 () (@var "Y3" tptp.option_trm)) % 0.45/0.95 (define @t258 () (@var "P3" (-> tptp.option_fml tptp.option_trm Bool))) % 0.45/0.95 (define @t259 () (_ (_ @t258 @t140) @t257)) % 0.45/0.95 (define @t260 () (@var "B" tptp.trm)) % 0.45/0.95 (define @t261 () (= @t257 (_ tptp.some_trm @t260))) % 0.45/0.95 (define @t262 () (= @t257 tptp.none_trm)) % 0.45/0.95 (define @t263 () (@var "Y3" tptp.option_game)) % 0.45/0.95 (define @t264 () (@var "P3" (-> tptp.option_fml tptp.option_game Bool))) % 0.45/0.95 (define @t265 () (_ (_ @t264 @t140) @t263)) % 0.45/0.95 (define @t266 () (@var "B" tptp.game)) % 0.45/0.95 (define @t267 () (= @t263 (_ tptp.some_game @t266))) % 0.45/0.95 (define @t268 () (= @t263 tptp.none_game)) % 0.45/0.95 (define @t269 () (@var "P3" (-> tptp.option_trm tptp.option_fml Bool))) % 0.45/0.95 (define @t270 () (_ (_ @t269 @t146) @t249)) % 0.45/0.95 (define @t271 () (@var "A" tptp.trm)) % 0.45/0.95 (define @t272 () (= @t146 (_ tptp.some_trm @t271))) % 0.45/0.95 (define @t273 () (@var "P3" (-> tptp.option_trm tptp.option_trm Bool))) % 0.45/0.95 (define @t274 () (_ (_ @t273 @t146) @t257)) % 0.45/0.95 (define @t275 () (@var "P3" (-> tptp.option_trm tptp.option_game Bool))) % 0.45/0.95 (define @t276 () (_ (_ @t275 @t146) @t263)) % 0.45/0.95 (define @t277 () (@var "P3" (-> tptp.option_game tptp.option_fml Bool))) % 0.45/0.95 (define @t278 () (_ (_ @t277 @t152) @t249)) % 0.45/0.95 (define @t279 () (@var "A" tptp.game)) % 0.45/0.95 (define @t280 () (= @t152 (_ tptp.some_game @t279))) % 0.45/0.95 (define @t281 () (@var "P3" (-> tptp.option_game tptp.option_trm Bool))) % 0.45/0.95 (define @t282 () (_ (_ @t281 @t152) @t257)) % 0.45/0.95 (define @t283 () (@var "P3" (-> tptp.option_game tptp.option_game Bool))) % 0.45/0.95 (define @t284 () (_ (_ @t283 @t152) @t263)) % 0.45/0.95 (define @t285 () (@var "P" (-> tptp.option_fml Bool))) % 0.45/0.95 (define @t286 () (_ @t285 (_ tptp.some_fml @t227))) % 0.45/0.95 (define @t287 () (_ @t285 tptp.none_fml)) % 0.45/0.95 (define @t288 () (@list @t285)) % 0.45/0.95 (define @t289 () (@var "X4" tptp.option_fml)) % 0.45/0.95 (define @t290 () (@var "P4" (-> tptp.option_fml Bool))) % 0.45/0.95 (define @t291 () (_ @t290 @t289)) % 0.45/0.95 (define @t292 () (@list @t289)) % 0.45/0.95 (define @t293 () (@list @t290)) % 0.45/0.95 (define @t294 () (@var "P" (-> tptp.option_trm Bool))) % 0.45/0.95 (define @t295 () (_ @t294 (_ tptp.some_trm @t231))) % 0.45/0.95 (define @t296 () (_ @t294 tptp.none_trm)) % 0.45/0.95 (define @t297 () (@list @t294)) % 0.45/0.95 (define @t298 () (@var "X4" tptp.option_trm)) % 0.45/0.95 (define @t299 () (@var "P4" (-> tptp.option_trm Bool))) % 0.45/0.95 (define @t300 () (_ @t299 @t298)) % 0.45/0.95 (define @t301 () (@list @t298)) % 0.45/0.95 (define @t302 () (@list @t299)) % 0.45/0.95 (define @t303 () (@var "P" (-> tptp.option_game Bool))) % 0.45/0.95 (define @t304 () (_ @t303 (_ tptp.some_game @t235))) % 0.45/0.95 (define @t305 () (_ @t303 tptp.none_game)) % 0.45/0.95 (define @t306 () (@list @t303)) % 0.45/0.95 (define @t307 () (@var "X4" tptp.option_game)) % 0.45/0.95 (define @t308 () (@var "P4" (-> tptp.option_game Bool))) % 0.45/0.95 (define @t309 () (_ @t308 @t307)) % 0.45/0.95 (define @t310 () (@list @t307)) % 0.45/0.95 (define @t311 () (@list @t308)) % 0.45/0.95 (define @t312 () (@var "X5" tptp.fml)) % 0.45/0.95 (define @t313 () (_ @t211 tptp.none_fml)) % 0.45/0.95 (define @t314 () (@var "X5" tptp.trm)) % 0.45/0.95 (define @t315 () (_ @t221 tptp.none_trm)) % 0.45/0.95 (define @t316 () (@var "P3" (-> tptp.option_game Bool))) % 0.45/0.95 (define @t317 () (@var "X5" tptp.game)) % 0.45/0.95 (define @t318 () (_ @t316 tptp.none_game)) % 0.45/0.95 (define @t319 () (@var "X23" tptp.fml)) % 0.45/0.95 (define @t320 () (not @t256)) % 0.45/0.95 (define @t321 () (@var "X23" tptp.trm)) % 0.45/0.95 (define @t322 () (@var "X23" tptp.game)) % 0.45/0.95 (define @t323 () (@var "A1" tptp.option_fml)) % 0.45/0.95 (define @t324 () (@var "A0" tptp.variable)) % 0.45/0.95 (define @t325 () (@var "P3" (-> tptp.variable tptp.option_fml Bool))) % 0.45/0.95 (define @t326 () (@var "X5" tptp.variable)) % 0.45/0.95 (define @t327 () (_ @t325 @t326)) % 0.45/0.95 (define @t328 () (@list @t326)) % 0.45/0.95 (define @t329 () (@var "Phi2" tptp.fml)) % 0.45/0.95 (define @t330 () (_ tptp.some_fml @t329)) % 0.45/0.95 (define @t331 () (@var "F" tptp.fml)) % 0.45/0.95 (define @t332 () (@var "Phi" tptp.option_fml)) % 0.45/0.95 (define @t333 () (@list @t331)) % 0.45/0.95 (define @t334 () (@var "A0" tptp.option_fml)) % 0.45/0.95 (define @t335 () (@list @t329)) % 0.45/0.95 (define @t336 () (@var "A2" tptp.variable)) % 0.45/0.95 (define @t337 () (@var "P3" (-> tptp.variable Bool))) % 0.45/0.95 (define @t338 () (_ tptp.collect_variable @t337)) % 0.45/0.95 (define @t339 () (_ tptp.member_variable @t336)) % 0.45/0.95 (define @t340 () (@var "A3" tptp.set_variable)) % 0.45/0.95 (define @t341 () (@var "X" tptp.variable)) % 0.45/0.95 (define @t342 () (_ tptp.member_variable @t341)) % 0.45/0.95 (define @t343 () (_ @t342 @t340)) % 0.45/0.95 (define @t344 () (@list @t341)) % 0.45/0.95 (define @t345 () (@list @t340)) % 0.45/0.95 (define @t346 () (@var "Q" (-> tptp.variable Bool))) % 0.45/0.95 (define @t347 () (_ tptp.collect_variable @t346)) % 0.45/0.95 (define @t348 () (_ @t346 @t326)) % 0.45/0.95 (define @t349 () (_ @t337 @t326)) % 0.45/0.95 (define @t350 () (@list @t337 @t346)) % 0.45/0.95 (define @t351 () (@var "V6" tptp.fml)) % 0.45/0.95 (define @t352 () (@var "X_1" tptp.option_fml)) % 0.45/0.95 (define @t353 () (@list @t352)) % 0.45/0.95 (define @t354 () (@var "Psi" tptp.fml)) % 0.45/0.95 (define @t355 () (@var "Option3" tptp.option_fml)) % 0.45/0.95 (define @t356 () (= @t355 tptp.none_fml)) % 0.45/0.95 (define @t357 () (@var "Option3" tptp.option_trm)) % 0.45/0.95 (define @t358 () (= @t357 tptp.none_trm)) % 0.45/0.95 (define @t359 () (@var "Option3" tptp.option_game)) % 0.45/0.95 (define @t360 () (= @t359 tptp.none_game)) % 0.45/0.95 (define @t361 () (@var "R3" tptp.fml)) % 0.45/0.95 (define @t362 () (@list @t54 @t57 @t108 @t107)) % 0.45/0.95 (define @t363 () (_ tptp.the_trm @t72)) % 0.45/0.95 (define @t364 () (_ tptp.if_option_fml (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVF @t331)) tptp.ua) tptp.bot_bot_set_variable))) % 0.45/0.95 (define @t365 () (@var "T" tptp.trm)) % 0.45/0.95 (define @t366 () (@list @t365)) % 0.45/0.95 (define @t367 () (_ tptp.case_o325794063ml_trm tptp.none_fml)) % 0.45/0.95 (define @t368 () (_ (_ @t367 (lambda @t366 (_ (_ (_ tptp.case_o209804997ml_fml (_ tptp.some_fml (_ @t8 @t365))) (lambda @t333 (_ (_ @t364 (_ (_ (_ tptp.uSubst516392804stappf (_ tptp.uSubst1408967625substt @t365)) tptp.bot_bot_set_variable) @t331)) tptp.none_fml))) @t27))) @t72)) % 0.45/0.95 (define @t369 () (@var "R" tptp.fml)) % 0.45/0.95 (define @t370 () (@var "Sigma_theta" tptp.trm)) % 0.45/0.95 (define @t371 () (_ tptp.uSubst1408967625substt @t370)) % 0.45/0.95 (define @t372 () (@list @t370)) % 0.45/0.95 (define @t373 () (@var "B2" tptp.set_variable)) % 0.45/0.95 (define @t374 () (@var "C" tptp.set_variable)) % 0.45/0.95 (define @t375 () (_ tptp.ord_le282106107riable @t374)) % 0.45/0.95 (define @t376 () (_ @t375 @t373)) % 0.45/0.95 (define @t377 () (_ @t375 @t340)) % 0.45/0.95 (define @t378 () (_ tptp.inf_inf_set_variable @t340)) % 0.45/0.95 (define @t379 () (_ @t378 @t373)) % 0.45/0.95 (define @t380 () (_ @t375 @t379)) % 0.45/0.95 (define @t381 () (@list @t374 @t340 @t373)) % 0.45/0.95 (define @t382 () (@var "X3" (-> tptp.variable Bool))) % 0.45/0.95 (define @t383 () (@list @t382)) % 0.45/0.95 (define @t384 () (@var "X3" tptp.set_variable)) % 0.45/0.95 (define @t385 () (_ tptp.inf_inf_set_variable tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t386 () (@list @t384)) % 0.45/0.95 (define @t387 () (_ tptp.inf_inf_variable_o @t382)) % 0.45/0.95 (define @t388 () (_ tptp.inf_inf_set_variable @t384)) % 0.45/0.95 (define @t389 () (= @t340 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t390 () (_ tptp.ord_le282106107riable @t340)) % 0.45/0.95 (define @t391 () (_ @t390 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t392 () (_ tptp.ord_le282106107riable tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t393 () (@var "Z2" (-> tptp.variable Bool))) % 0.45/0.95 (define @t394 () (_ tptp.ord_le1407353162able_o @t382)) % 0.45/0.95 (define @t395 () (@var "Y3" (-> tptp.variable Bool))) % 0.45/0.95 (define @t396 () (_ tptp.inf_inf_variable_o @t395)) % 0.45/0.95 (define @t397 () (_ @t396 @t393)) % 0.45/0.95 (define @t398 () (@list @t382 @t395 @t393)) % 0.45/0.95 (define @t399 () (@var "Z2" tptp.set_variable)) % 0.45/0.95 (define @t400 () (_ tptp.ord_le282106107riable @t384)) % 0.45/0.95 (define @t401 () (_ @t400 @t399)) % 0.45/0.95 (define @t402 () (@var "Y3" tptp.set_variable)) % 0.45/0.95 (define @t403 () (_ @t400 @t402)) % 0.45/0.95 (define @t404 () (_ tptp.inf_inf_set_variable @t402)) % 0.45/0.95 (define @t405 () (_ @t404 @t399)) % 0.45/0.95 (define @t406 () (_ @t400 @t405)) % 0.45/0.95 (define @t407 () (@list @t384 @t402 @t399)) % 0.45/0.95 (define @t408 () (@var "C2" (-> tptp.variable Bool))) % 0.45/0.95 (define @t409 () (@var "A2" (-> tptp.variable Bool))) % 0.45/0.95 (define @t410 () (_ tptp.ord_le1407353162able_o @t409)) % 0.45/0.95 (define @t411 () (@var "B3" (-> tptp.variable Bool))) % 0.45/0.95 (define @t412 () (_ tptp.inf_inf_variable_o @t411)) % 0.45/0.95 (define @t413 () (_ @t412 @t408)) % 0.45/0.95 (define @t414 () (@list @t409 @t411 @t408)) % 0.45/0.95 (define @t415 () (@var "C2" tptp.set_variable)) % 0.45/0.95 (define @t416 () (@var "A2" tptp.set_variable)) % 0.45/0.95 (define @t417 () (_ tptp.ord_le282106107riable @t416)) % 0.45/0.95 (define @t418 () (_ @t417 @t415)) % 0.45/0.95 (define @t419 () (@var "B3" tptp.set_variable)) % 0.45/0.95 (define @t420 () (_ @t417 @t419)) % 0.45/0.95 (define @t421 () (_ tptp.inf_inf_set_variable @t419)) % 0.45/0.95 (define @t422 () (_ @t421 @t415)) % 0.45/0.95 (define @t423 () (_ @t417 @t422)) % 0.45/0.95 (define @t424 () (@list @t416 @t419 @t415)) % 0.45/0.95 (define @t425 () (@var "Za" tptp.option_trm)) % 0.45/0.95 (define @t426 () (@var "F3" (-> tptp.trm tptp.option_fml))) % 0.45/0.95 (define @t427 () (_ (_ (_ tptp.case_o325794063ml_trm @t118) @t426) @t425)) % 0.45/0.95 (define @t428 () (= @t425 tptp.none_trm)) % 0.45/0.95 (define @t429 () (_ @t337 @t341)) % 0.45/0.95 (define @t430 () (forall @t344 (not @t429))) % 0.45/0.95 (define @t431 () (@list @t337)) % 0.45/0.95 (define @t432 () (= @t338 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t433 () (@var "C2" tptp.variable)) % 0.45/0.95 (define @t434 () (_ tptp.member_variable @t433)) % 0.45/0.95 (define @t435 () (= @t340 @t373)) % 0.45/0.95 (define @t436 () (_ tptp.ord_le282106107riable @t373)) % 0.45/0.95 (define @t437 () (_ @t436 @t340)) % 0.45/0.95 (define @t438 () (_ @t390 @t373)) % 0.45/0.95 (define @t439 () (@list @t340 @t373)) % 0.45/0.95 (define @t440 () (_ tptp.member_variable @t326)) % 0.45/0.95 (define @t441 () (_ @t440 @t373)) % 0.45/0.95 (define @t442 () (_ @t440 @t340)) % 0.45/0.95 (define @t443 () (_ @t387 @t395)) % 0.45/0.95 (define @t444 () (_ tptp.inf_inf_variable_o @t443)) % 0.45/0.95 (define @t445 () (@list @t382 @t395)) % 0.45/0.95 (define @t446 () (_ @t388 @t402)) % 0.45/0.95 (define @t447 () (_ tptp.inf_inf_set_variable @t446)) % 0.45/0.95 (define @t448 () (@list @t384 @t402)) % 0.45/0.95 (define @t449 () (_ tptp.inf_inf_variable_o @t409)) % 0.45/0.95 (define @t450 () (_ @t449 @t411)) % 0.45/0.95 (define @t451 () (_ tptp.inf_inf_variable_o @t450)) % 0.45/0.95 (define @t452 () (@list @t409 @t411)) % 0.45/0.95 (define @t453 () (_ tptp.inf_inf_set_variable @t416)) % 0.45/0.95 (define @t454 () (_ @t453 @t419)) % 0.45/0.95 (define @t455 () (_ tptp.inf_inf_set_variable @t454)) % 0.45/0.95 (define @t456 () (@list @t416 @t419)) % 0.45/0.95 (define @t457 () (@list @t416)) % 0.45/0.95 (define @t458 () (_ @t434 @t373)) % 0.45/0.95 (define @t459 () (_ @t434 @t340)) % 0.45/0.95 (define @t460 () (_ @t434 @t379)) % 0.45/0.95 (define @t461 () (@list @t433 @t340 @t373)) % 0.45/0.95 (define @t462 () (@var "Sigma_theta2" tptp.trm)) % 0.45/0.95 (define @t463 () (_ tptp.uSubst1408967625substt @t462)) % 0.45/0.95 (define @t464 () (= @t246 (_ tptp.some_trm @t462))) % 0.45/0.95 (define @t465 () (@var "A1" tptp.option_trm)) % 0.45/0.95 (define @t466 () (@var "A0" tptp.char)) % 0.45/0.95 (define @t467 () (@var "P3" (-> tptp.char tptp.option_trm Bool))) % 0.45/0.95 (define @t468 () (@var "X5" tptp.char)) % 0.45/0.95 (define @t469 () (_ @t467 @t468)) % 0.45/0.95 (define @t470 () (@var "Theta2" tptp.trm)) % 0.45/0.95 (define @t471 () (_ tptp.some_trm @t470)) % 0.45/0.95 (define @t472 () (@var "Theta" tptp.option_trm)) % 0.45/0.95 (define @t473 () (= @t472 tptp.none_trm)) % 0.45/0.95 (define @t474 () (@var "A0" tptp.option_trm)) % 0.45/0.95 (define @t475 () (@var "V6" tptp.trm)) % 0.45/0.95 (define @t476 () (_ tptp.some_trm @t475)) % 0.45/0.95 (define @t477 () (@list @t475)) % 0.45/0.95 (define @t478 () (@var "X_1" tptp.option_trm)) % 0.45/0.95 (define @t479 () (@var "Eta" tptp.trm)) % 0.45/0.95 (define @t480 () (_ tptp.some_trm @t479)) % 0.45/0.95 (define @t481 () (@var "P3" (-> tptp.variable tptp.option_trm Bool))) % 0.45/0.95 (define @t482 () (_ @t481 @t326)) % 0.45/0.95 (define @t483 () (= @t146 @t471)) % 0.45/0.95 (define @t484 () (@list @t470)) % 0.45/0.95 (define @t485 () (@list (@var "Uu" tptp.fml))) % 0.45/0.95 (define @t486 () (@list (@var "Uu" tptp.trm))) % 0.45/0.95 (define @t487 () (@list (@var "Uu" tptp.game))) % 0.45/0.95 (define @t488 () (@var "A0" tptp.option_game)) % 0.45/0.95 (define @t489 () (@var "V6" tptp.game)) % 0.45/0.95 (define @t490 () (_ tptp.some_game @t489)) % 0.45/0.95 (define @t491 () (@list @t489)) % 0.45/0.95 (define @t492 () (@var "Alpha" tptp.game)) % 0.45/0.95 (define @t493 () (_ tptp.some_game @t492)) % 0.45/0.95 (define @t494 () (@list @t492 @t329)) % 0.45/0.95 (define @t495 () (@var "Y4" tptp.fml)) % 0.45/0.95 (define @t496 () (@var "Q" (-> tptp.fml Bool))) % 0.45/0.95 (define @t497 () (@var "P3" Bool)) % 0.45/0.95 (define @t498 () (not @t497)) % 0.45/0.95 (define @t499 () (_ (_ (_ tptp.case_option_o_fml @t497) @t496) @t140)) % 0.45/0.95 (define @t500 () (@var "Y4" tptp.trm)) % 0.45/0.95 (define @t501 () (@var "Q" (-> tptp.trm Bool))) % 0.45/0.95 (define @t502 () (_ (_ (_ tptp.case_option_o_trm @t497) @t501) @t146)) % 0.45/0.95 (define @t503 () (@var "Y4" tptp.game)) % 0.45/0.95 (define @t504 () (@var "Q" (-> tptp.game Bool))) % 0.45/0.95 (define @t505 () (@var "Y4" tptp.variable)) % 0.45/0.95 (define @t506 () (_ @t346 @t341)) % 0.45/0.95 (define @t507 () (_ (_ tptp.ord_le282106107riable @t338) @t347)) % 0.45/0.95 (define @t508 () (@var "A4" tptp.set_variable)) % 0.45/0.95 (define @t509 () (@var "B4" tptp.set_variable)) % 0.45/0.95 (define @t510 () (@list @t508 @t509)) % 0.45/0.95 (define @t511 () (@var "Z3" tptp.set_variable)) % 0.45/0.95 (define @t512 () (@var "Y5" tptp.set_variable)) % 0.45/0.95 (define @t513 () (lambda (@list @t512 @t511) (= @t512 @t511))) % 0.45/0.95 (define @t514 () (_ @t390 @t374)) % 0.45/0.95 (define @t515 () (@list @t340 @t373 @t374)) % 0.45/0.95 (define @t516 () (=> @t349 @t348)) % 0.45/0.95 (define @t517 () (@var "T" tptp.variable)) % 0.45/0.95 (define @t518 () (_ tptp.member_variable @t517)) % 0.45/0.95 (define @t519 () (_ @t342 @t509)) % 0.45/0.95 (define @t520 () (_ @t342 @t508)) % 0.45/0.95 (define @t521 () (@var "X3" tptp.variable)) % 0.45/0.95 (define @t522 () (_ tptp.member_variable @t521)) % 0.45/0.95 (define @t523 () (_ @t522 @t340)) % 0.45/0.95 (define @t524 () (_ @t387 @t397)) % 0.45/0.95 (define @t525 () (_ @t388 @t405)) % 0.45/0.95 (define @t526 () (_ @t449 @t413)) % 0.45/0.95 (define @t527 () (_ @t453 @t422)) % 0.45/0.95 (define @t528 () (@list @t419 @t416 @t415)) % 0.45/0.95 (define @t529 () (@var "__flatten_var_0" tptp.variable)) % 0.45/0.95 (define @t530 () (@var "X" (-> tptp.variable Bool))) % 0.45/0.95 (define @t531 () (@var "Y" (-> tptp.variable Bool))) % 0.45/0.95 (define @t532 () (@var "X" tptp.set_variable)) % 0.45/0.95 (define @t533 () (@var "Y" tptp.set_variable)) % 0.45/0.95 (define @t534 () (@list @t532 @t533)) % 0.45/0.95 (define @t535 () (@var "A5" (-> tptp.variable Bool))) % 0.45/0.95 (define @t536 () (@var "B5" (-> tptp.variable Bool))) % 0.45/0.95 (define @t537 () (@var "A5" tptp.set_variable)) % 0.45/0.95 (define @t538 () (@var "B5" tptp.set_variable)) % 0.45/0.95 (define @t539 () (@list @t537 @t538)) % 0.45/0.95 (define @t540 () (@var "K" (-> tptp.variable Bool))) % 0.45/0.95 (define @t541 () (_ tptp.inf_inf_variable_o @t540)) % 0.45/0.95 (define @t542 () (_ @t541 @t450)) % 0.45/0.95 (define @t543 () (@var "B2" (-> tptp.variable Bool))) % 0.45/0.95 (define @t544 () (@var "K" tptp.set_variable)) % 0.45/0.95 (define @t545 () (_ tptp.inf_inf_set_variable @t544)) % 0.45/0.95 (define @t546 () (_ @t545 @t454)) % 0.45/0.95 (define @t547 () (@var "A3" (-> tptp.variable Bool))) % 0.45/0.95 (define @t548 () (_ tptp.inf_inf_set_variable @t373)) % 0.45/0.95 (define @t549 () (_ @t378 (_ @t548 @t374))) % 0.45/0.95 (define @t550 () (lambda @t344 false)) % 0.45/0.95 (define @t551 () (= tptp.bot_bot_set_variable (_ tptp.collect_variable @t550))) % 0.45/0.95 (define @t552 () (_ tptp.collect_variable (lambda @t344 (and @t343 @t429)))) % 0.45/0.95 (define @t553 () (_ @t337 @t521)) % 0.45/0.95 (define @t554 () (_ @t378 @t338)) % 0.45/0.95 (define @t555 () (_ tptp.collect_variable (lambda @t344 (and @t429 @t506)))) % 0.45/0.95 (define @t556 () (_ tptp.ord_le282106107riable @t454)) % 0.45/0.95 (define @t557 () (_ @t556 @t415)) % 0.45/0.95 (define @t558 () (_ tptp.ord_le282106107riable @t419)) % 0.45/0.95 (define @t559 () (_ @t558 @t415)) % 0.45/0.95 (define @t560 () (_ (_ tptp.inf_inf_set_variable @t537) @t538)) % 0.45/0.95 (define @t561 () (_ tptp.ord_le282106107riable @t402)) % 0.45/0.95 (define @t562 () (_ @t561 @t384)) % 0.45/0.95 (define @t563 () (@list @t402 @t384)) % 0.45/0.95 (define @t564 () (_ @t558 @t416)) % 0.45/0.95 (define @t565 () (@list @t419 @t416)) % 0.45/0.95 (define @t566 () (@var "F2" (-> tptp.set_variable tptp.set_variable tptp.set_variable))) % 0.45/0.95 (define @t567 () (@var "Z4" tptp.set_variable)) % 0.45/0.95 (define @t568 () (@var "Y4" tptp.set_variable)) % 0.45/0.95 (define @t569 () (@var "X5" tptp.set_variable)) % 0.45/0.95 (define @t570 () (_ tptp.ord_le282106107riable @t569)) % 0.45/0.95 (define @t571 () (_ @t570 @t568)) % 0.45/0.95 (define @t572 () (_ tptp.ord_le282106107riable (_ (_ @t566 @t569) @t568))) % 0.45/0.95 (define @t573 () (@list @t569 @t568)) % 0.45/0.95 (define @t574 () (= @t416 @t454)) % 0.45/0.95 (define @t575 () (_ @t556 @t384)) % 0.45/0.95 (define @t576 () (@var "D" tptp.set_variable)) % 0.45/0.95 (define @t577 () (_ @t400 @t454)) % 0.45/0.95 (define @t578 () (_ @t400 @t419)) % 0.45/0.95 (define @t579 () (_ @t400 @t416)) % 0.45/0.95 (define @t580 () (@list @t384 @t416 @t419)) % 0.45/0.95 (define @t581 () (_ tptp.ord_le282106107riable @t446)) % 0.45/0.95 (define @t582 () (@var "Y" tptp.variable)) % 0.45/0.95 (define @t583 () (= @t379 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t584 () (_ @t342 @t373)) % 0.45/0.95 (define @t585 () (_ tptp.ord_le282106107riable @t379)) % 0.45/0.95 (define @t586 () (@var "D2" tptp.set_variable)) % 0.45/0.95 (define @t587 () (= @t416 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t588 () (_ @t417 tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t589 () (@var "Eta2" tptp.trm)) % 0.45/0.95 (define @t590 () (_ @t245 @t589)) % 0.45/0.95 (define @t591 () (_ (_ tptp.geq @t107) @t589)) % 0.45/0.95 (define @t592 () (_ @t58 @t591)) % 0.45/0.95 (define @t593 () (= @t592 (_ tptp.some_fml (_ (_ tptp.geq (_ tptp.the_trm @t246)) (_ tptp.the_trm @t590))))) % 0.45/0.95 (define @t594 () (not (= @t592 tptp.none_fml))) % 0.45/0.95 (define @t595 () (@list @t54 @t57 @t107 @t589)) % 0.45/0.95 (define @t596 () (@var "Y22" tptp.trm)) % 0.45/0.95 (define @t597 () (@var "X222" tptp.trm)) % 0.45/0.95 (define @t598 () (@var "Y21" tptp.trm)) % 0.45/0.95 (define @t599 () (@var "X21" tptp.trm)) % 0.45/0.95 (define @t600 () (_ (_ tptp.geq @t599) @t597)) % 0.45/0.95 (define @t601 () (@list @t492)) % 0.45/0.95 (define @t602 () (@var "G" tptp.game)) % 0.45/0.95 (define @t603 () (@var "Alpha2" tptp.option_game)) % 0.45/0.95 (define @t604 () (@var "A1" tptp.option_game)) % 0.45/0.95 (define @t605 () (@var "Alpha" tptp.option_game)) % 0.45/0.95 (define @t606 () (@var "Beta" tptp.game)) % 0.45/0.95 (define @t607 () (@var "F2" (-> tptp.set_variable tptp.set_variable))) % 0.45/0.95 (define @t608 () (forall @t573 (=> @t571 (_ (_ tptp.ord_le282106107riable (_ @t607 @t569)) (_ @t607 @t568))))) % 0.45/0.95 (define @t609 () (=> @t559 (=> @t608 (_ @t417 (_ @t607 @t415))))) % 0.45/0.95 (define @t610 () (_ @t607 @t419)) % 0.45/0.95 (define @t611 () (@list @t416 @t607 @t419 @t415)) % 0.45/0.95 (define @t612 () (=> @t608 (_ (_ tptp.ord_le282106107riable (_ @t607 @t416)) @t415))) % 0.45/0.95 (define @t613 () (@list @t416 @t419 @t607 @t415)) % 0.45/0.95 (define @t614 () (= @t384 @t402)) % 0.45/0.95 (define @t615 () (=> @t559 @t418)) % 0.45/0.95 (define @t616 () (_ (_ tptp.ord_le282106107riable @t538) @t537)) % 0.45/0.95 (define @t617 () (_ (_ tptp.ord_le282106107riable @t537) @t538)) % 0.45/0.95 (define @t618 () (= @t416 @t419)) % 0.45/0.95 (define @t619 () (_ tptp.ord_le282106107riable @t415)) % 0.45/0.95 (define @t620 () (@var "X6" tptp.set_variable)) % 0.45/0.95 (define @t621 () (_ tptp.collect_variable (lambda @t344 (and (_ @t342 @t620) @t429)))) % 0.45/0.95 (define @t622 () (@var "Z5" tptp.set_variable)) % 0.45/0.95 (define @t623 () (not (= @t590 tptp.none_trm))) % 0.45/0.95 (define @t624 () (@var "G2" (-> tptp.fml tptp.option_fml))) % 0.45/0.95 (define @t625 () (@var "F2" tptp.option_fml)) % 0.45/0.95 (define @t626 () (@var "R4" (-> tptp.option_fml Bool))) % 0.45/0.95 (define @t627 () (@var "Q2" tptp.fml)) % 0.45/0.95 (define @t628 () (=> @t497 (_ @t626 @t625))) % 0.45/0.95 (define @t629 () (@var "G2" (-> tptp.trm tptp.option_fml))) % 0.45/0.95 (define @t630 () (@var "Q2" tptp.trm)) % 0.45/0.95 (define @t631 () (_ @t501 @t630)) % 0.45/0.95 (define @t632 () (@list @t630)) % 0.45/0.95 (define @t633 () (@var "G2" (-> tptp.trm tptp.option_trm))) % 0.45/0.95 (define @t634 () (@var "F2" tptp.option_trm)) % 0.45/0.95 (define @t635 () (@var "R4" (-> tptp.option_trm Bool))) % 0.45/0.95 (define @t636 () (@var "Xa" tptp.option_trm)) % 0.45/0.95 (define @t637 () (@var "S" tptp.set_variable)) % 0.45/0.95 (define @t638 () (@var "R4" tptp.set_variable)) % 0.45/0.95 (define @t639 () (lambda @t344 (_ @t342 @t637))) % 0.45/0.95 (define @t640 () (lambda @t344 (_ @t342 @t638))) % 0.45/0.95 (define @t641 () (@list @t638 @t637)) % 0.45/0.95 (define @t642 () (@var "Eta2" tptp.option_trm)) % 0.45/0.95 (define @t643 () (@var "V7" tptp.trm)) % 0.45/0.95 (define @t644 () (@var "F2" tptp.char)) % 0.45/0.95 (define @t645 () (@var "F4" (-> tptp.char tptp.option_trm))) % 0.45/0.95 (define @t646 () (@list (@var "Uv" (-> tptp.char tptp.option_fml)) @t19 @t17)) % 0.45/0.95 (define @t647 () (_ (_ (_ tptp.produc866613687on_trm (lambda @t24 (_ (_ (_ tptp.produc1231571704on_trm (lambda (@list @t645 @t16 @t14) (_ (_ (_ tptp.produc1036610745on_trm (lambda @t646 (_ @t645 @t17))) @t16) @t14))) @t15) @t14))) @t54) @t644)) % 0.45/0.95 (define @t648 () (@var "R" tptp.trm)) % 0.45/0.95 (define @t649 () (_ tptp.inf_inf_set_variable (_ tptp.static_FVT @t648))) % 0.45/0.95 (define @t650 () (@list @t648)) % 0.45/0.95 (define @t651 () (_ tptp.func @t644)) % 0.45/0.95 (define @t652 () (_ @t245 (_ @t651 @t107))) % 0.45/0.95 (define @t653 () (@list @t54 @t57 @t644 @t107)) % 0.45/0.95 (define @t654 () (@var "Y42" tptp.trm)) % 0.45/0.95 (define @t655 () (@var "X42" tptp.trm)) % 0.45/0.95 (define @t656 () (@var "Y41" tptp.char)) % 0.45/0.95 (define @t657 () (@var "X41" tptp.char)) % 0.45/0.95 (define @t658 () (_ (_ tptp.func @t657) @t655)) % 0.45/0.95 (define @t659 () (= @t652 tptp.none_trm)) % 0.45/0.95 (define @t660 () (@var "R2" tptp.trm)) % 0.45/0.95 (define @t661 () (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVT @t660)) @t57) tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t662 () (_ tptp.some_trm @t660)) % 0.45/0.95 (define @t663 () (= @t647 @t662)) % 0.45/0.95 (define @t664 () (@var "R3" tptp.trm)) % 0.45/0.95 (define @t665 () (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVT @t664)) @t57) tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t666 () (_ tptp.some_trm @t664)) % 0.45/0.95 (define @t667 () (@list @t664)) % 0.45/0.95 (define @t668 () (_ (_ (_ tptp.uSubst1559070963pconst @t54) @t57) @t644)) % 0.45/0.95 (define @t669 () (@var "F0" (-> tptp.char tptp.option_trm))) % 0.45/0.95 (define @t670 () (_ tptp.produc866613687on_trm (lambda (@list @t669 @t15 @t14) (_ (_ (_ tptp.produc1231571704on_trm (lambda (@list @t23 @t16 @t14) (_ (_ (_ tptp.produc1036610745on_trm (lambda @t646 (_ @t669 @t17))) @t16) @t14))) @t15) @t14)))) % 0.45/0.95 (define @t671 () (_ (_ @t670 @t54) @t644)) % 0.45/0.95 (define @t672 () (= @t671 @t662)) % 0.45/0.95 (define @t673 () (@list @t54 @t644 @t660 @t57)) % 0.45/0.95 (define @t674 () (or (= @t671 tptp.none_trm) (exists @t667 (and (= @t671 @t666) @t665)))) % 0.45/0.95 (define @t675 () (@list @t54 @t57 @t644)) % 0.45/0.95 (define @t676 () (_ @t245 (_ tptp.const @t644))) % 0.45/0.95 (define @t677 () (@var "Y32" tptp.char)) % 0.45/0.95 (define @t678 () (@var "X32" tptp.char)) % 0.45/0.95 (define @t679 () (_ tptp.const @t678)) % 0.45/0.95 (define @t680 () (@var "X3" tptp.produc1739631244on_fml)) % 0.45/0.95 (define @t681 () (@var "Phi2" tptp.option_fml)) % 0.45/0.95 (define @t682 () (@list @t140 @t249)) % 0.45/0.95 (define @t683 () (@list @t146 @t257)) % 0.45/0.95 (define @t684 () (not (= @t43 tptp.none_fml))) % 0.45/0.95 (define @t685 () (or @t684 @t41)) % 0.45/0.95 (define @t686 () (not @t685)) % 0.45/0.95 (define @t687 () (@var "X" tptp.produc1418842292n_game)) % 0.45/0.95 (define @t688 () (@var "Y" tptp.char)) % 0.45/0.95 (define @t689 () (@var "R" tptp.produc62062515n_game)) % 0.45/0.95 (define @t690 () (@var "L" (-> tptp.char tptp.option_trm))) % 0.45/0.95 (define @t691 () (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc62062515n_game tptp.char tptp.option_fml))) % 0.45/0.95 (define @t692 () (@list @t690 @t689)) % 0.45/0.95 (define @t693 () (lambda (@list @t691 @t687 @t688) (_ (_ tptp.produc1499310791on_fml (lambda @t692 (_ (_ (_ @t691 @t690) @t689) @t688))) @t687))) % 0.45/0.95 (define @t694 () (@var "X" tptp.produc62062515n_game)) % 0.45/0.95 (define @t695 () (@var "R" tptp.produc799602994n_game)) % 0.45/0.95 (define @t696 () (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_trm))) % 0.45/0.95 (define @t697 () (@list @t690 @t695)) % 0.45/0.95 (define @t698 () (lambda (@list @t696 @t694 @t688) (_ (_ tptp.produc692578258on_trm (lambda @t697 (_ (_ (_ @t696 @t690) @t695) @t688))) @t694))) % 0.45/0.95 (define @t699 () (@var "F" (-> (-> tptp.char tptp.option_trm) tptp.produc799602994n_game tptp.char tptp.option_fml))) % 0.45/0.95 (define @t700 () (lambda (@list @t699 @t694 @t688) (_ (_ tptp.produc154833544on_fml (lambda @t697 (_ (_ (_ @t699 @t690) @t695) @t688))) @t694))) % 0.45/0.95 (define @t701 () (@var "X" tptp.produc799602994n_game)) % 0.45/0.95 (define @t702 () (@var "R" (-> tptp.char tptp.option_game))) % 0.45/0.95 (define @t703 () (@var "L" (-> tptp.char tptp.option_fml))) % 0.45/0.95 (define @t704 () (@var "F" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_trm))) % 0.45/0.95 (define @t705 () (@list @t703 @t702)) % 0.45/0.95 (define @t706 () (lambda (@list @t704 @t701 @t688) (_ (_ tptp.produc885547027on_trm (lambda @t705 (_ (_ (_ @t704 @t703) @t702) @t688))) @t701))) % 0.45/0.95 (define @t707 () (@var "F" (-> (-> tptp.char tptp.option_fml) (-> tptp.char tptp.option_game) tptp.char tptp.option_fml))) % 0.45/0.95 (define @t708 () (lambda (@list @t707 @t701 @t688) (_ (_ tptp.produc347802313on_fml (lambda @t705 (_ (_ (_ @t707 @t703) @t702) @t688))) @t701))) % 0.45/0.95 (define @t709 () (@var "Option2" tptp.option_game)) % 0.45/0.95 (define @t710 () (@var "F23" (-> tptp.game Bool))) % 0.45/0.95 (define @t711 () (= @t709 tptp.none_game)) % 0.45/0.95 (define @t712 () (@var "F12" Bool)) % 0.45/0.95 (define @t713 () (lambda (@list @t712 @t710 @t709) (and (=> @t711 @t712) (=> (not @t711) (_ @t710 (_ tptp.the_game @t709)))))) % 0.45/0.95 (define @t714 () (@var "Option2" tptp.option_trm)) % 0.45/0.95 (define @t715 () (_ tptp.the_trm @t714)) % 0.45/0.95 (define @t716 () (@var "F23" (-> tptp.trm Bool))) % 0.45/0.95 (define @t717 () (= @t714 tptp.none_trm)) % 0.45/0.95 (define @t718 () (lambda (@list @t712 @t716 @t714) (and (=> @t717 @t712) (=> (not @t717) (_ @t716 @t715))))) % 0.45/0.95 (define @t719 () (@var "Option2" tptp.option_fml)) % 0.45/0.95 (define @t720 () (_ tptp.the_fml @t719)) % 0.45/0.95 (define @t721 () (@var "F23" (-> tptp.fml Bool))) % 0.45/0.95 (define @t722 () (= @t719 tptp.none_fml)) % 0.45/0.95 (define @t723 () (lambda (@list @t712 @t721 @t719) (and (=> @t722 @t712) (=> (not @t722) (_ @t721 @t720))))) % 0.45/0.95 (define @t724 () (@var "F23" (-> tptp.fml tptp.option_fml))) % 0.45/0.95 (define @t725 () (@var "F12" tptp.option_fml)) % 0.45/0.95 (define @t726 () (lambda (@list @t725 @t724 @t719) (_ (_ (_ tptp.if_option_fml @t722) @t725) (_ @t724 @t720)))) % 0.45/0.95 (define @t727 () (@var "F23" (-> tptp.trm tptp.option_fml))) % 0.45/0.95 (define @t728 () (lambda (@list @t725 @t727 @t714) (_ (_ (_ tptp.if_option_fml @t717) @t725) (_ @t727 @t715)))) % 0.45/0.95 (define @t729 () (@var "F23" (-> tptp.trm tptp.option_trm))) % 0.45/0.95 (define @t730 () (@var "F12" tptp.option_trm)) % 0.45/0.95 (define @t731 () (lambda (@list @t730 @t729 @t714) (_ (_ (_ tptp.if_option_trm @t717) @t730) (_ @t729 @t715)))) % 0.45/0.95 (define @t732 () (@var "G" (-> tptp.variable Bool))) % 0.45/0.95 (define @t733 () (_ @t732 @t341)) % 0.45/0.95 (define @t734 () (@var "F" (-> tptp.variable Bool))) % 0.45/0.95 (define @t735 () (lambda (@list @t734 @t732 @t341) (_ (_ tptp.inf_inf_o (_ @t734 @t341)) @t733))) % 0.45/0.95 (define @t736 () (lambda @t344 @t519)) % 0.45/0.95 (define @t737 () (lambda @t344 @t520)) % 0.45/0.95 (define @t738 () (lambda @t510 (_ tptp.collect_variable (_ (_ tptp.inf_inf_variable_o @t737) @t736)))) % 0.45/0.95 (define @t739 () (lambda @t510 (_ (_ tptp.ord_le1407353162able_o @t737) @t736))) % 0.45/0.95 (define @t740 () (lambda @t344 (_ @t342 tptp.bot_bot_set_variable))) % 0.45/0.95 (define @t741 () (lambda (@list @t508) (= @t508 tptp.bot_bot_set_variable))) % 0.45/0.95 (define @t742 () (@var "F" tptp.char)) % 0.45/0.95 (define @t743 () (@var "Sigma2" tptp.produc1418842292n_game)) % 0.45/0.95 (define @t744 () (@var "U2" tptp.set_variable)) % 0.45/0.95 (define @t745 () (lambda (@list @t743 @t744 @t742) (_ (_ (_ tptp.case_o487727941rm_trm (_ tptp.some_trm (_ tptp.const @t742))) (lambda @t650 (_ (_ (_ tptp.if_option_trm (= (_ @t649 @t744) tptp.bot_bot_set_variable)) (_ tptp.some_trm @t648)) tptp.none_trm))) (_ (_ @t670 @t743) @t742)))) % 0.45/0.95 (define @t746 () (tptp.pred tptp.p tptp.theta)) % 0.45/0.95 (define @t747 () (tptp.uSubst516392804stappf tptp.sigma tptp.ua @t746)) % 0.45/0.95 (define @t748 () (tptp.uSubst516392804stappf tptp.sigma tptp.va @t746)) % 0.45/0.95 (define @t749 () (@var "BOUND_VARIABLE_11097" (-> tptp.char tptp.option_trm))) % 0.45/0.95 (define @t750 () (@list @t749 @t695)) % 0.45/0.95 (define @t751 () (lambda @t692 (_ (_ tptp.produc154833544on_fml (lambda @t750 (_ (_ tptp.produc347802313on_fml (lambda @t705 (_ @t703 tptp.p))) @t695))) @t689))) % 0.45/0.95 (define @t752 () (_ (_ tptp.produc1499310791on_fml @t751) tptp.sigma)) % 0.45/0.95 (define @t753 () (_ @t703 @t688)) % 0.45/0.95 (define @t754 () (_ tptp.produc347802313on_fml (lambda @t705 @t753))) % 0.45/0.95 (define @t755 () (_ @t754 @t695)) % 0.45/0.95 (define @t756 () (_ (_ tptp.produc154833544on_fml (lambda @t750 @t755)) @t689)) % 0.45/0.95 (define @t757 () (_ tptp.produc1499310791on_fml (lambda @t692 @t756))) % 0.45/0.95 (define @t758 () (@list @t688)) % 0.45/0.95 (define @t759 () (lambda @t758 (_ @t757 tptp.sigma))) % 0.45/0.95 (define @t760 () (@list @t687 @t688)) % 0.45/0.95 (define @t761 () (_ tptp.produc347802313on_fml (lambda @t705 (_ @t703 @t14)))) % 0.45/0.95 (define @t762 () (_ @t761 @t695)) % 0.45/0.95 (define @t763 () (_ tptp.produc154833544on_fml (lambda @t750 @t762))) % 0.45/0.95 (define @t764 () (@list @t14)) % 0.45/0.95 (define @t765 () (lambda @t764 (_ @t763 @t689))) % 0.45/0.95 (define @t766 () (_ @t763 @t15)) % 0.45/0.95 (define @t767 () (lambda (@list @t15 @t14) @t766)) % 0.45/0.95 (define @t768 () (lambda @t697 @t762)) % 0.45/0.95 (define @t769 () (_ (_ tptp.produc154833544on_fml @t768) @t15)) % 0.45/0.95 (define @t770 () (lambda @t24 @t769)) % 0.45/0.95 (define @t771 () (lambda @t692 (_ (_ (_ @t770 @t690) @t689) @t688))) % 0.45/0.95 (define @t772 () (lambda @t760 (_ (_ tptp.produc1499310791on_fml @t771) @t687))) % 0.45/0.95 (define @t773 () (_ tptp.produc154833544on_fml (lambda @t697 @t755))) % 0.45/0.95 (define @t774 () (lambda @t758 (_ @t773 @t15))) % 0.45/0.95 (define @t775 () (@list @t694 @t688)) % 0.45/0.95 (define @t776 () (lambda @t764 @t762)) % 0.45/0.95 (define @t777 () (_ @t761 @t16)) % 0.45/0.95 (define @t778 () (lambda (@list @t16 @t14) @t777)) % 0.45/0.95 (define @t779 () (lambda @t21 @t777)) % 0.45/0.95 (define @t780 () (_ @t779 @t690)) % 0.45/0.95 (define @t781 () (lambda @t697 (_ (_ @t780 @t695) @t688))) % 0.45/0.95 (define @t782 () (lambda @t775 (_ (_ tptp.produc154833544on_fml @t781) @t694))) % 0.45/0.95 (define @t783 () (lambda @t758 (_ @t754 @t16))) % 0.45/0.95 (define @t784 () (@list @t701 @t688)) % 0.45/0.95 (define @t785 () (_ @t703 @t17)) % 0.45/0.95 (define @t786 () (lambda (@list @t17) @t785)) % 0.45/0.95 (define @t787 () (lambda (@list @t19 @t17) @t785)) % 0.45/0.95 (define @t788 () (_ @t20 @t703)) % 0.45/0.95 (define @t789 () (lambda @t705 (_ (_ @t788 @t702) @t688))) % 0.45/0.95 (define @t790 () (lambda @t784 (_ (_ tptp.produc347802313on_fml @t789) @t701))) % 0.45/0.95 (define @t791 () (_ @t708 @t20)) % 0.45/0.95 (define @t792 () (lambda @t21 (_ (_ @t791 @t16) @t14))) % 0.45/0.95 (define @t793 () (lambda @t24 (_ (_ (_ @t700 @t792) @t15) @t14))) % 0.45/0.95 (define @t794 () (_ (_ (_ @t693 @t793) tptp.sigma) tptp.p)) % 0.45/0.95 (define @t795 () (= @t794 tptp.none_fml)) % 0.45/0.95 (define @t796 () (or @t684 @t795)) % 0.45/0.95 (define @t797 () (= tptp.none_fml @t12)) % 0.45/0.95 (define @t798 () (@purify @t751)) % 0.45/0.95 (define @t799 () (_ (_ tptp.produc1499310791on_fml @t798) tptp.sigma)) % 0.45/0.95 (define @t800 () (_ tptp.the_fml @t799)) % 0.45/0.95 (define @t801 () (@var "BOUND_VARIABLE_20968" tptp.variable)) % 0.45/0.95 (define @t802 () (lambda (@list @t801) false)) % 0.45/0.95 (define @t803 () (@purify @t802)) % 0.45/0.95 (define @t804 () (_ tptp.collect_variable @t803)) % 0.45/0.95 (define @t805 () (tptp.produc1499310791on_fml @t798 tptp.sigma)) % 0.45/0.95 (define @t806 () (tptp.the_fml @t805)) % 0.45/0.95 (define @t807 () (tptp.collect_variable @t803)) % 0.45/0.95 (define @t808 () (tptp.uSubst516392818stappt tptp.sigma tptp.va tptp.theta)) % 0.45/0.95 (define @t809 () (tptp.the_trm @t808)) % 0.45/0.95 (define @t810 () (tptp.uSubst1408967625substt @t809)) % 0.45/0.95 (define @t811 () (tptp.uSubst516392804stappf @t810 @t807 @t806)) % 0.45/0.95 (define @t812 () (_ tptp.the_fml @t752)) % 0.45/0.95 (define @t813 () (_ tptp.collect_variable @t802)) % 0.45/0.95 (define @t814 () (= @t43 (_ (_ @t33 @t813) @t812))) % 0.45/0.95 (define @t815 () (_ tptp.static_FVF @t812)) % 0.45/0.95 (define @t816 () (_ tptp.inf_inf_o (_ @t342 @t815))) % 0.45/0.95 (define @t817 () (lambda @t344 (_ @t816 (_ @t342 tptp.va)))) % 0.45/0.95 (define @t818 () (@purify @t817)) % 0.45/0.95 (define @t819 () (tptp.collect_variable @t818)) % 0.45/0.95 (define @t820 () (_ tptp.collect_variable @t818)) % 0.45/0.95 (define @t821 () (_ tptp.collect_variable @t817)) % 0.45/0.95 (define @t822 () (= @t821 @t813)) % 0.45/0.95 (define @t823 () (=> @t822 @t814)) % 0.45/0.95 (define @t824 () (not @t823)) % 0.45/0.95 (define @t825 () (= @t813 @t821)) % 0.45/0.95 (define @t826 () (=> @t825 @t814)) % 0.45/0.95 (define @t827 () (_ @t34 @t812)) % 0.45/0.95 (define @t828 () (= tptp.none_fml @t827)) % 0.45/0.95 (define @t829 () (= tptp.bot_bot_set_variable @t821)) % 0.45/0.95 (define @t830 () (=> @t829 @t828)) % 0.45/0.95 (define @t831 () (_ tptp.the_fml @t794)) % 0.45/0.95 (define @t832 () (_ @t34 @t831)) % 0.45/0.95 (define @t833 () (= @t832 tptp.none_fml)) % 0.45/0.95 (define @t834 () (lambda (@list @t509) (_ tptp.collect_variable (lambda @t344 (_ @t816 @t519))))) % 0.45/0.95 (define @t835 () (_ tptp.inf_inf_o @t520)) % 0.45/0.95 (define @t836 () (lambda @t510 (_ tptp.collect_variable (lambda @t344 (_ @t835 @t519))))) % 0.45/0.95 (define @t837 () (= (_ (_ @t836 (_ tptp.static_FVF @t831)) tptp.va) tptp.bot_bot_set_variable)) % 0.45/0.95 (define @t838 () (=> @t837 @t833)) % 0.45/0.95 (define @t839 () (_ @t736 @t341)) % 0.45/0.95 (define @t840 () (lambda @t344 (_ @t835 @t839))) % 0.45/0.95 (define @t841 () (@list @t732 @t341)) % 0.45/0.95 (define @t842 () (_ @t737 @t341)) % 0.45/0.95 (define @t843 () (lambda @t841 (_ (_ tptp.inf_inf_o @t842) @t733))) % 0.45/0.95 (define @t844 () (= @t748 @t805)) % 0.45/0.95 (define @t845 () (=> (= @t807 @t819) (= @t748 @t811))) % 0.45/0.95 (define @t846 () (= @t43 @t752)) % 0.45/0.95 (define @t847 () (not @t825)) % 0.45/0.95 (define @t848 () (=> @t847 (= @t43 @t43))) % 0.45/0.95 (define @t849 () (and @t826 @t848)) % 0.45/0.95 (define @t850 () (not @t849)) % 0.45/0.95 (define @t851 () (= tptp.none_fml @t752)) % 0.45/0.95 (define @t852 () (not @t829)) % 0.45/0.95 (define @t853 () (=> @t852 @t44)) % 0.45/0.95 (define @t854 () (= @t43 @t827)) % 0.45/0.95 (define @t855 () (=> @t829 @t854)) % 0.45/0.95 (define @t856 () (and @t855 @t853)) % 0.45/0.95 (define @t857 () (not @t856)) % 0.45/0.95 (define @t858 () (not @t837)) % 0.45/0.95 (define @t859 () (=> @t858 @t44)) % 0.45/0.95 (define @t860 () (= @t832 @t43)) % 0.45/0.95 (define @t861 () (=> @t837 @t860)) % 0.45/0.95 (define @t862 () (and @t861 @t859)) % 0.45/0.95 (define @t863 () (not @t862)) % 0.45/0.95 (define @t864 () (= @t748 @t747)) % 0.45/0.95 (assume @p1 (forall (@list @t3 @t2) (= (exists (@list @t7) (and (_ (_ tptp.member_variable @t7) @t2) (exists @t6 (and @t5 (= @t7 @t1))))) (and (_ (_ tptp.member_variable @t4) @t2) (exists @t6 (and @t5 (= @t4 @t1))))))) % 0.45/0.95 (assume @p2 @t13) % 0.45/0.95 (assume @p3 @t40) % 0.45/0.95 (assume @p4 @t51) % 0.45/0.95 (assume @p5 (forall (@list @t54 @t57 @t52 @t53) (=> (not (= @t59 tptp.none_fml)) (=> (not (= @t56 tptp.none_fml)) (= @t59 @t56))))) % 0.45/0.95 (assume @p6 @t61) % 0.45/0.95 (assume @p7 (or (not @t66) (not @t65) (not @t64))) % 0.45/0.95 (assume @p8 (forall (@list @t70 @t68 @t69 @t67) (= (= @t71 (_ (_ tptp.pred @t69) @t67)) (and (= @t70 @t69) (= @t68 @t67))))) % 0.45/0.95 (assume @p9 (= @t72 @t30)) % 0.45/0.95 (assume @p10 (forall @t75 (or (not (_ @t74 tptp.va)) (_ @t74 tptp.ua)))) % 0.45/0.95 (assume @p11 (and (or @t45 (forall @t75 (or (not (_ @t74 @t37)) (forall @t79 (or (not (_ @t78 tptp.va)) @t77))))) (or @t38 (and @t66 @t65 @t64)))) % 0.45/0.95 (assume @p12 (forall (@list @t85 @t83 @t80) (= (_ @t85 @t87) (_ (_ tptp.produc347802313on_fml (lambda @t86 (_ @t85 @t84))) @t80)))) % 0.45/0.95 (assume @p13 (forall (@list @t88 @t83 @t80) (= (_ @t88 @t87) (_ (_ tptp.produc885547027on_trm (lambda @t86 (_ @t88 @t84))) @t80)))) % 0.45/0.95 (assume @p14 (forall (@list @t91 @t89 @t80) (= (_ @t91 @t92) (_ (_ tptp.produc347802313on_fml (lambda @t86 (_ @t91 @t90))) @t80)))) % 0.45/0.95 (assume @p15 (forall (@list @t93 @t89 @t80) (= (_ @t93 @t92) (_ (_ tptp.produc885547027on_trm (lambda @t86 (_ @t93 @t90))) @t80)))) % 0.45/0.95 (assume @p16 (forall (@list @t96 @t94 @t80) (= (_ @t96 @t97) (_ (_ tptp.produc347802313on_fml (lambda @t86 (_ @t96 @t95))) @t80)))) % 0.45/0.95 (assume @p17 (forall (@list @t98 @t94 @t80) (= (_ @t98 @t97) (_ (_ tptp.produc885547027on_trm (lambda @t86 (_ @t98 @t95))) @t80)))) % 0.45/0.95 (assume @p18 (forall (@list @t101 @t99 @t80) (= (_ @t101 @t102) (_ (_ tptp.produc347802313on_fml (lambda @t86 (_ @t101 @t100))) @t80)))) % 0.45/0.95 (assume @p19 (forall (@list @t103 @t99 @t80) (= (_ @t103 @t102) (_ (_ tptp.produc885547027on_trm (lambda @t86 (_ @t103 @t100))) @t80)))) % 0.45/0.95 (assume @p20 (forall (@list @t104 @t83 @t80) (= (_ @t104 @t87) (_ (_ tptp.produc1036610745on_trm (lambda @t105 (_ (_ @t104 @t84) @t17))) @t80)))) % 0.45/0.95 (assume @p21 (forall (@list @t106 @t83 @t80) (= (_ @t106 @t87) (_ (_ tptp.produc1420172399on_fml (lambda @t105 (_ (_ @t106 @t84) @t17))) @t80)))) % 0.45/0.95 (assume @p22 (forall (@list @t54 @t108 @t112 @t57 @t107) (=> @t115 (=> (not @t113) @t111)))) % 0.45/0.95 (assume @p23 (forall (@list @t118 @t117 @t116) (and (=> @t120 (= @t119 @t118)) (=> (not @t120) (= @t119 (_ @t117 (_ tptp.the_fml @t116))))))) % 0.45/0.95 (assume @p24 (_ (_ tptp.ord_le282106107riable tptp.va) tptp.ua)) % 0.45/0.95 (assume @p25 (forall @t128 (and @t127 (or @t126 (and @t125 (_ (_ tptp.member_variable @t123) @t122) (= @t124 @t123)))))) % 0.45/0.95 (assume @p26 (not (forall (@list @t129) (not (forall @t128 (and @t127 (or @t126 (and @t125 (_ (_ tptp.member_variable @t130) @t122) (= @t124 @t130))))))))) % 0.45/0.95 (assume @p27 (forall (@list @t132 @t131) (= (= @t133 (_ tptp.some_fml @t131)) (= @t132 @t131)))) % 0.45/0.95 (assume @p28 (forall (@list @t135 @t134) (= (= @t136 (_ tptp.some_trm @t134)) (= @t135 @t134)))) % 0.45/0.95 (assume @p29 (forall (@list @t138 @t137) (= (= @t139 (_ tptp.some_game @t137)) (= @t138 @t137)))) % 0.45/0.95 (assume @p30 (not (= @t72 tptp.none_trm))) % 0.45/0.95 (assume @p31 (forall @t145 (= (forall @t144 (not @t143)) @t141))) % 0.45/0.95 (assume @p32 (forall @t151 (= (forall @t150 (not @t149)) @t147))) % 0.45/0.95 (assume @p33 (forall @t157 (= (forall @t156 (not @t155)) @t153))) % 0.45/0.95 (assume @p34 (forall @t145 (= (not @t141) (exists @t144 @t143)))) % 0.45/0.95 (assume @p35 (forall @t151 (= (not @t147) (exists @t150 @t149)))) % 0.45/0.95 (assume @p36 (forall @t157 (= (not @t153) (exists @t156 @t155)))) % 0.45/0.95 (assume @p37 (forall @t163 (=> @t162 (= @t160 @t158)))) % 0.45/0.95 (assume @p38 (forall @t169 (=> @t168 (= @t166 @t164)))) % 0.45/0.95 (assume @p39 (forall @t175 (=> @t174 (= @t172 @t170)))) % 0.45/0.95 (assume @p40 (forall (@list @t177 @t176 @t138) (= (_ @t178 @t139) (_ @t176 @t138)))) % 0.45/0.95 (assume @p41 (forall (@list @t177 @t179 @t135) (= (_ @t180 @t136) (_ @t179 @t135)))) % 0.45/0.95 (assume @p42 (forall (@list @t177 @t181 @t132) (= (_ @t182 @t133) (_ @t181 @t132)))) % 0.45/0.95 (assume @p43 (forall (@list @t184 @t183 @t132) (= (_ @t185 @t133) (_ @t183 @t132)))) % 0.45/0.95 (assume @p44 (forall (@list @t184 @t186 @t135) (= (_ @t187 @t136) (_ @t186 @t135)))) % 0.45/0.95 (assume @p45 (forall (@list @t189 @t188 @t135) (= (_ @t190 @t136) (_ @t188 @t135)))) % 0.45/0.95 (assume @p46 (forall @t191 (= (_ tptp.the_fml @t133) @t132))) % 0.45/0.95 (assume @p47 (forall @t192 (= (_ tptp.the_trm @t136) @t135))) % 0.45/0.95 (assume @p48 (forall @t193 (= (_ tptp.the_game @t139) @t138))) % 0.45/0.95 (assume @p49 (forall @t200 (= @t199 (and (=> @t173 @t197) (=> @t196 @t195))))) % 0.45/0.95 (assume @p50 (forall @t205 (= @t204 (and (=> @t167 @t197) (=> @t202 @t201))))) % 0.45/0.95 (assume @p51 (forall @t210 (= @t209 (and (=> @t161 @t197) (=> @t207 @t206))))) % 0.45/0.95 (assume @p52 (forall @t216 (= @t215 (and (=> @t161 @t213) (=> @t207 @t212))))) % 0.45/0.95 (assume @p53 (forall @t220 (= @t219 (and (=> @t167 @t213) (=> @t202 @t217))))) % 0.45/0.95 (assume @p54 (forall @t226 (= @t225 (and (=> @t167 @t223) (=> @t202 @t222))))) % 0.45/0.95 (assume @p55 (forall (@list @t85 @t184 @t183 @t158) (= (_ @t85 @t214) (_ (_ (_ tptp.case_o209804997ml_fml @t230) (lambda @t229 (_ @t85 @t228))) @t158)))) % 0.45/0.95 (assume @p56 (forall (@list @t85 @t184 @t186 @t164) (= (_ @t85 @t218) (_ (_ (_ tptp.case_o325794063ml_trm @t230) (lambda @t233 (_ @t85 @t232))) @t164)))) % 0.45/0.95 (assume @p57 (forall (@list @t88 @t184 @t186 @t164) (= (_ @t88 @t218) (_ (_ (_ tptp.case_o487727941rm_trm (_ @t88 @t184)) (lambda @t233 (_ @t88 @t232))) @t164)))) % 0.45/0.95 (assume @p58 (forall (@list @t91 @t189 @t188 @t164) (= (_ @t91 @t224) (_ (_ (_ tptp.case_o325794063ml_trm (_ @t91 @t189)) (lambda @t233 (_ @t91 @t234))) @t164)))) % 0.45/0.95 (assume @p59 (forall (@list @t93 @t189 @t188 @t164) (= (_ @t93 @t224) (_ (_ (_ tptp.case_o487727941rm_trm (_ @t93 @t189)) (lambda @t233 (_ @t93 @t234))) @t164)))) % 0.45/0.95 (assume @p60 (forall (@list @t236 @t177 @t176 @t170) (= (_ @t236 @t198) (_ (_ (_ tptp.case_option_o_game @t238) (lambda @t237 (_ @t236 (_ @t176 @t235)))) @t170)))) % 0.45/0.95 (assume @p61 (forall (@list @t236 @t177 @t179 @t164) (= (_ @t236 @t203) (_ (_ (_ tptp.case_option_o_trm @t238) (lambda @t233 (_ @t236 (_ @t179 @t231)))) @t164)))) % 0.45/0.95 (assume @p62 (forall (@list @t236 @t177 @t181 @t158) (= (_ @t236 @t208) (_ (_ (_ tptp.case_option_o_fml @t238) (lambda @t229 (_ @t236 (_ @t181 @t227)))) @t158)))) % 0.45/0.95 (assume @p63 (forall (@list @t239 @t184 @t183 @t158) (= (_ @t239 @t214) (_ (_ (_ tptp.case_option_o_fml @t240) (lambda @t229 (_ @t239 @t228))) @t158)))) % 0.45/0.95 (assume @p64 (forall (@list @t239 @t184 @t186 @t164) (= (_ @t239 @t218) (_ (_ (_ tptp.case_option_o_trm @t240) (lambda @t233 (_ @t239 @t232))) @t164)))) % 0.45/0.95 (assume @p65 (forall @t200 (= @t199 (not (or (and @t173 @t241) (and @t196 (not @t195))))))) % 0.45/0.95 (assume @p66 (forall @t205 (= @t204 (not (or (and @t167 @t241) (and @t202 (not @t201))))))) % 0.45/0.95 (assume @p67 (forall @t210 (= @t209 (not (or (and @t161 @t241) (and @t207 (not @t206))))))) % 0.45/0.95 (assume @p68 (forall @t216 (= @t215 (not (or (and @t161 @t242) (and @t207 (not @t212))))))) % 0.45/0.95 (assume @p69 (forall @t220 (= @t219 (not (or (and @t167 @t242) (and @t202 (not @t217))))))) % 0.45/0.95 (assume @p70 (forall @t226 (= @t225 (not (or (and @t167 (not @t223)) (and @t202 (not @t222))))))) % 0.45/0.95 (assume @p71 (forall (@list @t54 @t57 @t107 @t53) (=> @t248 (=> (not (= @t244 tptp.none_trm)) @t247)))) % 0.45/0.95 (assume @p72 (forall (@list @t53 @t57 @t54 @t107) (=> (_ (_ tptp.ord_le282106107riable @t53) @t57) (=> @t248 @t247)))) % 0.45/0.95 (assume @p73 (forall @t163 (=> @t162 @t207))) % 0.45/0.95 (assume @p74 (forall @t169 (=> @t168 @t202))) % 0.45/0.95 (assume @p75 (forall @t175 (=> @t174 @t196))) % 0.45/0.95 (assume @p76 (forall (@list @t140 @t250 @t249) (=> (=> @t141 @t251) (=> (=> @t256 @t251) (=> (forall (@list @t254 @t252) (=> @t255 (=> @t253 @t251))) @t251))))) % 0.45/0.95 (assume @p77 (forall (@list @t140 @t258 @t257) (=> (=> @t141 @t259) (=> (=> @t262 @t259) (=> (forall (@list @t254 @t260) (=> @t255 (=> @t261 @t259))) @t259))))) % 0.45/0.95 (assume @p78 (forall (@list @t140 @t264 @t263) (=> (=> @t141 @t265) (=> (=> @t268 @t265) (=> (forall (@list @t254 @t266) (=> @t255 (=> @t267 @t265))) @t265))))) % 0.45/0.95 (assume @p79 (forall (@list @t146 @t269 @t249) (=> (=> @t147 @t270) (=> (=> @t256 @t270) (=> (forall (@list @t271 @t252) (=> @t272 (=> @t253 @t270))) @t270))))) % 0.45/0.95 (assume @p80 (forall (@list @t146 @t273 @t257) (=> (=> @t147 @t274) (=> (=> @t262 @t274) (=> (forall (@list @t271 @t260) (=> @t272 (=> @t261 @t274))) @t274))))) % 0.45/0.95 (assume @p81 (forall (@list @t146 @t275 @t263) (=> (=> @t147 @t276) (=> (=> @t268 @t276) (=> (forall (@list @t271 @t266) (=> @t272 (=> @t267 @t276))) @t276))))) % 0.45/0.95 (assume @p82 (forall (@list @t152 @t277 @t249) (=> (=> @t153 @t278) (=> (=> @t256 @t278) (=> (forall (@list @t279 @t252) (=> @t280 (=> @t253 @t278))) @t278))))) % 0.45/0.95 (assume @p83 (forall (@list @t152 @t281 @t257) (=> (=> @t153 @t282) (=> (=> @t262 @t282) (=> (forall (@list @t279 @t260) (=> @t280 (=> @t261 @t282))) @t282))))) % 0.45/0.95 (assume @p84 (forall (@list @t152 @t283 @t263) (=> (=> @t153 @t284) (=> (=> @t268 @t284) (=> (forall (@list @t279 @t266) (=> @t280 (=> @t267 @t284))) @t284))))) % 0.45/0.95 (assume @p85 (= (lambda @t293 (forall @t292 @t291)) (lambda @t288 (and @t287 (forall @t229 @t286))))) % 0.45/0.95 (assume @p86 (= (lambda @t302 (forall @t301 @t300)) (lambda @t297 (and @t296 (forall @t233 @t295))))) % 0.45/0.95 (assume @p87 (= (lambda @t311 (forall @t310 @t309)) (lambda @t306 (and @t305 (forall @t237 @t304))))) % 0.45/0.95 (assume @p88 (= (lambda @t293 (exists @t292 @t291)) (lambda @t288 (or @t287 (exists @t229 @t286))))) % 0.45/0.95 (assume @p89 (= (lambda @t302 (exists @t301 @t300)) (lambda @t297 (or @t296 (exists @t233 @t295))))) % 0.45/0.95 (assume @p90 (= (lambda @t311 (exists @t310 @t309)) (lambda @t306 (or @t305 (exists @t237 @t304))))) % 0.45/0.95 (assume @p91 (forall (@list @t211 @t158) (=> @t313 (=> (forall (@list @t312) (_ @t211 (_ tptp.some_fml @t312))) (_ @t211 @t158))))) % 0.45/0.95 (assume @p92 (forall (@list @t221 @t164) (=> @t315 (=> (forall (@list @t314) (_ @t221 (_ tptp.some_trm @t314))) (_ @t221 @t164))))) % 0.45/0.95 (assume @p93 (forall (@list @t316 @t170) (=> @t318 (=> (forall (@list @t317) (_ @t316 (_ tptp.some_game @t317))) (_ @t316 @t170))))) % 0.45/0.95 (assume @p94 (forall (@list @t249) (=> @t320 (not (forall (@list @t319) (not (= @t249 (_ tptp.some_fml @t319)))))))) % 0.45/0.95 (assume @p95 (forall (@list @t257) (=> (not @t262) (not (forall (@list @t321) (not (= @t257 (_ tptp.some_trm @t321)))))))) % 0.45/0.95 (assume @p96 (forall (@list @t263) (=> (not @t268) (not (forall (@list @t322) (not (= @t263 (_ tptp.some_game @t322)))))))) % 0.45/0.95 (assume @p97 (forall (@list @t158 @t132) (=> (= @t158 @t133) @t162))) % 0.45/0.95 (assume @p98 (forall (@list @t164 @t135) (=> (= @t164 @t136) @t168))) % 0.45/0.95 (assume @p99 (forall (@list @t170 @t138) (=> (= @t170 @t139) @t174))) % 0.45/0.95 (assume @p100 (forall @t191 (not (= tptp.none_fml @t133)))) % 0.45/0.95 (assume @p101 (forall @t192 (not (= tptp.none_trm @t136)))) % 0.45/0.95 (assume @p102 (forall @t193 (not (= tptp.none_game @t139)))) % 0.45/0.95 (assume @p103 (forall (@list @t177 @t176) (= (_ @t178 tptp.none_game) @t177))) % 0.45/0.95 (assume @p104 (forall (@list @t177 @t179) (= (_ @t180 tptp.none_trm) @t177))) % 0.45/0.95 (assume @p105 (forall (@list @t177 @t181) (= (_ @t182 tptp.none_fml) @t177))) % 0.45/0.95 (assume @p106 (forall (@list @t184 @t183) (= (_ @t185 tptp.none_fml) @t184))) % 0.45/0.95 (assume @p107 (forall (@list @t184 @t186) (= (_ @t187 tptp.none_trm) @t184))) % 0.45/0.95 (assume @p108 (forall (@list @t189 @t188) (= (_ @t190 tptp.none_trm) @t189))) % 0.45/0.95 (assume @p109 (forall (@list @t325 @t324 @t323) (=> (forall (@list @t326 @t329) (_ @t327 @t330)) (=> (forall @t328 (_ @t327 tptp.none_fml)) (_ (_ @t325 @t324) @t323))))) % 0.45/0.95 (assume @p110 (forall (@list @t332) (= (not (= @t332 tptp.none_fml)) (exists @t333 (= @t332 (_ tptp.some_fml @t331)))))) % 0.45/0.95 (assume @p111 (forall (@list @t211 @t334) (=> (forall @t335 (_ @t211 @t330)) (=> @t313 (_ @t211 @t334))))) % 0.45/0.95 (assume @p112 (forall @t145 (=> (forall @t335 (not (= @t140 @t330))) @t141))) % 0.45/0.95 (assume @p113 (forall (@list @t336 @t337) (= (_ @t339 @t338) (_ @t337 @t336)))) % 0.45/0.95 (assume @p114 (forall @t345 (= (_ tptp.collect_variable (lambda @t344 @t343)) @t340))) % 0.45/0.95 (assume @p115 (forall @t350 (=> (forall @t328 (= @t349 @t348)) (= @t338 @t347)))) % 0.45/0.95 (assume @p116 (forall (@list @t250 @t334 @t323) (=> (forall (@list @t329 @t354) (_ (_ @t250 @t330) (_ tptp.some_fml @t354))) (=> (forall @t353 (_ (_ @t250 tptp.none_fml) @t352)) (=> (forall (@list @t351) (_ (_ @t250 (_ tptp.some_fml @t351)) tptp.none_fml)) (_ (_ @t250 @t334) @t323)))))) % 0.45/0.95 (assume @p117 (forall (@list @t158 @t355) (=> (= @t161 @t356) (=> (=> @t162 (=> (not @t356) (= @t159 (_ tptp.the_fml @t355)))) (= @t158 @t355))))) % 0.45/0.95 (assume @p118 (forall (@list @t164 @t357) (=> (= @t167 @t358) (=> (=> @t168 (=> (not @t358) (= @t165 (_ tptp.the_trm @t357)))) (= @t164 @t357))))) % 0.45/0.95 (assume @p119 (forall (@list @t170 @t359) (=> (= @t173 @t360) (=> (=> @t174 (=> (not @t360) (= @t171 (_ tptp.the_game @t359)))) (= @t170 @t359))))) % 0.45/0.95 (assume @p120 (forall @t362 (=> (not @t111) (and @t248 (or (= @t114 tptp.none_fml) (exists (@list @t361) (and (= @t114 (_ tptp.some_fml @t361)) (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVF @t361)) @t57) tptp.bot_bot_set_variable)))))))) % 0.45/0.95 (assume @p121 (= @t368 (_ (_ (_ tptp.case_o209804997ml_fml (_ tptp.some_fml (_ @t8 @t363))) (lambda @t333 (_ (_ @t364 (_ (_ (_ tptp.uSubst516392804stappf (_ tptp.uSubst1408967625substt @t363)) tptp.bot_bot_set_variable) @t331)) tptp.none_fml))) @t27))) % 0.45/0.95 (assume @p122 (not (= @t368 tptp.none_fml))) % 0.45/0.95 (assume @p123 (forall @t362 (= @t110 (_ (_ @t367 (lambda @t372 (_ (_ (_ tptp.case_o209804997ml_fml (_ tptp.some_fml (_ @t109 @t370))) (lambda (@list @t369) (_ (_ (_ tptp.if_option_fml (= (_ (_ tptp.inf_inf_set_variable (_ tptp.static_FVF @t369)) @t57) tptp.bot_bot_set_variable)) (_ (_ (_ tptp.uSubst516392804stappf @t371) tptp.bot_bot_set_variable) @t369)) tptp.none_fml))) @t114))) @t246)))) % 0.45/0.95 (assume @p124 (forall @t381 (= @t380 (and @t377 @t376)))) % 0.45/0.95 (assume @p125 (forall @t383 (= (_ (_ tptp.inf_inf_variable_o tptp.bot_bot_variable_o) @t382) tptp.bot_bot_variable_o))) % 0.45/0.95 (assume @p126 (forall @t386 (= (_ @t385 @t384) tptp.bot_bot_set_variable))) % 0.45/0.95 (assume @p127 (forall @t383 (= (_ @t387 tptp.bot_bot_variable_o) tptp.bot_bot_variable_o))) % 0.45/0.95 (assume @p128 (forall @t386 (= (_ @t388 tptp.bot_bot_set_variable) tptp.bot_bot_set_variable))) % 0.45/0.95 (assume @p129 (forall @t345 (= @t391 @t389))) % 0.45/0.95 (assume @p130 (forall @t345 (_ @t392 @t340))) % 0.45/0.95 (assume @p131 (forall @t398 (= (_ @t394 @t397) (and (_ @t394 @t395) (_ @t394 @t393))))) % 0.45/0.95 (assume @p132 (forall @t407 (= @t406 (and @t403 @t401)))) % 0.45/0.95 (assume @p133 (forall @t414 (= (_ @t410 @t413) (and (_ @t410 @t411) (_ @t410 @t408))))) % 0.45/0.95 (assume @p134 (forall @t424 (= @t423 (and @t420 @t418)))) % 0.45/0.95 (assume @p135 (forall (@list @t118 @t426 @t425) (and (=> @t428 (= @t427 @t118)) (=> (not @t428) (= @t427 (_ @t426 (_ tptp.the_trm @t425))))))) % 0.45/0.95 (assume @p136 (forall @t431 (= (= tptp.bot_bot_set_variable @t338) @t430))) % 0.45/0.95 (assume @p137 (forall @t431 (= @t432 @t430))) % 0.45/0.95 (assume @p138 (forall @t345 (= (forall @t344 (not @t343)) @t389))) % 0.45/0.95 (assume @p139 (forall (@list @t433) (not (_ @t434 tptp.bot_bot_set_variable)))) % 0.45/0.95 (assume @p140 (forall @t439 (=> @t438 (=> @t437 @t435)))) % 0.45/0.95 (assume @p141 (forall @t439 (=> (forall @t328 (=> @t442 @t441)) @t438))) % 0.45/0.95 (assume @p142 (forall @t445 (= (_ @t444 @t395) @t443))) % 0.45/0.95 (assume @p143 (forall @t448 (= (_ @t447 @t402) @t446))) % 0.45/0.95 (assume @p144 (forall @t452 (= (_ @t451 @t411) @t450))) % 0.45/0.95 (assume @p145 (forall @t456 (= (_ @t455 @t419) @t454))) % 0.45/0.95 (assume @p146 (forall @t445 (= (_ @t387 @t443) @t443))) % 0.45/0.95 (assume @p147 (forall @t448 (= (_ @t388 @t446) @t446))) % 0.45/0.95 (assume @p148 (forall @t452 (= (_ @t449 @t450) @t450))) % 0.45/0.95 (assume @p149 (forall @t456 (= (_ @t453 @t454) @t454))) % 0.45/0.95 (assume @p150 (forall @t383 (= (_ @t387 @t382) @t382))) % 0.45/0.95 (assume @p151 (forall @t386 (= (_ @t388 @t384) @t384))) % 0.45/0.95 (assume @p152 (forall (@list @t409) (= (_ @t449 @t409) @t409))) % 0.45/0.95 (assume @p153 (forall @t457 (= (_ @t453 @t416) @t416))) % 0.45/0.95 (assume @p154 (forall @t461 (= @t460 (and @t459 @t458)))) % 0.45/0.95 (assume @p155 (forall @t461 (=> @t459 (=> @t458 @t460)))) % 0.45/0.95 (assume @p156 (forall (@list @t54 @t108 @t112 @t57 @t107 @t462) (=> @t115 (=> @t113 (=> @t464 (= @t110 (_ (_ (_ tptp.uSubst516392804stappf @t463) tptp.bot_bot_set_variable) @t112))))))) % 0.45/0.95 (assume @p157 (forall (@list @t467 @t466 @t465) (=> (forall (@list @t468 @t470) (_ @t469 @t471)) (=> (forall (@list @t468) (_ @t469 tptp.none_trm)) (_ (_ @t467 @t466) @t465))))) % 0.45/0.95 (assume @p158 (= tptp.none_trm tptp.none_trm)) % 0.45/0.95 (assume @p159 (forall (@list @t472) (= (not @t473) (exists @t366 (= @t472 (_ tptp.some_trm @t365)))))) % 0.45/0.95 (assume @p160 (forall (@list @t273 @t474 @t465) (=> (forall (@list @t470 @t479) (_ (_ @t273 @t471) @t480)) (=> (forall (@list @t478) (_ (_ @t273 tptp.none_trm) @t478)) (=> (forall @t477 (_ (_ @t273 @t476) tptp.none_trm)) (_ (_ @t273 @t474) @t465)))))) % 0.45/0.95 (assume @p161 (forall (@list @t481 @t324 @t465) (=> (forall (@list @t326 @t470) (_ @t482 @t471)) (=> (forall @t328 (_ @t482 tptp.none_trm)) (_ (_ @t481 @t324) @t465))))) % 0.45/0.95 (assume @p162 (forall @t151 (=> (forall @t484 (not @t483)) @t147))) % 0.45/0.95 (assume @p163 (forall (@list @t221 @t474) (=> (forall @t484 (_ @t221 @t471)) (=> @t315 (_ @t221 @t474))))) % 0.45/0.95 (assume @p164 (= tptp.bot_bot_set_variable (_ tptp.collect_variable tptp.bot_bot_variable_o))) % 0.45/0.95 (assume @p165 (forall @t163 (= @t162 (_ (_ (_ tptp.case_option_o_fml false) (lambda @t485 true)) @t158)))) % 0.45/0.95 (assume @p166 (forall @t169 (= @t168 (_ (_ (_ tptp.case_option_o_trm false) (lambda @t486 true)) @t164)))) % 0.45/0.95 (assume @p167 (forall @t175 (= @t174 (_ (_ (_ tptp.case_option_o_game false) (lambda @t487 true)) @t170)))) % 0.45/0.95 (assume @p168 (forall @t163 (= @t161 (_ (_ (_ tptp.case_option_o_fml true) (lambda @t485 false)) @t158)))) % 0.45/0.95 (assume @p169 (forall @t169 (= @t167 (_ (_ (_ tptp.case_option_o_trm true) (lambda @t486 false)) @t164)))) % 0.45/0.95 (assume @p170 (forall @t175 (= @t173 (_ (_ (_ tptp.case_option_o_game true) (lambda @t487 false)) @t170)))) % 0.45/0.95 (assume @p171 (forall (@list @t277 @t488 @t323) (=> (forall @t494 (_ (_ @t277 @t493) @t330)) (=> (forall @t353 (_ (_ @t277 tptp.none_game) @t352)) (=> (forall @t491 (_ (_ @t277 @t490) tptp.none_fml)) (_ (_ @t277 @t488) @t323)))))) % 0.45/0.95 (assume @p172 (forall (@list @t497 @t496 @t140) (=> @t499 (=> (=> @t141 @t498) (not (forall (@list @t495) (=> (= @t140 (_ tptp.some_fml @t495)) (not (_ @t496 @t495))))))))) % 0.45/0.95 (assume @p173 (forall (@list @t497 @t501 @t146) (=> @t502 (=> (=> @t147 @t498) (not (forall (@list @t500) (=> (= @t146 (_ tptp.some_trm @t500)) (not (_ @t501 @t500))))))))) % 0.45/0.95 (assume @p174 (forall (@list @t497 @t504 @t152) (=> (_ (_ (_ tptp.case_option_o_game @t497) @t504) @t152) (=> (=> @t153 @t498) (not (forall (@list @t503) (=> (= @t152 (_ tptp.some_game @t503)) (not (_ @t504 @t503))))))))) % 0.45/0.95 (assume @p175 (forall @t345 (= (exists @t344 @t343) (not @t389)))) % 0.45/0.95 (assume @p176 (forall @t345 (=> (forall (@list @t505) (not (_ (_ tptp.member_variable @t505) @t340))) @t389))) % 0.45/0.95 (assume @p177 (forall (@list @t340 @t336) (=> @t389 (not (_ @t339 @t340))))) % 0.45/0.95 (assume @p178 (forall (@list @t336) (not (_ @t339 tptp.bot_bot_set_variable)))) % 0.45/0.95 (assume @p179 (forall @t350 (= @t507 (forall @t344 (=> @t429 @t506))))) % 0.45/0.95 (assume @p180 (= @t513 (lambda @t510 (and (_ (_ tptp.ord_le282106107riable @t508) @t509) (_ (_ tptp.ord_le282106107riable @t509) @t508))))) % 0.45/0.95 (assume @p181 (forall @t515 (=> @t438 (=> (_ @t436 @t374) @t514)))) % 0.45/0.95 (assume @p182 (forall @t350 (=> (forall @t328 @t516) @t507))) % 0.45/0.95 (assume @p183 (forall @t345 (_ @t390 @t340))) % 0.45/0.95 (assume @p184 (= tptp.ord_le282106107riable (lambda @t510 (forall (@list @t517) (=> (_ @t518 @t508) (_ @t518 @t509)))))) % 0.45/0.95 (assume @p185 (forall @t439 (=> @t435 @t437))) % 0.45/0.95 (assume @p186 (forall @t439 (=> @t435 @t438))) % 0.45/0.95 (assume @p187 (= tptp.ord_le282106107riable (lambda @t510 (forall @t344 (=> @t520 @t519))))) % 0.45/0.95 (assume @p188 (forall @t439 (=> @t435 (not (=> @t438 (not @t437)))))) % 0.45/0.95 (assume @p189 (forall (@list @t340 @t373 @t433) (=> @t438 (=> @t459 @t458)))) % 0.45/0.95 (assume @p190 (forall (@list @t340 @t373 @t521) (=> @t438 (=> @t523 (_ @t522 @t373))))) % 0.45/0.95 (assume @p191 (forall @t398 (= @t524 (_ @t396 (_ @t387 @t393))))) % 0.45/0.95 (assume @p192 (forall @t407 (= @t525 (_ @t404 (_ @t388 @t399))))) % 0.45/0.95 (assume @p193 (forall (@list @t411 @t409 @t408) (= (_ @t412 (_ @t449 @t408)) @t526))) % 0.45/0.95 (assume @p194 (forall @t528 (= (_ @t421 (_ @t453 @t415)) @t527))) % 0.45/0.95 (assume @p195 (= tptp.inf_inf_variable_o (lambda (@list @t530 @t531 @t529) (_ (_ (_ tptp.inf_inf_variable_o @t531) @t530) @t529)))) % 0.45/0.95 (assume @p196 (= tptp.inf_inf_set_variable (lambda @t534 (_ (_ tptp.inf_inf_set_variable @t533) @t532)))) % 0.45/0.95 (assume @p197 (= tptp.inf_inf_variable_o (lambda (@list @t535 @t536 @t529) (_ (_ (_ tptp.inf_inf_variable_o @t536) @t535) @t529)))) % 0.45/0.95 (assume @p198 (= tptp.inf_inf_set_variable (lambda @t539 (_ (_ tptp.inf_inf_set_variable @t538) @t537)))) % 0.45/0.95 (assume @p199 (forall @t398 (= (_ @t444 @t393) @t524))) % 0.45/0.95 (assume @p200 (forall @t407 (= (_ @t447 @t399) @t525))) % 0.45/0.95 (assume @p201 (forall @t414 (= (_ @t451 @t408) @t526))) % 0.45/0.95 (assume @p202 (forall @t424 (= (_ @t455 @t415) @t527))) % 0.45/0.95 (assume @p203 (forall (@list @t543 @t540 @t411 @t409) (=> (= @t543 (_ @t541 @t411)) (= (_ @t449 @t543) @t542)))) % 0.45/0.95 (assume @p204 (forall (@list @t373 @t544 @t419 @t416) (=> (= @t373 (_ @t545 @t419)) (= (_ @t453 @t373) @t546)))) % 0.45/0.95 (assume @p205 (forall (@list @t547 @t540 @t409 @t411) (=> (= @t547 (_ @t541 @t409)) (= (_ (_ tptp.inf_inf_variable_o @t547) @t411) @t542)))) % 0.45/0.95 (assume @p206 (forall (@list @t340 @t544 @t416 @t419) (=> (= @t340 (_ @t545 @t416)) (= (_ @t378 @t419) @t546)))) % 0.45/0.95 (assume @p207 (forall @t515 (= @t549 (_ @t548 (_ @t378 @t374))))) % 0.45/0.95 (assume @p208 (forall @t439 (= (_ @t378 @t379) @t379))) % 0.45/0.95 (assume @p209 (= tptp.inf_inf_set_variable (lambda @t510 (_ (_ tptp.inf_inf_set_variable @t509) @t508)))) % 0.45/0.95 (assume @p210 (forall @t345 (= (_ @t378 @t340) @t340))) % 0.45/0.95 (assume @p211 (forall @t515 (= (_ (_ tptp.inf_inf_set_variable @t379) @t374) @t549))) % 0.45/0.95 (assume @p212 (forall @t461 (=> @t460 @t458))) % 0.45/0.95 (assume @p213 (forall @t461 (=> @t460 @t459))) % 0.45/0.95 (assume @p214 (forall @t461 (=> @t460 (not (=> @t459 (not @t458)))))) % 0.45/0.95 (assume @p215 @t551) % 0.45/0.95 (assume @p216 (forall (@list @t340 @t337) (_ (_ tptp.ord_le282106107riable @t552) @t340))) % 0.45/0.95 (assume @p217 (= tptp.inf_inf_set_variable (lambda @t510 (_ tptp.collect_variable (lambda @t344 (and @t520 @t519)))))) % 0.45/0.95 (assume @p218 (forall (@list @t521 @t340 @t337) (= (_ @t522 @t554) (and @t523 @t553)))) % 0.45/0.95 (assume @p219 (forall @t350 (= @t555 (_ (_ tptp.inf_inf_set_variable @t338) @t347)))) % 0.45/0.95 (assume @p220 (forall (@list @t419 @t415 @t416) (=> @t559 @t557))) % 0.45/0.95 (assume @p221 (forall (@list @t416 @t415 @t419) (=> @t418 @t557))) % 0.45/0.95 (assume @p222 (= tptp.ord_le282106107riable (lambda (@list @t538 @t537) (= @t560 @t538)))) % 0.45/0.95 (assume @p223 (= tptp.ord_le282106107riable (lambda @t539 (= @t560 @t537)))) % 0.45/0.95 (assume @p224 (forall @t456 (_ @t556 @t419))) % 0.45/0.95 (assume @p225 (forall @t456 (_ @t556 @t416))) % 0.45/0.95 (assume @p226 (= tptp.ord_le282106107riable (lambda @t539 (= @t537 @t560)))) % 0.45/0.95 (assume @p227 (forall @t407 (=> @t403 (=> @t401 @t406)))) % 0.45/0.95 (assume @p228 (forall @t424 (=> @t420 (=> @t418 @t423)))) % 0.45/0.95 (assume @p229 (forall @t424 (=> @t423 (not (=> @t420 (not @t418)))))) % 0.45/0.95 (assume @p230 (forall @t563 (=> @t562 (= @t446 @t402)))) % 0.45/0.95 (assume @p231 (forall @t448 (=> @t403 (= @t446 @t384)))) % 0.45/0.95 (assume @p232 (forall @t565 (=> @t564 (= @t454 @t419)))) % 0.45/0.95 (assume @p233 (forall @t456 (=> @t420 (= @t454 @t416)))) % 0.45/0.95 (assume @p234 (= tptp.ord_le282106107riable (lambda @t534 (= (_ (_ tptp.inf_inf_set_variable @t532) @t533) @t532)))) % 0.45/0.95 (assume @p235 (forall (@list @t566 @t384 @t402) (=> (forall @t573 (_ @t572 @t569)) (=> (forall @t573 (_ @t572 @t568)) (=> (forall (@list @t569 @t568 @t567) (=> @t571 (=> (_ @t570 @t567) (_ @t570 (_ (_ @t566 @t568) @t567))))) (= @t446 (_ (_ @t566 @t384) @t402))))))) % 0.45/0.95 (assume @p236 (forall @t456 (=> @t574 @t420))) % 0.45/0.95 (assume @p237 (forall @t456 (=> @t420 @t574))) % 0.45/0.95 (assume @p238 (forall (@list @t419 @t384 @t416) (=> (_ @t558 @t384) @t575))) % 0.45/0.95 (assume @p239 (forall (@list @t416 @t384 @t419) (=> (_ @t417 @t384) @t575))) % 0.45/0.95 (assume @p240 (forall (@list @t416 @t415 @t419 @t576) (=> @t418 (=> (_ @t558 @t576) (_ @t556 (_ (_ tptp.inf_inf_set_variable @t415) @t576)))))) % 0.45/0.95 (assume @p241 (forall @t580 (=> @t579 (=> @t578 @t577)))) % 0.45/0.95 (assume @p242 (forall @t580 (=> @t577 (not (=> @t579 (not @t578)))))) % 0.45/0.95 (assume @p243 (forall @t448 (_ @t581 @t402))) % 0.45/0.95 (assume @p244 (forall @t448 (_ @t581 @t384))) % 0.45/0.95 (assume @p245 (forall @t439 (= @t583 (forall @t344 (=> @t343 (forall (@list @t582) (=> (_ (_ tptp.member_variable @t582) @t373) (not (= @t341 @t582))))))))) % 0.45/0.95 (assume @p246 (forall @t345 (= (_ @t378 tptp.bot_bot_set_variable) tptp.bot_bot_set_variable))) % 0.45/0.95 (assume @p247 (forall (@list @t373) (= (_ @t385 @t373) tptp.bot_bot_set_variable))) % 0.45/0.95 (assume @p248 (forall @t439 (= @t583 (forall @t344 (=> @t343 (not @t584)))))) % 0.45/0.95 (assume @p249 (forall @t439 (=> (forall @t328 (=> @t442 (not @t441))) @t583))) % 0.45/0.95 (assume @p250 (forall (@list @t340 @t373 @t337 @t346) (=> @t438 (=> (forall @t328 (=> @t442 @t516)) (_ (_ tptp.ord_le282106107riable @t554) (_ @t548 @t347)))))) % 0.45/0.95 (assume @p251 (forall @t381 (=> @t377 (=> @t376 @t380)))) % 0.45/0.95 (assume @p252 (forall @t439 (=> @t438 (= @t379 @t340)))) % 0.45/0.95 (assume @p253 (forall (@list @t373 @t340) (=> @t437 (= @t379 @t373)))) % 0.45/0.95 (assume @p254 (forall @t439 (_ @t585 @t373))) % 0.45/0.95 (assume @p255 (forall @t439 (_ @t585 @t340))) % 0.45/0.95 (assume @p256 (forall (@list @t340 @t374 @t373 @t586) (=> @t514 (=> (_ @t436 @t586) (_ @t585 (_ (_ tptp.inf_inf_set_variable @t374) @t586)))))) % 0.45/0.95 (assume @p257 (forall @t386 (_ @t400 @t384))) % 0.45/0.95 (assume @p258 (forall @t345 (=> (forall @t328 (not @t442)) @t391))) % 0.45/0.95 (assume @p259 (forall @t457 (=> @t588 @t587))) % 0.45/0.95 (assume @p260 (forall @t457 (= @t588 @t587))) % 0.45/0.95 (assume @p261 (forall @t457 (_ @t392 @t416))) % 0.45/0.95 (assume @p262 (forall @t595 (=> @t594 @t593))) % 0.45/0.95 (assume @p263 (forall (@list @t599 @t597 @t598 @t596) (= (= @t600 (_ (_ tptp.geq @t598) @t596)) (and (= @t599 @t598) (= @t597 @t596))))) % 0.45/0.95 (assume @p264 (= tptp.some_trm tptp.some_trm)) % 0.45/0.95 (assume @p265 (forall @t157 (=> (forall @t601 (not (= @t152 @t493))) @t153))) % 0.45/0.95 (assume @p266 (forall (@list @t316 @t488) (=> (forall @t601 (_ @t316 @t493)) (=> @t318 (_ @t316 @t488))))) % 0.45/0.95 (assume @p267 (forall (@list @t603) (= (not (= @t603 tptp.none_game)) (exists (@list @t602) (= @t603 (_ tptp.some_game @t602)))))) % 0.45/0.95 (assume @p268 (forall (@list @t283 @t488 @t604) (=> (forall (@list @t492 @t606) (_ (_ @t283 @t493) (_ tptp.some_game @t606))) (=> (forall (@list @t605) (_ (_ @t283 @t605) tptp.none_game)) (=> (forall @t491 (_ (_ @t283 tptp.none_game) @t490)) (_ (_ @t283 @t488) @t604)))))) % 0.45/0.95 (assume @p269 (forall (@list @t70 @t68 @t599 @t597) (not (= @t71 @t600)))) % 0.45/0.95 (assume @p270 (forall @t611 (=> (_ @t417 @t610) @t609))) % 0.45/0.95 (assume @p271 (forall @t613 (=> @t420 (=> (_ (_ tptp.ord_le282106107riable @t610) @t415) @t612)))) % 0.45/0.95 (assume @p272 (forall @t611 (=> (= @t416 @t610) @t609))) % 0.45/0.95 (assume @p273 (forall @t613 (=> @t420 (=> (= @t610 @t415) @t612)))) % 0.45/0.95 (assume @p274 (= @t513 (lambda @t534 (and (_ (_ tptp.ord_le282106107riable @t532) @t533) (_ (_ tptp.ord_le282106107riable @t533) @t532))))) % 0.45/0.95 (assume @p275 (forall @t448 (=> @t403 (=> @t562 @t614)))) % 0.45/0.95 (assume @p276 (forall @t448 (=> @t614 @t403))) % 0.45/0.95 (assume @p277 (forall @t424 (=> @t420 @t615))) % 0.45/0.95 (assume @p278 (forall @t563 (=> @t562 (= @t403 @t614)))) % 0.45/0.95 (assume @p279 (= @t513 (lambda @t539 (and @t617 @t616)))) % 0.45/0.95 (assume @p280 (forall @t424 (=> @t618 @t615))) % 0.45/0.95 (assume @p281 (forall @t424 (=> @t420 (=> (= @t419 @t415) @t418)))) % 0.45/0.95 (assume @p282 (forall @t456 (=> @t420 (=> @t564 @t618)))) % 0.45/0.95 (assume @p283 (forall @t407 (=> @t403 (=> (_ @t561 @t399) @t401)))) % 0.45/0.95 (assume @p284 (forall @t457 (_ @t417 @t416))) % 0.45/0.95 (assume @p285 (forall @t528 (=> @t564 (=> (_ @t619 @t419) (_ @t619 @t416))))) % 0.45/0.95 (assume @p286 (= @t513 (lambda @t539 (and @t616 @t617)))) % 0.45/0.95 (assume @p287 (forall @t565 (=> @t564 (=> @t420 @t618)))) % 0.45/0.95 (assume @p288 (forall (@list @t521 @t622 @t620 @t337) (=> (_ @t522 @t622) (=> (_ (_ tptp.ord_le282106107riable @t622) @t621) @t553)))) % 0.45/0.95 (assume @p289 (forall (@list @t620 @t337) (_ (_ tptp.ord_le282106107riable @t621) @t620))) % 0.45/0.95 (assume @p290 (forall @t595 (=> @t594 (and @t248 @t623)))) % 0.45/0.95 (assume @p291 (forall @t595 (=> @t248 (=> @t623 @t593)))) % 0.45/0.95 (assume @p292 (forall (@list @t497 @t496 @t140 @t626 @t625 @t624) (=> @t499 (=> @t628 (=> (forall (@list @t627) (=> (_ @t496 @t627) (_ @t626 (_ @t624 @t627)))) (_ @t626 (_ (_ (_ tptp.case_o209804997ml_fml @t625) @t624) @t140))))))) % 0.45/0.95 (assume @p293 (forall (@list @t497 @t501 @t146 @t626 @t625 @t629) (=> @t502 (=> @t628 (=> (forall @t632 (=> @t631 (_ @t626 (_ @t629 @t630)))) (_ @t626 (_ (_ (_ tptp.case_o325794063ml_trm @t625) @t629) @t146))))))) % 0.45/0.95 (assume @p294 (forall (@list @t497 @t501 @t146 @t635 @t634 @t633) (=> @t502 (=> (=> @t497 (_ @t635 @t634)) (=> (forall @t632 (=> @t631 (_ @t635 (_ @t633 @t630)))) (_ @t635 (_ (_ (_ tptp.case_o487727941rm_trm @t634) @t633) @t146))))))) % 0.45/0.95 (assume @p295 (forall (@list @t146 @t636 @t249) (=> (= (_ (_ tptp.uSubst152838031e_Geqo @t146) @t636) @t249) (=> (forall @t484 (=> @t483 (forall (@list @t479) (=> (= @t636 @t480) (not (= @t249 (_ tptp.some_fml (_ (_ tptp.geq @t470) @t479)))))))) (=> (=> @t147 @t320) (not (=> (exists @t477 (= @t146 @t476)) (=> (= @t636 tptp.none_trm) @t320)))))))) % 0.45/0.95 (assume @p296 (forall @t641 (= (_ (_ tptp.inf_inf_variable_o @t640) @t639) (lambda @t344 (_ @t342 (_ (_ tptp.inf_inf_set_variable @t638) @t637)))))) % 0.45/0.95 (assume @p297 (forall (@list @t642) (= (_ (_ tptp.uSubst152838031e_Geqo tptp.none_trm) @t642) tptp.none_fml))) % 0.45/0.95 (assume @p298 (forall (@list @t472 @t642) (= (= (_ (_ tptp.uSubst152838031e_Geqo @t472) @t642) tptp.none_fml) (or @t473 (= @t642 tptp.none_trm))))) % 0.45/0.95 (assume @p299 (forall (@list @t643) (= (_ (_ tptp.uSubst152838031e_Geqo (_ tptp.some_trm @t643)) tptp.none_trm) tptp.none_fml))) % 0.45/0.95 (assume @p300 (forall (@list @t107 @t589) (= (_ (_ tptp.uSubst152838031e_Geqo (_ tptp.some_trm @t107)) (_ tptp.some_trm @t589)) (_ tptp.some_fml @t591)))) % 0.45/0.95 (assume @p301 (forall @t595 (= @t592 (_ (_ tptp.uSubst152838031e_Geqo @t246) @t590)))) % 0.45/0.95 (assume @p302 (forall @t641 (= (_ (_ tptp.ord_le1407353162able_o @t640) @t639) (_ (_ tptp.ord_le282106107riable @t638) @t637)))) % 0.45/0.95 (assume @p303 (forall @t431 (= @t432 (= @t337 tptp.bot_bot_variable_o)))) % 0.45/0.95 (assume @p304 (= tptp.produc1278328899on_fml tptp.produc1250175341on_fml)) % 0.45/0.95 (assume @p305 (= tptp.produc2141841102on_trm tptp.produc1231571704on_trm)) % 0.45/0.95 (assume @p306 (= tptp.produc377919108on_fml tptp.produc1615133358on_fml)) % 0.45/0.95 (assume @p307 (= tptp.produc1214549391on_trm tptp.produc1036610745on_trm)) % 0.45/0.95 (assume @p308 (= tptp.produc1598111045on_fml tptp.produc1420172399on_fml)) % 0.45/0.95 (assume @p309 (= tptp.produc1591622303on_fml tptp.produc347802313on_fml)) % 0.45/0.95 (assume @p310 (= tptp.produc2129367017on_trm tptp.produc885547027on_trm)) % 0.45/0.95 (assume @p311 (= tptp.produc1903410526on_fml tptp.produc154833544on_fml)) % 0.45/0.95 (assume @p312 (= tptp.produc293671592on_trm tptp.produc692578258on_trm)) % 0.45/0.95 (assume @p313 (= tptp.produc724717725on_fml tptp.produc1499310791on_fml)) % 0.45/0.95 (assume @p314 (forall @t653 (= @t652 (_ (_ (_ tptp.case_o487727941rm_trm tptp.none_trm) (lambda @t372 (_ (_ (_ tptp.case_o487727941rm_trm (_ tptp.some_trm (_ @t651 @t370))) (lambda @t650 (_ (_ (_ tptp.if_option_trm (= (_ @t649 @t57) tptp.bot_bot_set_variable)) (_ (_ (_ tptp.uSubst516392818stappt @t371) tptp.bot_bot_set_variable) @t648)) tptp.none_trm))) @t647))) @t246)))) % 0.45/0.95 (assume @p315 (forall (@list @t657 @t655 @t656 @t654) (= (= @t658 (_ (_ tptp.func @t656) @t654)) (and (= @t657 @t656) (= @t655 @t654))))) % 0.45/0.95 (assume @p316 (forall (@list @t54 @t644 @t660 @t57 @t107) (=> @t663 (=> (not @t661) @t659)))) % 0.45/0.95 (assume @p317 (forall (@list @t54 @t644 @t660 @t57 @t107 @t462) (=> @t663 (=> @t661 (=> @t464 (= @t652 (_ (_ (_ tptp.uSubst516392818stappt @t463) tptp.bot_bot_set_variable) @t660))))))) % 0.45/0.95 (assume @p318 (forall @t653 (=> (not @t659) (and @t248 (or (= @t647 tptp.none_trm) (exists @t667 (and (= @t647 @t666) @t665))))))) % 0.45/0.95 (assume @p319 (forall @t673 (=> @t672 (=> @t661 (= @t668 @t662))))) % 0.45/0.95 (assume @p320 (forall @t675 (=> (not (= @t668 tptp.none_trm)) @t674))) % 0.45/0.95 (assume @p321 (forall @t673 (=> @t672 (=> @t661 (= @t676 @t662))))) % 0.45/0.95 (assume @p322 (forall (@list @t678 @t677) (= (= @t679 (_ tptp.const @t677)) (= @t678 @t677)))) % 0.45/0.95 (assume @p323 (forall @t675 (= @t676 @t668))) % 0.45/0.95 (assume @p324 (forall (@list @t678 @t657 @t655) (not (= @t679 @t658)))) % 0.45/0.95 (assume @p325 (forall @t675 (=> (not (= @t676 tptp.none_trm)) @t674))) % 0.45/0.95 (assume @p326 (forall (@list @t373 @t340 @t337) (=> @t437 (= (_ @t436 @t552) (forall @t344 (=> @t584 @t429)))))) % 0.45/0.95 (assume @p327 (forall (@list @t373 @t340 @t346 @t337) (=> @t437 (=> (forall @t328 (=> @t441 (=> @t348 @t349))) (_ (_ tptp.ord_le282106107riable (_ tptp.collect_variable (lambda @t344 (and @t584 @t506)))) @t552))))) % 0.45/0.95 (assume @p328 (forall (@list @t340 @t337 @t346) (= (_ @t390 @t555) (and (_ @t390 @t338) (_ @t390 @t347))))) % 0.45/0.95 (assume @p329 (forall (@list @t680) (=> (forall @t494 (not (= @t680 (_ (_ tptp.produc2124676926on_fml @t493) @t330)))) (=> (forall (@list @t681) (not (= @t680 (_ (_ tptp.produc2124676926on_fml tptp.none_game) @t681)))) (not (forall @t491 (not (= @t680 (_ (_ tptp.produc2124676926on_fml @t490) tptp.none_fml))))))))) % 0.45/0.95 (assume @p330 (forall @t682 (= (_ (_ (_ tptp.if_option_fml false) @t140) @t249) @t249))) % 0.45/0.95 (assume @p331 (forall @t682 (= (_ (_ (_ tptp.if_option_fml true) @t140) @t249) @t140))) % 0.45/0.95 (assume @p332 (forall (@list @t497) (or (= @t497 true) (= @t497 false)))) % 0.45/0.95 (assume @p333 (forall @t683 (= (_ (_ (_ tptp.if_option_trm false) @t146) @t257) @t257))) % 0.45/0.95 (assume @p334 (forall @t683 (= (_ (_ (_ tptp.if_option_trm true) @t146) @t257) @t146))) % 0.45/0.95 (assume @p335 @t686) % 0.45/0.95 (assume @p336 true) % 0.45/0.95 (step @p337 (= tptp.produc1250175341on_fml @t693) :rule refl :args (@t693)) % 0.45/0.95 (step @p338 (= tptp.produc1231571704on_trm @t698) :rule refl :args (@t698)) % 0.45/0.95 (step @p339 (= tptp.produc1615133358on_fml @t700) :rule refl :args (@t700)) % 0.45/0.95 (step @p340 (= tptp.produc1036610745on_trm @t706) :rule refl :args (@t706)) % 0.45/0.95 (step @p341 (= tptp.produc1420172399on_fml @t708) :rule refl :args (@t708)) % 0.45/0.95 (step @p342 (= tptp.case_option_o_game @t713) :rule refl :args (@t713)) % 0.45/0.95 (step @p343 (= tptp.case_option_o_trm @t718) :rule refl :args (@t718)) % 0.45/0.95 (step @p344 (= tptp.case_option_o_fml @t723) :rule refl :args (@t723)) % 0.45/0.95 (step @p345 (= tptp.case_o209804997ml_fml @t726) :rule refl :args (@t726)) % 0.45/0.95 (step @p346 (= tptp.case_o325794063ml_trm @t728) :rule refl :args (@t728)) % 0.45/0.95 (step @p347 (= tptp.case_o487727941rm_trm @t731) :rule refl :args (@t731)) % 0.45/0.95 (step @p348 (= tptp.inf_inf_variable_o @t735) :rule refl :args (@t735)) % 0.45/0.95 (step @p349 (= tptp.inf_inf_set_variable @t738) :rule refl :args (@t738)) % 0.45/0.95 (step @p350 (= tptp.ord_le282106107riable @t739) :rule refl :args (@t739)) % 0.45/0.95 (step @p351 (= tptp.bot_bot_variable_o @t740) :rule refl :args (@t740)) % 0.45/0.95 (step @p352 (= tptp.is_empty_variable @t741) :rule refl :args (@t741)) % 0.45/0.95 (step @p353 (= tptp.uSubst1559070963pconst @t745) :rule refl :args (@t745)) % 0.45/0.95 (step @p354 :rule eq-symm :args (@t747 @t748)) % 0.45/0.95 (step @p355 :rule refl :args ((tptp.uSubst516392804stappf tptp.sigma tptp.va @t9))) % 0.45/0.95 (step @p356 :rule refl :args (@t746)) % 0.45/0.95 (step @p357 :rule refl :args (tptp.va)) % 0.45/0.95 (step @p358 :rule refl :args (tptp.sigma)) % 0.45/0.95 (step @p359 :rule cong :premises (@p358 @p357 @p356) :args (@t748)) % 0.45/0.95 (step @p360 :rule trans :premises (@p359 @p355)) % 0.45/0.95 (step @p361 :rule refl :args (@t42)) % 0.45/0.95 (step @p362 :rule ho_cong :premises (@p361 @p356)) % 0.45/0.95 (step @p363 :rule cong :premises (@p362 @p360) :args ((= (_ @t42 @t746) @t748))) % 0.45/0.95 (step @p364 :rule symm :premises (@p363)) % 0.45/0.95 (step @p365 :rule refl :args (@t43)) % 0.45/0.95 (step @p366 :rule eq_resolve :premises (@p365 @p364)) % 0.45/0.95 (step @p367 :rule refl :args (@t9)) % 0.45/0.95 (step @p368 :rule cong :premises (@p367 @p356) :args ((= @t9 @t746))) % 0.45/0.95 (step @p369 :rule symm :premises (@p368)) % 0.45/0.95 (step @p370 :rule eq_resolve :premises (@p367 @p369)) % 0.45/0.95 (step @p371 :rule refl :args (@t42)) % 0.45/0.95 (step @p372 :rule ho_cong :premises (@p371 @p370)) % 0.45/0.95 (step @p373 :rule trans :premises (@p372 @p366)) % 0.45/0.95 (step @p374 :rule refl :args ((tptp.uSubst516392804stappf tptp.sigma tptp.ua @t9))) % 0.45/0.95 (step @p375 :rule refl :args (tptp.ua)) % 0.45/0.95 (step @p376 :rule cong :premises (@p358 @p375 @p356) :args (@t747)) % 0.45/0.95 (step @p377 :rule trans :premises (@p376 @p374)) % 0.45/0.95 (step @p378 :rule refl :args (@t11)) % 0.45/0.95 (step @p379 :rule ho_cong :premises (@p378 @p356)) % 0.45/0.95 (step @p380 :rule cong :premises (@p379 @p377) :args ((= (_ @t11 @t746) @t747))) % 0.45/0.95 (step @p381 :rule symm :premises (@p380)) % 0.45/0.95 (step @p382 :rule refl :args (@t12)) % 0.45/0.95 (step @p383 :rule eq_resolve :premises (@p382 @p381)) % 0.45/0.95 (step @p384 :rule refl :args (@t11)) % 0.45/0.95 (step @p385 :rule ho_cong :premises (@p384 @p370)) % 0.45/0.95 (step @p386 :rule trans :premises (@p385 @p383)) % 0.45/0.95 (step @p387 :rule cong :premises (@p386 @p373) :args (@t60)) % 0.45/0.95 (step @p388 :rule trans :premises (@p387 @p354)) % 0.45/0.95 (step @p389 :rule cong :premises (@p388) :args ((not @t60))) % 0.45/0.95 (step @p390 :rule eq-symm :args (@t43 @t12)) % 0.45/0.95 (step @p391 :rule cong :premises (@p390) :args ((not (= @t43 @t12)))) % 0.45/0.95 (step @p392 :rule refl :args (@t12)) % 0.45/0.95 (step @p393 :rule eq-symm :args (@t752 tptp.none_fml)) % 0.45/0.95 (step @p394 :rule refl :args (tptp.none_fml)) % 0.45/0.95 (step @p395 :rule beta-reduce :args ((= (_ @t759 tptp.p) @t752))) % 0.45/0.95 (step @p396 :rule refl :args (tptp.p)) % 0.45/0.95 (step @p397 :rule beta-reduce :args ((= (_ (lambda @t760 (_ @t757 @t687)) tptp.sigma) @t759))) % 0.45/0.95 (step @p398 :rule refl :args (tptp.sigma)) % 0.45/0.95 (step @p399 :rule refl :args (@t687)) % 0.45/0.95 (step @p400 :rule beta-reduce :args ((= (_ @t765 @t688) @t756))) % 0.45/0.95 (step @p401 :rule refl :args (@t688)) % 0.45/0.95 (step @p402 :rule beta-reduce :args ((= (_ @t767 @t689) @t765))) % 0.45/0.95 (step @p403 :rule refl :args (@t689)) % 0.45/0.95 (step @p404 :rule beta-reduce :args ((= (_ (lambda @t24 @t766) @t690) @t767))) % 0.45/0.95 (step @p405 :rule refl :args (@t690)) % 0.45/0.95 (step @p406 :rule refl :args (@t15)) % 0.45/0.95 (step @p407 :rule alpha_equiv :args (@t768 (@list @t690) (@list @t749))) % 0.45/0.95 (step @p408 :rule refl :args (tptp.produc154833544on_fml)) % 0.45/0.95 (step @p409 :rule ho_cong :premises (@p408 @p407)) % 0.45/0.95 (step @p410 :rule ho_cong :premises (@p409 @p406)) % 0.45/0.95 (step @p411 :rule cong :premises (@p410) :args (@t770)) % 0.45/0.95 (step @p412 :rule ho_cong :premises (@p411 @p405)) % 0.45/0.95 (step @p413 :rule trans :premises (@p412 @p404)) % 0.45/0.95 (step @p414 :rule ho_cong :premises (@p413 @p403)) % 0.45/0.95 (step @p415 :rule trans :premises (@p414 @p402)) % 0.45/0.95 (step @p416 :rule ho_cong :premises (@p415 @p401)) % 0.45/0.95 (step @p417 :rule trans :premises (@p416 @p400)) % 0.45/0.95 (step @p418 :rule cong :premises (@p417) :args (@t771)) % 0.45/0.95 (step @p419 :rule refl :args (tptp.produc1499310791on_fml)) % 0.45/0.95 (step @p420 :rule ho_cong :premises (@p419 @p418)) % 0.45/0.95 (step @p421 :rule ho_cong :premises (@p420 @p399)) % 0.45/0.95 (step @p422 :rule cong :premises (@p421) :args (@t772)) % 0.45/0.95 (step @p423 :rule beta-reduce :args ((= (_ @t693 @t770) @t772))) % 0.45/0.95 (step @p424 :rule trans :premises (@p423 @p422)) % 0.45/0.95 (step @p425 :rule beta-reduce :args ((= (_ @t774 @t14) @t769))) % 0.45/0.95 (step @p426 :rule refl :args (@t14)) % 0.45/0.95 (step @p427 :rule beta-reduce :args ((= (_ (lambda @t775 (_ @t773 @t694)) @t15) @t774))) % 0.45/0.95 (step @p428 :rule refl :args (@t15)) % 0.45/0.95 (step @p429 :rule refl :args (@t694)) % 0.45/0.95 (step @p430 :rule beta-reduce :args ((= (_ @t776 @t688) @t755))) % 0.45/0.95 (step @p431 :rule beta-reduce :args ((= (_ @t778 @t695) @t776))) % 0.45/0.95 (step @p432 :rule refl :args (@t695)) % 0.45/0.95 (step @p433 :rule beta-reduce :args ((= @t780 @t778))) % 0.45/0.95 (step @p434 :rule ho_cong :premises (@p433 @p432)) % 0.45/0.95 (step @p435 :rule trans :premises (@p434 @p431)) % 0.45/0.95 (step @p436 :rule ho_cong :premises (@p435 @p401)) % 0.45/0.95 (step @p437 :rule trans :premises (@p436 @p430)) % 0.45/0.95 (step @p438 :rule cong :premises (@p437) :args (@t781)) % 0.45/0.95 (step @p439 :rule refl :args (tptp.produc154833544on_fml)) % 0.45/0.95 (step @p440 :rule ho_cong :premises (@p439 @p438)) % 0.45/0.95 (step @p441 :rule ho_cong :premises (@p440 @p429)) % 0.45/0.95 (step @p442 :rule cong :premises (@p441) :args (@t782)) % 0.45/0.95 (step @p443 :rule beta-reduce :args ((= (_ @t700 @t779) @t782))) % 0.45/0.95 (step @p444 :rule trans :premises (@p443 @p442)) % 0.45/0.95 (step @p445 :rule beta-reduce :args ((= (_ @t783 @t14) @t777))) % 0.45/0.95 (step @p446 :rule beta-reduce :args ((= (_ (lambda @t784 (_ @t754 @t701)) @t16) @t783))) % 0.45/0.95 (step @p447 :rule refl :args (@t16)) % 0.45/0.95 (step @p448 :rule refl :args (@t701)) % 0.45/0.95 (step @p449 :rule beta-reduce :args ((= (_ @t786 @t688) @t753))) % 0.45/0.95 (step @p450 :rule beta-reduce :args ((= (_ @t787 @t702) @t786))) % 0.45/0.95 (step @p451 :rule refl :args (@t702)) % 0.45/0.95 (step @p452 :rule beta-reduce :args ((= @t788 @t787))) % 0.45/0.95 (step @p453 :rule ho_cong :premises (@p452 @p451)) % 0.45/0.95 (step @p454 :rule trans :premises (@p453 @p450)) % 0.45/0.95 (step @p455 :rule ho_cong :premises (@p454 @p401)) % 0.45/0.95 (step @p456 :rule trans :premises (@p455 @p449)) % 0.45/0.95 (step @p457 :rule cong :premises (@p456) :args (@t789)) % 0.45/0.95 (step @p458 :rule refl :args (tptp.produc347802313on_fml)) % 0.45/0.95 (step @p459 :rule ho_cong :premises (@p458 @p457)) % 0.45/0.95 (step @p460 :rule ho_cong :premises (@p459 @p448)) % 0.45/0.95 (step @p461 :rule cong :premises (@p460) :args (@t790)) % 0.45/0.95 (step @p462 :rule beta-reduce :args ((= @t791 @t790))) % 0.45/0.95 (step @p463 :rule trans :premises (@p462 @p461)) % 0.45/0.95 (step @p464 :rule ho_cong :premises (@p463 @p447)) % 0.45/0.95 (step @p465 :rule trans :premises (@p464 @p446)) % 0.45/0.95 (step @p466 :rule ho_cong :premises (@p465 @p426)) % 0.45/0.95 (step @p467 :rule trans :premises (@p466 @p445)) % 0.45/0.95 (step @p468 :rule cong :premises (@p467) :args (@t792)) % 0.45/0.95 (step @p469 :rule refl :args (@t700)) % 0.45/0.95 (step @p470 :rule ho_cong :premises (@p469 @p468)) % 0.45/0.95 (step @p471 :rule trans :premises (@p470 @p444)) % 0.45/0.95 (step @p472 :rule ho_cong :premises (@p471 @p428)) % 0.45/0.95 (step @p473 :rule trans :premises (@p472 @p427)) % 0.45/0.95 (step @p474 :rule ho_cong :premises (@p473 @p426)) % 0.45/0.95 (step @p475 :rule trans :premises (@p474 @p425)) % 0.45/0.95 (step @p476 :rule cong :premises (@p475) :args (@t793)) % 0.45/0.95 (step @p477 :rule refl :args (@t693)) % 0.45/0.95 (step @p478 :rule ho_cong :premises (@p477 @p476)) % 0.45/0.95 (step @p479 :rule trans :premises (@p478 @p424)) % 0.45/0.95 (step @p480 :rule ho_cong :premises (@p479 @p398)) % 0.45/0.95 (step @p481 :rule trans :premises (@p480 @p397)) % 0.45/0.95 (step @p482 :rule ho_cong :premises (@p481 @p396)) % 0.45/0.95 (step @p483 :rule trans :premises (@p482 @p395)) % 0.45/0.95 (step @p484 :rule cong :premises (@p483 @p394) :args (@t795)) % 0.45/0.95 (step @p485 :rule trans :premises (@p484 @p393)) % 0.45/0.95 (step @p486 :rule eq-symm :args (@t43 tptp.none_fml)) % 0.45/0.95 (step @p487 :rule cong :premises (@p486) :args (@t684)) % 0.45/0.95 (step @p488 :rule nary_cong :premises (@p487 @p485) :args (@t796)) % 0.45/0.95 (step @p489 :rule cong :premises (@p488) :args ((not @t796))) % 0.45/0.95 (step @p490 :rule refl :args (@t20)) % 0.45/0.95 (step @p491 :rule ho_cong :premises (@p341 @p490)) % 0.45/0.95 (step @p492 :rule ho_cong :premises (@p491 @p447)) % 0.45/0.95 (step @p493 :rule ho_cong :premises (@p492 @p426)) % 0.45/0.95 (step @p494 :rule cong :premises (@p493) :args (@t22)) % 0.45/0.95 (step @p495 :rule ho_cong :premises (@p339 @p494)) % 0.45/0.95 (step @p496 :rule ho_cong :premises (@p495 @p428)) % 0.45/0.95 (step @p497 :rule ho_cong :premises (@p496 @p426)) % 0.45/0.95 (step @p498 :rule cong :premises (@p497) :args (@t25)) % 0.45/0.95 (step @p499 :rule ho_cong :premises (@p337 @p498)) % 0.45/0.95 (step @p500 :rule ho_cong :premises (@p499 @p398)) % 0.45/0.95 (step @p501 :rule ho_cong :premises (@p500 @p396)) % 0.45/0.95 (step @p502 :rule cong :premises (@p501 @p394) :args (@t41)) % 0.45/0.95 (step @p503 :rule refl :args (@t684)) % 0.45/0.95 (step @p504 :rule nary_cong :premises (@p503 @p502) :args (@t685)) % 0.45/0.95 (step @p505 :rule cong :premises (@p504) :args (@t686)) % 0.45/0.95 (step @p506 :rule trans :premises (@p505 @p489)) % 0.45/0.95 (step @p507 :rule eq_resolve :premises (@p335 @p506)) % 0.45/0.95 (step @p508 :rule not_or_elim :premises (@p507) :args (0)) % 0.45/0.95 (step @p509 :rule not_not_elim :premises (@p508)) % 0.45/0.95 (step @p510 :rule cong :premises (@p509 @p392) :args (@t797)) % 0.45/0.95 (step @p511 :rule cong :premises (@p510) :args ((not @t797))) % 0.45/0.95 (step @p512 :rule trans :premises (@p511 @p391)) % 0.45/0.95 (step @p513 :rule eq-symm :args (@t12 tptp.none_fml)) % 0.45/0.95 (step @p514 :rule cong :premises (@p513) :args (@t13)) % 0.45/0.95 (step @p515 :rule trans :premises (@p514 @p512 @p389)) % 0.45/0.95 (step @p516 :rule eq_resolve :premises (@p2 @p515)) % 0.45/0.95 (step @p517 :rule refl :args ((tptp.uSubst516392804stappf @t32 @t804 @t800))) % 0.45/0.95 (step @p518 :rule refl :args ((tptp.the_fml @t799))) % 0.45/0.95 (step @p519 :rule refl :args (@t805)) % 0.45/0.95 (step @p520 :rule cong :premises (@p519) :args (@t806)) % 0.45/0.95 (step @p521 :rule trans :premises (@p520 @p518)) % 0.45/0.95 (step @p522 :rule refl :args (@t807)) % 0.45/0.95 (step @p523 :rule refl :args ((tptp.uSubst1408967625substt @t31))) % 0.45/0.95 (step @p524 :rule refl :args ((tptp.the_trm @t30))) % 0.45/0.95 (step @p525 :rule refl :args (@t808)) % 0.45/0.95 (step @p526 :rule cong :premises (@p525) :args (@t809)) % 0.45/0.95 (step @p527 :rule trans :premises (@p526 @p524)) % 0.45/0.95 (step @p528 :rule cong :premises (@p527) :args (@t810)) % 0.45/0.95 (step @p529 :rule trans :premises (@p528 @p523)) % 0.45/0.95 (step @p530 :rule cong :premises (@p529 @p522 @p521) :args (@t811)) % 0.45/0.95 (step @p531 :rule trans :premises (@p530 @p517)) % 0.45/0.95 (step @p532 :rule refl :args (tptp.uSubst516392804stappf)) % 0.45/0.95 (step @p533 :rule ho_cong :premises (@p532 @p529)) % 0.45/0.95 (step @p534 :rule ho_cong :premises (@p533 @p522)) % 0.45/0.95 (step @p535 :rule ho_cong :premises (@p534 @p521)) % 0.45/0.95 (step @p536 :rule cong :premises (@p535 @p531) :args ((= (_ (_ (_ tptp.uSubst516392804stappf @t810) @t807) @t806) @t811))) % 0.45/0.95 (step @p537 :rule symm :premises (@p536)) % 0.45/0.95 (step @p538 :rule refl :args ((_ (_ @t33 @t804) @t800))) % 0.45/0.95 (step @p539 :rule eq_resolve :premises (@p538 @p537)) % 0.45/0.95 (step @p540 :rule refl :args (tptp.the_fml)) % 0.45/0.95 (step @p541 :rule ho_cong :premises (@p540 @p519)) % 0.45/0.95 (step @p542 :rule cong :premises (@p541 @p521) :args ((= (_ tptp.the_fml @t805) @t806))) % 0.45/0.95 (step @p543 :rule symm :premises (@p542)) % 0.45/0.95 (step @p544 :rule refl :args (@t800)) % 0.45/0.95 (step @p545 :rule eq_resolve :premises (@p544 @p543)) % 0.45/0.95 (step @p546 :rule refl :args (@t799)) % 0.45/0.95 (step @p547 :rule cong :premises (@p546 @p519) :args ((= @t799 @t805))) % 0.45/0.95 (step @p548 :rule symm :premises (@p547)) % 0.45/0.95 (step @p549 :rule eq_resolve :premises (@p546 @p548)) % 0.45/0.95 (step @p550 :rule eq-refl :args (@t751)) % 0.45/0.95 (step @p551 :rule skolem_intro :args (@t798)) % 0.45/0.95 (step @p552 :rule refl :args (@t751)) % 0.45/0.95 (step @p553 :rule cong :premises (@p552 @p551) :args ((= @t751 @t798))) % 0.45/0.95 (step @p554 :rule trans :premises (@p553 @p550)) % 0.45/0.95 (step @p555 :rule true_elim :premises (@p554)) % 0.45/0.95 (step @p556 :rule ho_cong :premises (@p419 @p555)) % 0.45/0.95 (step @p557 :rule ho_cong :premises (@p556 @p398)) % 0.45/0.95 (step @p558 :rule trans :premises (@p557 @p549)) % 0.45/0.95 (step @p559 :rule refl :args (tptp.the_fml)) % 0.45/0.95 (step @p560 :rule ho_cong :premises (@p559 @p558)) % 0.45/0.95 (step @p561 :rule trans :premises (@p560 @p545)) % 0.45/0.95 (step @p562 :rule refl :args (@t804)) % 0.45/0.95 (step @p563 :rule cong :premises (@p562 @p522) :args ((= @t804 @t807))) % 0.45/0.95 (step @p564 :rule symm :premises (@p563)) % 0.45/0.95 (step @p565 :rule eq_resolve :premises (@p562 @p564)) % 0.45/0.95 (step @p566 :rule eq-refl :args (@t802)) % 0.45/0.95 (step @p567 :rule refl :args (@t802)) % 0.45/0.95 (step @p568 :rule symm :premises (@p567)) % 0.45/0.95 (step @p569 :rule refl :args (@t802)) % 0.45/0.95 (step @p570 :rule cong :premises (@p569 @p568) :args ((= @t802 @t802))) % 0.45/0.95 (step @p571 :rule trans :premises (@p570 @p566)) % 0.45/0.95 (step @p572 :rule skolem_intro :args (@t803)) % 0.45/0.95 (step @p573 :rule cong :premises (@p569 @p572) :args ((= @t802 @t803))) % 0.45/0.95 (step @p574 :rule trans :premises (@p573 @p571)) % 0.45/0.95 (step @p575 :rule true_elim :premises (@p574)) % 0.45/0.95 (step @p576 :rule refl :args (tptp.collect_variable)) % 0.45/0.95 (step @p577 :rule ho_cong :premises (@p576 @p575)) % 0.45/0.95 (step @p578 :rule trans :premises (@p577 @p565)) % 0.45/0.95 (step @p579 :rule refl :args (tptp.uSubst1408967625substt)) % 0.45/0.95 (step @p580 :rule ho_cong :premises (@p579 @p527)) % 0.45/0.95 (step @p581 :rule cong :premises (@p580 @p529) :args ((= (_ tptp.uSubst1408967625substt @t809) @t810))) % 0.45/0.95 (step @p582 :rule symm :premises (@p581)) % 0.45/0.95 (step @p583 :rule refl :args (@t32)) % 0.45/0.95 (step @p584 :rule eq_resolve :premises (@p583 @p582)) % 0.45/0.95 (step @p585 :rule refl :args (tptp.the_trm)) % 0.45/0.95 (step @p586 :rule ho_cong :premises (@p585 @p525)) % 0.45/0.95 (step @p587 :rule cong :premises (@p586 @p527) :args ((= (_ tptp.the_trm @t808) @t809))) % 0.45/0.95 (step @p588 :rule symm :premises (@p587)) % 0.45/0.95 (step @p589 :rule refl :args (@t31)) % 0.45/0.95 (step @p590 :rule eq_resolve :premises (@p589 @p588)) % 0.45/0.95 (step @p591 :rule refl :args (@t30)) % 0.45/0.95 (step @p592 :rule cong :premises (@p591 @p525) :args ((= @t30 @t808))) % 0.45/0.95 (step @p593 :rule symm :premises (@p592)) % 0.45/0.95 (step @p594 :rule eq_resolve :premises (@p591 @p593)) % 0.45/0.95 (step @p595 :rule refl :args (tptp.the_trm)) % 0.45/0.95 (step @p596 :rule ho_cong :premises (@p595 @p594)) % 0.45/0.95 (step @p597 :rule trans :premises (@p596 @p590)) % 0.45/0.95 (step @p598 :rule refl :args (tptp.uSubst1408967625substt)) % 0.45/0.95 (step @p599 :rule ho_cong :premises (@p598 @p597)) % 0.45/0.95 (step @p600 :rule trans :premises (@p599 @p584)) % 0.45/0.95 (step @p601 :rule refl :args (tptp.uSubst516392804stappf)) % 0.45/0.95 (step @p602 :rule ho_cong :premises (@p601 @p600)) % 0.45/0.95 (step @p603 :rule ho_cong :premises (@p602 @p578)) % 0.45/0.95 (step @p604 :rule ho_cong :premises (@p603 @p561)) % 0.45/0.95 (step @p605 :rule trans :premises (@p604 @p539)) % 0.45/0.95 (step @p606 :rule cong :premises (@p373 @p605) :args (@t814)) % 0.45/0.95 (step @p607 :rule eq-symm :args (@t819 @t807)) % 0.45/0.95 (step @p608 :rule refl :args (@t819)) % 0.45/0.95 (step @p609 :rule refl :args (@t820)) % 0.45/0.95 (step @p610 :rule cong :premises (@p609 @p608) :args ((= @t820 @t819))) % 0.45/0.95 (step @p611 :rule symm :premises (@p610)) % 0.45/0.95 (step @p612 :rule eq_resolve :premises (@p609 @p611)) % 0.45/0.95 (step @p613 :rule eq-refl :args (@t817)) % 0.45/0.95 (step @p614 :rule skolem_intro :args (@t818)) % 0.45/0.95 (step @p615 :rule refl :args (@t817)) % 0.45/0.95 (step @p616 :rule cong :premises (@p615 @p614) :args ((= @t817 @t818))) % 0.45/0.95 (step @p617 :rule trans :premises (@p616 @p613)) % 0.45/0.95 (step @p618 :rule true_elim :premises (@p617)) % 0.45/0.95 (step @p619 :rule ho_cong :premises (@p576 @p618)) % 0.45/0.95 (step @p620 :rule trans :premises (@p619 @p612)) % 0.45/0.95 (step @p621 :rule cong :premises (@p620 @p578) :args (@t822)) % 0.45/0.95 (step @p622 :rule trans :premises (@p621 @p607)) % 0.45/0.95 (step @p623 :rule cong :premises (@p622 @p606) :args (@t823)) % 0.45/0.95 (step @p624 :rule cong :premises (@p623) :args (@t824)) % 0.45/0.95 (step @p625 :rule refl :args (@t814)) % 0.45/0.95 (step @p626 :rule eq-symm :args (@t813 @t821)) % 0.45/0.95 (step @p627 :rule cong :premises (@p626 @p625) :args (@t826)) % 0.45/0.95 (step @p628 :rule cong :premises (@p627) :args ((not @t826))) % 0.45/0.95 (step @p629 :rule refl :args (@t812)) % 0.45/0.95 (step @p630 :rule symm :premises (@p567)) % 0.45/0.95 (step @p631 :rule alpha_equiv :args (@t550 (@list @t341) (@list @t801))) % 0.45/0.95 (step @p632 :rule trans :premises (@p631 @p630)) % 0.45/0.95 (step @p633 :rule ho_cong :premises (@p576 @p632)) % 0.45/0.95 (step @p634 :rule refl :args (tptp.bot_bot_set_variable)) % 0.45/0.95 (step @p635 :rule cong :premises (@p634 @p633) :args (@t551)) % 0.45/0.95 (step @p636 :rule eq_resolve :premises (@p215 @p635)) % 0.45/0.95 (step @p637 :rule refl :args (@t33)) % 0.45/0.95 (step @p638 :rule ho_cong :premises (@p637 @p636)) % 0.45/0.95 (step @p639 :rule ho_cong :premises (@p638 @p629)) % 0.45/0.95 (step @p640 :rule cong :premises (@p509 @p639) :args (@t828)) % 0.45/0.95 (step @p641 :rule refl :args (@t821)) % 0.45/0.95 (step @p642 :rule cong :premises (@p636 @p641) :args (@t829)) % 0.45/0.95 (step @p643 :rule cong :premises (@p642 @p640) :args (@t830)) % 0.45/0.95 (step @p644 :rule cong :premises (@p643) :args ((not @t830))) % 0.45/0.95 (step @p645 :rule trans :premises (@p644 @p628)) % 0.45/0.95 (step @p646 :rule eq-symm :args (@t827 tptp.none_fml)) % 0.45/0.95 (step @p647 :rule ho_cong :premises (@p559 @p483)) % 0.45/0.95 (step @p648 :rule refl :args (@t34)) % 0.45/0.95 (step @p649 :rule ho_cong :premises (@p648 @p647)) % 0.45/0.95 (step @p650 :rule cong :premises (@p649 @p394) :args (@t833)) % 0.45/0.95 (step @p651 :rule trans :premises (@p650 @p646)) % 0.45/0.95 (step @p652 :rule eq-symm :args (@t821 tptp.bot_bot_set_variable)) % 0.45/0.95 (step @p653 :rule beta-reduce :args ((= (_ @t834 tptp.va) @t821))) % 0.45/0.95 (step @p654 :rule refl :args (tptp.va)) % 0.45/0.95 (step @p655 :rule beta-reduce :args ((= (_ @t836 @t815) @t834))) % 0.45/0.95 (step @p656 :rule refl :args (tptp.static_FVF)) % 0.45/0.95 (step @p657 :rule ho_cong :premises (@p656 @p647)) % 0.45/0.95 (step @p658 :rule refl :args (@t836)) % 0.45/0.95 (step @p659 :rule ho_cong :premises (@p658 @p657)) % 0.45/0.95 (step @p660 :rule trans :premises (@p659 @p655)) % 0.45/0.95 (step @p661 :rule ho_cong :premises (@p660 @p654)) % 0.45/0.95 (step @p662 :rule trans :premises (@p661 @p653)) % 0.45/0.95 (step @p663 :rule cong :premises (@p662 @p634) :args (@t837)) % 0.45/0.95 (step @p664 :rule trans :premises (@p663 @p652)) % 0.45/0.95 (step @p665 :rule cong :premises (@p664 @p651) :args (@t838)) % 0.45/0.95 (step @p666 :rule cong :premises (@p665) :args ((not @t838))) % 0.45/0.95 (step @p667 :rule ho_cong :premises (@p559 @p501)) % 0.45/0.95 (step @p668 :rule ho_cong :premises (@p648 @p667)) % 0.45/0.95 (step @p669 :rule cong :premises (@p668 @p394) :args (@t36)) % 0.45/0.95 (step @p670 :rule ho_cong :premises (@p656 @p667)) % 0.45/0.95 (step @p671 :rule beta-reduce :args ((= @t839 @t519))) % 0.45/0.95 (step @p672 :rule refl :args (@t835)) % 0.45/0.95 (step @p673 :rule ho_cong :premises (@p672 @p671)) % 0.45/0.95 (step @p674 :rule cong :premises (@p673) :args (@t840)) % 0.45/0.95 (step @p675 :rule beta-reduce :args ((= (_ (lambda @t841 (_ @t835 @t733)) @t736) @t840))) % 0.45/0.95 (step @p676 :rule trans :premises (@p675 @p674)) % 0.45/0.95 (step @p677 :rule refl :args (@t736)) % 0.45/0.95 (step @p678 :rule refl :args (@t733)) % 0.45/0.95 (step @p679 :rule beta-reduce :args ((= @t842 @t520))) % 0.45/0.95 (step @p680 :rule refl :args (tptp.inf_inf_o)) % 0.45/0.95 (step @p681 :rule ho_cong :premises (@p680 @p679)) % 0.45/0.95 (step @p682 :rule ho_cong :premises (@p681 @p678)) % 0.45/0.95 (step @p683 :rule cong :premises (@p682) :args (@t843)) % 0.45/0.95 (step @p684 :rule beta-reduce :args ((= (_ @t735 @t737) @t843))) % 0.45/0.95 (step @p685 :rule trans :premises (@p684 @p683)) % 0.45/0.95 (step @p686 :rule ho_cong :premises (@p685 @p677)) % 0.45/0.95 (step @p687 :rule trans :premises (@p686 @p676)) % 0.45/0.95 (step @p688 :rule ho_cong :premises (@p576 @p687)) % 0.45/0.95 (step @p689 :rule refl :args (@t737)) % 0.45/0.95 (step @p690 :rule ho_cong :premises (@p348 @p689)) % 0.45/0.95 (step @p691 :rule ho_cong :premises (@p690 @p677)) % 0.45/0.95 (step @p692 :rule ho_cong :premises (@p576 @p691)) % 0.45/0.95 (step @p693 :rule trans :premises (@p692 @p688)) % 0.45/0.95 (step @p694 :rule cong :premises (@p693) :args (@t738)) % 0.45/0.95 (step @p695 :rule trans :premises (@p349 @p694)) % 0.45/0.95 (step @p696 :rule ho_cong :premises (@p695 @p670)) % 0.45/0.95 (step @p697 :rule ho_cong :premises (@p696 @p654)) % 0.45/0.95 (step @p698 :rule cong :premises (@p697 @p634) :args (@t38)) % 0.45/0.95 (step @p699 :rule cong :premises (@p698 @p669) :args (@t39)) % 0.45/0.95 (step @p700 :rule cong :premises (@p699) :args (@t40)) % 0.45/0.95 (step @p701 :rule trans :premises (@p700 @p666)) % 0.45/0.95 (step @p702 :rule trans :premises (@p701 @p645 @p624)) % 0.45/0.95 (step @p703 :rule eq_resolve :premises (@p3 @p702)) % 0.45/0.95 (step @p704 :rule refl :args (@t844)) % 0.45/0.95 (step @p705 :rule bool-double-not-elim :args (@t845)) % 0.45/0.95 (step @p706 :rule nary_cong :premises (@p705 @p704) :args ((or (not (not @t845)) @t844))) % 0.45/0.95 (step @p707 :rule cong :premises (@p373 @p558) :args (@t846)) % 0.45/0.95 (step @p708 :rule cong :premises (@p624 @p707) :args ((=> @t824 @t846))) % 0.45/0.95 (step @p709 :rule refl :args (@t846)) % 0.45/0.95 (step @p710 :rule aci_norm :args ((= (and @t823 true) @t823))) % 0.45/0.95 (step @p711 :rule bool-impl-true1 :args ((not @t822))) % 0.45/0.95 (step @p712 :rule eq-refl :args (@t43)) % 0.45/0.95 (step @p713 :rule cong :premises (@p626) :args (@t847)) % 0.45/0.95 (step @p714 :rule cong :premises (@p713 @p712) :args (@t848)) % 0.45/0.95 (step @p715 :rule trans :premises (@p714 @p711)) % 0.45/0.95 (step @p716 :rule nary_cong :premises (@p627 @p715) :args (@t849)) % 0.45/0.95 (step @p717 :rule trans :premises (@p716 @p710)) % 0.45/0.95 (step @p718 :rule cong :premises (@p717) :args (@t850)) % 0.45/0.95 (step @p719 :rule cong :premises (@p718 @p709) :args ((=> @t850 @t846))) % 0.45/0.95 (step @p720 :rule refl :args (@t752)) % 0.45/0.95 (step @p721 :rule cong :premises (@p509 @p720) :args (@t851)) % 0.45/0.95 (step @p722 :rule refl :args (@t43)) % 0.45/0.95 (step @p723 :rule cong :premises (@p509 @p722) :args (@t44)) % 0.45/0.95 (step @p724 :rule cong :premises (@p642) :args (@t852)) % 0.45/0.95 (step @p725 :rule cong :premises (@p724 @p723) :args (@t853)) % 0.45/0.95 (step @p726 :rule cong :premises (@p722 @p639) :args (@t854)) % 0.45/0.95 (step @p727 :rule cong :premises (@p642 @p726) :args (@t855)) % 0.45/0.95 (step @p728 :rule nary_cong :premises (@p727 @p725) :args (@t856)) % 0.45/0.95 (step @p729 :rule cong :premises (@p728) :args (@t857)) % 0.45/0.95 (step @p730 :rule cong :premises (@p729 @p721) :args ((=> @t857 @t851))) % 0.45/0.95 (step @p731 :rule trans :premises (@p730 @p719)) % 0.45/0.95 (step @p732 :rule refl :args (@t44)) % 0.45/0.95 (step @p733 :rule cong :premises (@p664) :args (@t858)) % 0.45/0.95 (step @p734 :rule cong :premises (@p733 @p732) :args (@t859)) % 0.45/0.95 (step @p735 :rule eq-symm :args (@t827 @t43)) % 0.45/0.95 (step @p736 :rule cong :premises (@p649 @p722) :args (@t860)) % 0.45/0.95 (step @p737 :rule trans :premises (@p736 @p735)) % 0.45/0.95 (step @p738 :rule cong :premises (@p664 @p737) :args (@t861)) % 0.45/0.95 (step @p739 :rule nary_cong :premises (@p738 @p734) :args (@t862)) % 0.45/0.95 (step @p740 :rule cong :premises (@p739) :args (@t863)) % 0.45/0.95 (step @p741 :rule cong :premises (@p740 @p485) :args ((=> @t863 @t795))) % 0.45/0.95 (step @p742 :rule cong :premises (@p698) :args (@t45)) % 0.45/0.95 (step @p743 :rule cong :premises (@p742 @p732) :args (@t46)) % 0.45/0.95 (step @p744 :rule cong :premises (@p668 @p722) :args (@t47)) % 0.45/0.95 (step @p745 :rule cong :premises (@p698 @p744) :args (@t48)) % 0.45/0.95 (step @p746 :rule nary_cong :premises (@p745 @p743) :args (@t49)) % 0.45/0.95 (step @p747 :rule cong :premises (@p746) :args (@t50)) % 0.45/0.95 (step @p748 :rule cong :premises (@p747 @p502) :args (@t51)) % 0.45/0.95 (step @p749 :rule trans :premises (@p748 @p741)) % 0.45/0.95 (step @p750 :rule trans :premises (@p749 @p731 @p708)) % 0.45/0.95 (step @p751 :rule eq_resolve :premises (@p4 @p750)) % 0.45/0.95 (step @p752 :rule implies_elim :premises (@p751)) % 0.45/0.95 (step @p753 :rule eq_resolve :premises (@p752 @p706)) % 0.45/0.95 (step @p754 :rule chain_m_resolution :premises (@p753 @p703) :args (@t844 (@list true) (@list @t845))) % 0.45/0.95 (step @p755 :rule cong :premises (@p707 @p388) :args ((=> @t846 @t60))) % 0.45/0.95 (step @p756 :rule refl :args (@t60)) % 0.45/0.95 (step @p757 :rule cong :premises (@p721 @p756) :args ((=> @t851 @t60))) % 0.45/0.95 (step @p758 :rule cong :premises (@p485 @p756) :args ((=> @t795 @t60))) % 0.45/0.95 (step @p759 :rule cong :premises (@p502 @p756) :args (@t61)) % 0.45/0.95 (step @p760 :rule trans :premises (@p759 @p758)) % 0.45/0.95 (step @p761 :rule trans :premises (@p760 @p757 @p755)) % 0.45/0.95 (step @p762 :rule eq_resolve :premises (@p6 @p761)) % 0.45/0.95 (step @p763 :rule implies_elim :premises (@p762)) % 0.45/0.95 (step @p764 :rule reordering :premises (@p763) :args ((or @t864 (not @t844)))) % 0.45/0.95 (step @p765 false :rule chain_m_resolution :premises (@p764 @p754 @p516) :args (false (@list false true) (@list @t844 @t864))) % 0.45/0.95 ) % 0.45/0.95 % SZS output end Proof % 0.45/0.95 % cvc5 exiting %------------------------------------------------------------------------------