The mouse needs the tiger. The tiger is round. If something needs the tiger then the tiger does not like the mouse. If something is round and it eats the mouse then the mouse is nice. If something needs the tiger then it is big.
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something needs the tiger then the tiger does not like the mouse.
((("something" "needs" "tiger" "+")) -> ("tiger" "likes" "mouse" "-"))
If something is round and it eats the mouse then the mouse is nice.
((("something" "is" "round" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something needs the tiger then it is big.
((("something" "needs" "tiger" "+")) -> ("something" "is" "big" "+"))
The mouse needs the tiger.
True
1
proof
[(triple1)]
("mouse" "needs" "tiger" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "-")
triple2
The tiger does not like the mouse.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "likes" "mouse" "-")
((triple1) -> (rule1 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1
The mouse is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "is" "big" "-")
((triple1) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "big" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "nice" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
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 round.[(triple2)] @1: The mouse is big.[(((triple1) -> rule3))] The tiger does not like the mouse.[(((triple1) -> rule1))]
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
((triple1) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
((triple1) -> (rule1 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1