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