The mouse likes the squirrel. The squirrel is not rough. If something is red then it eats the squirrel. If something likes the squirrel and the squirrel is young then it eats the squirrel. If something likes the squirrel then the squirrel likes the mouse. If something sees the squirrel then it is not red. If something likes the squirrel and the squirrel likes the mouse then the squirrel sees the mouse. If something is cold and it does not see the mouse then the mouse is kind.
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
If something is red then it eats the squirrel.
((("something" "is" "red" "+")) -> ("something" "eats" "squirrel" "+"))
If something likes the squirrel and the squirrel is young then it eats the squirrel.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "young" "+")) -> ("something" "eats" "squirrel" "+"))
If something likes the squirrel then the squirrel likes the mouse.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If something sees the squirrel then it is not red.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "red" "-"))
If something likes the squirrel and the squirrel likes the mouse then the squirrel sees the mouse.
((("something" "likes" "squirrel" "+") ("squirrel" "likes" "mouse" "+")) -> ("squirrel" "sees" "mouse" "+"))
If something is cold and it does not see the mouse then the mouse is kind.
((("something" "is" "cold" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "is" "kind" "+"))
The mouse likes the squirrel.
True
1
proof
[(triple1)]
("mouse" "likes" "squirrel" "+")
triple1
The squirrel is rough.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "rough" "+")
triple2
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse likes the squirrel.[(triple1)] The squirrel is not rough.[(triple2)] @1: The squirrel likes the mouse.[(((triple1) -> rule3))] @2: The squirrel sees the mouse.[(((triple1 ((triple1) -> rule3)) -> rule5))]
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple1
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2