Page updated 19/05/2013.

I am implementing a Calculus Of Constructions based Automated Theorem Prover: cocATP.

The system description for The 24ยบ CADE ATP System Competition.

34/200 solved of the THF 2012 battery in local tests:
SWV447^1 in 4.02715992928 (v5.4.0 rating: 0.33)
SEU585^2 in 14.8452968597 (v5.4.0 rating: 0.33)
SEU592^2 in 0.649981975555 (v5.4.0 rating: 0.33)
SYO287^5 in 10.0150780678 (v5.4.0 rating: 0.60)
LCL730^5 in 1.61012196541 (v5.4.0 rating: 0.60)
LCL741^5 in 3.20630979538 (v5.4.0 rating: 0.60)
SEV310^5 in 10.6719009876 (v5.4.0 rating: 0.60)
LCL740^5 in 2.72701883316 (v5.4.0 rating: 0.60)
NUM419^1 in 28.2771999836 (v5.4.0 rating: 0.33)
LCL728^5 in 1.87325501442 (v5.4.0 rating: 0.60)
SEU649^2 in 89.0511090755 (v5.4.0 rating: 0.33)
SYN999^1 in 0.6495449543 (v5.4.0 rating: 0.33)
LCL731^5 in 92.0969810486 (v5.4.0 rating: 0.60)
SYO226^5 in 1.86965298653 (v5.4.0 rating: 0.33)
SEU960^5 in 111.909964085 (v5.4.0 rating: 0.80)
SEU508^2 in 3.97644901276 (v5.4.0 rating: 0.33)
LCL734^5 in 2.60430383682 (v5.4.0 rating: 0.80)
LCL738^5 in 2.59439706802 (v5.4.0 rating: 0.80)
SYO364^5 in 134.446177006 (v5.4.0 rating: 0.80)
SEV225^5 in 12.2766680717 (v5.4.0 rating: 0.33)
SYO514^1 in 0.990988969803 (v5.4.0 rating: 0.80)
SYO309^5 in 1.67491793633 (v5.4.0 rating: 0.80)
LCL736^5 in 3.02055716515 (v5.4.0 rating: 0.80)
SEU666^2 in 1.85143208504 (v5.4.0 rating: 0.33)
SEU685^2 in 3.58294796944 (v5.4.0 rating: 0.33)
SEU675^2 in 1.93615889549 (v5.4.0 rating: 0.33)
SEU642^2 in 48.077865839 (v5.4.0 rating: 0.33)
SWW478^3 in 13.3726868629 (v5.4.0 rating: 0.50)
SWW470^1 in 70.7626700401 (v5.4.0 rating: 0.50)
SYO008^1 in 2.09907388687 (v5.4.0 rating: 0.50)
SCT171^1 in 87.4044189453 (v5.4.0 rating: 0.50)
SYO304^5 in 0.892263889313 (v5.4.0 rating: 0.67)
NUM800^1 in 36.2824540138 (v5.4.0 rating: 0.83)
ALG269^2 in 226.738154888 (v5.4.0 rating: 0.83)