Missing "not a large tetrahedron"

See ~/lingo/openproof/Server  for server.py

; In ~/newopen, get fresh copy of SVN repository for Openproof
svn co svn+ssh://svnusers@scm.gradegrinder.net/openproof/LingoService/trunk LingoService

; AWS instance:
ssh -i ~/.ssh/Danskey.pem ubuntu@18.237.245.193

------------------------------------------------------------------------------
No result

|B| and |c| are both the same size if and only if either it is the case both that |b| is a tetrahedron and that |c| is a dodecahedron or it is the case both that |b| is a dodecahedron and that |c| is a tetrahedron. paired-both-rev-gpr conj-s-rev-gpr thecase-cleft-gpr thecase-cleft-gpr paired-both-nrev-gpr paired-either-nrev-gpr both-adv-op-gpr same-to-and-size-op-gpr

Unwanted:
Both |d| and |e| are between |c| and |a| both. paired-both-x-rev-gpr conj-s-rev-gpr both-adv-op-gpr coord-subj-three-op-gpr
|C| and |c| are not in front of |b| and |d| and |d| are not in front of |c|. conj-s-rev-gpr conj-s-rev-gpr coord-subj-two-neg-op-gpr coord-subj-two-neg-op-gpr
|A| is a cube and |b| is a dodecahedron only if it is also to the left of |b|. also-adv-pro-op-gpr onlyif-pro-subj-gpr ifthen-to-onlyif-gpr
|B| is a dodecahedron only if if |b| is not in front of |d| then |b| is not in back of |d| either. either-adv-op-gpr ifthen-to-onlyif-gpr
At least one, of |a|, |c|, and |e| is a cube. at-least-one-gpr one-of-set-two-gpr coord-subj-two-noprop-nary-op-gpr coord-subj-two-noprop-op-gpr

Either |a| is to the left of |d| or it (i.e., |d|) is to the left of |a| if |d| is a cube but it is. conj-s-rev-gpr cond-pro-subj-rev-gpr drop-then-opt-gpr and-but-loc-op-gpr vp-ellip-coord-pos-two-gpr cond-pro-subj-ambig-gpr

missing:
|D| is between |c| and |a|, and |e| is. conj-s-rev-gpr vp-ellip-coord-pos-twoconj-gpr
|F| either is in back of or is smaller than |a|. paired-either-nrev-gpr common-dobj-onetwopred-op-gpr coord-vp-one-op-gpr
|E| is neither larger than |d| nor smaller than |d|. not-or-to-nor-op-gpr coord-vp-one-op-gpr
|E| is not either larger than or smaller than |d|. paired-either-nrev-gpr common-dobj-twopred-op-gpr coord-vp-one-op-gpr
|C| is larger than |e|; however |c| is smaller than |a|. conj-s-rev-gpr semicol-but-op-gpr and-but-large-small-op-gpr
|C| both is in front of and is smaller than |f|. paired-both-nrev-gpr common-dobj-onetwopred-op-gpr coord-vp-one-op-gpr
|E| is not in the same column as |c| or as |d|. common-vp-same-n-op-gpr coord-vp-two-op-gpr
Both |c| and |d| are cubes and both |c| and |d| are not small. paired-both-x-rev-gpr paired-both-x-rev-gpr conj-s-rev-neg-gpr conj-s-rev-gpr coord-subj-one-neg-op-gpr coord-subj-two-noprop-op-gpr
|C| is not between |a| and |b| and |c| both is not in front of |b| and is not in front of |a|. paired-both-rev-gpr conj-s-rev-neg-gpr coord-vp-two-op-gpr
|B| is neither to the left nor to the right of |d| only if either |b| is a tetrahedron or |d| is a tetrahedron. conj-s-rev-gpr ifthen-to-onlyif-gpr not-or-to-nor-op-gpr common-ppof-right-op-gpr coord-vp-two-op-gpr
|C| is to the right of |d| only if it is the case both that |b| is to the left of |e| and that |b| is to the right of |c|. paired-both-rev-gpr conj-s-rev-gpr ifthen-to-onlyif-gpr
|E| is in front of |d| if |e| is not a large tetrahedron. conj-s-rev-gpr drop-then-opt-gpr predn-adj-gpr
|B| is larger than |a|; moreover |b| is larger than |e|. semicol-and-op-gpr
|C| is not a tetrahedron only if |b| is a cube. ifthen-to-onlyif-gpr
|E| is not a cube only if either |b| is large or |d| is large. ifthen-to-onlyif-gpr
|C| is a tetrahedron or |a| is a tetrahedron only if either |b| is a cube or |d| is a cube. conj-s-rev-gpr ifthen-to-onlyif-gpr
If |a| is a tetrahedron |b| is. drop-then-opt-gpr vp-ellip-if-pos-two-gpr
|C| is small and |d| is a dodecahedron only if |d| is neither large nor small. ifthen-to-onlyif-gpr not-or-to-nor-op-gpr coord-vp-one-op-gpr

Dave:
For -(large(e)&tet(e)), do we want |E is not a large tetrahedron| ?
  cf. 7-12: -(large(e)&tet(e))-->frontof(e,d)
  
------------------------------------------------------------------------------
Slack
https://uit.stanford.edu/service/slack

------------------------------------------------------------------------------
:: Good not getting these in 7-12
Either |a| is a cube or |c| is a cube or |e| is a cube. paired-either-gpr
|A| or |c| is a cube or |e| is a cube. coord-subj-two-noprop-op-gpr
|E| is a cube or it is the case either that |a| is a cube or that |c| is a cube. thecase cleft gpr paired-either-gpr
Either |a| or |c| is a cube or |e| is a cube. paired-either-gpr coord-subj-two-noprop-op-gpr

;; Alas, not getting this in 7-12
|A| is a cube or either |c| is a cube or |e| is a cube. paired-either-gpr

;; Not getting this in fols (because of blocking coord-S source)
|E| is not to both the right of |c| and the left of |b| and |a| is not both to the right of |c| and to the left of |b|. paired-both-x-gpr paired-both-gpr common-pred-op-gpr coord-vp-two-op-gpr coord-vp-two-op-gpr
|E| is not to both the right of |c| and the left of |b| and |a| isn't to the right of |c| and to the left of |b|. paired-both-x-gpr common-pred-op-gpr coord-vp-two-op-gpr coord-vp-two-op-gpr
|C| is not between |a| and |b| and |c| both is not in front of |a| and is not in front of |b|. paired-both-gpr coord-vp-two-op-gpr
|D| is not in front of |c| and it is the case that |d| is not in front of |b| and that |c| both is not in front of |c| and is not in front of |b|. thecase cright gpr paired-both-gpr coord-vp-two-op-gpr

-----
;; Examples of less ambiguity
: Keep:
|A| and |E| are both larger than |C| and it is not the case that both |A| and |E| are large.
; Now block:
|A| and |E| are both larger than |C| and it is not the case that |A| is large and |E| is not large.

; Keep:
|C| is medium only if |D| is not a cube and it is not the case that both |E| and |F| are cubes.
; Now block:
|C| is medium only if |D| is not a cube and |E| is not a cube and |F| is not a cube.
-----

;; Blocking these because the coord-S source would be ambig
;;
|A| is small or |c| and |d| are large. both-adv-op-gpr coord-subj-one-pos-op-gpr
;; or this
|A| and |e| are both tetrahedra or |a| and |f| are both tetrahedra. both-adv-op-gpr both-adv-op-gpr coord-subj-two-noprop-op-gpr coord-subj-two-noprop-op-gpr
;; or this
|C| is between |d| and |f| or |c| is smaller than |d| and is smaller than |f|. coord-vp-one-op-gpr

;; Improvement: now correctly getting the first but not the second for
;; cube(d)&cube(c)&-small(d)&-small(c)
Both |d| and |c| are cubes and it is the case that |d| is not small and that |c| is not small. thecase cright gpr paired-both-x-gpr coord-subj-two-noprop-op-gpr
Both |d| and |c| are cubes and it's not the case that both |d| and |c| are small. paired-both-x-gpr paired-both-x-gpr coord-subj-one-neg-op-gpr coord-subj-two-noprop-op-gpr

---
To avoid generating |B and C or D|, |B or C and D|:
  also avoid |it is (not) the case both that B and that C and/or D|
  also avoid |it is (not) the case either that B or that C and/or D|

In s-coord-top rule
  left conj is nonconj, and also not |it is (not) the case that...|
Want right conj to be either nonconj or marked as overt pair of either-or
  So s-coord-mid is only overt either-or.
Add paraphr rule to convert |B and C| to |it is the case both that B and that C|
(following suggested phrasing by Aaron), so we can still get output for |A&B&C|

See also for similar if-then constraints:
  ~/Desktop/hyper/unambigous-rendering.pdf
  ~/Desktop/hyper/Categ*.pdf
---------
To do (2015-03-13)
+(1) Vertical bars in ORTH for letter names
+(2) Reduce or eliminate ambiguous outputs
(3) Larger set of `rule' names including syntactic variants (a+b => b+a)
(4) Pairing of rule+anchor to show where a (para) rule has applied in a sentence
    - assume single pivot per rule (at most)
(5) Reflexive pronouns (e.g. samesize; B is not between C and itself)

------------------------------------------------------------------------------
FOL => English paraphrases

To test web server on cypriot, check to see that the server is running
(~/start-op-server) and then open this form in a browser:
/home/danf/openproof/form.html
Enter an FOL expression such as tet(c)&tet(d) in the first box, and the name 
of a rules file in the second, where the filename is "rules.all" or 
"rules.pro": one of the preset rules files in ~/erg/openproof/rules.*".

The python server code is in ~/openproof, with the main file as Server/server.py

;; Test run: Compile a version of the paraphrase grammar, then call Aaron 
;; Kalb's FOL converter to MRS syntax, then inflate, add paraphrased MRSs, 
;; generate, sort uniquely, and package output as XML

;; Note: no longer need ACE version 0919 (latest ace works fine)
;; was basque:/home/danf/logon/lingo/answer/bin/linux.x86.64/ace.0919
;; and cypriot:/home/danf/bin/ace.0919

;; 1. Compile the MRS-inflation, paraphrase, and generator grammars
;;
cd ~/erg
ace -G openproof/inflatemrs.dat -g openproof/config-inflate.tdl
ace -G openproof/paraphrase-op.dat -g openproof/config.tdl
ace -G openproof/ergopen.dat -g ace/config-open.tdl

;; 2. To run single examples interactively, call `runfol' with at least the
;; first two arguments


;; 2a. Run one particular example interactively, using just aggregation rules:
;;
cd ~/erg/openproof; ./runfol -f "small(c)&small(b)" -r rules.agg > /tmp/out2.txt; more /tmp/out2.txt

;; 2b. Run example, and apply all rules in "rules.*" except those in "no.*"
;; (here, exclude "only if" and "provided (that)" in conditionals):
;; 
cd ~/erg/openproof; ./runfol -f "small(a)-->large(b)" -r rules.all -x no.onlyif+prov > /tmp/out.txt

;; 2c. Run example, and apply all rules in "rules.*" except those in "no.*", 
;; and add those in "req.*" (here, obligatorily omit "then" in conditionals):
cd ~/erg/openproof; ./runfol -f "small(a)-->large(b)" -r rules.all -x no.optthen -a req.dropthen > /tmp/out.txt; more /tmp/out.txt


;; 3. Batch run 7-12 set of fols
;;
cd ~/erg/openproof; for i in $(cat 7-12.txt); do \python scripts/e2e.py $i | ace -g inflatemrs.dat -f | ace -g paraphrase-op.dat -f --transfer-config rules.all | ace -g ergopen.dat -e | sort -u; echo "---ITEM---"; done > /tmp/out7-12.txt
Time: 1:40 on 2014.07.26
      1:27 on 2014.09.09
      1:34 on 2015.03.19
      2:04 on 2015.05.14
      4:00 on 2015.07.25

;; 7-12 set with just coordination (aggregation) rules
;;
cd ~/erg/openproof; for i in $(cat 7-12.txt); do \python scripts/e2e.py $i | ace -g inflatemrs.dat -f | ace -g paraphrase-op.dat -f --transfer-config rules.agg | ace -g ergopen.dat -e | sort -u; echo "---ITEM---"; done > /tmp/out7-12c.txt

;; 7-12 set with just pronoun rules
;;
cd ~/erg/openproof; for i in $(cat 7-12.txt); do \python scripts/e2e.py $i | ace -g inflatemrs.dat -f | ace -g paraphrase-op.dat -f --transfer-config rules.pro | ace -g ergopen.dat -e | sort -u; echo "---ITEM---"; done > /tmp/out7-12p.txt

;; Batch run the full set of FOLS used currently in LPP book:
;;
cd ~/erg/openproof; for i in $(cat fols.txt); do \python scripts/e2e.py $i | ace -g inflatemrs.dat -f | ace -g paraphrase-op.dat -f --transfer-config rules.all --timeout 10 | ace -g ergopen.dat -e | sort -u; echo "---ITEM---"; done > /tmp/outfols.txt
Time: 19:45 vs. 19:00 (old)
      19:00 15-02-08
      19:30 15-03-19
      19:30 15-05-14


;; To evaluate using Aaron's script, do the following
;;
cd ~/erg/openproof
python scripts/corpus_test.py 7-12.txt scripts/712goals.txt out7-12.txt
python scripts/corpus_test.py fols.txt scripts/goals.txt out.txt