The mouse eats the rabbit. The mouse eats the tiger. The mouse likes the tiger. The mouse sees the tiger. The rabbit eats the mouse. The rabbit eats the tiger. The rabbit sees the tiger. The tiger eats the mouse. The tiger is green. The tiger is rough. The tiger likes the mouse. The tiger sees the rabbit. If something likes the mouse then it likes the rabbit. If something sees the rabbit then the rabbit eats the tiger. If something sees the mouse then the mouse is green. If the rabbit sees the tiger and the rabbit is round then the tiger is green. If something likes the tiger then the tiger sees the rabbit. If something likes the mouse and it likes the tiger then it sees the rabbit.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something likes the mouse then it likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "rabbit" "+"))
If something sees the rabbit then the rabbit eats the tiger.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "eats" "tiger" "+"))
If something sees the mouse then the mouse is green.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If the rabbit sees the tiger and the rabbit is round then the tiger is green.
((("rabbit" "sees" "tiger" "+") ("rabbit" "is" "round" "+")) -> ("tiger" "is" "green" "+"))
If something likes the tiger then the tiger sees the rabbit.
((("something" "likes" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something likes the mouse and it likes the tiger then it sees the rabbit.
((("something" "likes" "mouse" "+") ("something" "likes" "tiger" "+")) -> ("something" "sees" "rabbit" "+"))
The tiger sees the rabbit.
True
1
proof
[(triple12 OR ((triple3) -> rule5))]
("tiger" "sees" "rabbit" "+")
triple12
((triple3) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The mouse does not see the tiger.
False
1
inv-proof
[(triple4)]
("mouse" "sees" "tiger" "-")
triple4
The tiger likes the rabbit.
True
2
proof
[(((triple11) -> rule1))]
("tiger" "likes" "rabbit" "+")
((triple11) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger does not like the rabbit.
False
2
inv-proof
[(((triple11) -> rule1))]
("tiger" "likes" "rabbit" "-")
((triple11) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse likes the tiger.[(triple3)] The mouse sees the tiger.[(triple4)] The rabbit eats the mouse.[(triple5)] The rabbit eats the tiger.[(triple6 OR ((triple12) -> rule2) OR ((((triple3) -> rule5)) -> rule2))] The rabbit sees the tiger.[(triple7)] The tiger eats the mouse.[(triple8)] The tiger is green.[(triple9)] The tiger is rough.[(triple10)] The tiger likes the mouse.[(triple11)] The tiger sees the rabbit.[(triple12 OR ((triple3) -> rule5))] @1: The tiger likes the rabbit.[(((triple11) -> rule1))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
((triple12) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple7
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
((triple3) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((triple11) -> (rule1 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1