{"entities":{"Q1337564":{"pageid":1348303,"ns":120,"title":"Item:Q1337564","lastrevid":67187490,"modified":"2026-04-12T15:55:24Z","type":"item","id":"Q1337564","labels":{"en":{"language":"en","value":"The rue theorem-proving system: The complete set of LIM+ challenge problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 683154"}},"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":"Q1337564$027459BC-3DB4-423C-A5DF-5BFDF3AF04AF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"26b9a23f616cb7eb2aa04955217ea64de676bfc2","datavalue":{"value":{"text":"The rue theorem-proving system: The complete set of LIM+ challenge problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1337564$28B1AF54-F41F-4AF0-9CE7-40D12C0C2074","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4fc75336cbc3af03ff6d08e42164b7ce9ec57d28","datavalue":{"value":"0812.68111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337564$CFCB27E6-DD90-45FD-BD7B-CACFAE228B1E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fba7c88dfc049841aa9afb654e367a8058d2ce1c","datavalue":{"value":"10.1007/BF00881889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337564$6A3986AE-0AFC-400E-9320-AFAFDB2417B9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c7b687217a28e46eaf95bcf4e4de6c87ca0aa219","datavalue":{"value":{"entity-type":"item","numeric-id":1337563,"id":"Q1337563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$45FB273B-2940-48DF-8322-0177E28E58AB","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":"Q1337564$0CA86766-CF8F-4DBC-B6AD-04DFE112AC49","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5d7b3792c6f1d919d9d108f6161dcb3e3ccde785","datavalue":{"value":{"time":"+1994-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1337564$8B3AA73E-ED75-4EFB-924E-09E8B600BD1D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337564$4E3D21BD-B085-4F5D-BFA4-471E1AF3ABE1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"39c6917eb025f3bc07c2d74049465f5df7169345","datavalue":{"value":"683154","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1337564$D0A36D94-8DBD-4CF4-A615-2B4EE7830B52","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337564$D2DE1097-A025-4504-9E8F-6DB026385AD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a14647a021d250427faa255f602975f365544ae7","datavalue":{"value":"hyperresolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337564$B0B4BCB5-258F-4696-9379-09047B216618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f58d5760bc49e292a2ac00f69df6aec329ab336","datavalue":{"value":"restriction strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337564$F897FCAB-D175-4ACE-B057-532AD7027FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"127a0da7dc11243c2649a05041fe8f094ebd78da","datavalue":{"value":"RUE hyperrefutations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1337564$56D0CAA6-CD33-4D49-B435-3185D338A9BC","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":"Q1337564$16007088-9720-475B-B715-8EA5FAB79EA7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"afb31cfec21be04f1ba8409c207f9c0a2daf7299","datavalue":{"value":{"entity-type":"item","numeric-id":915496,"id":"Q915496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$325E3FF0-AE08-410A-BFD3-BEBEB2323016","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$EFDF92D4-7C21-47EC-8862-90F4B128D1C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab28196900649513f2df64714ed07752bd2d34d3","datavalue":{"value":{"entity-type":"item","numeric-id":3490993,"id":"Q3490993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$22367562-6B41-466C-897D-9F9DB078C4B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49814c2ab9d6d7f7f1dbcc32c815090446937a30","datavalue":{"value":{"entity-type":"item","numeric-id":1311402,"id":"Q1311402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$A3175309-1B4A-40CC-A467-8ADFF8E5FEA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98accc748f2654bc76222dfd845dbf5f71dfd55f","datavalue":{"value":{"entity-type":"item","numeric-id":3883568,"id":"Q3883568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$AC0021DD-01F0-4A80-9975-33FE8B79BA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d75089528348e2ee7d07dc2ae126b0ed3005ed24","datavalue":{"value":{"entity-type":"item","numeric-id":4096460,"id":"Q4096460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$CAA7C2E5-1FAF-4422-A502-A745287EFEF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1af0fa3ab79d3aca7d0c2eb038f3a2d86af567","datavalue":{"value":{"entity-type":"item","numeric-id":5541351,"id":"Q5541351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$E72A3E16-CB87-40D6-8076-E3667FDC54CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0aefa01969c4c5ab3568e4445e95ff48e256399","datavalue":{"value":{"entity-type":"item","numeric-id":4095910,"id":"Q4095910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1337564$64337017-22DD-40FB-AE70-A82ABFE5D618","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a8f08964365bf14e7e5de57d302a111fa64bcf4","datavalue":{"value":{"entity-type":"item","numeric-id":408157,"id":"Q408157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6e1b6746ecb38782f1fed3e394bff1705ea4b1c","datavalue":{"value":{"amount":"+0.84582704","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":"Q1337564$6875056B-EE06-413C-924F-ABBFED55E6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9541788a4abb7db239f8ec05398f50c05aabecf6","datavalue":{"value":{"entity-type":"item","numeric-id":3576195,"id":"Q3576195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6e1b6746ecb38782f1fed3e394bff1705ea4b1c","datavalue":{"value":{"amount":"+0.84582704","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":"Q1337564$2A5B8A0C-5948-4DFB-82E9-32CCC24E2089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc5eb68999c3412297b5ef52f0fb23f5595c190c","datavalue":{"value":{"entity-type":"item","numeric-id":3804236,"id":"Q3804236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d08866f282addac6bf384e87cd66c919c4351c7c","datavalue":{"value":{"amount":"+0.84310204","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":"Q1337564$E8FB45DD-4088-4789-B6F8-39043C34DB09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9c776f6be15dc6e8d8d94c807e5ba472ccedb3b","datavalue":{"value":{"entity-type":"item","numeric-id":4538915,"id":"Q4538915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bef86736274faec937fd84ef779aa37d188758ab","datavalue":{"value":{"amount":"+0.8298751","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":"Q1337564$168F9C0D-80D3-4FF5-B450-57ADA496C671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3605788f4b22defe4c7a11f58a5e8bc655c6aca8","datavalue":{"value":{"entity-type":"item","numeric-id":5475741,"id":"Q5475741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5ab81c3043f3f9551958579ce68b2125c2c310c","datavalue":{"value":{"amount":"+0.82552886","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":"Q1337564$FFABA2F1-B01B-47CC-8547-E358536EA334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a71ecbaf84f28c342c3776fbbc4438d17d87a980","datavalue":{"value":{"entity-type":"item","numeric-id":4223458,"id":"Q4223458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"afb78aa1ac8e035ea32dc94843386bc1a067fec4","datavalue":{"value":{"amount":"+0.8251694","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":"Q1337564$84ADE683-D5DD-4A11-BDF0-294C61F4170C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7e09e78c03182ddccc8515798a059c7aec069a5","datavalue":{"value":{"entity-type":"item","numeric-id":3454123,"id":"Q3454123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50de1d1819b8ec82cc61964a9e4df1d4bd1c7097","datavalue":{"value":{"amount":"+0.82507116","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":"Q1337564$C03BB110-4BC2-4E5C-AA90-200BF252F49B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4043424a019ad7473006eca39e1b8daadbac8cf","datavalue":{"value":{"entity-type":"item","numeric-id":2102932,"id":"Q2102932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a93f2fcf40241387a76f6ae1a27d3894695ca51d","datavalue":{"value":{"amount":"+0.8246231","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":"Q1337564$6360724B-35D3-408C-83B8-72D3559AC25A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37f9377c4604b01b815ce46c853e8d801c0d9c8d","datavalue":{"value":{"entity-type":"item","numeric-id":3515519,"id":"Q3515519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"070567d87ca59211c2f9aecc95069471b18bda2b","datavalue":{"value":{"amount":"+0.82161033","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":"Q1337564$922825F2-743E-4E0B-9986-3D3E9BAA8481","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfe776d3fe927c40ec99f1c0a53436cc939d25ea","datavalue":{"value":{"entity-type":"item","numeric-id":4381398,"id":"Q4381398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3be78e50da4e9ef2ec7a127ea941eb3b1feb3943","datavalue":{"value":{"amount":"+0.82136816","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":"Q1337564$A2021749-D12F-407D-AACF-29163EA6DA54","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The rue theorem-proving system: The complete set of LIM+ challenge problems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_rue_theorem-proving_system:_The_complete_set_of_LIM%2B_challenge_problems"}}}}}