The lion eats the mouse. The lion is green. The lion is kind. The lion is red. The lion is rough. The lion is young. The lion sees the mouse. The lion visits the mouse. The mouse eats the lion. The mouse is green. The mouse is kind. The mouse is red. The mouse is rough. The mouse is young. The mouse does not see the lion. The mouse visits the lion. If someone visits the lion then they eat the lion. If someone sees the mouse then they do not see the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone visits the lion then they eat the lion.
((("someone" "visits" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone sees the mouse then they do not see the lion.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "lion" "-"))
The mouse eats the lion.
True
1
proof
[(triple9 OR ((triple16) -> rule1))]
("mouse" "eats" "lion" "+")
triple9
((triple16) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is not young.
False
1
inv-proof
[(triple14)]
("mouse" "is" "young" "-")
triple14
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion eats the mouse.[(triple1)] The lion is green.[(triple2)] The lion is kind.[(triple3)] The lion is red.[(triple4)] The lion is rough.[(triple5)] The lion is young.[(triple6)] The lion sees the mouse.[(triple7)] The lion visits the mouse.[(triple8)] The mouse does not see the lion.[(triple15)] The mouse eats the lion.[(triple9 OR ((triple16) -> rule1))] The mouse is green.[(triple10)] The mouse is kind.[(triple11)] The mouse is red.[(triple12)] The mouse is rough.[(triple13)] The mouse is young.[(triple14)] The mouse visits the lion.[(triple16)] @1: The lion does not see the lion.[(((triple7) -> rule2))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple15
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
((triple16) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple16
The lion does not see the lion.
("lion" "sees" "lion" "-")
((triple7) -> (rule2 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1