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