%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP181^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 : n020.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:18 AM UTC 2026 % Result : Theorem 0.48s 0.89s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP181^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n020.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 04:18:10 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.62 %----Proving TH0 % 0.48/0.89 --- 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.48/0.89 % SZS status Theorem % 0.48/0.89 % SZS output start Proof % 0.48/0.89 ( % 0.48/0.89 (declare-sort tptp.late_freeRes 0) % 0.48/0.89 (declare-sort tptp.pi 0) % 0.48/0.89 (declare-sort tptp.name 0) % 0.48/0.89 (declare-sort tptp.noption_name 0) % 0.48/0.89 (declare-sort tptp.produc1141751126_pi_pi 0) % 0.48/0.89 (declare-sort tptp.noptio1575811931_pi_pi 0) % 0.48/0.89 (declare-sort tptp.noption_Late_freeRes 0) % 0.48/0.89 (declare-sort tptp.noption_pi 0) % 0.48/0.89 (declare-sort tptp.set_Pr1834926343_pi_pi 0) % 0.48/0.89 (declare-sort tptp.set_Pr1569510577ion_pi 0) % 0.48/0.89 (declare-sort tptp.produc629157763_pi_pi 0) % 0.48/0.89 (declare-sort tptp.set_Pr1694908217_pi_pi 0) % 0.48/0.89 (declare-sort tptp.produc405342261i_name 0) % 0.48/0.89 (declare-sort tptp.set_Pr1294453099i_name 0) % 0.48/0.89 (declare-sort tptp.produc53907987_pi_pi 0) % 0.48/0.89 (declare-sort tptp.set_Pr100209225_pi_pi 0) % 0.48/0.89 (declare-sort tptp.produc1834551554reeRes 0) % 0.48/0.89 (declare-sort tptp.set_Pr305743074reeRes 0) % 0.48/0.89 (declare-sort tptp.set_Pr1654044726_pi_pi 0) % 0.48/0.89 (declare-sort tptp.late_residual 0) % 0.48/0.89 (declare-sort tptp.produc1462499409ion_pi 0) % 0.48/0.89 (declare-sort tptp.product_prod_pi_pi 0) % 0.48/0.89 (declare-sort tptp.produc1217648014ion_pi 0) % 0.48/0.89 (declare-sort tptp.produc992857746Res_pi 0) % 0.48/0.89 (declare-sort tptp.produc2052722628s_name 0) % 0.48/0.89 (declare-sort tptp.produc2008547984reeRes 0) % 0.48/0.89 (declare-sort tptp.produc1357834675reeRes 0) % 0.48/0.89 (declare-sort tptp.produc1961110975reeRes 0) % 0.48/0.89 (declare-sort tptp.produc1559976732_pi_pi 0) % 0.48/0.89 (declare-sort tptp.late_subject 0) % 0.48/0.89 (declare-sort tptp.product_prod_name_pi 0) % 0.48/0.89 (declare-sort tptp.produc1443308494i_name 0) % 0.48/0.89 (declare-sort tptp.produc367475239e_name 0) % 0.48/0.89 (declare-sort tptp.product_prod_pi_name 0) % 0.48/0.89 (declare-sort tptp.produc649380958reeRes 0) % 0.48/0.89 (declare-const tptp.member558706512_pi_pi (-> tptp.product_prod_pi_pi tptp.set_Pr1834926343_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.product_Pair_pi_pi (-> tptp.pi tptp.pi tptp.product_prod_pi_pi)) % 0.48/0.89 (declare-const tptp.late_BoundR (-> tptp.late_subject tptp.name tptp.pi tptp.late_residual)) % 0.48/0.89 (declare-const tptp.late_FreeR (-> tptp.late_freeRes tptp.pi tptp.late_residual)) % 0.48/0.89 (declare-const tptp.late_transitions (-> tptp.pi tptp.late_residual Bool)) % 0.48/0.89 (declare-const tptp.strong2129052853vative (-> tptp.pi tptp.pi tptp.late_subject tptp.name tptp.set_Pr1834926343_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.fresh_name_pi (-> tptp.name tptp.pi Bool)) % 0.48/0.89 (declare-const tptp.subs (-> tptp.pi tptp.name tptp.name tptp.pi)) % 0.48/0.89 (declare-const tptp.output (-> tptp.name tptp.name tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.fresh_1093033124n_name (-> tptp.name (-> tptp.name tptp.noption_name) Bool)) % 0.48/0.89 (declare-const tptp.abs_fun_name_name (-> tptp.name tptp.name tptp.name tptp.noption_name)) % 0.48/0.89 (declare-const tptp.late_OutputR (-> tptp.name tptp.name tptp.late_freeRes)) % 0.48/0.89 (declare-const tptp.late_BoundOutputS (-> tptp.name tptp.late_subject)) % 0.48/0.89 (declare-const tptp.ord_le1032043601ion_pi (-> tptp.set_Pr1569510577ion_pi tptp.set_Pr1569510577ion_pi Bool)) % 0.48/0.89 (declare-const tptp.abs_fu385186459_pi_pi (-> tptp.name tptp.produc1141751126_pi_pi tptp.name tptp.noptio1575811931_pi_pi)) % 0.48/0.89 (declare-const tptp.member772629402_pi_pi (-> tptp.produc629157763_pi_pi tptp.set_Pr1694908217_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.ord_le1854926745_pi_pi (-> tptp.set_Pr1694908217_pi_pi tptp.set_Pr1694908217_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.abs_fu681348580reeRes (-> tptp.name tptp.late_freeRes tptp.name tptp.noption_Late_freeRes)) % 0.48/0.89 (declare-const tptp.member1353687244i_name (-> tptp.produc405342261i_name tptp.set_Pr1294453099i_name Bool)) % 0.48/0.89 (declare-const tptp.ord_le2082425291i_name (-> tptp.set_Pr1294453099i_name tptp.set_Pr1294453099i_name Bool)) % 0.48/0.89 (declare-const tptp.member695660714_pi_pi (-> tptp.produc53907987_pi_pi tptp.set_Pr100209225_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.ord_le211833513_pi_pi (-> tptp.set_Pr100209225_pi_pi tptp.set_Pr100209225_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.member2081207979reeRes (-> tptp.produc1834551554reeRes tptp.set_Pr305743074reeRes Bool)) % 0.48/0.89 (declare-const tptp.ord_le1762471042reeRes (-> tptp.set_Pr305743074reeRes tptp.set_Pr305743074reeRes Bool)) % 0.48/0.89 (declare-const tptp.ord_le797229014_pi_pi (-> tptp.set_Pr1654044726_pi_pi tptp.set_Pr1654044726_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.fresh_93646139ame_pi (-> tptp.name tptp.product_prod_name_pi Bool)) % 0.48/0.89 (declare-const tptp.product_Pair_name_pi (-> tptp.name tptp.pi tptp.product_prod_name_pi)) % 0.48/0.89 (declare-const tptp.sum (-> tptp.pi tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.fresh_1963366730reeRes (-> tptp.name tptp.produc2008547984reeRes Bool)) % 0.48/0.89 (declare-const tptp.mismatch (-> tptp.name tptp.name tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.produc1531804426reeRes (-> tptp.name tptp.late_freeRes tptp.produc2008547984reeRes)) % 0.48/0.89 (declare-const tptp.tau (-> tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.fresh_1847501388Res_pi (-> tptp.name tptp.produc992857746Res_pi Bool)) % 0.48/0.89 (declare-const tptp.produc1701355766s_name (-> tptp.late_freeRes tptp.name tptp.produc2052722628s_name)) % 0.48/0.89 (declare-const tptp.fresh_493808761reeRes (-> tptp.name tptp.produc1357834675reeRes Bool)) % 0.48/0.89 (declare-const tptp.late_InputS (-> tptp.name tptp.late_subject)) % 0.48/0.89 (declare-const tptp.collec1051790738_pi_pi (-> (-> tptp.product_prod_pi_pi Bool) tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (declare-const tptp.fresh_1641682979reeRes (-> tptp.name tptp.late_freeRes Bool)) % 0.48/0.89 (declare-const tptp.fresh_785364841reeRes (-> tptp.name (-> tptp.name tptp.noption_Late_freeRes) Bool)) % 0.48/0.89 (declare-const tptp.p tptp.pi) % 0.48/0.89 (declare-const tptp.fresh_1504024600reeRes (-> tptp.name tptp.produc649380958reeRes Bool)) % 0.48/0.89 (declare-const tptp.late_TauR tptp.late_freeRes) % 0.48/0.89 (declare-const tptp.produc1244821099reeRes (-> tptp.late_freeRes tptp.late_freeRes tptp.produc1357834675reeRes)) % 0.48/0.89 (declare-const tptp.fresh_2065563522_pi_pi (-> tptp.name (-> tptp.name tptp.noptio1575811931_pi_pi) Bool)) % 0.48/0.89 (declare-const tptp.rel tptp.set_Pr1834926343_pi_pi) % 0.48/0.89 (declare-const tptp.produc1505598906reeRes (-> (-> tptp.name tptp.noption_pi) tptp.late_freeRes tptp.produc1834551554reeRes)) % 0.48/0.89 (declare-const tptp.fresh_717452603ubject (-> tptp.name tptp.late_subject Bool)) % 0.48/0.89 (declare-const tptp.a tptp.late_subject) % 0.48/0.89 (declare-const tptp.q tptp.pi) % 0.48/0.89 (declare-const tptp.fresh_81631222sidual (-> tptp.name tptp.late_residual Bool)) % 0.48/0.89 (declare-const tptp.fresh_2007541374s_name (-> tptp.name tptp.produc2052722628s_name Bool)) % 0.48/0.89 (declare-const tptp.id_name_noption_pi tptp.set_Pr1569510577ion_pi) % 0.48/0.89 (declare-const tptp.eqvt_pi (-> tptp.set_Pr1834926343_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.x tptp.name) % 0.48/0.89 (declare-const tptp.produc674047040ion_pi (-> (-> tptp.name tptp.noption_pi) tptp.produc1462499409ion_pi tptp.produc1217648014ion_pi)) % 0.48/0.89 (declare-const tptp.fresh_441084397e_name (-> tptp.name tptp.produc367475239e_name Bool)) % 0.48/0.89 (declare-const tptp.produc235456326_pi_pi (-> tptp.name tptp.product_prod_pi_pi tptp.produc1141751126_pi_pi)) % 0.48/0.89 (declare-const tptp.produc1638681944reeRes (-> tptp.pi tptp.late_freeRes tptp.produc649380958reeRes)) % 0.48/0.89 (declare-const tptp.fresh_1376661020_pi_pi (-> tptp.name tptp.produc1141751126_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.produc1177552196Res_pi (-> tptp.late_freeRes tptp.pi tptp.produc992857746Res_pi)) % 0.48/0.89 (declare-const tptp.pq tptp.pi) % 0.48/0.89 (declare-const tptp.produc1820286517_pi_pi (-> (-> tptp.name tptp.noption_pi) tptp.pi tptp.produc629157763_pi_pi)) % 0.48/0.89 (declare-const tptp.y tptp.name) % 0.48/0.89 (declare-const tptp.fresh_225680151ion_pi (-> tptp.name tptp.produc1462499409ion_pi Bool)) % 0.48/0.89 (declare-const tptp.produc1570949143e_name (-> tptp.name tptp.name tptp.produc367475239e_name)) % 0.48/0.89 (declare-const tptp.res (-> tptp.name tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.fresh_1335311330_pi_pi (-> tptp.name tptp.produc1559976732_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.piNil tptp.pi) % 0.48/0.89 (declare-const tptp.product_Pair_pi_name (-> tptp.pi tptp.name tptp.product_prod_pi_name)) % 0.48/0.89 (declare-const tptp.fresh_261416607i_name (-> tptp.name tptp.product_prod_pi_name Bool)) % 0.48/0.89 (declare-const tptp.fresh_1627595501_pi_pi (-> tptp.name tptp.product_prod_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.fresh_1711070152reeRes (-> tptp.name tptp.produc1834551554reeRes Bool)) % 0.48/0.89 (declare-const tptp.produc540578151i_name (-> (-> tptp.name tptp.noption_pi) tptp.name tptp.produc405342261i_name)) % 0.48/0.89 (declare-const tptp.fresh_453496559i_name (-> tptp.name tptp.produc405342261i_name Bool)) % 0.48/0.89 (declare-const tptp.fresh_253309757_pi_pi (-> tptp.name tptp.produc629157763_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.member540268543_pi_pi (-> tptp.produc1141751126_pi_pi tptp.set_Pr1654044726_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.fresh_543891186ion_pi (-> tptp.name (-> tptp.name tptp.noption_pi) Bool)) % 0.48/0.89 (declare-const tptp.produc1342893193ion_pi (-> (-> tptp.name tptp.noption_pi) (-> tptp.name tptp.noption_pi) tptp.produc1462499409ion_pi)) % 0.48/0.89 (declare-const tptp.produc1275980869_pi_pi (-> (-> tptp.name tptp.noption_pi) tptp.produc1141751126_pi_pi tptp.produc53907987_pi_pi)) % 0.48/0.89 (declare-const tptp.par (-> tptp.pi tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.fresh_975559885_pi_pi (-> tptp.name tptp.produc53907987_pi_pi Bool)) % 0.48/0.89 (declare-const tptp.produc703114481reeRes (-> (-> tptp.name tptp.noption_pi) tptp.produc1834551554reeRes tptp.produc1961110975reeRes)) % 0.48/0.89 (declare-const tptp.fresh_1729533561reeRes (-> tptp.name tptp.produc1961110975reeRes Bool)) % 0.48/0.89 (declare-const tptp.produc1024533510i_name (-> (-> tptp.name tptp.noption_pi) tptp.produc405342261i_name tptp.produc1443308494i_name)) % 0.48/0.89 (declare-const tptp.fresh_1513292180i_name (-> tptp.name tptp.produc1443308494i_name Bool)) % 0.48/0.89 (declare-const tptp.produc1189045204_pi_pi (-> (-> tptp.name tptp.noption_pi) tptp.produc629157763_pi_pi tptp.produc1559976732_pi_pi)) % 0.48/0.89 (declare-const tptp.input (-> tptp.name tptp.name tptp.pi tptp.pi)) % 0.48/0.89 (declare-const tptp.id_pi tptp.set_Pr1834926343_pi_pi) % 0.48/0.89 (declare-const tptp.abs_fun_name_pi (-> tptp.name tptp.pi tptp.name tptp.noption_pi)) % 0.48/0.89 (declare-const tptp.member1632198138ion_pi (-> tptp.produc1462499409ion_pi tptp.set_Pr1569510577ion_pi Bool)) % 0.48/0.89 (define tptp.ord_le630093991_pi_pi () (let ((_let_1 (@var "B6" tptp.set_Pr1834926343_pi_pi))) (let ((_let_2 (@var "T" tptp.product_prod_pi_pi))) (let ((_let_3 (_ tptp.member558706512_pi_pi _let_2))) (let ((_let_4 (@var "A6" tptp.set_Pr1834926343_pi_pi))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.48/0.89 (define tptp.strong743114133lation () (let ((_let_1 (@var "Rel2" tptp.set_Pr1834926343_pi_pi))) (let ((_let_2 (@var "Q6" tptp.pi))) (let ((_let_3 (@var "P8" tptp.pi))) (let ((_let_4 (@var "Alpha3" tptp.late_freeRes))) (let ((_let_5 (_ tptp.late_FreeR _let_4))) (let ((_let_6 (@var "P7" tptp.pi))) (let ((_let_7 (_ tptp.late_transitions _let_6))) (let ((_let_8 (@list _let_3))) (let ((_let_9 (@var "Q5" tptp.pi))) (let ((_let_10 (_ tptp.late_transitions _let_9))) (let ((_let_11 (@var "X4" tptp.name))) (let ((_let_12 (@var "A5" tptp.late_subject))) (let ((_let_13 (_ (_ tptp.late_BoundR _let_12) _let_11))) (lambda (@list _let_6 _let_1 _let_9) (and (forall (@list _let_12 _let_11 _let_2) (=> (and (_ _let_10 (_ _let_13 _let_2)) (_ (_ tptp.fresh_name_pi _let_11) _let_6)) (exists _let_8 (and (_ _let_7 (_ _let_13 _let_3)) (_ (_ (_ (_ (_ tptp.strong2129052853vative _let_3) _let_2) _let_12) _let_11) _let_1))))) (forall (@list _let_4 _let_2) (=> (_ _let_10 (_ _let_5 _let_2)) (exists _let_8 (and (_ _let_7 (_ _let_5 _let_3)) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi _let_3) _let_2)) _let_1))))))))))))))))))))) % 0.48/0.89 (define tptp.fresh_name_name () (let ((_let_1 (@var "B5" tptp.name))) (let ((_let_2 (@var "A5" tptp.name))) (lambda (@list _let_2 _let_1) (not (= _let_2 _let_1)))))) % 0.48/0.89 (define @t1 () (_ (_ tptp.product_Pair_pi_pi tptp.p) tptp.q)) % 0.48/0.89 (define @t2 () (_ tptp.fresh_1376661020_pi_pi tptp.y)) % 0.48/0.89 (define @t3 () (_ tptp.res tptp.x)) % 0.48/0.89 (define @t4 () (_ @t3 (_ (_ tptp.sum tptp.p) tptp.q))) % 0.48/0.89 (define @t5 () (_ tptp.fresh_name_pi tptp.y)) % 0.48/0.89 (define @t6 () (@var "Y" tptp.late_freeRes)) % 0.48/0.89 (define @t7 () (@var "A" tptp.name)) % 0.48/0.89 (define @t8 () (_ tptp.fresh_1641682979reeRes @t7)) % 0.48/0.89 (define @t9 () (_ @t8 @t6)) % 0.48/0.89 (define @t10 () (@var "X" tptp.late_freeRes)) % 0.48/0.89 (define @t11 () (_ @t8 @t10)) % 0.48/0.89 (define @t12 () (@var "Y" tptp.name)) % 0.48/0.89 (define @t13 () (_ tptp.fresh_name_name @t7)) % 0.48/0.89 (define @t14 () (_ @t13 @t12)) % 0.48/0.89 (define @t15 () (@var "Y" tptp.pi)) % 0.48/0.89 (define @t16 () (_ tptp.fresh_name_pi @t7)) % 0.48/0.89 (define @t17 () (_ @t16 @t15)) % 0.48/0.89 (define @t18 () (@var "X" tptp.name)) % 0.48/0.89 (define @t19 () (_ @t13 @t18)) % 0.48/0.89 (define @t20 () (@var "X" tptp.pi)) % 0.48/0.89 (define @t21 () (_ @t16 @t20)) % 0.48/0.89 (define @t22 () (_ tptp.fresh_1627595501_pi_pi @t7)) % 0.48/0.89 (define @t23 () (_ @t22 (_ (_ tptp.product_Pair_pi_pi @t20) @t15))) % 0.48/0.89 (define @t24 () (@list @t7 @t20 @t15)) % 0.48/0.89 (define @t25 () (@var "Y" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t26 () (_ @t22 @t25)) % 0.48/0.89 (define @t27 () (and @t19 @t26)) % 0.48/0.89 (define @t28 () (_ (_ tptp.produc235456326_pi_pi @t18) @t25)) % 0.48/0.89 (define @t29 () (_ tptp.fresh_1376661020_pi_pi @t7)) % 0.48/0.89 (define @t30 () (_ @t29 @t28)) % 0.48/0.89 (define @t31 () (= @t30 @t27)) % 0.48/0.89 (define @t32 () (@list @t7 @t18 @t25)) % 0.48/0.89 (define @t33 () (forall @t32 @t31)) % 0.48/0.89 (define @t34 () (@var "X1" tptp.pi)) % 0.48/0.89 (define @t35 () (_ @t16 @t34)) % 0.48/0.89 (define @t36 () (@var "X2" tptp.pi)) % 0.48/0.89 (define @t37 () (and (_ @t16 @t36) @t35)) % 0.48/0.89 (define @t38 () (_ (_ tptp.sum @t36) @t34)) % 0.48/0.89 (define @t39 () (@list @t7 @t36 @t34)) % 0.48/0.89 (define @t40 () (@var "P2" tptp.pi)) % 0.48/0.89 (define @t41 () (_ tptp.res @t12)) % 0.48/0.89 (define @t42 () (_ @t41 @t40)) % 0.48/0.89 (define @t43 () (@var "A" tptp.late_subject)) % 0.48/0.89 (define @t44 () (_ tptp.late_BoundR @t43)) % 0.48/0.89 (define @t45 () (_ @t44 @t18)) % 0.48/0.89 (define @t46 () (@var "P" tptp.pi)) % 0.48/0.89 (define @t47 () (_ tptp.late_transitions (_ @t41 @t46))) % 0.48/0.89 (define @t48 () (_ @t47 (_ @t45 @t42))) % 0.48/0.89 (define @t49 () (_ tptp.fresh_717452603ubject @t18)) % 0.48/0.89 (define @t50 () (_ @t49 @t43)) % 0.48/0.89 (define @t51 () (_ tptp.fresh_name_pi @t18)) % 0.48/0.89 (define @t52 () (_ @t51 @t46)) % 0.48/0.89 (define @t53 () (not (= @t12 @t18))) % 0.48/0.89 (define @t54 () (_ (_ tptp.fresh_717452603ubject @t12) @t43)) % 0.48/0.89 (define @t55 () (_ @t45 @t40)) % 0.48/0.89 (define @t56 () (_ tptp.late_transitions @t46)) % 0.48/0.89 (define @t57 () (_ @t56 @t55)) % 0.48/0.89 (define @t58 () (@list @t46 @t43 @t18 @t40 @t12)) % 0.48/0.89 (define @t59 () (_ tptp.fresh_name_pi @t12)) % 0.48/0.89 (define @t60 () (_ @t59 @t46)) % 0.48/0.89 (define @t61 () (@var "X" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t62 () (_ tptp.fresh_1711070152reeRes @t7)) % 0.48/0.89 (define @t63 () (_ @t62 (_ (_ tptp.produc1505598906reeRes @t61) @t6))) % 0.48/0.89 (define @t64 () (@list @t7 @t61 @t6)) % 0.48/0.89 (define @t65 () (_ tptp.fresh_453496559i_name @t7)) % 0.48/0.89 (define @t66 () (_ @t65 (_ (_ tptp.produc540578151i_name @t61) @t12))) % 0.48/0.89 (define @t67 () (@list @t7 @t61 @t12)) % 0.48/0.89 (define @t68 () (_ tptp.fresh_253309757_pi_pi @t7)) % 0.48/0.89 (define @t69 () (_ @t68 (_ (_ tptp.produc1820286517_pi_pi @t61) @t15))) % 0.48/0.89 (define @t70 () (@list @t7 @t61 @t15)) % 0.48/0.89 (define @t71 () (@var "Y" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t72 () (_ tptp.fresh_543891186ion_pi @t7)) % 0.48/0.89 (define @t73 () (_ (_ tptp.fresh_225680151ion_pi @t7) (_ (_ tptp.produc1342893193ion_pi @t61) @t71))) % 0.48/0.89 (define @t74 () (@list @t7 @t61 @t71)) % 0.48/0.89 (define @t75 () (@var "Y" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t76 () (_ (_ tptp.fresh_975559885_pi_pi @t7) (_ (_ tptp.produc1275980869_pi_pi @t61) @t75))) % 0.48/0.89 (define @t77 () (@list @t7 @t61 @t75)) % 0.48/0.89 (define @t78 () (@var "Y" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t79 () (_ (_ tptp.fresh_1729533561reeRes @t7) (_ (_ tptp.produc703114481reeRes @t61) @t78))) % 0.48/0.89 (define @t80 () (@list @t7 @t61 @t78)) % 0.48/0.89 (define @t81 () (@var "Y" tptp.produc405342261i_name)) % 0.48/0.89 (define @t82 () (_ (_ tptp.fresh_1513292180i_name @t7) (_ (_ tptp.produc1024533510i_name @t61) @t81))) % 0.48/0.89 (define @t83 () (@list @t7 @t61 @t81)) % 0.48/0.89 (define @t84 () (@var "Y" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t85 () (_ (_ tptp.fresh_1335311330_pi_pi @t7) (_ (_ tptp.produc1189045204_pi_pi @t61) @t84))) % 0.48/0.89 (define @t86 () (@list @t7 @t61 @t84)) % 0.48/0.89 (define @t87 () (_ @t72 @t61)) % 0.48/0.89 (define @t88 () (_ @t59 @t40)) % 0.48/0.89 (define @t89 () (@var "Y2" tptp.pi)) % 0.48/0.89 (define @t90 () (= @t36 @t89)) % 0.48/0.89 (define @t91 () (@var "Y1" tptp.pi)) % 0.48/0.89 (define @t92 () (= @t34 @t91)) % 0.48/0.89 (define @t93 () (@var "Y2" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t94 () (@var "X2" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t95 () (@var "Y1" tptp.name)) % 0.48/0.89 (define @t96 () (@var "X1" tptp.name)) % 0.48/0.89 (define @t97 () (= @t96 @t95)) % 0.48/0.89 (define @t98 () (@var "Y2" tptp.late_freeRes)) % 0.48/0.89 (define @t99 () (@var "X2" tptp.late_freeRes)) % 0.48/0.89 (define @t100 () (= @t99 @t98)) % 0.48/0.89 (define @t101 () (@var "Y1" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t102 () (@var "X1" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t103 () (= @t102 @t101)) % 0.48/0.89 (define @t104 () (@var "Y2" tptp.name)) % 0.48/0.89 (define @t105 () (@var "X2" tptp.name)) % 0.48/0.89 (define @t106 () (= @t105 @t104)) % 0.48/0.89 (define @t107 () (@var "Y2" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t108 () (@var "X2" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t109 () (@var "Y2" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t110 () (@var "X2" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t111 () (@var "Y2" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t112 () (@var "X2" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t113 () (@var "Y2" tptp.produc405342261i_name)) % 0.48/0.89 (define @t114 () (@var "X2" tptp.produc405342261i_name)) % 0.48/0.89 (define @t115 () (@var "Y2" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t116 () (@var "X2" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t117 () (@var "B2" tptp.pi)) % 0.48/0.89 (define @t118 () (@var "B" tptp.pi)) % 0.48/0.89 (define @t119 () (= @t118 @t117)) % 0.48/0.89 (define @t120 () (@var "A2" tptp.pi)) % 0.48/0.89 (define @t121 () (@var "A" tptp.pi)) % 0.48/0.89 (define @t122 () (= @t121 @t120)) % 0.48/0.89 (define @t123 () (_ tptp.product_Pair_pi_pi @t121)) % 0.48/0.89 (define @t124 () (_ @t123 @t118)) % 0.48/0.89 (define @t125 () (= @t124 (_ (_ tptp.product_Pair_pi_pi @t120) @t117))) % 0.48/0.89 (define @t126 () (@list @t121 @t118 @t120 @t117)) % 0.48/0.89 (define @t127 () (@var "B2" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t128 () (@var "B" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t129 () (= @t128 @t127)) % 0.48/0.89 (define @t130 () (@var "A2" tptp.name)) % 0.48/0.89 (define @t131 () (= @t7 @t130)) % 0.48/0.89 (define @t132 () (= (_ (_ tptp.produc235456326_pi_pi @t7) @t128) (_ (_ tptp.produc235456326_pi_pi @t130) @t127))) % 0.48/0.89 (define @t133 () (@list @t7 @t128 @t130 @t127)) % 0.48/0.89 (define @t134 () (@var "B2" tptp.late_freeRes)) % 0.48/0.89 (define @t135 () (@var "B" tptp.late_freeRes)) % 0.48/0.89 (define @t136 () (= @t135 @t134)) % 0.48/0.89 (define @t137 () (@var "A2" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t138 () (@var "A" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t139 () (= @t138 @t137)) % 0.48/0.89 (define @t140 () (= (_ (_ tptp.produc1505598906reeRes @t138) @t135) (_ (_ tptp.produc1505598906reeRes @t137) @t134))) % 0.48/0.89 (define @t141 () (@list @t138 @t135 @t137 @t134)) % 0.48/0.89 (define @t142 () (@var "B2" tptp.name)) % 0.48/0.89 (define @t143 () (@var "B" tptp.name)) % 0.48/0.89 (define @t144 () (= @t143 @t142)) % 0.48/0.89 (define @t145 () (= (_ (_ tptp.produc540578151i_name @t138) @t143) (_ (_ tptp.produc540578151i_name @t137) @t142))) % 0.48/0.89 (define @t146 () (@list @t138 @t143 @t137 @t142)) % 0.48/0.89 (define @t147 () (= (_ (_ tptp.produc1820286517_pi_pi @t138) @t118) (_ (_ tptp.produc1820286517_pi_pi @t137) @t117))) % 0.48/0.89 (define @t148 () (@list @t138 @t118 @t137 @t117)) % 0.48/0.89 (define @t149 () (@var "B2" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t150 () (@var "B" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t151 () (= @t150 @t149)) % 0.48/0.89 (define @t152 () (_ tptp.produc1342893193ion_pi @t138)) % 0.48/0.89 (define @t153 () (_ @t152 @t150)) % 0.48/0.89 (define @t154 () (= @t153 (_ (_ tptp.produc1342893193ion_pi @t137) @t149))) % 0.48/0.89 (define @t155 () (@list @t138 @t150 @t137 @t149)) % 0.48/0.89 (define @t156 () (@var "B2" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t157 () (@var "B" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t158 () (= @t157 @t156)) % 0.48/0.89 (define @t159 () (= (_ (_ tptp.produc1275980869_pi_pi @t138) @t157) (_ (_ tptp.produc1275980869_pi_pi @t137) @t156))) % 0.48/0.89 (define @t160 () (@list @t138 @t157 @t137 @t156)) % 0.48/0.89 (define @t161 () (@var "B2" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t162 () (@var "B" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t163 () (= @t162 @t161)) % 0.48/0.89 (define @t164 () (= (_ (_ tptp.produc703114481reeRes @t138) @t162) (_ (_ tptp.produc703114481reeRes @t137) @t161))) % 0.48/0.89 (define @t165 () (@list @t138 @t162 @t137 @t161)) % 0.48/0.89 (define @t166 () (@var "B2" tptp.produc405342261i_name)) % 0.48/0.89 (define @t167 () (@var "B" tptp.produc405342261i_name)) % 0.48/0.89 (define @t168 () (= @t167 @t166)) % 0.48/0.89 (define @t169 () (= (_ (_ tptp.produc1024533510i_name @t138) @t167) (_ (_ tptp.produc1024533510i_name @t137) @t166))) % 0.48/0.89 (define @t170 () (@list @t138 @t167 @t137 @t166)) % 0.48/0.89 (define @t171 () (@var "B2" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t172 () (@var "B" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t173 () (= @t172 @t171)) % 0.48/0.89 (define @t174 () (= (_ (_ tptp.produc1189045204_pi_pi @t138) @t172) (_ (_ tptp.produc1189045204_pi_pi @t137) @t171))) % 0.48/0.89 (define @t175 () (@list @t138 @t172 @t137 @t171)) % 0.48/0.89 (define @t176 () (@var "Pi" tptp.pi)) % 0.48/0.89 (define @t177 () (@var "Name" tptp.name)) % 0.48/0.89 (define @t178 () (_ (_ tptp.res @t177) @t176)) % 0.48/0.89 (define @t179 () (@var "Pi2" tptp.pi)) % 0.48/0.89 (define @t180 () (@var "Pi1" tptp.pi)) % 0.48/0.89 (define @t181 () (_ (_ tptp.sum @t180) @t179)) % 0.48/0.89 (define @t182 () (@list @t180 @t179 @t177 @t176)) % 0.48/0.89 (define @t183 () (@var "Rs" tptp.late_residual)) % 0.48/0.89 (define @t184 () (_ @t56 @t183)) % 0.48/0.89 (define @t185 () (@var "Prod" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t186 () (@var "P" (-> tptp.product_prod_pi_pi Bool))) % 0.48/0.89 (define @t187 () (@var "B3" tptp.pi)) % 0.48/0.89 (define @t188 () (@var "A3" tptp.pi)) % 0.48/0.89 (define @t189 () (_ (_ tptp.product_Pair_pi_pi @t188) @t187)) % 0.48/0.89 (define @t190 () (@list @t188 @t187)) % 0.48/0.89 (define @t191 () (forall @t190 (_ @t186 @t189))) % 0.48/0.89 (define @t192 () (@var "Prod" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t193 () (@var "P" (-> tptp.produc1141751126_pi_pi Bool))) % 0.48/0.89 (define @t194 () (@var "B3" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t195 () (@var "A3" tptp.name)) % 0.48/0.89 (define @t196 () (_ tptp.produc235456326_pi_pi @t195)) % 0.48/0.89 (define @t197 () (_ @t196 @t194)) % 0.48/0.89 (define @t198 () (@list @t195 @t194)) % 0.48/0.89 (define @t199 () (forall @t198 (_ @t193 @t197))) % 0.48/0.89 (define @t200 () (@var "Prod" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t201 () (@var "P" (-> tptp.produc1834551554reeRes Bool))) % 0.48/0.89 (define @t202 () (@var "B3" tptp.late_freeRes)) % 0.48/0.89 (define @t203 () (@var "A3" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t204 () (_ (_ tptp.produc1505598906reeRes @t203) @t202)) % 0.48/0.89 (define @t205 () (@list @t203 @t202)) % 0.48/0.89 (define @t206 () (forall @t205 (_ @t201 @t204))) % 0.48/0.89 (define @t207 () (@var "Prod" tptp.produc405342261i_name)) % 0.48/0.89 (define @t208 () (@var "P" (-> tptp.produc405342261i_name Bool))) % 0.48/0.89 (define @t209 () (@var "B3" tptp.name)) % 0.48/0.89 (define @t210 () (_ (_ tptp.produc540578151i_name @t203) @t209)) % 0.48/0.89 (define @t211 () (@list @t203 @t209)) % 0.48/0.89 (define @t212 () (forall @t211 (_ @t208 @t210))) % 0.48/0.89 (define @t213 () (@var "Prod" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t214 () (@var "P" (-> tptp.produc629157763_pi_pi Bool))) % 0.48/0.89 (define @t215 () (_ (_ tptp.produc1820286517_pi_pi @t203) @t187)) % 0.48/0.89 (define @t216 () (@list @t203 @t187)) % 0.48/0.89 (define @t217 () (forall @t216 (_ @t214 @t215))) % 0.48/0.89 (define @t218 () (@var "Prod" tptp.produc1462499409ion_pi)) % 0.48/0.89 (define @t219 () (@var "P" (-> tptp.produc1462499409ion_pi Bool))) % 0.48/0.89 (define @t220 () (@var "B3" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t221 () (_ (_ tptp.produc1342893193ion_pi @t203) @t220)) % 0.48/0.89 (define @t222 () (@list @t203 @t220)) % 0.48/0.89 (define @t223 () (forall @t222 (_ @t219 @t221))) % 0.48/0.89 (define @t224 () (@var "Prod" tptp.produc53907987_pi_pi)) % 0.48/0.89 (define @t225 () (@var "P" (-> tptp.produc53907987_pi_pi Bool))) % 0.48/0.89 (define @t226 () (@var "B3" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t227 () (_ tptp.produc1275980869_pi_pi @t203)) % 0.48/0.89 (define @t228 () (_ @t227 @t226)) % 0.48/0.89 (define @t229 () (@list @t203 @t226)) % 0.48/0.89 (define @t230 () (forall @t229 (_ @t225 @t228))) % 0.48/0.89 (define @t231 () (@var "Prod" tptp.produc1961110975reeRes)) % 0.48/0.89 (define @t232 () (@var "P" (-> tptp.produc1961110975reeRes Bool))) % 0.48/0.89 (define @t233 () (@var "B3" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t234 () (_ (_ tptp.produc703114481reeRes @t203) @t233)) % 0.48/0.89 (define @t235 () (@list @t203 @t233)) % 0.48/0.89 (define @t236 () (forall @t235 (_ @t232 @t234))) % 0.48/0.89 (define @t237 () (@var "Prod" tptp.produc1443308494i_name)) % 0.48/0.89 (define @t238 () (@var "P" (-> tptp.produc1443308494i_name Bool))) % 0.48/0.89 (define @t239 () (@var "B3" tptp.produc405342261i_name)) % 0.48/0.89 (define @t240 () (_ (_ tptp.produc1024533510i_name @t203) @t239)) % 0.48/0.89 (define @t241 () (@list @t203 @t239)) % 0.48/0.89 (define @t242 () (forall @t241 (_ @t238 @t240))) % 0.48/0.89 (define @t243 () (@var "Prod" tptp.produc1559976732_pi_pi)) % 0.48/0.89 (define @t244 () (@var "P" (-> tptp.produc1559976732_pi_pi Bool))) % 0.48/0.89 (define @t245 () (@var "B3" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t246 () (_ (_ tptp.produc1189045204_pi_pi @t203) @t245)) % 0.48/0.89 (define @t247 () (@list @t203 @t245)) % 0.48/0.89 (define @t248 () (forall @t247 (_ @t244 @t246))) % 0.48/0.89 (define @t249 () (@list @t75)) % 0.48/0.89 (define @t250 () (@var "Y" tptp.produc1462499409ion_pi)) % 0.48/0.89 (define @t251 () (@var "Y" tptp.produc53907987_pi_pi)) % 0.48/0.89 (define @t252 () (@list @t251)) % 0.48/0.89 (define @t253 () (@var "Y" tptp.produc1961110975reeRes)) % 0.48/0.89 (define @t254 () (@var "Y" tptp.produc1443308494i_name)) % 0.48/0.89 (define @t255 () (@var "Y" tptp.produc1559976732_pi_pi)) % 0.48/0.89 (define @t256 () (not @t119)) % 0.48/0.89 (define @t257 () (@var "P3" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t258 () (@var "P3" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t259 () (@var "P3" tptp.produc1834551554reeRes)) % 0.48/0.89 (define @t260 () (@var "P3" tptp.produc405342261i_name)) % 0.48/0.89 (define @t261 () (@var "P3" tptp.produc629157763_pi_pi)) % 0.48/0.89 (define @t262 () (@var "P3" tptp.produc1462499409ion_pi)) % 0.48/0.89 (define @t263 () (@var "P3" tptp.produc53907987_pi_pi)) % 0.48/0.89 (define @t264 () (@var "P3" tptp.produc1961110975reeRes)) % 0.48/0.89 (define @t265 () (@var "P3" tptp.produc1443308494i_name)) % 0.48/0.89 (define @t266 () (@var "P3" tptp.produc1559976732_pi_pi)) % 0.48/0.89 (define @t267 () (@var "Y3" tptp.produc1462499409ion_pi)) % 0.48/0.89 (define @t268 () (@var "X3" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t269 () (@var "P3" tptp.produc1217648014ion_pi)) % 0.48/0.89 (define @t270 () (@var "Y3" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t271 () (@var "X3" tptp.name)) % 0.48/0.89 (define @t272 () (_ (_ tptp.produc235456326_pi_pi @t271) @t270)) % 0.48/0.89 (define @t273 () (@list @t271 @t270)) % 0.48/0.89 (define @t274 () (@var "Y3" tptp.pi)) % 0.48/0.89 (define @t275 () (@var "X3" tptp.pi)) % 0.48/0.89 (define @t276 () (_ tptp.product_Pair_pi_pi @t275)) % 0.48/0.89 (define @t277 () (_ @t276 @t274)) % 0.48/0.89 (define @t278 () (@list @t275 @t274)) % 0.48/0.89 (define @t279 () (@list @t257)) % 0.48/0.89 (define @t280 () (@var "Y3" tptp.late_freeRes)) % 0.48/0.89 (define @t281 () (_ (_ tptp.produc1505598906reeRes @t268) @t280)) % 0.48/0.89 (define @t282 () (@list @t268 @t280)) % 0.48/0.89 (define @t283 () (@var "Y3" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t284 () (_ (_ tptp.produc1275980869_pi_pi @t268) @t283)) % 0.48/0.89 (define @t285 () (@list @t268 @t283)) % 0.48/0.89 (define @t286 () (@var "Y3" tptp.name)) % 0.48/0.89 (define @t287 () (_ (_ tptp.produc540578151i_name @t268) @t286)) % 0.48/0.89 (define @t288 () (@list @t268 @t286)) % 0.48/0.89 (define @t289 () (_ (_ tptp.produc1820286517_pi_pi @t268) @t274)) % 0.48/0.89 (define @t290 () (@list @t268 @t274)) % 0.48/0.89 (define @t291 () (@var "Y3" (-> tptp.name tptp.noption_pi))) % 0.48/0.89 (define @t292 () (_ tptp.produc1342893193ion_pi @t268)) % 0.48/0.89 (define @t293 () (_ @t292 @t291)) % 0.48/0.89 (define @t294 () (@list @t268 @t291)) % 0.48/0.89 (define @t295 () (@list @t262)) % 0.48/0.89 (define @t296 () (@var "C" tptp.name)) % 0.48/0.89 (define @t297 () (@list @t296)) % 0.48/0.89 (define @t298 () (@var "X" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t299 () (and @t90 @t92)) % 0.48/0.89 (define @t300 () (@list @t36 @t34 @t89 @t91)) % 0.48/0.89 (define @t301 () (@var "X" tptp.produc53907987_pi_pi)) % 0.48/0.89 (define @t302 () (_ @t225 @t301)) % 0.48/0.89 (define @t303 () (@var "D" tptp.pi)) % 0.48/0.89 (define @t304 () (@var "C" tptp.pi)) % 0.48/0.89 (define @t305 () (_ tptp.produc235456326_pi_pi @t209)) % 0.48/0.89 (define @t306 () (_ @t227 (_ @t305 (_ (_ tptp.product_Pair_pi_pi @t304) @t303)))) % 0.48/0.89 (define @t307 () (@list @t203 @t209 @t304 @t303)) % 0.48/0.89 (define @t308 () (@list @t225 @t301)) % 0.48/0.89 (define @t309 () (_ @t196 (_ (_ tptp.product_Pair_pi_pi @t187) @t304))) % 0.48/0.89 (define @t310 () (@list @t195 @t187 @t304)) % 0.48/0.89 (define @t311 () (@var "C" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t312 () (_ @t227 (_ @t305 @t311))) % 0.48/0.89 (define @t313 () (@list @t203 @t209 @t311)) % 0.48/0.89 (define @t314 () (_ (_ tptp.res @t7) @t46)) % 0.48/0.89 (define @t315 () (@var "Q" tptp.pi)) % 0.48/0.89 (define @t316 () (_ tptp.sum @t46)) % 0.48/0.89 (define @t317 () (_ @t316 @t315)) % 0.48/0.89 (define @t318 () (_ (_ tptp.late_transitions @t317) @t183)) % 0.48/0.89 (define @t319 () (_ tptp.late_transitions @t315)) % 0.48/0.89 (define @t320 () (_ @t319 @t183)) % 0.48/0.89 (define @t321 () (_ tptp.ord_le630093991_pi_pi tptp.id_pi)) % 0.48/0.89 (define @t322 () (@var "Q2" tptp.pi)) % 0.48/0.89 (define @t323 () (_ tptp.par @t46)) % 0.48/0.89 (define @t324 () (_ @t323 @t322)) % 0.48/0.89 (define @t325 () (_ @t323 @t315)) % 0.48/0.89 (define @t326 () (_ tptp.late_transitions @t325)) % 0.48/0.89 (define @t327 () (_ @t326 (_ @t45 @t324))) % 0.48/0.89 (define @t328 () (_ @t51 @t315)) % 0.48/0.89 (define @t329 () (_ @t319 (_ @t45 @t322))) % 0.48/0.89 (define @t330 () (@list @t315 @t43 @t18 @t322 @t46)) % 0.48/0.89 (define @t331 () (_ tptp.par @t40)) % 0.48/0.89 (define @t332 () (_ @t331 @t315)) % 0.48/0.89 (define @t333 () (_ @t326 (_ @t45 @t332))) % 0.48/0.89 (define @t334 () (@list @t46 @t43 @t18 @t40 @t315)) % 0.48/0.89 (define @t335 () (@var "A" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t336 () (_ tptp.collec1051790738_pi_pi @t186)) % 0.48/0.89 (define @t337 () (@var "A4" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t338 () (@var "X4" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t339 () (_ tptp.member558706512_pi_pi @t338)) % 0.48/0.89 (define @t340 () (@list @t338)) % 0.48/0.89 (define @t341 () (@list @t337)) % 0.48/0.89 (define @t342 () (@var "A3" tptp.late_subject)) % 0.48/0.89 (define @t343 () (_ (_ tptp.fresh_717452603ubject @t271) @t342)) % 0.48/0.89 (define @t344 () (not @t343)) % 0.48/0.89 (define @t345 () (@var "Q3" tptp.pi)) % 0.48/0.89 (define @t346 () (_ tptp.fresh_name_pi @t271)) % 0.48/0.89 (define @t347 () (@var "P4" tptp.pi)) % 0.48/0.89 (define @t348 () (_ @t346 @t347)) % 0.48/0.89 (define @t349 () (=> @t348 (=> (_ @t346 @t345) @t344))) % 0.48/0.89 (define @t350 () (@var "Q4" tptp.pi)) % 0.48/0.89 (define @t351 () (_ tptp.late_BoundR @t342)) % 0.48/0.89 (define @t352 () (_ @t351 @t271)) % 0.48/0.89 (define @t353 () (_ @t352 @t350)) % 0.48/0.89 (define @t354 () (_ tptp.par @t347)) % 0.48/0.89 (define @t355 () (@var "B" tptp.late_subject)) % 0.48/0.89 (define @t356 () (_ (_ (_ tptp.late_BoundR @t355) @t12) @t40)) % 0.48/0.89 (define @t357 () (= @t325 (_ @t354 @t345))) % 0.48/0.89 (define @t358 () (@var "P5" tptp.pi)) % 0.48/0.89 (define @t359 () (_ tptp.late_transitions @t347)) % 0.48/0.89 (define @t360 () (_ @t359 (_ @t352 @t358))) % 0.48/0.89 (define @t361 () (_ tptp.par @t358)) % 0.48/0.89 (define @t362 () (_ tptp.fresh_717452603ubject @t7)) % 0.48/0.89 (define @t363 () (_ tptp.input @t7)) % 0.48/0.89 (define @t364 () (_ (_ @t363 @t18) @t46)) % 0.48/0.89 (define @t365 () (_ tptp.late_transitions @t364)) % 0.48/0.89 (define @t366 () (_ tptp.tau @t46)) % 0.48/0.89 (define @t367 () (_ tptp.res @t18)) % 0.48/0.89 (define @t368 () (_ tptp.late_transitions (_ @t367 @t366))) % 0.48/0.89 (define @t369 () (@var "Residual" tptp.late_residual)) % 0.48/0.89 (define @t370 () (@var "Z" tptp.late_freeRes)) % 0.48/0.89 (define @t371 () (@var "P" (-> tptp.late_freeRes tptp.late_residual Bool))) % 0.48/0.89 (define @t372 () (@var "Pi3" tptp.pi)) % 0.48/0.89 (define @t373 () (@var "FreeRes" tptp.late_freeRes)) % 0.48/0.89 (define @t374 () (_ (_ tptp.late_FreeR @t373) @t372)) % 0.48/0.89 (define @t375 () (@var "Z2" tptp.late_freeRes)) % 0.48/0.89 (define @t376 () (_ @t371 @t375)) % 0.48/0.89 (define @t377 () (@var "Name2" tptp.name)) % 0.48/0.89 (define @t378 () (@var "Subject" tptp.late_subject)) % 0.48/0.89 (define @t379 () (_ (_ (_ tptp.late_BoundR @t378) @t377) @t372)) % 0.48/0.89 (define @t380 () (_ (_ tptp.fresh_717452603ubject @t377) @t378)) % 0.48/0.89 (define @t381 () (@var "Z" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t382 () (@var "P" (-> tptp.produc1141751126_pi_pi tptp.late_residual Bool))) % 0.48/0.89 (define @t383 () (@var "Z2" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t384 () (_ @t382 @t383)) % 0.48/0.89 (define @t385 () (@var "Z" tptp.name)) % 0.48/0.89 (define @t386 () (@var "P" (-> tptp.name tptp.late_residual Bool))) % 0.48/0.89 (define @t387 () (@var "Z2" tptp.name)) % 0.48/0.89 (define @t388 () (_ @t386 @t387)) % 0.48/0.89 (define @t389 () (@var "Z" tptp.pi)) % 0.48/0.89 (define @t390 () (@var "P" (-> tptp.pi tptp.late_residual Bool))) % 0.48/0.89 (define @t391 () (@var "Z2" tptp.pi)) % 0.48/0.89 (define @t392 () (_ @t390 @t391)) % 0.48/0.89 (define @t393 () (_ (_ tptp.par @t36) @t34)) % 0.48/0.89 (define @t394 () (_ tptp.tau @t34)) % 0.48/0.89 (define @t395 () (_ (_ tptp.late_FreeR @t99) @t34)) % 0.48/0.89 (define @t396 () (_ tptp.fresh_81631222sidual @t7)) % 0.48/0.89 (define @t397 () (@var "Name22" tptp.name)) % 0.48/0.89 (define @t398 () (@var "Name1" tptp.name)) % 0.48/0.89 (define @t399 () (_ (_ (_ tptp.input @t398) @t397) @t176)) % 0.48/0.89 (define @t400 () (@var "Pi4" tptp.pi)) % 0.48/0.89 (define @t401 () (_ tptp.tau @t400)) % 0.48/0.89 (define @t402 () (@list @t400 @t398 @t397 @t176)) % 0.48/0.89 (define @t403 () (@var "Pi22" tptp.pi)) % 0.48/0.89 (define @t404 () (@var "Pi12" tptp.pi)) % 0.48/0.89 (define @t405 () (_ (_ tptp.par @t404) @t403)) % 0.48/0.89 (define @t406 () (@list @t400 @t404 @t403)) % 0.48/0.89 (define @t407 () (@var "Name23" tptp.name)) % 0.48/0.89 (define @t408 () (@var "Name12" tptp.name)) % 0.48/0.89 (define @t409 () (_ (_ (_ tptp.input @t408) @t407) @t400)) % 0.48/0.89 (define @t410 () (@list @t408 @t407 @t400 @t404 @t403)) % 0.48/0.89 (define @t411 () (@var "Alpha" tptp.late_freeRes)) % 0.48/0.89 (define @t412 () (_ tptp.late_FreeR @t411)) % 0.48/0.89 (define @t413 () (_ @t319 (_ @t412 @t322))) % 0.48/0.89 (define @t414 () (_ @t412 @t40)) % 0.48/0.89 (define @t415 () (_ @t56 @t414)) % 0.48/0.89 (define @t416 () (_ tptp.late_transitions (_ @t367 (_ (_ @t363 @t12) @t46)))) % 0.48/0.89 (define @t417 () (@var "FreeRes2" tptp.late_freeRes)) % 0.48/0.89 (define @t418 () (@var "Name3" tptp.name)) % 0.48/0.89 (define @t419 () (@var "Subject2" tptp.late_subject)) % 0.48/0.89 (define @t420 () (@var "P" (-> tptp.late_residual Bool))) % 0.48/0.89 (define @t421 () (@list @t408 @t407 @t400 @t177 @t176)) % 0.48/0.89 (define @t422 () (_ (_ tptp.sum @t404) @t403)) % 0.48/0.89 (define @t423 () (@var "XP" tptp.pi)) % 0.48/0.89 (define @t424 () (@var "F" (-> tptp.pi Bool))) % 0.48/0.89 (define @t425 () (_ tptp.fresh_1641682979reeRes @t18)) % 0.48/0.89 (define @t426 () (_ @t56 (_ @t412 @t358))) % 0.48/0.89 (define @t427 () (@list @t358)) % 0.48/0.89 (define @t428 () (_ @t367 @t46)) % 0.48/0.89 (define @t429 () (_ tptp.late_transitions @t428)) % 0.48/0.89 (define @t430 () (@var "Alpha2" tptp.late_freeRes)) % 0.48/0.89 (define @t431 () (_ tptp.fresh_1641682979reeRes @t286)) % 0.48/0.89 (define @t432 () (_ tptp.late_FreeR @t430)) % 0.48/0.89 (define @t433 () (=> (_ @t359 (_ @t432 @t358)) (not (_ @t431 @t430)))) % 0.48/0.89 (define @t434 () (_ tptp.res @t286)) % 0.48/0.89 (define @t435 () (_ @t434 @t358)) % 0.48/0.89 (define @t436 () (_ @t432 @t435)) % 0.48/0.89 (define @t437 () (_ @t434 @t347)) % 0.48/0.89 (define @t438 () (= @t428 @t437)) % 0.48/0.89 (define @t439 () (@list @t347 @t430 @t358 @t286)) % 0.48/0.89 (define @t440 () (_ (_ tptp.fresh_1641682979reeRes @t12) @t411)) % 0.48/0.89 (define @t441 () (@list @t46 @t411 @t40 @t12)) % 0.48/0.89 (define @t442 () (_ tptp.late_transitions @t366)) % 0.48/0.89 (define @t443 () (@var "PQ" tptp.pi)) % 0.48/0.89 (define @t444 () (@var "Prop" (-> tptp.pi Bool))) % 0.48/0.89 (define @t445 () (_ @t56 (_ @t45 @t358))) % 0.48/0.89 (define @t446 () (= @t121 @t118)) % 0.48/0.89 (define @t447 () (_ (_ tptp.member558706512_pi_pi @t124) tptp.id_pi)) % 0.48/0.89 (define @t448 () (@list @t121 @t118)) % 0.48/0.89 (define @t449 () (= @t138 @t150)) % 0.48/0.89 (define @t450 () (_ (_ tptp.member1632198138ion_pi @t153) tptp.id_name_noption_pi)) % 0.48/0.89 (define @t451 () (@list @t138 @t150)) % 0.48/0.89 (define @t452 () (@var "B4" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t453 () (_ tptp.ord_le630093991_pi_pi @t337)) % 0.48/0.89 (define @t454 () (_ @t453 @t452)) % 0.48/0.89 (define @t455 () (@var "X3" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t456 () (_ tptp.member558706512_pi_pi @t455)) % 0.48/0.89 (define @t457 () (@list @t455)) % 0.48/0.89 (define @t458 () (@list @t337 @t452)) % 0.48/0.89 (define @t459 () (= @t337 @t452)) % 0.48/0.89 (define @t460 () (_ tptp.ord_le630093991_pi_pi @t452)) % 0.48/0.89 (define @t461 () (_ @t460 @t337)) % 0.48/0.89 (define @t462 () (@var "X" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t463 () (_ tptp.ord_le630093991_pi_pi @t462)) % 0.48/0.89 (define @t464 () (@var "S" tptp.set_Pr1654044726_pi_pi)) % 0.48/0.89 (define @t465 () (@var "R" tptp.set_Pr1654044726_pi_pi)) % 0.48/0.89 (define @t466 () (_ tptp.member540268543_pi_pi @t272)) % 0.48/0.89 (define @t467 () (@var "S" tptp.set_Pr305743074reeRes)) % 0.48/0.89 (define @t468 () (@var "R" tptp.set_Pr305743074reeRes)) % 0.48/0.89 (define @t469 () (_ tptp.member2081207979reeRes @t281)) % 0.48/0.89 (define @t470 () (@var "S" tptp.set_Pr100209225_pi_pi)) % 0.48/0.89 (define @t471 () (@var "R" tptp.set_Pr100209225_pi_pi)) % 0.48/0.89 (define @t472 () (_ tptp.member695660714_pi_pi @t284)) % 0.48/0.89 (define @t473 () (@var "S" tptp.set_Pr1294453099i_name)) % 0.48/0.89 (define @t474 () (@var "R" tptp.set_Pr1294453099i_name)) % 0.48/0.89 (define @t475 () (_ tptp.member1353687244i_name @t287)) % 0.48/0.89 (define @t476 () (@var "S" tptp.set_Pr1694908217_pi_pi)) % 0.48/0.89 (define @t477 () (@var "R" tptp.set_Pr1694908217_pi_pi)) % 0.48/0.89 (define @t478 () (_ tptp.member772629402_pi_pi @t289)) % 0.48/0.89 (define @t479 () (@var "S" tptp.set_Pr1569510577ion_pi)) % 0.48/0.89 (define @t480 () (@var "R" tptp.set_Pr1569510577ion_pi)) % 0.48/0.89 (define @t481 () (_ tptp.member1632198138ion_pi @t293)) % 0.48/0.89 (define @t482 () (@var "S" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t483 () (@var "R" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t484 () (_ tptp.member558706512_pi_pi @t277)) % 0.48/0.89 (define @t485 () (@var "B" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t486 () (@var "A" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t487 () (= @t486 @t485)) % 0.48/0.89 (define @t488 () (_ tptp.ord_le630093991_pi_pi @t486)) % 0.48/0.89 (define @t489 () (_ @t488 @t485)) % 0.48/0.89 (define @t490 () (_ tptp.ord_le630093991_pi_pi @t485)) % 0.48/0.89 (define @t491 () (_ @t490 @t486)) % 0.48/0.89 (define @t492 () (@var "B5" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t493 () (@var "A5" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t494 () (_ (_ tptp.ord_le630093991_pi_pi @t493) @t492)) % 0.48/0.89 (define @t495 () (_ (_ tptp.ord_le630093991_pi_pi @t492) @t493)) % 0.48/0.89 (define @t496 () (@list @t493 @t492)) % 0.48/0.89 (define @t497 () (@var "Z3" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t498 () (@var "Y4" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t499 () (lambda (@list @t498 @t497) (= @t498 @t497))) % 0.48/0.89 (define @t500 () (@var "C2" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t501 () (_ tptp.ord_le630093991_pi_pi @t500)) % 0.48/0.89 (define @t502 () (@var "Z" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t503 () (@var "Y" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t504 () (_ tptp.ord_le630093991_pi_pi @t503)) % 0.48/0.89 (define @t505 () (_ @t463 @t503)) % 0.48/0.89 (define @t506 () (_ @t488 @t500)) % 0.48/0.89 (define @t507 () (@list @t486 @t485 @t500)) % 0.48/0.89 (define @t508 () (_ @t490 @t500)) % 0.48/0.89 (define @t509 () (=> @t508 @t506)) % 0.48/0.89 (define @t510 () (= @t462 @t503)) % 0.48/0.89 (define @t511 () (_ @t504 @t462)) % 0.48/0.89 (define @t512 () (@list @t462 @t503)) % 0.48/0.89 (define @t513 () (@var "X4" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t514 () (@var "Y5" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t515 () (@var "F2" (-> tptp.set_Pr1834926343_pi_pi tptp.set_Pr1834926343_pi_pi))) % 0.48/0.89 (define @t516 () (@var "Y3" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t517 () (@var "X3" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t518 () (forall (@list @t517 @t516) (=> (_ (_ tptp.ord_le630093991_pi_pi @t517) @t516) (_ (_ tptp.ord_le630093991_pi_pi (_ @t515 @t517)) (_ @t515 @t516))))) % 0.48/0.89 (define @t519 () (=> @t518 (_ (_ tptp.ord_le630093991_pi_pi (_ @t515 @t486)) @t500))) % 0.48/0.89 (define @t520 () (_ @t515 @t485)) % 0.48/0.89 (define @t521 () (@list @t486 @t485 @t515 @t500)) % 0.48/0.89 (define @t522 () (=> @t508 (=> @t518 (_ @t488 (_ @t515 @t500))))) % 0.48/0.89 (define @t523 () (@list @t486 @t515 @t485 @t500)) % 0.48/0.89 (define @t524 () (@var "Q" (-> tptp.product_prod_pi_pi Bool))) % 0.48/0.89 (define @t525 () (_ (_ tptp.ord_le630093991_pi_pi @t336) (_ tptp.collec1051790738_pi_pi @t524))) % 0.48/0.89 (define @t526 () (@list @t186 @t524)) % 0.48/0.89 (define @t527 () (@var "A6" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t528 () (@var "B6" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t529 () (@list @t527 @t528)) % 0.48/0.89 (define @t530 () (@var "C3" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t531 () (@var "C2" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t532 () (_ tptp.member558706512_pi_pi @t531)) % 0.48/0.89 (define @t533 () (@var "X" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t534 () (_ tptp.member558706512_pi_pi @t533)) % 0.48/0.89 (define @t535 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t143))) % 0.48/0.89 (define @t536 () (_ (_ tptp.late_OutputR @t7) @t143)) % 0.48/0.89 (define @t537 () (_ tptp.late_FreeR @t536)) % 0.48/0.89 (define @t538 () (_ @t537 @t40)) % 0.48/0.89 (define @t539 () (@var "Rel" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t540 () (_ tptp.strong743114133lation @t46)) % 0.48/0.89 (define @t541 () (_ @t540 @t539)) % 0.48/0.89 (define @t542 () (_ @t541 @t315)) % 0.48/0.89 (define @t543 () (@var "P6" tptp.pi)) % 0.48/0.89 (define @t544 () (_ tptp.product_Pair_pi_pi @t543)) % 0.48/0.89 (define @t545 () (_ (_ tptp.member558706512_pi_pi (_ @t544 @t350)) @t539)) % 0.48/0.89 (define @t546 () (_ @t56 (_ @t432 @t543))) % 0.48/0.89 (define @t547 () (@list @t543)) % 0.48/0.89 (define @t548 () (_ @t319 (_ @t432 @t350))) % 0.48/0.89 (define @t549 () (=> (forall (@list @t430 @t350) (=> @t548 (exists @t547 (and @t546 @t545)))) @t542)) % 0.48/0.89 (define @t550 () (_ tptp.strong2129052853vative @t543)) % 0.48/0.89 (define @t551 () (_ (_ @t550 @t350) @t342)) % 0.48/0.89 (define @t552 () (exists @t547 (and (_ @t56 (_ @t352 @t543)) (_ (_ @t551 @t271) @t539)))) % 0.48/0.89 (define @t553 () (@var "C3" tptp.late_freeRes)) % 0.48/0.89 (define @t554 () (_ @t346 @t315)) % 0.48/0.89 (define @t555 () (_ @t346 @t46)) % 0.48/0.89 (define @t556 () (_ @t319 @t353)) % 0.48/0.89 (define @t557 () (@list @t342 @t271 @t350)) % 0.48/0.89 (define @t558 () (_ tptp.eqvt_pi @t539)) % 0.48/0.89 (define @t559 () (@var "C3" tptp.produc1141751126_pi_pi)) % 0.48/0.89 (define @t560 () (@var "C3" tptp.name)) % 0.48/0.89 (define @t561 () (@var "C3" tptp.pi)) % 0.48/0.89 (define @t562 () (_ (_ tptp.abs_fun_name_pi @t96) @t36)) % 0.48/0.89 (define @t563 () (_ @t72 @t562)) % 0.48/0.89 (define @t564 () (@var "X32" tptp.late_subject)) % 0.48/0.89 (define @t565 () (_ (_ (_ tptp.late_BoundR @t564) @t96) @t36)) % 0.48/0.89 (define @t566 () (=> @t360 (=> (_ (_ tptp.fresh_717452603ubject @t286) @t342) (=> (not (= @t286 @t271)) (=> @t348 @t344))))) % 0.48/0.89 (define @t567 () (_ @t352 @t435)) % 0.48/0.89 (define @t568 () (@list @t347 @t342 @t271 @t358 @t286)) % 0.48/0.89 (define @t569 () (_ tptp.late_OutputR @t195)) % 0.48/0.89 (define @t570 () (_ tptp.late_FreeR (_ @t569 @t209))) % 0.48/0.89 (define @t571 () (=> (_ @t359 (_ @t570 @t358)) (= @t195 @t209))) % 0.48/0.89 (define @t572 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t195))) % 0.48/0.89 (define @t573 () (_ (_ @t572 @t209) @t358)) % 0.48/0.89 (define @t574 () (_ (_ tptp.res @t209) @t347)) % 0.48/0.89 (define @t575 () (@list @t347 @t195 @t209)) % 0.48/0.89 (define @t576 () (_ (_ tptp.late_OutputR @t105) @t96)) % 0.48/0.89 (define @t577 () (_ tptp.late_BoundOutputS @t96)) % 0.48/0.89 (define @t578 () (_ @t13 @t96)) % 0.48/0.89 (define @t579 () (@list @t7 @t96)) % 0.48/0.89 (define @t580 () (_ @t13 @t105)) % 0.48/0.89 (define @t581 () (_ (_ tptp.res @t96) @t36)) % 0.48/0.89 (define @t582 () (@var "X32" tptp.name)) % 0.48/0.89 (define @t583 () (_ @t13 @t582)) % 0.48/0.89 (define @t584 () (_ (_ (_ tptp.input @t582) @t96) @t36)) % 0.48/0.89 (define @t585 () (_ tptp.abs_fun_name_pi @t7)) % 0.48/0.89 (define @t586 () (_ @t585 @t20)) % 0.48/0.89 (define @t587 () (_ tptp.strong2129052853vative @t46)) % 0.48/0.89 (define @t588 () (_ (_ (_ @t587 @t315) @t43) @t18)) % 0.48/0.89 (define @t589 () (= @t562 (_ (_ tptp.abs_fun_name_pi @t95) @t89))) % 0.48/0.89 (define @t590 () (@var "Y32" tptp.late_subject)) % 0.48/0.89 (define @t591 () (_ tptp.fresh_1641682979reeRes @t143)) % 0.48/0.89 (define @t592 () (= @t143 @t7)) % 0.48/0.89 (define @t593 () (_ tptp.fresh_name_pi @t143)) % 0.48/0.89 (define @t594 () (@var "Y32" tptp.name)) % 0.48/0.89 (define @t595 () (= @t582 @t594)) % 0.48/0.89 (define @t596 () (_ @t321 @t539)) % 0.48/0.89 (define @t597 () (@list @t539 @t46)) % 0.48/0.89 (define @t598 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t7))) % 0.48/0.89 (define @t599 () (_ tptp.res @t143)) % 0.48/0.89 (define @t600 () (not (= @t7 @t143))) % 0.48/0.89 (define @t601 () (_ @t56 @t538)) % 0.48/0.89 (define @t602 () (@list @t46 @t7 @t143 @t40)) % 0.48/0.89 (define @t603 () (_ @t367 @t350)) % 0.48/0.89 (define @t604 () (=> (forall (@list @t350 @t430) (=> @t548 (=> (_ @t425 @t430) (exists @t547 (and @t546 (_ (_ tptp.member558706512_pi_pi (_ @t544 @t603)) @t539)))))) (_ @t541 (_ @t367 @t315)))) % 0.48/0.89 (define @t605 () (_ @t351 @t286)) % 0.48/0.89 (define @t606 () (_ @t56 (_ @t605 @t543))) % 0.48/0.89 (define @t607 () (exists @t547 (and @t606 (_ (_ (_ (_ @t550 @t603) @t342) @t286) @t539)))) % 0.48/0.89 (define @t608 () (not (= @t18 @t286))) % 0.48/0.89 (define @t609 () (_ @t49 @t342)) % 0.48/0.89 (define @t610 () (_ @t319 (_ @t605 @t350))) % 0.48/0.89 (define @t611 () (@list @t350 @t342 @t286)) % 0.48/0.89 (define @t612 () (forall (@list @t350 @t195) (=> (_ @t319 (_ (_ tptp.late_FreeR (_ @t569 @t18)) @t350)) (=> (not (= @t195 @t18)) (exists @t547 (and (_ @t56 (_ (_ @t572 @t18) @t543)) @t545)))))) % 0.48/0.89 (define @t613 () (_ tptp.fresh_name_pi @t286)) % 0.48/0.89 (define @t614 () (@var "Y6" tptp.name)) % 0.48/0.89 (define @t615 () (_ (_ @t44 @t614) @t40)) % 0.48/0.89 (define @t616 () (@var "X5" tptp.name)) % 0.48/0.89 (define @t617 () (_ (_ tptp.res @t616) @t46)) % 0.48/0.89 (define @t618 () (_ @t316 @t46)) % 0.48/0.89 (define @t619 () (@var "R2" tptp.pi)) % 0.48/0.89 (define @t620 () (_ (_ tptp.sum @t317) @t619)) % 0.48/0.89 (define @t621 () (_ tptp.sum @t315)) % 0.48/0.89 (define @t622 () (_ @t316 (_ @t621 @t619))) % 0.48/0.89 (define @t623 () (@list @t539 @t46 @t315 @t619)) % 0.48/0.89 (define @t624 () (_ tptp.late_BoundOutputS @t105)) % 0.48/0.89 (define @t625 () (@var "Y12" tptp.name)) % 0.48/0.89 (define @t626 () (@var "X12" tptp.name)) % 0.48/0.89 (define @t627 () (@var "Y11" tptp.name)) % 0.48/0.89 (define @t628 () (@var "X11" tptp.name)) % 0.48/0.89 (define @t629 () (_ (_ tptp.late_OutputR @t628) @t626)) % 0.48/0.89 (define @t630 () (_ @t316 tptp.piNil)) % 0.48/0.89 (define @t631 () (@list @t7)) % 0.48/0.89 (define @t632 () (@list @t404 @t403)) % 0.48/0.89 (define @t633 () (@list @t398 @t397 @t176)) % 0.48/0.89 (define @t634 () (_ tptp.tau @t176)) % 0.48/0.89 (define @t635 () (_ (_ tptp.strong743114133lation tptp.piNil) @t539)) % 0.48/0.89 (define @t636 () (= @t7 @t195)) % 0.48/0.89 (define @t637 () (@list @t7 @t143 @t46 @t183)) % 0.48/0.89 (define @t638 () (_ tptp.late_InputS @t96)) % 0.48/0.89 (define @t639 () (@var "X22" tptp.name)) % 0.48/0.89 (define @t640 () (@var "Y" tptp.late_subject)) % 0.48/0.89 (define @t641 () (@var "X13" tptp.name)) % 0.48/0.89 (define @t642 () (@var "P" (-> tptp.late_subject Bool))) % 0.48/0.89 (define @t643 () (@list @t377)) % 0.48/0.89 (define @t644 () (_ (_ tptp.late_BoundR (_ tptp.late_InputS @t7)) @t18)) % 0.48/0.89 (define @t645 () (_ @t365 (_ @t644 @t46))) % 0.48/0.89 (define @t646 () (not (= @t18 @t7))) % 0.48/0.89 (define @t647 () (@var "C2" tptp.name)) % 0.48/0.89 (define @t648 () (_ tptp.output @t7)) % 0.48/0.89 (define @t649 () (_ (_ @t648 @t143) @t46)) % 0.48/0.89 (define @t650 () (_ tptp.late_transitions (_ @t367 @t649))) % 0.48/0.89 (define @t651 () (_ (_ tptp.subs @t40) @t18)) % 0.48/0.89 (define @t652 () (_ tptp.late_FreeR tptp.late_TauR)) % 0.48/0.89 (define @t653 () (_ @t326 (_ @t652 (_ @t41 (_ (_ tptp.par (_ @t651 @t12)) @t322))))) % 0.48/0.89 (define @t654 () (_ @t598 @t12)) % 0.48/0.89 (define @t655 () (_ @t319 (_ @t654 @t322))) % 0.48/0.89 (define @t656 () (_ @t56 (_ @t644 @t40))) % 0.48/0.89 (define @t657 () (@list @t46 @t7 @t18 @t40 @t315 @t12 @t322)) % 0.48/0.89 (define @t658 () (_ tptp.subs @t46)) % 0.48/0.89 (define @t659 () (_ @t658 @t7)) % 0.48/0.89 (define @t660 () (@var "D2" tptp.name)) % 0.48/0.89 (define @t661 () (_ (_ @t658 @t647) @t660)) % 0.48/0.89 (define @t662 () (_ (_ (_ tptp.subs @t315) @t647) @t660)) % 0.48/0.89 (define @t663 () (@list @t46 @t315 @t647 @t660)) % 0.48/0.89 (define @t664 () (_ @t659 @t143)) % 0.48/0.89 (define @t665 () (_ @t593 @t46)) % 0.48/0.89 (define @t666 () (and @t583 @t580 @t35)) % 0.48/0.89 (define @t667 () (_ (_ (_ tptp.output @t582) @t105) @t34)) % 0.48/0.89 (define @t668 () (@list @t7 @t582 @t105 @t34)) % 0.48/0.89 (define @t669 () (_ @t652 @t40)) % 0.48/0.89 (define @t670 () (_ tptp.late_transitions @t649)) % 0.48/0.89 (define @t671 () (_ (_ (_ tptp.output @t408) @t407) @t400)) % 0.48/0.89 (define @t672 () (and @t595 @t106 @t92)) % 0.48/0.89 (define @t673 () (@list @t582 @t105 @t34 @t594 @t104 @t91)) % 0.48/0.89 (define @t674 () (@var "FreeRes3" tptp.late_freeRes)) % 0.48/0.89 (define @t675 () (@var "P" (-> tptp.late_freeRes Bool))) % 0.48/0.89 (define @t676 () (@var "Name24" tptp.name)) % 0.48/0.89 (define @t677 () (@var "Name13" tptp.name)) % 0.48/0.89 (define @t678 () (@list @t408 @t407 @t400 @t398 @t397 @t176)) % 0.48/0.89 (define @t679 () (@list @t7 @t143 @t46)) % 0.48/0.89 (define @t680 () (not (= @t7 @t647))) % 0.48/0.89 (define @t681 () (_ @t16 @t46)) % 0.48/0.89 (define @t682 () (@var "X122" tptp.name)) % 0.48/0.89 (define @t683 () (@var "X112" tptp.name)) % 0.48/0.89 (define @t684 () (_ @t599 @t664)) % 0.48/0.89 (define @t685 () (@list @t143 @t46 @t7)) % 0.48/0.89 (define @t686 () (@var "C2" tptp.late_subject)) % 0.48/0.89 (define @t687 () (@list @t539 @t7 @t143 @t46)) % 0.48/0.89 (define @t688 () (_ (_ tptp.subs @t322) @t18)) % 0.48/0.89 (define @t689 () (_ @t326 (_ @t652 (_ @t331 (_ @t688 @t143))))) % 0.48/0.89 (define @t690 () (_ @t319 (_ @t644 @t322))) % 0.48/0.89 (define @t691 () (@list @t46 @t7 @t143 @t40 @t315 @t18 @t322)) % 0.48/0.89 (define @t692 () (_ @t326 (_ @t652 (_ (_ tptp.par (_ @t651 @t143)) @t322)))) % 0.48/0.89 (define @t693 () (_ @t319 (_ @t537 @t322))) % 0.48/0.89 (define @t694 () (@list @t46 @t7 @t18 @t40 @t315 @t143 @t322)) % 0.48/0.89 (define @t695 () (@var "Prop" (-> tptp.late_freeRes tptp.pi Bool))) % 0.48/0.89 (define @t696 () (_ (_ @t695 @t411) @t40)) % 0.48/0.89 (define @t697 () (= @t46 @t40)) % 0.48/0.89 (define @t698 () (_ @t670 @t414)) % 0.48/0.89 (define @t699 () (_ @t51 @t40)) % 0.48/0.89 (define @t700 () (not (= @t18 @t143))) % 0.48/0.89 (define @t701 () (_ @t51 @t322)) % 0.48/0.89 (define @t702 () (_ @t326 (_ @t652 (_ @t41 (_ @t331 (_ @t688 @t12)))))) % 0.48/0.89 (define @t703 () (not (= @t18 @t12))) % 0.48/0.89 (define @t704 () (not (= @t12 @t7))) % 0.48/0.89 (define @t705 () (_ @t59 @t315)) % 0.48/0.89 (define @t706 () (_ @t56 (_ @t654 @t40))) % 0.48/0.89 (define @t707 () (@list @t46 @t7 @t12 @t40 @t315 @t18 @t322)) % 0.48/0.89 (define @t708 () (_ (_ (_ tptp.mismatch @t7) @t143) @t46)) % 0.48/0.89 (define @t709 () (_ (_ (_ tptp.mismatch @t582) @t105) @t34)) % 0.48/0.89 (define @t710 () (_ (_ (_ tptp.mismatch @t398) @t397) @t176)) % 0.48/0.89 (define @t711 () (_ (_ (_ tptp.mismatch @t408) @t407) @t400)) % 0.48/0.89 (define @t712 () (= tptp.y tptp.x)) % 0.48/0.89 (define @t713 () (@var "T" tptp.product_prod_pi_pi)) % 0.48/0.89 (define @t714 () (_ tptp.member558706512_pi_pi @t713)) % 0.48/0.89 (define @t715 () (lambda @t529 (forall (@list @t713) (=> (_ @t714 @t527) (_ @t714 @t528))))) % 0.48/0.89 (define @t716 () (@var "Rel2" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.89 (define @t717 () (@var "Q6" tptp.pi)) % 0.48/0.89 (define @t718 () (@var "P8" tptp.pi)) % 0.48/0.89 (define @t719 () (@var "Alpha3" tptp.late_freeRes)) % 0.48/0.89 (define @t720 () (_ tptp.late_FreeR @t719)) % 0.48/0.89 (define @t721 () (@var "P7" tptp.pi)) % 0.48/0.89 (define @t722 () (_ tptp.late_transitions @t721)) % 0.48/0.89 (define @t723 () (@list @t718)) % 0.48/0.89 (define @t724 () (@var "Q5" tptp.pi)) % 0.48/0.89 (define @t725 () (_ tptp.late_transitions @t724)) % 0.48/0.89 (define @t726 () (@var "X4" tptp.name)) % 0.48/0.89 (define @t727 () (@var "A5" tptp.late_subject)) % 0.48/0.89 (define @t728 () (_ (_ tptp.late_BoundR @t727) @t726)) % 0.48/0.89 (define @t729 () (lambda (@list @t721 @t716 @t724) (and (forall (@list @t727 @t726 @t717) (=> (and (_ @t725 (_ @t728 @t717)) (_ (_ tptp.fresh_name_pi @t726) @t721)) (exists @t723 (and (_ @t722 (_ @t728 @t718)) (_ (_ (_ (_ (_ tptp.strong2129052853vative @t718) @t717) @t727) @t726) @t716))))) (forall (@list @t719 @t717) (=> (_ @t725 (_ @t720 @t717)) (exists @t723 (and (_ @t722 (_ @t720 @t718)) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t718) @t717)) @t716)))))))) % 0.48/0.89 (define @t730 () (@var "B5" tptp.name)) % 0.48/0.89 (define @t731 () (@var "A5" tptp.name)) % 0.48/0.89 (define @t732 () (lambda (@list @t731 @t730) (not (= @t731 @t730)))) % 0.48/0.89 (define @t733 () (_ tptp.produc235456326_pi_pi tptp.y)) % 0.48/0.89 (define @t734 () (_ @t733 @t1)) % 0.48/0.89 (define @t735 () (tptp.product_Pair_pi_pi tptp.p tptp.q)) % 0.48/0.89 (define @t736 () (tptp.produc235456326_pi_pi tptp.y @t735)) % 0.48/0.89 (define @t737 () (tptp.fresh_1376661020_pi_pi tptp.y @t736)) % 0.48/0.89 (define @t738 () (tptp.fresh_1627595501_pi_pi @t7 @t25)) % 0.48/0.89 (define @t739 () (not (= @t7 @t18))) % 0.48/0.89 (define @t740 () (and @t739 @t26)) % 0.48/0.89 (define @t741 () (tptp.produc235456326_pi_pi @t18 @t25)) % 0.48/0.89 (define @t742 () (tptp.fresh_1376661020_pi_pi @t7 @t741)) % 0.48/0.89 (define @t743 () (= @t30 @t740)) % 0.48/0.89 (define @t744 () (lambda (@list @t730) (not (= @t7 @t730)))) % 0.48/0.89 (define @t745 () (_ @t732 @t7)) % 0.48/0.89 (define @t746 () (and (_ @t745 @t18) @t26)) % 0.48/0.89 (define @t747 () (= @t30 @t746)) % 0.48/0.89 (define @t748 () (tptp.fresh_1627595501_pi_pi tptp.y @t735)) % 0.48/0.89 (define @t749 () (not (= tptp.y tptp.y))) % 0.48/0.89 (define @t750 () (and @t749 @t748)) % 0.48/0.89 (define @t751 () (= @t737 @t750)) % 0.48/0.89 (define @t752 () (forall @t32 (= @t742 (and @t739 @t738)))) % 0.48/0.89 (assume @p1 (_ tptp.eqvt_pi tptp.rel)) % 0.48/0.89 (assume @p2 (_ @t2 (_ (_ tptp.produc235456326_pi_pi tptp.x) @t1))) % 0.48/0.89 (assume @p3 (_ (_ tptp.fresh_717452603ubject tptp.y) tptp.a)) % 0.48/0.89 (assume @p4 (_ @t5 @t4)) % 0.48/0.89 (assume @p5 (_ @t5 (_ (_ tptp.sum (_ @t3 tptp.p)) (_ @t3 tptp.q)))) % 0.48/0.89 (assume @p6 (_ (_ tptp.late_transitions @t4) (_ (_ (_ tptp.late_BoundR tptp.a) tptp.y) tptp.pq))) % 0.48/0.89 (assume @p7 (forall (@list @t7 @t10 @t6) (= (_ (_ tptp.fresh_493808761reeRes @t7) (_ (_ tptp.produc1244821099reeRes @t10) @t6)) (and @t11 @t9)))) % 0.48/0.89 (assume @p8 (forall (@list @t7 @t10 @t12) (= (_ (_ tptp.fresh_2007541374s_name @t7) (_ (_ tptp.produc1701355766s_name @t10) @t12)) (and @t11 @t14)))) % 0.48/0.89 (assume @p9 (forall (@list @t7 @t10 @t15) (= (_ (_ tptp.fresh_1847501388Res_pi @t7) (_ (_ tptp.produc1177552196Res_pi @t10) @t15)) (and @t11 @t17)))) % 0.48/0.89 (assume @p10 (forall (@list @t7 @t18 @t6) (= (_ (_ tptp.fresh_1963366730reeRes @t7) (_ (_ tptp.produc1531804426reeRes @t18) @t6)) (and @t19 @t9)))) % 0.48/0.89 (assume @p11 (forall (@list @t7 @t18 @t12) (= (_ (_ tptp.fresh_441084397e_name @t7) (_ (_ tptp.produc1570949143e_name @t18) @t12)) (and @t19 @t14)))) % 0.48/0.89 (assume @p12 (forall (@list @t7 @t18 @t15) (= (_ (_ tptp.fresh_93646139ame_pi @t7) (_ (_ tptp.product_Pair_name_pi @t18) @t15)) (and @t19 @t17)))) % 0.48/0.89 (assume @p13 (forall (@list @t7 @t20 @t6) (= (_ (_ tptp.fresh_1504024600reeRes @t7) (_ (_ tptp.produc1638681944reeRes @t20) @t6)) (and @t21 @t9)))) % 0.48/0.89 (assume @p14 (forall (@list @t7 @t20 @t12) (= (_ (_ tptp.fresh_261416607i_name @t7) (_ (_ tptp.product_Pair_pi_name @t20) @t12)) (and @t21 @t14)))) % 0.48/0.89 (assume @p15 (forall @t24 (= @t23 (and @t21 @t17)))) % 0.48/0.89 (assume @p16 @t33) % 0.48/0.89 (assume @p17 (forall @t39 (= (_ @t16 @t38) @t37))) % 0.48/0.89 (assume @p18 (forall @t58 (=> @t57 (=> @t54 (=> @t53 (=> @t52 (=> @t50 @t48))))))) % 0.48/0.89 (assume @p19 (forall @t58 (=> @t57 (=> @t60 @t54)))) % 0.48/0.89 (assume @p20 (forall @t58 (=> @t57 (=> @t54 (=> @t53 @t48))))) % 0.48/0.89 (assume @p21 (forall @t24 (=> @t23 @t17))) % 0.48/0.89 (assume @p22 (forall @t32 (=> @t30 @t26))) % 0.48/0.89 (assume @p23 (forall @t64 (=> @t63 @t9))) % 0.48/0.89 (assume @p24 (forall @t67 (=> @t66 @t14))) % 0.48/0.89 (assume @p25 (forall @t70 (=> @t69 @t17))) % 0.48/0.89 (assume @p26 (forall @t74 (=> @t73 (_ @t72 @t71)))) % 0.48/0.89 (assume @p27 (forall @t77 (=> @t76 (_ @t29 @t75)))) % 0.48/0.89 (assume @p28 (forall @t80 (=> @t79 (_ @t62 @t78)))) % 0.48/0.89 (assume @p29 (forall @t83 (=> @t82 (_ @t65 @t81)))) % 0.48/0.89 (assume @p30 (forall @t86 (=> @t85 (_ @t68 @t84)))) % 0.48/0.89 (assume @p31 (forall @t24 (=> @t23 @t21))) % 0.48/0.89 (assume @p32 (forall @t32 (=> @t30 @t19))) % 0.48/0.89 (assume @p33 (forall @t64 (=> @t63 @t87))) % 0.48/0.89 (assume @p34 (forall @t67 (=> @t66 @t87))) % 0.48/0.89 (assume @p35 (forall @t70 (=> @t69 @t87))) % 0.48/0.89 (assume @p36 (forall @t74 (=> @t73 @t87))) % 0.48/0.89 (assume @p37 (forall @t77 (=> @t76 @t87))) % 0.48/0.89 (assume @p38 (forall @t80 (=> @t79 @t87))) % 0.48/0.89 (assume @p39 (forall @t83 (=> @t82 @t87))) % 0.48/0.89 (assume @p40 (forall @t86 (=> @t85 @t87))) % 0.48/0.89 (assume @p41 (forall @t58 (=> @t57 (=> @t60 (=> @t53 @t88))))) % 0.48/0.89 (assume @p42 (forall (@list @t34 @t36 @t91 @t89) (= (= (_ (_ tptp.product_Pair_pi_pi @t34) @t36) (_ (_ tptp.product_Pair_pi_pi @t91) @t89)) (and @t92 @t90)))) % 0.48/0.89 (assume @p43 (forall (@list @t96 @t94 @t95 @t93) (= (= (_ (_ tptp.produc235456326_pi_pi @t96) @t94) (_ (_ tptp.produc235456326_pi_pi @t95) @t93)) (and @t97 (= @t94 @t93))))) % 0.48/0.89 (assume @p44 (forall (@list @t102 @t99 @t101 @t98) (= (= (_ (_ tptp.produc1505598906reeRes @t102) @t99) (_ (_ tptp.produc1505598906reeRes @t101) @t98)) (and @t103 @t100)))) % 0.48/0.89 (assume @p45 (forall (@list @t102 @t105 @t101 @t104) (= (= (_ (_ tptp.produc540578151i_name @t102) @t105) (_ (_ tptp.produc540578151i_name @t101) @t104)) (and @t103 @t106)))) % 0.48/0.89 (assume @p46 (forall (@list @t102 @t36 @t101 @t89) (= (= (_ (_ tptp.produc1820286517_pi_pi @t102) @t36) (_ (_ tptp.produc1820286517_pi_pi @t101) @t89)) (and @t103 @t90)))) % 0.48/0.89 (assume @p47 (forall (@list @t102 @t108 @t101 @t107) (= (= (_ (_ tptp.produc1342893193ion_pi @t102) @t108) (_ (_ tptp.produc1342893193ion_pi @t101) @t107)) (and @t103 (= @t108 @t107))))) % 0.48/0.89 (assume @p48 (forall (@list @t102 @t110 @t101 @t109) (= (= (_ (_ tptp.produc1275980869_pi_pi @t102) @t110) (_ (_ tptp.produc1275980869_pi_pi @t101) @t109)) (and @t103 (= @t110 @t109))))) % 0.48/0.89 (assume @p49 (forall (@list @t102 @t112 @t101 @t111) (= (= (_ (_ tptp.produc703114481reeRes @t102) @t112) (_ (_ tptp.produc703114481reeRes @t101) @t111)) (and @t103 (= @t112 @t111))))) % 0.48/0.89 (assume @p50 (forall (@list @t102 @t114 @t101 @t113) (= (= (_ (_ tptp.produc1024533510i_name @t102) @t114) (_ (_ tptp.produc1024533510i_name @t101) @t113)) (and @t103 (= @t114 @t113))))) % 0.48/0.89 (assume @p51 (forall (@list @t102 @t116 @t101 @t115) (= (= (_ (_ tptp.produc1189045204_pi_pi @t102) @t116) (_ (_ tptp.produc1189045204_pi_pi @t101) @t115)) (and @t103 (= @t116 @t115))))) % 0.48/0.89 (assume @p52 (forall @t126 (= @t125 (and @t122 @t119)))) % 0.48/0.89 (assume @p53 (forall @t133 (= @t132 (and @t131 @t129)))) % 0.48/0.89 (assume @p54 (forall @t141 (= @t140 (and @t139 @t136)))) % 0.48/0.89 (assume @p55 (forall @t146 (= @t145 (and @t139 @t144)))) % 0.48/0.89 (assume @p56 (forall @t148 (= @t147 (and @t139 @t119)))) % 0.48/0.89 (assume @p57 (forall @t155 (= @t154 (and @t139 @t151)))) % 0.48/0.89 (assume @p58 (forall @t160 (= @t159 (and @t139 @t158)))) % 0.48/0.89 (assume @p59 (forall @t165 (= @t164 (and @t139 @t163)))) % 0.48/0.89 (assume @p60 (forall @t170 (= @t169 (and @t139 @t168)))) % 0.48/0.89 (assume @p61 (forall @t175 (= @t174 (and @t139 @t173)))) % 0.48/0.89 (assume @p62 (forall @t182 (not (= @t181 @t178)))) % 0.48/0.89 (assume @p63 (forall (@list @t46 @t183 @t18) (=> @t184 (=> @t52 (_ (_ tptp.fresh_81631222sidual @t18) @t183))))) % 0.48/0.89 (assume @p64 (forall (@list @t186 @t185) (=> @t191 (_ @t186 @t185)))) % 0.48/0.89 (assume @p65 (forall (@list @t193 @t192) (=> @t199 (_ @t193 @t192)))) % 0.48/0.89 (assume @p66 (forall (@list @t201 @t200) (=> @t206 (_ @t201 @t200)))) % 0.48/0.89 (assume @p67 (forall (@list @t208 @t207) (=> @t212 (_ @t208 @t207)))) % 0.48/0.89 (assume @p68 (forall (@list @t214 @t213) (=> @t217 (_ @t214 @t213)))) % 0.48/0.89 (assume @p69 (forall (@list @t219 @t218) (=> @t223 (_ @t219 @t218)))) % 0.48/0.89 (assume @p70 (forall (@list @t225 @t224) (=> @t230 (_ @t225 @t224)))) % 0.48/0.89 (assume @p71 (forall (@list @t232 @t231) (=> @t236 (_ @t232 @t231)))) % 0.48/0.89 (assume @p72 (forall (@list @t238 @t237) (=> @t242 (_ @t238 @t237)))) % 0.48/0.89 (assume @p73 (forall (@list @t244 @t243) (=> @t248 (_ @t244 @t243)))) % 0.48/0.89 (assume @p74 (forall (@list @t25) (not (forall @t190 (not (= @t25 @t189)))))) % 0.48/0.89 (assume @p75 (forall @t249 (not (forall @t198 (not (= @t75 @t197)))))) % 0.48/0.89 (assume @p76 (forall (@list @t78) (not (forall @t205 (not (= @t78 @t204)))))) % 0.48/0.89 (assume @p77 (forall (@list @t81) (not (forall @t211 (not (= @t81 @t210)))))) % 0.48/0.89 (assume @p78 (forall (@list @t84) (not (forall @t216 (not (= @t84 @t215)))))) % 0.48/0.89 (assume @p79 (forall (@list @t250) (not (forall @t222 (not (= @t250 @t221)))))) % 0.48/0.89 (assume @p80 (forall @t252 (not (forall @t229 (not (= @t251 @t228)))))) % 0.48/0.89 (assume @p81 (forall (@list @t253) (not (forall @t235 (not (= @t253 @t234)))))) % 0.48/0.89 (assume @p82 (forall (@list @t254) (not (forall @t241 (not (= @t254 @t240)))))) % 0.48/0.89 (assume @p83 (forall (@list @t255) (not (forall @t247 (not (= @t255 @t246)))))) % 0.48/0.89 (assume @p84 (forall @t126 (=> @t125 (not (=> @t122 @t256))))) % 0.48/0.89 (assume @p85 (forall @t133 (=> @t132 (not (=> @t131 (not @t129)))))) % 0.48/0.89 (assume @p86 (forall @t141 (=> @t140 (not (=> @t139 (not @t136)))))) % 0.48/0.89 (assume @p87 (forall @t146 (=> @t145 (not (=> @t139 (not @t144)))))) % 0.48/0.89 (assume @p88 (forall @t148 (=> @t147 (not (=> @t139 @t256))))) % 0.48/0.89 (assume @p89 (forall @t155 (=> @t154 (not (=> @t139 (not @t151)))))) % 0.48/0.89 (assume @p90 (forall @t160 (=> @t159 (not (=> @t139 (not @t158)))))) % 0.48/0.89 (assume @p91 (forall @t165 (=> @t164 (not (=> @t139 (not @t163)))))) % 0.48/0.89 (assume @p92 (forall @t170 (=> @t169 (not (=> @t139 (not @t168)))))) % 0.48/0.89 (assume @p93 (forall @t175 (=> @t174 (not (=> @t139 (not @t173)))))) % 0.48/0.89 (assume @p94 (forall (@list @t186 @t257) (=> @t191 (_ @t186 @t257)))) % 0.48/0.89 (assume @p95 (forall (@list @t193 @t258) (=> @t199 (_ @t193 @t258)))) % 0.48/0.89 (assume @p96 (forall (@list @t201 @t259) (=> @t206 (_ @t201 @t259)))) % 0.48/0.89 (assume @p97 (forall (@list @t208 @t260) (=> @t212 (_ @t208 @t260)))) % 0.48/0.89 (assume @p98 (forall (@list @t214 @t261) (=> @t217 (_ @t214 @t261)))) % 0.48/0.89 (assume @p99 (forall (@list @t219 @t262) (=> @t223 (_ @t219 @t262)))) % 0.48/0.89 (assume @p100 (forall (@list @t225 @t263) (=> @t230 (_ @t225 @t263)))) % 0.48/0.89 (assume @p101 (forall (@list @t232 @t264) (=> @t236 (_ @t232 @t264)))) % 0.48/0.89 (assume @p102 (forall (@list @t238 @t265) (=> @t242 (_ @t238 @t265)))) % 0.48/0.89 (assume @p103 (forall (@list @t244 @t266) (=> @t248 (_ @t244 @t266)))) % 0.48/0.89 (assume @p104 (forall (@list @t269) (exists (@list @t268 @t267) (= @t269 (_ (_ tptp.produc674047040ion_pi @t268) @t267))))) % 0.48/0.89 (assume @p105 (forall (@list @t258) (exists @t273 (= @t258 @t272)))) % 0.48/0.89 (assume @p106 (forall @t279 (exists @t278 (= @t257 @t277)))) % 0.48/0.89 (assume @p107 (forall (@list @t259) (exists @t282 (= @t259 @t281)))) % 0.48/0.89 (assume @p108 (forall (@list @t263) (exists @t285 (= @t263 @t284)))) % 0.48/0.89 (assume @p109 (forall (@list @t260) (exists @t288 (= @t260 @t287)))) % 0.48/0.89 (assume @p110 (forall (@list @t261) (exists @t290 (= @t261 @t289)))) % 0.48/0.89 (assume @p111 (forall @t295 (exists @t294 (= @t262 @t293)))) % 0.48/0.89 (assume @p112 (forall (@list @t10) (not (forall @t297 (not (_ (_ tptp.fresh_1641682979reeRes @t296) @t10)))))) % 0.48/0.89 (assume @p113 (forall (@list @t298) (not (forall @t297 (not (_ (_ tptp.fresh_1376661020_pi_pi @t296) @t298)))))) % 0.48/0.89 (assume @p114 (forall (@list @t18) (not (forall @t297 (not (_ (_ tptp.fresh_name_name @t296) @t18)))))) % 0.48/0.89 (assume @p115 (forall (@list @t20) (not (forall @t297 (not (_ (_ tptp.fresh_name_pi @t296) @t20)))))) % 0.48/0.89 (assume @p116 (forall @t300 (= (= @t38 (_ (_ tptp.sum @t89) @t91)) @t299))) % 0.48/0.89 (assume @p117 (forall @t308 (=> (forall @t307 (_ @t225 @t306)) @t302))) % 0.48/0.89 (assume @p118 (forall (@list @t193 @t298) (=> (forall @t310 (_ @t193 @t309)) (_ @t193 @t298)))) % 0.48/0.89 (assume @p119 (forall @t308 (=> (forall @t313 (_ @t225 @t312)) @t302))) % 0.48/0.89 (assume @p120 (forall @t252 (not (forall @t307 (not (= @t251 @t306)))))) % 0.48/0.89 (assume @p121 (forall @t249 (not (forall @t310 (not (= @t75 @t309)))))) % 0.48/0.89 (assume @p122 (forall @t252 (not (forall @t313 (not (= @t251 @t312)))))) % 0.48/0.89 (assume @p123 (forall (@list @t7 @t46) (_ @t16 @t314))) % 0.48/0.89 (assume @p124 (forall (@list @t315 @t183 @t46) (=> @t320 @t318))) % 0.48/0.89 (assume @p125 (forall (@list @t46 @t183 @t315) (=> @t184 @t318))) % 0.48/0.89 (assume @p126 (forall (@list @t46 @t315 @t183) (=> @t318 (=> (not @t184) @t320)))) % 0.48/0.89 (assume @p127 (_ @t321 tptp.rel)) % 0.48/0.89 (assume @p128 (forall @t330 (=> @t329 (=> @t52 (=> @t328 (=> @t50 @t327)))))) % 0.48/0.89 (assume @p129 (forall @t334 (=> @t57 (=> @t52 (=> @t328 (=> @t50 @t333)))))) % 0.48/0.89 (assume @p130 (forall (@list @t335 @t186) (= (_ (_ tptp.member558706512_pi_pi @t335) @t336) (_ @t186 @t335)))) % 0.48/0.89 (assume @p131 (forall @t341 (= (_ tptp.collec1051790738_pi_pi (lambda @t340 (_ @t339 @t337))) @t337))) % 0.48/0.89 (assume @p132 (forall (@list @t46 @t315 @t355 @t12 @t40) (=> (_ @t326 @t356) (=> (forall (@list @t347 @t342 @t271 @t358 @t345) (=> @t357 (=> (= @t356 (_ @t352 (_ @t361 @t345))) (=> @t360 @t349)))) (not (forall (@list @t345 @t342 @t271 @t350 @t347) (=> @t357 (=> (= @t356 (_ @t352 (_ @t354 @t350))) (=> (_ (_ tptp.late_transitions @t345) @t353) @t349))))))))) % 0.48/0.89 (assume @p133 (forall (@list @t7 @t18 @t46 @t355 @t12 @t40) (=> (_ @t365 @t356) (not (_ @t362 @t355))))) % 0.48/0.89 (assume @p134 (forall (@list @t18 @t46 @t43 @t12 @t40) (not (_ @t368 (_ (_ @t44 @t12) @t40))))) % 0.48/0.89 (assume @p135 (forall (@list @t371 @t370 @t369) (=> (forall (@list @t378 @t377 @t372 @t375) (=> (_ (_ tptp.fresh_1641682979reeRes @t377) @t375) (=> @t380 (_ @t376 @t379)))) (=> (forall (@list @t373 @t372 @t375) (_ @t376 @t374)) (_ (_ @t371 @t370) @t369))))) % 0.48/0.89 (assume @p136 (forall (@list @t382 @t381 @t369) (=> (forall (@list @t378 @t377 @t372 @t383) (=> (_ (_ tptp.fresh_1376661020_pi_pi @t377) @t383) (=> @t380 (_ @t384 @t379)))) (=> (forall (@list @t373 @t372 @t383) (_ @t384 @t374)) (_ (_ @t382 @t381) @t369))))) % 0.48/0.89 (assume @p137 (forall (@list @t386 @t385 @t369) (=> (forall (@list @t378 @t377 @t372 @t387) (=> (_ (_ tptp.fresh_name_name @t377) @t387) (=> @t380 (_ @t388 @t379)))) (=> (forall (@list @t373 @t372 @t387) (_ @t388 @t374)) (_ (_ @t386 @t385) @t369))))) % 0.48/0.89 (assume @p138 (forall (@list @t390 @t389 @t369) (=> (forall (@list @t378 @t377 @t372 @t391) (=> (_ (_ tptp.fresh_name_pi @t377) @t391) (=> @t380 (_ @t392 @t379)))) (=> (forall (@list @t373 @t372 @t391) (_ @t392 @t374)) (_ (_ @t390 @t389) @t369))))) % 0.48/0.89 (assume @p139 (forall @t39 (= (_ @t16 @t393) @t37))) % 0.48/0.89 (assume @p140 (forall (@list @t7 @t34) (= (_ @t16 @t394) @t35))) % 0.48/0.89 (assume @p141 (forall (@list @t7 @t99 @t34) (= (_ @t396 @t395) (and (_ @t8 @t99) @t35)))) % 0.48/0.89 (assume @p142 (forall (@list @t99 @t34 @t98 @t91) (= (= @t395 (_ (_ tptp.late_FreeR @t98) @t91)) (and @t100 @t92)))) % 0.48/0.89 (assume @p143 (forall @t402 (not (= @t401 @t399)))) % 0.48/0.89 (assume @p144 (forall @t406 (not (= @t401 @t405)))) % 0.48/0.89 (assume @p145 (forall @t410 (not (= @t409 @t405)))) % 0.48/0.89 (assume @p146 (forall (@list @t34 @t91) (= (= @t394 (_ tptp.tau @t91)) @t92))) % 0.48/0.89 (assume @p147 (forall @t300 (= (= @t393 (_ (_ tptp.par @t89) @t91)) @t299))) % 0.48/0.89 (assume @p148 (forall (@list @t315 @t411 @t322 @t46) (=> @t413 (_ @t326 (_ @t412 @t324))))) % 0.48/0.89 (assume @p149 (forall (@list @t46 @t411 @t40 @t315) (=> @t415 (_ @t326 (_ @t412 @t332))))) % 0.48/0.89 (assume @p150 (forall (@list @t7 @t18 @t46 @t411 @t40) (not (_ @t365 @t414)))) % 0.48/0.89 (assume @p151 (forall (@list @t18 @t7 @t12 @t46 @t411 @t40) (not (_ @t416 @t414)))) % 0.48/0.89 (assume @p152 (forall @t182 (not (= (_ (_ tptp.par @t180) @t179) @t178)))) % 0.48/0.89 (assume @p153 (forall (@list @t180 @t179 @t404 @t403) (not (= @t181 @t405)))) % 0.48/0.89 (assume @p154 (forall (@list @t419 @t418 @t400 @t417 @t176) (not (= (_ (_ (_ tptp.late_BoundR @t419) @t418) @t400) (_ (_ tptp.late_FreeR @t417) @t176))))) % 0.48/0.89 (assume @p155 (forall (@list @t420 @t369) (=> (forall (@list @t378 @t377 @t372) (_ @t420 @t379)) (=> (forall (@list @t373 @t372) (_ @t420 @t374)) (_ @t420 @t369))))) % 0.48/0.89 (assume @p156 (forall @t421 (not (= @t409 @t178)))) % 0.48/0.89 (assume @p157 (forall (@list @t400 @t177 @t176) (not (= @t401 @t178)))) % 0.48/0.89 (assume @p158 (forall @t410 (not (= @t409 @t422)))) % 0.48/0.89 (assume @p159 (forall @t406 (not (= @t401 @t422)))) % 0.48/0.89 (assume @p160 (forall (@list @t18 @t46 @t411 @t423 @t424) (=> (_ @t429 (_ @t412 @t423)) (=> (forall @t427 (=> @t426 (=> (_ @t425 @t411) (_ @t424 (_ @t367 @t358))))) (_ @t424 @t423))))) % 0.48/0.89 (assume @p161 (forall (@list @t18 @t46 @t411 @t40) (=> (_ @t429 @t414) (not (forall @t439 (=> @t438 (=> (= @t414 @t436) @t433))))))) % 0.48/0.89 (assume @p162 (forall @t441 (=> @t415 (=> @t440 (_ @t47 (_ @t412 @t42)))))) % 0.48/0.89 (assume @p163 (forall @t441 (=> @t415 (=> @t60 @t88)))) % 0.48/0.89 (assume @p164 (forall @t441 (=> @t415 (=> @t60 @t440)))) % 0.48/0.89 (assume @p165 (forall (@list @t18 @t12 @t46 @t183) (not (_ (_ tptp.late_transitions (_ @t367 (_ (_ (_ tptp.input @t18) @t12) @t46))) @t183)))) % 0.48/0.89 (assume @p166 (forall (@list @t46 @t43 @t18 @t40) (not (_ @t442 @t55)))) % 0.48/0.89 (assume @p167 (forall @t334 (=> @t57 (=> @t328 @t333)))) % 0.48/0.89 (assume @p168 (forall @t330 (=> @t329 (=> @t52 @t327)))) % 0.48/0.89 (assume @p169 (forall (@list @t46 @t315 @t43 @t18 @t443 @t444) (=> (_ @t326 (_ @t45 @t443)) (=> @t52 (=> @t328 (=> (forall @t427 (=> @t445 (_ @t444 (_ @t361 @t315)))) (=> (forall (@list @t350) (=> (_ @t319 (_ @t45 @t350)) (_ @t444 (_ @t323 @t350)))) (_ @t444 @t443)))))))) % 0.48/0.89 (assume @p170 (forall (@list @t121) (_ (_ tptp.member558706512_pi_pi (_ @t123 @t121)) tptp.id_pi))) % 0.48/0.89 (assume @p171 (forall (@list @t138) (_ (_ tptp.member1632198138ion_pi (_ @t152 @t138)) tptp.id_name_noption_pi))) % 0.48/0.89 (assume @p172 (forall @t448 (= @t447 @t446))) % 0.48/0.89 (assume @p173 (forall @t451 (= @t450 @t449))) % 0.48/0.89 (assume @p174 (forall @t458 (=> (forall @t457 (=> (_ @t456 @t337) (_ @t456 @t452))) @t454))) % 0.48/0.89 (assume @p175 (forall @t458 (=> @t454 (=> @t461 @t459)))) % 0.48/0.89 (assume @p176 (forall (@list @t462) (_ @t463 @t462))) % 0.48/0.89 (assume @p177 (forall @t279 (=> (_ (_ tptp.member558706512_pi_pi @t257) tptp.id_pi) (not (forall (@list @t275) (not (= @t257 (_ @t276 @t275)))))))) % 0.48/0.89 (assume @p178 (forall @t295 (=> (_ (_ tptp.member1632198138ion_pi @t262) tptp.id_name_noption_pi) (not (forall (@list @t268) (not (= @t262 (_ @t292 @t268)))))))) % 0.48/0.89 (assume @p179 (forall @t448 (=> @t447 @t446))) % 0.48/0.89 (assume @p180 (forall @t451 (=> @t450 @t449))) % 0.48/0.89 (assume @p181 (forall (@list @t465 @t464) (=> (forall @t273 (=> (_ @t466 @t465) (_ @t466 @t464))) (_ (_ tptp.ord_le797229014_pi_pi @t465) @t464)))) % 0.48/0.89 (assume @p182 (forall (@list @t468 @t467) (=> (forall @t282 (=> (_ @t469 @t468) (_ @t469 @t467))) (_ (_ tptp.ord_le1762471042reeRes @t468) @t467)))) % 0.48/0.89 (assume @p183 (forall (@list @t471 @t470) (=> (forall @t285 (=> (_ @t472 @t471) (_ @t472 @t470))) (_ (_ tptp.ord_le211833513_pi_pi @t471) @t470)))) % 0.48/0.89 (assume @p184 (forall (@list @t474 @t473) (=> (forall @t288 (=> (_ @t475 @t474) (_ @t475 @t473))) (_ (_ tptp.ord_le2082425291i_name @t474) @t473)))) % 0.48/0.89 (assume @p185 (forall (@list @t477 @t476) (=> (forall @t290 (=> (_ @t478 @t477) (_ @t478 @t476))) (_ (_ tptp.ord_le1854926745_pi_pi @t477) @t476)))) % 0.48/0.89 (assume @p186 (forall (@list @t480 @t479) (=> (forall @t294 (=> (_ @t481 @t480) (_ @t481 @t479))) (_ (_ tptp.ord_le1032043601ion_pi @t480) @t479)))) % 0.48/0.89 (assume @p187 (forall (@list @t483 @t482) (=> (forall @t278 (=> (_ @t484 @t483) (_ @t484 @t482))) (_ (_ tptp.ord_le630093991_pi_pi @t483) @t482)))) % 0.48/0.89 (assume @p188 (forall (@list @t485 @t486) (=> @t491 (=> @t489 @t487)))) % 0.48/0.89 (assume @p189 (= @t499 (lambda @t496 (and @t495 @t494)))) % 0.48/0.89 (assume @p190 (forall (@list @t485 @t486 @t500) (=> @t491 (=> (_ @t501 @t485) (_ @t501 @t486))))) % 0.48/0.89 (assume @p191 (forall (@list @t486) (_ @t488 @t486))) % 0.48/0.89 (assume @p192 (forall (@list @t462 @t503 @t502) (=> @t505 (=> (_ @t504 @t502) (_ @t463 @t502))))) % 0.48/0.89 (assume @p193 (forall (@list @t486 @t485) (=> @t489 (=> @t491 @t487)))) % 0.48/0.89 (assume @p194 (forall @t507 (=> @t489 (=> (= @t485 @t500) @t506)))) % 0.48/0.89 (assume @p195 (forall @t507 (=> @t487 @t509))) % 0.48/0.89 (assume @p196 (= @t499 (lambda @t496 (and @t494 @t495)))) % 0.48/0.89 (assume @p197 (forall (@list @t503 @t462) (=> @t511 (= @t505 @t510)))) % 0.48/0.89 (assume @p198 (forall @t507 (=> @t489 @t509))) % 0.48/0.89 (assume @p199 (forall @t512 (=> @t510 @t505))) % 0.48/0.89 (assume @p200 (forall @t512 (=> @t505 (=> @t511 @t510)))) % 0.48/0.89 (assume @p201 (= @t499 (lambda (@list @t513 @t514) (and (_ (_ tptp.ord_le630093991_pi_pi @t513) @t514) (_ (_ tptp.ord_le630093991_pi_pi @t514) @t513))))) % 0.48/0.89 (assume @p202 (forall @t521 (=> @t489 (=> (= @t520 @t500) @t519)))) % 0.48/0.89 (assume @p203 (forall @t523 (=> (= @t486 @t520) @t522))) % 0.48/0.89 (assume @p204 (forall @t521 (=> @t489 (=> (_ (_ tptp.ord_le630093991_pi_pi @t520) @t500) @t519)))) % 0.48/0.89 (assume @p205 (forall @t523 (=> (_ @t488 @t520) @t522))) % 0.48/0.89 (assume @p206 (forall @t526 (= @t525 (forall @t340 (=> (_ @t186 @t338) (_ @t524 @t338)))))) % 0.48/0.89 (assume @p207 (= @t499 (lambda @t529 (and (_ (_ tptp.ord_le630093991_pi_pi @t527) @t528) (_ (_ tptp.ord_le630093991_pi_pi @t528) @t527))))) % 0.48/0.89 (assume @p208 (forall (@list @t337 @t452 @t530) (=> @t454 (=> (_ @t460 @t530) (_ @t453 @t530))))) % 0.48/0.89 (assume @p209 (forall @t526 (=> (forall @t457 (=> (_ @t186 @t455) (_ @t524 @t455))) @t525))) % 0.48/0.89 (assume @p210 (forall @t341 (_ @t453 @t337))) % 0.48/0.89 (assume @p211 (forall @t458 (=> @t459 @t461))) % 0.48/0.89 (assume @p212 (forall @t458 (=> @t459 @t454))) % 0.48/0.89 (assume @p213 (= tptp.ord_le630093991_pi_pi (lambda @t529 (forall @t340 (=> (_ @t339 @t527) (_ @t339 @t528)))))) % 0.48/0.89 (assume @p214 (forall @t458 (=> @t459 (not (=> @t454 (not @t461)))))) % 0.48/0.89 (assume @p215 (forall (@list @t337 @t452 @t531) (=> @t454 (=> (_ @t532 @t337) (_ @t532 @t452))))) % 0.48/0.89 (assume @p216 (forall (@list @t337 @t452 @t533) (=> @t454 (=> (_ @t534 @t337) (_ @t534 @t452))))) % 0.48/0.89 (assume @p217 (forall (@list @t18 @t7 @t12 @t46 @t143 @t385 @t40) (not (_ @t416 (_ (_ @t535 @t385) @t40))))) % 0.48/0.89 (assume @p218 (forall (@list @t18 @t46 @t7 @t143 @t40) (not (_ @t368 @t538)))) % 0.48/0.89 (assume @p219 (forall (@list @t539 @t315 @t46 @t553) (=> @t558 (=> (forall @t557 (=> @t556 (=> @t555 (=> @t554 (=> @t343 (=> (_ (_ tptp.fresh_1641682979reeRes @t271) @t553) @t552)))))) @t549)))) % 0.48/0.89 (assume @p220 (forall (@list @t539 @t315 @t46 @t559) (=> @t558 (=> (forall @t557 (=> @t556 (=> @t555 (=> @t554 (=> @t343 (=> (_ (_ tptp.fresh_1376661020_pi_pi @t271) @t559) @t552)))))) @t549)))) % 0.48/0.89 (assume @p221 (forall (@list @t539 @t315 @t46 @t560) (=> @t558 (=> (forall @t557 (=> @t556 (=> @t555 (=> @t554 (=> @t343 (=> (_ (_ tptp.fresh_name_name @t271) @t560) @t552)))))) @t549)))) % 0.48/0.89 (assume @p222 (forall (@list @t539 @t315 @t46 @t561) (=> @t558 (=> (forall @t557 (=> @t556 (=> @t555 (=> @t554 (=> @t343 (=> (_ @t346 @t561) @t552)))))) @t549)))) % 0.48/0.89 (assume @p223 (forall (@list @t7 @t564 @t96 @t36) (= (_ @t396 @t565) (and (_ @t362 @t564) @t563)))) % 0.48/0.89 (assume @p224 (forall (@list @t18 @t46 @t183) (=> (_ @t429 @t183) (=> (forall @t575 (=> (= @t428 @t574) (forall @t427 (=> (= @t183 @t573) @t571)))) (=> (forall @t568 (=> @t438 (=> (= @t183 @t567) @t566))) (not (forall @t439 (=> @t438 (=> (= @t183 @t436) @t433))))))))) % 0.48/0.89 (assume @p225 (forall (@list @t105 @t96 @t104 @t95) (= (= @t576 (_ (_ tptp.late_OutputR @t104) @t95)) (and @t106 @t97)))) % 0.48/0.89 (assume @p226 (forall (@list @t96 @t95) (= (= @t577 (_ tptp.late_BoundOutputS @t95)) @t97))) % 0.48/0.89 (assume @p227 (forall @t579 (= (_ @t362 @t577) @t578))) % 0.48/0.89 (assume @p228 (forall (@list @t7 @t105 @t96) (= (_ @t8 @t576) (and @t580 @t578)))) % 0.48/0.89 (assume @p229 (forall (@list @t7 @t96 @t36) (= (_ @t16 @t581) @t563))) % 0.48/0.89 (assume @p230 (forall (@list @t7 @t582 @t96 @t36) (= (_ @t16 @t584) (and @t583 @t563)))) % 0.48/0.89 (assume @p231 (forall (@list @t46 @t337 @t40 @t452) (=> (_ (_ @t540 @t337) @t40) (=> @t454 (_ (_ @t540 @t452) @t40))))) % 0.48/0.89 (assume @p232 (forall @t24 (= (= @t586 (_ @t585 @t15)) (= @t20 @t15)))) % 0.48/0.89 (assume @p233 (forall (@list @t46 @t315 @t43 @t18 @t337 @t452) (=> (_ @t588 @t337) (=> @t454 (_ @t588 @t452))))) % 0.48/0.89 (assume @p234 (forall (@list @t96 @t36 @t95 @t89) (= (= @t581 (_ (_ tptp.res @t95) @t89)) @t589))) % 0.48/0.89 (assume @p235 (forall (@list @t564 @t96 @t36 @t590 @t95 @t89) (= (= @t565 (_ (_ (_ tptp.late_BoundR @t590) @t95) @t89)) (and (= @t564 @t590) @t589)))) % 0.48/0.89 (assume @p236 (forall (@list @t143 @t7 @t10) (= (_ (_ tptp.fresh_785364841reeRes @t143) (_ (_ tptp.abs_fu681348580reeRes @t7) @t10)) (or @t592 (_ @t591 @t10))))) % 0.48/0.89 (assume @p237 (forall (@list @t143 @t7 @t298) (= (_ (_ tptp.fresh_2065563522_pi_pi @t143) (_ (_ tptp.abs_fu385186459_pi_pi @t7) @t298)) (or @t592 (_ (_ tptp.fresh_1376661020_pi_pi @t143) @t298))))) % 0.48/0.89 (assume @p238 (forall (@list @t143 @t7 @t18) (= (_ (_ tptp.fresh_1093033124n_name @t143) (_ (_ tptp.abs_fun_name_name @t7) @t18)) (or @t592 (_ (_ tptp.fresh_name_name @t143) @t18))))) % 0.48/0.89 (assume @p239 (forall (@list @t143 @t7 @t20) (= (_ (_ tptp.fresh_543891186ion_pi @t143) @t586) (or @t592 (_ @t593 @t20))))) % 0.48/0.89 (assume @p240 (forall (@list @t582 @t96 @t36 @t594 @t95 @t89) (= (= @t584 (_ (_ (_ tptp.input @t594) @t95) @t89)) (and @t595 @t589)))) % 0.48/0.89 (assume @p241 (forall (@list @t46 @t539 @t315 @t43 @t18 @t322) (=> @t542 (=> @t329 (=> @t52 (exists @t427 (and @t445 (_ (_ (_ (_ (_ tptp.strong2129052853vative @t358) @t322) @t43) @t18) @t539)))))))) % 0.48/0.89 (assume @p242 (forall @t597 (=> @t596 (_ @t541 @t46)))) % 0.48/0.89 (assume @p243 (forall @t602 (=> @t601 (=> @t600 (_ (_ tptp.late_transitions (_ @t599 @t46)) (_ (_ @t598 @t143) @t40)))))) % 0.48/0.89 (assume @p244 (forall (@list @t539 @t46 @t43 @t18) (=> @t596 (_ (_ (_ (_ @t587 @t46) @t43) @t18) @t539)))) % 0.48/0.89 (assume @p245 (forall (@list @t46 @t539 @t315 @t411 @t322) (=> @t542 (=> @t413 (exists @t427 (and @t426 (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t358) @t322)) @t539))))))) % 0.48/0.89 (assume @p246 (forall (@list @t539 @t315 @t18 @t46 @t553) (=> @t558 (=> @t612 (=> (forall @t611 (=> @t610 (=> @t609 (=> @t608 (=> (_ @t431 @t553) @t607))))) @t604))))) % 0.48/0.89 (assume @p247 (forall (@list @t539 @t315 @t18 @t46 @t559) (=> @t558 (=> @t612 (=> (forall @t611 (=> @t610 (=> @t609 (=> @t608 (=> (_ (_ tptp.fresh_1376661020_pi_pi @t286) @t559) @t607))))) @t604))))) % 0.48/0.89 (assume @p248 (forall (@list @t539 @t315 @t18 @t46 @t560) (=> @t558 (=> @t612 (=> (forall @t611 (=> @t610 (=> @t609 (=> @t608 (=> (_ (_ tptp.fresh_name_name @t286) @t560) @t607))))) @t604))))) % 0.48/0.89 (assume @p249 (forall (@list @t539 @t315 @t18 @t46 @t561) (=> @t558 (=> @t612 (=> (forall @t611 (=> @t610 (=> @t609 (=> @t608 (=> (_ @t613 @t561) @t607))))) @t604))))) % 0.48/0.89 (assume @p250 (forall (@list @t315 @t46 @t539) (=> (forall (@list @t342 @t286 @t350) (=> @t610 (=> (_ @t613 @t46) (exists @t547 (and @t606 (_ (_ @t551 @t286) @t539)))))) @t549))) % 0.48/0.89 (assume @p251 (forall (@list @t616 @t46 @t43 @t614 @t40) (=> (_ (_ tptp.late_transitions @t617) @t615) (=> (forall @t575 (=> (= @t617 @t574) (forall @t427 (=> (= @t615 @t573) @t571)))) (not (forall @t568 (=> (= @t617 @t437) (=> (= @t615 @t567) @t566)))))))) % 0.48/0.89 (assume @p252 (forall @t602 (not (_ @t442 @t538)))) % 0.48/0.89 (assume @p253 (forall (@list @t7 @t18 @t46 @t143 @t12 @t40) (not (_ @t365 (_ (_ @t535 @t12) @t40))))) % 0.48/0.89 (assume @p254 (forall @t597 (=> @t596 (_ (_ (_ tptp.strong743114133lation @t618) @t539) @t46)))) % 0.48/0.89 (assume @p255 (forall @t623 (=> @t596 (_ (_ (_ tptp.strong743114133lation @t622) @t539) @t620)))) % 0.48/0.89 (assume @p256 (forall @t597 (=> @t596 (_ @t541 @t618)))) % 0.48/0.89 (assume @p257 (forall @t623 (=> @t596 (_ (_ (_ tptp.strong743114133lation @t620) @t539) @t622)))) % 0.48/0.89 (assume @p258 (forall (@list @t539 @t46 @t315) (=> @t596 (_ (_ (_ tptp.strong743114133lation @t317) @t539) (_ @t621 @t46))))) % 0.48/0.89 (assume @p259 (forall (@list @t105 @t104) (= (= @t624 (_ tptp.late_BoundOutputS @t104)) @t106))) % 0.48/0.89 (assume @p260 (forall (@list @t628 @t626 @t627 @t625) (= (= @t629 (_ (_ tptp.late_OutputR @t627) @t625)) (and (= @t628 @t627) (= @t626 @t625))))) % 0.48/0.89 (assume @p261 (forall @t597 (=> @t596 (_ @t541 @t630)))) % 0.48/0.89 (assume @p262 (forall @t597 (=> @t596 (_ (_ (_ tptp.strong743114133lation @t630) @t539) @t46)))) % 0.48/0.89 (assume @p263 (forall @t631 (_ @t16 tptp.piNil))) % 0.48/0.89 (assume @p264 (forall (@list @t183) (not (_ (_ tptp.late_transitions tptp.piNil) @t183)))) % 0.48/0.89 (assume @p265 (forall (@list @t177 @t176) (not (= tptp.piNil @t178)))) % 0.48/0.89 (assume @p266 (forall @t632 (not (= tptp.piNil @t405)))) % 0.48/0.89 (assume @p267 (forall @t632 (not (= tptp.piNil @t422)))) % 0.48/0.89 (assume @p268 (forall @t633 (not (= tptp.piNil @t399)))) % 0.48/0.89 (assume @p269 (forall (@list @t176) (not (= tptp.piNil @t634)))) % 0.48/0.89 (assume @p270 (forall (@list @t46 @t539) (_ @t541 tptp.piNil))) % 0.48/0.89 (assume @p271 (forall (@list @t18 @t183) (not (_ (_ tptp.late_transitions (_ @t367 tptp.piNil)) @t183)))) % 0.48/0.89 (assume @p272 (forall (@list @t539 @t7 @t18 @t46) (not (_ @t635 @t364)))) % 0.48/0.89 (assume @p273 (forall @t597 (not (_ @t635 @t366)))) % 0.48/0.89 (assume @p274 (forall @t637 (=> (_ (_ tptp.late_transitions (_ (_ @t363 @t143) @t46)) @t183) (not (forall (@list @t271 @t195 @t347) (=> (and @t636 (= (_ (_ tptp.abs_fun_name_pi @t143) @t46) (_ (_ tptp.abs_fun_name_pi @t271) @t347))) (=> (= @t183 (_ (_ (_ tptp.late_BoundR (_ tptp.late_InputS @t195)) @t271) @t347)) (= @t271 @t195)))))))) % 0.48/0.89 (assume @p275 (forall @t579 (= (_ @t362 @t638) @t578))) % 0.48/0.89 (assume @p276 (forall (@list @t96 @t105) (not (= @t638 @t624)))) % 0.48/0.89 (assume @p277 (forall (@list @t640) (=> (forall (@list @t641) (not (= @t640 (_ tptp.late_InputS @t641)))) (not (forall (@list @t639) (not (= @t640 (_ tptp.late_BoundOutputS @t639)))))))) % 0.48/0.89 (assume @p278 (forall (@list @t418 @t177) (not (= (_ tptp.late_InputS @t418) (_ tptp.late_BoundOutputS @t177))))) % 0.48/0.89 (assume @p279 (forall (@list @t642 @t419) (=> (forall @t643 (_ @t642 (_ tptp.late_InputS @t377))) (=> (forall @t643 (_ @t642 (_ tptp.late_BoundOutputS @t377))) (_ @t642 @t419))))) % 0.48/0.89 (assume @p280 (forall (@list @t7 @t18 @t46) @t645)) % 0.48/0.89 (assume @p281 (forall (@list @t18 @t7 @t46) (=> @t646 @t645))) % 0.48/0.89 (assume @p282 (forall (@list @t18 @t7 @t143 @t46 @t647 @t12 @t40) (not (_ @t650 (_ (_ (_ tptp.late_BoundR (_ tptp.late_InputS @t647)) @t12) @t40))))) % 0.48/0.89 (assume @p283 (forall (@list @t18 @t7 @t46 @t143 @t12 @t40) (not (_ (_ tptp.late_transitions (_ @t367 (_ (_ @t648 @t18) @t46))) (_ (_ tptp.late_FreeR (_ (_ tptp.late_OutputR @t143) @t12)) @t40))))) % 0.48/0.89 (assume @p284 (forall @t657 (=> @t656 (=> @t655 (=> @t60 @t653))))) % 0.48/0.89 (assume @p285 (forall (@list @t46 @t7) (= (_ @t659 @t7) @t46))) % 0.48/0.89 (assume @p286 (forall (@list @t18 @t647 @t660 @t46) (=> (not (= @t18 @t647)) (=> (not (= @t18 @t660)) (= (_ (_ (_ tptp.subs @t428) @t647) @t660) (_ @t367 @t661)))))) % 0.48/0.89 (assume @p287 (forall @t663 (= (_ (_ (_ tptp.subs @t325) @t647) @t660) (_ (_ tptp.par @t661) @t662)))) % 0.48/0.89 (assume @p288 (forall (@list @t143 @t46 @t7 @t647) (=> @t665 (= (_ (_ (_ tptp.subs @t664) @t143) @t647) (_ @t659 @t647))))) % 0.48/0.89 (assume @p289 (forall @t663 (= (_ (_ (_ tptp.subs @t317) @t647) @t660) (_ (_ tptp.sum @t661) @t662)))) % 0.48/0.89 (assume @p290 (forall (@list @t46 @t647 @t660) (= (_ (_ (_ tptp.subs @t366) @t647) @t660) (_ tptp.tau @t661)))) % 0.48/0.89 (assume @p291 (forall (@list @t647 @t660) (= (_ (_ (_ tptp.subs tptp.piNil) @t647) @t660) tptp.piNil))) % 0.48/0.89 (assume @p292 (forall @t631 (_ @t8 tptp.late_TauR))) % 0.48/0.89 (assume @p293 (forall @t668 (= (_ @t16 @t667) @t666))) % 0.48/0.89 (assume @p294 (forall (@list @t18 @t7 @t143 @t46 @t40) (not (_ @t650 @t669)))) % 0.48/0.89 (assume @p295 (forall (@list @t7 @t143 @t46 @t40) (not (_ @t670 @t669)))) % 0.48/0.89 (assume @p296 (forall @t421 (not (= @t671 @t178)))) % 0.48/0.89 (assume @p297 (forall @t410 (not (= @t671 @t405)))) % 0.48/0.89 (assume @p298 (forall @t410 (not (= @t671 @t422)))) % 0.48/0.89 (assume @p299 (forall @t673 (= (= @t667 (_ (_ (_ tptp.output @t594) @t104) @t91)) @t672))) % 0.48/0.89 (assume @p300 (forall (@list @t675 @t674) (=> (forall (@list @t677 @t676) (_ @t675 (_ (_ tptp.late_OutputR @t677) @t676))) (=> (_ @t675 tptp.late_TauR) (_ @t675 @t674))))) % 0.48/0.89 (assume @p301 (forall (@list @t408 @t407) (not (= (_ (_ tptp.late_OutputR @t408) @t407) tptp.late_TauR)))) % 0.48/0.89 (assume @p302 (forall (@list @t408 @t407 @t400 @t176) (not (= @t671 @t634)))) % 0.48/0.89 (assume @p303 (forall @t678 (not (= @t671 @t399)))) % 0.48/0.89 (assume @p304 (forall @t633 (not (= tptp.piNil (_ (_ (_ tptp.output @t398) @t397) @t176))))) % 0.48/0.89 (assume @p305 (forall @t679 (=> @t600 (_ @t16 @t664)))) % 0.48/0.89 (assume @p306 (forall (@list @t7 @t46 @t647 @t143) (=> @t681 (=> @t680 (_ @t16 (_ (_ @t658 @t143) @t647)))))) % 0.48/0.89 (assume @p307 (forall (@list @t7 @t46 @t143) (=> @t681 (= @t664 @t46)))) % 0.48/0.89 (assume @p308 (forall (@list @t6) (=> (forall (@list @t683 @t682) (not (= @t6 (_ (_ tptp.late_OutputR @t683) @t682)))) (= @t6 tptp.late_TauR)))) % 0.48/0.89 (assume @p309 (forall (@list @t628 @t626) (not (= @t629 tptp.late_TauR)))) % 0.48/0.89 (assume @p310 (forall @t685 (=> @t665 (= (_ (_ (_ tptp.subs @t314) @t7) @t143) @t684)))) % 0.48/0.89 (assume @p311 (forall @t685 (=> @t665 (= @t314 @t684)))) % 0.48/0.89 (assume @p312 (forall (@list @t18 @t143 @t46 @t183) (not (_ (_ tptp.late_transitions (_ @t367 (_ (_ (_ tptp.output @t18) @t143) @t46))) @t183)))) % 0.48/0.89 (assume @p313 (forall (@list @t7 @t143 @t46 @t686 @t18 @t40) (not (_ @t670 (_ (_ (_ tptp.late_BoundR @t686) @t18) @t40))))) % 0.48/0.89 (assume @p314 (forall @t687 (not (_ @t635 @t649)))) % 0.48/0.89 (assume @p315 (forall @t691 (=> @t601 (=> @t690 @t689)))) % 0.48/0.89 (assume @p316 (forall @t694 (=> @t656 (=> @t693 @t692)))) % 0.48/0.89 (assume @p317 (forall @t679 (_ @t670 (_ @t537 @t46)))) % 0.48/0.89 (assume @p318 (forall (@list @t7 @t143 @t46 @t647 @t660 @t40) (=> (_ @t670 (_ (_ tptp.late_FreeR (_ (_ tptp.late_OutputR @t647) @t660)) @t40)) (not (or @t680 (not (= @t143 @t660))))))) % 0.48/0.89 (assume @p319 (forall @t637 (=> (_ @t670 @t183) (not (forall (@list @t195 @t209 @t347) (=> (and @t636 (= @t143 @t209) (= @t46 @t347)) (not (= @t183 (_ @t570 @t347))))))))) % 0.48/0.89 (assume @p320 (forall (@list @t7 @t143 @t46 @t411 @t40 @t695) (=> @t698 (=> (=> (= @t411 @t536) (=> @t697 (_ (_ @t695 @t536) @t46))) @t696)))) % 0.48/0.89 (assume @p321 (forall (@list @t7 @t143 @t46 @t411 @t40) (=> @t698 (not (or (_ @t8 @t411) (_ @t591 @t411)))))) % 0.48/0.89 (assume @p322 (forall @t691 (=> @t601 (=> @t690 (=> @t52 (=> @t328 (=> @t646 (=> @t700 (=> @t699 @t689))))))))) % 0.48/0.89 (assume @p323 (forall @t694 (=> @t656 (=> @t693 (=> @t52 (=> @t328 (=> @t646 (=> @t700 (=> @t701 @t692))))))))) % 0.48/0.89 (assume @p324 (forall (@list @t46) (_ @t442 (_ @t652 @t46)))) % 0.48/0.89 (assume @p325 (forall (@list @t46 @t183) (=> (_ @t442 @t183) (not (forall (@list @t347) (=> (= @t366 (_ tptp.tau @t347)) (not (= @t183 (_ @t652 @t347))))))))) % 0.48/0.89 (assume @p326 (forall (@list @t46 @t411 @t40 @t695) (=> (_ @t442 @t414) (=> (=> (= @t411 tptp.late_TauR) (=> @t697 (_ (_ @t695 tptp.late_TauR) @t46))) @t696)))) % 0.48/0.89 (assume @p327 (forall @t707 (=> @t706 (=> @t690 (=> @t52 (=> @t328 (=> @t60 (=> @t705 (=> @t646 (=> @t699 (=> @t704 (=> (_ @t59 @t322) (=> @t703 @t702))))))))))))) % 0.48/0.89 (assume @p328 (forall @t657 (=> @t656 (=> @t655 (=> @t52 (=> @t328 (=> @t60 (=> @t705 (=> @t646 (=> @t701 (=> @t704 (=> @t88 (=> @t703 @t653))))))))))))) % 0.48/0.89 (assume @p329 (forall @t707 (=> @t706 (=> @t690 (=> @t705 @t702))))) % 0.48/0.89 (assume @p330 (forall @t687 (=> @t596 (=> @t600 (_ @t541 @t708))))) % 0.48/0.89 (assume @p331 (forall @t687 (=> @t596 (=> @t600 (_ (_ (_ tptp.strong743114133lation @t708) @t539) @t46))))) % 0.48/0.89 (assume @p332 (forall @t668 (= (_ @t16 @t709) @t666))) % 0.48/0.89 (assume @p333 (forall @t678 (not (= @t671 @t710)))) % 0.48/0.89 (assume @p334 (forall @t633 (not (= tptp.piNil @t710)))) % 0.48/0.89 (assume @p335 (forall @t410 (not (= @t711 @t422)))) % 0.48/0.89 (assume @p336 (forall @t678 (not (= @t409 @t710)))) % 0.48/0.89 (assume @p337 (forall @t402 (not (= @t401 @t710)))) % 0.48/0.89 (assume @p338 (forall @t673 (= (= @t709 (_ (_ (_ tptp.mismatch @t594) @t104) @t91)) @t672))) % 0.48/0.89 (assume @p339 (forall @t410 (not (= @t711 @t405)))) % 0.48/0.89 (assume @p340 (not (not @t712))) % 0.48/0.89 (assume @p341 true) % 0.48/0.89 (step @p342 (= tptp.ord_le630093991_pi_pi @t715) :rule refl :args (@t715)) % 0.48/0.89 (step @p343 (= tptp.strong743114133lation @t729) :rule refl :args (@t729)) % 0.48/0.89 (step @p344 (= tptp.fresh_name_name @t732) :rule refl :args (@t732)) % 0.48/0.89 (step @p345 :rule refl :args ((tptp.fresh_1376661020_pi_pi tptp.y @t734))) % 0.48/0.89 (step @p346 :rule refl :args ((tptp.produc235456326_pi_pi tptp.y @t1))) % 0.48/0.89 (step @p347 :rule refl :args (@t735)) % 0.48/0.89 (step @p348 :rule refl :args (tptp.y)) % 0.48/0.89 (step @p349 :rule cong :premises (@p348 @p347) :args (@t736)) % 0.48/0.89 (step @p350 :rule trans :premises (@p349 @p346)) % 0.48/0.89 (step @p351 :rule cong :premises (@p348 @p350) :args (@t737)) % 0.48/0.89 (step @p352 :rule trans :premises (@p351 @p345)) % 0.48/0.89 (step @p353 :rule refl :args (@t2)) % 0.48/0.89 (step @p354 :rule ho_cong :premises (@p353 @p350)) % 0.48/0.89 (step @p355 :rule cong :premises (@p354 @p352) :args ((= (_ @t2 @t736) @t737))) % 0.48/0.89 (step @p356 :rule symm :premises (@p355)) % 0.48/0.89 (step @p357 :rule refl :args ((_ @t2 @t734))) % 0.48/0.89 (step @p358 :rule eq_resolve :premises (@p357 @p356)) % 0.48/0.89 (step @p359 :rule refl :args (@t733)) % 0.48/0.89 (step @p360 :rule ho_cong :premises (@p359 @p347)) % 0.48/0.89 (step @p361 :rule cong :premises (@p360 @p350) :args ((= (_ @t733 @t735) @t736))) % 0.48/0.89 (step @p362 :rule symm :premises (@p361)) % 0.48/0.89 (step @p363 :rule refl :args (@t734)) % 0.48/0.89 (step @p364 :rule eq_resolve :premises (@p363 @p362)) % 0.48/0.89 (step @p365 :rule refl :args (@t1)) % 0.48/0.89 (step @p366 :rule cong :premises (@p365 @p347) :args ((= @t1 @t735))) % 0.48/0.89 (step @p367 :rule symm :premises (@p366)) % 0.48/0.89 (step @p368 :rule eq_resolve :premises (@p365 @p367)) % 0.48/0.89 (step @p369 :rule refl :args (@t733)) % 0.48/0.89 (step @p370 :rule ho_cong :premises (@p369 @p368)) % 0.48/0.89 (step @p371 :rule trans :premises (@p370 @p364)) % 0.48/0.89 (step @p372 :rule refl :args (@t2)) % 0.48/0.89 (step @p373 :rule ho_cong :premises (@p372 @p371)) % 0.48/0.89 (step @p374 :rule trans :premises (@p373 @p358)) % 0.48/0.89 (step @p375 :rule refl :args (@t1)) % 0.48/0.89 (step @p376 :rule eq-symm :args (tptp.y tptp.x)) % 0.48/0.89 (step @p377 :rule bool-double-not-elim :args (@t712)) % 0.48/0.89 (step @p378 :rule trans :premises (@p377 @p376)) % 0.48/0.89 (step @p379 :rule eq_resolve :premises (@p340 @p378)) % 0.48/0.89 (step @p380 :rule refl :args (tptp.produc235456326_pi_pi)) % 0.48/0.89 (step @p381 :rule ho_cong :premises (@p380 @p379)) % 0.48/0.89 (step @p382 :rule ho_cong :premises (@p381 @p375)) % 0.48/0.89 (step @p383 :rule ho_cong :premises (@p372 @p382)) % 0.48/0.89 (step @p384 :rule trans :premises (@p383 @p374)) % 0.48/0.89 (step @p385 :rule eq_resolve :premises (@p2 @p384)) % 0.48/0.89 (step @p386 :rule refl :args (@t738)) % 0.48/0.89 (step @p387 :rule refl :args (@t26)) % 0.48/0.89 (step @p388 :rule cong :premises (@p387 @p386) :args ((= @t26 @t738))) % 0.48/0.89 (step @p389 :rule symm :premises (@p388)) % 0.48/0.89 (step @p390 :rule eq_resolve :premises (@p387 @p389)) % 0.48/0.89 (step @p391 :rule refl :args (@t739)) % 0.48/0.89 (step @p392 :rule nary_cong :premises (@p391 @p390) :args (@t740)) % 0.48/0.89 (step @p393 :rule refl :args ((tptp.fresh_1376661020_pi_pi @t7 @t28))) % 0.48/0.89 (step @p394 :rule refl :args (@t741)) % 0.48/0.89 (step @p395 :rule refl :args (@t7)) % 0.48/0.89 (step @p396 :rule cong :premises (@p395 @p394) :args (@t742)) % 0.48/0.89 (step @p397 :rule trans :premises (@p396 @p393)) % 0.48/0.89 (step @p398 :rule refl :args (@t29)) % 0.48/0.89 (step @p399 :rule ho_cong :premises (@p398 @p394)) % 0.48/0.89 (step @p400 :rule cong :premises (@p399 @p397) :args ((= (_ @t29 @t741) @t742))) % 0.48/0.89 (step @p401 :rule symm :premises (@p400)) % 0.48/0.89 (step @p402 :rule refl :args (@t30)) % 0.48/0.89 (step @p403 :rule eq_resolve :premises (@p402 @p401)) % 0.48/0.89 (step @p404 :rule refl :args (@t28)) % 0.48/0.89 (step @p405 :rule cong :premises (@p404 @p394) :args ((= @t28 @t741))) % 0.48/0.89 (step @p406 :rule symm :premises (@p405)) % 0.48/0.89 (step @p407 :rule eq_resolve :premises (@p404 @p406)) % 0.48/0.89 (step @p408 :rule ho_cong :premises (@p398 @p407)) % 0.48/0.89 (step @p409 :rule trans :premises (@p408 @p403)) % 0.48/0.89 (step @p410 :rule cong :premises (@p409 @p392) :args (@t743)) % 0.48/0.89 (step @p411 :rule cong :premises (@p410) :args ((forall @t32 @t743))) % 0.48/0.89 (step @p412 :rule refl :args (@t26)) % 0.48/0.89 (step @p413 :rule beta-reduce :args ((= (_ @t744 @t18) @t739))) % 0.48/0.89 (step @p414 :rule refl :args (@t18)) % 0.48/0.89 (step @p415 :rule beta-reduce :args ((= @t745 @t744))) % 0.48/0.89 (step @p416 :rule ho_cong :premises (@p415 @p414)) % 0.48/0.89 (step @p417 :rule trans :premises (@p416 @p413)) % 0.48/0.89 (step @p418 :rule nary_cong :premises (@p417 @p412) :args (@t746)) % 0.48/0.89 (step @p419 :rule refl :args (@t30)) % 0.48/0.89 (step @p420 :rule cong :premises (@p419 @p418) :args (@t747)) % 0.48/0.89 (step @p421 :rule cong :premises (@p420) :args ((forall @t32 @t747))) % 0.48/0.89 (step @p422 :rule trans :premises (@p421 @p411)) % 0.48/0.89 (step @p423 :rule refl :args (@t7)) % 0.48/0.89 (step @p424 :rule ho_cong :premises (@p344 @p423)) % 0.48/0.89 (step @p425 :rule ho_cong :premises (@p424 @p414)) % 0.48/0.89 (step @p426 :rule nary_cong :premises (@p425 @p412) :args (@t27)) % 0.48/0.89 (step @p427 :rule cong :premises (@p419 @p426) :args (@t31)) % 0.48/0.89 (step @p428 :rule cong :premises (@p427) :args (@t33)) % 0.48/0.89 (step @p429 :rule trans :premises (@p428 @p422)) % 0.48/0.89 (step @p430 :rule eq_resolve :premises (@p16 @p429)) % 0.48/0.89 (step @p431 :rule bool-eq-false :args (@t737)) % 0.48/0.89 (step @p432 :rule absorb :args ((= (and false @t748) false))) % 0.48/0.89 (step @p433 :rule refl :args (@t748)) % 0.48/0.89 (step @p434 :rule evaluate :args ((not true))) % 0.48/0.89 (step @p435 :rule eq-refl :args (tptp.y)) % 0.48/0.89 (step @p436 :rule cong :premises (@p435) :args (@t749)) % 0.48/0.89 (step @p437 :rule trans :premises (@p436 @p434)) % 0.48/0.89 (step @p438 :rule nary_cong :premises (@p437 @p433) :args (@t750)) % 0.48/0.89 (step @p439 :rule trans :premises (@p438 @p432)) % 0.48/0.89 (step @p440 :rule refl :args (@t737)) % 0.48/0.89 (step @p441 :rule cong :premises (@p440 @p439) :args (@t751)) % 0.48/0.89 (step @p442 :rule trans :premises (@p441 @p431)) % 0.48/0.89 (step @p443 :rule refl :args (@t752)) % 0.48/0.89 (step @p444 :rule cong :premises (@p443 @p442) :args ((=> @t752 @t751))) % 0.48/0.89 (assume-push @p453 @t752) % 0.48/0.89 (step @p446 :rule instantiate :premises (@p430) :args ((@list tptp.y tptp.y @t735))) % 0.48/0.89 (step-pop @p454 :rule scope :premises (@p446)) % 0.48/0.89 (step @p447 :rule process_scope :premises (@p454) :args (@t751)) % 0.48/0.89 (step @p449 :rule eq_resolve :premises (@p447 @p444)) % 0.48/0.89 (step @p450 :rule implies_elim :premises (@p449)) % 0.48/0.89 (step @p451 :rule reordering :premises (@p450) :args ((or (not @t737) (not @t752)))) % 0.48/0.89 (step @p452 false :rule chain_m_resolution :premises (@p451 @p430 @p385) :args (false (@list false false) (@list @t752 @t737))) % 0.48/0.89 ) % 0.48/0.89 % SZS output end Proof % 0.48/0.89 % cvc5 exiting %------------------------------------------------------------------------------