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