The cow chases the mouse. The cow chases the rabbit. The cow sees the mouse. The cow sees the rabbit. The lion chases the rabbit. The lion needs the cow. The mouse chases the cow. The mouse chases the lion. The mouse needs the rabbit. The mouse sees the lion. The rabbit chases the mouse. The rabbit is cold. The rabbit is rough. The rabbit needs the mouse. The rabbit sees the mouse. If someone chases the cow and the cow is nice then they see the cow. If someone sees the mouse then they are kind. If someone needs the cow and they need the rabbit then the cow is rough. If the mouse sees the rabbit and the rabbit is rough then the mouse chases the cow. If someone chases the cow then they are rough. If someone sees the mouse and they see the lion then the mouse sees the cow.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone chases the cow and the cow is nice then they see the cow.
((("someone" "chases" "cow" "+") ("cow" "is" "nice" "+")) -> ("someone" "sees" "cow" "+"))
If someone sees the mouse then they are kind.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the cow and they need the rabbit then the cow is rough.
((("someone" "needs" "cow" "+") ("someone" "needs" "rabbit" "+")) -> ("cow" "is" "rough" "+"))
If the mouse sees the rabbit and the rabbit is rough then the mouse chases the cow.
((("mouse" "sees" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("mouse" "chases" "cow" "+"))
If someone chases the cow then they are rough.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the mouse and they see the lion then the mouse sees the cow.
((("someone" "sees" "mouse" "+") ("someone" "sees" "lion" "+")) -> ("mouse" "sees" "cow" "+"))
The lion chases the rabbit.
True
1
proof
[(triple5)]
("lion" "chases" "rabbit" "+")
triple5
The rabbit is not rough.
False
1
inv-proof
[(triple13)]
("rabbit" "is" "rough" "-")
triple13
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The cow chases the rabbit.[(triple2)] The cow sees the mouse.[(triple3)] The cow sees the rabbit.[(triple4)] The lion chases the rabbit.[(triple5)] The lion needs the cow.[(triple6)] The mouse chases the cow.[(triple7)] The mouse chases the lion.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse sees the lion.[(triple10)] The rabbit chases the mouse.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is rough.[(triple13)] The rabbit needs the mouse.[(triple14)] The rabbit sees the mouse.[(triple15)] @1: The cow is kind.[(((triple3) -> rule2))] The mouse is rough.[(((triple7) -> rule5))] The rabbit is kind.[(((triple15) -> rule2))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple4
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple5
The lion needs the cow.
("lion" "needs" "cow" "+")
triple6
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple7
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The cow is kind.
("cow" "is" "kind" "+")
((triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple7) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple15) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1