diff -r a315a3862bb4 -r b2a1d9c20df7 lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Fri Apr 27 17:16:21 2001 +0200
+++ b/lib/scripts/convert.pl	Mon Apr 30 11:57:10 2001 +0200
@@ -20,6 +20,7 @@
 sub subst_RS {
   s/ RS ([\w\'\.]+)/ [THEN $1]/g;
   s/ RS \((.+?)\)/ [THEN $1]/g;
+  s/\(([\w\'\.]+ \[THEN [\w\'\.]+\])\)/$1/g;
   s/\] \[THEN /, /g;
   s/THEN sym\b/symmetric/g;
 }
@@ -59,6 +60,10 @@
   s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
   s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
 
+  if(s/^\(EVERY\'\[(.*?)\]\s*(\d+)\)$/\($1 $2\)/) {
+    $goal = $2;
+    s/,/ $goal,/g;
+  }
   s/Blast_tac 1/blast/g;
   s/^Blast_tac (\d+)/{$prefer="prefer $1 "; "blast"}/e;
   s/Fast_tac 1/fast/g;