---------------------------------------------------------------------------- Abbreviations ---------------------------------------------------------------------------- --- Timeout (or unspecified). -g- GaveUp (Used only by CASC). -u- Unknown (Used only by CASC). -m- Out of Memory (Used only by KRH). -l- Max number of vars exceeded (Used only by KRH). -?- No result available. -x- Tptp2X preprocessing failure. -p- Preprocessing failure. % /home/wernhard/krh_eval/tables/nne.pl compiled 0.02 sec, 159,816 bytes % /home/wernhard/krh_eval/tables/krh_nne.pl compiled 0.01 sec, 36,792 bytes ---------------------------------------------------------------------------- Problem set tptp_nne(satisfiable, range restricted), 63 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, satisfiable and range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 52 solved Prob. Rating \ Prover| 1| ---------------------|------| SYN906-1 1.00| ---| SYN910-1 1.00| ---| SYN911-1 1.00| ---| SYN913-1 1.00| ---| SYN903-1 0.75| ---| SYN904-1 0.75| ---| SYN905-1 0.75| ---| SYN907-1 0.75| ---| SYN908-1 0.75| ---| SYN909-1 0.75| ---| SYN912-1 0.75| ---| GRP131-2.005 0.67| 0.1| GRP132-2.005 0.67| 0.1| GRP135-1.005 0.67| 0.1| GRP129-1.005 0.50| 0.0| GRP129-2.005 0.50| 0.0| GRP129-3.005 0.50| 0.1| GRP129-4.005 0.50| 0.0| GRP130-1.005 0.50| 0.0| GRP130-2.005 0.50| 0.0| GRP131-1.005 0.50| 0.1| GRP132-1.005 0.50| 0.1| GRP133-1.004 0.50| 0.0| GRP134-1.005 0.50| 0.0| GRP134-2.005 0.50| 0.0| GRP135-2.005 0.50| 0.1| HWV035-1 0.50| 0.0| HWV036-1 0.50| 0.0| GRP128-4.004 0.33| 0.0| GRP130-4.004 0.33| 0.0| HWV036-2 0.25| 0.0| GRP128-1.004 0.17| 0.0| GRP128-2.004 0.17| 0.0| GRP128-3.004 0.17| 0.0| GRP130-3.004 0.17| 0.0| GRP133-2.004 0.17| 0.0| HWV034-1 0.00| 0.0| HWV034-2 0.00| 0.0| HWV035-2 0.00| 0.0| KRS005-1 0.00| 0.0| KRS011-1 0.00| 0.0| KRS014-1 0.00| 0.0| NLP114-1 0.00| 0.0| NLP115-1 0.00| 0.0| NLP116-1 0.00| 0.0| NLP118-1 0.00| 0.0| NLP119-1 0.00| 0.0| NLP120-1 0.00| 0.0| NLP121-1 0.00| 0.0| NLP123-1 0.00| 0.0| NUM285-1 0.00| 0.0| PUZ001-3 0.00| 0.0| PUZ016-2.004 0.00| 0.0| PUZ028-1 0.00| 0.0| PUZ028-2 0.00| 0.0| PUZ028-3 0.00| 0.1| PUZ028-4 0.00| 0.1| SYN056-1 0.00| 0.0| SYN059-1 0.00| 0.0| SYN091-1.003 0.00| 0.0| SYN092-1.003 0.00| 0.0| SYN431-1 0.00| 0.0| SYN497-1 0.00| 0.0| ---------------------------------------------------------------------------- Problem set tptp_nne(satisfiable, not range restricted), 331 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, satisfiable and not range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 67 solved Prob. Rating \ Prover| 1| ---------------------|------| MSC008-1.010 1.00| ---| PUZ034-1.003 1.00| ---| SYN519-1 0.83| ---| SYN812-1 0.83| -m-| SYN816-1 0.83| -m-| SYN817-1 0.83| -m-| SYN818-1 0.83| -m-| SYN821-1 0.83| -m-| SYN825-1 0.83| -m-| SYN826-1 0.83| -m-| SYN829-1 0.83| -m-| SYN830-1 0.83| -m-| SYN831-1 0.83| -m-| SYN832-1 0.83| -m-| SYN839-1 0.83| -m-| SYN840-1 0.83| -m-| SYN841-1 0.83| -m-| SYN842-1 0.83| -m-| SYN852-1 0.83| -m-| SYN853-1 0.83| -m-| SYN854-1 0.83| -m-| SYN855-1 0.83| -m-| SYN864-1 0.83| -m-| NLP027-1 0.75| ---| NLP028-1 0.75| ---| NLP029-1 0.75| ---| NLP030-1 0.75| ---| NLP032-1 0.75| ---| NLP034-1 0.75| ---| SET781-1 0.75| ---| SYN765-1 0.75| ---| SYN767-1 0.75| ---| SYN770-1 0.75| ---| SYN771-1 0.75| ---| SYN773-1 0.75| ---| SYN776-1 0.75| ---| SYN777-1 0.75| ---| SYN778-1 0.75| ---| SYN779-1 0.75| ---| SYN781-1 0.75| ---| SYN782-1 0.75| ---| SYN783-1 0.75| ---| SYN788-1 0.75| ---| SYN789-1 0.75| ---| SYN792-1 0.75| ---| SYN793-1 0.75| ---| SYN794-1 0.75| ---| SYN795-1 0.75| ---| SYN803-1 0.75| ---| SYN805-1 0.75| ---| SYN806-1 0.75| ---| SYN807-1 0.75| ---| SYN808-1 0.75| ---| SYN809-1 0.75| ---| SYN810-1 0.75| ---| TOP001-1 0.75| ---| TOP002-1 0.75| ---| TOP003-1 0.75| ---| TOP005-1 0.75| ---| TOP006-1 0.75| ---| TOP008-1 0.75| ---| TOP009-1 0.75| ---| TOP012-1 0.75| ---| TOP013-1 0.75| ---| TOP015-1 0.75| ---| TOP017-1 0.75| ---| TOP018-1 0.75| ---| TOP019-1 0.75| ---| GRP127-4.005 0.67| 0.0| SYN426-1 0.67| ---| SYN441-1 0.67| ---| SYN464-1 0.67| ---| SYN514-1 0.67| ---| SYN815-1 0.67| -m-| SYN824-1 0.67| -m-| SYN828-1 0.67| -m-| SYN838-1 0.67| -m-| SYN851-1 0.67| -m-| SYN863-1 0.67| -m-| GRP123-1.005 0.50| 0.0| GRP123-2.005 0.50| 0.0| GRP123-6.005 0.50| 0.5| GRP123-7.005 0.50| 0.5| GRP124-1.005 0.50| 0.0| GRP124-2.005 0.50| 0.0| GRP124-3.005 0.50| 0.1| GRP124-4.005 0.50| 0.0| GRP124-6.005 0.50| 0.0| GRP124-7.005 0.50| 0.0| GRP124-8.005 0.50| 0.0| GRP124-9.005 0.50| 0.3| GRP126-1.005 0.50| 0.0| GRP126-3.005 0.50| 0.0| GRP126-4.005 0.50| 0.0| GRP127-1.005 0.50| 0.0| NLP026-1 0.50| ---| NLP031-1 0.50| ---| NLP033-1 0.50| ---| NLP035-1 0.50| ---| NLP060-1 0.50| ---| NLP061-1 0.50| ---| NLP062-1 0.50| ---| NLP063-1 0.50| ---| NLP065-1 0.50| ---| NLP160-1 0.50| ---| NLP161-1 0.50| ---| NLP162-1 0.50| ---| NLP163-1 0.50| ---| NLP164-1 0.50| ---| NLP165-1 0.50| ---| NLP166-1 0.50| ---| NLP167-1 0.50| ---| NLP168-1 0.50| ---| NLP169-1 0.50| ---| NLP190-1 0.50| ---| NLP191-1 0.50| ---| NLP192-1 0.50| ---| NLP193-1 0.50| ---| NLP194-1 0.50| ---| NLP195-1 0.50| ---| NLP196-1 0.50| ---| NLP197-1 0.50| ---| NLP198-1 0.50| ---| NLP199-1 0.50| ---| NUM288-1 0.50| ---| SYN307-1 0.50| 0.0| SYN428-1 0.50| ---| SYN434-1 0.50| ---| SYN437-1 0.50| ---| SYN449-1 0.50| ---| SYN453-1 0.50| ---| SYN456-1 0.50| ---| SYN520-1 0.50| ---| SYN542-1 0.50| ---| SYN543-1 0.50| ---| SYN736-1 0.50| ---| SYN745-1 0.50| ---| SYN746-1 0.50| ---| SYN747-1 0.50| ---| SYN750-1 0.50| ---| SYN751-1 0.50| ---| SYN752-1 0.50| ---| SYN753-1 0.50| ---| SYN754-1 0.50| ---| SYN757-1 0.50| ---| SYN761-1 0.50| ---| SYN763-1 0.50| ---| SYN764-1 0.50| ---| SYN766-1 0.50| ---| SYN768-1 0.50| ---| SYN769-1 0.50| ---| SYN775-1 0.50| ---| SYN780-1 0.50| ---| SYN787-1 0.50| ---| SYN790-1 0.50| ---| SYN791-1 0.50| ---| SYN797-1 0.50| ---| SYN798-1 0.50| ---| SYN799-1 0.50| ---| SYN800-1 0.50| ---| SYN801-1 0.50| ---| SYN804-1 0.50| ---| SYN811-1 0.50| ---| SYN888-1 0.50| ---| TOP010-1 0.50| ---| TOP011-1 0.50| ---| TOP014-1 0.50| ---| TOP016-1 0.50| ---| GRP123-4.004 0.33| 0.0| GRP125-4.004 0.33| 0.0| GRP126-2.005 0.33| 0.0| GRP127-3.005 0.33| 0.1| SYN418-1 0.33| -m-| SYN420-1 0.33| ---| SYN423-1 0.33| ---| SYN424-1 0.33| ---| SYN425-1 0.33| ---| SYN427-1 0.33| ---| SYN429-1 0.33| ---| SYN438-1 0.33| 0.5| SYN446-1 0.33| ---| SYN463-1 0.33| 5.8| SYN513-1 0.33| ---| SYN518-1 0.33| ---| SYN544-1 0.33| 10.6| SYN545-1 0.33| ---| SYN546-1 0.33| ---| SYN823-1 0.33| ---| SYN827-1 0.33| ---| SYN835-1 0.33| ---| SYN872-1 0.33| ---| SYN902-1 0.33| ---| NLP059-1 0.25| ---| NLP064-1 0.25| ---| PUZ044-1 0.25| ---| PUZ045-1 0.25| ---| SYN036-2 0.25| ---| SYN316-1 0.25| ---| SYN324-1 0.25| ---| SYN330-1 0.25| ---| SYN335-1 0.25| ---| SYN351-1 0.25| ---| SYN734-1 0.25| ---| SYN737-1 0.25| ---| SYN740-1 0.25| ---| SYN741-1 0.25| ---| SYN742-1 0.25| ---| SYN743-1 0.25| ---| SYN748-1 0.25| ---| SYN749-1 0.25| ---| SYN760-1 0.25| ---| SYN774-1 0.25| ---| SYN785-1 0.25| ---| SYN786-1 0.25| ---| TOP003-2 0.25| ---| GRP123-3.004 0.17| 0.0| GRP123-8.004 0.17| 0.0| GRP123-9.004 0.17| 0.1| GRP125-1.004 0.17| 0.0| GRP125-2.004 0.17| 0.0| GRP125-3.004 0.17| 0.0| GRP127-2.005 0.17| 0.0| PUZ018-2 0.17| 2.3| SYN419-1 0.17| ---| SYN421-1 0.17| 241.2| SYN422-1 0.17| ---| SYN435-1 0.17| ---| SYN539-1 0.17| 0.3| SYN547-1 0.17| ---| SYN867-1 0.17| ---| SYN868-1 0.17| ---| SYN870-1 0.17| ---| KRS006-1 0.00| -m-| KRS007-1 0.00| -m-| KRS008-1 0.00| ---| KRS009-1 0.00| -m-| KRS016-1 0.00| -m-| MSC009-1 0.00| ---| NLP043-1 0.00| ---| NLP044-1 0.00| ---| NLP045-1 0.00| ---| NLP046-1 0.00| ---| NLP047-1 0.00| ---| NLP048-1 0.00| ---| NLP066-1 0.00| ---| NLP067-1 0.00| ---| NLP068-1 0.00| ---| NLP095-1 0.00| ---| NLP096-1 0.00| ---| NLP097-1 0.00| ---| NLP098-1 0.00| ---| NLP099-1 0.00| ---| NLP100-1 0.00| ---| NLP101-1 0.00| ---| NLP102-1 0.00| ---| NLP103-1 0.00| ---| NLP130-1 0.00| ---| NLP131-1 0.00| ---| NLP132-1 0.00| ---| NLP133-1 0.00| ---| NLP134-1 0.00| ---| NLP135-1 0.00| ---| NLP136-1 0.00| ---| NLP137-1 0.00| ---| NLP138-1 0.00| ---| NLP139-1 0.00| ---| NLP221-1 0.00| -m-| NLP222-1 0.00| -m-| NLP223-1 0.00| -m-| NLP230-1 0.00| -m-| NLP231-1 0.00| -m-| NLP232-1 0.00| -m-| NLP233-1 0.00| -m-| NLP234-1 0.00| -m-| NLP235-1 0.00| -m-| NLP236-1 0.00| -m-| NLP237-1 0.00| -m-| NLP238-1 0.00| -m-| NLP239-1 0.00| -m-| SET777-1 0.00| ---| SET778-1 0.00| ---| SET779-1 0.00| ---| SET780-1 0.00| ---| SYN084-1 0.00| ---| SYN304-1 0.00| -m-| SYN306-1 0.00| ---| SYN308-1 0.00| ---| SYN309-1 0.00| ---| SYN317-1 0.00| 0.0| SYN320-1 0.00| ---| SYN344-1 0.00| ---| SYN348-1 0.00| ---| SYN430-1 0.00| 0.0| SYN432-1 0.00| ---| SYN433-1 0.00| 2.0| SYN490-1 0.00| 0.0| SYN491-1 0.00| 0.0| SYN492-1 0.00| 0.0| SYN493-1 0.00| 0.0| SYN494-1 0.00| 0.0| SYN495-1 0.00| 0.0| SYN496-1 0.00| 0.0| SYN515-1 0.00| 0.2| SYN516-1 0.00| 0.0| SYN517-1 0.00| 0.1| SYN521-1 0.00| 0.0| SYN522-1 0.00| 0.4| SYN523-1 0.00| 0.0| SYN524-1 0.00| 0.1| SYN525-1 0.00| 5.8| SYN526-1 0.00| 0.1| SYN527-1 0.00| 0.1| SYN528-1 0.00| 0.1| SYN529-1 0.00| ---| SYN530-1 0.00| 0.1| SYN531-1 0.00| 0.3| SYN532-1 0.00| 0.0| SYN533-1 0.00| 0.0| SYN534-1 0.00| 0.1| SYN535-1 0.00| 0.0| SYN536-1 0.00| 0.1| SYN537-1 0.00| 0.1| SYN538-1 0.00| 0.2| SYN540-1 0.00| 0.8| SYN541-1 0.00| 0.2| SYN735-1 0.00| ---| SYN738-1 0.00| ---| SYN739-1 0.00| ---| SYN744-1 0.00| ---| SYN756-1 0.00| ---| SYN772-1 0.00| ---| ---------------------------------------------------------------------------- Problem set tptp_nne(unsatisfiable, range restricted), 235 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, unsatisfiable and range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 164 solved Prob. Rating \ Prover| 1| ---------------------|------| FLD050-1 1.00| ---| FLD050-2 1.00| ---| FLD072-4 1.00| ---| FLD005-1 0.67| ---| FLD007-3 0.67| 146.5| FLD008-4 0.67| 3.0| FLD009-1 0.67| ---| FLD010-5 0.67| 1.0| FLD011-3 0.67| ---| FLD012-4 0.67| 36.9| FLD014-3 0.67| 26.6| FLD015-1 0.67| ---| FLD016-1 0.67| ---| FLD020-1 0.67| ---| FLD022-1 0.67| ---| FLD024-1 0.67| ---| FLD025-2 0.67| ---| FLD026-3 0.67| 115.9| FLD027-1 0.67| ---| FLD028-1 0.67| ---| FLD033-1 0.67| ---| FLD035-1 0.67| ---| FLD036-1 0.67| ---| FLD038-1 0.67| ---| FLD040-1 0.67| ---| FLD041-3 0.67| 1.0| FLD041-4 0.67| 2.1| FLD042-3 0.67| 1.0| FLD043-5 0.67| ---| FLD047-4 0.67| ---| FLD048-4 0.67| ---| FLD049-3 0.67| ---| FLD049-4 0.67| 11.5| FLD050-3 0.67| ---| FLD050-4 0.67| 11.5| FLD051-4 0.67| ---| FLD052-4 0.67| ---| FLD054-4 0.67| ---| FLD062-3 0.67| ---| FLD063-1 0.67| ---| FLD065-1 0.67| ---| FLD068-1 0.67| ---| FLD068-2 0.67| ---| FLD097-4 0.67| ---| MSC007-1.008 0.56| 32.3| GRP128-2.006 0.44| 2.0| PUZ010-1 0.44| 3.3| FLD001-3 0.33| 0.1| FLD002-3 0.33| 0.1| FLD003-1 0.33| ---| FLD004-1 0.33| ---| FLD005-3 0.33| ---| FLD009-3 0.33| ---| FLD013-1 0.33| ---| FLD013-2 0.33| ---| FLD013-3 0.33| 232.4| FLD013-4 0.33| 0.4| FLD013-5 0.33| 0.6| FLD015-3 0.33| 0.6| FLD016-3 0.33| 2.9| FLD016-5 0.33| 5.2| FLD017-1 0.33| ---| FLD017-3 0.33| 0.2| FLD018-1 0.33| ---| FLD019-1 0.33| ---| FLD021-1 0.33| ---| FLD022-3 0.33| 2.9| FLD023-1 0.33| ---| FLD025-1 0.33| ---| FLD025-3 0.33| 236.5| FLD025-4 0.33| 0.4| FLD025-5 0.33| 0.6| FLD027-3 0.33| 1.0| FLD028-3 0.33| 3.5| FLD029-3 0.33| 24.6| FLD030-1 0.33| 0.0| FLD030-2 0.33| ---| FLD030-3 0.33| 65.0| FLD030-4 0.33| 0.2| FLD031-1 0.33| ---| FLD032-1 0.33| ---| FLD034-1 0.33| ---| FLD035-3 0.33| 3.5| FLD036-3 0.33| 3.5| FLD037-1 0.33| ---| FLD037-3 0.33| 0.8| FLD038-3 0.33| 0.6| FLD040-3 0.33| 0.3| FLD040-5 0.33| 0.3| FLD055-3 0.33| 0.1| FLD058-3 0.33| 0.1| FLD059-1 0.33| ---| FLD059-2 0.33| ---| FLD059-3 0.33| 6.2| FLD059-4 0.33| 0.1| FLD060-1 0.33| ---| FLD060-2 0.33| ---| FLD060-3 0.33| ---| FLD060-4 0.33| 234.7| FLD061-1 0.33| ---| FLD061-2 0.33| ---| FLD061-3 0.33| ---| FLD061-4 0.33| ---| FLD063-3 0.33| ---| FLD064-1 0.33| ---| FLD064-3 0.33| 4.5| FLD065-3 0.33| 0.2| FLD066-3 0.33| 5.3| FLD067-1 0.33| ---| FLD067-2 0.33| ---| FLD067-3 0.33| ---| FLD067-4 0.33| 1.5| FLD068-3 0.33| ---| FLD068-4 0.33| 1.5| FLD069-1 0.33| ---| FLD069-3 0.33| 0.1| FLD070-1 0.33| ---| FLD070-2 0.33| ---| FLD070-3 0.33| 27.1| FLD070-4 0.33| 0.1| FLD071-1 0.33| 0.0| FLD071-2 0.33| ---| FLD071-3 0.33| 20.3| HWV006-1 0.33| 0.0| HWV006-2 0.33| 0.0| HWV007-1 0.33| 0.0| HWV007-2 0.33| 0.0| PUZ035-3 0.33| 0.0| PUZ035-4 0.33| 0.0| GRP128-3.005 0.22| 0.3| GRP129-3.004 0.11| 0.0| GRP129-4.004 0.11| 0.0| PUZ028-6 0.11| 0.1| FLD006-1 0.00| ---| FLD006-3 0.00| 0.0| FLD010-1 0.00| ---| FLD010-3 0.00| 0.0| FLD018-3 0.00| 0.2| FLD019-3 0.00| 0.2| FLD020-3 0.00| 0.6| FLD021-3 0.00| 0.0| FLD023-3 0.00| 0.6| FLD024-3 0.00| 0.5| FLD031-3 0.00| 0.3| FLD031-5 0.00| 5.8| FLD032-3 0.00| 0.2| FLD033-3 0.00| 0.6| FLD034-3 0.00| 0.0| FLD039-1 0.00| 0.0| FLD039-3 0.00| 0.0| FLD043-3 0.00| 0.6| FLD055-1 0.00| 0.0| FLD056-1 0.00| 0.0| FLD056-3 0.00| 0.0| FLD058-1 0.00| 0.0| FLD071-4 0.00| 0.0| GRA001-1 0.00| 0.0| GRP128-1.003 0.00| 0.0| GRP128-4.003 0.00| 0.0| GRP129-1.003 0.00| 0.0| GRP129-2.004 0.00| 0.0| GRP130-1.003 0.00| 0.0| GRP130-2.003 0.00| 0.0| GRP130-3.003 0.00| 0.0| GRP130-4.003 0.00| 0.0| GRP131-1.002 0.00| 0.0| GRP131-2.002 0.00| 0.0| GRP132-1.002 0.00| 0.0| GRP132-2.002 0.00| 0.0| GRP133-1.003 0.00| 0.0| GRP133-2.003 0.00| 0.0| GRP134-1.003 0.00| 0.0| GRP134-2.003 0.00| 0.0| GRP135-1.002 0.00| 0.0| GRP135-2.002 0.00| 0.0| HWV005-1 0.00| 0.0| HWV005-2 0.00| 0.0| HWV008-1.001 0.00| 0.0| HWV008-1.002 0.00| 0.0| HWV008-2.001 0.00| 0.0| HWV008-2.002 0.00| 0.0| KRS010-1 0.00| 0.0| KRS017-1 0.00| 0.0| LCL181-2 0.00| 0.0| LCL230-2 0.00| 0.0| MGT004-1 0.00| 0.0| MGT007-1 0.00| 0.0| MGT016-1 0.00| 0.0| MGT018-1 0.00| 0.0| MGT022-1 0.00| 0.0| MGT022-2 0.00| 0.0| MGT028-1 0.00| 0.0| MGT030-1 0.00| 0.0| MGT041-2 0.00| 0.0| NLP001-1 0.00| 0.0| NLP117-1 0.00| 0.0| NLP122-1 0.00| 0.0| NUM022-1 0.00| 0.0| PUZ001-1 0.00| 0.0| PUZ004-1 0.00| 0.0| PUZ009-1 0.00| 0.0| PUZ013-1 0.00| 0.0| PUZ014-1 0.00| 0.0| PUZ015-2.006 0.00| 3.0| PUZ016-2.005 0.00| 0.2| PUZ028-5 0.00| 0.1| PUZ031-1 0.00| 0.0| PUZ033-1 0.00| 0.0| PUZ035-1 0.00| 0.0| PUZ035-2 0.00| 0.0| SYN001-1.005 0.00| 0.0| SYN008-1 0.00| 0.0| SYN009-1 0.00| 0.0| SYN009-2 0.00| 0.0| SYN009-3 0.00| 0.0| SYN009-4 0.00| 0.1| SYN011-1 0.00| 0.0| SYN028-1 0.00| 0.0| SYN029-1 0.00| 0.0| SYN030-1 0.00| 0.0| SYN032-1 0.00| 0.0| SYN044-1 0.00| 0.0| SYN045-1 0.00| 0.0| SYN047-1 0.00| 0.0| SYN054-1 0.00| 0.0| SYN055-1 0.00| 0.0| SYN069-1 0.00| 0.0| SYN070-1 0.00| 0.0| SYN082-1 0.00| 0.0| SYN093-1.002 0.00| 0.0| SYN094-1.005 0.00| 0.0| SYN097-1.002 0.00| 0.0| SYN098-1.002 0.00| 0.0| SYN354-1 0.00| 0.0| SYN724-1 0.00| 0.0| ---------------------------------------------------------------------------- Problem set tptp_nne(unsatisfiable, not range restricted), 399 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, unsatisfiable and not range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 137 solved Prob. Rating \ Prover| 1| ---------------------|------| GRP025-3 1.00| ---| GRP026-3 1.00| ---| GRP027-2 1.00| ---| TOP007-1 1.00| ---| ANA002-1 0.67| ---| ANA002-3 0.67| ---| COM003-1 0.67| ---| PUZ034-1.004 0.67| ---| SET010-1 0.67| ---| SET012-1 0.67| ---| SET012-2 0.67| 117.5| SET013-1 0.67| ---| SET013-2 0.67| ---| SET015-1 0.67| ---| SET015-2 0.67| ---| SYN067-1 0.67| ---| SYN067-2 0.67| ---| SYN067-3 0.67| ---| SYN314-1.002.001 0.67| ---| SYN436-1 0.67| ---| SYN439-1 0.67| ---| SYN440-1 0.67| ---| SYN457-1 0.67| ---| SYN460-1 0.67| ---| SYN466-1 0.67| ---| SYN802-1 0.67| 218.2| SYN850-1 0.62| -m-| SYN861-1 0.62| -m-| SYN862-1 0.62| -m-| SYN865-1 0.62| -m-| SYN866-1 0.62| -m-| SYN442-1 0.56| ---| SYN443-1 0.56| ---| SYN447-1 0.56| ---| SYN454-1 0.56| ---| SYN455-1 0.56| ---| SYN458-1 0.56| ---| SYN465-1 0.56| ---| SYN468-1 0.56| ---| SYN469-1 0.56| ---| SYN470-1 0.56| ---| SYN471-1 0.56| ---| SYN472-1 0.56| ---| SYN473-1 0.56| ---| SYN474-1 0.56| ---| SYN476-1 0.56| ---| SYN477-1 0.56| ---| SYN479-1 0.56| ---| SYN481-1 0.56| ---| SYN482-1 0.56| ---| SYN485-1 0.56| ---| SYN486-1 0.56| ---| SYN487-1 0.56| ---| SYN488-1 0.56| ---| SYN499-1 0.56| ---| SYN500-1 0.56| ---| SYN503-1 0.56| ---| SYN507-1 0.56| ---| SYN844-1 0.50| -m-| SYN846-1 0.50| -m-| SYN847-1 0.50| -m-| PUZ017-1 0.44| ---| SYN444-1 0.44| ---| SYN448-1 0.44| ---| SYN450-1 0.44| ---| SYN459-1 0.44| ---| SYN467-1 0.44| ---| SYN475-1 0.44| ---| SYN478-1 0.44| ---| SYN483-1 0.44| ---| SYN489-1 0.44| ---| SYN498-1 0.44| ---| SYN502-1 0.44| ---| SYN511-1 0.44| 105.5| SYN512-1 0.44| ---| SYN813-1 0.38| ---| SYN819-1 0.38| ---| SYN820-1 0.38| ---| SYN833-1 0.38| ---| SYN834-1 0.38| ---| SYN836-1 0.38| ---| SYN837-1 0.38| -m-| SYN843-1 0.38| -m-| SYN845-1 0.38| ---| SYN848-1 0.38| -m-| SYN849-1 0.38| -m-| SYN856-1 0.38| ---| SYN857-1 0.38| ---| SYN858-1 0.38| -m-| SYN859-1 0.38| -m-| SYN860-1 0.38| -m-| SYN885-1 0.38| ---| SYN896-1 0.38| ---| SYN897-1 0.38| ---| SYN898-1 0.38| ---| SYN901-1 0.38| ---| ANA002-2 0.33| ---| ANA002-4 0.33| ---| ANA003-4 0.33| ---| ANA004-4 0.33| ---| GRP039-6 0.33| 8.5| PUZ035-7 0.33| ---| SET014-2 0.33| ---| SYN015-2 0.33| 0.0| SYN036-1 0.33| ---| SYN353-1 0.33| ---| SYN451-1 0.33| ---| SYN452-1 0.33| ---| SYN461-1 0.33| ---| SYN462-1 0.33| ---| SYN480-1 0.33| ---| SYN501-1 0.33| ---| SYN505-1 0.33| ---| SYN506-1 0.33| 105.5| SYN508-1 0.33| ---| SYN509-1 0.33| 246.7| SYN568-1 0.33| ---| SYN576-1 0.33| ---| SYN595-1 0.33| ---| SYN604-1 0.33| ---| SYN606-1 0.33| ---| SYN607-1 0.33| ---| SYN609-1 0.33| ---| SYN610-1 0.33| ---| SYN611-1 0.33| ---| SYN612-1 0.33| ---| SYN620-1 0.33| ---| SYN625-1 0.33| ---| SYN633-1 0.33| ---| SYN634-1 0.33| ---| SYN635-1 0.33| ---| SYN636-1 0.33| ---| SYN641-1 0.33| ---| SYN642-1 0.33| ---| SYN643-1 0.33| ---| SYN644-1 0.33| ---| SYN645-1 0.33| ---| SYN650-1 0.33| ---| SYN657-1 0.33| ---| SYN658-1 0.33| ---| SYN659-1 0.33| ---| SYN673-1 0.33| ---| SYN687-1 0.33| ---| SYN690-1 0.33| ---| SYN692-1 0.33| ---| SYN693-1 0.33| ---| SYN694-1 0.33| ---| SYN695-1 0.33| ---| SYN696-1 0.33| ---| SYN697-1 0.33| ---| SYN698-1 0.33| ---| SYN699-1 0.33| ---| SYN700-1 0.33| ---| SYN701-1 0.33| ---| SYN714-1 0.33| ---| SYN755-1 0.33| 0.1| SYN758-1 0.33| 0.7| SYN759-1 0.33| 0.9| SYN762-1 0.33| 0.8| SYN784-1 0.33| 0.2| SYN796-1 0.33| 0.2| TOP005-2 0.33| ---| SYN876-1 0.25| ---| SYN883-1 0.25| ---| SYN884-1 0.25| ---| SYN886-1 0.25| ---| SYN887-1 0.25| ---| SYN891-1 0.25| ---| SYN893-1 0.25| ---| SYN899-1 0.25| ---| SYN900-1 0.25| ---| GRP127-2.006 0.22| 0.1| SYN484-1 0.22| ---| SYN504-1 0.22| ---| SYN510-1 0.22| ---| SYN869-1 0.12| ---| SYN871-1 0.12| ---| SYN873-1 0.12| ---| SYN874-1 0.12| ---| SYN875-1 0.12| ---| SYN877-1 0.12| ---| SYN878-1 0.12| ---| SYN879-1 0.12| ---| SYN880-1 0.12| ---| SYN881-1 0.12| ---| SYN882-1 0.12| ---| SYN889-1 0.12| ---| SYN890-1 0.12| ---| SYN892-1 0.12| ---| SYN894-1 0.12| ---| SYN895-1 0.12| ---| GRP125-2.005 0.11| 0.0| GRP126-4.004 0.11| 0.0| GRP127-4.004 0.11| 0.0| MSC008-1.002 0.11| 0.0| MSC008-2.002 0.11| 0.0| PUZ018-1 0.11| 1.0| PUZ019-1 0.11| 0.0| SYN445-1 0.11| ---| ALG002-1 0.00| 0.0| CAT007-3 0.00| 0.0| COM002-2 0.00| 0.4| COM003-2 0.00| 0.0| GRP123-1.003 0.00| 0.0| GRP123-2.003 0.00| 0.0| GRP123-3.003 0.00| 0.0| GRP123-4.003 0.00| 0.0| GRP123-6.003 0.00| 0.0| GRP123-7.003 0.00| 0.0| GRP123-8.003 0.00| 0.0| GRP123-9.003 0.00| 0.0| GRP124-1.004 0.00| 0.0| GRP124-2.004 0.00| 0.0| GRP124-3.004 0.00| 0.0| GRP124-4.004 0.00| 0.0| GRP124-6.004 0.00| 0.0| GRP124-7.004 0.00| 0.0| GRP124-8.004 0.00| 0.0| GRP124-9.004 0.00| 0.0| GRP125-1.003 0.00| 0.0| GRP125-3.005 0.00| 0.1| GRP125-4.003 0.00| 0.0| GRP126-1.004 0.00| 0.0| GRP126-2.004 0.00| 0.0| GRP126-3.004 0.00| 0.0| GRP127-1.004 0.00| 0.0| GRP127-3.004 0.00| 0.0| KRS001-1 0.00| 0.0| KRS002-1 0.00| 0.3| KRS003-1 0.00| 0.0| KRS012-1 0.00| 0.0| KRS013-1 0.00| -m-| KRS015-1 0.00| 1.2| MGT036-1 0.00| 0.1| MGT036-2 0.00| 0.1| MSC001-1 0.00| ---| MSC002-1 0.00| ---| MSC002-2 0.00| ---| MSC003-1 0.00| ---| MSC004-1 0.00| ---| MSC006-1 0.00| 0.0| NLP079-1 0.00| ---| NLP080-1 0.00| ---| NLP081-1 0.00| ---| NLP094-1 0.00| ---| NUM014-1 0.00| 0.0| NUM015-1 0.00| 0.0| NUM016-1 0.00| 0.0| NUM016-2 0.00| 0.0| NUM021-1 0.00| ---| NUM025-2 0.00| 0.0| NUM027-1 0.00| ---| PLA002-1 0.00| ---| PLA002-2 0.00| ---| PUZ002-1 0.00| 0.0| PUZ005-1 0.00| 0.0| PUZ012-1 0.00| 0.0| PUZ021-1 0.00| ---| PUZ023-1 0.00| 0.0| PUZ024-1 0.00| 0.0| PUZ025-1 0.00| 0.1| PUZ026-1 0.00| 0.0| PUZ027-1 0.00| 0.0| PUZ029-1 0.00| 0.0| PUZ030-1 0.00| 0.0| PUZ030-2 0.00| 0.0| PUZ032-1 0.00| 0.1| PUZ035-5 0.00| 0.0| PUZ035-6 0.00| 0.0| SET001-1 0.00| 0.0| SET002-1 0.00| 0.1| SET003-1 0.00| 0.1| SET004-1 0.00| 2.0| SET005-1 0.00| ---| SET006-1 0.00| 0.1| SET007-1 0.00| ---| SET008-1 0.00| ---| SET009-1 0.00| 111.5| SET011-1 0.00| ---| SET043-5 0.00| 0.0| SET044-5 0.00| 0.0| SET045-5 0.00| 0.0| SET046-5 0.00| 0.0| SET047-5 0.00| 0.0| SET055-6 0.00| ---| SET055-7 0.00| 0.0| SET786-1 0.00| 0.0| SWV001-1 0.00| 0.0| SWV009-1 0.00| 0.0| SYN002-1.007.008 0.00| 0.0| SYN006-1 0.00| 0.0| SYN012-1 0.00| ---| SYN014-2 0.00| 0.0| SYN031-1 0.00| 0.0| SYN034-1 0.00| 0.0| SYN036-3 0.00| 0.0| SYN036-4 0.00| 0.0| SYN037-1 0.00| 0.0| SYN037-2 0.00| 0.0| SYN038-1 0.00| ---| SYN039-1 0.00| ---| SYN051-1 0.00| 0.0| SYN052-1 0.00| 0.0| SYN053-1 0.00| 0.0| SYN060-1 0.00| 0.0| SYN061-1 0.00| 0.0| SYN063-1 0.00| 0.0| SYN066-1 0.00| 0.1| SYN081-1 0.00| 0.0| SYN084-2 0.00| 0.0| SYN099-1.003 0.00| 0.0| SYN100-1.005 0.00| 0.0| SYN313-1.001.002 0.00| ---| SYN315-1 0.00| 0.0| SYN319-1 0.00| 0.0| SYN321-1 0.00| 0.0| SYN323-1 0.00| 0.0| SYN325-1 0.00| 0.0| SYN326-1 0.00| 0.0| SYN327-1 0.00| 0.0| SYN328-1 0.00| 0.1| SYN331-1 0.00| ---| SYN332-1 0.00| ---| SYN334-1 0.00| ---| SYN343-1 0.00| 0.0| SYN345-1 0.00| 0.5| SYN347-1 0.00| 0.0| SYN349-1 0.00| 0.0| SYN350-1 0.00| 0.0| SYN352-1 0.00| 21.4| SYN554-1 0.00| 0.1| SYN560-1 0.00| ---| SYN567-1 0.00| 0.1| SYN571-1 0.00| ---| SYN573-1 0.00| 0.2| SYN574-1 0.00| ---| SYN575-1 0.00| ---| SYN578-1 0.00| 24.4| SYN579-1 0.00| 24.5| SYN580-1 0.00| 0.1| SYN581-1 0.00| ---| SYN582-1 0.00| ---| SYN583-1 0.00| ---| SYN585-1 0.00| ---| SYN586-1 0.00| ---| SYN587-1 0.00| ---| SYN591-1 0.00| ---| SYN592-1 0.00| ---| SYN593-1 0.00| 0.0| SYN594-1 0.00| ---| SYN605-1 0.00| ---| SYN608-1 0.00| ---| SYN613-1 0.00| ---| SYN619-1 0.00| ---| SYN621-1 0.00| ---| SYN622-1 0.00| ---| SYN623-1 0.00| ---| SYN624-1 0.00| ---| SYN626-1 0.00| ---| SYN627-1 0.00| ---| SYN630-1 0.00| 0.0| SYN648-1 0.00| ---| SYN656-1 0.00| ---| SYN660-1 0.00| ---| SYN661-1 0.00| ---| SYN662-1 0.00| ---| SYN663-1 0.00| ---| SYN664-1 0.00| ---| SYN665-1 0.00| ---| SYN666-1 0.00| ---| SYN667-1 0.00| ---| SYN668-1 0.00| ---| SYN669-1 0.00| ---| SYN670-1 0.00| ---| SYN671-1 0.00| ---| SYN672-1 0.00| ---| SYN674-1 0.00| ---| SYN675-1 0.00| ---| SYN676-1 0.00| ---| SYN677-1 0.00| ---| SYN678-1 0.00| ---| SYN679-1 0.00| ---| SYN680-1 0.00| ---| SYN681-1 0.00| ---| SYN682-1 0.00| ---| SYN683-1 0.00| ---| SYN684-1 0.00| ---| SYN685-1 0.00| ---| SYN686-1 0.00| ---| SYN710-1 0.00| ---| SYN713-1 0.00| ---| SYN717-1 0.00| ---| SYN718-1 0.00| ---| SYN726-1 0.00| 0.0| SYN728-1 0.00| ---| TOP001-2 0.00| ---| TOP002-2 0.00| 0.0| TOP004-1 0.00| 0.0| TOP004-2 0.00| 0.0| ---------------------------------------------------------------------------- Problem set tptp_nne(unknown, range restricted), 137 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, unknown and range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 0 solved Prob. Rating \ Prover| 1| ---------------------|------| FLD007-1 1.00| ---| FLD008-1 1.00| ---| FLD008-2 1.00| ---| FLD008-3 1.00| ---| FLD011-1 1.00| ---| FLD012-1 1.00| ---| FLD012-2 1.00| ---| FLD012-3 1.00| ---| FLD014-1 1.00| ---| FLD026-1 1.00| ---| FLD029-1 1.00| ---| FLD041-1 1.00| ---| FLD041-2 1.00| ---| FLD042-1 1.00| ---| FLD043-1 1.00| ---| FLD044-1 1.00| ---| FLD044-2 1.00| ---| FLD044-3 1.00| ---| FLD044-4 1.00| ---| FLD045-1 1.00| ---| FLD045-2 1.00| ---| FLD045-3 1.00| ---| FLD045-4 1.00| ---| FLD046-1 1.00| ---| FLD046-3 1.00| ---| FLD047-1 1.00| ---| FLD047-2 1.00| ---| FLD047-3 1.00| ---| FLD048-1 1.00| ---| FLD048-2 1.00| ---| FLD048-3 1.00| ---| FLD049-1 1.00| ---| FLD049-2 1.00| ---| FLD051-1 1.00| ---| FLD051-2 1.00| ---| FLD051-3 1.00| ---| FLD052-1 1.00| ---| FLD052-2 1.00| ---| FLD052-3 1.00| ---| FLD053-1 1.00| ---| FLD053-2 1.00| ---| FLD053-3 1.00| ---| FLD053-4 1.00| ---| FLD054-1 1.00| ---| FLD054-2 1.00| ---| FLD054-3 1.00| ---| FLD057-1 1.00| ---| FLD057-3 1.00| ---| FLD062-1 1.00| ---| FLD066-1 1.00| ---| FLD072-1 1.00| ---| FLD072-2 1.00| ---| FLD072-3 1.00| ---| FLD073-1 1.00| ---| FLD073-2 1.00| ---| FLD073-3 1.00| ---| FLD073-4 1.00| ---| FLD074-1 1.00| ---| FLD074-2 1.00| ---| FLD074-3 1.00| ---| FLD074-4 1.00| ---| FLD075-1 1.00| ---| FLD075-2 1.00| ---| FLD075-3 1.00| ---| FLD075-4 1.00| ---| FLD076-1 1.00| ---| FLD076-2 1.00| ---| FLD076-3 1.00| ---| FLD076-4 1.00| ---| FLD077-1 1.00| ---| FLD077-2 1.00| ---| FLD077-3 1.00| ---| FLD077-4 1.00| ---| FLD078-1 1.00| ---| FLD078-2 1.00| ---| FLD078-3 1.00| ---| FLD078-4 1.00| ---| FLD079-1 1.00| ---| FLD079-2 1.00| ---| FLD079-3 1.00| ---| FLD079-4 1.00| ---| FLD080-1 1.00| ---| FLD080-2 1.00| ---| FLD080-3 1.00| ---| FLD080-4 1.00| ---| FLD081-1 1.00| ---| FLD081-2 1.00| ---| FLD081-3 1.00| ---| FLD081-4 1.00| ---| FLD082-1 1.00| ---| FLD082-3 1.00| ---| FLD083-1 1.00| ---| FLD083-3 1.00| ---| FLD084-1 1.00| ---| FLD084-3 1.00| ---| FLD085-1 1.00| ---| FLD085-3 1.00| ---| FLD086-1 1.00| ---| FLD086-3 1.00| ---| FLD087-1 1.00| ---| FLD087-3 1.00| ---| FLD088-1 1.00| ---| FLD088-3 1.00| ---| FLD089-1 1.00| ---| FLD089-3 1.00| ---| FLD090-3 1.00| ---| FLD091-1 1.00| ---| FLD091-3 1.00| ---| FLD092-1 1.00| ---| FLD092-3 1.00| ---| FLD093-1 1.00| ---| FLD093-3 1.00| ---| FLD094-1 1.00| ---| FLD094-3 1.00| ---| FLD095-1 1.00| ---| FLD095-2 1.00| ---| FLD095-3 1.00| ---| FLD095-4 1.00| ---| FLD096-1 1.00| ---| FLD096-2 1.00| ---| FLD096-3 1.00| ---| FLD096-4 1.00| ---| FLD097-1 1.00| ---| FLD097-2 1.00| ---| FLD097-3 1.00| ---| FLD098-1 1.00| ---| FLD098-2 1.00| ---| FLD098-3 1.00| ---| FLD098-4 1.00| ---| FLD099-1 1.00| ---| FLD099-2 1.00| ---| FLD099-3 1.00| ---| FLD099-4 1.00| ---| FLD100-1 1.00| ---| FLD100-2 1.00| ---| FLD100-3 1.00| ---| FLD100-4 1.00| ---| ---------------------------------------------------------------------------- Problem set tptp_nne(unknown, not range restricted), 7 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, unknown and not range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 0 solved Prob. Rating \ Prover| 1| ---------------------|------| ANA001-1 1.00| ---| ANA004-5 1.00| ---| ANA005-4 1.00| ---| ANA005-5 1.00| ---| FLD090-1 1.00| ---| SYN814-1 1.00| -m-| SYN822-1 1.00| -m-| ---------------------------------------------------------------------------- Problem set tptp_nne(open, range restricted), 0 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, open and range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 0 solved Prob. Rating \ Prover| 1| ---------------------|------| ---------------------------------------------------------------------------- Problem set tptp_nne(open, not range restricted), 0 problems All problems in TPTP 2.5.0 which are non-Horn, without equality, open and not range restricted. ---------------------------------------------------------------------------- 1 Krh 7.4.03, 300s. 0 solved Prob. Rating \ Prover| 1| ---------------------|------|