The cat does not chase the lion. The cat is not red. The cat visits the lion. The lion is young. The lion likes the cat. The lion does not visit the cat. The rabbit visits the lion. If someone is young and they like the cat then they chase the cat. If someone likes the rabbit and the rabbit is not red then they chase the cat. If someone visits the lion and the lion chases the rabbit then they like the cat. If someone likes the cat and the cat likes the rabbit then the rabbit is young. If someone likes the cat and the cat does not chase the lion then they chase the rabbit. If someone chases the rabbit and the rabbit visits the cat then the cat chases the rabbit.
The cat does not chase the lion.
("cat" "chases" "lion" "-")
The cat is not red.
("cat" "is" "red" "-")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion does not visit the cat.
("lion" "visits" "cat" "-")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone is young and they like the cat then they chase the cat.
((("someone" "is" "young" "+") ("someone" "likes" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone likes the rabbit and the rabbit is not red then they chase the cat.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "red" "~")) -> ("someone" "chases" "cat" "+"))
If someone visits the lion and the lion chases the rabbit then they like the cat.
((("someone" "visits" "lion" "+") ("lion" "chases" "rabbit" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cat and the cat likes the rabbit then the rabbit is young.
((("someone" "likes" "cat" "+") ("cat" "likes" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone likes the cat and the cat does not chase the lion then they chase the rabbit.
((("someone" "likes" "cat" "+") ("cat" "chases" "lion" "~")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the rabbit and the rabbit visits the cat then the cat chases the rabbit.
((("someone" "chases" "rabbit" "+") ("rabbit" "visits" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
The cat is not red.
True
1
proof
[(triple2)]
("cat" "is" "red" "-")
triple2
The rabbit does not visit the lion.
False
1
inv-proof
[(triple7)]
("rabbit" "visits" "lion" "-")
triple7
The lion chases the rabbit.
True
3
proof
[(((triple5 triple1) -> rule5))]
("lion" "chases" "rabbit" "+")
((triple5 triple1) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion does not chase the rabbit.
False
3
inv-proof
[(((triple5 triple1) -> rule5))]
("lion" "chases" "rabbit" "-")
((triple5 triple1) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit likes the cat.
True
5
proof
[(((triple7 ((triple5 triple1) -> rule5)) -> rule3))]
("rabbit" "likes" "cat" "+")
((triple7 ((triple5 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The rabbit does not like the cat.
False
5
inv-proof
[(((triple7 ((triple5 triple1) -> rule5)) -> rule3))]
("rabbit" "likes" "cat" "-")
((triple7 ((triple5 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The rabbit chases the rabbit.
True
7
proof
[(((((triple7 ((triple5 triple1) -> rule5)) -> rule3) triple1) -> rule5))]
("rabbit" "chases" "rabbit" "+")
((((triple7 ((triple5 triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
7
inv-proof
[(((((triple7 ((triple5 triple1) -> rule5)) -> rule3) triple1) -> rule5))]
("rabbit" "chases" "rabbit" "-")
((((triple7 ((triple5 triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The rabbit does not chase the cat.
Unknown
inv-rconc
[@2: The rabbit chases the cat.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("rabbit" "chases" "cat" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat does not like the lion.
Unknown
inv-random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cat does not chase the lion.[(triple1)] The cat is not red.[(triple2)] The cat visits the lion.[(triple3)] The lion does not visit the cat.[(triple6)] The lion is young.[(triple4)] The lion likes the cat.[(triple5)] The rabbit visits the lion.[(triple7)] @1: The lion chases the cat.[(((triple4 triple5) -> rule1))] The lion chases the rabbit.[(((triple5 triple1) -> rule5))] @2: The cat likes the cat.[(((triple3 ((triple5 triple1) -> rule5)) -> rule3))] The rabbit likes the cat.[(((triple7 ((triple5 triple1) -> rule5)) -> rule3))] @3: The cat chases the rabbit.[(((((triple3 ((triple5 triple1) -> rule5)) -> rule3) triple1) -> rule5))] The rabbit chases the rabbit.[(((((triple7 ((triple5 triple1) -> rule5)) -> rule3) triple1) -> rule5))]
The cat does not chase the lion.
("cat" "chases" "lion" "-")
triple1
The cat is not red.
("cat" "is" "red" "-")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The lion does not visit the cat.
("lion" "visits" "cat" "-")
triple6
The lion is young.
("lion" "is" "young" "+")
triple4
The lion likes the cat.
("lion" "likes" "cat" "+")
triple5
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple4 triple5) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple5 triple1) -> (rule5 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3 ((triple5 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple7 ((triple5 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((((triple3 ((triple5 triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple7 ((triple5 triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3