The cat is kind. The mouse does not chase the squirrel. The rabbit is kind. The squirrel does not chase the mouse. Young things are kind. If something sees the mouse and it likes the squirrel then the squirrel does not like the mouse.
The cat is kind.
("cat" "is" "kind" "+")
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something sees the mouse and it likes the squirrel then the squirrel does not like the mouse.
((("something" "sees" "mouse" "+") ("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "-"))
The cat is kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "-")
The cat chases the mouse.
Unknown
random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "+")
@0: The cat is kind.[(triple1)] The mouse does not chase the squirrel.[(triple2)] The rabbit is kind.[(triple3)] The squirrel does not chase the mouse.[(triple4)]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The mouse does not chase the squirrel.
("mouse" "chases" "squirrel" "-")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
triple4