;OFFICE
;HISTORY OF THE SYSTEM
Happens(Init(),0).
Happens(AttCreateTP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),0).
Happens(AttCreateComm(Seller,Buyer,TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),TP(PTrue(),2,3,Exist)),1).
Happens(Deliver(Seller,Buyer,CD),2).

>>> decreasoner.run('sviluppo/TPExistComm.e')
Discrete Event Calculus Reasoner 1.0
loading sviluppo/TPExistComm.e
loading foundations/Root.e
loading foundations/EC.e
19567 variables and 41615 clauses
relsat solver
1 model
---
model 1:
0
Happens(AttCreateTP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), 0).
Happens(Elapse(0), 0).
Happens(Init(), 0).
1
+ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), Undef).
+ETP(TP(PTrue(), 2, 3, Exist), True).
+TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist).
+TP(PTrue(), 2, 3, Exist).
Happens(AttCreateComm(Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)), 1).
Happens(Elapse(1), 1).
2
+Comm(Pending, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
Happens(Deliver(Seller, Buyer, CD), 2).
Happens(Elapse(2), 2).
3
-Comm(Pending, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
-ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), Undef).
+Comm(Fulfilled, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
+Done(Seller, Deliver(Seller, Buyer, CD)).
+ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), True).
EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
TPExistComm: 0 predicates, 0 functions, 5 fluents, 5 events, 18 axioms
encoding 6592.3s/109.9m/1.8h
solution 5.9s
total 6614.0s/110.2m/1.8h

---------------------------------------------------------------------------------------------------------------
Happens(Init(),0).
Happens(AttCreateTP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),0).
Happens(AttCreateComm(Seller,Buyer,TP(Done(Seller,Deliver(Seller,Buyer,CD)),2,3,Exist),TP(PTrue(),2,3,Exist)),1).
Happens(Deliver(Seller,Buyer,CD),3).

>>> decreasoner.run('sviluppo/TPExistComm.e')
Discrete Event Calculus Reasoner 1.0
loading sviluppo/TPExistComm.e
loading foundations/Root.e
loading foundations/EC.e
24873 variables and 54044 clauses
relsat solver
1 model
---
model 1:
0
Happens(AttCreateTP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), 0).
Happens(Elapse(0), 0).
Happens(Init(), 0).
1
+ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), Undef).
+ETP(TP(PTrue(), 2, 3, Exist), True).
+TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist).
+TP(PTrue(), 2, 3, Exist).
Happens(AttCreateComm(Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)), 1).
Happens(Elapse(1), 1).
2
+Comm(Pending, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
Happens(Elapse(2), 2).
3
Happens(Deliver(Seller, Buyer, CD), 3).
Happens(Elapse(3), 3).
4
-Comm(Pending, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
-ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), Undef).
+Comm(Violated, Seller, Buyer, TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), TP(PTrue(), 2, 3, Exist)).
+Done(Seller, Deliver(Seller, Buyer, CD)).
+ETP(TP(Done(Seller, Deliver(Seller, Buyer, CD)), 2, 3, Exist), False).
EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms
TPExistComm: 0 predicates, 0 functions, 5 fluents, 5 events, 20 axioms
encoding 16784.1s/279.7m/4.7h
solution 8.0s
total 16813.4s/280.2m/4.7h