The mouse eats the tiger. The tiger is young. The tiger needs the mouse. If something eats the tiger and the tiger is green then it needs the tiger. If something needs the mouse then the mouse needs the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something eats the tiger and the tiger is green then it needs the tiger.
((("something" "eats" "tiger" "+") ("tiger" "is" "green" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the mouse then the mouse needs the tiger.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
The mouse eats the tiger.
True
1
proof
[(triple1)]
("mouse" "eats" "tiger" "+")
triple1
The tiger is not young.
False
1
inv-proof
[(triple2)]
("tiger" "is" "young" "-")
triple2
The mouse needs the tiger.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "needs" "tiger" "+")
((triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "needs" "tiger" "-")
((triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The mouse eats the tiger.[(triple1)] The tiger is young.[(triple2)] The tiger needs the mouse.[(triple3)] @1: The mouse needs the tiger.[(((triple3) -> rule2))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The tiger is young.
("tiger" "is" "young" "+")
triple2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1