Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 32
Описание файла
Файл "Диссертация" внутри архива находится в папке "Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова". PDF-файл из архива "Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова", который расположен в категории "". Всё это находится в предмете "физико-математические науки" из Аспирантура и докторантура, которые можно найти в файловом архиве СПбГУ. Не смотря на прямую связь этого архива с СПбГУ, его также можно найти и в других разделах. , а ещё этот архив представляет собой кандидатскую диссертацию, поэтому ещё представлен в разделе всех диссертаций на соискание учёной степени кандидата физико-математических наук.
Просмотр PDF-файла онлайн
Текст 32 страницы из PDF
РЕЗУЛЬТАТЫ ТЕСТИРОВАНИЯ ПРОГРАММЫ НАЗАДАЧАХ ИЗ БИБЛИОТЕКИ ILTPВ таблице Г.1 представлены результаты тестирования производительностипрограммы WhaleProver на задачах из библиотеки ILTP версии 1.1.2 [144].Тестирование проводилось на персональном компьютере с процессором Intel Corei5 3.40 GHz, ОС Windows 7 и 16 Gb ОЗУ.
Лимит времени на каждую задачу100 секунд. В таблице приведены только те задачи, которые были решены (т. е.доказаны или опровергнуты) программой WhaleProver. Отсутствующие в таблицезадачи программа WhaleProver не решила либо по причине истечения отведенноголимита времени, либо по причине исчерпания доступного объема оперативнойпамяти.В таблице также приведены времена решения задач из ILTP двумя другимипрограммами: ileanCoP 1.0 и Imogen.Таблица Г.1 содержит следующие столбцы:1. «Задача»: название задачи.2. «Время»: время, затраченное на задачу программой WhaleProver.3.
«Результат»: результат, полученный программой WhaleProver. Может бытьодним из двух: «Теорема» (утверждение доказано) или «Не теорема»(утверждение опровергнуто).4. «Статус ILTP»: обобщенный «интуиционистский статус» задачи.5. «Статус TPTP»: обобщенный «классический статус» задачи.6. «Время ileanCoP»: время, затраченное на задачу программой ileanCoP 1.0.Результаты программы взяты с сайта ILTP [144].7. «Время Imogen»: время, затраченное на задачу программой Imogen.Использованы результаты регрессионного тестирования, предоставляемыевместе с исходным кодом [89].Обобщенный «интуиционистский статус» — это специальным образомсгруппированный статус задач из ILTP («intuitionistic status» в терминах [121]):204 «Теорема» — соответствует статусу «Theorem» из статьи [121]; «Не теорема» — соответствует статусу «Non-Theorem»; «Неизвестен» — соответствует статусам «Unsolved» и «Open» (нерешеннаязадача, статус не определен).Обобщенный «классический статус» позволяет аналогичным образомсгруппировать статус задач по классификации TPTP («classical status» в терминахстатьи [121]; подробнее см.
в [137]): «Теорема» — соответствует статусам «Theorem» и «Unsatisfiable» (обастатусаозначаютневыполнимостьотрицанияформулы,котораяизвлекается из формулировки задачи указанным в параграфе 4.3 способом); «Не теорема» — соответствует статусам «Satisfiable» и «CounterSatisfiable»(которые означают выполнимость отрицания соответствующей формулы); «Неизвестен» — соответствует статусам «Unknown» и «Open», а такжеуказывается, если «классический статус» в задаче не приведен.Присоставлениитаблицыиспользоваласьинформацияоб«интуиционистском статусе» задач из сводки, опубликованной на сайте ILTP[144], и информация о «классическом статусе» из заголовков задач.Значение «Не решена» в двух последних столбцах означает, что программене удалось решить задачу.
Значение «–» означает, что для задачи отсутствуютрезультаты тестирования программы. Все времена в таблице указаны в секундах.Таблица Г.1. Результаты программы WhaleProver на задачах из ILTPЗадачаВремя Результат Статус ILTP Статус TPTP Время ileanCoP Время ImogenALG028+1 11,29 ТеоремаТеорема0,0358,85ТеоремаALG171+10,63Теорема НеизвестенНе решена–ТеоремаALG173+15,51Теорема НеизвестенНерешена–ТеоремаALG198+10,37ТеоремаТеорема0,030,14ТеоремаALG199+14,89ТеоремаТеорема17,050,55ТеоремаALG200+13,1ТеоремаТеорема0,030,78ТеоремаCOM003+10,19ТеоремаТеоремаНе решена118,9ТеоремаCOM003+22,33ТеоремаТеорема25,060,6ТеоремаCOM003+30,07ТеоремаТеоремаНе решена–ТеоремаGEJ001+10,1ТеоремаТеорема0,030,05Неизвестен205ЗадачаGEJ001+2GEJ001+3GEJ002+1GEJ002+2GEJ003+1GEJ003+2GEJ004+1GEJ004+2GEJ004+3GEJ005+1GEJ005+2GEJ005+3GEJ006+1GEJ006+2GEJ007+1GEJ007+2GEJ007+3GEJ007+4GEJ008+1GEJ008+2GEJ009+1GEJ009+2GEJ009+3GEJ009+4GEJ010+3GEJ013+1GEJ013+2GEJ014+1GEJ014+2GEJ015+1GEJ015+2GEJ016+1GEJ016+2GEJ017+1GEJ017+2GEJ018+1GEJ018+2GEJ019+1GEJ019+2GEJ020+1GEJ020+2GEJ021+1GEJ021+2GEJ022+2GEJ023+1Время Результат Статус ILTP0,65ТеоремаТеорема0,06ТеоремаТеорема0,02ТеоремаТеорема0,01ТеоремаТеорема8,6ТеоремаТеорема3,12ТеоремаТеорема0,66ТеоремаТеорема1,05ТеоремаТеорема0,18ТеоремаТеорема1,13ТеоремаТеорема1,26ТеоремаТеорема0,02ТеоремаТеорема17,64 ТеоремаТеорема5,61ТеоремаТеорема0,72ТеоремаТеорема0,03ТеоремаТеорема0,02ТеоремаТеорема0,01ТеоремаТеорема27,2ТеоремаТеорема30,78 ТеоремаТеорема13,7ТеоремаТеорема0,03ТеоремаТеорема0,03ТеоремаТеорема0,01ТеоремаТеорема0,05ТеоремаТеорема1,61ТеоремаТеорема7,4Теорема Неизвестен0,09ТеоремаТеорема1,16Теорема Неизвестен0,15ТеоремаТеорема0,85ТеоремаТеорема0,13ТеоремаТеорема0,02ТеоремаТеорема21,09 ТеоремаТеорема8,68ТеоремаТеорема11,02 Теорема Неизвестен18,35 Теорема Неизвестен43,21 ТеоремаТеорема30,44 ТеоремаТеорема40,28 ТеоремаТеорема28,58 ТеоремаТеорема8,17ТеоремаТеорема15,18 Теорема Неизвестен5,99ТеоремаТеорема8,8Теорема НеизвестенСтатус TPTP Время ileanCoP Время Imogen0,080,02Неизвестен0,010,02Неизвестен0,090,41Неизвестен0,010,01Неизвестен0,130,11Неизвестен0,070,06Неизвестен0,031Неизвестен0,160,09Неизвестен0,010,36Неизвестен10,430,21Неизвестен6,320,09Неизвестен0,050,02Неизвестен0,190,28Неизвестен0,112,96Неизвестен16,590,02Неизвестен0,250,02Неизвестен0,050,03Неизвестен0,020,01Неизвестен46,8221,24Неизвестен112,577,13Неизвестен0,020,01Неизвестен0,010,01Неизвестен0,010,02Неизвестен0,010,02Неизвестен0,060,08Неизвестен0,2417,21НеизвестенНе решена–Неизвестен95,030,02НеизвестенНе решена0,04Неизвестен0,020,16Неизвестен0,130,08Неизвестен15,390,03НеизвестенНе решена0,02Неизвестен0,190,16Неизвестен0,10,07НеизвестенНе решена0,2НеизвестенНе решена0,54Неизвестен22,520,63Неизвестен3,238,06Неизвестен0,220,09Неизвестен3,010,17Неизвестен20,7927,88НеизвестенНе решена0,81Неизвестен5,653,69НеизвестенНе решена5,72Неизвестен206ЗадачаGEJ024+1GEJ025+1GEJ027+1GEJ027+2GEJ028+1GEJ028+2GEJ029+1GEJ029+2GEJ030+1GEJ030+2GEJ031+1GEJ031+2GEJ032+1GEJ032+2GEJ033+1GEJ033+2GEJ034+1GEJ034+2GEJ035+1GEJ035+2GEJ036+2GEJ038+1GEJ038+2GEJ039+1GEJ039+2GEJ041+2GEJ042+1GEJ042+2GEJ047+1GEJ047+2GEJ051+1GEJ051+2GEJ052+1GEJ052+2GEJ060+1GEJ061+1GEJ062+1GEJ063+1GEJ064+1GEJ065+1GEJ066+1GEJ067+1GEJ068+1GEJ069+1GEJ070+1Время Результат Статус ILTP12,77 ТеоремаТеорема50,14 ТеоремаТеорема46,4Теорема Неизвестен12,94 Теорема Неизвестен9,97ТеоремаТеорема55,66 ТеоремаТеорема44,83 ТеоремаТеорема67,55 ТеоремаТеорема14,62 Теорема Неизвестен37,78 Теорема Неизвестен0,23ТеоремаТеорема0,1ТеоремаТеорема6,04ТеоремаТеорема0,95ТеоремаТеорема56,19 ТеоремаТеорема3,28ТеоремаТеорема0,08ТеоремаТеорема0,68ТеоремаТеорема38,34 ТеоремаТеорема24,88 ТеоремаТеорема19,22 ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,03ТеоремаТеорема0,03ТеоремаТеорема0,09Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,03Теорема Неизвестен0,03Теорема Неизвестен0,05Теорема Неизвестен0,05Теорема Неизвестен0,02Теорема Неизвестен0,03Теорема Неизвестен0,01Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,02Теорема Неизвестен0,03Теорема НеизвестенСтатус TPTP Время ileanCoP Время Imogen0,31Не решенаНеизвестен0,33,36НеизвестенНе решена0,32НеизвестенНе решена0,54Неизвестен0,328,31Неизвестен0,170,17Неизвестен0,290,49Неизвестен0,1250,33НеизвестенНе решена–НеизвестенНе решена–Неизвестен0,10,14Неизвестен1,990,09Неизвестен67,920,25Неизвестен588,385,58Неизвестен0,50,35Неизвестен4,741,21Неизвестен0,060,18Неизвестен2,840,11Неизвестен52,150,37Неизвестен60,990,68Неизвестен58,3711,55Неизвестен0,010,01Неизвестен0,010,02Неизвестен0,020,02Неизвестен0,020,02Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен207ЗадачаGEJ071+1GEJ072+1GEJ073+1GEJ074+1GEJ075+1GEJ076+1GEJ077+1GEJ078+1GEJ079+1GEJ080+1GEJ081+1GEJ082+1GEJ083+1GEJ084+1GEJ085+1GEJ086+1GEJ087+1GEJ088+1GEJ089+1GEJ090+1GEJ091+1GEJ092+1GEJ093+1GEJ094+1GEJ095+1GEJ096+1GEJ097+1GEO080+1GPJ001+2GPJ002+1GPJ003+1HAL003+3KRS018+1KRS019+1KRS020+1KRS021+1KRS022+1KRS023+1KRS024+1KRS025+1KRS026+1KRS027+1KRS053+1KRS054+1KRS055+1Время0,030,020,020,020,020,020,020,020,020,030,020,020,020,020,020,030,030,030,030,030,030,030,030,030,030,030,020,270,060,030,4310,960,030,010,160,010,010,010,010,010,050,010,030,010,01РезультатТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаСтатус ILTPНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаТеоремаТеоремаТеоремаНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенСтатус TPTP Время ileanCoP Время Imogen––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен0,0650,04ТеоремаНе решена57,86Неизвестен0,010,47Неизвестен0,0157,13НеизвестенНерешена–ТеоремаНе решена0,01Не теоремаНе решена0,02Не теоремаНе решена1,48Не теоремаНе решена0,01Не теоремаНе решена0,01НеизвестенНе решена0,01Не теоремаНе решена0,01Не теоремаНерешена0,01Не теоремаНе решена0,06Не теоремаНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теорема208ЗадачаKRS056+1KRS058+1KRS059+1KRS060+1KRS061+1KRS062+1KRS063+1KRS064+1KRS065+1KRS066+1KRS067+1KRS068+1KRS072+1KRS074+1KRS077+1KRS078+1KRS082+1KRS084+1KRS085+1KRS086+1KRS087+1KRS089+1KRS090+1KRS091+1KRS092+1KRS093+1KRS094+1KRS095+1KRS096+1KRS097+1KRS099+1KRS100+1KRS105+1KRS106+1KRS110+1KRS113+1KRS114+1KRS118+1KRS119+1KRS120+1KRS121+1KRS122+1KRS123+1KRS124+1KRS125+1Время0,010,030,010,010,010,010,150,010,010,010,010,011,030,0312,771,050,1675,680,210,470,217,490,020,010,010,010,010,040,294,780,220,020,0190,550,461,391,6556,341,5311,71,524,760,010,020,01РезультатНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаСтатус ILTPНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНеизвестенНеизвестенТеоремаНеизвестенТеоремаТеоремаТеоремаНеизвестенТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаТеоремаТеоремаСтатус TPTP Время ileanCoP Время ImogenНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теоремаНе решена0,01Не теорема0,010,03Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,040,02Теорема0,010,01Теорема285,681,25Теорема0,010,02ТеоремаНе решена55,63ТеоремаНерешена–Теорема0,020,86ТеоремаНе решена–Теорема0,230,19Теорема21,1358,18Теорема0,210,16ТеоремаНе решена–Теорема0,030,04Теорема0,010,01Теорема0,010,03Теорема0,010,01Теорема0,010,01Теорема0,020,05Теорема0,0635,46Теорема0,7468,19Теорема1,124,26Теорема0,080,03Теорема0,020,01Теорема4,52–Теорема0,170,02ТеоремаНе решена–ТеоремаНе решена0,48ТеоремаНе решена–ТеоремаНе решена1,63ТеоремаНерешена–ТеоремаНе решена2,58ТеоремаНе решена–Теорема0,010,01Теорема0,030,02Теорема0,010,01Теорема209ЗадачаKRS126+1KRS127+1KRS128+1KRS129+1KRS130+1KRS131+1KRS132+1KRS133+1KRS134+1KRS135+1KRS136+1KRS137+1KRS139+1KRS141+1KRS142+1KRS143+1KRS144+1KRS145+1KRS150+1KRS152+1KRS163+1KRS164+1KRS165+1KRS166+1KRS167+1KRS168+1KRS169+1KRS170+1KRS171+1KRS172+1KRS173+1KRS174+1KRS175+1LCL181+1LCL230+1LCL414+1MGT003+1MGT008+1MGT015+1MGT016+1MGT017+1MGT018+1MGT022+1MGT022+2MGT023+1Время0,010,510,050,530,010,020,3732,580,010,010,010,010,010,010,040,130,221,160,110,040,040,010,010,010,360,010,010,010,010,180,010,080,090,010,010,010,415,541,681,691,681,680,010,010,61РезультатТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаСтатус ILTP Статус TPTP Время ileanCoP Время ImogenТеорема0,010,01ТеоремаТеорема0,150,09ТеоремаТеорема0,020,03ТеоремаНеизвестенНе решена57,52ТеоремаТеоремаНе решена0,02ТеоремаТеоремаНе решена0,02ТеоремаНеизвестенНе решена2,27ТеоремаНеизвестенНерешена–ТеоремаТеоремаНе решена0,01ТеоремаТеоремаНе решена0,01ТеоремаТеорема0,880,03ТеоремаТеорема32,70,03ТеоремаТеорема8,990,02ТеоремаТеорема0,540,01ТеоремаНеизвестенНе решена0,04ТеоремаНеизвестенНерешена0,04ТеоремаНеизвестенНе решена0,05ТеоремаНеизвестенНе решена0,05ТеоремаНеизвестенНе решена0,57ТеоремаТеоремаНе решена0,09ТеоремаНеизвестенНе решена0,02ТеоремаТеорема31,110,02ТеоремаТеоремаНе решена0,02ТеоремаТеоремаНе решена0,04ТеоремаНеизвестенНерешена5,48ТеоремаТеоремаНе решена0,02ТеоремаТеорема9,280,03ТеоремаТеоремаНе решена0,03ТеоремаТеоремаНе решена0,02ТеоремаНеизвестенНе решена0,17ТеоремаНеизвестен Не теоремаНе решена–НеизвестенНерешена50,72ТеоремаНеизвестенНе решена41,2ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,09ТеоремаНеизвестенНе решена55,66ТеоремаТеорема1,4857,85ТеоремаТеорема0,1658,11ТеоремаТеорема0,2758,22ТеоремаТеорема0,1757,93ТеоремаТеорема0,2857,1ТеоремаТеорема0,160,03ТеоремаТеорема0,130,03ТеоремаНеизвестенНе решена57,95Теорема210ЗадачаMGT023+2MGT028+1MGT030+1MGT032+2MGT036+1MGT036+2MGT036+3MGT041+2MGT045+1MGT052+1MGT053+1MGT059+1NLP001+1NLP026+1NLP027+1NLP028+1NLP029+1NLP030+1NLP031+1NLP032+1NLP033+1NLP034+1NLP035+1NLP043+1NLP044+1NLP045+1NLP046+1NLP047+1NLP048+1NLP059+1NLP060+1NLP061+1NLP062+1NLP063+1NLP064+1NLP065+1NLP066+1NLP067+1NLP068+1NLP079+1NLP080+1NLP081+1NLP094+1NLP095+1NLP096+1Время0,980,010,010,010,040,040,010,020,670,020,0716,170,030,090,090,10,090,10,090,080,090,10,090,10,10,110,090,090,10,050,110,090,060,150,130,10,040,040,041,21,090,690,060,070,07РезультатТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаСтатус ILTPНеизвестенТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНеизвестенНеизвестенТеоремаТеоремаНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаТеоремаТеоремаТеоремаНеизвестенНеизвестенСтатус TPTP Время ileanCoP Время ImogenНе решена57,11Теорема0,240,01ТеоремаНе решена0,03Теорема0,010,01Теорема0,020,71Теорема0,030,98Теорема0,010,01Теорема0,010,01Теорема0,020,31ТеоремаНе решена0,11ТеоремаНе решена56,38Теорема0,110,43Теорема3,5856,37ТеоремаНе решена0,07Не теоремаНе решена0,13Не теоремаНерешена0,12Не теоремаНе решена0,09Не теоремаНе решена0,08Не теоремаНе решена0,05Не теоремаНе решена0,06Не теоремаНе решена0,02Не теоремаНе решена0,13Не теоремаНе решена0,07Не теоремаНе решена18Не теоремаНерешена14,14Не теоремаНе решена12,54Не теоремаНе решена2,78Не теоремаНе решена3,08Не теоремаНе решена2,95Не теоремаНе решена0,27Не теоремаНе решена0,74Не теоремаНерешена6,22Не теоремаНе решена0,16Не теоремаНе решена–Не теоремаНе решена0,65Не теоремаНе решена0,46Не теоремаНе решена0,12Не теоремаНе решена0,15Не теоремаНе решена0,1Не теоремаНерешена–ТеоремаНе решена–ТеоремаНе решена0,59ТеоремаНе решена0,08ТеоремаНе решена0,09Не теоремаНе решена0,08Не теорема211ЗадачаNLP097+1NLP098+1NLP099+1NLP100+1NLP101+1NLP102+1NLP103+1NLP114+1NLP115+1NLP116+1NLP117+1NLP118+1NLP119+1NLP120+1NLP121+1NLP122+1NLP123+1NLP130+1NLP131+1NLP132+1NLP133+1NLP134+1NLP135+1NLP136+1NLP137+1NLP138+1NLP139+1NLP160+1NLP161+1NLP162+1NLP163+1NLP164+1NLP165+1NLP166+1NLP167+1NLP168+1NLP169+1NLP198+1NLP204+1NLP208+1NLP221+1NLP222+1NLP223+1PUZ031+1PUZ047+1Время0,090,080,130,080,070,080,070,120,110,030,220,080,090,10,030,060,10,090,120,10,090,10,080,210,150,210,157,811,0618,7349,5460,1766,392,258,2411,0933,5473,243,7540,60,110,110,090,2176,3РезультатНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаСтатус ILTPНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаНеизвестенНеизвестенНеизвестенНеизвестенТеоремаНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенНеизвестенТеоремаТеоремаСтатус TPTP Время ileanCoP Время ImogenНе решена0,07Не теоремаНе решена0,08Не теоремаНе решена0,08Не теоремаНе решена0,07Не теоремаНе решена0,07Не теоремаНе решена0,08Не теоремаНе решена0,08Не теоремаНерешена0,17Не теоремаНе решена0,18Не теоремаНе решена0,22Не теорема70,360,15ТеоремаНе решена0,14Не теоремаНе решена0,14Не теоремаНе решена0,17Не теоремаНе решена0,25Не теорема71,580,11ТеоремаНе решена0,17Не теоремаНе решена1,7Не теоремаНе решена11,89Не теоремаНе решена4,76Не теоремаНе решена4,71Не теоремаНе решена10,74Не теоремаНе решена1,66Не теоремаНе решена1,34Не теоремаНерешена2,45Не теоремаНе решена1,29Не теоремаНе решена2,4Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНерешена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–ТеоремаНерешена–ТеоремаНе решена–Не теоремаНе решена–Не теоремаНе решена–Не теорема0,74–Теорема0,020,02Теорема212ЗадачаPUZ060+1PUZ061+1SET002+3SET002+4SET019+4SET027+3SET043+1SET044+1SET045+1SET046+1SET047+1SET062+3SET062+4SET063+3SET063+4SET146+3SET148+3SET148+4SET194+3SET196+3SET347+4SET366+4SET573+3SET574+3SET575+3SET576+3SET583+3SET585+3SET590+3SET602+3SET602+4SET604+3SET605+3SET618+3SET627+3SET630+3SET643+3SET687+4SET705+4SET786+1SET788+1SWC128+1SWV010+1SWV011+1SWV022+1Время Результат Статус ILTP Статус TPTP Время ileanCoP Время Imogen0,01ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема0,010,01Теорема0,02ТеоремаТеорема0,010,06Теорема7,86ТеоремаТеорема386,6–Теорема0,12ТеоремаТеорема0,014,55Теорема0,02ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема0,010,01Теорема0,02ТеоремаТеорема0,010,02Теорема0,01ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема0,010,03Теорема0,01ТеоремаТеоремаНе решена0,06Теорема0,01ТеоремаТеорема0,0153,44Теорема0,1ТеоремаТеорема0,0190,76Теорема0,02ТеоремаТеорема0,010,02Теорема7,24ТеоремаТеорема384,81–Теорема0,14ТеоремаТеорема83,4852,73Теорема0,02ТеоремаТеорема0,020,01Теорема10,31 ТеоремаТеорема380,34–Теорема0,04ТеоремаТеорема0,2211,4Теорема0,03ТеоремаТеорема0,2252,69Теорема7,25ТеоремаТеорема363,2–Теорема57,04 ТеоремаТеорема0,09–Теорема0,01ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема0,010,01Теорема0,01ТеоремаТеорема87,030,01Теорема0,01ТеоремаТеорема0,010,01Теорема0,06ТеоремаТеорема0,0252,56Теорема0,01ТеоремаТеорема0,0466,85Теорема0,02ТеоремаТеорема0,0253,32Теорема7,29ТеоремаТеорема387,23–Теорема0,02ТеоремаТеорема0,0253,12Теорема0,09ТеоремаТеорема0,0457,98Теорема9,29ТеоремаТеорема0,31–Теорема0,01ТеоремаТеорема0,010,04Теорема4,63ТеоремаТеорема1,53–Теорема0,89ТеоремаТеорема539,61–Теорема0,09ТеоремаТеорема0,0395,36Теорема57,38 ТеоремаТеорема0,94–Теорема0,01ТеоремаТеорема0,010,01Теорема0,02ТеоремаТеоремаНе решена0,04Теорема0,03ТеоремаТеоремаТеорема0,020,020,01 Не теорема Не теорема Не теорема0,010,010,01ТеоремаТеорема0,010,01Теорема0,17ТеоремаТеорема0,020,06Теорема213ЗадачаSWV023+1SWV043+1SWV045+1SWV047+1SWV054+1SWV057+1SWV058+1SWV059+1SWV060+1SWV061+1SWV063+1SWV066+1SWV068+1SWV070+1SWV071+1SWV072+1SWV073+1SWV074+1SWV075+1SWV076+1SWV078+1SWV080+1SWV081+1SWV082+1SWV083+1SWV084+1SWV085+1SWV086+1SWV087+1SWV088+1SWV105+1SWV106+1SWV107+1SWV119+1SWV121+1SWV123+1SWV126+1SWV128+1SWV131+1SWV132+1SWV145+1SWV146+1SWV147+1SWV148+1SWV149+1Время Результат Статус ILTP Статус TPTP Время ileanCoP Время Imogen0,17ТеоремаТеорема0,020,05Теорема0,19ТеоремаТеорема0,020,06Теорема0,19ТеоремаТеорема0,010,06Теорема0,19ТеоремаТеорема0,010,05Теорема0,17ТеоремаТеорема0,010,06Теорема0,18ТеоремаТеорема0,010,06Теорема0,18ТеоремаТеорема0,020,05Теорема8,16ТеоремаТеорема0,020,07Теорема0,17ТеоремаТеорема0,020,06Теорема7,9ТеоремаТеорема0,020,06Теорема45,73 ТеоремаТеорема0,010,09Теорема45,9ТеоремаТеорема0,020,08Теорема0,17ТеоремаТеорема0,020,05Теорема9,22ТеоремаТеорема0,010,07Теорема45,25 ТеоремаТеорема0,020,09Теорема8,5ТеоремаТеорема0,010,06Теорема45,23 ТеоремаТеорема0,020,09Теорема46,25 ТеоремаТеорема0,020,09Теорема45,51 ТеоремаТеорема0,010,1Теорема8,58ТеоремаТеорема0,010,07Теорема17,4ТеоремаТеорема0,010,08Теорема9,56ТеоремаТеорема0,010,06Теорема9,83ТеоремаТеорема0,010,06Теорема9,76ТеоремаТеорема0,020,06Теорема9,82ТеоремаТеорема0,010,07Теорема9,6ТеоремаТеорема0,010,06Теорема9,2ТеоремаТеорема0,010,07Теорема0,19ТеоремаТеорема0,020,05Теорема8,37ТеоремаТеорема0,020,07Теорема0,18ТеоремаТеорема0,020,04Теорема0,21ТеоремаТеорема0,020,05Теорема0,19ТеоремаТеорема0,020,04Теорема0,22ТеоремаТеорема0,020,05Теорема0,21ТеоремаТеорема0,010,06Теорема0,2ТеоремаТеорема0,020,05Теорема0,2ТеоремаТеорема0,020,06Теорема0,19ТеоремаТеорема0,020,07Теорема0,2ТеоремаТеорема0,010,04Теорема10,39 ТеоремаТеорема0,030,05Теорема11,14 ТеоремаТеорема0,040,05Теорема0,21ТеоремаТеорема0,020,04Теорема0,18ТеоремаТеорема0,020,04Теорема0,18ТеоремаТеорема0,020,04Теорема0,18ТеоремаТеорема0,030,04Теорема0,18ТеоремаТеорема0,020,04Теорема214ЗадачаSWV150+1SWV155+1SWV159+1SWV169+1SWV171+1SWV172+1SWV179+1SWV180+1SWV183+1SWV186+1SWV211+1SWV212+1SWV213+1SWV214+1SWV215+1SWV216+1SWV217+1SWV218+1SWV219+1SWV220+1SWV222+1SWV223+1SWV224+1SWV225+1SWV226+1SWV227+1SWV228+1SWV229+1SWV230+1SWV231+1SWV232+1SYJ001+1.001SYJ001+1.002SYJ001+1.003SYJ001+1.004SYJ001+1.005SYJ001+1.006SYJ001+1.007SYJ001+1.008SYJ001+1.009SYJ001+1.010SYJ001+1.011SYJ001+1.012SYJ001+1.013SYJ001+1.014Время Результат Статус ILTP0,18ТеоремаТеорема26,18 ТеоремаТеорема30,44 ТеоремаТеорема23,94 ТеоремаТеорема24,92 ТеоремаТеорема22,62 ТеоремаТеорема19,93 ТеоремаТеорема21,2ТеоремаТеорема20,85 ТеоремаТеорема23,47 ТеоремаТеорема16,12 ТеоремаТеорема15,17 ТеоремаТеорема15,43 ТеоремаТеорема16,31 ТеоремаТеорема15,87 ТеоремаТеорема17,06 ТеоремаТеорема16,08 ТеоремаТеорема15,26 ТеоремаТеорема15,39 ТеоремаТеорема17,05 ТеоремаТеорема14,48 ТеоремаТеорема14,7ТеоремаТеорема14,5ТеоремаТеорема14,48 ТеоремаТеорема15,16 ТеоремаТеорема14,7ТеоремаТеорема14,98 ТеоремаТеорема15,11 ТеоремаТеорема14,52 ТеоремаТеорема14,71 ТеоремаТеорема14,42 ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,02Теорема Неизвестен0,02ТеоремаТеорема0,02Теорема Неизвестен0,03ТеоремаТеорема0,03Теорема Неизвестен0,04ТеоремаТеоремаСтатус TPTP Время ileanCoP Время Imogen0,020,04Теорема0,040,06Теорема0,040,05Теорема0,030,04Теорема0,020,04Теорема0,020,04Теорема0,020,04Теорема0,020,04Теорема0,030,04Теорема0,030,04Теорема0,030,05Теорема0,060,05Теорема0,030,05Теорема0,040,05Теорема0,030,05Теорема0,040,04Теорема0,040,04Теорема0,020,05Теорема0,030,04Теорема0,040,04Теорема0,030,05Теорема0,040,05Теорема0,040,04Теорема0,040,05Теорема0,040,04Теорема0,050,04Теорема0,050,04Теорема0,030,04Теорема0,040,04Теорема0,040,04Теорема0,030,04Теорема––Неизвестен0,010,01Неизвестен––Неизвестен0,070,02Неизвестен––Неизвестен0,380,04Неизвестен––Неизвестен1,620,26Неизвестен––Неизвестен4,7911,32Неизвестен––Неизвестен12,6652,92Неизвестен––Неизвестен29,4654,39Неизвестен215ЗадачаSYJ001+1.015SYJ001+1.016SYJ001+1.017SYJ001+1.018SYJ001+1.019SYJ001+1.020SYJ002+1.001SYJ002+1.002SYJ002+1.003SYJ002+1.004SYJ002+1.005SYJ002+1.006SYJ002+1.007SYJ002+1.008SYJ002+1.009SYJ002+1.010SYJ002+1.011SYJ002+1.012SYJ002+1.013SYJ002+1.014SYJ002+1.015SYJ002+1.016SYJ002+1.017SYJ002+1.018SYJ002+1.019SYJ002+1.020SYJ003+1.001SYJ003+1.002SYJ003+1.003SYJ003+1.004SYJ003+1.005SYJ003+1.006SYJ003+1.007SYJ003+1.008SYJ003+1.009SYJ003+1.010SYJ003+1.011SYJ003+1.012SYJ004+1.001SYJ004+1.002SYJ004+1.003SYJ004+1.004SYJ004+1.005SYJ004+1.006SYJ004+1.007Время Результат Статус ILTP0,04Теорема Неизвестен0,05ТеоремаТеорема0,05Теорема Неизвестен0,06Теорема Неизвестен0,09Теорема Неизвестен0,1Теорема Неизвестен0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,02Теорема Неизвестен0,02ТеоремаТеорема0,02Теорема Неизвестен0,03ТеоремаТеорема0,03Теорема Неизвестен0,03ТеоремаТеорема0,04Теорема Неизвестен0,05ТеоремаТеорема0,06Теорема Неизвестен0,06Теорема Неизвестен0,07Теорема Неизвестен0,08Теорема Неизвестен0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,02ТеоремаТеорема0,02Теорема Неизвестен0,03ТеоремаТеорема0,16Теорема Неизвестен30,05 ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема НеизвестенСтатус TPTP Время ileanCoP Время Imogen––Неизвестен62,23–Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен0,010,02Неизвестен––Неизвестен0,070,02Неизвестен––Неизвестен0,420,05Неизвестен––Неизвестен1,520,36Неизвестен––Неизвестен4,910,81Неизвестен––Неизвестен12,786,32Неизвестен––Неизвестен29,952,87Неизвестен––Неизвестен62,9354,41Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен0,010,02Неизвестен––Неизвестен0,010,03Неизвестен––Неизвестен0,010,66Неизвестен––Неизвестен0,0122,02Неизвестен––Неизвестен0,01Не решенаНеизвестен––Неизвестен0,01–Неизвестен––Неизвестен0,010,02Неизвестен––Неизвестен0,010,02Неизвестен––Неизвестен0,010,02Неизвестен––Неизвестен216ЗадачаSYJ004+1.008SYJ004+1.009SYJ004+1.010SYJ004+1.011SYJ004+1.012SYJ004+1.013SYJ004+1.014SYJ004+1.015SYJ004+1.016SYJ004+1.017SYJ004+1.018SYJ004+1.019SYJ004+1.020SYJ013+1SYJ014+1SYJ015+1SYJ016+1SYJ017+1SYJ019+1SYJ020+1SYJ021+1SYJ022+1SYJ023+1SYJ024+1SYJ025+1SYJ026+1SYJ027+1SYJ028+1SYJ029+1SYJ030+1SYJ031+1SYJ032+1SYJ033+1SYJ034+1SYJ035+1SYJ038+1SYJ039+1SYJ101+1SYJ102+1SYJ103+1SYJ104+1SYJ105+1.002SYJ105+1.003SYJ105+1.004SYJ106+1Время Результат Статус ILTP0,02ТеоремаТеорема0,01Теорема Неизвестен0,02ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,01ТеоремаТеорема0,01Теорема Неизвестен0,03ТеоремаТеорема0,02Теорема Неизвестен0,01Теорема Неизвестен0,01Теорема Неизвестен0,01Теорема Неизвестен0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,02ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,29ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеорема0,01ТеоремаТеоремаСтатус TPTP Время ileanCoP Время Imogen0,010,02Неизвестен––Неизвестен0,010,03Неизвестен––Неизвестен0,010,03Неизвестен––Неизвестен0,011,33Неизвестен––Неизвестен0,020,02Неизвестен––Неизвестен––Неизвестен––Неизвестен––Неизвестен0,010,01Неизвестен0,020,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,040,09Неизвестен0,050,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,620,01НеизвестенНе решена0,02Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,070,01Неизвестен0,010,01Неизвестен0,017,82Неизвестен0,0456,16Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен217ЗадачаSYJ107+1.001SYJ107+1.002SYJ107+1.003SYJ107+1.004SYJ108+1SYJ109+1SYJ110+1SYJ111+1SYJ112+1SYJ113+1SYJ114+1SYJ115+1SYJ116+1.001SYJ116+1.002SYJ116+1.003SYJ116+1.004SYJ117+1SYJ118+1SYJ119+1SYJ120+1SYJ121+1SYJ122+1SYJ123+1SYJ124+1SYJ125+1SYJ201+1.002SYJ202+1.002SYJ203+1.002SYJ203+1.006SYJ203+1.010SYJ204+1.002SYJ204+1.006SYJ204+1.010SYJ205+1.002SYJ205+1.006SYJ205+1.010SYJ206+1.002SYJ207+1.002SYJ208+1.002SYJ208+1.006SYJ209+1.002SYJ209+1.006SYJ209+1.010SYJ210+1.002SYJ210+1.006Время0,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,040,370,010,010,020,050,010,010,010,010,010,020,010,180,020,210,010,010,040,010,02РезультатТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаСтатус ILTPТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНеизвестенТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаСтатус TPTP Время ileanCoP Время Imogen0,010,01Неизвестен0,010,01Неизвестен0,010,02Неизвестен0,010,02Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,02Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,02Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,020,03НеизвестенНе решена0,04Неизвестен0,010,04Неизвестен0,010,01НеизвестенНе решена0,02НеизвестенНе решена0,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен0,050,02НеизвестенНе решена0,01НеизвестенНе решена0,01НеизвестенНе решена0,01НеизвестенНе решена0,03НеизвестенНе решена0,01Неизвестен0,010,02НеизвестенНерешена2,01НеизвестенНе решена0,01НеизвестенНе решена0,01НеизвестенНе решена0,01Неизвестен0,010,01Неизвестен0,010,01Неизвестен218ЗадачаSYJ210+1.010SYJ211+1.002SYJ211+1.006SYJ211+1.010SYJ212+1.002SYN001+1SYN036+1SYN036+2SYN040+1SYN041+1SYN044+1SYN045+1SYN046+1SYN047+1SYN048+1SYN049+1SYN050+1SYN051+1SYN052+1SYN053+1SYN054+1SYN055+1SYN056+1SYN057+1SYN058+1SYN059+1SYN060+1SYN061+1SYN062+1SYN063+1SYN064+1SYN065+1SYN066+1SYN067+1SYN068+1SYN069+1SYN070+1SYN071+1SYN072+1SYN073+1SYN074+1SYN075+1SYN078+1SYN079+1SYN080+1Время0,070,010,020,070,010,010,136,810,010,010,010,010,010,010,010,010,010,030,010,010,020,010,010,010,010,010,010,010,010,010,010,010,010,020,010,010,020,1964,320,010,040,0223,940,010,01РезультатНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаСтатус ILTPНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНеизвестенНе теоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНеизвестенТеоремаНеизвестенНеизвестенТеоремаТеоремаТеоремаТеоремаТеоремаНеизвестенТеоремаТеоремаНеизвестенНе теоремаТеоремаТеоремаНеизвестенТеоремаТеоремаНеизвестенТеоремаНеизвестенНе теоремаНеизвестенНеизвестенТеоремаТеоремаТеоремаСтатус TPTP Время ileanCoP Время Imogen0,090,01Неизвестен0,010,02Неизвестен0,070,01Неизвестен7,350,01НеизвестенНе решена0,01Неизвестен0,010,01ТеоремаНе решена0,04ТеоремаНерешена0,02ТеоремаНе решена0,01Теорема0,010,01Теорема0,290,01ТеоремаНе решена0,02ТеоремаНе решена0,01ТеоремаНе решена0,01Теорема0,010,01Теорема0,010,01Теорема0,010,01ТеоремаНе решена0,01Теорема0,030,01ТеоремаНе решена0,01ТеоремаНе решена0,01Теорема0,010,01ТеоремаНе решена0,01Теорема0,010,02Теорема0,010,01ТеоремаНе решена0,02ТеоремаНе решена0,01Теорема0,010,01Теорема0,010,01ТеоремаНе решена0,01Теорема0,010,01Теорема0,010,01Теорема0,010,01ТеоремаНе решена0,01Теорема0,010,01Теорема0,010,02ТеоремаНе решена0,09Теорема40,660,03ТеоремаНе решена0,88Теорема0,010,01ТеоремаНе решена60,14ТеоремаНе решена58,25ТеоремаНе решена0,02Теорема0,010,01Теорема0,010,01Теорема219ЗадачаSYN082+1SYN083+1SYN315+1SYN316+1SYN317+1SYN318+1SYN320+1SYN321+1SYN322+1SYN323+1SYN324+1SYN325+1SYN326+1SYN327+1SYN329+1SYN333+1SYN336+1SYN337+1SYN338+1SYN339+1SYN340+1SYN341+1SYN342+1SYN343+1SYN344+1SYN345+1SYN346+1SYN355+1SYN356+1SYN357+1SYN358+1SYN359+1SYN360+1SYN361+1SYN362+1SYN363+1SYN364+1SYN365+1SYN366+1SYN367+1SYN368+1SYN369+1SYN370+1SYN371+1SYN372+1Время0,010,010,030,010,010,010,010,010,010,010,020,010,010,010,010,010,010,010,010,010,010,010,010,010,020,010,010,020,010,010,010,010,010,010,010,010,0182,880,010,010,010,010,010,010,01РезультатТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаСтатус ILTPТеоремаТеоремаНеизвестенНе теоремаНеизвестенНе теоремаНе теоремаТеоремаНеизвестенТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаНеизвестенНе теоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаСтатус TPTP Время ileanCoP Время Imogen0,040,01Теорема0,010,02ТеоремаНе решена0,01Теорема0,010,01Не теоремаНе решена0,01Теорема0,010,01Теорема0,010,01Не теорема0,040,01ТеоремаНе решена0,01Не теорема0,010,01Теорема0,010,02Не теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Не теорема0,010,01Теорема0,010,01Теорема0,010,01Не теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Не теорема0,010,01ТеоремаНерешена0,01Не теорема0,010,02Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,02Теорема0,010,02Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема0,010,01Теорема220ЗадачаSYN373+1SYN374+1SYN375+1SYN376+1SYN377+1SYN378+1SYN379+1SYN380+1SYN381+1SYN382+1SYN383+1SYN384+1SYN385+1SYN386+1SYN387+1SYN388+1SYN389+1SYN390+1SYN391+1SYN392+1SYN393+1SYN394+1SYN395+1SYN396+1SYN397+1SYN398+1SYN399+1SYN400+1SYN401+1SYN402+1SYN403+1SYN404+1SYN405+1SYN406+1SYN407+1SYN408+1SYN409+1SYN410+1SYN411+1SYN412+1SYN413+1SYN414+1SYN415+1SYN416+1SYN549+1Время0,060,010,010,070,010,020,010,010,010,010,010,010,010,010,010,010,010,010,010,010,210,010,020,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,040,010,04РезультатНе теоремаТеоремаТеоремаНе теоремаТеоремаНе теоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаНе теоремаТеоремаСтатус ILTP Статус TPTP Время ileanCoP Время ImogenНеизвестенНе решена0,01ТеоремаТеоремаНе решена0,02ТеоремаТеоремаНе решена0,02ТеоремаНеизвестенНе решена0,01ТеоремаТеоремаНе решена0,02ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,012,5ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,04ТеоремаНе теоремаНе решена0,01ТеоремаНе теоремаНе решена0,02ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,02ТеоремаТеорема0,020,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,02ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,02ТеоремаНе теорема Не теорема0,010,01ТеоремаНе решена0,02ТеоремаНе теорема0,010,01ТеоремаТеоремаНе решена0,03Теорема221ЗадачаSYN550+1SYN721+1SYN722+1SYN724+1SYN725+1SYN727+1SYN728+1SYN729+1SYN730+1SYN731+1SYN732+1SYN733+1SYN915+1SYN916+1SYN917+1SYN918+1SYN919+1SYN920+1SYN921+1SYN922+1SYN923+1SYN924+1SYN925+1SYN926+1SYN927+1SYN928+1SYN929+1SYN930+1SYN931+1SYN932+1SYN933+1SYN934+1SYN935+1SYN936+1SYN937+1SYN938+1SYN939+1SYN940+1SYN941+1SYN942+1SYN943+1SYN944+1SYN945+1SYN946+1SYN947+1Время0,060,010,010,010,010,010,0183,140,010,010,010,010,010,010,060,020,010,010,010,010,010,010,010,010,010,010,010,010,010,010,020,010,020,010,010,10,010,010,010,010,010,010,010,010,01РезультатТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаНе теоремаНе теоремаНе теоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаСтатус ILTP Статус TPTP Время ileanCoP Время ImogenТеоремаНе решена0,02ТеоремаТеорема0,010,02ТеоремаТеорема0,010,02ТеоремаТеоремаНе решена0,02ТеоремаНе теорема Не теорема0,010,01Теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,02ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема Не теорема0,010,01НеизвестенНе решена0,01ТеоремаНеизвестенНерешена0,02ТеоремаТеорема0,010,01ТеоремаНеизвестенНе решена0,02ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,02ТеоремаТеорема0,010,01ТеоремаТеорема0,020,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНеизвестенНе решена0,01ТеоремаТеорема0,010,02ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНеизвестенНерешена0,01ТеоремаНеизвестенНе решена0,01ТеоремаТеорема0,020,01ТеоремаТеорема0,010,01ТеоремаНеизвестенНе решена0,02ТеоремаНеизвестенНе решена0,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,03ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01Теорема222ЗадачаSYN948+1SYN949+1SYN950+1SYN951+1SYN952+1SYN953+1SYN954+1SYN955+1SYN956+1SYN957+1SYN958+1SYN959+1SYN960+1SYN961+1SYN962+1SYN963+1SYN964+1SYN965+1SYN966+1SYN967+1SYN968+1SYN969+1SYN970+1SYN971+1SYN972+1SYN973+1SYN974+1SYN975+1SYN976+1SYN977+1SYN978+1SYN979+1SYN980+1SYN981+1TOP021+1TOP022+1Время0,010,010,020,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,010,030,010,010,010,010,010,010,010,010,010,010,010,010,010,010,03РезультатТеоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаНе теоремаНе теоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаНе теоремаТеоремаТеоремаТеоремаТеоремаТеоремаТеоремаСтатус ILTP Статус TPTP Время ileanCoP Время ImogenТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНеизвестенНе решена0,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНеизвестенНе решена0,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеоремаНе решена0,03ТеоремаНеизвестенНе решена0,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаНе теорема0,010,01ТеоремаТеорема0,010,02ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,01ТеоремаТеорема0,010,04ТеоремаВ таблице Г.2 представлена сводная информация о задачах, решенныхпрограммой WhaleProver.
