{"entities":{"Q287384":{"pageid":289151,"ns":120,"title":"Item:Q287384","lastrevid":60714948,"modified":"2026-04-10T18:41:24Z","type":"item","id":"Q287384","labels":{"en":{"language":"en","value":"Adding decision procedures to SMT solvers using axioms with triggers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585665"}},"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":"Q287384$798EDFB6-2B46-4111-93DF-DCA0C17B2A6F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"61f561acbccb4b59f9e47bed96dc1189f79e2316","datavalue":{"value":{"text":"Adding decision procedures to SMT solvers using axioms with triggers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287384$DD6651AE-E7EE-4441-BF7F-3C8EEBEC0AAF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8eca1832bcbbae3e1b6db177f9e04ae377392b29","datavalue":{"value":"1356.68187","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$625393FC-CA02-4AFC-AAA5-689401A650F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"04b9b333faef48487aee57ac4daec8c3dea61e77","datavalue":{"value":{"entity-type":"item","numeric-id":287380,"id":"Q287380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$6AD564A7-5866-46BB-B479-D10696AB27B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a9c3e977eb61b9fc5b2fcb92fe6e8ddc0a12670","datavalue":{"value":{"entity-type":"item","numeric-id":287381,"id":"Q287381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$676A4E16-6430-48CE-900D-5327F2C0C61B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2913586d3cd4e308bb98ff964967d2ad18399c39","datavalue":{"value":{"entity-type":"item","numeric-id":287382,"id":"Q287382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$901B4A46-63B4-4A41-9BA0-E05887D4233B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ec54547b4f5c25170660bf9ec332f673814ae34c","datavalue":{"value":{"entity-type":"item","numeric-id":287383,"id":"Q287383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$F31B7E5F-8465-4F15-A69F-8BC79C9ADF6B","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":"Q287384$FA5E1897-90E5-4216-ACAB-B48D9C91AC98","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":"Q287384$F97D538B-9A51-4CE3-A408-A4BF0D85933D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$CCDDA528-CADA-45B4-A73A-089F001B8F86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$5BC3D222-646B-4BD8-9B28-6664D0AD199E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1b1dbdf04bb6a1388438c23b1b7c234420febb92","datavalue":{"value":"6585665","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$A4EB4673-1FDA-4587-B02D-C19985516B10","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q287384$F4D5A41B-846D-4264-A659-A6F54FA6EA1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac8daf9b2a0058692665d0c45ec7b53d7ff6b82e","datavalue":{"value":"satisfiability modulo theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q287384$C97BC78A-E7DE-4A32-B235-D0F2302E89F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q287384$836D3AB1-68D5-48D5-A673-861102A4A71D","rank":"normal"}],"P1463":[{"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":"Q287384$45CF0356-BD75-4256-AFF1-5418FA6418F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$E7C05C1C-A1B8-480E-879D-725F2842B754","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":"Q287384$BAA203F7-B4CF-4A6A-AAC0-20DFD9CB7636","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$15EE9DF8-E5AF-444D-97ED-713F094DA75E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$959D5334-0A18-445E-8BE3-BC58489BD1AC","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":"Q287384$A194B988-EEA0-4CDC-A40B-0417FBAF45F8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"423bed233e89539f8b1cbf3da82e060479486127","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9352-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q287384$5B8140E6-F81E-4EF0-92A1-33A60BFBD8C1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"519d34e4aa32af0898192ae86c66085bf0f184f5","datavalue":{"value":"W798190714","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$312D3B6D-F907-4C8C-A734-D5E9C7FFC7BC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f176d988fabbd626744eee2651f4ef8cf9c0825f","datavalue":{"value":{"entity-type":"item","numeric-id":3457775,"id":"Q3457775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$6D8A82D6-41B3-41B6-ACC3-062E625505FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"103360585a9bffb1c1cc70bf60b5d74438ed3255","datavalue":{"value":{"entity-type":"item","numeric-id":1401930,"id":"Q1401930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$BCF2EB5B-375A-491C-89B9-A2F2E8326C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d147c7656be905f6aa02053ac3f0750db3cda17","datavalue":{"value":{"entity-type":"item","numeric-id":1702888,"id":"Q1702888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$F16A6579-A63B-4FA7-9D5A-8E1C2A4B7904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e06c9ee7f63c1861be20393d8a1882f7729ec88e","datavalue":{"value":{"entity-type":"item","numeric-id":549666,"id":"Q549666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$2A8221B0-B099-4E13-830B-FD57805BB0F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f814032017aa40390d4c6f26a550d62bb08ff374","datavalue":{"value":{"entity-type":"item","numeric-id":5503674,"id":"Q5503674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$28212DA6-DA7A-4D6D-B04D-F2C8EEBD2356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a45353a92b2d8942bc72a107031aea6f94ba8d0","datavalue":{"value":{"entity-type":"item","numeric-id":649643,"id":"Q649643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$5437F06E-FDFD-4F31-9E10-6A0E037EC3AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$019A17AA-7CE5-4CF2-91D2-E7D100580937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$5080AF83-C504-4086-9A37-F63D25749D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a8f27245772c2159d3ccf93c502a4163695153f","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$9EFDF98D-65BB-4A73-B8FB-4459DF42BB49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$21CB5FEB-2254-4C60-B634-EF43B3C2A537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"447a0faf8040907462e3b0d2ddb87f159fc3baae","datavalue":{"value":{"entity-type":"item","numeric-id":287384,"id":"Q287384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$39145164-F7F2-46F2-8834-6A351EE0C7BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2783b262b45229c044817d7b28465fa7e095f5ab","datavalue":{"value":{"entity-type":"item","numeric-id":3012966,"id":"Q3012966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$D1AC9DDB-F189-4442-B1AB-B2C472D82209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8764d8364aa0df8893b959d7d0bc7a5f95624fe5","datavalue":{"value":{"entity-type":"item","numeric-id":5387915,"id":"Q5387915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$01618F69-DD4D-4788-85A1-261F5F6D15C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$D1EEF0D0-4B04-4BFC-9E88-92A3B2B3F494","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$8D967069-49A9-4923-B1AC-CDE344F227B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"620e4e63cec9d7a183b3bc9b7082cb1e2f14d371","datavalue":{"value":{"entity-type":"item","numeric-id":3075488,"id":"Q3075488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$E39C1BD9-D47E-44A2-A9DE-7A7BB417FF8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$53B7C94E-6937-46A2-8DCB-1AF02B927050","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":"Q287384$605EBA5A-454A-4352-9B80-A6096E01D6B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f146ef032705198a0202edddd0325ae6774f2a","datavalue":{"value":{"entity-type":"item","numeric-id":5716590,"id":"Q5716590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$8B70418B-8BBB-4545-9F95-1D6C27DEF6F8","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":"Q287384$32BDC982-81B2-48B1-B76A-7C4C98556E0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c46c4f857cf4bfe9a86ccb0054651ce04fca385b","datavalue":{"value":{"entity-type":"item","numeric-id":2891467,"id":"Q2891467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$105ADD4D-8510-4642-87EA-1FD2502581B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f6489cf91e9b20f63ed7456f579d1977e07a3f9","datavalue":{"value":{"entity-type":"item","numeric-id":3075499,"id":"Q3075499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287384$433871EB-0AE2-402A-80F1-8F2AC8F49C1F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a006cc4d906c02d983aed510a12c11733e0ead54","datavalue":{"value":"10.1007/S10817-015-9352-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287384$BAE290A2-47DF-4736-A109-654094321248","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"501c7195d1665650cc115ce98973e595bd8a52e0","datavalue":{"value":{"entity-type":"item","numeric-id":2305406,"id":"Q2305406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53c64b6899fae64a4e92c2774929c8d33e878932","datavalue":{"value":{"amount":"+0.8423115","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$020E3388-A069-47E0-AB2A-2E7DFB41CBD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e42c0696ebfd3fb16c17afdd0eec4ae5147edf7","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3250f0b7b17953e65e38bc3680e004a2ab653294","datavalue":{"value":{"amount":"+0.83621705","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$09A24FD0-A988-4419-ADD3-CF409402748D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e434c6f686246887cde238823958ad79571304c4","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3250f0b7b17953e65e38bc3680e004a2ab653294","datavalue":{"value":{"amount":"+0.83621705","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$0B192B62-81B5-4D8D-934E-4C0BD1AFB8FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4396432ef5ab133000893590ebe84a1984c3c53","datavalue":{"value":{"entity-type":"item","numeric-id":5172636,"id":"Q5172636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"740853add7737bb3dfd43eb152040fd4055d7e3f","datavalue":{"value":{"amount":"+0.830698","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$913771FC-1AAB-4604-B7DC-64BAFFE48CF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51ac25501e10601116990b60965b583eec10389c","datavalue":{"value":{"entity-type":"item","numeric-id":2891425,"id":"Q2891425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a081ba5b4518217b1fd52115bd39c703cc717b9","datavalue":{"value":{"amount":"+0.82979697","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$3DB138A3-B889-4E1C-90E4-3AC756C83392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2736b661563708670c0260aac3786ab930b183d","datavalue":{"value":{"entity-type":"item","numeric-id":2360873,"id":"Q2360873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8173bcb9e0b99c63d56834dc91ba929b7d01c484","datavalue":{"value":{"amount":"+0.82979167","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$17CDBB7B-7FEF-4370-A9CE-C96895D1CAE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b5192e189433aa3c67746a2f4880b6830d9d2b3","datavalue":{"value":{"entity-type":"item","numeric-id":3454092,"id":"Q3454092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8173bcb9e0b99c63d56834dc91ba929b7d01c484","datavalue":{"value":{"amount":"+0.82979167","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$AC413F24-CE64-48DB-85FD-9BFB2285C94D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d1337f6f778fe290fe3a403311747133f44a1a0","datavalue":{"value":{"entity-type":"item","numeric-id":1990511,"id":"Q1990511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d02d31678cf89de59f02e5595a9014fec14ec09","datavalue":{"value":{"amount":"+0.8281807","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$E72ABC34-1B16-44BA-BD32-3AB71D6AEA09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f612c19d36b5343291184177035541706928820d","datavalue":{"value":{"entity-type":"item","numeric-id":4263161,"id":"Q4263161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3fa706e0298a49abdee67a373293db5755c7da12","datavalue":{"value":{"amount":"+0.82181555","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287384$27F704F7-C6C5-44B4-9500-F7D0734DE430","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Adding decision procedures to SMT solvers using axioms with triggers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Adding_decision_procedures_to_SMT_solvers_using_axioms_with_triggers"}}}}}