The cat likes the dog. The dog likes the cat. The dog likes the mouse. The mouse is rough. The mouse visits the tiger. The tiger is cold. The tiger is nice. The tiger likes the cat. The tiger likes the dog. The tiger needs the mouse. If something is cold then it likes the mouse. If something likes the tiger and it visits the mouse then the mouse needs the tiger. If something is young and it visits the dog then it likes the cat.
The cat likes the dog.
("cat" "likes" "dog" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something is cold then it likes the mouse.
((("something" "is" "cold" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the tiger and it visits the mouse then the mouse needs the tiger.
((("something" "likes" "tiger" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If something is young and it visits the dog then it likes the cat.
((("something" "is" "young" "+") ("something" "visits" "dog" "+")) -> ("something" "likes" "cat" "+"))
The tiger is nice.
True
1
proof
[(triple7)]
("tiger" "is" "nice" "+")
triple7
The tiger is not cold.
False
1
inv-proof
[(triple6)]
("tiger" "is" "cold" "-")
triple6
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat likes the dog.[(triple1)] The dog likes the cat.[(triple2)] The dog likes the mouse.[(triple3)] The mouse is rough.[(triple4)] The mouse visits the tiger.[(triple5)] The tiger is cold.[(triple6)] The tiger is nice.[(triple7)] The tiger likes the cat.[(triple8)] The tiger likes the dog.[(triple9)] The tiger needs the mouse.[(triple10)] @1: The tiger likes the mouse.[(((triple6) -> rule1))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The dog likes the cat.
("dog" "likes" "cat" "+")
triple2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple8
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple9
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple10
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple6) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1