| 4 | | disprover_po('prob/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Red'),identifier(none,'LIGHTS')),member(none,identifier(none,'CONFLICT'),pow_subset(none,cartesian_product(none,identifier(none,'DIRECTION'),identifier(none,'DIRECTION')))),member(none,identifier(none,'Green'),identifier(none,'LIGHTS')),member(none,identifier(none,'NorthRight'),identifier(none,'DIRECTION')),member(none,identifier(none,'EastWest'),identifier(none,'DIRECTION')),member(none,identifier(none,'SouthRight'),identifier(none,'DIRECTION')),member(none,identifier(none,'North'),identifier(none,'DIRECTION')),member(none,identifier(none,'South'),identifier(none,'DIRECTION')),member(none,identifier(none,'Amber'),identifier(none,'LIGHTS')),partition(none,identifier(none,'LIGHTS'),[set_extension(none,[identifier(none,'Red')]),set_extension(none,[identifier(none,'Green')]),set_extension(none,[identifier(none,'Amber')])]),finite(none,identifier(none,'LIGHTS')),partition(none,identifier(none,'DIRECTION'),[set_extension(none,[identifier(none,'North')]),set_extension(none,[identifier(none,'SouthRight')]),set_extension(none,[identifier(none,'NorthRight')]),set_extension(none,[identifier(none,'EastWest')]),set_extension(none,[identifier(none,'South')])]),finite(none,identifier(none,'DIRECTION')),member(none,identifier(none,'CONFLICT'),relations(none,identifier(none,'DIRECTION'),identifier(none,'DIRECTION'))),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'EastWest')])),set_extension(none,[identifier(none,'North'),identifier(none,'South'),identifier(none,'SouthRight'),identifier(none,'NorthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'North')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'SouthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'South')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'NorthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'SouthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'North')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'NorthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'South')])),forall(none,[identifier(none,d1)],implication(none,conjunct(none,member(none,identifier(none,d1),identifier(none,'DIRECTION')),member(none,identifier(none,d1),identifier(none,'DIRECTION'))),not_subset(none,set_extension(none,[identifier(none,d1)]),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,d1)])))))]),constants(none,[identifier(none,'Red'),identifier(none,'CONFLICT'),identifier(none,'Green'),identifier(none,'NorthRight'),identifier(none,'EastWest'),identifier(none,'SouthRight'),identifier(none,'North'),identifier(none,'South'),identifier(none,'Amber')]),sets(none,[deferred_set(none,'DIRECTION'),deferred_set(none,'LIGHTS')])]),equal(none,identifier(none,'CONFLICT'),set_extension(none,[couple(none,[identifier(none,'North'),identifier(none,'SouthRight')]),couple(none,[identifier(none,'North'),identifier(none,'EastWest')]),couple(none,[identifier(none,'SouthRight'),identifier(none,'North')]),couple(none,[identifier(none,'SouthRight'),identifier(none,'EastWest')]),couple(none,[identifier(none,'NorthRight'),identifier(none,'EastWest')]),couple(none,[identifier(none,'NorthRight'),identifier(none,'South')]),couple(none,[identifier(none,'EastWest'),identifier(none,'North')]),couple(none,[identifier(none,'EastWest'),identifier(none,'SouthRight')]),couple(none,[identifier(none,'EastWest'),identifier(none,'NorthRight')]),couple(none,[identifier(none,'EastWest'),identifier(none,'South')]),couple(none,[identifier(none,'South'),identifier(none,'NorthRight')]),couple(none,[identifier(none,'South'),identifier(none,'EastWest')])])),[partition(none,identifier(none,'LIGHTS'),[set_extension(none,[identifier(none,'Red')]),set_extension(none,[identifier(none,'Green')]),set_extension(none,[identifier(none,'Amber')])]),finite(none,identifier(none,'LIGHTS')),partition(none,identifier(none,'DIRECTION'),[set_extension(none,[identifier(none,'North')]),set_extension(none,[identifier(none,'SouthRight')]),set_extension(none,[identifier(none,'NorthRight')]),set_extension(none,[identifier(none,'EastWest')]),set_extension(none,[identifier(none,'South')])]),finite(none,identifier(none,'DIRECTION')),member(none,identifier(none,'CONFLICT'),relations(none,identifier(none,'DIRECTION'),identifier(none,'DIRECTION'))),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'EastWest')])),set_extension(none,[identifier(none,'North'),identifier(none,'South'),identifier(none,'SouthRight'),identifier(none,'NorthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'North')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'SouthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'South')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'NorthRight')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'SouthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'North')])),equal(none,image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'NorthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'South')])),forall(none,[identifier(none,d1)],implication(none,conjunct(none,member(none,identifier(none,d1),identifier(none,'DIRECTION')),member(none,identifier(none,d1),identifier(none,'DIRECTION'))),not_subset(none,set_extension(none,[identifier(none,d1)]),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,d1)])))))],[],unknown). |