The bald eagle is cold. The bald eagle needs the lion. The dog is nice. The dog likes the lion. The lion likes the dog. The lion sees the bald eagle. The lion sees the rabbit. The rabbit is nice. The rabbit needs the dog. The rabbit sees the dog. If someone likes the lion then they need the rabbit. If someone likes the rabbit then the rabbit is nice. If someone sees the lion and they are round then the lion sees the rabbit.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone likes the lion then they need the rabbit.
((("someone" "likes" "lion" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the rabbit then the rabbit is nice.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If someone sees the lion and they are round then the lion sees the rabbit.
((("someone" "sees" "lion" "+") ("someone" "is" "round" "+")) -> ("lion" "sees" "rabbit" "+"))
The rabbit is nice.
True
1
proof
[(triple8)]
("rabbit" "is" "nice" "+")
triple8
The dog is not nice.
False
1
inv-proof
[(triple3)]
("dog" "is" "nice" "-")
triple3
The dog needs the rabbit.
True
2
proof
[(((triple4) -> rule1))]
("dog" "needs" "rabbit" "+")
((triple4) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog does not need the rabbit.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "needs" "rabbit" "-")
((triple4) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The bald eagle needs the rabbit.
Unknown
rconc
[@1: The bald eagle needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "needs" "rabbit" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle needs the lion.[(triple2)] The dog is nice.[(triple3)] The dog likes the lion.[(triple4)] The lion likes the dog.[(triple5)] The lion sees the bald eagle.[(triple6)] The lion sees the rabbit.[(triple7)] The rabbit is nice.[(triple8)] The rabbit needs the dog.[(triple9)] The rabbit sees the dog.[(triple10)] @1: The dog needs the rabbit.[(((triple4) -> rule1))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog likes the lion.
("dog" "likes" "lion" "+")
triple4
The lion likes the dog.
("lion" "likes" "dog" "+")
triple5
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple10
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple4) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1