%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW470_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 : n014.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:04:59 AM UTC 2026 % Result : Theorem 0.40s 0.81s % Output : Proof 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW470_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.16/0.34 % Computer : n014.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 22:02:58 EDT 2026 % 0.16/0.34 % CPUTime : % 0.30/0.54 %----Proving TF0_NAR, FOF, or CNF % 0.40/0.81 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.40/0.81 % SZS status Theorem % 0.40/0.81 % SZS output start Proof % 0.40/0.81 ( % 0.40/0.81 (declare-sort tptp.fun_fu2008829792e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu734682033e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu281355805e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_a_2117018159e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1047394976e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_bo1936561970e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_st2063251938l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu373216837e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho843200573iple_a 0) % 0.40/0.81 (declare-sort tptp.fun_Ho333840202iple_a 0) % 0.40/0.81 (declare-sort tptp.fun_fu1644852787l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1563903738a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1905604217a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu276214394a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1033095803iple_a 0) % 0.40/0.81 (declare-sort tptp.fun_fu1192765369a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_bool_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1249172034a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_a_998512028e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1585556401a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_bo675861616e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu893561155a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho1630563774a_bool 0) % 0.40/0.81 (declare-sort tptp.hoare_1927711152iple_a 0) % 0.40/0.81 (declare-sort tptp.com 0) % 0.40/0.81 (declare-sort tptp.fun_fu1658206819l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_a_fun_state_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu832487784l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_a_1632297036l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1591723597e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho1877127206a_bool 0) % 0.40/0.81 (declare-sort tptp.bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu1219323149e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu2118559873l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_bo1549164019l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu222103665e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_state_bool 0) % 0.40/0.81 (declare-sort tptp.x_a 0) % 0.40/0.81 (declare-sort tptp.state 0) % 0.40/0.81 (declare-sort tptp.fun_fu402792811e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_st1506752259e_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho525994229l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho440810351a_bool 0) % 0.40/0.81 (declare-sort tptp.fun_Ho957066028l_bool 0) % 0.40/0.81 (declare-sort tptp.fun_fu269925879l_bool 0) % 0.40/0.81 (declare-const tptp.c tptp.com) % 0.40/0.81 (declare-const tptp.hAPP_f963367678e_bool (-> tptp.fun_fu2008829792e_bool tptp.fun_a_1632297036l_bool tptp.fun_a_2117018159e_bool)) % 0.40/0.81 (declare-const tptp.cOMBB_145932198bool_a (-> tptp.fun_fu1047394976e_bool tptp.fun_fu2008829792e_bool)) % 0.40/0.81 (declare-const tptp.hAPP_a849909144l_bool (-> tptp.fun_a_1632297036l_bool tptp.x_a tptp.fun_st2063251938l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f762886889e_bool (-> tptp.fun_fu281355805e_bool tptp.fun_state_bool tptp.fun_a_fun_state_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1261923407e_bool (-> tptp.fun_fu734682033e_bool tptp.fun_a_2117018159e_bool tptp.fun_fu281355805e_bool)) % 0.40/0.81 (declare-const tptp.cOMBC_892787026e_bool tptp.fun_fu734682033e_bool) % 0.40/0.81 (declare-const tptp.hAPP_a1200519163e_bool (-> tptp.fun_a_2117018159e_bool tptp.x_a tptp.fun_fu373216837e_bool)) % 0.40/0.81 (declare-const tptp.hAPP_H1487873860l_bool (-> tptp.fun_Ho957066028l_bool tptp.hoare_1927711152iple_a tptp.fun_bool_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1259673775l_bool (-> tptp.fun_fu1658206819l_bool tptp.fun_state_bool tptp.fun_st2063251938l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_a723219176e_bool (-> tptp.fun_a_998512028e_bool tptp.x_a tptp.fun_bo1936561970e_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f644196280e_bool (-> tptp.fun_fu1047394976e_bool tptp.fun_st2063251938l_bool tptp.fun_fu373216837e_bool)) % 0.40/0.81 (declare-const tptp.cOMBS_1378840469l_bool tptp.fun_fu1047394976e_bool) % 0.40/0.81 (declare-const tptp.hAPP_b2019457360e_bool (-> tptp.fun_bo1936561970e_bool tptp.bool tptp.fun_state_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f167292325e_bool (-> tptp.fun_fu1219323149e_bool tptp.fun_st2063251938l_bool tptp.fun_bo1936561970e_bool)) % 0.40/0.81 (declare-const tptp.hAPP_s58564346l_bool (-> tptp.fun_st2063251938l_bool tptp.state tptp.fun_bool_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1759915619e_bool (-> tptp.fun_fu373216837e_bool tptp.fun_state_bool tptp.fun_state_bool)) % 0.40/0.81 (declare-const tptp.cOMBB_160679318_state (-> tptp.fun_bool_bool tptp.fun_fu373216837e_bool)) % 0.40/0.81 (declare-const tptp.cOMBK_bool_state (-> tptp.bool tptp.fun_state_bool)) % 0.40/0.81 (declare-const tptp.fTrue tptp.bool) % 0.40/0.81 (declare-const tptp.finite1511031594iple_a (-> tptp.fun_Ho333840202iple_a tptp.fun_fu1033095803iple_a tptp.bool)) % 0.40/0.81 (declare-const tptp.finite1943414032iple_a (-> tptp.fun_Ho333840202iple_a tptp.fun_fu1033095803iple_a)) % 0.40/0.81 (declare-const tptp.finite68738179iple_a tptp.fun_fu832487784l_bool) % 0.40/0.81 (declare-const tptp.hAPP_H963118037iple_a (-> tptp.fun_Ho843200573iple_a tptp.hoare_1927711152iple_a tptp.hoare_1927711152iple_a)) % 0.40/0.81 (declare-const tptp.hAPP_H1700437986iple_a (-> tptp.fun_Ho333840202iple_a tptp.hoare_1927711152iple_a tptp.fun_Ho843200573iple_a)) % 0.40/0.81 (declare-const tptp.finite148164294iple_a (-> tptp.fun_Ho333840202iple_a tptp.hoare_1927711152iple_a tptp.fun_Ho1877127206a_bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.finite83514413iple_a (-> tptp.fun_Ho333840202iple_a tptp.fun_fu1033095803iple_a tptp.bool)) % 0.40/0.81 (declare-const tptp.finite2098837632iple_a (-> tptp.fun_Ho333840202iple_a tptp.fun_Ho1877127206a_bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.hAPP_b589554111l_bool (-> tptp.fun_bo1549164019l_bool tptp.bool tptp.fun_bool_bool)) % 0.40/0.81 (declare-const tptp.hAPP_H1027145665a_bool (-> tptp.fun_Ho440810351a_bool tptp.hoare_1927711152iple_a tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.fequal1440857775iple_a tptp.fun_Ho440810351a_bool) % 0.40/0.81 (declare-const tptp.hAPP_H694056973l_bool (-> tptp.fun_Ho525994229l_bool tptp.hoare_1927711152iple_a tptp.fun_fu832487784l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_state_bool (-> tptp.fun_state_bool tptp.state tptp.bool)) % 0.40/0.81 (declare-const tptp.cOMBK_1458035955bool_a (-> tptp.fun_state_bool tptp.fun_a_fun_state_bool)) % 0.40/0.81 (declare-const tptp.hAPP_H1448631928a_bool (-> tptp.fun_Ho1877127206a_bool tptp.hoare_1927711152iple_a tptp.bool)) % 0.40/0.81 (declare-const tptp.hAPP_f817621513e_bool (-> tptp.fun_fu402792811e_bool tptp.fun_st1506752259e_bool tptp.fun_st1506752259e_bool)) % 0.40/0.81 (declare-const tptp.fconj tptp.fun_bo1549164019l_bool) % 0.40/0.81 (declare-const tptp.fequal_state tptp.fun_st1506752259e_bool) % 0.40/0.81 (declare-const tptp.hAPP_b540892988e_bool (-> tptp.fun_bo675861616e_bool tptp.bool tptp.fun_a_fun_state_bool)) % 0.40/0.81 (declare-const tptp.b tptp.fun_state_bool) % 0.40/0.81 (declare-const tptp.cOMBC_825881325a_bool tptp.fun_fu1905604217a_bool) % 0.40/0.81 (declare-const tptp.hAPP_f1824947087e_bool (-> tptp.fun_fu222103665e_bool tptp.fun_a_998512028e_bool tptp.fun_bo675861616e_bool)) % 0.40/0.81 (declare-const tptp.hoare_1652181356iple_a (-> tptp.fun_a_fun_state_bool tptp.com tptp.fun_a_fun_state_bool tptp.hoare_1927711152iple_a)) % 0.40/0.81 (declare-const tptp.hAPP_s1806633685e_bool (-> tptp.fun_st1506752259e_bool tptp.state tptp.fun_state_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f340725611e_bool (-> tptp.fun_fu1591723597e_bool tptp.fun_a_1632297036l_bool tptp.fun_a_998512028e_bool)) % 0.40/0.81 (declare-const tptp.the_Ho1307659873iple_a tptp.fun_fu1033095803iple_a) % 0.40/0.81 (declare-const tptp.bot_bo1208640912a_bool tptp.fun_Ho1877127206a_bool) % 0.40/0.81 (declare-const tptp.hoare_1617968510rivs_a (-> tptp.fun_Ho1877127206a_bool tptp.fun_fu832487784l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_a2036067514e_bool (-> tptp.fun_a_fun_state_bool tptp.x_a tptp.fun_state_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1454306822l_bool (-> tptp.fun_fu832487784l_bool tptp.fun_Ho1877127206a_bool tptp.bool)) % 0.40/0.81 (declare-const tptp.cOMBB_188601460_state (-> tptp.fun_bo1549164019l_bool tptp.fun_fu1658206819l_bool)) % 0.40/0.81 (declare-const tptp.cOMBC_2027030106e_bool tptp.fun_fu402792811e_bool) % 0.40/0.81 (declare-const tptp.hBOOL (-> tptp.bool Bool)) % 0.40/0.81 (declare-const tptp.member127332739iple_a tptp.fun_Ho525994229l_bool) % 0.40/0.81 (declare-const tptp.cOMBC_231445413l_bool tptp.fun_fu1219323149e_bool) % 0.40/0.81 (declare-const tptp.hAPP_f909473944a_bool (-> tptp.fun_fu1563903738a_bool tptp.fun_Ho440810351a_bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.cOMBB_1355796797bool_a (-> tptp.fun_fu1658206819l_bool tptp.fun_fu2118559873l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f16502863a_bool (-> tptp.fun_fu1585556401a_bool tptp.fun_Ho1877127206a_bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.insert1434104874iple_a tptp.fun_Ho1630563774a_bool) % 0.40/0.81 (declare-const tptp.hAPP_H1975128022a_bool (-> tptp.fun_Ho1630563774a_bool tptp.hoare_1927711152iple_a tptp.fun_fu1585556401a_bool)) % 0.40/0.81 (declare-const tptp.cOMBB_1348041619bool_a (-> tptp.fun_fu1219323149e_bool tptp.fun_fu1591723597e_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f749678531l_bool (-> tptp.fun_fu269925879l_bool tptp.fun_Ho1877127206a_bool tptp.fun_Ho957066028l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1509969235l_bool (-> tptp.fun_fu2118559873l_bool tptp.fun_a_fun_state_bool tptp.fun_a_1632297036l_bool)) % 0.40/0.81 (declare-const tptp.collec829051333iple_a (-> tptp.fun_Ho1877127206a_bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.g tptp.fun_Ho1877127206a_bool) % 0.40/0.81 (declare-const tptp.cOMBC_671859290a_bool tptp.fun_fu893561155a_bool) % 0.40/0.81 (declare-const tptp.hAPP_bool_bool (-> tptp.fun_bool_bool tptp.bool tptp.bool)) % 0.40/0.81 (declare-const tptp.hAPP_f1216137953a_bool (-> tptp.fun_fu893561155a_bool tptp.fun_Ho440810351a_bool tptp.fun_Ho440810351a_bool)) % 0.40/0.81 (declare-const tptp.p tptp.fun_a_fun_state_bool) % 0.40/0.81 (declare-const tptp.cOMBC_862840740l_bool tptp.fun_fu1192765369a_bool) % 0.40/0.81 (declare-const tptp.cOMBB_196465322iple_a (-> tptp.fun_bo1549164019l_bool tptp.fun_fu269925879l_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f490779847iple_a (-> tptp.fun_fu1033095803iple_a tptp.fun_Ho1877127206a_bool tptp.hoare_1927711152iple_a)) % 0.40/0.81 (declare-const tptp.cOMBS_2061548107l_bool tptp.fun_fu1249172034a_bool) % 0.40/0.81 (declare-const tptp.hAPP_f2112551770a_bool (-> tptp.fun_fu1249172034a_bool tptp.fun_Ho957066028l_bool tptp.fun_fu1585556401a_bool)) % 0.40/0.81 (declare-const tptp.fFalse tptp.bool) % 0.40/0.81 (declare-const tptp.cOMBK_712844119iple_a (-> tptp.bool tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (declare-const tptp.fNot tptp.fun_bool_bool) % 0.40/0.81 (declare-const tptp.cOMBB_213049548iple_a (-> tptp.fun_bool_bool tptp.fun_fu1585556401a_bool)) % 0.40/0.81 (declare-const tptp.fequal1285825639a_bool tptp.fun_fu1644852787l_bool) % 0.40/0.81 (declare-const tptp.fimplies tptp.fun_bo1549164019l_bool) % 0.40/0.81 (declare-const tptp.hAPP_f684479953a_bool (-> tptp.fun_fu1192765369a_bool tptp.fun_Ho525994229l_bool tptp.fun_fu1585556401a_bool)) % 0.40/0.81 (declare-const tptp.fdisj tptp.fun_bo1549164019l_bool) % 0.40/0.81 (declare-const tptp.the_el1997360207iple_a tptp.fun_fu1033095803iple_a) % 0.40/0.81 (declare-const tptp.bot_bot_bool tptp.bool) % 0.40/0.81 (declare-const tptp.skip tptp.com) % 0.40/0.81 (declare-const tptp.semi (-> tptp.com tptp.com tptp.com)) % 0.40/0.81 (declare-const tptp.cOMBC_41962815e_bool tptp.fun_fu222103665e_bool) % 0.40/0.81 (declare-const tptp.hAPP_f1022403729a_bool (-> tptp.fun_fu1905604217a_bool tptp.fun_Ho1630563774a_bool tptp.fun_fu276214394a_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f993216280a_bool (-> tptp.fun_fu276214394a_bool tptp.fun_Ho1877127206a_bool tptp.fun_Ho440810351a_bool)) % 0.40/0.81 (declare-const tptp.hAPP_f625100287l_bool (-> tptp.fun_fu1644852787l_bool tptp.fun_Ho1877127206a_bool tptp.fun_fu832487784l_bool)) % 0.40/0.81 (declare-const tptp.cOMBB_1083611331iple_a (-> tptp.fun_fu832487784l_bool tptp.fun_fu1563903738a_bool)) % 0.40/0.81 (define @t1 () (@var "Ga" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t2 () (tptp.hoare_1617968510rivs_a @t1)) % 0.40/0.81 (define @t3 () (@var "Fun2_1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t4 () (@var "Fun2_2" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t5 () (@var "Com_1" tptp.com)) % 0.40/0.81 (define @t6 () (@var "Com_2" tptp.com)) % 0.40/0.81 (define @t7 () (@var "Fun1_1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t8 () (@var "Fun1_2" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t9 () (@var "Ts" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t10 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 @t9))) % 0.40/0.81 (define @t11 () (@var "G_1" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t12 () (@var "T" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t13 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t12)) % 0.40/0.81 (define @t14 () (@var "Q_1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t15 () (@var "Ca" tptp.com)) % 0.40/0.81 (define @t16 () (@var "C" tptp.bool)) % 0.40/0.81 (define @t17 () (@var "Pa" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t18 () (tptp.cOMBB_1355796797bool_a (tptp.cOMBB_188601460_state tptp.fconj))) % 0.40/0.81 (define @t19 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t17 @t15 @t14)) tptp.bot_bo1208640912a_bool)))) % 0.40/0.81 (define @t20 () (@var "Z_1" tptp.x_a)) % 0.40/0.81 (define @t21 () (tptp.hAPP_a2036067514e_bool @t14 @t20)) % 0.40/0.81 (define @t22 () (@var "S" tptp.state)) % 0.40/0.81 (define @t23 () (tptp.hAPP_f817621513e_bool tptp.cOMBC_2027030106e_bool tptp.fequal_state)) % 0.40/0.81 (define @t24 () (tptp.cOMBK_1458035955bool_a (tptp.hAPP_s1806633685e_bool @t23 @t22))) % 0.40/0.81 (define @t25 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t24 @t15 (tptp.cOMBK_1458035955bool_a @t21))) tptp.bot_bo1208640912a_bool)))) % 0.40/0.81 (define @t26 () (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t17 @t20) @t22))) % 0.40/0.81 (define @t27 () (@list @t20 @t22)) % 0.40/0.81 (define @t28 () (forall @t27 (=> @t26 @t25))) % 0.40/0.81 (define @t29 () (=> @t28 @t19)) % 0.40/0.81 (define @t30 () (@list @t1 @t15 @t14 @t17)) % 0.40/0.81 (define @t31 () (forall @t30 @t29)) % 0.40/0.81 (define @t32 () (@var "Q_3" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t33 () (@var "P_2" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t34 () (@var "S_1" tptp.state)) % 0.40/0.81 (define @t35 () (tptp.hBOOL (tptp.hAPP_state_bool @t21 @t34))) % 0.40/0.81 (define @t36 () (@var "Z_2" tptp.x_a)) % 0.40/0.81 (define @t37 () (@list @t36)) % 0.40/0.81 (define @t38 () (@list @t34)) % 0.40/0.81 (define @t39 () (@var "A" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t40 () (@var "A_3" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t41 () (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t40)) % 0.40/0.81 (define @t42 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 @t39))) % 0.40/0.81 (define @t43 () (@var "Ba" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t44 () (= @t40 @t43)) % 0.40/0.81 (define @t45 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t43)) % 0.40/0.81 (define @t46 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 (tptp.hAPP_f16502863a_bool @t45 @t39)))) % 0.40/0.81 (define @t47 () (@list @t40 @t43 @t39)) % 0.40/0.81 (define @t48 () (@var "B_1" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t49 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 (tptp.hAPP_f16502863a_bool @t45 @t48)))) % 0.40/0.81 (define @t50 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 @t48))) % 0.40/0.81 (define @t51 () (@list @t43 @t40 @t48)) % 0.40/0.81 (define @t52 () (@list @t40)) % 0.40/0.81 (define @t53 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t40)) % 0.40/0.81 (define @t54 () (tptp.hAPP_f16502863a_bool @t53 tptp.bot_bo1208640912a_bool)) % 0.40/0.81 (define @t55 () (tptp.hAPP_H1027145665a_bool tptp.fequal1440857775iple_a @t40)) % 0.40/0.81 (define @t56 () (tptp.hAPP_f1216137953a_bool tptp.cOMBC_671859290a_bool tptp.fequal1440857775iple_a)) % 0.40/0.81 (define @t57 () (tptp.hAPP_H1027145665a_bool @t56 @t40)) % 0.40/0.81 (define @t58 () (@var "Pa" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t59 () (tptp.cOMBB_196465322iple_a tptp.fconj)) % 0.40/0.81 (define @t60 () (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t59 @t55)) @t58))) % 0.40/0.81 (define @t61 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t58 @t40))) % 0.40/0.81 (define @t62 () (not @t61)) % 0.40/0.81 (define @t63 () (@list @t58 @t40)) % 0.40/0.81 (define @t64 () (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t59 @t57)) @t58))) % 0.40/0.81 (define @t65 () (not @t42)) % 0.40/0.81 (define @t66 () (= @t39 tptp.bot_bo1208640912a_bool)) % 0.40/0.81 (define @t67 () (@list @t40 @t39)) % 0.40/0.81 (define @t68 () (@var "X_2" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t69 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t58 @t68))) % 0.40/0.81 (define @t70 () (@list @t68)) % 0.40/0.81 (define @t71 () (forall @t70 (not @t69))) % 0.40/0.81 (define @t72 () (tptp.collec829051333iple_a @t58)) % 0.40/0.81 (define @t73 () (@list @t58)) % 0.40/0.81 (define @t74 () (@var "Ca" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t75 () (not @t66)) % 0.40/0.81 (define @t76 () (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t68)) % 0.40/0.81 (define @t77 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t76 @t39))) % 0.40/0.81 (define @t78 () (@list @t39)) % 0.40/0.81 (define @t79 () (tptp.hAPP_f16502863a_bool @t53 @t39)) % 0.40/0.81 (define @t80 () (@var "X_1" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t81 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t80)) % 0.40/0.81 (define @t82 () (tptp.hAPP_f16502863a_bool @t81 @t39)) % 0.40/0.81 (define @t83 () (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t80)) % 0.40/0.81 (define @t84 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t83 @t39))) % 0.40/0.81 (define @t85 () (not @t84)) % 0.40/0.81 (define @t86 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t39 @t80))) % 0.40/0.81 (define @t87 () (@var "Y_2" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t88 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t87)) % 0.40/0.81 (define @t89 () (tptp.hAPP_f16502863a_bool @t88 @t39)) % 0.40/0.81 (define @t90 () (@list @t80 @t39)) % 0.40/0.81 (define @t91 () (@list @t40 @t58)) % 0.40/0.81 (define @t92 () (tptp.hAPP_f684479953a_bool tptp.cOMBC_862840740l_bool tptp.member127332739iple_a)) % 0.40/0.81 (define @t93 () (tptp.cOMBB_196465322iple_a tptp.fdisj)) % 0.40/0.81 (define @t94 () (tptp.hAPP_f16502863a_bool @t53 @t48)) % 0.40/0.81 (define @t95 () (@list @t40 @t48)) % 0.40/0.81 (define @t96 () (@var "Xa" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t97 () (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t68)) % 0.40/0.81 (define @t98 () (tptp.hAPP_f16502863a_bool @t45 tptp.bot_bo1208640912a_bool)) % 0.40/0.81 (define @t99 () (= @t43 @t40)) % 0.40/0.81 (define @t100 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t43) @t54))) % 0.40/0.81 (define @t101 () (@list @t43 @t40)) % 0.40/0.81 (define @t102 () (@var "D" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t103 () (tptp.hAPP_f16502863a_bool @t81 tptp.bot_bo1208640912a_bool)) % 0.40/0.81 (define @t104 () (@list @t80)) % 0.40/0.81 (define @t105 () (tptp.hBOOL tptp.bot_bot_bool)) % 0.40/0.81 (define @t106 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool tptp.bot_bo1208640912a_bool @t68))) % 0.40/0.81 (define @t107 () (@var "R_1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t108 () (@var "D" tptp.com)) % 0.40/0.81 (define @t109 () (@var "Fun2" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t110 () (@var "Com" tptp.com)) % 0.40/0.81 (define @t111 () (@var "Fun1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t112 () (@var "B" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t113 () (@list @t112)) % 0.40/0.81 (define @t114 () (@var "Com2_2" tptp.com)) % 0.40/0.81 (define @t115 () (@var "Com1_2" tptp.com)) % 0.40/0.81 (define @t116 () (tptp.semi @t115 @t114)) % 0.40/0.81 (define @t117 () (@list @t115 @t114)) % 0.40/0.81 (define @t118 () (@var "X_3" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t119 () (@var "Com2" tptp.com)) % 0.40/0.81 (define @t120 () (@var "Com2_1" tptp.com)) % 0.40/0.81 (define @t121 () (@var "Com1" tptp.com)) % 0.40/0.81 (define @t122 () (@var "Com1_1" tptp.com)) % 0.40/0.81 (define @t123 () (@var "Pa" tptp.bool)) % 0.40/0.81 (define @t124 () (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t59 (tptp.hAPP_f16502863a_bool (tptp.cOMBB_213049548iple_a (tptp.hAPP_b589554111l_bool tptp.fimplies @t123)) (tptp.hAPP_H1027145665a_bool @t56 @t80)))) (tptp.hAPP_f16502863a_bool (tptp.cOMBB_213049548iple_a (tptp.hAPP_b589554111l_bool tptp.fimplies (tptp.hAPP_bool_bool tptp.fNot @t123))) (tptp.hAPP_H1027145665a_bool @t56 @t87))))) % 0.40/0.81 (define @t125 () (tptp.hBOOL @t123)) % 0.40/0.81 (define @t126 () (@var "Y_1" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t127 () (@list @t126)) % 0.40/0.81 (define @t128 () (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a @t58)) % 0.40/0.81 (define @t129 () (= @t128 @t40)) % 0.40/0.81 (define @t130 () (forall @t70 (=> @t69 (= @t68 @t40)))) % 0.40/0.81 (define @t131 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t58 @t128))) % 0.40/0.81 (define @t132 () (exists @t70 (and @t69 (forall @t127 (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t58 @t126)) (= @t126 @t68)))))) % 0.40/0.81 (define @t133 () (@var "Q_2" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t134 () (@var "P_1" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t135 () (@var "F_1" tptp.fun_Ho333840202iple_a)) % 0.40/0.81 (define @t136 () (@var "F" tptp.fun_fu1033095803iple_a)) % 0.40/0.81 (define @t137 () (tptp.hBOOL (tptp.finite83514413iple_a @t135 @t136))) % 0.40/0.81 (define @t138 () (@list @t80 @t135 @t136)) % 0.40/0.81 (define @t139 () (tptp.finite2098837632iple_a @t135 @t39)) % 0.40/0.81 (define @t140 () (tptp.hAPP_f490779847iple_a @t136 @t39)) % 0.40/0.81 (define @t141 () (tptp.hAPP_H1700437986iple_a @t135 @t80)) % 0.40/0.81 (define @t142 () (tptp.hAPP_H963118037iple_a @t141 @t140)) % 0.40/0.81 (define @t143 () (=> @t75 (= (tptp.hAPP_f490779847iple_a @t136 @t82) @t142))) % 0.40/0.81 (define @t144 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t39))) % 0.40/0.81 (define @t145 () (@list @t80 @t39 @t135 @t136)) % 0.40/0.81 (define @t146 () (tptp.finite1943414032iple_a @t135)) % 0.40/0.81 (define @t147 () (tptp.hAPP_f490779847iple_a @t146 @t39)) % 0.40/0.81 (define @t148 () (@list @t135 @t39)) % 0.40/0.81 (define @t149 () (@var "Q_1" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t150 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a (tptp.collec829051333iple_a @t149)))) % 0.40/0.81 (define @t151 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t72))) % 0.40/0.81 (define @t152 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t79))) % 0.40/0.81 (define @t153 () (@list @t39 @t135 @t136)) % 0.40/0.81 (define @t154 () (@var "Z" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t155 () (tptp.finite148164294iple_a @t135 @t154 tptp.bot_bo1208640912a_bool)) % 0.40/0.81 (define @t156 () (tptp.finite148164294iple_a @t135 @t154 @t39)) % 0.40/0.81 (define @t157 () (@var "G" tptp.fun_fu1033095803iple_a)) % 0.40/0.81 (define @t158 () (tptp.hAPP_H963118037iple_a (tptp.hAPP_H1700437986iple_a @t135 @t68) @t126)) % 0.40/0.81 (define @t159 () (@var "A_1" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t160 () (@var "A_2" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t161 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t160) @t159))) % 0.40/0.81 (define @t162 () (tptp.finite148164294iple_a @t135 @t160 @t159)) % 0.40/0.81 (define @t163 () (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t160) @t159)) % 0.40/0.81 (define @t164 () (tptp.hAPP_f16502863a_bool @t53 @t118)) % 0.40/0.81 (define @t165 () (@var "X1" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t166 () (@list @t165)) % 0.40/0.81 (define @t167 () (@var "F" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t168 () (@var "Pa" tptp.fun_fu832487784l_bool)) % 0.40/0.81 (define @t169 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t168 @t167))) % 0.40/0.81 (define @t170 () (@var "F_2" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t171 () (=> (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t76 @t170))) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t168 @t170)) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t168 (tptp.hAPP_f16502863a_bool @t97 @t170)))))) % 0.40/0.81 (define @t172 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t170))) % 0.40/0.81 (define @t173 () (@list @t68 @t170)) % 0.40/0.81 (define @t174 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t167))) % 0.40/0.81 (define @t175 () (@list @t168 @t167)) % 0.40/0.81 (define @t176 () (@var "A_3" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t177 () (@var "A2" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t178 () (@var "A1" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t179 () (tptp.hBOOL (tptp.finite1511031594iple_a @t135 @t136))) % 0.40/0.81 (define @t180 () (@var "P" tptp.bool)) % 0.40/0.81 (define @t181 () (tptp.hBOOL @t180)) % 0.40/0.81 (define @t182 () (not @t181)) % 0.40/0.81 (define @t183 () (tptp.hBOOL (tptp.hAPP_bool_bool tptp.fNot @t180))) % 0.40/0.81 (define @t184 () (@list @t180)) % 0.40/0.81 (define @t185 () (@var "Q" tptp.bool)) % 0.40/0.81 (define @t186 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fconj @t180) @t185))) % 0.40/0.81 (define @t187 () (tptp.hBOOL @t185)) % 0.40/0.81 (define @t188 () (not @t187)) % 0.40/0.81 (define @t189 () (@list @t185 @t180)) % 0.40/0.81 (define @t190 () (not @t186)) % 0.40/0.81 (define @t191 () (@list @t180 @t185)) % 0.40/0.81 (define @t192 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fdisj @t180) @t185))) % 0.40/0.81 (define @t193 () (tptp.hBOOL tptp.fFalse)) % 0.40/0.81 (define @t194 () (tptp.hBOOL (tptp.hAPP_bool_bool (tptp.hAPP_b589554111l_bool tptp.fimplies @t180) @t185))) % 0.40/0.81 (define @t195 () (@var "Y" tptp.state)) % 0.40/0.81 (define @t196 () (@var "X" tptp.state)) % 0.40/0.81 (define @t197 () (= @t196 @t195)) % 0.40/0.81 (define @t198 () (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_s1806633685e_bool tptp.fequal_state @t196) @t195))) % 0.40/0.81 (define @t199 () (@list @t196 @t195)) % 0.40/0.81 (define @t200 () (@var "Q" tptp.state)) % 0.40/0.81 (define @t201 () (tptp.hAPP_state_bool (tptp.cOMBK_bool_state @t180) @t200)) % 0.40/0.81 (define @t202 () (forall (@list @t180 @t200) (= @t201 @t180))) % 0.40/0.81 (define @t203 () (@var "P" tptp.fun_state_bool)) % 0.40/0.81 (define @t204 () (@var "Q" tptp.x_a)) % 0.40/0.81 (define @t205 () (tptp.hAPP_a2036067514e_bool (tptp.cOMBK_1458035955bool_a @t203) @t204)) % 0.40/0.81 (define @t206 () (forall (@list @t203 @t204) (= @t205 @t203))) % 0.40/0.81 (define @t207 () (@var "R" tptp.state)) % 0.40/0.81 (define @t208 () (@var "Q" tptp.fun_state_bool)) % 0.40/0.81 (define @t209 () (tptp.hAPP_state_bool @t208 @t207)) % 0.40/0.81 (define @t210 () (@var "P" tptp.fun_bool_bool)) % 0.40/0.81 (define @t211 () (@var "P" tptp.fun_st2063251938l_bool)) % 0.40/0.81 (define @t212 () (tptp.hAPP_s58564346l_bool @t211 @t207)) % 0.40/0.81 (define @t213 () (@var "P" tptp.fun_st1506752259e_bool)) % 0.40/0.81 (define @t214 () (@var "Y" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t215 () (@var "X" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t216 () (= @t215 @t214)) % 0.40/0.81 (define @t217 () (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.hAPP_H1027145665a_bool tptp.fequal1440857775iple_a @t215) @t214))) % 0.40/0.81 (define @t218 () (@list @t215 @t214)) % 0.40/0.81 (define @t219 () (@var "R" tptp.x_a)) % 0.40/0.81 (define @t220 () (@var "P" tptp.fun_a_998512028e_bool)) % 0.40/0.81 (define @t221 () (@var "Q" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t222 () (@var "P" tptp.fun_bo1549164019l_bool)) % 0.40/0.81 (define @t223 () (@var "Y" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t224 () (@var "X" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t225 () (= @t224 @t223)) % 0.40/0.81 (define @t226 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_f625100287l_bool tptp.fequal1285825639a_bool @t224) @t223))) % 0.40/0.81 (define @t227 () (@list @t224 @t223)) % 0.40/0.81 (define @t228 () (@var "R" tptp.hoare_1927711152iple_a)) % 0.40/0.81 (define @t229 () (@var "Q" tptp.fun_Ho1877127206a_bool)) % 0.40/0.81 (define @t230 () (tptp.hAPP_H1448631928a_bool @t229 @t228)) % 0.40/0.81 (define @t231 () (@var "P" tptp.fun_Ho957066028l_bool)) % 0.40/0.81 (define @t232 () (@var "P" tptp.fun_a_2117018159e_bool)) % 0.40/0.81 (define @t233 () (@var "Q" tptp.fun_a_fun_state_bool)) % 0.40/0.81 (define @t234 () (@var "P" tptp.fun_fu1658206819l_bool)) % 0.40/0.81 (define @t235 () (@var "P" tptp.fun_Ho440810351a_bool)) % 0.40/0.81 (define @t236 () (@var "Q" tptp.fun_a_1632297036l_bool)) % 0.40/0.81 (define @t237 () (tptp.hAPP_a849909144l_bool @t236 @t219)) % 0.40/0.81 (define @t238 () (@var "P" tptp.fun_fu1219323149e_bool)) % 0.40/0.81 (define @t239 () (@var "Q" tptp.fun_Ho440810351a_bool)) % 0.40/0.81 (define @t240 () (@var "P" tptp.fun_fu832487784l_bool)) % 0.40/0.81 (define @t241 () (@var "P" tptp.fun_Ho525994229l_bool)) % 0.40/0.81 (define @t242 () (@var "P" tptp.fun_fu1047394976e_bool)) % 0.40/0.81 (define @t243 () (@var "P" tptp.fun_Ho1630563774a_bool)) % 0.40/0.81 (define @t244 () (tptp.hAPP_f762886889e_bool (tptp.hAPP_f1261923407e_bool tptp.cOMBC_892787026e_bool (tptp.hAPP_f963367678e_bool (tptp.cOMBB_145932198bool_a tptp.cOMBS_1378840469l_bool) (tptp.hAPP_f1509969235l_bool @t18 tptp.p))) (tptp.hAPP_f1759915619e_bool (tptp.cOMBB_160679318_state tptp.fNot) tptp.b))) % 0.40/0.81 (define @t245 () (tptp.cOMBK_bool_state tptp.fFalse)) % 0.40/0.81 (define @t246 () (tptp.cOMBK_1458035955bool_a @t245)) % 0.40/0.81 (define @t247 () (tptp.hoare_1617968510rivs_a tptp.g)) % 0.40/0.81 (define @t248 () (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t247 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t246 tptp.c @t244)) tptp.bot_bo1208640912a_bool)))) % 0.40/0.81 (define @t249 () (forall @t27 (or (not @t26) @t25))) % 0.40/0.81 (define @t250 () (forall @t27 (or (not (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t246 @t20) @t22))) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t247 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t24 tptp.c (tptp.cOMBK_1458035955bool_a (tptp.hAPP_a2036067514e_bool @t244 @t20)))) tptp.bot_bo1208640912a_bool)))))) % 0.40/0.81 (define @t251 () (not @t250)) % 0.40/0.81 (define @t252 () (or @t251 @t248)) % 0.40/0.81 (define @t253 () (@quantifiers_skolemize @t250 1)) % 0.40/0.81 (define @t254 () (@quantifiers_skolemize @t250 0)) % 0.40/0.81 (define @t255 () (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t246 @t254) @t253))) % 0.40/0.81 (define @t256 () (not @t255)) % 0.40/0.81 (define @t257 () (or @t256 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t247 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a (tptp.cOMBK_1458035955bool_a (tptp.hAPP_s1806633685e_bool @t23 @t253)) tptp.c (tptp.cOMBK_1458035955bool_a (tptp.hAPP_a2036067514e_bool @t244 @t254)))) tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p1 (forall (@list @t1) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 tptp.bot_bo1208640912a_bool)))) % 0.40/0.81 (assume @p2 (forall (@list @t8 @t6 @t4 @t7 @t5 @t3) (= (= (tptp.hoare_1652181356iple_a @t8 @t6 @t4) (tptp.hoare_1652181356iple_a @t7 @t5 @t3)) (and (= @t8 @t7) (= @t6 @t5) (= @t4 @t3))))) % 0.40/0.81 (assume @p3 (forall (@list @t1 @t11 @t9) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hoare_1617968510rivs_a @t11) @t9)) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 @t11)) @t10)))) % 0.40/0.81 (assume @p4 (forall (@list @t9 @t1 @t12) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool @t13 tptp.bot_bo1208640912a_bool))) (=> @t10 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool @t13 @t9))))))) % 0.40/0.81 (assume @p5 (forall (@list @t1 @t17 @t15 @t14 @t16) (=> (=> (tptp.hBOOL @t16) @t19) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a (tptp.hAPP_b540892988e_bool (tptp.hAPP_f1824947087e_bool tptp.cOMBC_41962815e_bool (tptp.hAPP_f340725611e_bool (tptp.cOMBB_1348041619bool_a tptp.cOMBC_231445413l_bool) (tptp.hAPP_f1509969235l_bool @t18 @t17))) @t16) @t15 @t14)) tptp.bot_bo1208640912a_bool)))))) % 0.40/0.81 (assume @p6 @t31) % 0.40/0.81 (assume @p7 (forall (@list @t14 @t1 @t17 @t15 @t32) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t17 @t15 @t32)) tptp.bot_bo1208640912a_bool))) (=> (forall @t27 (=> (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t32 @t20) @t22)) (tptp.hBOOL (tptp.hAPP_state_bool @t21 @t22)))) @t19)))) % 0.40/0.81 (assume @p8 (forall (@list @t17 @t1 @t33 @t15 @t14) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t33 @t15 @t14)) tptp.bot_bo1208640912a_bool))) (=> (forall @t27 (=> @t26 (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t33 @t20) @t22)))) @t19)))) % 0.40/0.81 (assume @p9 (forall (@list @t14 @t17 @t1 @t33 @t15 @t32) (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t33 @t15 @t32)) tptp.bot_bo1208640912a_bool))) (=> (forall @t27 (=> @t26 (forall @t38 (=> (forall @t37 (=> (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t33 @t36) @t22)) (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t32 @t36) @t34)))) @t35)))) @t19)))) % 0.40/0.81 (assume @p10 (forall @t47 (=> @t46 (=> (not @t44) @t42)))) % 0.40/0.81 (assume @p11 (forall @t51 (=> (=> (not @t50) @t44) @t49))) % 0.40/0.81 (assume @p12 (forall @t52 (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p13 (forall @t52 (= (tptp.collec829051333iple_a @t55) @t54))) % 0.40/0.81 (assume @p14 (forall @t52 (= (tptp.collec829051333iple_a @t57) @t54))) % 0.40/0.81 (assume @p15 (forall @t63 (and (=> @t61 (= @t60 @t54)) (=> @t62 (= @t60 tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p16 (forall @t63 (and (=> @t61 (= @t64 @t54)) (=> @t62 (= @t64 tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p17 (forall @t67 (=> @t66 @t65))) % 0.40/0.81 (assume @p18 (forall @t73 (= (= @t72 tptp.bot_bo1208640912a_bool) @t71))) % 0.40/0.81 (assume @p19 (forall (@list @t74) (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t74) tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p20 (forall @t73 (= (= tptp.bot_bo1208640912a_bool @t72) @t71))) % 0.40/0.81 (assume @p21 (forall @t78 (= (exists @t70 @t77) @t75))) % 0.40/0.81 (assume @p22 (forall @t78 (= (forall @t70 (not @t77)) @t66))) % 0.40/0.81 (assume @p23 (= tptp.bot_bo1208640912a_bool (tptp.collec829051333iple_a (tptp.cOMBK_712844119iple_a tptp.fFalse)))) % 0.40/0.81 (assume @p24 (forall @t67 (=> @t42 (= @t79 @t39)))) % 0.40/0.81 (assume @p25 (forall @t51 (=> @t50 @t49))) % 0.40/0.81 (assume @p26 (forall (@list @t48 @t80 @t39) (=> @t85 (=> (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t83 @t48))) (= (= @t82 (tptp.hAPP_f16502863a_bool @t81 @t48)) (= @t39 @t48)))))) % 0.40/0.81 (assume @p27 (forall (@list @t87 @t39 @t80) (= (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t89 @t80)) (or (= @t87 @t80) @t86)))) % 0.40/0.81 (assume @p28 (forall @t47 (= @t46 (or @t44 @t42)))) % 0.40/0.81 (assume @p29 (forall (@list @t80 @t87 @t39) (= (tptp.hAPP_f16502863a_bool @t81 @t89) (tptp.hAPP_f16502863a_bool @t88 @t82)))) % 0.40/0.81 (assume @p30 (forall @t90 (= (tptp.hAPP_f16502863a_bool @t81 @t82) @t82))) % 0.40/0.81 (assume @p31 (forall @t91 (= (tptp.hAPP_f16502863a_bool @t53 @t72) (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool (tptp.cOMBB_196465322iple_a tptp.fimplies) (tptp.hAPP_f16502863a_bool (tptp.cOMBB_213049548iple_a tptp.fNot) @t57))) @t58))))) % 0.40/0.81 (assume @p32 (forall @t95 (= @t94 (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t93 @t57)) (tptp.hAPP_f16502863a_bool @t92 @t48)))))) % 0.40/0.81 (assume @p33 (forall @t95 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 @t94)))) % 0.40/0.81 (assume @p34 (forall (@list @t68 @t96) (= (tptp.hAPP_f16502863a_bool @t97 @t96) (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t93 (tptp.hAPP_H1027145665a_bool @t56 @t68))) (tptp.hAPP_f16502863a_bool @t92 @t96)))))) % 0.40/0.81 (assume @p35 (forall (@list @t40 @t43) (=> (= @t54 @t98) @t44))) % 0.40/0.81 (assume @p36 (forall @t101 (=> @t100 @t99))) % 0.40/0.81 (assume @p37 (forall (@list @t40 @t43 @t74 @t102) (= (= (tptp.hAPP_f16502863a_bool @t53 @t98) (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t74) (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t102) tptp.bot_bo1208640912a_bool))) (or (and (= @t40 @t74) (= @t43 @t102)) (and (= @t40 @t102) (= @t43 @t74)))))) % 0.40/0.81 (assume @p38 (forall @t101 (= @t100 @t99))) % 0.40/0.81 (assume @p39 (forall @t67 (not (= @t79 tptp.bot_bo1208640912a_bool)))) % 0.40/0.81 (assume @p40 (forall @t67 (not (= tptp.bot_bo1208640912a_bool @t79)))) % 0.40/0.81 (assume @p41 (forall @t104 (= (tptp.hAPP_f490779847iple_a tptp.the_el1997360207iple_a @t103) @t80))) % 0.40/0.81 (assume @p42 (forall @t104 (= (tptp.hBOOL (tptp.hAPP_H1448631928a_bool tptp.bot_bo1208640912a_bool @t80)) @t105))) % 0.40/0.81 (assume @p43 (forall @t70 (= @t106 @t105))) % 0.40/0.81 (assume @p44 (forall (@list @t1 @t17) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t17 tptp.skip @t17)) tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p45 (forall (@list @t108 @t107 @t1 @t17 @t15 @t14) (=> @t19 (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t14 @t108 @t107)) tptp.bot_bo1208640912a_bool))) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t17 (tptp.semi @t15 @t108) @t107)) tptp.bot_bo1208640912a_bool))))))) % 0.40/0.81 (assume @p46 (forall (@list @t87) (not (forall (@list @t111 @t110 @t109) (not (= @t87 (tptp.hoare_1652181356iple_a @t111 @t110 @t109))))))) % 0.40/0.81 (assume @p47 (forall @t90 (=> @t84 (not (forall @t113 (=> (= @t39 (tptp.hAPP_f16502863a_bool @t81 @t112)) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t83 @t112)))))))) % 0.40/0.81 (assume @p48 (forall @t117 (not (= @t116 tptp.skip)))) % 0.40/0.81 (assume @p49 (forall @t117 (not (= tptp.skip @t116)))) % 0.40/0.81 (assume @p50 (forall (@list @t118) (= (tptp.hAPP_f490779847iple_a tptp.the_el1997360207iple_a @t118) (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a (tptp.hAPP_f909473944a_bool (tptp.cOMBB_1083611331iple_a (tptp.hAPP_f625100287l_bool tptp.fequal1285825639a_bool @t118)) (tptp.hAPP_f993216280a_bool (tptp.hAPP_f1022403729a_bool tptp.cOMBC_825881325a_bool tptp.insert1434104874iple_a) tptp.bot_bo1208640912a_bool)))))) % 0.40/0.81 (assume @p51 (forall @t67 (=> @t42 (exists @t113 (and (= @t39 (tptp.hAPP_f16502863a_bool @t53 @t112)) (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t41 @t112)))))))) % 0.40/0.81 (assume @p52 (forall (@list @t122 @t120 @t121 @t119) (= (= (tptp.semi @t122 @t120) (tptp.semi @t121 @t119)) (and (= @t122 @t121) (= @t120 @t119))))) % 0.40/0.81 (assume @p53 (forall @t104 (= (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a (tptp.hAPP_H1027145665a_bool tptp.fequal1440857775iple_a @t80)) @t80))) % 0.40/0.81 (assume @p54 (forall @t52 (= (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a @t57) @t40))) % 0.40/0.81 (assume @p55 (forall (@list @t80 @t87 @t123) (and (=> @t125 (= @t80 @t124)) (=> (not @t125) (= @t87 @t124))))) % 0.40/0.81 (assume @p56 (forall @t78 (=> (forall @t127 (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t126) @t39)))) @t66))) % 0.40/0.81 (assume @p57 (forall @t63 (=> @t61 (=> @t130 @t129)))) % 0.40/0.81 (assume @p58 (forall @t63 (=> @t61 (=> @t130 @t131)))) % 0.40/0.81 (assume @p59 (forall @t91 (=> @t132 (=> @t61 @t129)))) % 0.40/0.81 (assume @p60 (forall @t73 (=> @t132 @t131))) % 0.40/0.81 (assume @p61 (forall (@list @t14 @t1 @t15 @t17) (=> (forall @t27 (=> @t26 (exists (@list @t134 @t133) (and (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t2 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a (tptp.hoare_1652181356iple_a @t134 @t15 @t133)) tptp.bot_bo1208640912a_bool))) (forall @t38 (=> (forall @t37 (=> (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t134 @t36) @t22)) (tptp.hBOOL (tptp.hAPP_state_bool (tptp.hAPP_a2036067514e_bool @t133 @t36) @t34)))) @t35)))))) @t19))) % 0.40/0.81 (assume @p62 (forall @t78 (= @t75 (exists (@list @t68 @t112) (and (= @t39 (tptp.hAPP_f16502863a_bool @t97 @t112)) (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t76 @t112)))))))) % 0.40/0.81 (assume @p63 (forall (@list @t135 @t40 @t43) (= (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite2098837632iple_a @t135 @t54) @t43)) @t44))) % 0.40/0.81 (assume @p64 (forall @t138 (=> @t137 (= (tptp.hAPP_f490779847iple_a @t136 @t103) @t80)))) % 0.40/0.81 (assume @p65 (forall @t70 (= @t106 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t76 tptp.bot_bo1208640912a_bool))))) % 0.40/0.81 (assume @p66 (forall (@list @t135 @t80) (not (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite2098837632iple_a @t135 tptp.bot_bo1208640912a_bool) @t80))))) % 0.40/0.81 (assume @p67 (forall (@list @t135 @t39 @t80) (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t139 @t80)) @t75))) % 0.40/0.81 (assume @p68 (forall (@list @t135 @t40 @t39 @t80) (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite148164294iple_a @t135 @t40 @t39) @t80)) (=> @t65 (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite2098837632iple_a @t135 @t79) @t80)))))) % 0.40/0.81 (assume @p69 (forall @t145 (=> @t137 (=> @t144 (=> @t85 @t143))))) % 0.40/0.81 (assume @p70 (forall @t148 (= @t147 (tptp.hAPP_f490779847iple_a tptp.the_Ho1307659873iple_a @t139)))) % 0.40/0.81 (assume @p71 (forall (@list @t149 @t58) (=> (or @t151 @t150) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t59 @t58)) @t149))))))) % 0.40/0.81 (assume @p72 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a tptp.bot_bo1208640912a_bool))) % 0.40/0.81 (assume @p73 (forall @t67 (=> @t144 @t152))) % 0.40/0.81 (assume @p74 (forall @t90 (= @t84 @t86))) % 0.40/0.81 (assume @p75 (forall @t73 (= @t72 @t58))) % 0.40/0.81 (assume @p76 (forall @t153 (=> @t137 (=> @t144 (= @t140 @t147))))) % 0.40/0.81 (assume @p77 (forall (@list @t135 @t154) (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t155 @t154)))) % 0.40/0.81 (assume @p78 (forall (@list @t135 @t154 @t80) (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t155 @t80)) (= @t80 @t154)))) % 0.40/0.81 (assume @p79 (forall (@list @t135 @t154 @t87 @t80 @t39) (=> @t85 (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t156 @t87)) (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite148164294iple_a @t135 @t154 @t82) (tptp.hAPP_H963118037iple_a @t141 @t87))))))) % 0.40/0.81 (assume @p80 (forall (@list @t58 @t149) (= (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a (tptp.collec829051333iple_a (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool (tptp.hAPP_f749678531l_bool @t93 @t58)) @t149)))) (and @t151 @t150)))) % 0.40/0.81 (assume @p81 (forall @t67 (= @t152 @t144))) % 0.40/0.81 (assume @p82 (forall (@list @t40 @t157 @t135) (=> (= @t157 @t146) (= (tptp.hAPP_f490779847iple_a @t157 @t54) @t40)))) % 0.40/0.81 (assume @p83 (forall (@list @t135 @t40) (= (tptp.hAPP_f490779847iple_a @t146 @t54) @t40))) % 0.40/0.81 (assume @p84 (forall @t153 (=> @t137 (=> @t144 (=> @t75 (=> (forall (@list @t68 @t126) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t158) (tptp.hAPP_f16502863a_bool @t97 (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool tptp.insert1434104874iple_a @t126) tptp.bot_bo1208640912a_bool))))) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool tptp.member127332739iple_a @t140) @t39)))))))) % 0.40/0.81 (assume @p85 (forall (@list @t135 @t40 @t118 @t80) (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite2098837632iple_a @t135 @t164) @t80)) (not (forall (@list @t160 @t159) (=> (= @t164 @t163) (=> (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t162 @t80)) @t161))))))) % 0.40/0.81 (assume @p86 (forall @t148 (=> @t144 (=> @t75 (exists @t166 (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t139 @t165))))))) % 0.40/0.81 (assume @p87 (forall @t175 (=> @t174 (=> (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t168 tptp.bot_bo1208640912a_bool)) (=> (forall @t173 (=> @t172 @t171)) @t169))))) % 0.40/0.81 (assume @p88 (forall (@list @t176) (= (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t176)) (or (= @t176 tptp.bot_bo1208640912a_bool) (exists (@list @t159 @t160) (and (= @t176 @t163) (tptp.hBOOL (tptp.hAPP_f1454306822l_bool tptp.finite68738179iple_a @t159)))))))) % 0.40/0.81 (assume @p89 (forall (@list @t135 @t154 @t39) (=> @t144 (exists @t166 (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t156 @t165)))))) % 0.40/0.81 (assume @p90 (forall (@list @t135 @t178 @t177) (= (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite2098837632iple_a @t135 @t178) @t177)) (exists (@list @t160 @t159 @t68) (and (= @t178 @t163) (= @t177 @t68) (tptp.hBOOL (tptp.hAPP_H1448631928a_bool @t162 @t68)) (not @t161)))))) % 0.40/0.81 (assume @p91 (forall (@list @t135 @t154 @t178 @t177) (= (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite148164294iple_a @t135 @t154 @t178) @t177)) (or (and (= @t178 tptp.bot_bo1208640912a_bool) (= @t177 @t154)) (exists (@list @t68 @t159 @t126) (and (= @t178 (tptp.hAPP_f16502863a_bool @t97 @t159)) (= @t177 @t158) (not (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t76 @t159))) (tptp.hBOOL (tptp.hAPP_H1448631928a_bool (tptp.finite148164294iple_a @t135 @t154 @t159) @t126)))))))) % 0.40/0.81 (assume @p92 (forall @t145 (=> @t179 (=> @t144 @t143)))) % 0.40/0.81 (assume @p93 (forall @t175 (=> @t174 (=> (not (= @t167 tptp.bot_bo1208640912a_bool)) (=> (forall @t70 (tptp.hBOOL (tptp.hAPP_f1454306822l_bool @t168 (tptp.hAPP_f16502863a_bool @t97 tptp.bot_bo1208640912a_bool)))) (=> (forall @t173 (=> @t172 (=> (not (= @t170 tptp.bot_bo1208640912a_bool)) @t171))) @t169)))))) % 0.40/0.81 (assume @p94 (forall @t138 (=> @t179 (= (tptp.hAPP_H963118037iple_a @t141 @t80) @t80)))) % 0.40/0.81 (assume @p95 (forall @t145 (=> @t179 (=> @t144 (=> @t84 (= @t142 @t140)))))) % 0.40/0.81 (assume @p96 (forall @t184 (or (not @t183) @t182))) % 0.40/0.81 (assume @p97 (forall @t184 (or @t181 @t183))) % 0.40/0.81 (assume @p98 (forall @t189 (or @t182 @t188 @t186))) % 0.40/0.81 (assume @p99 (forall @t191 (or @t190 @t181))) % 0.40/0.81 (assume @p100 (forall @t191 (or @t190 @t187))) % 0.40/0.81 (assume @p101 (forall @t189 (or @t182 @t192))) % 0.40/0.81 (assume @p102 (forall @t191 (or @t188 @t192))) % 0.40/0.81 (assume @p103 (forall @t191 (or (not @t192) @t181 @t187))) % 0.40/0.81 (assume @p104 (not @t193)) % 0.40/0.81 (assume @p105 (forall @t184 (or (= @t180 tptp.fTrue) (= @t180 tptp.fFalse)))) % 0.40/0.81 (assume @p106 (forall @t189 (or @t181 @t194))) % 0.40/0.81 (assume @p107 (forall @t191 (or @t188 @t194))) % 0.40/0.81 (assume @p108 (forall @t191 (or (not @t194) @t182 @t187))) % 0.40/0.81 (assume @p109 (forall @t199 (or (not @t198) @t197))) % 0.40/0.81 (assume @p110 (forall @t199 (or (not @t197) @t198))) % 0.40/0.81 (assume @p111 @t202) % 0.40/0.81 (assume @p112 @t206) % 0.40/0.81 (assume @p113 (forall (@list @t210 @t208 @t207) (= (tptp.hAPP_state_bool (tptp.hAPP_f1759915619e_bool (tptp.cOMBB_160679318_state @t210) @t208) @t207) (tptp.hAPP_bool_bool @t210 @t209)))) % 0.40/0.81 (assume @p114 (forall (@list @t211 @t185 @t207) (= (tptp.hAPP_state_bool (tptp.hAPP_b2019457360e_bool (tptp.hAPP_f167292325e_bool tptp.cOMBC_231445413l_bool @t211) @t185) @t207) (tptp.hAPP_bool_bool @t212 @t185)))) % 0.40/0.81 (assume @p115 (forall (@list @t211 @t208 @t207) (= (tptp.hAPP_state_bool (tptp.hAPP_f1759915619e_bool (tptp.hAPP_f644196280e_bool tptp.cOMBS_1378840469l_bool @t211) @t208) @t207) (tptp.hAPP_bool_bool @t212 @t209)))) % 0.40/0.81 (assume @p116 (forall (@list @t213 @t200 @t207) (= (tptp.hAPP_state_bool (tptp.hAPP_s1806633685e_bool (tptp.hAPP_f817621513e_bool tptp.cOMBC_2027030106e_bool @t213) @t200) @t207) (tptp.hAPP_state_bool (tptp.hAPP_s1806633685e_bool @t213 @t207) @t200)))) % 0.40/0.81 (assume @p117 (forall @t218 (or (not @t217) @t216))) % 0.40/0.81 (assume @p118 (forall @t218 (or (not @t216) @t217))) % 0.40/0.81 (assume @p119 (forall (@list @t220 @t185 @t219) (= (tptp.hAPP_a2036067514e_bool (tptp.hAPP_b540892988e_bool (tptp.hAPP_f1824947087e_bool tptp.cOMBC_41962815e_bool @t220) @t185) @t219) (tptp.hAPP_b2019457360e_bool (tptp.hAPP_a723219176e_bool @t220 @t219) @t185)))) % 0.40/0.81 (assume @p120 (forall (@list @t180 @t221) (= (tptp.hAPP_H1448631928a_bool (tptp.cOMBK_712844119iple_a @t180) @t221) @t180))) % 0.40/0.81 (assume @p121 (forall (@list @t222 @t208 @t207) (= (tptp.hAPP_s58564346l_bool (tptp.hAPP_f1259673775l_bool (tptp.cOMBB_188601460_state @t222) @t208) @t207) (tptp.hAPP_b589554111l_bool @t222 @t209)))) % 0.40/0.81 (assume @p122 (forall @t227 (or (not @t226) @t225))) % 0.40/0.81 (assume @p123 (forall @t227 (or (not @t225) @t226))) % 0.40/0.81 (assume @p124 (forall (@list @t210 @t229 @t228) (= (tptp.hAPP_H1448631928a_bool (tptp.hAPP_f16502863a_bool (tptp.cOMBB_213049548iple_a @t210) @t229) @t228) (tptp.hAPP_bool_bool @t210 @t230)))) % 0.40/0.81 (assume @p125 (forall (@list @t231 @t229 @t228) (= (tptp.hAPP_H1448631928a_bool (tptp.hAPP_f16502863a_bool (tptp.hAPP_f2112551770a_bool tptp.cOMBS_2061548107l_bool @t231) @t229) @t228) (tptp.hAPP_bool_bool (tptp.hAPP_H1487873860l_bool @t231 @t228) @t230)))) % 0.40/0.81 (assume @p126 (forall (@list @t232 @t208 @t219) (= (tptp.hAPP_a2036067514e_bool (tptp.hAPP_f762886889e_bool (tptp.hAPP_f1261923407e_bool tptp.cOMBC_892787026e_bool @t232) @t208) @t219) (tptp.hAPP_f1759915619e_bool (tptp.hAPP_a1200519163e_bool @t232 @t219) @t208)))) % 0.40/0.81 (assume @p127 (forall (@list @t222 @t229 @t228) (= (tptp.hAPP_H1487873860l_bool (tptp.hAPP_f749678531l_bool (tptp.cOMBB_196465322iple_a @t222) @t229) @t228) (tptp.hAPP_b589554111l_bool @t222 @t230)))) % 0.40/0.81 (assume @p128 (forall (@list @t234 @t233 @t219) (= (tptp.hAPP_a849909144l_bool (tptp.hAPP_f1509969235l_bool (tptp.cOMBB_1355796797bool_a @t234) @t233) @t219) (tptp.hAPP_f1259673775l_bool @t234 (tptp.hAPP_a2036067514e_bool @t233 @t219))))) % 0.40/0.81 (assume @p129 (forall (@list @t235 @t221 @t228) (= (tptp.hAPP_H1448631928a_bool (tptp.hAPP_H1027145665a_bool (tptp.hAPP_f1216137953a_bool tptp.cOMBC_671859290a_bool @t235) @t221) @t228) (tptp.hAPP_H1448631928a_bool (tptp.hAPP_H1027145665a_bool @t235 @t228) @t221)))) % 0.40/0.81 (assume @p130 (forall (@list @t238 @t236 @t219) (= (tptp.hAPP_a723219176e_bool (tptp.hAPP_f340725611e_bool (tptp.cOMBB_1348041619bool_a @t238) @t236) @t219) (tptp.hAPP_f167292325e_bool @t238 @t237)))) % 0.40/0.81 (assume @p131 (forall (@list @t240 @t239 @t228) (= (tptp.hAPP_H1448631928a_bool (tptp.hAPP_f909473944a_bool (tptp.cOMBB_1083611331iple_a @t240) @t239) @t228) (tptp.hAPP_f1454306822l_bool @t240 (tptp.hAPP_H1027145665a_bool @t239 @t228))))) % 0.40/0.81 (assume @p132 (forall (@list @t241 @t229 @t228) (= (tptp.hAPP_H1448631928a_bool (tptp.hAPP_f16502863a_bool (tptp.hAPP_f684479953a_bool tptp.cOMBC_862840740l_bool @t241) @t229) @t228) (tptp.hAPP_f1454306822l_bool (tptp.hAPP_H694056973l_bool @t241 @t228) @t229)))) % 0.40/0.81 (assume @p133 (forall (@list @t242 @t236 @t219) (= (tptp.hAPP_a1200519163e_bool (tptp.hAPP_f963367678e_bool (tptp.cOMBB_145932198bool_a @t242) @t236) @t219) (tptp.hAPP_f644196280e_bool @t242 @t237)))) % 0.40/0.81 (assume @p134 (forall (@list @t243 @t229 @t228) (= (tptp.hAPP_H1027145665a_bool (tptp.hAPP_f993216280a_bool (tptp.hAPP_f1022403729a_bool tptp.cOMBC_825881325a_bool @t243) @t229) @t228) (tptp.hAPP_f16502863a_bool (tptp.hAPP_H1975128022a_bool @t243 @t228) @t229)))) % 0.40/0.81 (assume @p135 (not @t248)) % 0.40/0.81 (assume @p136 true) % 0.40/0.81 (step @p137 :rule evaluate :args ((= false true))) % 0.40/0.81 (step @p138 :rule bool-impl-elim :args (@t249 @t19)) % 0.40/0.81 (step @p139 :rule cong :premises (@p138) :args ((forall @t30 (=> @t249 @t19)))) % 0.40/0.81 (step @p140 :rule refl :args (@t19)) % 0.40/0.81 (step @p141 :rule bool-impl-elim :args (@t26 @t25)) % 0.40/0.81 (step @p142 :rule cong :premises (@p141) :args (@t28)) % 0.40/0.81 (step @p143 :rule cong :premises (@p142 @p140) :args (@t29)) % 0.40/0.81 (step @p144 :rule cong :premises (@p143) :args (@t31)) % 0.40/0.81 (step @p145 :rule trans :premises (@p144 @p139)) % 0.40/0.81 (step @p146 :rule eq_resolve :premises (@p6 @p145)) % 0.40/0.81 (step @p147 :rule instantiate :premises (@p146) :args ((@list tptp.g tptp.c @t244 @t246))) % 0.40/0.81 (step @p148 :rule cnf_or_pos :args (@t252)) % 0.40/0.81 (step @p149 :rule reordering :premises (@p148) :args ((or @t248 @t251 (not @t252)))) % 0.40/0.81 (step @p150 :rule chain_m_resolution :premises (@p149 @p135 @p147) :args (@t251 (@list true false) (@list @t248 @t252))) % 0.40/0.81 (step @p151 :rule skolemize :premises (@p150)) % 0.40/0.81 (step @p152 :rule bool-double-not-elim :args (@t255)) % 0.40/0.81 (step @p153 :rule refl :args (@t257)) % 0.40/0.81 (step @p154 :rule nary_cong :premises (@p153 @p152) :args ((or @t257 (not @t256)))) % 0.40/0.81 (step @p155 :rule cnf_or_neg :args (@t257 0)) % 0.40/0.81 (step @p156 :rule eq_resolve :premises (@p155 @p154)) % 0.40/0.81 (step @p157 :rule reordering :premises (@p156) :args ((or @t255 @t257))) % 0.40/0.81 (step @p158 :rule chain_m_resolution :premises (@p157 @p151) :args (@t255 (@list true) (@list @t257))) % 0.40/0.81 (step @p159 :rule true_intro :premises (@p158)) % 0.40/0.81 (step @p160 :rule refl :args (@t253)) % 0.40/0.81 (step @p161 :rule eq-symm :args (@t205 @t203)) % 0.40/0.81 (step @p162 :rule cong :premises (@p161) :args (@t206)) % 0.40/0.81 (step @p163 :rule eq_resolve :premises (@p112 @p162)) % 0.40/0.81 (step @p164 :rule instantiate :premises (@p163) :args ((@list @t245 @t254))) % 0.40/0.81 (step @p165 :rule cong :premises (@p164 @p160) :args ((tptp.hAPP_state_bool @t245 @t253))) % 0.40/0.81 (step @p166 :rule eq-symm :args (@t201 @t180)) % 0.40/0.81 (step @p167 :rule cong :premises (@p166) :args (@t202)) % 0.40/0.81 (step @p168 :rule eq_resolve :premises (@p111 @p167)) % 0.40/0.81 (step @p169 :rule instantiate :premises (@p168) :args ((@list tptp.fFalse @t253))) % 0.40/0.81 (step @p170 :rule trans :premises (@p169 @p165)) % 0.40/0.81 (step @p171 :rule cong :premises (@p170) :args (@t193)) % 0.40/0.81 (step @p172 :rule false_intro :premises (@p104)) % 0.40/0.81 (step @p173 :rule symm :premises (@p172)) % 0.40/0.81 (step @p174 :rule trans :premises (@p173 @p171 @p159)) % 0.40/0.81 (step @p175 false :rule eq_resolve :premises (@p174 @p137)) % 0.40/0.81 ) % 0.40/0.81 % SZS output end Proof % 0.40/0.81 % cvc5 exiting %------------------------------------------------------------------------------