The dog is blue. The dog is green. The dog is rough. The dog is young. The dog needs the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is blue. The tiger is green. The tiger is nice. The tiger is rough. The tiger is young. The tiger needs the dog. The tiger sees the dog. The tiger visits the dog. If someone needs the dog then the dog is blue. If someone visits the dog then they see the tiger. If someone visits the tiger then the tiger visits the dog. If someone needs the dog and the dog visits the tiger then the tiger needs the dog. If the tiger needs the dog and the tiger sees the dog then the tiger is nice. If someone visits the tiger and the tiger needs the dog then the tiger visits the dog. If someone needs the dog and the dog sees the tiger then the tiger visits the dog. If the dog visits the tiger and the tiger sees the dog then the dog is nice.
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone needs the dog then the dog is blue.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "blue" "+"))
If someone visits the dog then they see the tiger.
((("someone" "visits" "dog" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the tiger then the tiger visits the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone needs the dog and the dog visits the tiger then the tiger needs the dog.
((("someone" "needs" "dog" "+") ("dog" "visits" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If the tiger needs the dog and the tiger sees the dog then the tiger is nice.
((("tiger" "needs" "dog" "+") ("tiger" "sees" "dog" "+")) -> ("tiger" "is" "nice" "+"))
If someone visits the tiger and the tiger needs the dog then the tiger visits the dog.
((("someone" "visits" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("tiger" "visits" "dog" "+"))
If someone needs the dog and the dog sees the tiger then the tiger visits the dog.
((("someone" "needs" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If the dog visits the tiger and the tiger sees the dog then the dog is nice.
((("dog" "visits" "tiger" "+") ("tiger" "sees" "dog" "+")) -> ("dog" "is" "nice" "+"))
The dog sees the tiger.
True
1
proof
[(triple6)]
("dog" "sees" "tiger" "+")
triple6
The tiger does not see the dog.
False
1
inv-proof
[(triple14)]
("tiger" "sees" "dog" "-")
triple14
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is blue.[(triple1 OR ((triple13) -> rule1))] The dog is green.[(triple2)] The dog is rough.[(triple3)] The dog is young.[(triple4)] The dog needs the tiger.[(triple5)] The dog sees the tiger.[(triple6)] The dog visits the tiger.[(triple7)] The tiger is blue.[(triple8)] The tiger is green.[(triple9)] The tiger is nice.[(triple10 OR ((triple13 triple14) -> rule5))] The tiger is rough.[(triple11)] The tiger is young.[(triple12)] The tiger needs the dog.[(triple13)] The tiger sees the dog.[(triple14)] The tiger visits the dog.[(triple15 OR ((triple7) -> rule3) OR ((triple13 triple6) -> rule7) OR ((triple7 triple13) -> rule6))] @1: The dog is nice.[(((triple7 triple14) -> rule8))] The tiger sees the tiger.[(((triple15) -> rule2) OR ((((triple7) -> rule3)) -> rule2) OR ((((triple13 triple6) -> rule7)) -> rule2) OR ((((triple7 triple13) -> rule6)) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
((triple13) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
((triple13 triple14) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple15
((triple7) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((triple13 triple6) -> (rule7 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
((triple7 triple13) -> (rule6 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple7 triple14) -> (rule8 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple15) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
((((triple13 triple6) -> (rule7 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
((((triple7 triple13) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2