The cat is kind. The lion visits the cat. If something visits the cat then the cat chases the lion. If something visits the lion then it likes the cat. If something chases the lion and it visits the lion then the lion is red. If the lion visits the cat and the cat chases the lion then the cat is kind. If something is rough then it chases the cat. If the lion chases the cat then the lion visits the cat. If something is rough and it likes the lion then the lion is kind. If something chases the cat and it likes the cat then the cat likes the lion.
The cat is kind.
("cat" "is" "kind" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If something visits the cat then the cat chases the lion.
((("something" "visits" "cat" "+")) -> ("cat" "chases" "lion" "+"))
If something visits the lion then it likes the cat.
((("something" "visits" "lion" "+")) -> ("something" "likes" "cat" "+"))
If something chases the lion and it visits the lion then the lion is red.
((("something" "chases" "lion" "+") ("something" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
If the lion visits the cat and the cat chases the lion then the cat is kind.
((("lion" "visits" "cat" "+") ("cat" "chases" "lion" "+")) -> ("cat" "is" "kind" "+"))
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
If the lion chases the cat then the lion visits the cat.
((("lion" "chases" "cat" "+")) -> ("lion" "visits" "cat" "+"))
If something is rough and it likes the lion then the lion is kind.
((("something" "is" "rough" "+") ("something" "likes" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something chases the cat and it likes the cat then the cat likes the lion.
((("something" "chases" "cat" "+") ("something" "likes" "cat" "+")) -> ("cat" "likes" "lion" "+"))
The cat is kind.
True
1
proof
[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("cat" "is" "kind" "+")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat is not kind.
False
1
inv-proof
[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("cat" "is" "kind" "-")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat chases the lion.
True
2
proof
[(((triple2) -> rule1))]
("cat" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat does not chase the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "chases" "lion" "-")
((triple2) -> (rule1 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The lion does not chase the cat.
Unknown
inv-rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "cat" "-")
The cat likes the lion.
Unknown
rconc
[@2: The cat likes the lion.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("cat" "likes" "lion" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat is kind.[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule4))] The lion visits the cat.[(triple2)] @1: The cat chases the lion.[(((triple2) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
triple2
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1