{"entities":{"Q5900726":{"pageid":8007031,"ns":120,"title":"Item:Q5900726","lastrevid":50958569,"modified":"2026-01-15T22:40:45Z","type":"item","id":"Q5900726","labels":{"en":{"language":"en","value":"Superposition with equivalence reasoning and delayed clause normal form transformation."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5695416"}},"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":"Q5900726$915ADCAF-F73A-4608-8792-3EF0BE1CD6E1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e7c3f040a8feb248e6dc29a1def291c92088958","datavalue":{"value":{"text":"Automated Deduction \u2013 CADE-19","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5900726$89FDCC88-8867-4316-B7F0-A8AC87667160","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"345ca970589cfe97db7718b2c5dba44302e56af1","datavalue":{"value":"1278.68261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900726$8D64A0CF-BFA0-4A0E-B759-930D85C0681F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b043e7c633006f3fac5c3bfd0395a92f663b5539","datavalue":{"value":{"entity-type":"item","numeric-id":758210,"id":"Q758210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900726$AF61C561-6208-4CE5-BC3B-B60EF858D609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f92e99a34db134ba4f25b89e7455bff7feb3ebfe","datavalue":{"value":{"entity-type":"item","numeric-id":1275019,"id":"Q1275019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900726$C13010B7-F2D1-4E94-8D8F-127E885068E5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900726$35AB96C7-DC6D-42A9-B069-1576DFB23C20","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c61bb6d282cc95675f5b726985d020f8b0e6f23","datavalue":{"value":{"time":"+2010-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5900726$C9E7E60A-DE49-48E2-A5AD-839B8959417F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900726$0929996F-B073-4FA3-BBFE-93AEDDCC9398","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4e6426e26eede6806f80bc4ec480eb98afe06dd9","datavalue":{"value":"5695416","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900726$07AB0C3C-B506-437D-AD88-F03E486322AD","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":"Q5900726$5EB740DB-12B0-47D3-9CA9-EE94CA6BD5F5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c1c668ddb4fae172b1931ef73496e5bcbc0e7e0c","datavalue":{"value":"https://doi.org/10.1007/b11829","type":"string"},"datatype":"url"},"type":"statement","id":"Q5900726$C072E35D-052D-452D-834C-3741C610984D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f2de3997ca74820eaa5379240d8d8210d2079dd","datavalue":{"value":"W2483160171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900726$1A41C4C0-1B83-4B8B-9A2A-7E7C3E408197","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"77803cf595c8808153636f8e001b2ddb16a0f0ed","datavalue":{"value":"10.1007/B11829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900726$A306A203-369C-434C-86BF-567D7F0CACA2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d16d61b4c27c1607e9ae2ffb9e23530d3edb050c","datavalue":{"value":{"entity-type":"item","numeric-id":2486577,"id":"Q2486577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48a22b47e71f32dcd3744c0cd6a014ca2f9aa203","datavalue":{"value":{"amount":"+0.9929879307746888","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":"Q5900726$E31B2F2A-ECC6-4B58-92FA-0C6E1A269078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9848e817c6fcd9fa4847b21172716f0a7fe083d5","datavalue":{"value":{"entity-type":"item","numeric-id":4249896,"id":"Q4249896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f0a33ca500a35070d03651e66cfbef6c0f2a6a7","datavalue":{"value":{"amount":"+0.806146502494812","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":"Q5900726$F2A13998-432F-4DDA-98EB-A9EBA987DEAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d8cdcc0bc38cde26587a3338b1faf976e3f210f","datavalue":{"value":{"entity-type":"item","numeric-id":5881276,"id":"Q5881276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f541c1693e10441958e79fdc09a22d198eec154","datavalue":{"value":{"amount":"+0.8033161759376526","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":"Q5900726$1876A3B1-61ED-48C2-81F1-660A04F87454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4b1cca5b3b4f8752faa6dd4c1672915b638687e","datavalue":{"value":{"entity-type":"item","numeric-id":1060857,"id":"Q1060857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1eb6955959850bbf1fc2c0ca01b3e089fe9a20ae","datavalue":{"value":{"amount":"+0.8012062311172485","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":"Q5900726$1BED758D-4FA7-4CBC-9EE6-F21457340857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc0648c5040259043bc4520353343d36d4ea6fc4","datavalue":{"value":{"amount":"+0.7999441027641296","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":"Q5900726$5F45ABAB-88F0-420B-B7BC-AB3DCAE4BE24","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5900726","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5900726"}}}}}