The bear eats the squirrel. The lion does not like the tiger. The squirrel is blue. The tiger is nice. If someone is green then they eat the squirrel. If someone likes the bear then the bear visits the squirrel. If someone is green then they do not visit the tiger.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone is green then they eat the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone likes the bear then the bear visits the squirrel.
((("someone" "likes" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If someone is green then they do not visit the tiger.
((("someone" "is" "green" "+")) -> ("someone" "visits" "tiger" "-"))
The bear eats the squirrel.
True
1
proof
[(triple1)]
("bear" "eats" "squirrel" "+")
triple1
The lion likes the tiger.
False
1
inv-proof
[(triple2)]
("lion" "likes" "tiger" "+")
triple2
The tiger does not eat the squirrel.
Unknown
inv-rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "squirrel" "-")
The tiger likes the lion.
Unknown
random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "+")
@0: The bear eats the squirrel.[(triple1)] The lion does not like the tiger.[(triple2)] The squirrel is blue.[(triple3)] The tiger is nice.[(triple4)]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4