The lion eats the rabbit. The lion sees the squirrel. The rabbit eats the squirrel. The rabbit is kind. The squirrel is cold. The squirrel is young. The squirrel sees the rabbit. If someone sees the squirrel then the squirrel eats the lion. If someone is kind and they see the squirrel then they visit the lion. If someone visits the lion then they eat the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the squirrel then the squirrel eats the lion.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "eats" "lion" "+"))
If someone is kind and they see the squirrel then they visit the lion.
((("someone" "is" "kind" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion then they eat the rabbit.
((("someone" "visits" "lion" "+")) -> ("someone" "eats" "rabbit" "+"))
The lion eats the rabbit.
True
1
proof
[(triple1)]
("lion" "eats" "rabbit" "+")
triple1
The rabbit does not eat the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "squirrel" "-")
triple3
The squirrel eats the lion.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "eats" "lion" "+")
((triple2) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "eats" "lion" "-")
((triple2) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@2: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit visits the lion.
Unknown
rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "lion" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion eats the rabbit.[(triple1)] The lion sees the squirrel.[(triple2)] The rabbit eats the squirrel.[(triple3)] The rabbit is kind.[(triple4)] The squirrel is cold.[(triple5)] The squirrel is young.[(triple6)] The squirrel sees the rabbit.[(triple7)] @1: The squirrel eats the lion.[(((triple2) -> rule1))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple7
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
((triple2) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1