The dog likes the tiger. The dog visits the tiger. The lion is blue. The lion likes the dog. The lion likes the mouse. The lion needs the dog. The lion needs the mouse. The mouse is nice. The mouse needs the dog. The mouse visits the lion. The tiger is green. The tiger is nice. The tiger is young. The tiger needs the lion. The tiger visits the lion. If something likes the mouse then it is blue. If something needs the lion then it is blue.
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something likes the mouse then it is blue.
((("something" "likes" "mouse" "+")) -> ("something" "is" "blue" "+"))
If something needs the lion then it is blue.
((("something" "needs" "lion" "+")) -> ("something" "is" "blue" "+"))
The mouse visits the lion.
True
1
proof
[(triple10)]
("mouse" "visits" "lion" "+")
triple10
The tiger does not need the lion.
False
1
inv-proof
[(triple14)]
("tiger" "needs" "lion" "-")
triple14
The tiger is blue.
True
2
proof
[(((triple14) -> rule2))]
("tiger" "is" "blue" "+")
((triple14) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple14) -> rule2))]
("tiger" "is" "blue" "-")
((triple14) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "blue" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "blue" "+")
The tiger does not like the dog.
Unknown
inv-random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The dog likes the tiger.[(triple1)] The dog visits the tiger.[(triple2)] The lion is blue.[(triple3 OR ((triple5) -> rule1))] The lion likes the dog.[(triple4)] The lion likes the mouse.[(triple5)] The lion needs the dog.[(triple6)] The lion needs the mouse.[(triple7)] The mouse is nice.[(triple8)] The mouse needs the dog.[(triple9)] The mouse visits the lion.[(triple10)] The tiger is green.[(triple11)] The tiger is nice.[(triple12)] The tiger is young.[(triple13)] The tiger needs the lion.[(triple14)] The tiger visits the lion.[(triple15)] @1: The tiger is blue.[(((triple14) -> rule2))]
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
((triple5) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
triple4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple5
The lion needs the dog.
("lion" "needs" "dog" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The tiger is blue.
("tiger" "is" "blue" "+")
((triple14) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1