%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP145^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:25:11 AM UTC 2026 % Result : Theorem 0.85s 1.09s % Output : Proof 0.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP145^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n019.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 04:16:04 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.66 %----Proving TH0 % 0.85/1.09 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.85/1.09 % SZS status Theorem % 0.85/1.09 % SZS output start Proof % 0.85/1.09 ( % 0.85/1.09 (declare-sort tptp.list_list_com 0) % 0.85/1.09 (declare-sort tptp.set_Pr1142642759_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr602326075st_com 0) % 0.85/1.09 (declare-sort tptp.com 0) % 0.85/1.09 (declare-sort tptp.list_com 0) % 0.85/1.09 (declare-sort tptp.list_P890094829_state 0) % 0.85/1.09 (declare-sort tptp.list_P1040014977_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr2096893127_state 0) % 0.85/1.09 (declare-sort tptp.produc2041926651_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr849496667_state 0) % 0.85/1.09 (declare-sort tptp.state 0) % 0.85/1.09 (declare-sort tptp.produc186437863_state 0) % 0.85/1.09 (declare-sort tptp.set_state 0) % 0.85/1.09 (declare-sort tptp.produc1225889383_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr541394119_state 0) % 0.85/1.09 (declare-sort tptp.produc2046512871_state 0) % 0.85/1.09 (declare-sort tptp.produc410756839_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr1165141447_state 0) % 0.85/1.09 (declare-sort tptp.list_state 0) % 0.85/1.09 (declare-sort tptp.produc1393453339_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr391631483_state 0) % 0.85/1.09 (declare-sort tptp.produc1586269031_state 0) % 0.85/1.09 (declare-sort tptp.set_Pr1325664839_state 0) % 0.85/1.09 (declare-sort tptp.nat 0) % 0.85/1.09 (declare-sort tptp.produc2058209240st_com 0) % 0.85/1.09 (declare-sort tptp.set_nat 0) % 0.85/1.09 (declare-sort tptp.set_Pr1822651163om_com 0) % 0.85/1.09 (declare-sort tptp.produc258871771st_com 0) % 0.85/1.09 (declare-sort tptp.product_prod_com_com 0) % 0.85/1.09 (declare-const tptp.pHoare259243666_exec1 tptp.set_Pr1165141447_state) % 0.85/1.09 (declare-const tptp.suc (-> tptp.nat tptp.nat)) % 0.85/1.09 (declare-const tptp.produc1909270103_state (-> tptp.produc2041926651_state tptp.produc2041926651_state tptp.produc410756839_state)) % 0.85/1.09 (declare-const tptp.member1069318160_state (-> tptp.produc410756839_state tptp.set_Pr1165141447_state Bool)) % 0.85/1.09 (declare-const tptp.zero_zero_nat tptp.nat) % 0.85/1.09 (declare-const tptp.produc1204172211_state (-> tptp.list_com tptp.state tptp.produc2041926651_state)) % 0.85/1.09 (declare-const tptp.n tptp.nat) % 0.85/1.09 (declare-const tptp.irrefl_com (-> tptp.set_Pr1822651163om_com Bool)) % 0.85/1.09 (declare-const tptp.f (-> tptp.nat tptp.produc2041926651_state)) % 0.85/1.09 (declare-const tptp.lexord1893203674_state (-> tptp.set_Pr2096893127_state tptp.set_Pr1325664839_state)) % 0.85/1.09 (declare-const tptp.c tptp.com) % 0.85/1.09 (declare-const tptp.lexord1062073966_state (-> tptp.set_Pr1165141447_state tptp.set_Pr1142642759_state)) % 0.85/1.09 (declare-const tptp.lexord_com (-> tptp.set_Pr1822651163om_com tptp.set_Pr602326075st_com)) % 0.85/1.09 (declare-const tptp.concat_com (-> tptp.list_list_com tptp.list_com)) % 0.85/1.09 (declare-const tptp.transi863150634cl_com (-> tptp.set_Pr1822651163om_com tptp.set_Pr1822651163om_com)) % 0.85/1.09 (declare-const tptp.transi1965148016_state (-> tptp.set_Pr1325664839_state tptp.set_Pr1325664839_state)) % 0.85/1.09 (declare-const tptp.transi339813252_state (-> tptp.set_Pr1142642759_state tptp.set_Pr1142642759_state)) % 0.85/1.09 (declare-const tptp.transi436345274st_com (-> tptp.set_Pr602326075st_com tptp.set_Pr602326075st_com)) % 0.85/1.09 (declare-const tptp.maps_com_com (-> (-> tptp.com tptp.list_com) tptp.list_com tptp.list_com)) % 0.85/1.09 (declare-const tptp.listre1725776070_state (-> tptp.set_Pr2096893127_state tptp.set_Pr1325664839_state)) % 0.85/1.09 (declare-const tptp.listre1738592858_state (-> tptp.set_Pr1165141447_state tptp.set_Pr1142642759_state)) % 0.85/1.09 (declare-const tptp.product_lists_com (-> tptp.list_list_com tptp.list_list_com)) % 0.85/1.09 (declare-const tptp.n_lists_com (-> tptp.nat tptp.list_com tptp.list_list_com)) % 0.85/1.09 (declare-const tptp.collec489924946_state (-> (-> tptp.produc186437863_state Bool) tptp.set_Pr2096893127_state)) % 0.85/1.09 (declare-const tptp.produc1914379986st_com (-> (-> tptp.com tptp.com Bool) tptp.list_com tptp.produc2058209240st_com)) % 0.85/1.09 (declare-const tptp.member423306384_state (-> tptp.produc1586269031_state tptp.set_Pr1325664839_state Bool)) % 0.85/1.09 (declare-const tptp.s tptp.state) % 0.85/1.09 (declare-const tptp.cons_list_com (-> tptp.list_com tptp.list_list_com tptp.list_list_com)) % 0.85/1.09 (declare-const tptp.produc1307105171st_com (-> tptp.list_com tptp.list_com tptp.produc258871771st_com)) % 0.85/1.09 (declare-const tptp.exec (-> tptp.state tptp.com tptp.state Bool)) % 0.85/1.09 (declare-const tptp.semi (-> tptp.com tptp.com tptp.com)) % 0.85/1.09 (declare-const tptp.append_list_com (-> tptp.list_list_com tptp.list_list_com tptp.list_list_com)) % 0.85/1.09 (declare-const tptp.member_state (-> tptp.state tptp.set_state Bool)) % 0.85/1.09 (declare-const tptp.bind_com_com (-> tptp.list_com (-> tptp.com tptp.list_com) tptp.list_com)) % 0.85/1.09 (declare-const tptp.collect_state (-> (-> tptp.state Bool) tptp.set_state)) % 0.85/1.09 (declare-const tptp.listrel_com_com (-> tptp.set_Pr1822651163om_com tptp.set_Pr602326075st_com)) % 0.85/1.09 (declare-const tptp.collec300063826_state (-> (-> tptp.produc410756839_state Bool) tptp.set_Pr1165141447_state)) % 0.85/1.09 (declare-const tptp.pHoare806997636termis (-> tptp.list_com tptp.state Bool)) % 0.85/1.09 (declare-const tptp.transi152726506_state (-> tptp.set_Pr541394119_state tptp.set_Pr541394119_state)) % 0.85/1.09 (declare-const tptp.nil_com tptp.list_com) % 0.85/1.09 (declare-const tptp.transi1995721864_state (-> tptp.set_Pr541394119_state tptp.set_Pr541394119_state)) % 0.85/1.09 (declare-const tptp.cond (-> (-> tptp.state Bool) tptp.com tptp.com tptp.com)) % 0.85/1.09 (declare-const tptp.produc2065881943_state (-> tptp.produc410756839_state tptp.produc410756839_state tptp.produc186437863_state)) % 0.85/1.09 (declare-const tptp.nil_Pr1347322605_state tptp.list_P890094829_state) % 0.85/1.09 (declare-const tptp.member512523024_state (-> tptp.produc186437863_state tptp.set_Pr2096893127_state Bool)) % 0.85/1.09 (declare-const tptp.nil_list_com tptp.list_list_com) % 0.85/1.09 (declare-const tptp.product_Pair_com_com (-> tptp.com tptp.com tptp.product_prod_com_com)) % 0.85/1.09 (declare-const tptp.transi463013610_state (-> tptp.set_Pr2096893127_state tptp.set_Pr2096893127_state)) % 0.85/1.09 (declare-const tptp.termi (-> tptp.com tptp.state Bool)) % 0.85/1.09 (declare-const tptp.cons_com (-> tptp.com tptp.list_com tptp.list_com)) % 0.85/1.09 (declare-const tptp.transi1666849160_state (-> tptp.set_Pr2096893127_state tptp.set_Pr2096893127_state)) % 0.85/1.09 (declare-const tptp.do (-> (-> tptp.state tptp.set_state) tptp.com)) % 0.85/1.09 (declare-const tptp.produc2049704791_state (-> tptp.produc186437863_state tptp.produc186437863_state tptp.produc2046512871_state)) % 0.85/1.09 (declare-const tptp.transi1726587420_state (-> tptp.set_Pr1165141447_state tptp.set_Pr1165141447_state)) % 0.85/1.09 (declare-const tptp.pHoare259243732_execs (-> tptp.state tptp.list_com tptp.state Bool)) % 0.85/1.09 (declare-const tptp.transi1302705790_state (-> tptp.set_Pr1165141447_state tptp.set_Pr1165141447_state)) % 0.85/1.09 (declare-const tptp.member284400400_state (-> tptp.produc2046512871_state tptp.set_Pr541394119_state Bool)) % 0.85/1.09 (declare-const tptp.produc1298457559_state (-> tptp.list_P1040014977_state tptp.list_P1040014977_state tptp.produc1225889383_state)) % 0.85/1.09 (declare-const tptp.subseqs_com (-> tptp.list_com tptp.list_list_com)) % 0.85/1.09 (declare-const tptp.gen_length_com (-> tptp.nat tptp.list_com tptp.nat)) % 0.85/1.09 (declare-const tptp.append982487830_state (-> tptp.list_P1040014977_state tptp.list_P1040014977_state tptp.list_P1040014977_state)) % 0.85/1.09 (declare-const tptp.member32358020st_com (-> tptp.produc258871771st_com tptp.set_Pr602326075st_com Bool)) % 0.85/1.09 (declare-const tptp.insert_com (-> tptp.com tptp.list_com tptp.list_com)) % 0.85/1.09 (declare-const tptp.append221843330_state (-> tptp.list_P890094829_state tptp.list_P890094829_state tptp.list_P890094829_state)) % 0.85/1.09 (declare-const tptp.member64234660_state (-> tptp.produc2041926651_state tptp.set_Pr849496667_state Bool)) % 0.85/1.09 (declare-const tptp.while (-> (-> tptp.state Bool) tptp.com tptp.com)) % 0.85/1.09 (declare-const tptp.nths_com (-> tptp.list_com tptp.set_nat tptp.list_com)) % 0.85/1.09 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.85/1.09 (declare-const tptp.member1333916004om_com (-> tptp.product_prod_com_com tptp.set_Pr1822651163om_com Bool)) % 0.85/1.09 (declare-const tptp.produc1742567891_state (-> tptp.list_list_com tptp.list_state tptp.produc1393453339_state)) % 0.85/1.09 (declare-const tptp.listre1268245261_state (-> tptp.set_Pr849496667_state tptp.set_Pr391631483_state)) % 0.85/1.09 (declare-const tptp.append_com (-> tptp.list_com tptp.list_com tptp.list_com)) % 0.85/1.09 (declare-const tptp.member1442949316_state (-> tptp.produc1393453339_state tptp.set_Pr391631483_state Bool)) % 0.85/1.09 (declare-const tptp.cons_state (-> tptp.state tptp.list_state tptp.list_state)) % 0.85/1.09 (declare-const tptp.nil_state tptp.list_state) % 0.85/1.09 (declare-const tptp.listre194873521_state (-> tptp.set_Pr1165141447_state tptp.set_Pr1142642759_state)) % 0.85/1.09 (declare-const tptp.member1267359376_state (-> tptp.produc1225889383_state tptp.set_Pr1142642759_state Bool)) % 0.85/1.09 (declare-const tptp.cons_P465369265_state (-> tptp.produc2041926651_state tptp.list_P1040014977_state tptp.list_P1040014977_state)) % 0.85/1.09 (declare-const tptp.nil_Pr1844458753_state tptp.list_P1040014977_state) % 0.85/1.09 (declare-const tptp.listre1244407729_state (-> tptp.set_Pr2096893127_state tptp.set_Pr1325664839_state)) % 0.85/1.09 (declare-const tptp.produc1354769367_state (-> tptp.list_P890094829_state tptp.list_P890094829_state tptp.produc1586269031_state)) % 0.85/1.09 (declare-const tptp.cons_P438230685_state (-> tptp.produc410756839_state tptp.list_P890094829_state tptp.list_P890094829_state)) % 0.85/1.09 (declare-const tptp.listrel1_com (-> tptp.set_Pr1822651163om_com tptp.set_Pr602326075st_com)) % 0.85/1.09 (define tptp.pHoare2126160787le_inf () (let ((_let_1 (@var "I3" tptp.nat))) (let ((_let_2 (@var "F3" (-> tptp.nat tptp.produc2041926651_state)))) (let ((_let_3 (@var "S3" tptp.state))) (let ((_let_4 (@var "Cs2" tptp.list_com))) (lambda (@list _let_4 _let_3) (exists (@list _let_2) (and (= (_ _let_2 tptp.zero_zero_nat) (_ (_ tptp.produc1204172211_state _let_4) _let_3)) (forall (@list _let_1) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ _let_2 _let_1)) (_ _let_2 (_ tptp.suc _let_1)))) tptp.pHoare259243666_exec1)))))))))) % 0.85/1.09 (define @t1 () (@var "S2" tptp.state)) % 0.85/1.09 (define @t2 () (@var "Cs" tptp.list_com)) % 0.85/1.09 (define @t3 () (_ tptp.produc1204172211_state @t2)) % 0.85/1.09 (define @t4 () (_ @t3 @t1)) % 0.85/1.09 (define @t5 () (@var "S" tptp.state)) % 0.85/1.09 (define @t6 () (_ tptp.produc1204172211_state tptp.nil_com)) % 0.85/1.09 (define @t7 () (@var "R" tptp.set_Pr2096893127_state)) % 0.85/1.09 (define @t8 () (@var "I2" tptp.nat)) % 0.85/1.09 (define @t9 () (_ tptp.suc @t8)) % 0.85/1.09 (define @t10 () (@var "F2" (-> tptp.nat tptp.produc410756839_state))) % 0.85/1.09 (define @t11 () (@list @t8)) % 0.85/1.09 (define @t12 () (@var "A" tptp.produc410756839_state)) % 0.85/1.09 (define @t13 () (exists (@list @t10) (and (= (_ @t10 tptp.zero_zero_nat) @t12) (forall @t11 (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state (_ @t10 @t8)) (_ @t10 @t9))) @t7))))) % 0.85/1.09 (define @t14 () (@var "I" tptp.nat)) % 0.85/1.09 (define @t15 () (_ tptp.suc @t14)) % 0.85/1.09 (define @t16 () (@var "F" (-> tptp.nat tptp.produc410756839_state))) % 0.85/1.09 (define @t17 () (_ @t16 @t14)) % 0.85/1.09 (define @t18 () (_ tptp.transi463013610_state @t7)) % 0.85/1.09 (define @t19 () (_ tptp.produc2065881943_state @t12)) % 0.85/1.09 (define @t20 () (@list @t14)) % 0.85/1.09 (define @t21 () (forall @t20 (and (_ (_ tptp.member512523024_state (_ @t19 @t17)) @t18) (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t17) (_ @t16 @t15))) @t7)))) % 0.85/1.09 (define @t22 () (@var "R" tptp.set_Pr1165141447_state)) % 0.85/1.09 (define @t23 () (@var "F2" (-> tptp.nat tptp.produc2041926651_state))) % 0.85/1.09 (define @t24 () (@var "A" tptp.produc2041926651_state)) % 0.85/1.09 (define @t25 () (exists (@list @t23) (and (= (_ @t23 tptp.zero_zero_nat) @t24) (forall @t11 (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ @t23 @t8)) (_ @t23 @t9))) @t22))))) % 0.85/1.09 (define @t26 () (@var "F" (-> tptp.nat tptp.produc2041926651_state))) % 0.85/1.09 (define @t27 () (_ @t26 @t14)) % 0.85/1.09 (define @t28 () (_ tptp.transi1302705790_state @t22)) % 0.85/1.09 (define @t29 () (_ tptp.produc1909270103_state @t24)) % 0.85/1.09 (define @t30 () (forall @t20 (and (_ (_ tptp.member1069318160_state (_ @t29 @t27)) @t28) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t27) (_ @t26 @t15))) @t22)))) % 0.85/1.09 (define @t31 () (@var "B" tptp.produc410756839_state)) % 0.85/1.09 (define @t32 () (_ @t19 @t31)) % 0.85/1.09 (define @t33 () (_ tptp.member512523024_state @t32)) % 0.85/1.09 (define @t34 () (_ @t33 @t18)) % 0.85/1.09 (define @t35 () (@var "B" tptp.produc2041926651_state)) % 0.85/1.09 (define @t36 () (_ @t29 @t35)) % 0.85/1.09 (define @t37 () (_ tptp.member1069318160_state @t36)) % 0.85/1.09 (define @t38 () (_ @t37 @t28)) % 0.85/1.09 (define @t39 () (@var "C2" tptp.com)) % 0.85/1.09 (define @t40 () (@var "C" tptp.com)) % 0.85/1.09 (define @t41 () (_ (_ tptp.termi @t40) @t5)) % 0.85/1.09 (define @t42 () (_ tptp.transi1302705790_state tptp.pHoare259243666_exec1)) % 0.85/1.09 (define @t43 () (_ tptp.cons_com @t40)) % 0.85/1.09 (define @t44 () (_ @t43 tptp.nil_com)) % 0.85/1.09 (define @t45 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t44) @t5))) % 0.85/1.09 (define @t46 () (@var "R2" tptp.set_Pr2096893127_state)) % 0.85/1.09 (define @t47 () (_ tptp.transi463013610_state @t46)) % 0.85/1.09 (define @t48 () (@list @t46)) % 0.85/1.09 (define @t49 () (@var "R2" tptp.set_Pr1165141447_state)) % 0.85/1.09 (define @t50 () (_ tptp.transi1302705790_state @t49)) % 0.85/1.09 (define @t51 () (@list @t49)) % 0.85/1.09 (define @t52 () (_ tptp.transi1666849160_state @t46)) % 0.85/1.09 (define @t53 () (_ tptp.transi1726587420_state @t49)) % 0.85/1.09 (define @t54 () (@var "By" tptp.produc410756839_state)) % 0.85/1.09 (define @t55 () (@var "Bx" tptp.produc410756839_state)) % 0.85/1.09 (define @t56 () (@var "P" (-> tptp.produc410756839_state tptp.produc410756839_state Bool))) % 0.85/1.09 (define @t57 () (_ (_ @t56 @t55) @t54)) % 0.85/1.09 (define @t58 () (@var "Ba" tptp.produc410756839_state)) % 0.85/1.09 (define @t59 () (@var "Aa" tptp.produc410756839_state)) % 0.85/1.09 (define @t60 () (_ (_ @t56 @t59) @t58)) % 0.85/1.09 (define @t61 () (@var "B2" tptp.produc410756839_state)) % 0.85/1.09 (define @t62 () (@var "A2" tptp.produc410756839_state)) % 0.85/1.09 (define @t63 () (_ @t56 @t62)) % 0.85/1.09 (define @t64 () (_ @t63 @t61)) % 0.85/1.09 (define @t65 () (@var "R" tptp.set_Pr541394119_state)) % 0.85/1.09 (define @t66 () (_ (_ tptp.produc2065881943_state @t59) @t58)) % 0.85/1.09 (define @t67 () (_ tptp.produc2065881943_state @t62)) % 0.85/1.09 (define @t68 () (_ @t67 @t61)) % 0.85/1.09 (define @t69 () (_ tptp.produc2049704791_state @t68)) % 0.85/1.09 (define @t70 () (_ (_ tptp.member284400400_state (_ @t69 @t66)) @t65)) % 0.85/1.09 (define @t71 () (=> @t70 (=> @t64 @t60))) % 0.85/1.09 (define @t72 () (_ tptp.transi1995721864_state @t65)) % 0.85/1.09 (define @t73 () (@var "Ay" tptp.produc410756839_state)) % 0.85/1.09 (define @t74 () (@var "Ax" tptp.produc410756839_state)) % 0.85/1.09 (define @t75 () (_ tptp.produc2049704791_state (_ (_ tptp.produc2065881943_state @t74) @t73))) % 0.85/1.09 (define @t76 () (_ tptp.member284400400_state (_ @t75 @t68))) % 0.85/1.09 (define @t77 () (@list @t62 @t61 @t59 @t58)) % 0.85/1.09 (define @t78 () (@list @t62 @t61)) % 0.85/1.09 (define @t79 () (_ (_ tptp.produc2065881943_state @t55) @t54)) % 0.85/1.09 (define @t80 () (_ tptp.member284400400_state (_ @t75 @t79))) % 0.85/1.09 (define @t81 () (@list @t74 @t73 @t55 @t54 @t65 @t56)) % 0.85/1.09 (define @t82 () (@var "By" tptp.produc2041926651_state)) % 0.85/1.09 (define @t83 () (@var "Bx" tptp.produc2041926651_state)) % 0.85/1.09 (define @t84 () (@var "P" (-> tptp.produc2041926651_state tptp.produc2041926651_state Bool))) % 0.85/1.09 (define @t85 () (_ (_ @t84 @t83) @t82)) % 0.85/1.09 (define @t86 () (@var "Ba" tptp.produc2041926651_state)) % 0.85/1.09 (define @t87 () (@var "Aa" tptp.produc2041926651_state)) % 0.85/1.09 (define @t88 () (_ (_ @t84 @t87) @t86)) % 0.85/1.09 (define @t89 () (@var "B2" tptp.produc2041926651_state)) % 0.85/1.09 (define @t90 () (@var "A2" tptp.produc2041926651_state)) % 0.85/1.09 (define @t91 () (_ @t84 @t90)) % 0.85/1.09 (define @t92 () (_ @t91 @t89)) % 0.85/1.09 (define @t93 () (_ (_ tptp.produc1909270103_state @t87) @t86)) % 0.85/1.09 (define @t94 () (_ tptp.produc1909270103_state @t90)) % 0.85/1.09 (define @t95 () (_ @t94 @t89)) % 0.85/1.09 (define @t96 () (_ tptp.produc2065881943_state @t95)) % 0.85/1.09 (define @t97 () (_ (_ tptp.member512523024_state (_ @t96 @t93)) @t7)) % 0.85/1.09 (define @t98 () (=> @t97 (=> @t92 @t88))) % 0.85/1.09 (define @t99 () (_ tptp.transi1666849160_state @t7)) % 0.85/1.09 (define @t100 () (@var "Ay" tptp.produc2041926651_state)) % 0.85/1.09 (define @t101 () (@var "Ax" tptp.produc2041926651_state)) % 0.85/1.09 (define @t102 () (_ tptp.produc2065881943_state (_ (_ tptp.produc1909270103_state @t101) @t100))) % 0.85/1.09 (define @t103 () (_ tptp.member512523024_state (_ @t102 @t95))) % 0.85/1.09 (define @t104 () (@list @t90 @t89 @t87 @t86)) % 0.85/1.09 (define @t105 () (@list @t90 @t89)) % 0.85/1.09 (define @t106 () (_ (_ tptp.produc1909270103_state @t83) @t82)) % 0.85/1.09 (define @t107 () (_ tptp.member512523024_state (_ @t102 @t106))) % 0.85/1.09 (define @t108 () (@list @t101 @t100 @t83 @t82 @t7 @t84)) % 0.85/1.09 (define @t109 () (@var "By" tptp.state)) % 0.85/1.09 (define @t110 () (@var "Bx" tptp.list_com)) % 0.85/1.09 (define @t111 () (@var "P" (-> tptp.list_com tptp.state Bool))) % 0.85/1.09 (define @t112 () (_ (_ @t111 @t110) @t109)) % 0.85/1.09 (define @t113 () (@var "Ba" tptp.state)) % 0.85/1.09 (define @t114 () (@var "Aa" tptp.list_com)) % 0.85/1.09 (define @t115 () (_ (_ @t111 @t114) @t113)) % 0.85/1.09 (define @t116 () (@var "B2" tptp.state)) % 0.85/1.09 (define @t117 () (@var "A2" tptp.list_com)) % 0.85/1.09 (define @t118 () (_ (_ @t111 @t117) @t116)) % 0.85/1.09 (define @t119 () (_ (_ tptp.produc1204172211_state @t114) @t113)) % 0.85/1.09 (define @t120 () (_ (_ tptp.produc1204172211_state @t117) @t116)) % 0.85/1.09 (define @t121 () (_ tptp.produc1909270103_state @t120)) % 0.85/1.09 (define @t122 () (_ (_ tptp.member1069318160_state (_ @t121 @t119)) @t22)) % 0.85/1.09 (define @t123 () (=> @t122 (=> @t118 @t115))) % 0.85/1.09 (define @t124 () (_ tptp.transi1726587420_state @t22)) % 0.85/1.09 (define @t125 () (@var "Ay" tptp.state)) % 0.85/1.09 (define @t126 () (@var "Ax" tptp.list_com)) % 0.85/1.09 (define @t127 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t126) @t125))) % 0.85/1.09 (define @t128 () (_ tptp.member1069318160_state (_ @t127 @t120))) % 0.85/1.09 (define @t129 () (@list @t117 @t116 @t114 @t113)) % 0.85/1.09 (define @t130 () (@list @t117 @t116)) % 0.85/1.09 (define @t131 () (_ (_ tptp.produc1204172211_state @t110) @t109)) % 0.85/1.09 (define @t132 () (_ tptp.member1069318160_state (_ @t127 @t131))) % 0.85/1.09 (define @t133 () (@list @t126 @t125 @t110 @t109 @t22 @t111)) % 0.85/1.09 (define @t134 () (_ tptp.transi152726506_state @t65)) % 0.85/1.09 (define @t135 () (_ (_ @t56 @t74) @t73)) % 0.85/1.09 (define @t136 () (_ @t80 @t134)) % 0.85/1.09 (define @t137 () (_ (_ @t84 @t101) @t100)) % 0.85/1.09 (define @t138 () (_ @t107 @t18)) % 0.85/1.09 (define @t139 () (_ (_ @t111 @t126) @t125)) % 0.85/1.09 (define @t140 () (_ @t132 @t28)) % 0.85/1.09 (define @t141 () (@var "Zb" tptp.produc410756839_state)) % 0.85/1.09 (define @t142 () (@var "Za" tptp.produc410756839_state)) % 0.85/1.09 (define @t143 () (_ (_ tptp.produc2065881943_state @t142) @t141)) % 0.85/1.09 (define @t144 () (@var "Xb" tptp.produc410756839_state)) % 0.85/1.09 (define @t145 () (@var "Xa" tptp.produc410756839_state)) % 0.85/1.09 (define @t146 () (_ (_ tptp.produc2065881943_state @t145) @t144)) % 0.85/1.09 (define @t147 () (_ tptp.produc2049704791_state @t146)) % 0.85/1.09 (define @t148 () (@var "Zb" tptp.produc2041926651_state)) % 0.85/1.09 (define @t149 () (@var "Za" tptp.produc2041926651_state)) % 0.85/1.09 (define @t150 () (_ (_ tptp.produc1909270103_state @t149) @t148)) % 0.85/1.09 (define @t151 () (@var "Xb" tptp.produc2041926651_state)) % 0.85/1.09 (define @t152 () (@var "Xa" tptp.produc2041926651_state)) % 0.85/1.09 (define @t153 () (_ (_ tptp.produc1909270103_state @t152) @t151)) % 0.85/1.09 (define @t154 () (_ tptp.produc2065881943_state @t153)) % 0.85/1.09 (define @t155 () (@var "Zb" tptp.state)) % 0.85/1.09 (define @t156 () (@var "Za" tptp.list_com)) % 0.85/1.09 (define @t157 () (_ (_ tptp.produc1204172211_state @t156) @t155)) % 0.85/1.09 (define @t158 () (@var "Xb" tptp.state)) % 0.85/1.09 (define @t159 () (@var "Xa" tptp.list_com)) % 0.85/1.09 (define @t160 () (_ (_ tptp.produc1204172211_state @t159) @t158)) % 0.85/1.09 (define @t161 () (_ tptp.produc1909270103_state @t160)) % 0.85/1.09 (define @t162 () (@var "Y" tptp.produc2041926651_state)) % 0.85/1.09 (define @t163 () (@var "Z" tptp.produc2041926651_state)) % 0.85/1.09 (define @t164 () (_ tptp.produc1909270103_state @t163)) % 0.85/1.09 (define @t165 () (_ tptp.member1069318160_state (_ @t164 @t162))) % 0.85/1.09 (define @t166 () (@var "X" tptp.produc2041926651_state)) % 0.85/1.09 (define @t167 () (_ tptp.produc1909270103_state @t166)) % 0.85/1.09 (define @t168 () (_ tptp.member1069318160_state (_ @t167 @t163))) % 0.85/1.09 (define @t169 () (@list @t163)) % 0.85/1.09 (define @t170 () (_ @t167 @t162)) % 0.85/1.09 (define @t171 () (_ tptp.member1069318160_state @t170)) % 0.85/1.09 (define @t172 () (_ @t171 @t53)) % 0.85/1.09 (define @t173 () (@list @t166 @t162 @t49)) % 0.85/1.09 (define @t174 () (@var "Y" tptp.produc410756839_state)) % 0.85/1.09 (define @t175 () (@var "Z" tptp.produc410756839_state)) % 0.85/1.09 (define @t176 () (_ tptp.produc2065881943_state @t175)) % 0.85/1.09 (define @t177 () (_ tptp.member512523024_state (_ @t176 @t174))) % 0.85/1.09 (define @t178 () (@var "X" tptp.produc410756839_state)) % 0.85/1.09 (define @t179 () (_ tptp.produc2065881943_state @t178)) % 0.85/1.09 (define @t180 () (_ tptp.member512523024_state (_ @t179 @t175))) % 0.85/1.09 (define @t181 () (@list @t175)) % 0.85/1.09 (define @t182 () (_ tptp.member512523024_state (_ @t179 @t174))) % 0.85/1.09 (define @t183 () (_ @t182 @t52)) % 0.85/1.09 (define @t184 () (@list @t178 @t174 @t46)) % 0.85/1.09 (define @t185 () (_ @t37 @t53)) % 0.85/1.09 (define @t186 () (= @t24 @t35)) % 0.85/1.09 (define @t187 () (not @t186)) % 0.85/1.09 (define @t188 () (and @t187 @t185)) % 0.85/1.09 (define @t189 () (or @t186 @t188)) % 0.85/1.09 (define @t190 () (_ @t37 @t50)) % 0.85/1.09 (define @t191 () (@list @t24 @t35 @t49)) % 0.85/1.09 (define @t192 () (forall @t191 (=> @t190 @t189))) % 0.85/1.09 (define @t193 () (= @t12 @t31)) % 0.85/1.09 (define @t194 () (not @t193)) % 0.85/1.09 (define @t195 () (_ @t37 @t124)) % 0.85/1.09 (define @t196 () (@list @t24 @t35 @t22)) % 0.85/1.09 (define @t197 () (forall @t196 (=> @t195 @t38))) % 0.85/1.09 (define @t198 () (_ @t33 @t99)) % 0.85/1.09 (define @t199 () (@list @t12 @t31 @t7)) % 0.85/1.09 (define @t200 () (= @t166 @t162)) % 0.85/1.09 (define @t201 () (not @t200)) % 0.85/1.09 (define @t202 () (= @t178 @t174)) % 0.85/1.09 (define @t203 () (not @t202)) % 0.85/1.09 (define @t204 () (@var "P2" tptp.produc410756839_state)) % 0.85/1.09 (define @t205 () (_ tptp.member1069318160_state @t204)) % 0.85/1.09 (define @t206 () (_ @t205 @t22)) % 0.85/1.09 (define @t207 () (@list @t204 @t22)) % 0.85/1.09 (define @t208 () (@var "P2" tptp.produc186437863_state)) % 0.85/1.09 (define @t209 () (_ tptp.member512523024_state @t208)) % 0.85/1.09 (define @t210 () (_ @t209 @t7)) % 0.85/1.09 (define @t211 () (@list @t208 @t7)) % 0.85/1.09 (define @t212 () (@list @t22)) % 0.85/1.09 (define @t213 () (@list @t7)) % 0.85/1.09 (define @t214 () (@var "C" tptp.produc2041926651_state)) % 0.85/1.09 (define @t215 () (_ tptp.member1069318160_state (_ @t29 @t214))) % 0.85/1.09 (define @t216 () (_ @t215 @t28)) % 0.85/1.09 (define @t217 () (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t35) @t214))) % 0.85/1.09 (define @t218 () (_ @t217 @t28)) % 0.85/1.09 (define @t219 () (_ @t37 @t22)) % 0.85/1.09 (define @t220 () (@list @t24 @t35 @t22 @t214)) % 0.85/1.09 (define @t221 () (@var "C" tptp.produc410756839_state)) % 0.85/1.09 (define @t222 () (_ tptp.member512523024_state (_ @t19 @t221))) % 0.85/1.09 (define @t223 () (_ @t222 @t18)) % 0.85/1.09 (define @t224 () (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t31) @t221))) % 0.85/1.09 (define @t225 () (_ @t224 @t18)) % 0.85/1.09 (define @t226 () (_ @t33 @t7)) % 0.85/1.09 (define @t227 () (@list @t12 @t31 @t7 @t221)) % 0.85/1.09 (define @t228 () (_ @t217 @t22)) % 0.85/1.09 (define @t229 () (_ @t224 @t7)) % 0.85/1.09 (define @t230 () (@var "P" (-> tptp.produc2041926651_state Bool))) % 0.85/1.09 (define @t231 () (_ @t230 @t24)) % 0.85/1.09 (define @t232 () (@var "Y2" tptp.produc2041926651_state)) % 0.85/1.09 (define @t233 () (_ @t230 @t232)) % 0.85/1.09 (define @t234 () (_ @t230 @t163)) % 0.85/1.09 (define @t235 () (=> @t234 @t233)) % 0.85/1.09 (define @t236 () (_ tptp.member1069318160_state (_ @t164 @t35))) % 0.85/1.09 (define @t237 () (_ tptp.produc1909270103_state @t232)) % 0.85/1.09 (define @t238 () (_ tptp.member1069318160_state (_ @t237 @t163))) % 0.85/1.09 (define @t239 () (_ @t238 @t22)) % 0.85/1.09 (define @t240 () (@list @t232 @t163)) % 0.85/1.09 (define @t241 () (_ @t230 @t35)) % 0.85/1.09 (define @t242 () (@list @t24 @t35 @t22 @t230)) % 0.85/1.09 (define @t243 () (@var "P" (-> tptp.produc410756839_state Bool))) % 0.85/1.09 (define @t244 () (_ @t243 @t12)) % 0.85/1.09 (define @t245 () (@var "Y2" tptp.produc410756839_state)) % 0.85/1.09 (define @t246 () (_ @t243 @t245)) % 0.85/1.09 (define @t247 () (_ @t243 @t175)) % 0.85/1.09 (define @t248 () (=> @t247 @t246)) % 0.85/1.09 (define @t249 () (_ tptp.member512523024_state (_ @t176 @t31))) % 0.85/1.09 (define @t250 () (_ tptp.produc2065881943_state @t245)) % 0.85/1.09 (define @t251 () (_ tptp.member512523024_state (_ @t250 @t175))) % 0.85/1.09 (define @t252 () (_ @t251 @t7)) % 0.85/1.09 (define @t253 () (@list @t245 @t175)) % 0.85/1.09 (define @t254 () (_ @t243 @t31)) % 0.85/1.09 (define @t255 () (@list @t12 @t31 @t7 @t243)) % 0.85/1.09 (define @t256 () (@var "Z2" tptp.produc2041926651_state)) % 0.85/1.09 (define @t257 () (_ tptp.member1069318160_state (_ @t237 @t256))) % 0.85/1.09 (define @t258 () (_ (_ tptp.member1069318160_state (_ @t167 @t232)) @t22)) % 0.85/1.09 (define @t259 () (@list @t232)) % 0.85/1.09 (define @t260 () (_ @t167 @t256)) % 0.85/1.09 (define @t261 () (_ tptp.member1069318160_state @t260)) % 0.85/1.09 (define @t262 () (_ @t261 @t28)) % 0.85/1.09 (define @t263 () (@list @t166 @t256 @t22)) % 0.85/1.09 (define @t264 () (@var "Z2" tptp.produc410756839_state)) % 0.85/1.09 (define @t265 () (_ tptp.member512523024_state (_ @t250 @t264))) % 0.85/1.09 (define @t266 () (_ (_ tptp.member512523024_state (_ @t179 @t245)) @t7)) % 0.85/1.09 (define @t267 () (@list @t245)) % 0.85/1.09 (define @t268 () (_ tptp.member512523024_state (_ @t179 @t264))) % 0.85/1.09 (define @t269 () (_ @t268 @t18)) % 0.85/1.09 (define @t270 () (@list @t178 @t264 @t7)) % 0.85/1.09 (define @t271 () (@var "X2" tptp.produc2041926651_state)) % 0.85/1.09 (define @t272 () (@var "X1" tptp.produc2041926651_state)) % 0.85/1.09 (define @t273 () (_ (_ @t84 @t272) @t271)) % 0.85/1.09 (define @t274 () (@var "C3" tptp.produc2041926651_state)) % 0.85/1.09 (define @t275 () (_ tptp.produc1909270103_state @t89)) % 0.85/1.09 (define @t276 () (_ @t275 @t274)) % 0.85/1.09 (define @t277 () (=> @t92 (=> (_ (_ tptp.member1069318160_state @t276) @t22) (_ @t91 @t274)))) % 0.85/1.09 (define @t278 () (_ tptp.member1069318160_state @t95)) % 0.85/1.09 (define @t279 () (@list @t90 @t89 @t274)) % 0.85/1.09 (define @t280 () (@list @t90)) % 0.85/1.09 (define @t281 () (_ (_ tptp.produc1909270103_state @t272) @t271)) % 0.85/1.09 (define @t282 () (_ tptp.member1069318160_state @t281)) % 0.85/1.09 (define @t283 () (@list @t272 @t271 @t22 @t84)) % 0.85/1.09 (define @t284 () (@var "X2" tptp.produc410756839_state)) % 0.85/1.09 (define @t285 () (@var "X1" tptp.produc410756839_state)) % 0.85/1.09 (define @t286 () (_ (_ @t56 @t285) @t284)) % 0.85/1.09 (define @t287 () (@var "C3" tptp.produc410756839_state)) % 0.85/1.09 (define @t288 () (_ tptp.produc2065881943_state @t61)) % 0.85/1.09 (define @t289 () (=> @t64 (=> (_ (_ tptp.member512523024_state (_ @t288 @t287)) @t7) (_ @t63 @t287)))) % 0.85/1.09 (define @t290 () (_ tptp.member512523024_state @t68)) % 0.85/1.09 (define @t291 () (@list @t62 @t61 @t287)) % 0.85/1.09 (define @t292 () (@list @t62)) % 0.85/1.09 (define @t293 () (_ (_ tptp.produc2065881943_state @t285) @t284)) % 0.85/1.09 (define @t294 () (_ tptp.member512523024_state @t293)) % 0.85/1.09 (define @t295 () (@list @t285 @t284 @t7 @t56)) % 0.85/1.09 (define @t296 () (=> @t239 (=> @t233 @t234))) % 0.85/1.09 (define @t297 () (_ tptp.member1069318160_state (_ @t29 @t232))) % 0.85/1.09 (define @t298 () (_ @t297 @t28)) % 0.85/1.09 (define @t299 () (=> @t252 (=> @t246 @t247))) % 0.85/1.09 (define @t300 () (_ tptp.member512523024_state (_ @t19 @t245))) % 0.85/1.09 (define @t301 () (_ @t300 @t18)) % 0.85/1.09 (define @t302 () (_ tptp.produc1909270103_state @t162)) % 0.85/1.09 (define @t303 () (_ @t302 @t256)) % 0.85/1.09 (define @t304 () (_ tptp.member1069318160_state @t303)) % 0.85/1.09 (define @t305 () (_ @t171 @t28)) % 0.85/1.09 (define @t306 () (@list @t166 @t162 @t22 @t256)) % 0.85/1.09 (define @t307 () (_ tptp.produc2065881943_state @t174)) % 0.85/1.09 (define @t308 () (_ tptp.member512523024_state (_ @t307 @t264))) % 0.85/1.09 (define @t309 () (_ @t182 @t18)) % 0.85/1.09 (define @t310 () (@list @t178 @t174 @t7 @t264)) % 0.85/1.09 (define @t311 () (@var "C4" tptp.produc2041926651_state)) % 0.85/1.09 (define @t312 () (@var "B3" tptp.produc2041926651_state)) % 0.85/1.09 (define @t313 () (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t312) @t311)) @t22)) % 0.85/1.09 (define @t314 () (@var "A3" tptp.produc2041926651_state)) % 0.85/1.09 (define @t315 () (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t314) @t312))) % 0.85/1.09 (define @t316 () (@var "A22" tptp.produc2041926651_state)) % 0.85/1.09 (define @t317 () (= @t316 @t311)) % 0.85/1.09 (define @t318 () (@var "A1" tptp.produc2041926651_state)) % 0.85/1.09 (define @t319 () (= @t318 @t314)) % 0.85/1.09 (define @t320 () (@list @t314 @t312 @t311)) % 0.85/1.09 (define @t321 () (_ tptp.produc1909270103_state @t318)) % 0.85/1.09 (define @t322 () (_ tptp.member1069318160_state (_ @t321 @t316))) % 0.85/1.09 (define @t323 () (_ @t322 @t28)) % 0.85/1.09 (define @t324 () (@list @t318 @t316 @t22)) % 0.85/1.09 (define @t325 () (@var "C4" tptp.produc410756839_state)) % 0.85/1.09 (define @t326 () (@var "B3" tptp.produc410756839_state)) % 0.85/1.09 (define @t327 () (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t326) @t325)) @t7)) % 0.85/1.09 (define @t328 () (@var "A3" tptp.produc410756839_state)) % 0.85/1.09 (define @t329 () (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t328) @t326))) % 0.85/1.09 (define @t330 () (@var "A22" tptp.produc410756839_state)) % 0.85/1.09 (define @t331 () (= @t330 @t325)) % 0.85/1.09 (define @t332 () (@var "A1" tptp.produc410756839_state)) % 0.85/1.09 (define @t333 () (= @t332 @t328)) % 0.85/1.09 (define @t334 () (@list @t328 @t326 @t325)) % 0.85/1.09 (define @t335 () (_ tptp.produc2065881943_state @t332)) % 0.85/1.09 (define @t336 () (_ tptp.member512523024_state (_ @t335 @t330))) % 0.85/1.09 (define @t337 () (_ @t336 @t18)) % 0.85/1.09 (define @t338 () (@list @t332 @t330 @t7)) % 0.85/1.09 (define @t339 () (not (_ (_ tptp.member1069318160_state (_ @t275 @t316)) @t22))) % 0.85/1.09 (define @t340 () (_ tptp.member1069318160_state (_ @t321 @t89))) % 0.85/1.09 (define @t341 () (@list @t89)) % 0.85/1.09 (define @t342 () (not (_ (_ tptp.member512523024_state (_ @t288 @t330)) @t7))) % 0.85/1.09 (define @t343 () (_ tptp.member512523024_state (_ @t335 @t61))) % 0.85/1.09 (define @t344 () (@list @t61)) % 0.85/1.09 (define @t345 () (_ (_ tptp.member1069318160_state (_ @t237 @t35)) @t22)) % 0.85/1.09 (define @t346 () (_ (_ tptp.member512523024_state (_ @t250 @t31)) @t7)) % 0.85/1.09 (define @t347 () (_ @t215 @t124)) % 0.85/1.09 (define @t348 () (=> @t228 @t347)) % 0.85/1.09 (define @t349 () (_ @t222 @t99)) % 0.85/1.09 (define @t350 () (=> @t229 @t349)) % 0.85/1.09 (define @t351 () (@var "X3" tptp.produc2041926651_state)) % 0.85/1.09 (define @t352 () (_ @t84 @t351)) % 0.85/1.09 (define @t353 () (_ @t352 @t232)) % 0.85/1.09 (define @t354 () (_ tptp.produc1909270103_state @t351)) % 0.85/1.09 (define @t355 () (_ @t354 @t232)) % 0.85/1.09 (define @t356 () (_ tptp.member1069318160_state @t355)) % 0.85/1.09 (define @t357 () (_ @t356 @t22)) % 0.85/1.09 (define @t358 () (@list @t351 @t232)) % 0.85/1.09 (define @t359 () (_ @t171 @t124)) % 0.85/1.09 (define @t360 () (@var "X3" tptp.produc410756839_state)) % 0.85/1.09 (define @t361 () (_ @t56 @t360)) % 0.85/1.09 (define @t362 () (_ @t361 @t245)) % 0.85/1.09 (define @t363 () (_ tptp.produc2065881943_state @t360)) % 0.85/1.09 (define @t364 () (_ @t363 @t245)) % 0.85/1.09 (define @t365 () (_ tptp.member512523024_state @t364)) % 0.85/1.09 (define @t366 () (_ @t365 @t7)) % 0.85/1.09 (define @t367 () (@list @t360 @t245)) % 0.85/1.09 (define @t368 () (_ @t182 @t99)) % 0.85/1.09 (define @t369 () (_ @t171 @t22)) % 0.85/1.09 (define @t370 () (_ tptp.member1069318160_state (_ @t354 @t351))) % 0.85/1.09 (define @t371 () (@list @t351)) % 0.85/1.09 (define @t372 () (_ @t182 @t7)) % 0.85/1.09 (define @t373 () (_ tptp.member512523024_state (_ @t363 @t360))) % 0.85/1.09 (define @t374 () (@list @t360)) % 0.85/1.09 (define @t375 () (_ @t261 @t124)) % 0.85/1.09 (define @t376 () (_ @t268 @t99)) % 0.85/1.09 (define @t377 () (_ @t278 @t22)) % 0.85/1.09 (define @t378 () (_ @t290 @t7)) % 0.85/1.09 (define @t379 () (_ @t304 @t124)) % 0.85/1.09 (define @t380 () (=> @t379 @t375)) % 0.85/1.09 (define @t381 () (forall @t306 (=> @t359 @t380))) % 0.85/1.09 (define @t382 () (=> (_ @t308 @t99) @t376)) % 0.85/1.09 (define @t383 () (_ @t322 @t124)) % 0.85/1.09 (define @t384 () (_ @t336 @t99)) % 0.85/1.09 (define @t385 () (_ (_ tptp.pHoare2126160787le_inf @t44) @t5)) % 0.85/1.09 (define @t386 () (@var "A" tptp.state)) % 0.85/1.09 (define @t387 () (@var "P" (-> tptp.state Bool))) % 0.85/1.09 (define @t388 () (@var "A" tptp.produc186437863_state)) % 0.85/1.09 (define @t389 () (@var "P" (-> tptp.produc186437863_state Bool))) % 0.85/1.09 (define @t390 () (@var "A4" tptp.set_Pr1165141447_state)) % 0.85/1.09 (define @t391 () (@var "X4" tptp.produc410756839_state)) % 0.85/1.09 (define @t392 () (@var "A4" tptp.set_state)) % 0.85/1.09 (define @t393 () (@var "X4" tptp.state)) % 0.85/1.09 (define @t394 () (@var "A4" tptp.set_Pr2096893127_state)) % 0.85/1.09 (define @t395 () (@var "X4" tptp.produc186437863_state)) % 0.85/1.09 (define @t396 () (=> @t218 @t347)) % 0.85/1.09 (define @t397 () (=> @t225 @t349)) % 0.85/1.09 (define @t398 () (@var "T" tptp.state)) % 0.85/1.09 (define @t399 () (@var "Cs3" tptp.list_com)) % 0.85/1.09 (define @t400 () (_ tptp.pHoare259243732_execs @t5)) % 0.85/1.09 (define @t401 () (_ @t6 @t398)) % 0.85/1.09 (define @t402 () (_ tptp.produc1204172211_state @t399)) % 0.85/1.09 (define @t403 () (_ @t402 @t5)) % 0.85/1.09 (define @t404 () (_ tptp.produc1909270103_state @t403)) % 0.85/1.09 (define @t405 () (_ tptp.pHoare806997636termis @t399)) % 0.85/1.09 (define @t406 () (=> (_ @t405 @t5) (_ (_ tptp.pHoare806997636termis @t2) @t1))) % 0.85/1.09 (define @t407 () (_ tptp.member1069318160_state (_ @t404 @t4))) % 0.85/1.09 (define @t408 () (_ @t407 @t42)) % 0.85/1.09 (define @t409 () (@list @t399 @t5 @t2 @t1)) % 0.85/1.09 (define @t410 () (@var "Nat2" tptp.nat)) % 0.85/1.09 (define @t411 () (@var "Nat" tptp.nat)) % 0.85/1.09 (define @t412 () (_ tptp.suc @t410)) % 0.85/1.09 (define @t413 () (@var "Y22" tptp.nat)) % 0.85/1.09 (define @t414 () (@var "X2" tptp.nat)) % 0.85/1.09 (define @t415 () (_ tptp.suc @t414)) % 0.85/1.09 (define @t416 () (@var "Y222" tptp.list_com)) % 0.85/1.09 (define @t417 () (@var "X22" tptp.list_com)) % 0.85/1.10 (define @t418 () (@var "Y21" tptp.com)) % 0.85/1.10 (define @t419 () (@var "X21" tptp.com)) % 0.85/1.10 (define @t420 () (= @t419 @t418)) % 0.85/1.10 (define @t421 () (_ (_ tptp.cons_com @t419) @t417)) % 0.85/1.10 (define @t422 () (_ tptp.exec @t5)) % 0.85/1.10 (define @t423 () (_ @t422 @t40)) % 0.85/1.10 (define @t424 () (_ @t423 @t398)) % 0.85/1.10 (define @t425 () (@var "B4" tptp.state)) % 0.85/1.10 (define @t426 () (@var "B" tptp.state)) % 0.85/1.10 (define @t427 () (= @t426 @t425)) % 0.85/1.10 (define @t428 () (@var "A5" tptp.list_com)) % 0.85/1.10 (define @t429 () (@var "A" tptp.list_com)) % 0.85/1.10 (define @t430 () (= @t429 @t428)) % 0.85/1.10 (define @t431 () (= (_ (_ tptp.produc1204172211_state @t429) @t426) (_ (_ tptp.produc1204172211_state @t428) @t425))) % 0.85/1.10 (define @t432 () (@list @t429 @t426 @t428 @t425)) % 0.85/1.10 (define @t433 () (@var "B4" tptp.produc2041926651_state)) % 0.85/1.10 (define @t434 () (= @t35 @t433)) % 0.85/1.10 (define @t435 () (@var "A5" tptp.produc2041926651_state)) % 0.85/1.10 (define @t436 () (= @t24 @t435)) % 0.85/1.10 (define @t437 () (= @t36 (_ (_ tptp.produc1909270103_state @t435) @t433))) % 0.85/1.10 (define @t438 () (@list @t24 @t35 @t435 @t433)) % 0.85/1.10 (define @t439 () (@var "B4" tptp.produc410756839_state)) % 0.85/1.10 (define @t440 () (= @t31 @t439)) % 0.85/1.10 (define @t441 () (@var "A5" tptp.produc410756839_state)) % 0.85/1.10 (define @t442 () (= @t12 @t441)) % 0.85/1.10 (define @t443 () (= @t32 (_ (_ tptp.produc2065881943_state @t441) @t439))) % 0.85/1.10 (define @t444 () (@list @t12 @t31 @t441 @t439)) % 0.85/1.10 (define @t445 () (@var "Y22" tptp.state)) % 0.85/1.10 (define @t446 () (@var "X2" tptp.state)) % 0.85/1.10 (define @t447 () (@var "Y1" tptp.list_com)) % 0.85/1.10 (define @t448 () (@var "X1" tptp.list_com)) % 0.85/1.10 (define @t449 () (@var "Y22" tptp.produc2041926651_state)) % 0.85/1.10 (define @t450 () (@var "Y1" tptp.produc2041926651_state)) % 0.85/1.10 (define @t451 () (@var "Y22" tptp.produc410756839_state)) % 0.85/1.10 (define @t452 () (@var "Y1" tptp.produc410756839_state)) % 0.85/1.10 (define @t453 () (@var "U" tptp.state)) % 0.85/1.10 (define @t454 () (_ @t43 @t399)) % 0.85/1.10 (define @t455 () (@var "A32" tptp.state)) % 0.85/1.10 (define @t456 () (@var "Cs4" tptp.list_com)) % 0.85/1.10 (define @t457 () (@var "T2" tptp.state)) % 0.85/1.10 (define @t458 () (_ (_ tptp.pHoare259243732_execs @t457) @t456)) % 0.85/1.10 (define @t459 () (@var "C3" tptp.com)) % 0.85/1.10 (define @t460 () (@var "A1" tptp.state)) % 0.85/1.10 (define @t461 () (_ (_ tptp.cons_com @t459) @t456)) % 0.85/1.10 (define @t462 () (@var "A22" tptp.list_com)) % 0.85/1.10 (define @t463 () (= @t462 tptp.nil_com)) % 0.85/1.10 (define @t464 () (@var "U2" tptp.state)) % 0.85/1.10 (define @t465 () (@var "Cs2" tptp.list_com)) % 0.85/1.10 (define @t466 () (@var "T3" tptp.state)) % 0.85/1.10 (define @t467 () (@var "C4" tptp.com)) % 0.85/1.10 (define @t468 () (@var "S3" tptp.state)) % 0.85/1.10 (define @t469 () (@var "A33" tptp.state)) % 0.85/1.10 (define @t470 () (@var "A23" tptp.list_com)) % 0.85/1.10 (define @t471 () (@var "A12" tptp.state)) % 0.85/1.10 (define @t472 () (= @t471 @t468)) % 0.85/1.10 (define @t473 () (@var "X32" tptp.state)) % 0.85/1.10 (define @t474 () (@var "X2" tptp.list_com)) % 0.85/1.10 (define @t475 () (@var "X1" tptp.state)) % 0.85/1.10 (define @t476 () (@var "P" (-> tptp.state tptp.list_com tptp.state Bool))) % 0.85/1.10 (define @t477 () (@var "U3" tptp.state)) % 0.85/1.10 (define @t478 () (@var "S4" tptp.state)) % 0.85/1.10 (define @t479 () (_ @t476 @t478)) % 0.85/1.10 (define @t480 () (@list @t40 @t399 @t5)) % 0.85/1.10 (define @t481 () (@list @t5)) % 0.85/1.10 (define @t482 () (@var "X" tptp.nat)) % 0.85/1.10 (define @t483 () (@var "Y2" tptp.state)) % 0.85/1.10 (define @t484 () (@var "X3" tptp.list_com)) % 0.85/1.10 (define @t485 () (_ tptp.produc1204172211_state @t484)) % 0.85/1.10 (define @t486 () (_ @t485 @t483)) % 0.85/1.10 (define @t487 () (@var "P2" tptp.produc2041926651_state)) % 0.85/1.10 (define @t488 () (forall @t130 (_ @t230 @t120))) % 0.85/1.10 (define @t489 () (forall @t105 (_ @t243 @t95))) % 0.85/1.10 (define @t490 () (forall @t78 (_ @t389 @t68))) % 0.85/1.10 (define @t491 () (@list @t174)) % 0.85/1.10 (define @t492 () (@var "Y" tptp.produc186437863_state)) % 0.85/1.10 (define @t493 () (@list @t492)) % 0.85/1.10 (define @t494 () (@var "Prod" tptp.produc2041926651_state)) % 0.85/1.10 (define @t495 () (@var "Prod" tptp.produc410756839_state)) % 0.85/1.10 (define @t496 () (@var "Prod" tptp.produc186437863_state)) % 0.85/1.10 (define @t497 () (@var "Xs" tptp.list_com)) % 0.85/1.10 (define @t498 () (@var "X" tptp.com)) % 0.85/1.10 (define @t499 () (_ tptp.cons_com @t498)) % 0.85/1.10 (define @t500 () (_ @t499 @t497)) % 0.85/1.10 (define @t501 () (@var "Y" tptp.nat)) % 0.85/1.10 (define @t502 () (@var "N" tptp.nat)) % 0.85/1.10 (define @t503 () (_ tptp.suc @t502)) % 0.85/1.10 (define @t504 () (@list @t502)) % 0.85/1.10 (define @t505 () (_ @t423 @t457)) % 0.85/1.10 (define @t506 () (@list @t457)) % 0.85/1.10 (define @t507 () (@list @t410)) % 0.85/1.10 (define @t508 () (@var "P" (-> tptp.nat Bool))) % 0.85/1.10 (define @t509 () (@var "N2" tptp.nat)) % 0.85/1.10 (define @t510 () (_ @t508 (_ tptp.suc @t509))) % 0.85/1.10 (define @t511 () (_ @t508 @t509)) % 0.85/1.10 (define @t512 () (@list @t509)) % 0.85/1.10 (define @t513 () (_ @t508 tptp.zero_zero_nat)) % 0.85/1.10 (define @t514 () (@var "M" tptp.nat)) % 0.85/1.10 (define @t515 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 0.85/1.10 (define @t516 () (@var "Y2" tptp.nat)) % 0.85/1.10 (define @t517 () (_ tptp.suc @t516)) % 0.85/1.10 (define @t518 () (@var "X3" tptp.nat)) % 0.85/1.10 (define @t519 () (_ @t515 @t518)) % 0.85/1.10 (define @t520 () (@var "K" tptp.nat)) % 0.85/1.10 (define @t521 () (_ tptp.suc @t514)) % 0.85/1.10 (define @t522 () (@list @t514)) % 0.85/1.10 (define @t523 () (@var "Nat3" tptp.nat)) % 0.85/1.10 (define @t524 () (_ tptp.suc @t523)) % 0.85/1.10 (define @t525 () (@list @t523)) % 0.85/1.10 (define @t526 () (@var "M2" tptp.nat)) % 0.85/1.10 (define @t527 () (= @t502 tptp.zero_zero_nat)) % 0.85/1.10 (define @t528 () (not @t527)) % 0.85/1.10 (define @t529 () (@var "List" tptp.list_com)) % 0.85/1.10 (define @t530 () (@var "X222" tptp.list_com)) % 0.85/1.10 (define @t531 () (@var "X212" tptp.com)) % 0.85/1.10 (define @t532 () (@var "Y" tptp.list_com)) % 0.85/1.10 (define @t533 () (@var "P" (-> tptp.list_com Bool))) % 0.85/1.10 (define @t534 () (@var "X23" tptp.list_com)) % 0.85/1.10 (define @t535 () (@var "X12" tptp.com)) % 0.85/1.10 (define @t536 () (_ @t533 tptp.nil_com)) % 0.85/1.10 (define @t537 () (@var "Ys" tptp.list_com)) % 0.85/1.10 (define @t538 () (@var "Y3" tptp.com)) % 0.85/1.10 (define @t539 () (_ (_ tptp.cons_com @t538) @t537)) % 0.85/1.10 (define @t540 () (= @t497 tptp.nil_com)) % 0.85/1.10 (define @t541 () (not @t540)) % 0.85/1.10 (define @t542 () (@list @t497)) % 0.85/1.10 (define @t543 () (@var "Ys2" tptp.list_com)) % 0.85/1.10 (define @t544 () (@var "P" (-> tptp.list_com tptp.list_com Bool))) % 0.85/1.10 (define @t545 () (@var "Ys3" tptp.list_com)) % 0.85/1.10 (define @t546 () (@var "Y2" tptp.com)) % 0.85/1.10 (define @t547 () (_ tptp.cons_com @t546)) % 0.85/1.10 (define @t548 () (_ @t547 @t545)) % 0.85/1.10 (define @t549 () (@var "Xs2" tptp.list_com)) % 0.85/1.10 (define @t550 () (@var "X3" tptp.com)) % 0.85/1.10 (define @t551 () (_ tptp.cons_com @t550)) % 0.85/1.10 (define @t552 () (_ @t551 @t549)) % 0.85/1.10 (define @t553 () (_ @t544 @t552)) % 0.85/1.10 (define @t554 () (_ @t553 @t548)) % 0.85/1.10 (define @t555 () (_ @t544 @t549)) % 0.85/1.10 (define @t556 () (=> (_ @t555 @t545) @t554)) % 0.85/1.10 (define @t557 () (@list @t550 @t549 @t546 @t545)) % 0.85/1.10 (define @t558 () (_ @t544 tptp.nil_com)) % 0.85/1.10 (define @t559 () (@list @t546 @t545)) % 0.85/1.10 (define @t560 () (@list @t550 @t549)) % 0.85/1.10 (define @t561 () (_ @t558 tptp.nil_com)) % 0.85/1.10 (define @t562 () (@var "A1" tptp.list_com)) % 0.85/1.10 (define @t563 () (@var "A0" tptp.list_com)) % 0.85/1.10 (define @t564 () (_ (_ @t544 @t563) @t562)) % 0.85/1.10 (define @t565 () (_ @t553 @t545)) % 0.85/1.10 (define @t566 () (@list @t550 @t549 @t545)) % 0.85/1.10 (define @t567 () (@var "X_1" tptp.list_com)) % 0.85/1.10 (define @t568 () (forall (@list @t567) (_ @t558 @t567))) % 0.85/1.10 (define @t569 () (@list @t544 @t563 @t562)) % 0.85/1.10 (define @t570 () (_ @t533 @t497)) % 0.85/1.10 (define @t571 () (@var "Zs" tptp.list_com)) % 0.85/1.10 (define @t572 () (_ @t547 @t571)) % 0.85/1.10 (define @t573 () (_ @t551 tptp.nil_com)) % 0.85/1.10 (define @t574 () (@list @t550)) % 0.85/1.10 (define @t575 () (forall @t574 (_ @t533 @t573))) % 0.85/1.10 (define @t576 () (@list @t533 @t497)) % 0.85/1.10 (define @t577 () (@list @t549)) % 0.85/1.10 (define @t578 () (@var "Xss" tptp.list_list_com)) % 0.85/1.10 (define @t579 () (@var "X" tptp.list_list_com)) % 0.85/1.10 (define @t580 () (_ tptp.cons_list_com tptp.nil_com)) % 0.85/1.10 (define @t581 () (_ @t547 @t549)) % 0.85/1.10 (define @t582 () (_ @t551 @t581)) % 0.85/1.10 (define @t583 () (@var "X" tptp.list_com)) % 0.85/1.10 (define @t584 () (@list @t550 @t546 @t549)) % 0.85/1.10 (define @t585 () (@var "A0" (-> tptp.com tptp.com Bool))) % 0.85/1.10 (define @t586 () (@var "P" (-> (-> tptp.com tptp.com Bool) tptp.list_com Bool))) % 0.85/1.10 (define @t587 () (_ (_ @t586 @t585) @t562)) % 0.85/1.10 (define @t588 () (_ @t551 @t545)) % 0.85/1.10 (define @t589 () (@var "P3" (-> tptp.com tptp.com Bool))) % 0.85/1.10 (define @t590 () (_ @t586 @t589)) % 0.85/1.10 (define @t591 () (@list @t589 @t550 @t545)) % 0.85/1.10 (define @t592 () (@list @t589)) % 0.85/1.10 (define @t593 () (forall @t592 (_ @t590 tptp.nil_com))) % 0.85/1.10 (define @t594 () (@list @t586 @t585 @t562)) % 0.85/1.10 (define @t595 () (= @t550 @t546)) % 0.85/1.10 (define @t596 () (_ @t533 @t552)) % 0.85/1.10 (define @t597 () (@list @t589 @t550 @t546 @t549)) % 0.85/1.10 (define @t598 () (@list @t589 @t550)) % 0.85/1.10 (define @t599 () (_ @t533 @t549)) % 0.85/1.10 (define @t600 () (not (= @t549 tptp.nil_com))) % 0.85/1.10 (define @t601 () (@list @t497 @t533)) % 0.85/1.10 (define @t602 () (@var "A0" (-> tptp.com tptp.com))) % 0.85/1.10 (define @t603 () (@var "P" (-> (-> tptp.com tptp.com) tptp.list_com tptp.list_com Bool))) % 0.85/1.10 (define @t604 () (@var "Bs" tptp.list_com)) % 0.85/1.10 (define @t605 () (@var "As" tptp.list_com)) % 0.85/1.10 (define @t606 () (@var "A2" tptp.com)) % 0.85/1.10 (define @t607 () (@var "F2" (-> tptp.com tptp.com))) % 0.85/1.10 (define @t608 () (_ @t603 @t607)) % 0.85/1.10 (define @t609 () (_ tptp.produc1307105171st_com @t552)) % 0.85/1.10 (define @t610 () (@var "X" tptp.produc258871771st_com)) % 0.85/1.10 (define @t611 () (_ tptp.produc1307105171st_com tptp.nil_com)) % 0.85/1.10 (define @t612 () (@list @t545)) % 0.85/1.10 (define @t613 () (forall @t612 (not (= @t610 (_ @t611 @t545))))) % 0.85/1.10 (define @t614 () (@list @t610)) % 0.85/1.10 (define @t615 () (_ tptp.produc1307105171st_com @t549)) % 0.85/1.10 (define @t616 () (_ tptp.produc1914379986st_com @t589)) % 0.85/1.10 (define @t617 () (@var "X" tptp.produc2058209240st_com)) % 0.85/1.10 (define @t618 () (forall @t592 (not (= @t617 (_ @t616 tptp.nil_com))))) % 0.85/1.10 (define @t619 () (@list @t617)) % 0.85/1.10 (define @t620 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t454) @t5))) % 0.85/1.10 (define @t621 () (@var "C3" tptp.state)) % 0.85/1.10 (define @t622 () (@var "B2" tptp.list_com)) % 0.85/1.10 (define @t623 () (_ @t94 (_ (_ tptp.produc1204172211_state @t622) @t621))) % 0.85/1.10 (define @t624 () (@list @t90 @t622 @t621)) % 0.85/1.10 (define @t625 () (_ @t67 @t276)) % 0.85/1.10 (define @t626 () (@list @t62 @t89 @t274)) % 0.85/1.10 (define @t627 () (@var "D" tptp.state)) % 0.85/1.10 (define @t628 () (@var "C3" tptp.list_com)) % 0.85/1.10 (define @t629 () (_ @t67 (_ @t275 (_ (_ tptp.produc1204172211_state @t628) @t627)))) % 0.85/1.10 (define @t630 () (@list @t62 @t89 @t628 @t627)) % 0.85/1.10 (define @t631 () (@var "X" tptp.produc186437863_state)) % 0.85/1.10 (define @t632 () (_ @t389 @t631)) % 0.85/1.10 (define @t633 () (@list @t389 @t631)) % 0.85/1.10 (define @t634 () (_ @t407 tptp.pHoare259243666_exec1)) % 0.85/1.10 (define @t635 () (= @t1 @t5)) % 0.85/1.10 (define @t636 () (@var "C22" tptp.com)) % 0.85/1.10 (define @t637 () (_ (_ tptp.cons_com @t636) @t399)) % 0.85/1.10 (define @t638 () (@var "C1" tptp.com)) % 0.85/1.10 (define @t639 () (_ tptp.cons_com @t638)) % 0.85/1.10 (define @t640 () (_ @t639 @t637)) % 0.85/1.10 (define @t641 () (_ (_ tptp.semi @t638) @t636)) % 0.85/1.10 (define @t642 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state (_ (_ tptp.cons_com @t641) @t399)) @t5))) % 0.85/1.10 (define @t643 () (_ (_ tptp.n_lists_com @t502) tptp.nil_com)) % 0.85/1.10 (define @t644 () (_ @t580 tptp.nil_list_com)) % 0.85/1.10 (define @t645 () (@var "F" (-> tptp.state tptp.set_state))) % 0.85/1.10 (define @t646 () (_ @t645 @t5)) % 0.85/1.10 (define @t647 () (= @t2 @t399)) % 0.85/1.10 (define @t648 () (_ tptp.do @t645)) % 0.85/1.10 (define @t649 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state (_ (_ tptp.cons_com @t648) @t399)) @t5))) % 0.85/1.10 (define @t650 () (_ (_ tptp.member_state @t398) @t646)) % 0.85/1.10 (define @t651 () (@var "S0" tptp.state)) % 0.85/1.10 (define @t652 () (@var "S1" tptp.state)) % 0.85/1.10 (define @t653 () (_ tptp.termi @t636)) % 0.85/1.10 (define @t654 () (_ tptp.exec @t651)) % 0.85/1.10 (define @t655 () (_ @t654 @t638)) % 0.85/1.10 (define @t656 () (_ tptp.termi @t638)) % 0.85/1.10 (define @t657 () (@var "Y222" tptp.com)) % 0.85/1.10 (define @t658 () (@var "X22" tptp.com)) % 0.85/1.10 (define @t659 () (_ (_ tptp.semi @t419) @t658)) % 0.85/1.10 (define @t660 () (@var "Y1" (-> tptp.state tptp.set_state))) % 0.85/1.10 (define @t661 () (@var "X1" (-> tptp.state tptp.set_state))) % 0.85/1.10 (define @t662 () (_ tptp.do @t661)) % 0.85/1.10 (define @t663 () (@var "S22" tptp.state)) % 0.85/1.10 (define @t664 () (@var "S12" tptp.state)) % 0.85/1.10 (define @t665 () (@var "B" (-> tptp.state Bool))) % 0.85/1.10 (define @t666 () (_ @t665 @t5)) % 0.85/1.10 (define @t667 () (=> @t635 @t666)) % 0.85/1.10 (define @t668 () (not @t666)) % 0.85/1.10 (define @t669 () (=> @t635 @t668)) % 0.85/1.10 (define @t670 () (_ @t639 @t399)) % 0.85/1.10 (define @t671 () (_ (_ (_ tptp.cond @t665) @t638) @t636)) % 0.85/1.10 (define @t672 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state (_ (_ tptp.cons_com @t671) @t399)) @t5))) % 0.85/1.10 (define @t673 () (@var "Y33" tptp.com)) % 0.85/1.10 (define @t674 () (@var "X33" tptp.com)) % 0.85/1.10 (define @t675 () (@var "Y32" tptp.com)) % 0.85/1.10 (define @t676 () (@var "X322" tptp.com)) % 0.85/1.10 (define @t677 () (@var "Y31" (-> tptp.state Bool))) % 0.85/1.10 (define @t678 () (@var "X31" (-> tptp.state Bool))) % 0.85/1.10 (define @t679 () (_ (_ (_ tptp.cond @t678) @t676) @t674)) % 0.85/1.10 (define @t680 () (_ (_ @t422 @t671) @t398)) % 0.85/1.10 (define @t681 () (_ (_ tptp.termi @t671) @t5)) % 0.85/1.10 (define @t682 () (@list @t665 @t5 @t638 @t636 @t399)) % 0.85/1.10 (define @t683 () (_ tptp.gen_length_com @t502)) % 0.85/1.10 (define @t684 () (_ @t499 tptp.nil_com)) % 0.85/1.10 (define @t685 () (_ (_ tptp.while @t665) @t40)) % 0.85/1.10 (define @t686 () (_ (_ tptp.cons_com @t685) @t399)) % 0.85/1.10 (define @t687 () (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t686) @t5))) % 0.85/1.10 (define @t688 () (@list @t665 @t5 @t40 @t399)) % 0.85/1.10 (define @t689 () (@var "Y42" tptp.com)) % 0.85/1.10 (define @t690 () (@var "X42" tptp.com)) % 0.85/1.10 (define @t691 () (@var "Y41" (-> tptp.state Bool))) % 0.85/1.10 (define @t692 () (@var "X41" (-> tptp.state Bool))) % 0.85/1.10 (define @t693 () (_ (_ tptp.while @t692) @t690)) % 0.85/1.10 (define @t694 () (_ tptp.termi @t685)) % 0.85/1.10 (define @t695 () (_ @t694 @t5)) % 0.85/1.10 (define @t696 () (_ @t422 @t685)) % 0.85/1.10 (define @t697 () (@list @t665 @t5 @t40)) % 0.85/1.10 (define @t698 () (@var "F" (-> tptp.nat tptp.state))) % 0.85/1.10 (define @t699 () (_ @t698 @t14)) % 0.85/1.10 (define @t700 () (exists @t20 (not (_ @t665 @t699)))) % 0.85/1.10 (define @t701 () (forall @t20 (_ (_ (_ tptp.exec @t699) @t40) (_ @t698 @t15)))) % 0.85/1.10 (define @t702 () (_ @t698 @t520)) % 0.85/1.10 (define @t703 () (@var "W" tptp.com)) % 0.85/1.10 (define @t704 () (@var "Fk" tptp.state)) % 0.85/1.10 (define @t705 () (_ @t43 @t686)) % 0.85/1.10 (define @t706 () (@var "A4" tptp.set_nat)) % 0.85/1.10 (define @t707 () (_ (_ tptp.nths_com @t684) @t706)) % 0.85/1.10 (define @t708 () (_ (_ tptp.member_nat tptp.zero_zero_nat) @t706)) % 0.85/1.10 (define @t709 () (@var "Cs22" tptp.list_com)) % 0.85/1.10 (define @t710 () (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state (_ (_ tptp.append_com @t399) @t709)) @t5)) (_ (_ tptp.produc1204172211_state (_ (_ tptp.append_com @t2) @t709)) @t1)))) % 0.85/1.10 (define @t711 () (@list @t399 @t5 @t2 @t1 @t709)) % 0.85/1.10 (define @t712 () (@var "R" tptp.set_Pr1822651163om_com)) % 0.85/1.10 (define @t713 () (_ tptp.listrel_com_com @t712)) % 0.85/1.10 (define @t714 () (_ (_ tptp.member32358020st_com (_ @t615 @t545)) @t713)) % 0.85/1.10 (define @t715 () (_ tptp.product_Pair_com_com @t550)) % 0.85/1.10 (define @t716 () (_ (_ tptp.member1333916004om_com (_ @t715 @t546)) @t712)) % 0.85/1.10 (define @t717 () (= @t562 tptp.nil_com)) % 0.85/1.10 (define @t718 () (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t562) @t462)) @t713)) % 0.85/1.10 (define @t719 () (@list @t562 @t462 @t712)) % 0.85/1.10 (define @t720 () (@var "R" tptp.set_Pr849496667_state)) % 0.85/1.10 (define @t721 () (_ tptp.listre1268245261_state @t720)) % 0.85/1.10 (define @t722 () (@var "Ys3" tptp.list_state)) % 0.85/1.10 (define @t723 () (@var "Xs2" tptp.list_list_com)) % 0.85/1.10 (define @t724 () (_ tptp.produc1742567891_state @t723)) % 0.85/1.10 (define @t725 () (_ (_ tptp.member1442949316_state (_ @t724 @t722)) @t721)) % 0.85/1.10 (define @t726 () (_ (_ tptp.member64234660_state @t486) @t720)) % 0.85/1.10 (define @t727 () (_ (_ tptp.cons_state @t483) @t722)) % 0.85/1.10 (define @t728 () (@var "A22" tptp.list_state)) % 0.85/1.10 (define @t729 () (_ (_ tptp.cons_list_com @t484) @t723)) % 0.85/1.10 (define @t730 () (@var "A1" tptp.list_list_com)) % 0.85/1.10 (define @t731 () (= @t728 tptp.nil_state)) % 0.85/1.10 (define @t732 () (= @t730 tptp.nil_list_com)) % 0.85/1.10 (define @t733 () (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state @t730) @t728)) @t721)) % 0.85/1.10 (define @t734 () (@list @t730 @t728 @t720)) % 0.85/1.10 (define @t735 () (_ tptp.listre194873521_state @t22)) % 0.85/1.10 (define @t736 () (@var "Ys3" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t737 () (@var "Xs2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t738 () (_ tptp.produc1298457559_state @t737)) % 0.85/1.10 (define @t739 () (_ (_ tptp.member1267359376_state (_ @t738 @t736)) @t735)) % 0.85/1.10 (define @t740 () (_ tptp.cons_P465369265_state @t232)) % 0.85/1.10 (define @t741 () (_ @t740 @t736)) % 0.85/1.10 (define @t742 () (@var "A22" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t743 () (_ tptp.cons_P465369265_state @t351)) % 0.85/1.10 (define @t744 () (_ @t743 @t737)) % 0.85/1.10 (define @t745 () (@var "A1" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t746 () (= @t742 tptp.nil_Pr1844458753_state)) % 0.85/1.10 (define @t747 () (= @t745 tptp.nil_Pr1844458753_state)) % 0.85/1.10 (define @t748 () (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t745) @t742)) @t735)) % 0.85/1.10 (define @t749 () (@list @t745 @t742 @t22)) % 0.85/1.10 (define @t750 () (_ tptp.listre1244407729_state @t7)) % 0.85/1.10 (define @t751 () (@var "Ys3" tptp.list_P890094829_state)) % 0.85/1.10 (define @t752 () (@var "Xs2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t753 () (_ tptp.produc1354769367_state @t752)) % 0.85/1.10 (define @t754 () (_ (_ tptp.member423306384_state (_ @t753 @t751)) @t750)) % 0.85/1.10 (define @t755 () (_ tptp.cons_P438230685_state @t245)) % 0.85/1.10 (define @t756 () (_ @t755 @t751)) % 0.85/1.10 (define @t757 () (@var "A22" tptp.list_P890094829_state)) % 0.85/1.10 (define @t758 () (_ tptp.cons_P438230685_state @t360)) % 0.85/1.10 (define @t759 () (_ @t758 @t752)) % 0.85/1.10 (define @t760 () (@var "A1" tptp.list_P890094829_state)) % 0.85/1.10 (define @t761 () (= @t757 tptp.nil_Pr1347322605_state)) % 0.85/1.10 (define @t762 () (= @t760 tptp.nil_Pr1347322605_state)) % 0.85/1.10 (define @t763 () (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t760) @t757)) @t750)) % 0.85/1.10 (define @t764 () (@list @t760 @t757 @t7)) % 0.85/1.10 (define @t765 () (@var "Zs2" tptp.list_com)) % 0.85/1.10 (define @t766 () (= @t543 @t765)) % 0.85/1.10 (define @t767 () (_ tptp.append_com @t497)) % 0.85/1.10 (define @t768 () (_ @t767 @t765)) % 0.85/1.10 (define @t769 () (_ @t767 @t543)) % 0.85/1.10 (define @t770 () (@list @t497 @t543 @t765)) % 0.85/1.10 (define @t771 () (_ tptp.append_com @t765)) % 0.85/1.10 (define @t772 () (_ tptp.append_com @t543)) % 0.85/1.10 (define @t773 () (_ @t772 @t765)) % 0.85/1.10 (define @t774 () (@var "C" tptp.list_com)) % 0.85/1.10 (define @t775 () (@var "B" tptp.list_com)) % 0.85/1.10 (define @t776 () (_ tptp.append_com @t429)) % 0.85/1.10 (define @t777 () (= @t543 tptp.nil_com)) % 0.85/1.10 (define @t778 () (@list @t497 @t543)) % 0.85/1.10 (define @t779 () (and @t540 @t777)) % 0.85/1.10 (define @t780 () (@list @t429)) % 0.85/1.10 (define @t781 () (@var "Y" tptp.com)) % 0.85/1.10 (define @t782 () (= @t498 @t781)) % 0.85/1.10 (define @t783 () (= @t497 @t543)) % 0.85/1.10 (define @t784 () (_ tptp.cons_com @t781)) % 0.85/1.10 (define @t785 () (_ @t772 (_ @t784 tptp.nil_com))) % 0.85/1.10 (define @t786 () (_ @t767 @t684)) % 0.85/1.10 (define @t787 () (_ tptp.listre194873521_state @t28)) % 0.85/1.10 (define @t788 () (@var "Xs" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t789 () (_ tptp.produc1298457559_state @t788)) % 0.85/1.10 (define @t790 () (_ tptp.member1267359376_state (_ @t789 @t788))) % 0.85/1.10 (define @t791 () (_ tptp.listre1244407729_state @t18)) % 0.85/1.10 (define @t792 () (@var "Xs" tptp.list_P890094829_state)) % 0.85/1.10 (define @t793 () (_ tptp.produc1354769367_state @t792)) % 0.85/1.10 (define @t794 () (_ tptp.member423306384_state (_ @t793 @t792))) % 0.85/1.10 (define @t795 () (@var "Ts" tptp.list_com)) % 0.85/1.10 (define @t796 () (@var "Us" tptp.list_com)) % 0.85/1.10 (define @t797 () (_ tptp.append_com @t796)) % 0.85/1.10 (define @t798 () (@var "Us2" tptp.list_com)) % 0.85/1.10 (define @t799 () (@var "Xs1" tptp.list_com)) % 0.85/1.10 (define @t800 () (_ tptp.append_com @t799)) % 0.85/1.10 (define @t801 () (_ tptp.append_com tptp.nil_com)) % 0.85/1.10 (define @t802 () (_ @t801 @t543)) % 0.85/1.10 (define @t803 () (= @t500 @t773)) % 0.85/1.10 (define @t804 () (_ tptp.append_com @t549)) % 0.85/1.10 (define @t805 () (=> @t599 (_ @t533 (_ @t804 @t573)))) % 0.85/1.10 (define @t806 () (@var "Ys4" tptp.list_com)) % 0.85/1.10 (define @t807 () (_ (_ tptp.append_com @t806) @t765)) % 0.85/1.10 (define @t808 () (_ @t499 @t806)) % 0.85/1.10 (define @t809 () (@list @t806)) % 0.85/1.10 (define @t810 () (_ tptp.member32358020st_com (_ @t611 @t497))) % 0.85/1.10 (define @t811 () (@list @t497 @t712)) % 0.85/1.10 (define @t812 () (_ tptp.produc1307105171st_com @t497)) % 0.85/1.10 (define @t813 () (_ tptp.member32358020st_com (_ @t812 tptp.nil_com))) % 0.85/1.10 (define @t814 () (@var "Zs2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t815 () (@var "Ys2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t816 () (_ tptp.produc1298457559_state @t815)) % 0.85/1.10 (define @t817 () (_ tptp.member1267359376_state (_ @t789 @t815))) % 0.85/1.10 (define @t818 () (_ @t817 @t787)) % 0.85/1.10 (define @t819 () (@var "Zs2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t820 () (@var "Ys2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t821 () (_ tptp.produc1354769367_state @t820)) % 0.85/1.10 (define @t822 () (_ tptp.member423306384_state (_ @t793 @t820))) % 0.85/1.10 (define @t823 () (_ @t822 @t791)) % 0.85/1.10 (define @t824 () (_ (_ tptp.member1333916004om_com (_ @t715 @t781)) @t712)) % 0.85/1.10 (define @t825 () (_ @t784 @t543)) % 0.85/1.10 (define @t826 () (_ tptp.member32358020st_com (_ @t812 @t825))) % 0.85/1.10 (define @t827 () (@list @t497 @t781 @t543 @t712)) % 0.85/1.10 (define @t828 () (@var "Ys2" tptp.list_state)) % 0.85/1.10 (define @t829 () (@var "Y" tptp.state)) % 0.85/1.10 (define @t830 () (@var "Xs" tptp.list_list_com)) % 0.85/1.10 (define @t831 () (_ (_ tptp.cons_state @t829) @t828)) % 0.85/1.10 (define @t832 () (_ tptp.produc1742567891_state @t830)) % 0.85/1.10 (define @t833 () (_ (_ tptp.member1069318160_state (_ @t354 @t162)) @t22)) % 0.85/1.10 (define @t834 () (_ tptp.cons_P465369265_state @t162)) % 0.85/1.10 (define @t835 () (_ @t834 @t815)) % 0.85/1.10 (define @t836 () (_ tptp.member1267359376_state (_ @t789 @t835))) % 0.85/1.10 (define @t837 () (@list @t788 @t162 @t815 @t22)) % 0.85/1.10 (define @t838 () (_ (_ tptp.member512523024_state (_ @t363 @t174)) @t7)) % 0.85/1.10 (define @t839 () (_ tptp.cons_P438230685_state @t174)) % 0.85/1.10 (define @t840 () (_ @t839 @t820)) % 0.85/1.10 (define @t841 () (_ tptp.member423306384_state (_ @t793 @t840))) % 0.85/1.10 (define @t842 () (@list @t792 @t174 @t820 @t7)) % 0.85/1.10 (define @t843 () (_ tptp.produc1307105171st_com @t543)) % 0.85/1.10 (define @t844 () (@var "Ys2" tptp.list_list_com)) % 0.85/1.10 (define @t845 () (@var "Xs" tptp.list_state)) % 0.85/1.10 (define @t846 () (_ tptp.produc1307105171st_com @t500)) % 0.85/1.10 (define @t847 () (_ tptp.member32358020st_com (_ @t846 @t825))) % 0.85/1.10 (define @t848 () (_ tptp.member32358020st_com (_ @t812 @t543))) % 0.85/1.10 (define @t849 () (_ tptp.product_Pair_com_com @t498)) % 0.85/1.10 (define @t850 () (_ tptp.member1333916004om_com (_ @t849 @t781))) % 0.85/1.10 (define @t851 () (_ @t850 @t712)) % 0.85/1.10 (define @t852 () (@list @t498 @t781 @t712 @t497 @t543)) % 0.85/1.10 (define @t853 () (_ (_ tptp.cons_list_com @t583) @t830)) % 0.85/1.10 (define @t854 () (_ tptp.cons_P465369265_state @t166)) % 0.85/1.10 (define @t855 () (_ tptp.produc1298457559_state (_ @t854 @t788))) % 0.85/1.10 (define @t856 () (_ tptp.member1267359376_state (_ @t855 @t835))) % 0.85/1.10 (define @t857 () (@list @t166 @t162 @t22 @t788 @t815)) % 0.85/1.10 (define @t858 () (_ tptp.cons_P438230685_state @t178)) % 0.85/1.10 (define @t859 () (_ tptp.produc1354769367_state (_ @t858 @t792))) % 0.85/1.10 (define @t860 () (_ tptp.member423306384_state (_ @t859 @t840))) % 0.85/1.10 (define @t861 () (@list @t178 @t174 @t7 @t792 @t820)) % 0.85/1.10 (define @t862 () (@var "Cs5" tptp.list_com)) % 0.85/1.10 (define @t863 () (@var "Cs1" tptp.list_com)) % 0.85/1.10 (define @t864 () (_ tptp.append_com @t863)) % 0.85/1.10 (define @t865 () (@list @t863)) % 0.85/1.10 (define @t866 () (@var "C5" tptp.com)) % 0.85/1.10 (define @t867 () (@var "Ccs" tptp.list_com)) % 0.85/1.10 (define @t868 () (_ @t3 @t398)) % 0.85/1.10 (define @t869 () (@var "Cs14" tptp.list_com)) % 0.85/1.10 (define @t870 () (@var "Cs13" tptp.list_com)) % 0.85/1.10 (define @t871 () (@var "Cs23" tptp.list_com)) % 0.85/1.10 (define @t872 () (@var "Cs1_2" tptp.list_com)) % 0.85/1.10 (define @t873 () (@var "Cs12" tptp.list_com)) % 0.85/1.10 (define @t874 () (@var "Cs16" tptp.list_com)) % 0.85/1.10 (define @t875 () (@var "Cs15" tptp.list_com)) % 0.85/1.10 (define @t876 () (@var "X2" tptp.list_state)) % 0.85/1.10 (define @t877 () (@var "X1" tptp.list_list_com)) % 0.85/1.10 (define @t878 () (@var "P" (-> tptp.list_list_com tptp.list_state Bool))) % 0.85/1.10 (define @t879 () (@var "X2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t880 () (@var "X1" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t881 () (@var "P" (-> tptp.list_P1040014977_state tptp.list_P1040014977_state Bool))) % 0.85/1.10 (define @t882 () (@var "X2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t883 () (@var "X1" tptp.list_P890094829_state)) % 0.85/1.10 (define @t884 () (@var "P" (-> tptp.list_P890094829_state tptp.list_P890094829_state Bool))) % 0.85/1.10 (define @t885 () (@var "Xs3" tptp.list_com)) % 0.85/1.10 (define @t886 () (@var "X4" tptp.com)) % 0.85/1.10 (define @t887 () (@var "Ys" tptp.list_state)) % 0.85/1.10 (define @t888 () (@var "Xs3" tptp.list_list_com)) % 0.85/1.10 (define @t889 () (@var "Y3" tptp.state)) % 0.85/1.10 (define @t890 () (@var "X4" tptp.list_com)) % 0.85/1.10 (define @t891 () (@var "Ys" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t892 () (@var "Xs3" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t893 () (@var "Y3" tptp.produc2041926651_state)) % 0.85/1.10 (define @t894 () (@var "X4" tptp.produc2041926651_state)) % 0.85/1.10 (define @t895 () (@var "Ys" tptp.list_P890094829_state)) % 0.85/1.10 (define @t896 () (@var "Xs3" tptp.list_P890094829_state)) % 0.85/1.10 (define @t897 () (@var "Y3" tptp.produc410756839_state)) % 0.85/1.10 (define @t898 () (@var "F" (-> tptp.com tptp.list_com))) % 0.85/1.10 (define @t899 () (_ tptp.append_com (_ @t898 @t498))) % 0.85/1.10 (define @t900 () (_ tptp.listrel1_com @t712)) % 0.85/1.10 (define @t901 () (_ @t848 @t900)) % 0.85/1.10 (define @t902 () (= @t788 @t815)) % 0.85/1.10 (define @t903 () (_ tptp.listre1738592858_state @t22)) % 0.85/1.10 (define @t904 () (_ @t817 @t903)) % 0.85/1.10 (define @t905 () (= @t792 @t820)) % 0.85/1.10 (define @t906 () (_ tptp.listre1725776070_state @t7)) % 0.85/1.10 (define @t907 () (_ @t822 @t906)) % 0.85/1.10 (define @t908 () (_ tptp.maps_com_com @t898)) % 0.85/1.10 (define @t909 () (@list @t898)) % 0.85/1.10 (define @t910 () (_ tptp.transi436345274st_com @t900)) % 0.85/1.10 (define @t911 () (_ tptp.member32358020st_com (_ @t846 (_ @t499 @t543)))) % 0.85/1.10 (define @t912 () (_ @t848 @t910)) % 0.85/1.10 (define @t913 () (@list @t497 @t543 @t712 @t498)) % 0.85/1.10 (define @t914 () (@var "Vs" tptp.list_com)) % 0.85/1.10 (define @t915 () (_ tptp.transi339813252_state @t903)) % 0.85/1.10 (define @t916 () (_ tptp.transi1965148016_state @t906)) % 0.85/1.10 (define @t917 () (@list @t571)) % 0.85/1.10 (define @t918 () (@var "Zs" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t919 () (@list @t918)) % 0.85/1.10 (define @t920 () (@var "Zs" tptp.list_P890094829_state)) % 0.85/1.10 (define @t921 () (@list @t920)) % 0.85/1.10 (define @t922 () (@list @t788 @t815 @t22)) % 0.85/1.10 (define @t923 () (@list @t792 @t820 @t7)) % 0.85/1.10 (define @t924 () (_ tptp.append_com @t798)) % 0.85/1.10 (define @t925 () (@var "Vs" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t926 () (@var "Us2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t927 () (_ tptp.append982487830_state @t926)) % 0.85/1.10 (define @t928 () (@var "Vs" tptp.list_P890094829_state)) % 0.85/1.10 (define @t929 () (@var "Us2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t930 () (_ tptp.append221843330_state @t929)) % 0.85/1.10 (define @t931 () (@var "Vs2" tptp.list_com)) % 0.85/1.10 (define @t932 () (@var "Us3" tptp.list_com)) % 0.85/1.10 (define @t933 () (_ tptp.append_com @t932)) % 0.85/1.10 (define @t934 () (@var "Vs2" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t935 () (@var "Us3" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t936 () (_ tptp.append982487830_state @t935)) % 0.85/1.10 (define @t937 () (@var "Vs2" tptp.list_P890094829_state)) % 0.85/1.10 (define @t938 () (@var "Us3" tptp.list_P890094829_state)) % 0.85/1.10 (define @t939 () (_ tptp.append221843330_state @t938)) % 0.85/1.10 (define @t940 () (@var "Xss22" tptp.list_list_com)) % 0.85/1.10 (define @t941 () (@var "Xs4" tptp.list_com)) % 0.85/1.10 (define @t942 () (@var "Xss1" tptp.list_list_com)) % 0.85/1.10 (define @t943 () (@var "Xss2" tptp.list_list_com)) % 0.85/1.10 (define @t944 () (= @t943 tptp.nil_list_com)) % 0.85/1.10 (define @t945 () (not @t944)) % 0.85/1.10 (define @t946 () (= (_ tptp.concat_com @t943) @t773)) % 0.85/1.10 (define @t947 () (@list @t943 @t543 @t765)) % 0.85/1.10 (define @t948 () (_ tptp.lexord_com @t712)) % 0.85/1.10 (define @t949 () (@var "B" tptp.com)) % 0.85/1.10 (define @t950 () (_ (_ tptp.cons_com @t949) @t532)) % 0.85/1.10 (define @t951 () (@var "U" tptp.list_com)) % 0.85/1.10 (define @t952 () (_ tptp.append_com @t951)) % 0.85/1.10 (define @t953 () (@var "A" tptp.com)) % 0.85/1.10 (define @t954 () (_ (_ tptp.cons_com @t953) @t583)) % 0.85/1.10 (define @t955 () (_ (_ tptp.member1333916004om_com (_ (_ tptp.product_Pair_com_com @t953) @t949)) @t712)) % 0.85/1.10 (define @t956 () (_ tptp.lexord1062073966_state @t22)) % 0.85/1.10 (define @t957 () (@var "Y" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t958 () (_ (_ tptp.cons_P465369265_state @t35) @t957)) % 0.85/1.10 (define @t959 () (@var "U" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t960 () (_ tptp.append982487830_state @t959)) % 0.85/1.10 (define @t961 () (@var "X" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t962 () (_ (_ tptp.cons_P465369265_state @t24) @t961)) % 0.85/1.10 (define @t963 () (_ tptp.lexord1893203674_state @t7)) % 0.85/1.10 (define @t964 () (@var "Y" tptp.list_P890094829_state)) % 0.85/1.10 (define @t965 () (_ (_ tptp.cons_P438230685_state @t31) @t964)) % 0.85/1.10 (define @t966 () (@var "U" tptp.list_P890094829_state)) % 0.85/1.10 (define @t967 () (_ tptp.append221843330_state @t966)) % 0.85/1.10 (define @t968 () (@var "X" tptp.list_P890094829_state)) % 0.85/1.10 (define @t969 () (_ (_ tptp.cons_P438230685_state @t12) @t968)) % 0.85/1.10 (define @t970 () (_ tptp.concat_com @t830)) % 0.85/1.10 (define @t971 () (_ tptp.produc1307105171st_com @t583)) % 0.85/1.10 (define @t972 () (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t961) @t957)) @t956)) % 0.85/1.10 (define @t973 () (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t968) @t964)) @t963)) % 0.85/1.10 (define @t974 () (@var "A3" tptp.com)) % 0.85/1.10 (define @t975 () (_ tptp.concat_com tptp.nil_list_com)) % 0.85/1.10 (define @t976 () (_ tptp.append_com @t583)) % 0.85/1.10 (define @t977 () (@var "V" tptp.list_com)) % 0.85/1.10 (define @t978 () (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com (_ @t976 @t951)) (_ @t976 @t977))) @t948)) % 0.85/1.10 (define @t979 () (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t951) @t977)) @t948)) % 0.85/1.10 (define @t980 () (@var "V" tptp.list_P1040014977_state)) % 0.85/1.10 (define @t981 () (_ tptp.append982487830_state @t961)) % 0.85/1.10 (define @t982 () (@var "V" tptp.list_P890094829_state)) % 0.85/1.10 (define @t983 () (_ tptp.append221843330_state @t968)) % 0.85/1.10 (define @t984 () (@var "Z3" tptp.list_com)) % 0.85/1.10 (define @t985 () (@var "B5" tptp.com)) % 0.85/1.10 (define @t986 () (@var "Xss23" tptp.list_list_com)) % 0.85/1.10 (define @t987 () (@var "Xs5" tptp.list_com)) % 0.85/1.10 (define @t988 () (@var "Xss12" tptp.list_list_com)) % 0.85/1.10 (define @t989 () (_ tptp.cons_com tptp.c)) % 0.85/1.10 (define @t990 () (_ (_ tptp.produc1204172211_state (_ @t989 tptp.nil_com)) tptp.s)) % 0.85/1.10 (define @t991 () (_ tptp.transi1726587420_state tptp.pHoare259243666_exec1)) % 0.85/1.10 (define @t992 () (_ tptp.f @t9)) % 0.85/1.10 (define @t993 () (_ tptp.f @t8)) % 0.85/1.10 (define @t994 () (_ (_ tptp.produc1909270103_state @t993) @t992)) % 0.85/1.10 (define @t995 () (_ (_ tptp.member1069318160_state @t994) @t991)) % 0.85/1.10 (define @t996 () (forall @t11 @t995)) % 0.85/1.10 (define @t997 () (_ tptp.f tptp.n)) % 0.85/1.10 (define @t998 () (_ tptp.produc1909270103_state @t990)) % 0.85/1.10 (define @t999 () (_ tptp.suc tptp.n)) % 0.85/1.10 (define @t1000 () (_ tptp.f @t999)) % 0.85/1.10 (define @t1001 () (not (_ (_ tptp.member1069318160_state (_ @t998 @t1000)) @t42))) % 0.85/1.10 (define @t1002 () (@var "I3" tptp.nat)) % 0.85/1.10 (define @t1003 () (@var "F3" (-> tptp.nat tptp.produc2041926651_state))) % 0.85/1.10 (define @t1004 () (lambda (@list @t465 @t468) (exists (@list @t1003) (and (= (_ @t1003 tptp.zero_zero_nat) (_ (_ tptp.produc1204172211_state @t465) @t468)) (forall (@list @t1002) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ @t1003 @t1002)) (_ @t1003 (_ tptp.suc @t1002)))) tptp.pHoare259243666_exec1)))))) % 0.85/1.10 (define @t1005 () (tptp.transi1726587420_state @t22)) % 0.85/1.10 (define @t1006 () (tptp.produc1909270103_state @t166 @t256)) % 0.85/1.10 (define @t1007 () (tptp.member1069318160_state @t1006 @t1005)) % 0.85/1.10 (define @t1008 () (tptp.produc1909270103_state @t162 @t256)) % 0.85/1.10 (define @t1009 () (tptp.member1069318160_state @t1008 @t1005)) % 0.85/1.10 (define @t1010 () (not @t379)) % 0.85/1.10 (define @t1011 () (tptp.produc1909270103_state @t166 @t162)) % 0.85/1.10 (define @t1012 () (tptp.member1069318160_state @t1011 @t1005)) % 0.85/1.10 (define @t1013 () (not @t359)) % 0.85/1.10 (define @t1014 () (or @t1013 @t1010 @t375)) % 0.85/1.10 (define @t1015 () (tptp.transi1726587420_state tptp.pHoare259243666_exec1)) % 0.85/1.10 (define @t1016 () (tptp.suc @t8)) % 0.85/1.10 (define @t1017 () (tptp.f @t1016)) % 0.85/1.10 (define @t1018 () (tptp.f @t8)) % 0.85/1.10 (define @t1019 () (tptp.produc1909270103_state @t1018 @t1017)) % 0.85/1.10 (define @t1020 () (tptp.member1069318160_state @t1019 @t1015)) % 0.85/1.10 (define @t1021 () (tptp.transi1726587420_state @t49)) % 0.85/1.10 (define @t1022 () (tptp.produc1909270103_state @t24 @t35)) % 0.85/1.10 (define @t1023 () (tptp.member1069318160_state @t1022 @t1021)) % 0.85/1.10 (define @t1024 () (_ tptp.member1069318160_state @t1022)) % 0.85/1.10 (define @t1025 () (tptp.transi1302705790_state @t49)) % 0.85/1.10 (define @t1026 () (tptp.member1069318160_state @t1022 @t1025)) % 0.85/1.10 (define @t1027 () (not @t190)) % 0.85/1.10 (define @t1028 () (or @t1027 @t186 @t188)) % 0.85/1.10 (define @t1029 () (tptp.f tptp.n)) % 0.85/1.10 (define @t1030 () (tptp.concat_com tptp.nil_list_com)) % 0.85/1.10 (define @t1031 () (tptp.cons_com tptp.c @t1030)) % 0.85/1.10 (define @t1032 () (tptp.produc1204172211_state @t1031 tptp.s)) % 0.85/1.10 (define @t1033 () (tptp.transi1302705790_state @t22)) % 0.85/1.10 (define @t1034 () (tptp.member1069318160_state @t1022 @t1033)) % 0.85/1.10 (define @t1035 () (tptp.member1069318160_state @t1022 @t1005)) % 0.85/1.10 (define @t1036 () (not @t195)) % 0.85/1.10 (define @t1037 () (or @t1036 @t38)) % 0.85/1.10 (define @t1038 () (tptp.suc tptp.n)) % 0.85/1.10 (define @t1039 () (tptp.f @t1038)) % 0.85/1.10 (define @t1040 () (_ @t989 @t975)) % 0.85/1.10 (define @t1041 () (_ (_ tptp.produc1204172211_state @t1040) tptp.s)) % 0.85/1.10 (define @t1042 () (_ tptp.produc1909270103_state @t1041)) % 0.85/1.10 (define @t1043 () (_ @t1042 @t1000)) % 0.85/1.10 (define @t1044 () (tptp.transi1302705790_state tptp.pHoare259243666_exec1)) % 0.85/1.10 (define @t1045 () (tptp.produc1909270103_state @t1032 @t1039)) % 0.85/1.10 (define @t1046 () (tptp.member1069318160_state @t1045 @t1044)) % 0.85/1.10 (define @t1047 () (_ (_ tptp.member1069318160_state @t1043) @t42)) % 0.85/1.10 (define @t1048 () (_ tptp.produc1909270103_state @t1032)) % 0.85/1.10 (define @t1049 () (tptp.member1069318160_state @t1045 @t1015)) % 0.85/1.10 (define @t1050 () (not @t1049)) % 0.85/1.10 (define @t1051 () (or @t1050 @t1046)) % 0.85/1.10 (define @t1052 () (@list true false)) % 0.85/1.10 (define @t1053 () (tptp.produc1909270103_state @t1029 @t1039)) % 0.85/1.10 (define @t1054 () (tptp.member1069318160_state @t1053 @t1015)) % 0.85/1.10 (define @t1055 () (not @t1054)) % 0.85/1.10 (define @t1056 () (= @t1032 @t1029)) % 0.85/1.10 (define @t1057 () (not @t1056)) % 0.85/1.10 (define @t1058 () (and @t1050 @t1056 @t1054)) % 0.85/1.10 (define @t1059 () (_ @t1042 @t997)) % 0.85/1.10 (define @t1060 () (tptp.produc1909270103_state @t1032 @t1029)) % 0.85/1.10 (define @t1061 () (tptp.member1069318160_state @t1060 @t1044)) % 0.85/1.10 (define @t1062 () (tptp.member1069318160_state @t1060 @t1015)) % 0.85/1.10 (define @t1063 () (and @t1057 @t1062)) % 0.85/1.10 (define @t1064 () (not @t1061)) % 0.85/1.10 (define @t1065 () (or @t1064 @t1056 @t1063)) % 0.85/1.10 (define @t1066 () (not @t1062)) % 0.85/1.10 (define @t1067 () (or @t1066 @t1055 @t1049)) % 0.85/1.10 (define @t1068 () (not @t1067)) % 0.85/1.10 (define @t1069 () (forall @t306 (or (not @t1012) (not @t1009) @t1007))) % 0.85/1.10 (assume @p1 (forall (@list @t5 @t2 @t1) (not (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ @t6 @t5)) @t4)) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p2 (forall (@list @t12 @t16 @t7) (=> @t21 @t13))) % 0.85/1.10 (assume @p3 (forall (@list @t24 @t26 @t22) (=> @t30 @t25))) % 0.85/1.10 (assume @p4 (forall (@list @t12 @t16 @t7 @t31) (=> @t21 (=> @t34 (=> (= @t31 (_ @t16 tptp.zero_zero_nat)) @t13))))) % 0.85/1.10 (assume @p5 (forall (@list @t24 @t26 @t22 @t35) (=> @t30 (=> @t38 (=> (= @t35 (_ @t26 tptp.zero_zero_nat)) @t25))))) % 0.85/1.10 (assume @p6 (forall (@list @t40 @t5 @t39 @t2 @t1) (=> (_ (_ tptp.member1069318160_state (_ @t45 (_ (_ tptp.produc1204172211_state (_ (_ tptp.cons_com @t39) @t2)) @t1))) @t42) (=> @t41 (_ (_ tptp.termi @t39) @t1))))) % 0.85/1.10 (assume @p7 (forall @t48 (= (_ tptp.transi1666849160_state @t47) @t47))) % 0.85/1.10 (assume @p8 (forall @t51 (= (_ tptp.transi1726587420_state @t50) @t50))) % 0.85/1.10 (assume @p9 (forall @t48 (= (_ tptp.transi463013610_state @t52) @t47))) % 0.85/1.10 (assume @p10 (forall @t51 (= (_ tptp.transi1302705790_state @t53) @t50))) % 0.85/1.10 (assume @p11 (forall @t81 (=> (_ @t80 @t72) (=> (forall @t78 (=> (_ @t76 @t65) @t64)) (=> (forall @t77 (=> (_ @t76 @t72) @t71)) @t57))))) % 0.85/1.10 (assume @p12 (forall @t108 (=> (_ @t107 @t99) (=> (forall @t105 (=> (_ @t103 @t7) @t92)) (=> (forall @t104 (=> (_ @t103 @t99) @t98)) @t85))))) % 0.85/1.10 (assume @p13 (forall @t133 (=> (_ @t132 @t124) (=> (forall @t130 (=> (_ @t128 @t22) @t118)) (=> (forall @t129 (=> (_ @t128 @t124) @t123)) @t112))))) % 0.85/1.10 (assume @p14 (forall @t81 (=> @t136 (=> @t135 (=> (forall @t77 (=> (_ @t76 @t134) @t71)) @t57))))) % 0.85/1.10 (assume @p15 (forall @t108 (=> @t138 (=> @t137 (=> (forall @t104 (=> (_ @t103 @t18) @t98)) @t85))))) % 0.85/1.10 (assume @p16 (forall @t133 (=> @t140 (=> @t139 (=> (forall @t129 (=> (_ @t128 @t28) @t123)) @t112))))) % 0.85/1.10 (assume @p17 (forall (@list @t145 @t144 @t142 @t141 @t65) (=> (_ (_ tptp.member284400400_state (_ @t147 @t143)) @t134) (=> (not (= @t146 @t143)) (not (forall @t78 (=> (_ (_ tptp.member284400400_state (_ @t147 @t68)) @t65) (not (_ (_ tptp.member284400400_state (_ @t69 @t143)) @t134))))))))) % 0.85/1.10 (assume @p18 (forall (@list @t152 @t151 @t149 @t148 @t7) (=> (_ (_ tptp.member512523024_state (_ @t154 @t150)) @t18) (=> (not (= @t153 @t150)) (not (forall @t105 (=> (_ (_ tptp.member512523024_state (_ @t154 @t95)) @t7) (not (_ (_ tptp.member512523024_state (_ @t96 @t150)) @t18))))))))) % 0.85/1.10 (assume @p19 (forall (@list @t159 @t158 @t156 @t155 @t22) (=> (_ (_ tptp.member1069318160_state (_ @t161 @t157)) @t28) (=> (not (= @t160 @t157)) (not (forall @t130 (=> (_ (_ tptp.member1069318160_state (_ @t161 @t120)) @t22) (not (_ (_ tptp.member1069318160_state (_ @t121 @t157)) @t28))))))))) % 0.85/1.10 (assume @p20 (forall @t81 (=> @t136 (=> @t57 (=> (forall @t77 (=> @t70 (=> (_ (_ tptp.member284400400_state (_ (_ tptp.produc2049704791_state @t66) @t79)) @t134) (=> @t60 @t64)))) @t135))))) % 0.85/1.10 (assume @p21 (forall @t133 (=> @t140 (=> @t112 (=> (forall @t129 (=> @t122 (=> (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t119) @t131)) @t28) (=> @t115 @t118)))) @t139))))) % 0.85/1.10 (assume @p22 (forall @t108 (=> @t138 (=> @t85 (=> (forall @t104 (=> @t97 (=> (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t93) @t106)) @t18) (=> @t88 @t92)))) @t137))))) % 0.85/1.10 (assume @p23 (forall @t173 (=> @t172 (exists @t169 (and (_ @t168 @t49) (_ @t165 @t50)))))) % 0.85/1.10 (assume @p24 (forall @t184 (=> @t183 (exists @t181 (and (_ @t180 @t46) (_ @t177 @t47)))))) % 0.85/1.10 (assume @p25 @t192) % 0.85/1.10 (assume @p26 (forall (@list @t12 @t31 @t46) (=> (_ @t33 @t47) (or @t193 (and @t194 (_ @t33 @t52)))))) % 0.85/1.10 (assume @p27 (forall @t173 (=> @t172 (exists @t169 (and (_ @t168 @t50) (_ @t165 @t49)))))) % 0.85/1.10 (assume @p28 (forall @t184 (=> @t183 (exists @t181 (and (_ @t180 @t47) (_ @t177 @t46)))))) % 0.85/1.10 (assume @p29 @t197) % 0.85/1.10 (assume @p30 (forall @t199 (=> @t198 @t34))) % 0.85/1.10 (assume @p31 (forall @t173 (= (_ @t171 @t50) (or @t200 (and @t201 @t172))))) % 0.85/1.10 (assume @p32 (forall @t184 (= (_ @t182 @t47) (or @t202 (and @t203 @t183))))) % 0.85/1.10 (assume @p33 (forall @t207 (=> @t206 (_ @t205 @t28)))) % 0.85/1.10 (assume @p34 (forall @t211 (=> @t210 (_ @t209 @t18)))) % 0.85/1.10 (assume @p35 (forall @t212 (= (_ tptp.transi1302705790_state @t28) @t28))) % 0.85/1.10 (assume @p36 (forall @t213 (= (_ tptp.transi463013610_state @t18) @t18))) % 0.85/1.10 (assume @p37 (forall @t207 (=> @t206 (_ @t205 @t124)))) % 0.85/1.10 (assume @p38 (forall @t211 (=> @t210 (_ @t209 @t99)))) % 0.85/1.10 (assume @p39 (forall @t220 (=> @t219 (=> @t218 @t216)))) % 0.85/1.10 (assume @p40 (forall @t227 (=> @t226 (=> @t225 @t223)))) % 0.85/1.10 (assume @p41 (forall @t220 (=> @t38 (=> @t228 @t216)))) % 0.85/1.10 (assume @p42 (forall @t227 (=> @t34 (=> @t229 @t223)))) % 0.85/1.10 (assume @p43 (forall @t242 (=> @t38 (=> @t241 (=> (forall @t240 (=> @t239 (=> (_ @t236 @t28) @t235))) @t231))))) % 0.85/1.10 (assume @p44 (forall @t255 (=> @t34 (=> @t254 (=> (forall @t253 (=> @t252 (=> (_ @t249 @t18) @t248))) @t244))))) % 0.85/1.10 (assume @p45 (forall (@list @t24 @t22) (_ (_ tptp.member1069318160_state (_ @t29 @t24)) @t28))) % 0.85/1.10 (assume @p46 (forall (@list @t12 @t7) (_ (_ tptp.member512523024_state (_ @t19 @t12)) @t18))) % 0.85/1.10 (assume @p47 (forall @t263 (=> @t262 (=> (not (= @t166 @t256)) (not (forall @t259 (=> @t258 (not (_ @t257 @t28))))))))) % 0.85/1.10 (assume @p48 (forall @t270 (=> @t269 (=> (not (= @t178 @t264)) (not (forall @t267 (=> @t266 (not (_ @t265 @t18))))))))) % 0.85/1.10 (assume @p49 (forall @t283 (=> (_ @t282 @t28) (=> (forall @t280 (_ @t91 @t90)) (=> (forall @t279 (=> (_ @t278 @t28) @t277)) @t273))))) % 0.85/1.10 (assume @p50 (forall @t295 (=> (_ @t294 @t18) (=> (forall @t292 (_ @t63 @t62)) (=> (forall @t291 (=> (_ @t290 @t18) @t289)) @t286))))) % 0.85/1.10 (assume @p51 (forall @t242 (=> @t38 (=> @t231 (=> (forall @t240 (=> @t298 @t296)) @t241))))) % 0.85/1.10 (assume @p52 (forall @t255 (=> @t34 (=> @t244 (=> (forall @t253 (=> @t301 @t299)) @t254))))) % 0.85/1.10 (assume @p53 (forall @t306 (=> @t305 (=> (_ @t304 @t28) @t262)))) % 0.85/1.10 (assume @p54 (forall @t310 (=> @t309 (=> (_ @t308 @t18) @t269)))) % 0.85/1.10 (assume @p55 (forall @t324 (= @t323 (or (exists (@list @t314) (and @t319 (= @t316 @t314))) (exists @t320 (and @t319 @t317 (_ @t315 @t28) @t313)))))) % 0.85/1.10 (assume @p56 (forall @t338 (= @t337 (or (exists (@list @t328) (and @t333 (= @t330 @t328))) (exists @t334 (and @t333 @t331 (_ @t329 @t18) @t327)))))) % 0.85/1.10 (assume @p57 (forall @t324 (=> @t323 (=> (not (= @t316 @t318)) (not (forall @t341 (=> (_ @t340 @t28) @t339))))))) % 0.85/1.10 (assume @p58 (forall @t338 (=> @t337 (=> (not (= @t330 @t332)) (not (forall @t344 (=> (_ @t343 @t18) @t342))))))) % 0.85/1.10 (assume @p59 (forall @t196 (=> @t38 (=> @t187 (not (forall @t259 (=> @t298 (not @t345)))))))) % 0.85/1.10 (assume @p60 (forall @t199 (=> @t34 (=> @t194 (not (forall @t267 (=> @t301 (not @t346)))))))) % 0.85/1.10 (assume @p61 (forall @t220 (=> @t195 @t348))) % 0.85/1.10 (assume @p62 (forall @t227 (=> @t198 @t350))) % 0.85/1.10 (assume @p63 (forall @t242 (=> @t195 (=> (forall @t259 (=> @t345 @t233)) (=> (forall @t240 (=> @t239 (=> (_ @t236 @t124) @t235))) @t231))))) % 0.85/1.10 (assume @p64 (forall @t255 (=> @t198 (=> (forall @t267 (=> @t346 @t246)) (=> (forall @t253 (=> @t252 (=> (_ @t249 @t99) @t248))) @t244))))) % 0.85/1.10 (assume @p65 (forall @t196 (=> @t219 @t195))) % 0.85/1.10 (assume @p66 (forall @t199 (=> @t226 @t198))) % 0.85/1.10 (assume @p67 (forall (@list @t166 @t162 @t22 @t84) (=> @t359 (=> (forall @t358 (=> @t357 @t353)) (=> (forall (@list @t351 @t232 @t163) (=> (_ @t356 @t124) (=> @t353 (=> (_ @t238 @t124) (=> (_ (_ @t84 @t232) @t163) (_ @t352 @t163)))))) (_ (_ @t84 @t166) @t162)))))) % 0.85/1.10 (assume @p68 (forall (@list @t178 @t174 @t7 @t56) (=> @t368 (=> (forall @t367 (=> @t366 @t362)) (=> (forall (@list @t360 @t245 @t175) (=> (_ @t365 @t99) (=> @t362 (=> (_ @t251 @t99) (=> (_ (_ @t56 @t245) @t175) (_ @t361 @t175)))))) (_ (_ @t56 @t178) @t174)))))) % 0.85/1.10 (assume @p69 (forall @t220 (=> @t219 (=> (_ @t217 @t124) @t347)))) % 0.85/1.10 (assume @p70 (forall @t227 (=> @t226 (=> (_ @t224 @t99) @t349)))) % 0.85/1.10 (assume @p71 (forall (@list @t22 @t166 @t162) (=> (forall @t371 (not (_ @t370 @t124))) (=> @t369 @t201)))) % 0.85/1.10 (assume @p72 (forall (@list @t7 @t178 @t174) (=> (forall @t374 (not (_ @t373 @t99))) (=> @t372 @t203)))) % 0.85/1.10 (assume @p73 (forall @t263 (=> @t375 (=> (not (_ @t261 @t22)) (not (forall @t259 (=> @t258 (not (_ @t257 @t124))))))))) % 0.85/1.10 (assume @p74 (forall @t270 (=> @t376 (=> (not (_ @t268 @t7)) (not (forall @t267 (=> @t266 (not (_ @t265 @t99))))))))) % 0.85/1.10 (assume @p75 (forall (@list @t24 @t35 @t49 @t214) (=> (_ @t37 @t49) (=> (_ @t217 @t49) (_ @t215 @t53))))) % 0.85/1.10 (assume @p76 (forall (@list @t12 @t31 @t46 @t221) (=> (_ @t33 @t46) (=> (_ @t224 @t46) (_ @t222 @t52))))) % 0.85/1.10 (assume @p77 (forall @t283 (=> (_ @t282 @t124) (=> (forall @t105 (=> @t377 @t92)) (=> (forall @t279 (=> (_ @t278 @t124) @t277)) @t273))))) % 0.85/1.10 (assume @p78 (forall @t295 (=> (_ @t294 @t99) (=> (forall @t78 (=> @t378 @t64)) (=> (forall @t291 (=> (_ @t290 @t99) @t289)) @t286))))) % 0.85/1.10 (assume @p79 (forall @t242 (=> @t195 (=> (forall @t259 (=> (_ @t297 @t22) @t233)) (=> (forall @t240 (=> (_ @t297 @t124) @t296)) @t241))))) % 0.85/1.10 (assume @p80 (forall @t255 (=> @t198 (=> (forall @t267 (=> (_ @t300 @t7) @t246)) (=> (forall @t253 (=> (_ @t300 @t99) @t299)) @t254))))) % 0.85/1.10 (assume @p81 @t381) % 0.85/1.10 (assume @p82 (forall @t310 (=> @t368 @t382))) % 0.85/1.10 (assume @p83 (forall @t324 (= @t383 (or (exists (@list @t314 @t312) (and @t319 (= @t316 @t312) (_ @t315 @t22))) (exists @t320 (and @t319 @t317 (_ @t315 @t124) @t313)))))) % 0.85/1.10 (assume @p84 (forall @t338 (= @t384 (or (exists (@list @t328 @t326) (and @t333 (= @t330 @t326) (_ @t329 @t7))) (exists @t334 (and @t333 @t331 (_ @t329 @t99) @t327)))))) % 0.85/1.10 (assume @p85 (forall @t324 (=> @t383 (=> (not (_ @t322 @t22)) (not (forall @t341 (=> (_ @t340 @t124) @t339))))))) % 0.85/1.10 (assume @p86 (forall @t338 (=> @t384 (=> (not (_ @t336 @t7)) (not (forall @t344 (=> (_ @t343 @t99) @t342))))))) % 0.85/1.10 (assume @p87 (forall @t196 (=> @t195 (=> (not @t219) (not (forall (@list @t274) (=> (_ (_ tptp.member1069318160_state (_ @t29 @t274)) @t124) (not (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t274) @t35)) @t22))))))))) % 0.85/1.10 (assume @p88 (forall @t199 (=> @t198 (=> (not @t226) (not (forall (@list @t287) (=> (_ (_ tptp.member512523024_state (_ @t19 @t287)) @t99) (not (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t287) @t31)) @t7))))))))) % 0.85/1.10 (assume @p89 (forall (@list @t40 @t5) (=> @t41 (not @t385)))) % 0.85/1.10 (assume @p90 (forall (@list @t12 @t243) (= (_ (_ tptp.member1069318160_state @t12) (_ tptp.collec300063826_state @t243)) @t244))) % 0.85/1.10 (assume @p91 (forall (@list @t386 @t387) (= (_ (_ tptp.member_state @t386) (_ tptp.collect_state @t387)) (_ @t387 @t386)))) % 0.85/1.10 (assume @p92 (forall (@list @t388 @t389) (= (_ (_ tptp.member512523024_state @t388) (_ tptp.collec489924946_state @t389)) (_ @t389 @t388)))) % 0.85/1.10 (assume @p93 (forall (@list @t390) (= (_ tptp.collec300063826_state (lambda (@list @t391) (_ (_ tptp.member1069318160_state @t391) @t390))) @t390))) % 0.85/1.10 (assume @p94 (forall (@list @t392) (= (_ tptp.collect_state (lambda (@list @t393) (_ (_ tptp.member_state @t393) @t392))) @t392))) % 0.85/1.10 (assume @p95 (forall (@list @t394) (= (_ tptp.collec489924946_state (lambda (@list @t395) (_ (_ tptp.member512523024_state @t395) @t394))) @t394))) % 0.85/1.10 (assume @p96 (forall @t220 (=> @t195 @t396))) % 0.85/1.10 (assume @p97 (forall @t227 (=> @t198 @t397))) % 0.85/1.10 (assume @p98 (forall @t306 (=> @t305 @t380))) % 0.85/1.10 (assume @p99 (forall @t310 (=> @t309 @t382))) % 0.85/1.10 (assume @p100 (forall @t220 (=> @t219 @t396))) % 0.85/1.10 (assume @p101 (forall @t227 (=> @t226 @t397))) % 0.85/1.10 (assume @p102 (forall @t220 (=> @t38 @t348))) % 0.85/1.10 (assume @p103 (forall @t227 (=> @t34 @t350))) % 0.85/1.10 (assume @p104 (forall (@list @t399 @t5 @t398) (=> (_ (_ tptp.member1069318160_state (_ @t404 @t401)) @t42) (_ (_ @t400 @t399) @t398)))) % 0.85/1.10 (assume @p105 (forall @t409 (=> @t408 @t406))) % 0.85/1.10 (assume @p106 (forall (@list @t411 @t410) (= (= (_ tptp.suc @t411) @t412) (= @t411 @t410)))) % 0.85/1.10 (assume @p107 (forall (@list @t414 @t413) (= (= @t415 (_ tptp.suc @t413)) (= @t414 @t413)))) % 0.85/1.10 (assume @p108 (forall (@list @t419 @t417 @t418 @t416) (= (= @t421 (_ (_ tptp.cons_com @t418) @t416)) (and @t420 (= @t417 @t416))))) % 0.85/1.10 (assume @p109 (forall (@list @t40 @t5 @t398) (=> (_ (_ tptp.member1069318160_state (_ @t45 @t401)) @t42) @t424))) % 0.85/1.10 (assume @p110 (forall @t432 (= @t431 (and @t430 @t427)))) % 0.85/1.10 (assume @p111 (forall @t438 (= @t437 (and @t436 @t434)))) % 0.85/1.10 (assume @p112 (forall @t444 (= @t443 (and @t442 @t440)))) % 0.85/1.10 (assume @p113 (forall (@list @t448 @t446 @t447 @t445) (= (= (_ (_ tptp.produc1204172211_state @t448) @t446) (_ (_ tptp.produc1204172211_state @t447) @t445)) (and (= @t448 @t447) (= @t446 @t445))))) % 0.85/1.10 (assume @p114 (forall (@list @t272 @t271 @t450 @t449) (= (= @t281 (_ (_ tptp.produc1909270103_state @t450) @t449)) (and (= @t272 @t450) (= @t271 @t449))))) % 0.85/1.10 (assume @p115 (forall (@list @t285 @t284 @t452 @t451) (= (= @t293 (_ (_ tptp.produc2065881943_state @t452) @t451)) (and (= @t285 @t452) (= @t284 @t451))))) % 0.85/1.10 (assume @p116 (forall (@list @t5 @t40 @t398 @t399 @t453) (=> @t424 (=> (_ (_ (_ tptp.pHoare259243732_execs @t398) @t399) @t453) (_ (_ @t400 @t454) @t453))))) % 0.85/1.10 (assume @p117 (forall (@list @t460 @t462 @t455) (=> (_ (_ (_ tptp.pHoare259243732_execs @t460) @t462) @t455) (=> (=> @t463 (not (= @t455 @t460))) (not (forall (@list @t459 @t457 @t456) (=> (= @t462 @t461) (=> (_ (_ (_ tptp.exec @t460) @t459) @t457) (not (_ @t458 @t455)))))))))) % 0.85/1.10 (assume @p118 (= tptp.pHoare259243732_execs (lambda (@list @t471 @t470 @t469) (or (exists (@list @t468) (and @t472 (= @t470 tptp.nil_com) (= @t469 @t468))) (exists (@list @t468 @t467 @t466 @t465 @t464) (and @t472 (= @t470 (_ (_ tptp.cons_com @t467) @t465)) (= @t469 @t464) (_ (_ (_ tptp.exec @t468) @t467) @t466) (_ (_ (_ tptp.pHoare259243732_execs @t466) @t465) @t464))))))) % 0.85/1.10 (assume @p119 (forall (@list @t475 @t474 @t473 @t476) (=> (_ (_ (_ tptp.pHoare259243732_execs @t475) @t474) @t473) (=> (forall (@list @t478) (_ (_ @t479 tptp.nil_com) @t478)) (=> (forall (@list @t478 @t459 @t457 @t456 @t477) (=> (_ (_ (_ tptp.exec @t478) @t459) @t457) (=> (_ @t458 @t477) (=> (_ (_ (_ @t476 @t457) @t456) @t477) (_ (_ @t479 @t461) @t477))))) (_ (_ (_ @t476 @t475) @t474) @t473)))))) % 0.85/1.10 (assume @p120 (forall @t480 (= (_ (_ tptp.pHoare806997636termis @t454) @t5) (and @t41 (forall (@list @t466) (=> (_ @t423 @t466) (_ @t405 @t466))))))) % 0.85/1.10 (assume @p121 (forall @t481 (_ (_ @t400 tptp.nil_com) @t5))) % 0.85/1.10 (assume @p122 (forall @t481 (_ (_ tptp.pHoare806997636termis tptp.nil_com) @t5))) % 0.85/1.10 (assume @p123 (forall (@list @t482) (= (= tptp.zero_zero_nat @t482) (= @t482 tptp.zero_zero_nat)))) % 0.85/1.10 (assume @p124 (forall (@list @t487) (exists (@list @t484 @t483) (= @t487 @t486)))) % 0.85/1.10 (assume @p125 (forall (@list @t204) (exists @t358 (= @t204 @t355)))) % 0.85/1.10 (assume @p126 (forall (@list @t208) (exists @t367 (= @t208 @t364)))) % 0.85/1.10 (assume @p127 (forall (@list @t230 @t487) (=> @t488 (_ @t230 @t487)))) % 0.85/1.10 (assume @p128 (forall (@list @t243 @t204) (=> @t489 (_ @t243 @t204)))) % 0.85/1.10 (assume @p129 (forall (@list @t389 @t208) (=> @t490 (_ @t389 @t208)))) % 0.85/1.10 (assume @p130 (forall @t432 (=> @t431 (not (=> @t430 (not @t427)))))) % 0.85/1.10 (assume @p131 (forall @t438 (=> @t437 (not (=> @t436 (not @t434)))))) % 0.85/1.10 (assume @p132 (forall @t444 (=> @t443 (not (=> @t442 (not @t440)))))) % 0.85/1.10 (assume @p133 (forall (@list @t162) (not (forall @t130 (not (= @t162 @t120)))))) % 0.85/1.10 (assume @p134 (forall @t491 (not (forall @t105 (not (= @t174 @t95)))))) % 0.85/1.10 (assume @p135 (forall @t493 (not (forall @t78 (not (= @t492 @t68)))))) % 0.85/1.10 (assume @p136 (forall (@list @t230 @t494) (=> @t488 (_ @t230 @t494)))) % 0.85/1.10 (assume @p137 (forall (@list @t243 @t495) (=> @t489 (_ @t243 @t495)))) % 0.85/1.10 (assume @p138 (forall (@list @t389 @t496) (=> @t490 (_ @t389 @t496)))) % 0.85/1.10 (assume @p139 (forall (@list @t498 @t497) (not (= @t500 @t497)))) % 0.85/1.10 (assume @p140 (forall (@list @t482 @t501) (=> (= (_ tptp.suc @t482) (_ tptp.suc @t501)) (= @t482 @t501)))) % 0.85/1.10 (assume @p141 (forall @t504 (not (= @t502 @t503)))) % 0.85/1.10 (assume @p142 (forall @t480 (=> (_ (_ tptp.pHoare2126160787le_inf @t454) @t5) (or @t385 (exists @t506 (and @t505 (_ (_ tptp.pHoare2126160787le_inf @t399) @t457))))))) % 0.85/1.10 (assume @p143 (forall (@list @t414) (not (= tptp.zero_zero_nat @t415)))) % 0.85/1.10 (assume @p144 (forall @t507 (not (= @t412 tptp.zero_zero_nat)))) % 0.85/1.10 (assume @p145 (forall @t507 (not (= tptp.zero_zero_nat @t412)))) % 0.85/1.10 (assume @p146 (forall (@list @t411 @t414) (=> (= @t411 @t415) (not (= @t411 tptp.zero_zero_nat))))) % 0.85/1.10 (assume @p147 (forall (@list @t508 @t502) (=> @t513 (=> (forall @t512 (=> @t511 @t510)) (_ @t508 @t502))))) % 0.85/1.10 (assume @p148 (forall (@list @t515 @t514 @t502) (=> (forall (@list @t518) (_ @t519 tptp.zero_zero_nat)) (=> (forall (@list @t516) (_ (_ @t515 tptp.zero_zero_nat) @t517)) (=> (forall (@list @t518 @t516) (=> (_ @t519 @t516) (_ (_ @t515 (_ tptp.suc @t518)) @t517))) (_ (_ @t515 @t514) @t502)))))) % 0.85/1.10 (assume @p149 (forall (@list @t508 @t520) (=> (_ @t508 @t520) (=> (forall @t512 (=> @t510 @t511)) @t513)))) % 0.85/1.10 (assume @p150 (forall @t522 (not (= @t521 tptp.zero_zero_nat)))) % 0.85/1.10 (assume @p151 (forall @t522 (not (= tptp.zero_zero_nat @t521)))) % 0.85/1.10 (assume @p152 (forall (@list @t501) (=> (not (= @t501 tptp.zero_zero_nat)) (not (forall @t525 (not (= @t501 @t524))))))) % 0.85/1.10 (assume @p153 (forall (@list @t508 @t411) (=> @t513 (=> (forall @t525 (=> (_ @t508 @t523) (_ @t508 @t524))) (_ @t508 @t411))))) % 0.85/1.10 (assume @p154 (forall @t504 (=> @t528 (exists (@list @t526) (= @t502 (_ tptp.suc @t526)))))) % 0.85/1.10 (assume @p155 (forall (@list @t419 @t417) (not (= tptp.nil_com @t421)))) % 0.85/1.10 (assume @p156 (forall (@list @t529 @t419 @t417) (=> (= @t529 @t421) (not (= @t529 tptp.nil_com))))) % 0.85/1.10 (assume @p157 (forall (@list @t532) (=> (not (= @t532 tptp.nil_com)) (not (forall (@list @t531 @t530) (not (= @t532 (_ (_ tptp.cons_com @t531) @t530)))))))) % 0.85/1.10 (assume @p158 (forall (@list @t533 @t529) (=> @t536 (=> (forall (@list @t535 @t534) (=> (_ @t533 @t534) (_ @t533 (_ (_ tptp.cons_com @t535) @t534)))) (_ @t533 @t529))))) % 0.85/1.10 (assume @p159 (forall @t542 (= @t541 (exists (@list @t538 @t537) (= @t497 @t539))))) % 0.85/1.10 (assume @p160 (forall (@list @t544 @t497 @t543) (=> @t561 (=> (forall @t560 (_ @t553 tptp.nil_com)) (=> (forall @t559 (_ @t558 @t548)) (=> (forall @t557 @t556) (_ (_ @t544 @t497) @t543))))))) % 0.85/1.10 (assume @p161 (forall @t569 (=> @t568 (=> (forall @t566 (=> (_ (_ @t544 @t545) @t549) @t565)) @t564)))) % 0.85/1.10 (assume @p162 (forall @t576 (=> @t536 (=> @t575 (=> (forall (@list @t550 @t546 @t571) (=> (_ @t533 @t571) (=> (_ @t533 @t572) (_ @t533 (_ @t551 @t572))))) @t570))))) % 0.85/1.10 (assume @p163 (forall @t569 (=> @t568 (=> (forall @t577 (_ @t555 tptp.nil_com)) (=> (forall @t557 (=> (_ @t555 @t548) (=> @t565 @t554))) @t564))))) % 0.85/1.10 (assume @p164 (forall (@list @t579) (=> (not (= @t579 tptp.nil_list_com)) (=> (forall (@list @t578) (not (= @t579 (_ @t580 @t578)))) (not (forall (@list @t550 @t549 @t578) (not (= @t579 (_ (_ tptp.cons_list_com @t552) @t578))))))))) % 0.85/1.10 (assume @p165 (forall (@list @t583) (=> (not (= @t583 tptp.nil_com)) (=> (forall @t574 (not (= @t583 @t573))) (not (forall @t584 (not (= @t583 @t582)))))))) % 0.85/1.10 (assume @p166 (forall @t594 (=> @t593 (=> (forall @t591 (=> (_ @t590 @t545) (_ @t590 @t588))) @t587)))) % 0.85/1.10 (assume @p167 (forall (@list @t533 @t563) (=> @t536 (=> @t575 (=> (forall @t584 (=> (=> @t595 @t596) (=> (=> (not @t595) (_ @t533 @t581)) (_ @t533 @t582)))) (_ @t533 @t563)))))) % 0.85/1.10 (assume @p168 (forall @t594 (=> @t593 (=> (forall @t598 (_ @t590 @t573)) (=> (forall @t597 (=> (_ @t590 @t581) (_ @t590 @t582))) @t587))))) % 0.85/1.10 (assume @p169 (forall @t601 (=> @t541 (=> @t575 (=> (forall @t560 (=> @t600 (=> @t599 @t596))) @t570))))) % 0.85/1.10 (assume @p170 (forall (@list @t603 @t602 @t562 @t462) (=> (forall (@list @t607 @t567) (_ (_ @t608 tptp.nil_com) @t567)) (=> (forall (@list @t607 @t606 @t605 @t604) (=> (_ (_ @t608 @t605) (_ (_ tptp.cons_com (_ @t607 @t606)) @t604)) (_ (_ @t608 (_ (_ tptp.cons_com @t606) @t605)) @t604))) (_ (_ (_ @t603 @t602) @t562) @t462))))) % 0.85/1.10 (assume @p171 (forall @t614 (=> @t613 (not (forall @t566 (not (= @t610 (_ @t609 @t545)))))))) % 0.85/1.10 (assume @p172 (forall @t614 (=> @t613 (=> (forall @t577 (not (= @t610 (_ @t615 tptp.nil_com)))) (not (forall @t557 (not (= @t610 (_ @t609 @t548))))))))) % 0.85/1.10 (assume @p173 (forall @t619 (=> @t618 (not (forall @t591 (not (= @t617 (_ @t616 @t588)))))))) % 0.85/1.10 (assume @p174 (forall @t619 (=> @t618 (=> (forall @t598 (not (= @t617 (_ @t616 @t573)))) (not (forall @t597 (not (= @t617 (_ @t616 @t582))))))))) % 0.85/1.10 (assume @p175 (forall (@list @t5 @t40 @t1 @t399) (=> (_ @t423 @t1) (_ (_ tptp.member1069318160_state (_ @t620 (_ @t402 @t1))) @t42)))) % 0.85/1.10 (assume @p176 (forall @t491 (not (forall @t624 (not (= @t174 @t623)))))) % 0.85/1.10 (assume @p177 (forall @t493 (not (forall @t626 (not (= @t492 @t625)))))) % 0.85/1.10 (assume @p178 (forall @t493 (not (forall @t630 (not (= @t492 @t629)))))) % 0.85/1.10 (assume @p179 (forall (@list @t243 @t178) (=> (forall @t624 (_ @t243 @t623)) (_ @t243 @t178)))) % 0.85/1.10 (assume @p180 (forall @t633 (=> (forall @t626 (_ @t389 @t625)) @t632))) % 0.85/1.10 (assume @p181 (forall @t633 (=> (forall @t630 (_ @t389 @t629)) @t632))) % 0.85/1.10 (assume @p182 (forall @t409 (=> @t634 @t406))) % 0.85/1.10 (assume @p183 (forall (@list @t638 @t636 @t399 @t5 @t2 @t1) (=> (_ (_ tptp.member1069318160_state (_ @t642 @t4)) tptp.pHoare259243666_exec1) (not (=> (= @t2 @t640) (not @t635)))))) % 0.85/1.10 (assume @p184 (forall (@list @t638 @t636 @t399 @t5) (_ (_ tptp.member1069318160_state (_ @t642 (_ (_ tptp.produc1204172211_state @t640) @t5))) tptp.pHoare259243666_exec1))) % 0.85/1.10 (assume @p185 (forall @t504 (and (=> @t527 (= @t643 @t644)) (=> @t528 (= @t643 tptp.nil_list_com))))) % 0.85/1.10 (assume @p186 (forall (@list @t645 @t399 @t5 @t2 @t1) (=> (_ (_ tptp.member1069318160_state (_ @t649 @t4)) tptp.pHoare259243666_exec1) (not (=> @t647 (not (_ (_ tptp.member_state @t1) @t646))))))) % 0.85/1.10 (assume @p187 (forall (@list @t398 @t645 @t5 @t399) (=> @t650 (_ (_ tptp.member1069318160_state (_ @t649 (_ @t402 @t398))) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p188 (forall @t542 (= (_ (_ tptp.n_lists_com tptp.zero_zero_nat) @t497) @t644))) % 0.85/1.10 (assume @p189 (forall (@list @t638 @t651 @t636) (=> (_ @t656 @t651) (=> (forall (@list @t652) (=> (_ @t655 @t652) (_ @t653 @t652))) (_ (_ tptp.termi @t641) @t651))))) % 0.85/1.10 (assume @p190 (forall (@list @t419 @t658 @t418 @t657) (= (= @t659 (_ (_ tptp.semi @t418) @t657)) (and @t420 (= @t658 @t657))))) % 0.85/1.10 (assume @p191 (forall (@list @t661 @t660) (= (= @t662 (_ tptp.do @t660)) (= @t661 @t660)))) % 0.85/1.10 (assume @p192 (forall (@list @t661 @t419 @t658) (not (= @t662 @t659)))) % 0.85/1.10 (assume @p193 (forall (@list @t398 @t645 @t5) (=> @t650 (_ (_ @t422 @t648) @t398)))) % 0.85/1.10 (assume @p194 (forall (@list @t651 @t638 @t664 @t636 @t663) (=> (_ @t655 @t664) (=> (_ (_ (_ tptp.exec @t664) @t636) @t663) (_ (_ @t654 @t641) @t663))))) % 0.85/1.10 (assume @p195 (= (_ tptp.product_lists_com tptp.nil_list_com) @t644)) % 0.85/1.10 (assume @p196 (= (_ tptp.subseqs_com tptp.nil_com) @t644)) % 0.85/1.10 (assume @p197 (forall (@list @t665 @t638 @t636 @t399 @t5 @t2 @t1) (=> (_ (_ tptp.member1069318160_state (_ @t672 @t4)) tptp.pHoare259243666_exec1) (=> (=> (= @t2 @t670) @t669) (not (=> (= @t2 @t637) @t667)))))) % 0.85/1.10 (assume @p198 (forall (@list @t678 @t676 @t674 @t677 @t675 @t673) (= (= @t679 (_ (_ (_ tptp.cond @t677) @t675) @t673)) (and (= @t678 @t677) (= @t676 @t675) (= @t674 @t673))))) % 0.85/1.10 (assume @p199 (forall (@list @t665 @t5 @t638 @t398 @t636) (=> @t666 (=> (_ (_ @t422 @t638) @t398) @t680)))) % 0.85/1.10 (assume @p200 (forall (@list @t665 @t5 @t636 @t398 @t638) (=> @t668 (=> (_ (_ @t422 @t636) @t398) @t680)))) % 0.85/1.10 (assume @p201 (forall (@list @t665 @t5 @t638 @t636) (=> @t666 (=> (_ @t656 @t5) @t681)))) % 0.85/1.10 (assume @p202 (forall (@list @t665 @t5 @t636 @t638) (=> @t668 (=> (_ @t653 @t5) @t681)))) % 0.85/1.10 (assume @p203 (forall (@list @t661 @t678 @t676 @t674) (not (= @t662 @t679)))) % 0.85/1.10 (assume @p204 (forall (@list @t419 @t658 @t678 @t676 @t674) (not (= @t659 @t679)))) % 0.85/1.10 (assume @p205 (forall @t682 (=> @t668 (_ (_ tptp.member1069318160_state (_ @t672 (_ (_ tptp.produc1204172211_state @t637) @t5))) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p206 (forall @t682 (=> @t666 (_ (_ tptp.member1069318160_state (_ @t672 (_ (_ tptp.produc1204172211_state @t670) @t5))) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p207 (forall (@list @t502 @t498 @t497) (= (_ @t683 @t500) (_ (_ tptp.gen_length_com @t503) @t497)))) % 0.85/1.10 (assume @p208 (forall (@list @t498) (= (_ (_ tptp.insert_com @t498) tptp.nil_com) @t684))) % 0.85/1.10 (assume @p209 (forall @t688 (=> @t668 (_ (_ tptp.member1069318160_state (_ @t687 @t403)) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p210 (forall (@list @t692 @t690 @t691 @t689) (= (= @t693 (_ (_ tptp.while @t691) @t689)) (and (= @t692 @t691) (= @t690 @t689))))) % 0.85/1.10 (assume @p211 (forall (@list @t678 @t676 @t674 @t692 @t690) (not (= @t679 @t693)))) % 0.85/1.10 (assume @p212 (forall (@list @t665 @t40 @t5) (=> @t695 (=> @t666 @t41)))) % 0.85/1.10 (assume @p213 (forall @t697 (=> @t668 (_ @t696 @t5)))) % 0.85/1.10 (assume @p214 (forall (@list @t665 @t5 @t40 @t398 @t453) (=> @t666 (=> @t424 (=> (_ (_ (_ tptp.exec @t398) @t685) @t453) (_ @t696 @t453)))))) % 0.85/1.10 (assume @p215 (forall @t697 (=> @t668 @t695))) % 0.85/1.10 (assume @p216 (forall (@list @t661 @t692 @t690) (not (= @t662 @t693)))) % 0.85/1.10 (assume @p217 (forall (@list @t419 @t658 @t692 @t690) (not (= @t659 @t693)))) % 0.85/1.10 (assume @p218 (forall @t697 (=> @t666 (=> @t41 (=> (forall @t506 (=> @t505 (_ @t694 @t457))) @t695))))) % 0.85/1.10 (assume @p219 (forall (@list @t665 @t40 @t5 @t398) (=> @t695 (=> @t666 (=> @t424 (_ @t694 @t398)))))) % 0.85/1.10 (assume @p220 (forall @t504 (= (_ @t683 tptp.nil_com) @t502))) % 0.85/1.10 (assume @p221 (forall (@list @t665 @t40 @t698 @t520) (=> (_ @t694 @t702) (=> @t701 @t700)))) % 0.85/1.10 (assume @p222 (forall (@list @t703 @t704 @t698 @t520 @t665 @t40) (=> (_ (_ tptp.termi @t703) @t704) (=> (and (= @t704 @t702) (= @t703 @t685) @t701) @t700)))) % 0.85/1.10 (assume @p223 (forall (@list @t665 @t40 @t399 @t5 @t2 @t1) (=> (_ (_ tptp.member1069318160_state (_ @t687 @t4)) tptp.pHoare259243666_exec1) (=> (=> @t647 @t667) (not (=> (= @t2 @t705) @t669)))))) % 0.85/1.10 (assume @p224 (forall @t688 (=> @t666 (_ (_ tptp.member1069318160_state (_ @t687 (_ (_ tptp.produc1204172211_state @t705) @t5))) tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p225 (forall (@list @t706 @t498) (and (=> @t708 (= @t707 @t684)) (=> (not @t708) (= @t707 tptp.nil_com))))) % 0.85/1.10 (assume @p226 (forall @t711 (=> @t408 (_ @t710 @t42)))) % 0.85/1.10 (assume @p227 (forall @t719 (=> @t718 (=> (=> @t717 (not @t463)) (not (forall @t584 (=> (= @t562 @t552) (forall @t612 (=> (= @t462 @t548) (=> @t716 (not @t714))))))))))) % 0.85/1.10 (assume @p228 (forall @t734 (=> @t733 (=> (=> @t732 (not @t731)) (not (forall (@list @t484 @t483 @t723) (=> (= @t730 @t729) (forall (@list @t722) (=> (= @t728 @t727) (=> @t726 (not @t725))))))))))) % 0.85/1.10 (assume @p229 (forall @t749 (=> @t748 (=> (=> @t747 (not @t746)) (not (forall (@list @t351 @t232 @t737) (=> (= @t745 @t744) (forall (@list @t736) (=> (= @t742 @t741) (=> @t357 (not @t739))))))))))) % 0.85/1.10 (assume @p230 (forall @t764 (=> @t763 (=> (=> @t762 (not @t761)) (not (forall (@list @t360 @t245 @t752) (=> (= @t760 @t759) (forall (@list @t751) (=> (= @t757 @t756) (=> @t366 (not @t754))))))))))) % 0.85/1.10 (assume @p231 (forall @t770 (= (= @t769 @t768) @t766))) % 0.85/1.10 (assume @p232 (forall (@list @t543 @t497 @t765) (= (= (_ @t772 @t497) (_ @t771 @t497)) @t766))) % 0.85/1.10 (assume @p233 (forall @t770 (= (_ (_ tptp.append_com @t769) @t765) (_ @t767 @t773)))) % 0.85/1.10 (assume @p234 (forall (@list @t429 @t775 @t774) (= (_ (_ tptp.append_com (_ @t776 @t775)) @t774) (_ @t776 (_ (_ tptp.append_com @t775) @t774))))) % 0.85/1.10 (assume @p235 (forall @t542 (= (_ @t767 tptp.nil_com) @t497))) % 0.85/1.10 (assume @p236 (forall @t778 (= (= @t769 @t497) @t777))) % 0.85/1.10 (assume @p237 (forall @t778 (= (= @t497 @t769) @t777))) % 0.85/1.10 (assume @p238 (forall @t778 (= (= @t769 @t543) @t540))) % 0.85/1.10 (assume @p239 (forall (@list @t543 @t497) (= (= @t543 @t769) @t540))) % 0.85/1.10 (assume @p240 (forall @t778 (= (= tptp.nil_com @t769) @t779))) % 0.85/1.10 (assume @p241 (forall @t778 (= (= @t769 tptp.nil_com) @t779))) % 0.85/1.10 (assume @p242 (forall @t780 (= (_ @t776 tptp.nil_com) @t429))) % 0.85/1.10 (assume @p243 (forall (@list @t706) (= (_ (_ tptp.nths_com tptp.nil_com) @t706) tptp.nil_com))) % 0.85/1.10 (assume @p244 (forall (@list @t497 @t498 @t543 @t781) (= (= @t786 @t785) (and @t783 @t782)))) % 0.85/1.10 (assume @p245 (forall (@list @t788 @t22) (_ @t790 @t787))) % 0.85/1.10 (assume @p246 (forall (@list @t792 @t7) (_ @t794 @t791))) % 0.85/1.10 (assume @p247 (forall (@list @t497 @t543 @t765 @t795) (= (= @t769 (_ @t771 @t795)) (exists (@list @t796) (or (and (= @t497 (_ @t771 @t796)) (= (_ @t797 @t543) @t795)) (and (= (_ @t767 @t796) @t765) (= @t543 (_ @t797 @t795)))))))) % 0.85/1.10 (assume @p248 (forall (@list @t497 @t799 @t765 @t543 @t798) (=> (= (_ @t767 @t799) @t765) (=> (= @t543 (_ @t800 @t798)) (= @t769 (_ @t771 @t798)))))) % 0.85/1.10 (assume @p249 (forall @t778 (=> @t783 (= @t497 @t802)))) % 0.85/1.10 (assume @p250 (forall (@list @t543) (= @t802 @t543))) % 0.85/1.10 (assume @p251 (forall @t780 (= (_ @t801 @t429) @t429))) % 0.85/1.10 (assume @p252 (forall (@list @t498 @t799 @t543 @t497 @t765) (=> (= (_ @t499 @t799) @t543) (=> (= @t497 (_ @t800 @t765)) @t803)))) % 0.85/1.10 (assume @p253 (forall (@list @t498 @t497 @t543) (= (_ (_ tptp.append_com @t500) @t543) (_ @t499 @t769)))) % 0.85/1.10 (assume @p254 (forall @t601 (=> @t541 (=> @t575 (=> (forall @t560 (=> @t600 @t805)) @t570))))) % 0.85/1.10 (assume @p255 (forall (@list @t543 @t765 @t498 @t497) (= (= @t773 @t500) (or (and @t777 (= @t765 @t500)) (exists @t809 (and (= @t543 @t808) (= @t807 @t497))))))) % 0.85/1.10 (assume @p256 (forall (@list @t498 @t497 @t543 @t765) (= @t803 (or (and @t777 (= @t500 @t765)) (exists @t809 (and (= @t808 @t543) (= @t497 @t807))))))) % 0.85/1.10 (assume @p257 (forall @t542 (=> @t541 (not (forall (@list @t545 @t546) (not (= @t497 (_ (_ tptp.append_com @t545) (_ @t547 tptp.nil_com))))))))) % 0.85/1.10 (assume @p258 (forall @t576 (=> @t536 (=> (forall @t560 @t805) @t570)))) % 0.85/1.10 (assume @p259 (forall (@list @t712) (_ (_ tptp.member32358020st_com (_ @t611 tptp.nil_com)) @t713))) % 0.85/1.10 (assume @p260 (forall @t811 (=> (_ @t810 @t713) @t540))) % 0.85/1.10 (assume @p261 (forall @t811 (=> (_ @t813 @t713) @t540))) % 0.85/1.10 (assume @p262 (forall (@list @t788 @t815 @t22 @t814) (=> @t818 (=> (_ (_ tptp.member1267359376_state (_ @t816 @t814)) @t787) (_ (_ tptp.member1267359376_state (_ @t789 @t814)) @t787))))) % 0.85/1.10 (assume @p263 (forall (@list @t792 @t820 @t7 @t819) (=> @t823 (=> (_ (_ tptp.member423306384_state (_ @t821 @t819)) @t791) (_ (_ tptp.member423306384_state (_ @t793 @t819)) @t791))))) % 0.85/1.10 (assume @p264 (forall @t711 (=> @t634 (_ @t710 tptp.pHoare259243666_exec1)))) % 0.85/1.10 (assume @p265 (forall @t827 (=> (_ @t826 @t713) (not (forall @t560 (=> (= @t497 @t552) (=> @t824 (not (_ (_ tptp.member32358020st_com (_ @t615 @t543)) @t713))))))))) % 0.85/1.10 (assume @p266 (forall (@list @t830 @t829 @t828 @t720) (=> (_ (_ tptp.member1442949316_state (_ @t832 @t831)) @t721) (not (forall (@list @t484 @t723) (=> (= @t830 @t729) (=> (_ (_ tptp.member64234660_state (_ @t485 @t829)) @t720) (not (_ (_ tptp.member1442949316_state (_ @t724 @t828)) @t721))))))))) % 0.85/1.10 (assume @p267 (forall @t837 (=> (_ @t836 @t735) (not (forall (@list @t351 @t737) (=> (= @t788 @t744) (=> @t833 (not (_ (_ tptp.member1267359376_state (_ @t738 @t815)) @t735))))))))) % 0.85/1.10 (assume @p268 (forall @t842 (=> (_ @t841 @t750) (not (forall (@list @t360 @t752) (=> (= @t792 @t759) (=> @t838 (not (_ (_ tptp.member423306384_state (_ @t753 @t820)) @t750))))))))) % 0.85/1.10 (assume @p269 (forall (@list @t781 @t543 @t497 @t712) (=> (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t825) @t497)) @t713) (not (forall @t559 (=> (= @t497 @t548) (=> (_ (_ tptp.member1333916004om_com (_ (_ tptp.product_Pair_com_com @t781) @t546)) @t712) (not (_ (_ tptp.member32358020st_com (_ @t843 @t545)) @t713))))))))) % 0.85/1.10 (assume @p270 (forall (@list @t532 @t844 @t845 @t720) (=> (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state (_ (_ tptp.cons_list_com @t532) @t844)) @t845)) @t721) (not (forall (@list @t483 @t722) (=> (= @t845 @t727) (=> (_ (_ tptp.member64234660_state (_ (_ tptp.produc1204172211_state @t532) @t483)) @t720) (not (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state @t844) @t722)) @t721))))))))) % 0.85/1.10 (assume @p271 (forall (@list @t162 @t815 @t788 @t22) (=> (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t835) @t788)) @t735) (not (forall (@list @t232 @t736) (=> (= @t788 @t741) (=> (_ (_ tptp.member1069318160_state (_ @t302 @t232)) @t22) (not (_ (_ tptp.member1267359376_state (_ @t816 @t736)) @t735))))))))) % 0.85/1.10 (assume @p272 (forall (@list @t174 @t820 @t792 @t7) (=> (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t840) @t792)) @t750) (not (forall (@list @t245 @t751) (=> (= @t792 @t756) (=> (_ (_ tptp.member512523024_state (_ @t307 @t245)) @t7) (not (_ (_ tptp.member423306384_state (_ @t821 @t751)) @t750))))))))) % 0.85/1.10 (assume @p273 (forall @t852 (=> @t851 (=> (_ @t848 @t713) (_ @t847 @t713))))) % 0.85/1.10 (assume @p274 (forall (@list @t583 @t829 @t720 @t830 @t828) (=> (_ (_ tptp.member64234660_state (_ (_ tptp.produc1204172211_state @t583) @t829)) @t720) (=> (_ (_ tptp.member1442949316_state (_ @t832 @t828)) @t721) (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state @t853) @t831)) @t721))))) % 0.85/1.10 (assume @p275 (forall @t857 (=> @t369 (=> (_ @t817 @t735) (_ @t856 @t735))))) % 0.85/1.10 (assume @p276 (forall @t861 (=> @t372 (=> (_ @t822 @t750) (_ @t860 @t750))))) % 0.85/1.10 (assume @p277 (forall (@list @t867 @t5 @t2 @t398) (=> (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t867) @t5)) @t868)) tptp.pHoare259243666_exec1) (forall (@list @t866 @t862) (=> (= @t867 (_ (_ tptp.cons_com @t866) @t862)) (exists @t865 (= @t2 (_ @t864 @t862)))))))) % 0.85/1.10 (assume @p278 (forall (@list @t40 @t399 @t5 @t2 @t398) (=> (_ (_ tptp.member1069318160_state (_ @t620 @t868)) tptp.pHoare259243666_exec1) (exists @t865 (= @t2 (_ @t864 @t399)))))) % 0.85/1.10 (assume @p279 (forall (@list @t873 @t5 @t872 @t1) (=> (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t873) @t5)) (_ (_ tptp.produc1204172211_state @t872) @t1))) tptp.pHoare259243666_exec1) (forall (@list @t870 @t871 @t869) (=> (and (= @t873 (_ (_ tptp.append_com @t870) @t871)) (= @t872 (_ (_ tptp.append_com @t869) @t871)) (not (= @t870 tptp.nil_com))) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t870) @t5)) (_ (_ tptp.produc1204172211_state @t869) @t1))) tptp.pHoare259243666_exec1)))))) % 0.85/1.10 (assume @p280 (forall (@list @t875 @t709 @t5 @t874 @t1) (=> (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state (_ (_ tptp.append_com @t875) @t709)) @t5)) (_ (_ tptp.produc1204172211_state (_ (_ tptp.append_com @t874) @t709)) @t1))) tptp.pHoare259243666_exec1) (=> (not (= @t875 tptp.nil_com)) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state (_ (_ tptp.produc1204172211_state @t875) @t5)) (_ (_ tptp.produc1204172211_state @t874) @t1))) tptp.pHoare259243666_exec1))))) % 0.85/1.10 (assume @p281 (forall (@list @t448 @t474 @t712 @t544) (=> (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t448) @t474)) @t713) (=> @t561 (=> (forall (@list @t550 @t546 @t549 @t545) (=> @t716 (=> @t714 @t556))) (_ (_ @t544 @t448) @t474)))))) % 0.85/1.10 (assume @p282 (forall (@list @t877 @t876 @t720 @t878) (=> (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state @t877) @t876)) @t721) (=> (_ (_ @t878 tptp.nil_list_com) tptp.nil_state) (=> (forall (@list @t484 @t483 @t723 @t722) (=> @t726 (=> @t725 (=> (_ (_ @t878 @t723) @t722) (_ (_ @t878 @t729) @t727))))) (_ (_ @t878 @t877) @t876)))))) % 0.85/1.10 (assume @p283 (forall (@list @t880 @t879 @t22 @t881) (=> (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t880) @t879)) @t735) (=> (_ (_ @t881 tptp.nil_Pr1844458753_state) tptp.nil_Pr1844458753_state) (=> (forall (@list @t351 @t232 @t737 @t736) (=> @t357 (=> @t739 (=> (_ (_ @t881 @t737) @t736) (_ (_ @t881 @t744) @t741))))) (_ (_ @t881 @t880) @t879)))))) % 0.85/1.10 (assume @p284 (forall (@list @t883 @t882 @t7 @t884) (=> (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t883) @t882)) @t750) (=> (_ (_ @t884 tptp.nil_Pr1347322605_state) tptp.nil_Pr1347322605_state) (=> (forall (@list @t360 @t245 @t752 @t751) (=> @t366 (=> @t754 (=> (_ (_ @t884 @t752) @t751) (_ (_ @t884 @t759) @t756))))) (_ (_ @t884 @t883) @t882)))))) % 0.85/1.10 (assume @p285 (forall @t719 (= @t718 (or (and @t717 @t463) (exists (@list @t886 @t538 @t885 @t537) (and (= @t562 (_ (_ tptp.cons_com @t886) @t885)) (= @t462 @t539) (_ (_ tptp.member1333916004om_com (_ (_ tptp.product_Pair_com_com @t886) @t538)) @t712) (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t885) @t537)) @t713))))))) % 0.85/1.10 (assume @p286 (forall @t734 (= @t733 (or (and @t732 @t731) (exists (@list @t890 @t889 @t888 @t887) (and (= @t730 (_ (_ tptp.cons_list_com @t890) @t888)) (= @t728 (_ (_ tptp.cons_state @t889) @t887)) (_ (_ tptp.member64234660_state (_ (_ tptp.produc1204172211_state @t890) @t889)) @t720) (_ (_ tptp.member1442949316_state (_ (_ tptp.produc1742567891_state @t888) @t887)) @t721))))))) % 0.85/1.10 (assume @p287 (forall @t749 (= @t748 (or (and @t747 @t746) (exists (@list @t894 @t893 @t892 @t891) (and (= @t745 (_ (_ tptp.cons_P465369265_state @t894) @t892)) (= @t742 (_ (_ tptp.cons_P465369265_state @t893) @t891)) (_ (_ tptp.member1069318160_state (_ (_ tptp.produc1909270103_state @t894) @t893)) @t22) (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t892) @t891)) @t735))))))) % 0.85/1.10 (assume @p288 (forall @t764 (= @t763 (or (and @t762 @t761) (exists (@list @t391 @t897 @t896 @t895) (and (= @t760 (_ (_ tptp.cons_P438230685_state @t391) @t896)) (= @t757 (_ (_ tptp.cons_P438230685_state @t897) @t895)) (_ (_ tptp.member512523024_state (_ (_ tptp.produc2065881943_state @t391) @t897)) @t7) (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t896) @t895)) @t750))))))) % 0.85/1.10 (assume @p289 (forall (@list @t498 @t497 @t898) (= (_ (_ tptp.bind_com_com @t500) @t898) (_ @t899 (_ (_ tptp.bind_com_com @t497) @t898))))) % 0.85/1.10 (assume @p290 (forall (@list @t497 @t498 @t543 @t781 @t712) (= (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t786) @t785)) @t900) (or (and @t901 @t782) (and @t783 @t851))))) % 0.85/1.10 (assume @p291 (forall (@list @t788 @t166 @t815 @t162 @t22) (= (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state (_ (_ tptp.append982487830_state @t788) (_ @t854 tptp.nil_Pr1844458753_state))) (_ (_ tptp.append982487830_state @t815) (_ @t834 tptp.nil_Pr1844458753_state)))) @t903) (or (and @t904 @t200) (and @t902 @t369))))) % 0.85/1.10 (assume @p292 (forall (@list @t792 @t178 @t820 @t174 @t7) (= (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state (_ (_ tptp.append221843330_state @t792) (_ @t858 tptp.nil_Pr1347322605_state))) (_ (_ tptp.append221843330_state @t820) (_ @t839 tptp.nil_Pr1347322605_state)))) @t906) (or (and @t907 @t202) (and @t905 @t372))))) % 0.85/1.10 (assume @p293 (forall (@list @t898 @t498 @t497) (= (_ @t908 @t500) (_ @t899 (_ @t908 @t497))))) % 0.85/1.10 (assume @p294 (forall @t909 (= (_ (_ tptp.bind_com_com tptp.nil_com) @t898) tptp.nil_com))) % 0.85/1.10 (assume @p295 (forall (@list @t498 @t497 @t781 @t543 @t712) (= (_ @t847 @t900) (or (and @t851 @t783) (and @t782 @t901))))) % 0.85/1.10 (assume @p296 (forall (@list @t166 @t788 @t162 @t815 @t22) (= (_ @t856 @t903) (or (and @t369 @t902) (and @t200 @t904))))) % 0.85/1.10 (assume @p297 (forall (@list @t178 @t792 @t174 @t820 @t7) (= (_ @t860 @t906) (or (and @t372 @t905) (and @t202 @t907))))) % 0.85/1.10 (assume @p298 (forall @t913 (=> @t912 (_ @t911 @t910)))) % 0.85/1.10 (assume @p299 (forall @t913 (=> @t901 (_ @t911 @t900)))) % 0.85/1.10 (assume @p300 (forall @t811 (not (_ @t813 @t900)))) % 0.85/1.10 (assume @p301 (forall @t811 (not (_ @t810 @t900)))) % 0.85/1.10 (assume @p302 (forall (@list @t497 @t543 @t712 @t798 @t914) (=> (or (and @t901 (= @t798 @t914)) (and @t783 (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t798) @t914)) @t900))) (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com (_ @t767 @t798)) (_ @t772 @t914))) @t900)))) % 0.85/1.10 (assume @p303 (forall @t212 (= @t787 @t915))) % 0.85/1.10 (assume @p304 (forall @t213 (= @t791 @t916))) % 0.85/1.10 (assume @p305 (forall @t909 (= (_ @t908 tptp.nil_com) tptp.nil_com))) % 0.85/1.10 (assume @p306 (forall (@list @t498 @t781 @t712 @t497) (=> @t851 (_ (_ tptp.member32358020st_com (_ @t846 (_ @t784 @t497))) @t900)))) % 0.85/1.10 (assume @p307 (forall (@list @t166 @t162 @t22 @t788) (=> @t369 (_ (_ tptp.member1267359376_state (_ @t855 (_ @t834 @t788))) @t903)))) % 0.85/1.10 (assume @p308 (forall (@list @t178 @t174 @t7 @t792) (=> @t372 (_ (_ tptp.member423306384_state (_ @t859 (_ @t839 @t792))) @t906)))) % 0.85/1.10 (assume @p309 (forall (@list @t498 @t497 @t543 @t712) (=> (_ (_ tptp.member32358020st_com (_ @t846 @t543)) @t900) (=> (forall (@list @t546) (=> (= @t543 (_ @t547 @t497)) (not (_ (_ tptp.member1333916004om_com (_ @t849 @t546)) @t712)))) (not (forall @t917 (=> (= @t543 (_ @t499 @t571)) (not (_ (_ tptp.member32358020st_com (_ @t812 @t571)) @t900))))))))) % 0.85/1.10 (assume @p310 (forall (@list @t166 @t788 @t815 @t22) (=> (_ (_ tptp.member1267359376_state (_ @t855 @t815)) @t903) (=> (forall @t259 (=> (= @t815 (_ @t740 @t788)) (not @t258))) (not (forall @t919 (=> (= @t815 (_ @t854 @t918)) (not (_ (_ tptp.member1267359376_state (_ @t789 @t918)) @t903))))))))) % 0.85/1.10 (assume @p311 (forall (@list @t178 @t792 @t820 @t7) (=> (_ (_ tptp.member423306384_state (_ @t859 @t820)) @t906) (=> (forall @t267 (=> (= @t820 (_ @t755 @t792)) (not @t266))) (not (forall @t921 (=> (= @t820 (_ @t858 @t920)) (not (_ (_ tptp.member423306384_state (_ @t793 @t920)) @t906))))))))) % 0.85/1.10 (assume @p312 (forall @t827 (=> (_ @t826 @t900) (=> (forall @t574 (=> (= @t497 (_ @t551 @t543)) (not @t824))) (not (forall @t917 (=> (= @t497 (_ @t784 @t571)) (not (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t571) @t543)) @t900))))))))) % 0.85/1.10 (assume @p313 (forall @t837 (=> (_ @t836 @t903) (=> (forall @t371 (=> (= @t788 (_ @t743 @t815)) (not @t833))) (not (forall @t919 (=> (= @t788 (_ @t834 @t918)) (not (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t918) @t815)) @t903))))))))) % 0.85/1.10 (assume @p314 (forall @t842 (=> (_ @t841 @t906) (=> (forall @t374 (=> (= @t792 (_ @t758 @t820)) (not @t838))) (not (forall @t921 (=> (= @t792 (_ @t839 @t920)) (not (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t920) @t820)) @t906))))))))) % 0.85/1.10 (assume @p315 (forall @t922 (=> @t904 @t818))) % 0.85/1.10 (assume @p316 (forall @t923 (=> @t907 @t823))) % 0.85/1.10 (assume @p317 (forall (@list @t498 @t781 @t712 @t497 @t798 @t914 @t543) (=> @t851 (=> (= @t497 (_ @t924 (_ @t499 @t914))) (=> (= @t543 (_ @t924 (_ @t784 @t914))) @t901))))) % 0.85/1.10 (assume @p318 (forall (@list @t166 @t162 @t22 @t788 @t926 @t925 @t815) (=> @t369 (=> (= @t788 (_ @t927 (_ @t854 @t925))) (=> (= @t815 (_ @t927 (_ @t834 @t925))) @t904))))) % 0.85/1.10 (assume @p319 (forall (@list @t178 @t174 @t7 @t792 @t929 @t928 @t820) (=> @t372 (=> (= @t792 (_ @t930 (_ @t858 @t928))) (=> (= @t820 (_ @t930 (_ @t839 @t928))) @t907))))) % 0.85/1.10 (assume @p320 (forall (@list @t497 @t543 @t712) (=> @t901 (not (forall (@list @t550 @t546) (=> @t716 (forall (@list @t932 @t931) (=> (= @t497 (_ @t933 (_ @t551 @t931))) (not (= @t543 (_ @t933 (_ @t547 @t931)))))))))))) % 0.85/1.10 (assume @p321 (forall @t922 (=> @t904 (not (forall @t358 (=> @t357 (forall (@list @t935 @t934) (=> (= @t788 (_ @t936 (_ @t743 @t934))) (not (= @t815 (_ @t936 (_ @t740 @t934)))))))))))) % 0.85/1.10 (assume @p322 (forall @t923 (=> @t907 (not (forall @t367 (=> @t366 (forall (@list @t938 @t937) (=> (= @t792 (_ @t939 (_ @t758 @t937))) (not (= @t820 (_ @t939 (_ @t755 @t937)))))))))))) % 0.85/1.10 (assume @p323 (forall @t852 (=> (_ @t850 (_ tptp.transi863150634cl_com @t712)) (=> @t912 (_ @t847 @t910))))) % 0.85/1.10 (assume @p324 (forall @t857 (=> @t305 (=> (_ @t817 @t915) (_ @t856 @t915))))) % 0.85/1.10 (assume @p325 (forall @t861 (=> @t309 (=> (_ @t822 @t916) (_ @t860 @t916))))) % 0.85/1.10 (assume @p326 (forall @t947 (= @t946 (and (=> @t944 (and @t777 (= @t765 tptp.nil_com))) (=> @t945 (exists (@list @t942 @t885 @t941 @t940) (and (= @t943 (_ (_ tptp.append_list_com @t942) (_ (_ tptp.cons_list_com (_ (_ tptp.append_com @t885) @t941)) @t940))) (= @t543 (_ (_ tptp.append_com (_ tptp.concat_com @t942)) @t885)) (= @t765 (_ (_ tptp.append_com @t941) (_ tptp.concat_com @t940)))))))))) % 0.85/1.10 (assume @p327 (forall (@list @t953 @t949 @t712 @t951 @t583 @t532) (=> @t955 (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com (_ @t952 @t954)) (_ @t952 @t950))) @t948)))) % 0.85/1.10 (assume @p328 (forall (@list @t24 @t35 @t22 @t959 @t961 @t957) (=> @t219 (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state (_ @t960 @t962)) (_ @t960 @t958))) @t956)))) % 0.85/1.10 (assume @p329 (forall (@list @t12 @t31 @t7 @t966 @t968 @t964) (=> @t226 (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state (_ @t967 @t969)) (_ @t967 @t965))) @t963)))) % 0.85/1.10 (assume @p330 (forall (@list @t830 @t844) (= (_ tptp.concat_com (_ (_ tptp.append_list_com @t830) @t844)) (_ (_ tptp.append_com @t970) (_ tptp.concat_com @t844))))) % 0.85/1.10 (assume @p331 (forall (@list @t953 @t583 @t949 @t532 @t712) (= (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t954) @t950)) @t948) (or @t955 (and (= @t953 @t949) (_ (_ tptp.member32358020st_com (_ @t971 @t532)) @t948)))))) % 0.85/1.10 (assume @p332 (forall (@list @t24 @t961 @t35 @t957 @t22) (= (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t962) @t958)) @t956) (or @t219 (and @t186 @t972))))) % 0.85/1.10 (assume @p333 (forall (@list @t12 @t968 @t31 @t964 @t7) (= (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t969) @t965)) @t963) (or @t226 (and @t193 @t973))))) % 0.85/1.10 (assume @p334 (forall (@list @t532 @t712) (= (_ (_ tptp.member32358020st_com (_ @t611 @t532)) @t948) (exists (@list @t974 @t890) (= @t532 (_ (_ tptp.cons_com @t974) @t890)))))) % 0.85/1.10 (assume @p335 (forall (@list @t22 @t961 @t957) (=> (forall @t105 (or @t377 (= @t90 @t89) (_ (_ tptp.member1069318160_state (_ @t275 @t90)) @t22))) (or @t972 (= @t961 @t957) (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t957) @t961)) @t956))))) % 0.85/1.10 (assume @p336 (forall (@list @t7 @t968 @t964) (=> (forall @t78 (or @t378 (= @t62 @t61) (_ (_ tptp.member512523024_state (_ @t288 @t62)) @t7))) (or @t973 (= @t968 @t964) (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t964) @t968)) @t963))))) % 0.85/1.10 (assume @p337 (forall (@list @t22 @t788) (=> (forall @t371 (not (_ @t370 @t22))) (not (_ @t790 @t956))))) % 0.85/1.10 (assume @p338 (forall (@list @t7 @t792) (=> (forall @t374 (not (_ @t373 @t7))) (not (_ @t794 @t963))))) % 0.85/1.10 (assume @p339 (= @t975 tptp.nil_com)) % 0.85/1.10 (assume @p340 (forall (@list @t583 @t712) (not (_ (_ tptp.member32358020st_com (_ @t971 tptp.nil_com)) @t948)))) % 0.85/1.10 (assume @p341 (forall (@list @t583 @t830) (= (_ tptp.concat_com @t853) (_ @t976 @t970)))) % 0.85/1.10 (assume @p342 (forall (@list @t951 @t977 @t712 @t583) (=> @t979 @t978))) % 0.85/1.10 (assume @p343 (forall (@list @t583 @t951 @t977 @t712) (=> @t978 (=> (forall (@list @t606) (not (_ (_ tptp.member1333916004om_com (_ (_ tptp.product_Pair_com_com @t606) @t606)) @t712))) @t979)))) % 0.85/1.10 (assume @p344 (forall (@list @t961 @t959 @t980 @t22) (=> (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state (_ @t981 @t959)) (_ @t981 @t980))) @t956) (=> (forall @t280 (not (_ (_ tptp.member1069318160_state (_ @t94 @t90)) @t22))) (_ (_ tptp.member1267359376_state (_ (_ tptp.produc1298457559_state @t959) @t980)) @t956))))) % 0.85/1.10 (assume @p345 (forall (@list @t968 @t966 @t982 @t7) (=> (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state (_ @t983 @t966)) (_ @t983 @t982))) @t963) (=> (forall @t292 (not (_ (_ tptp.member512523024_state (_ @t67 @t62)) @t7))) (_ (_ tptp.member423306384_state (_ (_ tptp.produc1354769367_state @t966) @t982)) @t963))))) % 0.85/1.10 (assume @p346 (forall (@list @t532 @t583 @t712) (=> (exists (@list @t985 @t984) (= @t532 (_ (_ tptp.cons_com @t985) @t984))) (_ (_ tptp.member32358020st_com (_ @t971 (_ @t976 @t532))) @t948)))) % 0.85/1.10 (assume @p347 (forall @t947 (=> @t946 (=> @t945 (exists (@list @t988 @t549 @t987 @t986) (and (= @t943 (_ (_ tptp.append_list_com @t988) (_ (_ tptp.cons_list_com (_ @t804 @t987)) @t986))) (= @t543 (_ (_ tptp.append_com (_ tptp.concat_com @t988)) @t549)) (= @t765 (_ (_ tptp.append_com @t987) (_ tptp.concat_com @t986))))))))) % 0.85/1.10 (assume @p348 (forall (@list @t712 @t497 @t543 @t765) (=> (_ tptp.irrefl_com @t712) (= (_ (_ tptp.member32358020st_com (_ (_ tptp.produc1307105171st_com @t769) @t768)) @t948) (_ (_ tptp.member32358020st_com (_ @t843 @t765)) @t948))))) % 0.85/1.10 (assume @p349 (_ (_ tptp.termi tptp.c) tptp.s)) % 0.85/1.10 (assume @p350 (= (_ tptp.f tptp.zero_zero_nat) @t990)) % 0.85/1.10 (assume @p351 @t996) % 0.85/1.10 (assume @p352 (_ (_ tptp.member1069318160_state (_ @t998 @t997)) @t42)) % 0.85/1.10 (assume @p353 @t1001) % 0.85/1.10 (assume @p354 true) % 0.85/1.10 (step @p355 (= tptp.pHoare2126160787le_inf @t1004) :rule refl :args (@t1004)) % 0.85/1.10 (step @p356 :rule refl :args ((tptp.member1069318160_state @t260 @t124))) % 0.85/1.10 (step @p357 :rule refl :args (@t1005)) % 0.85/1.10 (step @p358 :rule refl :args (@t1006)) % 0.85/1.10 (step @p359 :rule cong :premises (@p358 @p357) :args (@t1007)) % 0.85/1.10 (step @p360 :rule trans :premises (@p359 @p356)) % 0.85/1.10 (step @p361 :rule refl :args (tptp.member1069318160_state)) % 0.85/1.10 (step @p362 :rule ho_cong :premises (@p361 @p358)) % 0.85/1.10 (step @p363 :rule ho_cong :premises (@p362 @p357)) % 0.85/1.10 (step @p364 :rule cong :premises (@p363 @p360) :args ((= (_ (_ tptp.member1069318160_state @t1006) @t1005) @t1007))) % 0.85/1.10 (step @p365 :rule symm :premises (@p364)) % 0.85/1.10 (step @p366 :rule refl :args (@t375)) % 0.85/1.10 (step @p367 :rule eq_resolve :premises (@p366 @p365)) % 0.85/1.10 (step @p368 :rule refl :args (@t124)) % 0.85/1.10 (step @p369 :rule cong :premises (@p368 @p357) :args ((= @t124 @t1005))) % 0.85/1.10 (step @p370 :rule symm :premises (@p369)) % 0.85/1.10 (step @p371 :rule eq_resolve :premises (@p368 @p370)) % 0.85/1.10 (step @p372 :rule refl :args (@t260)) % 0.85/1.10 (step @p373 :rule cong :premises (@p372 @p358) :args ((= @t260 @t1006))) % 0.85/1.10 (step @p374 :rule symm :premises (@p373)) % 0.85/1.10 (step @p375 :rule eq_resolve :premises (@p372 @p374)) % 0.85/1.10 (step @p376 :rule ho_cong :premises (@p361 @p375)) % 0.85/1.10 (step @p377 :rule ho_cong :premises (@p376 @p371)) % 0.85/1.10 (step @p378 :rule trans :premises (@p377 @p367)) % 0.85/1.10 (step @p379 :rule refl :args ((tptp.member1069318160_state @t303 @t124))) % 0.85/1.10 (step @p380 :rule refl :args (@t1008)) % 0.85/1.10 (step @p381 :rule cong :premises (@p380 @p357) :args (@t1009)) % 0.85/1.10 (step @p382 :rule trans :premises (@p381 @p379)) % 0.85/1.10 (step @p383 :rule ho_cong :premises (@p361 @p380)) % 0.85/1.10 (step @p384 :rule ho_cong :premises (@p383 @p357)) % 0.85/1.10 (step @p385 :rule cong :premises (@p384 @p382) :args ((= (_ (_ tptp.member1069318160_state @t1008) @t1005) @t1009))) % 0.85/1.10 (step @p386 :rule symm :premises (@p385)) % 0.85/1.10 (step @p387 :rule refl :args (@t379)) % 0.85/1.10 (step @p388 :rule eq_resolve :premises (@p387 @p386)) % 0.85/1.10 (step @p389 :rule refl :args (@t303)) % 0.85/1.10 (step @p390 :rule cong :premises (@p389 @p380) :args ((= @t303 @t1008))) % 0.85/1.10 (step @p391 :rule symm :premises (@p390)) % 0.85/1.10 (step @p392 :rule eq_resolve :premises (@p389 @p391)) % 0.85/1.10 (step @p393 :rule ho_cong :premises (@p361 @p392)) % 0.85/1.10 (step @p394 :rule ho_cong :premises (@p393 @p371)) % 0.85/1.10 (step @p395 :rule trans :premises (@p394 @p388)) % 0.85/1.10 (step @p396 :rule cong :premises (@p395) :args (@t1010)) % 0.85/1.10 (step @p397 :rule refl :args ((tptp.member1069318160_state @t170 @t124))) % 0.85/1.10 (step @p398 :rule refl :args (@t1011)) % 0.85/1.10 (step @p399 :rule cong :premises (@p398 @p357) :args (@t1012)) % 0.85/1.10 (step @p400 :rule trans :premises (@p399 @p397)) % 0.85/1.10 (step @p401 :rule ho_cong :premises (@p361 @p398)) % 0.85/1.10 (step @p402 :rule ho_cong :premises (@p401 @p357)) % 0.85/1.10 (step @p403 :rule cong :premises (@p402 @p400) :args ((= (_ (_ tptp.member1069318160_state @t1011) @t1005) @t1012))) % 0.85/1.10 (step @p404 :rule symm :premises (@p403)) % 0.85/1.10 (step @p405 :rule refl :args (@t359)) % 0.85/1.10 (step @p406 :rule eq_resolve :premises (@p405 @p404)) % 0.85/1.10 (step @p407 :rule refl :args (@t170)) % 0.85/1.10 (step @p408 :rule cong :premises (@p407 @p398) :args ((= @t170 @t1011))) % 0.85/1.10 (step @p409 :rule symm :premises (@p408)) % 0.85/1.10 (step @p410 :rule eq_resolve :premises (@p407 @p409)) % 0.85/1.10 (step @p411 :rule ho_cong :premises (@p361 @p410)) % 0.85/1.10 (step @p412 :rule ho_cong :premises (@p411 @p371)) % 0.85/1.10 (step @p413 :rule trans :premises (@p412 @p406)) % 0.85/1.10 (step @p414 :rule cong :premises (@p413) :args (@t1013)) % 0.85/1.10 (step @p415 :rule nary_cong :premises (@p414 @p396 @p378) :args (@t1014)) % 0.85/1.10 (step @p416 :rule cong :premises (@p415) :args ((forall @t306 @t1014))) % 0.85/1.10 (step @p417 :rule aci_norm :args ((= (or @t1013 (or @t1010 @t375)) @t1014))) % 0.85/1.10 (step @p418 :rule bool-impl-elim :args (@t379 @t375)) % 0.85/1.10 (step @p419 :rule refl :args (@t1013)) % 0.85/1.10 (step @p420 :rule nary_cong :premises (@p419 @p418) :args ((or @t1013 @t380))) % 0.85/1.10 (step @p421 :rule trans :premises (@p420 @p417)) % 0.85/1.10 (step @p422 :rule bool-impl-elim :args (@t359 @t380)) % 0.85/1.10 (step @p423 :rule trans :premises (@p422 @p421)) % 0.85/1.10 (step @p424 :rule cong :premises (@p423) :args (@t381)) % 0.85/1.10 (step @p425 :rule trans :premises (@p424 @p416)) % 0.85/1.10 (step @p426 :rule eq_resolve :premises (@p81 @p425)) % 0.85/1.10 (step @p427 :rule refl :args ((tptp.member1069318160_state @t994 @t991))) % 0.85/1.10 (step @p428 :rule refl :args (@t1015)) % 0.85/1.10 (step @p429 :rule refl :args ((tptp.produc1909270103_state @t993 @t992))) % 0.85/1.10 (step @p430 :rule refl :args ((tptp.f @t9))) % 0.85/1.10 (step @p431 :rule refl :args (@t1016)) % 0.85/1.10 (step @p432 :rule cong :premises (@p431) :args (@t1017)) % 0.85/1.10 (step @p433 :rule trans :premises (@p432 @p430)) % 0.85/1.10 (step @p434 :rule refl :args (@t1018)) % 0.85/1.10 (step @p435 :rule cong :premises (@p434 @p433) :args (@t1019)) % 0.85/1.10 (step @p436 :rule trans :premises (@p435 @p429)) % 0.85/1.10 (step @p437 :rule cong :premises (@p436 @p428) :args (@t1020)) % 0.85/1.10 (step @p438 :rule trans :premises (@p437 @p427)) % 0.85/1.10 (step @p439 :rule ho_cong :premises (@p361 @p436)) % 0.85/1.10 (step @p440 :rule ho_cong :premises (@p439 @p428)) % 0.85/1.10 (step @p441 :rule cong :premises (@p440 @p438) :args ((= (_ (_ tptp.member1069318160_state @t1019) @t1015) @t1020))) % 0.85/1.10 (step @p442 :rule symm :premises (@p441)) % 0.85/1.10 (step @p443 :rule refl :args (@t995)) % 0.85/1.10 (step @p444 :rule eq_resolve :premises (@p443 @p442)) % 0.85/1.10 (step @p445 :rule refl :args (@t991)) % 0.85/1.10 (step @p446 :rule cong :premises (@p445 @p428) :args ((= @t991 @t1015))) % 0.85/1.10 (step @p447 :rule symm :premises (@p446)) % 0.85/1.10 (step @p448 :rule eq_resolve :premises (@p445 @p447)) % 0.85/1.10 (step @p449 :rule refl :args (tptp.produc1909270103_state)) % 0.85/1.10 (step @p450 :rule ho_cong :premises (@p449 @p434)) % 0.85/1.10 (step @p451 :rule ho_cong :premises (@p450 @p433)) % 0.85/1.10 (step @p452 :rule cong :premises (@p451 @p436) :args ((= (_ (_ tptp.produc1909270103_state @t1018) @t1017) @t1019))) % 0.85/1.10 (step @p453 :rule symm :premises (@p452)) % 0.85/1.10 (step @p454 :rule refl :args (@t994)) % 0.85/1.10 (step @p455 :rule eq_resolve :premises (@p454 @p453)) % 0.85/1.10 (step @p456 :rule refl :args (tptp.f)) % 0.85/1.10 (step @p457 :rule ho_cong :premises (@p456 @p431)) % 0.85/1.10 (step @p458 :rule cong :premises (@p457 @p433) :args ((= (_ tptp.f @t1016) @t1017))) % 0.85/1.10 (step @p459 :rule symm :premises (@p458)) % 0.85/1.10 (step @p460 :rule refl :args (@t992)) % 0.85/1.10 (step @p461 :rule eq_resolve :premises (@p460 @p459)) % 0.85/1.10 (step @p462 :rule refl :args (@t9)) % 0.85/1.10 (step @p463 :rule cong :premises (@p462 @p431) :args ((= @t9 @t1016))) % 0.85/1.10 (step @p464 :rule symm :premises (@p463)) % 0.85/1.10 (step @p465 :rule eq_resolve :premises (@p462 @p464)) % 0.85/1.10 (step @p466 :rule ho_cong :premises (@p456 @p465)) % 0.85/1.10 (step @p467 :rule trans :premises (@p466 @p461)) % 0.85/1.10 (step @p468 :rule refl :args (@t993)) % 0.85/1.10 (step @p469 :rule cong :premises (@p468 @p434) :args ((= @t993 @t1018))) % 0.85/1.10 (step @p470 :rule symm :premises (@p469)) % 0.85/1.10 (step @p471 :rule eq_resolve :premises (@p468 @p470)) % 0.85/1.10 (step @p472 :rule ho_cong :premises (@p449 @p471)) % 0.85/1.10 (step @p473 :rule ho_cong :premises (@p472 @p467)) % 0.85/1.10 (step @p474 :rule trans :premises (@p473 @p455)) % 0.85/1.10 (step @p475 :rule ho_cong :premises (@p361 @p474)) % 0.85/1.10 (step @p476 :rule ho_cong :premises (@p475 @p448)) % 0.85/1.10 (step @p477 :rule trans :premises (@p476 @p444)) % 0.85/1.10 (step @p478 :rule cong :premises (@p477) :args (@t996)) % 0.85/1.10 (step @p479 :rule eq_resolve :premises (@p351 @p478)) % 0.85/1.10 (step @p480 :rule instantiate :premises (@p479) :args ((@list tptp.n))) % 0.85/1.10 (step @p481 :rule refl :args ((tptp.member1069318160_state @t36 @t53))) % 0.85/1.10 (step @p482 :rule refl :args (@t1021)) % 0.85/1.10 (step @p483 :rule refl :args (@t1022)) % 0.85/1.10 (step @p484 :rule cong :premises (@p483 @p482) :args (@t1023)) % 0.85/1.10 (step @p485 :rule trans :premises (@p484 @p481)) % 0.85/1.10 (step @p486 :rule ho_cong :premises (@p361 @p483)) % 0.85/1.10 (step @p487 :rule ho_cong :premises (@p486 @p482)) % 0.85/1.10 (step @p488 :rule cong :premises (@p487 @p485) :args ((= (_ @t1024 @t1021) @t1023))) % 0.85/1.10 (step @p489 :rule symm :premises (@p488)) % 0.85/1.10 (step @p490 :rule refl :args (@t185)) % 0.85/1.10 (step @p491 :rule eq_resolve :premises (@p490 @p489)) % 0.85/1.10 (step @p492 :rule refl :args (@t53)) % 0.85/1.10 (step @p493 :rule cong :premises (@p492 @p482) :args ((= @t53 @t1021))) % 0.85/1.10 (step @p494 :rule symm :premises (@p493)) % 0.85/1.10 (step @p495 :rule eq_resolve :premises (@p492 @p494)) % 0.85/1.10 (step @p496 :rule refl :args (@t36)) % 0.85/1.10 (step @p497 :rule cong :premises (@p496 @p483) :args ((= @t36 @t1022))) % 0.85/1.10 (step @p498 :rule symm :premises (@p497)) % 0.85/1.10 (step @p499 :rule eq_resolve :premises (@p496 @p498)) % 0.85/1.10 (step @p500 :rule ho_cong :premises (@p361 @p499)) % 0.85/1.10 (step @p501 :rule ho_cong :premises (@p500 @p495)) % 0.85/1.10 (step @p502 :rule trans :premises (@p501 @p491)) % 0.85/1.10 (step @p503 :rule refl :args (@t187)) % 0.85/1.10 (step @p504 :rule nary_cong :premises (@p503 @p502) :args (@t188)) % 0.85/1.10 (step @p505 :rule refl :args (@t186)) % 0.85/1.10 (step @p506 :rule refl :args ((tptp.member1069318160_state @t36 @t50))) % 0.85/1.10 (step @p507 :rule refl :args (@t1025)) % 0.85/1.10 (step @p508 :rule cong :premises (@p483 @p507) :args (@t1026)) % 0.85/1.10 (step @p509 :rule trans :premises (@p508 @p506)) % 0.85/1.10 (step @p510 :rule ho_cong :premises (@p486 @p507)) % 0.85/1.10 (step @p511 :rule cong :premises (@p510 @p509) :args ((= (_ @t1024 @t1025) @t1026))) % 0.85/1.10 (step @p512 :rule symm :premises (@p511)) % 0.85/1.10 (step @p513 :rule refl :args (@t190)) % 0.85/1.10 (step @p514 :rule eq_resolve :premises (@p513 @p512)) % 0.85/1.10 (step @p515 :rule refl :args (@t50)) % 0.85/1.10 (step @p516 :rule cong :premises (@p515 @p507) :args ((= @t50 @t1025))) % 0.85/1.10 (step @p517 :rule symm :premises (@p516)) % 0.85/1.10 (step @p518 :rule eq_resolve :premises (@p515 @p517)) % 0.85/1.10 (step @p519 :rule ho_cong :premises (@p500 @p518)) % 0.85/1.10 (step @p520 :rule trans :premises (@p519 @p514)) % 0.85/1.10 (step @p521 :rule cong :premises (@p520) :args (@t1027)) % 0.85/1.10 (step @p522 :rule nary_cong :premises (@p521 @p505 @p504) :args (@t1028)) % 0.85/1.10 (step @p523 :rule cong :premises (@p522) :args ((forall @t191 @t1028))) % 0.85/1.10 (step @p524 :rule aci_norm :args ((= (or @t1027 @t189) @t1028))) % 0.85/1.10 (step @p525 :rule bool-impl-elim :args (@t190 @t189)) % 0.85/1.10 (step @p526 :rule trans :premises (@p525 @p524)) % 0.85/1.10 (step @p527 :rule cong :premises (@p526) :args (@t192)) % 0.85/1.10 (step @p528 :rule trans :premises (@p527 @p523)) % 0.85/1.10 (step @p529 :rule eq_resolve :premises (@p25 @p528)) % 0.85/1.10 (step @p530 :rule instantiate :premises (@p529) :args ((@list @t1032 @t1029 tptp.pHoare259243666_exec1))) % 0.85/1.10 (step @p531 :rule refl :args ((tptp.member1069318160_state @t36 @t28))) % 0.85/1.10 (step @p532 :rule refl :args (@t1033)) % 0.85/1.10 (step @p533 :rule cong :premises (@p483 @p532) :args (@t1034)) % 0.85/1.10 (step @p534 :rule trans :premises (@p533 @p531)) % 0.85/1.10 (step @p535 :rule ho_cong :premises (@p486 @p532)) % 0.85/1.10 (step @p536 :rule cong :premises (@p535 @p534) :args ((= (_ @t1024 @t1033) @t1034))) % 0.85/1.10 (step @p537 :rule symm :premises (@p536)) % 0.85/1.10 (step @p538 :rule refl :args (@t38)) % 0.85/1.10 (step @p539 :rule eq_resolve :premises (@p538 @p537)) % 0.85/1.10 (step @p540 :rule refl :args (@t28)) % 0.85/1.10 (step @p541 :rule cong :premises (@p540 @p532) :args ((= @t28 @t1033))) % 0.85/1.10 (step @p542 :rule symm :premises (@p541)) % 0.85/1.10 (step @p543 :rule eq_resolve :premises (@p540 @p542)) % 0.85/1.10 (step @p544 :rule ho_cong :premises (@p500 @p543)) % 0.85/1.10 (step @p545 :rule trans :premises (@p544 @p539)) % 0.85/1.10 (step @p546 :rule refl :args ((tptp.member1069318160_state @t36 @t124))) % 0.85/1.10 (step @p547 :rule cong :premises (@p483 @p357) :args (@t1035)) % 0.85/1.10 (step @p548 :rule trans :premises (@p547 @p546)) % 0.85/1.10 (step @p549 :rule ho_cong :premises (@p486 @p357)) % 0.85/1.10 (step @p550 :rule cong :premises (@p549 @p548) :args ((= (_ @t1024 @t1005) @t1035))) % 0.85/1.10 (step @p551 :rule symm :premises (@p550)) % 0.85/1.10 (step @p552 :rule refl :args (@t195)) % 0.85/1.10 (step @p553 :rule eq_resolve :premises (@p552 @p551)) % 0.85/1.10 (step @p554 :rule ho_cong :premises (@p500 @p371)) % 0.85/1.10 (step @p555 :rule trans :premises (@p554 @p553)) % 0.85/1.10 (step @p556 :rule cong :premises (@p555) :args (@t1036)) % 0.85/1.10 (step @p557 :rule nary_cong :premises (@p556 @p545) :args (@t1037)) % 0.85/1.10 (step @p558 :rule cong :premises (@p557) :args ((forall @t196 @t1037))) % 0.85/1.10 (step @p559 :rule bool-impl-elim :args (@t195 @t38)) % 0.85/1.10 (step @p560 :rule cong :premises (@p559) :args (@t197)) % 0.85/1.10 (step @p561 :rule trans :premises (@p560 @p558)) % 0.85/1.10 (step @p562 :rule eq_resolve :premises (@p29 @p561)) % 0.85/1.10 (step @p563 :rule instantiate :premises (@p562) :args ((@list @t1032 @t1039 tptp.pHoare259243666_exec1))) % 0.85/1.10 (step @p564 :rule refl :args ((tptp.member1069318160_state @t1043 @t42))) % 0.85/1.10 (step @p565 :rule refl :args (@t1044)) % 0.85/1.10 (step @p566 :rule refl :args ((tptp.produc1909270103_state @t1041 @t1000))) % 0.85/1.10 (step @p567 :rule refl :args ((tptp.f @t999))) % 0.85/1.10 (step @p568 :rule refl :args (@t1038)) % 0.85/1.10 (step @p569 :rule cong :premises (@p568) :args (@t1039)) % 0.85/1.10 (step @p570 :rule trans :premises (@p569 @p567)) % 0.85/1.10 (step @p571 :rule refl :args ((tptp.produc1204172211_state @t1040 tptp.s))) % 0.85/1.10 (step @p572 :rule refl :args (tptp.s)) % 0.85/1.10 (step @p573 :rule refl :args ((tptp.cons_com tptp.c @t975))) % 0.85/1.10 (step @p574 :rule refl :args (@t1030)) % 0.85/1.10 (step @p575 :rule refl :args (tptp.c)) % 0.85/1.10 (step @p576 :rule cong :premises (@p575 @p574) :args (@t1031)) % 0.85/1.10 (step @p577 :rule trans :premises (@p576 @p573)) % 0.85/1.10 (step @p578 :rule cong :premises (@p577 @p572) :args (@t1032)) % 0.85/1.10 (step @p579 :rule trans :premises (@p578 @p571)) % 0.85/1.10 (step @p580 :rule cong :premises (@p579 @p570) :args (@t1045)) % 0.85/1.10 (step @p581 :rule trans :premises (@p580 @p566)) % 0.85/1.10 (step @p582 :rule cong :premises (@p581 @p565) :args (@t1046)) % 0.85/1.10 (step @p583 :rule trans :premises (@p582 @p564)) % 0.85/1.10 (step @p584 :rule ho_cong :premises (@p361 @p581)) % 0.85/1.10 (step @p585 :rule ho_cong :premises (@p584 @p565)) % 0.85/1.10 (step @p586 :rule cong :premises (@p585 @p583) :args ((= (_ (_ tptp.member1069318160_state @t1045) @t1044) @t1046))) % 0.85/1.10 (step @p587 :rule symm :premises (@p586)) % 0.85/1.10 (step @p588 :rule refl :args (@t1047)) % 0.85/1.10 (step @p589 :rule eq_resolve :premises (@p588 @p587)) % 0.85/1.10 (step @p590 :rule refl :args (@t42)) % 0.85/1.10 (step @p591 :rule cong :premises (@p590 @p565) :args ((= @t42 @t1044))) % 0.85/1.10 (step @p592 :rule symm :premises (@p591)) % 0.85/1.10 (step @p593 :rule eq_resolve :premises (@p590 @p592)) % 0.85/1.10 (step @p594 :rule ho_cong :premises (@p449 @p579)) % 0.85/1.10 (step @p595 :rule ho_cong :premises (@p594 @p570)) % 0.85/1.10 (step @p596 :rule cong :premises (@p595 @p581) :args ((= (_ @t1048 @t1039) @t1045))) % 0.85/1.10 (step @p597 :rule symm :premises (@p596)) % 0.85/1.10 (step @p598 :rule refl :args (@t1043)) % 0.85/1.10 (step @p599 :rule eq_resolve :premises (@p598 @p597)) % 0.85/1.10 (step @p600 :rule ho_cong :premises (@p456 @p568)) % 0.85/1.10 (step @p601 :rule cong :premises (@p600 @p570) :args ((= (_ tptp.f @t1038) @t1039))) % 0.85/1.10 (step @p602 :rule symm :premises (@p601)) % 0.85/1.10 (step @p603 :rule refl :args (@t1000)) % 0.85/1.10 (step @p604 :rule eq_resolve :premises (@p603 @p602)) % 0.85/1.10 (step @p605 :rule refl :args (@t999)) % 0.85/1.10 (step @p606 :rule cong :premises (@p605 @p568) :args ((= @t999 @t1038))) % 0.85/1.10 (step @p607 :rule symm :premises (@p606)) % 0.85/1.10 (step @p608 :rule eq_resolve :premises (@p605 @p607)) % 0.85/1.10 (step @p609 :rule refl :args (tptp.f)) % 0.85/1.10 (step @p610 :rule ho_cong :premises (@p609 @p608)) % 0.85/1.10 (step @p611 :rule trans :premises (@p610 @p604)) % 0.85/1.10 (step @p612 :rule refl :args (tptp.produc1204172211_state)) % 0.85/1.10 (step @p613 :rule ho_cong :premises (@p612 @p577)) % 0.85/1.10 (step @p614 :rule ho_cong :premises (@p613 @p572)) % 0.85/1.10 (step @p615 :rule cong :premises (@p614 @p579) :args ((= (_ (_ tptp.produc1204172211_state @t1031) tptp.s) @t1032))) % 0.85/1.10 (step @p616 :rule symm :premises (@p615)) % 0.85/1.10 (step @p617 :rule refl :args (@t1041)) % 0.85/1.10 (step @p618 :rule eq_resolve :premises (@p617 @p616)) % 0.85/1.10 (step @p619 :rule refl :args (tptp.s)) % 0.85/1.10 (step @p620 :rule refl :args (@t989)) % 0.85/1.10 (step @p621 :rule ho_cong :premises (@p620 @p574)) % 0.85/1.10 (step @p622 :rule cong :premises (@p621 @p577) :args ((= (_ @t989 @t1030) @t1031))) % 0.85/1.10 (step @p623 :rule symm :premises (@p622)) % 0.85/1.10 (step @p624 :rule refl :args (@t1040)) % 0.85/1.10 (step @p625 :rule eq_resolve :premises (@p624 @p623)) % 0.85/1.10 (step @p626 :rule refl :args (@t975)) % 0.85/1.10 (step @p627 :rule cong :premises (@p626 @p574) :args ((= @t975 @t1030))) % 0.85/1.10 (step @p628 :rule symm :premises (@p627)) % 0.85/1.10 (step @p629 :rule eq_resolve :premises (@p626 @p628)) % 0.85/1.10 (step @p630 :rule refl :args (@t989)) % 0.85/1.10 (step @p631 :rule ho_cong :premises (@p630 @p629)) % 0.85/1.10 (step @p632 :rule trans :premises (@p631 @p625)) % 0.85/1.10 (step @p633 :rule refl :args (tptp.produc1204172211_state)) % 0.85/1.10 (step @p634 :rule ho_cong :premises (@p633 @p632)) % 0.85/1.10 (step @p635 :rule ho_cong :premises (@p634 @p619)) % 0.85/1.10 (step @p636 :rule trans :premises (@p635 @p618)) % 0.85/1.10 (step @p637 :rule refl :args (tptp.produc1909270103_state)) % 0.85/1.10 (step @p638 :rule ho_cong :premises (@p637 @p636)) % 0.85/1.10 (step @p639 :rule ho_cong :premises (@p638 @p611)) % 0.85/1.10 (step @p640 :rule trans :premises (@p639 @p599)) % 0.85/1.10 (step @p641 :rule refl :args (tptp.member1069318160_state)) % 0.85/1.10 (step @p642 :rule ho_cong :premises (@p641 @p640)) % 0.85/1.10 (step @p643 :rule ho_cong :premises (@p642 @p593)) % 0.85/1.10 (step @p644 :rule trans :premises (@p643 @p589)) % 0.85/1.10 (step @p645 :rule cong :premises (@p644) :args ((not @t1047))) % 0.85/1.10 (step @p646 :rule refl :args (@t42)) % 0.85/1.10 (step @p647 :rule refl :args (@t1000)) % 0.85/1.10 (step @p648 :rule symm :premises (@p339)) % 0.85/1.10 (step @p649 :rule ho_cong :premises (@p630 @p648)) % 0.85/1.10 (step @p650 :rule ho_cong :premises (@p633 @p649)) % 0.85/1.10 (step @p651 :rule ho_cong :premises (@p650 @p619)) % 0.85/1.10 (step @p652 :rule ho_cong :premises (@p637 @p651)) % 0.85/1.10 (step @p653 :rule ho_cong :premises (@p652 @p647)) % 0.85/1.10 (step @p654 :rule ho_cong :premises (@p641 @p653)) % 0.85/1.10 (step @p655 :rule ho_cong :premises (@p654 @p646)) % 0.85/1.10 (step @p656 :rule cong :premises (@p655) :args (@t1001)) % 0.85/1.10 (step @p657 :rule trans :premises (@p656 @p645)) % 0.85/1.10 (step @p658 :rule eq_resolve :premises (@p353 @p657)) % 0.85/1.10 (step @p659 :rule cnf_or_pos :args (@t1051)) % 0.85/1.10 (step @p660 :rule reordering :premises (@p659) :args ((or @t1046 @t1050 (not @t1051)))) % 0.85/1.10 (step @p661 :rule chain_m_resolution :premises (@p660 @p658 @p563) :args (@t1050 @t1052 (@list @t1046 @t1051))) % 0.85/1.10 (step @p662 :rule refl :args (@t1055)) % 0.85/1.10 (step @p663 :rule bool-double-not-elim :args (@t1049)) % 0.85/1.10 (step @p664 :rule refl :args (@t1057)) % 0.85/1.10 (step @p665 :rule nary_cong :premises (@p664 @p663 @p662) :args ((or @t1057 (not @t1050) @t1055))) % 0.85/1.10 (assume-push @p745 @t1050) % 0.85/1.10 (assume-push @p746 @t1056) % 0.85/1.10 (assume-push @p747 @t1054) % 0.85/1.10 (step @p669 :rule evaluate :args ((= true false))) % 0.85/1.10 (step @p670 :rule false_intro :premises (@p661)) % 0.85/1.10 (step @p671 :rule refl :args (@t1015)) % 0.85/1.10 (step @p672 :rule refl :args (@t1039)) % 0.85/1.10 (step @p673 :rule symm :premises (@p746)) % 0.85/1.10 (step @p674 :rule cong :premises (@p673 @p672) :args (@t1053)) % 0.85/1.10 (step @p675 :rule cong :premises (@p674 @p671) :args (@t1054)) % 0.85/1.10 (step @p676 :rule true_intro :premises (@p480)) % 0.85/1.10 (step @p677 :rule symm :premises (@p676)) % 0.85/1.10 (step @p678 :rule trans :premises (@p677 @p675 @p670)) % 0.85/1.10 (step @p679 false :rule eq_resolve :premises (@p678 @p669)) % 0.85/1.10 (step-pop @p748 :rule scope :premises (@p679)) % 0.85/1.10 (step-pop @p749 :rule scope :premises (@p748)) % 0.85/1.10 (step-pop @p750 :rule scope :premises (@p749)) % 0.85/1.10 (step @p680 :rule process_scope :premises (@p750) :args (false)) % 0.85/1.10 (assume-push @p751 @t1056) % 0.85/1.10 (assume-push @p752 @t1050) % 0.85/1.10 (assume-push @p753 @t1054) % 0.85/1.10 (step @p687 :rule and_intro :premises (@p661 @p751 @p480)) % 0.85/1.10 (step-pop @p754 :rule scope :premises (@p687)) % 0.85/1.10 (step-pop @p755 :rule scope :premises (@p754)) % 0.85/1.10 (step-pop @p756 :rule scope :premises (@p755)) % 0.85/1.10 (step @p688 :rule process_scope :premises (@p756) :args (@t1058)) % 0.85/1.10 (step @p692 :rule implies_elim :premises (@p688)) % 0.85/1.10 (step @p693 :rule resolution :premises (@p692 @p680) :args (true @t1058)) % 0.85/1.10 (step @p694 :rule not_and :premises (@p693)) % 0.85/1.10 (step @p695 :rule eq_resolve :premises (@p694 @p665)) % 0.85/1.10 (step @p696 :rule chain_m_resolution :premises (@p695 @p661 @p480) :args (@t1057 @t1052 (@list @t1049 @t1054))) % 0.85/1.10 (step @p697 :rule refl :args ((tptp.member1069318160_state @t1059 @t42))) % 0.85/1.10 (step @p698 :rule refl :args ((tptp.produc1909270103_state @t1041 @t997))) % 0.85/1.10 (step @p699 :rule refl :args (@t1029)) % 0.85/1.10 (step @p700 :rule cong :premises (@p579 @p699) :args (@t1060)) % 0.85/1.10 (step @p701 :rule trans :premises (@p700 @p698)) % 0.85/1.10 (step @p702 :rule cong :premises (@p701 @p565) :args (@t1061)) % 0.85/1.10 (step @p703 :rule trans :premises (@p702 @p697)) % 0.85/1.10 (step @p704 :rule ho_cong :premises (@p361 @p701)) % 0.85/1.10 (step @p705 :rule ho_cong :premises (@p704 @p565)) % 0.85/1.10 (step @p706 :rule cong :premises (@p705 @p703) :args ((= (_ (_ tptp.member1069318160_state @t1060) @t1044) @t1061))) % 0.85/1.10 (step @p707 :rule symm :premises (@p706)) % 0.85/1.10 (step @p708 :rule refl :args ((_ (_ tptp.member1069318160_state @t1059) @t42))) % 0.85/1.10 (step @p709 :rule eq_resolve :premises (@p708 @p707)) % 0.85/1.10 (step @p710 :rule ho_cong :premises (@p594 @p699)) % 0.85/1.10 (step @p711 :rule cong :premises (@p710 @p701) :args ((= (_ @t1048 @t1029) @t1060))) % 0.85/1.10 (step @p712 :rule symm :premises (@p711)) % 0.85/1.10 (step @p713 :rule refl :args (@t1059)) % 0.85/1.10 (step @p714 :rule eq_resolve :premises (@p713 @p712)) % 0.85/1.10 (step @p715 :rule refl :args (@t997)) % 0.85/1.10 (step @p716 :rule cong :premises (@p715 @p699) :args ((= @t997 @t1029))) % 0.85/1.10 (step @p717 :rule symm :premises (@p716)) % 0.85/1.10 (step @p718 :rule eq_resolve :premises (@p715 @p717)) % 0.85/1.10 (step @p719 :rule ho_cong :premises (@p638 @p718)) % 0.85/1.10 (step @p720 :rule trans :premises (@p719 @p714)) % 0.85/1.10 (step @p721 :rule ho_cong :premises (@p641 @p720)) % 0.85/1.10 (step @p722 :rule ho_cong :premises (@p721 @p593)) % 0.85/1.10 (step @p723 :rule trans :premises (@p722 @p709)) % 0.85/1.10 (step @p724 :rule refl :args (@t997)) % 0.85/1.10 (step @p725 :rule ho_cong :premises (@p652 @p724)) % 0.85/1.10 (step @p726 :rule ho_cong :premises (@p641 @p725)) % 0.85/1.10 (step @p727 :rule ho_cong :premises (@p726 @p646)) % 0.85/1.10 (step @p728 :rule trans :premises (@p727 @p723)) % 0.85/1.10 (step @p729 :rule eq_resolve :premises (@p352 @p728)) % 0.85/1.10 (step @p730 :rule cnf_or_pos :args (@t1065)) % 0.85/1.10 (step @p731 :rule reordering :premises (@p730) :args ((or @t1064 @t1056 @t1063 (not @t1065)))) % 0.85/1.10 (step @p732 :rule chain_m_resolution :premises (@p731 @p729 @p696 @p530) :args (@t1063 (@list false true false) (@list @t1061 @t1056 @t1065))) % 0.85/1.10 (step @p733 :rule cnf_and_pos :args (@t1063 1)) % 0.85/1.10 (step @p734 :rule reordering :premises (@p733) :args ((or @t1062 (not @t1063)))) % 0.85/1.10 (step @p735 :rule chain_m_resolution :premises (@p734 @p732) :args (@t1062 (@list false) (@list @t1063))) % 0.85/1.10 (step @p736 :rule cnf_or_pos :args (@t1067)) % 0.85/1.10 (step @p737 :rule reordering :premises (@p736) :args ((or @t1049 @t1066 @t1055 @t1068))) % 0.85/1.10 (step @p738 :rule chain_m_resolution :premises (@p737 @p661 @p735 @p480) :args (@t1068 (@list true false false) (@list @t1049 @t1062 @t1054))) % 0.85/1.10 (assume-push @p757 @t1069) % 0.85/1.10 (step @p740 :rule instantiate :premises (@p426) :args ((@list @t1032 @t1029 tptp.pHoare259243666_exec1 @t1039))) % 0.85/1.10 (step-pop @p758 :rule scope :premises (@p740)) % 0.85/1.10 (step @p741 :rule process_scope :premises (@p758) :args (@t1067)) % 0.85/1.10 (step @p743 :rule implies_elim :premises (@p741)) % 0.85/1.10 (step @p744 false :rule chain_m_resolution :premises (@p743 @p738 @p426) :args (false @t1052 (@list @t1067 @t1069))) % 0.85/1.10 ) % 0.85/1.10 % SZS output end Proof % 0.85/1.10 % cvc5 exiting %------------------------------------------------------------------------------