The dog likes the rabbit. The rabbit is young. If the rabbit eats the dog then the rabbit is rough. If something likes the dog then the dog sees the rabbit. If something sees the dog and the dog eats the rabbit then it likes the dog. If the rabbit sees the dog then the dog sees the rabbit. If something eats the dog then it eats the rabbit. If something likes the rabbit then it likes the dog.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If the rabbit eats the dog then the rabbit is rough.
((("rabbit" "eats" "dog" "+")) -> ("rabbit" "is" "rough" "+"))
If something likes the dog then the dog sees the rabbit.
((("something" "likes" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
If something sees the dog and the dog eats the rabbit then it likes the dog.
((("something" "sees" "dog" "+") ("dog" "eats" "rabbit" "+")) -> ("something" "likes" "dog" "+"))
If the rabbit sees the dog then the dog sees the rabbit.
((("rabbit" "sees" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
If something eats the dog then it eats the rabbit.
((("something" "eats" "dog" "+")) -> ("something" "eats" "rabbit" "+"))
If something likes the rabbit then it likes the dog.
((("something" "likes" "rabbit" "+")) -> ("something" "likes" "dog" "+"))
The dog likes the rabbit.
True
1
proof
[(triple1)]
("dog" "likes" "rabbit" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "young" "-")
triple2
The dog likes the dog.
True
2
proof
[(((triple1) -> rule6))]
("dog" "likes" "dog" "+")
((triple1) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not like the dog.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "likes" "dog" "-")
((triple1) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the rabbit.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("dog" "sees" "rabbit" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not see the rabbit.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("dog" "sees" "rabbit" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "-")
The dog eats the rabbit.
Unknown
rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "rabbit" "+")
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit eats the dog.
Unknown
random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog likes the rabbit.[(triple1)] The rabbit is young.[(triple2)] @1: The dog likes the dog.[(((triple1) -> rule6))] @2: The dog sees the rabbit.[(((((triple1) -> rule6)) -> rule2))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
triple2
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple1) -> (rule6 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2