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