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