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