{"entities":{"Q1353991":{"pageid":1364730,"ns":120,"title":"Item:Q1353991","lastrevid":68534655,"modified":"2026-04-13T00:23:01Z","type":"item","id":"Q1353991","labels":{"en":{"language":"en","value":"Davis-Putnam resolution versus unrestricted resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1005825"}},"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":"Q1353991$7BB15918-9979-4570-944D-7901A4C78AD3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d9d07fb3ed39776a9836d9080ef2621307116882","datavalue":{"value":{"text":"Davis-Putnam resolution versus unrestricted resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1353991$6495B7CA-E67B-46E7-98D3-57AA183AE794","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"515b7fe0a5c04af02de554f24788b90da9edc7e2","datavalue":{"value":"0865.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1353991$607CA338-852B-4ACB-9F61-A4EFA385D41C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ee190287d611e8c9a8339db93fa33fe8f2477e2c","datavalue":{"value":"10.1007/BF01531027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1353991$01DAAADB-34A2-427E-8B26-DF6767681FCB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2f77b99534bc776002bbbb76fab00244081288fe","datavalue":{"value":{"entity-type":"item","numeric-id":676450,"id":"Q676450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$589DB547-1106-4866-85F7-C9C848922F77","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7346dc34d1d50fea46ec345fbc7e3214530889ab","datavalue":{"value":{"entity-type":"item","numeric-id":276517,"id":"Q276517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$269B13D5-FBC5-4B2C-B9BF-D7DF8B58CF12","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"253a0cc57300e2194fc1b5d1f13fbbc8bc97b0de","datavalue":{"value":{"time":"+1997-05-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1353991$9A5BCC8E-264B-4D9E-853A-50EE7913E606","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1353991$4BD78A1E-DB50-4E88-86A3-5367F0398549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1353991$F26A0376-272A-4BBA-A8B9-AB4319E91A9F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6ce9c9455bd0b741a6610ef560a7d38ac1b1edd2","datavalue":{"value":"1005825","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1353991$D7EECAC0-01C6-4C0F-B753-848BC7D93C40","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0ade98bea3e2b12abff896a2f57a3d66783bfd00","datavalue":{"value":"proofs of superpolynomial length","type":"string"},"datatype":"string"},"type":"statement","id":"Q1353991$0F5F0A9C-EAD3-4C0B-9D46-96F0B3865A77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b3c11951d652b4de5155da91be01497d3347670","datavalue":{"value":"Davis-Putnam resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1353991$58882A8F-767B-49D9-A310-C9A18EA6F353","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dff5d0435c0674cdd6d45a703ff7ce5dda5366d3","datavalue":{"value":"unsatisfiable propositional formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q1353991$36673372-2639-4540-9A3C-763ECA451498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4af1f40f9625759269bfa8b9df817566c5566409","datavalue":{"value":"unrestricted resolution proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1353991$DDE1C1AE-3C59-4D24-A4DE-18AB452A8C0C","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":"Q1353991$A3568543-0012-4576-8306-99493E0DE295","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5035ead90ebf2e92af4cb88fdfc91c7dfa88c06a","datavalue":{"value":{"entity-type":"item","numeric-id":920967,"id":"Q920967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$6825C0F4-6603-43B1-A8F6-02C5A17EAB59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c636dd583a22faf929d1cb972aae014f779c04","datavalue":{"value":{"entity-type":"item","numeric-id":3496310,"id":"Q3496310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$17696A72-0D06-47F5-9ADC-B004CF303680","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$FEFA9005-D148-4838-8F89-E5FF6F639358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$8F84A753-789D-4C79-8F5E-556E6C621312","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a35cc55e5b10a424a85f3ddcd5c540cf5328ff0d","datavalue":{"value":{"entity-type":"item","numeric-id":1249435,"id":"Q1249435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$3AD35F2C-4759-428D-AA40-5FA72A057BC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e209e4fa3ae3f97cdbdf801f4c481dca6413fa3","datavalue":{"value":{"entity-type":"item","numeric-id":1185013,"id":"Q1185013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$88346F61-1518-474C-A369-3F801CF88AE5","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":"Q1353991$CD66CD06-B7B0-4C2C-BE0E-2838EAEC6D8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81494301ed40478ad47563138f01784b63003971","datavalue":{"value":{"entity-type":"item","numeric-id":4152212,"id":"Q4152212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$EED98E62-7934-46CB-B2EE-618AB79B278C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1353991$D6FB7D8B-6887-4818-9AA0-5595CABB7A85","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b7af018f8b2ebf4b0b3e603a833e0faa6948251","datavalue":{"value":{"entity-type":"item","numeric-id":3358707,"id":"Q3358707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"daecda1beefcaaae39207241ba058b12f6cd85d0","datavalue":{"value":{"amount":"+0.8593423962593079","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":"Q1353991$9019D017-9085-4F7A-ABC0-84C393E6F1AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb7dd7121840a604fc08203d23cac813c1e85682","datavalue":{"value":{"entity-type":"item","numeric-id":1185013,"id":"Q1185013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b4fb1b30f7f07ca7946d9fcd8ea80ff7bbb784f","datavalue":{"value":{"amount":"+0.8529286980628967","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":"Q1353991$978BF8C5-83B3-4E08-BBF8-3A84D4DD4E4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"daa7bdae693216d7f67ac726ebf3ab505aaf4170","datavalue":{"value":{"entity-type":"item","numeric-id":2784492,"id":"Q2784492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a559de1b7e41366f5f817e0a8972da85f07a29eb","datavalue":{"value":{"amount":"+0.8244456648826599","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":"Q1353991$B98F6B86-41B3-4516-8205-30CF0F74D8C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Davis-Putnam resolution versus unrestricted resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Davis-Putnam_resolution_versus_unrestricted_resolution"}}}}}