The cow likes the squirrel. The dog is blue. The rabbit eats the cow. The squirrel needs the rabbit. If something is blue then it eats the squirrel. If the rabbit is young then the rabbit likes the cow.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The dog is blue.
("dog" "is" "blue" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If something is blue then it eats the squirrel.
((("something" "is" "blue" "+")) -> ("something" "eats" "squirrel" "+"))
If the rabbit is young then the rabbit likes the cow.
((("rabbit" "is" "young" "+")) -> ("rabbit" "likes" "cow" "+"))
The rabbit eats the cow.
True
1
proof
[(triple3)]
("rabbit" "eats" "cow" "+")
triple3
The cow does not like the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "likes" "squirrel" "-")
triple1
The rabbit does not like the cow.
Unknown
inv-rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "cow" "-")
The rabbit needs the cow.
Unknown
random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "+")
@0: The cow likes the squirrel.[(triple1)] The dog is blue.[(triple2)] The rabbit eats the cow.[(triple3)] The squirrel needs the rabbit.[(triple4)] @1: The dog eats the squirrel.[(((triple2) -> rule1))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1