The cat chases the lion. The cat chases the tiger. The cat is cold. The cat visits the lion. The lion chases the rabbit. The lion does not like the cat. The rabbit is nice. The rabbit is young. The rabbit visits the cat. The tiger chases the rabbit. The tiger is kind. The tiger likes the rabbit. If something likes the rabbit and the rabbit likes the cat then the cat likes the tiger. If something is kind then it does not like the cat. If something visits the cat and it chases the rabbit then the rabbit likes the tiger. If the cat likes the lion then the cat does not chase the tiger. If the tiger does not like the cat then the cat is rough. If something is rough then it chases the tiger. If something chases the tiger and the tiger chases the cat then it visits the tiger. If something is rough then it chases the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If something likes the rabbit and the rabbit likes the cat then the cat likes the tiger.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If something is kind then it does not like the cat.
((("something" "is" "kind" "+")) -> ("something" "likes" "cat" "-"))
If something visits the cat and it chases the rabbit then the rabbit likes the tiger.
((("something" "visits" "cat" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If the cat likes the lion then the cat does not chase the tiger.
((("cat" "likes" "lion" "+")) -> ("cat" "chases" "tiger" "-"))
If the tiger does not like the cat then the cat is rough.
((("tiger" "likes" "cat" "~")) -> ("cat" "is" "rough" "+"))
If something is rough then it chases the tiger.
((("something" "is" "rough" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the tiger and the tiger chases the cat then it visits the tiger.
((("something" "chases" "tiger" "+") ("tiger" "chases" "cat" "+")) -> ("something" "visits" "tiger" "+"))
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
The tiger likes the rabbit.
True
1
proof
[(triple12)]
("tiger" "likes" "rabbit" "+")
triple12
The tiger does not chase the rabbit.
False
1
inv-proof
[(triple10)]
("tiger" "chases" "rabbit" "-")
triple10
The tiger does not like the cat.
True
2
proof
[(((triple11) -> rule2))]
("tiger" "likes" "cat" "-")
((triple11) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The tiger likes the cat.
False
2
inv-proof
[(((triple11) -> rule2))]
("tiger" "likes" "cat" "+")
((triple11) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The cat is rough.
True
3
proof
[(((((triple11) -> rule2)) -> rule5))]
("cat" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The cat is not rough.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule5))]
("cat" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The cat chases the cat.
True
4
proof
[(((((((triple11) -> rule2)) -> rule5)) -> rule8))]
("cat" "chases" "cat" "+")
((((((triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple11) -> rule2)) -> rule5)) -> rule8))]
("cat" "chases" "cat" "-")
((((((triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@2: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The cat likes the tiger.
Unknown
rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The lion chases the cat.
Unknown
rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "chases" "cat" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The cat chases the lion.[(triple1)] The cat chases the tiger.[(triple2 OR ((((((triple11) -> rule2)) -> rule5)) -> rule6))] The cat is cold.[(triple3)] The cat visits the lion.[(triple4)] The lion chases the rabbit.[(triple5)] The lion does not like the cat.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is young.[(triple8)] The rabbit visits the cat.[(triple9)] The tiger chases the rabbit.[(triple10)] The tiger is kind.[(triple11)] The tiger likes the rabbit.[(triple12)] @1: The tiger does not like the cat.[(((triple11) -> rule2))] @2: The cat is rough.[(((((triple11) -> rule2)) -> rule5))] @3: The cat chases the cat.[(((((((triple11) -> rule2)) -> rule5)) -> rule8))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
((((((triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
triple4
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple5
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple9
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple12
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
((triple11) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3