The cat chases the lion. The cat likes the lion. The lion chases the cat. The lion is not kind. The lion is red. The lion likes the cat. The lion does not see the cat. If someone likes the lion then they are not big. If someone is red and they chase the lion then the lion does not chase the cat. If someone chases the lion and they do not see the cat then they are rough. If someone chases the lion and the lion is green then the lion does not like the cat. If someone sees the lion and they chase the cat then the lion likes the cat. If someone likes the cat then they like the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is red.
("lion" "is" "red" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion does not see the cat.
("lion" "sees" "cat" "-")
If someone likes the lion then they are not big.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "big" "-"))
If someone is red and they chase the lion then the lion does not chase the cat.
((("someone" "is" "red" "+") ("someone" "chases" "lion" "+")) -> ("lion" "chases" "cat" "-"))
If someone chases the lion and they do not see the cat then they are rough.
((("someone" "chases" "lion" "+") ("someone" "sees" "cat" "~")) -> ("someone" "is" "rough" "+"))
If someone chases the lion and the lion is green then the lion does not like the cat.
((("someone" "chases" "lion" "+") ("lion" "is" "green" "+")) -> ("lion" "likes" "cat" "-"))
If someone sees the lion and they chase the cat then the lion likes the cat.
((("someone" "sees" "lion" "+") ("someone" "chases" "cat" "+")) -> ("lion" "likes" "cat" "+"))
If someone likes the cat then they like the lion.
((("someone" "likes" "cat" "+")) -> ("someone" "likes" "lion" "+"))
The lion is red.
True
1
proof
[(triple5)]
("lion" "is" "red" "+")
triple5
The lion does not chase the cat.
False
1
inv-proof
[(triple3)]
("lion" "chases" "cat" "-")
triple3
The cat is not big.
True
2
proof
[(((triple2) -> rule1))]
("cat" "is" "big" "-")
((triple2) -> (rule1 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat is big.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "is" "big" "+")
((triple2) -> (rule1 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The lion is not big.
True
3
proof
[(((((triple6) -> rule6)) -> rule1))]
("lion" "is" "big" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is big.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1))]
("lion" "is" "big" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "rough" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "rough" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The cat chases the lion.[(triple1)] The cat likes the lion.[(triple2)] The lion chases the cat.[(triple3)] The lion does not see the cat.[(triple7)] The lion is not kind.[(triple4)] The lion is red.[(triple5)] The lion likes the cat.[(triple6)] @1: The cat is not big.[(((triple2) -> rule1))] The lion likes the lion.[(((triple6) -> rule6))] @2: The lion is not big.[(((((triple6) -> rule6)) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The lion chases the cat.
("lion" "chases" "cat" "+")
triple3
The lion does not see the cat.
("lion" "sees" "cat" "-")
triple7
The lion is not kind.
("lion" "is" "kind" "-")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion likes the cat.
("lion" "likes" "cat" "+")
triple6
The cat is not big.
("cat" "is" "big" "-")
((triple2) -> (rule1 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple6) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is not big.
("lion" "is" "big" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2