The mouse is kind. The mouse is young. The mouse likes the tiger. The mouse needs the tiger. The mouse visits the tiger. The tiger needs the mouse. The tiger visits the mouse. If someone likes the tiger and they are blue then the tiger needs the mouse. If someone likes the tiger then the tiger visits the mouse. If someone needs the mouse and the mouse likes the tiger then the mouse visits the tiger. If the tiger is kind and the tiger visits the mouse then the mouse visits the tiger. If someone likes the tiger then they need the mouse. If someone needs the tiger and the tiger is round then the tiger likes the mouse.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone likes the tiger and they are blue then the tiger needs the mouse.
((("someone" "likes" "tiger" "+") ("someone" "is" "blue" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone likes the tiger then the tiger visits the mouse.
((("someone" "likes" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone needs the mouse and the mouse likes the tiger then the mouse visits the tiger.
((("someone" "needs" "mouse" "+") ("mouse" "likes" "tiger" "+")) -> ("mouse" "visits" "tiger" "+"))
If the tiger is kind and the tiger visits the mouse then the mouse visits the tiger.
((("tiger" "is" "kind" "+") ("tiger" "visits" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If someone likes the tiger then they need the mouse.
((("someone" "likes" "tiger" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the tiger and the tiger is round then the tiger likes the mouse.
((("someone" "needs" "tiger" "+") ("tiger" "is" "round" "+")) -> ("tiger" "likes" "mouse" "+"))
The mouse likes the tiger.
True
1
proof
[(triple3)]
("mouse" "likes" "tiger" "+")
triple3
The mouse does not visit the tiger.
False
1
inv-proof
[(triple5 OR ((triple6 triple3) -> rule3) OR ((((triple3) -> rule5) triple3) -> rule3))]
("mouse" "visits" "tiger" "-")
triple5
((triple6 triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The mouse is kind.[(triple1)] The mouse is young.[(triple2)] The mouse likes the tiger.[(triple3)] The mouse needs the tiger.[(triple4)] The mouse visits the tiger.[(triple5 OR ((triple6 triple3) -> rule3) OR ((((triple3) -> rule5) triple3) -> rule3))] The tiger needs the mouse.[(triple6)] The tiger visits the mouse.[(triple7 OR ((triple3) -> rule2))] @1: The mouse needs the mouse.[(((triple3) -> rule5))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
((triple6 triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
((triple3) -> (rule2 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1