The bear likes the dog. The dog likes the rabbit. The rabbit visits the bear. The squirrel likes the bear. If something is kind then it eats the dog. If something visits the squirrel and the squirrel is green then it is green. If something visits the bear then the bear visits the squirrel. If something likes the squirrel then the squirrel visits the dog. If something visits the squirrel then it visits the dog. If something visits the dog and it is cold then the dog is kind. If something visits the bear then it eats the bear. If something eats the squirrel then it visits the rabbit.
The bear likes the dog.
("bear" "likes" "dog" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
If something is kind then it eats the dog.
((("something" "is" "kind" "+")) -> ("something" "eats" "dog" "+"))
If something visits the squirrel and the squirrel is green then it is green.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("something" "is" "green" "+"))
If something visits the bear then the bear visits the squirrel.
((("something" "visits" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If something likes the squirrel then the squirrel visits the dog.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If something visits the squirrel then it visits the dog.
((("something" "visits" "squirrel" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog and it is cold then the dog is kind.
((("something" "visits" "dog" "+") ("something" "is" "cold" "+")) -> ("dog" "is" "kind" "+"))
If something visits the bear then it eats the bear.
((("something" "visits" "bear" "+")) -> ("something" "eats" "bear" "+"))
If something eats the squirrel then it visits the rabbit.
((("something" "eats" "squirrel" "+")) -> ("something" "visits" "rabbit" "+"))
The dog likes the rabbit.
True
1
proof
[(triple2)]
("dog" "likes" "rabbit" "+")
triple2
The bear does not like the dog.
False
1
inv-proof
[(triple1)]
("bear" "likes" "dog" "-")
triple1
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "-")
The bear eats the rabbit.
Unknown
random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "+")
@0: The bear likes the dog.[(triple1)] The dog likes the rabbit.[(triple2)] The rabbit visits the bear.[(triple3)] The squirrel likes the bear.[(triple4)] @1: The bear visits the squirrel.[(((triple3) -> rule3))] The rabbit eats the bear.[(((triple3) -> rule7))] @2: The bear visits the dog.[(((((triple3) -> rule3)) -> rule5))]
The bear likes the dog.
("bear" "likes" "dog" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple4
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((triple3) -> (rule3 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((triple3) -> (rule7 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2