The mouse likes the tiger. The mouse visits the tiger. The rabbit does not like the mouse. The tiger eats the rabbit. The tiger is big. The tiger does not visit the mouse. The tiger visits the rabbit. If the mouse visits the rabbit then the rabbit eats the mouse. If the tiger is young and the tiger does not visit the rabbit then the tiger eats the mouse. If someone is kind then they like the tiger. If someone eats the rabbit then the rabbit visits the tiger. If someone likes the mouse then the mouse eats the rabbit. If the tiger does not visit the mouse and the tiger does not eat the mouse then the mouse visits the tiger.
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the mouse visits the rabbit then the rabbit eats the mouse.
((("mouse" "visits" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
If the tiger is young and the tiger does not visit the rabbit then the tiger eats the mouse.
((("tiger" "is" "young" "+") ("tiger" "visits" "rabbit" "~")) -> ("tiger" "eats" "mouse" "+"))
If someone is kind then they like the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "tiger" "+"))
If someone eats the rabbit then the rabbit visits the tiger.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If someone likes the mouse then the mouse eats the rabbit.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If the tiger does not visit the mouse and the tiger does not eat the mouse then the mouse visits the tiger.
((("tiger" "visits" "mouse" "~") ("tiger" "eats" "mouse" "~")) -> ("mouse" "visits" "tiger" "+"))
The mouse visits the tiger.
True
1
proof
[(triple2)]
("mouse" "visits" "tiger" "+")
triple2
The rabbit likes the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "mouse" "+")
triple3
The rabbit visits the tiger.
True
2
proof
[(((triple4) -> rule4))]
("rabbit" "visits" "tiger" "+")
((triple4) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit does not visit the tiger.
False
2
inv-proof
[(((triple4) -> rule4))]
("rabbit" "visits" "tiger" "-")
((triple4) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger does not eat the mouse.
Unknown
inv-rconc
[@1: The tiger eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "mouse" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The mouse likes the tiger.[(triple1)] The mouse visits the tiger.[(triple2)] The rabbit does not like the mouse.[(triple3)] The tiger does not visit the mouse.[(triple6)] The tiger eats the rabbit.[(triple4)] The tiger is big.[(triple5)] The tiger visits the rabbit.[(triple7)] @1: The rabbit visits the tiger.[(((triple4) -> rule4))]
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple2
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple3
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple6
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple7
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple4) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1