{"entities":{"Q2044190":{"pageid":2054932,"ns":120,"title":"Item:Q2044190","lastrevid":57710463,"modified":"2026-04-01T00:56:37Z","type":"item","id":"Q2044190","labels":{"en":{"language":"en","value":"A flexible proof format for SAT solver-elaborator communication"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7378297"}},"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":"Q2044190$AA19A5AE-A933-47A2-BB6A-CDCF80C25A3C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"966b913d2c6b917279b00115da39b95004efcd80","datavalue":{"value":{"text":"A flexible proof format for SAT solver-elaborator communication","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2044190$ECE206D1-CD8F-44EA-9028-311CBEB1F52D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3e7b68d570d2af404631a6b61bef25561bb34272","datavalue":{"value":"1467.68159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$46A781F1-1DA6-4D94-88E2-2B392FCD4E28","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1cfdeefac0d5791c65cc9940d842572ea96f1aec","datavalue":{"value":"10.1007/978-3-030-72016-2_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$00BE9B32-FCA0-4C81-8F1E-9EBFE057A430","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$45D0A38F-88CE-4770-9FEA-C6D0959F0DD3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6f25f924676185979ab6f246b476dde833797f44","datavalue":{"value":{"time":"+2021-08-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2044190$4006EF82-A282-436C-9EA1-7772F9889D0C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0f80babaf0ea4664072896380dce884ad196d35e","datavalue":{"value":"https://arxiv.org/abs/2109.09665","type":"string"},"datatype":"url"},"type":"statement","id":"Q2044190$C8DDC03E-E94D-40CC-8A6F-D1F6CB55D4D7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$A3323AB8-BFC6-4209-B625-57D60EBAF288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$4DDF324F-E9A6-4966-8DE7-D45FD51F10E2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dcac5166be2332fdc69113f26d0b16728d9bed04","datavalue":{"value":"7378297","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$E38B6A90-426D-405C-A231-EDC1FFEB9A44","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044190$C6E19FC1-F3D8-4F84-B526-BC80B4442033","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c981250d58ffbb2ce323c73cba72d45c0f2891c","datavalue":{"value":"proof format","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044190$0FECAE14-245F-4EA0-9E23-EB1D2D973DD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec2bd7f972687691fd228f5fff91285d00c4ce4f","datavalue":{"value":"DRAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044190$65546A57-2C6B-446D-A56C-F9F09693646F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"914c4fb672c5e9fcb02ce3cac02eea7131783a06","datavalue":{"value":"LRAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044190$A8AA11D6-FC36-4C42-836D-0111F2C2C569","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9a8e2ead841f7eccf643ba8d0d78f718b4e128a","datavalue":{"value":"FRAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2044190$3060C347-A72A-4E33-B75C-91BDB7446ECF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"93f80e8be8dfa9273ba88c387586c0aa18035da2","datavalue":{"value":{"entity-type":"item","numeric-id":1350631,"id":"Q1350631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$00852FBB-4BE7-450D-A635-D3B86670453F","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":"Q2044190$B47F16F5-59FB-4DED-8F31-E61A7AC518C4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aeeeed997cdda08d77e1b9c326fdd4e8c2c78d4a","datavalue":{"value":"W3138848921","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2044190$BAD5E907-D35F-402C-A42E-B574EAD37785","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6788f8c83d5a5db6237942eed0df1dc9fb4fc24b","datavalue":{"value":{"entity-type":"item","numeric-id":5919479,"id":"Q5919479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$ED03816A-3D15-4F97-A5CB-F061CBD1B42B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$AA7C1F42-042B-47B6-B395-374FF8B8FBB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$4C91C1CF-49AF-4945-9B65-A313037CCFF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd1ae1eae0bbb3048cc59d85f34aded019099780","datavalue":{"value":{"entity-type":"item","numeric-id":4928451,"id":"Q4928451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$67179DA4-6AE4-4D34-BE5E-C11F47644168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7012bf2c8e1ba10cf9896acdd463864da284937a","datavalue":{"value":{"entity-type":"item","numeric-id":2818017,"id":"Q2818017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$5748D0EF-63BA-42E0-8A70-D28FF62C4486","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87be12daaa9049d37eba12568fd639bb8a1c86c9","datavalue":{"value":{"entity-type":"item","numeric-id":2908507,"id":"Q2908507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$9500B1D4-570E-4ACB-A30E-ED0C355B6440","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e4aed9b8c360dba198361b37afc63de7b6c5158","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$B130B086-580B-4786-B087-A54524AC3581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839fe9e80ad88458f41a8a24be5284fc203e2e80","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$E7CD453C-C711-4863-A81A-75D740C991BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f24266047ac8ffcefe32630c940ffdb70489bec0","datavalue":{"value":{"entity-type":"item","numeric-id":2891429,"id":"Q2891429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$D6B2E679-3A51-4524-8A1E-631E09B0A3BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f769fe6ef8dd71200eafe07970c69907f40fbcb","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$9B82273F-9E80-4427-B43D-F7BF6ACF4398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee09e75a430fc0be911c9a36f98899b21bf0296","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$069B59E7-888F-4247-94D1-A0931EED317B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd36dae5803e0965ad10705e59b8bf6df76adb51","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$8FAA031C-D99B-47BA-A636-F68B6CCEFB2A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a90383e897183ac4f95a9e0efc890c2563e827e","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65805b0496c9ccb0d00ea3324aff67b27ce94173","datavalue":{"value":{"amount":"+0.7639137506484985","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":"Q2044190$2C7D3EC4-7CCE-45EE-92E6-07515D2457DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8de78b6076dabd1a68c913f5338b22a8d693321","datavalue":{"value":{"entity-type":"item","numeric-id":4928451,"id":"Q4928451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bc52eefb7e0ee2d3a5cdbf6e62a04abc05832dc","datavalue":{"value":{"amount":"+0.7616212964057922","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":"Q2044190$8CECE506-87F8-4112-9AA2-B2A183CDE4A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4fd319d3f3d0549dc990cb8bdf00c9505d81eda","datavalue":{"value":{"entity-type":"item","numeric-id":2835888,"id":"Q2835888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03a7fd68b1c847019701dd6fa134be0b8556527b","datavalue":{"value":{"amount":"+0.7513880729675293","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":"Q2044190$138960FB-E3F4-4215-B8B0-3ABC78AEDD2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b00f5c94cc43d8c2bb549b10ae10cb5879e32bf","datavalue":{"value":{"entity-type":"item","numeric-id":694550,"id":"Q694550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e26a1eb5800a921a1b165d0f823fc87f17abedb3","datavalue":{"value":{"amount":"+0.7461919784545898","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":"Q2044190$0F9C2F07-61BB-4971-B05E-755B666EBAF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85488e95f5d94d91ddf6ae5e7cb8dbe575d0db12","datavalue":{"value":{"entity-type":"item","numeric-id":3192088,"id":"Q3192088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c689b8e9854be42edfaf01e43485048ecf131418","datavalue":{"value":{"amount":"+0.7459157109260559","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":"Q2044190$E1FAA89D-F002-40CE-B0C1-A235E46D1F16","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2044190$A0D086E6-A55E-484C-9E41-CE737F787E6D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2044190","badges":[]}}}}}