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