The dog is blue. The dog is rough. The dog likes the mouse. The dog likes the rabbit. The mouse is blue. The mouse sees the rabbit. The rabbit eats the dog. The rabbit does not eat the mouse. The rabbit is blue. The rabbit is not cold. The rabbit is round. The rabbit likes the dog. The rabbit likes the mouse. The rabbit does not see the dog. The rabbit sees the mouse. If something sees the dog and it eats the mouse then it sees the mouse. If something likes the dog then it eats the rabbit.
The dog is blue.
("dog" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the dog and it eats the mouse then it sees the mouse.
((("something" "sees" "dog" "+") ("something" "eats" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something likes the dog then it eats the rabbit.
((("something" "likes" "dog" "+")) -> ("something" "eats" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple11)]
("rabbit" "is" "round" "+")
triple11
The rabbit sees the dog.
False
1
inv-proof
[(triple14)]
("rabbit" "sees" "dog" "+")
triple14
The rabbit eats the rabbit.
True
2
proof
[(((triple12) -> rule2))]
("rabbit" "eats" "rabbit" "+")
((triple12) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple12) -> rule2))]
("rabbit" "eats" "rabbit" "-")
((triple12) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The dog is blue.[(triple1)] The dog is rough.[(triple2)] The dog likes the mouse.[(triple3)] The dog likes the rabbit.[(triple4)] The mouse is blue.[(triple5)] The mouse sees the rabbit.[(triple6)] The rabbit does not eat the mouse.[(triple8)] The rabbit does not see the dog.[(triple14)] The rabbit eats the dog.[(triple7)] The rabbit is blue.[(triple9)] The rabbit is not cold.[(triple10)] The rabbit is round.[(triple11)] The rabbit likes the dog.[(triple12)] The rabbit likes the mouse.[(triple13)] The rabbit sees the mouse.[(triple15)] @1: The rabbit eats the rabbit.[(((triple12) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple3
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
triple8
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple14
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple12
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple12) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1