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