Prolog Terminal session with alcas.pl
Captured on Nov 6, 2005

?- run('oct28.cas').
File Read
Tokenized
Parsed Ontology
Parsed Queries
File parsed: 10 msec
Topological sorted concept uri(c:Person)
Topological sorted concept uri(c:Female)
Topological sorted concept uri(c:Woman)
Topological sorted concept uri(c:Man)
Topological sorted concept uri(c:Wife)
Topological sorted concept uri(c:Mother)
Topological sorted concept uri(c:MotherWithoutDaughter)
Topological sorted concept uri(c:Father)
Topological sorted concept uri(c:Parent)
Topological sorted concept uri(c:GrandMother)
Unfolded: 0 msec
Query 1) classSubsumes(uri(c:Woman), uri(c:Mother))
Query 1 after expanding classSubsumes(intersect(uri(c:Person), uri(c:Female)), intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))))
Query (#1)
   Testing sat of [$28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Selecting $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))
Leaving tableau [$28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))] and []
Apply conjunction rule. 
Adding $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))) and $28:union(not(uri(c:Person)), not(uri(c:Female)))
Selecting $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person)))
Leaving tableau [$28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Apply conjunction rule. 
Adding $28:intersect(uri(c:Person), uri(c:Female)) and $28:some(uri(c:hasChild), uri(c:Person))
Selecting $28:intersect(uri(c:Person), uri(c:Female))
Leaving tableau [$28:intersect(uri(c:Person), uri(c:Female)), $28:some(uri(c:hasChild), uri(c:Person)), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Apply conjunction rule. 
Adding $28:uri(c:Person) and $28:uri(c:Female)
Selecting $28:uri(c:Person)
Leaving tableau [$28:uri(c:Person), $28:uri(c:Female), $28:some(uri(c:hasChild), uri(c:Person)), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Moved a-box assertion to LD
Selecting $28:uri(c:Female)
Leaving tableau [$28:uri(c:Female), $28:some(uri(c:hasChild), uri(c:Person)), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:uri(c:Person), $28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Moved a-box assertion to LD
Selecting $28:some(uri(c:hasChild), uri(c:Person))
Leaving tableau [$28:some(uri(c:hasChild), uri(c:Person)), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:uri(c:Female), $28:uri(c:Person), $28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Applying role-exists rule. 
Fresh individual $29 for witness $29:uri(c:Person) and [$28, $29]:uri(c:hasChild)
Selecting [$28, $29]:uri(c:hasChild)
Leaving tableau [[$28, $29]:uri(c:hasChild), $29:uri(c:Person), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$28:uri(c:Female), $28:uri(c:Person), $28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Moved a-box assertion to LD
Selecting $29:uri(c:Person)
Leaving tableau [$29:uri(c:Person), $28:union(not(uri(c:Person)), not(uri(c:Female)))] and [[$28, $29]:uri(c:hasChild), $28:uri(c:Female), $28:uri(c:Person), $28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Moved a-box assertion to LD
Selecting $28:union(not(uri(c:Person)), not(uri(c:Female)))
Leaving tableau [$28:union(not(uri(c:Person)), not(uri(c:Female)))] and [$29:uri(c:Person), [$28, $29]:uri(c:hasChild), $28:uri(c:Female), $28:uri(c:Person), $28:intersect(uri(c:Person), uri(c:Female)), $28:intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), $28:intersect(intersect(intersect(uri(c:Person), uri(c:Female)), some(uri(c:hasChild), uri(c:Person))), union(not(uri(c:Person)), not(uri(c:Female))))]
Apply disjunction rule.
Splitting. 
Clash found $28:uri(c:Person)
Clash found $28:uri(c:Female)
   yes 10 msec

Yes