To the TPTPCD/SGCD Experiments main page

Results on the TPTPCD2 Corpus – Purely Goal-Driven Proving

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

Compacted Size / Tree Size / Height.

SGCD Configurations and Other Provers

SGCD-G1
SGCD in single Configuration.
SGCD-G2
SGCD in single Configuration.
SGCD-G1+G2
SGCD, union of: Configuration-1, Configuration-2.
CM+TABX
Union of CMProver and TABX.
CMProver
CMProver, union of various configurations, according to http://cs.christophwernhard.com/pie/cmprover/evaluation_201803/tptp_neq.html.
TABX
Union of S-SETHEO, SETHEO 3.3, SATCoP 0.1, lazyCoP 0.1.
S-SETHEO
S-SETHEO according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
SETHEO 3.3
SETHEO 3.3 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
SATCoP 0.1
SATCoP 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
lazyCoP 0.1
lazyCoP 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
ProblemRatingSGCD-G1SGCD-G2SGCD-G1+G2CM+TABXCMProverTABXS-SETHEOSETHEO 3.3SATCoP 0.1lazyCoP 0.1
Totals of 196:81658992897666655942
LCL006-10.000.030.000.000.02
LCL007-10.000.000.000.000.01
LCL008-10.000.000.000.000.01
LCL009-10.000.010.010.010.03
LCL010-10.000.000.000.000.02
LCL011-10.000.060.140.060.07
LCL012-10.00
LCL013-10.000.000.000.000.01
LCL014-10.003.763.763.19
LCL015-10.00
LCL016-10.00
LCL017-10.00
LCL018-10.00
LCL019-10.00
LCL021-10.00
LCL022-10.000.040.000.000.01
LCL023-10.000.010.000.000.01
LCL024-10.003.113.116.44
LCL025-10.000.020.020.05
LCL026-10.00
LCL027-10.000.000.000.000.01
LCL029-10.001.0428.201.041.69
LCL030-10.0037.2837.2861.64
LCL032-10.00
LCL033-10.000.005.670.000.02
LCL034-10.00
LCL035-10.000.000.000.000.02
LCL036-10.00
LCL038-10.00
LCL040-10.003.953.952.67
LCL041-10.000.000.000.000.01
LCL042-10.0012.6715.6112.670.67
LCL043-10.000.000.000.000.01
LCL044-10.000.000.000.000.01
LCL045-10.000.010.000.000.02
LCL046-10.000.000.000.000.01
LCL047-10.0086.7086.70
LCL048-10.00
LCL049-10.00
LCL050-10.00
LCL051-10.00
LCL052-10.00
LCL053-10.00
LCL054-10.00
LCL055-10.00
LCL056-10.00
LCL057-10.00
LCL058-10.00
LCL059-10.0050.1350.1382.09
LCL060-10.00
LCL064-10.000.020.020.05
LCL064-20.000.01216.760.010.03
LCL065-10.000.540.540.15
LCL066-10.000.020.020.04
LCL067-10.0013.59
LCL068-10.00
LCL069-10.000.0466.660.040.07
LCL070-10.001,345.861,345.865.80
LCL071-10.0083.00
LCL072-10.000.050.010.010.01
LCL075-10.00356.92356.92122.90
LCL076-10.000.320.320.44
LCL076-20.000.000.000.000.01
LCL077-10.000.080.080.10
LCL079-10.000.000.000.000.01
LCL080-10.0029.9829.983.75
LCL080-20.00704.27704.274.72
LCL081-10.000.010.000.000.02
LCL082-10.000.005.620.000.02
LCL083-10.001.681.68
LCL083-20.000.320.320.05
LCL084-20.00
LCL084-30.00
LCL085-10.00
LCL086-10.001,523.501,523.50
LCL087-10.000.060.060.13
LCL088-10.00129.47129.47213.39
LCL089-10.00
LCL090-10.0076.2776.27125.66
LCL091-10.001.991.993.46
LCL093-10.00
LCL094-10.00
LCL095-10.00674.43674.43
LCL096-10.000.000.000.000.02
LCL097-10.000.010.000.000.02
LCL098-10.000.000.000.000.01
LCL100-10.00
LCL101-10.001.040.670.670.07
LCL102-10.000.030.030.030.01
LCL103-10.0073.7173.7142.26
LCL104-10.000.690.190.190.04
LCL106-10.000.000.000.000.01
LCL107-10.000.010.000.000.02
LCL108-10.000.430.060.060.12
LCL110-10.000.350.020.020.06
LCL111-10.000.000.000.000.01
LCL112-10.001.831.830.92
LCL113-10.00523.74
LCL114-10.00
LCL115-10.00338.82
LCL116-10.00
LCL117-10.000.000.000.000.01
LCL118-10.000.000.000.000.01
LCL120-10.000.000.220.000.02
LCL121-10.00
LCL122-10.00
LCL123-10.000.030.030.01
LCL126-10.000.000.000.000.01
LCL127-10.00
LCL128-10.00418.15
LCL129-10.00
LCL130-10.000.000.000.000.01
LCL131-10.00120.36
LCL166-10.00
LCL256-10.00
LCL257-10.000.010.000.000.01
LCL355-10.000.000.000.000.01
LCL356-10.000.000.000.000.01
LCL357-10.000.000.000.000.01
LCL358-10.000.000.000.000.01
LCL360-10.000.000.000.000.01
LCL361-10.000.000.000.000.01
LCL362-10.000.000.000.000.01
LCL363-10.000.000.430.000.03
LCL364-10.0024.240.160.164.06
LCL366-10.00910.9052.9652.9673.27
LCL367-10.0099.5699.56
LCL370-10.00
LCL371-10.00
LCL373-10.00
LCL378-10.00
LCL380-10.00
LCL381-10.00
LCL382-10.00
LCL384-10.0014.3314.33357.07
LCL385-10.00
LCL386-10.00
LCL387-10.00
LCL390-10.00
LCL391-10.00
LCL396-10.00
LCL397-10.000.100.430.100.27
LCL398-10.000.000.000.000.01
LCL399-10.00891.46891.46
LCL400-10.00
LCL401-10.00
LCL402-10.00
LCL403-10.00
LCL404-10.00
LCL405-10.00
LCL416-10.0059.2159.2196.97
LCL020-10.25
LCL031-10.25
LCL037-10.25
LCL062-10.25
LCL074-10.25
LCL092-10.2532.0532.0551.16
LCL099-10.25
LCL105-10.25
LCL119-10.25
LCL125-10.25
LCL167-10.25
LCL359-10.250.000.000.000.01
LCL365-10.25105.420.250.2512.40
LCL368-10.25
LCL369-10.25
LCL372-10.25
LCL375-10.25
LCL376-10.25
LCL379-10.25
LCL383-10.25
LCL388-10.25
LCL389-10.25
LCL392-10.25
LCL393-10.25
LCL394-10.25
LCL028-10.50
LCL061-10.50
LCL124-10.50
LCL374-10.50
LCL377-10.50
LCL395-10.50
LCL428-10.50
LCL875-10.50
LCL063-10.75
LCL109-10.75
LCL417-10.75
LCL422-10.75
LCL876+10.93
LCL073-11.00
LCL418-11.00
LCL419-11.00
LCL420-11.00
LCL421-11.00
LCL425-11.00
LCL426-11.00
ProblemRatingSGCD-G1SGCD-G2SGCD-G1+G2CM+TABXCMProverTABXS-SETHEOSETHEO 3.3SATCoP 0.1lazyCoP 0.1
Totals of 196:81658992897666655942