{"entities":{"Q2128804":{"pageid":2139547,"ns":120,"title":"Item:Q2128804","lastrevid":54302018,"modified":"2026-01-26T14:44:54Z","type":"item","id":"Q2128804","labels":{"en":{"language":"en","value":"Heterogeneous heuristic optimisation and scheduling for first-order theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7511929"}},"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":"Q2128804$B07A49C6-55F6-4058-9C35-188677DE0E33","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dfceceaa456bc481c464db801db7e20127b59067","datavalue":{"value":{"text":"Heterogeneous heuristic optimisation and scheduling for first-order theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2128804$D1E7F180-D379-4BD8-A29E-D5CE0B834A26","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c41a8e036af8a999864732498e92d31b15accffa","datavalue":{"value":"1485.68282","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$6F241458-0401-45F4-A245-B3521CE03E67","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5d7d8df0005a2a850384c1b62f090c36764ad131","datavalue":{"value":"10.1007/978-3-030-81097-9_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$270A03AD-226B-47A2-A0B2-635EB47E652F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e603ffebdd685f60b120ed7de5cd18c55a6b33f6","datavalue":{"value":{"entity-type":"item","numeric-id":2128803,"id":"Q2128803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$28B80642-136A-4A97-89A5-238BE2706220","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce9e1735095a7237c0c699c31f4c0eb57566d709","datavalue":{"value":{"entity-type":"item","numeric-id":1401931,"id":"Q1401931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$79083969-241B-4692-8A3E-B1BE63B41A3A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6a2d220bbda83e730799716cad61153265e68ffa","datavalue":{"value":{"time":"+2022-04-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2128804$7FE79DA7-90F0-4BDF-A32A-5DD92F5A8C05","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$89B274E1-65CE-4F74-840D-EAFF92AF1B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$65B60449-1C92-4603-925C-0BE8EBD2E3B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$5736753C-5113-4DE3-9659-458AA2255673","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a7b2e0425e406c7ce0b60d318de8241fa2d4ac9e","datavalue":{"value":"7511929","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$460B4EFB-D0DC-44BE-A921-944D17C9633C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128804$1E756573-BAE2-4F73-B0F8-48110CA26602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128804$76F44998-8634-477B-8509-3C41449B7AE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a27603983e64939c81aefe6780fdbe04c0fbf22c","datavalue":{"value":"heuristic optimisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128804$2D94C5B0-56A6-4F4E-9B79-01ED3C26ED4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d85165e0e8a32adcb713de3888410eb7026cc0d","datavalue":{"value":"heuristic selection","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128804$1259B6EB-35C3-45BB-872C-CF544AAF204D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a04bbc2dd1c6977212f3b2d5a350b9d34fe8c78c","datavalue":{"value":"dynamic clustering","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128804$D19FB0A9-0C87-4DFF-AFB4-9C2BD305370E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"75051848b474128e4985ed4bd6de9dfa91223569","datavalue":{"value":{"entity-type":"item","numeric-id":18412,"id":"Q18412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$D35329DF-E5EF-4942-802D-0FD1B32B529A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"484f589bd857c6ecd5604196ba88033adb11a795","datavalue":{"value":{"entity-type":"item","numeric-id":15128,"id":"Q15128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$8384E29A-2DA3-4094-AF6D-1996AC6DF63E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$7B4A80F7-4FA6-4A7C-88EB-3DAB5108A549","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":"Q2128804$3144DDF8-3BAC-401C-95B0-59C83467951D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"742d2cb656243f7db933c39696cbb7d1991ef1dd","datavalue":{"value":{"entity-type":"item","numeric-id":32848,"id":"Q32848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$9787A4ED-585D-49D5-A667-6BC41E16FBF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"30c23680895c6c05b43b4be92074136c496750ec","datavalue":{"value":{"entity-type":"item","numeric-id":28682,"id":"Q28682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$94F4F821-C6C1-430D-92AD-4B93759F6F61","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":"Q2128804$EE52046D-55EF-4AAA-A61D-43E862EC10DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$15ED767D-AA91-4A74-B7E2-6CF529BF047A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$A3DF48E0-7779-484C-88DE-3412A34524EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$F849BFAE-DFAE-435F-9CFA-EAE2D8486D12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90f139681161cf03fca3b88a13657b8b8fd37862","datavalue":{"value":{"entity-type":"item","numeric-id":25180,"id":"Q25180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$10275066-F32A-4A68-A554-B9E2B134C096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4db67863b5fec3bef62722f41df2cb373dae295e","datavalue":{"value":{"entity-type":"item","numeric-id":27083,"id":"Q27083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$838FE6AA-3480-4473-81EB-B8CB9932E086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e46473070f3c81a2b3e6d8305bbf4ff6145b7c3e","datavalue":{"value":{"entity-type":"item","numeric-id":30553,"id":"Q30553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$40897C58-5C82-4A68-9A52-CE5DB12342A2","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":"Q2128804$8F64B2E0-E469-42A3-8890-69CA88881B95","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"05629d2aeff49d8f4db6001fd174009342352d0c","datavalue":{"value":"https://doi.org/10.1007/978-3-030-81097-9_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2128804$906FE00F-00CA-492D-87AC-EECC29356319","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e65e53cbf138d69917e8b8be8e06d1bab15c6880","datavalue":{"value":"W3185228372","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128804$62654741-475B-4821-B133-2E579523B9E4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac67b0c70c19b31fa9cfcf25b6c73ae9921fdd98","datavalue":{"value":{"entity-type":"item","numeric-id":2351414,"id":"Q2351414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$7ADE32B1-A181-4B06-90AC-435E8524B93D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b945f2840d1c2d5e46ba120dbb78eb02edc11ef","datavalue":{"value":{"entity-type":"item","numeric-id":5049017,"id":"Q5049017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$93E4D312-9911-4655-AD95-4046131A72E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$B809FEB1-DB13-4B5F-AB62-479A9FB7E1D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a72cc7e7b9cacb2df1c9f3d9a1db5cf48ca2da9","datavalue":{"value":{"entity-type":"item","numeric-id":4928455,"id":"Q4928455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$A99DC624-7936-4302-8999-84B8615F4398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f44b125cf3594b01960f6a5396e298346e4cfbbd","datavalue":{"value":{"entity-type":"item","numeric-id":2870167,"id":"Q2870167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$2412646B-EA6D-457B-8967-6C42D6EEB5E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f0f40ab66cf033c5a229880b34de6b2284f9c","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$D65CAFD5-A042-4BE3-9C41-F01AA23415FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7b4ce3ab96d4236a4c36e2f89589530011a89","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$138945E1-F0DC-4754-9903-47E826A5E955","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2667127ff7e04fad7bf3f88432b6dcb7791cab15","datavalue":{"value":{"entity-type":"item","numeric-id":3624141,"id":"Q3624141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128804$760AD9EE-90D6-44DE-AF5B-B3496B1D22D8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"676fa17f9c4ed2fbc42976c93fb4c6b0c314d0d2","datavalue":{"value":{"entity-type":"item","numeric-id":2104545,"id":"Q2104545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3dce70f7efd1ef766da1be3345bdfc069946bc1d","datavalue":{"value":{"amount":"+0.7794066071510315","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":"Q2128804$8D3C514A-5D3A-4029-8E60-DB0A6977109F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93a06995049033d6a54d16a5490c6c75d6de519a","datavalue":{"value":{"entity-type":"item","numeric-id":4932637,"id":"Q4932637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20e0fe706f1319812b8abcd49d4b89fbba6666d0","datavalue":{"value":{"amount":"+0.7620574831962585","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":"Q2128804$6455FFE0-62CC-48B6-B187-B1559AC30228","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eab127e20c4e479e5e30e398294a19c06fe4cca4","datavalue":{"value":{"entity-type":"item","numeric-id":2351414,"id":"Q2351414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45b7e8b31dce16c245babb0200d77eaea1abaf5a","datavalue":{"value":{"amount":"+0.7394464612007141","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":"Q2128804$D30ED3E2-F6EC-439B-B075-28EC92DAED95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c546c37062a648d50a89f0a16d38293ac6aa402","datavalue":{"value":{"entity-type":"item","numeric-id":2104548,"id":"Q2104548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc6015be8855fd30b154984919a21be0164c8c1a","datavalue":{"value":{"amount":"+0.7277382612228394","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":"Q2128804$D1E35114-8AF4-476A-9D68-7066FD0347E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c49c35a0a21d14143c6b3154bff03edaff8fe00","datavalue":{"value":{"entity-type":"item","numeric-id":4928455,"id":"Q4928455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38f387855bcf445e2fba1cadece65cdfe915894b","datavalue":{"value":{"amount":"+0.7244656682014465","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":"Q2128804$5F4D50F0-233F-444F-8703-940AD69A9E62","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2128804","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2128804"}}}}}