The dog visits the rabbit. The rabbit visits the dog. If the rabbit needs the dog and the dog likes the rabbit then the rabbit is young. If someone is young then they like the rabbit. If the rabbit visits the dog and the dog likes the rabbit then the rabbit likes the dog. If someone visits the dog and the dog visits the rabbit then the dog likes the rabbit. If someone visits the dog and they are cold then they need the dog. If someone likes the dog then they need the rabbit. If someone likes the dog and they need the dog then they like the rabbit. If someone needs the dog and they like the rabbit then they are big.
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If the rabbit needs the dog and the dog likes the rabbit then the rabbit is young.
((("rabbit" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone is young then they like the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "likes" "rabbit" "+"))
If the rabbit visits the dog and the dog likes the rabbit then the rabbit likes the dog.
((("rabbit" "visits" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
If someone visits the dog and the dog visits the rabbit then the dog likes the rabbit.
((("someone" "visits" "dog" "+") ("dog" "visits" "rabbit" "+")) -> ("dog" "likes" "rabbit" "+"))
If someone visits the dog and they are cold then they need the dog.
((("someone" "visits" "dog" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "dog" "+"))
If someone likes the dog then they need the rabbit.
((("someone" "likes" "dog" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the dog and they need the dog then they like the rabbit.
((("someone" "likes" "dog" "+") ("someone" "needs" "dog" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone needs the dog and they like the rabbit then they are big.
((("someone" "needs" "dog" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "is" "big" "+"))
The dog visits the rabbit.
True
1
proof
[(triple1)]
("dog" "visits" "rabbit" "+")
triple1
The dog does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "visits" "rabbit" "-")
triple1
The dog likes the rabbit.
True
3
proof
[(((triple2 triple1) -> rule4))]
("dog" "likes" "rabbit" "+")
((triple2 triple1) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog does not like the rabbit.
False
3
inv-proof
[(((triple2 triple1) -> rule4))]
("dog" "likes" "rabbit" "-")
((triple2 triple1) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog is not big.
Unknown
inv-rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("dog" "is" "big" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@3: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The dog visits the rabbit.[(triple1)] The rabbit visits the dog.[(triple2)] @1: The dog likes the rabbit.[(((triple2 triple1) -> rule4))] @2: The rabbit likes the dog.[(((triple2 ((triple2 triple1) -> rule4)) -> rule3))] @3: The rabbit needs the rabbit.[(((((triple2 ((triple2 triple1) -> rule4)) -> rule3)) -> rule6))]
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((triple2 triple1) -> (rule4 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
((triple2 ((triple2 triple1) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple2 ((triple2 triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3