The cow is rough. The mouse is kind. The mouse likes the tiger. The mouse visits the tiger. The rabbit is rough. The rabbit likes the cow. The rabbit does not visit the mouse. The tiger does not chase the mouse. The tiger chases the rabbit. The tiger visits the cow. If something is blue then it chases the cow.
The cow is rough.
("cow" "is" "rough" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is blue then it chases the cow.
((("something" "is" "blue" "+")) -> ("something" "chases" "cow" "+"))
The tiger chases the rabbit.
True
1
proof
[(triple9)]
("tiger" "chases" "rabbit" "+")
triple9
The tiger does not chase the rabbit.
False
1
inv-proof
[(triple9)]
("tiger" "chases" "rabbit" "-")
triple9
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is rough.[(triple1)] The mouse is kind.[(triple2)] The mouse likes the tiger.[(triple3)] The mouse visits the tiger.[(triple4)] The rabbit does not visit the mouse.[(triple7)] The rabbit is rough.[(triple5)] The rabbit likes the cow.[(triple6)] The tiger chases the rabbit.[(triple9)] The tiger does not chase the mouse.[(triple8)] The tiger visits the cow.[(triple10)]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple4
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple6
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
triple8
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10