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