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