The cat likes the dog. The dog likes the tiger. The mouse sees the tiger. The tiger sees the cat. If something needs the cat and the cat likes the tiger then the cat sees the mouse. If something likes the cat and the cat likes the tiger then the cat needs the mouse. If something is green then it needs the dog. If something sees the cat then the cat is blue. If something is rough then it sees the dog. If the dog likes the mouse then the dog needs the cat.
The cat likes the dog.
("cat" "likes" "dog" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something needs the cat and the cat likes the tiger then the cat sees the mouse.
((("something" "needs" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("cat" "sees" "mouse" "+"))
If something likes the cat and the cat likes the tiger then the cat needs the mouse.
((("something" "likes" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("cat" "needs" "mouse" "+"))
If something is green then it needs the dog.
((("something" "is" "green" "+")) -> ("something" "needs" "dog" "+"))
If something sees the cat then the cat is blue.
((("something" "sees" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something is rough then it sees the dog.
((("something" "is" "rough" "+")) -> ("something" "sees" "dog" "+"))
If the dog likes the mouse then the dog needs the cat.
((("dog" "likes" "mouse" "+")) -> ("dog" "needs" "cat" "+"))
The mouse sees the tiger.
True
1
proof
[(triple3)]
("mouse" "sees" "tiger" "+")
triple3
The tiger does not see the cat.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "cat" "-")
triple4
The mouse does not need the dog.
Unknown
inv-rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "dog" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat likes the dog.[(triple1)] The dog likes the tiger.[(triple2)] The mouse sees the tiger.[(triple3)] The tiger sees the cat.[(triple4)] @1: The cat is blue.[(((triple4) -> rule4))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4
The cat is blue.
("cat" "is" "blue" "+")
((triple4) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1