The dog is kind. The mouse is rough. If something visits the dog then it chases the dog. If something is rough then it does not chase the dog. If the mouse chases the dog and the mouse is green then the mouse eats the dog.
The dog is kind.
("dog" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If something visits the dog then it chases the dog.
((("something" "visits" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something is rough then it does not chase the dog.
((("something" "is" "rough" "+")) -> ("something" "chases" "dog" "-"))
If the mouse chases the dog and the mouse is green then the mouse eats the dog.
((("mouse" "chases" "dog" "+") ("mouse" "is" "green" "+")) -> ("mouse" "eats" "dog" "+"))
The mouse is rough.
True
1
proof
[(triple2)]
("mouse" "is" "rough" "+")
triple2
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The mouse does not chase the dog.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "chases" "dog" "-")
((triple2) -> (rule2 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1
The mouse chases the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "chases" "dog" "+")
((triple2) -> (rule2 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1
The mouse does not eat the dog.
Unknown
inv-rconc
[@1: The mouse eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "dog" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog is kind.[(triple1)] The mouse is rough.[(triple2)] @1: The mouse does not chase the dog.[(((triple2) -> rule2))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
((triple2) -> (rule2 % int1))
The mouse does not chase the dog.
("mouse" "chases" "dog" "-")
int1