%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW474_1 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n001.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 09:05:04 AM UTC 2026 % Result : Theorem 0.49s 0.90s % Output : Proof 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW474_1 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n001.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue Jun 2 22:09:20 EDT 2026 % 0.18/0.35 % CPUTime : % 0.39/0.62 %----Proving TF0_NAR, FOF, or CNF % 0.49/0.90 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.49/0.90 % SZS status Theorem % 0.49/0.90 % SZS output start Proof % 0.49/0.90 ( % 0.49/0.90 (declare-sort tptp.fun_fu1137856163l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu2087345469l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu77875581e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1664106117_pname 0) % 0.49/0.90 (declare-sort tptp.fun_pn447269700_state 0) % 0.49/0.90 (declare-sort tptp.fun_fu1911931399l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1483785331l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu325884881l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1086940979l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu64031073l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu399576434l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_pname_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1438281908l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_option_com_com 0) % 0.49/0.90 (declare-sort tptp.bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho734851753e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_pname_com 0) % 0.49/0.90 (declare-sort tptp.fun_fu1783763359l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1690815831l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1430349052l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho2109050089l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1478462177l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu867166233l_bool 0) % 0.49/0.90 (declare-sort tptp.com 0) % 0.49/0.90 (declare-sort tptp.pname 0) % 0.49/0.90 (declare-sort tptp.fun_fu802393907l_bool 0) % 0.49/0.90 (declare-sort tptp.hoare_1848483303_state 0) % 0.49/0.90 (declare-sort tptp.fun_fu2065874474l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_co1814942666_state 0) % 0.49/0.90 (declare-sort tptp.option_com 0) % 0.49/0.90 (declare-sort tptp.fun_pname_option_com 0) % 0.49/0.90 (declare-sort tptp.fun_fu1931361878_pname 0) % 0.49/0.90 (declare-sort tptp.fun_fu891110808_pname 0) % 0.49/0.90 (declare-sort tptp.fun_fu1499449723_pname 0) % 0.49/0.90 (declare-sort tptp.fun_fu230733820_state 0) % 0.49/0.90 (declare-sort tptp.fun_fu1538259051_state 0) % 0.49/0.90 (declare-sort tptp.fun_fu1404623273_state 0) % 0.49/0.90 (declare-sort tptp.fun_fu1387033222_state 0) % 0.49/0.90 (declare-sort tptp.fun_pn422929397l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_pn1359388668l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_pn2079317538e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_pn800050071e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho872578118l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho1489168363l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho1480763635e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho585232518e_bool 0) % 0.49/0.90 (declare-sort tptp.fun_Ho862234382_pname 0) % 0.49/0.90 (declare-sort tptp.fun_pname_pname 0) % 0.49/0.90 (declare-sort tptp.fun_pn250273176l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_bo1549164019l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1171508960l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu296636465l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu947309171l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu31783638l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu931343505l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu1259080373l_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu799392094on_com 0) % 0.49/0.90 (declare-sort tptp.fun_fu549469569on_com 0) % 0.49/0.90 (declare-sort tptp.fun_bool_bool 0) % 0.49/0.90 (declare-sort tptp.fun_fu410713561e_bool 0) % 0.49/0.90 (declare-const tptp.pn tptp.pname) % 0.49/0.90 (declare-const tptp.hAPP_f2022158333l_bool (-> tptp.fun_fu296636465l_bool tptp.fun_fu1783763359l_bool tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f170941835l_bool (-> tptp.fun_fu947309171l_bool tptp.fun_Ho734851753e_bool tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f32027384l_bool (-> tptp.fun_fu1171508960l_bool tptp.fun_fu1430349052l_bool tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.hAPP_H590162869l_bool (-> tptp.fun_Ho2109050089l_bool tptp.hoare_1848483303_state tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_573322273_pname (-> tptp.fun_co1814942666_state tptp.fun_pname_com tptp.fun_pn447269700_state)) % 0.49/0.90 (declare-const tptp.hAPP_f1476298914l_bool (-> tptp.fun_fu31783638l_bool tptp.fun_pname_bool tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_923936821_pname (-> tptp.fun_option_com_com tptp.fun_pname_option_com tptp.fun_pname_com)) % 0.49/0.90 (declare-const tptp.hAPP_p393069232l_bool (-> tptp.fun_pn250273176l_bool tptp.pname tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.fTrue tptp.bool) % 0.49/0.90 (declare-const tptp.hAPP_b589554111l_bool (-> tptp.fun_bo1549164019l_bool tptp.bool tptp.fun_bool_bool)) % 0.49/0.90 (declare-const tptp.hAPP_bool_bool (-> tptp.fun_bool_bool tptp.bool tptp.bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1360064833l_bool (-> tptp.fun_fu1137856163l_bool tptp.fun_fu1783763359l_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1100692246l_bool (-> tptp.fun_fu1259080373l_bool tptp.fun_fu1137856163l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f559147733l_bool (-> tptp.fun_fu2087345469l_bool tptp.fun_fu1430349052l_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1988546018l_bool (-> tptp.fun_fu931343505l_bool tptp.fun_fu2087345469l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f617245717e_bool (-> tptp.fun_fu77875581e_bool tptp.fun_Ho734851753e_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1803918242l_bool (-> tptp.fun_Ho1489168363l_bool tptp.fun_fu77875581e_bool)) % 0.49/0.90 (declare-const tptp.fdisj tptp.fun_bo1549164019l_bool) % 0.49/0.90 (declare-const tptp.hAPP_f759274231e_bool (-> tptp.fun_fu410713561e_bool tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1058051404l_bool (-> tptp.fun_pn422929397l_bool tptp.fun_fu410713561e_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_1356070853e_bool (-> tptp.fun_bool_bool tptp.fun_fu1783763359l_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.fequal1145749800e_bool tptp.fun_fu1478462177l_bool) % 0.49/0.90 (declare-const tptp.cOMBB_307249310e_bool (-> tptp.fun_bool_bool tptp.fun_fu1430349052l_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.fequal533582459e_bool tptp.fun_fu802393907l_bool) % 0.49/0.90 (declare-const tptp.cOMBB_1397003211_state (-> tptp.fun_bool_bool tptp.fun_Ho734851753e_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1947058646e_bool (-> tptp.fun_Ho1480763635e_bool tptp.fun_Ho1480763635e_bool)) % 0.49/0.90 (declare-const tptp.fequal364418600_state tptp.fun_Ho1480763635e_bool) % 0.49/0.90 (declare-const tptp.fimplies tptp.fun_bo1549164019l_bool) % 0.49/0.90 (declare-const tptp.cOMBB_647938656_pname (-> tptp.fun_bool_bool tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.fNot tptp.fun_bool_bool) % 0.49/0.90 (declare-const tptp.cOMBC_1149511130e_bool (-> tptp.fun_pn800050071e_bool tptp.fun_pn800050071e_bool)) % 0.49/0.90 (declare-const tptp.fequal_pname tptp.fun_pn800050071e_bool) % 0.49/0.90 (declare-const tptp.cOMBK_bool_pname (-> tptp.bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_2059960192_state (-> tptp.bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_1857069011e_bool (-> tptp.bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_2110745040e_bool (-> tptp.bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_2014663096l_bool (-> tptp.bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.fFalse tptp.bool) % 0.49/0.90 (declare-const tptp.hAPP_pname_bool (-> tptp.fun_pname_bool tptp.pname tptp.bool)) % 0.49/0.90 (declare-const tptp.hAPP_H2060173127e_bool (-> tptp.fun_Ho734851753e_bool tptp.hoare_1848483303_state tptp.bool)) % 0.49/0.90 (declare-const tptp.hAPP_p675228438_state (-> tptp.fun_pn447269700_state tptp.pname tptp.hoare_1848483303_state)) % 0.49/0.90 (declare-const tptp.hAPP_f50667184_pname (-> tptp.fun_fu891110808_pname tptp.fun_Ho734851753e_bool tptp.pname)) % 0.49/0.90 (declare-const tptp.hAPP_f1297739591_pname (-> tptp.fun_fu1499449723_pname tptp.fun_pname_bool tptp.pname)) % 0.49/0.90 (declare-const tptp.hAPP_pname_pname (-> tptp.fun_pname_pname tptp.pname tptp.pname)) % 0.49/0.90 (declare-const tptp.hAPP_H1494965722_pname (-> tptp.fun_Ho862234382_pname tptp.hoare_1848483303_state tptp.pname)) % 0.49/0.90 (declare-const tptp.hAPP_f2099317627_state (-> tptp.fun_fu1404623273_state tptp.fun_Ho734851753e_bool tptp.hoare_1848483303_state)) % 0.49/0.90 (declare-const tptp.hAPP_f141816996_state (-> tptp.fun_fu1387033222_state tptp.fun_pname_bool tptp.hoare_1848483303_state)) % 0.49/0.90 (declare-const tptp.hAPP_p276714170e_bool (-> tptp.fun_pn2079317538e_bool tptp.pname tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.image_1283814551_pname (-> tptp.fun_fu1499449723_pname tptp.fun_fu1430349052l_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.image_1256224870_state (-> tptp.fun_pn447269700_state tptp.fun_pname_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.collec2020384458l_bool (-> tptp.fun_fu64031073l_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.image_1825746272_pname (-> tptp.fun_fu891110808_pname tptp.fun_fu1783763359l_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f511954751l_bool (-> tptp.fun_fu1483785331l_bool tptp.fun_fu1783763359l_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_80545690l_bool (-> tptp.fun_fu1478462177l_bool tptp.fun_fu1478462177l_bool)) % 0.49/0.90 (declare-const tptp.ord_le1819283413l_bool tptp.fun_fu1483785331l_bool) % 0.49/0.90 (declare-const tptp.image_2078273054_state (-> tptp.fun_fu230733820_state tptp.fun_fu399576434l_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1359865257l_bool (-> tptp.fun_fu1690815831l_bool tptp.fun_fu64031073l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1690116422l_bool (-> tptp.fun_fu1483785331l_bool tptp.fun_fu1483785331l_bool)) % 0.49/0.90 (declare-const tptp.finite181314444l_bool tptp.fun_fu1690815831l_bool) % 0.49/0.90 (declare-const tptp.ord_le675606854l_bool tptp.fun_fu1911931399l_bool) % 0.49/0.90 (declare-const tptp.hAPP_f844837559l_bool (-> tptp.fun_fu867166233l_bool tptp.fun_fu1690815831l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.member_pname tptp.fun_pn422929397l_bool) % 0.49/0.90 (declare-const tptp.cOMBK_pname_pname (-> tptp.pname tptp.fun_pname_pname)) % 0.49/0.90 (declare-const tptp.image_2036190066_pname (-> tptp.fun_fu1931361878_pname tptp.fun_fu64031073l_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1607907235l_bool (-> tptp.fun_fu325884881l_bool tptp.fun_fu64031073l_bool tptp.fun_fu1690815831l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_336095980l_bool (-> tptp.fun_fu1086940979l_bool tptp.fun_fu1086940979l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f510955609l_bool (-> tptp.fun_fu1911931399l_bool tptp.fun_fu1430349052l_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_1420373658l_bool (-> tptp.fun_fu325884881l_bool tptp.fun_fu325884881l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f595608956l_bool (-> tptp.fun_fu2065874474l_bool tptp.fun_fu1438281908l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.hAPP_f389811538l_bool (-> tptp.fun_fu1438281908l_bool tptp.fun_fu399576434l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.finite786885583l_bool tptp.fun_fu1438281908l_bool) % 0.49/0.90 (declare-const tptp.finite1491191519l_bool tptp.fun_fu2065874474l_bool) % 0.49/0.90 (declare-const tptp.collec792590109l_bool (-> tptp.fun_fu1438281908l_bool tptp.fun_fu1438281908l_bool)) % 0.49/0.90 (declare-const tptp.image_1705983821_pname (-> tptp.fun_fu1664106117_pname tptp.fun_fu399576434l_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1759205631l_bool (-> tptp.fun_fu1086940979l_bool tptp.fun_fu399576434l_bool tptp.fun_fu1438281908l_bool)) % 0.49/0.90 (declare-const tptp.cOMBC_7971162l_bool (-> tptp.fun_fu1911931399l_bool tptp.fun_fu1911931399l_bool)) % 0.49/0.90 (declare-const tptp.finite1393641268l_bool tptp.fun_fu867166233l_bool) % 0.49/0.90 (declare-const tptp.body tptp.fun_pname_option_com) % 0.49/0.90 (declare-const tptp.image_71018297_state (-> tptp.fun_fu1538259051_state tptp.fun_fu64031073l_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.ord_le313189616e_bool tptp.fun_fu802393907l_bool) % 0.49/0.90 (declare-const tptp.hAPP_f2138803836on_com (-> tptp.fun_fu799392094on_com tptp.fun_pname_bool tptp.option_com)) % 0.49/0.90 (declare-const tptp.hAPP_c379084956_state (-> tptp.fun_co1814942666_state tptp.com tptp.hoare_1848483303_state)) % 0.49/0.90 (declare-const tptp.cOMBC_1284144636l_bool (-> tptp.fun_fu802393907l_bool tptp.fun_fu802393907l_bool)) % 0.49/0.90 (declare-const tptp.hoare_Mirabelle_MGT tptp.fun_co1814942666_state) % 0.49/0.90 (declare-const tptp.hAPP_pname_com (-> tptp.fun_pname_com tptp.pname tptp.com)) % 0.49/0.90 (declare-const tptp.body_1 tptp.fun_pname_com) % 0.49/0.90 (declare-const tptp.hAPP_f15397171l_bool (-> tptp.fun_fu1478462177l_bool tptp.fun_Ho734851753e_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_689948150l_bool (-> tptp.fun_bo1549164019l_bool tptp.fun_fu399576434l_bool tptp.fun_fu1171508960l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_p799580910on_com (-> tptp.fun_pname_option_com tptp.pname tptp.option_com)) % 0.49/0.90 (declare-const tptp.finite595471783e_bool tptp.fun_fu399576434l_bool) % 0.49/0.90 (declare-const tptp.insert668001005_state (-> tptp.hoare_1848483303_state tptp.fun_Ho734851753e_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.ord_le1375671464l_bool tptp.fun_fu1086940979l_bool) % 0.49/0.90 (declare-const tptp.hBOOL (-> tptp.bool Bool)) % 0.49/0.90 (declare-const tptp.member799430823e_bool tptp.fun_fu931343505l_bool) % 0.49/0.90 (declare-const tptp.cOMBK_1568566301_state (-> tptp.pname tptp.fun_Ho862234382_pname)) % 0.49/0.90 (declare-const tptp.ord_le101734315l_bool tptp.fun_fu325884881l_bool) % 0.49/0.90 (declare-const tptp.hAPP_f1664156314l_bool (-> tptp.fun_fu1430349052l_bool tptp.fun_pname_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.bot_bo1649642514l_bool tptp.fun_fu1430349052l_bool) % 0.49/0.90 (declare-const tptp.collec1616186998l_bool (-> tptp.fun_fu1690815831l_bool tptp.fun_fu1690815831l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f355887345l_bool (-> tptp.fun_fu1783763359l_bool tptp.fun_Ho734851753e_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.hoare_1193527299_state (-> tptp.fun_Ho734851753e_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.bot_bo454148287e_bool tptp.fun_Ho734851753e_bool) % 0.49/0.90 (declare-const tptp.the_com tptp.fun_option_com_com) % 0.49/0.90 (declare-const tptp.ord_le1119700979e_bool tptp.fun_fu1478462177l_bool) % 0.49/0.90 (declare-const tptp.hAPP_option_com_com (-> tptp.fun_option_com_com tptp.option_com tptp.com)) % 0.49/0.90 (declare-const tptp.some_com (-> tptp.com tptp.option_com)) % 0.49/0.90 (declare-const tptp.finite1765195604_state tptp.fun_fu1783763359l_bool) % 0.49/0.90 (declare-const tptp.hAPP_p338031245l_bool (-> tptp.fun_pn422929397l_bool tptp.pname tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.collec1613912337l_bool (-> tptp.fun_fu399576434l_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f434788991l_bool (-> tptp.fun_fu802393907l_bool tptp.fun_pname_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.collec1974731493e_bool (-> tptp.fun_fu1430349052l_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.finite297877756e_bool tptp.fun_fu64031073l_bool) % 0.49/0.90 (declare-const tptp.hAPP_f1935102916l_bool (-> tptp.fun_fu399576434l_bool tptp.fun_fu1430349052l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.finite_finite_pname tptp.fun_fu1430349052l_bool) % 0.49/0.90 (declare-const tptp.collec1657840446e_bool (-> tptp.fun_fu1783763359l_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1526158591l_bool (-> tptp.fun_fu64031073l_bool tptp.fun_fu1783763359l_bool tptp.bool)) % 0.49/0.90 (declare-const tptp.image_730818763_state (-> tptp.fun_fu1404623273_state tptp.fun_fu1783763359l_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.image_1916896084_state (-> tptp.fun_fu1387033222_state tptp.fun_fu1430349052l_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.image_1642285373l_bool (-> tptp.fun_pn422929397l_bool tptp.fun_pname_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.image_1820576158l_bool (-> tptp.fun_pn1359388668l_bool tptp.fun_pname_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.image_2051793258e_bool (-> tptp.fun_pn2079317538e_bool tptp.fun_pname_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.image_47868345e_bool (-> tptp.fun_pn800050071e_bool tptp.fun_pname_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.image_7400930l_bool (-> tptp.fun_Ho872578118l_bool tptp.fun_Ho734851753e_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.image_783059513l_bool (-> tptp.fun_Ho1489168363l_bool tptp.fun_Ho734851753e_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.image_249571983e_bool (-> tptp.fun_Ho1480763635e_bool tptp.fun_Ho734851753e_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.image_983321428e_bool (-> tptp.fun_Ho585232518e_bool tptp.fun_Ho734851753e_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.image_2075962154_pname (-> tptp.fun_Ho862234382_pname tptp.fun_Ho734851753e_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.image_pname_pname (-> tptp.fun_pname_pname tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.bot_bo2068035593l_bool tptp.fun_fu1783763359l_bool) % 0.49/0.90 (declare-const tptp.bot_bo844097828e_bool tptp.fun_pname_bool) % 0.49/0.90 (declare-const tptp.insert_pname (-> tptp.pname tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.insert1117693814l_bool (-> tptp.fun_fu1430349052l_bool tptp.fun_fu399576434l_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.insert1735796133l_bool (-> tptp.fun_fu1783763359l_bool tptp.fun_fu64031073l_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.insert1390540323e_bool (-> tptp.fun_Ho734851753e_bool tptp.fun_fu1783763359l_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.insert1325755072e_bool (-> tptp.fun_pname_bool tptp.fun_fu1430349052l_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.bot_bo1537088220l_bool tptp.fun_fu399576434l_bool) % 0.49/0.90 (declare-const tptp.bot_bo973295223l_bool tptp.fun_fu64031073l_bool) % 0.49/0.90 (declare-const tptp.fconj tptp.fun_bo1549164019l_bool) % 0.49/0.90 (declare-const tptp.cOMBB_675860798_pname (-> tptp.fun_bo1549164019l_bool tptp.fun_pname_bool tptp.fun_pn250273176l_bool)) % 0.49/0.90 (declare-const tptp.cOMBS_568398431l_bool (-> tptp.fun_pn250273176l_bool tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.collect_pname (-> tptp.fun_pname_bool tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_215065709_state (-> tptp.fun_bo1549164019l_bool tptp.fun_Ho734851753e_bool tptp.fun_Ho2109050089l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f636233299on_com (-> tptp.fun_fu549469569on_com tptp.fun_Ho734851753e_bool tptp.option_com)) % 0.49/0.90 (declare-const tptp.cOMBS_1990964188l_bool (-> tptp.fun_Ho2109050089l_bool tptp.fun_Ho734851753e_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.collec1708318610_state (-> tptp.fun_Ho734851753e_bool tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.cOMBS_811933079l_bool (-> tptp.fun_fu1171508960l_bool tptp.fun_fu399576434l_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_1936369445l_bool (-> tptp.fun_bo1549164019l_bool tptp.fun_fu64031073l_bool tptp.fun_fu296636465l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f1258983629l_bool (-> tptp.fun_fu1259080373l_bool tptp.fun_Ho734851753e_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.cOMBS_101732372l_bool (-> tptp.fun_fu296636465l_bool tptp.fun_fu64031073l_bool tptp.fun_fu64031073l_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_1418941603e_bool (-> tptp.fun_bo1549164019l_bool tptp.fun_fu1783763359l_bool tptp.fun_fu947309171l_bool)) % 0.49/0.90 (declare-const tptp.cOMBS_1278217668l_bool (-> tptp.fun_fu947309171l_bool tptp.fun_fu1783763359l_bool tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.cOMBB_2095475776e_bool (-> tptp.fun_bo1549164019l_bool tptp.fun_fu1430349052l_bool tptp.fun_fu31783638l_bool)) % 0.49/0.90 (declare-const tptp.cOMBS_350070575l_bool (-> tptp.fun_fu31783638l_bool tptp.fun_fu1430349052l_bool tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_240819937_pname (-> tptp.hoare_1848483303_state tptp.fun_pn447269700_state)) % 0.49/0.90 (declare-const tptp.cOMBK_1288377053_state (-> tptp.fun_pname_bool tptp.fun_Ho585232518e_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_1751623554_state (-> tptp.fun_Ho734851753e_bool tptp.fun_Ho1480763635e_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_37193422_pname (-> tptp.fun_pname_bool tptp.fun_pn800050071e_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_1197227241_pname (-> tptp.fun_Ho734851753e_bool tptp.fun_pn2079317538e_bool)) % 0.49/0.90 (declare-const tptp.cOMBK_354802397e_bool (-> tptp.hoare_1848483303_state tptp.fun_fu1387033222_state)) % 0.49/0.90 (declare-const tptp.cOMBK_1270376774e_bool (-> tptp.hoare_1848483303_state tptp.fun_fu1404623273_state)) % 0.49/0.90 (declare-const tptp.fa tptp.fun_Ho734851753e_bool) % 0.49/0.90 (declare-const tptp.cOMBK_948730864e_bool (-> tptp.pname tptp.fun_fu1499449723_pname)) % 0.49/0.90 (declare-const tptp.member591555156_state tptp.fun_Ho1489168363l_bool) % 0.49/0.90 (declare-const tptp.y tptp.com) % 0.49/0.90 (declare-const tptp.cOMBK_1423274227e_bool (-> tptp.pname tptp.fun_fu891110808_pname)) % 0.49/0.90 (declare-const tptp.member1948767740e_bool tptp.fun_fu1259080373l_bool) % 0.49/0.90 (declare-const tptp.hAPP_H1199573897l_bool (-> tptp.fun_Ho1489168363l_bool tptp.hoare_1848483303_state tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.dom_fu475558963ol_com (-> tptp.fun_fu549469569on_com tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_f556039215l_bool (-> tptp.fun_fu931343505l_bool tptp.fun_pname_bool tptp.fun_fu399576434l_bool)) % 0.49/0.90 (declare-const tptp.dom_pname_com (-> tptp.fun_pname_option_com tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.dom_fu2081503504ol_com (-> tptp.fun_fu799392094on_com tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (declare-const tptp.hAPP_H1618070847e_bool (-> tptp.fun_Ho1480763635e_bool tptp.hoare_1848483303_state tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (declare-const tptp.wt (-> tptp.com tptp.bool)) % 0.49/0.90 (declare-const tptp.wT_bodies tptp.bool) % 0.49/0.90 (declare-const tptp.hoare_1310879719gleton tptp.bool) % 0.49/0.90 (declare-const tptp.hAPP_H1355725988e_bool (-> tptp.fun_Ho585232518e_bool tptp.hoare_1848483303_state tptp.fun_pname_bool)) % 0.49/0.90 (declare-const tptp.hAPP_p61793385e_bool (-> tptp.fun_pn800050071e_bool tptp.pname tptp.fun_pname_bool)) % 0.49/0.90 (define @t1 () (@var "G" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t2 () (tptp.hoare_1193527299_state @t1)) % 0.49/0.90 (define @t3 () (@var "Ts" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t4 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 @t3))) % 0.49/0.90 (define @t5 () (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t3)) % 0.49/0.90 (define @t6 () (@var "Ts_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t7 () (@var "G_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t8 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hoare_1193527299_state @t7) @t3))) % 0.49/0.90 (define @t9 () (@list @t1 @t7 @t3)) % 0.49/0.90 (define @t10 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 @t7))) % 0.49/0.90 (define @t11 () (=> @t10 @t4)) % 0.49/0.90 (define @t12 () (forall @t9 (=> @t8 @t11))) % 0.49/0.90 (define @t13 () (@var "T" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t14 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 (tptp.insert668001005_state @t13 @t3)))) % 0.49/0.90 (define @t15 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 (tptp.insert668001005_state @t13 tptp.bot_bo454148287e_bool)))) % 0.49/0.90 (define @t16 () (@var "Pn_1" tptp.pname)) % 0.49/0.90 (define @t17 () (tptp.hAPP_c379084956_state tptp.hoare_Mirabelle_MGT (tptp.hAPP_pname_com tptp.body_1 @t16))) % 0.49/0.90 (define @t18 () (@var "A" tptp.fun_pname_bool)) % 0.49/0.90 (define @t19 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t18))) % 0.49/0.90 (define @t20 () (@list @t18)) % 0.49/0.90 (define @t21 () (@var "A" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t22 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t21))) % 0.49/0.90 (define @t23 () (@list @t21)) % 0.49/0.90 (define @t24 () (@var "A" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t25 () (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool @t24))) % 0.49/0.90 (define @t26 () (@var "A" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t27 () (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool @t26))) % 0.49/0.90 (define @t28 () (@var "A" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t29 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool @t28))) % 0.49/0.90 (define @t30 () (@list @t28)) % 0.49/0.90 (define @t31 () (@var "A" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t32 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool @t31))) % 0.49/0.90 (define @t33 () (@list @t31)) % 0.49/0.90 (define @t34 () (@var "Fa" tptp.fun_pname_bool)) % 0.49/0.90 (define @t35 () (@var "H" tptp.fun_pn447269700_state)) % 0.49/0.90 (define @t36 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t34))) % 0.49/0.90 (define @t37 () (@var "Fa" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t38 () (@var "H" tptp.fun_fu1664106117_pname)) % 0.49/0.90 (define @t39 () (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool @t37))) % 0.49/0.90 (define @t40 () (@var "Fa" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t41 () (@var "H" tptp.fun_fu1931361878_pname)) % 0.49/0.90 (define @t42 () (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool @t40))) % 0.49/0.90 (define @t43 () (@var "Fa" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t44 () (@var "H" tptp.fun_fu891110808_pname)) % 0.49/0.90 (define @t45 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool @t43))) % 0.49/0.90 (define @t46 () (@var "Fa" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t47 () (@var "H" tptp.fun_fu1499449723_pname)) % 0.49/0.90 (define @t48 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool @t46))) % 0.49/0.90 (define @t49 () (@var "H" tptp.fun_fu230733820_state)) % 0.49/0.90 (define @t50 () (@var "H" tptp.fun_fu1538259051_state)) % 0.49/0.90 (define @t51 () (@var "H" tptp.fun_fu1404623273_state)) % 0.49/0.90 (define @t52 () (@var "H" tptp.fun_fu1387033222_state)) % 0.49/0.90 (define @t53 () (@var "H" tptp.fun_pn422929397l_bool)) % 0.49/0.90 (define @t54 () (@var "H" tptp.fun_pn1359388668l_bool)) % 0.49/0.90 (define @t55 () (@var "H" tptp.fun_pn2079317538e_bool)) % 0.49/0.90 (define @t56 () (@var "H" tptp.fun_pn800050071e_bool)) % 0.49/0.90 (define @t57 () (@var "Fa" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t58 () (@var "H" tptp.fun_Ho872578118l_bool)) % 0.49/0.90 (define @t59 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t57))) % 0.49/0.90 (define @t60 () (@var "H" tptp.fun_Ho1489168363l_bool)) % 0.49/0.90 (define @t61 () (@var "H" tptp.fun_Ho1480763635e_bool)) % 0.49/0.90 (define @t62 () (@var "H" tptp.fun_Ho585232518e_bool)) % 0.49/0.90 (define @t63 () (@var "H" tptp.fun_Ho862234382_pname)) % 0.49/0.90 (define @t64 () (@var "H" tptp.fun_pname_pname)) % 0.49/0.90 (define @t65 () (@var "A_2" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t66 () (tptp.insert668001005_state @t65 @t21)) % 0.49/0.90 (define @t67 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t66))) % 0.49/0.90 (define @t68 () (@list @t65 @t21)) % 0.49/0.90 (define @t69 () (@var "A_2" tptp.pname)) % 0.49/0.90 (define @t70 () (tptp.insert_pname @t69 @t18)) % 0.49/0.90 (define @t71 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t70))) % 0.49/0.90 (define @t72 () (@list @t69 @t18)) % 0.49/0.90 (define @t73 () (@var "A_2" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t74 () (@var "A_2" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t75 () (@var "A_2" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t76 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.insert1390540323e_bool @t75 @t28)))) % 0.49/0.90 (define @t77 () (@list @t75 @t28)) % 0.49/0.90 (define @t78 () (@var "A_2" tptp.fun_pname_bool)) % 0.49/0.90 (define @t79 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.insert1325755072e_bool @t78 @t31)))) % 0.49/0.90 (define @t80 () (@list @t78 @t31)) % 0.49/0.90 (define @t81 () (@var "Q_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t82 () (@var "P_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t83 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.collect_pname @t81)))) % 0.49/0.90 (define @t84 () (tptp.collect_pname @t82)) % 0.49/0.90 (define @t85 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t84))) % 0.49/0.90 (define @t86 () (@var "Q_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t87 () (@var "P_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t88 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.collec1708318610_state @t86)))) % 0.49/0.90 (define @t89 () (tptp.collec1708318610_state @t87)) % 0.49/0.90 (define @t90 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t89))) % 0.49/0.90 (define @t91 () (@var "Q_1" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t92 () (@var "P_1" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t93 () (tptp.collec1613912337l_bool @t92)) % 0.49/0.90 (define @t94 () (@var "Q_1" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t95 () (@var "P_1" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t96 () (tptp.collec2020384458l_bool @t95)) % 0.49/0.90 (define @t97 () (@var "Q_1" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t98 () (@var "P_1" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t99 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.collec1657840446e_bool @t97)))) % 0.49/0.90 (define @t100 () (tptp.collec1657840446e_bool @t98)) % 0.49/0.90 (define @t101 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool @t100))) % 0.49/0.90 (define @t102 () (@var "Q_1" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t103 () (@var "P_1" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t104 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.collec1974731493e_bool @t102)))) % 0.49/0.90 (define @t105 () (tptp.collec1974731493e_bool @t103)) % 0.49/0.90 (define @t106 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool @t105))) % 0.49/0.90 (define @t107 () (@var "C_1" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t108 () (tptp.insert668001005_state @t107 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t109 () (tptp.image_1256224870_state (tptp.cOMBK_240819937_pname @t107) @t18)) % 0.49/0.90 (define @t110 () (= @t109 @t108)) % 0.49/0.90 (define @t111 () (= @t18 tptp.bot_bo844097828e_bool)) % 0.49/0.90 (define @t112 () (not @t111)) % 0.49/0.90 (define @t113 () (@var "C_1" tptp.pname)) % 0.49/0.90 (define @t114 () (tptp.insert_pname @t113 tptp.bot_bo844097828e_bool)) % 0.49/0.90 (define @t115 () (tptp.image_2075962154_pname (tptp.cOMBK_1568566301_state @t113) @t21)) % 0.49/0.90 (define @t116 () (= @t115 @t114)) % 0.49/0.90 (define @t117 () (= @t21 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t118 () (not @t117)) % 0.49/0.90 (define @t119 () (@var "C_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t120 () (tptp.insert1325755072e_bool @t119 tptp.bot_bo1649642514l_bool)) % 0.49/0.90 (define @t121 () (tptp.image_983321428e_bool (tptp.cOMBK_1288377053_state @t119) @t21)) % 0.49/0.90 (define @t122 () (= @t121 @t120)) % 0.49/0.90 (define @t123 () (@var "C_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t124 () (tptp.insert1390540323e_bool @t123 tptp.bot_bo2068035593l_bool)) % 0.49/0.90 (define @t125 () (tptp.image_249571983e_bool (tptp.cOMBK_1751623554_state @t123) @t21)) % 0.49/0.90 (define @t126 () (= @t125 @t124)) % 0.49/0.90 (define @t127 () (tptp.image_47868345e_bool (tptp.cOMBK_37193422_pname @t119) @t18)) % 0.49/0.90 (define @t128 () (= @t127 @t120)) % 0.49/0.90 (define @t129 () (tptp.image_2051793258e_bool (tptp.cOMBK_1197227241_pname @t123) @t18)) % 0.49/0.90 (define @t130 () (= @t129 @t124)) % 0.49/0.90 (define @t131 () (tptp.image_pname_pname (tptp.cOMBK_pname_pname @t113) @t18)) % 0.49/0.90 (define @t132 () (= @t131 @t114)) % 0.49/0.90 (define @t133 () (tptp.image_1916896084_state (tptp.cOMBK_354802397e_bool @t107) @t31)) % 0.49/0.90 (define @t134 () (= @t133 @t108)) % 0.49/0.90 (define @t135 () (= @t31 tptp.bot_bo1649642514l_bool)) % 0.49/0.90 (define @t136 () (not @t135)) % 0.49/0.90 (define @t137 () (tptp.image_730818763_state (tptp.cOMBK_1270376774e_bool @t107) @t28)) % 0.49/0.90 (define @t138 () (= @t137 @t108)) % 0.49/0.90 (define @t139 () (= @t28 tptp.bot_bo2068035593l_bool)) % 0.49/0.90 (define @t140 () (not @t139)) % 0.49/0.90 (define @t141 () (tptp.image_1283814551_pname (tptp.cOMBK_948730864e_bool @t113) @t31)) % 0.49/0.90 (define @t142 () (= @t141 @t114)) % 0.49/0.90 (define @t143 () (tptp.image_1825746272_pname (tptp.cOMBK_1423274227e_bool @t113) @t28)) % 0.49/0.90 (define @t144 () (= @t143 @t114)) % 0.49/0.90 (define @t145 () (@var "X_2" tptp.pname)) % 0.49/0.90 (define @t146 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t145)) % 0.49/0.90 (define @t147 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t146 @t18))) % 0.49/0.90 (define @t148 () (@var "X_2" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t149 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t148)) % 0.49/0.90 (define @t150 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t149 @t21))) % 0.49/0.90 (define @t151 () (@var "X_2" tptp.fun_pname_bool)) % 0.49/0.90 (define @t152 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t151) @t31))) % 0.49/0.90 (define @t153 () (@var "X_2" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t154 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t153) @t28))) % 0.49/0.90 (define @t155 () (@var "F" tptp.fun_pname_option_com)) % 0.49/0.90 (define @t156 () (tptp.dom_pname_com @t155)) % 0.49/0.90 (define @t157 () (@var "Y_2" tptp.com)) % 0.49/0.90 (define @t158 () (tptp.some_com @t157)) % 0.49/0.90 (define @t159 () (@var "F" tptp.fun_fu799392094on_com)) % 0.49/0.90 (define @t160 () (tptp.dom_fu2081503504ol_com @t159)) % 0.49/0.90 (define @t161 () (@var "F" tptp.fun_fu549469569on_com)) % 0.49/0.90 (define @t162 () (tptp.dom_fu475558963ol_com @t161)) % 0.49/0.90 (define @t163 () (@var "B" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t164 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t163))) % 0.49/0.90 (define @t165 () (@var "F" tptp.fun_pn447269700_state)) % 0.49/0.90 (define @t166 () (tptp.image_1256224870_state @t165 @t18)) % 0.49/0.90 (define @t167 () (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t163)) % 0.49/0.90 (define @t168 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t166))) % 0.49/0.90 (define @t169 () (@list @t163 @t165 @t18)) % 0.49/0.90 (define @t170 () (@var "B" tptp.fun_pname_bool)) % 0.49/0.90 (define @t171 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t170))) % 0.49/0.90 (define @t172 () (@var "F" tptp.fun_fu1664106117_pname)) % 0.49/0.90 (define @t173 () (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t170)) % 0.49/0.90 (define @t174 () (@var "F" tptp.fun_fu1931361878_pname)) % 0.49/0.90 (define @t175 () (@var "F" tptp.fun_fu891110808_pname)) % 0.49/0.90 (define @t176 () (tptp.image_1825746272_pname @t175 @t28)) % 0.49/0.90 (define @t177 () (@var "F" tptp.fun_fu1499449723_pname)) % 0.49/0.90 (define @t178 () (tptp.image_1283814551_pname @t177 @t31)) % 0.49/0.90 (define @t179 () (@var "F" tptp.fun_fu230733820_state)) % 0.49/0.90 (define @t180 () (@var "F" tptp.fun_fu1538259051_state)) % 0.49/0.90 (define @t181 () (@var "F" tptp.fun_fu1404623273_state)) % 0.49/0.90 (define @t182 () (tptp.image_730818763_state @t181 @t28)) % 0.49/0.90 (define @t183 () (@var "F" tptp.fun_fu1387033222_state)) % 0.49/0.90 (define @t184 () (tptp.image_1916896084_state @t183 @t31)) % 0.49/0.90 (define @t185 () (@var "B" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t186 () (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool @t185))) % 0.49/0.90 (define @t187 () (@var "F" tptp.fun_pn422929397l_bool)) % 0.49/0.90 (define @t188 () (tptp.hAPP_f1759205631l_bool tptp.ord_le1375671464l_bool @t185)) % 0.49/0.90 (define @t189 () (@var "B" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t190 () (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool @t189))) % 0.49/0.90 (define @t191 () (@var "F" tptp.fun_pn1359388668l_bool)) % 0.49/0.90 (define @t192 () (tptp.hAPP_f1607907235l_bool tptp.ord_le101734315l_bool @t189)) % 0.49/0.90 (define @t193 () (@var "F" tptp.fun_pname_pname)) % 0.49/0.90 (define @t194 () (tptp.image_pname_pname @t193 @t18)) % 0.49/0.90 (define @t195 () (@var "B" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t196 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool @t195))) % 0.49/0.90 (define @t197 () (@var "F" tptp.fun_pn2079317538e_bool)) % 0.49/0.90 (define @t198 () (tptp.image_2051793258e_bool @t197 @t18)) % 0.49/0.90 (define @t199 () (tptp.hAPP_f511954751l_bool tptp.ord_le1819283413l_bool @t195)) % 0.49/0.90 (define @t200 () (@var "B" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t201 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool @t200))) % 0.49/0.90 (define @t202 () (@var "F" tptp.fun_pn800050071e_bool)) % 0.49/0.90 (define @t203 () (tptp.image_47868345e_bool @t202 @t18)) % 0.49/0.90 (define @t204 () (tptp.hAPP_f510955609l_bool tptp.ord_le675606854l_bool @t200)) % 0.49/0.90 (define @t205 () (@var "F" tptp.fun_Ho872578118l_bool)) % 0.49/0.90 (define @t206 () (@var "F" tptp.fun_Ho1489168363l_bool)) % 0.49/0.90 (define @t207 () (@var "F" tptp.fun_Ho862234382_pname)) % 0.49/0.90 (define @t208 () (tptp.image_2075962154_pname @t207 @t21)) % 0.49/0.90 (define @t209 () (@var "F" tptp.fun_Ho1480763635e_bool)) % 0.49/0.90 (define @t210 () (tptp.image_249571983e_bool @t209 @t21)) % 0.49/0.90 (define @t211 () (@var "F" tptp.fun_Ho585232518e_bool)) % 0.49/0.90 (define @t212 () (tptp.image_983321428e_bool @t211 @t21)) % 0.49/0.90 (define @t213 () (tptp.insert668001005_state @t148 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t214 () (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t21)) % 0.49/0.90 (define @t215 () (tptp.insert1325755072e_bool @t151 tptp.bot_bo1649642514l_bool)) % 0.49/0.90 (define @t216 () (tptp.hAPP_f510955609l_bool tptp.ord_le675606854l_bool @t31)) % 0.49/0.90 (define @t217 () (tptp.insert1390540323e_bool @t153 tptp.bot_bo2068035593l_bool)) % 0.49/0.90 (define @t218 () (tptp.hAPP_f511954751l_bool tptp.ord_le1819283413l_bool @t28)) % 0.49/0.90 (define @t219 () (tptp.insert_pname @t145 tptp.bot_bo844097828e_bool)) % 0.49/0.90 (define @t220 () (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t18)) % 0.49/0.90 (define @t221 () (@var "C_1" tptp.com)) % 0.49/0.90 (define @t222 () (tptp.insert668001005_state (tptp.hAPP_c379084956_state tptp.hoare_Mirabelle_MGT @t221) tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t223 () (tptp.hoare_1193527299_state tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t224 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t223 @t222))) % 0.49/0.90 (define @t225 () (tptp.hBOOL (tptp.wt @t221))) % 0.49/0.90 (define @t226 () (=> @t225 @t224)) % 0.49/0.90 (define @t227 () (tptp.hBOOL tptp.wT_bodies)) % 0.49/0.90 (define @t228 () (=> @t227 @t226)) % 0.49/0.90 (define @t229 () (tptp.hBOOL tptp.hoare_1310879719gleton)) % 0.49/0.90 (define @t230 () (@list @t221)) % 0.49/0.90 (define @t231 () (forall @t230 (=> @t229 @t228))) % 0.49/0.90 (define @t232 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t65)) % 0.49/0.90 (define @t233 () (@list @t65)) % 0.49/0.90 (define @t234 () (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t78)) % 0.49/0.90 (define @t235 () (@list @t78)) % 0.49/0.90 (define @t236 () (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t75)) % 0.49/0.90 (define @t237 () (@list @t75)) % 0.49/0.90 (define @t238 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t69)) % 0.49/0.90 (define @t239 () (@list @t69)) % 0.49/0.90 (define @t240 () (@var "B_1" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t241 () (tptp.insert668001005_state @t240 @t163)) % 0.49/0.90 (define @t242 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 @t241))) % 0.49/0.90 (define @t243 () (= @t65 @t240)) % 0.49/0.90 (define @t244 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 @t163))) % 0.49/0.90 (define @t245 () (@list @t240 @t65 @t163)) % 0.49/0.90 (define @t246 () (@var "B_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t247 () (= @t78 @t246)) % 0.49/0.90 (define @t248 () (@var "B_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t249 () (= @t75 @t248)) % 0.49/0.90 (define @t250 () (@var "B_1" tptp.pname)) % 0.49/0.90 (define @t251 () (tptp.insert_pname @t250 @t170)) % 0.49/0.90 (define @t252 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 @t251))) % 0.49/0.90 (define @t253 () (= @t69 @t250)) % 0.49/0.90 (define @t254 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 @t170))) % 0.49/0.90 (define @t255 () (@list @t250 @t69 @t170)) % 0.49/0.90 (define @t256 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 @t21))) % 0.49/0.90 (define @t257 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 (tptp.insert668001005_state @t240 @t21)))) % 0.49/0.90 (define @t258 () (@list @t65 @t240 @t21)) % 0.49/0.90 (define @t259 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t234 @t31))) % 0.49/0.90 (define @t260 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t236 @t28))) % 0.49/0.90 (define @t261 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 @t18))) % 0.49/0.90 (define @t262 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 (tptp.insert_pname @t250 @t18)))) % 0.49/0.90 (define @t263 () (@list @t69 @t250 @t18)) % 0.49/0.90 (define @t264 () (= @t21 @t163)) % 0.49/0.90 (define @t265 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t21))) % 0.49/0.90 (define @t266 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t163))) % 0.49/0.90 (define @t267 () (@list @t21 @t163)) % 0.49/0.90 (define @t268 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t216 @t200))) % 0.49/0.90 (define @t269 () (@list @t31 @t200)) % 0.49/0.90 (define @t270 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t218 @t195))) % 0.49/0.90 (define @t271 () (@list @t28 @t195)) % 0.49/0.90 (define @t272 () (= @t18 @t170)) % 0.49/0.90 (define @t273 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t18))) % 0.49/0.90 (define @t274 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t170))) % 0.49/0.90 (define @t275 () (@list @t18 @t170)) % 0.49/0.90 (define @t276 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t107)) % 0.49/0.90 (define @t277 () (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t119)) % 0.49/0.90 (define @t278 () (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t123)) % 0.49/0.90 (define @t279 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t113)) % 0.49/0.90 (define @t280 () (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t246)) % 0.49/0.90 (define @t281 () (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t248)) % 0.49/0.90 (define @t282 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t240)) % 0.49/0.90 (define @t283 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t250)) % 0.49/0.90 (define @t284 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t282 @t166))) % 0.49/0.90 (define @t285 () (tptp.hAPP_p675228438_state @t165 @t145)) % 0.49/0.90 (define @t286 () (= @t240 @t285)) % 0.49/0.90 (define @t287 () (@var "X_1" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t288 () (forall (@list @t287) (not (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t92 @t287))))) % 0.49/0.90 (define @t289 () (@list @t92)) % 0.49/0.90 (define @t290 () (@var "X_1" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t291 () (forall (@list @t290) (not (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t95 @t290))))) % 0.49/0.90 (define @t292 () (@list @t95)) % 0.49/0.90 (define @t293 () (@var "X_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t294 () (@list @t293)) % 0.49/0.90 (define @t295 () (forall @t294 (not (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 @t293))))) % 0.49/0.90 (define @t296 () (@list @t98)) % 0.49/0.90 (define @t297 () (@var "X_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t298 () (@list @t297)) % 0.49/0.90 (define @t299 () (forall @t298 (not (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 @t297))))) % 0.49/0.90 (define @t300 () (@list @t103)) % 0.49/0.90 (define @t301 () (@var "X_1" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t302 () (@list @t301)) % 0.49/0.90 (define @t303 () (forall @t302 (not (tptp.hBOOL (tptp.hAPP_H2060173127e_bool @t87 @t301))))) % 0.49/0.90 (define @t304 () (@list @t87)) % 0.49/0.90 (define @t305 () (@var "X_1" tptp.pname)) % 0.49/0.90 (define @t306 () (@list @t305)) % 0.49/0.90 (define @t307 () (forall @t306 (not (tptp.hBOOL (tptp.hAPP_pname_bool @t82 @t305))))) % 0.49/0.90 (define @t308 () (@list @t82)) % 0.49/0.90 (define @t309 () (tptp.hBOOL (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t297) @t31))) % 0.49/0.90 (define @t310 () (tptp.hBOOL (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t293) @t28))) % 0.49/0.90 (define @t311 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t301)) % 0.49/0.90 (define @t312 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t311 @t21))) % 0.49/0.90 (define @t313 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t305)) % 0.49/0.90 (define @t314 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t313 @t18))) % 0.49/0.90 (define @t315 () (not @t314)) % 0.49/0.90 (define @t316 () (tptp.insert_pname @t145 @t170)) % 0.49/0.90 (define @t317 () (tptp.insert_pname @t145 @t18)) % 0.49/0.90 (define @t318 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t146 @t170))) % 0.49/0.90 (define @t319 () (not @t147)) % 0.49/0.90 (define @t320 () (@list @t170 @t145 @t18)) % 0.49/0.90 (define @t321 () (tptp.insert668001005_state @t148 @t163)) % 0.49/0.90 (define @t322 () (tptp.insert668001005_state @t148 @t21)) % 0.49/0.90 (define @t323 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t149 @t163))) % 0.49/0.90 (define @t324 () (not @t150)) % 0.49/0.90 (define @t325 () (@list @t163 @t148 @t21)) % 0.49/0.90 (define @t326 () (tptp.hBOOL (tptp.hAPP_pname_bool @t18 @t145))) % 0.49/0.90 (define @t327 () (@var "Y_2" tptp.pname)) % 0.49/0.90 (define @t328 () (tptp.insert_pname @t327 @t18)) % 0.49/0.90 (define @t329 () (tptp.hBOOL (tptp.hAPP_H2060173127e_bool @t21 @t148))) % 0.49/0.90 (define @t330 () (@var "Y_2" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t331 () (tptp.insert668001005_state @t330 @t21)) % 0.49/0.90 (define @t332 () (@list @t145 @t18)) % 0.49/0.90 (define @t333 () (@list @t148 @t21)) % 0.49/0.90 (define @t334 () (tptp.cOMBC_1149511130e_bool tptp.fequal_pname)) % 0.49/0.90 (define @t335 () (tptp.hAPP_p61793385e_bool @t334 @t69)) % 0.49/0.90 (define @t336 () (tptp.cOMBC_1947058646e_bool tptp.fequal364418600_state)) % 0.49/0.90 (define @t337 () (tptp.hAPP_H1618070847e_bool @t336 @t65)) % 0.49/0.90 (define @t338 () (tptp.cOMBC_1284144636l_bool tptp.fequal533582459e_bool)) % 0.49/0.90 (define @t339 () (tptp.hAPP_f434788991l_bool @t338 @t78)) % 0.49/0.90 (define @t340 () (tptp.cOMBC_80545690l_bool tptp.fequal1145749800e_bool)) % 0.49/0.90 (define @t341 () (tptp.hAPP_f15397171l_bool @t340 @t75)) % 0.49/0.90 (define @t342 () (tptp.cOMBC_1058051404l_bool tptp.member_pname)) % 0.49/0.90 (define @t343 () (tptp.insert_pname @t69 @t170)) % 0.49/0.90 (define @t344 () (@list @t69 @t170)) % 0.49/0.90 (define @t345 () (tptp.cOMBC_1803918242l_bool tptp.member591555156_state)) % 0.49/0.90 (define @t346 () (tptp.insert668001005_state @t65 @t163)) % 0.49/0.90 (define @t347 () (@list @t65 @t163)) % 0.49/0.90 (define @t348 () (tptp.cOMBC_1988546018l_bool tptp.member799430823e_bool)) % 0.49/0.90 (define @t349 () (tptp.cOMBC_1100692246l_bool tptp.member1948767740e_bool)) % 0.49/0.90 (define @t350 () (@var "C_2" tptp.fun_pname_bool)) % 0.49/0.90 (define @t351 () (@var "C_2" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t352 () (@list @t145 @t18 @t170)) % 0.49/0.90 (define @t353 () (@list @t148 @t21 @t163)) % 0.49/0.90 (define @t354 () (@list @t165 @t145 @t18)) % 0.49/0.90 (define @t355 () (tptp.hAPP_p675228438_state @t165 @t305)) % 0.49/0.90 (define @t356 () (@var "Z" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t357 () (@var "Xa" tptp.fun_pname_bool)) % 0.49/0.90 (define @t358 () (@var "Xa" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t359 () (@var "Xa" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t360 () (@var "Xa" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t361 () (tptp.insert_pname @t250 tptp.bot_bo844097828e_bool)) % 0.49/0.90 (define @t362 () (tptp.insert_pname @t69 tptp.bot_bo844097828e_bool)) % 0.49/0.90 (define @t363 () (tptp.insert668001005_state @t240 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t364 () (tptp.insert668001005_state @t65 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t365 () (= @t250 @t69)) % 0.49/0.90 (define @t366 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t283 @t362))) % 0.49/0.90 (define @t367 () (@list @t250 @t69)) % 0.49/0.90 (define @t368 () (= @t240 @t65)) % 0.49/0.90 (define @t369 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t282 @t364))) % 0.49/0.90 (define @t370 () (@list @t240 @t65)) % 0.49/0.90 (define @t371 () (@var "D_1" tptp.pname)) % 0.49/0.90 (define @t372 () (@var "D_1" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t373 () (@list @t165 @t18)) % 0.49/0.90 (define @t374 () (@var "D" tptp.fun_pname_bool)) % 0.49/0.90 (define @t375 () (@var "D" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t376 () (tptp.image_1256224870_state @t165 @t170)) % 0.49/0.90 (define @t377 () (@var "AA" tptp.fun_pname_bool)) % 0.49/0.90 (define @t378 () (@var "M" tptp.fun_pname_option_com)) % 0.49/0.90 (define @t379 () (@var "B_1" tptp.com)) % 0.49/0.90 (define @t380 () (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fconj @t335) @t82))) % 0.49/0.90 (define @t381 () (tptp.hBOOL (tptp.hAPP_pname_bool @t82 @t69))) % 0.49/0.90 (define @t382 () (not @t381)) % 0.49/0.90 (define @t383 () (@list @t82 @t69)) % 0.49/0.90 (define @t384 () (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fconj @t337) @t87))) % 0.49/0.90 (define @t385 () (tptp.hBOOL (tptp.hAPP_H2060173127e_bool @t87 @t65))) % 0.49/0.90 (define @t386 () (not @t385)) % 0.49/0.90 (define @t387 () (@list @t87 @t65)) % 0.49/0.90 (define @t388 () (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fconj @t339) @t103))) % 0.49/0.90 (define @t389 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 @t78))) % 0.49/0.90 (define @t390 () (not @t389)) % 0.49/0.90 (define @t391 () (tptp.insert1325755072e_bool @t78 tptp.bot_bo1649642514l_bool)) % 0.49/0.90 (define @t392 () (@list @t103 @t78)) % 0.49/0.90 (define @t393 () (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fconj @t341) @t98))) % 0.49/0.90 (define @t394 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 @t75))) % 0.49/0.90 (define @t395 () (not @t394)) % 0.49/0.90 (define @t396 () (tptp.insert1390540323e_bool @t75 tptp.bot_bo2068035593l_bool)) % 0.49/0.90 (define @t397 () (@list @t98 @t75)) % 0.49/0.90 (define @t398 () (tptp.hAPP_p61793385e_bool tptp.fequal_pname @t69)) % 0.49/0.90 (define @t399 () (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fconj @t398) @t82))) % 0.49/0.90 (define @t400 () (tptp.hAPP_H1618070847e_bool tptp.fequal364418600_state @t65)) % 0.49/0.90 (define @t401 () (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fconj @t400) @t87))) % 0.49/0.90 (define @t402 () (tptp.hAPP_f434788991l_bool tptp.fequal533582459e_bool @t78)) % 0.49/0.90 (define @t403 () (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fconj @t402) @t103))) % 0.49/0.90 (define @t404 () (tptp.hAPP_f15397171l_bool tptp.fequal1145749800e_bool @t75)) % 0.49/0.90 (define @t405 () (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fconj @t404) @t98))) % 0.49/0.90 (define @t406 () (tptp.dom_pname_com tptp.body)) % 0.49/0.90 (define @t407 () (@var "B_2" tptp.com)) % 0.49/0.90 (define @t408 () (tptp.hBOOL (tptp.wt @t407))) % 0.49/0.90 (define @t409 () (@var "Pn" tptp.pname)) % 0.49/0.90 (define @t410 () (= (tptp.hAPP_p799580910on_com tptp.body @t409) (tptp.some_com @t407))) % 0.49/0.90 (define @t411 () (=> @t410 @t408)) % 0.49/0.90 (define @t412 () (@list @t409 @t407)) % 0.49/0.90 (define @t413 () (forall @t412 (=> @t227 @t411))) % 0.49/0.90 (define @t414 () (@var "F_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t415 () (@var "A_1" tptp.pname)) % 0.49/0.90 (define @t416 () (tptp.hAPP_p338031245l_bool tptp.member_pname @t415)) % 0.49/0.90 (define @t417 () (@var "F_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t418 () (@var "A_1" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t419 () (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t418)) % 0.49/0.90 (define @t420 () (@var "F_1" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t421 () (@var "A_1" tptp.fun_pname_bool)) % 0.49/0.90 (define @t422 () (tptp.hAPP_f556039215l_bool tptp.member799430823e_bool @t421)) % 0.49/0.90 (define @t423 () (@var "F_1" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t424 () (@var "A_1" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t425 () (tptp.hAPP_f1258983629l_bool tptp.member1948767740e_bool @t424)) % 0.49/0.90 (define @t426 () (@var "Y_1" tptp.com)) % 0.49/0.90 (define @t427 () (@var "P" tptp.pname)) % 0.49/0.90 (define @t428 () (@var "C" tptp.fun_pname_bool)) % 0.49/0.90 (define @t429 () (@var "Pname" tptp.pname)) % 0.49/0.90 (define @t430 () (@var "Pname_1" tptp.pname)) % 0.49/0.90 (define @t431 () (@var "P" tptp.bool)) % 0.49/0.90 (define @t432 () (tptp.hBOOL @t431)) % 0.49/0.90 (define @t433 () (not @t432)) % 0.49/0.90 (define @t434 () (tptp.hBOOL (tptp.hAPP_bool_bool tptp.fNot @t431))) % 0.49/0.90 (define @t435 () (@list @t431)) % 0.49/0.90 (define @t436 () (@var "Q" tptp.bool)) % 0.49/0.90 (define @t437 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fconj @t431) @t436))) % 0.49/0.90 (define @t438 () (tptp.hBOOL @t436)) % 0.49/0.90 (define @t439 () (not @t438)) % 0.49/0.90 (define @t440 () (@list @t436 @t431)) % 0.49/0.90 (define @t441 () (not @t437)) % 0.49/0.90 (define @t442 () (@list @t431 @t436)) % 0.49/0.90 (define @t443 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fdisj @t431) @t436))) % 0.49/0.90 (define @t444 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fimplies @t431) @t436))) % 0.49/0.90 (define @t445 () (@var "Y" tptp.pname)) % 0.49/0.90 (define @t446 () (@var "X" tptp.pname)) % 0.49/0.90 (define @t447 () (= @t446 @t445)) % 0.49/0.90 (define @t448 () (tptp.hBOOL (tptp.hAPP_pname_bool (tptp.hAPP_p61793385e_bool tptp.fequal_pname @t446) @t445))) % 0.49/0.90 (define @t449 () (@list @t446 @t445)) % 0.49/0.90 (define @t450 () (@var "Q" tptp.pname)) % 0.49/0.90 (define @t451 () (@var "Y" tptp.fun_pname_bool)) % 0.49/0.90 (define @t452 () (@var "X" tptp.fun_pname_bool)) % 0.49/0.90 (define @t453 () (= @t452 @t451)) % 0.49/0.90 (define @t454 () (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.fequal533582459e_bool @t452) @t451))) % 0.49/0.90 (define @t455 () (@list @t452 @t451)) % 0.49/0.90 (define @t456 () (@var "R" tptp.pname)) % 0.49/0.90 (define @t457 () (@var "Q" tptp.fun_pname_bool)) % 0.49/0.90 (define @t458 () (tptp.hAPP_pname_bool @t457 @t456)) % 0.49/0.90 (define @t459 () (@var "P" tptp.fun_bool_bool)) % 0.49/0.90 (define @t460 () (@var "P" tptp.fun_pn250273176l_bool)) % 0.49/0.90 (define @t461 () (@var "P" tptp.fun_pn800050071e_bool)) % 0.49/0.90 (define @t462 () (@var "P" tptp.fun_pname_bool)) % 0.49/0.90 (define @t463 () (@var "Y" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t464 () (@var "X" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t465 () (= @t464 @t463)) % 0.49/0.90 (define @t466 () (tptp.hBOOL (tptp.hAPP_H2060173127e_bool (tptp.hAPP_H1618070847e_bool tptp.fequal364418600_state @t464) @t463))) % 0.49/0.90 (define @t467 () (@list @t464 @t463)) % 0.49/0.90 (define @t468 () (@var "Q" tptp.fun_pname_option_com)) % 0.49/0.90 (define @t469 () (@var "P" tptp.fun_option_com_com)) % 0.49/0.90 (define @t470 () (@var "R" tptp.fun_pname_bool)) % 0.49/0.90 (define @t471 () (@var "Q" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t472 () (tptp.hAPP_f1664156314l_bool @t471 @t470)) % 0.49/0.90 (define @t473 () (@var "P" tptp.fun_bo1549164019l_bool)) % 0.49/0.90 (define @t474 () (@var "P" tptp.fun_fu31783638l_bool)) % 0.49/0.90 (define @t475 () (@var "P" tptp.fun_pn422929397l_bool)) % 0.49/0.90 (define @t476 () (@var "Q" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t477 () (@var "P" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t478 () (@var "Y" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t479 () (@var "X" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t480 () (= @t479 @t478)) % 0.49/0.90 (define @t481 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.fequal1145749800e_bool @t479) @t478))) % 0.49/0.90 (define @t482 () (@list @t479 @t478)) % 0.49/0.90 (define @t483 () (@var "Q" tptp.fun_pname_com)) % 0.49/0.90 (define @t484 () (@var "P" tptp.fun_co1814942666_state)) % 0.49/0.90 (define @t485 () (@var "R" tptp.hoare_1848483303_state)) % 0.49/0.90 (define @t486 () (@var "Q" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t487 () (tptp.hAPP_H2060173127e_bool @t486 @t485)) % 0.49/0.90 (define @t488 () (@var "P" tptp.fun_Ho2109050089l_bool)) % 0.49/0.90 (define @t489 () (@var "R" tptp.fun_fu1430349052l_bool)) % 0.49/0.90 (define @t490 () (@var "Q" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t491 () (tptp.hAPP_f1935102916l_bool @t490 @t489)) % 0.49/0.90 (define @t492 () (@var "P" tptp.fun_fu1171508960l_bool)) % 0.49/0.90 (define @t493 () (@var "P" tptp.fun_fu802393907l_bool)) % 0.49/0.90 (define @t494 () (@var "P" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t495 () (@var "R" tptp.fun_Ho734851753e_bool)) % 0.49/0.90 (define @t496 () (@var "Q" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t497 () (tptp.hAPP_f355887345l_bool @t496 @t495)) % 0.49/0.90 (define @t498 () (@var "P" tptp.fun_fu947309171l_bool)) % 0.49/0.90 (define @t499 () (@var "P" tptp.fun_fu931343505l_bool)) % 0.49/0.90 (define @t500 () (@var "P" tptp.fun_Ho1480763635e_bool)) % 0.49/0.90 (define @t501 () (@var "R" tptp.fun_fu1783763359l_bool)) % 0.49/0.90 (define @t502 () (@var "Q" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t503 () (tptp.hAPP_f1526158591l_bool @t502 @t501)) % 0.49/0.90 (define @t504 () (@var "P" tptp.fun_fu296636465l_bool)) % 0.49/0.90 (define @t505 () (@var "P" tptp.fun_fu1911931399l_bool)) % 0.49/0.90 (define @t506 () (@var "P" tptp.fun_Ho1489168363l_bool)) % 0.49/0.90 (define @t507 () (@var "P" tptp.fun_fu1478462177l_bool)) % 0.49/0.90 (define @t508 () (@var "R" tptp.fun_fu399576434l_bool)) % 0.49/0.90 (define @t509 () (@var "P" tptp.fun_fu1086940979l_bool)) % 0.49/0.90 (define @t510 () (@var "P" tptp.fun_fu1259080373l_bool)) % 0.49/0.90 (define @t511 () (@var "P" tptp.fun_fu1483785331l_bool)) % 0.49/0.90 (define @t512 () (@var "R" tptp.fun_fu64031073l_bool)) % 0.49/0.90 (define @t513 () (@var "P" tptp.fun_fu325884881l_bool)) % 0.49/0.90 (define @t514 () (tptp.hAPP_c379084956_state tptp.hoare_Mirabelle_MGT tptp.y)) % 0.49/0.90 (define @t515 () (= (tptp.hAPP_p799580910on_com tptp.body tptp.pn) (tptp.some_com tptp.y))) % 0.49/0.90 (define @t516 () (tptp.image_1256224870_state (tptp.cOMBB_573322273_pname tptp.hoare_Mirabelle_MGT tptp.body_1) @t406)) % 0.49/0.90 (define @t517 () (tptp.hoare_1193527299_state @t516)) % 0.49/0.90 (define @t518 () (tptp.insert668001005_state @t514 tptp.bot_bo454148287e_bool)) % 0.49/0.90 (define @t519 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t517 @t518))) % 0.49/0.90 (define @t520 () (not @t10)) % 0.49/0.90 (define @t521 () (not @t8)) % 0.49/0.90 (define @t522 () (or @t521 @t520 @t4)) % 0.49/0.90 (define @t523 () (not @t225)) % 0.49/0.90 (define @t524 () (or @t523 @t224)) % 0.49/0.90 (define @t525 () (forall @t230 @t524)) % 0.49/0.90 (define @t526 () (not @t227)) % 0.49/0.90 (define @t527 () (not @t229)) % 0.49/0.90 (define @t528 () (or @t527 @t526 @t524)) % 0.49/0.90 (define @t529 () (or @t527 @t526 @t523 @t224)) % 0.49/0.90 (define @t530 () (or @t526 @t523 @t224)) % 0.49/0.90 (define @t531 () (@list false false)) % 0.49/0.90 (define @t532 () (not @t410)) % 0.49/0.90 (define @t533 () (or @t532 @t408)) % 0.49/0.90 (define @t534 () (forall @t412 @t533)) % 0.49/0.90 (define @t535 () (or @t526 @t533)) % 0.49/0.90 (define @t536 () (or @t526 @t532 @t408)) % 0.49/0.90 (define @t537 () (tptp.hBOOL (tptp.wt tptp.y))) % 0.49/0.90 (define @t538 () (not @t515)) % 0.49/0.90 (define @t539 () (or @t538 @t537)) % 0.49/0.90 (define @t540 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t223 @t518))) % 0.49/0.90 (define @t541 () (not @t537)) % 0.49/0.90 (define @t542 () (or @t541 @t540)) % 0.49/0.90 (define @t543 () (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t517 tptp.bot_bo454148287e_bool))) % 0.49/0.90 (define @t544 () (not @t543)) % 0.49/0.90 (define @t545 () (not @t540)) % 0.49/0.90 (define @t546 () (or @t545 @t544 @t519)) % 0.49/0.90 (define @t547 () (not @t546)) % 0.49/0.90 (define @t548 () (forall @t9 @t522)) % 0.49/0.90 (assume @p1 (forall (@list @t1) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 tptp.bot_bo454148287e_bool)))) % 0.49/0.90 (assume @p2 (forall (@list @t3 @t1) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t5 @t1)) @t4))) % 0.49/0.90 (assume @p3 (forall (@list @t3 @t1 @t6) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 @t6)) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t5 @t6)) @t4)))) % 0.49/0.90 (assume @p4 (forall @t9 (=> @t8 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t7) @t1)) @t4)))) % 0.49/0.90 (assume @p5 @t12) % 0.49/0.90 (assume @p6 (forall (@list @t3 @t1 @t13) (=> @t15 (=> @t4 @t14)))) % 0.49/0.90 (assume @p7 (forall (@list @t1 @t13 @t3) (=> @t14 (and @t15 @t4)))) % 0.49/0.90 (assume @p8 (forall (@list @t16 @t1) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hoare_1193527299_state (tptp.insert668001005_state @t17 @t1)) (tptp.insert668001005_state (tptp.hAPP_c379084956_state tptp.hoare_Mirabelle_MGT (tptp.hAPP_option_com_com tptp.the_com (tptp.hAPP_p799580910on_com tptp.body @t16))) tptp.bot_bo454148287e_bool))) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 (tptp.insert668001005_state @t17 tptp.bot_bo454148287e_bool)))))) % 0.49/0.90 (assume @p9 (forall @t20 (=> @t19 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.collec1974731493e_bool (tptp.hAPP_f434788991l_bool (tptp.cOMBC_1284144636l_bool tptp.ord_le313189616e_bool) @t18))))))) % 0.49/0.90 (assume @p10 (forall @t23 (=> @t22 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.collec1657840446e_bool (tptp.hAPP_f15397171l_bool (tptp.cOMBC_80545690l_bool tptp.ord_le1119700979e_bool) @t21))))))) % 0.49/0.90 (assume @p11 (forall (@list @t24) (=> @t25 (tptp.hBOOL (tptp.hAPP_f595608956l_bool tptp.finite1491191519l_bool (tptp.collec792590109l_bool (tptp.hAPP_f1759205631l_bool (tptp.cOMBC_336095980l_bool tptp.ord_le1375671464l_bool) @t24))))))) % 0.49/0.90 (assume @p12 (forall (@list @t26) (=> @t27 (tptp.hBOOL (tptp.hAPP_f844837559l_bool tptp.finite1393641268l_bool (tptp.collec1616186998l_bool (tptp.hAPP_f1607907235l_bool (tptp.cOMBC_1420373658l_bool tptp.ord_le101734315l_bool) @t26))))))) % 0.49/0.90 (assume @p13 (forall @t30 (=> @t29 (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.collec2020384458l_bool (tptp.hAPP_f511954751l_bool (tptp.cOMBC_1690116422l_bool tptp.ord_le1819283413l_bool) @t28))))))) % 0.49/0.90 (assume @p14 (forall @t33 (=> @t32 (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.collec1613912337l_bool (tptp.hAPP_f510955609l_bool (tptp.cOMBC_7971162l_bool tptp.ord_le675606854l_bool) @t31))))))) % 0.49/0.90 (assume @p15 (forall (@list @t35 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.image_1256224870_state @t35 @t34)))))) % 0.49/0.90 (assume @p16 (forall (@list @t38 @t37) (=> @t39 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_1705983821_pname @t38 @t37)))))) % 0.49/0.90 (assume @p17 (forall (@list @t41 @t40) (=> @t42 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_2036190066_pname @t41 @t40)))))) % 0.49/0.90 (assume @p18 (forall (@list @t44 @t43) (=> @t45 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_1825746272_pname @t44 @t43)))))) % 0.49/0.90 (assume @p19 (forall (@list @t47 @t46) (=> @t48 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_1283814551_pname @t47 @t46)))))) % 0.49/0.90 (assume @p20 (forall (@list @t49 @t37) (=> @t39 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.image_2078273054_state @t49 @t37)))))) % 0.49/0.90 (assume @p21 (forall (@list @t50 @t40) (=> @t42 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.image_71018297_state @t50 @t40)))))) % 0.49/0.90 (assume @p22 (forall (@list @t51 @t43) (=> @t45 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.image_730818763_state @t51 @t43)))))) % 0.49/0.90 (assume @p23 (forall (@list @t52 @t46) (=> @t48 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.image_1916896084_state @t52 @t46)))))) % 0.49/0.90 (assume @p24 (forall (@list @t53 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.image_1642285373l_bool @t53 @t34)))))) % 0.49/0.90 (assume @p25 (forall (@list @t54 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.image_1820576158l_bool @t54 @t34)))))) % 0.49/0.90 (assume @p26 (forall (@list @t55 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.image_2051793258e_bool @t55 @t34)))))) % 0.49/0.90 (assume @p27 (forall (@list @t56 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.image_47868345e_bool @t56 @t34)))))) % 0.49/0.90 (assume @p28 (forall (@list @t58 @t57) (=> @t59 (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.image_7400930l_bool @t58 @t57)))))) % 0.49/0.90 (assume @p29 (forall (@list @t60 @t57) (=> @t59 (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.image_783059513l_bool @t60 @t57)))))) % 0.49/0.90 (assume @p30 (forall (@list @t61 @t57) (=> @t59 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.image_249571983e_bool @t61 @t57)))))) % 0.49/0.90 (assume @p31 (forall (@list @t62 @t57) (=> @t59 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.image_983321428e_bool @t62 @t57)))))) % 0.49/0.90 (assume @p32 (forall (@list @t63 @t57) (=> @t59 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_2075962154_pname @t63 @t57)))))) % 0.49/0.90 (assume @p33 (forall (@list @t64 @t34) (=> @t36 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.image_pname_pname @t64 @t34)))))) % 0.49/0.90 (assume @p34 (forall @t23 (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool tptp.bot_bo454148287e_bool) @t21)))) % 0.49/0.90 (assume @p35 (forall @t33 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f510955609l_bool tptp.ord_le675606854l_bool tptp.bot_bo1649642514l_bool) @t31)))) % 0.49/0.90 (assume @p36 (forall @t30 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f511954751l_bool tptp.ord_le1819283413l_bool tptp.bot_bo2068035593l_bool) @t28)))) % 0.49/0.90 (assume @p37 (forall @t20 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool tptp.bot_bo844097828e_bool) @t18)))) % 0.49/0.90 (assume @p38 (forall @t68 (=> @t22 @t67))) % 0.49/0.90 (assume @p39 (forall @t72 (=> @t19 @t71))) % 0.49/0.90 (assume @p40 (forall (@list @t73 @t24) (=> @t25 (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.insert1117693814l_bool @t73 @t24)))))) % 0.49/0.90 (assume @p41 (forall (@list @t74 @t26) (=> @t27 (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.insert1735796133l_bool @t74 @t26)))))) % 0.49/0.90 (assume @p42 (forall @t77 (=> @t29 @t76))) % 0.49/0.90 (assume @p43 (forall @t80 (=> @t32 @t79))) % 0.49/0.90 (assume @p44 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname tptp.bot_bo844097828e_bool))) % 0.49/0.90 (assume @p45 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state tptp.bot_bo454148287e_bool))) % 0.49/0.90 (assume @p46 (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool tptp.bot_bo1537088220l_bool))) % 0.49/0.90 (assume @p47 (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool tptp.bot_bo973295223l_bool))) % 0.49/0.90 (assume @p48 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool tptp.bot_bo2068035593l_bool))) % 0.49/0.90 (assume @p49 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool tptp.bot_bo1649642514l_bool))) % 0.49/0.90 (assume @p50 (forall (@list @t81 @t82) (=> (or @t85 @t83) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fconj @t82) @t81))))))) % 0.49/0.90 (assume @p51 (forall (@list @t86 @t87) (=> (or @t90 @t88) (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fconj @t87) @t86))))))) % 0.49/0.90 (assume @p52 (forall (@list @t91 @t92) (=> (or (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool @t93)) (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.collec1613912337l_bool @t91)))) (tptp.hBOOL (tptp.hAPP_f389811538l_bool tptp.finite786885583l_bool (tptp.collec1613912337l_bool (tptp.cOMBS_811933079l_bool (tptp.cOMBB_689948150l_bool tptp.fconj @t92) @t91))))))) % 0.49/0.90 (assume @p53 (forall (@list @t94 @t95) (=> (or (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool @t96)) (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.collec2020384458l_bool @t94)))) (tptp.hBOOL (tptp.hAPP_f1359865257l_bool tptp.finite181314444l_bool (tptp.collec2020384458l_bool (tptp.cOMBS_101732372l_bool (tptp.cOMBB_1936369445l_bool tptp.fconj @t95) @t94))))))) % 0.49/0.90 (assume @p54 (forall (@list @t97 @t98) (=> (or @t101 @t99) (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fconj @t98) @t97))))))) % 0.49/0.90 (assume @p55 (forall (@list @t102 @t103) (=> (or @t106 @t104) (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fconj @t103) @t102))))))) % 0.49/0.90 (assume @p56 (forall (@list @t107 @t18) (and (=> @t111 (= @t109 tptp.bot_bo454148287e_bool)) (=> @t112 @t110)))) % 0.49/0.90 (assume @p57 (forall (@list @t113 @t21) (and (=> @t117 (= @t115 tptp.bot_bo844097828e_bool)) (=> @t118 @t116)))) % 0.49/0.90 (assume @p58 (forall (@list @t119 @t21) (and (=> @t117 (= @t121 tptp.bot_bo1649642514l_bool)) (=> @t118 @t122)))) % 0.49/0.90 (assume @p59 (forall (@list @t123 @t21) (and (=> @t117 (= @t125 tptp.bot_bo2068035593l_bool)) (=> @t118 @t126)))) % 0.49/0.90 (assume @p60 (forall (@list @t119 @t18) (and (=> @t111 (= @t127 tptp.bot_bo1649642514l_bool)) (=> @t112 @t128)))) % 0.49/0.90 (assume @p61 (forall (@list @t123 @t18) (and (=> @t111 (= @t129 tptp.bot_bo2068035593l_bool)) (=> @t112 @t130)))) % 0.49/0.90 (assume @p62 (forall (@list @t113 @t18) (and (=> @t111 (= @t131 tptp.bot_bo844097828e_bool)) (=> @t112 @t132)))) % 0.49/0.90 (assume @p63 (forall (@list @t107 @t31) (and (=> @t135 (= @t133 tptp.bot_bo454148287e_bool)) (=> @t136 @t134)))) % 0.49/0.90 (assume @p64 (forall (@list @t107 @t28) (and (=> @t139 (= @t137 tptp.bot_bo454148287e_bool)) (=> @t140 @t138)))) % 0.49/0.90 (assume @p65 (forall (@list @t113 @t31) (and (=> @t135 (= @t141 tptp.bot_bo844097828e_bool)) (=> @t136 @t142)))) % 0.49/0.90 (assume @p66 (forall (@list @t113 @t28) (and (=> @t139 (= @t143 tptp.bot_bo844097828e_bool)) (=> @t140 @t144)))) % 0.49/0.90 (assume @p67 (forall (@list @t107 @t145 @t18) (=> @t147 @t110))) % 0.49/0.90 (assume @p68 (forall (@list @t113 @t148 @t21) (=> @t150 @t116))) % 0.49/0.90 (assume @p69 (forall (@list @t119 @t148 @t21) (=> @t150 @t122))) % 0.49/0.90 (assume @p70 (forall (@list @t123 @t148 @t21) (=> @t150 @t126))) % 0.49/0.90 (assume @p71 (forall (@list @t119 @t145 @t18) (=> @t147 @t128))) % 0.49/0.90 (assume @p72 (forall (@list @t123 @t145 @t18) (=> @t147 @t130))) % 0.49/0.90 (assume @p73 (forall (@list @t113 @t145 @t18) (=> @t147 @t132))) % 0.49/0.90 (assume @p74 (forall (@list @t107 @t151 @t31) (=> @t152 @t134))) % 0.49/0.90 (assume @p75 (forall (@list @t107 @t153 @t28) (=> @t154 @t138))) % 0.49/0.90 (assume @p76 (forall (@list @t113 @t151 @t31) (=> @t152 @t142))) % 0.49/0.90 (assume @p77 (forall (@list @t113 @t153 @t28) (=> @t154 @t144))) % 0.49/0.90 (assume @p78 (forall (@list @t155 @t145 @t157) (=> (= (tptp.hAPP_p799580910on_com @t155 @t145) @t158) (= (tptp.insert_pname @t145 @t156) @t156)))) % 0.49/0.90 (assume @p79 (forall (@list @t159 @t151 @t157) (=> (= (tptp.hAPP_f2138803836on_com @t159 @t151) @t158) (= (tptp.insert1325755072e_bool @t151 @t160) @t160)))) % 0.49/0.90 (assume @p80 (forall (@list @t161 @t153 @t157) (=> (= (tptp.hAPP_f636233299on_com @t161 @t153) @t158) (= (tptp.insert1390540323e_bool @t153 @t162) @t162)))) % 0.49/0.90 (assume @p81 (forall @t169 (=> @t19 (=> @t168 @t164)))) % 0.49/0.90 (assume @p82 (forall (@list @t170 @t172 @t24) (=> @t25 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 (tptp.image_1705983821_pname @t172 @t24))) @t171)))) % 0.49/0.90 (assume @p83 (forall (@list @t170 @t174 @t26) (=> @t27 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 (tptp.image_2036190066_pname @t174 @t26))) @t171)))) % 0.49/0.90 (assume @p84 (forall (@list @t170 @t175 @t28) (=> @t29 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t176)) @t171)))) % 0.49/0.90 (assume @p85 (forall (@list @t170 @t177 @t31) (=> @t32 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t178)) @t171)))) % 0.49/0.90 (assume @p86 (forall (@list @t163 @t179 @t24) (=> @t25 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 (tptp.image_2078273054_state @t179 @t24))) @t164)))) % 0.49/0.90 (assume @p87 (forall (@list @t163 @t180 @t26) (=> @t27 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 (tptp.image_71018297_state @t180 @t26))) @t164)))) % 0.49/0.90 (assume @p88 (forall (@list @t163 @t181 @t28) (=> @t29 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t182)) @t164)))) % 0.49/0.90 (assume @p89 (forall (@list @t163 @t183 @t31) (=> @t32 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t184)) @t164)))) % 0.49/0.90 (assume @p90 (forall (@list @t185 @t187 @t18) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f389811538l_bool @t188 (tptp.image_1642285373l_bool @t187 @t18))) @t186)))) % 0.49/0.90 (assume @p91 (forall (@list @t189 @t191 @t18) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f1359865257l_bool @t192 (tptp.image_1820576158l_bool @t191 @t18))) @t190)))) % 0.49/0.90 (assume @p92 (forall (@list @t170 @t193 @t18) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t194)) @t171)))) % 0.49/0.90 (assume @p93 (forall (@list @t195 @t197 @t18) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t199 @t198)) @t196)))) % 0.49/0.90 (assume @p94 (forall (@list @t200 @t202 @t18) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t204 @t203)) @t201)))) % 0.49/0.90 (assume @p95 (forall (@list @t185 @t205 @t21) (=> @t22 (=> (tptp.hBOOL (tptp.hAPP_f389811538l_bool @t188 (tptp.image_7400930l_bool @t205 @t21))) @t186)))) % 0.49/0.90 (assume @p96 (forall (@list @t189 @t206 @t21) (=> @t22 (=> (tptp.hBOOL (tptp.hAPP_f1359865257l_bool @t192 (tptp.image_783059513l_bool @t206 @t21))) @t190)))) % 0.49/0.90 (assume @p97 (forall (@list @t170 @t207 @t21) (=> @t22 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t208)) @t171)))) % 0.49/0.90 (assume @p98 (forall (@list @t195 @t209 @t21) (=> @t22 (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t199 @t210)) @t196)))) % 0.49/0.90 (assume @p99 (forall (@list @t200 @t211 @t21) (=> @t22 (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t204 @t212)) @t201)))) % 0.49/0.90 (assume @p100 (forall (@list @t21 @t148) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t213)) (or @t117 (= @t21 @t213))))) % 0.49/0.90 (assume @p101 (forall (@list @t31 @t151) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t216 @t215)) (or @t135 (= @t31 @t215))))) % 0.49/0.90 (assume @p102 (forall (@list @t28 @t153) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t218 @t217)) (or @t139 (= @t28 @t217))))) % 0.49/0.90 (assume @p103 (forall (@list @t18 @t145) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t219)) (or @t111 (= @t18 @t219))))) % 0.49/0.90 (assume @p104 @t231) % 0.49/0.90 (assume @p105 (forall @t233 (not (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 tptp.bot_bo454148287e_bool))))) % 0.49/0.90 (assume @p106 (forall @t235 (not (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t234 tptp.bot_bo1649642514l_bool))))) % 0.49/0.90 (assume @p107 (forall @t237 (not (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t236 tptp.bot_bo2068035593l_bool))))) % 0.49/0.90 (assume @p108 (forall @t239 (not (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 tptp.bot_bo844097828e_bool))))) % 0.49/0.90 (assume @p109 (forall @t245 (=> (=> (not @t244) @t243) @t242))) % 0.49/0.90 (assume @p110 (forall (@list @t246 @t78 @t200) (=> (=> (not (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t234 @t200))) @t247) (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t234 (tptp.insert1325755072e_bool @t246 @t200)))))) % 0.49/0.90 (assume @p111 (forall (@list @t248 @t75 @t195) (=> (=> (not (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t236 @t195))) @t249) (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t236 (tptp.insert1390540323e_bool @t248 @t195)))))) % 0.49/0.90 (assume @p112 (forall @t255 (=> (=> (not @t254) @t253) @t252))) % 0.49/0.90 (assume @p113 (forall @t258 (=> @t257 (=> (not @t243) @t256)))) % 0.49/0.90 (assume @p114 (forall (@list @t78 @t246 @t31) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t234 (tptp.insert1325755072e_bool @t246 @t31))) (=> (not @t247) @t259)))) % 0.49/0.90 (assume @p115 (forall (@list @t75 @t248 @t28) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t236 (tptp.insert1390540323e_bool @t248 @t28))) (=> (not @t249) @t260)))) % 0.49/0.90 (assume @p116 (forall @t263 (=> @t262 (=> (not @t253) @t261)))) % 0.49/0.90 (assume @p117 (forall @t267 (=> @t266 (=> @t265 @t264)))) % 0.49/0.90 (assume @p118 (forall @t269 (=> @t268 (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t204 @t31)) (= @t31 @t200))))) % 0.49/0.90 (assume @p119 (forall @t271 (=> @t270 (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t199 @t28)) (= @t28 @t195))))) % 0.49/0.90 (assume @p120 (forall @t275 (=> @t274 (=> @t273 @t272)))) % 0.49/0.90 (assume @p121 (forall (@list @t107 @t21 @t163) (=> @t266 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t276 @t21)) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t276 @t163)))))) % 0.49/0.90 (assume @p122 (forall (@list @t119 @t31 @t200) (=> @t268 (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t277 @t31)) (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t277 @t200)))))) % 0.49/0.90 (assume @p123 (forall (@list @t123 @t28 @t195) (=> @t270 (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t278 @t28)) (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t278 @t195)))))) % 0.49/0.90 (assume @p124 (forall (@list @t113 @t18 @t170) (=> @t274 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t279 @t18)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t279 @t170)))))) % 0.49/0.90 (assume @p125 (forall (@list @t21 @t246 @t211 @t148) (=> (= @t246 (tptp.hAPP_H1355725988e_bool @t211 @t148)) (=> @t150 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t280 @t212)))))) % 0.49/0.90 (assume @p126 (forall (@list @t21 @t248 @t209 @t148) (=> (= @t248 (tptp.hAPP_H1618070847e_bool @t209 @t148)) (=> @t150 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t281 @t210)))))) % 0.49/0.90 (assume @p127 (forall (@list @t18 @t246 @t202 @t145) (=> (= @t246 (tptp.hAPP_p61793385e_bool @t202 @t145)) (=> @t147 (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t280 @t203)))))) % 0.49/0.90 (assume @p128 (forall (@list @t18 @t248 @t197 @t145) (=> (= @t248 (tptp.hAPP_p276714170e_bool @t197 @t145)) (=> @t147 (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t281 @t198)))))) % 0.49/0.90 (assume @p129 (forall (@list @t31 @t240 @t183 @t151) (=> (= @t240 (tptp.hAPP_f141816996_state @t183 @t151)) (=> @t152 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t282 @t184)))))) % 0.49/0.90 (assume @p130 (forall (@list @t28 @t240 @t181 @t153) (=> (= @t240 (tptp.hAPP_f2099317627_state @t181 @t153)) (=> @t154 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t282 @t182)))))) % 0.49/0.90 (assume @p131 (forall (@list @t21 @t250 @t207 @t148) (=> (= @t250 (tptp.hAPP_H1494965722_pname @t207 @t148)) (=> @t150 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t283 @t208)))))) % 0.49/0.90 (assume @p132 (forall (@list @t18 @t250 @t193 @t145) (=> (= @t250 (tptp.hAPP_pname_pname @t193 @t145)) (=> @t147 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t283 @t194)))))) % 0.49/0.90 (assume @p133 (forall (@list @t31 @t250 @t177 @t151) (=> (= @t250 (tptp.hAPP_f1297739591_pname @t177 @t151)) (=> @t152 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t283 @t178)))))) % 0.49/0.90 (assume @p134 (forall (@list @t28 @t250 @t175 @t153) (=> (= @t250 (tptp.hAPP_f50667184_pname @t175 @t153)) (=> @t154 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t283 @t176)))))) % 0.49/0.90 (assume @p135 (forall (@list @t18 @t240 @t165 @t145) (=> @t286 (=> @t147 @t284)))) % 0.49/0.90 (assume @p136 (forall @t80 (=> @t135 (not @t259)))) % 0.49/0.90 (assume @p137 (forall @t77 (=> @t139 (not @t260)))) % 0.49/0.90 (assume @p138 (forall @t68 (=> @t117 (not @t256)))) % 0.49/0.90 (assume @p139 (forall @t72 (=> @t111 (not @t261)))) % 0.49/0.90 (assume @p140 (forall @t289 (= (= @t93 tptp.bot_bo1537088220l_bool) @t288))) % 0.49/0.90 (assume @p141 (forall @t292 (= (= @t96 tptp.bot_bo973295223l_bool) @t291))) % 0.49/0.90 (assume @p142 (forall @t296 (= (= @t100 tptp.bot_bo2068035593l_bool) @t295))) % 0.49/0.90 (assume @p143 (forall @t300 (= (= @t105 tptp.bot_bo1649642514l_bool) @t299))) % 0.49/0.90 (assume @p144 (forall @t304 (= (= @t89 tptp.bot_bo454148287e_bool) @t303))) % 0.49/0.90 (assume @p145 (forall @t308 (= (= @t84 tptp.bot_bo844097828e_bool) @t307))) % 0.49/0.90 (assume @p146 (forall (@list @t119) (not (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t277 tptp.bot_bo1649642514l_bool))))) % 0.49/0.90 (assume @p147 (forall (@list @t123) (not (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t278 tptp.bot_bo2068035593l_bool))))) % 0.49/0.90 (assume @p148 (forall (@list @t107) (not (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t276 tptp.bot_bo454148287e_bool))))) % 0.49/0.90 (assume @p149 (forall (@list @t113) (not (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t279 tptp.bot_bo844097828e_bool))))) % 0.49/0.90 (assume @p150 (forall @t289 (= (= tptp.bot_bo1537088220l_bool @t93) @t288))) % 0.49/0.90 (assume @p151 (forall @t292 (= (= tptp.bot_bo973295223l_bool @t96) @t291))) % 0.49/0.90 (assume @p152 (forall @t296 (= (= tptp.bot_bo2068035593l_bool @t100) @t295))) % 0.49/0.90 (assume @p153 (forall @t300 (= (= tptp.bot_bo1649642514l_bool @t105) @t299))) % 0.49/0.90 (assume @p154 (forall @t304 (= (= tptp.bot_bo454148287e_bool @t89) @t303))) % 0.49/0.90 (assume @p155 (forall @t308 (= (= tptp.bot_bo844097828e_bool @t84) @t307))) % 0.49/0.90 (assume @p156 (forall @t33 (= (exists @t298 @t309) @t136))) % 0.49/0.90 (assume @p157 (forall @t30 (= (exists @t294 @t310) @t140))) % 0.49/0.90 (assume @p158 (forall @t23 (= (exists @t302 @t312) @t118))) % 0.49/0.90 (assume @p159 (forall @t20 (= (exists @t306 @t314) @t112))) % 0.49/0.90 (assume @p160 (forall @t33 (= (forall @t298 (not @t309)) @t135))) % 0.49/0.90 (assume @p161 (forall @t30 (= (forall @t294 (not @t310)) @t139))) % 0.49/0.90 (assume @p162 (forall @t23 (= (forall @t302 (not @t312)) @t117))) % 0.49/0.90 (assume @p163 (forall @t20 (= (forall @t306 @t315) @t111))) % 0.49/0.90 (assume @p164 (= tptp.bot_bo973295223l_bool (tptp.collec2020384458l_bool (tptp.cOMBK_2014663096l_bool tptp.fFalse)))) % 0.49/0.90 (assume @p165 (= tptp.bot_bo2068035593l_bool (tptp.collec1657840446e_bool (tptp.cOMBK_2110745040e_bool tptp.fFalse)))) % 0.49/0.90 (assume @p166 (= tptp.bot_bo1649642514l_bool (tptp.collec1974731493e_bool (tptp.cOMBK_1857069011e_bool tptp.fFalse)))) % 0.49/0.90 (assume @p167 (= tptp.bot_bo454148287e_bool (tptp.collec1708318610_state (tptp.cOMBK_2059960192_state tptp.fFalse)))) % 0.49/0.90 (assume @p168 (= tptp.bot_bo844097828e_bool (tptp.collect_pname (tptp.cOMBK_bool_pname tptp.fFalse)))) % 0.49/0.90 (assume @p169 (forall @t72 (=> @t261 (= @t70 @t18)))) % 0.49/0.90 (assume @p170 (forall @t68 (=> @t256 (= @t66 @t21)))) % 0.49/0.90 (assume @p171 (forall @t255 (=> @t254 @t252))) % 0.49/0.90 (assume @p172 (forall @t245 (=> @t244 @t242))) % 0.49/0.90 (assume @p173 (forall @t320 (=> @t319 (=> (not @t318) (= (= @t317 @t316) @t272))))) % 0.49/0.90 (assume @p174 (forall @t325 (=> @t324 (=> (not @t323) (= (= @t322 @t321) @t264))))) % 0.49/0.90 (assume @p175 (forall (@list @t327 @t18 @t145) (= (tptp.hBOOL (tptp.hAPP_pname_bool @t328 @t145)) (or (= @t327 @t145) @t326)))) % 0.49/0.90 (assume @p176 (forall (@list @t330 @t21 @t148) (= (tptp.hBOOL (tptp.hAPP_H2060173127e_bool @t331 @t148)) (or (= @t330 @t148) @t329)))) % 0.49/0.90 (assume @p177 (forall @t263 (= @t262 (or @t253 @t261)))) % 0.49/0.90 (assume @p178 (forall @t258 (= @t257 (or @t243 @t256)))) % 0.49/0.90 (assume @p179 (forall (@list @t145 @t327 @t18) (= (tptp.insert_pname @t145 @t328) (tptp.insert_pname @t327 @t317)))) % 0.49/0.90 (assume @p180 (forall (@list @t148 @t330 @t21) (= (tptp.insert668001005_state @t148 @t331) (tptp.insert668001005_state @t330 @t322)))) % 0.49/0.90 (assume @p181 (forall @t332 (= (tptp.insert_pname @t145 @t317) @t317))) % 0.49/0.90 (assume @p182 (forall @t333 (= (tptp.insert668001005_state @t148 @t322) @t322))) % 0.49/0.90 (assume @p183 (forall (@list @t69 @t82) (= (tptp.insert_pname @t69 @t84) (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fimplies (tptp.cOMBB_647938656_pname tptp.fNot @t335)) @t82))))) % 0.49/0.90 (assume @p184 (forall (@list @t65 @t87) (= (tptp.insert668001005_state @t65 @t89) (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fimplies (tptp.cOMBB_1397003211_state tptp.fNot @t337)) @t87))))) % 0.49/0.90 (assume @p185 (forall (@list @t78 @t103) (= (tptp.insert1325755072e_bool @t78 @t105) (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fimplies (tptp.cOMBB_307249310e_bool tptp.fNot @t339)) @t103))))) % 0.49/0.90 (assume @p186 (forall (@list @t75 @t98) (= (tptp.insert1390540323e_bool @t75 @t100) (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fimplies (tptp.cOMBB_1356070853e_bool tptp.fNot @t341)) @t98))))) % 0.49/0.90 (assume @p187 (forall @t344 (= @t343 (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fdisj @t335) (tptp.hAPP_f759274231e_bool @t342 @t170)))))) % 0.49/0.90 (assume @p188 (forall @t347 (= @t346 (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fdisj @t337) (tptp.hAPP_f617245717e_bool @t345 @t163)))))) % 0.49/0.90 (assume @p189 (forall (@list @t78 @t200) (= (tptp.insert1325755072e_bool @t78 @t200) (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fdisj @t339) (tptp.hAPP_f559147733l_bool @t348 @t200)))))) % 0.49/0.90 (assume @p190 (forall (@list @t75 @t195) (= (tptp.insert1390540323e_bool @t75 @t195) (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fdisj @t341) (tptp.hAPP_f1360064833l_bool @t349 @t195)))))) % 0.49/0.90 (assume @p191 (forall @t344 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 @t343)))) % 0.49/0.90 (assume @p192 (forall @t347 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t232 @t346)))) % 0.49/0.90 (assume @p193 (forall @t275 (=> @t272 (not (=> @t274 (not @t273)))))) % 0.49/0.90 (assume @p194 (forall @t267 (=> @t264 (not (=> @t266 (not @t265)))))) % 0.49/0.90 (assume @p195 (forall (@list @t350 @t18 @t170) (=> @t274 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t350)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t350)))))) % 0.49/0.90 (assume @p196 (forall (@list @t351 @t21 @t163) (=> @t266 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t351)) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t351)))))) % 0.49/0.90 (assume @p197 (forall @t352 (=> @t274 (=> @t147 @t318)))) % 0.49/0.90 (assume @p198 (forall @t353 (=> @t266 (=> @t150 @t323)))) % 0.49/0.90 (assume @p199 (forall @t320 (=> @t147 (=> @t274 @t318)))) % 0.49/0.90 (assume @p200 (forall @t325 (=> @t150 (=> @t266 @t323)))) % 0.49/0.90 (assume @p201 (forall @t275 (=> @t272 @t273))) % 0.49/0.90 (assume @p202 (forall @t267 (=> @t264 @t265))) % 0.49/0.90 (assume @p203 (forall @t275 (=> @t272 @t274))) % 0.49/0.90 (assume @p204 (forall @t267 (=> @t264 @t266))) % 0.49/0.90 (assume @p205 (forall @t275 (= @t272 (and @t274 @t273)))) % 0.49/0.90 (assume @p206 (forall @t267 (= @t264 (and @t266 @t265)))) % 0.49/0.90 (assume @p207 (forall @t20 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t18)))) % 0.49/0.90 (assume @p208 (forall @t23 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t21)))) % 0.49/0.90 (assume @p209 (forall (@list @t240 @t165 @t145 @t18) (=> @t147 (=> @t286 @t284)))) % 0.49/0.90 (assume @p210 (forall @t354 (=> @t147 (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t285) @t166))))) % 0.49/0.90 (assume @p211 (forall (@list @t356 @t165 @t18) (= (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t356) @t166)) (exists @t306 (and @t314 (= @t356 @t355)))))) % 0.49/0.90 (assume @p212 (forall (@list @t82 @t81) (= (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fdisj @t82) @t81)))) (and @t85 @t83)))) % 0.49/0.90 (assume @p213 (forall (@list @t87 @t86) (= (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fdisj @t87) @t86)))) (and @t90 @t88)))) % 0.49/0.90 (assume @p214 (forall (@list @t103 @t102) (= (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fdisj @t103) @t102)))) (and @t106 @t104)))) % 0.49/0.90 (assume @p215 (forall (@list @t98 @t97) (= (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fdisj @t98) @t97)))) (and @t101 @t99)))) % 0.49/0.90 (assume @p216 (forall (@list @t305 @t357) (= (tptp.insert_pname @t305 @t357) (tptp.collect_pname (tptp.cOMBS_568398431l_bool (tptp.cOMBB_675860798_pname tptp.fdisj (tptp.hAPP_p61793385e_bool @t334 @t305)) (tptp.hAPP_f759274231e_bool @t342 @t357)))))) % 0.49/0.90 (assume @p217 (forall (@list @t301 @t358) (= (tptp.insert668001005_state @t301 @t358) (tptp.collec1708318610_state (tptp.cOMBS_1990964188l_bool (tptp.cOMBB_215065709_state tptp.fdisj (tptp.hAPP_H1618070847e_bool @t336 @t301)) (tptp.hAPP_f617245717e_bool @t345 @t358)))))) % 0.49/0.90 (assume @p218 (forall (@list @t297 @t359) (= (tptp.insert1325755072e_bool @t297 @t359) (tptp.collec1974731493e_bool (tptp.cOMBS_350070575l_bool (tptp.cOMBB_2095475776e_bool tptp.fdisj (tptp.hAPP_f434788991l_bool @t338 @t297)) (tptp.hAPP_f559147733l_bool @t348 @t359)))))) % 0.49/0.90 (assume @p219 (forall (@list @t293 @t360) (= (tptp.insert1390540323e_bool @t293 @t360) (tptp.collec1657840446e_bool (tptp.cOMBS_1278217668l_bool (tptp.cOMBB_1418941603e_bool tptp.fdisj (tptp.hAPP_f15397171l_bool @t340 @t293)) (tptp.hAPP_f1360064833l_bool @t349 @t360)))))) % 0.49/0.90 (assume @p220 (forall (@list @t69 @t250) (=> (= @t362 @t361) @t253))) % 0.49/0.90 (assume @p221 (forall (@list @t65 @t240) (=> (= @t364 @t363) @t243))) % 0.49/0.90 (assume @p222 (forall @t367 (=> @t366 @t365))) % 0.49/0.90 (assume @p223 (forall @t370 (=> @t369 @t368))) % 0.49/0.90 (assume @p224 (forall (@list @t69 @t250 @t113 @t371) (= (= (tptp.insert_pname @t69 @t361) (tptp.insert_pname @t113 (tptp.insert_pname @t371 tptp.bot_bo844097828e_bool))) (or (and (= @t69 @t113) (= @t250 @t371)) (and (= @t69 @t371) (= @t250 @t113)))))) % 0.49/0.90 (assume @p225 (forall (@list @t65 @t240 @t107 @t372) (= (= (tptp.insert668001005_state @t65 @t363) (tptp.insert668001005_state @t107 (tptp.insert668001005_state @t372 tptp.bot_bo454148287e_bool))) (or (and (= @t65 @t107) (= @t240 @t372)) (and (= @t65 @t372) (= @t240 @t107)))))) % 0.49/0.90 (assume @p226 (forall @t367 (= @t366 @t365))) % 0.49/0.90 (assume @p227 (forall @t370 (= @t369 @t368))) % 0.49/0.90 (assume @p228 (forall @t72 (not (= @t70 tptp.bot_bo844097828e_bool)))) % 0.49/0.90 (assume @p229 (forall @t68 (not (= @t66 tptp.bot_bo454148287e_bool)))) % 0.49/0.90 (assume @p230 (forall @t72 (not (= tptp.bot_bo844097828e_bool @t70)))) % 0.49/0.90 (assume @p231 (forall @t68 (not (= tptp.bot_bo454148287e_bool @t66)))) % 0.49/0.90 (assume @p232 (forall @t72 (= @t71 @t19))) % 0.49/0.90 (assume @p233 (forall @t68 (= @t67 @t22))) % 0.49/0.90 (assume @p234 (forall @t80 (= @t79 @t32))) % 0.49/0.90 (assume @p235 (forall @t77 (= @t76 @t29))) % 0.49/0.90 (assume @p236 (forall @t20 (= (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 tptp.bot_bo844097828e_bool)) @t111))) % 0.49/0.90 (assume @p237 (forall @t23 (= (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 tptp.bot_bo454148287e_bool)) @t117))) % 0.49/0.90 (assume @p238 (forall @t373 (= (= @t166 tptp.bot_bo454148287e_bool) @t111))) % 0.49/0.90 (assume @p239 (forall (@list @t165) (= (tptp.image_1256224870_state @t165 tptp.bot_bo844097828e_bool) tptp.bot_bo454148287e_bool))) % 0.49/0.90 (assume @p240 (forall @t373 (= (= tptp.bot_bo454148287e_bool @t166) @t111))) % 0.49/0.90 (assume @p241 (forall @t269 (=> @t268 (=> @t201 @t32)))) % 0.49/0.90 (assume @p242 (forall @t271 (=> @t270 (=> @t196 @t29)))) % 0.49/0.90 (assume @p243 (forall @t275 (=> @t274 (=> @t171 @t19)))) % 0.49/0.90 (assume @p244 (forall @t267 (=> @t266 (=> @t164 @t22)))) % 0.49/0.90 (assume @p245 (forall @t269 (=> @t201 (=> @t268 @t32)))) % 0.49/0.90 (assume @p246 (forall @t271 (=> @t196 (=> @t270 @t29)))) % 0.49/0.90 (assume @p247 (forall @t275 (=> @t171 (=> @t274 @t19)))) % 0.49/0.90 (assume @p248 (forall @t267 (=> @t164 (=> @t266 @t22)))) % 0.49/0.90 (assume @p249 (forall (@list @t69 @t350 @t374) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t350) @t374)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool (tptp.insert_pname @t69 @t350)) (tptp.insert_pname @t69 @t374)))))) % 0.49/0.90 (assume @p250 (forall (@list @t65 @t351 @t375) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t351) @t375)) (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool (tptp.insert668001005_state @t65 @t351)) (tptp.insert668001005_state @t65 @t375)))))) % 0.49/0.90 (assume @p251 (forall @t332 (= @t147 @t326))) % 0.49/0.90 (assume @p252 (forall @t333 (= @t150 @t329))) % 0.49/0.90 (assume @p253 (forall @t308 (= @t84 @t82))) % 0.49/0.90 (assume @p254 (forall @t304 (= @t89 @t87))) % 0.49/0.90 (assume @p255 (forall @t300 (= @t105 @t103))) % 0.49/0.90 (assume @p256 (forall @t296 (= @t100 @t98))) % 0.49/0.90 (assume @p257 (forall (@list @t250 @t18 @t170) (=> @t274 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t251))))) % 0.49/0.90 (assume @p258 (forall (@list @t240 @t21 @t163) (=> @t266 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t241))))) % 0.49/0.90 (assume @p259 (forall @t320 (=> @t319 (= (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t220 @t316)) @t274)))) % 0.49/0.90 (assume @p260 (forall @t325 (=> @t324 (= (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t214 @t321)) @t266)))) % 0.49/0.90 (assume @p261 (forall @t352 (= (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t317) @t170)) (and @t318 @t274)))) % 0.49/0.90 (assume @p262 (forall @t353 (= (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t322) @t163)) (and @t323 @t266)))) % 0.49/0.90 (assume @p263 (forall (@list @t170 @t69) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t173 @t343)))) % 0.49/0.90 (assume @p264 (forall (@list @t163 @t65) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t167 @t346)))) % 0.49/0.90 (assume @p265 (forall @t354 (=> @t147 (= (tptp.insert668001005_state @t285 @t166) @t166)))) % 0.49/0.90 (assume @p266 (forall (@list @t165 @t69 @t170) (= (tptp.image_1256224870_state @t165 @t343) (tptp.insert668001005_state (tptp.hAPP_p675228438_state @t165 @t69) @t376)))) % 0.49/0.90 (assume @p267 (forall (@list @t165 @t18 @t170) (=> @t274 (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t166) @t376))))) % 0.49/0.90 (assume @p268 (forall @t169 (= @t168 (exists (@list @t377) (and (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t377) @t18)) (= @t163 (tptp.image_1256224870_state @t165 @t377))))))) % 0.49/0.90 (assume @p269 (forall (@list @t378 @t69 @t379) (=> (= (tptp.hAPP_p799580910on_com @t378 @t69) (tptp.some_com @t379)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t238 (tptp.dom_pname_com @t378)))))) % 0.49/0.90 (assume @p270 (forall @t383 (and (=> @t381 (= @t380 @t362)) (=> @t382 (= @t380 tptp.bot_bo844097828e_bool))))) % 0.49/0.90 (assume @p271 (forall @t387 (and (=> @t385 (= @t384 @t364)) (=> @t386 (= @t384 tptp.bot_bo454148287e_bool))))) % 0.49/0.90 (assume @p272 (forall @t392 (and (=> @t389 (= @t388 @t391)) (=> @t390 (= @t388 tptp.bot_bo1649642514l_bool))))) % 0.49/0.90 (assume @p273 (forall @t397 (and (=> @t394 (= @t393 @t396)) (=> @t395 (= @t393 tptp.bot_bo2068035593l_bool))))) % 0.49/0.90 (assume @p274 (forall @t383 (and (=> @t381 (= @t399 @t362)) (=> @t382 (= @t399 tptp.bot_bo844097828e_bool))))) % 0.49/0.90 (assume @p275 (forall @t387 (and (=> @t385 (= @t401 @t364)) (=> @t386 (= @t401 tptp.bot_bo454148287e_bool))))) % 0.49/0.90 (assume @p276 (forall @t392 (and (=> @t389 (= @t403 @t391)) (=> @t390 (= @t403 tptp.bot_bo1649642514l_bool))))) % 0.49/0.90 (assume @p277 (forall @t397 (and (=> @t394 (= @t405 @t396)) (=> @t395 (= @t405 tptp.bot_bo2068035593l_bool))))) % 0.49/0.90 (assume @p278 (forall @t239 (= (tptp.collect_pname @t335) @t362))) % 0.49/0.90 (assume @p279 (forall @t233 (= (tptp.collec1708318610_state @t337) @t364))) % 0.49/0.90 (assume @p280 (forall @t235 (= (tptp.collec1974731493e_bool @t339) @t391))) % 0.49/0.90 (assume @p281 (forall @t237 (= (tptp.collec1657840446e_bool @t341) @t396))) % 0.49/0.90 (assume @p282 (forall @t239 (= (tptp.collect_pname @t398) @t362))) % 0.49/0.90 (assume @p283 (forall @t233 (= (tptp.collec1708318610_state @t400) @t364))) % 0.49/0.90 (assume @p284 (forall @t235 (= (tptp.collec1974731493e_bool @t402) @t391))) % 0.49/0.90 (assume @p285 (forall @t237 (= (tptp.collec1657840446e_bool @t404) @t396))) % 0.49/0.90 (assume @p286 (forall (@list @t221 @t1) (=> @t229 (=> (forall @t306 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t313 @t406)) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 (tptp.insert668001005_state (tptp.hAPP_c379084956_state tptp.hoare_Mirabelle_MGT (tptp.hAPP_pname_com tptp.body_1 @t305)) tptp.bot_bo454148287e_bool))))) (=> @t225 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t2 @t222))))))) % 0.49/0.90 (assume @p287 @t413) % 0.49/0.90 (assume @p288 (forall (@list @t240 @t165 @t18) (=> @t284 (not (forall @t306 (=> (= @t240 @t355) @t315)))))) % 0.49/0.90 (assume @p289 (forall (@list @t103 @t18 @t34) (=> @t36 (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t34) @t18)) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 tptp.bot_bo844097828e_bool)) (=> (forall (@list @t415 @t414) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t414)) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t416 @t18)) (=> (not (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t416 @t414))) (=> (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 @t414)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 (tptp.insert_pname @t415 @t414)))))))) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t103 @t34)))))))) % 0.49/0.90 (assume @p290 (forall (@list @t98 @t21 @t57) (=> @t59 (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool @t57) @t21)) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 tptp.bot_bo454148287e_bool)) (=> (forall (@list @t418 @t417) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state @t417)) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t419 @t21)) (=> (not (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t419 @t417))) (=> (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 @t417)) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 (tptp.insert668001005_state @t418 @t417)))))))) (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t98 @t57)))))))) % 0.49/0.90 (assume @p291 (forall (@list @t92 @t31 @t46) (=> @t48 (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f510955609l_bool tptp.ord_le675606854l_bool @t46) @t31)) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t92 tptp.bot_bo1649642514l_bool)) (=> (forall (@list @t421 @t420) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool tptp.finite595471783e_bool @t420)) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t422 @t31)) (=> (not (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t422 @t420))) (=> (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t92 @t420)) (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t92 (tptp.insert1325755072e_bool @t421 @t420)))))))) (tptp.hBOOL (tptp.hAPP_f1935102916l_bool @t92 @t46)))))))) % 0.49/0.90 (assume @p292 (forall (@list @t95 @t28 @t43) (=> @t45 (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f511954751l_bool tptp.ord_le1819283413l_bool @t43) @t28)) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t95 tptp.bot_bo2068035593l_bool)) (=> (forall (@list @t424 @t423) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool tptp.finite297877756e_bool @t423)) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t425 @t28)) (=> (not (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t425 @t423))) (=> (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t95 @t423)) (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t95 (tptp.insert1390540323e_bool @t424 @t423)))))))) (tptp.hBOOL (tptp.hAPP_f1526158591l_bool @t95 @t43)))))))) % 0.49/0.90 (assume @p293 (forall (@list @t427) (=> (tptp.hBOOL (tptp.wt (tptp.hAPP_pname_com tptp.body_1 @t427))) (not (forall (@list @t426) (not (= (tptp.hAPP_p799580910on_com tptp.body @t427) (tptp.some_com @t426)))))))) % 0.49/0.90 (assume @p294 (forall (@list @t170 @t18) (=> (forall @t306 (=> @t314 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool @t313 @t170)))) @t274))) % 0.49/0.90 (assume @p295 (forall (@list @t163 @t21) (=> (forall @t302 (=> @t312 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t311 @t163)))) @t266))) % 0.49/0.90 (assume @p296 (forall (@list @t165 @t18 @t163) (=> @t164 (=> @t168 (exists (@list @t428) (and (tptp.hBOOL (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool tptp.ord_le313189616e_bool @t428) @t18)) (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t428)) (= @t163 (tptp.image_1256224870_state @t165 @t428)))))))) % 0.49/0.90 (assume @p297 (tptp.hBOOL (tptp.hAPP_f1664156314l_bool tptp.finite_finite_pname @t406))) % 0.49/0.90 (assume @p298 (forall (@list @t430 @t429) (= (= (tptp.hAPP_pname_com tptp.body_1 @t430) (tptp.hAPP_pname_com tptp.body_1 @t429)) (= @t430 @t429)))) % 0.49/0.90 (assume @p299 (forall @t435 (or (not @t434) @t433))) % 0.49/0.90 (assume @p300 (forall @t435 (or @t432 @t434))) % 0.49/0.90 (assume @p301 (forall @t440 (or @t433 @t439 @t437))) % 0.49/0.90 (assume @p302 (forall @t442 (or @t441 @t432))) % 0.49/0.90 (assume @p303 (forall @t442 (or @t441 @t438))) % 0.49/0.90 (assume @p304 (forall @t440 (or @t433 @t443))) % 0.49/0.90 (assume @p305 (forall @t442 (or @t439 @t443))) % 0.49/0.90 (assume @p306 (forall @t442 (or (not @t443) @t432 @t438))) % 0.49/0.90 (assume @p307 (not (tptp.hBOOL tptp.fFalse))) % 0.49/0.90 (assume @p308 (forall @t435 (or (= @t431 tptp.fTrue) (= @t431 tptp.fFalse)))) % 0.49/0.90 (assume @p309 (forall @t440 (or @t432 @t444))) % 0.49/0.90 (assume @p310 (forall @t442 (or @t439 @t444))) % 0.49/0.90 (assume @p311 (forall @t442 (or (not @t444) @t433 @t438))) % 0.49/0.90 (assume @p312 (forall @t449 (or (not @t448) @t447))) % 0.49/0.90 (assume @p313 (forall @t449 (or (not @t447) @t448))) % 0.49/0.90 (assume @p314 (forall (@list @t431 @t450) (= (tptp.hAPP_pname_bool (tptp.cOMBK_bool_pname @t431) @t450) @t431))) % 0.49/0.90 (assume @p315 (forall (@list @t427 @t450) (= (tptp.hAPP_pname_pname (tptp.cOMBK_pname_pname @t427) @t450) @t427))) % 0.49/0.90 (assume @p316 (forall @t455 (or (not @t454) @t453))) % 0.49/0.90 (assume @p317 (forall @t455 (or (not @t453) @t454))) % 0.49/0.90 (assume @p318 (forall (@list @t459 @t457 @t456) (= (tptp.hAPP_pname_bool (tptp.cOMBB_647938656_pname @t459 @t457) @t456) (tptp.hAPP_bool_bool @t459 @t458)))) % 0.49/0.90 (assume @p319 (forall (@list @t460 @t457 @t456) (= (tptp.hAPP_pname_bool (tptp.cOMBS_568398431l_bool @t460 @t457) @t456) (tptp.hAPP_bool_bool (tptp.hAPP_p393069232l_bool @t460 @t456) @t458)))) % 0.49/0.90 (assume @p320 (forall (@list @t461 @t450 @t456) (= (tptp.hAPP_pname_bool (tptp.hAPP_p61793385e_bool (tptp.cOMBC_1149511130e_bool @t461) @t450) @t456) (tptp.hAPP_pname_bool (tptp.hAPP_p61793385e_bool @t461 @t456) @t450)))) % 0.49/0.90 (assume @p321 (forall (@list @t431 @t457) (= (tptp.hAPP_f1664156314l_bool (tptp.cOMBK_1857069011e_bool @t431) @t457) @t431))) % 0.49/0.90 (assume @p322 (forall (@list @t427 @t457) (= (tptp.hAPP_f1297739591_pname (tptp.cOMBK_948730864e_bool @t427) @t457) @t427))) % 0.49/0.90 (assume @p323 (forall (@list @t462 @t450) (= (tptp.hAPP_p61793385e_bool (tptp.cOMBK_37193422_pname @t462) @t450) @t462))) % 0.49/0.90 (assume @p324 (forall @t467 (or (not @t466) @t465))) % 0.49/0.90 (assume @p325 (forall @t467 (or (not @t465) @t466))) % 0.49/0.90 (assume @p326 (forall (@list @t469 @t468 @t456) (= (tptp.hAPP_pname_com (tptp.cOMBB_923936821_pname @t469 @t468) @t456) (tptp.hAPP_option_com_com @t469 (tptp.hAPP_p799580910on_com @t468 @t456))))) % 0.49/0.90 (assume @p327 (forall (@list @t459 @t471 @t470) (= (tptp.hAPP_f1664156314l_bool (tptp.cOMBB_307249310e_bool @t459 @t471) @t470) (tptp.hAPP_bool_bool @t459 @t472)))) % 0.49/0.90 (assume @p328 (forall (@list @t473 @t457 @t456) (= (tptp.hAPP_p393069232l_bool (tptp.cOMBB_675860798_pname @t473 @t457) @t456) (tptp.hAPP_b589554111l_bool @t473 @t458)))) % 0.49/0.90 (assume @p329 (forall (@list @t474 @t471 @t470) (= (tptp.hAPP_f1664156314l_bool (tptp.cOMBS_350070575l_bool @t474 @t471) @t470) (tptp.hAPP_bool_bool (tptp.hAPP_f1476298914l_bool @t474 @t470) @t472)))) % 0.49/0.90 (assume @p330 (forall (@list @t475 @t457 @t456) (= (tptp.hAPP_pname_bool (tptp.hAPP_f759274231e_bool (tptp.cOMBC_1058051404l_bool @t475) @t457) @t456) (tptp.hAPP_f1664156314l_bool (tptp.hAPP_p338031245l_bool @t475 @t456) @t457)))) % 0.49/0.90 (assume @p331 (forall (@list @t431 @t476) (= (tptp.hAPP_H2060173127e_bool (tptp.cOMBK_2059960192_state @t431) @t476) @t431))) % 0.49/0.90 (assume @p332 (forall (@list @t427 @t476) (= (tptp.hAPP_H1494965722_pname (tptp.cOMBK_1568566301_state @t427) @t476) @t427))) % 0.49/0.90 (assume @p333 (forall (@list @t477 @t450) (= (tptp.hAPP_p675228438_state (tptp.cOMBK_240819937_pname @t477) @t450) @t477))) % 0.49/0.90 (assume @p334 (forall @t482 (or (not @t481) @t480))) % 0.49/0.90 (assume @p335 (forall @t482 (or (not @t480) @t481))) % 0.49/0.90 (assume @p336 (forall (@list @t484 @t483 @t456) (= (tptp.hAPP_p675228438_state (tptp.cOMBB_573322273_pname @t484 @t483) @t456) (tptp.hAPP_c379084956_state @t484 (tptp.hAPP_pname_com @t483 @t456))))) % 0.49/0.90 (assume @p337 (forall (@list @t459 @t486 @t485) (= (tptp.hAPP_H2060173127e_bool (tptp.cOMBB_1397003211_state @t459 @t486) @t485) (tptp.hAPP_bool_bool @t459 @t487)))) % 0.49/0.90 (assume @p338 (forall (@list @t488 @t486 @t485) (= (tptp.hAPP_H2060173127e_bool (tptp.cOMBS_1990964188l_bool @t488 @t486) @t485) (tptp.hAPP_bool_bool (tptp.hAPP_H590162869l_bool @t488 @t485) @t487)))) % 0.49/0.90 (assume @p339 (forall (@list @t473 @t471 @t470) (= (tptp.hAPP_f1476298914l_bool (tptp.cOMBB_2095475776e_bool @t473 @t471) @t470) (tptp.hAPP_b589554111l_bool @t473 @t472)))) % 0.49/0.90 (assume @p340 (forall (@list @t492 @t490 @t489) (= (tptp.hAPP_f1935102916l_bool (tptp.cOMBS_811933079l_bool @t492 @t490) @t489) (tptp.hAPP_bool_bool (tptp.hAPP_f32027384l_bool @t492 @t489) @t491)))) % 0.49/0.90 (assume @p341 (forall (@list @t493 @t457 @t470) (= (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool (tptp.cOMBC_1284144636l_bool @t493) @t457) @t470) (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f434788991l_bool @t493 @t470) @t457)))) % 0.49/0.90 (assume @p342 (forall (@list @t431 @t486) (= (tptp.hAPP_f355887345l_bool (tptp.cOMBK_2110745040e_bool @t431) @t486) @t431))) % 0.49/0.90 (assume @p343 (forall (@list @t427 @t486) (= (tptp.hAPP_f50667184_pname (tptp.cOMBK_1423274227e_bool @t427) @t486) @t427))) % 0.49/0.90 (assume @p344 (forall (@list @t477 @t457) (= (tptp.hAPP_f141816996_state (tptp.cOMBK_354802397e_bool @t477) @t457) @t477))) % 0.49/0.90 (assume @p345 (forall (@list @t462 @t476) (= (tptp.hAPP_H1355725988e_bool (tptp.cOMBK_1288377053_state @t462) @t476) @t462))) % 0.49/0.90 (assume @p346 (forall (@list @t494 @t450) (= (tptp.hAPP_p276714170e_bool (tptp.cOMBK_1197227241_pname @t494) @t450) @t494))) % 0.49/0.90 (assume @p347 (forall (@list @t459 @t496 @t495) (= (tptp.hAPP_f355887345l_bool (tptp.cOMBB_1356070853e_bool @t459 @t496) @t495) (tptp.hAPP_bool_bool @t459 @t497)))) % 0.49/0.90 (assume @p348 (forall (@list @t473 @t486 @t485) (= (tptp.hAPP_H590162869l_bool (tptp.cOMBB_215065709_state @t473 @t486) @t485) (tptp.hAPP_b589554111l_bool @t473 @t487)))) % 0.49/0.90 (assume @p349 (forall (@list @t498 @t496 @t495) (= (tptp.hAPP_f355887345l_bool (tptp.cOMBS_1278217668l_bool @t498 @t496) @t495) (tptp.hAPP_bool_bool (tptp.hAPP_f170941835l_bool @t498 @t495) @t497)))) % 0.49/0.90 (assume @p350 (forall (@list @t473 @t490 @t489) (= (tptp.hAPP_f32027384l_bool (tptp.cOMBB_689948150l_bool @t473 @t490) @t489) (tptp.hAPP_b589554111l_bool @t473 @t491)))) % 0.49/0.90 (assume @p351 (forall (@list @t499 @t471 @t470) (= (tptp.hAPP_f1664156314l_bool (tptp.hAPP_f559147733l_bool (tptp.cOMBC_1988546018l_bool @t499) @t471) @t470) (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f556039215l_bool @t499 @t470) @t471)))) % 0.49/0.90 (assume @p352 (forall (@list @t431 @t496) (= (tptp.hAPP_f1526158591l_bool (tptp.cOMBK_2014663096l_bool @t431) @t496) @t431))) % 0.49/0.90 (assume @p353 (forall (@list @t500 @t476 @t485) (= (tptp.hAPP_H2060173127e_bool (tptp.hAPP_H1618070847e_bool (tptp.cOMBC_1947058646e_bool @t500) @t476) @t485) (tptp.hAPP_H2060173127e_bool (tptp.hAPP_H1618070847e_bool @t500 @t485) @t476)))) % 0.49/0.90 (assume @p354 (forall (@list @t473 @t496 @t495) (= (tptp.hAPP_f170941835l_bool (tptp.cOMBB_1418941603e_bool @t473 @t496) @t495) (tptp.hAPP_b589554111l_bool @t473 @t497)))) % 0.49/0.90 (assume @p355 (forall (@list @t504 @t502 @t501) (= (tptp.hAPP_f1526158591l_bool (tptp.cOMBS_101732372l_bool @t504 @t502) @t501) (tptp.hAPP_bool_bool (tptp.hAPP_f2022158333l_bool @t504 @t501) @t503)))) % 0.49/0.90 (assume @p356 (forall (@list @t477 @t486) (= (tptp.hAPP_f2099317627_state (tptp.cOMBK_1270376774e_bool @t477) @t486) @t477))) % 0.49/0.90 (assume @p357 (forall (@list @t494 @t476) (= (tptp.hAPP_H1618070847e_bool (tptp.cOMBK_1751623554_state @t494) @t476) @t494))) % 0.49/0.90 (assume @p358 (forall (@list @t505 @t471 @t489) (= (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f510955609l_bool (tptp.cOMBC_7971162l_bool @t505) @t471) @t489) (tptp.hAPP_f1935102916l_bool (tptp.hAPP_f510955609l_bool @t505 @t489) @t471)))) % 0.49/0.90 (assume @p359 (forall (@list @t506 @t486 @t485) (= (tptp.hAPP_H2060173127e_bool (tptp.hAPP_f617245717e_bool (tptp.cOMBC_1803918242l_bool @t506) @t486) @t485) (tptp.hAPP_f355887345l_bool (tptp.hAPP_H1199573897l_bool @t506 @t485) @t486)))) % 0.49/0.90 (assume @p360 (forall (@list @t473 @t502 @t501) (= (tptp.hAPP_f2022158333l_bool (tptp.cOMBB_1936369445l_bool @t473 @t502) @t501) (tptp.hAPP_b589554111l_bool @t473 @t503)))) % 0.49/0.90 (assume @p361 (forall (@list @t507 @t486 @t495) (= (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool (tptp.cOMBC_80545690l_bool @t507) @t486) @t495) (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool @t507 @t495) @t486)))) % 0.49/0.90 (assume @p362 (forall (@list @t509 @t490 @t508) (= (tptp.hAPP_f389811538l_bool (tptp.hAPP_f1759205631l_bool (tptp.cOMBC_336095980l_bool @t509) @t490) @t508) (tptp.hAPP_f389811538l_bool (tptp.hAPP_f1759205631l_bool @t509 @t508) @t490)))) % 0.49/0.90 (assume @p363 (forall (@list @t510 @t496 @t495) (= (tptp.hAPP_f355887345l_bool (tptp.hAPP_f1360064833l_bool (tptp.cOMBC_1100692246l_bool @t510) @t496) @t495) (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f1258983629l_bool @t510 @t495) @t496)))) % 0.49/0.90 (assume @p364 (forall (@list @t511 @t496 @t501) (= (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f511954751l_bool (tptp.cOMBC_1690116422l_bool @t511) @t496) @t501) (tptp.hAPP_f1526158591l_bool (tptp.hAPP_f511954751l_bool @t511 @t501) @t496)))) % 0.49/0.90 (assume @p365 (forall (@list @t513 @t502 @t512) (= (tptp.hAPP_f1359865257l_bool (tptp.hAPP_f1607907235l_bool (tptp.cOMBC_1420373658l_bool @t513) @t502) @t512) (tptp.hAPP_f1359865257l_bool (tptp.hAPP_f1607907235l_bool @t513 @t512) @t502)))) % 0.49/0.90 (assume @p366 @t229) % 0.49/0.90 (assume @p367 @t227) % 0.49/0.90 (assume @p368 (tptp.hBOOL (tptp.hAPP_f355887345l_bool tptp.finite1765195604_state tptp.fa))) % 0.49/0.90 (assume @p369 (not (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_H1199573897l_bool tptp.member591555156_state @t514) tptp.fa)))) % 0.49/0.90 (assume @p370 (tptp.hBOOL (tptp.hAPP_f355887345l_bool (tptp.hAPP_f15397171l_bool tptp.ord_le1119700979e_bool tptp.fa) (tptp.image_1256224870_state (tptp.cOMBB_573322273_pname tptp.hoare_Mirabelle_MGT (tptp.cOMBB_923936821_pname tptp.the_com tptp.body)) @t406)))) % 0.49/0.90 (assume @p371 @t515) % 0.49/0.90 (assume @p372 (tptp.hBOOL (tptp.hAPP_f355887345l_bool @t517 tptp.fa))) % 0.49/0.90 (assume @p373 (not @t519)) % 0.49/0.90 (assume @p374 true) % 0.49/0.90 (step @p375 :rule aci_norm :args ((= (or @t521 (or @t520 @t4)) @t522))) % 0.49/0.90 (step @p376 :rule bool-impl-elim :args (@t10 @t4)) % 0.49/0.90 (step @p377 :rule refl :args (@t521)) % 0.49/0.90 (step @p378 :rule nary_cong :premises (@p377 @p376) :args ((or @t521 @t11))) % 0.49/0.90 (step @p379 :rule trans :premises (@p378 @p375)) % 0.49/0.90 (step @p380 :rule bool-impl-elim :args (@t8 @t11)) % 0.49/0.90 (step @p381 :rule trans :premises (@p380 @p379)) % 0.49/0.90 (step @p382 :rule cong :premises (@p381) :args (@t12)) % 0.49/0.90 (step @p383 :rule eq_resolve :premises (@p5 @p382)) % 0.49/0.90 (step @p384 :rule quant-miniscope-or :args ((= (forall @t230 @t528) (or @t527 @t526 @t525)))) % 0.49/0.90 (step @p385 :rule aci_norm :args ((= @t529 @t528))) % 0.49/0.90 (step @p386 :rule cong :premises (@p385) :args ((forall @t230 @t529))) % 0.49/0.90 (step @p387 :rule trans :premises (@p386 @p384)) % 0.49/0.90 (step @p388 :rule aci_norm :args ((= (or @t527 @t530) @t529))) % 0.49/0.90 (step @p389 :rule aci_norm :args ((= (or @t526 @t524) @t530))) % 0.49/0.90 (step @p390 :rule bool-impl-elim :args (@t225 @t224)) % 0.49/0.90 (step @p391 :rule refl :args (@t526)) % 0.49/0.90 (step @p392 :rule nary_cong :premises (@p391 @p390) :args ((or @t526 @t226))) % 0.49/0.90 (step @p393 :rule trans :premises (@p392 @p389)) % 0.49/0.90 (step @p394 :rule bool-impl-elim :args (@t227 @t226)) % 0.49/0.90 (step @p395 :rule trans :premises (@p394 @p393)) % 0.49/0.90 (step @p396 :rule refl :args (@t527)) % 0.49/0.90 (step @p397 :rule nary_cong :premises (@p396 @p395) :args ((or @t527 @t228))) % 0.49/0.90 (step @p398 :rule trans :premises (@p397 @p388)) % 0.49/0.90 (step @p399 :rule bool-impl-elim :args (@t229 @t228)) % 0.49/0.90 (step @p400 :rule trans :premises (@p399 @p398)) % 0.49/0.90 (step @p401 :rule cong :premises (@p400) :args (@t231)) % 0.49/0.90 (step @p402 :rule trans :premises (@p401 @p387)) % 0.49/0.90 (step @p403 :rule eq_resolve :premises (@p104 @p402)) % 0.49/0.90 (step @p404 :rule chain_m_resolution :premises (@p403 @p366 @p367) :args (@t525 @t531 (@list @t229 @t227))) % 0.49/0.90 (step @p405 :rule instantiate :premises (@p404) :args ((@list tptp.y))) % 0.49/0.90 (step @p406 :rule quant-miniscope-or :args ((= (forall @t412 @t535) (or @t526 @t534)))) % 0.49/0.90 (step @p407 :rule aci_norm :args ((= @t536 @t535))) % 0.49/0.90 (step @p408 :rule cong :premises (@p407) :args ((forall @t412 @t536))) % 0.49/0.90 (step @p409 :rule trans :premises (@p408 @p406)) % 0.49/0.90 (step @p410 :rule aci_norm :args ((= @t535 @t536))) % 0.49/0.90 (step @p411 :rule bool-impl-elim :args (@t410 @t408)) % 0.49/0.90 (step @p412 :rule nary_cong :premises (@p391 @p411) :args ((or @t526 @t411))) % 0.49/0.90 (step @p413 :rule trans :premises (@p412 @p410)) % 0.49/0.90 (step @p414 :rule bool-impl-elim :args (@t227 @t411)) % 0.49/0.90 (step @p415 :rule trans :premises (@p414 @p413)) % 0.49/0.90 (step @p416 :rule cong :premises (@p415) :args (@t413)) % 0.49/0.90 (step @p417 :rule trans :premises (@p416 @p409)) % 0.49/0.90 (step @p418 :rule eq_resolve :premises (@p287 @p417)) % 0.49/0.90 (step @p419 :rule chain_m_resolution :premises (@p418 @p367) :args (@t534 (@list false) (@list @t227))) % 0.49/0.90 (step @p420 :rule instantiate :premises (@p419) :args ((@list tptp.pn tptp.y))) % 0.49/0.90 (step @p421 :rule cnf_or_pos :args (@t539)) % 0.49/0.90 (step @p422 :rule reordering :premises (@p421) :args ((or @t538 @t537 (not @t539)))) % 0.49/0.90 (step @p423 :rule chain_m_resolution :premises (@p422 @p371 @p420) :args (@t537 @t531 (@list @t515 @t539))) % 0.49/0.90 (step @p424 :rule cnf_or_pos :args (@t542)) % 0.49/0.90 (step @p425 :rule reordering :premises (@p424) :args ((or @t541 @t540 (not @t542)))) % 0.49/0.90 (step @p426 :rule chain_m_resolution :premises (@p425 @p423 @p405) :args (@t540 @t531 (@list @t537 @t542))) % 0.49/0.90 (step @p427 :rule instantiate :premises (@p1) :args ((@list @t516))) % 0.49/0.90 (step @p428 :rule cnf_or_pos :args (@t546)) % 0.49/0.90 (step @p429 :rule reordering :premises (@p428) :args ((or @t519 @t544 @t545 @t547))) % 0.49/0.90 (step @p430 :rule chain_m_resolution :premises (@p429 @p373 @p427 @p426) :args (@t547 (@list true false false) (@list @t519 @t543 @t540))) % 0.49/0.90 (assume-push @p437 @t548) % 0.49/0.90 (step @p432 :rule instantiate :premises (@p383) :args ((@list @t516 tptp.bot_bo454148287e_bool @t518))) % 0.49/0.90 (step-pop @p438 :rule scope :premises (@p432)) % 0.49/0.90 (step @p433 :rule process_scope :premises (@p438) :args (@t546)) % 0.49/0.90 (step @p435 :rule implies_elim :premises (@p433)) % 0.49/0.90 (step @p436 false :rule chain_m_resolution :premises (@p435 @p430 @p383) :args (false (@list true false) (@list @t546 @t548))) % 0.49/0.90 ) % 0.49/0.90 % SZS output end Proof % 0.49/0.90 % cvc5 exiting %------------------------------------------------------------------------------