The cat is big. The cat likes the dog. The cat visits the dog. The cat visits the tiger. The dog is cold. The dog visits the rabbit. The rabbit is rough. The rabbit likes the dog. The rabbit likes the tiger. The tiger visits the cat. If someone chases the rabbit and they are rough then they chase the tiger. If someone is rough then they chase the rabbit.
The cat is big.
("cat" "is" "big" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone chases the rabbit and they are rough then they chase the tiger.
((("someone" "chases" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is rough then they chase the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "rabbit" "+"))
The cat likes the dog.
True
1
proof
[(triple2)]
("cat" "likes" "dog" "+")
triple2
The rabbit is not rough.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "rough" "-")
triple7
The rabbit chases the rabbit.
True
2
proof
[(((triple7) -> rule2))]
("rabbit" "chases" "rabbit" "+")
((triple7) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple7) -> rule2))]
("rabbit" "chases" "rabbit" "-")
((triple7) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the tiger.
True
4
proof
[(((((triple7) -> rule2) triple7) -> rule1))]
("rabbit" "chases" "tiger" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit does not chase the tiger.
False
4
inv-proof
[(((((triple7) -> rule2) triple7) -> rule1))]
("rabbit" "chases" "tiger" "-")
((((triple7) -> (rule2 % int2)) triple7) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The tiger does not chase the rabbit.
Unknown
inv-rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "rabbit" "-")
The cat chases the tiger.
Unknown
rconc
[@1: The cat chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "tiger" "+")
The dog does not chase the rabbit.
Unknown
inv-rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The rabbit does not visit the tiger.
Unknown
inv-random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The cat is big.[(triple1)] The cat likes the dog.[(triple2)] The cat visits the dog.[(triple3)] The cat visits the tiger.[(triple4)] The dog is cold.[(triple5)] The dog visits the rabbit.[(triple6)] The rabbit is rough.[(triple7)] The rabbit likes the dog.[(triple8)] The rabbit likes the tiger.[(triple9)] The tiger visits the cat.[(triple10)] @1: The rabbit chases the rabbit.[(((triple7) -> rule2))] @2: The rabbit chases the tiger.[(((((triple7) -> rule2) triple7) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cat visits the dog.
("cat" "visits" "dog" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple8
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple7) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule1 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2