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/CarryingPDA.e
loading foundations/Root.e
loading foundations/EC.e
234 variables and 773 clauses
relsat solver
1 model
---
model 1:
0
InRoom(PDA, ISLLab).
InRoom(Teo, ISLLab).
KP_InRoom(PDA, ISLLab).
KP_InRoom(Teo, ISLLab).
KP_NotHolding(Teo, PDA).
KP_NotHolding(Teo, Teo).
KP_NotInRoom(PDA, CARVLab).
KP_NotInRoom(Teo, CARVLab).
Knows_InRoom(PDA, ISLLab).
Knows_InRoom(Teo, ISLLab).
Knows_NotHolding(Teo, PDA).
Knows_NotHolding(Teo, Teo).
Knows_NotInRoom(PDA, CARVLab).
Knows_NotInRoom(Teo, CARVLab).
Kw_Holding(Teo, PDA).
Kw_Holding(Teo, Teo).
Kw_InRoom(PDA, CARVLab).
Kw_InRoom(PDA, ISLLab).
Kw_InRoom(Teo, CARVLab).
Kw_InRoom(Teo, ISLLab).
Happens(PickUp(Teo, PDA), 0).
1
-KP_InRoom(PDA, ISLLab).
-KP_NotHolding(Teo, PDA).
-KP_NotInRoom(PDA, CARVLab).
-Knows_NotHolding(Teo, PDA).
+Holding(Teo, PDA).
+KP_Holding(Teo, PDA).
+Knows_Holding(Teo, PDA).
Happens(Walk(Teo, ISLLab, CARVLab), 1).
2
-InRoom(PDA, ISLLab).
-InRoom(Teo, ISLLab).
-KP_InRoom(Teo, ISLLab).
-KP_NotInRoom(Teo, CARVLab).
-Knows_InRoom(PDA, ISLLab).
-Knows_InRoom(Teo, ISLLab).
-Knows_NotInRoom(PDA, CARVLab).
-Knows_NotInRoom(Teo, CARVLab).
+InRoom(PDA, CARVLab).
+InRoom(Teo, CARVLab).
+KP_InRoom(Teo, CARVLab).
+KP_NotInRoom(Teo, ISLLab).
+Knows_InRoom(PDA, CARVLab).
+Knows_InRoom(Teo, CARVLab).
+Knows_NotInRoom(PDA, ISLLab).
+Knows_NotInRoom(Teo, ISLLab).
P
ReleasedAt(InRoom(PDA, CARVLab), 1).
ReleasedAt(InRoom(PDA, CARVLab), 2).
ReleasedAt(InRoom(PDA, ISLLab), 1).
ReleasedAt(InRoom(PDA, ISLLab), 2).
ReleasedAt(Knows_Holding(Teo, PDA), 0).
ReleasedAt(Knows_Holding(Teo, PDA), 1).
ReleasedAt(Knows_Holding(Teo, PDA), 2).
ReleasedAt(Knows_Holding(Teo, Teo), 0).
ReleasedAt(Knows_Holding(Teo, Teo), 1).
ReleasedAt(Knows_Holding(Teo, Teo), 2).
ReleasedAt(Knows_InRoom(PDA, CARVLab), 0).
ReleasedAt(Knows_InRoom(PDA, CARVLab), 1).
ReleasedAt(Knows_InRoom(PDA, CARVLab), 2).
ReleasedAt(Knows_InRoom(PDA, ISLLab), 0).
ReleasedAt(Knows_InRoom(PDA, ISLLab), 1).
ReleasedAt(Knows_InRoom(PDA, ISLLab), 2).
ReleasedAt(Knows_InRoom(Teo, CARVLab), 0).
ReleasedAt(Knows_InRoom(Teo, CARVLab), 1).
ReleasedAt(Knows_InRoom(Teo, CARVLab), 2).
ReleasedAt(Knows_InRoom(Teo, ISLLab), 0).
ReleasedAt(Knows_InRoom(Teo, ISLLab), 1).
ReleasedAt(Knows_InRoom(Teo, ISLLab), 2).
ReleasedAt(Knows_NotHolding(Teo, PDA), 0).
ReleasedAt(Knows_NotHolding(Teo, PDA), 1).
ReleasedAt(Knows_NotHolding(Teo, PDA), 2).
ReleasedAt(Knows_NotHolding(Teo, Teo), 0).
ReleasedAt(Knows_NotHolding(Teo, Teo), 1).
ReleasedAt(Knows_NotHolding(Teo, Teo), 2).
ReleasedAt(Knows_NotInRoom(PDA, CARVLab), 0).
ReleasedAt(Knows_NotInRoom(PDA, CARVLab), 1).
ReleasedAt(Knows_NotInRoom(PDA, CARVLab), 2).
ReleasedAt(Knows_NotInRoom(PDA, ISLLab), 0).
ReleasedAt(Knows_NotInRoom(PDA, ISLLab), 1).
ReleasedAt(Knows_NotInRoom(PDA, ISLLab), 2).
ReleasedAt(Knows_NotInRoom(Teo, CARVLab), 0).
ReleasedAt(Knows_NotInRoom(Teo, CARVLab), 1).
ReleasedAt(Knows_NotInRoom(Teo, CARVLab), 2).
ReleasedAt(Knows_NotInRoom(Teo, ISLLab), 0).
ReleasedAt(Knows_NotInRoom(Teo, ISLLab), 1).
ReleasedAt(Knows_NotInRoom(Teo, ISLLab), 2).
ReleasedAt(Kw_Holding(Teo, PDA), 0).
ReleasedAt(Kw_Holding(Teo, PDA), 1).
ReleasedAt(Kw_Holding(Teo, PDA), 2).
ReleasedAt(Kw_Holding(Teo, Teo), 0).
ReleasedAt(Kw_Holding(Teo, Teo), 1).
ReleasedAt(Kw_Holding(Teo, Teo), 2).
ReleasedAt(Kw_InRoom(PDA, CARVLab), 0).
ReleasedAt(Kw_InRoom(PDA, CARVLab), 1).
ReleasedAt(Kw_InRoom(PDA, CARVLab), 2).
ReleasedAt(Kw_InRoom(PDA, ISLLab), 0).
ReleasedAt(Kw_InRoom(PDA, ISLLab), 1).
ReleasedAt(Kw_InRoom(PDA, ISLLab), 2).
ReleasedAt(Kw_InRoom(Teo, CARVLab), 0).
ReleasedAt(Kw_InRoom(Teo, CARVLab), 1).
ReleasedAt(Kw_InRoom(Teo, CARVLab), 2).
ReleasedAt(Kw_InRoom(Teo, ISLLab), 0).
ReleasedAt(Kw_InRoom(Teo, ISLLab), 1).
ReleasedAt(Kw_InRoom(Teo, ISLLab), 2).
!Happens(PickUp(Teo, PDA), 1).
!Happens(PickUp(Teo, PDA), 2).
!Happens(PickUp(Teo, Teo), 0).
!Happens(PickUp(Teo, Teo), 1).
!Happens(PickUp(Teo, Teo), 2).
!Happens(Walk(Teo, CARVLab, CARVLab), 0).
!Happens(Walk(Teo, CARVLab, CARVLab), 1).
!Happens(Walk(Teo, CARVLab, CARVLab), 2).
!Happens(Walk(Teo, CARVLab, ISLLab), 0).
!Happens(Walk(Teo, CARVLab, ISLLab), 1).
!Happens(Walk(Teo, CARVLab, ISLLab), 2).
!Happens(Walk(Teo, ISLLab, CARVLab), 0).
!Happens(Walk(Teo, ISLLab, CARVLab), 2).
!Happens(Walk(Teo, ISLLab, ISLLab), 0).
!Happens(Walk(Teo, ISLLab, ISLLab), 1).
!Happens(Walk(Teo, ISLLab, ISLLab), 2).
!ReleasedAt(Holding(Teo, PDA), 0).
!ReleasedAt(Holding(Teo, PDA), 1).
!ReleasedAt(Holding(Teo, PDA), 2).
!ReleasedAt(Holding(Teo, Teo), 0).
!ReleasedAt(Holding(Teo, Teo), 1).
!ReleasedAt(Holding(Teo, Teo), 2).
!ReleasedAt(InRoom(PDA, CARVLab), 0).
!ReleasedAt(InRoom(PDA, ISLLab), 0).
!ReleasedAt(InRoom(Teo, CARVLab), 0).
!ReleasedAt(InRoom(Teo, CARVLab), 1).
!ReleasedAt(InRoom(Teo, CARVLab), 2).
!ReleasedAt(InRoom(Teo, ISLLab), 0).
!ReleasedAt(InRoom(Teo, ISLLab), 1).
!ReleasedAt(InRoom(Teo, ISLLab), 2).
!ReleasedAt(KP_Holding(Teo, PDA), 0).
!ReleasedAt(KP_Holding(Teo, PDA), 1).
!ReleasedAt(KP_Holding(Teo, PDA), 2).
!ReleasedAt(KP_Holding(Teo, Teo), 0).
!ReleasedAt(KP_Holding(Teo, Teo), 1).
!ReleasedAt(KP_Holding(Teo, Teo), 2).
!ReleasedAt(KP_InRoom(PDA, CARVLab), 0).
!ReleasedAt(KP_InRoom(PDA, CARVLab), 1).
!ReleasedAt(KP_InRoom(PDA, CARVLab), 2).
!ReleasedAt(KP_InRoom(PDA, ISLLab), 0).
!ReleasedAt(KP_InRoom(PDA, ISLLab), 1).
!ReleasedAt(KP_InRoom(PDA, ISLLab), 2).
!ReleasedAt(KP_InRoom(Teo, CARVLab), 0).
!ReleasedAt(KP_InRoom(Teo, CARVLab), 1).
!ReleasedAt(KP_InRoom(Teo, CARVLab), 2).
!ReleasedAt(KP_InRoom(Teo, ISLLab), 0).
!ReleasedAt(KP_InRoom(Teo, ISLLab), 1).
!ReleasedAt(KP_InRoom(Teo, ISLLab), 2).
!ReleasedAt(KP_NotHolding(Teo, PDA), 0).
!ReleasedAt(KP_NotHolding(Teo, PDA), 1).
!ReleasedAt(KP_NotHolding(Teo, PDA), 2).
!ReleasedAt(KP_NotHolding(Teo, Teo), 0).
!ReleasedAt(KP_NotHolding(Teo, Teo), 1).
!ReleasedAt(KP_NotHolding(Teo, Teo), 2).
!ReleasedAt(KP_NotInRoom(PDA, CARVLab), 0).
!ReleasedAt(KP_NotInRoom(PDA, CARVLab), 1).
!ReleasedAt(KP_NotInRoom(PDA, CARVLab), 2).
!ReleasedAt(KP_NotInRoom(PDA, ISLLab), 0).
!ReleasedAt(KP_NotInRoom(PDA, ISLLab), 1).
!ReleasedAt(KP_NotInRoom(PDA, ISLLab), 2).
!ReleasedAt(KP_NotInRoom(Teo, CARVLab), 0).
!ReleasedAt(KP_NotInRoom(Teo, CARVLab), 1).
!ReleasedAt(KP_NotInRoom(Teo, CARVLab), 2).
!ReleasedAt(KP_NotInRoom(Teo, ISLLab), 0).
!ReleasedAt(KP_NotInRoom(Teo, ISLLab), 1).
!ReleasedAt(KP_NotInRoom(Teo, ISLLab), 2).
CarryingPDA: 0 predicates, 0 functions, 12 fluents, 2 events, 38 axioms
EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
encoding 0.3s
solution 0.1s
total 0.6s