The bear chases the rabbit. The bear eats the rabbit. The rabbit chases the bear. If something eats the bear then the bear eats the rabbit. If something chases the bear and the bear is green then the bear chases the rabbit. If something eats the rabbit then the rabbit visits the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If something eats the bear then the bear eats the rabbit.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "rabbit" "+"))
If something chases the bear and the bear is green then the bear chases the rabbit.
((("something" "chases" "bear" "+") ("bear" "is" "green" "+")) -> ("bear" "chases" "rabbit" "+"))
If something eats the rabbit then the rabbit visits the bear.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
The bear chases the rabbit.
True
1
proof
[(triple1)]
("bear" "chases" "rabbit" "+")
triple1
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The rabbit visits the bear.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "visits" "bear" "+")
((triple2) -> (rule3 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit does not visit the bear.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "visits" "bear" "-")
((triple2) -> (rule3 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The bear visits the rabbit.
Unknown
random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The bear eats the rabbit.[(triple2)] The rabbit chases the bear.[(triple3)] @1: The rabbit visits the bear.[(((triple2) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((triple2) -> (rule3 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1