The bald eagle is not cold. The dog is cold. The lion is round. Cold things are blue. If something is red then it visits the dog. If the lion needs the dog and the lion is not round then the lion eats the bald eagle. If the lion eats the bald eagle and the lion does not need the dog then the dog does not need the lion. If the lion visits the dog and the lion does not need the bald eagle then the bald eagle is not round. If something visits the dog then it does not eat the lion. All red things are not cold. If something eats the lion then it is cold.
The bald eagle is not cold.
("bald eagle" "is" "cold" "-")
The dog is cold.
("dog" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is red then it visits the dog.
((("something" "is" "red" "+")) -> ("something" "visits" "dog" "+"))
If the lion needs the dog and the lion is not round then the lion eats the bald eagle.
((("lion" "needs" "dog" "+") ("lion" "is" "round" "~")) -> ("lion" "eats" "bald eagle" "+"))
If the lion eats the bald eagle and the lion does not need the dog then the dog does not need the lion.
((("lion" "eats" "bald eagle" "+") ("lion" "needs" "dog" "~")) -> ("dog" "needs" "lion" "-"))
If the lion visits the dog and the lion does not need the bald eagle then the bald eagle is not round.
((("lion" "visits" "dog" "+") ("lion" "needs" "bald eagle" "~")) -> ("bald eagle" "is" "round" "-"))
If something visits the dog then it does not eat the lion.
((("something" "visits" "dog" "+")) -> ("something" "eats" "lion" "-"))
All red things are not cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "-"))
If something eats the lion then it is cold.
((("something" "eats" "lion" "+")) -> ("something" "is" "cold" "+"))
The bald eagle is not cold.
True
1
proof
[(triple1)]
("bald eagle" "is" "cold" "-")
triple1
The lion is not round.
False
1
inv-proof
[(triple3)]
("lion" "is" "round" "-")
triple3
The dog is blue.
True
2
proof
[(((triple2) -> rule1))]
("dog" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion does not eat the bald eagle.
Unknown
inv-rconc
[@1: The lion eats the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "bald eagle" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("lion" "is" "blue" "+")
The dog does not visit the bald eagle.
Unknown
inv-random
[@0: The dog visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bald eagle" "-")
The lion visits the bald eagle.
Unknown
random
[@0: The lion visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bald eagle" "+")
@0: The bald eagle is not cold.[(triple1)] The dog is cold.[(triple2)] The lion is round.[(triple3)] @1: The dog is blue.[(((triple2) -> rule1))]
The bald eagle is not cold.
("bald eagle" "is" "cold" "-")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1