The bear visits the cow. The cow likes the bear. The cow likes the lion. The cow visits the lion. The lion is big. The lion visits the mouse. The mouse chases the bear. The mouse chases the lion. The mouse is round. The mouse likes the lion. If someone likes the bear then the bear chases the mouse. If someone is big and not red then they do not chase the cow.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If someone likes the bear then the bear chases the mouse.
((("someone" "likes" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If someone is big and not red then they do not chase the cow.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "chases" "cow" "-"))
The cow likes the lion.
True
1
proof
[(triple3)]
("cow" "likes" "lion" "+")
triple3
The bear does not visit the cow.
False
1
inv-proof
[(triple1)]
("bear" "visits" "cow" "-")
triple1
The bear chases the mouse.
True
2
proof
[(((triple2) -> rule1))]
("bear" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the cow.
Unknown
random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The bear visits the cow.[(triple1)] The cow likes the bear.[(triple2)] The cow likes the lion.[(triple3)] The cow visits the lion.[(triple4)] The lion is big.[(triple5)] The lion visits the mouse.[(triple6)] The mouse chases the bear.[(triple7)] The mouse chases the lion.[(triple8)] The mouse is round.[(triple9)] The mouse likes the lion.[(triple10)] @1: The bear chases the mouse.[(((triple2) -> rule1))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow likes the bear.
("cow" "likes" "bear" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The lion is big.
("lion" "is" "big" "+")
triple5
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple6
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple7
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple10
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1