{"entities":{"Q3780485":{"pageid":5810391,"ns":120,"title":"Item:Q3780485","lastrevid":52353677,"modified":"2026-01-22T10:42:21Z","type":"item","id":"Q3780485","labels":{"en":{"language":"en","value":"Hard examples for resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4043296"}},"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":"Q3780485$C4223E9F-772D-4238-B913-AF7D8D580861","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd720d1bacae60c75c59368c9f4cbf93e8e0327e","datavalue":{"value":{"text":"Hard examples for resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3780485$DC5B08A5-5B66-4A1D-9D7B-7340254D0679","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bfa4291239317bb11ae5e9cbfbea05e9e1fc3832","datavalue":{"value":"0639.68093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$EE918AA0-D466-44E3-92CA-E1E5DA74196B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fda23cd5d9b8ad27f796f5749a4bd4e9e8106d86","datavalue":{"value":"10.1145/7531.8928","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$9493779C-B672-49B5-9E47-445B837698E8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ffd6a40ad54574dfdc72407e5223fefee18b3ec7","datavalue":{"value":{"entity-type":"item","numeric-id":647404,"id":"Q647404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3780485$50D93710-1424-4FA6-82C6-21D5E4BB8C38","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f12bfc80fe4a431c556e028f5134a217234a7cc4","datavalue":{"value":{"entity-type":"item","numeric-id":63915,"id":"Q63915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3780485$65AE40EC-578B-4821-A8FB-2EFE3A47F13A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3780485$2FBA9DE1-3344-49B3-AF19-C503AAC25C39","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$99775550-180E-4756-99B1-4F89C04ECF5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$BE68E178-2B81-4005-9DBF-0D3796D29D71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$E2EE2098-6EA0-49C3-B64F-289958ED121A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0e41b117fa0bfe7073c0593c35f2350c1f2a0228","datavalue":{"value":"4043296","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$0B33BA8D-7F79-47A3-AB19-272E6E213EC8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e226b5ff06f687d5fbfa0849fb43796ec25f0925","datavalue":{"value":"pigeonhole clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$9C546875-5953-4EED-B030-904B8EDBB35D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2db40c62fbba481c23c52e595e1d3bd4320088e","datavalue":{"value":"mechanical theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$6196FE54-E6AE-4468-B993-13B246C37566","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ee539f3c66b5148353f42975573a39b50c5340f","datavalue":{"value":"complexity of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$C8A12196-E0F1-4BEA-B6D5-50135A1DBC2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1128b713fdd4bed0e39cdba707d1119f0d9df2e3","datavalue":{"value":"hard examples","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$0983DFAD-136C-4360-9251-214E726A3822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e1630fc900439d5dfeb37bb596a5b9ef3839060b","datavalue":{"value":"resolution proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$99EE64A6-DAD9-4545-8FD3-6F5D51A66831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7eb7ce57864bad79eb8b1130037c18cbe7109e9b","datavalue":{"value":"expander graphs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$4BEDB84E-0693-4D44-996C-08AA4326C870","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67d8a2f07d7915fd98dfb4b12ad3c7d69d7cec7f","datavalue":{"value":"refutations","type":"string"},"datatype":"string"},"type":"statement","id":"Q3780485$FFE7DDD2-BD48-4985-937F-7138F679C63B","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":"Q3780485$D81AAB1A-0B99-455C-A03C-87A33184AE51","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5b391aa3eda161d9113674e2af837aa6e93caf51","datavalue":{"value":"https://doi.org/10.1145/7531.8928","type":"string"},"datatype":"url"},"type":"statement","id":"Q3780485$C112CBF0-B2BE-4C4D-AFC9-7EBD25E98201","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0a4808373cc775934e7e1c5731231c70849f8492","datavalue":{"value":"W2098022011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3780485$E7B00588-178A-47A4-85F7-72666DD25A90","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33796a6906fd66794fcaa18e20c9ae9d4a4cf4fc","datavalue":{"value":{"entity-type":"item","numeric-id":4699289,"id":"Q4699289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"226c56715eb1b037b145918079210515b87604fe","datavalue":{"value":{"amount":"+0.8743531","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$AECC9323-2368-422A-9475-50720C6B311D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6c460ab9452cab48d0b8b3d1092c71e9ba657a1","datavalue":{"value":{"entity-type":"item","numeric-id":4708587,"id":"Q4708587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2f71dab412ac9355826a9812a4fe83e4d1181e3","datavalue":{"value":{"amount":"+0.8496065","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$269F998D-3AA3-4434-8084-419762FB3102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86bb30c857885d253bf26bca70742f428e38536d","datavalue":{"value":{"entity-type":"item","numeric-id":5898862,"id":"Q5898862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"051a4f0484bd5a59aa6ff390b0f71dfdedf9b874","datavalue":{"value":{"amount":"+0.820733","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$53031C79-0D92-4B6C-BB9D-3F796B8B8CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44a13204615f85c9fa4953a0f158a78851a47c05","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec3fe643b7c4e81f78f9e12379cd5463f7770ab6","datavalue":{"value":{"amount":"+0.80532837","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$F25259B4-F195-4F91-A553-23AF5ECF4E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d05f9b3a21b08f7902cbeb2c0ee0a3673f6b8ed","datavalue":{"value":{"entity-type":"item","numeric-id":1430570,"id":"Q1430570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c9bc117d985890ca03defe58791425eccfb0b35","datavalue":{"value":{"amount":"+0.8018288","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$D9D8068B-88D4-4285-9B8F-7522ADCA8B41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"912a939e92de378a73d8d1ec3fa814460af9ed6f","datavalue":{"value":{"entity-type":"item","numeric-id":1861903,"id":"Q1861903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99365ca7409b5d031f390715ba5d8332626cea06","datavalue":{"value":{"amount":"+0.8004902","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$77F7A736-5BB7-4356-9290-AF878C9E25A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc93200fd5ae2868139b8ab4dcb5ef3779f471b1","datavalue":{"value":{"entity-type":"item","numeric-id":2382288,"id":"Q2382288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c72619cc2dec4ccc247b64d3a90ca783eb6e7508","datavalue":{"value":{"amount":"+0.79205096","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$F8D2ADAE-E72F-4353-BF9D-C7C3D3D099A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5619316a94b6e1269ab17e15d058f8c10567d579","datavalue":{"value":{"entity-type":"item","numeric-id":2888509,"id":"Q2888509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cf14adc4fcb50d3b4afc6715c96d7e27e5c4013","datavalue":{"value":{"amount":"+0.782361","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$BCA88BEB-96EB-4360-A789-242557CB8DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c753af4cd3f62258c428430ac7d20fb4d480877a","datavalue":{"value":{"entity-type":"item","numeric-id":4417352,"id":"Q4417352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b6e6dad69bb5b7314115d41a0f8aa9d6c5b7564","datavalue":{"value":{"amount":"+0.78191435","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$A16B3FED-657C-44F2-AF09-2D1FA78E70EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04c0feb6dbc148a238fbe7e3cc5beaac2e5ced1d","datavalue":{"value":{"entity-type":"item","numeric-id":1854472,"id":"Q1854472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"737b35fddc92e508e0e718fac47ef9f44924e312","datavalue":{"value":{"amount":"+0.7819034","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3780485$1B871351-8B7D-440C-840D-35B36FE78E31","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3780485","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3780485"}}}}}