Copyright (c) 2005 IBM Corporation and others.
All rights reserved. This program and the accompanying materials
are made available under the terms of the Common Public License v1.0
which accompanies this distribution, and is available at
http://www.eclipse.org/legal/cpl-v10.html

Contributors:
IBM - Initial implementation

Discrete Event Calculus Reasoner 1.0
loading deckt/PassThroughDoor.e
loading foundations/Root.e
loading foundations/EC.e
114 variables and 352 clauses
relsat solver
2 models
---
model 1:
0
KP_NotInRoom(R1).
KP_NotOpened(D1).
Knows_NotInRoom(R1).
Knows_NotOpened(D1).
Kw_InRoom(R1).
Kw_Opened(D1).
Happens(Speak(), 0).
1
-KP_NotOpened(D1).
-Knows_NotOpened(D1).
-Kw_Opened(D1).
Happens(Sense_Opened(D1), 1).
Happens(Sense_OpenedF(D1), 1).
Happens(X(D1), 1).
2
+KP_NotOpened(D1).
+Knows_NotOpened(D1).
+Kw_Opened(D1).
Happens(PassThrough(D1, R1), 2).
3
P
ReleasedAt(Knows_InRoom(R1), 0).
ReleasedAt(Knows_InRoom(R1), 1).
ReleasedAt(Knows_InRoom(R1), 2).
ReleasedAt(Knows_InRoom(R1), 3).
ReleasedAt(Knows_NotInRoom(R1), 0).
ReleasedAt(Knows_NotInRoom(R1), 1).
ReleasedAt(Knows_NotInRoom(R1), 2).
ReleasedAt(Knows_NotInRoom(R1), 3).
ReleasedAt(Knows_NotOpened(D1), 0).
ReleasedAt(Knows_NotOpened(D1), 1).
ReleasedAt(Knows_NotOpened(D1), 2).
ReleasedAt(Knows_NotOpened(D1), 3).
ReleasedAt(Knows_Opened(D1), 0).
ReleasedAt(Knows_Opened(D1), 1).
ReleasedAt(Knows_Opened(D1), 2).
ReleasedAt(Knows_Opened(D1), 3).
ReleasedAt(Kw_InRoom(R1), 0).
ReleasedAt(Kw_InRoom(R1), 1).
ReleasedAt(Kw_InRoom(R1), 2).
ReleasedAt(Kw_InRoom(R1), 3).
ReleasedAt(Kw_Opened(D1), 0).
ReleasedAt(Kw_Opened(D1), 1).
ReleasedAt(Kw_Opened(D1), 2).
ReleasedAt(Kw_Opened(D1), 3).
ReleasedAt(Opened(D1), 1).
!Happens(PassThrough(D1, R1), 0).
!Happens(PassThrough(D1, R1), 1).
!Happens(Sense_Opened(D1), 0).
!Happens(Sense_Opened(D1), 2).
!Happens(Sense_OpenedF(D1), 0).
!Happens(Sense_OpenedF(D1), 2).
!Happens(Sense_OpenedT(D1), 0).
!Happens(Sense_OpenedT(D1), 1).
!Happens(Sense_OpenedT(D1), 2).
!Happens(Speak(), 1).
!Happens(Speak(), 2).
!Happens(X(D1), 0).
!Happens(X(D1), 2).
!ReleasedAt(InRoom(R1), 0).
!ReleasedAt(InRoom(R1), 1).
!ReleasedAt(InRoom(R1), 2).
!ReleasedAt(InRoom(R1), 3).
!ReleasedAt(KP_InRoom(R1), 0).
!ReleasedAt(KP_InRoom(R1), 1).
!ReleasedAt(KP_InRoom(R1), 2).
!ReleasedAt(KP_InRoom(R1), 3).
!ReleasedAt(KP_NotInRoom(R1), 0).
!ReleasedAt(KP_NotInRoom(R1), 1).
!ReleasedAt(KP_NotInRoom(R1), 2).
!ReleasedAt(KP_NotInRoom(R1), 3).
!ReleasedAt(KP_NotOpened(D1), 0).
!ReleasedAt(KP_NotOpened(D1), 1).
!ReleasedAt(KP_NotOpened(D1), 2).
!ReleasedAt(KP_NotOpened(D1), 3).
!ReleasedAt(KP_Opened(D1), 0).
!ReleasedAt(KP_Opened(D1), 1).
!ReleasedAt(KP_Opened(D1), 2).
!ReleasedAt(KP_Opened(D1), 3).
!ReleasedAt(Opened(D1), 0).
!ReleasedAt(Opened(D1), 2).
!ReleasedAt(Opened(D1), 3).
---
model 2:
0
KP_NotInRoom(R1).
KP_NotOpened(D1).
Knows_NotInRoom(R1).
Knows_NotOpened(D1).
Kw_InRoom(R1).
Kw_Opened(D1).
Happens(Speak(), 0).
1
-KP_NotOpened(D1).
-Knows_NotOpened(D1).
-Kw_Opened(D1).
+Opened(D1).
Happens(Sense_Opened(D1), 1).
Happens(Sense_OpenedT(D1), 1).
Happens(X(D1), 1).
2
+KP_Opened(D1).
+Knows_Opened(D1).
+Kw_Opened(D1).
Happens(PassThrough(D1, R1), 2).
3
-KP_NotInRoom(R1).
-Knows_NotInRoom(R1).
+InRoom(R1).
+KP_InRoom(R1).
+Knows_InRoom(R1).
P
ReleasedAt(Knows_InRoom(R1), 0).
ReleasedAt(Knows_InRoom(R1), 1).
ReleasedAt(Knows_InRoom(R1), 2).
ReleasedAt(Knows_InRoom(R1), 3).
ReleasedAt(Knows_NotInRoom(R1), 0).
ReleasedAt(Knows_NotInRoom(R1), 1).
ReleasedAt(Knows_NotInRoom(R1), 2).
ReleasedAt(Knows_NotInRoom(R1), 3).
ReleasedAt(Knows_NotOpened(D1), 0).
ReleasedAt(Knows_NotOpened(D1), 1).
ReleasedAt(Knows_NotOpened(D1), 2).
ReleasedAt(Knows_NotOpened(D1), 3).
ReleasedAt(Knows_Opened(D1), 0).
ReleasedAt(Knows_Opened(D1), 1).
ReleasedAt(Knows_Opened(D1), 2).
ReleasedAt(Knows_Opened(D1), 3).
ReleasedAt(Kw_InRoom(R1), 0).
ReleasedAt(Kw_InRoom(R1), 1).
ReleasedAt(Kw_InRoom(R1), 2).
ReleasedAt(Kw_InRoom(R1), 3).
ReleasedAt(Kw_Opened(D1), 0).
ReleasedAt(Kw_Opened(D1), 1).
ReleasedAt(Kw_Opened(D1), 2).
ReleasedAt(Kw_Opened(D1), 3).
ReleasedAt(Opened(D1), 1).
!Happens(PassThrough(D1, R1), 0).
!Happens(PassThrough(D1, R1), 1).
!Happens(Sense_Opened(D1), 0).
!Happens(Sense_Opened(D1), 2).
!Happens(Sense_OpenedF(D1), 0).
!Happens(Sense_OpenedF(D1), 1).
!Happens(Sense_OpenedF(D1), 2).
!Happens(Sense_OpenedT(D1), 0).
!Happens(Sense_OpenedT(D1), 2).
!Happens(Speak(), 1).
!Happens(Speak(), 2).
!Happens(X(D1), 0).
!Happens(X(D1), 2).
!ReleasedAt(InRoom(R1), 0).
!ReleasedAt(InRoom(R1), 1).
!ReleasedAt(InRoom(R1), 2).
!ReleasedAt(InRoom(R1), 3).
!ReleasedAt(KP_InRoom(R1), 0).
!ReleasedAt(KP_InRoom(R1), 1).
!ReleasedAt(KP_InRoom(R1), 2).
!ReleasedAt(KP_InRoom(R1), 3).
!ReleasedAt(KP_NotInRoom(R1), 0).
!ReleasedAt(KP_NotInRoom(R1), 1).
!ReleasedAt(KP_NotInRoom(R1), 2).
!ReleasedAt(KP_NotInRoom(R1), 3).
!ReleasedAt(KP_NotOpened(D1), 0).
!ReleasedAt(KP_NotOpened(D1), 1).
!ReleasedAt(KP_NotOpened(D1), 2).
!ReleasedAt(KP_NotOpened(D1), 3).
!ReleasedAt(KP_Opened(D1), 0).
!ReleasedAt(KP_Opened(D1), 1).
!ReleasedAt(KP_Opened(D1), 2).
!ReleasedAt(KP_Opened(D1), 3).
!ReleasedAt(Opened(D1), 0).
!ReleasedAt(Opened(D1), 2).
!ReleasedAt(Opened(D1), 3).
EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
PassThroughDoor: 0 predicates, 0 functions, 12 fluents, 6 events, 34 axioms
Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
encoding 0.1s
solution 0.0s
total 0.4s