The cat chases the lion. The cat eats the lion. The cat is red. The lion chases the cat. The lion is not green. The lion is kind. The lion visits the cat. If the lion chases the cat then the lion does not eat the cat. If the cat visits the lion then the cat is green. If the cat eats the lion and the cat visits the lion then the lion visits the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is red.
("cat" "is" "red" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the lion chases the cat then the lion does not eat the cat.
((("lion" "chases" "cat" "+")) -> ("lion" "eats" "cat" "-"))
If the cat visits the lion then the cat is green.
((("cat" "visits" "lion" "+")) -> ("cat" "is" "green" "+"))
If the cat eats the lion and the cat visits the lion then the lion visits the cat.
((("cat" "eats" "lion" "+") ("cat" "visits" "lion" "+")) -> ("lion" "visits" "cat" "+"))
The lion is kind.
True
1
proof
[(triple6)]
("lion" "is" "kind" "+")
triple6
The lion is not kind.
False
1
inv-proof
[(triple6)]
("lion" "is" "kind" "-")
triple6
The lion does not eat the cat.
True
2
proof
[(((triple4) -> rule1))]
("lion" "eats" "cat" "-")
((triple4) -> (rule1 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1
The lion eats the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "eats" "cat" "+")
((triple4) -> (rule1 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "green" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat chases the lion.[(triple1)] The cat eats the lion.[(triple2)] The cat is red.[(triple3)] The lion chases the cat.[(triple4)] The lion is kind.[(triple6)] The lion is not green.[(triple5)] The lion visits the cat.[(triple7)] @1: The lion does not eat the cat.[(((triple4) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The lion chases the cat.
("lion" "chases" "cat" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion is not green.
("lion" "is" "green" "-")
triple5
The lion visits the cat.
("lion" "visits" "cat" "+")
triple7
The lion does not eat the cat.
("lion" "eats" "cat" "-")
((triple4) -> (rule1 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1