The bald eagle is kind. The cat sees the bald eagle. The lion needs the bald eagle. If something is nice then it likes the cat. If something likes the cat and the cat is cold then the cat likes the lion. If the cat sees the bald eagle then the cat sees the lion. If the lion likes the bald eagle and the lion needs the bald eagle then the bald eagle likes the cat. If something likes the lion and the lion sees the cat then it needs the cat. If something needs the lion and the lion is nice then it needs the bald eagle.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
If something is nice then it likes the cat.
((("something" "is" "nice" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cat and the cat is cold then the cat likes the lion.
((("something" "likes" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "likes" "lion" "+"))
If the cat sees the bald eagle then the cat sees the lion.
((("cat" "sees" "bald eagle" "+")) -> ("cat" "sees" "lion" "+"))
If the lion likes the bald eagle and the lion needs the bald eagle then the bald eagle likes the cat.
((("lion" "likes" "bald eagle" "+") ("lion" "needs" "bald eagle" "+")) -> ("bald eagle" "likes" "cat" "+"))
If something likes the lion and the lion sees the cat then it needs the cat.
((("something" "likes" "lion" "+") ("lion" "sees" "cat" "+")) -> ("something" "needs" "cat" "+"))
If something needs the lion and the lion is nice then it needs the bald eagle.
((("something" "needs" "lion" "+") ("lion" "is" "nice" "+")) -> ("something" "needs" "bald eagle" "+"))
The bald eagle is kind.
True
1
proof
[(triple1)]
("bald eagle" "is" "kind" "+")
triple1
The cat does not see the bald eagle.
False
1
inv-proof
[(triple2)]
("cat" "sees" "bald eagle" "-")
triple2
The cat sees the lion.
True
2
proof
[(((triple2) -> rule3))]
("cat" "sees" "lion" "+")
((triple2) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat does not see the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "sees" "lion" "-")
((triple2) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "cat" "-")
The bald eagle needs the bald eagle.
Unknown
rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The bald eagle sees the cat.
Unknown
random
[@0: The bald eagle sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "cat" "+")
@0: The bald eagle is kind.[(triple1)] The cat sees the bald eagle.[(triple2)] The lion needs the bald eagle.[(triple3)] @1: The cat sees the lion.[(((triple2) -> rule3))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple2) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1