The dog is rough. The mouse is kind. The rabbit chases the dog. If someone is young and they do not visit the mouse then they chase the rabbit. If someone visits the rabbit then the rabbit visits the dog. If someone chases the dog then the dog chases the rabbit.
The dog is rough.
("dog" "is" "rough" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
If someone is young and they do not visit the mouse then they chase the rabbit.
((("someone" "is" "young" "+") ("someone" "visits" "mouse" "~")) -> ("someone" "chases" "rabbit" "+"))
If someone visits the rabbit then the rabbit visits the dog.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If someone chases the dog then the dog chases the rabbit.
((("someone" "chases" "dog" "+")) -> ("dog" "chases" "rabbit" "+"))
The dog is rough.
True
1
proof
[(triple1)]
("dog" "is" "rough" "+")
triple1
The rabbit does not chase the dog.
False
1
inv-proof
[(triple3)]
("rabbit" "chases" "dog" "-")
triple3
The dog chases the rabbit.
True
2
proof
[(((triple3) -> rule3))]
("dog" "chases" "rabbit" "+")
((triple3) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog does not chase the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "chases" "rabbit" "-")
((triple3) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The rabbit does not visit the dog.
Unknown
inv-rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "dog" "-")
The mouse chases the rabbit.
Unknown
rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "rabbit" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The dog is rough.[(triple1)] The mouse is kind.[(triple2)] The rabbit chases the dog.[(triple3)] @1: The dog chases the rabbit.[(((triple3) -> rule3))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((triple3) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1