{"entities":{"Q2104500":{"pageid":2115243,"ns":120,"title":"Item:Q2104500","lastrevid":56991816,"modified":"2026-03-25T13:40:31Z","type":"item","id":"Q2104500","labels":{"en":{"language":"en","value":"Cooperating techniques for solving nonlinear real arithmetic in the \\texttt{cvc5} SMT solver (system description)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7628183"}},"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":"Q2104500$12D11B02-52FF-465D-A2FD-88E23E1186ED","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f0400d5e37e83be707f36790c2f008e86a4528a1","datavalue":{"value":{"text":"Cooperating techniques for solving nonlinear real arithmetic in the \\texttt{cvc5} SMT solver (system description)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2104500$36EF1FA1-E4D2-4AF2-9130-E92BEA349921","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3ffd13068c2a25111ec47cfd33f9a5d8f9c06697","datavalue":{"value":"10.1007/978-3-031-10769-6_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2104500$25B0DF2F-573F-4463-AA76-910932A151F7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d65ce0e3bca3659eb391ae066b8d6d43db4ca8d","datavalue":{"value":{"entity-type":"item","numeric-id":1996868,"id":"Q1996868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$F881EDA9-650C-4DE0-BA77-BF5B9BFB8086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$6A0032DA-A5CB-4AF0-9CE9-1B444093C878","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$9F132AC3-5A3E-4F45-A77D-F42E5ED47766","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$DD4C93D1-D0CF-4B20-AEBC-79BF01B9C886","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"db8b1b210f5d78274958848712ad4088833e6550","datavalue":{"value":{"time":"+2022-12-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2104500$5F761B02-91A9-4BF1-A1AF-C60619F1DA66","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2104500$1D7EDE9E-89A7-4230-897B-6C1B542F956A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"703090897140693ea7364a1b58e7a2746ba3e092","datavalue":{"value":"7628183","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2104500$A04A84FF-C6D8-419B-B4D6-8E29888EECFD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2104500$FF3B6542-E02D-48D2-B6A3-B71D4B38F04F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"afd78757037ec84963d77be55fc12c9fc31ad9d9","datavalue":{"value":"nonlinear real arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2104500$D1D1DDEF-178C-4139-A09A-187625ADE39E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9917a2dfd376250c18f9925b8d22d45575bb3eef","datavalue":{"value":"abstraction refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q2104500$14EABA84-6E1B-4F1B-96C3-9A4188AC1C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"32f6acfc79cc74f9063323be62fcee8d2662149c","datavalue":{"value":"cylindrical algebraic coverings","type":"string"},"datatype":"string"},"type":"statement","id":"Q2104500$1FB312E7-CD2E-4BB2-AB7C-A3B25460EC50","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c9c1f58b8025297b76815155d9e858d1b402d938","datavalue":{"value":{"entity-type":"item","numeric-id":12911,"id":"Q12911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$5CB99315-70CF-4D4E-8257-33D93F8832E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bc2b2680c6c8d1107d491dd7bc325e46943fcb90","datavalue":{"value":{"entity-type":"item","numeric-id":12912,"id":"Q12912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$10A6C89C-A241-4E5A-8620-CAF482EA00A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5df14ee9c6f65085bdee53a419634b2235aa5c43","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$F1553EA6-092B-4E3D-B677-E7FEB8AF4E2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"42950e8602f0bf155e8f0e40e68f674e5831f7bb","datavalue":{"value":{"entity-type":"item","numeric-id":21550,"id":"Q21550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$84602380-DC2F-4FD8-ADFB-BE37656C5F33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$C6783CD7-DD1D-4F39-9D5A-E838A7DAF6F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2704b04c837be55ede02d9103b8b97888a2d5c14","datavalue":{"value":{"entity-type":"item","numeric-id":27097,"id":"Q27097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$736B4502-8E8D-49B1-AEEE-7830CBB2D697","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d2f61eeddf1828d82b7393c95d22003b9c58afa3","datavalue":{"value":{"entity-type":"item","numeric-id":19210,"id":"Q19210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$BF271150-B5EA-4F9E-A076-B292557503FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bafed3392d4887bba7b89f28a9dc216193a57801","datavalue":{"value":{"entity-type":"item","numeric-id":5974820,"id":"Q5974820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$8F867949-543B-47E0-B2A7-27E51B70DD76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fed35f2083e1592d074e2b779038b334adec1c0c","datavalue":{"value":{"entity-type":"item","numeric-id":16433,"id":"Q16433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$D9407E1A-8065-4FEE-BA1C-FB3E2C8A83DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f22790b7d685d2c32362b8971015fd7b35add539","datavalue":{"value":{"entity-type":"item","numeric-id":25009,"id":"Q25009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$D0E62477-4FB7-43AB-9F6D-3558AE2184E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3fb0ea419607a73fe3d9c33ccee5e6abb6ec7a7","datavalue":{"value":{"entity-type":"item","numeric-id":17891,"id":"Q17891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$445AA4F4-D8EA-427F-8B42-B5D871DB2138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$C893489F-A880-4CAD-8512-76F0F9EBDD00","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":"Q2104500$4009B7E3-A468-4980-8FDF-C6602DE6EF8C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d383c2f7be457dbf0f1a83519d470fd5612c6cdf","datavalue":{"value":"https://doi.org/10.1007/978-3-031-10769-6_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q2104500$2CBAAB77-E644-4F3B-BDB5-BECADAA3568D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6a35fbacfacc0b9949d20e0df09c7a157aa612c8","datavalue":{"value":"W4289104052","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2104500$55118037-C330-4817-8E9D-88E60B471920","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9172794cc6d13649d0166d25dee722d6acdb3f7d","datavalue":{"value":{"entity-type":"item","numeric-id":1996869,"id":"Q1996869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$8E5B2CC4-0218-45D1-B8F9-8837FB0AF5EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8661438afabfc55e25d2d4bf6b19e2486427094","datavalue":{"value":{"entity-type":"item","numeric-id":4371694,"id":"Q4371694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$08E68714-006B-424A-84E2-B614F1CB7EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66b759afa270728a57491f1ea43fda415deb1d34","datavalue":{"value":{"entity-type":"item","numeric-id":5109894,"id":"Q5109894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$A250032F-0A0D-47E7-8CF5-7D3B65A5A4CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1645d5977fcbb346c223f2e9f46edf7dc223d58","datavalue":{"value":{"entity-type":"item","numeric-id":4691738,"id":"Q4691738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$53B6B75D-6AC6-4DA5-AF1A-9D3C799B73DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21640ae8e3aa02debe92970cf2184aca918b76e5","datavalue":{"value":{"entity-type":"item","numeric-id":5326318,"id":"Q5326318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$B858ABA7-E3F0-4776-8E12-EFCFE4586CEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4d7798eba50e0ffe1e4306d4a4aa338f6be7be4","datavalue":{"value":{"entity-type":"item","numeric-id":4079605,"id":"Q4079605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$59BD9E36-C1EB-4D40-B729-8C9B9AA45E27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5272a653f0a5de015db1319e07aaca0697a931e7","datavalue":{"value":{"entity-type":"item","numeric-id":3088298,"id":"Q3088298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$E851D574-0361-4392-B86E-D14813FA2C44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"028b173fd504347e5ec217a7eca5bf3210ea8348","datavalue":{"value":{"entity-type":"item","numeric-id":3453240,"id":"Q3453240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$DE791FA0-6439-4ABD-ADEC-575769E7C65D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dfdf450746c95865439cf08883bd3a1c78d6c83","datavalue":{"value":{"entity-type":"item","numeric-id":1114669,"id":"Q1114669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$082BBE1E-F7C6-4DC5-A4D3-2704E17F0D9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9f747e3e17dfdd736a92b2d2fca660cdcbe7408","datavalue":{"value":{"entity-type":"item","numeric-id":3502696,"id":"Q3502696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$56555EDC-4FCE-49A4-A918-76B0EAD9FE1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e388ab4b33af6c248e3feac793bdd22710c597b9","datavalue":{"value":{"entity-type":"item","numeric-id":1687555,"id":"Q1687555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$366ED9B1-F9F4-471E-BED5-FCFABA7F3681","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe33bf4e1ec51f59c09f65752ea810761eb09a2a","datavalue":{"value":{"entity-type":"item","numeric-id":4928439,"id":"Q4928439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$F4CE80F5-AF2D-4CA8-A16F-1EE97D72B4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7d21ba7c9e01a1e4d50952aba9cb27df7aae8db","datavalue":{"value":{"entity-type":"item","numeric-id":1113939,"id":"Q1113939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$B90DAEB7-5374-4B51-B894-E45E1B711F40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$D7F4792A-1C68-4804-9308-03890F82F7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a93cea25cf71843c15442f30a22b9117fe9d9104","datavalue":{"value":{"entity-type":"item","numeric-id":2307621,"id":"Q2307621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$88CC0015-15D7-45F5-A927-86044226669D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef0cfa005db30ee2379f3032b81e86e439f1d6b2","datavalue":{"value":{"entity-type":"item","numeric-id":4295433,"id":"Q4295433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$5AE91D10-4321-4DE2-AC95-F122D6E319C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29d264afad535ca761de02f7bef78c4c7deadd7a","datavalue":{"value":{"entity-type":"item","numeric-id":4928438,"id":"Q4928438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$F2A26329-8838-4425-81E6-330BE5A28117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f934ae69cb480c6dacbcb34d47160cc7f0fc73","datavalue":{"value":{"entity-type":"item","numeric-id":1757004,"id":"Q1757004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$6C8D5764-6FA7-42F6-86C5-A5D2DAE487B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$C47C6972-0488-4F30-9B85-2A1FFCA49DE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$EA3780B1-AF95-44CE-81D4-8194A6BEE699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e63030c254b23297ad01b03126cf85f6997eeb7b","datavalue":{"value":{"entity-type":"item","numeric-id":1687536,"id":"Q1687536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$48F2125B-3C90-4845-80FC-A8302490FD58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8351a3b28b69d24d131a1d97580f000dfcc0a4f8","datavalue":{"value":{"entity-type":"item","numeric-id":2817923,"id":"Q2817923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$AC97E327-C3C0-45F9-98FD-9F1FDCECB21E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"add4491e8fd66ac82b780ec4494c2c2d28510122","datavalue":{"value":{"entity-type":"item","numeric-id":677553,"id":"Q677553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2104500$0637FB5F-FCE0-4A18-AF0B-CC5C79693B25","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":"Q2104500$E0A8A948-86F1-4D90-926D-54685FCE3ABC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2104500","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2104500"}}}}}