The cat is rough. The cat likes the tiger. The mouse is cold. The mouse likes the rabbit. The mouse visits the tiger. The rabbit visits the tiger. The tiger visits the mouse. If someone visits the tiger then the tiger visits the rabbit. If someone visits the cat and the cat likes the tiger then they are blue. If someone sees the rabbit and they visit the cat then they see the cat.
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone visits the tiger then the tiger visits the rabbit.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone visits the cat and the cat likes the tiger then they are blue.
((("someone" "visits" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the rabbit and they visit the cat then they see the cat.
((("someone" "sees" "rabbit" "+") ("someone" "visits" "cat" "+")) -> ("someone" "sees" "cat" "+"))
The mouse likes the rabbit.
True
1
proof
[(triple4)]
("mouse" "likes" "rabbit" "+")
triple4
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple6)]
("rabbit" "visits" "tiger" "-")
triple6
The tiger visits the rabbit.
True
2
proof
[(((triple5) -> rule1) OR ((triple6) -> rule1))]
("tiger" "visits" "rabbit" "+")
((triple5) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
((triple6) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger does not visit the rabbit.
False
2
inv-proof
[(((triple5) -> rule1) OR ((triple6) -> rule1))]
("tiger" "visits" "rabbit" "-")
((triple5) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
((triple6) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "cat" "-")
The rabbit sees the cat.
Unknown
rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "cat" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The rabbit sees the mouse.
Unknown
random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "+")
@0: The cat is rough.[(triple1)] The cat likes the tiger.[(triple2)] The mouse is cold.[(triple3)] The mouse likes the rabbit.[(triple4)] The mouse visits the tiger.[(triple5)] The rabbit visits the tiger.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The tiger visits the rabbit.[(((triple5) -> rule1) OR ((triple6) -> rule1))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple5) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
((triple6) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1