The dog sees the tiger. The tiger sees the dog. The tiger does not visit the dog. If someone is nice then they do not visit the dog. If someone is young then they visit the dog. If someone sees the tiger then the tiger sees the dog. If the tiger is rough and the tiger is blue then the tiger does not visit the dog. If someone visits the tiger then the tiger visits the dog. If someone sees the tiger then the tiger likes the dog.
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
If someone is nice then they do not visit the dog.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "dog" "-"))
If someone is young then they visit the dog.
((("someone" "is" "young" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the tiger then the tiger sees the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If the tiger is rough and the tiger is blue then the tiger does not visit the dog.
((("tiger" "is" "rough" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "visits" "dog" "-"))
If someone visits the tiger then the tiger visits the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone sees the tiger then the tiger likes the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
The tiger sees the dog.
True
1
proof
[(triple2 OR ((triple1) -> rule3))]
("tiger" "sees" "dog" "+")
triple2
((triple1) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The dog does not see the tiger.
False
1
inv-proof
[(triple1)]
("dog" "sees" "tiger" "-")
triple1
The tiger likes the dog.
True
2
proof
[(((triple1) -> rule6))]
("tiger" "likes" "dog" "+")
((triple1) -> (rule6 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not like the dog.
False
2
inv-proof
[(((triple1) -> rule6))]
("tiger" "likes" "dog" "-")
((triple1) -> (rule6 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "dog" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The dog visits the tiger.
Unknown
random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "+")
@0: The dog sees the tiger.[(triple1)] The tiger does not visit the dog.[(triple3)] The tiger sees the dog.[(triple2 OR ((triple1) -> rule3))] @1: The tiger likes the dog.[(((triple1) -> rule6))]
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple1
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
triple3
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple2
((triple1) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple1) -> (rule6 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1