The bear does not like the squirrel. The dog is big. The lion sees the squirrel. The squirrel likes the bear. If something visits the bear and it is big then the bear is red. If something likes the bear then the bear does not like the lion. If something is red then it visits the dog. If the dog likes the bear and the bear is round then the dog sees the bear. If something visits the dog and the dog is not red then it visits the lion. If something is nice and not red then it visits the lion.
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
The dog is big.
("dog" "is" "big" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
If something visits the bear and it is big then the bear is red.
((("something" "visits" "bear" "+") ("something" "is" "big" "+")) -> ("bear" "is" "red" "+"))
If something likes the bear then the bear does not like the lion.
((("something" "likes" "bear" "+")) -> ("bear" "likes" "lion" "-"))
If something is red then it visits the dog.
((("something" "is" "red" "+")) -> ("something" "visits" "dog" "+"))
If the dog likes the bear and the bear is round then the dog sees the bear.
((("dog" "likes" "bear" "+") ("bear" "is" "round" "+")) -> ("dog" "sees" "bear" "+"))
If something visits the dog and the dog is not red then it visits the lion.
((("something" "visits" "dog" "+") ("dog" "is" "red" "~")) -> ("something" "visits" "lion" "+"))
If something is nice and not red then it visits the lion.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "visits" "lion" "+"))
The bear does not like the squirrel.
True
1
proof
[(triple1)]
("bear" "likes" "squirrel" "-")
triple1
The squirrel does not like the bear.
False
1
inv-proof
[(triple4)]
("squirrel" "likes" "bear" "-")
triple4
The bear does not visit the lion.
Unknown
inv-rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The bear does not like the squirrel.[(triple1)] The dog is big.[(triple2)] The lion sees the squirrel.[(triple3)] The squirrel likes the bear.[(triple4)] @1: The bear does not like the lion.[(((triple4) -> rule2))]
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple4
The bear does not like the lion.
("bear" "likes" "lion" "-")
((triple4) -> (rule2 % int1))
The bear does not like the lion.
("bear" "likes" "lion" "-")
int1