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