The cat sees the mouse. The cat sees the tiger. The cat visits the mouse. The mouse likes the tiger. The rabbit is nice. The rabbit likes the cat. The rabbit visits the tiger. The tiger is cold. The tiger is nice. The tiger visits the cat. If someone likes the tiger then the tiger likes the cat. If the tiger is young and the tiger sees the mouse then the mouse visits the cat. If the tiger likes the cat and the tiger sees the cat then the tiger sees the mouse. If someone is young then they see the mouse. If someone visits the tiger then they see the tiger. If someone is young and they like the cat then they see the rabbit. If someone visits the rabbit and they like the mouse then the mouse sees the cat. If someone visits the rabbit then they see the rabbit.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone likes the tiger then the tiger likes the cat.
((("someone" "likes" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If the tiger is young and the tiger sees the mouse then the mouse visits the cat.
((("tiger" "is" "young" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "visits" "cat" "+"))
If the tiger likes the cat and the tiger sees the cat then the tiger sees the mouse.
((("tiger" "likes" "cat" "+") ("tiger" "sees" "cat" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone is young then they see the mouse.
((("someone" "is" "young" "+")) -> ("someone" "sees" "mouse" "+"))
If someone visits the tiger then they see the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is young and they like the cat then they see the rabbit.
((("someone" "is" "young" "+") ("someone" "likes" "cat" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone visits the rabbit and they like the mouse then the mouse sees the cat.
((("someone" "visits" "rabbit" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone visits the rabbit then they see the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "sees" "rabbit" "+"))
The tiger is nice.
True
1
proof
[(triple9)]
("tiger" "is" "nice" "+")
triple9
The cat does not see the mouse.
False
1
inv-proof
[(triple1)]
("cat" "sees" "mouse" "-")
triple1
The tiger likes the cat.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger does not like the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "likes" "cat" "-")
((triple4) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The rabbit sees the mouse.
Unknown
rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "mouse" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The cat sees the mouse.[(triple1)] The cat sees the tiger.[(triple2)] The cat visits the mouse.[(triple3)] The mouse likes the tiger.[(triple4)] The rabbit is nice.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit visits the tiger.[(triple7)] The tiger is cold.[(triple8)] The tiger is nice.[(triple9)] The tiger visits the cat.[(triple10)] @1: The rabbit sees the tiger.[(((triple7) -> rule5))] The tiger likes the cat.[(((triple4) -> rule1))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple7) -> (rule5 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1