The mouse is green. The tiger sees the mouse. If someone eats the tiger then they like the tiger. If the tiger is kind and the tiger sees the mouse then the tiger eats the mouse. If someone sees the mouse then the mouse eats the tiger. If someone sees the tiger and the tiger sees the mouse then the mouse likes the tiger. If someone likes the mouse and they eat the mouse then they are nice. If someone sees the tiger and the tiger likes the mouse then the tiger sees the mouse.
The mouse is green.
("mouse" "is" "green" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone eats the tiger then they like the tiger.
((("someone" "eats" "tiger" "+")) -> ("someone" "likes" "tiger" "+"))
If the tiger is kind and the tiger sees the mouse then the tiger eats the mouse.
((("tiger" "is" "kind" "+") ("tiger" "sees" "mouse" "+")) -> ("tiger" "eats" "mouse" "+"))
If someone sees the mouse then the mouse eats the tiger.
((("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If someone sees the tiger and the tiger sees the mouse then the mouse likes the tiger.
((("someone" "sees" "tiger" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone likes the mouse and they eat the mouse then they are nice.
((("someone" "likes" "mouse" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the tiger and the tiger likes the mouse then the tiger sees the mouse.
((("someone" "sees" "tiger" "+") ("tiger" "likes" "mouse" "+")) -> ("tiger" "sees" "mouse" "+"))
The mouse is green.
True
1
proof
[(triple1)]
("mouse" "is" "green" "+")
triple1
The tiger does not see the mouse.
False
1
inv-proof
[(triple2)]
("tiger" "sees" "mouse" "-")
triple2
The mouse eats the tiger.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "eats" "tiger" "+")
((triple2) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse does not eat the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "eats" "tiger" "-")
((triple2) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("mouse" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse does not like the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("mouse" "likes" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "nice" "+")
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 mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse is green.[(triple1)] The tiger sees the mouse.[(triple2)] @1: The mouse eats the tiger.[(((triple2) -> rule3))] @2: The mouse likes the tiger.[(((((triple2) -> rule3)) -> rule1))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple2) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2