The cow likes the squirrel. The lion likes the squirrel. The squirrel eats the cow. If someone likes the squirrel then the squirrel is rough. If the cow eats the lion and the cow likes the lion then the lion sees the cow. If the lion sees the cow and the cow likes the squirrel then the lion eats the squirrel. If the lion sees the squirrel then the squirrel sees the lion. If someone sees the lion and they are red then the lion sees the cow. If the lion likes the cow then the cow is rough. If the squirrel is nice then the squirrel is cold. If someone likes the lion and the lion eats the cow then the lion is red.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
If someone likes the squirrel then the squirrel is rough.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If the cow eats the lion and the cow likes the lion then the lion sees the cow.
((("cow" "eats" "lion" "+") ("cow" "likes" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the lion sees the cow and the cow likes the squirrel then the lion eats the squirrel.
((("lion" "sees" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("lion" "eats" "squirrel" "+"))
If the lion sees the squirrel then the squirrel sees the lion.
((("lion" "sees" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If someone sees the lion and they are red then the lion sees the cow.
((("someone" "sees" "lion" "+") ("someone" "is" "red" "+")) -> ("lion" "sees" "cow" "+"))
If the lion likes the cow then the cow is rough.
((("lion" "likes" "cow" "+")) -> ("cow" "is" "rough" "+"))
If the squirrel is nice then the squirrel is cold.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "cold" "+"))
If someone likes the lion and the lion eats the cow then the lion is red.
((("someone" "likes" "lion" "+") ("lion" "eats" "cow" "+")) -> ("lion" "is" "red" "+"))
The squirrel eats the cow.
True
1
proof
[(triple3)]
("squirrel" "eats" "cow" "+")
triple3
The squirrel does not eat the cow.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "cow" "-")
triple3
The squirrel is rough.
True
2
proof
[(((triple1) -> rule1) OR ((triple2) -> rule1))]
("squirrel" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple2) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple2) -> rule1))]
("squirrel" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple2) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "red" "-")
The squirrel sees the lion.
Unknown
rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "lion" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cow likes the squirrel.[(triple1)] The lion likes the squirrel.[(triple2)] The squirrel eats the cow.[(triple3)] @1: The squirrel is rough.[(((triple1) -> rule1) OR ((triple2) -> rule1))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
((triple2) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1