{"entities":{"Q6869957":{"pageid":20716333,"ns":120,"title":"Item:Q6869957","lastrevid":97022201,"modified":"2026-06-05T13:03:35Z","type":"item","id":"Q6869957","labels":{"en":{"language":"en","value":"Ground truth: checking \\textsc{Vampire} proofs via satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8149349"}},"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":"Q6869957$1ED6FA43-3267-4353-BACB-5DBA83CC8F69","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5f10d698ac9a22a4a4fe1b66703c143f237bb038","datavalue":{"value":{"text":"Ground truth: checking \\textsc{Vampire} proofs via satisfiability modulo theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6869957$F8824F6D-A370-4FB1-AEB8-C435B3272682","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6530a2f474ec3c82feb9977226c053ebb5eb5c6a","datavalue":{"value":"10.1007/978-3-031-99984-0_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869957$4771A7B6-4DF3-403D-843E-2AD6CFC40072","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c317a0c80aecdbeefe69f1f6cac115022f894c88","datavalue":{"value":{"entity-type":"item","numeric-id":6429156,"id":"Q6429156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$9D54C774-6A5A-497F-A46F-C385B24B5EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$C3944580-4651-43BD-8ADD-EFFBF8F6611C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4356e07e26c819aaf28872c09ac7d0a6f42a7b72","datavalue":{"value":{"entity-type":"item","numeric-id":2128806,"id":"Q2128806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$2822688D-4B99-4734-9DE8-ACDB7ED12074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c1ddc7c87ccd4acfce96a5417e0b991236936b1","datavalue":{"value":{"entity-type":"item","numeric-id":5028471,"id":"Q5028471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$391C5D62-58D8-4783-8717-52123DEC7E2D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bd0535754d1571e407a6ce2636467dab5aaebc85","datavalue":{"value":{"time":"+2026-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6869957$6008DA5F-2A11-439A-9210-2DD0D0506158","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869957$657F86E9-F746-48CE-863B-220AA4A6406D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869957$037D29DF-DECA-4DB8-A7AE-2443E408EA4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869957$94531044-C4DE-4E5F-985E-217591AD41AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8c2ff9f2d7ae6c73fc90bc1b3dc4a375984fd5a2","datavalue":{"value":"8149349","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869957$A10E0762-3838-4C9A-973E-79DE6C35F3C9","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":"Q6869957$0B00970D-DDDB-487E-A8C3-1B51D431BF1F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869957$2EB065A6-89D5-4949-A9A1-E3A973CABEB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869957$95DE015E-4F5D-49A0-8E75-0045359D3742","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5174037a951618f6f15517e6135b73ffb86e1477","datavalue":{"value":"verified proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869957$4306FAFE-CF81-44A9-A4C8-3AB84C261445","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":"Q6869957$F2AC1C2D-DD4D-4F58-A7C1-0FC5DB5763A3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7123f84d6e4eb80889035fb4bfb02477147975ff","datavalue":{"value":{"entity-type":"item","numeric-id":6535368,"id":"Q6535368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$D53DCE28-DCA5-499A-9386-C6C3118A9067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$13FCC3B5-669E-41FA-BEE7-71749FFDD1A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$D1C09FC0-452F-42F9-976D-853B1B169FA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf7518b1302b421727bc51952e31ef9eaefb0e3f","datavalue":{"value":{"entity-type":"item","numeric-id":6157247,"id":"Q6157247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$6E7914CD-F4BB-48BD-A423-F41BA718A7B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$30A63E83-6BE6-4338-AFB0-4B1994841B85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4669aa80f1b8115df57035710adf683c0764c3","datavalue":{"value":{"entity-type":"item","numeric-id":4928456,"id":"Q4928456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$13DED68D-5D56-46D1-A804-6EF769BA578E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4370175d8030918ba7fe1c9ab8112224b76824d","datavalue":{"value":{"entity-type":"item","numeric-id":3498463,"id":"Q3498463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$AD7A8EFD-FAAF-4E79-BB95-B28117A5EDC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00230673e703c339b2d770b71ef179a8241cadd5","datavalue":{"value":{"entity-type":"item","numeric-id":2270573,"id":"Q2270573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$DCEAF3CE-D22A-439B-AE6F-311D18897C47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dea55e8090675bfebf34e7fbee4bcbf68f46112c","datavalue":{"value":{"entity-type":"item","numeric-id":2209546,"id":"Q2209546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$B23B7C2F-D2ED-4CCE-8B88-4B97D12D40B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b370ff9c08ff8547f00c67a9a28c6facf0878e13","datavalue":{"value":{"entity-type":"item","numeric-id":6643080,"id":"Q6643080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$A28AC058-077D-41D0-A59D-187C7E960D67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9bcd33943731bfa2ecd0fbea7c90d9866badb75","datavalue":{"value":{"entity-type":"item","numeric-id":1819255,"id":"Q1819255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$54537B8F-F492-4242-BED5-3B3850B00961","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":"Q6869957$A8102438-75A0-423B-9638-FC60ED0F68F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1724d356c4240ecf23b9ed1ec3ae79248a719b1c","datavalue":{"value":{"entity-type":"item","numeric-id":6535381,"id":"Q6535381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$DE046216-B34B-4514-A691-44A926189CEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a00d2d613f7c3b23de52ea377d6e6eca71ead76","datavalue":{"value":{"entity-type":"item","numeric-id":7034881,"id":"Q7034881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$DD1A63B5-9F6E-450B-8BDC-28EA64418F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f38c339bbd571c9f13a1b3052c0abde7b640b4a","datavalue":{"value":{"entity-type":"item","numeric-id":2471742,"id":"Q2471742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$E5C00418-9354-45BC-9C58-2B5D93C5D910","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"171f2f23484cc563361b9a949250d7cf0cf0889e","datavalue":{"value":{"entity-type":"item","numeric-id":2479551,"id":"Q2479551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$75AE1E80-3A68-45E8-B316-E77430789ACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f029e84cfc32ab5205c9ea68fc444f1299028665","datavalue":{"value":{"entity-type":"item","numeric-id":2055873,"id":"Q2055873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$B8A33034-4877-4529-84D8-E4311B5668E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69e114146a9d2d5e6b8c252e3e4a144fcee5ae9e","datavalue":{"value":{"entity-type":"item","numeric-id":1404981,"id":"Q1404981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$6AFD8B70-1131-4207-9197-236BA23D8000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"727bf6303f28578cce92a2bdc6c0d3c263a24381","datavalue":{"value":{"entity-type":"item","numeric-id":2324203,"id":"Q2324203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$C3122772-6690-4FD7-8097-F8A025DE80C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e797d69ccc16ac41adec3adfdcc63bc05d0208ed","datavalue":{"value":{"entity-type":"item","numeric-id":5172636,"id":"Q5172636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$CD7A6E88-C9C5-4648-96F7-F59F06AA5119","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d521ff011b7b02e45b83817cc2b73d756f532e8a","datavalue":{"value":{"entity-type":"item","numeric-id":7025191,"id":"Q7025191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$10780A35-9D1D-47F1-9714-743C369F4168","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":"Q6869957$11E7BAFA-08C6-4A0A-8D48-2701E3FEF8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a4e0edf0e28b481677ec6286aff34ea615b8e86","datavalue":{"value":{"entity-type":"item","numeric-id":2891471,"id":"Q2891471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$DA18DC70-DCE2-45ED-8DFB-AC25074CB5B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$2FEED57F-3314-4789-A4D0-18D28C309D8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de61fdcccb88d2f352f7a27c4d3d90e13a3d174a","datavalue":{"value":{"entity-type":"item","numeric-id":2198231,"id":"Q2198231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869957$89220870-0206-4B75-9195-C63803495B03","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6869957","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6869957"}}}}}