The bear visits the mouse. The mouse needs the tiger. The tiger needs the mouse. If someone visits the bear and the bear eats the tiger then the bear is not nice. If someone visits the bear then they do not need the mouse. If the mouse is blue and the mouse visits the bear then the mouse needs the bear. If someone eats the tiger and they do not eat the mouse then the mouse eats the bear. If someone is nice and round then they eat the tiger. If someone needs the mouse then the mouse is not round.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone visits the bear and the bear eats the tiger then the bear is not nice.
((("someone" "visits" "bear" "+") ("bear" "eats" "tiger" "+")) -> ("bear" "is" "nice" "-"))
If someone visits the bear then they do not need the mouse.
((("someone" "visits" "bear" "+")) -> ("someone" "needs" "mouse" "-"))
If the mouse is blue and the mouse visits the bear then the mouse needs the bear.
((("mouse" "is" "blue" "+") ("mouse" "visits" "bear" "+")) -> ("mouse" "needs" "bear" "+"))
If someone eats the tiger and they do not eat the mouse then the mouse eats the bear.
((("someone" "eats" "tiger" "+") ("someone" "eats" "mouse" "~")) -> ("mouse" "eats" "bear" "+"))
If someone is nice and round then they eat the tiger.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "eats" "tiger" "+"))
If someone needs the mouse then the mouse is not round.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "round" "-"))
The mouse needs the tiger.
True
1
proof
[(triple2)]
("mouse" "needs" "tiger" "+")
triple2
The bear does not visit the mouse.
False
1
inv-proof
[(triple1)]
("bear" "visits" "mouse" "-")
triple1
The mouse is not round.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "is" "round" "-")
((triple3) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is round.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "is" "round" "+")
((triple3) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse does not eat the bear.
Unknown
inv-rconc
[@1: The mouse eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "bear" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bear visits the mouse.[(triple1)] The mouse needs the tiger.[(triple2)] The tiger needs the mouse.[(triple3)] @1: The mouse is not round.[(((triple3) -> rule6))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple3
The mouse is not round.
("mouse" "is" "round" "-")
((triple3) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1