%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP191^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:25:19 AM UTC 2026 % Result : Theorem 0.48s 0.93s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP191^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 : n020.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:25 EDT 2026 % 0.16/0.34 % CPUTime : % 0.38/0.64 %----Proving TH0 % 0.48/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.48/0.93 % SZS status Theorem % 0.48/0.93 % SZS output start Proof % 0.48/0.93 ( % 0.48/0.93 (declare-sort tptp.produc367475239e_name 0) % 0.48/0.93 (declare-sort tptp.name 0) % 0.48/0.93 (declare-sort tptp.late_freeRes 0) % 0.48/0.93 (declare-sort tptp.pi 0) % 0.48/0.93 (declare-sort tptp.late_residual_Rep 0) % 0.48/0.93 (declare-sort tptp.late_subject 0) % 0.48/0.93 (declare-sort tptp.set_Pr443758855e_name 0) % 0.48/0.93 (declare-sort tptp.produc1212344719pi_Rep 0) % 0.48/0.93 (declare-sort tptp.set_Pr1131282415pi_Rep 0) % 0.48/0.93 (declare-sort tptp.produc1357834675reeRes 0) % 0.48/0.93 (declare-sort tptp.set_Pr1780909331reeRes 0) % 0.48/0.93 (declare-sort tptp.produc1359399907ubject 0) % 0.48/0.93 (declare-sort tptp.set_Pr806375235ubject 0) % 0.48/0.93 (declare-sort tptp.list_P227219501e_name 0) % 0.48/0.93 (declare-sort tptp.list_pi 0) % 0.48/0.93 (declare-sort tptp.list_name 0) % 0.48/0.93 (declare-sort tptp.pi_Rep 0) % 0.48/0.93 (declare-sort tptp.list_pi_Rep 0) % 0.48/0.93 (declare-sort tptp.list_Late_freeRes 0) % 0.48/0.93 (declare-sort tptp.list_Late_subject 0) % 0.48/0.93 (declare-sort tptp.produc992857746Res_pi 0) % 0.48/0.93 (declare-sort tptp.produc2052722628s_name 0) % 0.48/0.93 (declare-sort tptp.produc1777919905pi_Rep 0) % 0.48/0.93 (declare-sort tptp.set_name 0) % 0.48/0.93 (declare-sort tptp.product_unit 0) % 0.48/0.93 (declare-sort tptp.produc971140967t_unit 0) % 0.48/0.93 (declare-sort tptp.produc546891580t_unit 0) % 0.48/0.93 (declare-sort tptp.set_pi_Rep 0) % 0.48/0.93 (declare-sort tptp.set_Late_freeRes 0) % 0.48/0.93 (declare-sort tptp.set_Late_subject 0) % 0.48/0.93 (declare-sort tptp.produc257012921pi_Rep 0) % 0.48/0.93 (declare-sort tptp.noption_pi 0) % 0.48/0.93 (declare-sort tptp.set_Pr1834926343_pi_pi 0) % 0.48/0.93 (declare-sort tptp.produc738223008nit_pi 0) % 0.48/0.93 (declare-sort tptp.late_residual 0) % 0.48/0.93 (declare-sort tptp.produc1141751126_pi_pi 0) % 0.48/0.93 (declare-sort tptp.product_prod_pi_pi 0) % 0.48/0.93 (declare-sort tptp.list_name_noption_pi 0) % 0.48/0.93 (declare-sort tptp.produc140253050ect_pi 0) % 0.48/0.93 (declare-sort tptp.product_prod_name_pi 0) % 0.48/0.93 (declare-sort tptp.set_pi 0) % 0.48/0.93 (declare-sort tptp.produc1998742700t_name 0) % 0.48/0.93 (declare-sort tptp.produc135724498t_name 0) % 0.48/0.93 (declare-sort tptp.produc214645451ubject 0) % 0.48/0.93 (declare-sort tptp.produc355105483reeRes 0) % 0.48/0.93 (declare-sort tptp.product_prod_pi_name 0) % 0.48/0.93 (declare-sort tptp.produc1028309998t_unit 0) % 0.48/0.93 (declare-sort tptp.late_freeRes_Rep 0) % 0.48/0.93 (declare-sort tptp.list_Product_unit 0) % 0.48/0.93 (declare-sort tptp.late_subject_Rep 0) % 0.48/0.93 (declare-sort tptp.list_P431515740_pi_pi 0) % 0.48/0.93 (declare-const tptp.perm_n1415585007_pi_pi (-> tptp.list_P227219501e_name tptp.product_prod_pi_pi tptp.product_prod_pi_pi)) % 0.48/0.93 (declare-const tptp.member558706512_pi_pi (-> tptp.product_prod_pi_pi tptp.set_Pr1834926343_pi_pi Bool)) % 0.48/0.93 (declare-const tptp.product_Pair_pi_pi (-> tptp.pi tptp.pi tptp.product_prod_pi_pi)) % 0.48/0.93 (declare-const tptp.fresh_name_pi (-> tptp.name tptp.pi Bool)) % 0.48/0.93 (declare-const tptp.late_FreeR (-> tptp.late_freeRes tptp.pi tptp.late_residual)) % 0.48/0.93 (declare-const tptp.late_transitions (-> tptp.pi tptp.late_residual Bool)) % 0.48/0.93 (declare-const tptp.strong2129052853vative (-> tptp.pi tptp.pi tptp.late_subject tptp.name tptp.set_Pr1834926343_pi_pi Bool)) % 0.48/0.93 (declare-const tptp.late_BoundR (-> tptp.late_subject tptp.name tptp.pi tptp.late_residual)) % 0.48/0.93 (declare-const tptp.abs_fun_name_pi (-> tptp.name tptp.pi tptp.name tptp.noption_pi)) % 0.48/0.93 (declare-const tptp.swap_name (-> tptp.produc367475239e_name tptp.name tptp.name)) % 0.48/0.93 (declare-const tptp.swap_name2 (-> tptp.produc367475239e_name tptp.name tptp.name)) % 0.48/0.93 (declare-const tptp.defaul1399868459t_unit tptp.product_unit) % 0.48/0.93 (declare-const tptp.input (-> tptp.name tptp.name tptp.pi tptp.pi)) % 0.48/0.93 (declare-const tptp.eqvt_name (-> tptp.set_Pr443758855e_name Bool)) % 0.48/0.93 (declare-const tptp.member695284560e_name (-> tptp.produc367475239e_name tptp.set_Pr443758855e_name Bool)) % 0.48/0.93 (declare-const tptp.eqvt_pi_Rep (-> tptp.set_Pr1131282415pi_Rep Bool)) % 0.48/0.93 (declare-const tptp.member1671908408pi_Rep (-> tptp.produc1212344719pi_Rep tptp.set_Pr1131282415pi_Rep Bool)) % 0.48/0.93 (declare-const tptp.produc784048711pi_Rep (-> tptp.pi_Rep tptp.pi_Rep tptp.produc1212344719pi_Rep)) % 0.48/0.93 (declare-const tptp.eqvt_Late_freeRes (-> tptp.set_Pr1780909331reeRes Bool)) % 0.48/0.93 (declare-const tptp.member1584979804reeRes (-> tptp.produc1357834675reeRes tptp.set_Pr1780909331reeRes Bool)) % 0.48/0.93 (declare-const tptp.eqvt_Late_subject (-> tptp.set_Pr806375235ubject Bool)) % 0.48/0.93 (declare-const tptp.late_r347633188eR_Rep (-> tptp.late_freeRes tptp.pi tptp.late_residual_Rep)) % 0.48/0.93 (declare-const tptp.member1586545036ubject (-> tptp.produc1359399907ubject tptp.set_Pr806375235ubject Bool)) % 0.48/0.93 (declare-const tptp.perm_name_list_pi (-> tptp.list_P227219501e_name tptp.list_pi tptp.list_pi)) % 0.48/0.93 (declare-const tptp.perm_name_list_name (-> tptp.list_P227219501e_name tptp.list_name tptp.list_name)) % 0.48/0.93 (declare-const tptp.perm_n729617823pi_Rep (-> tptp.list_P227219501e_name tptp.list_pi_Rep tptp.list_pi_Rep)) % 0.48/0.93 (declare-const tptp.member_Late_freeRes (-> tptp.late_freeRes tptp.set_Late_freeRes Bool)) % 0.48/0.93 (declare-const tptp.perm_n1938283068es_Rep (-> tptp.list_P227219501e_name tptp.late_freeRes_Rep tptp.late_freeRes_Rep)) % 0.48/0.93 (declare-const tptp.if_Late_subject (-> Bool tptp.late_subject tptp.late_subject tptp.late_subject)) % 0.48/0.93 (declare-const tptp.perm_n1555914327reeRes (-> tptp.list_P227219501e_name tptp.set_Late_freeRes tptp.set_Late_freeRes)) % 0.48/0.93 (declare-const tptp.fresh_name_list_name (-> tptp.name tptp.list_name Bool)) % 0.48/0.93 (declare-const tptp.member_Late_subject (-> tptp.late_subject tptp.set_Late_subject Bool)) % 0.48/0.93 (declare-const tptp.late_OutputR (-> tptp.name tptp.name tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.perm_n414416632sidual (-> tptp.list_P227219501e_name tptp.late_residual tptp.late_residual)) % 0.48/0.93 (declare-const tptp.perm_n675238095_pi_pi (-> tptp.list_P227219501e_name tptp.set_Pr1834926343_pi_pi tptp.set_Pr1834926343_pi_pi)) % 0.48/0.93 (declare-const tptp.fresh_922791155e_name (-> tptp.name tptp.list_P227219501e_name Bool)) % 0.48/0.93 (declare-const tptp.perm_n382765978reeRes (-> tptp.list_P227219501e_name (-> tptp.name tptp.late_freeRes) tptp.name tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.produc1647375838t_name (-> tptp.late_subject tptp.name tptp.produc1998742700t_name)) % 0.48/0.93 (declare-const tptp.perm_n1446290985reeRes (-> tptp.list_P227219501e_name (-> tptp.late_freeRes tptp.late_freeRes) tptp.late_freeRes tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.perm_n443561793reeRes (-> tptp.list_P227219501e_name (-> tptp.late_subject tptp.late_freeRes) tptp.late_subject tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.perm_n1387060402ubject (-> tptp.list_P227219501e_name (-> tptp.name tptp.late_subject) tptp.name tptp.late_subject)) % 0.48/0.93 (declare-const tptp.produc324947500ect_pi (-> tptp.late_subject tptp.pi tptp.produc140253050ect_pi)) % 0.48/0.93 (declare-const tptp.perm_n412725103ubject (-> tptp.list_P227219501e_name tptp.set_Late_subject tptp.set_Late_subject)) % 0.48/0.93 (declare-const tptp.fresh_name_list_pi (-> tptp.name tptp.list_pi Bool)) % 0.48/0.93 (declare-const tptp.res (-> tptp.name tptp.pi tptp.pi)) % 0.48/0.93 (declare-const tptp.collec1051790738_pi_pi (-> (-> tptp.product_prod_pi_pi Bool) tptp.set_Pr1834926343_pi_pi)) % 0.48/0.93 (declare-const tptp.perm_n1447856217ubject (-> tptp.list_P227219501e_name (-> tptp.late_subject tptp.late_subject) tptp.late_subject tptp.late_subject)) % 0.48/0.93 (declare-const tptp.perm_name_o (-> tptp.list_P227219501e_name Bool Bool)) % 0.48/0.93 (declare-const tptp.fresh_1376661020_pi_pi (-> tptp.name tptp.produc1141751126_pi_pi Bool)) % 0.48/0.93 (declare-const tptp.fresh_1143631827t_unit (-> tptp.name tptp.product_unit Bool)) % 0.48/0.93 (declare-const tptp.perm_n1960409557t_unit (-> tptp.list_P227219501e_name tptp.product_unit tptp.product_unit)) % 0.48/0.93 (declare-const tptp.fresh_1641682979reeRes (-> tptp.name tptp.late_freeRes Bool)) % 0.48/0.93 (declare-const tptp.perm_n303101761ubject (-> tptp.list_P227219501e_name (-> tptp.late_freeRes tptp.late_subject) tptp.late_freeRes tptp.late_subject)) % 0.48/0.93 (declare-const tptp.fresh_717452603ubject (-> tptp.name tptp.late_subject Bool)) % 0.48/0.93 (declare-const tptp.perm_name_set_pi (-> tptp.list_P227219501e_name tptp.set_pi tptp.set_pi)) % 0.48/0.93 (declare-const tptp.perm_n1667196784ion_pi (-> tptp.list_P227219501e_name (-> tptp.name tptp.noption_pi) tptp.name tptp.noption_pi)) % 0.48/0.93 (declare-const tptp.produc843063281pi_Rep (-> tptp.late_subject tptp.pi_Rep tptp.produc257012921pi_Rep)) % 0.48/0.93 (declare-const tptp.perm_n1559866809ubject (-> tptp.list_P227219501e_name tptp.late_subject tptp.late_subject)) % 0.48/0.93 (declare-const tptp.y tptp.name) % 0.48/0.93 (declare-const tptp.cons_Late_freeRes (-> tptp.late_freeRes tptp.list_Late_freeRes tptp.list_Late_freeRes)) % 0.48/0.93 (declare-const tptp.subs (-> tptp.pi tptp.name tptp.name tptp.pi)) % 0.48/0.93 (declare-const tptp.rel tptp.set_Pr1834926343_pi_pi) % 0.48/0.93 (declare-const tptp.perm_n1812647369ubject (-> tptp.list_P227219501e_name tptp.list_Late_subject tptp.list_Late_subject)) % 0.48/0.93 (declare-const tptp.aa tptp.late_subject) % 0.48/0.93 (declare-const tptp.par (-> tptp.pi tptp.pi tptp.pi)) % 0.48/0.93 (declare-const tptp.perm_n190055296ubject (-> tptp.list_P227219501e_name (-> tptp.pi tptp.late_subject) tptp.pi tptp.late_subject)) % 0.48/0.93 (declare-const tptp.produc421428802t_name (-> tptp.product_unit tptp.name tptp.produc135724498t_name)) % 0.48/0.93 (declare-const tptp.fresh_543891186ion_pi (-> tptp.name (-> tptp.name tptp.noption_pi) Bool)) % 0.48/0.93 (declare-const tptp.perm_n359102898ect_pi (-> tptp.list_P227219501e_name tptp.produc140253050ect_pi tptp.produc140253050ect_pi)) % 0.48/0.93 (declare-const tptp.perm_n1160739829e_name (-> tptp.list_P227219501e_name tptp.list_P227219501e_name tptp.list_P227219501e_name)) % 0.48/0.93 (declare-const tptp.perm_n1841560599reeRes (-> tptp.list_P227219501e_name (-> tptp.pi_Rep tptp.late_freeRes) tptp.pi_Rep tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.x tptp.name) % 0.48/0.93 (declare-const tptp.perm_n1467004033pi_Rep (-> tptp.list_P227219501e_name tptp.produc257012921pi_Rep tptp.produc257012921pi_Rep)) % 0.48/0.93 (declare-const tptp.cons_name (-> tptp.name tptp.list_name tptp.list_name)) % 0.48/0.93 (declare-const tptp.c tptp.name) % 0.48/0.93 (declare-const tptp.perm_n1255502110_pi_pi (-> tptp.list_P227219501e_name tptp.produc1141751126_pi_pi tptp.produc1141751126_pi_pi)) % 0.48/0.93 (declare-const tptp.perm_name_name (-> tptp.list_P227219501e_name tptp.name tptp.name)) % 0.48/0.93 (declare-const tptp.if_name (-> Bool tptp.name tptp.name tptp.name)) % 0.48/0.93 (declare-const tptp.b tptp.name) % 0.48/0.93 (declare-const tptp.xPQ tptp.pi) % 0.48/0.93 (declare-const tptp.cons_pi (-> tptp.pi tptp.list_pi tptp.list_pi)) % 0.48/0.93 (declare-const tptp.perm_n698371375ubject (-> tptp.list_P227219501e_name (-> tptp.pi_Rep tptp.late_subject) tptp.pi_Rep tptp.late_subject)) % 0.48/0.93 (declare-const tptp.fresh_name_pi_Rep (-> tptp.name tptp.pi_Rep Bool)) % 0.48/0.93 (declare-const tptp.perm_n171497387ubject (-> tptp.list_P227219501e_name tptp.produc1359399907ubject tptp.produc1359399907ubject)) % 0.48/0.93 (declare-const tptp.cons_pi_Rep (-> tptp.pi_Rep tptp.list_pi_Rep tptp.list_pi_Rep)) % 0.48/0.93 (declare-const tptp.ya tptp.name) % 0.48/0.93 (declare-const tptp.perm_n258463228s_name (-> tptp.list_P227219501e_name tptp.produc2052722628s_name tptp.produc2052722628s_name)) % 0.48/0.93 (declare-const tptp.pq tptp.pi) % 0.48/0.93 (declare-const tptp.late_BoundOutputS (-> tptp.name tptp.late_subject)) % 0.48/0.93 (declare-const tptp.produc1570949143e_name (-> tptp.name tptp.name tptp.produc367475239e_name)) % 0.48/0.93 (declare-const tptp.perm_n336613537reeRes (-> tptp.list_P227219501e_name tptp.late_freeRes tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.member_pi_Rep (-> tptp.pi_Rep tptp.set_pi_Rep Bool)) % 0.48/0.93 (declare-const tptp.if_Late_freeRes (-> Bool tptp.late_freeRes tptp.late_freeRes tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.p tptp.pi) % 0.48/0.93 (declare-const tptp.perm_n1333244520reeRes (-> tptp.list_P227219501e_name (-> tptp.pi tptp.late_freeRes) tptp.pi tptp.late_freeRes)) % 0.48/0.93 (declare-const tptp.q2 tptp.pi) % 0.48/0.93 (declare-const tptp.ab tptp.name) % 0.48/0.93 (declare-const tptp.cons_name_noption_pi (-> (-> tptp.name tptp.noption_pi) tptp.list_name_noption_pi tptp.list_name_noption_pi)) % 0.48/0.93 (declare-const tptp.q tptp.pi) % 0.48/0.93 (declare-const tptp.perm_n808352945reeRes (-> tptp.list_P227219501e_name tptp.list_Late_freeRes tptp.list_Late_freeRes)) % 0.48/0.93 (declare-const tptp.nil_Pr743626285e_name tptp.list_P227219501e_name) % 0.48/0.93 (declare-const tptp.perm_n1174226579ubject (-> tptp.list_P227219501e_name tptp.produc214645451ubject tptp.produc214645451ubject)) % 0.48/0.93 (declare-const tptp.late_TauR tptp.late_freeRes) % 0.48/0.93 (declare-const tptp.perm_name_pi (-> tptp.list_P227219501e_name tptp.pi tptp.pi)) % 0.48/0.93 (declare-const tptp.member_name (-> tptp.name tptp.set_name Bool)) % 0.48/0.93 (declare-const tptp.if_pi (-> Bool tptp.pi tptp.pi tptp.pi)) % 0.48/0.93 (declare-const tptp.cons_P1213805021e_name (-> tptp.produc367475239e_name tptp.list_P227219501e_name tptp.list_P227219501e_name)) % 0.48/0.93 (declare-const tptp.late_InputS (-> tptp.name tptp.late_subject)) % 0.48/0.93 (declare-const tptp.p2 tptp.pi) % 0.48/0.93 (declare-const tptp.perm_name_pi_Rep (-> tptp.list_P227219501e_name tptp.pi_Rep tptp.pi_Rep)) % 0.48/0.93 (declare-const tptp.member_pi (-> tptp.pi tptp.set_pi Bool)) % 0.48/0.93 (declare-const tptp.if_pi_Rep (-> Bool tptp.pi_Rep tptp.pi_Rep tptp.pi_Rep)) % 0.48/0.93 (declare-const tptp.perm_name_set_pi_Rep (-> tptp.list_P227219501e_name tptp.set_pi_Rep tptp.set_pi_Rep)) % 0.48/0.93 (declare-const tptp.fresh_1135477378ion_pi (-> tptp.name tptp.list_name_noption_pi Bool)) % 0.48/0.93 (declare-const tptp.perm_name_set_name (-> tptp.list_P227219501e_name tptp.set_name tptp.set_name)) % 0.48/0.93 (declare-const tptp.fresh_81631222sidual (-> tptp.name tptp.late_residual Bool)) % 0.48/0.93 (declare-const tptp.perm_n697952036ct_Rep (-> tptp.list_P227219501e_name tptp.late_subject_Rep tptp.late_subject_Rep)) % 0.48/0.93 (declare-const tptp.perm_n890803237al_Rep (-> tptp.list_P227219501e_name tptp.late_residual_Rep tptp.late_residual_Rep)) % 0.48/0.93 (declare-const tptp.product_Unity tptp.product_unit) % 0.48/0.93 (declare-const tptp.produc1076565719t_unit (-> tptp.product_unit tptp.product_unit tptp.produc971140967t_unit)) % 0.48/0.93 (declare-const tptp.fresh_994967853t_unit (-> tptp.name tptp.produc971140967t_unit Bool)) % 0.48/0.93 (declare-const tptp.fresh_1826856600t_name (-> tptp.name tptp.produc135724498t_name Bool)) % 0.48/0.93 (declare-const tptp.produc1806354576nit_pi (-> tptp.product_unit tptp.pi tptp.produc738223008nit_pi)) % 0.48/0.93 (declare-const tptp.fresh_707692390nit_pi (-> tptp.name tptp.produc738223008nit_pi Bool)) % 0.48/0.93 (declare-const tptp.produc1785453612t_unit (-> tptp.name tptp.product_unit tptp.produc546891580t_unit)) % 0.48/0.93 (declare-const tptp.fresh_90540034t_unit (-> tptp.name tptp.produc546891580t_unit Bool)) % 0.48/0.93 (declare-const tptp.product_Pair_name_pi (-> tptp.name tptp.pi tptp.product_prod_name_pi)) % 0.48/0.93 (declare-const tptp.fresh_93646139ame_pi (-> tptp.name tptp.product_prod_name_pi Bool)) % 0.48/0.93 (declare-const tptp.produc1831798878t_unit (-> tptp.pi tptp.product_unit tptp.produc1028309998t_unit)) % 0.48/0.93 (declare-const tptp.fresh_997779380t_unit (-> tptp.name tptp.produc1028309998t_unit Bool)) % 0.48/0.93 (declare-const tptp.product_Pair_pi_name (-> tptp.pi tptp.name tptp.product_prod_pi_name)) % 0.48/0.93 (declare-const tptp.fresh_261416607i_name (-> tptp.name tptp.product_prod_pi_name Bool)) % 0.48/0.93 (declare-const tptp.fresh_441084397e_name (-> tptp.name tptp.produc367475239e_name Bool)) % 0.48/0.93 (declare-const tptp.fresh_1627595501_pi_pi (-> tptp.name tptp.product_prod_pi_pi Bool)) % 0.48/0.93 (declare-const tptp.produc235456326_pi_pi (-> tptp.name tptp.product_prod_pi_pi tptp.produc1141751126_pi_pi)) % 0.48/0.93 (declare-const tptp.fresh_1732817625t_unit (-> tptp.name tptp.list_Product_unit Bool)) % 0.48/0.93 (declare-const tptp.cons_Product_unit (-> tptp.product_unit tptp.list_Product_unit tptp.list_Product_unit)) % 0.48/0.93 (declare-const tptp.fresh_1958133282_pi_pi (-> tptp.name tptp.list_P431515740_pi_pi Bool)) % 0.48/0.93 (declare-const tptp.cons_P749510156_pi_pi (-> tptp.produc1141751126_pi_pi tptp.list_P431515740_pi_pi tptp.list_P431515740_pi_pi)) % 0.48/0.93 (declare-const tptp.produc1465345179ubject (-> tptp.late_subject tptp.late_subject tptp.produc1359399907ubject)) % 0.48/0.93 (declare-const tptp.produc242091907reeRes (-> tptp.late_subject tptp.late_freeRes tptp.produc355105483reeRes)) % 0.48/0.93 (declare-const tptp.perm_n1314686611reeRes (-> tptp.list_P227219501e_name tptp.produc355105483reeRes tptp.produc355105483reeRes)) % 0.48/0.93 (declare-const tptp.perm_n204483300t_name (-> tptp.list_P227219501e_name tptp.produc1998742700t_name tptp.produc1998742700t_name)) % 0.48/0.93 (declare-const tptp.produc320590723ubject (-> tptp.late_freeRes tptp.late_subject tptp.produc214645451ubject)) % 0.48/0.93 (declare-const tptp.produc1244821099reeRes (-> tptp.late_freeRes tptp.late_freeRes tptp.produc1357834675reeRes)) % 0.48/0.93 (declare-const tptp.perm_n169932155reeRes (-> tptp.list_P227219501e_name tptp.produc1357834675reeRes tptp.produc1357834675reeRes)) % 0.48/0.93 (declare-const tptp.produc216486617pi_Rep (-> tptp.late_freeRes tptp.pi_Rep tptp.produc1777919905pi_Rep)) % 0.48/0.93 (declare-const tptp.perm_n840427369pi_Rep (-> tptp.list_P227219501e_name tptp.produc1777919905pi_Rep tptp.produc1777919905pi_Rep)) % 0.48/0.93 (declare-const tptp.produc1701355766s_name (-> tptp.late_freeRes tptp.name tptp.produc2052722628s_name)) % 0.48/0.93 (declare-const tptp.produc1177552196Res_pi (-> tptp.late_freeRes tptp.pi tptp.produc992857746Res_pi)) % 0.48/0.93 (declare-const tptp.perm_n1211707594Res_pi (-> tptp.list_P227219501e_name tptp.produc992857746Res_pi tptp.produc992857746Res_pi)) % 0.48/0.93 (declare-const tptp.cons_Late_subject (-> tptp.late_subject tptp.list_Late_subject tptp.list_Late_subject)) % 0.48/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.48/0.93 (define tptp.eqvt_pi () (let ((_let_1 (@var "Rel2" tptp.set_Pr1834926343_pi_pi))) (let ((_let_2 (@var "X3" tptp.product_prod_pi_pi))) (let ((_let_3 (@var "Perm2" tptp.list_P227219501e_name))) (lambda (@list _let_1) (forall (@list _let_2 _let_3) (=> (_ (_ tptp.member558706512_pi_pi _let_2) _let_1) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.perm_n1415585007_pi_pi _let_3) _let_2)) _let_1)))))))) % 0.48/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 "P8" tptp.pi))) (let ((_let_4 (@var "Alpha3" tptp.late_freeRes))) (let ((_let_5 (_ tptp.late_FreeR _let_4))) (let ((_let_6 (@var "P7" tptp.pi))) (let ((_let_7 (_ tptp.late_transitions _let_6))) (let ((_let_8 (@list _let_3))) (let ((_let_9 (@var "Q5" tptp.pi))) (let ((_let_10 (_ tptp.late_transitions _let_9))) (let ((_let_11 (@var "X3" 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.48/0.93 (define @t1 () (_ (_ tptp.late_OutputR tptp.ab) tptp.x)) % 0.48/0.93 (define @t2 () (_ tptp.late_BoundOutputS tptp.ab)) % 0.48/0.93 (define @t3 () (_ tptp.par tptp.p)) % 0.48/0.93 (define @t4 () (_ @t3 tptp.q)) % 0.48/0.93 (define @t5 () (_ tptp.res tptp.x)) % 0.48/0.93 (define @t6 () (_ @t5 @t4)) % 0.48/0.93 (define @t7 () (_ tptp.fresh_name_pi tptp.ya)) % 0.48/0.93 (define @t8 () (_ tptp.fresh_name_pi tptp.y)) % 0.48/0.93 (define @t9 () (_ @t3 (_ @t5 tptp.q))) % 0.48/0.93 (define @t10 () (@var "P" tptp.pi)) % 0.48/0.93 (define @t11 () (@var "A" tptp.name)) % 0.48/0.93 (define @t12 () (@var "X" tptp.name)) % 0.48/0.93 (define @t13 () (_ tptp.produc1570949143e_name @t12)) % 0.48/0.93 (define @t14 () (_ tptp.res @t12)) % 0.48/0.93 (define @t15 () (_ (_ tptp.res @t11) @t10)) % 0.48/0.93 (define @t16 () (_ tptp.subs @t15)) % 0.48/0.93 (define @t17 () (@var "X" tptp.late_subject)) % 0.48/0.93 (define @t18 () (@var "B" tptp.name)) % 0.48/0.93 (define @t19 () (_ tptp.produc1570949143e_name @t11)) % 0.48/0.93 (define @t20 () (_ @t19 @t18)) % 0.48/0.93 (define @t21 () (_ tptp.cons_P1213805021e_name @t20)) % 0.48/0.93 (define @t22 () (_ @t21 tptp.nil_Pr743626285e_name)) % 0.48/0.93 (define @t23 () (_ tptp.perm_n1559866809ubject @t22)) % 0.48/0.93 (define @t24 () (_ @t23 @t17)) % 0.48/0.93 (define @t25 () (@list @t11 @t18 @t17)) % 0.48/0.93 (define @t26 () (@var "X" tptp.late_freeRes)) % 0.48/0.93 (define @t27 () (_ tptp.perm_n336613537reeRes @t22)) % 0.48/0.93 (define @t28 () (_ @t27 @t26)) % 0.48/0.93 (define @t29 () (@list @t11 @t18 @t26)) % 0.48/0.93 (define @t30 () (@var "X" tptp.pi_Rep)) % 0.48/0.93 (define @t31 () (_ tptp.perm_name_pi_Rep @t22)) % 0.48/0.93 (define @t32 () (_ @t31 @t30)) % 0.48/0.93 (define @t33 () (@list @t11 @t18 @t30)) % 0.48/0.93 (define @t34 () (_ tptp.perm_name_name @t22)) % 0.48/0.93 (define @t35 () (_ @t34 @t12)) % 0.48/0.93 (define @t36 () (@list @t11 @t18 @t12)) % 0.48/0.93 (define @t37 () (@var "X" tptp.pi)) % 0.48/0.93 (define @t38 () (_ tptp.perm_name_pi @t22)) % 0.48/0.93 (define @t39 () (_ @t38 @t37)) % 0.48/0.93 (define @t40 () (@list @t11 @t18 @t37)) % 0.48/0.93 (define @t41 () (_ (_ tptp.cons_P1213805021e_name (_ @t19 @t11)) tptp.nil_Pr743626285e_name)) % 0.48/0.93 (define @t42 () (_ (_ tptp.cons_P1213805021e_name (_ (_ tptp.produc1570949143e_name @t18) @t11)) tptp.nil_Pr743626285e_name)) % 0.48/0.93 (define @t43 () (_ (_ tptp.perm_n1559866809ubject @t42) @t17)) % 0.48/0.93 (define @t44 () (_ (_ tptp.perm_n336613537reeRes @t42) @t26)) % 0.48/0.93 (define @t45 () (_ (_ tptp.perm_name_pi_Rep @t42) @t30)) % 0.48/0.93 (define @t46 () (_ (_ tptp.perm_name_name @t42) @t12)) % 0.48/0.93 (define @t47 () (_ (_ tptp.perm_name_pi @t42) @t37)) % 0.48/0.93 (define @t48 () (@var "X1" tptp.pi)) % 0.48/0.93 (define @t49 () (@var "Pi" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t50 () (_ tptp.perm_name_pi @t49)) % 0.48/0.93 (define @t51 () (_ @t50 @t48)) % 0.48/0.93 (define @t52 () (@var "X2" tptp.pi)) % 0.48/0.93 (define @t53 () (_ @t50 @t52)) % 0.48/0.93 (define @t54 () (_ (_ tptp.par @t52) @t48)) % 0.48/0.93 (define @t55 () (@var "D" tptp.name)) % 0.48/0.93 (define @t56 () (@var "C" tptp.name)) % 0.48/0.93 (define @t57 () (@var "Q" tptp.pi)) % 0.48/0.93 (define @t58 () (_ tptp.subs @t10)) % 0.48/0.93 (define @t59 () (_ (_ @t58 @t56) @t55)) % 0.48/0.93 (define @t60 () (_ tptp.par @t10)) % 0.48/0.93 (define @t61 () (_ @t60 @t57)) % 0.48/0.93 (define @t62 () (_ @t14 @t10)) % 0.48/0.93 (define @t63 () (_ tptp.perm_name_pi_Rep tptp.nil_Pr743626285e_name)) % 0.48/0.93 (define @t64 () (@list @t12)) % 0.48/0.93 (define @t65 () (@list @t37)) % 0.48/0.93 (define @t66 () (_ @t58 @t11)) % 0.48/0.93 (define @t67 () (@var "Pi_Rep" tptp.pi_Rep)) % 0.48/0.93 (define @t68 () (_ tptp.fresh_name_pi @t11)) % 0.48/0.93 (define @t69 () (_ @t68 @t48)) % 0.48/0.93 (define @t70 () (@var "X1" tptp.name)) % 0.48/0.93 (define @t71 () (_ tptp.perm_name_name @t49)) % 0.48/0.93 (define @t72 () (_ @t71 @t70)) % 0.48/0.93 (define @t73 () (_ (_ tptp.res @t70) @t52)) % 0.48/0.93 (define @t74 () (_ tptp.fresh_717452603ubject @t11)) % 0.48/0.93 (define @t75 () (_ @t74 @t17)) % 0.48/0.93 (define @t76 () (_ tptp.fresh_1641682979reeRes @t11)) % 0.48/0.93 (define @t77 () (_ @t76 @t26)) % 0.48/0.93 (define @t78 () (_ tptp.fresh_name_pi_Rep @t11)) % 0.48/0.93 (define @t79 () (_ @t78 @t30)) % 0.48/0.93 (define @t80 () (@var "X" tptp.product_unit)) % 0.48/0.93 (define @t81 () (_ (_ tptp.perm_n1960409557t_unit @t22) @t80)) % 0.48/0.93 (define @t82 () (_ tptp.fresh_1143631827t_unit @t11)) % 0.48/0.93 (define @t83 () (_ @t82 @t80)) % 0.48/0.93 (define @t84 () (@var "X" tptp.produc1141751126_pi_pi)) % 0.48/0.93 (define @t85 () (_ (_ tptp.perm_n1255502110_pi_pi @t22) @t84)) % 0.48/0.93 (define @t86 () (_ tptp.fresh_1376661020_pi_pi @t11)) % 0.48/0.93 (define @t87 () (_ @t86 @t84)) % 0.48/0.93 (define @t88 () (_ tptp.fresh_name_name @t11)) % 0.48/0.93 (define @t89 () (_ @t88 @t12)) % 0.48/0.93 (define @t90 () (_ tptp.fresh_name_pi @t18)) % 0.48/0.93 (define @t91 () (_ @t68 @t37)) % 0.48/0.93 (define @t92 () (@var "X" (-> tptp.name tptp.noption_pi))) % 0.48/0.93 (define @t93 () (_ (_ tptp.perm_n1667196784ion_pi @t22) @t92)) % 0.48/0.93 (define @t94 () (_ tptp.fresh_543891186ion_pi @t11)) % 0.48/0.93 (define @t95 () (_ @t94 @t92)) % 0.48/0.93 (define @t96 () (_ tptp.perm_n1559866809ubject @t49)) % 0.48/0.93 (define @t97 () (_ @t96 @t17)) % 0.48/0.93 (define @t98 () (_ (_ tptp.fresh_922791155e_name @t11) @t49)) % 0.48/0.93 (define @t99 () (_ tptp.perm_n336613537reeRes @t49)) % 0.48/0.93 (define @t100 () (_ @t99 @t26)) % 0.48/0.93 (define @t101 () (_ tptp.perm_name_pi_Rep @t49)) % 0.48/0.93 (define @t102 () (_ @t101 @t30)) % 0.48/0.93 (define @t103 () (_ (_ tptp.perm_n1960409557t_unit @t49) @t80)) % 0.48/0.93 (define @t104 () (_ (_ tptp.perm_n1255502110_pi_pi @t49) @t84)) % 0.48/0.93 (define @t105 () (_ @t71 @t12)) % 0.48/0.93 (define @t106 () (_ @t50 @t37)) % 0.48/0.93 (define @t107 () (_ (_ tptp.perm_n1667196784ion_pi @t49) @t92)) % 0.48/0.93 (define @t108 () (@var "C2" tptp.name)) % 0.48/0.93 (define @t109 () (@list @t108)) % 0.48/0.93 (define @t110 () (_ @t71 @t11)) % 0.48/0.93 (define @t111 () (_ (_ tptp.fresh_717452603ubject @t110) @t97)) % 0.48/0.93 (define @t112 () (_ tptp.perm_name_o @t49)) % 0.48/0.93 (define @t113 () (@list @t49 @t11 @t17)) % 0.48/0.93 (define @t114 () (_ (_ tptp.fresh_1641682979reeRes @t110) @t100)) % 0.48/0.93 (define @t115 () (@list @t49 @t11 @t26)) % 0.48/0.93 (define @t116 () (_ (_ tptp.fresh_name_pi_Rep @t110) @t102)) % 0.48/0.93 (define @t117 () (@list @t49 @t11 @t30)) % 0.48/0.93 (define @t118 () (_ (_ tptp.fresh_1143631827t_unit @t110) @t103)) % 0.48/0.93 (define @t119 () (@list @t49 @t11 @t80)) % 0.48/0.93 (define @t120 () (_ (_ tptp.fresh_1376661020_pi_pi @t110) @t104)) % 0.48/0.93 (define @t121 () (@list @t49 @t11 @t84)) % 0.48/0.93 (define @t122 () (_ (_ tptp.fresh_name_name @t110) @t105)) % 0.48/0.93 (define @t123 () (@list @t49 @t11 @t12)) % 0.48/0.93 (define @t124 () (_ (_ tptp.fresh_name_pi @t110) @t106)) % 0.48/0.93 (define @t125 () (@list @t49 @t11 @t37)) % 0.48/0.93 (define @t126 () (_ (_ tptp.fresh_543891186ion_pi @t110) @t107)) % 0.48/0.93 (define @t127 () (@list @t49 @t11 @t92)) % 0.48/0.93 (define @t128 () (_ @t66 @t18)) % 0.48/0.93 (define @t129 () (not (= @t11 @t18))) % 0.48/0.93 (define @t130 () (= @t11 @t56)) % 0.48/0.93 (define @t131 () (not @t130)) % 0.48/0.93 (define @t132 () (_ @t68 @t10)) % 0.48/0.93 (define @t133 () (@var "A" tptp.product_prod_pi_pi)) % 0.48/0.93 (define @t134 () (@var "P" (-> tptp.product_prod_pi_pi Bool))) % 0.48/0.93 (define @t135 () (@var "A2" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.93 (define @t136 () (@var "X3" tptp.product_prod_pi_pi)) % 0.48/0.93 (define @t137 () (_ tptp.member558706512_pi_pi @t136)) % 0.48/0.93 (define @t138 () (_ tptp.res @t18)) % 0.48/0.93 (define @t139 () (_ @t138 @t128)) % 0.48/0.93 (define @t140 () (_ @t90 @t10)) % 0.48/0.93 (define @t141 () (@list @t18 @t10 @t11)) % 0.48/0.93 (define @t142 () (@var "P2" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t143 () (_ tptp.perm_name_name @t142)) % 0.48/0.93 (define @t144 () (_ tptp.perm_name_pi @t142)) % 0.48/0.93 (define @t145 () (@list @t11 @t18)) % 0.48/0.93 (define @t146 () (= @t18 @t56)) % 0.48/0.93 (define @t147 () (not @t146)) % 0.48/0.93 (define @t148 () (@list @t11 @t56 @t18)) % 0.48/0.93 (define @t149 () (_ tptp.fresh_717452603ubject @t56)) % 0.48/0.93 (define @t150 () (not (= @t56 @t11))) % 0.48/0.93 (define @t151 () (_ tptp.fresh_1641682979reeRes @t56)) % 0.48/0.93 (define @t152 () (_ tptp.fresh_name_pi_Rep @t56)) % 0.48/0.93 (define @t153 () (_ tptp.fresh_1143631827t_unit @t56)) % 0.48/0.93 (define @t154 () (_ tptp.fresh_1376661020_pi_pi @t56)) % 0.48/0.93 (define @t155 () (_ tptp.fresh_name_name @t56)) % 0.48/0.93 (define @t156 () (_ tptp.fresh_name_pi @t56)) % 0.48/0.93 (define @t157 () (_ tptp.fresh_543891186ion_pi @t56)) % 0.48/0.93 (define @t158 () (@var "Pi1" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t159 () (_ tptp.perm_n1559866809ubject @t158)) % 0.48/0.93 (define @t160 () (_ @t159 @t17)) % 0.48/0.93 (define @t161 () (@var "Pi2" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t162 () (_ (_ tptp.perm_n1160739829e_name @t158) @t161)) % 0.48/0.93 (define @t163 () (_ tptp.perm_n1559866809ubject @t161)) % 0.48/0.93 (define @t164 () (_ @t163 @t17)) % 0.48/0.93 (define @t165 () (_ tptp.perm_n336613537reeRes @t158)) % 0.48/0.93 (define @t166 () (_ @t165 @t26)) % 0.48/0.93 (define @t167 () (_ tptp.perm_n336613537reeRes @t161)) % 0.48/0.93 (define @t168 () (_ @t167 @t26)) % 0.48/0.93 (define @t169 () (_ tptp.perm_name_pi_Rep @t158)) % 0.48/0.93 (define @t170 () (_ @t169 @t30)) % 0.48/0.93 (define @t171 () (_ tptp.perm_name_pi_Rep @t161)) % 0.48/0.93 (define @t172 () (_ @t171 @t30)) % 0.48/0.93 (define @t173 () (_ tptp.perm_name_name @t158)) % 0.48/0.93 (define @t174 () (_ @t173 @t12)) % 0.48/0.93 (define @t175 () (_ tptp.perm_name_name @t161)) % 0.48/0.93 (define @t176 () (_ @t175 @t12)) % 0.48/0.93 (define @t177 () (_ tptp.perm_name_pi @t158)) % 0.48/0.93 (define @t178 () (_ @t177 @t37)) % 0.48/0.93 (define @t179 () (_ tptp.perm_name_pi @t161)) % 0.48/0.93 (define @t180 () (_ @t179 @t37)) % 0.48/0.93 (define @t181 () (_ (_ tptp.perm_n1160739829e_name @t161) @t158)) % 0.48/0.93 (define @t182 () (@var "Y" tptp.late_subject)) % 0.48/0.93 (define @t183 () (= @t17 @t182)) % 0.48/0.93 (define @t184 () (_ @t96 @t182)) % 0.48/0.93 (define @t185 () (= @t97 @t184)) % 0.48/0.93 (define @t186 () (@list @t49 @t17 @t182)) % 0.48/0.93 (define @t187 () (@var "Y" tptp.late_freeRes)) % 0.48/0.93 (define @t188 () (= @t26 @t187)) % 0.48/0.93 (define @t189 () (_ @t99 @t187)) % 0.48/0.93 (define @t190 () (= @t100 @t189)) % 0.48/0.93 (define @t191 () (@list @t49 @t26 @t187)) % 0.48/0.93 (define @t192 () (@var "Y" tptp.pi_Rep)) % 0.48/0.93 (define @t193 () (= @t30 @t192)) % 0.48/0.93 (define @t194 () (_ @t101 @t192)) % 0.48/0.93 (define @t195 () (= @t102 @t194)) % 0.48/0.93 (define @t196 () (@list @t49 @t30 @t192)) % 0.48/0.93 (define @t197 () (@var "Y" tptp.name)) % 0.48/0.93 (define @t198 () (= @t12 @t197)) % 0.48/0.93 (define @t199 () (_ @t71 @t197)) % 0.48/0.93 (define @t200 () (= @t105 @t199)) % 0.48/0.93 (define @t201 () (@list @t49 @t12 @t197)) % 0.48/0.93 (define @t202 () (@var "Y" tptp.pi)) % 0.48/0.93 (define @t203 () (= @t37 @t202)) % 0.48/0.93 (define @t204 () (_ @t50 @t202)) % 0.48/0.93 (define @t205 () (= @t106 @t204)) % 0.48/0.93 (define @t206 () (@list @t49 @t37 @t202)) % 0.48/0.93 (define @t207 () (@var "F" (-> tptp.late_subject tptp.late_subject))) % 0.48/0.93 (define @t208 () (@var "F" (-> tptp.late_freeRes tptp.late_subject))) % 0.48/0.93 (define @t209 () (@var "F" (-> tptp.pi_Rep tptp.late_subject))) % 0.48/0.93 (define @t210 () (@var "F" (-> tptp.name tptp.late_subject))) % 0.48/0.93 (define @t211 () (@var "F" (-> tptp.pi tptp.late_subject))) % 0.48/0.93 (define @t212 () (@var "F" (-> tptp.late_subject tptp.late_freeRes))) % 0.48/0.93 (define @t213 () (@var "F" (-> tptp.late_freeRes tptp.late_freeRes))) % 0.48/0.93 (define @t214 () (@var "F" (-> tptp.pi_Rep tptp.late_freeRes))) % 0.48/0.93 (define @t215 () (@var "F" (-> tptp.name tptp.late_freeRes))) % 0.48/0.93 (define @t216 () (@var "F" (-> tptp.pi tptp.late_freeRes))) % 0.48/0.93 (define @t217 () (@var "X4" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.93 (define @t218 () (@var "X" tptp.product_prod_pi_pi)) % 0.48/0.93 (define @t219 () (@var "X4" tptp.set_Late_subject)) % 0.48/0.93 (define @t220 () (@var "X4" tptp.set_Late_freeRes)) % 0.48/0.93 (define @t221 () (@var "X4" tptp.set_pi_Rep)) % 0.48/0.93 (define @t222 () (@var "X4" tptp.set_name)) % 0.48/0.93 (define @t223 () (@var "X4" tptp.set_pi)) % 0.48/0.93 (define @t224 () (@var "Y1" tptp.pi)) % 0.48/0.93 (define @t225 () (= @t48 @t224)) % 0.48/0.93 (define @t226 () (@var "Y2" tptp.pi)) % 0.48/0.93 (define @t227 () (_ @t156 @t10)) % 0.48/0.93 (define @t228 () (@var "Pi3" tptp.pi)) % 0.48/0.93 (define @t229 () (@var "Name" tptp.name)) % 0.48/0.93 (define @t230 () (_ (_ tptp.res @t229) @t228)) % 0.48/0.93 (define @t231 () (@var "Pi2" tptp.pi)) % 0.48/0.93 (define @t232 () (@var "Pi1" tptp.pi)) % 0.48/0.93 (define @t233 () (@var "Q2" tptp.pi)) % 0.48/0.93 (define @t234 () (_ (_ tptp.subs @t233) @t12)) % 0.48/0.93 (define @t235 () (@var "P3" tptp.pi)) % 0.48/0.93 (define @t236 () (_ tptp.par @t235)) % 0.48/0.93 (define @t237 () (_ tptp.res @t197)) % 0.48/0.93 (define @t238 () (_ tptp.late_FreeR tptp.late_TauR)) % 0.48/0.93 (define @t239 () (_ tptp.late_transitions @t61)) % 0.48/0.93 (define @t240 () (_ @t239 (_ @t238 (_ @t237 (_ @t236 (_ @t234 @t197)))))) % 0.48/0.93 (define @t241 () (not @t198)) % 0.48/0.93 (define @t242 () (_ tptp.fresh_name_pi @t197)) % 0.48/0.93 (define @t243 () (not (= @t197 @t11))) % 0.48/0.93 (define @t244 () (_ tptp.fresh_name_pi @t12)) % 0.48/0.93 (define @t245 () (_ @t244 @t235)) % 0.48/0.93 (define @t246 () (not (= @t12 @t11))) % 0.48/0.93 (define @t247 () (_ @t242 @t57)) % 0.48/0.93 (define @t248 () (_ @t242 @t10)) % 0.48/0.93 (define @t249 () (_ @t244 @t57)) % 0.48/0.93 (define @t250 () (_ @t244 @t10)) % 0.48/0.93 (define @t251 () (_ tptp.late_InputS @t11)) % 0.48/0.93 (define @t252 () (_ (_ tptp.late_BoundR @t251) @t12)) % 0.48/0.93 (define @t253 () (_ tptp.late_transitions @t57)) % 0.48/0.93 (define @t254 () (_ @t253 (_ @t252 @t233))) % 0.48/0.93 (define @t255 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t11))) % 0.48/0.93 (define @t256 () (_ @t255 @t197)) % 0.48/0.93 (define @t257 () (_ tptp.late_transitions @t10)) % 0.48/0.93 (define @t258 () (_ @t257 (_ @t256 @t235))) % 0.48/0.93 (define @t259 () (@list @t10 @t11 @t197 @t235 @t57 @t12 @t233)) % 0.48/0.93 (define @t260 () (_ (_ tptp.subs @t235) @t12)) % 0.48/0.93 (define @t261 () (_ @t239 (_ @t238 (_ @t237 (_ (_ tptp.par (_ @t260 @t197)) @t233))))) % 0.48/0.93 (define @t262 () (_ @t242 @t235)) % 0.48/0.93 (define @t263 () (_ @t244 @t233)) % 0.48/0.93 (define @t264 () (_ @t253 (_ @t256 @t233))) % 0.48/0.93 (define @t265 () (_ @t257 (_ @t252 @t235))) % 0.48/0.93 (define @t266 () (@list @t10 @t11 @t12 @t235 @t57 @t197 @t233)) % 0.48/0.93 (define @t267 () (_ @t239 (_ @t238 (_ @t236 (_ @t234 @t18))))) % 0.48/0.93 (define @t268 () (not (= @t12 @t18))) % 0.48/0.93 (define @t269 () (_ tptp.late_FreeR (_ (_ tptp.late_OutputR @t11) @t18))) % 0.48/0.93 (define @t270 () (_ @t257 (_ @t269 @t235))) % 0.48/0.93 (define @t271 () (@list @t10 @t11 @t18 @t235 @t57 @t12 @t233)) % 0.48/0.93 (define @t272 () (_ @t239 (_ @t238 (_ (_ tptp.par (_ @t260 @t18)) @t233)))) % 0.48/0.93 (define @t273 () (_ @t253 (_ @t269 @t233))) % 0.48/0.93 (define @t274 () (@list @t10 @t11 @t12 @t235 @t57 @t18 @t233)) % 0.48/0.93 (define @t275 () (@var "X5" tptp.name)) % 0.48/0.93 (define @t276 () (@var "A" tptp.late_subject)) % 0.48/0.93 (define @t277 () (_ tptp.late_BoundR @t276)) % 0.48/0.93 (define @t278 () (_ @t277 @t12)) % 0.48/0.93 (define @t279 () (@var "FreeRes_Rep" tptp.late_freeRes_Rep)) % 0.48/0.93 (define @t280 () (@var "Subject_Rep" tptp.late_subject_Rep)) % 0.48/0.93 (define @t281 () (@var "Residual_Rep" tptp.late_residual_Rep)) % 0.48/0.93 (define @t282 () (_ @t88 @t70)) % 0.48/0.93 (define @t283 () (@var "X2" tptp.name)) % 0.48/0.93 (define @t284 () (_ (_ tptp.late_OutputR @t283) @t70)) % 0.48/0.93 (define @t285 () (@var "Y1" tptp.name)) % 0.48/0.93 (define @t286 () (= @t70 @t285)) % 0.48/0.93 (define @t287 () (@var "Y2" tptp.name)) % 0.48/0.93 (define @t288 () (= @t283 @t287)) % 0.48/0.93 (define @t289 () (_ tptp.late_BoundOutputS @t70)) % 0.48/0.93 (define @t290 () (@list @t70 @t285)) % 0.48/0.93 (define @t291 () (@list @t11)) % 0.48/0.93 (define @t292 () (@var "X2" tptp.late_freeRes)) % 0.48/0.93 (define @t293 () (_ (_ tptp.late_FreeR @t292) @t48)) % 0.48/0.93 (define @t294 () (_ tptp.perm_n414416632sidual @t49)) % 0.48/0.93 (define @t295 () (_ tptp.late_InputS @t70)) % 0.48/0.93 (define @t296 () (@list @t49 @t70)) % 0.48/0.93 (define @t297 () (@list @t11 @t70)) % 0.48/0.93 (define @t298 () (@var "X32" tptp.late_subject)) % 0.48/0.93 (define @t299 () (@var "Rs" tptp.late_residual)) % 0.48/0.93 (define @t300 () (@var "XP" tptp.pi)) % 0.48/0.93 (define @t301 () (@var "F2" (-> tptp.pi Bool))) % 0.48/0.93 (define @t302 () (@var "P4" tptp.pi)) % 0.48/0.93 (define @t303 () (@var "Alpha" tptp.late_freeRes)) % 0.48/0.93 (define @t304 () (_ tptp.fresh_1641682979reeRes @t12)) % 0.48/0.93 (define @t305 () (_ tptp.late_FreeR @t303)) % 0.48/0.93 (define @t306 () (_ @t257 (_ @t305 @t302))) % 0.48/0.93 (define @t307 () (@list @t302)) % 0.48/0.93 (define @t308 () (_ tptp.late_transitions @t62)) % 0.48/0.93 (define @t309 () (@var "Alpha2" tptp.late_freeRes)) % 0.48/0.93 (define @t310 () (@var "Y3" tptp.name)) % 0.48/0.93 (define @t311 () (_ tptp.late_FreeR @t309)) % 0.48/0.93 (define @t312 () (@var "P5" tptp.pi)) % 0.48/0.93 (define @t313 () (_ tptp.late_transitions @t312)) % 0.48/0.93 (define @t314 () (=> (_ @t313 (_ @t311 @t302)) (not (_ (_ tptp.fresh_1641682979reeRes @t310) @t309)))) % 0.48/0.93 (define @t315 () (_ tptp.res @t310)) % 0.48/0.93 (define @t316 () (_ @t315 @t302)) % 0.48/0.93 (define @t317 () (_ @t311 @t316)) % 0.48/0.93 (define @t318 () (_ @t305 @t235)) % 0.48/0.93 (define @t319 () (_ @t315 @t312)) % 0.48/0.93 (define @t320 () (= @t62 @t319)) % 0.48/0.93 (define @t321 () (@list @t312 @t309 @t302 @t310)) % 0.48/0.93 (define @t322 () (_ @t237 @t235)) % 0.48/0.93 (define @t323 () (_ tptp.late_transitions (_ @t237 @t10))) % 0.48/0.93 (define @t324 () (_ (_ tptp.fresh_1641682979reeRes @t197) @t303)) % 0.48/0.93 (define @t325 () (_ @t257 @t318)) % 0.48/0.93 (define @t326 () (@list @t10 @t303 @t235 @t197)) % 0.48/0.93 (define @t327 () (_ @t323 (_ @t278 @t322))) % 0.48/0.93 (define @t328 () (not (= @t197 @t12))) % 0.48/0.93 (define @t329 () (_ (_ tptp.fresh_717452603ubject @t197) @t276)) % 0.48/0.93 (define @t330 () (_ @t257 (_ @t278 @t235))) % 0.48/0.93 (define @t331 () (@list @t10 @t276 @t12 @t235 @t197)) % 0.48/0.93 (define @t332 () (_ tptp.fresh_717452603ubject @t12)) % 0.48/0.93 (define @t333 () (_ @t332 @t276)) % 0.48/0.93 (define @t334 () (@var "A3" tptp.late_subject)) % 0.48/0.93 (define @t335 () (@var "X6" tptp.name)) % 0.48/0.93 (define @t336 () (_ (_ tptp.fresh_717452603ubject @t335) @t334)) % 0.48/0.93 (define @t337 () (not @t336)) % 0.48/0.93 (define @t338 () (@var "Q3" tptp.pi)) % 0.48/0.93 (define @t339 () (_ tptp.fresh_name_pi @t335)) % 0.48/0.93 (define @t340 () (_ @t339 @t312)) % 0.48/0.93 (define @t341 () (=> @t340 (=> (_ @t339 @t338) @t337))) % 0.48/0.93 (define @t342 () (@var "Q4" tptp.pi)) % 0.48/0.93 (define @t343 () (_ tptp.late_BoundR @t334)) % 0.48/0.93 (define @t344 () (_ @t343 @t335)) % 0.48/0.93 (define @t345 () (_ @t344 @t342)) % 0.48/0.93 (define @t346 () (_ tptp.par @t312)) % 0.48/0.93 (define @t347 () (@var "B" tptp.late_subject)) % 0.48/0.93 (define @t348 () (_ (_ tptp.late_BoundR @t347) @t197)) % 0.48/0.93 (define @t349 () (_ @t348 @t235)) % 0.48/0.93 (define @t350 () (= @t61 (_ @t346 @t338))) % 0.48/0.93 (define @t351 () (_ @t313 (_ @t344 @t302))) % 0.48/0.93 (define @t352 () (_ tptp.par @t302)) % 0.48/0.93 (define @t353 () (_ @t236 @t57)) % 0.48/0.93 (define @t354 () (_ @t239 (_ @t278 @t353))) % 0.48/0.93 (define @t355 () (@list @t10 @t276 @t12 @t235 @t57)) % 0.48/0.93 (define @t356 () (_ @t60 @t233)) % 0.48/0.93 (define @t357 () (_ @t239 (_ @t278 @t356))) % 0.48/0.93 (define @t358 () (_ @t253 (_ @t278 @t233))) % 0.48/0.93 (define @t359 () (@list @t57 @t276 @t12 @t233 @t10)) % 0.48/0.93 (define @t360 () (=> @t351 (=> (_ (_ tptp.fresh_717452603ubject @t310) @t334) (=> (not (= @t310 @t335)) (=> @t340 @t337))))) % 0.48/0.93 (define @t361 () (_ @t344 @t316)) % 0.48/0.93 (define @t362 () (@list @t312 @t334 @t335 @t302 @t310)) % 0.48/0.93 (define @t363 () (@var "B2" tptp.name)) % 0.48/0.93 (define @t364 () (@var "A3" tptp.name)) % 0.48/0.93 (define @t365 () (_ tptp.late_OutputR @t364)) % 0.48/0.93 (define @t366 () (=> (_ @t313 (_ (_ tptp.late_FreeR (_ @t365 @t363)) @t302)) (= @t364 @t363))) % 0.48/0.93 (define @t367 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t364))) % 0.48/0.93 (define @t368 () (_ (_ @t367 @t363) @t302)) % 0.48/0.93 (define @t369 () (_ (_ tptp.res @t363) @t312)) % 0.48/0.93 (define @t370 () (@list @t312 @t364 @t363)) % 0.48/0.93 (define @t371 () (@var "Y2" tptp.late_freeRes)) % 0.48/0.93 (define @t372 () (@var "Y4" tptp.name)) % 0.48/0.93 (define @t373 () (_ (_ @t277 @t372) @t235)) % 0.48/0.93 (define @t374 () (_ (_ tptp.res @t275) @t10)) % 0.48/0.93 (define @t375 () (@var "FreeRes" tptp.late_freeRes)) % 0.48/0.93 (define @t376 () (@var "Pi" tptp.pi)) % 0.48/0.93 (define @t377 () (@var "Name2" tptp.name)) % 0.48/0.93 (define @t378 () (@var "Subject" tptp.late_subject)) % 0.48/0.93 (define @t379 () (@var "Residual" tptp.late_residual)) % 0.48/0.93 (define @t380 () (@var "P" (-> tptp.late_residual Bool))) % 0.48/0.93 (define @t381 () (@var "Pi4" tptp.pi)) % 0.48/0.93 (define @t382 () (@var "FreeRes2" tptp.late_freeRes)) % 0.48/0.93 (define @t383 () (_ (_ tptp.late_FreeR @t382) @t381)) % 0.48/0.93 (define @t384 () (@var "Name3" tptp.name)) % 0.48/0.93 (define @t385 () (@var "Subject2" tptp.late_subject)) % 0.48/0.93 (define @t386 () (_ (_ (_ tptp.late_BoundR @t385) @t384) @t381)) % 0.48/0.93 (define @t387 () (@var "X2" tptp.late_residual)) % 0.48/0.93 (define @t388 () (@var "FreeRes3" tptp.late_freeRes)) % 0.48/0.93 (define @t389 () (@var "P" (-> tptp.late_freeRes Bool))) % 0.48/0.93 (define @t390 () (@var "Name22" tptp.name)) % 0.48/0.93 (define @t391 () (@var "Name1" tptp.name)) % 0.48/0.93 (define @t392 () (@var "Name23" tptp.name)) % 0.48/0.93 (define @t393 () (@var "Name12" tptp.name)) % 0.48/0.93 (define @t394 () (_ (_ tptp.late_OutputR @t393) @t392)) % 0.48/0.93 (define @t395 () (not (= @t394 tptp.late_TauR))) % 0.48/0.93 (define @t396 () (@list @t393 @t392)) % 0.48/0.93 (define @t397 () (forall @t396 @t395)) % 0.48/0.93 (define @t398 () (@var "P" (-> tptp.late_subject Bool))) % 0.48/0.93 (define @t399 () (@list @t384)) % 0.48/0.93 (define @t400 () (@var "YP" tptp.pi)) % 0.48/0.93 (define @t401 () (@var "F2" (-> tptp.late_subject tptp.pi Bool))) % 0.48/0.93 (define @t402 () (_ @t401 @t276)) % 0.48/0.93 (define @t403 () (_ @t257 (_ @t278 @t302))) % 0.48/0.93 (define @t404 () (_ @t13 @t197)) % 0.48/0.93 (define @t405 () (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name @t404) tptp.nil_Pr743626285e_name))) % 0.48/0.93 (define @t406 () (_ tptp.late_BoundOutputS @t363)) % 0.48/0.93 (define @t407 () (_ @t253 (_ @t305 @t233))) % 0.48/0.93 (define @t408 () (@var "Z" tptp.product_unit)) % 0.48/0.93 (define @t409 () (@var "P" (-> tptp.product_unit tptp.late_residual Bool))) % 0.48/0.93 (define @t410 () (@var "Z2" tptp.product_unit)) % 0.48/0.93 (define @t411 () (_ @t409 @t410)) % 0.48/0.93 (define @t412 () (_ (_ tptp.fresh_717452603ubject @t384) @t385)) % 0.48/0.93 (define @t413 () (@var "Z" tptp.produc1141751126_pi_pi)) % 0.48/0.93 (define @t414 () (@var "P" (-> tptp.produc1141751126_pi_pi tptp.late_residual Bool))) % 0.48/0.93 (define @t415 () (@var "Z2" tptp.produc1141751126_pi_pi)) % 0.48/0.93 (define @t416 () (_ @t414 @t415)) % 0.48/0.93 (define @t417 () (@var "Z" tptp.name)) % 0.48/0.93 (define @t418 () (@var "P" (-> tptp.name tptp.late_residual Bool))) % 0.48/0.93 (define @t419 () (@var "Z2" tptp.name)) % 0.48/0.93 (define @t420 () (_ @t418 @t419)) % 0.48/0.93 (define @t421 () (@var "Z" tptp.pi)) % 0.48/0.93 (define @t422 () (@var "P" (-> tptp.pi tptp.late_residual Bool))) % 0.48/0.93 (define @t423 () (@var "Z2" tptp.pi)) % 0.48/0.93 (define @t424 () (_ @t422 @t423)) % 0.48/0.93 (define @t425 () (@var "PQ" tptp.pi)) % 0.48/0.93 (define @t426 () (@var "Prop" (-> tptp.pi Bool))) % 0.48/0.93 (define @t427 () (@var "Rel" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.93 (define @t428 () (@var "Perm" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t429 () (_ tptp.perm_name_name @t428)) % 0.48/0.93 (define @t430 () (_ @t429 @t12)) % 0.48/0.93 (define @t431 () (_ tptp.perm_name_pi @t428)) % 0.48/0.93 (define @t432 () (_ @t431 @t57)) % 0.48/0.93 (define @t433 () (_ @t431 @t10)) % 0.48/0.93 (define @t434 () (_ (_ tptp.strong2129052853vative @t433) @t432)) % 0.48/0.93 (define @t435 () (_ tptp.eqvt_pi @t427)) % 0.48/0.93 (define @t436 () (_ (_ (_ (_ (_ tptp.strong2129052853vative @t10) @t57) @t276) @t12) @t427)) % 0.48/0.93 (define @t437 () (@list @t10 @t57 @t276 @t12 @t427 @t428)) % 0.48/0.93 (define @t438 () (_ tptp.perm_n1559866809ubject @t428)) % 0.48/0.93 (define @t439 () (@var "Y" tptp.product_unit)) % 0.48/0.93 (define @t440 () (_ @t82 @t439)) % 0.48/0.93 (define @t441 () (_ @t88 @t197)) % 0.48/0.93 (define @t442 () (_ @t68 @t202)) % 0.48/0.93 (define @t443 () (_ (_ tptp.fresh_441084397e_name @t11) @t404)) % 0.48/0.93 (define @t444 () (@list @t11 @t12 @t197)) % 0.48/0.93 (define @t445 () (_ tptp.fresh_1627595501_pi_pi @t11)) % 0.48/0.93 (define @t446 () (_ @t445 (_ (_ tptp.product_Pair_pi_pi @t37) @t202))) % 0.48/0.93 (define @t447 () (@list @t11 @t37 @t202)) % 0.48/0.93 (define @t448 () (@var "Y" tptp.product_prod_pi_pi)) % 0.48/0.93 (define @t449 () (_ @t445 @t448)) % 0.48/0.93 (define @t450 () (_ @t86 (_ (_ tptp.produc235456326_pi_pi @t12) @t448))) % 0.48/0.93 (define @t451 () (@list @t11 @t12 @t448)) % 0.48/0.93 (define @t452 () (@var "S" tptp.pi)) % 0.48/0.93 (define @t453 () (@var "R" tptp.pi)) % 0.48/0.93 (define @t454 () (_ tptp.par @t453)) % 0.48/0.93 (define @t455 () (_ @t454 @t452)) % 0.48/0.93 (define @t456 () (_ @t454 (_ @t237 @t452))) % 0.48/0.93 (define @t457 () (_ @t242 @t453)) % 0.48/0.93 (define @t458 () (_ tptp.res @t417)) % 0.48/0.93 (define @t459 () (@var "Xs" tptp.list_Product_unit)) % 0.48/0.93 (define @t460 () (_ tptp.fresh_1732817625t_unit @t11)) % 0.48/0.93 (define @t461 () (@var "Xs" tptp.list_P431515740_pi_pi)) % 0.48/0.93 (define @t462 () (_ tptp.fresh_1958133282_pi_pi @t11)) % 0.48/0.93 (define @t463 () (@var "Xs" tptp.list_name)) % 0.48/0.93 (define @t464 () (_ tptp.fresh_name_list_name @t11)) % 0.48/0.93 (define @t465 () (_ (_ tptp.cons_name @t12) @t463)) % 0.48/0.93 (define @t466 () (@var "Xs" tptp.list_pi)) % 0.48/0.93 (define @t467 () (_ tptp.fresh_name_list_pi @t11)) % 0.48/0.93 (define @t468 () (_ (_ tptp.cons_pi @t37) @t466)) % 0.48/0.93 (define @t469 () (@var "Xs" tptp.list_name_noption_pi)) % 0.48/0.93 (define @t470 () (_ tptp.fresh_1135477378ion_pi @t11)) % 0.48/0.93 (define @t471 () (@var "P" (-> tptp.list_P227219501e_name Bool))) % 0.48/0.93 (define @t472 () (@var "X_1" tptp.list_P227219501e_name)) % 0.48/0.93 (define @t473 () (@var "C" Bool)) % 0.48/0.93 (define @t474 () (_ @t96 (_ (_ (_ tptp.if_Late_subject @t473) @t17) @t182))) % 0.48/0.93 (define @t475 () (not @t473)) % 0.48/0.93 (define @t476 () (_ @t99 (_ (_ (_ tptp.if_Late_freeRes @t473) @t26) @t187))) % 0.48/0.93 (define @t477 () (_ @t101 (_ (_ (_ tptp.if_pi_Rep @t473) @t30) @t192))) % 0.48/0.93 (define @t478 () (_ @t71 (_ (_ (_ tptp.if_name @t473) @t12) @t197))) % 0.48/0.93 (define @t479 () (_ @t50 (_ (_ (_ tptp.if_pi @t473) @t37) @t202))) % 0.48/0.93 (define @t480 () (@var "C22" tptp.late_subject)) % 0.48/0.93 (define @t481 () (@var "C1" tptp.late_subject)) % 0.48/0.93 (define @t482 () (@var "B" Bool)) % 0.48/0.93 (define @t483 () (_ @t96 (_ (_ (_ tptp.if_Late_subject @t482) @t481) @t480))) % 0.48/0.93 (define @t484 () (_ @t112 @t482)) % 0.48/0.93 (define @t485 () (not @t484)) % 0.48/0.93 (define @t486 () (@var "C22" tptp.late_freeRes)) % 0.48/0.93 (define @t487 () (@var "C1" tptp.late_freeRes)) % 0.48/0.93 (define @t488 () (_ @t99 (_ (_ (_ tptp.if_Late_freeRes @t482) @t487) @t486))) % 0.48/0.93 (define @t489 () (@var "C22" tptp.pi_Rep)) % 0.48/0.93 (define @t490 () (@var "C1" tptp.pi_Rep)) % 0.48/0.93 (define @t491 () (_ @t101 (_ (_ (_ tptp.if_pi_Rep @t482) @t490) @t489))) % 0.48/0.93 (define @t492 () (@var "C22" tptp.name)) % 0.48/0.93 (define @t493 () (@var "C1" tptp.name)) % 0.48/0.93 (define @t494 () (_ @t71 (_ (_ (_ tptp.if_name @t482) @t493) @t492))) % 0.48/0.93 (define @t495 () (@var "C22" tptp.pi)) % 0.48/0.93 (define @t496 () (@var "C1" tptp.pi)) % 0.48/0.93 (define @t497 () (_ @t50 (_ (_ (_ tptp.if_pi @t482) @t496) @t495))) % 0.48/0.93 (define @t498 () (@var "Xs" tptp.list_Late_subject)) % 0.48/0.93 (define @t499 () (_ tptp.perm_n1812647369ubject @t49)) % 0.48/0.93 (define @t500 () (@var "Xs" tptp.list_Late_freeRes)) % 0.48/0.93 (define @t501 () (_ tptp.perm_n808352945reeRes @t49)) % 0.48/0.93 (define @t502 () (@var "Xs" tptp.list_pi_Rep)) % 0.48/0.93 (define @t503 () (_ tptp.perm_n729617823pi_Rep @t49)) % 0.48/0.93 (define @t504 () (_ tptp.perm_name_list_name @t49)) % 0.48/0.93 (define @t505 () (_ tptp.perm_name_list_pi @t49)) % 0.48/0.93 (define @t506 () (_ (_ tptp.strong743114133lation @t10) @t427)) % 0.48/0.93 (define @t507 () (_ @t14 @t342)) % 0.48/0.93 (define @t508 () (@var "P6" tptp.pi)) % 0.48/0.93 (define @t509 () (_ tptp.product_Pair_pi_pi @t508)) % 0.48/0.93 (define @t510 () (_ @t257 (_ @t311 @t508))) % 0.48/0.93 (define @t511 () (@list @t508)) % 0.48/0.93 (define @t512 () (_ @t253 (_ @t311 @t342))) % 0.48/0.93 (define @t513 () (=> (forall (@list @t342 @t309) (=> @t512 (=> (_ @t304 @t309) (exists @t511 (and @t510 (_ (_ tptp.member558706512_pi_pi (_ @t509 @t507)) @t427)))))) (_ @t506 (_ @t14 @t57)))) % 0.48/0.93 (define @t514 () (_ tptp.strong2129052853vative @t508)) % 0.48/0.93 (define @t515 () (_ @t343 @t310)) % 0.48/0.93 (define @t516 () (_ @t257 (_ @t515 @t508))) % 0.48/0.93 (define @t517 () (exists @t511 (and @t516 (_ (_ (_ (_ @t514 @t507) @t334) @t310) @t427)))) % 0.48/0.93 (define @t518 () (@var "C3" tptp.product_unit)) % 0.48/0.93 (define @t519 () (not (= @t12 @t310))) % 0.48/0.93 (define @t520 () (_ @t332 @t334)) % 0.48/0.93 (define @t521 () (_ @t253 (_ @t515 @t342))) % 0.48/0.93 (define @t522 () (@list @t342 @t334 @t310)) % 0.48/0.93 (define @t523 () (_ (_ tptp.member558706512_pi_pi (_ @t509 @t342)) @t427)) % 0.48/0.93 (define @t524 () (forall (@list @t342 @t364) (=> (_ @t253 (_ (_ tptp.late_FreeR (_ @t365 @t12)) @t342)) (=> (not (= @t364 @t12)) (exists @t511 (and (_ @t257 (_ (_ @t367 @t12) @t508)) @t523)))))) % 0.48/0.93 (define @t525 () (@var "C3" tptp.produc1141751126_pi_pi)) % 0.48/0.93 (define @t526 () (@var "C3" tptp.name)) % 0.48/0.93 (define @t527 () (@var "C3" tptp.pi)) % 0.48/0.93 (define @t528 () (_ tptp.fresh_name_pi @t310)) % 0.48/0.93 (define @t529 () (_ @t506 @t57)) % 0.48/0.93 (define @t530 () (=> (forall (@list @t309 @t342) (=> @t512 (exists @t511 (and @t510 @t523)))) @t529)) % 0.48/0.93 (define @t531 () (_ (_ @t514 @t342) @t334)) % 0.48/0.93 (define @t532 () (exists @t511 (and (_ @t257 (_ @t344 @t508)) (_ (_ @t531 @t335) @t427)))) % 0.48/0.93 (define @t533 () (_ @t339 @t57)) % 0.48/0.93 (define @t534 () (_ @t339 @t10)) % 0.48/0.93 (define @t535 () (_ @t253 @t345)) % 0.48/0.93 (define @t536 () (@list @t334 @t335 @t342)) % 0.48/0.93 (define @t537 () (@var "Rel" tptp.set_Pr806375235ubject)) % 0.48/0.93 (define @t538 () (@var "Q" tptp.late_subject)) % 0.48/0.93 (define @t539 () (@var "P" tptp.late_subject)) % 0.48/0.93 (define @t540 () (_ (_ tptp.member1586545036ubject (_ (_ tptp.produc1465345179ubject (_ @t438 @t539)) (_ @t438 @t538))) @t537)) % 0.48/0.93 (define @t541 () (_ (_ tptp.member1586545036ubject (_ (_ tptp.produc1465345179ubject @t539) @t538)) @t537)) % 0.48/0.93 (define @t542 () (_ tptp.eqvt_Late_subject @t537)) % 0.48/0.93 (define @t543 () (@var "Rel" tptp.set_Pr1780909331reeRes)) % 0.48/0.93 (define @t544 () (@var "Q" tptp.late_freeRes)) % 0.48/0.93 (define @t545 () (_ tptp.perm_n336613537reeRes @t428)) % 0.48/0.93 (define @t546 () (@var "P" tptp.late_freeRes)) % 0.48/0.93 (define @t547 () (_ (_ tptp.member1584979804reeRes (_ (_ tptp.produc1244821099reeRes (_ @t545 @t546)) (_ @t545 @t544))) @t543)) % 0.48/0.93 (define @t548 () (_ (_ tptp.member1584979804reeRes (_ (_ tptp.produc1244821099reeRes @t546) @t544)) @t543)) % 0.48/0.93 (define @t549 () (_ tptp.eqvt_Late_freeRes @t543)) % 0.48/0.93 (define @t550 () (@var "Rel" tptp.set_Pr1131282415pi_Rep)) % 0.48/0.93 (define @t551 () (@var "Q" tptp.pi_Rep)) % 0.48/0.93 (define @t552 () (_ tptp.perm_name_pi_Rep @t428)) % 0.48/0.93 (define @t553 () (@var "P" tptp.pi_Rep)) % 0.48/0.93 (define @t554 () (_ (_ tptp.member1671908408pi_Rep (_ (_ tptp.produc784048711pi_Rep (_ @t552 @t553)) (_ @t552 @t551))) @t550)) % 0.48/0.93 (define @t555 () (_ (_ tptp.member1671908408pi_Rep (_ (_ tptp.produc784048711pi_Rep @t553) @t551)) @t550)) % 0.48/0.93 (define @t556 () (_ tptp.eqvt_pi_Rep @t550)) % 0.48/0.94 (define @t557 () (@var "Rel" tptp.set_Pr443758855e_name)) % 0.48/0.94 (define @t558 () (@var "Q" tptp.name)) % 0.48/0.94 (define @t559 () (@var "P" tptp.name)) % 0.48/0.94 (define @t560 () (_ (_ tptp.member695284560e_name (_ (_ tptp.produc1570949143e_name (_ @t429 @t559)) (_ @t429 @t558))) @t557)) % 0.48/0.94 (define @t561 () (_ (_ tptp.member695284560e_name (_ (_ tptp.produc1570949143e_name @t559) @t558)) @t557)) % 0.48/0.94 (define @t562 () (_ tptp.eqvt_name @t557)) % 0.48/0.94 (define @t563 () (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t433) @t432)) @t427)) % 0.48/0.94 (define @t564 () (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t10) @t57)) @t427)) % 0.48/0.94 (define @t565 () (_ tptp.par @t57)) % 0.48/0.94 (define @t566 () (@var "S2" tptp.pi)) % 0.48/0.94 (define @t567 () (_ tptp.res @t335)) % 0.48/0.94 (define @t568 () (_ @t567 @t566)) % 0.48/0.94 (define @t569 () (@var "R2" tptp.pi)) % 0.48/0.94 (define @t570 () (_ tptp.par @t566)) % 0.48/0.94 (define @t571 () (@var "U" tptp.pi)) % 0.48/0.94 (define @t572 () (@var "T" tptp.pi)) % 0.48/0.94 (define @t573 () (_ (_ tptp.par @t572) @t571)) % 0.48/0.94 (define @t574 () (_ @t570 @t573)) % 0.48/0.94 (define @t575 () (_ @t570 @t572)) % 0.48/0.94 (define @t576 () (@list @t566 @t572 @t571 @t335)) % 0.48/0.94 (define @t577 () (_ (_ tptp.par @t575) @t571)) % 0.48/0.94 (define @t578 () (_ tptp.late_BoundOutputS @t283)) % 0.48/0.94 (define @t579 () (@var "Y12" tptp.name)) % 0.48/0.94 (define @t580 () (@var "X12" tptp.name)) % 0.48/0.94 (define @t581 () (@var "Y11" tptp.name)) % 0.48/0.94 (define @t582 () (@var "X11" tptp.name)) % 0.48/0.94 (define @t583 () (_ (_ tptp.late_OutputR @t582) @t580)) % 0.48/0.94 (define @t584 () (@var "X122" tptp.name)) % 0.48/0.94 (define @t585 () (@var "X112" tptp.name)) % 0.48/0.94 (define @t586 () (@var "X22" tptp.name)) % 0.48/0.94 (define @t587 () (@var "X13" tptp.name)) % 0.48/0.94 (define @t588 () (@var "Prop" (-> tptp.late_subject tptp.name tptp.pi Bool))) % 0.48/0.94 (define @t589 () (_ @t405 @t10)) % 0.48/0.94 (define @t590 () (_ tptp.input @t11)) % 0.48/0.94 (define @t591 () (_ (_ @t590 @t12) @t10)) % 0.48/0.94 (define @t592 () (_ tptp.late_transitions @t591)) % 0.48/0.94 (define @t593 () (@var "Y22" tptp.list_P227219501e_name)) % 0.48/0.94 (define @t594 () (@var "X222" tptp.list_P227219501e_name)) % 0.48/0.94 (define @t595 () (@var "Y21" tptp.produc367475239e_name)) % 0.48/0.94 (define @t596 () (@var "X21" tptp.produc367475239e_name)) % 0.48/0.94 (define @t597 () (@var "X32" tptp.name)) % 0.48/0.94 (define @t598 () (_ (_ (_ tptp.input @t393) @t392) @t376)) % 0.48/0.94 (define @t599 () (@var "Pi22" tptp.pi)) % 0.48/0.94 (define @t600 () (@var "Pi12" tptp.pi)) % 0.48/0.94 (define @t601 () (_ tptp.late_transitions (_ @t14 (_ (_ @t590 @t197) @t10)))) % 0.48/0.94 (define @t602 () (@var "Unit" tptp.product_unit)) % 0.48/0.94 (define @t603 () (@var "P" (-> tptp.product_unit Bool))) % 0.48/0.94 (define @t604 () (_ tptp.late_BoundR (_ tptp.late_BoundOutputS @t18))) % 0.48/0.94 (define @t605 () (_ @t592 (_ @t252 @t10))) % 0.48/0.94 (define @t606 () (@var "Y22" tptp.pi)) % 0.48/0.94 (define @t607 () (@var "X222" tptp.pi)) % 0.48/0.94 (define @t608 () (@var "Y21" tptp.late_freeRes)) % 0.48/0.94 (define @t609 () (@var "X21" tptp.late_freeRes)) % 0.48/0.94 (define @t610 () (_ tptp.swap_name2 @t20)) % 0.48/0.94 (define @t611 () (_ @t610 @t56)) % 0.48/0.94 (define @t612 () (@list @t37 @t202)) % 0.48/0.94 (define @t613 () (@list @t12 @t197)) % 0.48/0.94 (define @t614 () (@list @t30 @t192)) % 0.48/0.94 (define @t615 () (@list @t26 @t187)) % 0.48/0.94 (define @t616 () (@var "P" Bool)) % 0.48/0.94 (define @t617 () (@list @t17 @t182)) % 0.48/0.94 (define @t618 () (@var "B3" tptp.name)) % 0.48/0.94 (define @t619 () (@var "A4" tptp.name)) % 0.48/0.94 (define @t620 () (lambda (@list @t619 @t618) (not (= @t619 @t618)))) % 0.48/0.94 (define @t621 () (@var "Rel2" tptp.set_Pr1834926343_pi_pi)) % 0.48/0.94 (define @t622 () (@var "Perm2" tptp.list_P227219501e_name)) % 0.48/0.94 (define @t623 () (lambda (@list @t621) (forall (@list @t136 @t622) (=> (_ @t137 @t621) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.perm_n1415585007_pi_pi @t622) @t136)) @t621))))) % 0.48/0.94 (define @t624 () (@var "Q6" tptp.pi)) % 0.48/0.94 (define @t625 () (@var "P8" tptp.pi)) % 0.48/0.94 (define @t626 () (@var "Alpha3" tptp.late_freeRes)) % 0.48/0.94 (define @t627 () (_ tptp.late_FreeR @t626)) % 0.48/0.94 (define @t628 () (@var "P7" tptp.pi)) % 0.48/0.94 (define @t629 () (_ tptp.late_transitions @t628)) % 0.48/0.94 (define @t630 () (@list @t625)) % 0.48/0.94 (define @t631 () (@var "Q5" tptp.pi)) % 0.48/0.94 (define @t632 () (_ tptp.late_transitions @t631)) % 0.48/0.94 (define @t633 () (@var "X3" tptp.name)) % 0.48/0.94 (define @t634 () (@var "A4" tptp.late_subject)) % 0.48/0.94 (define @t635 () (_ (_ tptp.late_BoundR @t634) @t633)) % 0.48/0.94 (define @t636 () (lambda (@list @t628 @t621 @t631) (and (forall (@list @t634 @t633 @t624) (=> (and (_ @t632 (_ @t635 @t624)) (_ (_ tptp.fresh_name_pi @t633) @t628)) (exists @t630 (and (_ @t629 (_ @t635 @t625)) (_ (_ (_ (_ (_ tptp.strong2129052853vative @t625) @t624) @t634) @t633) @t621))))) (forall (@list @t626 @t624) (=> (_ @t632 (_ @t627 @t624)) (exists @t630 (and (_ @t629 (_ @t627 @t625)) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t625) @t624)) @t621)))))))) % 0.48/0.94 (define @t637 () (tptp.late_OutputR tptp.ab tptp.x)) % 0.48/0.94 (define @t638 () (tptp.late_OutputR @t393 @t392)) % 0.48/0.94 (define @t639 () (not (= @t637 @t638))) % 0.48/0.94 (define @t640 () (= @t1 @t638)) % 0.48/0.94 (define @t641 () (not @t640)) % 0.48/0.94 (define @t642 () (= tptp.late_TauR @t638)) % 0.48/0.94 (define @t643 () (not @t642)) % 0.48/0.94 (define @t644 () (= tptp.late_TauR @t394)) % 0.48/0.94 (define @t645 () (not @t644)) % 0.48/0.94 (define @t646 () (forall @t396 (not (= @t638 @t637)))) % 0.48/0.94 (define @t647 () (not (= @t637 @t637))) % 0.48/0.94 (assume @p1 (not (= tptp.ya tptp.b))) % 0.48/0.94 (assume @p2 (= @t1 tptp.late_TauR)) % 0.48/0.94 (assume @p3 (not (= tptp.ab tptp.x))) % 0.48/0.94 (assume @p4 (not (= tptp.ya tptp.c))) % 0.48/0.94 (assume @p5 (= tptp.aa @t2)) % 0.48/0.94 (assume @p6 (_ tptp.eqvt_pi tptp.rel)) % 0.48/0.94 (assume @p7 (not (= tptp.y tptp.x))) % 0.48/0.94 (assume @p8 (_ (_ tptp.late_transitions @t6) (_ (_ (_ tptp.late_BoundR tptp.aa) tptp.y) tptp.xPQ))) % 0.48/0.94 (assume @p9 (_ (_ tptp.fresh_name_pi tptp.x) tptp.p)) % 0.48/0.94 (assume @p10 (_ @t7 tptp.p)) % 0.48/0.94 (assume @p11 (_ @t7 tptp.q)) % 0.48/0.94 (assume @p12 (_ @t7 tptp.q2)) % 0.48/0.94 (assume @p13 (_ @t8 @t6)) % 0.48/0.94 (assume @p14 (_ @t8 @t9)) % 0.48/0.94 (assume @p15 (forall (@list @t11 @t10 @t12) (= (_ (_ @t16 @t12) @t11) (_ @t14 (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ @t13 @t11)) tptp.nil_Pr743626285e_name)) @t10))))) % 0.48/0.94 (assume @p16 (_ (_ tptp.late_transitions tptp.p) (_ (_ (_ tptp.late_BoundR (_ tptp.late_InputS tptp.b)) tptp.ya) tptp.p2))) % 0.48/0.94 (assume @p17 (forall @t25 (= (_ @t23 @t24) @t17))) % 0.48/0.94 (assume @p18 (forall @t29 (= (_ @t27 @t28) @t26))) % 0.48/0.94 (assume @p19 (forall @t33 (= (_ @t31 @t32) @t30))) % 0.48/0.94 (assume @p20 (forall @t36 (= (_ @t34 @t35) @t12))) % 0.48/0.94 (assume @p21 (forall @t40 (= (_ @t38 @t39) @t37))) % 0.48/0.94 (assume @p22 (forall (@list @t11 @t17) (= (_ (_ tptp.perm_n1559866809ubject @t41) @t17) @t17))) % 0.48/0.94 (assume @p23 (forall (@list @t11 @t26) (= (_ (_ tptp.perm_n336613537reeRes @t41) @t26) @t26))) % 0.48/0.94 (assume @p24 (forall (@list @t11 @t30) (= (_ (_ tptp.perm_name_pi_Rep @t41) @t30) @t30))) % 0.48/0.94 (assume @p25 (forall (@list @t11 @t12) (= (_ (_ tptp.perm_name_name @t41) @t12) @t12))) % 0.48/0.94 (assume @p26 (forall (@list @t11 @t37) (= (_ (_ tptp.perm_name_pi @t41) @t37) @t37))) % 0.48/0.94 (assume @p27 (forall @t25 (= @t24 @t43))) % 0.48/0.94 (assume @p28 (forall @t29 (= @t28 @t44))) % 0.48/0.94 (assume @p29 (forall @t33 (= @t32 @t45))) % 0.48/0.94 (assume @p30 (forall @t36 (= @t35 @t46))) % 0.48/0.94 (assume @p31 (forall @t40 (= @t39 @t47))) % 0.48/0.94 (assume @p32 (_ (_ tptp.late_transitions @t4) (_ (_ tptp.late_FreeR @t1) tptp.pq))) % 0.48/0.94 (assume @p33 (forall (@list @t49 @t52 @t48) (= (_ @t50 @t54) (_ (_ tptp.par @t53) @t51)))) % 0.48/0.94 (assume @p34 (forall (@list @t10 @t57 @t56 @t55) (= (_ (_ (_ tptp.subs @t61) @t56) @t55) (_ (_ tptp.par @t59) (_ (_ (_ tptp.subs @t57) @t56) @t55))))) % 0.48/0.94 (assume @p35 (forall (@list @t12 @t56 @t55 @t10) (=> (not (= @t12 @t56)) (=> (not (= @t12 @t55)) (= (_ (_ (_ tptp.subs @t62) @t56) @t55) (_ @t14 @t59)))))) % 0.48/0.94 (assume @p36 (forall (@list @t17) (= (_ (_ tptp.perm_n1559866809ubject tptp.nil_Pr743626285e_name) @t17) @t17))) % 0.48/0.94 (assume @p37 (forall (@list @t26) (= (_ (_ tptp.perm_n336613537reeRes tptp.nil_Pr743626285e_name) @t26) @t26))) % 0.48/0.94 (assume @p38 (forall (@list @t30) (= (_ @t63 @t30) @t30))) % 0.48/0.94 (assume @p39 (forall @t64 (= (_ (_ tptp.perm_name_name tptp.nil_Pr743626285e_name) @t12) @t12))) % 0.48/0.94 (assume @p40 (forall @t65 (= (_ (_ tptp.perm_name_pi tptp.nil_Pr743626285e_name) @t37) @t37))) % 0.48/0.94 (assume @p41 (_ (_ tptp.late_transitions tptp.q) (_ (_ tptp.late_FreeR (_ (_ tptp.late_OutputR tptp.b) tptp.c)) tptp.q2))) % 0.48/0.94 (assume @p42 (_ @t8 @t4)) % 0.48/0.94 (assume @p43 (forall (@list @t10 @t11) (= (_ @t66 @t11) @t10))) % 0.48/0.94 (assume @p44 (forall (@list @t67) (= (_ @t63 @t67) @t67))) % 0.48/0.94 (assume @p45 (_ @t8 tptp.p)) % 0.48/0.94 (assume @p46 (_ @t8 tptp.q)) % 0.48/0.94 (assume @p47 (forall (@list @t11 @t52 @t48) (= (_ @t68 @t54) (and (_ @t68 @t52) @t69)))) % 0.48/0.94 (assume @p48 (forall (@list @t49 @t70 @t52) (= (_ @t50 @t73) (_ (_ tptp.res @t72) @t53)))) % 0.48/0.94 (assume @p49 (forall (@list @t11 @t17 @t18) (=> @t75 (=> (_ (_ tptp.fresh_717452603ubject @t18) @t17) (= @t24 @t17))))) % 0.48/0.94 (assume @p50 (forall (@list @t11 @t26 @t18) (=> @t77 (=> (_ (_ tptp.fresh_1641682979reeRes @t18) @t26) (= @t28 @t26))))) % 0.48/0.94 (assume @p51 (forall (@list @t11 @t30 @t18) (=> @t79 (=> (_ (_ tptp.fresh_name_pi_Rep @t18) @t30) (= @t32 @t30))))) % 0.48/0.94 (assume @p52 (forall (@list @t11 @t80 @t18) (=> @t83 (=> (_ (_ tptp.fresh_1143631827t_unit @t18) @t80) (= @t81 @t80))))) % 0.48/0.94 (assume @p53 (forall (@list @t11 @t84 @t18) (=> @t87 (=> (_ (_ tptp.fresh_1376661020_pi_pi @t18) @t84) (= @t85 @t84))))) % 0.48/0.94 (assume @p54 (forall (@list @t11 @t12 @t18) (=> @t89 (=> (_ (_ tptp.fresh_name_name @t18) @t12) (= @t35 @t12))))) % 0.48/0.94 (assume @p55 (forall (@list @t11 @t37 @t18) (=> @t91 (=> (_ @t90 @t37) (= @t39 @t37))))) % 0.48/0.94 (assume @p56 (forall (@list @t11 @t92 @t18) (=> @t95 (=> (_ (_ tptp.fresh_543891186ion_pi @t18) @t92) (= @t93 @t92))))) % 0.48/0.94 (assume @p57 (_ (_ tptp.fresh_717452603ubject tptp.y) tptp.aa)) % 0.48/0.94 (assume @p58 (forall (@list @t11 @t49 @t17) (=> @t98 (=> @t75 (_ @t74 @t97))))) % 0.48/0.94 (assume @p59 (forall (@list @t11 @t49 @t26) (=> @t98 (=> @t77 (_ @t76 @t100))))) % 0.48/0.94 (assume @p60 (forall (@list @t11 @t49 @t30) (=> @t98 (=> @t79 (_ @t78 @t102))))) % 0.48/0.94 (assume @p61 (forall (@list @t11 @t49 @t80) (=> @t98 (=> @t83 (_ @t82 @t103))))) % 0.48/0.94 (assume @p62 (forall (@list @t11 @t49 @t84) (=> @t98 (=> @t87 (_ @t86 @t104))))) % 0.48/0.94 (assume @p63 (forall (@list @t11 @t49 @t12) (=> @t98 (=> @t89 (_ @t88 @t105))))) % 0.48/0.94 (assume @p64 (forall (@list @t11 @t49 @t37) (=> @t98 (=> @t91 (_ @t68 @t106))))) % 0.48/0.94 (assume @p65 (forall (@list @t11 @t49 @t92) (=> @t98 (=> @t95 (_ @t94 @t107))))) % 0.48/0.94 (assume @p66 (forall (@list @t80) (not (forall @t109 (not (_ (_ tptp.fresh_1143631827t_unit @t108) @t80)))))) % 0.48/0.94 (assume @p67 (forall (@list @t84) (not (forall @t109 (not (_ (_ tptp.fresh_1376661020_pi_pi @t108) @t84)))))) % 0.48/0.94 (assume @p68 (forall @t64 (not (forall @t109 (not (_ (_ tptp.fresh_name_name @t108) @t12)))))) % 0.48/0.94 (assume @p69 (forall @t65 (not (forall @t109 (not (_ (_ tptp.fresh_name_pi @t108) @t37)))))) % 0.48/0.94 (assume @p70 (forall @t113 (= (_ @t112 @t75) @t111))) % 0.48/0.94 (assume @p71 (forall @t115 (= (_ @t112 @t77) @t114))) % 0.48/0.94 (assume @p72 (forall @t117 (= (_ @t112 @t79) @t116))) % 0.48/0.94 (assume @p73 (forall @t119 (= (_ @t112 @t83) @t118))) % 0.48/0.94 (assume @p74 (forall @t121 (= (_ @t112 @t87) @t120))) % 0.48/0.94 (assume @p75 (forall @t123 (= (_ @t112 @t89) @t122))) % 0.48/0.94 (assume @p76 (forall @t125 (= (_ @t112 @t91) @t124))) % 0.48/0.94 (assume @p77 (forall @t127 (= (_ @t112 @t95) @t126))) % 0.48/0.94 (assume @p78 (forall @t113 (= @t111 @t75))) % 0.48/0.94 (assume @p79 (forall @t115 (= @t114 @t77))) % 0.48/0.94 (assume @p80 (forall @t117 (= @t116 @t79))) % 0.48/0.94 (assume @p81 (forall @t119 (= @t118 @t83))) % 0.48/0.94 (assume @p82 (forall @t121 (= @t120 @t87))) % 0.48/0.94 (assume @p83 (forall @t123 (= @t122 @t89))) % 0.48/0.94 (assume @p84 (forall @t125 (= @t124 @t91))) % 0.48/0.94 (assume @p85 (forall @t127 (= @t126 @t95))) % 0.48/0.94 (assume @p86 (forall (@list @t11 @t10) (_ @t68 @t15))) % 0.48/0.94 (assume @p87 (forall (@list @t11 @t18 @t10) (=> @t129 (_ @t68 @t128)))) % 0.48/0.94 (assume @p88 (forall (@list @t11 @t10 @t56 @t18) (=> @t132 (=> @t131 (_ @t68 (_ (_ @t58 @t18) @t56)))))) % 0.48/0.94 (assume @p89 (forall (@list @t11 @t10 @t18) (=> @t132 (= @t128 @t10)))) % 0.48/0.94 (assume @p90 (forall (@list @t133 @t134) (= (_ (_ tptp.member558706512_pi_pi @t133) (_ tptp.collec1051790738_pi_pi @t134)) (_ @t134 @t133)))) % 0.48/0.94 (assume @p91 (forall (@list @t135) (= (_ tptp.collec1051790738_pi_pi (lambda (@list @t136) (_ @t137 @t135))) @t135))) % 0.48/0.94 (assume @p92 (forall @t141 (=> @t140 (= (_ (_ @t16 @t11) @t18) @t139)))) % 0.48/0.94 (assume @p93 (forall @t141 (=> @t140 (= @t15 @t139)))) % 0.48/0.94 (assume @p94 (forall (@list @t142 @t10 @t11 @t18) (= (_ @t144 @t128) (_ (_ (_ tptp.subs (_ @t144 @t10)) (_ @t143 @t11)) (_ @t143 @t18))))) % 0.48/0.94 (assume @p95 (forall @t145 (= (_ @t34 @t11) @t18))) % 0.48/0.94 (assume @p96 (forall @t145 (= (_ @t34 @t18) @t11))) % 0.48/0.94 (assume @p97 (forall @t148 (=> @t131 (=> @t147 (= (_ @t34 @t56) @t56))))) % 0.48/0.94 (assume @p98 (forall (@list @t56 @t11 @t17 @t18) (=> @t150 (=> @t75 (=> (_ @t149 @t17) (_ @t149 @t24)))))) % 0.48/0.94 (assume @p99 (forall (@list @t56 @t11 @t26 @t18) (=> @t150 (=> @t77 (=> (_ @t151 @t26) (_ @t151 @t28)))))) % 0.48/0.94 (assume @p100 (forall (@list @t56 @t11 @t30 @t18) (=> @t150 (=> @t79 (=> (_ @t152 @t30) (_ @t152 @t32)))))) % 0.48/0.94 (assume @p101 (forall (@list @t56 @t11 @t80 @t18) (=> @t150 (=> @t83 (=> (_ @t153 @t80) (_ @t153 @t81)))))) % 0.48/0.94 (assume @p102 (forall (@list @t56 @t11 @t84 @t18) (=> @t150 (=> @t87 (=> (_ @t154 @t84) (_ @t154 @t85)))))) % 0.48/0.94 (assume @p103 (forall (@list @t56 @t11 @t12 @t18) (=> @t150 (=> @t89 (=> (_ @t155 @t12) (_ @t155 @t35)))))) % 0.48/0.94 (assume @p104 (forall (@list @t56 @t11 @t37 @t18) (=> @t150 (=> @t91 (=> (_ @t156 @t37) (_ @t156 @t39)))))) % 0.48/0.94 (assume @p105 (forall (@list @t56 @t11 @t92 @t18) (=> @t150 (=> @t95 (=> (_ @t157 @t92) (_ @t157 @t93)))))) % 0.48/0.94 (assume @p106 (forall (@list @t158 @t161 @t17) (= (_ @t159 @t164) (_ (_ tptp.perm_n1559866809ubject @t162) @t160)))) % 0.48/0.94 (assume @p107 (forall (@list @t158 @t161 @t26) (= (_ @t165 @t168) (_ (_ tptp.perm_n336613537reeRes @t162) @t166)))) % 0.48/0.94 (assume @p108 (forall (@list @t158 @t161 @t30) (= (_ @t169 @t172) (_ (_ tptp.perm_name_pi_Rep @t162) @t170)))) % 0.48/0.94 (assume @p109 (forall (@list @t158 @t161 @t12) (= (_ @t173 @t176) (_ (_ tptp.perm_name_name @t162) @t174)))) % 0.48/0.94 (assume @p110 (forall (@list @t158 @t161 @t37) (= (_ @t177 @t180) (_ (_ tptp.perm_name_pi @t162) @t178)))) % 0.48/0.94 (assume @p111 (forall (@list @t161 @t158 @t17) (= (_ @t163 @t160) (_ (_ tptp.perm_n1559866809ubject @t181) @t164)))) % 0.48/0.94 (assume @p112 (forall (@list @t161 @t158 @t26) (= (_ @t167 @t166) (_ (_ tptp.perm_n336613537reeRes @t181) @t168)))) % 0.48/0.94 (assume @p113 (forall (@list @t161 @t158 @t30) (= (_ @t171 @t170) (_ (_ tptp.perm_name_pi_Rep @t181) @t172)))) % 0.48/0.94 (assume @p114 (forall (@list @t161 @t158 @t12) (= (_ @t175 @t174) (_ (_ tptp.perm_name_name @t181) @t176)))) % 0.48/0.94 (assume @p115 (forall (@list @t161 @t158 @t37) (= (_ @t179 @t178) (_ (_ tptp.perm_name_pi @t181) @t180)))) % 0.48/0.94 (assume @p116 (forall @t186 (= @t185 @t183))) % 0.48/0.94 (assume @p117 (forall @t191 (= @t190 @t188))) % 0.48/0.94 (assume @p118 (forall @t196 (= @t195 @t193))) % 0.48/0.94 (assume @p119 (forall @t201 (= @t200 @t198))) % 0.48/0.94 (assume @p120 (forall @t206 (= @t205 @t203))) % 0.48/0.94 (assume @p121 (forall (@list @t49 @t207 @t17) (= (_ @t96 (_ @t207 @t17)) (_ (_ (_ tptp.perm_n1447856217ubject @t49) @t207) @t97)))) % 0.48/0.94 (assume @p122 (forall (@list @t49 @t208 @t26) (= (_ @t96 (_ @t208 @t26)) (_ (_ (_ tptp.perm_n303101761ubject @t49) @t208) @t100)))) % 0.48/0.94 (assume @p123 (forall (@list @t49 @t209 @t30) (= (_ @t96 (_ @t209 @t30)) (_ (_ (_ tptp.perm_n698371375ubject @t49) @t209) @t102)))) % 0.48/0.94 (assume @p124 (forall (@list @t49 @t210 @t12) (= (_ @t96 (_ @t210 @t12)) (_ (_ (_ tptp.perm_n1387060402ubject @t49) @t210) @t105)))) % 0.48/0.94 (assume @p125 (forall (@list @t49 @t211 @t37) (= (_ @t96 (_ @t211 @t37)) (_ (_ (_ tptp.perm_n190055296ubject @t49) @t211) @t106)))) % 0.48/0.94 (assume @p126 (forall (@list @t49 @t212 @t17) (= (_ @t99 (_ @t212 @t17)) (_ (_ (_ tptp.perm_n443561793reeRes @t49) @t212) @t97)))) % 0.48/0.94 (assume @p127 (forall (@list @t49 @t213 @t26) (= (_ @t99 (_ @t213 @t26)) (_ (_ (_ tptp.perm_n1446290985reeRes @t49) @t213) @t100)))) % 0.48/0.94 (assume @p128 (forall (@list @t49 @t214 @t30) (= (_ @t99 (_ @t214 @t30)) (_ (_ (_ tptp.perm_n1841560599reeRes @t49) @t214) @t102)))) % 0.48/0.94 (assume @p129 (forall (@list @t49 @t215 @t12) (= (_ @t99 (_ @t215 @t12)) (_ (_ (_ tptp.perm_n382765978reeRes @t49) @t215) @t105)))) % 0.48/0.94 (assume @p130 (forall (@list @t49 @t216 @t37) (= (_ @t99 (_ @t216 @t37)) (_ (_ (_ tptp.perm_n1333244520reeRes @t49) @t216) @t106)))) % 0.48/0.94 (assume @p131 (forall (@list @t49 @t218 @t217) (= (_ @t112 (_ (_ tptp.member558706512_pi_pi @t218) @t217)) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.perm_n1415585007_pi_pi @t49) @t218)) (_ (_ tptp.perm_n675238095_pi_pi @t49) @t217))))) % 0.48/0.94 (assume @p132 (forall (@list @t49 @t17 @t219) (= (_ @t112 (_ (_ tptp.member_Late_subject @t17) @t219)) (_ (_ tptp.member_Late_subject @t97) (_ (_ tptp.perm_n412725103ubject @t49) @t219))))) % 0.48/0.94 (assume @p133 (forall (@list @t49 @t26 @t220) (= (_ @t112 (_ (_ tptp.member_Late_freeRes @t26) @t220)) (_ (_ tptp.member_Late_freeRes @t100) (_ (_ tptp.perm_n1555914327reeRes @t49) @t220))))) % 0.48/0.94 (assume @p134 (forall (@list @t49 @t30 @t221) (= (_ @t112 (_ (_ tptp.member_pi_Rep @t30) @t221)) (_ (_ tptp.member_pi_Rep @t102) (_ (_ tptp.perm_name_set_pi_Rep @t49) @t221))))) % 0.48/0.94 (assume @p135 (forall (@list @t49 @t12 @t222) (= (_ @t112 (_ (_ tptp.member_name @t12) @t222)) (_ (_ tptp.member_name @t105) (_ (_ tptp.perm_name_set_name @t49) @t222))))) % 0.48/0.94 (assume @p136 (forall (@list @t49 @t37 @t223) (= (_ @t112 (_ (_ tptp.member_pi @t37) @t223)) (_ (_ tptp.member_pi @t106) (_ (_ tptp.perm_name_set_pi @t49) @t223))))) % 0.48/0.94 (assume @p137 (forall @t186 (= (_ @t112 @t183) @t185))) % 0.48/0.94 (assume @p138 (forall @t191 (= (_ @t112 @t188) @t190))) % 0.48/0.94 (assume @p139 (forall @t196 (= (_ @t112 @t193) @t195))) % 0.48/0.94 (assume @p140 (forall @t201 (= (_ @t112 @t198) @t200))) % 0.48/0.94 (assume @p141 (forall @t206 (= (_ @t112 @t203) @t205))) % 0.48/0.94 (assume @p142 (forall (@list @t52 @t48 @t226 @t224) (= (= @t54 (_ (_ tptp.par @t226) @t224)) (and (= @t52 @t226) @t225)))) % 0.48/0.94 (assume @p143 (forall (@list @t56 @t10 @t11) (=> @t227 (= @t15 (_ (_ tptp.res @t56) (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ @t19 @t56)) tptp.nil_Pr743626285e_name)) @t10)))))) % 0.48/0.94 (assume @p144 (forall @t141 (=> @t140 (= (_ @t38 @t10) @t128)))) % 0.48/0.94 (assume @p145 (forall (@list @t56 @t10 @t11 @t18) (=> @t227 (= @t128 (_ (_ (_ tptp.subs (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ (_ tptp.produc1570949143e_name @t56) @t11)) tptp.nil_Pr743626285e_name)) @t10)) @t56) @t18))))) % 0.48/0.94 (assume @p146 (forall (@list @t232 @t231 @t229 @t228) (not (= (_ (_ tptp.par @t232) @t231) @t230)))) % 0.48/0.94 (assume @p147 (forall @t25 (= (_ @t23 @t43) @t17))) % 0.48/0.94 (assume @p148 (forall @t29 (= (_ @t27 @t44) @t26))) % 0.48/0.94 (assume @p149 (forall @t33 (= (_ @t31 @t45) @t30))) % 0.48/0.94 (assume @p150 (forall @t36 (= (_ @t34 @t46) @t12))) % 0.48/0.94 (assume @p151 (forall @t40 (= (_ @t38 @t47) @t37))) % 0.48/0.94 (assume @p152 (forall @t259 (=> @t258 (=> @t254 (=> @t250 (=> @t249 (=> @t248 (=> @t247 (=> @t246 (=> @t245 (=> @t243 (=> (_ @t242 @t233) (=> @t241 @t240))))))))))))) % 0.48/0.94 (assume @p153 (forall @t266 (=> @t265 (=> @t264 (=> @t250 (=> @t249 (=> @t248 (=> @t247 (=> @t246 (=> @t263 (=> @t243 (=> @t262 (=> @t241 @t261))))))))))))) % 0.48/0.94 (assume @p154 (forall @t259 (=> @t258 (=> @t254 (=> @t247 @t240))))) % 0.48/0.94 (assume @p155 (forall @t266 (=> @t265 (=> @t264 (=> @t248 @t261))))) % 0.48/0.94 (assume @p156 (forall @t271 (=> @t270 (=> @t254 (=> @t250 (=> @t249 (=> @t246 (=> @t268 (=> @t245 @t267))))))))) % 0.48/0.94 (assume @p157 (forall @t274 (=> @t265 (=> @t273 (=> @t250 (=> @t249 (=> @t246 (=> @t268 (=> @t263 @t272))))))))) % 0.48/0.94 (assume @p158 (forall @t271 (=> @t270 (=> @t254 @t267)))) % 0.48/0.94 (assume @p159 (forall @t274 (=> @t265 (=> @t273 @t272)))) % 0.48/0.94 (assume @p160 (forall (@list @t275 @t10 @t276 @t12) (=> (_ (_ tptp.fresh_name_pi @t275) @t10) (= (_ @t278 @t10) (_ (_ @t277 @t275) (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ @t13 @t275)) tptp.nil_Pr743626285e_name)) @t10)))))) % 0.48/0.94 (assume @p161 (forall (@list @t279) (= (_ (_ tptp.perm_n1938283068es_Rep tptp.nil_Pr743626285e_name) @t279) @t279))) % 0.48/0.94 (assume @p162 (forall (@list @t280) (= (_ (_ tptp.perm_n697952036ct_Rep tptp.nil_Pr743626285e_name) @t280) @t280))) % 0.48/0.94 (assume @p163 (forall (@list @t281) (= (_ (_ tptp.perm_n890803237al_Rep tptp.nil_Pr743626285e_name) @t281) @t281))) % 0.48/0.94 (assume @p164 (forall (@list @t11 @t283 @t70) (= (_ @t76 @t284) (and (_ @t88 @t283) @t282)))) % 0.48/0.94 (assume @p165 (forall (@list @t283 @t70 @t287 @t285) (= (= @t284 (_ (_ tptp.late_OutputR @t287) @t285)) (and @t288 @t286)))) % 0.48/0.94 (assume @p166 (forall @t290 (= (= @t289 (_ tptp.late_BoundOutputS @t285)) @t286))) % 0.48/0.94 (assume @p167 (forall @t291 (_ @t76 tptp.late_TauR))) % 0.48/0.94 (assume @p168 (forall (@list @t49) (= (_ @t99 tptp.late_TauR) tptp.late_TauR))) % 0.48/0.94 (assume @p169 (_ (_ tptp.fresh_1143631827t_unit tptp.ya) tptp.product_Unity)) % 0.48/0.94 (assume @p170 (forall (@list @t11 @t292 @t48) (= (_ (_ tptp.fresh_81631222sidual @t11) @t293) (and (_ @t76 @t292) @t69)))) % 0.48/0.94 (assume @p171 (forall (@list @t18 @t10 @t11 @t56) (=> @t140 (= (_ (_ (_ tptp.subs @t128) @t18) @t56) (_ @t66 @t56))))) % 0.48/0.94 (assume @p172 (forall (@list @t49 @t292 @t48) (= (_ @t294 @t293) (_ (_ tptp.late_FreeR (_ @t99 @t292)) @t51)))) % 0.48/0.94 (assume @p173 (forall (@list @t49 @t283 @t70) (= (_ @t99 @t284) (_ (_ tptp.late_OutputR (_ @t71 @t283)) @t72)))) % 0.48/0.94 (assume @p174 (forall @t296 (= (_ @t96 @t295) (_ tptp.late_InputS @t72)))) % 0.48/0.94 (assume @p175 (forall @t296 (= (_ @t96 @t289) (_ tptp.late_BoundOutputS @t72)))) % 0.48/0.94 (assume @p176 (forall @t297 (= (_ @t74 @t289) @t282))) % 0.48/0.94 (assume @p177 (forall @t297 (= (_ @t74 @t295) @t282))) % 0.48/0.94 (assume @p178 (forall (@list @t49 @t298 @t70 @t52) (= (_ @t294 (_ (_ (_ tptp.late_BoundR @t298) @t70) @t52)) (_ (_ (_ tptp.late_BoundR (_ @t96 @t298)) @t72) @t53)))) % 0.48/0.94 (assume @p179 (forall (@list @t10 @t299 @t12) (=> (_ @t257 @t299) (=> @t250 (_ (_ tptp.fresh_81631222sidual @t12) @t299))))) % 0.48/0.94 (assume @p180 (forall (@list @t12 @t10 @t303 @t300 @t301) (=> (_ @t308 (_ @t305 @t300)) (=> (forall @t307 (=> @t306 (=> (_ @t304 @t303) (_ @t301 (_ @t14 @t302))))) (_ @t301 @t300))))) % 0.48/0.94 (assume @p181 (forall (@list @t12 @t10 @t303 @t235) (=> (_ @t308 @t318) (not (forall @t321 (=> @t320 (=> (= @t318 @t317) @t314))))))) % 0.48/0.94 (assume @p182 (forall @t326 (=> @t325 (=> @t324 (_ @t323 (_ @t305 @t322)))))) % 0.48/0.94 (assume @p183 (forall @t331 (=> @t330 (=> @t329 (=> @t328 @t327))))) % 0.48/0.94 (assume @p184 (forall @t326 (=> @t325 (=> @t248 @t324)))) % 0.48/0.94 (assume @p185 (forall @t331 (=> @t330 (=> @t248 @t329)))) % 0.48/0.94 (assume @p186 (forall @t331 (=> @t330 (=> @t329 (=> @t328 (=> @t250 (=> @t333 @t327))))))) % 0.48/0.94 (assume @p187 (forall (@list @t10 @t57 @t347 @t197 @t235) (=> (_ @t239 @t349) (=> (forall (@list @t312 @t334 @t335 @t302 @t338) (=> @t350 (=> (= @t349 (_ @t344 (_ @t352 @t338))) (=> @t351 @t341)))) (not (forall (@list @t338 @t334 @t335 @t342 @t312) (=> @t350 (=> (= @t349 (_ @t344 (_ @t346 @t342))) (=> (_ (_ tptp.late_transitions @t338) @t345) @t341))))))))) % 0.48/0.94 (assume @p188 (forall @t355 (=> @t330 (=> @t250 (=> @t249 (=> @t333 @t354)))))) % 0.48/0.94 (assume @p189 (forall @t359 (=> @t358 (=> @t250 (=> @t249 (=> @t333 @t357)))))) % 0.48/0.94 (assume @p190 (forall (@list @t12 @t10 @t299) (=> (_ @t308 @t299) (=> (forall @t370 (=> (= @t62 @t369) (forall @t307 (=> (= @t299 @t368) @t366)))) (=> (forall @t362 (=> @t320 (=> (= @t299 @t361) @t360))) (not (forall @t321 (=> @t320 (=> (= @t299 @t317) @t314))))))))) % 0.48/0.94 (assume @p191 (forall (@list @t292 @t48 @t371 @t224) (= (= @t293 (_ (_ tptp.late_FreeR @t371) @t224)) (and (= @t292 @t371) @t225)))) % 0.48/0.94 (assume @p192 (forall (@list @t275 @t10 @t276 @t372 @t235) (=> (_ (_ tptp.late_transitions @t374) @t373) (=> (forall @t370 (=> (= @t374 @t369) (forall @t307 (=> (= @t373 @t368) @t366)))) (not (forall @t362 (=> (= @t374 @t319) (=> (= @t373 @t361) @t360)))))))) % 0.48/0.94 (assume @p193 (forall (@list @t378 @t377 @t376 @t375 @t228) (not (= (_ (_ (_ tptp.late_BoundR @t378) @t377) @t376) (_ (_ tptp.late_FreeR @t375) @t228))))) % 0.48/0.94 (assume @p194 (forall (@list @t380 @t379) (=> (forall (@list @t385 @t384 @t381) (_ @t380 @t386)) (=> (forall (@list @t382 @t381) (_ @t380 @t383)) (_ @t380 @t379))))) % 0.48/0.94 (assume @p195 (forall (@list @t48 @t387 @t49) (=> (_ (_ tptp.late_transitions @t48) @t387) (_ (_ tptp.late_transitions @t51) (_ @t294 @t387))))) % 0.48/0.94 (assume @p196 (forall (@list @t389 @t388) (=> (forall (@list @t391 @t390) (_ @t389 (_ (_ tptp.late_OutputR @t391) @t390))) (=> (_ @t389 tptp.late_TauR) (_ @t389 @t388))))) % 0.48/0.94 (assume @p197 @t397) % 0.48/0.94 (assume @p198 (forall (@list @t377 @t229) (not (= (_ tptp.late_InputS @t377) (_ tptp.late_BoundOutputS @t229))))) % 0.48/0.94 (assume @p199 (forall (@list @t398 @t378) (=> (forall @t399 (_ @t398 (_ tptp.late_InputS @t384))) (=> (forall @t399 (_ @t398 (_ tptp.late_BoundOutputS @t384))) (_ @t398 @t378))))) % 0.48/0.94 (assume @p200 (forall (@list @t197 @t10 @t276 @t12 @t400 @t401) (=> (_ @t323 (_ @t278 @t400)) (=> @t241 (=> @t250 (=> (forall (@list @t363 @t302) (=> (_ @t257 (_ (_ tptp.late_FreeR (_ (_ tptp.late_OutputR @t363) @t197)) @t302)) (=> (not (= @t363 @t197)) (=> (= @t276 @t406) (_ (_ @t401 @t406) (_ @t405 @t302)))))) (=> (forall @t307 (=> @t403 (=> @t329 (_ @t402 (_ @t237 @t302))))) (_ @t402 @t400)))))))) % 0.48/0.94 (assume @p201 (forall (@list @t10 @t303 @t235 @t57) (=> @t325 (_ @t239 (_ @t305 @t353))))) % 0.48/0.94 (assume @p202 (forall (@list @t57 @t303 @t233 @t10) (=> @t407 (_ @t239 (_ @t305 @t356))))) % 0.48/0.94 (assume @p203 (forall @t331 (=> @t330 (=> @t248 (=> @t328 @t262))))) % 0.48/0.94 (assume @p204 (forall (@list @t409 @t408 @t379) (=> (forall (@list @t385 @t384 @t381 @t410) (=> (_ (_ tptp.fresh_1143631827t_unit @t384) @t410) (=> @t412 (_ @t411 @t386)))) (=> (forall (@list @t382 @t381 @t410) (_ @t411 @t383)) (_ (_ @t409 @t408) @t379))))) % 0.48/0.94 (assume @p205 (forall (@list @t414 @t413 @t379) (=> (forall (@list @t385 @t384 @t381 @t415) (=> (_ (_ tptp.fresh_1376661020_pi_pi @t384) @t415) (=> @t412 (_ @t416 @t386)))) (=> (forall (@list @t382 @t381 @t415) (_ @t416 @t383)) (_ (_ @t414 @t413) @t379))))) % 0.48/0.94 (assume @p206 (forall (@list @t418 @t417 @t379) (=> (forall (@list @t385 @t384 @t381 @t419) (=> (_ (_ tptp.fresh_name_name @t384) @t419) (=> @t412 (_ @t420 @t386)))) (=> (forall (@list @t382 @t381 @t419) (_ @t420 @t383)) (_ (_ @t418 @t417) @t379))))) % 0.48/0.94 (assume @p207 (forall (@list @t422 @t421 @t379) (=> (forall (@list @t385 @t384 @t381 @t423) (=> (_ (_ tptp.fresh_name_pi @t384) @t423) (=> @t412 (_ @t424 @t386)))) (=> (forall (@list @t382 @t381 @t423) (_ @t424 @t383)) (_ (_ @t422 @t421) @t379))))) % 0.48/0.94 (assume @p208 (forall @t326 (=> @t325 (=> @t248 @t262)))) % 0.48/0.94 (assume @p209 (forall @t355 (=> @t330 (=> @t249 @t354)))) % 0.48/0.94 (assume @p210 (forall @t359 (=> @t358 (=> @t250 @t357)))) % 0.48/0.94 (assume @p211 (forall (@list @t10 @t57 @t276 @t12 @t425 @t426) (=> (_ @t239 (_ @t278 @t425)) (=> @t250 (=> @t249 (=> (forall @t307 (=> @t403 (_ @t426 (_ @t352 @t57)))) (=> (forall (@list @t342) (=> (_ @t253 (_ @t278 @t342)) (_ @t426 (_ @t60 @t342)))) (_ @t426 @t425)))))))) % 0.48/0.94 (assume @p212 (forall (@list @t10 @t11 @t18 @t235) (=> @t270 (=> @t129 (_ (_ tptp.late_transitions (_ @t138 @t10)) (_ (_ @t255 @t18) @t235)))))) % 0.48/0.94 (assume @p213 (forall @t437 (=> @t436 (=> @t435 (_ (_ (_ @t434 @t276) @t430) @t427))))) % 0.48/0.94 (assume @p214 (forall @t437 (=> @t436 (=> @t435 (_ (_ (_ @t434 (_ @t438 @t276)) @t430) @t427))))) % 0.48/0.94 (assume @p215 (forall (@list @t11 @t80 @t439) (= (_ (_ tptp.fresh_994967853t_unit @t11) (_ (_ tptp.produc1076565719t_unit @t80) @t439)) (and @t83 @t440)))) % 0.48/0.94 (assume @p216 (forall (@list @t11 @t80 @t197) (= (_ (_ tptp.fresh_1826856600t_name @t11) (_ (_ tptp.produc421428802t_name @t80) @t197)) (and @t83 @t441)))) % 0.48/0.94 (assume @p217 (forall (@list @t11 @t80 @t202) (= (_ (_ tptp.fresh_707692390nit_pi @t11) (_ (_ tptp.produc1806354576nit_pi @t80) @t202)) (and @t83 @t442)))) % 0.48/0.94 (assume @p218 (forall (@list @t11 @t12 @t439) (= (_ (_ tptp.fresh_90540034t_unit @t11) (_ (_ tptp.produc1785453612t_unit @t12) @t439)) (and @t89 @t440)))) % 0.48/0.94 (assume @p219 (forall (@list @t11 @t12 @t202) (= (_ (_ tptp.fresh_93646139ame_pi @t11) (_ (_ tptp.product_Pair_name_pi @t12) @t202)) (and @t89 @t442)))) % 0.48/0.94 (assume @p220 (forall (@list @t11 @t37 @t439) (= (_ (_ tptp.fresh_997779380t_unit @t11) (_ (_ tptp.produc1831798878t_unit @t37) @t439)) (and @t91 @t440)))) % 0.48/0.94 (assume @p221 (forall (@list @t11 @t37 @t197) (= (_ (_ tptp.fresh_261416607i_name @t11) (_ (_ tptp.product_Pair_pi_name @t37) @t197)) (and @t91 @t441)))) % 0.48/0.94 (assume @p222 (forall @t444 (= @t443 (and @t89 @t441)))) % 0.48/0.94 (assume @p223 (forall @t447 (= @t446 (and @t91 @t442)))) % 0.48/0.94 (assume @p224 (forall @t451 (= @t450 (and @t89 @t449)))) % 0.48/0.94 (assume @p225 (forall (@list @t197 @t453 @t452) (=> @t457 (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t456) (_ @t237 @t455))) tptp.rel)))) % 0.48/0.94 (assume @p226 (forall (@list @t197 @t453 @t417 @t452) (=> @t457 (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi (_ @t458 @t456)) (_ @t237 (_ @t458 @t455)))) tptp.rel)))) % 0.48/0.94 (assume @p227 (forall (@list @t11 @t80 @t459) (= (_ @t460 (_ (_ tptp.cons_Product_unit @t80) @t459)) (and @t83 (_ @t460 @t459))))) % 0.48/0.94 (assume @p228 (forall (@list @t11 @t84 @t461) (= (_ @t462 (_ (_ tptp.cons_P749510156_pi_pi @t84) @t461)) (and @t87 (_ @t462 @t461))))) % 0.48/0.94 (assume @p229 (forall (@list @t11 @t12 @t463) (= (_ @t464 @t465) (and @t89 (_ @t464 @t463))))) % 0.48/0.94 (assume @p230 (forall (@list @t11 @t37 @t466) (= (_ @t467 @t468) (and @t91 (_ @t467 @t466))))) % 0.48/0.94 (assume @p231 (forall (@list @t11 @t92 @t469) (= (_ @t470 (_ (_ tptp.cons_name_noption_pi @t92) @t469)) (and @t95 (_ @t470 @t469))))) % 0.48/0.94 (assume @p232 (_ (_ tptp.fresh_1376661020_pi_pi tptp.y) (_ (_ tptp.produc235456326_pi_pi tptp.x) (_ (_ tptp.product_Pair_pi_pi tptp.p) tptp.q)))) % 0.48/0.94 (assume @p233 (forall @t291 (_ @t82 tptp.product_Unity))) % 0.48/0.94 (assume @p234 (forall (@list @t197) (_ (_ tptp.fresh_1143631827t_unit @t197) tptp.product_Unity))) % 0.48/0.94 (assume @p235 (forall (@list @t471) (=> (forall (@list @t472) (_ @t471 @t472)) (_ @t471 tptp.nil_Pr743626285e_name)))) % 0.48/0.94 (assume @p236 (forall (@list @t473 @t49 @t17 @t182) (and (=> @t473 (= @t474 @t97)) (=> @t475 (= @t474 @t184))))) % 0.48/0.94 (assume @p237 (forall (@list @t473 @t49 @t26 @t187) (and (=> @t473 (= @t476 @t100)) (=> @t475 (= @t476 @t189))))) % 0.48/0.94 (assume @p238 (forall (@list @t473 @t49 @t30 @t192) (and (=> @t473 (= @t477 @t102)) (=> @t475 (= @t477 @t194))))) % 0.48/0.94 (assume @p239 (forall (@list @t473 @t49 @t12 @t197) (and (=> @t473 (= @t478 @t105)) (=> @t475 (= @t478 @t199))))) % 0.48/0.94 (assume @p240 (forall (@list @t473 @t49 @t37 @t202) (and (=> @t473 (= @t479 @t106)) (=> @t475 (= @t479 @t204))))) % 0.48/0.94 (assume @p241 (forall (@list @t17 @t182 @t49) (=> @t183 @t185))) % 0.48/0.94 (assume @p242 (forall (@list @t26 @t187 @t49) (=> @t188 @t190))) % 0.48/0.94 (assume @p243 (forall (@list @t30 @t192 @t49) (=> @t193 @t195))) % 0.48/0.94 (assume @p244 (forall (@list @t12 @t197 @t49) (=> @t198 @t200))) % 0.48/0.94 (assume @p245 (forall (@list @t37 @t202 @t49) (=> @t203 @t205))) % 0.48/0.94 (assume @p246 (forall @t186 (= (_ (_ tptp.perm_n171497387ubject @t49) (_ (_ tptp.produc1465345179ubject @t17) @t182)) (_ (_ tptp.produc1465345179ubject @t97) @t184)))) % 0.48/0.94 (assume @p247 (forall (@list @t49 @t17 @t187) (= (_ (_ tptp.perm_n1314686611reeRes @t49) (_ (_ tptp.produc242091907reeRes @t17) @t187)) (_ (_ tptp.produc242091907reeRes @t97) @t189)))) % 0.48/0.94 (assume @p248 (forall (@list @t49 @t17 @t192) (= (_ (_ tptp.perm_n1467004033pi_Rep @t49) (_ (_ tptp.produc843063281pi_Rep @t17) @t192)) (_ (_ tptp.produc843063281pi_Rep @t97) @t194)))) % 0.48/0.94 (assume @p249 (forall (@list @t49 @t17 @t197) (= (_ (_ tptp.perm_n204483300t_name @t49) (_ (_ tptp.produc1647375838t_name @t17) @t197)) (_ (_ tptp.produc1647375838t_name @t97) @t199)))) % 0.48/0.94 (assume @p250 (forall (@list @t49 @t17 @t202) (= (_ (_ tptp.perm_n359102898ect_pi @t49) (_ (_ tptp.produc324947500ect_pi @t17) @t202)) (_ (_ tptp.produc324947500ect_pi @t97) @t204)))) % 0.48/0.94 (assume @p251 (forall (@list @t49 @t26 @t182) (= (_ (_ tptp.perm_n1174226579ubject @t49) (_ (_ tptp.produc320590723ubject @t26) @t182)) (_ (_ tptp.produc320590723ubject @t100) @t184)))) % 0.48/0.94 (assume @p252 (forall @t191 (= (_ (_ tptp.perm_n169932155reeRes @t49) (_ (_ tptp.produc1244821099reeRes @t26) @t187)) (_ (_ tptp.produc1244821099reeRes @t100) @t189)))) % 0.48/0.94 (assume @p253 (forall (@list @t49 @t26 @t192) (= (_ (_ tptp.perm_n840427369pi_Rep @t49) (_ (_ tptp.produc216486617pi_Rep @t26) @t192)) (_ (_ tptp.produc216486617pi_Rep @t100) @t194)))) % 0.48/0.94 (assume @p254 (forall (@list @t49 @t26 @t197) (= (_ (_ tptp.perm_n258463228s_name @t49) (_ (_ tptp.produc1701355766s_name @t26) @t197)) (_ (_ tptp.produc1701355766s_name @t100) @t199)))) % 0.48/0.94 (assume @p255 (forall (@list @t49 @t26 @t202) (= (_ (_ tptp.perm_n1211707594Res_pi @t49) (_ (_ tptp.produc1177552196Res_pi @t26) @t202)) (_ (_ tptp.produc1177552196Res_pi @t100) @t204)))) % 0.48/0.94 (assume @p256 (forall @t444 (=> @t443 @t441))) % 0.48/0.94 (assume @p257 (forall @t447 (=> @t446 @t442))) % 0.48/0.94 (assume @p258 (forall @t451 (=> @t450 @t449))) % 0.48/0.94 (assume @p259 (forall @t444 (=> @t443 @t89))) % 0.48/0.94 (assume @p260 (forall @t447 (=> @t446 @t91))) % 0.48/0.94 (assume @p261 (forall @t451 (=> @t450 @t89))) % 0.48/0.94 (assume @p262 (forall (@list @t49 @t482 @t481 @t480) (and (=> @t484 (= @t483 (_ @t96 @t481))) (=> @t485 (= @t483 (_ @t96 @t480)))))) % 0.48/0.94 (assume @p263 (forall (@list @t49 @t482 @t487 @t486) (and (=> @t484 (= @t488 (_ @t99 @t487))) (=> @t485 (= @t488 (_ @t99 @t486)))))) % 0.48/0.94 (assume @p264 (forall (@list @t49 @t482 @t490 @t489) (and (=> @t484 (= @t491 (_ @t101 @t490))) (=> @t485 (= @t491 (_ @t101 @t489)))))) % 0.48/0.94 (assume @p265 (forall (@list @t49 @t482 @t493 @t492) (and (=> @t484 (= @t494 (_ @t71 @t493))) (=> @t485 (= @t494 (_ @t71 @t492)))))) % 0.48/0.94 (assume @p266 (forall (@list @t49 @t482 @t496 @t495) (and (=> @t484 (= @t497 (_ @t50 @t496))) (=> @t485 (= @t497 (_ @t50 @t495)))))) % 0.48/0.94 (assume @p267 (forall (@list @t49 @t17 @t498) (= (_ @t499 (_ (_ tptp.cons_Late_subject @t17) @t498)) (_ (_ tptp.cons_Late_subject @t97) (_ @t499 @t498))))) % 0.48/0.94 (assume @p268 (forall (@list @t49 @t26 @t500) (= (_ @t501 (_ (_ tptp.cons_Late_freeRes @t26) @t500)) (_ (_ tptp.cons_Late_freeRes @t100) (_ @t501 @t500))))) % 0.48/0.94 (assume @p269 (forall (@list @t49 @t30 @t502) (= (_ @t503 (_ (_ tptp.cons_pi_Rep @t30) @t502)) (_ (_ tptp.cons_pi_Rep @t102) (_ @t503 @t502))))) % 0.48/0.94 (assume @p270 (forall (@list @t49 @t12 @t463) (= (_ @t504 @t465) (_ (_ tptp.cons_name @t105) (_ @t504 @t463))))) % 0.48/0.94 (assume @p271 (forall (@list @t49 @t37 @t466) (= (_ @t505 @t468) (_ (_ tptp.cons_pi @t106) (_ @t505 @t466))))) % 0.48/0.94 (assume @p272 (forall (@list @t427 @t57 @t12 @t10 @t518) (=> @t435 (=> @t524 (=> (forall @t522 (=> @t521 (=> @t520 (=> @t519 (=> (_ (_ tptp.fresh_1143631827t_unit @t310) @t518) @t517))))) @t513))))) % 0.48/0.94 (assume @p273 (forall (@list @t427 @t57 @t12 @t10 @t525) (=> @t435 (=> @t524 (=> (forall @t522 (=> @t521 (=> @t520 (=> @t519 (=> (_ (_ tptp.fresh_1376661020_pi_pi @t310) @t525) @t517))))) @t513))))) % 0.48/0.94 (assume @p274 (forall (@list @t427 @t57 @t12 @t10 @t526) (=> @t435 (=> @t524 (=> (forall @t522 (=> @t521 (=> @t520 (=> @t519 (=> (_ (_ tptp.fresh_name_name @t310) @t526) @t517))))) @t513))))) % 0.48/0.94 (assume @p275 (forall (@list @t427 @t57 @t12 @t10 @t527) (=> @t435 (=> @t524 (=> (forall @t522 (=> @t521 (=> @t520 (=> @t519 (=> (_ @t528 @t527) @t517))))) @t513))))) % 0.48/0.94 (assume @p276 (forall (@list @t427 @t57 @t10 @t518) (=> @t435 (=> (forall @t536 (=> @t535 (=> @t534 (=> @t533 (=> @t336 (=> (_ (_ tptp.fresh_1143631827t_unit @t335) @t518) @t532)))))) @t530)))) % 0.48/0.94 (assume @p277 (forall (@list @t427 @t57 @t10 @t525) (=> @t435 (=> (forall @t536 (=> @t535 (=> @t534 (=> @t533 (=> @t336 (=> (_ (_ tptp.fresh_1376661020_pi_pi @t335) @t525) @t532)))))) @t530)))) % 0.48/0.94 (assume @p278 (forall (@list @t427 @t57 @t10 @t526) (=> @t435 (=> (forall @t536 (=> @t535 (=> @t534 (=> @t533 (=> @t336 (=> (_ (_ tptp.fresh_name_name @t335) @t526) @t532)))))) @t530)))) % 0.48/0.94 (assume @p279 (forall (@list @t427 @t57 @t10 @t527) (=> @t435 (=> (forall @t536 (=> @t535 (=> @t534 (=> @t533 (=> @t336 (=> (_ @t339 @t527) @t532)))))) @t530)))) % 0.48/0.94 (assume @p280 (forall (@list @t537 @t539 @t538 @t428) (=> @t542 (=> @t541 @t540)))) % 0.48/0.94 (assume @p281 (forall (@list @t543 @t546 @t544 @t428) (=> @t549 (=> @t548 @t547)))) % 0.48/0.94 (assume @p282 (forall (@list @t550 @t553 @t551 @t428) (=> @t556 (=> @t555 @t554)))) % 0.48/0.94 (assume @p283 (forall (@list @t557 @t559 @t558 @t428) (=> @t562 (=> @t561 @t560)))) % 0.48/0.94 (assume @p284 (forall (@list @t427 @t10 @t57 @t428) (=> @t435 (=> @t564 @t563)))) % 0.48/0.94 (assume @p285 (forall (@list @t537 @t428 @t539 @t538) (=> @t542 (=> @t540 @t541)))) % 0.48/0.94 (assume @p286 (forall (@list @t543 @t428 @t546 @t544) (=> @t549 (=> @t547 @t548)))) % 0.48/0.94 (assume @p287 (forall (@list @t550 @t428 @t553 @t551) (=> @t556 (=> @t554 @t555)))) % 0.48/0.94 (assume @p288 (forall (@list @t557 @t428 @t559 @t558) (=> @t562 (=> @t560 @t561)))) % 0.48/0.94 (assume @p289 (forall (@list @t427 @t428 @t10 @t57) (=> @t435 (=> @t563 @t564)))) % 0.48/0.94 (assume @p290 (forall (@list @t427 @t10 @t57) (=> (forall (@list @t569 @t566) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi (_ (_ tptp.par @t569) @t566)) (_ @t570 @t569))) @t427)) (=> (forall (@list @t569 @t566 @t335) (=> (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t569) @t566)) @t427) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi (_ @t567 @t569)) @t568)) @t427))) (_ (_ (_ tptp.strong743114133lation @t61) @t427) (_ @t565 @t10)))))) % 0.48/0.94 (assume @p291 (forall (@list @t10 @t427 @t57 @t303 @t233) (=> @t529 (=> @t407 (exists @t307 (and @t306 (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t302) @t233)) @t427))))))) % 0.48/0.94 (assume @p292 (forall (@list @t427 @t10 @t57 @t453) (=> (forall (@list @t566 @t572 @t571) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t577) @t574)) @t427)) (=> (forall (@list @t566 @t572 @t335) (=> (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t566) @t572)) @t427) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi @t568) (_ @t567 @t572))) @t427))) (=> (forall @t576 (=> (_ @t339 @t566) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi (_ @t567 @t577)) (_ @t570 (_ @t567 @t573)))) @t427))) (=> (forall @t576 (=> (_ @t339 @t571) (_ (_ tptp.member558706512_pi_pi (_ (_ tptp.product_Pair_pi_pi (_ (_ tptp.par (_ @t567 @t575)) @t571)) (_ @t567 @t574))) @t427))) (_ (_ (_ tptp.strong743114133lation (_ (_ tptp.par @t61) @t453)) @t427) (_ @t60 (_ @t565 @t453))))))))) % 0.48/0.94 (assume @p293 (forall (@list @t10 @t427 @t57 @t276 @t12 @t233) (=> @t529 (=> @t358 (=> @t250 (exists @t307 (and @t403 (_ (_ (_ (_ (_ tptp.strong2129052853vative @t302) @t233) @t276) @t12) @t427)))))))) % 0.48/0.94 (assume @p294 (forall (@list @t57 @t10 @t427) (=> (forall (@list @t334 @t310 @t342) (=> @t521 (=> (_ @t528 @t10) (exists @t511 (and @t516 (_ (_ @t531 @t310) @t427)))))) @t530))) % 0.48/0.94 (assume @p295 (forall (@list @t283 @t287) (= (= @t578 (_ tptp.late_BoundOutputS @t287)) @t288))) % 0.48/0.94 (assume @p296 (forall @t290 (= (= @t295 (_ tptp.late_InputS @t285)) @t286))) % 0.48/0.94 (assume @p297 (forall (@list @t582 @t580 @t581 @t579) (= (= @t583 (_ (_ tptp.late_OutputR @t581) @t579)) (and (= @t582 @t581) (= @t580 @t579))))) % 0.48/0.94 (assume @p298 (forall (@list @t582 @t580) (not (= @t583 tptp.late_TauR)))) % 0.48/0.94 (assume @p299 (forall (@list @t187) (=> (forall (@list @t585 @t584) (not (= @t187 (_ (_ tptp.late_OutputR @t585) @t584)))) (= @t187 tptp.late_TauR)))) % 0.48/0.94 (assume @p300 (forall (@list @t182) (=> (forall (@list @t587) (not (= @t182 (_ tptp.late_InputS @t587)))) (not (forall (@list @t586) (not (= @t182 (_ tptp.late_BoundOutputS @t586)))))))) % 0.48/0.94 (assume @p301 (forall (@list @t70 @t283) (not (= @t295 @t578)))) % 0.48/0.94 (assume @p302 (forall (@list @t11 @t12 @t10 @t347 @t197 @t400 @t588) (=> (_ @t592 (_ @t348 @t400)) (=> @t243 (=> @t328 (=> @t248 (=> (=> (= @t347 @t251) (=> (= @t400 @t589) (_ (_ (_ @t588 @t251) @t197) @t589))) (_ (_ (_ @t588 @t347) @t197) @t400)))))))) % 0.48/0.94 (assume @p303 (forall (@list @t596 @t594 @t595 @t593) (= (= (_ (_ tptp.cons_P1213805021e_name @t596) @t594) (_ (_ tptp.cons_P1213805021e_name @t595) @t593)) (and (= @t596 @t595) (= @t594 @t593))))) % 0.48/0.94 (assume @p304 (forall (@list @t49 @t597 @t70 @t52) (= (_ @t50 (_ (_ (_ tptp.input @t597) @t70) @t52)) (_ (_ (_ tptp.input (_ @t71 @t597)) @t72) @t53)))) % 0.48/0.94 (assume @p305 (forall (@list @t393 @t392 @t376 @t229 @t228) (not (= @t598 @t230)))) % 0.48/0.94 (assume @p306 (forall (@list @t393 @t392 @t376 @t600 @t599) (not (= @t598 (_ (_ tptp.par @t600) @t599))))) % 0.48/0.94 (assume @p307 (forall (@list @t12 @t197 @t10 @t299) (not (_ (_ tptp.late_transitions (_ @t14 (_ (_ (_ tptp.input @t12) @t197) @t10))) @t299)))) % 0.48/0.94 (assume @p308 (forall (@list @t11 @t12 @t10 @t303 @t235) (not (_ @t592 @t318)))) % 0.48/0.94 (assume @p309 (forall (@list @t12 @t11 @t197 @t10 @t303 @t235) (not (_ @t601 @t318)))) % 0.48/0.94 (assume @p310 (forall (@list @t603 @t602) (=> (_ @t603 tptp.product_Unity) (_ @t603 @t602)))) % 0.48/0.94 (assume @p311 (forall (@list @t439) (= @t439 tptp.product_Unity))) % 0.48/0.94 (assume @p312 (forall (@list @t11 @t12 @t10 @t18 @t197 @t235) (not (_ @t592 (_ (_ @t604 @t197) @t235))))) % 0.48/0.94 (assume @p313 (forall (@list @t11 @t12 @t10) @t605)) % 0.48/0.94 (assume @p314 (forall (@list @t12 @t11 @t10) (=> @t246 @t605))) % 0.48/0.94 (assume @p315 (forall (@list @t11 @t12 @t10 @t347 @t197 @t235) (=> (_ @t592 @t349) (not (_ @t74 @t347))))) % 0.48/0.94 (assume @p316 (forall (@list @t12 @t11 @t197 @t10 @t18 @t417 @t235) (not (_ @t601 (_ (_ @t604 @t417) @t235))))) % 0.48/0.94 (assume @p317 (forall (@list @t56 @t10 @t11 @t12) (=> @t227 (= @t591 (_ (_ @t590 @t56) (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ @t13 @t56)) tptp.nil_Pr743626285e_name)) @t10)))))) % 0.48/0.94 (assume @p318 (= tptp.defaul1399868459t_unit tptp.product_Unity)) % 0.48/0.94 (assume @p319 (forall (@list @t609 @t607 @t608 @t606) (= (= (_ (_ tptp.late_r347633188eR_Rep @t609) @t607) (_ (_ tptp.late_r347633188eR_Rep @t608) @t606)) (and (= @t609 @t608) (= @t607 @t606))))) % 0.48/0.94 (assume @p320 (forall (@list @t11 @t18 @t49 @t12) (= (_ (_ tptp.perm_name_name (_ @t21 @t49)) @t12) (_ @t610 @t105)))) % 0.48/0.94 (assume @p321 (forall @t148 (and (=> @t130 (= @t611 @t18)) (=> @t131 (and (=> @t146 (= @t611 @t11)) (=> @t147 (= @t611 @t56))))))) % 0.48/0.94 (assume @p322 (= tptp.swap_name2 tptp.swap_name)) % 0.48/0.94 (assume @p323 (forall (@list @t11 @t70 @t52) (= (_ @t68 @t73) (_ @t94 (_ (_ tptp.abs_fun_name_pi @t70) @t52))))) % 0.48/0.94 (assume @p324 (forall @t612 (= (_ (_ (_ tptp.if_pi false) @t37) @t202) @t202))) % 0.48/0.94 (assume @p325 (forall @t612 (= (_ (_ (_ tptp.if_pi true) @t37) @t202) @t37))) % 0.48/0.94 (assume @p326 (forall @t613 (= (_ (_ (_ tptp.if_name false) @t12) @t197) @t197))) % 0.48/0.94 (assume @p327 (forall @t613 (= (_ (_ (_ tptp.if_name true) @t12) @t197) @t12))) % 0.48/0.94 (assume @p328 (forall @t614 (= (_ (_ (_ tptp.if_pi_Rep false) @t30) @t192) @t192))) % 0.48/0.94 (assume @p329 (forall @t614 (= (_ (_ (_ tptp.if_pi_Rep true) @t30) @t192) @t30))) % 0.48/0.94 (assume @p330 (forall @t615 (= (_ (_ (_ tptp.if_Late_freeRes false) @t26) @t187) @t187))) % 0.48/0.94 (assume @p331 (forall @t615 (= (_ (_ (_ tptp.if_Late_freeRes true) @t26) @t187) @t26))) % 0.48/0.94 (assume @p332 (forall (@list @t616) (or (= @t616 true) (= @t616 false)))) % 0.48/0.94 (assume @p333 (forall @t617 (= (_ (_ (_ tptp.if_Late_subject false) @t17) @t182) @t182))) % 0.48/0.94 (assume @p334 (forall @t617 (= (_ (_ (_ tptp.if_Late_subject true) @t17) @t182) @t17))) % 0.48/0.94 (assume @p335 (not (exists @t511 (and (_ (_ tptp.late_transitions @t9) (_ (_ (_ tptp.late_BoundR @t2) tptp.y) @t508)) (_ (_ (_ (_ @t514 (_ (_ tptp.perm_name_pi (_ (_ tptp.cons_P1213805021e_name (_ (_ tptp.produc1570949143e_name tptp.y) tptp.x)) tptp.nil_Pr743626285e_name)) (_ (_ tptp.par (_ (_ (_ tptp.subs tptp.p2) tptp.ya) tptp.c)) tptp.q2))) @t2) tptp.y) tptp.rel))))) % 0.48/0.94 (assume @p336 true) % 0.48/0.94 (step @p337 (= tptp.fresh_name_name @t620) :rule refl :args (@t620)) % 0.48/0.94 (step @p338 (= tptp.eqvt_pi @t623) :rule refl :args (@t623)) % 0.48/0.94 (step @p339 (= tptp.strong743114133lation @t636) :rule refl :args (@t636)) % 0.48/0.94 (step @p340 :rule eq-symm :args (@t637 @t638)) % 0.48/0.94 (step @p341 :rule cong :premises (@p340) :args (@t639)) % 0.48/0.94 (step @p342 :rule cong :premises (@p341) :args ((forall @t396 @t639))) % 0.48/0.94 (step @p343 :rule refl :args (@t638)) % 0.48/0.94 (step @p344 :rule refl :args (@t637)) % 0.48/0.94 (step @p345 :rule refl :args (@t1)) % 0.48/0.94 (step @p346 :rule cong :premises (@p345 @p344) :args ((= @t1 @t637))) % 0.48/0.94 (step @p347 :rule symm :premises (@p346)) % 0.48/0.94 (step @p348 :rule eq_resolve :premises (@p345 @p347)) % 0.48/0.94 (step @p349 :rule cong :premises (@p348 @p343) :args (@t640)) % 0.48/0.94 (step @p350 :rule cong :premises (@p349) :args (@t641)) % 0.48/0.94 (step @p351 :rule cong :premises (@p350) :args ((forall @t396 @t641))) % 0.48/0.94 (step @p352 :rule trans :premises (@p351 @p342)) % 0.48/0.94 (step @p353 :rule refl :args (@t638)) % 0.48/0.94 (step @p354 :rule symm :premises (@p2)) % 0.48/0.94 (step @p355 :rule cong :premises (@p354 @p353) :args (@t642)) % 0.48/0.94 (step @p356 :rule cong :premises (@p355) :args (@t643)) % 0.48/0.94 (step @p357 :rule cong :premises (@p356) :args ((forall @t396 @t643))) % 0.48/0.94 (step @p358 :rule trans :premises (@p357 @p352)) % 0.48/0.94 (step @p359 :rule refl :args (@t638)) % 0.48/0.94 (step @p360 :rule refl :args (@t394)) % 0.48/0.94 (step @p361 :rule cong :premises (@p360 @p359) :args ((= @t394 @t638))) % 0.48/0.94 (step @p362 :rule symm :premises (@p361)) % 0.48/0.94 (step @p363 :rule eq_resolve :premises (@p360 @p362)) % 0.48/0.94 (step @p364 :rule refl :args (tptp.late_TauR)) % 0.48/0.94 (step @p365 :rule cong :premises (@p364 @p363) :args (@t644)) % 0.48/0.94 (step @p366 :rule cong :premises (@p365) :args (@t645)) % 0.48/0.94 (step @p367 :rule cong :premises (@p366) :args ((forall @t396 @t645))) % 0.48/0.94 (step @p368 :rule eq-symm :args (@t394 tptp.late_TauR)) % 0.48/0.94 (step @p369 :rule cong :premises (@p368) :args (@t395)) % 0.48/0.94 (step @p370 :rule cong :premises (@p369) :args (@t397)) % 0.48/0.94 (step @p371 :rule trans :premises (@p370 @p367)) % 0.48/0.94 (step @p372 :rule trans :premises (@p371 @p358)) % 0.48/0.94 (step @p373 :rule eq_resolve :premises (@p197 @p372)) % 0.48/0.94 (step @p374 :rule bool-impl-false1 :args (@t646)) % 0.48/0.94 (step @p375 :rule evaluate :args ((not true))) % 0.48/0.94 (step @p376 :rule eq-refl :args (@t637)) % 0.48/0.94 (step @p377 :rule cong :premises (@p376) :args (@t647)) % 0.48/0.94 (step @p378 :rule trans :premises (@p377 @p375)) % 0.48/0.94 (step @p379 :rule refl :args (@t646)) % 0.48/0.94 (step @p380 :rule cong :premises (@p379 @p378) :args ((=> @t646 @t647))) % 0.48/0.94 (step @p381 :rule trans :premises (@p380 @p374)) % 0.48/0.94 (assume-push @p388 @t646) % 0.48/0.94 (step @p383 :rule instantiate :premises (@p373) :args ((@list tptp.ab tptp.x))) % 0.48/0.94 (step-pop @p389 :rule scope :premises (@p383)) % 0.48/0.94 (step @p384 :rule process_scope :premises (@p389) :args (@t647)) % 0.48/0.94 (step @p386 :rule eq_resolve :premises (@p384 @p381)) % 0.48/0.94 (step @p387 false :rule chain_m_resolution :premises (@p386 @p373) :args (false (@list false) (@list @t646))) % 0.48/0.94 ) % 0.48/0.94 % SZS output end Proof % 0.48/0.94 % cvc5 exiting %------------------------------------------------------------------------------