To the CCS 2022-04 Experiments main page

Exhaustive Search with CCS on the Real-First-Order Horn Problems in the TPTP

This table shows for the 562 problems of the CNF_UNS_RFO_NEQ_HRN specialist class of TPTP 8.0.0 the proving time and compacted size of proofs by CCS in different configurations with exhaustive search.

For comparison, also known results for provers based on clausal tableaux, the connection method or model elimination are shown.

Configurations and Provers

CM+TABX
Union of CMProver, SETHEOs, lazyCoP 0.1, SATCoP 0.1. For comparison. Represents what is solvable by clausal tableaux and similar techniques.
H-1-5
Best time values of CCS in the five configurations ximp102 (aka H-1), ximp00 (aka H-2) ximp14 (aka H-3), ximp15 (aka H-4), ximp16 (aka H-5). The individual contributions of these configurations are shown in subsequent columns H-1 to H-5. The further considered configurations H-6 to H-9 do not provide proofs for additional problems.
H-1
CCS in configuration ximp102. It provides proof schemas that express hyperresolution as inference rule, which, however, is used by CCS in a goal-driven way.
H-2
CCS in configuration ximp00. A vanilla configuration that just uses condensed detachment generalized for arbitrary Horn clauses to construct proofs.
H-3
CCS in configuration ximp14. A configuration with proof schemas r0, r2, r4, r6. Highlighting indicates use of r4 or r6.
H-4
CCS in configuration ximp15. A configuration with proof schemas r1, r2, r4, r5, r6. Highlighting indicates use of r4, r5 or r6.
H-5
CCS in configuration ximp16. A configuration with proof schemas r1, r2, r3, r4, r5, r6. Highlighting indicates use of r3, r4, r5 or r6.
H-6
CCS in configuration rimp104. It provides proof schemas that express a restricted form of binary resolution. Highlighting indicates use of a shuffle proof schema, which expresses re-ordering of atoms in a clause body.
H-7
CCS in configuration ximp17. It permits the B4 combinator. Highlighting indicates use of B4.
H-8
CCS in configuration ximp11. It permits the B combinator. Highlighting indicates use of B.
H-9
CCS in configuration ximp18. It permits the B4 and C4 combinators. Highlighting indicates use of B4 or C4.
CMProver
CMProver, union of various configurations, according to http://cs.christophwernhard.com/pie/cmprover/evaluation_201803/tptp_neq.html.
TABX
Union of SETHEOs, lazyCoP 0.1, SATCoP 0.1.
SETHEOs
Union of SETHEO 3.3 and S-SETHEO 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.
SATCoP 0.1
SATCoP 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
ProblemRatingCM-TABXH-1-5H-1H-2H-3H-4H-5H-6H-7H-8H-9CMProverSETHEOslazyCop 0.1SATCop 0.1
Totals of 562:430421413390250239236327365355351414387338394
ANA013-20.00•0.060.0620.1020.0620.0620.0620.0620.062••••
ANA037-20.00•0.060.0660.10100.48100.06100.07100.0810••••
ANA038-20.00•0.060.0660.10100.47100.06100.07100.0810••••
ANA039-20.00•0.060.0670.11112.24110.06110.07110.3411••••
ANA041-20.00•0.060.0600.1100.0600.0700.0600.0600.0600.0600.060••••
ANA042-20.00•0.060.0600.1000.0600.0600.0800.0600.0600.0600.060••••
COL101-20.00•0.060.0600.1100.0600.0600.0600.0500.0600.0600.060••••
COL102-20.00•0.060.0630.1140.0640.0730.0630.0640.0640.0640.064••••
COL104-20.00•0.060.0630.1040.0640.0730.0630.0640.0640.0640.064••••
COL105-20.00•0.060.0610.0920.0620.0610.0610.0620.0620.0620.062••••
COL109-20.00•0.060.0640.0670.0670.0640.0640.0670.0670.0670.067••••
COL110-20.00•0.060.0670.06100.09100.0770.0870.20100.06100.08100.0910••••
COL111-20.00•0.060.0610.0620.0620.0610.0710.0620.0620.0620.062••••
COL112-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL113-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
COL114-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL115-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL116-20.00•0.060.0600.0600.0600.0600.0700.0500.0600.0600.060••••
COL117-20.00•0.060.0640.0670.0670.0640.0640.0670.0670.0670.067••••
COL118-20.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
COL119-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL120-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL121-20.00•0.060.0670.1113827.93130.35133.2113143.9613••••
COL122-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COL123-20.00•0.060.0670.07110.56110.8281.3482.83110.10110.21110.5411••••
COL124-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
COM001-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0650.065••••
COM002-10.00•0.060.0670.07110.1490.0750.0750.78100.08110.22111.1411••••
GEO002-40.00•7.1615.6287.161329.89839.07850.1913171.1313325.1713•
GRP003-10.00•0.050.0520.0660.0660.0660.0660.066••••
GRP003-20.00•0.060.0620.0660.0660.0660.0660.066••••
GRP004-10.00•0.050.0520.0660.0660.0660.0660.066••••
GRP004-20.00•0.060.0620.0660.0660.0660.0660.066••••
GRP005-10.00•0.060.0610.0630.0630.0630.0630.063••••
GRP006-10.00•0.060.0620.0660.0660.0660.0660.066••••
GRP028-10.00•0.060.0610.0630.0630.0630.0630.063••••
GRP028-30.00•0.060.0610.0630.0630.0630.0630.063••••
GRP028-40.00•0.060.0610.0630.0630.0630.0630.063••••
GRP029-20.00•0.060.0620.0860.3560.0760.0760.076••••
GRP031-20.00•0.060.0620.0660.0660.0660.0660.066••••
GRP033-30.00•0.060.0620.0660.0660.0660.0660.066••••
GRP034-40.00•0.060.0620.0650.0650.0660.0660.066••••
GRP041-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
GRP042-20.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
GRP043-20.00•0.060.0630.0660.0660.0630.0630.0660.0660.0660.066••••
GRP044-20.00•0.060.0620.0650.0650.0650.0650.065••••
GRP045-20.00•0.060.0630.0880.3180.0880.0980.088••••
GRP046-20.00•0.060.0630.0670.0770.0670.0670.067••••
GRP047-20.00•0.100.1040.1590.9790.1890.2290.219••••
GRP048-20.00•155.26155.266•
LAT270-20.00•0.050.0510.0630.0630.0630.0630.063••••
LAT272-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
LCL002-10.00
LCL003-10.00
LCL004-10.00•105.21105.2113•
LCL005-10.00
LCL006-10.00•0.060.0650.331041.39100.0750.07526.9690.50100.93100.7810••••
LCL007-10.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
LCL008-10.00•0.060.0650.0680.0780.0850.0650.0670.0680.0680.068••••
LCL009-10.00•0.080.0870.241210.58110.1370.18732.79100.43121.15124.1212•••
LCL010-10.00•0.060.0650.06100.1090.0650.0650.0980.06100.07100.0810••••
LCL011-10.00•0.090.0970.12110.80100.1270.1775.46100.13110.21110.3911•••
LCL012-10.00
LCL013-10.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL014-10.00•13.7113.711093.0515230.7510486.59101,406.34151,961.9614•
LCL015-10.00
LCL016-10.00
LCL017-10.00
LCL018-10.00
LCL019-10.00
LCL021-10.00
LCL022-10.00•0.120.4180.22120.1290.3470.3970.4090.08100.19100.1110•••
LCL023-10.00•0.070.0770.07100.4190.1170.1570.10090.08100.10100.1110•••
LCL024-10.00•10.5812.301010.5814308.4110622.621037.8414127.50142,019.1214•
LCL025-10.00•0.150.1560.391146.68100.2160.2666.0590.34103.35110.9610••••
LCL026-10.00
LCL027-10.00•0.050.0530.0660.0660.0630.0630.0760.0660.0660.066••••
LCL029-10.00•7.777.7777.80122,269.011111.79716.137305.041030.111217.23113.2110••
LCL030-10.00•50.6350.63891.0813161.358277.298342.3913867.01131,140.6613•
LCL032-10.00
LCL033-10.00•0.060.0660.0690.0880.0760.0761.0490.0790.0790.079••••
LCL034-10.00
LCL035-10.00•0.060.0650.0690.0660.0650.0650.0670.0690.0790.079••••
LCL036-10.00210.45738.6811210.4510443.6710
LCL038-10.00
LCL040-10.00•10.0914.35819.49131,497.651110.09714.947117.541016.961251.941217.7711••
LCL041-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0650.065••••
LCL042-10.00•46.97493.60846.9712134.357178.6771,250.341074.2512161.2912154.3312••
LCL043-10.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL044-10.00•0.060.0630.0660.0660.0630.0630.0760.0660.0660.066••••
LCL045-10.00•0.120.1250.2296.8890.1350.15543.9690.2590.3690.369••••
LCL046-10.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL047-10.00
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.00••
LCL060-10.00
LCL064-10.00•0.150.1560.341137.23100.2160.2665.2590.30102.78110.9010••••
LCL064-20.00•0.090.0960.14117.83100.1260.1461.1990.13100.48110.4410••••
LCL065-10.00•0.200.2770.201132.29100.9571.77727.0290.69112.08112.8411••
LCL066-10.00•0.280.3570.281134.24101.1072.0375.1090.27102.50110.8410••••
LCL067-10.00•250.63867.7410250.6315••
LCL068-10.00
LCL069-10.00•1.891.8983.87132.2174.31734.0913124.7413305.8013••
LCL070-10.00•241.38241.3810343.6415••
LCL071-10.00••
LCL072-10.00•0.290.2975.11130.7371.42734.9913124.6813289.3713••
LCL075-10.00•0.120.1880.12111.31100.2770.50733.95100.17110.34110.4411•
LCL076-10.00•0.170.1770.4111630.78110.6271.1570.92112.38113.0811••
LCL076-20.00•0.050.0510.0620.0620.0610.0610.0620.0620.0620.062••••
LCL076-30.00•0.070.0750.56104.2790.0850.09539.4490.83101.54101.4910••••
LCL077-10.00•0.070.0760.091032.45100.1160.15629.9490.16100.36100.4110••
LCL077-20.00•0.060.0640.0880.1470.0640.0741.8680.0980.1080.108••••
LCL079-10.00•0.060.0630.0660.0660.0630.0630.0660.0660.0660.066••••
LCL080-10.00•303.24323.689303.2414345.008545.9681,216.2114992.5513••
LCL080-20.00•1,783.121,783.12142,378.728••
LCL081-10.00•0.060.0660.09110.69100.0760.0761.2290.11110.16110.3211••••
LCL082-10.00•0.060.0660.11111.01100.0760.0760.8790.15110.26110.3911••••
LCL083-10.0011.31434.331111.31923.119872.26161,948.4813
LCL083-20.00•5.875.87828.111324.381015.59827.0481,630.791174.3913201.1313109.5712••
LCL084-20.00
LCL084-30.00
LCL085-10.00
LCL086-10.00•23.6690.8610269.901023.669932.09111,861.0413•
LCL087-10.00•0.540.54812.79143.83101.0381.8680.85920.77149.88130.2710••
LCL088-10.00•1,125.881,125.8810••
LCL089-10.0092.67350.35101,053.521092.6792,129.6014
LCL090-10.00•1,296.651,296.6512••
LCL091-10.00•80.14209.651180.1411110.0410255.4210••
LCL093-10.00
LCL094-10.00
LCL095-10.00••
LCL096-10.00•0.060.0640.0770.1370.0740.0740.0860.0770.0770.077••••
LCL097-10.00•0.060.0640.0770.0650.0640.0740.0650.0670.0770.077••••
LCL098-10.00•0.060.0640.0670.0650.0640.0740.0650.0670.0670.067••••
LCL100-10.00
LCL101-10.00•0.090.0970.331176.91100.1060.13648.0890.32104.25110.7310••
LCL102-10.00•0.530.5371.74112,172.96111.8273.4373.40117.56116.8511••••
LCL103-10.00•378.301,212.63101,256.2815378.309624.239•
LCL104-10.00•0.070.0760.3511146.60100.0960.116221.66101.35113.67111.1310•••
LCL106-10.00•0.060.0640.0670.0770.0640.0740.0970.0670.0670.067••••
LCL107-10.00•0.060.0650.0893.1490.0650.0754.9390.1090.1590.119•••
LCL108-10.00•0.080.0870.951290.79110.1370.1871,583.89111.65123.38125.9712•••
LCL110-10.00•0.490.7770.4911101.69102.5574.597254.13101.14113.02114.5211••
LCL111-10.00•0.060.0650.0780.2780.0750.0850.1270.0780.0880.088••••
LCL112-10.00•7.187.18813.881343.25881.17842.5513135.4413359.7613••
LCL113-10.00••
LCL114-10.00
LCL115-10.00••
LCL116-10.00
LCL117-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0650.065••••
LCL118-10.00•0.060.0670.13118.63100.0970.1376.5790.36111.03110.2110••••
LCL120-10.00•0.060.0660.0790.7990.0760.0765.3490.0790.0890.089••••
LCL121-10.001,562.341,562.3412
LCL122-10.00
LCL123-10.00•0.860.86102.311635.2110123.50104.221674.9916••
LCL126-10.00•0.060.0640.0670.0770.0640.0640.0970.0670.0770.067••••
LCL127-10.00
LCL128-10.00••
LCL129-10.0051.19525.1611313.791651.19999.819899.46161,834.3715
LCL130-10.00•0.060.0650.0680.2380.0650.0751.2780.0780.0780.078••••
LCL131-10.00•182.28182.28111,296.8716901.96101,797.0110•
LCL166-10.00
LCL169-10.00•0.060.0610.0610.0610.0620.0620.0610.0610.0610.061••••
LCL170-10.00•0.060.0610.0610.0610.0630.0630.0610.0610.0610.061••••
LCL171-10.00•0.060.0610.0610.0710.0630.0630.0610.0610.0610.061••••
LCL172-10.00•0.060.0610.0710.0610.0630.0630.0610.0610.0610.061••••
LCL173-10.00•0.060.0610.0610.0610.0630.0630.0610.0610.0610.061••••
LCL174-10.00•0.060.0620.0630.0630.0620.0620.0630.0630.0630.083••••
LCL175-10.00•0.060.0610.0610.0610.0620.0620.0610.0610.0610.061••••
LCL176-10.00•0.060.0620.0630.0630.0620.0620.0630.0630.0630.063••••
LCL177-10.00•0.060.0630.0650.0750.0630.0630.0650.0650.0650.085••••
LCL178-10.00•0.060.0630.0650.0750.0630.0630.0650.0650.0650.065••••
LCL182-10.00•0.110.1162.30110.2160.23612.071129.761119.6611••••
LCL185-10.00•0.060.0620.0730.0630.0620.0620.0630.0630.0630.063••••
LCL186-10.00•0.060.0620.0630.0630.0620.0620.0630.0630.0730.063••••
LCL187-10.00•0.060.0630.0650.0750.0630.0630.0650.0650.0650.065••••
LCL188-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0650.065••••
LCL189-10.00•0.060.0630.0650.0750.0630.0630.0650.1050.0650.065••••
LCL190-10.00•0.060.0620.0630.0630.0620.0620.0630.0630.0630.063••••
LCL191-10.00
LCL192-10.00•0.060.0640.0870.2170.0740.0740.2470.0870.0970.087••••
LCL193-10.00•0.060.0630.0650.0750.0630.0630.0650.0650.0750.065••••
LCL194-10.00•0.060.0640.0760.0860.0640.0640.0760.0760.0760.076••••
LCL195-10.00•0.130.1360.721040.9490.2460.26683.5992.23104.95102.9810••••
LCL196-10.00•0.720.728111.94146.10089.608••••
LCL197-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0750.065••••
LCL198-10.00•1.311.318174.89148.73811.458••••
LCL199-10.00•0.070.0760.1192.0680.1360.1560.8580.1990.3390.239••••
LCL200-10.00•0.060.0650.0770.0860.0750.0750.0760.0770.0770.077••••
LCL201-10.00•0.090.0960.1592.7180.1860.2061.1980.2790.5090.339••••
LCL202-10.00•0.140.1470.391012.6091.0871.4272.2481.28102.87101.8010••••
LCL203-10.00•0.090.0960.1592.7480.1860.2061.1980.2890.5190.349••••
LCL204-10.00•0.090.0960.1592.7280.1860.2061.1980.2890.5090.339••••
LCL205-10.00•0.180.1870.451014.6491.2271.6172.4881.50103.32102.1210••••
LCL206-10.00•0.090.0960.1792.7480.1860.2061.2180.2890.5190.349••••
LCL207-10.00•0.060.0650.0770.0960.0750.0850.0760.0770.0870.077••••
LCL208-10.00•0.440.44715.01122.3573.027130.4112312.6412241.3712••••
LCL211-10.00•0.070.0750.21915.3990.0850.09525.0490.4090.6990.469••••
LCL212-10.00•0.120.1260.711042.1090.2460.26686.7292.23104.77102.9810••••
LCL213-10.00•0.080.0850.33928.8790.1050.10540.9990.6591.2190.779••••
LCL215-10.00•0.120.1260.681039.1390.2260.25681.9092.11104.49102.7810••••
LCL216-10.00•0.070.0750.19913.10090.0850.08525.8990.3490.6390.419••••
LCL221-10.00460.67460.6711
LCL223-10.00
LCL224-10.00•1,029.691,029.6911•
LCL225-10.00•1,831.531,831.5311•
LCL226-10.00•0.060.0620.0630.0630.0620.0620.0630.0630.0730.063••••
LCL234-10.00•2.292.299432.311580.429119.679•••
LCL236-10.00•0.060.0630.0650.0650.0630.0630.0650.0650.0750.075••••
LCL237-10.00•12.9512.95101,237.06101,973.3310•••
LCL238-10.00•0.060.0650.0880.2170.0750.0750.2670.1080.1180.108••••
LCL250-10.00•16.2216.2292,227.3915415.119620.569•••
LCL256-10.00
LCL257-10.00•0.070.0770.08110.93100.1070.106156.38110.09110.13110.3511•••
LCL355-10.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
LCL356-10.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL357-10.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL358-10.00•0.060.0640.0660.0660.0640.0640.0660.0660.0660.066••••
LCL360-10.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
LCL361-10.00•0.060.0640.0670.0870.0640.0640.0660.0670.0670.066••••
LCL362-10.00•0.060.0640.0670.0870.0640.0640.0970.0670.0670.077••••
LCL363-10.00•0.090.0960.161036.27100.1260.14623.9090.28100.56100.4810••••
LCL364-10.00•41.5941.599468.121572.158109.128•
LCL366-10.00•1,764.511,764.519•
LCL367-10.00
LCL370-10.00
LCL371-10.00
LCL373-10.00
LCL378-10.00742.26742.26151,806.649
LCL380-10.00
LCL381-10.00
LCL382-10.00
LCL384-10.00••
LCL385-10.00
LCL386-10.00
LCL387-10.00
LCL390-10.00
LCL391-10.00
LCL396-10.00
LCL397-10.00•0.310.3170.5011755.61110.8771.437509.36101.39113.52113.1211•••
LCL398-10.00•0.060.0630.0660.0660.0630.0630.0660.0660.0660.066••••
LCL399-10.00•2,004.412,004.419•
LCL400-10.00
LCL401-10.00
LCL402-10.00
LCL403-10.00
LCL404-10.00
LCL405-10.00
LCL414-10.00•0.060.0620.0630.0740.0620.0620.0630.0640.0640.064••••
LCL416-10.00•97.9297.92101,031.9116437.69101,148.6110••
LCL429-20.00•0.060.0640.0680.0780.0640.0740.1080.0680.0780.078••••
LCL430-20.00•0.060.0640.0680.0780.0640.0640.1080.0680.0780.078••••
LCL432-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
LCL433-20.00•0.060.0650.0660.0660.0750.0750.0660.0660.0660.066••••
LCL435-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
LCL436-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
LCL437-20.00•0.050.0510.0610.0610.0610.0610.0610.061••••
LCL438-20.00•0.060.0620.0640.0640.0620.0620.0640.0640.0640.064••••
LCL439-20.00•0.060.0640.0650.0650.0650.0650.0650.065••••
LCL440-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
LCL441-20.00•0.050.0520.0630.0630.0630.0630.0630.0630.0630.063••••
LCL443-20.00•0.060.0660.0880.258113.229182.3491.5180.0780.0780.078••••
LCL445-20.00•0.060.0640.0660.0650.0630.0630.0650.0660.0660.066••••
LCL446-20.00•0.060.0620.0630.0640.0620.0720.0630.0640.0640.064••••
LCL447-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
MGT001-10.00•0.080.081016.7343••••
MGT003-10.00•0.070.0767.31193.2719••••
MGT006-10.00•0.060.0660.1628••••
MGT008-10.00•0.060.0640.10200.9820••••
MGT009-10.00•0.060.0640.09201.0320••••
MGT010-10.00•0.060.0660.7933••••
MGT015-10.00•0.060.0640.102315.4823••••
MGT032-20.00•0.060.0660.061341.75130.07130.3413114.1713••••
MGT036-30.00•0.060.0630.0690.1290.0690.0690.069••••
MSC005-10.00•0.060.0640.0680.0680.0640.0640.0980.0680.0780.078••••
NUM001-10.00•0.060.0630.0750.0750.0730.0630.0650.0650.0650.065••••
NUM002-10.00•0.060.0630.0860.0860.0730.0730.1560.0760.0760.076••••
NUM003-10.00•0.060.0630.0760.0760.0630.0630.1360.0660.0760.076••••
NUM004-10.00•0.060.0630.0760.0860.0730.0730.1360.0760.0760.076••••
NUM019-10.00•0.060.0620.0630.0630.0630.0630.0630.063••••
NUM020-10.00•0.060.0630.0640.0640.0640.0640.0640.064••••
NUM023-10.00•0.060.0620.0720.0620.0620.0620.0620.062••••
NUM024-10.00•0.100.1050.2279.18712.92614.18614.5670.2970.3870.327••••
NUM025-10.00•0.060.0620.0630.0630.0630.0630.0730.063••••
NUM283-1.0050.00•26.3926.3939170.0348•••
PLA001-10.00•0.070.0760.36110.0860.1363.911119.171120.4611••••
PLA003-10.00•0.060.0660.0660.1460.1460.0660.0760.066••••
PLA006-10.00•0.060.0620.0650.0750.0650.0750.065••••
PLA007-10.00•0.250.25108.6722•••
PLA016-10.00•0.110.1192.3621•••
PLA017-10.00•0.060.0640.0789.9580.0980.0980.108••••
PLA019-10.00•0.080.0880.8919•••
PLA020-10.00•0.060.0610.0630.0630.0630.0630.073••••
PLA022-10.00•0.080.0870.50134.751330.1013231.3513••••
PLA022-20.00•0.060.0670.08131.591310.1813223.0613••••
PUZ008-10.00•0.060.0610.0610.0610.0610.0610.0610.071••••
PUZ008-30.00•437.13437.1340••••
PUZ038-10.00•0.060.0610.0710.0710.0610.0710.0710.071••••
PUZ039-10.00
PUZ040-10.00
PUZ042-10.00
PUZ047-10.00•0.060.0670.0870.1170.1070.0670.0670.077••••
RNG001-20.00•2.232.23483.4513223.7813320.0613501.0613•
RNG001-30.00•0.060.0640.6314570.19140.74142.8514••••
RNG001-50.00•1.991.994381.951126.321136.551135.2511•••
RNG005-20.00•0.060.0610.0640.0840.0740.0640.064••••
RNG006-20.00•0.070.0720.0750.0750.0850.0750.075••••
RNG037-20.00•0.060.0620.0750.0650.0750.0650.065••••
RNG038-20.00•0.060.1240.0660.0760.0660.0760.0660.066••••
RNG039-20.00•37.0937.093454.6991,044.1961,092.286327.979365.319345.159•••
SET818-20.00•0.060.0600.0600.0600.0600.0600.0500.0600.0600.060••••
SET819-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SET824-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET826-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET827-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET828-20.00•0.060.0610.0720.0620.0610.0610.0620.0620.0620.062••••
SET829-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET832-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET833-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET835-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SET836-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.072••••
SET846-20.00•0.060.0630.0630.0630.0630.0630.0630.063••••
SET850-20.00•0.060.0610.0820.0620.0610.0610.0620.0620.0620.062••••
SET859-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SWV011-10.00•0.060.0610.0720.0620.0610.0610.0620.0620.0620.062••••
SWV242-20.00•0.060.0650.0680.0780.0640.0640.0670.0780.0680.068••••
SWV256-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV257-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV258-20.00•0.060.0630.0740.0640.0640.0640.0640.064••••
SWV259-20.00•0.060.0630.0630.0630.0630.0630.0630.063••••
SWV263-20.00•0.060.0620.0630.0630.0630.0630.0630.063••••
SWV264-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV265-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV266-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV267-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SWV269-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV273-20.00•0.060.0630.0640.0740.0630.0630.0640.0640.0640.064••••
SWV277-20.00•0.060.0620.0730.0630.0620.0620.0630.0630.0630.063••••
SWV279-20.00•0.060.0670.07100.1192.7282.9681.71100.0790.0690.069••••
SWV280-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SWV299-20.00•0.060.06120.07141.93110.08120.20124.0712••••
SWV309-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV310-20.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SWV312-20.00•0.060.0610.0610.0610.0710.0610.0610.061••••
SWV320-20.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SWV330-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SWV331-20.00•0.060.0620.0650.0750.0650.0650.065••••
SWV333-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SWV334-20.00•0.060.0600.0600.0600.0600.0600.0700.0600.0600.060••••
SWV336-20.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SWV341-20.00•0.060.0620.0620.0620.0720.0620.0620.062••••
SWV349-20.00•0.050.0500.0600.0600.0600.0600.0500.0600.0600.060••••
SWV350-20.00•0.050.0500.0600.0600.0600.0600.0600.0600.0600.060••••
SWV351-20.00•0.060.0600.0700.0600.0600.0600.0500.0600.0600.060••••
SWV355-20.00•0.060.0670.0670.1570.1470.0770.0670.067••••
SWV356-20.00•0.060.0620.0620.0620.0620.0620.0620.062••••
SWV357-20.00•0.060.0620.0630.0630.0630.0630.0630.063••••
SWV358-20.00•0.060.0670.0770.1570.1470.0670.0670.067••••
SWV364-20.00•0.060.0620.0630.0630.0630.0630.0630.063••••
SYN033-10.00•0.060.0610.0630.0630.0630.0630.063••••
SYN035-10.00•0.060.0620.0660.0660.0660.0660.066••••
SYN048-10.00•0.060.0600.0600.0600.0600.0700.0600.0600.0600.060••••
SYN049-10.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SYN050-10.00•0.060.0610.0720.0620.0610.0610.0620.0620.0620.062••••
SYN064-10.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SYN065-10.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SYN068-10.00•0.060.0640.0650.0650.0650.0650.0650.0650.0650.065••••
SYN079-10.00•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
SYN310-10.00•1.679.351212.18121.6761.6364.96929.3495.549••••
SYN312-10.00•19.45112.641319.451487.598137.188156.59884.96821.4210412.011138.4810••••
SYN336-10.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SYN338-10.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SYN339-10.00•0.060.0600.0700.0600.0600.0700.0600.0600.0600.060••••
SYN340-10.00•0.060.0600.0600.0600.0600.0700.0600.0600.0600.060••••
SYN341-10.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SYN346-10.00•0.060.0610.0720.0620.0610.0710.0620.0620.0620.062••••
SYN553-10.00•0.060.0650.0991.8993.8190.1290.1790.149••••
SYN555-10.00•0.060.0620.0640.0640.0620.0720.0640.0640.0640.064••••
SYN558-10.00•0.070.07526.891452.2914138.9014••••
SYN559-10.00•0.060.0640.07100.42100.07100.07100.0910••••
SYN561-10.00•0.060.0640.07100.43100.06100.07100.0910••••
SYN562-10.00•0.060.0610.0630.0630.0630.0630.063••••
SYN564-10.00•0.090.0950.1295.3190.1490.1990.199••••
SYN565-10.00•10.2720.65710.27121,055.121116.971232.831275.6312••••
SYN566-10.00•0.060.0650.081115.74110.13110.19110.5711••••
SYN569-10.00•20.5944.08820.591526.091568.1415••••
SYN570-10.00•0.060.0640.0680.0980.0780.0780.078••••
SYN572-10.00•8.188.18629.781239.811264.641256.6512••••
SYN577-10.00•1,184.351,184.35171,636.2014•••
SYN584-10.00•0.060.0630.0660.0660.0760.0660.066••••
SYN590-10.00•0.120.4160.12106.02100.07100.08100.1210••••
SYN596-10.00•0.060.0620.0650.0650.0650.0650.065••••
SYN597-10.00•0.060.0640.07100.91100.11100.15100.1710••••
SYN602-10.00•0.060.0640.0790.3090.0890.0790.079••••
SYN603-10.00•0.060.0640.0790.3090.0790.0790.079••••
SYN618-10.00•0.620.62612.421222.591247.881266.2212••••
SYN628-10.00•0.420.4260.421146.58110.52110.81111.7411••••
SYN629-10.00•0.430.5060.431146.98110.53110.83111.7511••••
SYN632-10.00•0.262.2980.26134.211316.1713367.7713••••
SYN651-10.00•0.060.0640.0760.0760.0740.0840.0660.0760.0660.076••••
SYN652-10.00•0.070.0750.1291.6490.1150.1255.5190.1590.2290.199••••
SYN691-10.00•0.070.0750.09854.1880.2880.4680.478••••
SYN715-10.00•0.070.0750.0895.7490.1090.1490.149••••
SYN719-10.00•0.070.0730.0770.2170.0870.0870.087••••
SYN727-10.00•0.060.0610.0610.0610.0610.0610.0610.061••••
SYN729-10.00•0.060.0650.0660.0660.0750.0750.0660.0660.0660.066••••
SYN731-10.00•0.060.0600.0600.0600.0600.0600.0600.0600.0600.060••••
SYO611-10.00•0.060.0610.0630.0630.0630.0630.063•••
SYO612-10.00•0.060.0610.0613133.17130.06130.191385.8813•••
SYO613-10.00•0.060.0610.062312.8523•••
SYO632-10.00•0.060.0610.0620.0620.0610.0710.0620.0620.0620.062•••
SYO633-10.00•0.060.0650.08201.8120•••
SYO634-10.00•0.150.1510••
SYO691-1.0000.00•0.060.0660.0690.8393.1083.4780.3290.0690.0690.069••
SYO691-1.0010.00•0.070.0790.09140.10141.79142,028.2914•
COL103-20.25•0.060.0600.1100.0600.0700.0600.0500.0600.0600.060••••
LAT271-20.25•0.060.0610.0620.0620.0610.0610.0620.0620.0620.062••••
LCL020-10.25
LCL031-10.25
LCL037-10.25
LCL039-10.25
LCL062-10.25
LCL074-10.25
LCL092-10.25•388.45484.75122,290.8511388.4510•
LCL099-10.25
LCL105-10.25
LCL119-10.25
LCL125-10.25
LCL167-10.25
LCL210-10.25•1.021.02835.601316.84823.608545.25131,412.56131,475.5313••••
LCL214-10.25•0.080.0850.28924.0590.0950.10533.2090.5791.0490.679••••
LCL217-10.25•0.070.0750.22918.3790.0850.08534.2990.4490.7990.529••••
LCL218-10.25•0.100.1060.1993.7080.2160.2361.6880.3790.6990.459••••
LCL222-10.25
LCL227-10.25
LCL230-10.25•0.650.6574.5811444.03102.9073.667977.721022.611154.691135.0011••••
LCL231-10.25•0.900.9075.6811536.93103.5074.3871,083.931026.911161.881140.6211••••
LCL249-10.25••
LCL359-10.25•0.060.0630.0650.0650.0630.0630.0650.0650.0650.065••••
LCL365-10.25•277.93379.4210277.939475.409•
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
LCL444-20.25
MGT002-10.25•0.070.0769.32193.3119••••
MGT017-10.25•0.060.0640.102315.3223••••
NUM017-10.25163.84163.847
NUM284-1.0140.25••
PLA004-10.25•494.94494.9415•••
PLA004-20.25•447.29447.2915•••
PLA005-10.25•995.73995.7316•••
PLA005-20.25•27.2327.2316806.6232•••
PLA009-10.25•166.82166.82142,325.7626•••
PLA009-20.25••••
PLA010-10.25••••
PLA011-10.25•2.972.971475.7429•••
PLA011-20.25•31.9431.9414•••
PLA012-10.25••••
PLA013-10.25•148.14148.1414•••
PLA014-10.25•952.24952.2415•••
PLA014-20.25•123.91123.9115•••
PLA015-10.25•••
PLA018-10.25•••
PLA021-10.25•951.45951.4518•••
PLA023-10.25•••
RNG004-30.25•3.383.384•••
SYN311-10.25•0.211.14131.53130.2160.2060.2282.2790.258•••
SYN333-10.25•0.060.0620.0660.0660.0660.0660.066••••
SYN556-10.25•0.250.25629.491379.1013208.9213337.5113••••
SYN557-10.25•0.060.0640.1070.5770.5750.5951.2970.1170.1270.117••••
SYN563-10.25•0.354.4170.3510397.15101.01102.01102.2310••••
SYN588-10.25•0.060.0620.0630.0730.0630.0730.0630.063••••
SYN589-10.25•0.060.0620.0630.0730.0630.0630.0630.063••••
SYN598-10.25•0.070.0740.0880.1680.0880.0880.088••••
SYN599-10.25•0.100.1050.1090.9090.1190.1290.119••••
SYN601-10.25•0.060.0650.1311102.58110.27110.57111.5811••••
SYN614-10.25•6.596.5962,008.1314••••
SYN616-10.25•0.060.0640.0790.4590.0990.1090.109••••
SYN617-10.25•0.220.2260.33102.4790.2860.32672.50100.50100.95100.8010••••
SYN631-10.25•9.71266.8079.71121,359.761218.101226.911237.8512•••
SYN637-10.25•0.060.0640.0770.1270.0770.0770.077••••
SYN638-10.25•0.060.0640.0770.1270.0770.0770.077••••
SYN646-10.25•0.080.0850.291174.41110.91111.47112.7211••••
SYN649-10.25•0.070.0760.0780.0880.8170.9870.1180.0780.0880.078••••
SYN653-10.25•0.61202.4680.6111274.3011780.86111.26112.80116.1211•••
SYN654-10.25•0.165.0070.161017.551052.41100.25100.47100.6410••••
SYN655-10.25•0.168.1970.161017.541053.40100.29100.47100.6410••••
SYN688-10.25•2.284.3162.2811481.611113.851121.431129.4311••••
SYN689-10.25•1.652.8561.6511411.161112.231118.591125.3111••••
SYN702-10.25•0.060.0630.0760.1760.0760.0760.076••••
SYN703-10.25•0.080.0860.119171.0890.4490.7390.819••••
SYN704-10.25•0.060.0640.09836.4380.1980.2780.278••••
SYN705-10.25•0.080.0860.129172.5690.4190.7490.829••••
SYN706-10.25•0.070.0750.1096.3190.1390.1990.219••••
SYN709-10.25•0.070.0750.0780.1380.0780.0780.078••••
SYN711-10.25•0.060.0630.0740.0740.0740.0740.0740.074••••
SYN712-10.25•0.070.0760.109102.5690.3090.5090.629••••
SYN716-10.25•0.060.0650.0884.4980.1080.1480.138••••
SYO691-1.0020.2522.0422.041444.522387.5423
ANA003-20.50
LCL001-10.50
LCL028-10.50
LCL061-10.50
LCL124-10.50
LCL253-10.50•58.8058.8010••
LCL374-10.50
LCL377-10.50
LCL395-10.50
LCL417-20.50
LCL428-10.50
LCL875-10.50
PLA008-10.50••••
PUZ050-10.50
SWV014-10.50••••
SYN600-10.50•2.802.8071,371.1414••••
SYN615-10.50•40.1240.127•••
SYN639-10.50•0.070.0750.6912642.97124.63128.401232.4012••••
SYN640-10.50•0.070.0750.7012641.34124.65128.391232.3812••••
SYN647-10.50•0.070.0750.281174.33110.88111.47112.7211••••
SYN707-10.50•4.584.58623.9812148.5612231.9112470.6712••••
SYN708-10.50•4.584.58623.5512147.5112232.0412470.2212••••
SYN982-10.50•••
LCL063-10.75
LCL109-10.75
LCL417-10.75
LCL422-10.75
LCL423-10.75
LCL927-10.75
LCL928-10.75
LCL929-10.75
GEO001-41.00
LCL419-11.00
LCL420-11.00
LCL421-11.00
LCL424-11.00
LCL425-11.00
LCL426-11.00
LCL427-11.00
LCL926-11.00
ROB025-11.00
SYO691-1.0031.00
SYO691-1.0041.00
SYO691-1.0051.00
ProblemRatingCM-TABXH-1-5H-1H-2H-3H-4H-5H-6H-7H-8H-9CMProverSETHEOslazyCop 0.1SATCop 0.1
Totals of 562:430421413390250239236327365355351414387338394