syosi@mr-burns:~/cvs-trunk/WWW/2000/10/swap/test/reason$ python ../../check.py --report /tmp/2.pf 1: @forAll :REGION, :WHERE, :WHO. @forSome foo:_g2 . gmp:dan a gmp:Man; gmp:home foo:_g2 . { gmp:dan gmp:home :WHERE . } log:implies {:WHERE gmp:in gmp:Texas . } . { :WHERE gmp:in :REGION . :WHO gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } . [by parsing ] 2: @forSome foo:_g2 . :dan :home foo:_g2 . [by erasure from step 1] 3: @forSome foo:_g2 . :dan :home foo:_g2 . [by erasure from step 1] 4: @forAll dou:WHERE . { :dan :home dou:WHERE . } log:implies {dou:WHERE :in :Texas . } . [by erasure from step 1] 5: ... [by rule from step 4 applied to steps [3] with bindings {'WHERE': '[...]'}] 6: @forSome foo:_g2 . foo:_g2 :in :Texas . [by erasure from step 5] 7: @forAll :REGION, :WHERE, :WHO . { :WHERE gmp:in :REGION . :WHO gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } . [by erasure from step 1] 8: :dan :homeRegion :Texas . [by rule from step 7 applied to steps [2, 6] with bindings {'REGION': '', 'WHO': '', 'WHERE': '[...]'}] 9: @forAll dou:REGION, dou:WHERE, dou:WHO. @forSome foo:_g2 . :dan a :Man; :home foo:_g2; :homeRegion :Texas . foo:_g2 :in :Texas . { :dan :home dou:WHERE . } log:implies {dou:WHERE :in :Texas . } . { dou:WHERE :in dou:REGION . dou:WHO :home dou:WHERE . } log:implies {dou:WHO :homeRegion dou:REGION . } . [by conjoining steps [8, 1, 5]] @prefix : . @prefix gmp: . @prefix log: . @forAll :REGION, :WHERE, :WHO. @forSome :_g_L3C17 . :_g_L3C17 gmp:in gmp:Texas . gmp:dan a gmp:Man; gmp:home :_g_L3C17; gmp:homeRegion gmp:Texas . { gmp:dan gmp:home :WHERE . } log:implies {:WHERE gmp:in gmp:Texas . } . { :WHERE gmp:in :REGION . :WHO gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } .