{"entities":{"Q3506045":{"pageid":5535949,"ns":120,"title":"Item:Q3506045","lastrevid":50381723,"modified":"2026-01-13T22:40:36Z","type":"item","id":"Q3506045","labels":{"en":{"language":"en","value":"Lazy satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5287581"}},"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":"Q3506045$95CED6D2-F67A-486C-A2B5-2BC0450B7003","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"33077a20f45a335c858758a23a94f8e8a8d14223","datavalue":{"value":"1145.68501","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$DDB53093-6A16-4F53-8DD5-8EEAADC0D576","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fd5a076641129df5baba24779caed9dec893447","datavalue":{"value":{"entity-type":"item","numeric-id":511776,"id":"Q511776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3506045$BC59C451-C34D-4DDB-A71E-7EB41C6DBDB4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f1c0b93a352a714c61ccd46766a52600d36f8c2","datavalue":{"value":{"time":"+2008-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3506045$D8F3E2CA-0DB9-4E3B-9418-D7F768597E02","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$68680B01-7D9A-4BA2-A124-4BF158E13774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$6A3D0A94-B3A4-4E9B-91D7-A2D4C5D701EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$1111E293-03E0-41EA-85B5-A1B70C5845F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$CABA1AA2-E57B-4C48-AF86-B1ACD10BCDDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$BAC07A21-897E-42B8-9E6A-725F258BB82B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"28d9ecc602607e2609f41f1a0de2f68458b0ebb0","datavalue":{"value":"5287581","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3506045$5E40CD32-23AF-410C-9E32-21365FE341EF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a97c468b9cecf4541368108100c9e45a9b8eb40f","datavalue":{"value":"lazy approach","type":"string"},"datatype":"string"},"type":"statement","id":"Q3506045$4ED43DAA-BC9D-4FD4-8F7A-F06567193596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69915e018ed669c5d09bb1f8b68333ef5bbefe95","datavalue":{"value":"SMT solver","type":"string"},"datatype":"string"},"type":"statement","id":"Q3506045$B0B9E963-0EF4-4DCE-8DA6-894CAD88E7D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q3506045$6E4B4525-EA9A-4248-B055-819A3738A856","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7a35a47cef9f2baec76c3bfc2bf8f6032431cb1c","datavalue":{"value":{"entity-type":"item","numeric-id":16827,"id":"Q16827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3506045$ACDE40CB-4C72-4AE1-8665-51DB546B65D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3506045$DF2CCEB9-3106-4FC2-9EE8-D3E00C205DD9","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":"Q3506045$21128F5B-7F47-4441-918B-6396A4DF9DB1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2eee3051a3262a82bbbee52c102ce20b2f176521","datavalue":{"value":{"amount":"+0.922096848487854","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":"Q3506045$0219EF2F-F30C-430D-9F57-B729DD0E63E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bcd5805657067d6e7605dbff8b056f18f37a6f5","datavalue":{"value":{"amount":"+0.8700841665267944","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":"Q3506045$AFF445FA-EC44-4014-9930-93AFF0CF157F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44a43da73541e40b8d93166832aeb92cd4bee415","datavalue":{"value":{"entity-type":"item","numeric-id":2830018,"id":"Q2830018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b7204f4369abff5d26e572efaff15039d369953","datavalue":{"value":{"amount":"+0.8630079627037048","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":"Q3506045$BE144384-CAF9-44C3-A421-10BB2D44D2B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1905f739cf619ec41f7a0632698a1edc5845bebb","datavalue":{"value":{"entity-type":"item","numeric-id":5429314,"id":"Q5429314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23420affea8de7069d96d18d121ce4ad79e6ab46","datavalue":{"value":{"amount":"+0.8369676470756531","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":"Q3506045$6614598F-9620-45CD-BBB4-C5006CE730A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353b46cb2a124cc2200384a940b087517c5b273c","datavalue":{"value":{"entity-type":"item","numeric-id":1037239,"id":"Q1037239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"006a1b60155ea07ddd85b6ea8cdc27413720d87d","datavalue":{"value":{"amount":"+0.8324459791183472","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":"Q3506045$E097EDFD-B049-46D4-A668-91B4417AA00D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3506045","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3506045"}}}}}