{"entities":{"Q5234711":{"pageid":7264279,"ns":120,"title":"Item:Q5234711","lastrevid":94688699,"modified":"2026-06-05T07:28:46Z","type":"item","id":"Q5234711","labels":{"en":{"language":"en","value":"SATO: An efficient propositional prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7111181"}},"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":"Q5234711$356085AD-9633-4C76-ACC2-2A1EC5B9EF12","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"818b6a343162fab134513628a916b1bdc05f6fa4","datavalue":{"value":{"text":"SATO: An efficient propositional prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5234711$8734FB85-F026-4979-871E-61D5DECC58EF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ddcfb243f5788d795136d742bb9eb566869ce894","datavalue":{"value":"1430.68427","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234711$BA07C798-5520-4A12-9B10-63E33E47A648","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"436af0636a712ea514bc6a4c0450afb8b1e42468","datavalue":{"value":"10.1007/3-540-63104-6_28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234711$FCD94BC2-E58C-4C57-B302-C59BE3D58578","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3d3860a2f9767fdefbee4661adcdc84432183bcd","datavalue":{"value":{"entity-type":"item","numeric-id":5234680,"id":"Q5234680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$38E08557-C6F2-4343-8B60-D426B0D7E1E1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dea1ace5968cb70ccc50b025abd55a0016bafdf0","datavalue":{"value":{"time":"+2019-10-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5234711$49D368B0-E3DF-4AF3-B4CC-77DC2929E2B6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234711$8E931161-3191-4D4D-A76C-B6F769C9CBA1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c9650dbf64478973a7584a52b41f159c9568f5c2","datavalue":{"value":"7111181","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234711$6714383A-2255-46AB-A3FE-06660CCAE2DB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93c047fb19c5161b32c5245d5c8c28b4500157fe","datavalue":{"value":"propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5234711$317925BB-D700-4949-A2C3-16ACB8C69665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a348f9efcaabdd35d491583f05dde8d8e0eb673","datavalue":{"value":"constraint satisfaction problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5234711$E63B334A-D3AC-42AD-ADA8-E5A17B72D28C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bb0c590fd75ef29f1db2bc395d8cf2ff6ec9577","datavalue":{"value":"empty clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q5234711$313AF690-7BC4-4937-AB61-CB3DE3721031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36bf05e48ae5122249e416a2566cccb31d4a1796","datavalue":{"value":"conflict analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5234711$BD0883A8-8117-4BD6-8A94-8A71CDA1469E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a00d955875730559833c31b3dab690baa6b4e46","datavalue":{"value":"splitting rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q5234711$D73D95BE-5F89-4848-A7E1-C54571BD8D57","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"19b168abea7db04055f6cf4c99009d9572497bb1","datavalue":{"value":{"entity-type":"item","numeric-id":1617008,"id":"Q1617008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$D789D762-8B97-42E1-9827-1EE01EC06961","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$347FBCF5-86B4-445B-8205-677374CA9BA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1eaabc0e561dc484a85bd72ad458c9fb5f2683d3","datavalue":{"value":{"entity-type":"item","numeric-id":15174,"id":"Q15174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$482C1D0B-FE4A-4654-BD49-58F2A9119477","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2a216d6c09dac0df49b00b19ed2bb5c4336ef7f4","datavalue":{"value":{"entity-type":"item","numeric-id":20231,"id":"Q20231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$8E6F72B0-CA40-4994-A78F-8617623D7BE2","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":"Q5234711$AE226F55-EB95-44F3-A1E5-AE9152EBE3A7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e96715690d490b703a556cffb5bbdfc7ae52a5c2","datavalue":{"value":"https://doi.org/10.1007/3-540-63104-6_28","type":"string"},"datatype":"url"},"type":"statement","id":"Q5234711$16646F86-9477-4E34-B383-9C9FDD43A082","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"88fbf827ae7342ce6a5470c309575e3f144a0408","datavalue":{"value":"W1511155470","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234711$C1C0F061-E164-4B96-8FED-4EB1C1681499","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$3ADE309B-B136-46CD-900C-8F2ED715D04D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5a384833facfee1bed7555c136a9c348cab3dd0","datavalue":{"value":{"entity-type":"item","numeric-id":5687266,"id":"Q5687266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$5F192BC3-57D7-451C-B1F4-0491361EA384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8d15a265400ee74b7ccc90f74849e6820eee631","datavalue":{"value":{"entity-type":"item","numeric-id":5687246,"id":"Q5687246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$677676FF-847D-4268-8AC2-E4161AF91258","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06844938098368d2f2cf613285d701ed35dce312","datavalue":{"value":{"entity-type":"item","numeric-id":5687269,"id":"Q5687269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$F5A26259-591D-469E-A87C-034D92382472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31b266c721655122dbe400bbee292733bb46b20d","datavalue":{"value":{"entity-type":"item","numeric-id":1244202,"id":"Q1244202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$CD823DE3-753A-4966-BCF7-226DC50A3392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5aeafb9ac2f2609d33e0e02fb8c95752a23334d9","datavalue":{"value":{"entity-type":"item","numeric-id":2365127,"id":"Q2365127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234711$49477790-ED0A-4A70-A0F2-D5416A6AE4EE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SATO: An efficient propositional prover","badges":[]}}}}}