The bear is blue. The bear likes the mouse. The mouse chases the bear. The mouse chases the rabbit. The mouse sees the bear. The rabbit chases the bear. The rabbit likes the bear. If someone chases the mouse then the mouse chases the rabbit.
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If someone chases the mouse then the mouse chases the rabbit.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
The mouse chases the bear.
True
1
proof
[(triple3)]
("mouse" "chases" "bear" "+")
triple3
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bear is blue.[(triple1)] The bear likes the mouse.[(triple2)] The mouse chases the bear.[(triple3)] The mouse chases the rabbit.[(triple4)] The mouse sees the bear.[(triple5)] The rabbit chases the bear.[(triple6)] The rabbit likes the bear.[(triple7)]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple4
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple5
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple6
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple7