The mouse is young. The squirrel is green. The squirrel visits the mouse. If someone chases the mouse then the mouse eats the squirrel. If someone chases the mouse then they are blue. If the mouse chases the squirrel then the mouse visits the squirrel. If someone visits the mouse then the mouse chases the squirrel. If someone eats the mouse and they visit the mouse then the mouse is young. If someone chases the mouse and they visit the mouse then they are kind.
The mouse is young.
("mouse" "is" "young" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone chases the mouse then the mouse eats the squirrel.
((("someone" "chases" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If someone chases the mouse then they are blue.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "blue" "+"))
If the mouse chases the squirrel then the mouse visits the squirrel.
((("mouse" "chases" "squirrel" "+")) -> ("mouse" "visits" "squirrel" "+"))
If someone visits the mouse then the mouse chases the squirrel.
((("someone" "visits" "mouse" "+")) -> ("mouse" "chases" "squirrel" "+"))
If someone eats the mouse and they visit the mouse then the mouse is young.
((("someone" "eats" "mouse" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone chases the mouse and they visit the mouse then they are kind.
((("someone" "chases" "mouse" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "is" "kind" "+"))
The mouse is young.
True
1
proof
[(triple1)]
("mouse" "is" "young" "+")
triple1
The squirrel is not green.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "green" "-")
triple2
The mouse chases the squirrel.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "chases" "squirrel" "+")
((triple3) -> (rule4 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "chases" "squirrel" "-")
((triple3) -> (rule4 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "kind" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The mouse is young.[(triple1)] The squirrel is green.[(triple2)] The squirrel visits the mouse.[(triple3)] @1: The mouse chases the squirrel.[(((triple3) -> rule4))] @2: The mouse visits the squirrel.[(((((triple3) -> rule4)) -> rule3))]
The mouse is young.
("mouse" "is" "young" "+")
triple1
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
((triple3) -> (rule4 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int2