{"entities":{"Q2870323":{"pageid":2881043,"ns":120,"title":"Item:Q2870323","lastrevid":51906815,"modified":"2026-01-20T12:42:46Z","type":"item","id":"Q2870323","labels":{"en":{"language":"en","value":"Distributing the workload in a lazy theorem-prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6247706"}},"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":"Q2870323$B990F3C9-60C8-4E0A-AB9E-E6654598F68A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ce2e1fc24ca54e3c6e491f3e7d537d919f74364","datavalue":{"value":"1279.68288","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$221704DC-81B3-48E1-8B93-76F70FC37241","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6bafd0a242f5618ddbbc7ea213aa39f63850788f","datavalue":{"value":{"entity-type":"item","numeric-id":436374,"id":"Q436374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$093D1946-DB43-4C5D-80BA-51A954DF7DF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a648f5f5c43d7007feb24ddb34b99c77877b620","datavalue":{"value":{"entity-type":"item","numeric-id":219438,"id":"Q219438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$521EEA2A-93FD-4C68-808D-D8DA3C535F05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e9f1088ba9f1d3d7866789761cabade8d750bc3e","datavalue":{"value":{"entity-type":"item","numeric-id":2870322,"id":"Q2870322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$1295240A-A281-4F0F-A5D3-C46654A5663E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$5DE8718A-28FA-4D72-9171-78DD4FAA6398","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7cbcb8793fff212e9a1970116a64b7b67cfe92e5","datavalue":{"value":{"time":"+2014-01-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2870323$52919386-866A-47B1-A1CE-68EC05F1B608","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$4240F902-AF5D-41C9-8D24-204890A917C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ff42057022552eaa82447a5a1563ef3bf93acd","datavalue":{"value":"68M14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$92C04226-088E-4134-984C-A3FDD438569C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$97945330-8E58-4292-A3E9-507A9F49CA87","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eedb0d31a6b9f09044ef244a389353fa2a7cfea7","datavalue":{"value":"6247706","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$6F2D6CB1-124D-41B4-A8F4-B299A4768D47","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870323$ED231B34-5C2C-4EFD-9CE0-B953E1E0700E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26385e325689868e7c23bf081a221ebba1fa240f","datavalue":{"value":"SMT prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870323$23E5D674-0C5C-45FD-9DC2-A707274CFB66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b36d924addd0d2f364b26835d91730b673a9f92","datavalue":{"value":"distributed computing","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870323$5B7F67BB-1A53-41FF-9A22-340A72F1E8CF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"61f1811d4a1c5c503a33d175dc2dfb5a0bc1c6d9","datavalue":{"value":{"entity-type":"item","numeric-id":37164,"id":"Q37164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$7AFE43DF-F33A-4D6A-88FC-30BA97977846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"02fecec5f329d4f94f5c075dd3db5196c201b598","datavalue":{"value":{"entity-type":"item","numeric-id":14586,"id":"Q14586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$5A76CF5D-5012-4E6B-B932-342EC7885510","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$09BA4908-FA69-4837-B407-397E97545F87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$7E114B91-018C-4592-A7EB-14E3D5E3F621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7e8c3789e3185f2513b118bd5b0118afe83106c8","datavalue":{"value":{"entity-type":"item","numeric-id":14509,"id":"Q14509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$AA03C0E7-1373-4796-BD97-6FCD1AB855FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$31DD05AD-F09D-466A-AAC1-31287BA52AC2","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":"Q2870323$E9E71160-3B8D-44B7-AFE5-386DCE922120","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"af91803435a70d7dcbc7e12027ef9149a388dd8b","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2007.03.013","type":"string"},"datatype":"url"},"type":"statement","id":"Q2870323$8CFFAD78-6156-4C21-AAB9-2AB8BC6836C9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"db7d13b1f384ce5ccc8df8e4873726719aa084ff","datavalue":{"value":"W2084101411","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$3925E05E-EF3F-4971-8974-C9CD07A1A1DB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd20eb24583a9716d40335e5e633c7acceb74dc7","datavalue":{"value":{"entity-type":"item","numeric-id":5312923,"id":"Q5312923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$D68CAACB-97DF-4B66-B528-6EFAAD64EA4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"302fba4972f027bccf62618a4d6131134324ec74","datavalue":{"value":{"entity-type":"item","numeric-id":4472235,"id":"Q4472235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$F2086F2D-C2A8-479E-9593-2E967C9F3B83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be67f799ffc5b3fd133657f657d0609a463820d","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$AB3D74A4-5DFF-42D1-BBDD-4B26BD444CDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e9b10388fa2d3e4b9f117907fadf2009c7f844c","datavalue":{"value":{"entity-type":"item","numeric-id":1818361,"id":"Q1818361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$F5FE0A97-48EC-4D74-BC6D-760B71B1A6E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$94356A3B-DE98-4F8C-AAAA-F3D0D957901C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6bc85061b2e01b3c39004d0ba311d60367a81324","datavalue":{"value":{"entity-type":"item","numeric-id":5738912,"id":"Q5738912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$E7F11AF9-1809-43CD-A62F-2A3178F6C10F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e966e8cc8535ebb93962012fb28c1c2cff17f3bb","datavalue":{"value":{"entity-type":"item","numeric-id":2505055,"id":"Q2505055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$D28F9CAB-E769-4B2C-9345-8B5C952D4D5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b026130fb14abb6ec25af9a49779c945ecc8f0fd","datavalue":{"value":{"entity-type":"item","numeric-id":3452508,"id":"Q3452508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$BB5162A6-D18B-4245-BD5B-02D1A291D029","rank":"normal"},{"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":"Q2870323$FE54EB8A-D760-4463-BB84-AAEF15A40132","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9883680049322ae9765556402a9650f1441780d","datavalue":{"value":{"entity-type":"item","numeric-id":5464711,"id":"Q5464711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$EAF8CEB4-D071-4EE7-B412-86529F3E19AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"625f6543cb45ef040d1e85336980be3f05f00677","datavalue":{"value":{"entity-type":"item","numeric-id":5900690,"id":"Q5900690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$1EDD6DB9-20E3-4659-918B-2340C99A9EAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e1218a29a5c78aac47d3b3acd08ffa2daae7e8c","datavalue":{"value":{"entity-type":"item","numeric-id":5897077,"id":"Q5897077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$D55FFEB4-2B20-4928-916B-283069793D45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da96dfa99f70c6b2b69c48b417a516b8fa851830","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$55EE5E20-02AE-4B32-95E2-8AD1C1B63156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$3643A966-6C2F-42CB-9F56-F0EF85A3E9A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"601ec2c706ddf45de31ee679a12674e1ca489252","datavalue":{"value":{"entity-type":"item","numeric-id":4916225,"id":"Q4916225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$836C3AC9-9E37-4A4F-9441-3EAC3FA6EF0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6262559df3842098f118ecbbb77dfbfa994753cf","datavalue":{"value":{"entity-type":"item","numeric-id":5709987,"id":"Q5709987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$662F431D-9095-44A1-8A5F-C1FDB7B07D6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870323$5ECF287A-6555-498E-B394-3DF10D99061A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6b4db96e60e2747dfabe0fa4b1a2cb593c9cc001","datavalue":{"value":"10.1016/J.ENTCS.2007.03.013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870323$7DDDCC63-197B-424C-876C-BA896F4C1F43","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ae810403ea1189c984c72ff02aea4b6363938e6a","datavalue":{"value":{"text":"Distributing the workload in a lazy theorem-prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2870323$577B1EC1-D939-4514-AF21-820BF430465A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"555ee5f39e2f5496be04ee5c114e599be5181310","datavalue":{"value":{"entity-type":"item","numeric-id":5055785,"id":"Q5055785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b730588a90b510681cf1f786beb11a345e83c225","datavalue":{"value":{"amount":"+0.7849345207214355","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":"Q2870323$C886DBFE-4035-4247-BB2B-41E5B9467333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a7d9eb368efdd31ead856ff0a227fb8c4c8a2f9","datavalue":{"value":{"entity-type":"item","numeric-id":5900690,"id":"Q5900690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e582dcea51b8b5a0519cc6927d6c33a6ca7dc878","datavalue":{"value":{"amount":"+0.7513775825500488","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":"Q2870323$CB06A302-AA92-48C4-92F5-2B618A79729C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2e4a459cd681602bde32370332d18516e07d6b4","datavalue":{"value":{"entity-type":"item","numeric-id":4227007,"id":"Q4227007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad375dd206c2813ecc722aa991c933d8d3691d9e","datavalue":{"value":{"amount":"+0.7346475720405579","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":"Q2870323$6D46B548-D735-4D0F-BDA8-2CBB07D9914B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7893947a6cf73e3f8310960fbedeeb5a60baaba","datavalue":{"value":{"entity-type":"item","numeric-id":4281516,"id":"Q4281516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"926b9ddfb494e10fc339453dae4f7f89e14533aa","datavalue":{"value":{"amount":"+0.7278044819831848","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":"Q2870323$2BAD4391-BA17-46E5-AF60-2098A75F2560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d75b0de3eaf6679dda011cd141a8b7574811f0db","datavalue":{"value":{"entity-type":"item","numeric-id":3491009,"id":"Q3491009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3830553cfc14e3efd96fa0de3bf1666f9ab33f82","datavalue":{"value":{"amount":"+0.7278043031692505","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":"Q2870323$F3A4EDFD-6F7E-474A-8665-4DDBB061BA9C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2870323","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2870323"}}}}}