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