{"entities":{"Q4647520":{"pageid":6677101,"ns":120,"title":"Item:Q4647520","lastrevid":36461866,"modified":"2024-07-17T19:48:39Z","type":"item","id":"Q4647520","labels":{"en":{"language":"en","value":"SiCoTHEO: Simple competitive parallel theorem provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001912"}},"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":"Q4647520$B0BC90A4-B2BE-4C46-9CFA-BA514A9EE386","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e01062201964137bc796f520056a85a895224779","datavalue":{"value":{"text":"SiCoTHEO: Simple competitive parallel theorem provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647520$51F16C21-8981-4D19-94A5-52C7CD1B4F3E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6b6169974e52753f7c29775baded58b3dc797f0e","datavalue":{"value":"1412.68259","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647520$F5817B82-2C1D-42D5-B573-2C2B3FBE10D7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d71e8a030582d0853267f1ac950edf372bace27f","datavalue":{"value":"10.1007/3-540-61511-3_87","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647520$ED59B420-1D60-4E54-B83A-5D0FB52A6486","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$22CFE000-ADCC-4220-A47F-7ECB1785D00B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647520$D18A4BDC-FA9B-4DE9-9930-0C50650E9675","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647520$10B2163E-3C2F-42B0-8D43-718C84232377","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"23ce9a2e56461bfde742f016fbc3dd7ac37165e5","datavalue":{"value":"7001912","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647520$157E5BD0-A9E8-441D-928F-BFCE68DBA5BA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647520$FB8EBF3B-0428-48B3-9CDA-F5263FDE2825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac7167e17667c0d63e2fa63595df7918ae81eb0e","datavalue":{"value":"search mode","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647520$DD10B14B-690D-4EAE-B0F6-8F60AEBC3060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c98e3dc64270ec0de715f8b38eca46cbd549427","datavalue":{"value":"model elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647520$87B80DB7-AA18-49E5-9946-5C57DB34374E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc60f8b4a637a6c4ef60783748ce8e2612a7ed2a","datavalue":{"value":"unit clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647520$B1FA093C-5B24-4946-A37D-370B27A90C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647520$7E1F4F9D-5D0D-404C-AF92-5D610D9DB71C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$9E189DC3-4433-4656-8C19-6F0E6A84F3F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$15CCDCAD-75C3-4952-8CA8-2ED18EC043C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"227cbd526ea4eef217fd567ef0b89e17137b97b4","datavalue":{"value":{"entity-type":"item","numeric-id":21959,"id":"Q21959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$E6A521D2-A1CA-41C3-B535-2ECFB963AA54","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":"Q4647520$2ED39443-1F00-4AC8-BA32-6D3B4980E5EC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"28f7d30635c02df5636a208481bbf2c4867a2918","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_87","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647520$AF770E69-CC3E-4143-AE41-0D900FF0401F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"811984b0776de3353ae8a48a09f50b66259b6516","datavalue":{"value":"W1514430395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647520$87972048-B493-409A-9CD6-DF08EB6F18CA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"07bde1b1ec996aeb071ba3c817fedaeed25122f5","datavalue":{"value":{"entity-type":"item","numeric-id":1189726,"id":"Q1189726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$DBF7827F-715B-4EE2-ADA5-D96428C1794F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$6500A798-5A9E-4397-852C-66896030BE66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"687ef395c627ab855029e1b6753ba31be5ed92f8","datavalue":{"value":{"entity-type":"item","numeric-id":4647520,"id":"Q4647520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$3E0DCF0A-EB91-465C-9B00-F72053D2A528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07441aec0715add91dbf903fea4c539fe7c16a9c","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647520$99CE885F-3BF6-4770-8F48-A63A4C6F1867","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647520","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647520"}}}}}