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