The cow chases the mouse. The cow chases the rabbit. The cow sees the mouse. The cow visits the mouse. The mouse chases the rabbit. The mouse visits the rabbit. The rabbit is kind. If something chases the rabbit and the rabbit chases the cow then the cow sees the rabbit. If something sees the cow then the cow chases the rabbit. If something is big then it chases the mouse. If the rabbit sees the mouse then the rabbit is cold. If something is green then it chases the rabbit. If something sees the rabbit then it visits the mouse. If the mouse sees the rabbit then the mouse is rough. If something chases the mouse then it is rough.
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 visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If something chases the rabbit and the rabbit chases the cow then the cow sees the rabbit.
((("something" "chases" "rabbit" "+") ("rabbit" "chases" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If something sees the cow then the cow chases the rabbit.
((("something" "sees" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If the rabbit sees the mouse then the rabbit is cold.
((("rabbit" "sees" "mouse" "+")) -> ("rabbit" "is" "cold" "+"))
If something is green then it chases the rabbit.
((("something" "is" "green" "+")) -> ("something" "chases" "rabbit" "+"))
If something sees the rabbit then it visits the mouse.
((("something" "sees" "rabbit" "+")) -> ("something" "visits" "mouse" "+"))
If the mouse sees the rabbit then the mouse is rough.
((("mouse" "sees" "rabbit" "+")) -> ("mouse" "is" "rough" "+"))
If something chases the mouse then it is rough.
((("something" "chases" "mouse" "+")) -> ("something" "is" "rough" "+"))
The cow chases the rabbit.
True
1
proof
[(triple2)]
("cow" "chases" "rabbit" "+")
triple2
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple6)]
("mouse" "visits" "rabbit" "-")
triple6
The rabbit is not rough.
Unknown
inv-rconc
[@2: The rabbit is rough.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("rabbit" "is" "rough" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow chases the mouse.[(triple1)] The cow chases the rabbit.[(triple2)] The cow sees the mouse.[(triple3)] The cow visits the mouse.[(triple4)] The mouse chases the rabbit.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit is kind.[(triple7)] @1: The cow is rough.[(((triple1) -> rule8))]
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 visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1