The cat chases the dog. The dog visits the lion. The lion is kind. If the dog visits the cat then the cat visits the lion. If someone visits the lion and the lion is kind then they visit the cat. If the lion is green and the lion chases the dog then the lion visits the dog. If someone is round then they see the cat. If someone visits the dog then the dog chases the lion. If someone visits the cat then the cat sees the dog. If someone chases the lion and they visit the lion then the lion is kind. If someone sees the cat and they see the lion then they are round.
The cat chases the dog.
("cat" "chases" "dog" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
If the dog visits the cat then the cat visits the lion.
((("dog" "visits" "cat" "+")) -> ("cat" "visits" "lion" "+"))
If someone visits the lion and the lion is kind then they visit the cat.
((("someone" "visits" "lion" "+") ("lion" "is" "kind" "+")) -> ("someone" "visits" "cat" "+"))
If the lion is green and the lion chases the dog then the lion visits the dog.
((("lion" "is" "green" "+") ("lion" "chases" "dog" "+")) -> ("lion" "visits" "dog" "+"))
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
If someone visits the dog then the dog chases the lion.
((("someone" "visits" "dog" "+")) -> ("dog" "chases" "lion" "+"))
If someone visits the cat then the cat sees the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "sees" "dog" "+"))
If someone chases the lion and they visit the lion then the lion is kind.
((("someone" "chases" "lion" "+") ("someone" "visits" "lion" "+")) -> ("lion" "is" "kind" "+"))
If someone sees the cat and they see the lion then they are round.
((("someone" "sees" "cat" "+") ("someone" "sees" "lion" "+")) -> ("someone" "is" "round" "+"))
The cat chases the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The dog does not visit the lion.
False
1
inv-proof
[(triple2)]
("dog" "visits" "lion" "-")
triple2
The dog visits the cat.
True
3
proof
[(((triple2 triple3) -> rule2))]
("dog" "visits" "cat" "+")
((triple2 triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog does not visit the cat.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("dog" "visits" "cat" "-")
((triple2 triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the lion.
True
4
proof
[(((((triple2 triple3) -> rule2)) -> rule1))]
("cat" "visits" "lion" "+")
((((triple2 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat does not visit the lion.
False
4
inv-proof
[(((((triple2 triple3) -> rule2)) -> rule1))]
("cat" "visits" "lion" "-")
((((triple2 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat visits the cat.
True
6
proof
[(((((((triple2 triple3) -> rule2)) -> rule1) triple3) -> rule2))]
("cat" "visits" "cat" "+")
((((((triple2 triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The cat does not visit the cat.
False
6
inv-proof
[(((((((triple2 triple3) -> rule2)) -> rule1) triple3) -> rule2))]
("cat" "visits" "cat" "-")
((((((triple2 triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "round" "+")
The dog does not see the cat.
Unknown
inv-rconc
[@2: The dog sees the cat.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("dog" "sees" "cat" "-")
The dog chases the lion.
Unknown
rconc
[@2: The dog chases the lion.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("dog" "chases" "lion" "+")
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 lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat chases the dog.[(triple1)] The dog visits the lion.[(triple2)] The lion is kind.[(triple3)] @1: The dog visits the cat.[(((triple2 triple3) -> rule2))] @2: The cat sees the dog.[(((((triple2 triple3) -> rule2)) -> rule6) OR ((((((((triple2 triple3) -> rule2)) -> rule1) triple3) -> rule2)) -> rule6))] The cat visits the lion.[(((((triple2 triple3) -> rule2)) -> rule1))] @3: The cat visits the cat.[(((((((triple2 triple3) -> rule2)) -> rule1) triple3) -> rule2))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple2 triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
((((triple2 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
((((((((triple2 triple3) -> (rule2 % int4))) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
int4
The cat visits the lion.
("cat" "visits" "lion" "+")
((((triple2 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((triple2 triple3) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3