{"entities":{"Q286787":{"pageid":288554,"ns":120,"title":"Item:Q286787","lastrevid":60662451,"modified":"2026-04-10T18:21:57Z","type":"item","id":"Q286787","labels":{"en":{"language":"en","value":"MaLeS: a framework for automatic tuning of automated theorem provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585236"}},"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":"Q286787$E2E5A591-BE90-41F3-BA9E-159F06878109","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"757b8e86c13cb30839063a78669047077ca0fcf0","datavalue":{"value":{"text":"MaLeS: a framework for automatic tuning of automated theorem provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q286787$A2A415A3-E9B0-46FA-8A9E-F896027FC929","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1c4ea56e312f4ba33e42f565609f24c53092a567","datavalue":{"value":"1356.68193","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$A11643C8-74F3-4BED-BCE1-F2D8D9CAF3F3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"10ac899857b53db65920b63129111456d82cf0ed","datavalue":{"value":{"entity-type":"item","numeric-id":286785,"id":"Q286785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$BF4ED8FF-FD97-4975-9E2F-F0D78FB0A0EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$9DCADC2E-8461-4FEA-85B3-B9DE02C98D5A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$E5947F6F-FCFD-445E-867B-F5D83158A72A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q286787$6E343F41-5E47-4B03-BCC8-033C108C7F8D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cbd9d9b23aa60771d9256e27ffdbb2efc4053a28","datavalue":{"value":"https://arxiv.org/abs/1308.2116","type":"string"},"datatype":"url"},"type":"statement","id":"Q286787$7F0B0E6E-AEEE-48B4-8F35-8790181D6D0B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$6E8AB4C2-E823-4814-82A1-0BE223C1FD43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$E0166136-E15A-4D77-80B8-5941EBCD9D93","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"26f781d52219f1990002994665a356424683a400","datavalue":{"value":"6585236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$43AC67B4-3AA7-4511-8533-EAF261EFA8BA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"146c033de146eed36673950f30eed4f1d1549832","datavalue":{"value":"strategy selection","type":"string"},"datatype":"string"},"type":"statement","id":"Q286787$F397D17A-FEBA-43CA-ADEC-06393BB80511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q286787$08A9E139-1DB9-421B-A96B-A20C746DD1D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d1585ca8380d459cc6fef1e6ce4a61850ace366","datavalue":{"value":"automated theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q286787$9006050B-7558-484A-AE04-76397137F720","rank":"normal"}],"P1463":[{"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":"Q286787$2C1411FC-3C4D-4D22-BDA1-C3A171F78B3C","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":"Q286787$E25C1ADF-F7B2-4E20-957B-3BF538A88D23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$E5EAF993-21EC-40D9-861F-E830B5964FFF","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":"Q286787$D5935D9B-CF0B-4896-A01A-8158FAABBA0C","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":"Q286787$426D6B6B-3F0F-4B4C-969A-F5DDE3B1E1AD","rank":"normal"},{"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":"Q286787$24F3A934-092A-4253-AA22-DD0607699226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"949824462ad75642ee7793400532e555fbc697cc","datavalue":{"value":{"entity-type":"item","numeric-id":1352844,"id":"Q1352844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$B733BF3E-C0C4-45A6-896C-65541F6C7FC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8617a61c90a632f23d3851deb94e1069d2479a78","datavalue":{"value":{"entity-type":"item","numeric-id":13268,"id":"Q13268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$9117192A-F5A8-4824-B114-772A5E473894","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0a3128c90e03896ee0d98cf8f52b2e52fa0a4d4e","datavalue":{"value":{"entity-type":"item","numeric-id":13432,"id":"Q13432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$58F6AB05-C1AE-4DA5-888C-06F6043DA047","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":"Q286787$4255EA1A-2EC3-4DB8-955B-0EB6CB6CB04C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"15e0f57c425991779433df8a745c283c5ccf7f73","datavalue":{"value":{"entity-type":"item","numeric-id":6230810,"id":"Q6230810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$D1E25756-4B8A-44FE-B91E-F196545ED65E","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":"Q286787$6B8B84FB-E5F1-4326-8EE3-B6D7DFF83B75","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"688ab57bb85afe34beabf189cf69afc0025329f1","datavalue":{"value":"W1834745875","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$72A449F4-A89E-4135-96BC-6D65CEEB47ED","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a2a4f9eb866eb3a271d9476d54c87445f236d7fc","datavalue":{"value":"Q59430126","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$63A7D33F-7C20-4D05-A2AD-D4E6D735E2FE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4adc22ed174f33297ffa675f67b5ee27a98ff71c","datavalue":{"value":{"entity-type":"item","numeric-id":3541699,"id":"Q3541699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$435A22B2-24CC-4CCA-B2B3-6008D8C02E50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1567a09831badd078143bff84c1a31067ac56c49","datavalue":{"value":{"entity-type":"item","numeric-id":5483032,"id":"Q5483032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$5977B355-B3ED-43E5-897F-A03C4FF25D28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ed4338cc88d42d689fda3243956f7504154c17b","datavalue":{"value":{"entity-type":"item","numeric-id":1606324,"id":"Q1606324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$06036516-BDA2-4DC8-8E44-65863AAF240E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73747d1be528c82497c6517bd1ecf143bfa790b1","datavalue":{"value":{"entity-type":"item","numeric-id":2908482,"id":"Q2908482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$CED97B61-C222-40B3-8C69-57F6E4D86803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c66f03ae58a1984709b26c2c3abbc1577f8d3a6","datavalue":{"value":{"entity-type":"item","numeric-id":3561621,"id":"Q3561621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$1384F47C-1269-41A5-879C-F5A16FD9D83A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8407f41a8ed3d78e6aec8a2d590e0589519f07d9","datavalue":{"value":{"entity-type":"item","numeric-id":4827807,"id":"Q4827807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$44D1A635-AF29-4EBC-8DF5-5E23B426CB13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cec92487e0774e4ecd565c4d24d646490b018f3c","datavalue":{"value":{"entity-type":"item","numeric-id":3651487,"id":"Q3651487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$BA33BC5C-F491-4CE8-A416-5BBF4D6A5CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e80c09d9c3245e0f030d35f8db61ce50dbf8693","datavalue":{"value":{"entity-type":"item","numeric-id":1953299,"id":"Q1953299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$8C24EE73-133D-4062-A04A-4BD464238C09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdbdefccbbde9531679a04de03ca4b92f2cf0625","datavalue":{"value":{"entity-type":"item","numeric-id":4208556,"id":"Q4208556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$BC88C614-B25B-4C8E-8612-1DAC6E167910","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$D4E0539B-C8B4-4C20-B1CB-460A80E96134","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":"Q286787$D9851BB9-4395-49D2-AF90-A39ED7115144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8df9f4577a0dcd8391487c5af1766a60e3ef7ebb","datavalue":{"value":{"entity-type":"item","numeric-id":2755103,"id":"Q2755103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$8879D1E6-8579-4E81-B3B1-BB94C2E2F42D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$8D264A18-CBD7-4C46-B2AE-A3C504306D78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea4ee858c8544ddaa2b36ea8b7a73636ae5df893","datavalue":{"value":{"entity-type":"item","numeric-id":3075241,"id":"Q3075241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$98A3AD94-EF6D-4F10-A566-B349DD87B501","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"140544c9a7690ad6a5b7ff8074229f58fc9345c5","datavalue":{"value":{"entity-type":"item","numeric-id":4856771,"id":"Q4856771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$8C5E9A70-821D-4B23-B53F-4E3D7BFBE4AE","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":"Q286787$E53C7B9D-4A62-40CC-BFB1-8D51C73C757E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"80fd73283ff4280a9df7070170969c1dddd4b761","datavalue":{"value":"10.1007/S10817-015-9329-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286787$26B0BB69-9992-4C4C-9D10-FE6E6E6BBFC5","rank":"normal"}],"P1643":[{"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":"896370cc0c87d23cbd5565ea47f6f6d1c71554c9","datavalue":{"value":{"amount":"+0.8233780264854431","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":"Q286787$BA449B87-5B50-46B8-A251-2771236BD2C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e54088ab89ee7fd16cce25941c8b5b0e69c66f97","datavalue":{"value":{"entity-type":"item","numeric-id":5145434,"id":"Q5145434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab7518b27ce0ac0ac0a54c93303f0e4abdee0ec1","datavalue":{"value":{"amount":"+0.7123881578445435","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":"Q286787$9ADF9E32-3DDA-4F3A-8D8F-69912938AC1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5fd00b74096a49c6bdcdada2f0fe0a4113fe0d7","datavalue":{"value":{"entity-type":"item","numeric-id":2766732,"id":"Q2766732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70d0ddc9bc94dc1bd53a1c860389373e09a3a46e","datavalue":{"value":{"amount":"+0.694351077079773","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":"Q286787$423516C6-4270-4FB5-9EF1-51FFA8510063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e14047829147d1d85bc19e655c64b7e92d2b003","datavalue":{"value":{"entity-type":"item","numeric-id":2721215,"id":"Q2721215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4384978b47f6718fc121c8df2aeb8a9cf7d43962","datavalue":{"value":{"amount":"+0.6902257204055786","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":"Q286787$21A70437-01C8-4742-BE14-051E54F6BA70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5415cbf1fd3476fc3d9eac1eb77a3d9b0a71d9c5","datavalue":{"value":{"entity-type":"item","numeric-id":3651487,"id":"Q3651487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dee2e4aab34770923324d3074bb603e44f2d5497","datavalue":{"value":{"amount":"+0.683616578578949","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":"Q286787$54884389-752D-45F7-AFCA-E2875F6B465D","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286787$83391DD3-CFCF-4916-BD62-E0C0625C47B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"MaLeS: a framework for automatic tuning of automated theorem provers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/MaLeS:_a_framework_for_automatic_tuning_of_automated_theorem_provers"}}}}}