{"entities":{"Q2817933":{"pageid":2828671,"ns":120,"title":"Item:Q2817933","lastrevid":52614398,"modified":"2026-01-23T02:50:57Z","type":"item","id":"Q2817933","labels":{"en":{"language":"en","value":"Performance of clause selection heuristics for saturation-based theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6623271"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$4390DB98-D158-4B4A-B23E-2925CC344493","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"688e0abc57d91fbb770c0d4433d36dff204eb4a0","datavalue":{"value":{"text":"Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2817933$8D598812-4D2E-4130-8EDC-FF5158638052","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8a5d628e28e84b6c35e03d2f858beb93f17522be","datavalue":{"value":"1475.68450","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$3C81464C-FA29-4188-978B-9B5BA58066B6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"24e13189cde1f2cb92427f9a51b7879b065b1f0e","datavalue":{"value":"10.1007/978-3-319-40229-1_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$823DE6AE-7DB0-42F5-B0B4-9DFA26D4E18C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"41390ccb2889a06af91bd7d467009a1fde2d1850","datavalue":{"value":{"entity-type":"item","numeric-id":862394,"id":"Q862394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$AD4FEA25-6EA9-4610-9C72-247435A9600A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9682b099d36ddd45ba9da667fdf1169c4ec75457","datavalue":{"value":{"entity-type":"item","numeric-id":2817932,"id":"Q2817932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$1B730817-585F-486E-9336-1A7C39EBA03B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$249BCBF9-A9BF-4ED9-B121-41F4E3CD923D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c42ad213f9b7f39d3e9ee142840c36c28e5864b9","datavalue":{"value":{"time":"+2016-09-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2817933$44736823-BE8D-4A1E-A675-A944744859D7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$0FAC1EF6-60D3-4348-AA33-29DD4BC06CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$379EFFF1-779A-4841-A437-FE685FE1A253","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"95d30d7f70b5d09fd978e20a464a1c2032286ef4","datavalue":{"value":"6623271","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$FA7ED6D0-8F42-4D54-802E-A4B18B0AB6C3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$F244C177-7D24-405C-BBF1-308496D4A373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$8044B6C5-622C-415A-AD54-92D1F397ACAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$CB14698F-FD1C-4F29-88A3-3452C09638E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ae8e244d27f4e93f1981ec80f87d04dfe89da","datavalue":{"value":{"entity-type":"item","numeric-id":31438,"id":"Q31438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$137B027F-C909-42B0-8B15-77EAFCACAB16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$12743323-7ECD-4FEF-BE68-F5E3B5905866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$8EAE0580-056E-4FCD-B32F-2B76B985A283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$1A950563-5F98-46AD-A085-0F07ED60EDD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$24C78FCB-DEA4-48FC-AA62-994B295DE274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45fa147ad24d78ff9111165d21eddec7203c8bfd","datavalue":{"value":{"entity-type":"item","numeric-id":20838,"id":"Q20838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$E1242A69-32EF-4085-9C32-3B9E7AA86BF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90f139681161cf03fca3b88a13657b8b8fd37862","datavalue":{"value":{"entity-type":"item","numeric-id":25180,"id":"Q25180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$0DE0A5FC-415F-436A-B2D1-52EC6D644FAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$CC8D5EDE-7BAB-4A9E-BA25-C9AA53D7C96E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$3FA61EFD-B78C-4D29-9317-08750E832757","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"73a4d908c70a08e8dfd237fb8798f9e5f0fff1a1","datavalue":{"value":"https://doi.org/10.1007/978-3-319-40229-1_23","type":"string"},"datatype":"url"},"type":"statement","id":"Q2817933$A090FFF0-0F26-467E-9E8D-69F8754033D6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ac48cd2d1def80ef7f9c6690d26d5f8b2d53b98b","datavalue":{"value":"W2460200316","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2817933$DA84F960-A5A0-4920-A2D3-9EAA622F694D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$111C19F5-8CB8-455C-94B2-5A188C2137B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05077010557fe0fc2bead50a48aa3376695c3133","datavalue":{"value":{"entity-type":"item","numeric-id":2365126,"id":"Q2365126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$2A7AD9B5-125B-44D4-BC1F-46AA7118BD93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c50bf30b5dabdf4dda50dde9e43de872f1c8761","datavalue":{"value":{"entity-type":"item","numeric-id":5200032,"id":"Q5200032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$4898BEF2-2B14-4F06-A73F-240CC35F185C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b95a10e194b852a6f6838734d909c8312bfc826f","datavalue":{"value":{"entity-type":"item","numeric-id":3028369,"id":"Q3028369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$D799637A-CA82-4416-8FDC-3BAA6B2B66AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$FE5BC9AD-C880-456F-9DE4-920C93916DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15c58f40f8893ea08e9b168dd3629a56d2e8291d","datavalue":{"value":{"entity-type":"item","numeric-id":2908509,"id":"Q2908509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$E480471F-2870-42E6-A4FC-EBDD52FDEA74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81c749cacf7214e709d79a5dc896004d1ffa511b","datavalue":{"value":{"entity-type":"item","numeric-id":3150302,"id":"Q3150302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$4E192293-458A-4E80-A498-91C8BEB172CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$66A563D8-FBDA-4F2B-A436-CD3D237986C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$7CF97D32-F9B3-4B6D-AD06-F0517BEF56B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2cf443dde1d2e5809a6b6bdf2e4ea1022579959","datavalue":{"value":{"entity-type":"item","numeric-id":1404979,"id":"Q1404979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$132C2EAB-BAE3-4C06-B2D7-5FFF133EBAE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$06EA62C6-DF09-4C9D-9D3A-EE941B708A41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$61F29061-F2A4-4973-BA21-FD111F9E5DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f44b125cf3594b01960f6a5396e298346e4cfbbd","datavalue":{"value":{"entity-type":"item","numeric-id":2870167,"id":"Q2870167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$818DF2EE-8CC5-4125-94A0-0A47FA9E4D27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$1C19C1B6-5DC4-4199-98F2-E1F66A036884","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"842d1c2c50e4f6152c1646f7649b15d27250c7c8","datavalue":{"value":{"entity-type":"item","numeric-id":3608799,"id":"Q3608799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2817933$9E06A990-9AE8-42EC-BE64-73C45620FA1E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e6ca25e782efc69d84ec6f429f6411d8ceba52a","datavalue":{"value":{"entity-type":"item","numeric-id":2817931,"id":"Q2817931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b84969a729c13cee904dc033e719fe8a31a12554","datavalue":{"value":{"amount":"+0.7936992645263672","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2817933$325E1416-9AD0-482C-A35F-74EA8C01E97F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9e5b31655744c22bb0dbc93fe0294f94ae986c1","datavalue":{"value":{"entity-type":"item","numeric-id":2817300,"id":"Q2817300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fa546349740a6e6e0dd013811c9d5b8105a2e03","datavalue":{"value":{"amount":"+0.7668841481208801","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2817933$DDF8D587-4FC1-4A24-B3F4-A6378FCE4BD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3328acb14c381645dbb1f9eb31b744a4a34bbbc0","datavalue":{"value":{"entity-type":"item","numeric-id":5210762,"id":"Q5210762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a4e0d1a8270e7b6c3a8490af62e1101a159be8a","datavalue":{"value":{"amount":"+0.7317231893539429","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2817933$9CF31416-1E35-40CA-BD55-752E93CA0B80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97e3dee283cb7c8f1714e45e58c9aefc2950b646","datavalue":{"value":{"entity-type":"item","numeric-id":4415137,"id":"Q4415137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bcf33d9b5a9ed25d06d9cc7bcb9707bd29cc02e","datavalue":{"value":{"amount":"+0.7289361357688904","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2817933$B7817810-FB76-42A0-B90A-BE42C97DE217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2e8b676e4df73b916e8709fcdd73767eda5020e","datavalue":{"value":{"entity-type":"item","numeric-id":5713744,"id":"Q5713744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b47d7c8ebeb7c1e22e830d4819e8cec4c0be7dd","datavalue":{"value":{"amount":"+0.727859377861023","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2817933$C2963F66-A2E7-46BD-8AE5-5A06A1C93A82","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2817933","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2817933"}}}}}