The mouse needs the tiger. The tiger is blue. If someone is big and they visit the tiger then they eat the tiger. If someone needs the mouse then they are red. If someone visits the tiger then the tiger visits the mouse. If someone needs the mouse and they eat the tiger then the tiger is kind. If someone is blue and they eat the mouse then the mouse needs the tiger. If someone needs the tiger and the tiger is blue then they visit the tiger. If the tiger needs the mouse and the mouse needs the tiger then the mouse is red. If the mouse eats the tiger then the mouse is blue.
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If someone is big and they visit the tiger then they eat the tiger.
((("someone" "is" "big" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "eats" "tiger" "+"))
If someone needs the mouse then they are red.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "red" "+"))
If someone visits the tiger then the tiger visits the mouse.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone needs the mouse and they eat the tiger then the tiger is kind.
((("someone" "needs" "mouse" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone is blue and they eat the mouse then the mouse needs the tiger.
((("someone" "is" "blue" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If someone needs the tiger and the tiger is blue then they visit the tiger.
((("someone" "needs" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("someone" "visits" "tiger" "+"))
If the tiger needs the mouse and the mouse needs the tiger then the mouse is red.
((("tiger" "needs" "mouse" "+") ("mouse" "needs" "tiger" "+")) -> ("mouse" "is" "red" "+"))
If the mouse eats the tiger then the mouse is blue.
((("mouse" "eats" "tiger" "+")) -> ("mouse" "is" "blue" "+"))
The mouse needs the tiger.
True
1
proof
[(triple1)]
("mouse" "needs" "tiger" "+")
triple1
The tiger is not blue.
False
1
inv-proof
[(triple2)]
("tiger" "is" "blue" "-")
triple2
The mouse visits the tiger.
True
3
proof
[(((triple1 triple2) -> rule6))]
("mouse" "visits" "tiger" "+")
((triple1 triple2) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse does not visit the tiger.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("mouse" "visits" "tiger" "-")
((triple1 triple2) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger visits the mouse.
True
4
proof
[(((((triple1 triple2) -> rule6)) -> rule3))]
("tiger" "visits" "mouse" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger does not visit the mouse.
False
4
inv-proof
[(((((triple1 triple2) -> rule6)) -> rule3))]
("tiger" "visits" "mouse" "-")
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse needs the tiger.[(triple1)] The tiger is blue.[(triple2)] @1: The mouse visits the tiger.[(((triple1 triple2) -> rule6))] @2: The tiger visits the mouse.[(((((triple1 triple2) -> rule6)) -> rule3))]
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple1 triple2) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2