The mouse eats the squirrel. The mouse is big. The mouse is blue. The mouse visits the squirrel. The squirrel likes the mouse. The tiger is big. The tiger visits the mouse. If someone is blue then they visit the mouse. If someone eats the tiger then the tiger is cold. If someone is green and they like the mouse then they are cold. If the squirrel is blue and the squirrel likes the mouse then the mouse is young. If someone is big and they eat the mouse then the mouse eats the squirrel. If the squirrel is cold and the squirrel likes the mouse then the mouse visits the squirrel.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is blue then they visit the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "mouse" "+"))
If someone eats the tiger then the tiger is cold.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If someone is green and they like the mouse then they are cold.
((("someone" "is" "green" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If the squirrel is blue and the squirrel likes the mouse then the mouse is young.
((("squirrel" "is" "blue" "+") ("squirrel" "likes" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone is big and they eat the mouse then the mouse eats the squirrel.
((("someone" "is" "big" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the squirrel is cold and the squirrel likes the mouse then the mouse visits the squirrel.
((("squirrel" "is" "cold" "+") ("squirrel" "likes" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
The squirrel likes the mouse.
True
1
proof
[(triple5)]
("squirrel" "likes" "mouse" "+")
triple5
The mouse does not visit the squirrel.
False
1
inv-proof
[(triple4)]
("mouse" "visits" "squirrel" "-")
triple4
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse is big.[(triple2)] The mouse is blue.[(triple3)] The mouse visits the squirrel.[(triple4)] The squirrel likes the mouse.[(triple5)] The tiger is big.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The mouse visits the mouse.[(((triple3) -> rule1))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple4
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1