The dog is cold. The mouse is rough. The rabbit sees the dog. If something likes the rabbit then the rabbit is green. If something is rough then it chases the mouse.
The dog is cold.
("dog" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something likes the rabbit then the rabbit is green.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something is rough then it chases the mouse.
((("something" "is" "rough" "+")) -> ("something" "chases" "mouse" "+"))
The dog is cold.
True
1
proof
[(triple1)]
("dog" "is" "cold" "+")
triple1
The rabbit does not see the dog.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "dog" "-")
triple3
The mouse chases the mouse.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "chases" "mouse" "-")
((triple2) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
Unknown
inv-rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "mouse" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
@0: The dog is cold.[(triple1)] The mouse is rough.[(triple2)] The rabbit sees the dog.[(triple3)] @1: The mouse chases the mouse.[(((triple2) -> rule2))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1