{"entities":{"Q1819949":{"pageid":1830691,"ns":120,"title":"Item:Q1819949","lastrevid":69402477,"modified":"2026-04-13T06:45:52Z","type":"item","id":"Q1819949","labels":{"en":{"language":"en","value":"Problem corner: Non-Horn problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3995087"}},"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":"Q1819949$0B808C13-C764-471C-BC89-86E997FF65AD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"65eed8cf36e710acf05ff77883af2e35d35b1850","datavalue":{"value":{"text":"Problem corner: Non-Horn problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1819949$432917C8-5416-44DD-9F51-166546045E7B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e0d067b917acfa40685f3130633c51e97fd256b2","datavalue":{"value":"0614.68069","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819949$FFB9D9AF-E446-4153-B572-6E695FB045B5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819949$2BABD8FB-303D-48BD-BE41-1003EF154B7C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-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":"Q1819949$6E61AEEE-D3A6-4A14-9566-41FCB40A895B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2b836723f24a894d5bcb32890c9a8b239153a515","datavalue":{"value":"The goal of automated reasoning research is to discover ways to solve problems. Specific problems have always been the spur to research in the field, and solving them the reward for inventing and implementing new ideas. Therefore it will be appropriate, hopefully useful, and certainly enjoyable if this Journal provides a regular forum for the presentation and discussion of specific problems in some detail.    This column will be hosted by the ''Argonne group'' and the ''Kaiserslautern group'', who will start the ball rolling by presenting here several sets of problems over the next several issues. Our intention is to present in each issue a set of problems that illuminate some area of automated reasoning. We will give rigorous formulations of the problems, their complete solutions where possible, and some discussion of the interesting features of each problem or its solution. We certainly encourage others to submit problem sets, comment on the problems or solutions presented here, and in general participate in this column.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819949$B8F74BE1-CCEB-4685-8B4A-0CFB9E9AC8E6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819949$1E56CACB-5C9C-46D3-96F6-18F54C68678D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"60e3a1a8acae5f52fc4de8e1dd05cd9c7ddd3457","datavalue":{"value":"3995087","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819949$48658FAD-1398-4580-8665-1083BE8A558F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819949$D01CB0B6-992D-4717-A7DF-5E69FEE945C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ef5a98087326b7b6ae23e1778e62561b3757de","datavalue":{"value":"problems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819949$9752D9F6-370E-4C4B-8214-4F6880B54444","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f961804fcabd02be29d669054528468c74d17e25","datavalue":{"value":{"entity-type":"item","numeric-id":1224804,"id":"Q1224804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819949$30280BFB-E07D-4DDD-B8F2-FF66CA91FA2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"49c1eac4057968c5fe949fe3628039d4be0f36fd","datavalue":{"value":{"entity-type":"item","numeric-id":1165593,"id":"Q1165593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819949$77D2DBDF-661F-4655-A805-EC7EF694EBD2","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":"Q1819949$6B95FF99-7F7A-4221-8C67-52C6534BB84A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f634d779ba6bf8edeab296847a80657a8c37794b","datavalue":{"value":{"entity-type":"item","numeric-id":5131525,"id":"Q5131525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e38422adf6ba1c122ab87a03da50dd9773d365ab","datavalue":{"value":{"amount":"+0.87400657","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$E8087FB3-A8AE-4BCD-983F-8C2976ADAB37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b85d204ba140de2ba0bcf39f4c004cfccbcbe62","datavalue":{"value":{"entity-type":"item","numeric-id":757095,"id":"Q757095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dffa0eb82f401782de37064925d0913255cea2f2","datavalue":{"value":{"amount":"+0.86180365","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$528B2FB6-4F66-4224-8159-4F6311BB6246","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e22139889fe6a0c06c71328055c35a5e40949a3","datavalue":{"value":{"entity-type":"item","numeric-id":3818295,"id":"Q3818295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ada9b68bc7a170b948a8ac08d9f00f5e50c41766","datavalue":{"value":{"amount":"+0.8618036","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$606F4747-3F3E-4C27-BCD0-F72D8CD21CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9671da2ace0d3eac481c7b09bdd1ba55db0362f5","datavalue":{"value":{"entity-type":"item","numeric-id":3798649,"id":"Q3798649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ada9b68bc7a170b948a8ac08d9f00f5e50c41766","datavalue":{"value":{"amount":"+0.8618036","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$0DC15D4D-70A8-4FB8-A6CC-3C4D8E170C2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08ccc2f4167e5958a2e0ea75b7f62f35056274d9","datavalue":{"value":{"entity-type":"item","numeric-id":3655139,"id":"Q3655139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f106df08ad25369e0523984560dca7b498b09b22","datavalue":{"value":{"amount":"+0.8529984","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$F57BA22B-3993-4F5D-9578-2E7D269AAD5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2186faea0888f7e17adca9046c38aa881642dd3a","datavalue":{"value":{"entity-type":"item","numeric-id":2354173,"id":"Q2354173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eee1053d80ab28bb583d20e1efe969ebdf390441","datavalue":{"value":{"amount":"+0.8453243","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$82F32D6A-7FD4-496E-9FCD-9A962358D41F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f414e9095605946bccbb6fc1f381c83a96a7f038","datavalue":{"value":{"entity-type":"item","numeric-id":3025725,"id":"Q3025725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56c13cb21325107f47be1eabeee49d58fee0c63e","datavalue":{"value":{"amount":"+0.838511","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$95280683-AFDB-4D3E-B586-166FA8A1E993","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"348375856ddbe52d0c30e53da7a44ae063f675c1","datavalue":{"value":{"entity-type":"item","numeric-id":1105181,"id":"Q1105181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56c13cb21325107f47be1eabeee49d58fee0c63e","datavalue":{"value":{"amount":"+0.838511","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$6BD65107-D522-4D50-B42A-9FCB546B607F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ef59de0bb70b4a95083ea051ef4a9bab155f59c","datavalue":{"value":{"entity-type":"item","numeric-id":4427994,"id":"Q4427994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1d5bf97fd0f7d094b60ee97ebe1c0bc93248e36","datavalue":{"value":{"amount":"+0.83546114","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1819949$79B99A5D-6503-4C08-9739-7F07B37325A7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Problem corner: Non-Horn problems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Problem_corner:_Non-Horn_problems"}}}}}