The cat likes the rabbit. The dog is rough. The rabbit eats the dog. If someone is rough then they are young. If someone eats the rabbit and they are not kind then they eat the dog. If someone chases the cat and the cat is nice then they like the cat. If someone is big then they like the rabbit. If someone likes the rabbit then the rabbit likes the cat. Young people are big. If the rabbit does not like the dog then the dog chases the cat. If the rabbit does not like the dog then the dog eats the rabbit.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The dog is rough.
("dog" "is" "rough" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone eats the rabbit and they are not kind then they eat the dog.
((("someone" "eats" "rabbit" "+") ("someone" "is" "kind" "~")) -> ("someone" "eats" "dog" "+"))
If someone chases the cat and the cat is nice then they like the cat.
((("someone" "chases" "cat" "+") ("cat" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
If someone is big then they like the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the rabbit then the rabbit likes the cat.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "likes" "cat" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If the rabbit does not like the dog then the dog chases the cat.
((("rabbit" "likes" "dog" "~")) -> ("dog" "chases" "cat" "+"))
If the rabbit does not like the dog then the dog eats the rabbit.
((("rabbit" "likes" "dog" "~")) -> ("dog" "eats" "rabbit" "+"))
The rabbit eats the dog.
True
1
proof
[(triple3)]
("rabbit" "eats" "dog" "+")
triple3
The cat does not like the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "likes" "rabbit" "-")
triple1
The dog is young.
True
2
proof
[(((triple2) -> rule1))]
("dog" "is" "young" "+")
((triple2) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The rabbit does not like the cat.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((((((triple2) -> rule1)) -> rule6)) -> rule4)) -> rule5))]
("rabbit" "likes" "cat" "-")
((triple1) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
((((((((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("dog" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("dog" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog likes the rabbit.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("dog" "likes" "rabbit" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog does not like the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("dog" "likes" "rabbit" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The rabbit is not big.
Unknown
inv-rconc
[@2: The rabbit is big.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("rabbit" "is" "big" "-")
The dog eats the rabbit.
Unknown
rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "eats" "rabbit" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "young" "-")
The cat eats the dog.
Unknown
rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "dog" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The cat chases the dog.
Unknown
random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat likes the rabbit.[(triple1)] The dog is rough.[(triple2)] The rabbit eats the dog.[(triple3)] @1: The dog is young.[(((triple2) -> rule1))] The rabbit likes the cat.[(((triple1) -> rule5) OR ((((((((triple2) -> rule1)) -> rule6)) -> rule4)) -> rule5))] @2: The dog is big.[(((((triple2) -> rule1)) -> rule6))] @3: The dog likes the rabbit.[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
((triple2) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple1) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
((((((((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog is big.
("dog" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3