The cat eats the mouse. The dog eats the cat. The mouse needs the dog. If something is round and it eats the mouse then it chases the dog. If something is kind then it needs the cat. If something eats the dog and it is round then it chases the dog. If something needs the mouse and it chases the mouse then it is round. If something needs the dog then the dog chases the mouse. If the cat eats the mouse and the cat is kind then the mouse eats the dog.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If something is round and it eats the mouse then it chases the dog.
((("something" "is" "round" "+") ("something" "eats" "mouse" "+")) -> ("something" "chases" "dog" "+"))
If something is kind then it needs the cat.
((("something" "is" "kind" "+")) -> ("something" "needs" "cat" "+"))
If something eats the dog and it is round then it chases the dog.
((("something" "eats" "dog" "+") ("something" "is" "round" "+")) -> ("something" "chases" "dog" "+"))
If something needs the mouse and it chases the mouse then it is round.
((("something" "needs" "mouse" "+") ("something" "chases" "mouse" "+")) -> ("something" "is" "round" "+"))
If something needs the dog then the dog chases the mouse.
((("something" "needs" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If the cat eats the mouse and the cat is kind then the mouse eats the dog.
((("cat" "eats" "mouse" "+") ("cat" "is" "kind" "+")) -> ("mouse" "eats" "dog" "+"))
The dog eats the cat.
True
1
proof
[(triple2)]
("dog" "eats" "cat" "+")
triple2
The mouse does not need the dog.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "dog" "-")
triple3
The dog chases the mouse.
True
2
proof
[(((triple3) -> rule5))]
("dog" "chases" "mouse" "+")
((triple3) -> (rule5 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "chases" "mouse" "-")
((triple3) -> (rule5 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse does not eat the dog.
Unknown
inv-rconc
[@1: The mouse eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "dog" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The cat eats the mouse.[(triple1)] The dog eats the cat.[(triple2)] The mouse needs the dog.[(triple3)] @1: The dog chases the mouse.[(((triple3) -> rule5))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple3) -> (rule5 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1