Small debugging in tptp2grafite

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index ca0534c52b7f3ae410376808cdf63ac9ca4a8dec..009a53a610686a0d352e5dce681f066372abdb79 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -221,7 +221,8 @@ let ng_generate_tactics fv ueq_case context arities =
   (HExtlib.list_mapi
    (fun (name,_) _-> 
      GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,name);GA.NDot(floc)])))
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
    arities)
   @
   (HExtlib.list_mapi
@@ -272,6 +273,8 @@ let ng_generate_tactics fv ueq_case context arities =
                GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+                                        GA.NSemicolon(floc)]))]@
   [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 ;;
 

diff --git a/helm/software/components/tptp_grafite/unit_equality_problems b/helm/software/components/tptp_grafite/unit_equality_problems
index c394ddd956fbebb3fabab2bf63eb32b5bf70f66a..60cb9fbbd20d2bc82bfdb4acc8e9d0a4f9b107eb 100644 (file)
--- a/helm/software/components/tptp_grafite/unit_equality_problems
+++ b/helm/software/components/tptp_grafite/unit_equality_problems
@@ -1,6 +1,18 @@
 ALG005-1
 ALG006-1
 ALG007-1
+ALG235-1
+ALG236-1
+ALG237-1
+ALG238-1
+ALG239-1
+ALG240-1
+ALG241-1
+ALG242-1
+ALG243-1
+ALG244-1
+ALG245-1
+ALG246-1
 BOO001-1
 BOO002-1
 BOO002-2
@@ -99,15 +111,15 @@ COL002-1
 COL002-4
 COL002-5
 COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-1
-COL003-2
+COL003-12
+COL003-13
+COL003-14
+COL003-15
+COL003-16
+COL003-17
+COL003-18
+COL003-19
+COL003-20
 COL004-1
 COL004-3
 COL005-1
@@ -199,8 +211,8 @@ COL064-6
 COL064-7
 COL064-8
 COL064-9
-COL064-1
-COL064-1
+COL064-10
+COL064-11
 COL065-1
 COL066-1
 COL066-2
@@ -217,6 +229,7 @@ COL084-1
 COL085-1
 COL086-1
 COL087-1
+COM010-2
 GRP001-2
 GRP001-4
 GRP002-2
@@ -571,6 +584,86 @@ GRP613-1
 GRP614-1
 GRP615-1
 GRP616-1
+GRP661-1
+GRP662-1
+GRP663-1
+GRP666-2
+GRP666-3
+GRP666-4
+GRP666-5
+GRP667-2
+GRP667-3
+GRP667-4
+GRP667-5
+GRP668-1
+GRP669-1
+GRP670-1
+GRP671-1
+GRP675-1
+GRP676-1
+GRP677-1
+GRP678-1
+GRP679-1
+GRP680-1
+GRP681-1
+GRP684-1
+GRP686-1
+GRP687-1
+GRP688-1
+GRP689-1
+GRP690-1
+GRP691-1
+GRP692-1
+GRP693-1
+GRP694-1
+GRP695-1
+GRP696-1
+GRP697-1
+GRP698-1
+GRP699-1
+GRP701-1
+GRP705-1
+GRP706-1
+GRP707-1
+GRP708-1
+GRP709-1
+GRP712-1
+GRP713-1
+GRP714-1
+GRP716-1
+GRP717-1
+GRP718-1
+GRP719-1
+GRP720-2
+GRP721-1
+GRP722-1
+GRP723-1
+GRP724-1
+GRP725-1
+GRP726-1
+GRP727-1
+GRP728-1
+GRP729-1
+GRP730-1
+GRP731-1
+GRP732-1
+GRP735-1
+GRP736-1
+GRP737-1
+GRP738-1
+GRP739-1
+GRP740-1
+GRP741-1
+GRP742-1
+GRP743-1
+GRP744-1
+GRP749-1
+GRP750-1
+GRP751-1
+GRP752-1
+GRP753-1
+GRP754-1
+GRP756-1
 HWC004-1
 HWC004-2
 LAT006-1
@@ -730,6 +823,10 @@ LAT174-1
 LAT175-1
 LAT176-1
 LAT177-1
+LAT389-1
+LAT390-1
+LAT391-1
+LAT392-1
 LCL109-2
 LCL109-6
 LCL110-2
@@ -769,6 +866,85 @@ LCL410-1
 LDA001-1
 LDA002-1
 LDA007-3
+REL001-1
+REL002-1
+REL004-1
+REL004-2
+REL004-3
+REL005-1
+REL005-3
+REL006-1
+REL007-1
+REL008-1
+REL008-3
+REL010-1
+REL010-2
+REL011-1
+REL011-2
+REL012-1
+REL012-2
+REL014-1
+REL015-1
+REL016-1
+REL016-3
+REL017-1
+REL017-3
+REL018-1
+REL019-1
+REL019-2
+REL020-1
+REL020-2
+REL021-1
+REL021-2
+REL022-1
+REL022-2
+REL023-1
+REL023-2
+REL024-1
+REL024-2
+REL025-1
+REL026-1
+REL026-3
+REL027-1
+REL027-3
+REL028-1
+REL028-2
+REL029-1
+REL029-3
+REL030-1
+REL030-3
+REL031-1
+REL031-2
+REL032-1
+REL032-2
+REL033-1
+REL033-3
+REL034-1
+REL034-2
+REL035-1
+REL035-2
+REL036-1
+REL036-2
+REL037-1
+REL037-2
+REL038-1
+REL039-1
+REL040-1
+REL040-3
+REL041-1
+REL041-2
+REL042-1
+REL042-2
+REL043-1
+REL043-2
+REL044-1
+REL044-2
+REL045-1
+REL045-2
+REL047-1
+REL049-1
+REL050-1
+REL050-3
 RNG007-4
 RNG008-3
 RNG008-4
@@ -854,7 +1030,9 @@ ROB028-1
 ROB030-1
 ROB031-1
 ROB032-1
+SWV243-2
+SWV262-2
 SYN080-1
 SYN083-1
 SYN305-1
-SYN552-1
+SYN552-1
\ No newline at end of file