The bear sees the tiger. The mouse is cold. The tiger is red. If someone sees the tiger then the tiger eats the mouse. If the bear sees the mouse and the bear is nice then the mouse eats the tiger. If someone visits the tiger then they eat the mouse.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
If someone sees the tiger then the tiger eats the mouse.
((("someone" "sees" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
If the bear sees the mouse and the bear is nice then the mouse eats the tiger.
((("bear" "sees" "mouse" "+") ("bear" "is" "nice" "+")) -> ("mouse" "eats" "tiger" "+"))
If someone visits the tiger then they eat the mouse.
((("someone" "visits" "tiger" "+")) -> ("someone" "eats" "mouse" "+"))
The tiger is red.
True
1
proof
[(triple3)]
("tiger" "is" "red" "+")
triple3
The tiger is not red.
False
1
inv-proof
[(triple3)]
("tiger" "is" "red" "-")
triple3
The tiger eats the mouse.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "eats" "mouse" "+")
((triple1) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "eats" "mouse" "-")
((triple1) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The mouse does not eat the tiger.
Unknown
inv-rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "tiger" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear sees the tiger.[(triple1)] The mouse is cold.[(triple2)] The tiger is red.[(triple3)] @1: The tiger eats the mouse.[(((triple1) -> rule1))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple1) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1