This table shows for the 196 problems of the TPTPCD2 corpus the proving time of SGCD in two purely goal-driven configurations and those other goal-driven provers based on clausal tableaux, the connection method or model elimination for which roughly comparable performance data were available. For SGCD also proof dimensions are show, written as
ProblemAndSolutionStatistics
document of TPTP 8.0.0.ProblemAndSolutionStatistics
document of TPTP 8.0.0.ProblemAndSolutionStatistics
document of TPTP 8.0.0.ProblemAndSolutionStatistics
document of TPTP 8.0.0.Problem | Rating | SGCD-G1 | SGCD-G2 | SGCD-G1+G2 | CM+TABX | CMProver | TABX | S-SETHEO | SETHEO 3.3 | SATCoP 0.1 | lazyCoP 0.1 |
---|---|---|---|---|---|---|---|---|---|---|---|
Totals of 196: | 81 | 65 | 89 | 92 | 89 | 76 | 66 | 65 | 59 | 42 | |
LCL006-1 | 0.00 | 0.03 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL007-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL008-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL009-1 | 0.00 | 0.01 | 0.01 | 0.01 | • | 0.03 | • | • | • | • | |
LCL010-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL011-1 | 0.00 | 0.06 | 0.14 | 0.06 | • | 0.07 | • | • | • | • | |
LCL012-1 | 0.00 | ||||||||||
LCL013-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL014-1 | 0.00 | 3.76 | 3.76 | • | 3.19 | ||||||
LCL015-1 | 0.00 | ||||||||||
LCL016-1 | 0.00 | ||||||||||
LCL017-1 | 0.00 | ||||||||||
LCL018-1 | 0.00 | ||||||||||
LCL019-1 | 0.00 | ||||||||||
LCL021-1 | 0.00 | ||||||||||
LCL022-1 | 0.00 | 0.04 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | |
LCL023-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | |
LCL024-1 | 0.00 | 3.11 | 3.11 | • | 6.44 | ||||||
LCL025-1 | 0.00 | 0.02 | 0.02 | • | 0.05 | • | • | • | • | • | |
LCL026-1 | 0.00 | ||||||||||
LCL027-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL029-1 | 0.00 | 1.04 | 28.20 | 1.04 | • | 1.69 | • | • | • | ||
LCL030-1 | 0.00 | 37.28 | 37.28 | • | 61.64 | ||||||
LCL032-1 | 0.00 | ||||||||||
LCL033-1 | 0.00 | 0.00 | 5.67 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL034-1 | 0.00 | ||||||||||
LCL035-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL036-1 | 0.00 | ||||||||||
LCL038-1 | 0.00 | ||||||||||
LCL040-1 | 0.00 | 3.95 | 3.95 | • | 2.67 | • | • | • | |||
LCL041-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL042-1 | 0.00 | 12.67 | 15.61 | 12.67 | • | 0.67 | • | • | • | ||
LCL043-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL044-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL045-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL046-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL047-1 | 0.00 | 86.70 | 86.70 | ||||||||
LCL048-1 | 0.00 | ||||||||||
LCL049-1 | 0.00 | ||||||||||
LCL050-1 | 0.00 | ||||||||||
LCL051-1 | 0.00 | ||||||||||
LCL052-1 | 0.00 | ||||||||||
LCL053-1 | 0.00 | ||||||||||
LCL054-1 | 0.00 | ||||||||||
LCL055-1 | 0.00 | ||||||||||
LCL056-1 | 0.00 | ||||||||||
LCL057-1 | 0.00 | ||||||||||
LCL058-1 | 0.00 | ||||||||||
LCL059-1 | 0.00 | 50.13 | 50.13 | • | 82.09 | ||||||
LCL060-1 | 0.00 | ||||||||||
LCL064-1 | 0.00 | 0.02 | 0.02 | • | 0.05 | • | • | • | • | • | |
LCL064-2 | 0.00 | 0.01 | 216.76 | 0.01 | • | 0.03 | • | • | • | • | • |
LCL065-1 | 0.00 | 0.54 | 0.54 | • | 0.15 | • | • | • | |||
LCL066-1 | 0.00 | 0.02 | 0.02 | • | 0.04 | • | • | • | • | • | |
LCL067-1 | 0.00 | • | 13.59 | • | • | ||||||
LCL068-1 | 0.00 | ||||||||||
LCL069-1 | 0.00 | 0.04 | 66.66 | 0.04 | • | 0.07 | • | • | • | ||
LCL070-1 | 0.00 | 1,345.86 | 1,345.86 | • | 5.80 | • | • | ||||
LCL071-1 | 0.00 | • | 83.00 | ||||||||
LCL072-1 | 0.00 | 0.05 | 0.01 | 0.01 | • | 0.01 | • | • | • | ||
LCL075-1 | 0.00 | 356.92 | 356.92 | • | 122.90 | ||||||
LCL076-1 | 0.00 | 0.32 | 0.32 | • | 0.44 | • | • | • | |||
LCL076-2 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL077-1 | 0.00 | 0.08 | 0.08 | • | 0.10 | • | • | • | |||
LCL079-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL080-1 | 0.00 | 29.98 | 29.98 | • | 3.75 | • | • | • | |||
LCL080-2 | 0.00 | 704.27 | 704.27 | • | 4.72 | • | • | • | |||
LCL081-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL082-1 | 0.00 | 0.00 | 5.62 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL083-1 | 0.00 | 1.68 | 1.68 | ||||||||
LCL083-2 | 0.00 | 0.32 | 0.32 | • | 0.05 | • | • | ||||
LCL084-2 | 0.00 | ||||||||||
LCL084-3 | 0.00 | ||||||||||
LCL085-1 | 0.00 | ||||||||||
LCL086-1 | 0.00 | 1,523.50 | 1,523.50 | • | • | • | |||||
LCL087-1 | 0.00 | 0.06 | 0.06 | • | 0.13 | • | • | ||||
LCL088-1 | 0.00 | 129.47 | 129.47 | • | 213.39 | • | • | ||||
LCL089-1 | 0.00 | ||||||||||
LCL090-1 | 0.00 | 76.27 | 76.27 | • | 125.66 | • | • | ||||
LCL091-1 | 0.00 | 1.99 | 1.99 | • | 3.46 | • | • | ||||
LCL093-1 | 0.00 | ||||||||||
LCL094-1 | 0.00 | ||||||||||
LCL095-1 | 0.00 | 674.43 | 674.43 | • | • | • | |||||
LCL096-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL097-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL098-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL100-1 | 0.00 | ||||||||||
LCL101-1 | 0.00 | 1.04 | 0.67 | 0.67 | • | 0.07 | • | • | • | ||
LCL102-1 | 0.00 | 0.03 | 0.03 | 0.03 | • | 0.01 | • | • | • | • | • |
LCL103-1 | 0.00 | 73.71 | 73.71 | • | 42.26 | ||||||
LCL104-1 | 0.00 | 0.69 | 0.19 | 0.19 | • | 0.04 | • | • | • | • | |
LCL106-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL107-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.02 | • | • | • | • | |
LCL108-1 | 0.00 | 0.43 | 0.06 | 0.06 | • | 0.12 | • | • | • | • | |
LCL110-1 | 0.00 | 0.35 | 0.02 | 0.02 | • | 0.06 | • | • | • | ||
LCL111-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL112-1 | 0.00 | 1.83 | 1.83 | • | 0.92 | • | • | • | |||
LCL113-1 | 0.00 | • | 523.74 | ||||||||
LCL114-1 | 0.00 | ||||||||||
LCL115-1 | 0.00 | • | 338.82 | ||||||||
LCL116-1 | 0.00 | ||||||||||
LCL117-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL118-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL120-1 | 0.00 | 0.00 | 0.22 | 0.00 | • | 0.02 | • | • | • | • | • |
LCL121-1 | 0.00 | ||||||||||
LCL122-1 | 0.00 | ||||||||||
LCL123-1 | 0.00 | 0.03 | 0.03 | • | 0.01 | • | • | • | |||
LCL126-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL127-1 | 0.00 | ||||||||||
LCL128-1 | 0.00 | • | 418.15 | ||||||||
LCL129-1 | 0.00 | ||||||||||
LCL130-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL131-1 | 0.00 | • | 120.36 | ||||||||
LCL166-1 | 0.00 | ||||||||||
LCL256-1 | 0.00 | ||||||||||
LCL257-1 | 0.00 | 0.01 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | |
LCL355-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL356-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL357-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL358-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL360-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL361-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL362-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL363-1 | 0.00 | 0.00 | 0.43 | 0.00 | • | 0.03 | • | • | • | • | |
LCL364-1 | 0.00 | 24.24 | 0.16 | 0.16 | • | 4.06 | |||||
LCL366-1 | 0.00 | 910.90 | 52.96 | 52.96 | • | 73.27 | |||||
LCL367-1 | 0.00 | 99.56 | 99.56 | ||||||||
LCL370-1 | 0.00 | ||||||||||
LCL371-1 | 0.00 | ||||||||||
LCL373-1 | 0.00 | ||||||||||
LCL378-1 | 0.00 | ||||||||||
LCL380-1 | 0.00 | ||||||||||
LCL381-1 | 0.00 | ||||||||||
LCL382-1 | 0.00 | ||||||||||
LCL384-1 | 0.00 | 14.33 | 14.33 | • | 357.07 | ||||||
LCL385-1 | 0.00 | ||||||||||
LCL386-1 | 0.00 | ||||||||||
LCL387-1 | 0.00 | ||||||||||
LCL390-1 | 0.00 | ||||||||||
LCL391-1 | 0.00 | ||||||||||
LCL396-1 | 0.00 | ||||||||||
LCL397-1 | 0.00 | 0.10 | 0.43 | 0.10 | • | 0.27 | • | • | • | ||
LCL398-1 | 0.00 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL399-1 | 0.00 | 891.46 | 891.46 | • | • | • | |||||
LCL400-1 | 0.00 | ||||||||||
LCL401-1 | 0.00 | ||||||||||
LCL402-1 | 0.00 | ||||||||||
LCL403-1 | 0.00 | ||||||||||
LCL404-1 | 0.00 | ||||||||||
LCL405-1 | 0.00 | ||||||||||
LCL416-1 | 0.00 | 59.21 | 59.21 | • | 96.97 | • | • | ||||
LCL020-1 | 0.25 | ||||||||||
LCL031-1 | 0.25 | ||||||||||
LCL037-1 | 0.25 | ||||||||||
LCL062-1 | 0.25 | ||||||||||
LCL074-1 | 0.25 | ||||||||||
LCL092-1 | 0.25 | 32.05 | 32.05 | • | 51.16 | ||||||
LCL099-1 | 0.25 | ||||||||||
LCL105-1 | 0.25 | ||||||||||
LCL119-1 | 0.25 | ||||||||||
LCL125-1 | 0.25 | ||||||||||
LCL167-1 | 0.25 | ||||||||||
LCL359-1 | 0.25 | 0.00 | 0.00 | 0.00 | • | 0.01 | • | • | • | • | • |
LCL365-1 | 0.25 | 105.42 | 0.25 | 0.25 | • | 12.40 | |||||
LCL368-1 | 0.25 | ||||||||||
LCL369-1 | 0.25 | ||||||||||
LCL372-1 | 0.25 | ||||||||||
LCL375-1 | 0.25 | ||||||||||
LCL376-1 | 0.25 | ||||||||||
LCL379-1 | 0.25 | ||||||||||
LCL383-1 | 0.25 | ||||||||||
LCL388-1 | 0.25 | ||||||||||
LCL389-1 | 0.25 | ||||||||||
LCL392-1 | 0.25 | ||||||||||
LCL393-1 | 0.25 | ||||||||||
LCL394-1 | 0.25 | ||||||||||
LCL028-1 | 0.50 | ||||||||||
LCL061-1 | 0.50 | ||||||||||
LCL124-1 | 0.50 | ||||||||||
LCL374-1 | 0.50 | ||||||||||
LCL377-1 | 0.50 | ||||||||||
LCL395-1 | 0.50 | ||||||||||
LCL428-1 | 0.50 | ||||||||||
LCL875-1 | 0.50 | ||||||||||
LCL063-1 | 0.75 | ||||||||||
LCL109-1 | 0.75 | ||||||||||
LCL417-1 | 0.75 | ||||||||||
LCL422-1 | 0.75 | ||||||||||
LCL876+1 | 0.93 | ||||||||||
LCL073-1 | 1.00 | ||||||||||
LCL418-1 | 1.00 | ||||||||||
LCL419-1 | 1.00 | ||||||||||
LCL420-1 | 1.00 | ||||||||||
LCL421-1 | 1.00 | ||||||||||
LCL425-1 | 1.00 | ||||||||||
LCL426-1 | 1.00 | ||||||||||
Problem | Rating | SGCD-G1 | SGCD-G2 | SGCD-G1+G2 | CM+TABX | CMProver | TABX | S-SETHEO | SETHEO 3.3 | SATCoP 0.1 | lazyCoP 0.1 |
Totals of 196: | 81 | 65 | 89 | 92 | 89 | 76 | 66 | 65 | 59 | 42 |