Did you know ... | Search Documentation: |
Pack logicmoo_ec -- ext/ec_sources/examples/Mueller2006/Chapter11/Lottery.txt |
# # 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 #
loading examples/Mueller2006/Chapter11/Lottery.e loading foundations/Root.e loading foundations/EC.e 408 variables and 980 clauses relsat solver 1 model --- model 1: 0 Desirability(Kate, Kate, WinLotteryKate, 1). Desirability(Kate, Kate, WinLotteryLisa, 0). Desirability(Kate, Lisa, WinLotteryKate, 0). Desirability(Kate, Lisa, WinLotteryLisa, 0). Desirability(Lisa, Kate, WinLotteryKate, 1). Desirability(Lisa, Kate, WinLotteryLisa, 1). Desirability(Lisa, Lisa, WinLotteryKate, 1). Desirability(Lisa, Lisa, WinLotteryLisa, 0). Like(Kate, Kate). Like(Kate, Lisa). Like(Lisa, Kate). Like(Lisa, Lisa). Happens(WinLottery(Kate), 0). 1 +Believe(Kate, WinLotteryKate). +Believe(Lisa, WinLotteryKate). Happens(AddHappyFor(Lisa, Kate, WinLotteryKate), 1). Happens(AddJoy(Kate, WinLotteryKate), 1). Happens(AddJoy(Lisa, WinLotteryKate), 1). 2 +HappyFor(Lisa, Kate, WinLotteryKate). +Joy(Kate, WinLotteryKate). +Joy(Lisa, WinLotteryKate). 3 P !Happens(AddHappyFor(Kate, Kate, WinLotteryKate), 0). !Happens(AddHappyFor(Kate, Kate, WinLotteryKate), 1). !Happens(AddHappyFor(Kate, Kate, WinLotteryKate), 2). !Happens(AddHappyFor(Kate, Kate, WinLotteryKate), 3). !Happens(AddHappyFor(Kate, Kate, WinLotteryLisa), 0). !Happens(AddHappyFor(Kate, Kate, WinLotteryLisa), 1). !Happens(AddHappyFor(Kate, Kate, WinLotteryLisa), 2). !Happens(AddHappyFor(Kate, Kate, WinLotteryLisa), 3). !Happens(AddHappyFor(Kate, Lisa, WinLotteryKate), 0). !Happens(AddHappyFor(Kate, Lisa, WinLotteryKate), 1). !Happens(AddHappyFor(Kate, Lisa, WinLotteryKate), 2). !Happens(AddHappyFor(Kate, Lisa, WinLotteryKate), 3). !Happens(AddHappyFor(Kate, Lisa, WinLotteryLisa), 0). !Happens(AddHappyFor(Kate, Lisa, WinLotteryLisa), 1). !Happens(AddHappyFor(Kate, Lisa, WinLotteryLisa), 2). !Happens(AddHappyFor(Kate, Lisa, WinLotteryLisa), 3). !Happens(AddHappyFor(Lisa, Kate, WinLotteryKate), 0). !Happens(AddHappyFor(Lisa, Kate, WinLotteryKate), 2). !Happens(AddHappyFor(Lisa, Kate, WinLotteryKate), 3). !Happens(AddHappyFor(Lisa, Kate, WinLotteryLisa), 0). !Happens(AddHappyFor(Lisa, Kate, WinLotteryLisa), 1). !Happens(AddHappyFor(Lisa, Kate, WinLotteryLisa), 2). !Happens(AddHappyFor(Lisa, Kate, WinLotteryLisa), 3). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryKate), 0). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryKate), 1). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryKate), 2). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryKate), 3). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryLisa), 0). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryLisa), 1). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryLisa), 2). !Happens(AddHappyFor(Lisa, Lisa, WinLotteryLisa), 3). !Happens(AddJoy(Kate, WinLotteryKate), 0). !Happens(AddJoy(Kate, WinLotteryKate), 2). !Happens(AddJoy(Kate, WinLotteryKate), 3). !Happens(AddJoy(Kate, WinLotteryLisa), 0). !Happens(AddJoy(Kate, WinLotteryLisa), 1). !Happens(AddJoy(Kate, WinLotteryLisa), 2). !Happens(AddJoy(Kate, WinLotteryLisa), 3). !Happens(AddJoy(Lisa, WinLotteryKate), 0). !Happens(AddJoy(Lisa, WinLotteryKate), 2). !Happens(AddJoy(Lisa, WinLotteryKate), 3). !Happens(AddJoy(Lisa, WinLotteryLisa), 0). !Happens(AddJoy(Lisa, WinLotteryLisa), 1). !Happens(AddJoy(Lisa, WinLotteryLisa), 2). !Happens(AddJoy(Lisa, WinLotteryLisa), 3). !Happens(WinLottery(Kate), 1). !Happens(WinLottery(Kate), 2). !Happens(WinLottery(Kate), 3). !Happens(WinLottery(Lisa), 0). !Happens(WinLottery(Lisa), 1). !Happens(WinLottery(Lisa), 2). !Happens(WinLottery(Lisa), 3). !ReleasedAt(Believe(Kate, WinLotteryKate), 0). !ReleasedAt(Believe(Kate, WinLotteryKate), 1). !ReleasedAt(Believe(Kate, WinLotteryKate), 2). !ReleasedAt(Believe(Kate, WinLotteryKate), 3). !ReleasedAt(Believe(Kate, WinLotteryLisa), 0). !ReleasedAt(Believe(Kate, WinLotteryLisa), 1). !ReleasedAt(Believe(Kate, WinLotteryLisa), 2). !ReleasedAt(Believe(Kate, WinLotteryLisa), 3). !ReleasedAt(Believe(Lisa, WinLotteryKate), 0). !ReleasedAt(Believe(Lisa, WinLotteryKate), 1). !ReleasedAt(Believe(Lisa, WinLotteryKate), 2). !ReleasedAt(Believe(Lisa, WinLotteryKate), 3). !ReleasedAt(Believe(Lisa, WinLotteryLisa), 0). !ReleasedAt(Believe(Lisa, WinLotteryLisa), 1). !ReleasedAt(Believe(Lisa, WinLotteryLisa), 2). !ReleasedAt(Believe(Lisa, WinLotteryLisa), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, -1), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, -1), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, -1), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, -1), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 0), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 0), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 0), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 0), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 1), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 1), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 1), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryKate, 1), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, -1), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, -1), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, -1), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, -1), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 0), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 0), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 0), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 0), 3). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 1), 0). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 1), 1). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 1), 2). !ReleasedAt(Desirability(Kate, Kate, WinLotteryLisa, 1), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, -1), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, -1), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, -1), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, -1), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 0), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 0), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 0), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 0), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 1), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 1), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 1), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryKate, 1), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, -1), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, -1), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, -1), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, -1), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 0), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 0), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 0), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 0), 3). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 1), 0). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 1), 1). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 1), 2). !ReleasedAt(Desirability(Kate, Lisa, WinLotteryLisa, 1), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, -1), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, -1), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, -1), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, -1), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 0), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 0), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 0), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 0), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 1), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 1), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 1), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryKate, 1), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, -1), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, -1), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, -1), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, -1), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 0), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 0), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 0), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 0), 3). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 1), 0). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 1), 1). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 1), 2). !ReleasedAt(Desirability(Lisa, Kate, WinLotteryLisa, 1), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, -1), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, -1), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, -1), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, -1), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 0), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 0), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 0), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 0), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 1), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 1), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 1), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryKate, 1), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, -1), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, -1), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, -1), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, -1), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 0), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 0), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 0), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 0), 3). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 1), 0). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 1), 1). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 1), 2). !ReleasedAt(Desirability(Lisa, Lisa, WinLotteryLisa, 1), 3). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryKate), 0). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryKate), 1). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryKate), 2). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryKate), 3). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryLisa), 0). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryLisa), 1). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryLisa), 2). !ReleasedAt(HappyFor(Kate, Kate, WinLotteryLisa), 3). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryKate), 0). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryKate), 1). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryKate), 2). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryKate), 3). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryLisa), 0). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryLisa), 1). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryLisa), 2). !ReleasedAt(HappyFor(Kate, Lisa, WinLotteryLisa), 3). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryKate), 0). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryKate), 1). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryKate), 2). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryKate), 3). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryLisa), 0). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryLisa), 1). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryLisa), 2). !ReleasedAt(HappyFor(Lisa, Kate, WinLotteryLisa), 3). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryKate), 0). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryKate), 1). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryKate), 2). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryKate), 3). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryLisa), 0). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryLisa), 1). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryLisa), 2). !ReleasedAt(HappyFor(Lisa, Lisa, WinLotteryLisa), 3). !ReleasedAt(Joy(Kate, WinLotteryKate), 0). !ReleasedAt(Joy(Kate, WinLotteryKate), 1). !ReleasedAt(Joy(Kate, WinLotteryKate), 2). !ReleasedAt(Joy(Kate, WinLotteryKate), 3). !ReleasedAt(Joy(Kate, WinLotteryLisa), 0). !ReleasedAt(Joy(Kate, WinLotteryLisa), 1). !ReleasedAt(Joy(Kate, WinLotteryLisa), 2). !ReleasedAt(Joy(Kate, WinLotteryLisa), 3). !ReleasedAt(Joy(Lisa, WinLotteryKate), 0). !ReleasedAt(Joy(Lisa, WinLotteryKate), 1). !ReleasedAt(Joy(Lisa, WinLotteryKate), 2). !ReleasedAt(Joy(Lisa, WinLotteryKate), 3). !ReleasedAt(Joy(Lisa, WinLotteryLisa), 0). !ReleasedAt(Joy(Lisa, WinLotteryLisa), 1). !ReleasedAt(Joy(Lisa, WinLotteryLisa), 2). !ReleasedAt(Joy(Lisa, WinLotteryLisa), 3). !ReleasedAt(Like(Kate, Kate), 0). !ReleasedAt(Like(Kate, Kate), 1). !ReleasedAt(Like(Kate, Kate), 2). !ReleasedAt(Like(Kate, Kate), 3). !ReleasedAt(Like(Kate, Lisa), 0). !ReleasedAt(Like(Kate, Lisa), 1). !ReleasedAt(Like(Kate, Lisa), 2). !ReleasedAt(Like(Kate, Lisa), 3). !ReleasedAt(Like(Lisa, Kate), 0). !ReleasedAt(Like(Lisa, Kate), 1). !ReleasedAt(Like(Lisa, Kate), 2). !ReleasedAt(Like(Lisa, Kate), 3). !ReleasedAt(Like(Lisa, Lisa), 0). !ReleasedAt(Like(Lisa, Lisa), 1). !ReleasedAt(Like(Lisa, Lisa), 2). !ReleasedAt(Like(Lisa, Lisa), 3). EC: 7 predicates, 0 functions, 0 fluents, 0 events, 0 axioms Lottery: 0 predicates, 0 functions, 5 fluents, 3 events, 21 axioms Root: 0 predicates, 0 functions, 0 fluents, 0 events, 0 axioms encoding 0.3s solution 0.0s total 0.6s Discrete Event Calculus Reasoner 1.0