The cat eats the lion. The lion is kind. The lion sees the cat. If something sees the lion and the lion chases the cat then it chases the lion. If the lion sees the cat then the cat sees the lion. If the cat is rough then the cat chases the lion. If something is green then it chases the lion. If something chases the lion then it eats the cat. If the lion chases the cat and the cat is nice then the cat is kind.
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something sees the lion and the lion chases the cat then it chases the lion.
((("something" "sees" "lion" "+") ("lion" "chases" "cat" "+")) -> ("something" "chases" "lion" "+"))
If the lion sees the cat then the cat sees the lion.
((("lion" "sees" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If the cat is rough then the cat chases the lion.
((("cat" "is" "rough" "+")) -> ("cat" "chases" "lion" "+"))
If something is green then it chases the lion.
((("something" "is" "green" "+")) -> ("something" "chases" "lion" "+"))
If something chases the lion then it eats the cat.
((("something" "chases" "lion" "+")) -> ("something" "eats" "cat" "+"))
If the lion chases the cat and the cat is nice then the cat is kind.
((("lion" "chases" "cat" "+") ("cat" "is" "nice" "+")) -> ("cat" "is" "kind" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple2)]
("lion" "is" "kind" "-")
triple2
The cat sees the lion.
True
2
proof
[(((triple3) -> rule2))]
("cat" "sees" "lion" "+")
((triple3) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat does not see the lion.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "sees" "lion" "-")
((triple3) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat does not eat the cat.
Unknown
inv-rconc
[@2: The cat eats the cat.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "kind" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat eats the lion.[(triple1)] The lion is kind.[(triple2)] The lion sees the cat.[(triple3)] @1: The cat sees the lion.[(((triple3) -> rule2))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion sees the cat.
("lion" "sees" "cat" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple3) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1